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 / #11b

`1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---`

#11blocal proof 14Kill claimedSkelet 1-like Class 2bbchallenge ↗Explorer parent: #11

How we proved it never halts

#11's proof, from a different start

#11 is a binary counter whose digits burn a unit of fuel each time a carry touches them, and its proof is an invariant showing that a digit only ever runs dry where that is harmless. This machine is #11's table with the state letters renamed, started in the state that is #11's B instead of A. Watching it, you see the same kind of counter at the right end of the tape, on a run of its own.

Everything in #11's proof except the start carries over unchanged: the two moves (add 1, and overflow), the invariant, and the proof that every move keeps it. What is new is a 732-step opening. In it the counter loses its digits to merges until none is left, an overflow builds a new one, and at step 732 the tape is a one-digit counter with fuel to spare, a state the invariant covers. From then on #11's argument applies, so this machine never halts.

The Rocq file is #11's with the states renamed and a new opening. It replays the 732 steps, checks the invariant there, and proves the result for this table directly.

#14local proof number

702lines of Rocq

9 sto compile

6/6automatic checks

Overview

In one sentence

Same counter as the parent. At each return to the right edge the tape is K = 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf, with digits (10)^u 00 (01)^v (bit 0) or (10)^u (01)^v (bit 1); d_m is the least significant bit. (submission/README.md, Mechanism)

parent #11; this machine is #11's table renamed by tau = EABCDF (no mirror), started in #11's state B

Upstream: Kill claimed · PR #16merged 2026-10-13 12:26 UTC by ccz181078 · Sk1Class2_v2.v · TM11 · on Submissions →
Rocq proof: check_kill PASS · first Oct 10 16:41
702 lines · 30 KB .v · compile 8.7 s · coqchk pass · 0 axioms · PASS Oct 10 16:41 (re-run Oct 12 18:17)
· the .v file
Automatic review: 6 of 6 checks passtemplate: #11's kill file (kill 3) (twin: parent kill's .v) · details in Proof →
Class: Skelet 1-like Class 2
On the list: not on BB6_holdouts_663.txt (line 511 of the previous list) · historical 740 line 511
eqv ×1sim 1e15
Derived from: 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---#11 Kill claimed

Mechanism

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

Figures

Fig 1 · Carry sweeps from a built counter tapeQ1
Every 10 steps from a built counter tape. Dotted diagonals are head sweeps; compare how deep each one goes.

Fig 2 · Edge records to 300,000 stepsQ2 Q3 viewer ↗
Edge records to 300,000 steps. Look at the dashed vertical walls and each band break (left edge steps out).

Fig 3 · Edge records to 5.1 million stepsQ3
The same view to 5.1M steps. Compare its walls and band breaks with Fig 2.

More figures (2)Fig 4–5: bbchallenge Default view, first 10,000 steps · Blaze view, 10 million steps

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

rule	from ⟶ to	cases	steps	checked
M_k carry (k = trailing 1-bits)	l (10)^u_k 0² (01)^v_k [(10)^u_i (01)^v_i]_{i=k-1..0} (10)^a 0³ (10)^b B> 0^∞ ⟶ l (10)^u_k+1 (01)^v_k-1 [(10)^u_i 0² (01)^v_i-1]_{i=k-1..0} (10)^a+1 0³ (10)^b+2 B> 0^∞	k=0..5 tested; needs v_i>=1 (i<=k), u_i>=1 (i<k), u_k>=0, a>=1, b>=0; v=1 gives a fused (merged) digit	32 + 8a + 8b + 8sum_{i<k} u_i + 4sum_{i<=k} v_i	✓84/84
O overflow (all bits 1)	0^∞ 10 01 [(10)^u_i (01)^v_i]_{i=1..n} (10)^a 0³ (10)^b B> 0^∞ ⟶ 0^∞ 10 01 00 (01)^u_1 [(10)^v_i-1 0² (01)^u_(i+1)]_{i=1..n-1} (10)^v_n (01)^a (10)^b+3 0³ 10 B> 0^∞	n=1..7 tested; needs v_i>=1 (i<n); left edge moves 3 cells; counter restarts at 1	89 - 4n + 8a + 20b + 4sum u_i + 8sum v_i	✓118/118
init (blank tape to first K)	0^∞ A> 0^∞ ⟶ 0^∞ 10 01 (10)³ 01 (10)² 0³ 10 B> 0^∞	twins: start B -> K((1,2);2,1) in 122 steps; start C -> K((1,1);2,1) in 101 steps	142	✓1/1
B sweep right	B> (01)ⁿ ⟶ (10)ⁿ B>	—	2n	✓10/10
D sweep left	(01)ⁿ <D ⟶ <D (10)ⁿ	—	2n	✓10/10

Compressed historythe tape as 0^∞ 10 01 [(10)^u_i (01)^v_i]_{i=1..n} (10)^a 0³ (10)^b B> 0^∞ at 40 moments: where the rules are read off

0^∞ 10 01 [(10)^u_i (01)^v_i]_{i=1..n} (10)^a 0³ (10)^b B> 0^∞

step	`n`	`u_1..u_n`	`v_1..v_n`	`a`	`b`
148,244	4	67,313,163	1,412,848	62	61
196,569	5	115,151,563	6,628,244,832	94	61
323,918	4	68,319,463	1,283,232	126	125
398,427	5	113,113,947	6,728,874,896	158	61
561,920	5	69,319,463,127	104,241,696	126	125
755,701	6	11,173,131,127	682,887,489,664	190	125
1,267,210	4	70,125,190,127	8,166,464	254	253
1,406,407	5	19,197,179	6.91·10¹³	286	61
1,659,148	5	7.11·10¹³	6,125,648,224	126	125
1,917,105	6	17,156,363,255	7.01·10¹⁵	190	125
2,517,862	6	7.21·10¹⁶	48,483,219,264	254	253
3,255,155	7	1.51·10¹³	7.11·10¹⁸	382	253
5,250,968	6	7.31·10¹⁶	244,016,160,128	510	509
6,469,645	7	1.37·10¹²	7.21·10¹⁹	638	253
9,142,178	4	389,382,382,511	3,212,864,384	510	509
9,463,015	5	13,313,171,399	3.88·10¹⁴	542	61
9,966,524	5	3.9·10¹⁴	3.01·10¹²	126	125
10,405,097	6	1.31·10¹³	3.89·10¹⁶	190	125
11,256,622	6	3.91·10¹⁷	2.81·10¹⁴	254	253
12,174,531	7	1.29·10¹⁶	3.9·10¹⁹	382	253
14,421,112	6	3.92·10¹⁷	2.61·10¹⁵	510	509
15,820,405	7	1.27·10¹⁶	3.91·10²⁰	638	253
18,743,706	7	3.93·10²⁰	2.41·10¹⁷	510	509
22,061,823	8	1.25·10¹⁹	3.92·10²³	766	509
30,571,412	7	3.94·10²⁰	2.21·10¹⁸	1,022	1,021
35,551,585	8	1.23·10¹⁹	3.93·10²³	1,278	509
46,376,294	8	3.95·10²⁴	2.01·10²¹	1,022	1,021
59,038,875	9	1.21·10²³	3.94·10²⁶	1,534	1,021
92,220,944	8	3.96·10²⁵	1.81·10²⁰	2,046	2,045
111,528,109	9	1.19·10²²	3.95·10²⁸	2,558	1,021
153,971,602	8	3.97·10²⁶	1.69·10²¹	2,046	2,045
176,217,463	9	1.17·10²²	3.96·10²⁹	2,558	1,021
222,615,948	9	3.98·10³⁰	1.49·10²⁵	2,046	2,045
275,605,721	10	1.15·10²⁶	3.97·10³³	3,070	2,045
411,458,142	8	3.99·10²⁷	1.28·10²⁴	4,094	4,093
447,518,227	9	1.13·10²⁵	3.98·10³¹	4,606	1,021
513,030,920	9	4·10³¹	1.08·10²⁵	2,046	2,045
579,826,725	10	1.11·10²⁹	3.99·10³⁵	3,070	2,045
734,793,354	10	4.01·10³⁵	8.8·10²⁸	4,094	4,093
924,601,615	11	1.98·10²⁹	4·10³⁹	6,142	4,093

nlast 11

u_1..u_nlast 1.98·10²⁹

v_1..v_nlast 4·10³⁹

alast 6,142

blast 4,093

Template comparisonSBCv6.v TM21: partly applies · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	0LE
B	1RC	0RC
C	1LD	0RB
D	1LA	0LE
E	1LD	1LF
F	1LD	---

file: SBCv6.v:3702
module: TM21
machine: 1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE (11 transitions apart)
diff: 10 of 12 transitions differ under the best renaming/mirror (Sk1like_TC_v2 TM1: 9 of 12)
note: Same architecture (LIncs = carries, Ov = re-pairing overflow, BigStep), but TM21's S' configs never recur here (0 real hits in 2e5 steps, all 6 states). Its LWF invariant fails: here digits run out and merge.

Proof & checks

6/6 automatic checks pass

Kill 14 · Skelet 1-like Class 2 · the kill file 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v: 702 lines, 105 items · the package submission/

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

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

1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---

vs holdout list

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

Theorem

✓ Lemma nonhalt: ~halts tm c0. L670

check_kill

✓ PASS · 17/17 checks pass · compile 8.67 s · coqchk pass (1.78 s) · assumptions: 0 (closed) · 2026-10-13 01:17:24 UTC · submission/check_kill.txt

Checked .v

sha256 5a95ad125127adee…

✓	1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v	`5a95ad125127adee…` = checked
✓	submission/1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v	`5a95ad125127adee…` = checked

Status

✓Killed: never halts updated 2026-10-10

✓ 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`	30345 bytes, 702 lines, 756 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`	6 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 26: TM_from_str "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---" == <tm> (41 bytes)
✓	`theorem_text`	line 670: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 ([local working file]
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 8.7s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---") 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 (1.8s); its context summary lists nothing of the file's own
✓	`integrity`	input sha256 and framework HEAD/cleanliness identical before and after

2Same machine as #11?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 #11 as the parent (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---); label: “#11b”; relation: “sibling of #11: #11's table renamed, started in #11's state B”; parent_note: “#11; this machine is #11's table renamed by tau = EABCDF (no mirror), started in #11's state B”. Everything below is computed from the two machine strings, not read from notes.

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

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

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

default view of 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- — Fig P1 · **bbchallenge default view: #11 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: it starts in #11's state B, not A, so the first steps differ; the numbers below read: trajectory twin, so after the start the bands should match line for line.

default view of 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- — Fig P1 · **bbchallenge default view: #11 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: it starts in #11's state B, not A, so the first steps differ; the numbers below read: trajectory twin, so after the start the bands should match line for line.

blaze view of 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- — Fig P2 · **Long run, Blaze (speed): #11 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 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- — Fig P2 · **Long run, Blaze (speed): #11 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)

✓ trajectory twin: within 0.013% at 1e9 (cells +8, nonzeros +5); the offset stays within 8 at every checkpoint instead of growing

steps	cells visited (hi − lo + 1)			nonzeros
steps	#11	this	ratio (Δ)	#11	this	ratio (Δ)
1e5	647	655	1.0124 (+8)	323	325	1.0062 (+2)
1e6	2,125	2,133	1.0038 (+8)	1,060	1,062	1.0019 (+2)
1e7	6,999	7,007	1.0011 (+8)	3,498	3,502	1.0011 (+4)
1e8	24,031	24,039	1.0003 (+8)	12,017	12,020	1.0002 (+3)
1e9	77,685	77,693	1.0001 (+8)	38,836	38,841	1.0001 (+5)

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 #11's kill file (kill 3) machines/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v · detected from status.json

92%of our lines identical to the template

46changed lines

1added lines (ours only)

1template lines dropped

71 / 34 / 0items identical / adapted / new

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

It extends the parent's .v, verify/Skelet1LikeC2_1RB0LE_1RC0RC.v (694 lines), which follows the architecture of busycoq SBCv6.v Module TM21 (carries plus a re-pairing overflow). The changes are those of proof.md §5:

the TM string;
the renaming on every state name: {{B}}->{{A}} (22), {{C}}->{{B}} (18), {{D}}->{{C}} (5), {{E}}->{{D}} (18);
init (732 steps to K [d1 1 10] 8 1, against the parent's 483 to K [d1 1 2] 8 5) and the base in nonhalt, closed by the parent's own tactic line;
the header and the comments.

Every proof script, the three rule specs and the invariant part are the parent's text; no tactic was changed. The file is 702 lines, imports only Individual62 from busycoq, and has one TM_from_str. It is a direct proof on the holdout string, with no Flip/Permute bridge.

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 595 lines

92% identical · 46 changed · 1 added

template 595 lines

92% kept verbatim · 1 not in ours

our items 105

71 identical · 34 adapted · 0 new · 0 template-only

identicalchanged / adaptedours only (new)template only

Template part: whole file, lines 11–694 (leading comment left out). Ours: lines 19–702 (header comment 1–18 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.

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

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

template		ours
12	From BusyCoq Require Import Individual62.	20	From BusyCoq Require Import Individual62.
13	Require Import ZifyNat Lia.	21	Require Import ZifyNat Lia.
⋯ 17 identical lines (template 14–35, ours 22–43)
36	Qed.	44	Qed.
38	(* ---------- one-block lemmas ---------- *)	46	(* ---------- one-block lemmas ---------- *)
39	Lemma S1_1 l r: l <* [] {{B}}> [0;1] > r --> l <* [0;1] <* [] {{B}}> r. Proof. es. Qed.	47	Lemma S1_1 l r: l <* [] {{A}}> [0;1] > r --> l <* [0;1] <* [] {{A}}> r. Proof. es. Qed.
40	Lemma S2_1 l r: l <* [] {{C}}> [1;0] > r --> l <* [1;0] <* [] {{C}}> r. Proof. es. Qed.	48	Lemma S2_1 l r: l <* [] {{B}}> [1;0] > r --> l <* [1;0] <* [] {{B}}> r. Proof. es. Qed.
41	Lemma S3_1 l r: l <* [1;0] <{{D}} [] > r --> l <{{D}} [] > [1;0] > r. Proof. es. Qed.	49	Lemma S3_1 l r: l <* [1;0] <{{C}} [] > r --> l <{{C}} [] > [1;0] > r. Proof. es. Qed.
42	Lemma S4_1 l r: l <* [0;1] <{{E}} [] > r --> l <{{E}} [] > [0;1] > r. Proof. es. Qed.	50	Lemma S4_1 l r: l <* [0;1] <{{D}} [] > r --> l <{{D}} [] > [0;1] > r. Proof. es. Qed.
43	Lemma S6_1 l r: l <* [0] {{B}}> [1;0] > r --> l <* [0;1] <* [0] {{B}}> r. Proof. es. Qed.	51	Lemma S6_1 l r: l <* [0] {{A}}> [1;0] > r --> l <* [0;1] <* [0] {{A}}> r. Proof. es. Qed.
44	Lemma S5_1 l r: l {{C}}> [1;1] > [0;1] > r -->* l <* [0;1] {{C}}> [1;1] *> r. Proof. es. Qed.	52	Lemma S5_1 l r: l {{B}}> [1;1] > [0;1] > r -->* l <* [0;1] {{B}}> [1;1] *> r. Proof. es. Qed.
46	Definition S1 := shift_rule_R _ _ _ _ _ S1_1.	54	Definition S1 := shift_rule_R _ _ _ _ _ S1_1.
47	Definition S2 := shift_rule_R _ _ _ _ _ S2_1.	55	Definition S2 := shift_rule_R _ _ _ _ _ S2_1.
48	Definition S3 := shift_rule_L _ _ _ _ _ S3_1.	56	Definition S3 := shift_rule_L _ _ _ _ _ S3_1.
49	Definition S4 := shift_rule_L _ _ _ _ _ S4_1.	57	Definition S4 := shift_rule_L _ _ _ _ _ S4_1.
50	Definition S6 := shift_rule_R _ _ _ _ _ S6_1.	58	Definition S6 := shift_rule_R _ _ _ _ _ S6_1.
52	Lemma S5 n: forall l r, l {{C}}> [1;1] > [0;1]^^n > r -->* l <* [0;1]^^n {{C}}> [1;1] *> r.	60	Lemma S5 n: forall l r, l {{B}}> [1;1] > [0;1]^^n > r -->* l <* [0;1]^^n {{B}}> [1;1] *> r.
53	Proof.	61	Proof.
54	induction n; intros.	62	induction n; intros.
⋯ 2 identical lines (template 55–56, ours 63–64)
57	Qed.	65	Qed.
59	(* ---------- finite turns ---------- *)	67	(* ---------- finite turns ---------- *)
60	Lemma T1 l: l {{B}}> 0inf -->* l <{{E}} [0;1] *> 0inf. Proof. es. Qed.	68	Lemma T1 l: l {{A}}> 0inf -->* l <{{D}} [0;1] *> 0inf. Proof. es. Qed.
61	Lemma T2 l r: l <* [0;0;0] <{{E}} r -->* l <* [0;0;1] {{B}}> r. Proof. es. Qed.	69	Lemma T2 l r: l <* [0;0;0] <{{D}} r -->* l <* [0;0;1] {{A}}> r. Proof. es. Qed.
62	Lemma T3 l r: l <* [0;0;1] <{{E}} r -->* l <{{E}} [0;1;1] *> r. Proof. es. Qed.	70	Lemma T3 l r: l <* [0;0;1] <{{D}} r -->* l <{{D}} [0;1;1] *> r. Proof. es. Qed.
63	Lemma T4 l r: l <* [1;0] <{{E}} r -->* l <{{D}} [1;1] *> r. Proof. es. Qed.	71	Lemma T4 l r: l <* [1;0] <{{D}} r -->* l <{{C}} [1;1] *> r. Proof. es. Qed.
64	Lemma T5 l r: l <* [0;1] <{{D}} r -->* l <{{E}} [0;1] *> r. Proof. es. Qed.	72	Lemma T5 l r: l <* [0;1] <{{C}} r -->* l <{{D}} [0;1] *> r. Proof. es. Qed.
65	Lemma T6 l r: l <* [0;0] <{{D}} r -->* l <* [0;1] {{C}}> r. Proof. es. Qed.	73	Lemma T6 l r: l <* [0;0] <{{C}} r -->* l <* [0;1] {{B}}> r. Proof. es. Qed.
66	Lemma T7 l r: l {{C}}> [1;1] > r --> l <* [0;0] {{C}}> r. Proof. es. Qed.	74	Lemma T7 l r: l {{B}}> [1;1] > r --> l <* [0;0] {{B}}> r. Proof. es. Qed.
67	Lemma T8 l r: l {{C}}> [1;1;0;1;1] > r --> l <* [0;0;0;0;1] {{B}}> r. Proof. es. Qed.	75	Lemma T8 l r: l {{B}}> [1;1;0;1;1] > r --> l <* [0;0;0;0;1] {{A}}> r. Proof. es. Qed.
68	Lemma T9 r: 0inf <* [1;0;0;1] <{{E}} r -->* 0inf <* [1;0;0;1] <* [0;0;0] {{B}}> r. Proof. es. Qed.	76	Lemma T9 r: 0inf <* [1;0;0;1] <{{D}} r -->* 0inf <* [1;0;0;1] <* [0;0;0] {{A}}> r. Proof. es. Qed.
69	Lemma T10 l r: l {{B}}> [1;1] > r --> l <* [0;0] {{B}}> r. Proof. es. Qed.	77	Lemma T10 l r: l {{A}}> [1;1] > r --> l <* [0;0] {{A}}> r. Proof. es. Qed.
70	Lemma T11 l r: l {{B}}> [0] > r --> l <* [1] {{C}}> r. Proof. es. Qed.	78	Lemma T11 l r: l {{A}}> [0] > r --> l <* [1] {{B}}> r. Proof. es. Qed.
71	Lemma T12 l: l {{C}}> [1;1] > 0inf --> l <{{E}} [0;1;1;0;1] *> 0inf. Proof. es. Qed.	79	Lemma T12 l: l {{B}}> [1;1] > 0inf --> l <{{D}} [0;1;1;0;1] *> 0inf. Proof. es. Qed.
72	Lemma T13 l r: l <* [1;0;1] <{{E}} r -->* l <{{E}} [0;1;1] *> r. Proof. es. Qed.	80	Lemma T13 l r: l <* [1;0;1] <{{D}} r -->* l <{{D}} [0;1;1] *> r. Proof. es. Qed.
73	Lemma T14 l r: l {{B}}> [1;1;0;1] > r --> l <* [0;1;0;0] {{B}}> r. Proof. es. Qed.	81	Lemma T14 l r: l {{A}}> [1;1;0;1] > r --> l <* [0;1;0;0] {{A}}> r. Proof. es. Qed.
76	Lemma p01 n (Y : side) : [0;1]^^n > 0 >> 1 >> Y = 0 >> 1 >> [0;1]^^n > Y.	84	Lemma p01 n (Y : side) : [0;1]^^n > 0 >> 1 >> Y = 0 >> 1 >> [0;1]^^n > Y.
77	Proof. exact (lpow_shift' _ n [0;1] Y). Qed.	85	Proof. exact (lpow_shift' _ n [0;1] Y). Qed.
⋯ 8 identical lines (template 78–86, ours 86–94)
88	(* ---------- digit lemmas ---------- *)	96	(* ---------- digit lemmas ---------- *)
89	Lemma Lb u v l r:	97	Lemma Lb u v l r:
90	l <* [0;1]^^(S u) <* [1;0]^^(S v) <{{E}} r -->*	98	l <* [0;1]^^(S u) <* [1;0]^^(S v) <{{D}} r -->*
91	l <{{E}} [0;1]^^(S u) > [1;0]^^v > [1;1] *> r.	99	l <{{D}} [0;1]^^(S u) > [1;0]^^v > [1;1] *> r.
92	Proof.	100	Proof.
93	follow T4. follow S3. follow T5. follow S4. fin.	101	follow T4. follow S3. follow T5. follow S4. fin.
94	Qed.	102	Qed.
96	Lemma Lf u v l r:	104	Lemma Lf u v l r:
97	l <* [0;1]^^u <* [0;0] <* [1;0]^^(S v) <{{E}} r -->*	105	l <* [0;1]^^u <* [0;0] <* [1;0]^^(S v) <{{D}} r -->*
98	l <* [0;1]^^(S u) <* [1;0]^^v {{C}}> [1;1] *> r.	106	l <* [0;1]^^(S u) <* [1;0]^^v {{B}}> [1;1] *> r.
99	Proof.	107	Proof.
100	follow T4. follow S3. follow T6. follow S2. fin.	108	follow T4. follow S3. follow T6. follow S2. fin.
101	Qed.	109	Qed.
103	Lemma Rb u v l r:	111	Lemma Rb u v l r:
104	l {{C}}> [1;1] > [0;1]^^u > [1;0]^^v > [1;1] > r -->*	112	l {{B}}> [1;1] > [0;1]^^u > [1;0]^^v > [1;1] > r -->*
105	l <* [0;1]^^u <* [0;0] <* [1;0]^^v {{C}}> [1;1] *> r.	113	l <* [0;1]^^u <* [0;0] <* [1;0]^^v {{B}}> [1;1] *> r.
106	Proof.	114	Proof.
107	follow S5. follow T7. follow S2. fin.	115	follow S5. follow T7. follow S2. fin.
108	Qed.	116	Qed.
110	Lemma Ro u v l r:	118	Lemma Ro u v l r:
111	l <* [0;0;0] {{B}}> [0;1]^^(S u) > [1;0]^^v > [1;1] > r -->	119	l <* [0;0;0] {{A}}> [0;1]^^(S u) > [1;0]^^v > [1;1] > r -->
112	l <* [0;0] <* [1;0]^^(S u) <* [0;1]^^v <* [0;0;0] {{B}}> r.	120	l <* [0;0] <* [1;0]^^(S u) <* [0;1]^^v <* [0;0;0] {{A}}> r.
113	Proof.	121	Proof.
114	follow S1.	122	follow S1.
⋯ 2 identical lines (template 115–116, ours 123–124)
117	fin.	125	fin.
118	Qed.	126	Qed.
120	(* right-edge chunk shared by M and O: (10)^a 000 (10)^b B> 0^inf -> <E (01)^a 011 (01)^(b+2) 0^inf *)	128	(* right-edge chunk shared by M and O: (10)^a 000 (10)^b A> 0^inf -> <D (01)^a 011 (01)^(b+2) 0^inf *)
121	Lemma chunkA a b l:	129	Lemma chunkA a b l:
122	l <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{B}}> 0inf -->+	130	l <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{A}}> 0inf -->+
123	l <{{E}} [0;1]^^a > [0;1;1] > [0;1]^^(S (S b)) *> 0inf.	131	l <{{D}} [0;1]^^a > [0;1;1] > [0;1]^^(S (S b)) *> 0inf.
124	Proof. es. Qed.	132	Proof. es. Qed.
126	(* end of M: C> 11 (01)^a 011 (01)^(b+2) 0^inf -> (10)^(a+1) 000 (10)^(b+2) B> 0^inf *)	134	(* end of M: B> 11 (01)^a 011 (01)^(b+2) 0^inf -> (10)^(a+1) 000 (10)^(b+2) A> 0^inf *)
127	Lemma chunkC a b l:	135	Lemma chunkC a b l:
128	l {{C}}> [1;1] > [0;1]^^a > [0;1;1] > [0;1]^^(S (S b)) > 0inf -->*	136	l {{B}}> [1;1] > [0;1]^^a > [0;1;1] > [0;1]^^(S (S b)) > 0inf -->*
129	l <* [0;1]^^(S a) <* [0;0;0] <* [0;1]^^(S (S b)) {{B}}> 0inf.	137	l <* [0;1]^^(S a) <* [0;0;0] <* [0;1]^^(S (S b)) {{A}}> 0inf.
130	Proof.	138	Proof.
131	follow S5. follow T8. follow S1. fin.	139	follow S5. follow T8. follow S1. fin.
132	Qed.	140	Qed.
134	(* end of O: 000 B> (01)^(a+1) 011 (01)^(b+2) 0^inf -> 10 (01)^(a+1) (10)^(b+3) 000 10 B> 0^inf *)	142	(* end of O: 000 A> (01)^(a+1) 011 (01)^(b+2) 0^inf -> 10 (01)^(a+1) (10)^(b+3) 000 10 A> 0^inf *)
135	Lemma chunkO a b l:	143	Lemma chunkO a b l:
136	l <* [0;0;0] {{B}}> [0;1]^^(S a) > [0;1;1] > [0;1]^^(S (S b)) > 0inf -->	144	l <* [0;0;0] {{A}}> [0;1]^^(S a) > [0;1;1] > [0;1]^^(S (S b)) > 0inf -->
137	l <* [0;1] <* [1;0]^^(S a) <* [0;1]^^(S (S (S b))) <* [0;0;0] <* [0;1] {{B}}> 0inf.	145	l <* [0;1] <* [1;0]^^(S a) <* [0;1]^^(S (S (S b))) <* [0;0;0] <* [0;1] {{A}}> 0inf.
138	Proof.	146	Proof.
139	follow S1. follow T11. follow S5. follow T12. follow S4. follow T13. follow S4. follow T2. follow S1. follow S1_1.	147	follow S1. follow T11. follow S5. follow T12. follow S4. follow T13. follow S4. follow T2. follow S1. follow S1_1.
⋯ 18 identical lines (template 140–160, ours 148–168)
162	Definition L0 : side := 0inf <* [1;0;0;1].	170	Definition L0 : side := 0inf <* [1;0;0;1].
164	Definition K (ds : list dg) (a b : nat) : Q * tape :=	172	Definition K (ds : list dg) (a b : nat) : Q * tape :=
165	app_ds L0 ds <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{B}}> 0inf.	173	app_ds L0 ds <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{A}}> 0inf.
167	Definition map1 (os : list (nat*nat)) := map (fun '(u,v) => d1 (S u) (S v)) os.	175	Definition map1 (os : list (nat*nat)) := map (fun '(u,v) => d1 (S u) (S v)) os.
168	Definition map0 (os : list (nat*nat)) := map (fun '(u,v) => d0 (S u) v) os.	176	Definition map0 (os : list (nat*nat)) := map (fun '(u,v) => d0 (S u) v) os.
⋯ 5 identical lines (template 170–174, ours 178–182)
176	Lemma app_ds_app l xs ys : app_ds l (xs ++ ys) = app_ds (app_ds l ys) xs.	184	Lemma app_ds_app l xs ys : app_ds l (xs ++ ys) = app_ds (app_ds l ys) xs.
177	Proof. induction xs; cbn; congruence. Qed.	185	Proof. induction xs; cbn; congruence. Qed.
179	Lemma LbS os: forall l r, app_ds l (map1 os) <{{E}} r -->* l <{{E}} rw os r.	187	Lemma LbS os: forall l r, app_ds l (map1 os) <{{D}} r -->* l <{{D}} rw os r.
180	Proof.	188	Proof.
181	induction os as [\|[u v] t IH]; intros.	189	induction os as [\|[u v] t IH]; intros.
182	- finish.	190	- finish.
183	- cbn [map1 map app_ds dl rw]. follow Lb. apply IH.	191	- cbn [map1 map app_ds dl rw]. follow Lb. apply IH.
184	Qed.	192	Qed.
186	Lemma RbS os: forall l r, l {{C}}> [1;1] > rw os r --> app_ds l (map0 os) {{C}}> [1;1] *> r.	194	Lemma RbS os: forall l r, l {{B}}> [1;1] > rw os r --> app_ds l (map0 os) {{B}}> [1;1] *> r.
187	Proof.	195	Proof.
188	induction os as [\|[u v] t IH]; intros.	196	induction os as [\|[u v] t IH]; intros.
⋯ 6 identical lines (template 189–195, ours 197–203)
196	\| (u,v) :: t => ro_out t l <* [0;0] <* [1;0]^^(S u) <* [0;1]^^v	204	\| (u,v) :: t => ro_out t l <* [0;0] <* [1;0]^^(S u) <* [0;1]^^v
197	end.	205	end.
199	Lemma RoS os: forall l r, l <* [0;0;0] {{B}}> rw os r -->* ro_out os l <* [0;0;0] {{B}}> r.	207	Lemma RoS os: forall l r, l <* [0;0;0] {{A}}> rw os r -->* ro_out os l <* [0;0;0] {{A}}> r.
200	Proof.	208	Proof.
201	induction os as [\|[u v] t IH]; intros.	209	induction os as [\|[u v] t IH]; intros.
⋯ 56 identical lines (template 202–263, ours 210–271)
264	apply evstep_refl'. cbn [Oout app_ds dl ro_out]. rewrite <- Ozeq. reflexivity.	272	apply evstep_refl'. cbn [Oout app_ds dl ro_out]. rewrite <- Ozeq. reflexivity.
265	Qed.	273	Qed.
267	Lemma init: c0 -->* K [d1 1 2] 8 5.	275	Lemma init: c0 -->* K [d1 1 10] 8 1.
268	Proof. unfold K, L0. cbn. solve_init. Qed.	276	Proof. unfold K, L0. cbn. solve_init. Qed.
270	(* ================= abstract invariant (write-up section 3) ================= *)
		278	(* ======= abstract invariant (section 3 of the parent's write-up, carried over unchanged) ======= *)
271	Open Scope nat_scope.	279	Open Scope nat_scope.
273	Definition bof d := match d with d0 _ _ => 0 \| d1 _ _ => 1 end.	281	Definition bof d := match d with d0 _ _ => 0 \| d1 _ _ => 1 end.
⋯ 346 identical lines (template 274–662, ours 282–670)
663	Proof.	671	Proof.
664	eapply multistep_nonhalt; [apply init\|].	672	eapply multistep_nonhalt; [apply init\|].
665	change (K [d1 1 2] 8 5) with (Kc ([d1 1 2], 8, 5)).	673	change (K [d1 1 10] 8 1) with (Kc ([d1 1 10], 8, 1)).
666	apply progress_nonhalt_cond with (P := INV).	674	apply progress_nonhalt_cond with (P := INV).
667	- exact step.	675	- exact step.
⋯ 4 identical lines (template 668–673, ours 676–681)
674	```	682	```
675	1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---	683	1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---
677	K(d_1 .. d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b B> 0^inf	685	K(d_1 .. d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf
678	digit (u,0,v) := (10)^u 00 (01)^v, (u,1,v) := (10)^u (01)^v (d_m least significant)	686	digit (u,0,v) := (10)^u 00 (01)^v, (u,1,v) := (10)^u (01)^v (d_m least significant)
679	start: 0^inf A> 0^inf -->* K((1,1,2); 8, 5) (step 483)	687	start: 0^inf A> 0^inf -->* K((1,1,10); 8, 1) (step 732)
681	M (j* = last bit-0 digit):	689	M (j* = last bit-0 digit):
682	K(.., (u,0,v), (u_j,1,v_j)_{j>j}; a, b) -->+ K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j>j}; a+1, b+2)	690	K(.., (u,0,v), (u_j,1,v_j)_{j>j}; a, b) -->+ K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j>j}; a+1, b+2)
⋯ 9 identical lines (template 683–692, ours 691–700)
693	```	701	```
694	*)	702	*)

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

105 items in 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v (702 lines): 75 Lemma, 23 Definition, 6 Fixpoint, 1 Inductive. 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 "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---").	L26	identicalexcept the TM string
2	Lemma	`rot01`	Lemma rot01 n (Y : side) : [0;1]^^n > (0 >> Y) = 0 >> ([1;0]^^n > Y).	L35	identical
3	Lemma	`lshift`	Lemma lshift (xs : list sym) n (l : side) : l <* xs <* xs^^n = l <* xs^^(S n).	L41	identical
4	Lemma	`S1_1`	Lemma S1_1 l r: l <* [] {{A}}> [0;1] > r --> l <* [0;1] <* [] {{A}}> r.	L47	adapted
5	Lemma	`S2_1`	Lemma S2_1 l r: l <* [] {{B}}> [1;0] > r --> l <* [1;0] <* [] {{B}}> r.	L48	adapted
6	Lemma	`S3_1`	Lemma S3_1 l r: l <* [1;0] <{{C}} [] > r --> l <{{C}} [] > [1;0] > r.	L49	adapted
7	Lemma	`S4_1`	Lemma S4_1 l r: l <* [0;1] <{{D}} [] > r --> l <{{D}} [] > [0;1] > r.	L50	adapted
8	Lemma	`S6_1`	Lemma S6_1 l r: l <* [0] {{A}}> [1;0] > r --> l <* [0;1] <* [0] {{A}}> r.	L51	adapted
9	Lemma	`S5_1`	Lemma S5_1 l r: l {{B}}> [1;1] > [0;1] > r -->* l <* [0;1] {{B}}> [1;1] *> r.	L52	adapted
10	Definition	`S1`	Definition S1 := shift_rule_R _ _ _ _ _ S1_1.	L54	identical
11	Definition	`S2`	Definition S2 := shift_rule_R _ _ _ _ _ S2_1.	L55	identical
12	Definition	`S3`	Definition S3 := shift_rule_L _ _ _ _ _ S3_1.	L56	identical
13	Definition	`S4`	Definition S4 := shift_rule_L _ _ _ _ _ S4_1.	L57	identical
14	Definition	`S6`	Definition S6 := shift_rule_R _ _ _ _ _ S6_1.	L58	identical
15	Lemma	`S5`	Lemma S5 n: forall l r, l {{B}}> [1;1] > [0;1]^^n > r -->* l <* [0;1]^^n {{B}}> [1;1] *> r.	L60	adapted
16	Lemma	`T1`	Lemma T1 l: l {{A}}> 0inf -->* l <{{D}} [0;1] *> 0inf.	L68	adapted
17	Lemma	`T2`	Lemma T2 l r: l <* [0;0;0] <{{D}} r -->* l <* [0;0;1] {{A}}> r.	L69	adapted
18	Lemma	`T3`	Lemma T3 l r: l <* [0;0;1] <{{D}} r -->* l <{{D}} [0;1;1] *> r.	L70	adapted
19	Lemma	`T4`	Lemma T4 l r: l <* [1;0] <{{D}} r -->* l <{{C}} [1;1] *> r.	L71	adapted
20	Lemma	`T5`	Lemma T5 l r: l <* [0;1] <{{C}} r -->* l <{{D}} [0;1] *> r.	L72	adapted
21	Lemma	`T6`	Lemma T6 l r: l <* [0;0] <{{C}} r -->* l <* [0;1] {{B}}> r.	L73	adapted
22	Lemma	`T7`	Lemma T7 l r: l {{B}}> [1;1] > r --> l <* [0;0] {{B}}> r.	L74	adapted
23	Lemma	`T8`	Lemma T8 l r: l {{B}}> [1;1;0;1;1] > r --> l <* [0;0;0;0;1] {{A}}> r.	L75	adapted
24	Lemma	`T9`	Lemma T9 r: 0inf <* [1;0;0;1] <{{D}} r -->* 0inf <* [1;0;0;1] <* [0;0;0] {{A}}> r.	L76	adapted
25	Lemma	`T10`	Lemma T10 l r: l {{A}}> [1;1] > r --> l <* [0;0] {{A}}> r.	L77	adapted
26	Lemma	`T11`	Lemma T11 l r: l {{A}}> [0] > r --> l <* [1] {{B}}> r.	L78	adapted
27	Lemma	`T12`	Lemma T12 l: l {{B}}> [1;1] > 0inf --> l <{{D}} [0;1;1;0;1] *> 0inf.	L79	adapted
28	Lemma	`T13`	Lemma T13 l r: l <* [1;0;1] <{{D}} r -->* l <{{D}} [0;1;1] *> r.	L80	adapted
29	Lemma	`T14`	Lemma T14 l r: l {{A}}> [1;1;0;1] > r --> l <* [0;1;0;0] {{A}}> r.	L81	adapted
30	Lemma	`p01`	Lemma p01 n (Y : side) : [0;1]^^n > 0 >> 1 >> Y = 0 >> 1 >> [0;1]^^n > Y.	L84	identical
31	Lemma	`p10`	Lemma p10 n (Y : side) : [1;0]^^n > 1 >> 0 >> Y = 1 >> 0 >> [1;0]^^n > Y.	L86	identical
32	Lemma	`rot10`	Lemma rot10 n (Y : side) : [1;0]^^n > (1 >> Y) = 1 >> ([0;1]^^n > Y).	L89	identical
33	Lemma	`Lb`	Lemma Lb u v l r: l <* [0;1]^^(S u) <* [1;0]^^(S v) <{{D}} r -->* l <{{D}} [0;1]^^(S u) > [1;0]^^v > [1;1] *> r.	L97	adapted
34	Lemma	`Lf`	Lemma Lf u v l r: l <* [0;1]^^u <* [0;0] <* [1;0]^^(S v) <{{D}} r -->* l <* [0;1]^^(S u) <* [1;0]^^v {{B}}> [1;1] *> r.	L104	adapted
35	Lemma	`Rb`	Lemma Rb u v l r: l {{B}}> [1;1] > [0;1]^^u > [1;0]^^v > [1;1] > r -->* l <* [0;1]^^u <* [0;0] <* [1;0]^^v {{B}}> [1;1] *> r.	L111	adapted
36	Lemma	`Ro`	Lemma Ro u v l r: l <* [0;0;0] {{A}}> [0;1]^^(S u) > [1;0]^^v > [1;1] > r --> l <* [0;0] <* [1;0]^^(S u) <* [0;1]^^v <* [0;0;0] {{A}}> r.	L118	adapted
37	Lemma	`chunkA`	Lemma chunkA a b l: l <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{A}}> 0inf -->+ l <{{D}} [0;1]^^a > [0;1;1] > [0;1]^^(S (S b)) *> 0inf.	L129	adapted
38	Lemma	`chunkC`	Lemma chunkC a b l: l {{B}}> [1;1] > [0;1]^^a > [0;1;1] > [0;1]^^(S (S b)) > 0inf -->* l <* [0;1]^^(S a) <* [0;0;0] <* [0;1]^^(S (S b)) {{A}}> 0inf.	L135	adapted
39	Lemma	`chunkO`	Lemma chunkO a b l: l <* [0;0;0] {{A}}> [0;1]^^(S a) > [0;1;1] > [0;1]^^(S (S b)) > 0inf --> l <* [0;1] <* [1;0]^^(S a) <* [0;1]^^(S (S (S b))) <* [0;0;0] <* [0;1] {{A}}> 0inf.	L143	adapted
40	Inductive	`dg`	Inductive dg := d0 (u v : nat) \| d1 (u v : nat).	L154	identical
41	Definition	`dl`	Definition dl (d : dg) (l : side) : side := match d with \| d0 u v => l <* [0;1]^^u <* [0;0] <* [1;0]^^v \| d1 u v => l <* [0;1]^^u <* [1;0]^^v end.	L157	identical
42	Fixpoint	`app_ds`	Fixpoint app_ds (l : side) (ds : list dg) : side := match ds with \| [] => l \| d :: t => dl d (app_ds l t) end.	L164	identical
43	Definition	`L0`	Definition L0 : side := 0inf <* [1;0;0;1].	L170	identical
44	Definition	`K`	Definition K (ds : list dg) (a b : nat) : Q * tape := app_ds L0 ds <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{A}}> 0inf.	L172	adapted
45	Definition	`map1`	Definition map1 (os : list (nat*nat)) := map (fun '(u,v) => d1 (S u) (S v)) os.	L175	identical
46	Definition	`map0`	Definition map0 (os : list (nat*nat)) := map (fun '(u,v) => d0 (S u) v) os.	L176	identical
47	Fixpoint	`rw`	Fixpoint rw (os : list (natnat)) (r : side) : side := match os with \| [] => r \| (u,v) :: t => rw t ([0;1]^^(S u) > [1;0]^^v > [1;1] > r) end.	L178	identical
48	Lemma	`app_ds_app`	Lemma app_ds_app l xs ys : app_ds l (xs ++ ys) = app_ds (app_ds l ys) xs.	L184	identical
49	Lemma	`LbS`	Lemma LbS os: forall l r, app_ds l (map1 os) <{{D}} r -->* l <{{D}} rw os r.	L187	adapted
50	Lemma	`RbS`	Lemma RbS os: forall l r, l {{B}}> [1;1] > rw os r --> app_ds l (map0 os) {{B}}> [1;1] *> r.	L194	adapted
51	Fixpoint	`ro_out`	Fixpoint ro_out (os : list (natnat)) (l : side) : side := match os with \| [] => l \| (u,v) :: t => ro_out t l < [0;0] <* [1;0]^^(S u) <* [0;1]^^v end.	L201	identical
52	Lemma	`RoS`	Lemma RoS os: forall l r, l <* [0;0;0] {{A}}> rw os r -->* ro_out os l <* [0;0;0] {{A}}> r.	L207	adapted
53	Fixpoint	`Oz`	Fixpoint Oz (t : list (nat*nat)) (u : nat) : list dg := match t with \| [] => [d0 0 u] \| (a, b) :: t' => d0 b u :: Oz t' (S a) end.	L214	identical
54	Definition	`Oout`	Definition Oout (os : list (nat*nat)) (A : nat) : list dg := match os with \| [] => [] \| (u, v) :: t => d1 (S v) A :: Oz t (S u) end.	L220	identical
55	Lemma	`Ozeq`	Lemma Ozeq t: forall u l, ro_out t l <* [0;0] <* [1;0]^^u = app_ds l (Oz t u).	L226	identical
56	Lemma	`M_spec`	Lemma M_spec os u v rest a b: K (map1 os ++ d0 u (S v) :: rest) a b -->+ K (map0 os ++ d1 (S u) v :: rest) (S a) (S (S b)).	L234	identical
57	Lemma	`Mdrop_spec`	Lemma Mdrop_spec os u2 v2 u rest a b: K (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) a b -->+ K (map0 os ++ d0 (S u2 + S u) v2 :: rest) (S a) (S (S b)).	L248	identical
58	Lemma	`O_spec`	Lemma O_spec os a b: os <> [] -> K (map1 os) (S a) b -->+ K (Oout os (S a)) (S (S (S b))) 1.	L262	identical
59	Lemma	`init`	Lemma init: c0 -->* K [d1 1 10] 8 1.	L275	adapted
60	Definition	`bof`	Definition bof d := match d with d0 _ _ => 0 \| d1 _ _ => 1 end.	L281	identical
61	Definition	`vof`	Definition vof d := match d with d0 _ v => v \| d1 _ v => v end.	L282	identical
62	Fixpoint	`Rof`	Fixpoint Rof (ds : list dg) : nat := match ds with \| [] => 0 \| d0 _ _ :: t => 2 * Rof t + 1 \| d1 _ _ :: t => 2 * Rof t end.	L285	identical
63	Definition	`Rd`	Definition Rd d r := match d with d0 _ _ => 2r+1 \| d1 _ _ => 2r end.	L293	identical
64	Definition	`ub`	Definition ub d r := match d with d0 u _ => u + r + 1 \| d1 u _ => u + r end.	L294	identical
65	Fixpoint	`AllD`	Fixpoint AllD (P : dg -> nat -> nat -> Prop) (ds : list dg) : Prop := match ds with \| [] => True \| d :: t => AllD P t /\ P d (Rof t) (length t) end.	L296	identical
66	Definition	`canon`	Definition canon d := match d with d0 _ v => v >= 1 \| d1 u v => u >= 1 /\ v >= 1 end.	L302	identical
67	Definition	`PA`	Definition PA d r p := canon d /\ vof d >= Rd d r + 1 /\ ub d r mod 2 = 1 /\ (p = 0 -> ub d r = 1).	L304	identical
68	Definition	`PB`	Definition PB k d r p := canon d /\ (vof d + bof d) mod 2 = 1 /\ ub d r >= 2^(p+k) /\ (k = 0 -> p = 0 -> d = d0 0 1).	L306	identical
69	Definition	`LSBok`	Definition LSBok ds := match ds with [] => False \| d :: _ => vof d >= Rof ds + 1 end.	L309	identical
70	Definition	`INV`	Definition INV (s : list dg * nat * nat) : Prop := let '(ds, a, b) := s in ds <> [] /\ a >= 1 /\ b mod 2 = 1 /\ (a + Rof ds) mod 2 = 0 /\ a + Rof ds + 2 >= 2^(S (length ds)) /\ b + 3 + 2 * Rof ds >= 2^(S (length ds)) /\ LSBok ds /\ ( (AllD PA ds /\ a + Rof ds + 1 >= 2^(S (length ds))) \/ AllD (PB 0) ds … +1 lines	L311	identical
71	Definition	`Kc`	Definition Kc (s : list dg * nat * nat) : Q * tape := let '(ds, a, b) := s in K ds a b.	L319	identical
72	Lemma	`pow2S`	Lemma pow2S n : 2^(S n) = 2 * 2^n.	L322	identical
73	Lemma	`pow2pos`	Lemma pow2pos n : 2^n >= 1.	L324	identical
74	Lemma	`Rof_bound`	Lemma Rof_bound ds : Rof ds + 1 <= 2^(length ds).	L327	identical
75	Lemma	`Rof_map1`	Lemma Rof_map1 os X : Rof (map1 os ++ X) = 2^(length os) * Rof X.	L332	identical
76	Lemma	`Rof_map1'`	Lemma Rof_map1' os : Rof (map1 os) = 0.	L339	identical
77	Lemma	`len_map1`	Lemma len_map1 os : length (map1 os) = length os.	L342	identical
78	Lemma	`len_map0`	Lemma len_map0 os : length (map0 os) = length os.	L344	identical
79	Lemma	`AllD_app`	Lemma AllD_app P xs ys : AllD P (xs ++ ys) -> AllD P ys.	L347	identical
80	Lemma	`AllD_last`	Lemma AllD_last P xs d : AllD P (xs ++ [d]) -> P d 0 0.	L350	identical
81	Lemma	`AllD_canon`	Lemma AllD_canon (P : dg -> nat -> nat -> Prop) ds : (forall d r p, P d r p -> canon d) -> AllD P ds -> Forall canon ds.	L353	identical
82	Lemma	`decomp`	Lemma decomp ds : Forall canon ds -> (exists os, ds = map1 os) \/ (exists os u v rest, ds = map1 os ++ d0 u (S v) :: rest).	L359	identical
83	Lemma	`F1`	Lemma F1 (P : dg -> nat -> nat -> Prop) os u v rest: (forall u v r p, P (d0 u (S (S v))) r p -> P (d1 (S u) (S v)) r p) -> (forall u v r p, P (d1 (S u) (S v)) (S r) p -> P (d0 (S u) v) r p) -> AllD P (map1 os ++ d0 u (S (S v)) :: rest) -> AllD P (map0 os ++ d1 (S u) (S v) :: rest) /\ Rof (map1 os ++ d0 u (S (S v)) :: rest) = S (Rof (map0 os ++ d1 (S u) (S v) :: rest)) /\ … +1 lines	L373	identical
84	Lemma	`PA_touch0`	Lemma PA_touch0 u v r p : PA (d0 u (S (S v))) r p -> PA (d1 (S u) (S v)) r p.	L389	identical
85	Lemma	`PA_touch1`	Lemma PA_touch1 u v r p : PA (d1 (S u) (S v)) (S r) p -> PA (d0 (S u) v) r p.	L393	identical
86	Lemma	`PB_touch0`	Lemma PB_touch0 k u v r p : PB k (d0 u (S (S v))) r p -> PB k (d1 (S u) (S v)) r p.	L397	identical
87	Lemma	`PB_touch1`	Lemma PB_touch1 k u v r p : PB k (d1 (S u) (S v)) (S r) p -> PB k (d0 (S u) v) r p.	L401	identical
88	Definition	`Rel`	Definition Rel r ro rn := rn + 1 <= ro /\ ro <= 2 * (rn + 1) /\ (r = 0 -> ro = rn + 1).	L406	identical
89	Lemma	`PB_chain`	Lemma PB_chain k k' r u v ro rn p : (k' = k \/ (k = 0 /\ k' = 1 /\ r = 0)) -> Rel r ro rn -> p >= 1 -> PB k (d1 (S u) (S v)) ro (S p) -> PB k' (d0 (S u) v) rn p.	L408	identical
90	Lemma	`PB_abs`	Lemma PB_abs k k' r p u2 v2 u : ((k' = k /\ (k = 0 -> p >= 1)) \/ (k = 0 /\ k' = 1 /\ p = 0 /\ r = 0)) -> PB k (d0 u 1) r p -> PB k (d1 (S u2) (S v2)) (2*r+1) (S p) -> PB k' (d0 (S u2 + S u) v2) r p.	L420	identical
91	Lemma	`F2chain`	Lemma F2chain k k' r os X X' : (k' = k \/ (k = 0 /\ k' = 1 /\ r = 0)) -> X' <> [] -> AllD (PB k) (map1 os ++ X) -> AllD (PB k') X' -> Rel r (Rof X) (Rof X') -> length X = S (length X') -> AllD (PB k') (map0 os ++ X') /\ Rel r (Rof (map1 os ++ X)) (Rof (map0 os ++ X')) /\ length (map1 os ++ X) = S (length (map0 os ++ X')).	L430	identical
92	Lemma	`F2`	Lemma F2 k k' os u2 v2 u rest: ((k' = k /\ (k = 0 -> rest <> [])) \/ (k = 0 /\ k' = 1 /\ rest = [])) -> AllD (PB k) (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) -> AllD (PB k') (map0 os ++ d0 (S u2 + S u) v2 :: rest) /\ Rel (Rof rest) (Rof (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest)) (Rof (map0 os ++ d0 (S u2 + S u) v2 :: rest)) /\ … +1 lines	L450	identical
93	Lemma	`Oz_len`	Lemma Oz_len t u : length (Oz t u) = S (length t).	L479	identical
94	Lemma	`Oz_R`	Lemma Oz_R t u : Rof (Oz t u) + 1 = 2^(S (length t)).	L482	identical
95	Lemma	`Oz_AB`	Lemma Oz_AB t : forall u, AllD PA (map1 t) -> u mod 2 = 1 -> (t = [] -> u = 1) -> AllD (PB 0) (Oz t u).	L489	identical
96	Lemma	`Oz_CA`	Lemma Oz_CA t : forall u, AllD (PB 1) (map1 t) -> u >= 2^(S (length t)) -> AllD PA (Oz t u).	L503	identical
97	Lemma	`Rof_M`	Lemma Rof_M os u v rest : Rof (map1 os ++ d0 u (S v) :: rest) = S (Rof (map0 os ++ d1 (S u) v :: rest)).	L518	identical
98	Lemma	`len_M`	Lemma len_M os u v w x rest : length (map0 os ++ d1 w x :: rest) = length (map1 os ++ d0 u v :: rest).	L524	identical
99	Lemma	`LSB_M`	Lemma LSB_M os u v rest : LSBok (map1 os ++ d0 u (S (S v)) :: rest) -> LSBok (map0 os ++ d1 (S u) (S v) :: rest).	L528	identical
100	Lemma	`Rof_head1`	Lemma Rof_head1 os X : os <> [] -> Rof (map1 os ++ X) mod 2 = 0.	L535	identical
101	Lemma	`Rof_head0`	Lemma Rof_head0 os x y rest : Rof (map0 os ++ d0 x y :: rest) mod 2 = 1.	L540	identical
102	Lemma	`LSB_drop`	Lemma LSB_drop os u2 v2 u rest r : LSBok (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) -> Rel r (Rof (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest)) (Rof (map0 os ++ d0 (S u2 + S u) v2 :: rest)) -> LSBok (map0 os ++ d0 (S u2 + S u) v2 :: rest).	L543	identical
103	Lemma	`app_cons_ne`	Lemma app_cons_ne {A} (xs : list A) y ys : xs ++ y :: ys <> [].	L552	identical
104	Lemma	`step`	Lemma step s : INV s -> exists s', Kc s -->+ Kc s' /\ INV s'.	L558	identical
105	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L670	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 174: The rules M and O

The rules in busycoq comment style, for this machine:

1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---     (= tau of 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, tau = EABCDF)

K(d_1 .. d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf
digit (u,0,v) := (10)^u 00 (01)^v,   (u,1,v) := (10)^u (01)^v      (d_m least significant)

start from K((1,1,10); 8, 1)                                  (step 732, section 2)

M  (carry; some bit is 0; j* = index of the LAST bit-0 digit, k = m - j*):
   K(.., (u,0,v), (u_j,1,v_j)_{j*<j<=m}; a, b) --> K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j*<j<=m}; a+1, b+2)
   steps 32 + 8a + 8b + 4v + sum_{j>j*} (8 u_j + 4 v_j);  needs v >= 1, u_j, v_j >= 1 (j > j*), a, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, P section 1)
O  (overflow; all bits 1):
   K((u_1,1,v_1) .. (u_m,1,v_m); a, b) --> K((0,0,u_1), (v_1-1,0,u_2), .., (v_{m-1}-1,0,u_m), (v_m,1,a); b+3, 1)
   steps 89 - 4m + 8a + 20b + 4 sum u_j + 8 sum v_j;  needs m >= 1, all u_j, v_j >= 1, a >= 1, b >= 0
O at m = 0:  K(; a, b) --> K((1,1,a); b+3, 1)   in 89 + 8a + 20b steps (a >= 1); used only inside the initial segment

We write M_k for an M step with k = m − j* trailing bit-1 digits.

O at m = 0 is the derivation of P§2.3 with no digits (no Lb and no Ro).

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

6 machines, 4 killed, 2 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
#11 kill 3	`1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---`	✓Killed: never halts	parent link; = #11b's table, run from state E; named in #11b's .v header; named in #11b's proof.md; named in #11b's notes.md; named in #11's proof.md; named in #11's notes.md · review · compared side by side above · mechanism
#33 kill 9	`1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---`	✓Killed: never halts	= #11b's table mirrored, run from state C; named in #11b's proof.md; named in #11b's notes.md; named in #33's proof.md; named in #33's notes.md · review · mechanism
#33b kill 10	`1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---`	✓Killed: never halts	= #11b's table mirrored, run from state B; named in #33b's notes.md · review · mechanism
#11b kill 14	`1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---`	✓Killed: never halts	this kill
#32	`1RB0LC_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---`	⚠Cryptid candidate	via #11: parent link; targeting: follow-on to #11; ledger: #32 = twin of #11; named in #32's proof.md; named in #32's notes.md · page
R4	`1RB0RE_1LC0RD_1LD0LD_1RA0LC_1RA1RF_1RA---`	⚠Cryptid candidate	via #32: = #32's table mirrored, run from state D; named in #32's proof.md; named in #32's notes.md; named in R4's notes.md · mechanism
Named in a file but not linked (not counted as family)
W4-4	`1RB0RA_1LC0RE_0LD0LB_1LA1LF_1RA0LF_1LC---`	▲Stuck	named in W4-4's notes.md · 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 541 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 1.78 s
✓
.v hash matches the checked hash
.v = checked sha256 5a95ad125127…; submission/ copy = checked sha256 5a95ad125127…
✓
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
- proof.md L1: # 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---: delta proof from kill #11 (#11b, Checkpoint B)
- proof.md L137: **Done as a scratch check.** `check_proof.py`'s `delta_text` applies exactly these edits (each one asserted to match the expected number of times). `rocq/make_delta.py` writes its output to `rocq/delta_check.v` (696 line
- proof.md L165: ## 7. Checkpoint B (Dennis)
○
Family posted together?
3 other kill(s) in the family: #11, #33, #33b; the Discord draft names 3 of them; 2 member(s) not killed: #32, R4

Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.0 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 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---

Files

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

name	size	changed
notes.md ↓	10 KB	2026-10-10 16:47
proof.md ↓	19 KB	2026-10-10 16:34
how_proved.md ↓	1.0 KB	2026-10-14 10:51
status.json ↓	1.8 KB	2026-10-13 06:44
1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v ↓	30 KB	2026-10-12 18:17
img/	5 items	2026-10-16 10:29
rocq/	6 items	2026-10-10 16:36
submission/	6 items	2026-10-12 17:49
work/	2 items	2026-10-12 17:33
check_proof.out ↓	4.1 KB	2026-10-10 16:31
check_proof.py ↓	37 KB	2026-10-10 16:29
check_proof_long.out ↓	4.0 KB	2026-10-10 16:32

status.json in full

{
 "tm": "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "label": "#11b",
 "parent": "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---",
 "parent_note": "#11; this machine is #11's table renamed by tau = EABCDF (no mirror), started in #11's state B",
 "relation": "sibling of #11: #11's table renamed, started in #11's state B",
 "existing_work": "There may be existing work by hipparcos. The sheet (Results row 1276, Level 1 row 44) gives 'Done By: hipparcos' and links the Discord thread https://discord.com/channels/960643023006490684/1432566675533992019. The thread's opening posts (2025-10-27, pasted by Dennis on 2026-10-10 into data/discord/2025-10-27_hipparcos_1RB0RB.txt) are about THIS string (1RB0RB_..., not #33's 1RB0RE_...): block rules, a stride acceleration and hypotheses, with 'I don't have enough analysis to prove that yet'. Later posts were not pasted. The string is not in busycoq and is still on the 740 list (line 511). Dennis, 2026-10-10: prove it anyway as part of the #11 family and say plainly that there may be existing work by hipparcos; the submission does so and credits the thread.",
 "note": "Killed 2026-10-10: check_kill PASS on sha256 153aa11a...290a (702 lines; the audited 7fc83eeb...2ae3 plus comment-only header edits that replace internal kill labels with 'the parent'; code identical with comments stripped). Package in submission/ (with parent-proof.md = #11's submission proof.md). Not posted. Before posting: #11's and #33b's README/discord twins paragraphs still call this machine not formalized.",
 "pr": "https://github.com/ccz181078/busycoq/pull/16",
 "pr_state": "merged",
 "pr_comments": 0,
 "pr_merged_at": "2026-10-13T12:26:07Z",
 "pr_merged_by": "ccz181078"
}

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