Built . It shows the files as they were then (ages and “working now” follow your clock). tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.

Machines / #31

`1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB`

#31local proof 17Claimed by someone elseBell eats counterbbchallenge ↗Explorer parent: #30

How we proved it never halts

#30's proof, from a different start

#30 keeps a binary counter fed by a marker that bounces through a run of budget blocks. Each epoch begins by tidying a messy leftover in the counter, and #30's proof shows that the tidying costs only about the square root of the budget, so the budget never runs out mid-cleanup. This machine is #30's table with the state letters renamed and no mirror, so its tape looks the same: 110 110 … 110 0 011 011 … 011 (used blocks, a 0 marker, budget blocks), then the head and the counter.

What differs is the start. The renaming makes this machine's first state #30's second one, so from the blank tape it runs #30's rules from a different opening and passes through a different sequence of epochs. After 55 steps it reaches a tidy epoch start with budget 3.

From there 691 epochs are computed exactly, until the budget reaches 17,712 and the condition that #30's proof carries from epoch to epoch holds. After that, #30's argument carries it forever, so the missing table entry (#30's, renamed) is never reached. This run only merges with #30's own at epoch 795, a fact the proof does not need.

The Rocq proof is #30's with the state names changed in its statements, so no transfer step is needed. New are the 55-step opening by verified simulation, the 691-epoch computation and the check that #30's condition holds at its end.

#17local proof number

1,755lines of Rocq

14 sto compile

6/6automatic checks

Claimed by someone else

We proved this machine locally, but our proof was still unsubmitted when we found it already covered upstream.

Submit completed proofs early. A local proof does not secure an upstream claim.

Upstream proof ↗ · Recorded timeline

What the timing evidence establishes

This describes upstream credit, not who first discovered the mathematics. The records do not establish adoption of our proof, first public push time, or whether an earlier submission would have secured credit.

Overview

In one sentence

Kill #30's table renamed (no mirror), started in #30's B: same rules; Inv reached after 691 epochs

Submitted mechanism The parent's table, from another start. Rename the parent's states A, B, C, D, E, F to E, A, B, C, D, F (no mirror) and you get this table, all 12 entries. The machine starts in A, which is the parent's B, so it runs the parent's table from 0^inf B> 0^inf: a different orbit of the same epoch map. (submission/README.md, Mechanism)

Upstream: The blank-start machine never halts: PR_BEC.v.TM2 ↗. We also have a local proof. This upstream addition is separate from our merged submissions; adoption credit is not established.
Rocq proof: check_kill PASS · first Oct 11 00:31
1,755 lines · 88 KB .v · compile 14.3 s · coqchk pass · 0 axioms · PASS Oct 11 00:31 · from #30
· the .v file
Automatic review: 6 of 6 checks passtemplate: #30's kill file (kill 15) (twin: parent kill's .v) · details in Proof →
Class: Bell eats counterours: Bell eats counter (sheet) · ours adds: partial eat with residue: kill #30's table, started in #30's B · high confidence
On the list: not on BB6_holdouts_663.txt (line 590 of the previous list) · historical 740 line 590
#31eqv ×1sim 1e15
Derived from: 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC#30 Kill claimed

Mechanism

What to check here: the pictures show the mechanism that the rule table describes.

How it works: 3 notes

sigma = A->E, B->A, C->B, D->C, E->D, F->F maps #30's table onto this one (12/12 cells), so #30's hub (110)^a 0 (011)^b B> X, local pass, eats and nested D6 sub-epochs apply; blank reaches K(1,3,1) at step 55.
#30's Rocq model from K(1,3,1): 691 epochs to N = 17,712, where #30's Inv holds (k = 11); model = TM on all 518 left records to 1e11; #30's Lemma D checks pass to N = 400,035.
Sibling #7 (740 line 381: same table mirrored, started in #30's E): the model matches it from step 1,059 (K(1,17,1)), and Inv holds after 687 epochs.

Figures for Checkpoint A

Fig 1 · bbchallenge default view, 10,000 steps
The site's view. Compare with kill #30's card: diagonal stripes inside the bell, busy right edge.

Fig 2 · Epochs: marker diagonals and the counterQ1
Rows are hub visits (B moving right). Follow one down-right diagonal; compare with Fig 2 of #30's card (C there).

Fig 3 · From blank to the first hub, 60 stepsQ2
One row per step. Find the leftmost green-then-magenta cells, then follow the head right to row 55.

More figures (2)Fig 4–5: Left and right records to 100M steps · Blaze, 10 million steps

Rules (12/12 validated)exact tape rewrites the proof will formalize, each re-checked by simulation

rule	from ⟶ to	cases	steps	checked
S conjugacy	#30 cell (q, r) = w m q' ⟶ W4-1 cell (sigma q, r) = w m sigma(q')	sigma = A->E, B->A, C->B, D->C, E->D, F->F, no mirror; all 12 cells incl. the halt cell	—	✓24/24
I start	0^∞ A> 0^∞ ⟶ 0^∞ 110 0 (011)³ B> 1 0^∞	via the pre-record 0^inf <D 01 001^2 000 1 0^inf at step 41 (left record at 42)	55	✓2/2
Rst restart	0^∞ <D 01 (001)^k 000 Y 0^∞ ⟶ 0^∞ 110 0 (011)^k+1 B> Y 0^∞	k <= 60, Y random words of every kind (#30 Rst)	—	✓400/400
LP local pass	l 011 B> X 0^∞ ⟶ l <E 100 X' 0^∞ (d=0) or l <E 101000 X' 0^∞ (d=1)	(X',d) = #30's lpf X, 18 constructors (corrected 2026-10-11, was 19): a-block -> b-block; b-block -> a-block + carry; tails; 11 001^x -> 01 001^(x-1) or 00 (absorbs); 01 -> 11; 00 -> 10; 10 a-block (D5); 10 b-block (D6); constant end words. Any left context l	—	✓4800/4800
D6 nested bounce	l 011 B> 10 101 (001)^e 000 R 0^∞ ⟶ l <E 100 0 01 (001)^k 000 Y 0^∞	(k,Y) = phif 1 (e+1) R: one bounce runs a whole sub-epoch of R (#30's LP_6); e <= 7, R random G words	—	✓403/403
Phi epoch	l (110)^a 0 (011)^b B> X 0^∞ ⟶ l <D 01 (001)^k 000 Y 0^∞	(k,Y) = #30's phif 1.. a b X: bounces then an eat; a <= 30, b <= 40, X random; includes the b = 1 eats below	—	✓4800/4800
E1 even eat	(110)^a 0 011 B> (001)^e+1 000 R ⟶ (110)^a+2 0 (011)^e+1 B> R	#30's Phi_E1; any rest R	—	✓937/937
E2 odd eat	(110)^a 0 011 B> 101 (001)^e 000 R ⟶ <D 01 (001)^a 000 11 (001)^e+d 000 R'	(R',d) = lpf R (#30's Phi_E2); the residue 11 001^x 000 W seeds the next epoch	—	✓992/992
Tail eats	(110)^a 0 011 B> t 0^∞ ⟶ <D 01 (001)^a+1 000 1 / <D 01 (001)^a 000 Y_t	t = '', 1, 010001, 110001 and the constant end words (#30's Phi_E0, Et1-Et3)	—	✓513/513
O model = TM	K(1,3,1) ⟶ every TM left record 0^∞ <E 101 (001)^k T 0^∞, by the model	518 records (3..520) to step 99,729,345,754, N = 12,698; no halt in 1e11 steps	—	✓518/518
FIN finite part	K(1,3,t1) ⟶ K(1,17712,Y691) with Inv 11	Python mirror of #30's orbit/phif (reproduces #30's fin694 exactly); Y691 = p11 10 (gw 11 blocks, tail t0); first epoch with Inv for any k	691 model epochs	✓1/1
D Lemma D chain	K(1,N,Y) on the orbit ⟶ next epoch: digestion beta <= N - 2 and all #30 D.1-D.7 links	#30's check_proof section D from this start: 11,074 epochs to N = 400,035, ALL PASS (the Rocq inv_step needs none of it)	—	✓11074/11074

Compressed historythe tape as 0^∞ <E 101 (001)^k T 0^∞ at 31 moments: where the rules are read off

0^∞ <E 101 (001)^k T 0^∞

step	`k (left record; next epoch has b = k+1)`	`len T (residue cells)`	`T (residue word)`
42	2	4	1
194	7	4	1
708	9	14	11,000,110,001
1,572	13	14	11,001,000,001
3,142	21	9	110,001
5,912	23	23	1.1·10¹⁹
10,170	34	18	1.1·10¹⁴
16,990	37	33	000110010010010000010...
40,052	63	18	1.1·10¹⁴
90,368	87	23	1.1·10¹⁹
234,068	121	36	000110010000010010000...
775,536	197	32	000110010000010010000...
1,858,170	253	71	000110010010010010001...
3,721,818	341	45	000110010000010010000...
11,211,948	499	92	000110010010010010010...
25,991,366	702	45	000110010001010010000...
51,186,726	879	59	000110010000010010001...
146,224,150	1,267	137	000110010010010010010...
331,882,290	1,741	50	000110010000010010000...
639,194,040	2,147	119	000110010010010010010...
1,406,584,146	2,859	138	000110010010010010010...
2,666,642,786	3,561	152	000110010010010010010...
4,533,948,242	4,303	59	000110010000010010001...
8,297,771,942	5,353	111	000110010010010010010...
13,855,516,484	6,393	155	000110010010010010010...
21,595,475,434	7,454	128	000110010010010010000...
31,793,441,090	8,489	155	000110010010010010010...
44,982,070,286	9,621	209	000110010010010010010...
61,614,014,162	10,711	222	000110010010010010010...
82,168,075,612	11,899	72	000110010001010010000...
99,729,345,754	12,697	173	000110010010010010010...

k (left record; next epoch has b = k+1)last 12,697

len T (residue cells)last 173

T (residue word)last 000110010010010010010...

Template comparisontemplate: applies · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	1RF
B	1LC	0RD
C	---	0LD
D	1LE	0LD
E	1RA	0RF
F	0RE	0LB

file: —
module: —
machine: 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC (11 transitions apart)
diff: none under sigma = EABCDF (A->E, B->A, C->B, D->C, E->D, F->F): all 12 entries equal after renaming, no mirror; the start state differs (#30's B)
note: Template = our kill #30's .v (1,726 lines, check_kill PASS, sha256 93a493f5...0c0). Start-independent: Sections 1-10 and inv_step. New: init c0 -->* K 3 t1 (55 steps), fin691 = orbit 100000 691 3 t1 = Some (17712, Y691), inv691 : Inv 11 17712 Y691. Route: rename A->E, C->B, E->D in the es lemmas (#25/F2 recipe), or keep #30's file as tm30 + Perm/perm_halts (#24 recipe, no flip).

Proof strategy & riskshow the formal proof will go · 3 risks to watch

Delta of kill #30: keep #30's development, add the new start (55 steps to K 3 t1) and a 691-epoch vm_compute finite part to Inv 11 at N = 17,712, then transport by renaming or Perm + perm_halts. Then check_kill; do #7 (same plus flip_halts) alongside.

▲The finite part is 691 vm_compute epochs, the same size as #30's fin694 (about 1 s there); fuel 100000 leaves 66,761 spare.
▲A start lemma from a non-c0 state (conjugacy route) needs solve_initD, not esx (atlas/rocq-notes.md); the rename route uses plain solve_init.
▲Discord #bb6 not searched for this string; once #30 is public others can port it here, so submit #30, W4-1 and #7 together.

Stats & provenance10¹¹ steps simulated · 7,726 cells · the status in full · files

simulated: 10¹¹ steps
tape: 7,726 cells · 4,057 nonzeros
growth: cells/nonzeros at 1e9 (#30: 7,720 / 4,642); left edge +2 cells/epoch; 520 left records to 1e11, k = 12,697 at step 99,729,345,754
status now: check_kill PASS, independently re-verified (status.json, 2026-10-11)
observer's note: Kill #30's table under sigma; every rule validated on this table, the model matches all TM left records to 1e11, and #30's Inv holds after 691 model epochs, so confidence high.
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v

Proof & checks

6/6 automatic checks pass

Kill 17 · Bell eats counter · the kill file 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v: 1755 lines, 219 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (twin: parent kill's .v): #30's kill file (kill 15) · 94% of our lines identical · vs #30: same table, started in #30's B; different orbit

1What is provedCheck: the string, the theorem and every check_kill line are green, and the .v on disk is the one that was checked (same sha256).

Machine

1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB

vs holdout list

✓ byte-exact: the .v literal (L44) == 2026-10-07_778.txt line 626 (41 bytes, via tools/holdouts.py)

Theorem

✓ Lemma nonhalt: ~halts tm c0. L1718

check_kill

✓ PASS · 17/17 checks pass · compile 14.33 s · coqchk pass (63.52 s) · assumptions: 0 (closed) · 2026-10-11 07:31:03 UTC · submission/check_kill.txt

Checked .v

sha256 1d62b3e870e268e0…

✓	1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v	`1d62b3e870e268e0…` = checked
✓	submission/1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v	`1d62b3e870e268e0…` = checked

Status

✓Killed: never halts updated 2026-10-11

✓ args✓ input✓ framework✓ framework_build✓ forbidden✓ structure✓ tm_text✓ theorem_text✓ coq✓ names✓ compile✓ tm_rocq✓ theorem_rocq✓ isolation✓ assumptions✓ coqchk✓ integrity

All 17 check_kill checks with their one-line results

✓	`args`	6x2 machine, framework module Individual62, mode nonhalt
✓	`input`	90476 bytes, 1755 lines, 2012 sentences
✓	`framework`	HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓	`framework_build`	13 needed framework .vo files present and fresh, with native code no older than the .vo
✓	`forbidden`	none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)
✓	`structure`	5 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 44: TM_from_str "1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB" == <tm> (41 bytes)
✓	`theorem_text`	line 1718: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 ([local working file]
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 14.3s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB") c0 with absolute names (in-file and isolated)
✓	`isolation`	only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off
✓	`assumptions`	0 assumption(s), all in the baseline
✓	`coqchk`	coqchk -norec BB6Kill.Candidate ok (63.5s); its context summary lists nothing of the file's own
✓	`integrity`	input sha256 and framework HEAD/cleanliness identical before and after

2Same machine as #30?Check: every row of the table is ✓ under the computed renaming (or the listed differences are what status.json's relation says), the two pictures show the same bands, and the trajectory numbers agree with the claimed relation (a twin keeps a fixed small offset; a sibling's gap grows).

status.json names #30 as the parent (1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC); label: “W4-1”; relation: “sibling of #30: #30's table renamed by sigma (A,B,C,D,E,F -> E,A,B,C,D,F, no mirror), started in #30's state B”. Everything below is computed from the two machine strings, not read from notes.

✓ Identical to #30's table under the renaming A→E, B→A, C→B, D→C, E→D, F→F (#30's state → this machine's), no mirror. This machine starts in #30's state B (#30 itself starts in A). The only such map.

#30	#30's row (read 0, read 1)	σ	predicted row: renamed by σ	this machine's actual row
A	`1RB` `0RF`	→ E	`1RA` `0RF`	`1RA` `0RF`	✓	start of #30
B	`1RC` `1RF`	→ A	`1RB` `1RF`	`1RB` `1RF`	✓	start of this machine
C	`1LD` `0RE`	→ B	`1LC` `0RD`	`1LC` `0RD`	✓
D	`---` `0LE`	→ C	`---` `0LD`	`---` `0LD`	✓
E	`1LA` `0LE`	→ D	`1LE` `0LD`	`1LE` `0LD`	✓
F	`0RA` `0LC`	→ F	`0RE` `0LB`	`0RE` `0LB`	✓

Rows aligned by σ: each of #30's states X sits next to this machine's state σ(X). ✓ = the actual row equals #30's row with every target state renamed by σ; --- (halt) must stay ---. Searched: all 720 renamings × with/without mirror.

default view of 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC — Fig P1 · **bbchallenge default view: #30 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: it starts in #30's state B, not A, so the first steps differ; the numbers below read: different orbit, so expect the same kind of bands, not the same picture.

default view of 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB — Fig P1 · **bbchallenge default view: #30 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: it starts in #30's state B, not A, so the first steps differ; the numbers below read: different orbit, so expect the same kind of bands, not the same picture.

blaze view of 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC — Fig P2 · **Long run, Blaze (speed): #30 and this machine, 100 million steps**
The macro behaviour, identical settings on both sides: each picture is its machine's own visited span stretched to 800 px, so compare the shape and order of the bands, not their absolute width. Speed mode samples one cell per column, so a one-cell shift can swap orange and white inside a band; compare band edges, not colours.

blaze view of 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB — Fig P2 · **Long run, Blaze (speed): #30 and this machine, 100 million steps**
The macro behaviour, identical settings on both sides: each picture is its machine's own visited span stretched to 800 px, so compare the shape and order of the bands, not their absolute width. Speed mode samples one cell per column, so a one-cell shift can swap orange and white inside a band; compare band edges, not colours.

Trajectory numbers, from blank (C core)

○ different orbit: 0.078% wider at 1e9 (7,726 vs 7,720 cells; nonzeros 4,057 vs 4,642); not a fixed offset: the cell gap reaches -31

steps	cells visited (hi − lo + 1)			nonzeros
steps	#30	this	ratio (Δ)	#30	this	ratio (Δ)
1e5	286	297	1.0385 (+11)	157	124	0.7898 (-33)
1e6	661	680	1.0287 (+19)	411	393	0.9562 (-18)
1e7	1,549	1,531	0.9884 (-18)	1,007	991	0.9841 (-16)
1e8	3,430	3,399	0.9910 (-31)	1,734	1,970	1.1361 (+236)
1e9	7,720	7,726	1.0008 (+6)	4,642	4,057	0.8740 (-585)

Each machine from blank in its own start state, sim.py C core. Trajectory twin = cells and nonzeros stay within 16 of the parent's at every checkpoint (a fixed offset from a different start, not a growing gap). Cached in img/vs-parent.json (2026-10-16 10:29 PDT); --force recomputes.

3Where it came fromCheck: the template is the one you expect, and the measured reuse (tiles, the reuse figure, diff) agrees with what the README says was kept and changed (quoted).

twin: parent kill's .v #30's kill file (kill 15) machines/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v · detected from status.json

94%of our lines identical to the template

72changed lines

25added lines (ours only)

10template lines dropped

183 / 32 / 4items identical / adapted / new

What the package README says it reused and changed (submission/README.md line 16, Template and what changed), quoted:

The file is the kill for 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC with σ applied, and that kill is adapted from busycoq's verify/FractalBEC.v, tm10 (it keeps tm10's marker bounce RInc). What changed: the TM string; σ (A→E, C→B, E→D) on the 59 state tokens, all in statements (the Section 1 runs, LPspec, Phispec, K, Rst); init (K 3 t1 for K 8 t2); the finite part (fin691/inv691 for fin694/inv694); and the nonhalt call. Every other proof script is the parent's. One TM literal, no bridge lemma. The file has 1,755 lines, every lemma top level, and imports only Individual62 from busycoq.

Fig P3 · Reuse of the template, line by line and by name

Top two bars: non-blank lines after the TM string is replaced by <TM> and whitespace is collapsed. Bottom bar: our Definitions/Lemmas/… by name.

ours 1526 lines

94% identical · 72 changed · 25 added

template 1511 lines

95% kept verbatim · 10 not in ours

our items 219

183 identical · 32 adapted · 4 new · 4 template-only

identicalchanged / adaptedours only (new)template only

Template part: whole file, lines 26–1726 (leading comment left out). Ours: lines 37–1755 (header comment 1–36 left out). Line diff: Python difflib SequenceMatcher; inside a replaced block, line pairs at least 75% alike count as changed, the rest as removed + added.

Template-only names: B694, Y694, fin694, inv694

Other references found:

adapted from vendor/busycoq/verify/FractalBEC.v (named in 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v line 30)

Side-by-side diff: template (1511 lines) vs ours (1526 lines), 107 lines differ; runs of identical lines and long template-only runs folded

identicalequal once each TM string is <TM>changedours onlytemplate only

template		ours
27	From BusyCoq Require Import Individual62.	38	From BusyCoq Require Import Individual62.
28	Require Import Lia.	39	Require Import Lia.
⋯ 10 identical lines (template 29–42, ours 40–53)
43	(* Left sides are written nearest-cell-first (<[...] reverses a literal). *)	54	(* Left sides are written nearest-cell-first (<[...] reverses a literal). *)
44	(* ===================================================================== *)	55	(* ===================================================================== *)
46	(* LP0: 011 C> 0 r -> <A 100 1 r *)	57	(* LP0: 011 B> 0 r -> <E 100 1 r *)
47	Lemma LP0 l r : l <* <[0;1;1] {{C}}> [0] > r -->+ l <{{A}} [1;0;0;1] > r.	58	Lemma LP0 l r : l <* <[0;1;1] {{B}}> [0] > r -->+ l <{{E}} [1;0;0;1] > r.
48	Proof. es. Qed.	59	Proof. es. Qed.
50	Lemma LP0z l : l <* <[0;1;1] {{C}}> 0inf -->+ l <{{A}} [1;0;0;1] *> 0inf.	61	Lemma LP0z l : l <* <[0;1;1] {{B}}> 0inf -->+ l <{{E}} [1;0;0;1] *> 0inf.
51	Proof. es. Qed.	62	Proof. es. Qed.
53	(* LP11: 011 C> 110 r -> <A 101 000 r *)	64	(* LP11: 011 B> 110 r -> <E 101 000 r *)
54	Lemma LP11 l r : l <* <[0;1;1] {{C}}> [1;1;0] > r -->+ l <{{A}} [1;0;1;0;0;0] > r.	65	Lemma LP11 l r : l <* <[0;1;1] {{B}}> [1;1;0] > r -->+ l <{{E}} [1;0;1;0;0;0] > r.
55	Proof. es. Qed.	66	Proof. es. Qed.
57	(* LPC (carry), right pass: 011 C> 101 (001)^e 000 r -> 011 111 (011)^e 011 C> r *)	68	(* LPC (carry), right pass: 011 B> 101 (001)^e 000 r -> 011 111 (011)^e 011 B> r *)
58	Lemma LPCr l e r : l <* <[0;1;1] {{C}}> [1;0;1] > [0;0;1]^^e > [0;0;0] *> r -->+	69	Lemma LPCr l e r : l <* <[0;1;1] {{B}}> [1;0;1] > [0;0;1]^^e > [0;0;0] *> r -->+
59	l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <* <[0;1;1] {{C}}> r.	70	l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <* <[0;1;1] {{B}}> r.
60	Proof. es. Qed.	71	Proof. es. Qed.
62	(* LPC, left pass after an exit with d = 0 / d = 1 *)	73	(* LPC, left pass after an exit with d = 0 / d = 1 *)
63	Lemma LPCl0 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;0] *> r -->+	74	Lemma LPCl0 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{E}} [1;0;0] *> r -->+
64	l <{{A}} [1;0;0;0;0;1] > [0;0;1]^^e > [0;0;0] *> r.	75	l <{{E}} [1;0;0;0;0;1] > [0;0;1]^^e > [0;0;0] *> r.
65	Proof. es. Qed.	76	Proof. es. Qed.
67	Lemma LPCl1 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;1;0;0;0] *> r -->+	78	Lemma LPCl1 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{E}} [1;0;1;0;0;0] *> r -->+
68	l <{{A}} [1;0;0;0;0;1] > [0;0;1]^^(S e) > [0;0;0] *> r.	79	l <{{E}} [1;0;0;0;0;1] > [0;0;1]^^(S e) > [0;0;0] *> r.
69	Proof. es. Qed.	80	Proof. es. Qed.
71	(* LP5 (D5): 011 C> 10 001 (001)^e 000 r -> 011 11 (011)^(e+1) 011 C> r, and back *)	82	(* LP5 (D5): 011 B> 10 001 (001)^e 000 r -> 011 11 (011)^(e+1) 011 B> r, and back *)
72	Lemma LP5r l e r : l <* <[0;1;1] {{C}}> [1;0;0;0;1] > [0;0;1]^^e > [0;0;0] *> r -->+	83	Lemma LP5r l e r : l <* <[0;1;1] {{B}}> [1;0;0;0;1] > [0;0;1]^^e > [0;0;0] *> r -->+
73	l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <* <[0;1;1] {{C}}> r.	84	l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <* <[0;1;1] {{B}}> r.
74	Proof. es. Qed.	85	Proof. es. Qed.
76	Lemma LP5l0 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{A}} [1;0;0] *> r -->+	87	Lemma LP5l0 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{E}} [1;0;0] *> r -->+
77	l <{{A}} [1;0;0;0;1] > [0;0;1]^^(S e) > [0;0;0] *> r.	88	l <{{E}} [1;0;0;0;1] > [0;0;1]^^(S e) > [0;0;0] *> r.
78	Proof. es. Qed.	89	Proof. es. Qed.
80	Lemma LP5l1 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{A}} [1;0;1;0;0;0] *> r -->+	91	Lemma LP5l1 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{E}} [1;0;1;0;0;0] *> r -->+
81	l <{{A}} [1;0;0;0;1] > [0;0;1]^^(S (S e)) > [0;0;0] *> r.	92	l <{{E}} [1;0;0;0;1] > [0;0;1]^^(S (S e)) > [0;0;0] *> r.
82	Proof. es. Qed.	93	Proof. es. Qed.
84	(* LP6 (D6), right pass: builds the sub-hub 011 1 . 110 0 (011)^(e+1) C> r *)	95	(* LP6 (D6), right pass: builds the sub-hub 011 1 . 110 0 (011)^(e+1) B> r *)
85	Lemma LP6r l e r : l <* <[0;1;1] {{C}}> [1;0;1;0;1] > [0;0;1]^^e > [0;0;0] *> r -->+	96	Lemma LP6r l e r : l <* <[0;1;1] {{B}}> [1;0;1;0;1] > [0;0;1]^^e > [0;0;0] *> r -->+
86	l <* <[0;1;1;1] <* <[1;1;0] <* [0] <* <[0;1;1]^^(S e) {{C}}> r.	97	l <* <[0;1;1;1] <* <[1;1;0] <* [0] <* <[0;1;1]^^(S e) {{B}}> r.
87	Proof. es. Qed.	98	Proof. es. Qed.
89	(* W10, the D6 exit: 011 E> 1 r -> <A 100 0 r *)	100	(* W10, the D6 exit: 011 D> 1 r -> <E 100 0 r *)
90	Lemma W10 l r : l <* <[0;1;1;1] <{{E}} r -->+ l <{{A}} [1;0;0;0] *> r.	101	Lemma W10 l r : l <* <[0;1;1;1] <{{D}} r -->+ l <{{E}} [1;0;0;0] *> r.
91	Proof. es. Qed.	102	Proof. es. Qed.
93	(* RP0 / RP1: the region pass (FractalBEC's RInc) *)	104	(* RP0 / RP1: the region pass (FractalBEC's RInc) *)
94	Lemma RP0 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{A}} [1;0;0] *> r -->+	105	Lemma RP0 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{E}} [1;0;0] *> r -->+
95	l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S n) {{C}}> r.	106	l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S n) {{B}}> r.
96	Proof. es. Qed.	107	Proof. es. Qed.
98	Lemma RP1 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{A}} [1;0;1;0;0;0] *> r -->+	109	Lemma RP1 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{E}} [1;0;1;0;0;0] *> r -->+
99	l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S (S n)) {{C}}> r.	110	l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S (S n)) {{B}}> r.
100	Proof. es. Qed.	111	Proof. es. Qed.
102	(* Eats at b = 1 *)	113	(* Eats at b = 1 *)
103	Lemma E1r l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [0;0;1]^^(S e) > [0;0;0] > r -->+	114	Lemma E1r l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> [0;0;1]^^(S e) > [0;0;0] > r -->+
104	l <* <[1;1;0]^^(S (S a)) <* [0] <* <[0;1;1]^^(S e) {{C}}> r.	115	l <* <[1;1;0]^^(S (S a)) <* [0] <* <[0;1;1]^^(S e) {{B}}> r.
105	Proof. es. Qed.	116	Proof. es. Qed.
107	Lemma E2l0 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;0] *> r -->+	118	Lemma E2l0 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{E}} [1;0;0] *> r -->+
108	l <{{E}} [0;1] > [0;0;1]^^a > [0;0;0;1;1] > [0;0;1]^^e > [0;0;0] *> r.	119	l <{{D}} [0;1] > [0;0;1]^^a > [0;0;0;1;1] > [0;0;1]^^e > [0;0;0] *> r.
109	Proof. es. Qed.	120	Proof. es. Qed.
111	Lemma E2l1 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;1;0;0;0] *> r -->+	122	Lemma E2l1 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{E}} [1;0;1;0;0;0] *> r -->+
112	l <{{E}} [0;1] > [0;0;1]^^a > [0;0;0;1;1] > [0;0;1]^^(S e) > [0;0;0] *> r.	123	l <{{D}} [0;1] > [0;0;1]^^a > [0;0;0;1;1] > [0;0;1]^^(S e) > [0;0;0] *> r.
113	Proof. es. Qed.	124	Proof. es. Qed.
115	Lemma Et0 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> 0inf -->+	126	Lemma Et0 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> 0inf -->+
116	l <{{E}} [0;1] > [0;0;1]^^(S a) > [0;0;0;1] *> 0inf.	127	l <{{D}} [0;1] > [0;0;1]^^(S a) > [0;0;0;1] *> 0inf.
117	Proof. es. Qed.	128	Proof. es. Qed.
119	Lemma Et1 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [1] *> 0inf -->+	130	Lemma Et1 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> [1] *> 0inf -->+
120	l <{{E}} [0;1] > [0;0;1]^^a > [0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.	131	l <{{D}} [0;1] > [0;0;1]^^a > [0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.
121	Proof. es. Qed.	132	Proof. es. Qed.
123	Lemma Et2 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [0;1;0;0;0;1] *> 0inf -->+	134	Lemma Et2 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> [0;1;0;0;0;1] *> 0inf -->+
124	l <{{E}} [0;1] > [0;0;1]^^a > [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.	135	l <{{D}} [0;1] > [0;0;1]^^a > [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
125	Proof. es. Qed.	136	Proof. es. Qed.
127	Lemma Et3 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [1;1;0;0;0;1] *> 0inf -->+	138	Lemma Et3 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> [1;1;0;0;0;1] *> 0inf -->+
128	l <* <[1;1;0]^^(S a) <* [0] <* <[0;1;1] {{C}}> [0;0;1] *> 0inf.	139	l <* <[1;1;0]^^(S a) <* [0] <* <[0;1;1] {{B}}> [0;0;1] *> 0inf.
129	Proof. es. Qed.	140	Proof. es. Qed.
131	(* Restart from a pre-record (write-up 3.7, plus the step L' -> L) *)	142	(* Restart from a pre-record (write-up 3.7, plus the step L' -> L) *)
132	Lemma Rst k r : const 0 <{{E}} [0;1] > [0;0;1]^^k > [0;0;0] *> r -->+	143	Lemma Rst k r : const 0 <{{D}} [0;1] > [0;0;1]^^k > [0;0;0] *> r -->+
133	const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^(S k) {{C}}> r.	144	const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^(S k) {{B}}> r.
134	Proof. rewrite (const_unfold _ S0) at 1. es. Qed.	145	Proof. rewrite (const_unfold _ S0) at 1. es. Qed.
136	(* LPT: the constant end words *)	147	(* LPT: the constant end words *)
137	Lemma LPT1 l : l <* <[0;1;1] {{C}}> [1] > 0inf -->+ l <{{A}} [1;0;0;0;1;0;0;0;1] > 0inf.	148	Lemma LPT1 l : l <* <[0;1;1] {{B}}> [1] > 0inf -->+ l <{{E}} [1;0;0;0;1;0;0;0;1] > 0inf.
138	Proof. es. Qed.	149	Proof. es. Qed.
140	Lemma LPT2 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;0;1] *> 0inf -->+	151	Lemma LPT2 l : l <* <[0;1;1] {{B}}> [1;0;0;1;0;0;0;1] *> 0inf -->+
141	l <{{A}} [1;0;0] > [0;1;0;0;1;0;0;0;0;1;0;0;1;0;0;0;1] > 0inf.	152	l <{{E}} [1;0;0] > [0;1;0;0;1;0;0;0;0;1;0;0;1;0;0;0;1] > 0inf.
142	Proof. es. Qed.	153	Proof. es. Qed.
144	Lemma LPT3 l : l <* <[0;1;1] {{C}}> [1;0;1;1;0;0;0;1] *> 0inf -->+	155	Lemma LPT3 l : l <* <[0;1;1] {{B}}> [1;0;1;1;0;0;0;1] *> 0inf -->+
145	l <{{A}} [1;0;0] > [0;0;0;1;0;0;0;0;1;0;0;0;1] > 0inf.	156	l <{{E}} [1;0;0] > [0;0;0;1;0;0;0;0;1;0;0;0;1] > 0inf.
146	Proof. es. Qed.	157	Proof. es. Qed.
148	Lemma LPT4 l : l <* <[0;1;1] {{C}}> [1;0;0;0;0;1;0;0;0;1] *> 0inf -->+	159	Lemma LPT4 l : l <* <[0;1;1] {{B}}> [1;0;0;0;0;1;0;0;0;1] *> 0inf -->+
149	l <{{A}} [1;0;0] > [0;1;0;0;0;0;1;0;0;1;0;0;0;1] > 0inf.	160	l <{{E}} [1;0;0] > [0;1;0;0;0;0;1;0;0;1;0;0;0;1] > 0inf.
150	Proof. es. Qed.	161	Proof. es. Qed.
152	Lemma LPT5 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf -->+	163	Lemma LPT5 l : l <* <[0;1;1] {{B}}> [1;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf -->+
153	l <{{A}} [1;0;0] > [0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] > 0inf.	164	l <{{E}} [1;0;0] > [0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] > 0inf.
154	Proof. es. Qed.	165	Proof. es. Qed.
156	Lemma LPT6 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;1;0;0;0;1] *> 0inf -->+	167	Lemma LPT6 l : l <* <[0;1;1] {{B}}> [1;0;0;1;0;0;1;0;0;0;1] *> 0inf -->+
157	l <{{A}} [1;0;0] > [0;1;0;0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] > 0inf.	168	l <{{E}} [1;0;0] > [0;1;0;0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] > 0inf.
158	Proof. es. Qed.	169	Proof. es. Qed.
160	Lemma z3 : [0;0;0] *> const 0 = const 0.	171	Lemma z3 : [0;0;0] *> const 0 = const 0.
⋯ 26 identical lines (template 161–190, ours 172–201)
192	Definition addb (e : nat) (d : bool) : nat := if d then S e else e.	203	Definition addb (e : nat) (d : bool) : nat := if d then S e else e.
194	(* LP w w' d: the local pass maps w to w', d = true if it absorbs one 011 block.	205	(* LP w w' d: the local pass maps w to w', d = true if it absorbs one 011 block.
195	Phi a b w k y: the epoch map from the hub (110)^a 0 (011)^b C> w to the pre-record	206	Phi a b w k y: the epoch map from the hub (110)^a 0 (011)^b B> w to the pre-record
196	E> . 01 (001)^k 000 y (write-up 3.8). *)	207	<D 01 (001)^k 000 y (write-up 3.8). *)
197	Inductive LP : word -> word -> bool -> Prop :=	208	Inductive LP : word -> word -> bool -> Prop :=
198	\| LP_a e w : LP (blk false e w) (blk true e w) false	209	\| LP_a e w : LP (blk false e w) (blk true e w) false
⋯ 30 identical lines (template 199–230, ours 210–241)
231	if d then [1;0;1;0;0;0] > r else [1;0;0] > r.	242	if d then [1;0;1;0;0;0] > r else [1;0;0] > r.
233	Definition LPspec (w w' : word) (d : bool) : Prop :=	244	Definition LPspec (w w' : word) (d : bool) : Prop :=
234	forall l, l <* <[0;1;1] {{C}}> enc w -->+ l <{{A}} outp d (enc w').	245	forall l, l <* <[0;1;1] {{B}}> enc w -->+ l <{{E}} outp d (enc w').
236	Definition Phispec (a b : nat) (w : word) (k : nat) (y : word) : Prop :=	247	Definition Phispec (a b : nat) (w : word) (k : nat) (y : word) : Prop :=
237	forall l, l <* <[1;1;0]^^a <* [0] <* <[0;1;1]^^b {{C}}> enc w -->+	248	forall l, l <* <[1;1;0]^^a <* [0] <* <[0;1;1]^^b {{B}}> enc w -->+
238	l <{{E}} [0;1] > [0;0;1]^^k > [0;0;0] *> enc y.	249	l <{{D}} [0;1] > [0;0;1]^^k > [0;0;0] *> enc y.
240	Lemma enc_a0 : enc (blk false 0 t0) = [0;0;1] *> const 0.	251	Lemma enc_a0 : enc (blk false 0 t0) = [0;0;1] *> const 0.
241	Proof. cbn [enc]. rewrite z3. reflexivity. Qed.	252	Proof. cbn [enc]. rewrite z3. reflexivity. Qed.
⋯ 68 identical lines (template 243–312, ours 254–323)
313	(* ===================================================================== *)	324	(* ===================================================================== *)
315	Definition K (N : nat) (y : word) : Q * tape :=	326	Definition K (N : nat) (y : word) : Q * tape :=
316	const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^N {{C}}> enc y.	327	const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^N {{B}}> enc y.
318	Lemma epoch_tm N y k y' : Phi 1 N y k y' -> K N y -->+ K (S k) y'.	329	Lemma epoch_tm N y k y' : Phi 1 N y k y' -> K N y -->+ K (S k) y'.
319	Proof.	330	Proof.
⋯ 2 identical lines (template 320–321, ours 331–332)
322	- apply Rst.	333	- apply Rst.
323	Qed.	334	Qed.
325	(* The blank tape reaches L(7, 000 010001) at step 304, then the restart gives K(1,8,t2). *)
		336	(* The blank tape reaches the pre-record 0^inf <D 01 (001)^2 000 1 0^inf at step 41
326	Lemma init : c0 -->* K 8 t2.
		337	(D0 = 1LE: the left record next), then the restart gives K(1,3,t1) at step 55. *)
		338	Lemma init : c0 -->* K 3 t1.
327	Proof. unfold K. cbn. solve_init. Qed.	339	Proof. unfold K. cbn. solve_init. Qed.
329	(* ===================================================================== *)	341	(* ===================================================================== *)
⋯ 1199 identical lines (template 330–1657, ours 342–1669)
1658	apply (next_inv k N n c bsp sp r HG Hs3 Hn HN HL); rewrite ?(MO_zero _ _ _ Hz); unfold Xf, Pf; lia.	1670	apply (next_inv k N n c bsp sp r HG Hs3 Hn HN HL); rewrite ?(MO_zero _ _ _ Hz); unfold Xf, Pf; lia.
1659	Qed.	1671	Qed.
1661	(* ---------- the finite part: the computable model from K(1,8,t2) to epoch 694 ---------- *)	1673	(* ---------- the finite part: the computable model from K(1,3,t1), 691 epochs ---------- *)
1663	Fixpoint orbit (f n N : nat) (y : word) : option (nat * word) :=	1675	Fixpoint orbit (f n N : nat) (y : word) : option (nat * word) :=
1664	match n with	1676	match n with
⋯ 8 identical lines (template 1665–1673, ours 1677–1685)
1674	eapply evstep_trans; [apply progress_evstep, epoch_tm, (proj2 (model_sound f) _ _ _ _ _ E) \| exact (IH _ _ _ _ H)].	1686	eapply evstep_trans; [apply progress_evstep, epoch_tm, (proj2 (model_sound f) _ _ _ _ _ E) \| exact (IH _ _ _ _ H)].
1675	Qed.	1687	Qed.
1677	Definition B694 : blks := [(false, 17); (true, 1); (true, 1); (true, 1); (true, 1);
		1689	Definition B691 : blks := [(false, 10); (false, 6); (true, 1); (false, 1); (true, 1); (false, 1);
1678	(false, 1); (false, 1); (false, 1); (true, 1); (false, 0)].	1690	(true, 1); (false, 1); (false, 1); (true, 1); (false, 0)].
1679	Definition Y694 : word := p11 7 (gw B694 0).	1691	Definition Y691 : word := p11 10 (gw B691 0).
1681	Lemma fin694 : orbit 100000 691 8 t2 = Some (17713, Y694).	1693	Lemma fin691 : orbit 100000 691 3 t1 = Some (17712, Y691).
1682	Proof. vm_compute. reflexivity. Qed.	1694	Proof. vm_compute. reflexivity. Qed.
1684	Lemma inv694 : Inv 10 17713 Y694.	1696	Lemma inv691 : Inv 11 17712 Y691.
1685	Proof.	1697	Proof.
1686	unfold Inv. split; [apply Nat.leb_le; vm_compute; reflexivity\|]. split; [apply Nat.leb_le; vm_compute; reflexivity\|].	1698	unfold Inv. split; [apply Nat.leb_le; vm_compute; reflexivity\|]. split; [apply Nat.leb_le; vm_compute; reflexivity\|].
1687	left. exists 7, B694, 0. split; [reflexivity\|]. split; [lia\|]. split; [cbn; lia\|].	1699	left. exists 10, B691, 0. split; [reflexivity\|]. split; [lia\|]. split; [cbn; lia\|].
1688	split; [\|split]; [apply Nat.leb_le; vm_compute; reflexivity \| apply Nat.leb_le; vm_compute; reflexivity \|].	1700	split; [\|split]; [apply Nat.leb_le; vm_compute; reflexivity \| apply Nat.leb_le; vm_compute; reflexivity \|].
1689	apply Nat.leb_le; vm_compute; reflexivity.	1701	apply Nat.leb_le; vm_compute; reflexivity.
⋯ 14 identical lines (template 1690–1704, ours 1702–1716)
1706	Lemma nonhalt: ~halts tm c0.	1718	Lemma nonhalt: ~halts tm c0.
1707	Proof.	1719	Proof.
1708	apply (nonhalt_from 17713 Y694 (fun N y => exists k, Inv k N y)).	1720	apply (nonhalt_from 17712 Y691 (fun N y => exists k, Inv k N y)).
1709	- eapply evstep_trans; [exact init \| exact (orbit_sound _ _ _ _ _ _ fin694)].	1721	- eapply evstep_trans; [exact init \| exact (orbit_sound _ _ _ _ _ _ fin691)].
1710	- exists 10. exact inv694.	1722	- exists 11. exact inv691.
1711	- intros N y [k Hk]. destruct (inv_step k N y Hk) as (kk & y' & H1 & H2). exists kk, y'. split; [exact H1 \| exact H2].	1723	- intros N y [k Hk]. destruct (inv_step k N y Hk) as (kk & y' & H1 & H2). exists kk, y'. split; [exact H1 \| exact H2].
1712	Qed.	1724	Qed.
1714	(*	1727	(*
1715	0 1	1728	0 1
1716	A 1RB 0RF	1729	A 1RB 1RF
1717	B 1RC 1RF
		1730	B 1LC 0RD
1718	C 1LD 0RE
		1731	C --- 0LD
1719	D --- 0LE
		1732	D 1LE 0LD
1720	E 1LA 0LE
		1733	E 1RA 0RF
1721	F 0RA 0LC	1734	F 0RE 0LB
1723	hub K(a,b,X) = 0^inf (110)^a 0 (011)^b C> X 0^inf
		1735	= 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC with its states renamed A->E, B->A, C->B, D->C, E->D
1724	pre-record L'(k,T) = 0^inf E> 0 01 (001)^k T 0^inf (E0 = 1LA, then the restart)
		1737	words blk d e w = d01 (001)^e 000 w p11 x w = 11 (001)^x 000 w p01 x w = 01 (001)^x 000 w
1725	start c0 -->* K(1,8,010001)
		1738	p00 w = 00 w p10 w = 10 w t0 = '' t1 = 1 t2 = 010001 t3 = 110001
		1739	hub K(a,b,w) = 0^inf (110)^a 0 (011)^b B> w 0^inf (the .v's K N y is K(1,N,y))
		1740	pre-record P(k,y) = 0^inf <D 01 (001)^k 000 y 0^inf (D0 = 1LE: the left record next)
		1741	left record L(k,T) = 0^inf <E 101 (001)^k T 0^inf
		1743	LP (local pass) l 011 B> w -->+ l <E 100 w' (d = 0)
		1744	l 011 B> w -->+ l <E 101 000 w' (d = 1) for LP w w' d (18 constructors)
		1745	Phi (epoch map) l (110)^a 0 (011)^b B> w -->+ l <D 01 (001)^k 000 y for Phi a b w k y
		1746	bounce b >= 2: LP w w' d, then Phi (a+1) (b-1+d) w'
		1747	eats b = 1: a-block -> Phi (a+2) (e+1) rest; b-block -> P(a, p11 (e+d) w');
		1748	t0 -> P(a+1, t1); t1 -> P(a, p01 1 t1); t2 -> P(a, p10 (p00 t2)); t3 -> Phi (a+1) 1 (blk false 0 t0)
		1749	D6 LP (p10 (blk true e w)) (blk false k y) when Phi 1 (e+1) w k y (one bounce runs a sub-epoch)
		1750	Rst P(k,y) -->+ K(1, k+1, y) 3k + 8 steps
		1751	epoch K(1,N,y) -->+ K(1,k+1,y') whenever Phi 1 N y k y'
		1753	start c0 -->(55) K(1,3,t1); 691 epochs (rules only) -->* K(1,17712,Y691); Inv 11 17712 Y691
		1754	invariant Inv k N y (Section 11): every Inv epoch has a Phi successor that is again Inv
1726	*)	1755	*)

4Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.

219 items in 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v (1755 lines): 158 Lemma, 41 Definition, 12 Fixpoint, 7 Inductive, 1 Theorem. Tags against the template: identical = same name and same text once each file's own TM string is <TM> (marked "except the TM string" when that is the only difference); adapted = same name, different text; new = no item of that name in the template part.

#	kind	name	statement (no proof body)	line	vs template
1	Definition	`tm`	Definition tm := Eval compute in (TM_from_str "1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB").	L44	identicalexcept the TM string
2	Lemma	`LP0`	Lemma LP0 l r : l <* <[0;1;1] {{B}}> [0] > r -->+ l <{{E}} [1;0;0;1] > r.	L58	adapted
3	Lemma	`LP0z`	Lemma LP0z l : l <* <[0;1;1] {{B}}> 0inf -->+ l <{{E}} [1;0;0;1] *> 0inf.	L61	adapted
4	Lemma	`LP11`	Lemma LP11 l r : l <* <[0;1;1] {{B}}> [1;1;0] > r -->+ l <{{E}} [1;0;1;0;0;0] > r.	L65	adapted
5	Lemma	`LPCr`	Lemma LPCr l e r : l <* <[0;1;1] {{B}}> [1;0;1] > [0;0;1]^^e > [0;0;0] > r -->+ l < <[0;1;1;1;1;1] <* <[0;1;1]^^e <* <[0;1;1] {{B}}> r.	L69	adapted
6	Lemma	`LPCl0`	Lemma LPCl0 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{E}} [1;0;0] > r -->+ l <{{E}} [1;0;0;0;0;1] > [0;0;1]^^e > [0;0;0] > r.	L74	adapted
7	Lemma	`LPCl1`	Lemma LPCl1 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{E}} [1;0;1;0;0;0] > r -->+ l <{{E}} [1;0;0;0;0;1] > [0;0;1]^^(S e) > [0;0;0] > r.	L78	adapted
8	Lemma	`LP5r`	Lemma LP5r l e r : l <* <[0;1;1] {{B}}> [1;0;0;0;1] > [0;0;1]^^e > [0;0;0] > r -->+ l < <[0;1;1;1;1] <* <[0;1;1]^^(S e) <* <[0;1;1] {{B}}> r.	L83	adapted
9	Lemma	`LP5l0`	Lemma LP5l0 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{E}} [1;0;0] > r -->+ l <{{E}} [1;0;0;0;1] > [0;0;1]^^(S e) > [0;0;0] > r.	L87	adapted
10	Lemma	`LP5l1`	Lemma LP5l1 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{E}} [1;0;1;0;0;0] > r -->+ l <{{E}} [1;0;0;0;1] > [0;0;1]^^(S (S e)) > [0;0;0] > r.	L91	adapted
11	Lemma	`LP6r`	Lemma LP6r l e r : l <* <[0;1;1] {{B}}> [1;0;1;0;1] > [0;0;1]^^e > [0;0;0] > r -->+ l < <[0;1;1;1] <* <[1;1;0] <* [0] <* <[0;1;1]^^(S e) {{B}}> r.	L96	adapted
12	Lemma	`W10`	Lemma W10 l r : l <* <[0;1;1;1] <{{D}} r -->+ l <{{E}} [1;0;0;0] *> r.	L101	adapted
13	Lemma	`RP0`	Lemma RP0 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{E}} [1;0;0] > r -->+ l < <[1;1;0] <* [0] <* <[0;1;1]^^(S n) {{B}}> r.	L105	adapted
14	Lemma	`RP1`	Lemma RP1 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{E}} [1;0;1;0;0;0] > r -->+ l < <[1;1;0] <* [0] <* <[0;1;1]^^(S (S n)) {{B}}> r.	L109	adapted
15	Lemma	`E1r`	Lemma E1r l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> [0;0;1]^^(S e) > [0;0;0] > r -->+ l <* <[1;1;0]^^(S (S a)) <* [0] <* <[0;1;1]^^(S e) {{B}}> r.	L114	adapted
16	Lemma	`E2l0`	Lemma E2l0 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{E}} [1;0;0] > r -->+ l <{{D}} [0;1] > [0;0;1]^^a > [0;0;0;1;1] > [0;0;1]^^e > [0;0;0] > r.	L118	adapted
17	Lemma	`E2l1`	Lemma E2l1 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{E}} [1;0;1;0;0;0] > r -->+ l <{{D}} [0;1] > [0;0;1]^^a > [0;0;0;1;1] > [0;0;1]^^(S e) > [0;0;0] > r.	L122	adapted
18	Lemma	`Et0`	Lemma Et0 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> 0inf -->+ l <{{D}} [0;1] > [0;0;1]^^(S a) > [0;0;0;1] *> 0inf.	L126	adapted
19	Lemma	`Et1`	Lemma Et1 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> [1] > 0inf -->+ l <{{D}} [0;1] > [0;0;1]^^a > [0;0;0;0;1;0;0;1;0;0;0;1] > 0inf.	L130	adapted
20	Lemma	`Et2`	Lemma Et2 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> [0;1;0;0;0;1] > 0inf -->+ l <{{D}} [0;1] > [0;0;1]^^a > [0;0;0;1;0;0;0;0;1;0;0;0;1] > 0inf.	L134	adapted
21	Lemma	`Et3`	Lemma Et3 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{B}}> [1;1;0;0;0;1] > 0inf -->+ l < <[1;1;0]^^(S a) <* [0] <* <[0;1;1] {{B}}> [0;0;1] *> 0inf.	L138	adapted
22	Lemma	`Rst`	Lemma Rst k r : const 0 <{{D}} [0;1] > [0;0;1]^^k > [0;0;0] > r -->+ const 0 < <[1;1;0] <* [0] <* <[0;1;1]^^(S k) {{B}}> r.	L143	adapted
23	Lemma	`LPT1`	Lemma LPT1 l : l <* <[0;1;1] {{B}}> [1] > 0inf -->+ l <{{E}} [1;0;0;0;1;0;0;0;1] > 0inf.	L148	adapted
24	Lemma	`LPT2`	Lemma LPT2 l : l <* <[0;1;1] {{B}}> [1;0;0;1;0;0;0;1] > 0inf -->+ l <{{E}} [1;0;0] > [0;1;0;0;1;0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.	L151	adapted
25	Lemma	`LPT3`	Lemma LPT3 l : l <* <[0;1;1] {{B}}> [1;0;1;1;0;0;0;1] > 0inf -->+ l <{{E}} [1;0;0] > [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.	L155	adapted
26	Lemma	`LPT4`	Lemma LPT4 l : l <* <[0;1;1] {{B}}> [1;0;0;0;0;1;0;0;0;1] > 0inf -->+ l <{{E}} [1;0;0] > [0;1;0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.	L159	adapted
27	Lemma	`LPT5`	Lemma LPT5 l : l <* <[0;1;1] {{B}}> [1;0;0;1;0;0;0;0;1;0;0;0;1] > 0inf -->+ l <{{E}} [1;0;0] > [0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.	L163	adapted
28	Lemma	`LPT6`	Lemma LPT6 l : l <* <[0;1;1] {{B}}> [1;0;0;1;0;0;1;0;0;0;1] > 0inf -->+ l <{{E}} [1;0;0] > [0;1;0;0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.	L167	adapted
29	Lemma	`z3`	Lemma z3 : [0;0;0] *> const 0 = const 0.	L171	identical
30	Inductive	`word`	Inductive word : Type := \| t0 \| t1 \| t2 \| t3 \| blk (d : bool) (e : nat) (w : word) \| p11 (x : nat) (w : word) \| p01 (x : nat) (w : word) \| p00 (w : word) … +1 lines	L180	identical
31	Definition	`dsym`	Definition dsym (d : bool) : Sym := if d then S1 else S0.	L188	identical
32	Fixpoint	`enc`	Fixpoint enc (w : word) : side := match w with \| t0 => const 0 \| t1 => [1] > const 0 \| t2 => [0;1;0;0;0;1] > const 0 \| t3 => [1;1;0;0;0;1] *> const 0 … +6 lines	L190	identical
33	Definition	`addb`	Definition addb (e : nat) (d : bool) : nat := if d then S e else e.	L203	identical
34	Inductive	`LP`	Inductive LP : word -> word -> bool -> Prop := \| LP_a e w : LP (blk false e w) (blk true e w) false \| LP_b e w w' d : LP w w' d -> LP (blk true e w) (blk false (addb e d) w') false \| LP_t0 : LP t0 t1 false \| LP_t1 : LP t1 t2 false \| LP_t2 : LP t2 t3 false … +22 lines	L208	identical
35	Definition	`outp`	Definition outp (d : bool) (r : side) : side := if d then [1;0;1;0;0;0] > r else [1;0;0] > r.	L241	identical
36	Definition	`LPspec`	Definition LPspec (w w' : word) (d : bool) : Prop := forall l, l <* <[0;1;1] {{B}}> enc w -->+ l <{{E}} outp d (enc w').	L244	adapted
37	Definition	`Phispec`	Definition Phispec (a b : nat) (w : word) (k : nat) (y : word) : Prop := forall l, l <* <[1;1;0]^^a <* [0] <* <[0;1;1]^^b {{B}}> enc w -->+ l <{{D}} [0;1] > [0;0;1]^^k > [0;0;0] *> enc y.	L247	adapted
38	Lemma	`enc_a0`	Lemma enc_a0 : enc (blk false 0 t0) = [0;0;1] *> const 0.	L251	identical
39	Theorem	`sound`	Theorem sound : (forall w w' d, LP w w' d -> LPspec w w' d) /\ (forall a b w k y, Phi a b w k y -> Phispec a b w k y).	L258	identical
40	Definition	`K`	Definition K (N : nat) (y : word) : Q * tape := const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^N {{B}}> enc y.	L326	adapted
41	Lemma	`epoch_tm`	Lemma epoch_tm N y k y' : Phi 1 N y k y' -> K N y -->+ K (S k) y'.	L329	identical
42	Lemma	`init`	Lemma init : c0 -->* K 3 t1.	L338	adapted
43	Fixpoint	`lpf`	Fixpoint lpf (n : nat) (w : word) {struct n} : option (word * bool) := match n with \| O => None \| S n' => match w with \| t0 => Some (t1, false) … +58 lines	L345	identical
44	Lemma	`enc_p10t0`	Lemma enc_p10t0 : enc (p10 t0) = enc t1.	L410	identical
45	Lemma	`enc_p10t1`	Lemma enc_p10t1 : enc (p10 t1) = enc (blk true 0 t0).	L413	identical
46	Lemma	`enc_p00t0`	Lemma enc_p00t0 : enc (p00 t0) = enc t0.	L416	identical
47	Lemma	`enc_p00t1`	Lemma enc_p00t1 : enc (p00 t1) = enc (blk false 0 t0).	L419	identical
48	Lemma	`enc_p10p00t0`	Lemma enc_p10p00t0 : enc (p10 (p00 t0)) = enc t1.	L422	identical
49	Lemma	`enc_p10p00t1`	Lemma enc_p10p00t1 : enc (p10 (p00 t1)) = enc (p10 (blk false 0 t0)).	L425	identical
50	Lemma	`model_sound`	Lemma model_sound n : (forall w w' d, lpf n w = Some (w', d) -> LP w w' d) /\ (forall a b w k y, phif n a b w = Some (k, y) -> Phi a b w k y).	L428	identical
51	Definition	`tl_of`	Definition tl_of (s : nat) : word := match s with O => t0 \| 1 => t1 \| 2 => t2 \| _ => t3 end.	L478	identical
52	Fixpoint	`gw`	Fixpoint gw (bs : list (bool * nat)) (s : nat) : word := match bs with [] => tl_of s \| (d, e) :: bs => blk d e (gw bs s) end.	L481	identical
53	Fixpoint	`ginc`	Fixpoint ginc (bs : list (bool * nat)) (s : nat) : list (bool * nat) * nat * bool := match bs with \| [] => match s with O => ([], 1, false) \| 1 => ([], 2, false) \| 2 => ([], 3, false) \| _ => ([(false, 0)], O, true) end \| (false, e) :: bs => ((true, e) :: bs, s, false) \| (true, e) :: bs => let '(bs', s', d) := ginc bs s in ((false, addb e d) :: bs', s', false) … +1 lines	L484	identical
54	Fixpoint	`gval`	Fixpoint gval (bs : list (bool * nat)) (s : nat) : nat := match bs with [] => 4 + s \| (d, _) :: bs => (if d then 1 else 0) + 2 * gval bs s end.	L492	identical
55	Fixpoint	`gsum`	Fixpoint gsum (bs : list (bool * nat)) : nat := match bs with [] => O \| (_, e) :: bs => e + gsum bs end.	L495	identical
56	Lemma	`ginc_LP`	Lemma ginc_LP bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) -> LP (gw bs s) (gw bs' s') d.	L498	identical
57	Lemma	`ginc_val`	Lemma ginc_val bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) -> gval bs' s' = S (gval bs s) /\ s' <= 3 /\ gsum bs' + length bs + (if d then 1 else 0) = gsum bs + length bs' /\ (d = true -> bs = []) /\ length bs <= length bs'.	L506	identical
58	Lemma	`gval_ge`	Lemma gval_ge bs s : 4 <= gval bs s.	L519	identical
59	Lemma	`gval_len`	Lemma gval_len bs s : length bs <= gval bs s.	L522	identical
60	Definition	`Psi`	Definition Psi (bs : list (bool * nat)) (s b : nat) : nat := gval bs s + b + gsum bs - length bs.	L528	identical
61	Definition	`blks`	Definition blks := list (bool * nat).	L536	identical
62	Definition	`b2n`	Definition b2n (d : bool) : nat := if d then 1 else 0.	L537	identical
63	Lemma	`addb_b2n`	Lemma addb_b2n e d : addb e d = e + b2n d.	L538	identical
64	Inductive	`GRes`	Inductive GRes : Type := RE2 (k x : nat) (bs : blks) (s : nat) \| RSp (k : nat) (y : word).	L541	identical
65	Definition	`rk`	Definition rk (r : GRes) : nat := match r with RE2 k _ _ _ => k \| RSp k _ => k end.	L542	identical
66	Definition	`ry`	Definition ry (r : GRes) : word := match r with RE2 _ x bs s => p11 x (gw bs s) \| RSp _ y => y end.	L543	identical
67	Inductive	`GPhi`	Inductive GPhi : nat -> nat -> blks -> nat -> GRes -> Prop := \| GB a b bs s bs' s' d r : ginc bs s = (bs', s', d) -> GPhi (S a) (addb (S b) d) bs' s' r -> GPhi a (S (S b)) bs s r \| GE1 a e bs s r : GPhi (S (S a)) (S e) bs s r -> GPhi a 1 ((false, e) :: bs) s r \| GE2 a e bs s bs' s' d : ginc bs s = (bs', s', d) -> GPhi a 1 ((true, e) :: bs) s (RE2 a (addb e d) bs' s') … +4 lines	L546	identical
68	Lemma	`ginc_s3`	Lemma ginc_s3 bs s bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> s' <= 3.	L557	identical
69	Lemma	`GPhi_sound`	Lemma GPhi_sound a b bs s r : GPhi a b bs s r -> s <= 3 -> Phi a b (gw bs s) (rk r) (ry r).	L560	identical
70	Lemma	`GPhi_s3`	Lemma GPhi_s3 a b bs s r : GPhi a b bs s r -> s <= 3 -> match r with RE2 _ _ _ s2 => s2 <= 3 \| RSp _ y => y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2) end.	L572	identical
71	Lemma	`GPhi_rk`	Lemma GPhi_rk a b bs s r : GPhi a b bs s r -> a + b <= S (rk r).	L579	identical
72	Lemma	`gcount`	Lemma gcount : forall P bs s a b, s <= 3 -> 1 <= b -> Psi bs s b <= P -> exists r, GPhi a b bs s r.	L582	identical
73	Inductive	`LPs`	Inductive LPs : word -> word -> nat -> nat -> Prop := \| LPs_eq w w' : enc w = enc w' -> LPs w w' 0 0 \| LPs_step w w1 w2 d n c : LP w w1 d -> LPs w1 w2 n c -> LPs w w2 (S n) (c + b2n d).	L615	identical
74	Lemma	`LPs_step'`	Lemma LPs_step' w w1 w2 d n c c' : LP w w1 d -> LPs w1 w2 n c -> c' = c + b2n d -> LPs w w2 (S n) c'.	L619	identical
75	Lemma	`LPs_eql`	Lemma LPs_eql w0 w1 w2 n c : enc w0 = enc w1 -> LPs w1 w2 n c -> LPs w0 w2 n c.	L622	identical
76	Lemma	`LPs_trans`	Lemma LPs_trans w1 w2 w3 n c n' c' : LPs w1 w2 n c -> LPs w2 w3 n' c' -> LPs w1 w3 (n + n') (c + c').	L629	identical
77	Lemma	`LPs_cn`	Lemma LPs_cn w w' n c : LPs w w' n c -> c <= n.	L636	identical
78	Lemma	`LPs_hub`	Lemma LPs_hub w w' n c : LPs w w' n c -> forall a B k y, n + 2 <= B + c -> Phi (a + n) (B + c - n) w' k y -> Phi a B w k y.	L639	identical
79	Lemma	`LPs_nest`	Lemma LPs_nest y y' n c : LPs y y' n c -> forall k, LPs (blk false k y) (blk false (k + c) y') (2 * n) 0.	L653	identical
80	Inductive	`DigE`	Inductive DigE : word -> nat -> nat -> blks -> nat -> Prop := \| DE0 : DigE (p10 t0) 0 0 [] 1 \| DE1 : DigE (p10 t1) 0 0 [(true, 0)] 0 \| DE2 : DigE (p10 t2) 13 5 [(false, 0)] 2 \| DE3 : DigE (p10 t3) 7 2 [(false, 0)] 2 \| DEs0 : DigE t1 0 0 [] 1 … +2 lines	L663	identical
81	Lemma	`DigE_sound`	Lemma DigE_sound y n c bs s : DigE y n c bs s -> LPs y (gw bs s) n c.	L675	identical
82	Lemma	`DigE_props`	Lemma DigE_props y n c bs s : DigE y n c bs s -> n <= 13 /\ c <= 5 /\ length bs <= 1 /\ s <= 3 /\ Forall (fun e => e = 0) (map snd bs).	L678	identical
83	Inductive	`DigP`	Inductive DigP : nat -> blks -> nat -> nat -> nat -> blks -> nat -> Prop := \| DP x bs s n c bsp sp : DigT bs s n c bsp sp -> DigP x bs s (2 * x + 2 + n) (S x + c) bsp sp with DigT : blks -> nat -> nat -> nat -> blks -> nat -> Prop := \| DTa e bs s bs' s' d n c bsp sp : ginc bs s = (bs', s', d) -> DigP (S (addb e d)) bs' s' n c bsp sp -> DigT ((false, e) :: bs) s (S (S n)) c bsp sp \| DTb e bs s k x bs2 s2 n c bsp sp : GPhi 1 (S e) bs s (RE2 k x bs2 s2) -> … +4 lines	L685	identical
84	Lemma	`prefix_LPs`	Lemma prefix_LPs x w : LPs (p11 x w) (p10 w) (2 * x + 2) (S x).	L700	identical
85	Lemma	`Dig_sound`	Lemma Dig_sound : (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> LPs (p11 x (gw bs s)) (gw bsp sp) n c) /\ (forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> LPs (p10 (gw bs s)) (gw bsp sp) n c).	L708	identical
86	Lemma	`Dig_sp`	Lemma Dig_sp : (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> sp <= 3) /\ (forall bs s n c bsp sp, DigT bs s n c bsp sp -> sp <= 3).	L728	identical
87	Lemma	`epoch_ord`	Lemma epoch_ord N x bs s n c bsp sp r : s <= 3 -> DigP x bs s n c bsp sp -> n + 2 <= N -> GPhi (1 + n) (N + c - n) bsp sp r -> Phi 1 N (p11 x (gw bs s)) (rk r) (ry r).	L736	identical
88	Lemma	`epoch_spec`	Lemma epoch_spec N y n c bsp sp r : DigE y n c bsp sp -> n + 2 <= N -> GPhi (1 + n) (N + c - n) bsp sp r -> Phi 1 N y (rk r) (ry r).	L744	identical
89	Definition	`exs`	Definition exs (bs : blks) : list nat := map snd bs.	L756	identical
90	Fixpoint	`bumpl`	Fixpoint bumpl (l : list nat) : list nat := match l with [] => [] \| e :: l' => match l' with [] => [S e] \| _ => e :: bumpl l' end end.	L758	identical
91	Lemma	`length_bumpl`	Lemma length_bumpl l : length (bumpl l) = length l.	L761	identical
92	Lemma	`length_exs`	Lemma length_exs bs : length (exs bs) = length bs.	L764	identical
93	Lemma	`ginc_exps`	Lemma ginc_exps bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) -> (exs bs' = exs bs /\ d = false) \/ (exs bs' = bumpl (exs bs) ++ [0] /\ d = match bs with [] => true \| _ => false end).	L768	identical
94	Fixpoint	`qsum`	Fixpoint qsum (l : list nat) : nat := match l with [] => 0 \| e :: l => S e + 2 * qsum l end.	L783	identical
95	Definition	`Qp`	Definition Qp (f : nat) (bs : blks) (s p : nat) : nat := 2 ^ f * (gval bs s + 2 * qsum (exs bs) + p).	L784	identical
96	Definition	`QI`	Definition QI (Q0 f : nat) (bs : blks) (s p : nat) : Prop := Qp f bs s p <= Q0 + 3 * 2 ^ (f + length bs).	L785	identical
97	Lemma	`qsum_app0`	Lemma qsum_app0 l : qsum (l ++ [0]) = qsum l + 2 ^ length l.	L787	identical
98	Lemma	`qsum_bumpl`	Lemma qsum_bumpl l : l <> [] -> 2 * qsum (bumpl l) = 2 * qsum l + 2 ^ length l.	L790	identical
99	Lemma	`gval_lb`	Lemma gval_lb bs s : 4 * 2 ^ length bs <= gval bs s.	L798	identical
100	Lemma	`gval_ub`	Lemma gval_ub bs s : s <= 3 -> gval bs s < 8 * 2 ^ length bs.	L801	identical
101	Lemma	`QI_low`	Lemma QI_low Q0 f bs s p : QI Q0 f bs s p -> 2 ^ (f + length bs) <= Q0.	L804	identical
102	Lemma	`QI_Ps`	Lemma QI_Ps Q0 Ps f bs s p : QI Q0 f bs s p -> Q0 < 2 ^ (Ps + 1) -> f + length bs <= Ps.	L811	identical
103	Lemma	`QI_drop`	Lemma QI_drop Q0 f bs s p : QI Q0 f bs s p -> QI Q0 f bs s 0.	L817	identical
104	Lemma	`QI_cons`	Lemma QI_cons Q0 f dd e bs s p : QI Q0 f ((dd, e) :: bs) s 0 -> p <= S e -> QI Q0 (S f) bs s p.	L820	identical
105	Lemma	`QI_inc`	Lemma QI_inc Q0 f bs s p bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> QI Q0 f bs s (S p) -> QI Q0 f bs' s' (p + b2n d).	L833	identical
106	Lemma	`QI_et3`	Lemma QI_et3 Q0 f : QI Q0 f [] 3 0 -> QI Q0 f [(false, 0)] 0 0.	L860	identical
107	Fixpoint	`wpot`	Fixpoint wpot (v : nat -> nat) (al be f : nat) (l : list nat) : nat := match l with [] => 0 \| e :: l => v f * (al * e + be) + wpot v al be (S f) l end.	L865	identical
108	Fixpoint	`vsum`	Fixpoint vsum (v : nat -> nat) (f m : nat) : nat := match m with 0 => 0 \| S m => v f + vsum v (S f) m end.	L868	identical
109	Definition	`Pot`	Definition Pot (v : nat -> nat) (al be ga Ps f : nat) (l : list nat) : nat := wpot v al be f l + ga * vsum v (f + length l) (Ps - (f + length l)).	L871	identical
110	Definition	`mono`	Definition mono (v : nat -> nat) : Prop := forall i j, i <= j -> v i <= v j.	L874	identical
111	Lemma	`Pot_cons`	Lemma Pot_cons v al be ga Ps f e l : Pot v al be ga Ps f (e :: l) = v f * (al * e + be) + Pot v al be ga Ps (S f) l.	L876	identical
112	Lemma	`wpot_app1`	Lemma wpot_app1 v al be f l x : wpot v al be f (l ++ [x]) = wpot v al be f l + v (f + length l) * (al * x + be).	L880	identical
113	Lemma	`wpot_bumpl`	Lemma wpot_bumpl v al be f l : mono v -> wpot v al be f (bumpl l) <= wpot v al be f l + al * v (f + length l).	L887	identical
114	Lemma	`Pot_ov`	Lemma Pot_ov v al be ga Ps f l : mono v -> al + be + 1 <= ga -> f + length l + 1 <= Ps -> Pot v al be ga Ps f (bumpl l ++ [0]) + v (f + length l) <= Pot v al be ga Ps f l.	L897	identical
115	Lemma	`Pot_inc`	Lemma Pot_inc v al be ga Ps Q0 f bs s p bs' s' d : mono v -> al + be + 1 <= ga -> Q0 < 2 ^ (Ps + 1) -> s <= 3 -> ginc bs s = (bs', s', d) -> QI Q0 f bs s (S p) -> Pot v al be ga Ps f (exs bs') + b2n d * v f <= Pot v al be ga Ps f (exs bs).	L909	identical
116	Lemma	`GPhi_pot`	Lemma GPhi_pot v al be ga Ps Q0 : mono v -> al + be + 1 <= ga -> 1 <= al -> 2 <= be -> Q0 < 2 ^ (Ps + 1) -> forall a b bs s r, GPhi a b bs s r -> s <= 3 -> forall f U, QI Q0 f bs s (b - 1) -> (forall q, f <= q -> U <= v q) -> match r with \| RE2 k x bs2 s2 => exists h, QI Q0 (f + S h) bs2 s2 0 /\ U * k + Pot v al be ga Ps (f + S h) (exs bs2) + v (f + h) * (al * x + be) <= … +3 lines	L924	identical
117	Definition	`w`	Definition w (q : nat) : nat := 2 ^ ((q + 1) / 2).	L993	identical
118	Lemma	`w_mono`	Lemma w_mono : mono w.	L995	identical
119	Lemma	`w_lev`	Lemma w_lev l q : 2 * l <= q -> 2 ^ l <= w q.	L998	identical
120	Lemma	`w_lev1`	Lemma w_lev1 l q : 2 * l + 1 <= q -> 2 ^ S l <= w q.	L1005	identical
121	Lemma	`GPhi_QI`	Lemma GPhi_QI Q0 Ps a b bs s k x bs2 s2 f : Q0 < 2 ^ (Ps + 1) -> GPhi a b bs s (RE2 k x bs2 s2) -> s <= 3 -> QI Q0 f bs s (b - 1) -> exists h, QI Q0 (f + S h) bs2 s2 0.	L1012	identical
122	Lemma	`Dig_cost`	Lemma Dig_cost Q0 Ps : Q0 < 2 ^ (Ps + 1) -> (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 -> 2 ^ l * n <= Pot w 2 8 11 Ps f (exs bs) + 2 ^ l * (2 * x + 2) + 13 * w Ps) /\ (forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 -> 2 ^ l * n <= Pot w 2 8 11 Ps f (exs bs) + 13 * w Ps).	L1021	identical
123	Fixpoint	`MO`	Fixpoint MO (u : nat -> nat) (l : nat) (es : list nat) : nat := match es with [] => 0 \| e :: es => u l * e + MO u (S l) es end.	L1073	identical
124	Definition	`pu`	Definition pu (u : nat -> nat) (l : nat) : nat := match l with 0 => 0 \| S l' => u l' end.	L1076	identical
125	Lemma	`pu_le`	Lemma pu_le u l : mono u -> pu u l <= u l.	L1078	identical
126	Lemma	`MO_zero`	Lemma MO_zero u l es : Forall (fun e => e = 0) es -> MO u l es = 0.	L1081	identical
127	Lemma	`Dig_mass`	Lemma Dig_mass u v Q0 Ps : mono v -> mono u -> (forall l q, 2 * l <= q -> u l <= v q) -> Q0 < 2 ^ (Ps + 1) -> (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 -> pu u l * c + MO u l (exs bsp) <= Pot v 1 3 5 Ps f (exs bs) + pu u l * S x + 6 * v Ps) /\ (forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 -> pu u l * c + MO u l (exs bsp) <= Pot v 1 3 5 Ps f (exs bs) + 6 * v Ps).	L1085	identical
128	Lemma	`Dig_len`	Lemma Dig_len Q0 Ps : Q0 < 2 ^ (Ps + 1) -> (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 -> 2 * (l + length bsp) <= Ps + 3) /\ (forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 -> 2 * (l + length bsp) <= Ps + 3).	L1140	identical
129	Lemma	`pow_gt_self`	Lemma pow_gt_self n : n < 2 ^ (n + 1).	L1165	identical
130	Lemma	`DigE_ex`	Lemma DigE_ex y : y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2) -> exists n c bsp sp, DigE y n c bsp sp.	L1168	identical
131	Lemma	`DigT_exists`	Lemma DigT_exists Q0 : forall D f bs s, s <= 3 -> QI Q0 f bs s 0 -> Q0 + 1 - 2 ^ f <= D -> exists n c bsp sp, DigT bs s n c bsp sp.	L1172	identical
132	Definition	`Rel`	Definition Rel (orig cur : list nat) : Prop := (forall i, S i < length cur -> nth i cur 0 <= nth i orig 0 + 1) /\ (forall i, length cur <= S i -> nth i cur 0 <= nth i orig 0).	L1206	identical
133	Lemma	`nth_bumpl`	Lemma nth_bumpl l i : nth i (bumpl l) 0 = nth i l 0 + (if Nat.eqb (S i) (length l) then 1 else 0).	L1210	identical
134	Lemma	`nth_app0`	Lemma nth_app0 l i : nth i (l ++ [0]) 0 = nth i l 0.	L1219	identical
135	Lemma	`Rel_ov`	Lemma Rel_ov orig l : Rel orig l -> Rel orig (bumpl l ++ [0]).	L1222	identical
136	Lemma	`Rel_inc`	Lemma Rel_inc orig bs s bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> Rel orig (exs bs) -> Rel orig (exs bs').	L1232	identical
137	Lemma	`Rel_tl`	Lemma Rel_tl orig cur : Rel orig cur -> Rel (tl orig) (tl cur).	L1238	identical
138	Lemma	`Rel_refl`	Lemma Rel_refl l : Rel l l.	L1248	identical
139	Lemma	`GPhi_rel`	Lemma GPhi_rel a b bs s r : GPhi a b bs s r -> s <= 3 -> forall orig, Rel orig (exs bs) -> match r with \| RE2 k x bs2 s2 => exists h, Rel (skipn (S h) orig) (exs bs2) /\ x <= nth h orig 0 + 1 \| RSp _ _ => True end.	L1251	identical
140	Lemma	`GPhi_val`	Lemma GPhi_val a b bs s r : GPhi a b bs s r -> s <= 3 -> match r with RE2 k x bs2 s2 => 2 * gval bs2 s2 + a <= gval bs s + k + 2 \| RSp _ _ => True end.	L1277	identical
141	Definition	`v2`	Definition v2 (q : nat) : nat := 2 ^ (q / 2).	L1292	identical
142	Definition	`p2`	Definition p2 (q : nat) : nat := 2 ^ S q.	L1293	identical
143	Definition	`cst1`	Definition cst1 (q : nat) : nat := 1.	L1294	identical
144	Definition	`u1`	Definition u1 (l : nat) : nat := match l with 0 => 0 \| S l' => 2 * w l' end.	L1295	identical
145	Definition	`u2`	Definition u2 (l : nat) : nat := match l with 0 => 0 \| S l' => 2 ^ S l' end.	L1296	identical
146	Lemma	`v2_mono`	Lemma v2_mono : mono v2.	L1298	identical
147	Lemma	`p2_mono`	Lemma p2_mono : mono p2.	L1300	identical
148	Lemma	`cst1_mono`	Lemma cst1_mono : mono cst1.	L1302	identical
149	Lemma	`v2_le_w`	Lemma v2_le_w q : v2 q <= w q.	L1304	identical
150	Lemma	`cst1_le_w`	Lemma cst1_le_w q : cst1 q <= w q.	L1306	identical
151	Lemma	`u1_mono`	Lemma u1_mono : mono u1.	L1309	identical
152	Lemma	`u1_w`	Lemma u1_w l q : 2 * l <= q -> u1 l <= w q.	L1311	identical
153	Lemma	`u2_mono`	Lemma u2_mono : mono u2.	L1322	identical
154	Lemma	`u2_v2`	Lemma u2_v2 l q : 2 * l <= q -> u2 l <= v2 q.	L1324	identical
155	Lemma	`MO_u1`	Lemma MO_u1 l es : MO u1 (S l) es = 2 * wpot w 1 0 l es.	L1331	identical
156	Lemma	`MO_u1_0`	Lemma MO_u1_0 es : MO u1 0 es = 2 * wpot w 1 0 0 (tl es).	L1333	identical
157	Lemma	`MO_u2`	Lemma MO_u2 l es : MO u2 (S l) es = wpot p2 1 0 l es.	L1335	identical
158	Lemma	`MO_u2_0`	Lemma MO_u2_0 es : MO u2 0 es = wpot p2 1 0 0 (tl es).	L1337	identical
159	Lemma	`nth_le_MO`	Lemma nth_le_MO h es : forall l, nth h es 0 <= MO cst1 l es.	L1339	identical
160	Lemma	`wpot_shift`	Lemma wpot_shift v al be f f' l : mono v -> f <= f' -> wpot v al be f l <= wpot v al be f' l.	L1345	identical
161	Lemma	`wpot_drop`	Lemma wpot_drop v al be f h l : wpot v al be (f + h) (skipn h l) <= wpot v al be f l.	L1351	identical
162	Lemma	`wpot_skipn_tl`	Lemma wpot_skipn_tl v h l : mono v -> wpot v 1 0 0 (skipn (S h) l) <= wpot v 1 0 0 (tl l).	L1357	identical
163	Lemma	`wpot_le_nth`	Lemma wpot_le_nth v l1 : mono v -> forall l2 f, (forall i, nth i l1 0 <= nth i l2 0 + 1) -> wpot v 1 0 f l1 <= wpot v 1 0 f l2 + vsum v f (length l1).	L1363	identical
164	Lemma	`Rel_nth`	Lemma Rel_nth orig cur : Rel orig cur -> forall i, nth i cur 0 <= nth i orig 0 + 1.	L1374	identical
165	Lemma	`wpot_split`	Lemma wpot_split v al be f l : wpot v al be f l = wpot v al 0 f l + be * vsum v f (length l).	L1376	identical
166	Lemma	`wpot_scale2`	Lemma wpot_scale2 v f l : wpot v 2 0 f l = 2 * wpot v 1 0 f l.	L1378	identical
167	Lemma	`wpot_le_v`	Lemma wpot_le_v v v' al be f l : (forall q, v q <= v' q) -> wpot v al be f l <= wpot v' al be f l.	L1380	identical
168	Lemma	`vsum_add`	Lemma vsum_add v f m m' : vsum v f (m + m') = vsum v f m + vsum v (f + m) m'.	L1385	identical
169	Lemma	`vsum_mono_m`	Lemma vsum_mono_m v f m m' : m <= m' -> vsum v f m <= vsum v f m'.	L1387	identical
170	Lemma	`vsum_cst1`	Lemma vsum_cst1 f m : vsum cst1 f m = m.	L1389	identical
171	Lemma	`vsum_p2`	Lemma vsum_p2 f m : vsum p2 f m + 2 ^ S f = 2 ^ S (f + m).	L1391	identical
172	Lemma	`wpot_p2_S`	Lemma wpot_p2_S f l : wpot p2 1 0 (S f) l = 2 * wpot p2 1 0 f l.	L1396	identical
173	Lemma	`qsum_p2`	Lemma qsum_p2 l : 2 * qsum l + 2 = 2 ^ S (length l) + wpot p2 1 0 0 l.	L1398	identical
174	Lemma	`wpot_zero`	Lemma wpot_zero v f l : Forall (fun e => e = 0) l -> wpot v 1 0 f l = 0.	L1403	identical
175	Lemma	`Pot_top`	Lemma Pot_top v al be ga Ps l : be <= ga -> length l <= Ps -> Pot v al be ga Ps 0 l <= wpot v al 0 0 l + ga * vsum v 0 Ps.	L1405	identical
176	Definition	`Ws`	Definition Ws (P : nat) : nat := vsum w 0 P.	L1417	identical
177	Definition	`V2s`	Definition V2s (P : nat) : nat := vsum v2 0 P.	L1418	identical
178	Definition	`Pf`	Definition Pf (k : nat) : nat := Nat.max 12 (k + 3).	L1419	identical
179	Definition	`Af`	Definition Af (k : nat) : nat := 5 * Ws (Pf k) + 6 * w (Pf k) + 2 * Ws k.	L1420	identical
180	Definition	`Bf`	Definition Bf (k : nat) : nat := Af k + 5 * V2s (Pf k) + 6 * v2 (Pf k) + 2 ^ (k + 1).	L1421	identical
181	Definition	`Xf`	Definition Xf (k : nat) : nat := Af k + 5 * Pf k + 7.	L1422	identical
182	Definition	`Costf`	Definition Costf (k : nat) : nat := 2 * Xf k + 2 + 2 * Af k + 11 * Ws (Pf k) + 13 * w (Pf k).	L1423	identical
183	Definition	`Nlo`	Definition Nlo (k : nat) : nat := 2 ^ (k + 3) - 8 * 2 ^ ((Pf k + 3) / 2).	L1424	identical
184	Definition	`Nstar`	Definition Nstar : nat := 17705.	L1425	identical
185	Lemma	`Pf_mono`	Lemma Pf_mono k k' : k <= k' -> Pf k <= Pf k'.	L1427	identical
186	Lemma	`Ws_mono`	Lemma Ws_mono P P' : P <= P' -> Ws P <= Ws P'.	L1429	identical
187	Lemma	`V2s_mono`	Lemma V2s_mono P P' : P <= P' -> V2s P <= V2s P'.	L1431	identical
188	Lemma	`Af_mono`	Lemma Af_mono k k' : k <= k' -> Af k <= Af k'.	L1433	identical
189	Lemma	`w_SS`	Lemma w_SS q : w (S (S q)) = 2 * w q.	L1439	identical
190	Lemma	`v2_SS`	Lemma v2_SS q : v2 (S (S q)) = 2 * v2 q.	L1444	identical
191	Lemma	`vsum_SS_w`	Lemma vsum_SS_w f m : vsum w (S (S f)) m = 2 * vsum w f m.	L1449	identical
192	Lemma	`vsum_SS_v2`	Lemma vsum_SS_v2 f m : vsum v2 (S (S f)) m = 2 * vsum v2 f m.	L1451	identical
193	Lemma	`Ws_SS`	Lemma Ws_SS P : Ws (S (S P)) = 2 * Ws P + 3.	L1453	identical
194	Lemma	`V2s_SS`	Lemma V2s_SS P : V2s (S (S P)) = 2 * V2s P + 2.	L1455	identical
195	Lemma	`Pf_big`	Lemma Pf_big k : 9 <= k -> Pf k = k + 3.	L1457	identical
196	Lemma	`Af_SS`	Lemma Af_SS k : 9 <= k -> Af (S (S k)) = 2 * Af k + 21.	L1459	identical
197	Definition	`gB`	Definition gB (k : nat) : nat := Af k + 5 * V2s (k + 3) + 6 * v2 (k + 3).	L1465	identical
198	Lemma	`gB_SS`	Lemma gB_SS k : 9 <= k -> gB (S (S k)) = 2 * gB k + 31.	L1466	identical
199	Lemma	`gB_all`	Lemma gB_all m : gB (10 + 2 * m) + 31 < 7 * 2 ^ (10 + 2 * m) /\ gB (11 + 2 * m) + 31 < 7 * 2 ^ (11 + 2 * m).	L1472	identical
200	Lemma	`gB_ge`	Lemma gB_ge k : 10 <= k -> gB k + 31 < 7 * 2 ^ k.	L1481	identical
201	Lemma	`N1`	Lemma N1 k : 7 * 2 ^ k + Bf k < 2 ^ (Pf k + 1).	L1489	identical
202	Lemma	`Costf_SS`	Lemma Costf_SS k : 9 <= k -> Costf (S (S k)) + 10 * (k + 3) = 2 * Costf k + 121.	L1500	identical
203	Lemma	`Nlo_SS`	Lemma Nlo_SS k : 9 <= k -> Nlo (S (S k)) = 4 * 2 ^ (k + 3) - 16 * 2 ^ ((k + 6) / 2) /\ Nlo k = 2 ^ (k + 3) - 8 * 2 ^ ((k + 6) / 2).	L1506	identical
204	Lemma	`D_all`	Lemma D_all m : Costf (12 + 2 * m) + 123 <= Nlo (12 + 2 * m) /\ Costf (13 + 2 * m) + 123 <= Nlo (13 + 2 * m).	L1518	identical
205	Lemma	`N2`	Lemma N2 k : Costf k + 2 <= Nstar \/ Costf k + 2 <= Nlo k.	L1530	identical
206	Lemma	`Nstar_ge`	Lemma Nstar_ge : 15 <= Nstar.	L1544	identical
207	Definition	`Mw`	Definition Mw (bs : blks) : nat := wpot w 1 0 0 (exs bs).	L1549	identical
208	Definition	`M2`	Definition M2 (bs : blks) : nat := wpot p2 1 0 0 (exs bs).	L1550	identical
209	Definition	`Inv`	Definition Inv (k N : nat) (y : word) : Prop := Nstar <= N /\ Nlo k <= N /\ ((exists x bs s, y = p11 x (gw bs s) /\ s <= 3 /\ length bs <= k /\ Mw bs <= Af k /\ M2 bs <= Bf k /\ x <= Xf k) \/ y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2)).	L1553	identical
210	Lemma	`next_inv`	Lemma next_inv k N n c bsp sp r : GPhi (1 + n) (N + c - n) bsp sp r -> sp <= 3 -> n + 2 <= N -> Nstar <= N -> Nlo k <= N -> MO u1 0 (exs bsp) <= Af k + 5 * Ws (Pf k) + 6 * w (Pf k) -> MO u2 0 (exs bsp) <= Af k + 5 * V2s (Pf k) + 6 * v2 (Pf k) -> MO cst1 0 (exs bsp) + 1 <= Xf k -> 2 * length bsp <= Pf k + 3 -> … +1 lines	L1559	identical
211	Lemma	`inv_step`	Lemma inv_step k N y : Inv k N y -> exists kk y', Phi 1 N y kk y' /\ exists k', Inv k' (S kk) y'.	L1616	identical
212	Fixpoint	`orbit`	Fixpoint orbit (f n N : nat) (y : word) : option (nat * word) := match n with \| O => Some (N, y) \| S n => match phif f 1 N y with Some (k, y') => orbit f n (S k) y' \| None => None end end.	L1675	identical
213	Lemma	`orbit_sound`	Lemma orbit_sound f n : forall N y N' y', orbit f n N y = Some (N', y') -> K N y -->* K N' y'.	L1681	identical
214	Definition	`B691`	Definition B691 : blks := [(false, 10); (false, 6); (true, 1); (false, 1); (true, 1); (false, 1); (true, 1); (false, 1); (false, 1); (true, 1); (false, 0)].	L1689	new
215	Definition	`Y691`	Definition Y691 : word := p11 10 (gw B691 0).	L1691	new
216	Lemma	`fin691`	Lemma fin691 : orbit 100000 691 3 t1 = Some (17712, Y691).	L1693	new
217	Lemma	`inv691`	Lemma inv691 : Inv 11 17712 Y691.	L1696	new
218	Lemma	`nonhalt_from`	Lemma nonhalt_from N0 y0 (P : nat -> word -> Prop) : c0 -->* K N0 y0 -> P N0 y0 -> (forall N y, P N y -> exists k y', Phi 1 N y k y' /\ P (S k) y') -> ~ halts tm c0.	L1704	identical
219	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L1718	adapted

5What a maintainer readsCheck: the rule table below is what the .v proves, and proof.md / README read cleanly for a maintainer.

submission/proof.md · informal proof (submitted copy)
submission/README.md · the package README
submission/discord.md · Discord draft (not posted)
submission/parent-proof.md · the parent's proof, as shipped
proof.md (working copy) · differs from the submitted copy

submission/proof.md line 92: 3. Rules (this machine's names)

Every statement below is an exact transition with universally quantified contexts. A rule never reads the cells of l or of r, except that its end may be "the head arrives on the last cell of l".

3.1 Window and shift rules (the informal proofs of the `es` lemmas) [W]

#	statement	steps
W1	`1 F> 1 → 1 1 F>`	5
W2	`F> 001 → 011 F>`	3
W3	`F> 000 → 011 B>`	3
W4	`B> 101 → 111 F>`	9
W5	`011 D> 0 → D> 0 010`	5
W6	`0 D> 0 → 1 1 F>` (marker turn)	3
W7	`F> 01 → 00 F>`	2
W8	`011 <E 100 → D> 001 000`	4
W9	`011 <E 101 → D> 001 001`	4
W10	`011 D> 1 → <E 100 0` (D6 exit)	4
W11	`B> 10 → 11 F>`	4
S1	`(011)^n D> 0 → D> 0 (010)^n`	5n (ind n: W5, IH)
S2	`F> (001)^n → (011)^n F>`	3n (ind n: W2, IH)
S3	`1 F> 1^n → 1^(n+1) F>`	5n (ind n: W1, IH)

[W] checks each rule in 4 contexts (all-0, all-1 and random l, r), with n = 1..14 for S1–S3 and the step counts as listed.

3.2 The finite runs of the .v's Section 1 [V]

These 27 lemmas are the .v's Section 1. Each is proved by one es (Rst after one const_unfold rewrite). They are the parent's runs with σ applied to the state names: {{A}}→{{E}}, {{C}}→{{B}}, {{E}}→{{D}}. Exponents are symbolic, and l, r are arbitrary. The step counts are exact.

lemma	statement (this machine's names)	steps
LP0	`l 011 B> 0 r → l <E 1001 r`	4
LP0z	`l 011 B> 0^inf → l <E 1001 0^inf`	4
LP11	`l 011 B> 110 r → l <E 101000 r`	8
LPCr	`l 011 B> 101 (001)^e 000 r → l 011111 (011)^e 011 B> r`	3e+12
LPCl0	`l 011111 (011)^e <E 100 r → l <E 100001 (001)^e 000 r`	5e+8
LPCl1	`l 011111 (011)^e <E 101000 r → l <E 100001 (001)^(e+1) 000 r`	5e+8
LP5r	`l 011 B> 10001 (001)^e 000 r → l 01111 (011)^(e+1) 011 B> r`	3e+10
LP5l0	`l 01111 (011)^(e+1) <E 100 r → l <E 10001 (001)^(e+1) 000 r`	5e+12
LP5l1	`l 01111 (011)^(e+1) <E 101000 r → l <E 10001 (001)^(e+2) 000 r`	5e+12
LP6r	`l 011 B> 10101 (001)^e 000 r → l 0111 110 0 (011)^(e+1) B> r`	3e+14
W10	`l 0111 <D r → l <E 1000 r`	4
RP0	`l 0 (011)^(n+1) <E 100 r → l 110 0 (011)^(n+1) B> r`	8n+12
RP1	`l 0 (011)^(n+1) <E 101000 r → l 110 0 (011)^(n+2) B> r`	8n+15
E1r	`l (110)^a 0 011 B> (001)^(e+1) 000 r → l (110)^(a+2) 0 (011)^(e+1) B> r`	3e+14
E2l0	`l (110)^a 0 011111 (011)^e <E 100 r → l <D 01 (001)^a 00011 (001)^e 000 r`	5a+5e+21
E2l1	`l (110)^a 0 011111 (011)^e <E 101000 r → l <D 01 (001)^a 00011 (001)^(e+1) 000 r`	5a+5e+21
Et0	`l (110)^a 0 011 B> 0^inf → l <D 01 (001)^(a+1) 0001 0^inf`	5a+25
Et1	`l (110)^a 0 011 B> 1 0^inf → l <D 01 (001)^a 000010010001 0^inf`	5a+53
Et2	`l (110)^a 0 011 B> 010001 0^inf → l <D 01 (001)^a 0001000010001 0^inf`	5a+45
Et3	`l (110)^a 0 011 B> 110001 0^inf → l (110)^(a+1) 0 011 B> 001 0^inf`	15
Rst	`0^inf <D 01 (001)^k 000 r → 0^inf 110 0 (011)^(k+1) B> r`	3k+8
LPT1	`l 011 B> 1 0^inf → l <E 100010001 0^inf`	18
LPT2	`l 011 B> 10010001 0^inf → l <E 100 01001000010010001 0^inf`	70
LPT3	`l 011 B> 10110001 0^inf → l <E 100 0001000010001 0^inf`	44
LPT4	`l 011 B> 1000010001 0^inf → l <E 100 01000010010001 0^inf`	40
LPT5	`l 011 B> 1001000010001 0^inf → l <E 100 010010001000010001 0^inf`	62
LPT6	`l 011 B> 10010010001 0^inf → l <E 100 010010010001000010001 0^inf`	100

For each lemma, [V] does the following:

It parses the statement from the .v text.
It runs this machine from the left side, for every assignment of the exponents in 0..6 and 4 contexts.
It requires the right side to be reached head-relative, in busycoq's sense, without reading a cell of l or r. The step counts above are fitted and then re-checked on every sample.
As a control, the parent's text (state names not renamed) is run on the parent's table. It passes with the same step counts [V30, V2].

3.3 The local pass LP (the .v's `LP w w' d`; proof = Section 3 `sound`) [LP]

LPspec w w' d: for every l, l 011 B> enc w -->+ l <E outp(d) enc w', with outp(0) = 100 and outp(1) = 101000. LP never reads left of the 011.

constructor	w → w' (d)	proof (runs in order)
LP_a	`blk false e w → blk true e w` (0)	LP0
LP_b	`blk true e w → blk false (e+d) w'` (0), given `LP w w' d`	LPCr(e); LP w in context `l 011111 (011)^e`; LPCl_d(e)
LP_t0 / t1 / t2	`t0 → t1`, `t1 → t2`, `t2 → t3` (0)	LP0z / LPT1 / LP0
LP_t3	`t3 → blk false 0 t0` (1): the overflow	LP11
LP_11S	`p11 (x+1) w → p01 x w` (1)	LP11
LP_110	`p11 0 w → p00 w` (1)	LP11
LP_01, LP_00	`p01 x w → p11 x w`, `p00 w → p10 w` (0)	LP0
LP_5 (D5)	`p10 (blk false e w) → p01 (e+d+1) w'` (0), given `LP w w' d`	LP5r(e); LP w in context `l 01111 (011)^(e+1)`; LP5l_d(e)
LP_6 (D6)	`p10 (blk true e w) → blk false k y` (0), given `Phi 1 (e+1) w k y`	LP6r(e); the sub-epoch `Phi` in context `l 0111`; W10
LP_T2..T6	`p10 t2 → p01 1 (p01 1 t1)`; `p10 t3 → p00 (p01 0 t2)`; `p10 (p00 t2) → p01 0 (p01 1 t1)`; `p10 (p01 0 t2) → p01 1 (p10 (p00 t2))`; `p10 (p01 1 t1) → p01 2 (p10 (p00 t2))` (all 0)	LPT2..LPT6
LP_eq	`LP w2 w' d` and `enc w1 = enc w2` give `LP w1 w' d` (normalization)	—

The D6 sub-epoch works in the context l 0111: the cell left of the sub-hub's (110) holds a 1 where a standalone hub has a 0. Every Phi run reads only cells at or right of its marker. It stops the first time the head reaches the cell left of (110)^a, in state D, so the context does not matter. W10 then reads that 1 and exits.

3.4 The epoch map Phi (the .v's `Phi a b w k y`) [PH]

Phispec a b w k y: for every l, l (110)^a 0 (011)^b B> enc w -->+ l <D 01 (001)^k 000 enc y. The <D reads the last cell of l.

constructor	case	proof
Phi_B (bounce)	`b = b'+2`: given `LP w w' d` and `Phi (a+1) (b'+1+d) w' k y`	LP in context; RP_d(b'); IH
Phi_E1 (a-block eat)	`b = 1`, `w = blk false e w0`: given `Phi (a+2) (e+1) w0 k y`	E1r(a, e); IH
Phi_E2 (b-block eat)	`b = 1`, `w = blk true e w0`, `LP w0 w0' d`: gives `k = a`, `y = p11 (e+d) w0'`	LPCr(e) in context; LP w0; E2l_d(a, e)
Phi_E0	`b = 1`, `w = t0`: gives `k = a+1`, `y = t1`	Et0
Phi_Et1	`b = 1`, `w = t1`: gives `k = a`, `y = p01 1 t1`	Et1
Phi_Et2	`b = 1`, `w = t2`: gives `k = a`, `y = p10 (p00 t2)`	Et2
Phi_Et3	`b = 1`, `w = t3`: given `Phi (a+1) 1 (blk false 0 t0) k y`	Et3; IH (then E1r and Et0)
Phi_eq	normalization	—

Case split at b = 1 (the eats), by the word: a-block → E1, b-block → E2, t0..t3 → E0, Et1, Et2, Et3. Up to enc-equality, also p10 t0 ≡ t1, p10 t1 ≡ b-block, p00 t0 ≡ t0 and p00 t1 ≡ a-block. Every other word at b = 1 has no rule; this is an unsafe eat. Two such eats, K(a, 1, '11' z t3) and K(a, 1, '00' t3), do halt (negative control [N]). Every G word at b = 1 has an eat [PH].

3.5 Restart and one epoch

Rst: P(k, y) -->+ K(1, k+1, y) in 3k + 8 steps, for every y [R]. The first step, D0 = 1LE, gives the left record L(k, 000 y).
epoch_tm (.v Section 4): Phi 1 N y k y' → K(1, N, y) -->+ K(1, k+1, y'). This is sound applied with l = 0^inf, followed by Rst.

3.6 The computable model (.v Section 5)

lpf n w and phif n a b w are fuel-bounded functions that follow the constructors above. model_sound states that every Some result is an LP/Phi derivation. orbit f n N y iterates phif f 1 N y n times with N := k + 1, and orbit_sound turns orbit … = Some (N', y') into K N y -->* K N' y'. An independent implementation of lpf, phif (same cases in the same order, same fuel accounting; the bounce loop is iterative), orbit and Inv gives the numbers of §6. As a control, it reproduces the parent's .v's fin694 literal exactly, and Inv 10 17713 Y694 [M].

6FamilyCheck: related machines are killed together or have a reason to be left open.

6 machines, 3 killed, 3 not. Family links: status.json parent, same transition table with another start (tools/dashboard.py), targeting.md follow-on rows, ledger "= twin" notes. A machine string named in a .v header / proof.md / notes.md is listed but does not make a family.

who	machine	status	relation to this kill
#30 kill 15	`1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC`	✓Killed: never halts	parent link; = #31's table, run from state E; named in #30's notes.md; named in #31's .v header; named in #31's proof.md; named in #31's notes.md · review · compared side by side above · mechanism
#7 kill 16	`1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA`	✓Killed: never halts	= #31's table mirrored, run from state D; named in #31's proof.md; named in #31's notes.md; named in #7's proof.md · review · mechanism
#31 kill 17	`1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB`	✓Killed: never halts	this kill
#10	`1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC`	⚠Cryptid candidate	via #30: targeting: follow-on to #10; named in #30's notes.md · mechanism
#15	`1RB1RF_1LC1RE_---0LD_1LE0LD_1RA0RF_0RE0LB`	⚠Cryptid candidate	targeting: follow-on to #15 · mechanism
#28	`1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA`	⚠Cryptid candidate	via #7: targeting: follow-on to #7 · mechanism

7ChecklistCheck: every ✓ is computed; the two ○ are yours to decide; an amber ! is an optional check that did not finish.

✓
Machine string exact
the .v literal == holdout list line 626 byte for byte
✓
Statement is ~halts tm c0
parsed from the .v and confirmed by check_kill (theorem_text, theorem_rocq)
✓
No axioms beyond baseline
0 assumption(s); tools/assumptions_baseline.txt allows only functional_extensionality_dep
✓
coqchk finished (optional)
coqchk pass in 63.52 s
✓
.v hash matches the checked hash
.v = checked sha256 1d62b3e870e2…; submission/ copy = checked sha256 1d62b3e870e2…
✓
No repo-local paths in the .v
comments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own verify/X.v is fine: none in the .v or the submission/ copy
✓
Public write-up is clean
tools/writeup_lint.py on submission/proof.md: 0 error(s)
○
proof.md reviewed by Dennis (Checkpoint B)
no Checkpoint B note from Dennis found
- notes.md L82: - proof.md: the public delta write-up, rewritten from the working proof.md (sha256 `a36b4c9a…`, untouched). Header (lists, parent, template FractalBEC tm10 via the parent, status, section map) + Summary + §1-§7 = the wor
- notes.md L85: - discord.md: a draft of 1,375 characters plus `<LINK>`. **Not posted.** Its before-pasting list: post #30 first or the three starts as one family (with an optional sentence for that); #7's draft note 3 still calls W4-1
- notes.md L86: - Still open: Dennis's Checkpoint A/B answers (non-blocking; observe.json checkpoint_questions incl. "submit the three together?", proof.md §11).
- proof.md L520: ## 11. Checkpoint B (Dennis)
- proof.md L535: - Not done in this stage: the .v (route A of §8.1 is the next step), and Checkpoint B. The mechanism is #30's with confidence high, so formalization can start without waiting for Checkpoint B.
- proof.md L553: - Dennis's Checkpoint B answers (§11), which do not block.
○
Family posted together?
2 other kill(s) in the family: #30, #7; the Discord draft names 2 of them; 3 member(s) not killed: #10, #15, #28

Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.1 s from the files linked above; nothing in this review is hand-written except the box “How we proved it never halts” (above), which quotes how_proved.md. Re-run: python3 -B tools/killreview.py 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB

Files

machines/<tm>/: 14 entries · raw notes, status, scripts, images

name	size	changed
notes.md ↓	13 KB	2026-10-11 00:35
proof.md ↓	45 KB	2026-10-11 00:19
how_proved.md ↓	1.4 KB	2026-10-14 10:51
status.json ↓	386 B	2026-10-11 00:34
observe.json ↓	14 KB	2026-10-11 00:15
1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v ↓	88 KB	2026-10-11 00:24
data/	19 items	2026-10-11 00:14
img/	15 items	2026-10-16 10:29
rocq/	4 items	2026-10-11 00:26
scripts/	7 items	2026-10-11 00:11
submission/	6 items	2026-10-11 00:34
work/	1 item	2026-10-11 00:38
check_proof.py ↓	50 KB	2026-10-11 00:13
sim_1e9.jsonl ↓	149 B	2026-10-10 23:20

status.json in full

{
 "tm": "1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-11",
 "reason": "check_kill PASS, independently re-verified",
 "label": "W4-1",
 "parent": "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC",
 "relation": "sibling of #30: #30's table renamed by sigma (A,B,C,D,E,F -> E,A,B,C,D,F, no mirror), started in #30's state B"
}

observe.json contract (tools/README-card.md):

1 contract warning

rank: missing

Rendered 2026-10-16 13:29 by tools/machinepage.py from status.json, observe.json (the card), the kill files (tools/killreview.py) and the dashboard records · rebuild: python3 -B tools/card.py 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB (the kill review: python3 -B tools/killreview.py 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB, which also renders a derived kill's same-machine pictures)