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

`1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---`

#11local proof 3Kill claimedSkelet 1-like Class 2bbchallenge ↗Explorer

How we proved it never halts

A counter whose digits burn fuel but never run dry the wrong way

It counts up in binary, like an odometer. Each digit is a run of 10s then a run of 01s, with two blank cells between them for a 0 (1010…10 00 0101…01) and none for a 1. To add 1, the head walks left from the right end to the nearest 0 digit, makes it a 1, turns the 1s it passed into 0s, and walks back; each digit it changes burns one 01 as fuel. When all digits are 1, an overflow swaps the two halves of every digit and adds a digit.

Trouble needs a carry to reach a digit with no fuel. A digit that runs dry while becoming a 1 just merges into the next digit, which is harmless. The danger is a 1 digit with one unit of fuel being turned into a 0.

The key idea: call the stretch between two overflows a cycle. In a quiet cycle every digit has more fuel than touches still to come. In the lossy cycle after it, digits run dry at irregular times, but each digit's fuel plus its value stays odd, since a touch burns one unit and flips the digit. So a digit on its last unit of fuel is always a 0, and runs dry harmlessly as it becomes a 1.

Why that settles it: each overflow sets up the next cycle. A quiet cycle leaves lengths that give the lossy one its odd sums, and a lossy cycle leaves runs long enough to fuel a quiet one. The run reaches this pattern at step 483 and every move keeps it, so the machine never halts.

The Rocq proof (checked against busycoq) builds both moves from 20 small tape lemmas, replays the first 483 steps, and proves that every move keeps the invariant.

#3local proof number

694lines of Rocq

9 sto compile

6/6automatic checks

Overview

In one sentence

Binary counter on (10)^u[00](01)^v blocks; carries + re-pairing overflow explain every step to 1e9

Submitted mechanism At the right edge the tape is K = 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b B> 0^inf. Each digit is (10)^u 00 (01)^v (bit 0) or (10)^u (01)^v (bit 1), and d_m is the least significant bit. (submission/README.md, Mechanism)

Upstream: Kill claimed · PR #16merged 2026-10-13 12:26 UTC by ccz181078 · Sk1Class2_v2.v · TM10 · on Submissions →
Rocq proof: check_kill PASS · first Oct 10 05:20
694 lines · 29 KB .v · compile 8.6 s · coqchk pass · 0 axioms · PASS Oct 10 05:20 (re-run Oct 12 18:15)
· the .v file
Automatic review: 6 of 6 checks passtemplate: verify/SBCv6.v Module TM21 (template) · details in Proof →
Class: Skelet 1-like Class 2ours: sheet Skelet 1-like Class 2 ≠ ours Binary counter over a block list with re-pairing overflow (TM21-like Skelet 1-like Class 2) · high confidence
On the list: not on BB6_holdouts_663.txt (line 438 of the previous list) · historical 740 line 438
#11eqv ×1sim 1e15

Mechanism

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

How it works: 3 notes

Tape = digits (10)^u J (01)^v (J = 00: bit 0, empty: bit 1), then a growing (10)^a 000 (10)^b block at the right end.
Every 4 right records = +1: the head runs left to the first 0-bit (ruler-depth carry); each touched v drops by 1.
All bits 1 -> overflow: a run to the far left re-pairs the blocks. A digit whose v runs out fuses with its neighbour.

Figures for Checkpoint A

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.

Checkpoint A · 3 open

check: does the figure show what I claim? A “no” stops proof work built on a wrong reading. decision: your call.

Q1
check Fig 1 do the sweep depths follow a ruler pattern (shallow, deeper, shallow, deepest), ending in one sweep to the left edge?
Q2
check Fig 2 does the tape look like blocks separated by dashed walls, with the whole pattern reshuffling at each band break?
Q3
check Fig 3 further out, are the walls and band breaks the same kind as in Fig 2, with nothing new appearing?

Discord message 2 · draft, not posted

Skelet 1-like Class 2 · ready to paste · source

Is anyone working on any of these Skelet 1-like Class 2 holdouts? @hipparcos, group 2 is the table of your `1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` (Oct 2025 thread), so that part is mainly for you.

1. `1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---`, `1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---`, `1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---` (identical trajectories to 1e9). Binary down-counter on a list of `(10)^p (01)^q` pairs; on overflow the list is re-paired.
2. `1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---` is hipparcos's machine with states renamed (A..F -> E,A,B,C,D,F), i.e. the same table started in E instead of A. `1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---` is its mirror. Binary counter over `(10)^u [00] (01)^v` blocks, also with a re-pairing overflow.

Both share SBCv6 TM21's architecture (carries plus a re-pairing overflow), but TM21's configs don't fit either one. What we checked: all are still on the 2026-10-07 holdout list; `Sk1Machines.v` only covers Class 1; the carry and overflow rules hold in simulation to 1e9. No proofs yet. If nobody has them, we'd like to try one Rocq proof per group.

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 strategy & riskshow the formal proof will go · 3 risks to watch

Copy TM21's shape: K(list,a,b) as a Fixpoint over (u,bit,v) blocks; prove M_k by induction on k (like LIncs_spec) and O by induction on the list (like Ov_spec) from es-level sweep lemmas. Then nonhalt via multistep_nonhalt + progress_nonhalt_cond with a merge-aware invariant that keeps every v reached by a carry >= 1. Same rules give the 2 twins (new init lemmas only).

▲Invariant is the real work: digits do run out and merge (9 -> 5 digits in one cycle); TM21's LWF does not carry over.
▲Twin on the 'worked on extensively' tab (hipparcos, Oct 2025 thread) is this same table: duplicate-work risk until he answers.
▲Size: list bookkeeping plus merge cases likely 20-50 KB of Rocq (TM21 is ~300 lines).

Stats & provenance10⁹ steps simulated · 77,685 cells · the status in full · files

simulated: 10⁹ steps
tape: 77,685 cells · 38,836 nonzeros
growth: right edge ~t^0.51; left edge -3 cells per overflow (54 by 1e9; rules-only model: 122 by 1e15, 23 digits)
status now: check_kill PASS, independently re-verified (status.json, 2026-10-10)
observer's note: M_k + O validated, exact to 1e9; rules-only model runs to 1e15 with no stuck case. Not cryptid. Ask hipparcos first (same table).
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v

Proof & checks

6/6 automatic checks pass

Kill 3 · Skelet 1-like Class 2 · the kill file 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v: 694 lines, 105 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (template): verify/SBCv6.v Module TM21 · 6% of our lines identical

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

1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---

vs holdout list

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

Theorem

✓ Lemma nonhalt: ~halts tm c0. L662

check_kill

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

Checked .v

sha256 d177c06de5df0ff2…

✓	1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v	`d177c06de5df0ff2…` = checked
✓	submission/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v	`d177c06de5df0ff2…` = 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`	29716 bytes, 694 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 18: TM_from_str "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---" == <tm> (41 bytes)
✓	`theorem_text`	line 662: 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.6s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---") 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.7s); its context summary lists nothing of the file's own
✓	`integrity`	input sha256 and framework HEAD/cleanliness identical before and after

2Where 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).

template verify/SBCv6.v Module TM21 · detected from submission/proof.md line 22

6%of our lines identical to the template

2changed lines

559added lines (ours only)

284template lines dropped

1 / 2 / 102items identical / adapted / new

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

It follows the architecture of SBCv6.v Module TM21 (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE), a binary counter over a list of (n, m) pairs with a re-pairing overflow. Its transitions are not close (10 of 12 differ under the best renaming).

Kept: a Fixpoint over a digit list as the configuration, the overflow as a list re-pairing (Oz/Oout, as TM21's Ov), and multistep_nonhalt + progress_nonhalt_cond with a list invariant.
Changed: every digit carries a bit. The macro step is one carry (M_spec) rather than TM21's whole-cycle LIncs/BigStep, because merges happen at data-dependent times. TM21's LWF (2^len ≤ m) fails here, so it is replaced by the three-phase INV. The window lemmas are direct es runs, not flip/sideRLs.

The file is 694 lines, about 2.2 times TM21's 308. The informal proof is proof.md (§6 maps it to lemma names).

Fig P1 · 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

6% identical · 2 changed · 559 added

template 320 lines

11% kept verbatim · 284 not in ours

our items 105

1 identical · 2 adapted · 102 new · 25 template-only

identicalchanged / adaptedours only (new)template only

Template part: lines 1–53 (shared header, before the first Module) + 3703–4008 (body of Module TM21; the Module/End lines left out). Ours: lines 11–694 (header comment 1–10 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: segRLs_trans_add, sideRLs_trans_add, sideRLs_trans_S, tm', C0, C1, LH, toLH, LC1, LC0, Ov, Ov_spec, RC, RIncs, Ov', LIncs, LIncs_spec, S', BigStep, length_LIncs, LIncs_k, length_Ov, LWF, aWF, LWF_spec

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

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

template		ours
1	From BusyCoq Require Import Individual62.	12	From BusyCoq Require Import Individual62.
2	Require Import ZifyNat Lia.	13	Require Import ZifyNat Lia.
3	Require Import ZArith.
4	Require Import String.	14	Require Import String.
5	Require Import List.	15	Require Import List.
6	From BusyCoq Require Import Longitudinal.
		16	Require Import Arith.
8	Open Scope list.
10	Ltac flia := repeat (lia \|\| f_equal).
⋯ 35 template-only lines (template 12–49), not in ours
50	[ eassumption \| ];
51	try esx ].
3704	Definition tm := Eval compute in (TM_from_str "1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE").	18	Definition tm := Eval compute in (TM_from_str "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---").
		20	Notation "c --> c'" := (c -[ tm ]-> c') (at level 40).
3706	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).	21	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
3707	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).	22	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
3709	Definition tm' := flip tm.
		24	Open Scope list.
3711	Notation "l <\| r" := (l <{{C}} [] *> r) (at level 30).
		26	(* rotation of a power by one cell *)
3712	Notation "l \|> r" := (l <* [] {{E}}> r) (at level 30).
		27	Lemma rot01 n (Y : side) : [0;1]^^n > (0 >> Y) = 0 >> ([1;0]^^n > Y).
3714	Notation hL := (C,[]).
		28	Proof.
3715	Notation hR := (E,[]).
		29	induction n; cbn; [reflexivity\|].
3716	Notation hLR2 := [(hL,hR)].
		30	rewrite IHn. reflexivity.
3717	Notation hRL2 := [(hR,hL)].
		31	Qed.
3719	Definition C0 n m := <[0;1]^^(n) <+ <[0;0;1] <+ <[0;1]^^m <+ <[1].
		33	Lemma lshift (xs : list sym) n (l : side) : l <* xs <* xs^^n = l <* xs^^(S n).
3720	Definition C1 n m := <[0;1]^^(n) <+ <[0;1;1] <+ <[0;1]^^m <+ <[1].
		34	Proof.
3722	Inductive LH := LH1\|LH2\|LH3.
		35	cbn. rewrite <-Str_app_assoc, lpow_shift. reflexivity.
3724	Definition toLH x :=
		36	Qed.
3725	match x with
		38	(* ---------- one-block lemmas ---------- *)
3726	\| LH1 => 0inf
		39	Lemma S1_1 l r: l <* [] {{B}}> [0;1] > r --> l <* [0;1] <* [] {{B}}> r. Proof. es. Qed.
3727	\| LH2 => 0inf <* <[1;1;0;1;0;1;1]
		40	Lemma S2_1 l r: l <* [] {{C}}> [1;0] > r --> l <* [1;0] <* [] {{C}}> r. Proof. es. Qed.
3728	\| LH3 => 0inf <* <[1;1;1]
		41	Lemma S3_1 l r: l <* [1;0] <{{D}} [] > r --> l <{{D}} [] > [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.
		43	Lemma S6_1 l r: l <* [0] {{B}}> [1;0] > r --> l <* [0;1] <* [0] {{B}}> 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.
		46	Definition S1 := shift_rule_R _ _ _ _ _ S1_1.
		47	Definition S2 := shift_rule_R _ _ _ _ _ S2_1.
		48	Definition S3 := shift_rule_L _ _ _ _ _ S3_1.
		49	Definition S4 := shift_rule_L _ _ _ _ _ S4_1.
		50	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.
		53	Proof.
		54	induction n; intros.
		55	- finish.
		56	- follow S5_1. follow IHn. rewrite lshift. finish.
		57	Qed.
		59	(* ---------- finite turns ---------- *)
		60	Lemma T1 l: l {{B}}> 0inf -->* l <{{E}} [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.
		62	Lemma T3 l r: l <* [0;0;1] <{{E}} r -->* l <{{E}} [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.
		64	Lemma T5 l r: l <* [0;1] <{{D}} r -->* l <{{E}} [0;1] *> r. Proof. es. Qed.
		65	Lemma T6 l r: l <* [0;0] <{{D}} r -->* l <* [0;1] {{C}}> r. Proof. es. Qed.
		66	Lemma T7 l r: l {{C}}> [1;1] > r --> l <* [0;0] {{C}}> 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.
		68	Lemma T9 r: 0inf <* [1;0;0;1] <{{E}} r -->* 0inf <* [1;0;0;1] <* [0;0;0] {{B}}> r. Proof. es. Qed.
		69	Lemma T10 l r: l {{B}}> [1;1] > r --> l <* [0;0] {{B}}> r. Proof. es. Qed.
		70	Lemma T11 l r: l {{B}}> [0] > r --> l <* [1] {{C}}> r. Proof. es. Qed.
		71	Lemma T12 l: l {{C}}> [1;1] > 0inf --> l <{{E}} [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.
		73	Lemma T14 l r: l {{B}}> [1;1;0;1] > r --> l <* [0;1;0;0] {{B}}> r. Proof. es. Qed.
		76	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.
		78	Lemma p10 n (Y : side) : [1;0]^^n > 1 >> 0 >> Y = 1 >> 0 >> [1;0]^^n > Y.
		79	Proof. exact (lpow_shift' _ n [1;0] Y). Qed.
		81	Lemma rot10 n (Y : side) : [1;0]^^n > (1 >> Y) = 1 >> ([0;1]^^n > Y).
		82	Proof.
		83	induction n; cbn; [reflexivity\|].
		84	rewrite IHn. reflexivity.
		85	Qed.
		86	Ltac fin := apply evstep_refl'; simpl_tape; repeat (rewrite rot01 \|\| rewrite rot10); try reflexivity.
		88	(* ---------- digit lemmas ---------- *)
		89	Lemma Lb u v l r:
		90	l <* [0;1]^^(S u) <* [1;0]^^(S v) <{{E}} r -->*
		91	l <{{E}} [0;1]^^(S u) > [1;0]^^v > [1;1] *> r.
		92	Proof.
		93	follow T4. follow S3. follow T5. follow S4. fin.
		94	Qed.
		96	Lemma Lf u v l r:
		97	l <* [0;1]^^u <* [0;0] <* [1;0]^^(S v) <{{E}} r -->*
		98	l <* [0;1]^^(S u) <* [1;0]^^v {{C}}> [1;1] *> r.
		99	Proof.
		100	follow T4. follow S3. follow T6. follow S2. fin.
		101	Qed.
		103	Lemma Rb u v l r:
		104	l {{C}}> [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.
		106	Proof.
		107	follow S5. follow T7. follow S2. fin.
		108	Qed.
		110	Lemma Ro u v l r:
		111	l <* [0;0;0] {{B}}> [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.
		113	Proof.
		114	follow S1.
		115	follow (S6 (l <* [0;0;0] <* [0;1]^^u <* [1])).
		116	follow T10.
		117	fin.
		118	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 *)
		121	Lemma chunkA a b l:
		122	l <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{B}}> 0inf -->+
		123	l <{{E}} [0;1]^^a > [0;1;1] > [0;1]^^(S (S b)) *> 0inf.
		124	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 *)
		127	Lemma chunkC a b l:
		128	l {{C}}> [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.
		130	Proof.
		131	follow S5. follow T8. follow S1. fin.
		132	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 *)
		135	Lemma chunkO a b l:
		136	l <* [0;0;0] {{B}}> [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.
		138	Proof.
		139	follow S1. follow T11. follow S5. follow T12. follow S4. follow T13. follow S4. follow T2. follow S1. follow S1_1.
		140	rewrite (rot01 (S (S b))).
		141	follow (S6 (l <* [0;0;1] <* [0;1]^^a <* [1]) ([1;1;0;1] *> 0inf) (S (S (S b)))).
		142	follow T14. fin.
		143	Qed.
		145	(* ---------- the digit list ---------- *)
		146	Inductive dg := d0 (u v : nat) \| d1 (u v : nat).
		148	(* left-side lists are written nearest-cell first: (10)^u is [0;1]^^u, (01)^v is [1;0]^^v *)
		149	Definition dl (d : dg) (l : side) : side :=
		150	match d with
		151	\| d0 u v => l <* [0;1]^^u <* [0;0] <* [1;0]^^v
		152	\| d1 u v => l <* [0;1]^^u <* [1;0]^^v
3729	end.	153	end.
3731	Notation LS := (list (nat*nat)).
		155	(* digit lists are least significant digit first *)
3733	Fixpoint LC1(x:LS)(y:LH):side :=
		156	Fixpoint app_ds (l : side) (ds : list dg) : side :=
3734	match x with	157	match ds with
3735	\| [] => toLH y
		158	\| [] => l
3736	\| (n,m)::t => LC1 t y <* C1 n m
		159	\| d :: t => dl d (app_ds l t)
3737	end.	160	end.
3739	Fixpoint LC0(x:LS)(y:LH):side :=
		162	Definition L0 : side := 0inf <* [1;0;0;1].
3740	match x with
		164	Definition K (ds : list dg) (a b : nat) : Q * tape :=
3741	\| [] => toLH y
		165	app_ds L0 ds <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{B}}> 0inf.
3742	\| (n,m)::t => LC0 t y <* C0 n m
		167	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.
		170	Fixpoint rw (os : list (nat*nat)) (r : side) : side :=
		171	match os with
		172	\| [] => r
		173	\| (u,v) :: t => rw t ([0;1]^^(S u) > [1;0]^^v > [1;1] *> r)
3743	end.	174	end.
3745	Inductive Ov: LS->LH->nat->LS->LH->Prop :=
		176	Lemma app_ds_app l xs ys : app_ds l (xs ++ ys) = app_ds (app_ds l ys) xs.
3746	\| Ov_1 m a:
		177	Proof. induction xs; cbn; congruence. Qed.
3747	m<>O ->
		179	Lemma LbS os: forall l r, app_ds l (map1 os) <{{E}} r -->* l <{{E}} rw os r.
3748	Ov [(2,m)] LH1 a [(m,a)] LH2
3749	\| Ov_2 a:
⋯ 11 template-only lines (template 3750–3761), not in ours
3762	LC1 x y <\| [0;1]^^(1+a) > [1] > r -->+
3763	LC0 x' y' \|> r.
3764	Proof.	180	Proof.
3765	intro H.
		181	induction os as [\|[u v] t IH]; intros.
3766	induction H; intros.
		182	- finish.
3767	- destruct m. 1: lia.
		183	- cbn [map1 map app_ds dl rw]. follow Lb. apply IH.
3768	es.
3769	- es.
⋯ 5 template-only lines (template 3770–3774), not in ours
3775	follow100 IHOv.
3776	es.
3777	Qed.	184	Qed.
3779	Definition RC n m := [0;1]^^(1+n) > [1] > [0;1]^^m *> 0inf.
		186	Lemma RbS os: forall l r, l {{C}}> [1;1] > rw os r --> app_ds l (map0 os) {{C}}> [1;1] *> r.
3781	Lemma RIncs k n m:
3782	sideRLs tm (hRL2^^k) (RC n m) (RC (k+n) (k+m)).
3783	Proof.	187	Proof.
3784	unfold RC.
		188	induction os as [\|[u v] t IH]; intros.
3785	sideRLs_ind k.
		189	- finish.
		190	- cbn [map0 map app_ds dl rw]. follow IH. apply Rb.
3786	Qed.	191	Qed.
3788	Lemma Ov' x y a x' y' b:
		193	Fixpoint ro_out (os : list (nat*nat)) (l : side) : side :=
3789	Ov x y a x' y' ->
		194	match os with
3790	LC1 x y <\| RC a b -->+
		195	\| [] => l
3791	LC0 x' y' <\| RC b 1.
		196	\| (u,v) :: t => ro_out t l <* [0;0] <* [1;0]^^(S u) <* [0;1]^^v
		197	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.
3792	Proof.	200	Proof.
3793	unfold RC.
		201	induction os as [\|[u v] t IH]; intros.
3794	intro H.
		202	- finish.
3795	eapply Ov_spec in H.
		203	- cbn [ro_out rw]. follow IH. apply Ro.
3796	follow10 H.
3797	es.
3798	Qed.	204	Qed.
3800	Inductive LIncs: LS->LS->nat->Prop :=
		206	Fixpoint Oz (t : list (nat*nat)) (u : nat) : list dg :=
3801	\| LIncs_O:
		207	match t with
3802	LIncs [] [] 0
		208	\| [] => [d0 0 u]
3803	\| LIncs_S x y k n m:
		209	\| (a, b) :: t' => d0 b u :: Oz t' (S a)
3804	LIncs x y k ->
		210	end.
3805	LIncs (x<:(n,k+m)) (y<:(k+n,m)) (k*2+1)
		212	Definition Oout (os : list (nat*nat)) (A : nat) : list dg :=
3806	.
		213	match os with
3808	Lemma LIncs_spec x y k z:
		214	\| [] => []
3809	LIncs x y k ->
		215	\| (u, v) :: t => d1 (S v) A :: Oz t (S u)
3810	sideRLs tm' (hLR2^^k) (LC0 x z) (LC1 y z).
		216	end.
		218	Lemma Ozeq t: forall u l, ro_out t l <* [0;0] <* [1;0]^^u = app_ds l (Oz t u).
3811	Proof.	219	Proof.
3812	intros H.
		220	induction t as [\|[a b] t IH]; intros.
3813	induction H.
		221	- reflexivity.
3814	- esx.
		222	- cbn [ro_out Oz app_ds dl]. rewrite <- IH. reflexivity.
3815	- cbn[LC0]; cbn[LC1].
3816	eapply segRLs_sideRLs_concat.
⋯ 14 template-only lines (template 3817–3830), not in ours
3831	simpl_tape; cbn.
3832	esx.
3833	Qed.	223	Qed.
3835	Definition S' '(x,y,z) := LC0 x y <\| RC z 1.
		225	(* M: carry *)
3837	Lemma BigStep x y z x0 x1 y0 k:
		226	Lemma M_spec os u v rest a b:
3838	LIncs x x0 k ->
		227	K (map1 os ++ d0 u (S v) :: rest) a b -->+
3839	Ov x0 y (k+z) x1 y0 ->
		228	K (map0 os ++ d1 (S u) v :: rest) (S a) (S (S b)).
3840	S' (x,y,z) -->+
3841	S' (x1,y0,k+1).
3842	Proof.	229	Proof.
3843	unfold S'.
		230	unfold K. rewrite !app_ds_app.
3844	intros I1 I2.
		231	follow10 chunkA.
3845	eapply LIncs_spec in I1.
		232	follow LbS.
3846	eapply Ov' in I2.
		233	cbn [app_ds dl].
3847	epose proof (sideRLs_concat_1L (RIncs k _ _) I1) as I1'.
		234	follow Lf.
3848	follow I1'.
		235	follow RbS.
3849	apply I2.
		236	apply chunkC.
3850	Qed.	237	Qed.
3852	Lemma init:
		239	(* M with the flipped digit dropping: (u+1,1,0) fuses into the digit below it *)
3853	c0 -->*
		240	Lemma Mdrop_spec os u2 v2 u rest a b:
3854	S' (<[(2,2);(1%nat,3);(2,5)],LH1,4).
		241	K (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) a b -->+
		242	K (map0 os ++ d0 (S u2 + S u) v2 :: rest) (S a) (S (S b)).
3855	Proof.	243	Proof.
3856	esx.
		244	follow10 (M_spec (os ++ [(u2,v2)]) u 0 rest a b).
		245	assert (E: app_ds L0 (map0 (os ++ [(u2,v2)]) ++ d1 (S u) 0 :: rest) =
		246	app_ds L0 (map0 os ++ d0 (S u2 + S u) v2 :: rest)).
		247	{ unfold map0. rewrite map_app, <- app_assoc. cbn [map app].
		248	rewrite !app_ds_app. f_equal. cbn [app_ds dl].
		249	rewrite (lpow_add _ (S u2) (S u)), Str_app_assoc. reflexivity. }
		250	unfold K. rewrite E. finish.
3857	Qed.	251	Qed.
3859	Lemma length_LIncs {x y k}:
		253	(* O: overflow *)
3860	LIncs x y k ->
		254	Lemma O_spec os a b: os <> [] ->
3861	length y = length x.
		255	K (map1 os) (S a) b -->+ K (Oout os (S a)) (S (S (S b))) 1.
3862	Proof.	256	Proof.
3863	intros H.
		257	intro H. destruct os as [\|[u v] t]; [congruence\|].
3864	induction H; cbn; lia.
		258	unfold K.
		259	follow10 chunkA.
		260	follow LbS.
		261	follow T9.
		262	follow RoS.
		263	follow chunkO.
		264	apply evstep_refl'. cbn [Oout app_ds dl ro_out]. rewrite <- Ozeq. reflexivity.
3865	Qed.	265	Qed.
3867	Lemma LIncs_k x y k:
		267	Lemma init: c0 -->* K [d1 1 2] 8 5.
3868	LIncs x y k ->
		268	Proof. unfold K, L0. cbn. solve_init. Qed.
3869	k = 2^(length x)-1.
		270	(* ================= abstract invariant (write-up section 3) ================= *)
		271	Open Scope nat_scope.
		273	Definition bof d := match d with d0 _ _ => 0 \| d1 _ _ => 1 end.
		274	Definition vof d := match d with d0 _ v => v \| d1 _ v => v end.
		276	(* R of a list: carries still to come into its last (least significant) digit *)
		277	Fixpoint Rof (ds : list dg) : nat :=
		278	match ds with
		279	\| [] => 0
		280	\| d0 _ _ :: t => 2 * Rof t + 1
		281	\| d1 _ _ :: t => 2 * Rof t
		282	end.
		284	(* per-digit quantities, r = Rof of the digits above *)
		285	Definition Rd d r := match d with d0 _ _ => 2r+1 \| d1 _ _ => 2r end.
		286	Definition ub d r := match d with d0 u _ => u + r + 1 \| d1 u _ => u + r end.
		288	Fixpoint AllD (P : dg -> nat -> nat -> Prop) (ds : list dg) : Prop :=
		289	match ds with
		290	\| [] => True
		291	\| d :: t => AllD P t /\ P d (Rof t) (length t)
		292	end.
		294	Definition canon d := match d with d0 _ v => v >= 1 \| d1 u v => u >= 1 /\ v >= 1 end.
		296	Definition PA d r p :=
		297	canon d /\ vof d >= Rd d r + 1 /\ ub d r mod 2 = 1 /\ (p = 0 -> ub d r = 1).
		298	Definition PB k d r p :=
		299	canon d /\ (vof d + bof d) mod 2 = 1 /\ ub d r >= 2^(p+k) /\ (k = 0 -> p = 0 -> d = d0 0 1).
		301	Definition LSBok ds := match ds with [] => False \| d :: _ => vof d >= Rof ds + 1 end.
		303	Definition INV (s : list dg * nat * nat) : Prop :=
		304	let '(ds, a, b) := s in
		305	ds <> [] /\ a >= 1 /\ b mod 2 = 1 /\ (a + Rof ds) mod 2 = 0 /\
		306	a + Rof ds + 2 >= 2^(S (length ds)) /\ b + 3 + 2 * Rof ds >= 2^(S (length ds)) /\ LSBok ds /\
		307	( (AllD PA ds /\ a + Rof ds + 1 >= 2^(S (length ds)))
		308	\/ AllD (PB 0) ds
		309	\/ (AllD (PB 1) ds /\ a + Rof ds + 1 >= 2^(S (length ds)) /\ b + 1 + 2 * Rof ds >= 2^(S (length ds))) ).
		311	Definition Kc (s : list dg * nat * nat) : Q * tape := let '(ds, a, b) := s in K ds a b.
		313	(* ---------- arithmetic helpers ---------- *)
		314	Lemma pow2S n : 2^(S n) = 2 * 2^n.
		315	Proof. apply Nat.pow_succ_r'. Qed.
		316	Lemma pow2pos n : 2^n >= 1.
		317	Proof. pose proof (Nat.pow_nonzero 2 n). lia. Qed.
		319	Lemma Rof_bound ds : Rof ds + 1 <= 2^(length ds).
3870	Proof.	320	Proof.
3871	intros H.
		321	induction ds as [\|[u v\|u v] t IH]; cbn [Rof length]; rewrite ?pow2S; cbn; lia.
3872	induction H; cbn; lia.
3873	Qed.	322	Qed.
3875	Lemma length_Ov {x y a x' y'}:
		324	Lemma Rof_map1 os X : Rof (map1 os ++ X) = 2^(length os) * Rof X.
3876	Ov x y a x' y' ->
3877	length x' = length x + (match y with LH1 => 0 \| _ => 1 end).
3878	Proof.	325	Proof.
3879	intro H.
		326	induction os as [\|[u v] t IH]; cbn [map1 map app Rof length] in *.
3880	induction H; cbn; trivial.
		327	- cbn; lia.
3881	rewrite IHOv; trivial.
		328	- unfold map1 in IH. rewrite IH, pow2S. lia.
3882	Qed.	329	Qed.
3884	Inductive LWF: LS->LH->Prop :=
		331	Lemma Rof_map1' os : Rof (map1 os) = 0.
3885	\| LWF_S x y n m
		332	Proof. rewrite <- (app_nil_r (map1 os)), Rof_map1. cbn. lia. Qed.
3886	(Ha:LWF x y)
		334	Lemma len_map1 os : length (map1 os) = length os.
3887	(Hb:2^(length x)<=m)
		335	Proof. apply length_map. Qed.
3888	(Hc:n<>O):
		336	Lemma len_map0 os : length (map0 os) = length os.
3889	LWF (x<:(n,m)) y
		337	Proof. apply length_map. Qed.
3890	\| LWF_O_1:
		339	Lemma AllD_app P xs ys : AllD P (xs ++ ys) -> AllD P ys.
3891	LWF [(2,2)] LH1
		340	Proof. induction xs; cbn; tauto. Qed.
3892	\| LWF_O_2 a:
		342	Lemma AllD_last P xs d : AllD P (xs ++ [d]) -> P d 0 0.
3893	2<=a ->
		343	Proof. intro H. apply AllD_app in H. cbn in H. tauto. Qed.
3894	LWF [(2,a)] LH2
		345	Lemma AllD_canon (P : dg -> nat -> nat -> Prop) ds :
3895	\| LWF_O_3 a a0:
		346	(forall d r p, P d r p -> canon d) -> AllD P ds -> Forall canon ds.
3896	2<=a ->
3897	2<=a0 ->
⋯ 14 template-only lines (template 3898–3914), not in ours
3915	Ov x0 y a x1 y0 /\
3916	LWF x1 y0.
3917	Proof.	347	Proof.
3918	intro H.
		348	intro HP. induction ds; cbn; intros; constructor; firstorder.
3919	gen a.
		349	Qed.
3920	induction H.
		351	Lemma decomp ds : Forall canon ds ->
3921	- intros.
		352	(exists os, ds = map1 os) \/ (exists os u v rest, ds = map1 os ++ d0 u (S v) :: rest).
3922	epose proof (IHLWF _ _) as [x0 [k [I1 [x1 [y0 [I2 I3]]]]]].
		353	Proof.
3923	epose proof (LIncs_k _ _ _ I1); subst.
		354	induction ds as [\|[u v\|u v] t IH]; intro H.
3924	eexists _,_; split.
		355	- left. exists (@nil (nat*nat)). reflexivity.
3925	{ applys_eq (LIncs_S _ _ _ n (m-(2^(length x)-1)) I1).
		356	- inversion H; subst. cbn in *. destruct v as [\|v]; [lia\|].
3926	flia. }
		357	right. exists (@nil (nat*nat)), u, v, t. reflexivity.
3927	eexists _,_; split.
		358	- inversion H; subst. cbn in *. destruct u as [\|u]; [lia\|]. destruct v as [\|v]; [lia\|].
3928	{ apply Ov_S.
		359	destruct (IH ltac:(assumption)) as [[os E]\|[os [u' [v' [rest E]]]]]; subst.
3929	2: lia.
		360	+ left. exists ((u,v)::os). reflexivity.
3930	apply I2. }
		361	+ right. exists ((u,v)::os), u', v', rest. reflexivity.
3931	eapply LWF_S.
		362	Qed.
3932	+ apply I3.
		364	(* ---------- F1: a carry without a drop keeps every ubar/vbar ---------- *)
3933	+ inverts H0.
		365	Lemma F1 (P : dg -> nat -> nat -> Prop) os u v rest:
3934	cbn in HaWF.
		366	(forall u v r p, P (d0 u (S (S v))) r p -> P (d1 (S u) (S v)) r p) ->
3935	epose proof (length_LIncs I1).
		367	(forall u v r p, P (d1 (S u) (S v)) (S r) p -> P (d0 (S u) v) r p) ->
3936	epose proof (length_Ov I2).
		368	AllD P (map1 os ++ d0 u (S (S v)) :: rest) ->
3937	rewrite H1,H0.
		369	AllD P (map0 os ++ d1 (S u) (S v) :: rest) /\
3938	destruct y; rewrite Nat.pow_add_r; lia.
		370	Rof (map1 os ++ d0 u (S (S v)) :: rest) = S (Rof (map0 os ++ d1 (S u) (S v) :: rest)) /\
		371	length (map0 os ++ d1 (S u) (S v) :: rest) = length (map1 os ++ d0 u (S (S v)) :: rest).
		372	Proof.
		373	intros H0 H1. induction os as [\|[u' v'] t IH]; intros HA.
		374	- cbn [map1 map0 map app AllD Rof length] in *. destruct HA as [HA HP].
		375	repeat split; auto. lia.
		376	- unfold map1, map0 in . cbn [map app AllD Rof length] in . destruct HA as [HA HP].
		377	destruct (IH HA) as [IA [IR IL]].
		378	rewrite IR in HP. rewrite IL. repeat split; auto. lia.
		379	Qed.
		381	Lemma PA_touch0 u v r p : PA (d0 u (S (S v))) r p -> PA (d1 (S u) (S v)) r p.
		382	Proof. unfold PA, canon, Rd, ub, vof. intros (H1 & H2 & H3 & H4).
		383	repeat split; try lia; intro E; specialize (H4 E); lia. Qed.
		385	Lemma PA_touch1 u v r p : PA (d1 (S u) (S v)) (S r) p -> PA (d0 (S u) v) r p.
		386	Proof. unfold PA, canon, Rd, ub, vof. intros (H1 & H2 & H3 & H4).
		387	repeat split; try lia; intro E; specialize (H4 E); lia. Qed.
		389	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.
		390	Proof. unfold PB, canon, ub, vof, bof. intros (H1 & H2 & H3 & H4).
		391	repeat split; try lia; intros E1 E2; specialize (H4 E1 E2); discriminate. Qed.
		393	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.
		394	Proof. unfold PB, canon, ub, vof, bof. intros (H1 & H2 & H3 & H4).
		395	repeat split; try lia; intros E1 E2; specialize (H4 E1 E2); discriminate. Qed.
		397	(* ---------- F2: a drop ---------- *)
		398	Definition Rel r ro rn := rn + 1 <= ro /\ ro <= 2 * (rn + 1) /\ (r = 0 -> ro = rn + 1).
		400	Lemma PB_chain k k' r u v ro rn p :
		401	(k' = k \/ (k = 0 /\ k' = 1 /\ r = 0)) -> Rel r ro rn -> p >= 1 ->
		402	PB k (d1 (S u) (S v)) ro (S p) -> PB k' (d0 (S u) v) rn p.
		403	Proof.
		404	unfold PB, Rel, canon, ub, vof, bof. intros Hk (R1 & R2 & R3) Hp (H1 & H2 & H3 & H4).
		405	cbn [Nat.add] in H3. rewrite pow2S in H3.
		406	repeat split; try lia.
		407	destruct Hk as [Hk\|(Hk & Hk' & Hr)]; subst.
		408	- lia.
		409	- specialize (R3 eq_refl). rewrite Nat.add_0_r in H3. rewrite (Nat.add_1_r p), pow2S. lia.
		410	Qed.
		412	Lemma PB_abs k k' r p u2 v2 u :
		413	((k' = k /\ (k = 0 -> p >= 1)) \/ (k = 0 /\ k' = 1 /\ p = 0 /\ r = 0)) ->
		414	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.
		415	Proof.
		416	unfold PB, canon, ub, vof, bof. intros Hk (A1 & A2 & A3 & A4) (H1 & H2 & H3 & H4).
		417	destruct Hk as [(Hk & Hp)\|(Hk & Hk' & Hp & Hr)]; subst.
		418	- repeat split; try lia; try (intros E1 E2; specialize (Hp E1); lia).
		419	- cbn [Nat.pow Nat.add] in *. repeat split; try lia; try (intros E1; discriminate).
		420	Qed.
		422	Lemma F2chain k k' r os X X' :
		423	(k' = k \/ (k = 0 /\ k' = 1 /\ r = 0)) -> X' <> [] ->
		424	AllD (PB k) (map1 os ++ X) -> AllD (PB k') X' -> Rel r (Rof X) (Rof X') -> length X = S (length X') ->
		425	AllD (PB k') (map0 os ++ X') /\ Rel r (Rof (map1 os ++ X)) (Rof (map0 os ++ X')) /\
		426	length (map1 os ++ X) = S (length (map0 os ++ X')).
		427	Proof.
		428	intros Hk HX'. induction os as [\|[u v] t IH]; intros HA HA' HR HL.
		429	- cbn [map1 map0 map app] in *. auto.
		430	- unfold map1, map0 in . cbn [map app AllD Rof length] in . destruct HA as [HA HP].
		431	destruct (IH HA HA' HR HL) as [IA [IR IL]].
		432	rewrite IL in HP.
		433	split; [split\|split].
		434	+ exact IA.
		435	+ eapply PB_chain; eauto.
		436	rewrite length_app. destruct X'; [congruence\|]. cbn. lia.
		437	+ unfold Rel in *. destruct IR as (R1 & R2 & R3). repeat split; try lia;
		438	try (intro E; specialize (R3 E); lia).
3939	+ lia.	439	+ lia.
3940	Unshelve.
3941	{ econstructor; lia. }
⋯ 35 template-only lines (template 3942–3976), not in ours
3977	2,3: cbn; lia.
3978	apply LWF_O_1.
3979	Qed.	440	Qed.
3981	Close Scope sym.
		442	Lemma F2 k k' os u2 v2 u rest:
		443	((k' = k /\ (k = 0 -> rest <> [])) \/ (k = 0 /\ k' = 1 /\ rest = [])) ->
		444	AllD (PB k) (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) ->
		445	AllD (PB k') (map0 os ++ d0 (S u2 + S u) v2 :: rest) /\
		446	Rel (Rof rest) (Rof (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest))
		447	(Rof (map0 os ++ d0 (S u2 + S u) v2 :: rest)) /\
		448	length (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) = S (length (map0 os ++ d0 (S u2 + S u) v2 :: rest)).
		449	Proof.
		450	intros Hk HA.
		451	replace (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest)
		452	with (map1 os ++ (d1 (S u2) (S v2) :: d0 u 1 :: rest)) in *
		453	by (unfold map1; rewrite map_app, <- app_assoc; reflexivity).
		454	pose proof (AllD_app _ _ _ HA) as HX. cbn [AllD Rof length] in HX.
		455	destruct HX as [[Hrest Hdrop] Habs].
		456	apply (F2chain k k' (Rof rest)).
		457	- destruct Hk as [(Hk & _)\|(Hk & Hk' & Hr)]; [left; auto\|right; subst; auto].
		458	- congruence.
		459	- exact HA.
		460	- cbn [AllD Rof length]. split.
		461	+ destruct Hk as [(Hk & _)\|(Hk & Hk' & Hr)]; subst; [exact Hrest\|exact I].
		462	+ eapply PB_abs; [\|exact Hdrop\|exact Habs].
		463	destruct Hk as [(Hk & Hne)\|(Hk & Hk' & Hr)]; subst.
		464	* left. split; auto. intro E. specialize (Hne E). destruct rest; [congruence\|]. cbn. lia.
		465	* right. cbn. auto.
		466	- unfold Rel. cbn [Rof]. lia.
		467	- reflexivity.
		468	Qed.
		470	(* ---------- F3: the overflow ---------- *)
		471	Lemma Oz_len t u : length (Oz t u) = S (length t).
		472	Proof. revert u. induction t as [\|[a b] t IH]; intro u; cbn; [reflexivity\|]. rewrite IH. reflexivity. Qed.
		474	Lemma Oz_R t u : Rof (Oz t u) + 1 = 2^(S (length t)).
		475	Proof.
		476	revert u. induction t as [\|[a b] t IH]; intro u; cbn [Oz Rof length].
		477	- cbn. reflexivity.
		478	- specialize (IH (S a)). rewrite (pow2S (S (length t))). lia.
		479	Qed.
		481	Lemma Oz_AB t : forall u, AllD PA (map1 t) -> u mod 2 = 1 -> (t = [] -> u = 1) -> AllD (PB 0) (Oz t u).
		482	Proof.
		483	induction t as [\|[a b] t IH]; intros u HA Hu Ht.
		484	- cbn. split; [exact I\|]. unfold PB, canon, ub, vof, bof. cbn.
		485	rewrite (Ht eq_refl). repeat split; lia.
		486	- unfold map1 in HA. cbn [map AllD] in HA. destruct HA as [HA HP]. fold (map1 t) in HA, HP.
		487	rewrite Rof_map1', len_map1 in HP. unfold PA, canon, Rd, ub, vof in HP. destruct HP as (P1 & P2 & P3 & P4).
		488	cbn [Oz AllD]. split.
		489	+ apply IH; [exact HA \| lia \| intro E; subst t; specialize (P4 eq_refl); lia].
		490	+ pose proof (Oz_R t (S a)) as HR. rewrite Oz_len.
		491	unfold PB, canon, ub, vof, bof. rewrite !Nat.add_0_r.
		492	repeat split; try lia; try (intros E1 E2; discriminate).
		493	Qed.
		495	Lemma Oz_CA t : forall u, AllD (PB 1) (map1 t) -> u >= 2^(S (length t)) -> AllD PA (Oz t u).
		496	Proof.
		497	induction t as [\|[a b] t IH]; intros u HA Hu.
		498	- cbn. split; [exact I\|]. unfold PA, canon, Rd, ub, vof. cbn in *. repeat split; lia.
		499	- unfold map1 in HA. cbn [map AllD] in HA. destruct HA as [HA HP]. fold (map1 t) in HA, HP.
		500	rewrite Rof_map1', len_map1 in HP. unfold PB, canon, ub, vof, bof in HP. destruct HP as (P1 & P2 & P3 & P4).
		501	cbn [Oz AllD]. split.
		502	+ apply IH; [exact HA\|]. rewrite (Nat.add_1_r (length t)) in P3. lia.
		503	+ pose proof (Oz_R t (S a)) as HR. rewrite Oz_len.
		504	cbn [length] in Hu. rewrite (pow2S (S (length t))), (pow2S (length t)) in Hu. rewrite (pow2S (length t)) in HR.
		505	unfold PA, canon, Rd, ub, vof.
		506	repeat split; try lia; try (intros E1; discriminate).
		507	Qed.
		509	(* ---------- bookkeeping for one carry ---------- *)
		510	Lemma Rof_M os u v rest :
		511	Rof (map1 os ++ d0 u (S v) :: rest) = S (Rof (map0 os ++ d1 (S u) v :: rest)).
		512	Proof.
		513	induction os as [\|[a b] t IH]; unfold map1, map0 in ; cbn [map app Rof] in ; lia.
		514	Qed.
		516	Lemma len_M os u v w x rest :
		517	length (map0 os ++ d1 w x :: rest) = length (map1 os ++ d0 u v :: rest).
		518	Proof. rewrite !length_app, len_map0, len_map1. reflexivity. Qed.
		520	Lemma LSB_M os u v rest :
		521	LSBok (map1 os ++ d0 u (S (S v)) :: rest) -> LSBok (map0 os ++ d1 (S u) (S v) :: rest).
		522	Proof.
		523	intro H. pose proof (Rof_M os u (S v) rest) as E.
		524	destruct os as [\|[a b] t]; cbn [map1 map0 map app LSBok vof] in *; lia.
		525	Qed.
		527	Lemma Rof_head1 os X : os <> [] -> Rof (map1 os ++ X) mod 2 = 0.
		528	Proof.
		529	destruct os as [\|[u v] t]; [congruence\|]. intros _. unfold map1. cbn [map app Rof]. lia.
		530	Qed.
		532	Lemma Rof_head0 os x y rest : Rof (map0 os ++ d0 x y :: rest) mod 2 = 1.
		533	Proof. destruct os as [\|[u v] t]; unfold map0; cbn [map app Rof]; lia. Qed.
		535	Lemma LSB_drop os u2 v2 u rest r :
		536	LSBok (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) ->
		537	Rel r (Rof (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest)) (Rof (map0 os ++ d0 (S u2 + S u) v2 :: rest)) ->
		538	LSBok (map0 os ++ d0 (S u2 + S u) v2 :: rest).
		539	Proof.
		540	unfold Rel. intros H (R1 & R2 & R3).
		541	destruct os as [\|[a b] t]; cbn [map1 map0 map app LSBok vof] in *; lia.
		542	Qed.
		544	Lemma app_cons_ne {A} (xs : list A) y ys : xs ++ y :: ys <> [].
		545	Proof. destruct xs; discriminate. Qed.
		547	Ltac pw := repeat (rewrite pow2S in *).
		549	(* ---------- closure: every INV state takes a macro step into INV ---------- *)
		550	Lemma step s : INV s -> exists s', Kc s -->+ Kc s' /\ INV s'.
		551	Proof.
		552	destruct s as [[ds a] b]. unfold INV.
		553	intros (Hne & Ha & Hb & Hpar & HS & HT & HL & Hcls).
		554	assert (Hc : Forall canon ds).
		555	{ destruct Hcls as [[HA _]\|[HB\|[HC _]]]; (eapply AllD_canon; [\|eassumption]);
		556	unfold PA, PB; intros; tauto. }
		557	destruct (decomp ds Hc) as [[os E]\|[os [u [v [rest E]]]]]; subst ds.
		558	- (* all bits 1: overflow O *)
		559	destruct a as [\|a]; [lia\|].
		560	assert (Hos : os <> []) by (intro; subst; apply Hne; reflexivity).
		561	rewrite Rof_map1', len_map1 in *.
		562	destruct os as [\|[u v] t]; [congruence\|].
		563	pose proof (Oz_R t (S u)) as HR. pose proof (Oz_len t (S u)) as HLz.
		564	exists (Oout ((u,v)::t) (S a), S (S (S b)), 1). split.
		565	{ apply O_spec. congruence. }
		566	unfold INV. cbn [Oout length Rof LSBok vof AllD] in *. rewrite HLz.
		567	destruct Hcls as [[HA HS1]\|[HB\|[HC [HS1 HT2]]]].
		568	+ (* A -> B *)
		569	unfold map1 in HA. cbn [map AllD] in HA. fold (map1 t) in HA. destruct HA as [HA HP].
		570	rewrite Rof_map1', len_map1 in HP. unfold PA, canon, Rd, ub, vof in HP. destruct HP as (P1 & P2 & P3 & P4).
		571	assert (HB' : AllD (PB 0) (Oz t (S u))).
		572	{ apply Oz_AB; [exact HA \| lia \| intro E; subst t; specialize (P4 eq_refl); lia]. }
		573	pw.
		574	repeat split; try lia; try discriminate.
		575	right. left. split; [exact HB'\|].
		576	unfold PB, canon, ub, vof, bof. rewrite ?Nat.add_0_r. pw.
		577	repeat split; try lia; try (intros E1 E2; discriminate).
		578	+ (* B cannot be all ones: its top is (0,0,1) *)
		579	exfalso. destruct (exists_last Hos) as [os' [o E]]. rewrite E in HB.
		580	unfold map1 in HB. rewrite map_app in HB. apply AllD_last in HB.
		581	destruct o as [x y]. unfold PB in HB. destruct HB as (_ & _ & _ & H4).
		582	specialize (H4 eq_refl eq_refl). discriminate.
		583	+ (* C -> A *)
		584	unfold map1 in HC. cbn [map AllD] in HC. fold (map1 t) in HC. destruct HC as [HC HP].
		585	rewrite Rof_map1', len_map1 in HP. unfold PB, canon, ub, vof, bof in HP. destruct HP as (P1 & P2 & P3 & P4).
		586	assert (HA' : AllD PA (Oz t (S u))).
		587	{ apply Oz_CA; [exact HC\|]. rewrite (Nat.add_1_r (length t)) in P3. lia. }
		588	pw.
		589	repeat split; try lia; try discriminate.
		590	left. split; [split; [exact HA'\|]\|].
		591	* unfold PA, canon, Rd, ub, vof.
		592	repeat split; try lia; try (intros E1; discriminate).
		593	* lia.
		594	- (* some bit 0: carry M *)
		595	destruct v as [\|v].
		596	+ (* the flipped digit drops *)
		597	destruct Hcls as [[HA _]\|[HB\|[HC [HS1 HT2]]]].
		598	{ exfalso. apply AllD_app in HA. cbn [AllD] in HA. destruct HA as [_ HP].
		599	unfold PA, Rd, vof in HP. lia. }
		600	all: destruct os as [\|o os0] eqn:Eos;
		601	[ exfalso; cbn [map1 map app LSBok vof Rof] in HL; lia \| ].
		602	all: assert (Hos : os <> []) by (subst os; discriminate).
		603	all: rewrite <- Eos in *; clear Eos o os0.
		604	all: destruct (exists_last Hos) as [os' [[u2 v2] Eo]]; subst os.
		605	all: exists (map0 os' ++ d0 (S u2 + S u) v2 :: rest, S a, S (S b)); split;
		606	[ apply Mdrop_spec \| unfold INV ].
		607	* (* B *)
		608	destruct rest as [\|d rest'] eqn:Er.
		609	-- (* top fall: B -> C *)
		610	rewrite <- Er in *.
		611	destruct (F2 0 1 os' u2 v2 u rest) as (HA' & HR & HLn); [right; auto \| exact HB \|].
		612	pose proof (Rof_bound (map0 os' ++ d0 (S u2 + S u) v2 :: rest)) as Hbd.
		613	pose proof (Rof_head1 (os' ++ [(u2,v2)]) (d0 u 1 :: rest) ltac:(apply app_cons_ne)) as Hp1.
		614	pose proof (Rof_head0 os' (S u2 + S u) v2 rest) as Hp0.
		615	pose proof (LSB_drop _ _ _ _ _ _ HL HR) as HL'.
		616	unfold Rel in HR. subst rest. cbn [Rof] in HR. destruct HR as (R1 & R2 & R3).
		617	specialize (R3 eq_refl).
		618	rewrite HLn in *. pw.
		619	repeat split; try lia; try apply app_cons_ne; auto.
		620	right. right. repeat split; auto; lia.
		621	-- (* B -> B *)
		622	rewrite <- Er in *.
		623	destruct (F2 0 0 os' u2 v2 u rest) as (HA' & HR & HLn);
		624	[left; split; auto; intros _; subst rest; discriminate \| exact HB \|].
		625	pose proof (Rof_bound (map0 os' ++ d0 (S u2 + S u) v2 :: rest)) as Hbd.
		626	pose proof (Rof_head1 (os' ++ [(u2,v2)]) (d0 u 1 :: rest) ltac:(apply app_cons_ne)) as Hp1.
		627	pose proof (Rof_head0 os' (S u2 + S u) v2 rest) as Hp0.
		628	pose proof (LSB_drop _ _ _ _ _ _ HL HR) as HL'.
		629	unfold Rel in HR. destruct HR as (R1 & R2 & R3).
		630	rewrite HLn in *. pw.
		631	repeat split; try lia; try apply app_cons_ne; auto.
		632	* (* C -> C *)
		633	destruct (F2 1 1 os' u2 v2 u rest) as (HA' & HR & HLn);
		634	[left; split; auto; intro E; discriminate \| exact HC \|].
		635	pose proof (Rof_bound (map0 os' ++ d0 (S u2 + S u) v2 :: rest)) as Hbd.
		636	pose proof (Rof_head1 (os' ++ [(u2,v2)]) (d0 u 1 :: rest) ltac:(apply app_cons_ne)) as Hp1.
		637	pose proof (Rof_head0 os' (S u2 + S u) v2 rest) as Hp0.
		638	pose proof (LSB_drop _ _ _ _ _ _ HL HR) as HL'.
		639	unfold Rel in HR. destruct HR as (R1 & R2 & R3).
		640	rewrite HLn in *. pw.
		641	repeat split; try lia; try apply app_cons_ne; auto.
		642	right. right. repeat split; auto; lia.
		643	+ (* no drop *)
		644	exists (map0 os ++ d1 (S u) (S v) :: rest, S a, S (S b)). split; [apply M_spec \| unfold INV].
		645	pose proof (Rof_M os u (S v) rest) as ER.
		646	pose proof (len_M os u (S (S v)) (S u) (S v) rest) as EL.
		647	pose proof (LSB_M os u v rest HL) as HL'.
		648	rewrite EL.
		649	destruct Hcls as [[HA HS1]\|[HB\|[HC [HS1 HT2]]]].
		650	* destruct (F1 PA os u v rest PA_touch0 PA_touch1 HA) as (HA' & _ & _).
		651	repeat split; try lia; try apply app_cons_ne; auto.
		652	left. split; [exact HA'\|lia].
		653	* destruct (F1 (PB 0) os u v rest (PB_touch0 0) (PB_touch1 0) HB) as (HB' & _ & _).
		654	repeat split; try lia; try apply app_cons_ne; auto.
		655	* destruct (F1 (PB 1) os u v rest (PB_touch0 1) (PB_touch1 1) HC) as (HC' & _ & _).
		656	repeat split; try lia; try apply app_cons_ne; auto.
		657	right. right. repeat split; auto; lia.
		658	Qed.
3983	Lemma nonhalt: ~halts tm c0.	662	Lemma nonhalt: ~halts tm c0.
3984	Proof.	663	Proof.
3985	eapply multistep_nonhalt.	664	eapply multistep_nonhalt; [apply init\|].
3986	1: apply init.
		665	change (K [d1 1 2] 8 5) with (Kc ([d1 1 2], 8, 5)).
3987	eapply progress_nonhalt_cond with (P:=fun '(x,y,z) => LWF x y /\ 1<=z).
		666	apply progress_nonhalt_cond with (P := INV).
3988	2:{
		667	- exact step.
3989	split.
		668	- unfold INV. cbn. repeat split; try lia; try discriminate.
3990	- apply LWF_S. 2,3: cbn; lia.
		669	left. unfold PA, canon, Rd, ub, vof. cbn. repeat split; lia.
3991	apply LWF_S. 2,3: cbn; lia.
3992	apply LWF_O_1.
⋯ 12 template-only lines (template 3993–4004), not in ours
4005	Unshelve.
4006	apply aWF_intro; lia.
4007	Qed.	670	Qed.
		673	(*
		674	```
		675	1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---
		677	K(d_1 .. d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b B> 0^inf
		678	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)
		681	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)
		683	v = 1: (u+1,1,0) fuses into the next digit: (u',0,v'-1) becomes (u'+u+1,0,v'-1)
		684	O (all bits 1):
		685	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,a); b+3, 1)
		687	per digit, r = R of the digits above: R = 2r+1-bit, ubar = u + r + 1 - bit, vbar = v - R
		688	INV: m >= 1, a >= 1, b odd, a+R even, a+R+2 >= 2^(m+1), b+3+2R >= 2^(m+1), v_m >= R+1, and
		689	A: every digit canonical, v >= R+1, ubar odd, ubar_1 = 1; a+R+1 >= 2^(m+1)
		690	B: every digit canonical, v+bit odd, ubar_j >= 2^(j-1), d_1 = (0,0,1)
		691	C: every digit canonical, v+bit odd, ubar_j >= 2^j; a+R+1 >= 2^(m+1), b+1+2R >= 2^(m+1)
		692	INV -> a macro step (M, M with a drop, or O) into INV (A->A, A->B, B->B, B->C, C->C, C->A)
		693	```
		694	*)

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

105 items in 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v (694 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 "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---").	L18	identicalexcept the TM string
2	Lemma	`rot01`	Lemma rot01 n (Y : side) : [0;1]^^n > (0 >> Y) = 0 >> ([1;0]^^n > Y).	L27	new
3	Lemma	`lshift`	Lemma lshift (xs : list sym) n (l : side) : l <* xs <* xs^^n = l <* xs^^(S n).	L33	new
4	Lemma	`S1_1`	Lemma S1_1 l r: l <* [] {{B}}> [0;1] > r --> l <* [0;1] <* [] {{B}}> r.	L39	new
5	Lemma	`S2_1`	Lemma S2_1 l r: l <* [] {{C}}> [1;0] > r --> l <* [1;0] <* [] {{C}}> r.	L40	new
6	Lemma	`S3_1`	Lemma S3_1 l r: l <* [1;0] <{{D}} [] > r --> l <{{D}} [] > [1;0] > r.	L41	new
7	Lemma	`S4_1`	Lemma S4_1 l r: l <* [0;1] <{{E}} [] > r --> l <{{E}} [] > [0;1] > r.	L42	new
8	Lemma	`S6_1`	Lemma S6_1 l r: l <* [0] {{B}}> [1;0] > r --> l <* [0;1] <* [0] {{B}}> r.	L43	new
9	Lemma	`S5_1`	Lemma S5_1 l r: l {{C}}> [1;1] > [0;1] > r -->* l <* [0;1] {{C}}> [1;1] *> r.	L44	new
10	Definition	`S1`	Definition S1 := shift_rule_R _ _ _ _ _ S1_1.	L46	new
11	Definition	`S2`	Definition S2 := shift_rule_R _ _ _ _ _ S2_1.	L47	new
12	Definition	`S3`	Definition S3 := shift_rule_L _ _ _ _ _ S3_1.	L48	new
13	Definition	`S4`	Definition S4 := shift_rule_L _ _ _ _ _ S4_1.	L49	new
14	Definition	`S6`	Definition S6 := shift_rule_R _ _ _ _ _ S6_1.	L50	new
15	Lemma	`S5`	Lemma S5 n: forall l r, l {{C}}> [1;1] > [0;1]^^n > r -->* l <* [0;1]^^n {{C}}> [1;1] *> r.	L52	new
16	Lemma	`T1`	Lemma T1 l: l {{B}}> 0inf -->* l <{{E}} [0;1] *> 0inf.	L60	new
17	Lemma	`T2`	Lemma T2 l r: l <* [0;0;0] <{{E}} r -->* l <* [0;0;1] {{B}}> r.	L61	new
18	Lemma	`T3`	Lemma T3 l r: l <* [0;0;1] <{{E}} r -->* l <{{E}} [0;1;1] *> r.	L62	new
19	Lemma	`T4`	Lemma T4 l r: l <* [1;0] <{{E}} r -->* l <{{D}} [1;1] *> r.	L63	new
20	Lemma	`T5`	Lemma T5 l r: l <* [0;1] <{{D}} r -->* l <{{E}} [0;1] *> r.	L64	new
21	Lemma	`T6`	Lemma T6 l r: l <* [0;0] <{{D}} r -->* l <* [0;1] {{C}}> r.	L65	new
22	Lemma	`T7`	Lemma T7 l r: l {{C}}> [1;1] > r --> l <* [0;0] {{C}}> r.	L66	new
23	Lemma	`T8`	Lemma T8 l r: l {{C}}> [1;1;0;1;1] > r --> l <* [0;0;0;0;1] {{B}}> r.	L67	new
24	Lemma	`T9`	Lemma T9 r: 0inf <* [1;0;0;1] <{{E}} r -->* 0inf <* [1;0;0;1] <* [0;0;0] {{B}}> r.	L68	new
25	Lemma	`T10`	Lemma T10 l r: l {{B}}> [1;1] > r --> l <* [0;0] {{B}}> r.	L69	new
26	Lemma	`T11`	Lemma T11 l r: l {{B}}> [0] > r --> l <* [1] {{C}}> r.	L70	new
27	Lemma	`T12`	Lemma T12 l: l {{C}}> [1;1] > 0inf --> l <{{E}} [0;1;1;0;1] *> 0inf.	L71	new
28	Lemma	`T13`	Lemma T13 l r: l <* [1;0;1] <{{E}} r -->* l <{{E}} [0;1;1] *> r.	L72	new
29	Lemma	`T14`	Lemma T14 l r: l {{B}}> [1;1;0;1] > r --> l <* [0;1;0;0] {{B}}> r.	L73	new
30	Lemma	`p01`	Lemma p01 n (Y : side) : [0;1]^^n > 0 >> 1 >> Y = 0 >> 1 >> [0;1]^^n > Y.	L76	new
31	Lemma	`p10`	Lemma p10 n (Y : side) : [1;0]^^n > 1 >> 0 >> Y = 1 >> 0 >> [1;0]^^n > Y.	L78	new
32	Lemma	`rot10`	Lemma rot10 n (Y : side) : [1;0]^^n > (1 >> Y) = 1 >> ([0;1]^^n > Y).	L81	new
33	Lemma	`Lb`	Lemma Lb u v l r: l <* [0;1]^^(S u) <* [1;0]^^(S v) <{{E}} r -->* l <{{E}} [0;1]^^(S u) > [1;0]^^v > [1;1] *> r.	L89	new
34	Lemma	`Lf`	Lemma Lf u v l r: l <* [0;1]^^u <* [0;0] <* [1;0]^^(S v) <{{E}} r -->* l <* [0;1]^^(S u) <* [1;0]^^v {{C}}> [1;1] *> r.	L96	new
35	Lemma	`Rb`	Lemma Rb u v l r: l {{C}}> [1;1] > [0;1]^^u > [1;0]^^v > [1;1] > r -->* l <* [0;1]^^u <* [0;0] <* [1;0]^^v {{C}}> [1;1] *> r.	L103	new
36	Lemma	`Ro`	Lemma Ro u v l r: l <* [0;0;0] {{B}}> [0;1]^^(S u) > [1;0]^^v > [1;1] > r --> l <* [0;0] <* [1;0]^^(S u) <* [0;1]^^v <* [0;0;0] {{B}}> r.	L110	new
37	Lemma	`chunkA`	Lemma chunkA a b l: l <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{B}}> 0inf -->+ l <{{E}} [0;1]^^a > [0;1;1] > [0;1]^^(S (S b)) *> 0inf.	L121	new
38	Lemma	`chunkC`	Lemma chunkC a b l: l {{C}}> [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)) {{B}}> 0inf.	L127	new
39	Lemma	`chunkO`	Lemma chunkO a b l: l <* [0;0;0] {{B}}> [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] {{B}}> 0inf.	L135	new
40	Inductive	`dg`	Inductive dg := d0 (u v : nat) \| d1 (u v : nat).	L146	new
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.	L149	new
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.	L156	new
43	Definition	`L0`	Definition L0 : side := 0inf <* [1;0;0;1].	L162	new
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 {{B}}> 0inf.	L164	new
45	Definition	`map1`	Definition map1 (os : list (nat*nat)) := map (fun '(u,v) => d1 (S u) (S v)) os.	L167	new
46	Definition	`map0`	Definition map0 (os : list (nat*nat)) := map (fun '(u,v) => d0 (S u) v) os.	L168	new
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.	L170	new
48	Lemma	`app_ds_app`	Lemma app_ds_app l xs ys : app_ds l (xs ++ ys) = app_ds (app_ds l ys) xs.	L176	new
49	Lemma	`LbS`	Lemma LbS os: forall l r, app_ds l (map1 os) <{{E}} r -->* l <{{E}} rw os r.	L179	new
50	Lemma	`RbS`	Lemma RbS os: forall l r, l {{C}}> [1;1] > rw os r --> app_ds l (map0 os) {{C}}> [1;1] *> r.	L186	new
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.	L193	new
52	Lemma	`RoS`	Lemma RoS os: forall l r, l <* [0;0;0] {{B}}> rw os r -->* ro_out os l <* [0;0;0] {{B}}> r.	L199	new
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.	L206	new
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.	L212	new
55	Lemma	`Ozeq`	Lemma Ozeq t: forall u l, ro_out t l <* [0;0] <* [1;0]^^u = app_ds l (Oz t u).	L218	new
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)).	L226	new
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)).	L240	new
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.	L254	new
59	Lemma	`init`	Lemma init: c0 -->* K [d1 1 2] 8 5.	L267	adapted
60	Definition	`bof`	Definition bof d := match d with d0 _ _ => 0 \| d1 _ _ => 1 end.	L273	new
61	Definition	`vof`	Definition vof d := match d with d0 _ v => v \| d1 _ v => v end.	L274	new
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.	L277	new
63	Definition	`Rd`	Definition Rd d r := match d with d0 _ _ => 2r+1 \| d1 _ _ => 2r end.	L285	new
64	Definition	`ub`	Definition ub d r := match d with d0 u _ => u + r + 1 \| d1 u _ => u + r end.	L286	new
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.	L288	new
66	Definition	`canon`	Definition canon d := match d with d0 _ v => v >= 1 \| d1 u v => u >= 1 /\ v >= 1 end.	L294	new
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).	L296	new
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).	L298	new
69	Definition	`LSBok`	Definition LSBok ds := match ds with [] => False \| d :: _ => vof d >= Rof ds + 1 end.	L301	new
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	L303	new
71	Definition	`Kc`	Definition Kc (s : list dg * nat * nat) : Q * tape := let '(ds, a, b) := s in K ds a b.	L311	new
72	Lemma	`pow2S`	Lemma pow2S n : 2^(S n) = 2 * 2^n.	L314	new
73	Lemma	`pow2pos`	Lemma pow2pos n : 2^n >= 1.	L316	new
74	Lemma	`Rof_bound`	Lemma Rof_bound ds : Rof ds + 1 <= 2^(length ds).	L319	new
75	Lemma	`Rof_map1`	Lemma Rof_map1 os X : Rof (map1 os ++ X) = 2^(length os) * Rof X.	L324	new
76	Lemma	`Rof_map1'`	Lemma Rof_map1' os : Rof (map1 os) = 0.	L331	new
77	Lemma	`len_map1`	Lemma len_map1 os : length (map1 os) = length os.	L334	new
78	Lemma	`len_map0`	Lemma len_map0 os : length (map0 os) = length os.	L336	new
79	Lemma	`AllD_app`	Lemma AllD_app P xs ys : AllD P (xs ++ ys) -> AllD P ys.	L339	new
80	Lemma	`AllD_last`	Lemma AllD_last P xs d : AllD P (xs ++ [d]) -> P d 0 0.	L342	new
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.	L345	new
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).	L351	new
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	L365	new
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.	L381	new
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.	L385	new
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.	L389	new
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.	L393	new
88	Definition	`Rel`	Definition Rel r ro rn := rn + 1 <= ro /\ ro <= 2 * (rn + 1) /\ (r = 0 -> ro = rn + 1).	L398	new
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.	L400	new
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.	L412	new
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')).	L422	new
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	L442	new
93	Lemma	`Oz_len`	Lemma Oz_len t u : length (Oz t u) = S (length t).	L471	new
94	Lemma	`Oz_R`	Lemma Oz_R t u : Rof (Oz t u) + 1 = 2^(S (length t)).	L474	new
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).	L481	new
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).	L495	new
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)).	L510	new
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).	L516	new
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).	L520	new
100	Lemma	`Rof_head1`	Lemma Rof_head1 os X : os <> [] -> Rof (map1 os ++ X) mod 2 = 0.	L527	new
101	Lemma	`Rof_head0`	Lemma Rof_head0 os x y rest : Rof (map0 os ++ d0 x y :: rest) mod 2 = 1.	L532	new
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).	L535	new
103	Lemma	`app_cons_ne`	Lemma app_cons_ne {A} (xs : list A) y ys : xs ++ y :: ys <> [].	L544	new
104	Lemma	`step`	Lemma step s : INV s -> exists s', Kc s -->+ Kc s' /\ INV s'.	L550	new
105	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L662	adapted

4What 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)
proof.md (working copy) · differs from the submitted copy

submission/proof.md line 137: 2. Rules

Transition table

     0    1
A   1RB  0LE
B   1RC  0RC
C   1LD  0RB
D   1LA  0LE
E   1LD  1LF
F   1LD  ---        halting transition: F reads 1

The macro rules M and O

In busycoq comment-block style:

1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---

start from K((1,1,2); 8, 5)                                   (step 483, §4)

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 >= 0), u_j >= 1 and v_j >= 1 for j > j*, a >= 0, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, §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

On the tape, O's right side is

0^inf 10 01 00 (01)^u_1 [(10)^(v_i-1) 00 (01)^u_(i+1)]_{i<m} (10)^v_m (01)^a (10)^(b+3) 0^3 10 B> 0^inf

M and O are derived from the 20 window lemmas of §2.1, as chains of intermediate configurations (§2.2, §2.3). Each step count above is the sum along the chain.

M needs only a ≥ 0; Common has a ≥ 1 anyway.

The .v proves the chains as -->+ statements (M_spec, Mdrop_spec, O_spec), so the step counts are not part of the formal statement.

2.1 Building blocks

Notation. X> means the head is in state X on the next cell, and <X means it is in state X on the previous cell (busycoq's {{X}}> and <{{X}}).

A window lemma w → w' means: started on the cells of w, the machine runs the stated number of steps without reading a cell outside w (the last step may move the head onto a neighbouring cell), and leaves w'. Such a lemma holds in every tape context.

How the lemmas are proved:

T1–T14 are exact finite runs (in the .v, each is one es).
S1–S6 are proved for one block by a finite run, and induction on n gives every n (in the .v, shift_rule_R/shift_rule_L, and plain induction for S5).

For example:

C> 11 (01)^(n+1) = C> 11 01 (01)^n → 10 C> 11 (01)^n → 10 (10)^n C> 11

Shift lemmas

	lemma	steps	one block	transitions
S1	`B> (01)^n → (10)^n B>`	2n	`B>01 → 10B>`	B0 C1
S2	`C> (10)^n → (01)^n C>`	2n	`C>10 → 01C>`	C1 B0
S3	`(01)^n <D → <D (10)^n`	2n	`01<D → <D10`	D1 E0
S4	`(10)^n <E → <E (01)^n`	2n	`10<E → <E01`	E0 D1
S5	`C> 11 (01)^n → (10)^n C> 11`	6n	`C>1101 → 10C>11`	C1 B1 C0 D0 A0 B1
S6	`0 B> (10)^n → (10)^n 0 B>`	6n	`0B>10 → 100B>`	B1 C0 D0 A0 B1 C1

S5 and S6 are the 2-cell back-bounces: on each block the head steps two cells right, two left and two right again.

Finite lemmas

	lemma	steps	transitions	where
T1	`B> 00 → <E 01`	3	B0 C0 D1	right-edge turn (on `0^inf`)
T2	`000 <E → 100 B>`	5	E0 D0 A0 B1 C1	turn inside a `0^3` gap
T3	`100 <E → <E 011`	3	E0 D0 A1
T4	`01 <E → <D 11`	2	E1 F0	start of a digit's `(01)^v`
T5	`10 <D → <E 01`	2	D0 A1	end of a bit-1 digit's `(01)^v`
T6	`00 <D → 10 C>`	3	D0 A0 B1	flips the `00` of a bit-0 digit
T7	`C> 11 → 00 C>`	2	C1 B1
T8	`C> 11011 → 10000 B>`	9	C1 B1 C0 D0 A0 B1 C1 B1 C1
T9	`0^inf 1001 <E → 0^inf 1001000 B>`	13	E1 F0 D0 A1 E0 D0 A0 B1 C1 B0 C1 B1 C1	far-left turn (window `0001001`)
T10	`B> 11 → 00 B>`	2	B1 C1
T11	`B> 0 → 1 C>`	1	B0
T12	`C> 11 0^inf → <E 01101 0^inf`	13	C1 B1 C0 D0 A0 B1 C1 B0 C0 D1 E0 D0 A1	right-edge turn in O (window `11000`)
T13	`101 <E → <E 011`	3	E1 F0 D1
T14	`B> 1101 → 0010 B>`	4	B1 C1 B0 C1

Digit lemmas

These are compositions; u, v are those of one digit.

	lemma	steps	made of	needs
Lb	`(10)^u (01)^v <E → <E (01)^u (10)^(v−1) 11`	2u+2v	T4, S3(v−1), T5, S4(u−1)	u, v ≥ 1
Lf	`(10)^u 00 (01)^v <E → (10)^(u+1) (01)^(v−1) C> 11`	4v+1	T4, S3(v−1), T6, S2(v−1)	v ≥ 1
Rb	`C> 11 (01)^u (10)^(v−1) 11 → (10)^u 00 (01)^(v−1) C> 11`	6u+2v	S5(u), T7, S2(v−1)	v ≥ 1
Ro	`B> (01)^u (10)^(v−1) 11 → (10)^(u−1) 1 (10)^(v−1) 000 B>`	2u+6v−4	S1(u), S6(v−1), T10	u, v ≥ 1

In Ro, S6 starts on the last 0 of (10)^u = (10)^(u−1) 1 0.

What each digit lemma does:

Lb sweeps a bit-1 digit leftward.
Lf flips the bit-0 digit.
Rb restores a swept digit as bit 0 on the way back in M.
Ro does the same in O.

2.2 Derivation of M

Write:

X for everything left of d_{j*} (it is never read);
(u*, v*) for d_{j*} = (u*,0,v*);
Y for the trailing bit-1 digits, with i = 1 being j*+1:

Y = Π_{i=1..k} (10)^u_i (01)^v_i

The chain

                                                                                        steps
    X (10)^u* 00 (01)^v* Y (10)^a 000 (10)^b B> 0^inf
 Phase 1: right-edge preamble with a dip into the 0^3 gap                               4b+10
T1  .. Y (10)^a 000 (10)^b <E 01                                                        3
S4  .. Y (10)^a 000 <E (01)^(b+1)                                                       2b
T2  .. Y (10)^a 100 B> (01)^(b+1)                                                       5
S1  .. Y (10)^(a+1) 0 (10)^(b+1) B> 0^inf                                               2b+2
 Phase 2: one long left sweep, down to the 00 of d_{j*}                                 2a+2b+9+4v*+Σ(2u_i+2v_i)
T1  .. Y (10)^(a+1) 0 (10)^(b+1) <E 01                                                  3
S4  .. Y (10)^(a+1) 0 <E (01)^(b+2)                                                     2b+2
T3  .. Y (10)^a <E 011 (01)^(b+2)                                                       3
S4  X (10)^u* 00 (01)^v* Y <E (01)^a 011 (01)^(b+2)                                     2a
Lb  X (10)^u* 00 (01)^v* <E Y' (01)^a 011 (01)^(b+2)       (i = k down to 1)            Σ(2u_i+2v_i)
                         Y' = Π_i (01)^u_i (10)^(v_i−1) 11
Lf  X (10)^(u*+1) (01)^(v*−1) C> 11 Y' (01)^a 011 (01)^(b+2)                            4v*+1
 Phase 3: rightward pass with 2-cell back-bounces, then a plain run to the edge         6a+2b+13+Σ(6u_i+2v_i)
Rb  X (10)^(u*+1) (01)^(v*−1) Y'' C> 11 (01)^a 011 (01)^(b+2)   (i = 1 up to k)         Σ(6u_i+2v_i)
                         Y'' = Π_i (10)^u_i 00 (01)^(v_i−1)
S5  .. Y'' (10)^a C> 11 011 (01)^(b+2)                                                  6a
T8  .. Y'' (10)^a 10000 B> (01)^(b+2)                                                   9
S1  X (10)^(u*+1) (01)^(v*−1) Y'' (10)^(a+1) 000 (10)^(b+2) B> 0^inf                    2b+4

The last line is

K(.., (u*+1,1,v*−1), (u_i,0,v_i−1)_i; a+1, b+2)

The sum is

(4b+10) + (2a+2b+9+4v*) + (6a+2b+13) + Σ(8u_i+4v_i) = 32 + 8a + 8b + 4v* + Σ(8u_i+4v_i)

Head path

Phase 1 runs left only to the 0^3 gap, turns (T2) and returns to the edge.

Phase 2 is the only long leftward leg. Its leftmost read is the first 0 of d_{j*}'s 00 (T6 reads both cells, then moves right). So M is a side rule: the tape X left of that 00 is never read.

Phase 3 moves right. It steps back two cells once per 01 block (S5, on the (01)^u_i blocks and on (01)^a), and it crosses the (10)^(v−1) blocks and the final (01)^(b+2) with plain sweeps (S2, S1).

When v* = 1, the flipped digit (u*+1,1,0) drops (§1). When some v_i = 1, the result has (u_i,0,0). That can happen only outside INV (§3.3).

2.3 Derivation of O

Let all digits be bit 1, and let

Y = Π_{i=1..m} (10)^u_i (01)^v_i

The chain

                                                                                        steps
    0^inf 10 01 Y (10)^a 000 (10)^b B> 0^inf
 Phases 1–2 as in M, with Lb on all m digits and no Lf                                  (4b+10)+(2a+2b+8)+Σ(2u_i+2v_i)
    0^inf 10 01 <E Y' (01)^a 011 (01)^(b+2)                Y' = Π_i (01)^u_i (10)^(v_i−1) 11
 Phase 3: turn at the far left
T9  0^inf 10 01 000 B> Y' (01)^a 011 (01)^(b+2)                                         13
 Phase 4: rightward pass
Ro  0^inf 10 01 000 Y''' B> (01)^a 011 (01)^(b+2)          (i = 1 up to m)              Σ(2u_i+6v_i−4)
                         Y''' = Π_i (10)^(u_i−1) 1 (10)^(v_i−1) 000
 Phase 5: right end                                                                     2a+8b+30
S1  .. Y''' (10)^a B> 011 (01)^(b+2)                                                    2a
T11 .. Y''' (10)^a 1 C> 11 (01)^(b+2)                                                   1
S5  .. Y''' (10)^a 1 (10)^(b+2) C> 11 0^inf                                             6b+12
T12 .. Y''' (10)^a 1 (10)^(b+2) <E 01101 0^inf                                          13
S4  .. Y''' (10)^a 1 <E (01)^(b+2) 01101                                                2b+4
 Phase 6: short left sweep over the a block, back to the 000 that Ro left after d_m    2a+1
T13 .. Y''' (10)^(a−1) <E 011 (01)^(b+2) 01101                                          3
S4  .. (10)^(v_m−1) 000 <E (01)^a 1 (01)^(b+2) 01101                                    2a−2
 Phase 7: turn in that 000, final run to the edge                                       2a+6b+27
T2  .. (10)^(v_m−1) 100 B> (01)^a (10)^(b+3) 1101          (1 (01)^(b+2) 0 = (10)^(b+3))  5
S1  .. (10)^(v_m−1) 100 (10)^a B> (10)^(b+3) 1101                                       2a
S6  .. (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 0 B> 1101                               6b+18
T14 .. (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 000 10 B> 0^inf                         4

Reading the result

Re-read the final tape with

0 (10)^(n−1) 1   = (01)^n
(10)^(v_m−1) 10  = (10)^v_m

This gives:

0^inf 10 01 000 Π_{i<m}[(10)^(u_i−1) 1 (10)^(v_i−1) 000] (10)^(u_m−1) 1 (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 000 10 B>
  = 0^inf 10 01 00 (01)^u_1 [(10)^(v_i−1) 00 (01)^u_(i+1)]_{i<m} (10)^v_m (01)^a (10)^(b+3) 000 10 B> 0^inf
  = 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)

The sum is

(4b+10) + (2a+2b+8) + 13 + (2a+8b+30) + (2a+1) + (2a+6b+27) + Σ(4u_i+8v_i−4) = 89 − 4m + 8a + 20b + 4Σu_i + 8Σv_i

Domain

Lb and Ro need u_i, v_i ≥ 1.
T13 and the S6 of phase 7 use the last 10 of (10)^a, so a ≥ 1.
T9 needs 0^inf on the left.

Head path

O has two leftward legs:

the long phase 2, which T9 ends 3 cells left of the leading 10 01 (so the leftmost cell visited moves 3 cells per overflow);
the short phase 6.

2.4 What the rules do, in words

The digits form a binary counter. Each M is one increment. It flips the trailing 1s to 0 and the last 0 to 1, and every digit it touches pays one 01 from its v. A digit flipping 0→1 also gains a 10.

When all bits are 1, O swaps the two halves of every digit:

each (10)^u becomes the (01)^u fuel of a new bit-0 digit;
each (01)^v becomes the next digit's (10)^(v-1).

The counter restarts at value 1 with one more digit.

When a digit flipping 0→1 has spent its last 01 (v = 1), it drops: its 10s merge into the next digit, and the counter loses that digit.

The only way the rules can fail is the failure mode: a carry arriving at a bit-0 digit with v = 0, where Lf's first lemma T4 has no 01 to read. That happens if a carry flips a bit-1 digit with v = 1 to 0.

Every macro step is an exact run of at least 32 steps, so every macro step makes progress.

5FamilyCheck: 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	this kill
#33 kill 9	`1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---`	✓Killed: never halts	= #11's table mirrored, run from state D; named in #33's .v header; 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	= #11's table mirrored, run from state C; named in #11's proof.md; named in #11's notes.md; named in #33b's .v header · review · mechanism
#11b kill 14	`1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---`	✓Killed: never halts	parent link; = #11's table, run from state B; 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 · same machine as this kill? (same table, started in #11's B; trajectory twin; tables, pictures and numbers side by side)
#32	`1RB0LC_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---`	⚠Cryptid candidate	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	named in R4's notes.md · mechanism
Named in a file but not linked (not counted as family)
#1	`1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---`	⚠Cryptid candidate	named in #1's proof.md · mechanism
W4-4	`1RB0RA_1LC0RE_0LD0LB_1LA1LF_1RA0LF_1LC---`	▲Stuck	named in W4-4's notes.md · mechanism
W4-3 kill 20	`1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---`	✓Killed: never halts	named in W4-3's proof.md; named in W4-3's notes.md · review · mechanism

6ChecklistCheck: 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 467 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.74 s
✓
.v hash matches the checked hash
.v = checked sha256 d177c06de5df…; submission/ copy = checked sha256 d177c06de5df…
✓
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 L101: - No Checkpoint B notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
- proof.md L6: - Status: informal proof, revised after the skeptic review (Review log at the end). Checkpoint B pending, non-blocking. Evidence: `check_proof.py` (§7).
○
Family posted together?
3 other kill(s) in the family: #33, #33b, #11b; the Discord draft names 2 of them; 2 member(s) not killed: #32, R4

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 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---

Files

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

name	size	changed
notes.md ↓	11 KB	2026-10-10 05:25
proof.md ↓	32 KB	2026-10-10 04:38
how_proved.md ↓	1.5 KB	2026-10-14 10:51
status.json ↓	353 B	2026-10-13 06:44
observe.json ↓	15 KB	2026-10-10 04:41
1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v ↓	29 KB	2026-10-12 18:15
img/	8 items	2026-10-10 01:54
rocq/	5 items	2026-10-10 05:18
scripts/	17 items	2026-10-10 00:38
submission/	6 items	2026-10-12 17:41
work/	2 items	2026-10-12 17:33
check_proof.py ↓	31 KB	2026-10-10 04:38
qsim.jsonl ↓	7.0 KB	2026-10-10 00:09
sim_records_1e9.jsonl ↓	7.4 MB	2026-10-10 00:07

status.json in full

{
 "tm": "1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "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, observe.json (the card), the kill files (tools/killreview.py) and the dashboard records · rebuild: python3 -B tools/card.py 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (the kill review: python3 -B tools/killreview.py 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, which also renders a derived kill's same-machine pictures)