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

`1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---`

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

How we proved it never halts

A countdown in which only safe blocks run out

It counts a binary number down, like an odometer running backward. The tape is a list of pairs, each like 1010…10 0101…01 0010: a block of 10s, a block of 01s, and one digit (0010 is a 0, 0001 a 1). On each trip the head goes from the left end to the first 1 digit and back, subtracting 1; every pair it reaches flips its digit and trades one 01 for one 10. About every second time the count reaches zero, the blocks are regrouped into new pairs, so growing and shrinking blocks swap roles, and a pair is added.

The danger is a block of 01s shrinking to nothing. At the first 1 digit that is a normal move: the pair fuses with the next one. Anywhere else the tape leaves the pattern, and some of those tapes halt. Parity decides which: a block whose length plus its digit is even can only run out at the first 1 digit.

The key idea: every block is one of two kinds for life. One kind shrinks in one countdown and grows in the next, and never runs out; every block with the wrong parity is of this kind. The other kind wears down and does run out, but always with the right parity, so it only fuses.

The proof turns this into a checklist of simple inequalities, checked at every second regrouping. If it holds at one, every move up to the next is one of nine known moves, none of which halts, and it holds again there. It holds after 78,710 steps, so the machine never halts.

The Rocq proof (checked against busycoq) proves the nine moves for all block lengths, replays the first 78,710 steps, and shows that a move-by-move version of the checklist holds there and survives every move.

#4local proof number

1,303lines of Rocq

71 sto compile

6/6automatic checks

Overview

In one sentence

Binary down-counter on a list of (10)^p(01)^q pairs; overflow re-pairs the list (TM21-like). 7 rules validated.

Submitted mechanism The tape is K(h; P; T) = 0^inf <A (10)^h 11001 [p_1,q_1,d_1] .. [p_L,q_L,d_L] T 0^inf, with pairs [p,q,d] = (10)^p (01)^q s(d), s(1) = 0001, s(0) = 0010. The digits form a binary number V, least significant next to the head. (submission/README.md, Mechanism)

Upstream: Kill claimed · PR #15merged 2026-10-13 12:25 UTC by ccz181078 · Sk1Class2_v1.v · TM2 · on Submissions →
Rocq proof: check_kill PASS · first Oct 10 07:06
1,303 lines · 62 KB .v · compile 71.1 s · coqchk pass · 0 axioms · PASS Oct 10 07:06 (re-run Oct 10 11:52)
· the .v file
Automatic review: 6 of 6 checks passtemplate: verify/SBCv6.v Module TM21 (loose template) · details in Proof →
Class: Skelet 1-like Class 2ours: Skelet 1-like Class 2 (sheet) · ours adds: binary down-counter on a list of (10)^p(01)^q pairs with overflow re-pairing (SBCv6 TM21 family) · high confidence
On the list: not on BB6_holdouts_663.txt (line 50 of the previous list) · historical 740 line 50
#3eqv ×1sim 1e15

Mechanism

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

How it works: 3 notes

Tape: (10)^h, marker 11001, then pairs (10)^p (01)^q, each ending in a digit block 0001 (=1) or 0010 (=0).
Each cycle (3 short bounces + 1 long sweep) subtracts 1 from that binary number; pairs the borrow passes get p+1, q-1.
At 0, End adds a tail; at the next 0, Overflow re-pairs the list and adds a pair (net ~1 per 2 epochs: width ~ t^0.5).

Figures for Checkpoint A

Fig 1 · One row per decrement, every 4th cell✓ Q1 ✓ Q2
One row per counter decrement, every 4th cell drawn. Watch the vertical and slanted colour edges, and where they kink.

Fig 2 · Three decrements up close, every step✓ Q3
Every step from counter value 12. Compare how far each long sweep reaches over three decrements.

Fig 3 · Every cell across two re-pairs, annotated✓ Q1 ✓ Q2 viewer ↗
The top-right corner of Fig 1, every cell drawn. Follow purple blocks and blue/orange borders down the rows.

Checkpoint A · all answered

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

Q1
check Fig 3 rows 8,319 to 17,139 (between the yellow RE-PAIR bands); each row is the tape at the start of one count-down step. A pair = a run of 10s (blue) then a run of 01s (orange); its digit block = the next 4 cells (purple), 0001 = 1, 0010 = 0. Expected: each purple block stays on the same 4 cells all the way down; only its one light (1) cell moves, one cell left or right, when the digit flips (0001 ↔ 0010): in pair 1's block every row (the zigzag), in pair 2's every other row, and in pair 3's once, at row 10,419. At row 13,983 pair 3 turns into the teal tail. Meanwhile each blue→orange border jumps 2 cells right on some rows: pair 1's on every row, pair 2's on every other row. The magnified box at the top shows one such step cell by cell. Is that what you see? (In Fig 1, zoomed far out, the purple blocks are the vertical edges and the borders the slanted ones.)
✓ you said: yes · Oct 10
“The purple block is a coherent column, but it shifts internally (light vs dark purple) and translates by one cell partway down; the single-cell checkerboard columns are what Q2 explains. So 'keeps its columns' is not literally true.”
Q2
check Fig 3 the two yellow RE-PAIR bands, above rows 8,319 and 19,436. Re-pairing = the tape is regrouped into new pairs and the counter restarts (here at 6); it happens when the counter (right margin) hits 0 for the second time. At the first 0 the step is End instead: it raises the counter (0 → 1 at row 6,366; 0 → 3 at row 13,983) and changes the right end, and the two Ends differ: '+ tail' (row 6,366) adds a 3-cell teal tail after the last pair, while 'pair 3 → tail' (row 13,983) absorbs pair 3 into the tail. Across each band, black dashed lines carry the old blue→orange borders down and purple dotted lines the middles of the old purple blocks. Expected: the dashed lines end on the new purple blocks of pairs 1 and 2, and the dotted lines end 1 cell left of the new borders of pairs 2 and 3 (pair 1's starts next to the old gold marker), so the two kinds of column swap roles. Re-pairing also adds a pair: the new pair 3's orange run takes over the old teal tail, and its purple block (the rightmost) sits just past where the tail ended, so no line leads to it. Is that what you see? (In Fig 1 each swap is a row where the vertical and slanted edges kink.)
✓ you said: yes · Oct 10
“Black dashed lines carry the old blue→orange borders down; purple dotted lines carry the old purple blocks down: that explains the checkerboard.”
Q3
check Fig 2 the long sweeps go deep, shallow, then medium as the counter goes 12 → 11 → 10 → 9. Does the sweep depth read as the borrow chain of a binary down-counter?
✓ you said: yes · Oct 10

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 (3)Fig 4–6: Blaze (speed mode), 100M steps · Snapshot every 1M steps, to 1 billion · bbchallenge default view, first 10,000 steps

Fig 6 · bbchallenge default view, first 10,000 stepsviewer ↗
The site's view: the tape grows mainly to the left; the right end barely moves.

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

rule	from ⟶ to	cases	steps	checked
Dec	0^∞ <A (10)^h 11001 Π_{i<k}[(10)^a_i (01)^b_i+1 0010] (10)^p (01)^q+1 0001 R ⟶ 0^∞ <A (10)^h+4 11001 Π_{i<k}[(10)^a_i+1 (01)^b_i 0001] (10)^p+1 (01)^q 0010 R	k=0..L-1 (borrow chain); b_i>=1, q>=1; any h mod 4; R = remaining pairs + any tail	—	✓48/48
DecMerge	0^∞ <A (10)^h 11001 Π_{i<k}[(10)^a_i (01)^b_i+1 0010] (10)^p (01) 0001 (10)^p2 (01)^q2 s R ⟶ 0^∞ <A (10)^h+4 11001 Π_{i<k}[(10)^a_i+1 (01)^b_i 0001] (10)^p+p2+3 (01)^q2 s R	q hits 0 on a 1->0 digit: fuse with next pair; last pair fuses into tail: (10)^p (01) 0001 (10)^t 1 -> (10)^(p+t+3) 1	—	✓36/36
End	0^∞ <A (10)^h 11001 Π_{i<L}[(10)^a_i (01)^b_i+1 0010] (10)^p (01)^q+1 0010 0^∞ ⟶ 0^∞ <A (10)^h+4 11001 Π_{i<L}[(10)^a_i+1 (01)^b_i 0001] (10)^p+1 (01)^q 0010 101 0^∞	all digits 0, no tail; b_i>=1, q>=1. q=0 (EndLast): last pair becomes tail (10)^(p+4) 1, validated 36/36	—	✓36/36
Ov	0^∞ <A (10)^h 11001 (10)^a_1+1 (01)^b_1 0010 Π_{j=2..L}[(10)^a_j (01)^b_j 0010] (10)^t 1 0^∞ ⟶ 0^∞ <A (10)² 11001 (10)^h+5 (01)^a_1 0010 Π_{j<L}[(10)^b_j (01)^a_(j+1) 0001] (10)^b_L (01)^t+1 0001 0^∞	all digits 0, tail present; a_1>=1; new counter value 2^(L+1)-2	—	✓36/36
X1	0^∞ <A (10)^h 11001 (10)^a_1+1 (01)^b_1 0010 Π_{j=2..L-2}[(10)^a_j (01)^b_j 0010] (10)^a (01) 0010 (10)^b (01) 0010 0^∞ ⟶ 0^∞ <A (10)² 11001 (10)^h+5 (01)^a_1 0010 Π_{j<L-2}[(10)^b_j (01)^a_(j+1) 0001] (10)^b_(L-2) (01)^a 0010 (101)² (01)^b+3 0^∞	End with the last two q = 1 (seen once, step 251,973,021)	—	✓30/30
X2	0^∞ <A (10)^h 11001 Π_{j<L}[(10)^a_j (01)^b_j+1 0010] (10)^p (01)^q+1 0010 (101)² (01)^k 0^∞ ⟶ 0^∞ <A (10)^h+4 11001 Π_{j<L}[(10)^a_j+1 (01)^b_j 0001] (10)^p+1 (01)^q 0010 (10)³ (01)^k 0001 0^∞	all digits 0 with tail (101)^2(01)^k; returns to the normal family	—	✓30/30

Compressed historythe tape as 0^∞ <A (10)^h 11001 (10)^p1 (01)^q1 s(d1) (10)^p2 (01)^q2 s(d2) ... (10)^pL (01)^qL s(dL) T 0^∞ [s(1)=0001, s(0)=0010; T = '' | (10)^t 1 | (101)² (01)^k] at 24 moments: where the rules are read off

0^∞ <A (10)^h 11001 (10)^p1 (01)^q1 s(d1) (10)^p2 (01)^q2 s(d2) ... (10)^pL (01)^qL s(dL) T 0^∞ [s(1)=0001, s(0)=0010; T = '' | (10)^t 1 | (101)² (01)^k]

step	`h`	`L`	`V=sum d_j 2^(j-1)`	`p1`	`q1`	`p2`	`q2`	`pL`	`qL`	`T`
1,845	2	2	2	11	11	10	2	10	2	-
4,610	2	2	2	23	14	7	16	7	16	-
8,319	2	3	6	23	26	10	9	14	2	-
19,436	2	3	6	47	32	16	15	4	20	-
34,137	2	4	14	47	56	22	21	18	2	-
78,710	2	4	14	95	68	34	33	1	24	-
137,547	2	5	30	95	116	46	45	22	2	-
276,384	2	4	14	159	132	78	65	6	43	-
368,693	2	5	30	95	180	110	89	41	2	-
598,490	2	5	30	191	140	134	133	3	47	-
868,551	2	6	62	191	236	94	157	45	2	-
1,637,772	2	5	30	383	284	142	141	14	84	-
2,053,945	2	6	62	191	428	238	165	82	2	-
3,050,262	2	6	62	383	284	334	285	11	88	-
4,178,299	2	7	126	383	476	190	381	86	2	-
7,335,144	2	7	126	767	572	286	285	8	92	-
11,309,893	2	8	254	767	956	382	381	90	2	-
23,109,954	2	8	254	1,535	1,148	574	573	5	96	-
38,479,639	2	9	510	1,535	1,916	766	765	94	2	-
84,867,492	2	9	510	3,071	2,300	1,150	1,149	2	100	-
145,833,457	2	10	1,022	3,071	3,836	1,534	1,533	98	2	-
252,225,526	2	9	254	4,095	4,092	2,814	2,045	28	63	(101)^2 (01)^102 [X1]
277,337,206	1,022	10	767	4,350	3,837	2,942	1,917	3	102	- [X2]
466,254,879	2	11	2,046	6,143	5,628	2,558	3,581	100	2	-

hlast 2

Llast 11

V=sum d_j 2^(j-1)last 2,046

p1last 6,143

q1last 5,628

p2last 2,558

q2last 3,581

pLlast 100

qLlast 2

Tlast -

not plottable

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

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

file: SBCv6.v:3702
module: TM21
machine: 1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE (11 transitions apart)
diff: 8 of 11 defined transitions differ under the best state renaming (no mirror); Sk1like_TC_v1/v2 machines differ in 8-9
note: Same architecture (pair list + counter sweeps + overflow re-pairing + finite tail states = TM21's LIncs/Ov/LH1-3), but not its shapes: from TM21's init config this machine halts in 4,539 steps. Sk1like_TC (eventual cycler via native_compute) doesn't fit.

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

Copy TM21's skeleton: pair-list datatype with digit tags; Dec/End/Ov/merge/X1/X2 as follow-chains of es/ind sweep lemmas over (10)^p(01)^q blocks (Longitudinal sideRLs like TM21's LIncs if sweeps are batched). Nonhalt via multistep_nonhalt + progress_nonhalt_cond with an LWF-style invariant: every q_j exceeds the borrows it gets before its digit next flips 0->1, plus a 3-state tail automaton (none / (10)^t 1 / (101)^2(01)^k).

▲Invariant: the far end has small margins (a far q shrinks by 3 per 2 epochs); excluding a bad merge (q->0 on a 0->1 digit) needs exact far-end bookkeeping. Simulation only so far (2^48 abstract cycles).
▲Size: TM21-style proof plus a tail automaton and 7 rule shapes, probably 15-30 KB.
▲Class 1 neighbour is being mined from a numbered Sk1 list; unknown whether that list covers Class 2 (memo Q3).

Stats & provenance10⁹ steps simulated · 67,343 cells · the status in full · files

simulated: 10⁹ steps
tape: 67,343 cells · 33,665 nonzeros
growth: left edge ~2.1*t^0.5 (doubling epochs); right edge almost static (157 -> 181 cells, 1e8 -> 1e9)
status now: check_kill PASS, independently re-verified (status.json, 2026-10-10)
observer's note: Mechanism found: 7 rules, 252/252 random-config checks; they reproduce all 8,374 canonical transitions to 1e9. Not a cryptid (linear arithmetic).
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v

Proof & checks

6/6 automatic checks pass

Kill 4 · Skelet 1-like Class 2 · the kill file 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v: 1303 lines, 138 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (loose template): verify/SBCv6.v Module TM21 · 3% 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

1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---

vs holdout list

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

Theorem

✓ Lemma nonhalt : ~ halts tm c0. L1268

check_kill

✓ PASS · 17/17 checks pass · compile 71.14 s · coqchk pass (24.69 s) · assumptions: 0 (closed) · 2026-10-10 18:52:37 UTC · submission/check_kill.txt

Checked .v

sha256 cfa603a314f65a81…

✓	1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v	`cfa603a314f65a81…` = checked
✓	submission/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v	`cfa603a314f65a81…` = 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`	63590 bytes, 1303 lines, 1484 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 23: TM_from_str "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---" == <tm> (41 bytes)
✓	`theorem_text`	line 1268: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 ([local working file]
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 71.1s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---") 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 (24.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).

loose template verify/SBCv6.v Module TM21 · detected from 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v line 4

3%of our lines identical to the template

2changed lines

1095added lines (ours only)

286template lines dropped

1 / 3 / 134items identical / adapted / new

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

It loosely follows SBCv6.v Module TM21 (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE): a pair list with counting sweeps and a re-pairing overflow.

Kept: a Fixpoint over the pair list as the configuration, the overflow as a list re-pairing (ovp/ovpX, as TM21's Ov), and multistep_nonhalt + progress_nonhalt_cond.
Changed: the macro step is one decrement, not TM21's whole-countdown LIncs. Here merges are routine and happen mid-countdown. The digits carry binary tags, and there is the X1/X2 tail detour. TM21's LWF (q >= 2^len, which rules out merges) is replaced by J. proof.md's per-cycle invariant INV+(e) (§3.8) appears inside J in projected form. J has no period lemma, and it does not need proof.md's L6 or L5'.

The file is 1,303 lines, about 4.2 times TM21's 308. proof.md §4 maps the informal proof 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 1129 lines

3% identical · 2 changed · 1095 added

template 320 lines

10% kept verbatim · 286 not in ours

our items 138

1 identical · 3 adapted · 134 new · 24 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 17–1303 (header comment 1–16 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_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 (1129 lines), 1383 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.	18	From BusyCoq Require Import Individual62.
2	Require Import ZifyNat Lia.	19	Require Import Arith Lia List.
3	Require Import ZArith.
4	Require Import String.	20	Require Import String.
5	Require Import List.
		21	Import ListNotations.
6	From BusyCoq Require Import Longitudinal.
8	Open Scope list.
⋯ 36 template-only lines (template 10–49), not in ours
50	[ eassumption \| ];
51	try esx ].
3704	Definition tm := Eval compute in (TM_from_str "1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE").	23	Definition tm := Eval compute in (TM_from_str "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---").
3706	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).	25	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
3707	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).	26	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
3709	Definition tm' := flip tm.
		28	Open Scope list.
3711	Notation "l <\| r" := (l <{{C}} [] *> r) (at level 30).
		30	Lemma ev_eq {c1 c2 c2'} : c1 -->* c2 -> c2 = c2' -> c1 -->* c2'.
3712	Notation "l \|> r" := (l <* [] {{E}}> r) (at level 30).
		31	Proof. intros H E. subst. exact H. Qed.
3714	Notation hL := (C,[]).
		33	Lemma prog_eq {c1 c2 c2'} : c1 -->+ c2 -> c2 = c2' -> c1 -->+ c2'.
3715	Notation hR := (E,[]).
		34	Proof. intros H E. subst. exact H. Qed.
3716	Notation hLR2 := [(hL,hR)].
		36	(** * Low-level sweeps (all by [es]).
3717	Notation hRL2 := [(hR,hL)].
		37	Paper words: pair [p,q,d] = (10)^p (01)^q s(d), s(1) = 0001, s(0) = 0010.
3719	Definition C0 n m := <[0;1]^^(n) <+ <[0;0;1] <+ <[0;1]^^m <+ <[1].
		38	During the long rightward sweep a passed pair [p,q+1,0] is left behind as
3720	Definition C1 n m := <[0;1]^^(n) <+ <[0;1;1] <+ <[0;1]^^m <+ <[1].
		39	region (paper) 0 (01)^p 110 (01)^q 11, the 0 being the boundary cell. *)
3722	Inductive LH := LH1\|LH2\|LH3.
		41	Lemma Start h r : 0inf <{{A}} [1;0]^^h > [1;1;0;0;1] > r -->+
3724	Definition toLH x :=
		42	0inf <* <[1;0]^^(4+h) <* <[1;1;1] <* [0] {{B}}> r.
3725	match x with
		43	Proof. es. Qed.
3726	\| LH1 => 0inf
		45	Lemma PassR l p q r : l <* [0] {{B}}> [1;0]^^p > [0;1]^^(S q) > [0;0;1;0] > r -->
3727	\| LH2 => 0inf <* <[1;1;0;1;0;1;1]
		46	l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^q <* <[1;1] <* [0] {{B}}> r.
3728	\| LH3 => 0inf <* <[1;1;1]
		47	Proof. es. Qed.
		49	Lemma Borrow l p q r : l {{B}}> [1;0]^^p > [0;1]^^(S (S q)) > [0;0;0;1] > r -->
		50	l <{{D}} [1;0]^^(S p) > [0;1]^^(S q) > [0;0;1;0] *> r.
		51	Proof. es. Qed.
		53	Lemma PassL l p q r : l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] <{{D}} r -->*
		54	l <* [0] <{{D}} [1;0]^^(S p) > [0;1]^^(S q) > [0;0;0;1] *> r.
		55	Proof. es. Qed.
		57	Lemma EndPh h r : 0inf <* <[1;0]^^(4+h) <* <[1;1;1] <* [0] <{{D}} r -->*
		58	0inf <{{A}} [1;0]^^(4+h) > [1;1;0;0;1] > r.
		59	Proof. es. Qed.
		61	Lemma EndT l p q : l <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] {{B}}> 0inf -->*
		62	l <{{D}} [1;0]^^(S p) > [0;1]^^(S q) > [0;0;1;0] > [1;0;1] > 0inf.
		63	Proof. es. Qed.
		65	Lemma EndLastT l p : l <* <[0;1]^^p <* <[1;1;0] <* <[1;1] <* [0] {{B}}> 0inf -->*
		66	l <{{D}} [1;0]^^(p+4) > [1] > 0inf.
		67	Proof. es. Qed.
		69	Lemma MergeB l p p' r : l {{B}}> [1;0]^^p > [0;1] > [0;0;0;1] > [1;0]^^p' > r -->*
		70	l <{{D}} [1;0]^^(p+p'+3) *> r.
		71	Proof. es. Qed.
		73	Lemma MergeE l p : l {{B}}> [1;0]^^p > [0;1] > [0;0;0;1] > 0inf -->
		74	l <{{D}} [1;0]^^(p+2) > [1] > 0inf.
		75	Proof. es. Qed.
		77	Lemma OvT l t : l <* [0] {{B}}> [1;0]^^t > [1] > 0inf -->*
		78	l <{{D}} [0;1]^^(S t) > [0;0;0;1] > 0inf.
		79	Proof. es. Qed.
		81	Lemma OvL l p q r : l <* [0] <* <[0;1]^^(S p) <* <[1;1;0] <* <[0;1]^^q <* <[1;1] <{{D}} r -->*
		82	l <{{D}} [0;1]^^(S p) > [0;0;0;1] > [1;0]^^(S q) *> r.
		83	Proof. es. Qed.
		85	Lemma OvEnd h p r : 0inf <* <[1;0]^^(4+h) <* <[1;1;1] <{{D}} [0;1]^^(S (S p)) > [0;0;0;1] > r -->*
		86	0inf <{{A}} [1;0]^^2 > [1;1;0;0;1] > [1;0]^^(h+5) > [0;1]^^(S p) > [0;0;1;0] *> r.
		87	Proof. es. Qed.
		89	Lemma X1Sw l p r : l <* [0] <* <[0;1]^^(S p) <* <[1;1;0] <* <[1;1] <* [0] <{{D}} r -->*
		90	l <{{D}} [0;1]^^(S p) > [0;0;1;0;1;0;1] > r.
		91	Proof. es. Qed.
		93	Lemma X2T l p q k : l <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] {{B}}> [1;0;1;1;0;1] > [0;1]^^(S k) > 0inf -->*
		94	l <{{D}} [1;0]^^(S p) > [0;1]^^(S q) > [0;0;1;0] > [1;0]^^3 > [0;1]^^(S k) > [0;0;0;1] > 0inf.
		95	Proof. es. Qed.
		97	(** * The family K (proof.md section 1) *)
		99	Definition sd (d : bool) : list Sym := if d then [0;0;0;1] else [0;0;1;0].
		101	Fixpoint RP (P : list (natnatbool)) (r : side) : side :=
		102	match P with
		103	\| [] => r
		104	\| (p,q,d) :: P' => [1;0]^^p > [0;1]^^q > sd d *> RP P' r
3729	end.	105	end.
3731	Notation LS := (list (nat*nat)).
		107	Inductive Tl := TN \| TA (t : nat) \| TB (k : nat).
3733	Fixpoint LC1(x:LS)(y:LH):side :=
		109	Definition RT (T : Tl) : side :=
3734	match x with	110	match T with
3735	\| [] => toLH y
		111	\| TN => 0inf
3736	\| (n,m)::t => LC1 t y <* C1 n m
		112	\| TA t => [1;0]^^t > [1] > 0inf
		113	\| TB k => [1;0;1;1;0;1] > [0;1]^^k > 0inf
3737	end.	114	end.
3739	Fixpoint LC0(x:LS)(y:LH):side :=
		116	Definition K (h : nat) (P : list (natnatbool)) (T : Tl) : Q * tape :=
3740	match x with
		117	0inf <{{A}} [1;0]^^h > [1;1;0;0;1] > RP P (RT T).
3741	\| [] => toLH y
		119	Definition pre (h : nat) : side := 0inf <* <[1;0]^^(4+h) <* <[1;1;1].
3742	\| (n,m)::t => LC0 t y <* C0 n m
		121	(** region left behind by the rightward sweep over pair (p,q,_) *)
		122	Definition reg (p q : nat) (l : side) : side :=
		123	l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(pred q) <* <[1;1].
		125	Fixpoint LP (Z : list (natnatbool)) (l : side) : side :=
		126	match Z with
		127	\| [] => l
		128	\| (p,q,d) :: Z' => LP Z' (reg p q l)
3743	end.	129	end.
3745	Inductive Ov: LS->LH->nat->LS->LH->Prop :=
		131	(** what the overflow sweep leaves for pair (p,q,_) *)
3746	\| Ov_1 m a:
		132	Fixpoint OvR (Z : list (natnatbool)) (r : side) : side :=
3747	m<>O ->
		133	match Z with
3748	Ov [(2,m)] LH1 a [(m,a)] LH2
		134	\| [] => r
3749	\| Ov_2 a:
		135	\| (p,q,d) :: Z' => [0;1]^^p > [0;0;0;1] > [1;0]^^q *> OvR Z' r
3750	Ov [] LH2 a [(2,a)] LH3
		136	end.
3751	\| Ov_3 a:
		138	Definition touch (x : natnatbool) : natnatbool :=
3752	Ov [] LH3 a [(2,a)] LH1
		139	let '(p,q,d) := x in (S p, pred q, negb d).
3753	\| Ov_S x y n m a x' y':
		141	Definition okR (x : natnatbool) : Prop := let '(p,q,d) := x in d = false /\ 1 <= q.
3754	Ov x y n x' y' ->
		142	Definition okL (x : natnatbool) : Prop := let '(p,q,d) := x in d = false /\ 2 <= q.
3755	m<>O ->
		143	Definition okO (x : natnatbool) : Prop := let '(p,q,d) := x in 1 <= p /\ 1 <= q.
3756	Ov (x<:(n,m)) y a (x'<:(m,a)) y'
		145	Lemma RP_app Z W r : RP (Z ++ W) r = RP Z (RP W r).
3757	.
3759	Lemma Ov_spec x y a x' y':
⋯ 2 template-only lines (template 3760–3761), not in ours
3762	LC1 x y <\| [0;1]^^(1+a) > [1] > r -->+
3763	LC0 x' y' \|> r.
3764	Proof.	146	Proof.
3765	intro H.
		147	induction Z as [\|[[p q] d] Z IH]; cbn; [reflexivity\|]. rewrite IH. reflexivity.
3766	induction H; intros.
3767	- destruct m. 1: lia.
⋯ 7 template-only lines (template 3768–3774), not in ours
3775	follow100 IHOv.
3776	es.
3777	Qed.	148	Qed.
3779	Definition RC n m := [0;1]^^(1+n) > [1] > [0;1]^^m *> 0inf.
		150	Lemma LP_app Z W l : LP (Z ++ W) l = LP W (LP Z l).
3781	Lemma RIncs k n m:
3782	sideRLs tm (hRL2^^k) (RC n m) (RC (k+n) (k+m)).
3783	Proof.	151	Proof.
3784	unfold RC.
		152	revert l. induction Z as [\|[[p q] d] Z IH]; intros l; cbn; [reflexivity\|]. apply IH.
3785	sideRLs_ind k.
3786	Qed.	153	Qed.
3788	Lemma Ov' x y a x' y' b:
		155	Lemma PassesR Z : Forall okR Z -> forall l r,
3789	Ov x y a x' y' ->
		156	l <* [0] {{B}}> RP Z r -->* LP Z l <* [0] {{B}}> r.
3790	LC1 x y <\| RC a b -->+
3791	LC0 x' y' <\| RC b 1.
3792	Proof.	157	Proof.
3793	unfold RC.
		158	induction Z as [\|[[p q] d] Z IH]; intros HZ l r; cbn [RP LP]; [finish\|].
3794	intro H.
		159	inversion HZ as [\|? ? Hx HZ']; subst; hnf in Hx; destruct Hx as [Hd Hq]; subst d.
3795	eapply Ov_spec in H.
		160	destruct q as [\|q]; [lia\|].
3796	follow10 H.
		161	eapply evstep_trans. { apply PassR. }
3797	es.
		162	apply (IH HZ' (reg p (S q) l) r).
3798	Qed.	163	Qed.
3800	Inductive LIncs: LS->LS->nat->Prop :=
		165	Lemma PassesL Z : Forall okL Z -> forall l r,
3801	\| LIncs_O:
		166	LP Z l <* [0] <{{D}} r -->* l <* [0] <{{D}} RP (map touch Z) r.
3802	LIncs [] [] 0
3803	\| LIncs_S x y k n m:
⋯ 4 template-only lines (template 3804–3808), not in ours
3809	LIncs x y k ->
3810	sideRLs tm' (hLR2^^k) (LC0 x z) (LC1 y z).
3811	Proof.	167	Proof.
3812	intros H.
		168	induction Z as [\|[[p q] d] Z IH]; intros HZ l r; cbn [RP LP map]; [finish\|].
3813	induction H.
		169	inversion HZ as [\|? ? Hx HZ']; subst; hnf in Hx; destruct Hx as [Hd Hq]; subst d.
3814	- esx.
		170	destruct q as [\|[\|q]]; [lia\|lia\|].
3815	- cbn[LC0]; cbn[LC1].
		171	eapply evstep_trans. { apply (IH HZ' (reg p (S (S q)) l)). }
3816	eapply segRLs_sideRLs_concat.
		172	unfold reg. cbn [pred]. apply PassL.
3817	2: apply IHLIncs.
3818	clear.
⋯ 12 template-only lines (template 3819–3830), not in ours
3831	simpl_tape; cbn.
3832	esx.
3833	Qed.	173	Qed.
3835	Definition S' '(x,y,z) := LC0 x y <\| RC z 1.
		175	Lemma OvPasses Z : Forall okO Z -> forall l r,
3837	Lemma BigStep x y z x0 x1 y0 k:
		176	LP Z l <{{D}} r -->* l <{{D}} OvR Z r.
3838	LIncs x x0 k ->
3839	Ov x0 y (k+z) x1 y0 ->
3840	S' (x,y,z) -->+
3841	S' (x1,y0,k+1).
3842	Proof.	177	Proof.
3843	unfold S'.
		178	induction Z as [\|[[p q] d] Z IH]; intros HZ l r; cbn [OvR LP]; [finish\|].
3844	intros I1 I2.
		179	inversion HZ as [\|? ? Hx HZ']; subst; hnf in Hx; destruct Hx as [Hp Hq].
3845	eapply LIncs_spec in I1.
		180	destruct p as [\|p]; [lia\|]. destruct q as [\|q]; [lia\|].
3846	eapply Ov' in I2.
		181	eapply evstep_trans. { apply (IH HZ' (reg (S p) (S q) l)). }
3847	epose proof (sideRLs_concat_1L (RIncs k _ _) I1) as I1'.
		182	unfold reg. cbn [pred]. apply OvL.
3848	follow I1'.
3849	apply I2.
3850	Qed.	183	Qed.
3852	Lemma init:
		185	Lemma okL_R Z : Forall okL Z -> Forall okR Z.
3853	c0 -->*
3854	S' (<[(2,2);(1%nat,3);(2,5)],LH1,4).
3855	Proof.	186	Proof.
3856	esx.
		187	intros H. eapply Forall_impl; [\|exact H]. intros [[p q] d] [H1 H2]. split; [exact H1 \| lia].
3857	Qed.	188	Qed.
3859	Lemma length_LIncs {x y k}:
		190	(** * Macro rules (proof.md section 2) *)
3860	LIncs x y k ->
		192	Lemma Dec h Z p q R T : Forall okL Z ->
3861	length y = length x.
		193	K h (Z ++ (p, S (S q), true) :: R) T -->+ K (4+h) (map touch Z ++ (S p, S q, false) :: R) T.
3862	Proof.	194	Proof.
3863	intros H.
		195	intros HZ. unfold K. rewrite !RP_app. cbn [RP sd].
3864	induction H; cbn; lia.
		196	eapply progress_evstep_trans. { apply Start. }
		197	eapply evstep_trans. { apply PassesR, okL_R, HZ. }
		198	eapply evstep_trans. { apply Borrow. }
		199	eapply evstep_trans. { apply (PassesL Z HZ). }
		200	apply EndPh.
3865	Qed.	201	Qed.
3867	Lemma LIncs_k x y k:
		203	Lemma DecMerge h Z p p' q' d' R T : Forall okL Z ->
3868	LIncs x y k ->
		204	K h (Z ++ (p, 1%nat, true) :: (p', q', d') :: R) T -->+ K (4+h) (map touch Z ++ (p+p'+3, q', d') :: R) T.
3869	k = 2^(length x)-1.
3870	Proof.	205	Proof.
3871	intros H.
		206	intros HZ. unfold K. rewrite !RP_app. cbn [RP sd].
3872	induction H; cbn; lia.
		207	eapply progress_evstep_trans. { apply Start. }
		208	eapply evstep_trans. { apply PassesR, okL_R, HZ. }
		209	eapply evstep_trans. { apply MergeB. }
		210	eapply evstep_trans. { apply (PassesL Z HZ). }
		211	apply EndPh.
3873	Qed.	212	Qed.
3875	Lemma length_Ov {x y a x' y'}:
		214	Lemma DecMergeTail h Z p t : Forall okL Z ->
3876	Ov x y a x' y' ->
		215	K h (Z ++ [(p, 1%nat, true)]) (TA t) -->+ K (4+h) (map touch Z) (TA (p+t+3)).
3877	length x' = length x + (match y with LH1 => 0 \| _ => 1 end).
3878	Proof.	216	Proof.
3879	intro H.
		217	intros HZ. unfold K. rewrite !RP_app. cbn [RP sd RT].
3880	induction H; cbn; trivial.
		218	eapply progress_evstep_trans. { apply Start. }
3881	rewrite IHOv; trivial.
		219	eapply evstep_trans. { apply PassesR, okL_R, HZ. }
		220	eapply evstep_trans. { apply MergeB. }
		221	eapply evstep_trans. { apply (PassesL Z HZ). }
		222	apply EndPh.
3882	Qed.	223	Qed.
3884	Inductive LWF: LS->LH->Prop :=
		225	Lemma DecMergeEmpty h Z p : Forall okL Z ->
3885	\| LWF_S x y n m
		226	K h (Z ++ [(p, 1%nat, true)]) TN -->+ K (4+h) (map touch Z) (TA (p+2)).
3886	(Ha:LWF x y)
3887	(Hb:2^(length x)<=m)
⋯ 24 template-only lines (template 3888–3914), not in ours
3915	Ov x0 y a x1 y0 /\
3916	LWF x1 y0.
3917	Proof.	227	Proof.
3918	intro H.
		228	intros HZ. unfold K. rewrite !RP_app. cbn [RP sd RT].
3919	gen a.
		229	eapply progress_evstep_trans. { apply Start. }
3920	induction H.
		230	eapply evstep_trans. { apply PassesR, okL_R, HZ. }
3921	- intros.
		231	eapply evstep_trans. { apply MergeE. }
3922	epose proof (IHLWF _ _) as [x0 [k [I1 [x1 [y0 [I2 I3]]]]]].
		232	eapply evstep_trans. { apply (PassesL Z HZ). }
3923	epose proof (LIncs_k _ _ _ I1); subst.
		233	apply EndPh.
3924	eexists _,_; split.
3925	{ applys_eq (LIncs_S _ _ _ n (m-(2^(length x)-1)) I1).
⋯ 51 template-only lines (template 3926–3976), not in ours
3977	2,3: cbn; lia.
3978	apply LWF_O_1.
3979	Qed.	234	Qed.
3981	Close Scope sym.
		236	Lemma Forall_snoc {A} (P : A -> Prop) Z x : Forall P Z -> P x -> Forall P (Z ++ [x]).
3983	Lemma nonhalt: ~halts tm c0.
		237	Proof. intros H1 H2. apply Forall_app. split; auto. Qed.
		239	Lemma EndR h Z p q : Forall okL Z ->
		240	K h (Z ++ [(p, S (S q), false)]) TN -->+ K (4+h) (map touch Z ++ [(S p, S q, false)]) (TA 1).
3984	Proof.	241	Proof.
3985	eapply multistep_nonhalt.
		242	intros HZ. unfold K.
3986	1: apply init.
		243	eapply progress_evstep_trans. { apply Start. }
3987	eapply progress_nonhalt_cond with (P:=fun '(x,y,z) => LWF x y /\ 1<=z).
		244	eapply evstep_trans. { apply PassesR. apply Forall_snoc; [apply okL_R, HZ \| cbn; split; [reflexivity \| lia]]. }
3988	2:{
		245	rewrite LP_app. cbn [LP RT]. unfold reg at 1. cbn [pred].
		246	eapply evstep_trans. { apply EndT. }
		247	eapply evstep_trans. { apply (PassesL Z HZ). }
		248	rewrite RP_app. apply EndPh.
		249	Qed.
		251	Lemma EndLast h Z p : Forall okL Z ->
		252	K h (Z ++ [(p, 1%nat, false)]) TN -->+ K (4+h) (map touch Z) (TA (p+4)).
		253	Proof.
		254	intros HZ. unfold K.
		255	eapply progress_evstep_trans. { apply Start. }
		256	eapply evstep_trans. { apply PassesR. apply Forall_snoc; [apply okL_R, HZ \| cbn; split; [reflexivity \| lia]]. }
		257	rewrite LP_app. cbn [LP RT]. unfold reg at 1. cbn [pred].
		258	eapply evstep_trans. { apply EndLastT. }
		259	eapply evstep_trans. { apply (PassesL Z HZ). }
		260	apply EndPh.
		261	Qed.
		263	Lemma X2 h Z p q k : Forall okL Z ->
		264	K h (Z ++ [(p, S (S q), false)]) (TB (S k)) -->+
		265	K (4+h) (map touch Z ++ [(S p, S q, false); (3%nat, S k, true)]) TN.
		266	Proof.
		267	intros HZ. unfold K.
		268	eapply progress_evstep_trans. { apply Start. }
		269	eapply evstep_trans. { apply PassesR. apply Forall_snoc; [apply okL_R, HZ \| cbn; split; [reflexivity \| lia]]. }
		270	rewrite LP_app. cbn [LP RT]. unfold reg at 1. cbn [pred].
		271	eapply evstep_trans. { apply X2T. }
		272	eapply evstep_trans. { apply (PassesL Z HZ). }
		273	rewrite RP_app. apply EndPh.
		274	Qed.
		276	Fixpoint ovp (q : nat) (Z : list (natnatbool)) (t : nat) : list (natnatbool) :=
		277	match Z with
		278	\| [] => [(q, S t, true)]
		279	\| (p',q',_) :: Z' => (q, p', true) :: ovp q' Z' t
		280	end.
		282	Lemma ovp_eq Z : forall q t, RP (ovp q Z t) 0inf = [1;0]^^q > OvR Z ([0;1]^^(S t) > [0;0;0;1] *> 0inf).
		283	Proof.
		284	induction Z as [\|[[p q'] d] Z IH]; intros q t; cbn [ovp RP OvR sd]; [reflexivity\|].
		285	rewrite IH. reflexivity.
		286	Qed.
		288	Lemma Ov h p1 q1 Z t : 1 <= q1 -> Forall okR Z -> Forall okO Z ->
		289	K h ((S (S p1), q1, false) :: Z) (TA t) -->+ K 2 ((h+5, S p1, false) :: ovp q1 Z t) TN.
		290	Proof.
		291	intros Hq HR HO. unfold K.
		292	eapply progress_evstep_trans. { apply Start. }
		293	eapply evstep_trans. { apply PassesR. constructor; [cbn; split; [reflexivity\|lia] \| exact HR]. }
		294	cbn [RT LP].
		295	eapply evstep_trans. { apply OvT. }
		296	eapply evstep_trans. { apply (OvPasses Z HO). }
		297	destruct q1 as [\|q1]; [lia\|]. unfold reg. cbn [pred].
		298	eapply evstep_trans. { apply OvL. }
		299	eapply ev_eq. { apply OvEnd. }
		300	cbn [RP sd RT]. rewrite ovp_eq. reflexivity.
		301	Qed.
		303	Fixpoint ovpX (q : nat) (Z : list (natnatbool)) (pa : nat) : list (natnatbool) :=
		304	match Z with
		305	\| [] => [(q, pa, false)]
		306	\| (p',q',_) :: Z' => (q, p', true) :: ovpX q' Z' pa
		307	end.
		309	Lemma ovpX_eq Z : forall q pa r, RP (ovpX q Z pa) r = [1;0]^^q > OvR Z ([0;1]^^pa > [0;0;1;0] *> r).
		310	Proof.
		311	induction Z as [\|[[p q'] d] Z IH]; intros q pa r; cbn [ovpX RP OvR sd]; [reflexivity\|].
		312	rewrite IH. reflexivity.
		313	Qed.
		315	Lemma tailB_eq n : [0;0;1;0;1;0;1] > [1;0]^^(S n) > [1] > 0inf = [0;0;1;0] > RT (TB n).
		316	Proof.
		317	cbn [RT]. cbn [lpow app]. cbn [Str_app]. f_equal. f_equal. f_equal. f_equal. f_equal. f_equal. f_equal.
		318	f_equal. f_equal. f_equal.
		319	change ([1;0]^^n > 1 >> 0inf = 1 >> [0;1]^^n > 0inf).
		320	apply lpow_rotate.
		321	Qed.
		323	Lemma X1 h p1 q1 Z pa pb : 1 <= q1 -> Forall okR Z -> Forall okO Z ->
		324	K h ((S (S p1), q1, false) :: Z ++ [(S pa, 1%nat, false); (pb, 1%nat, false)]) TN -->+
		325	K 2 ((h+5, S p1, false) :: ovpX q1 Z (S pa)) (TB (pb+3)).
		326	Proof.
		327	intros Hq HR HO. unfold K.
		328	eapply progress_evstep_trans. { apply Start. }
		329	eapply evstep_trans. { apply PassesR. constructor; [cbn; split; [reflexivity\|lia] \|].
		330	apply Forall_app. split; [exact HR\|]. repeat constructor; lia. }
		331	cbn [LP]. rewrite LP_app. cbn [LP RT]. unfold reg at 1. cbn [pred].
		332	eapply evstep_trans. { apply EndLastT. }
		333	unfold reg at 1. cbn [pred].
		334	eapply evstep_trans. { apply X1Sw. }
		335	eapply evstep_trans. { apply (OvPasses Z HO). }
		336	destruct q1 as [\|q1]; [lia\|]. unfold reg. cbn [pred].
		337	eapply evstep_trans. { apply OvL. }
		338	eapply ev_eq. { apply OvEnd. }
		339	cbn [RP sd]. rewrite ovpX_eq. replace (pb+4) with (S (pb+3)) by lia. rewrite tailB_eq. reflexivity.
		340	Qed.
		342	(** * Start (proof.md 3.7): c0 reaches K0 = K(2; (11,11,0); -) in 956 steps, and the base
		343	E-start after overflow 6, K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); -), in 78,710 steps.
		344	Both by direct execution ([esx]); the second takes about 30 s. *)
		346	Lemma init0 : c0 -->* K 2 [(11%nat, 11%nat, false)] TN.
		347	Proof. unfold K. cbn [RP RT sd]. esx. Qed.
		349	Definition base : list (natnatbool) :=
		350	[(95%nat, 68%nat, false); (34%nat, 33%nat, true); (10%nat, 15%nat, true); (1%nat, 24%nat, true)].
		352	Lemma init : c0 -->* K 2 base TN.
		353	Proof. unfold K, base. cbn [RP RT sd]. esx. Qed.
		356	(** * The invariant (round 2). Arithmetic layer, then the step lemma. *)
		358	Require Import ZifyNat.
		359	Import Coq.Init.Datatypes.
		361	Local Open Scope nat_scope.
		363	Notation tri := (nat * nat * bool)%type.
		364	Definition bv (d : bool) : nat := if d then 1 else 0.
		366	Fixpoint dv (P : list tri) : nat :=
		367	match P with
		368	\| [] => 0
		369	\| (_,_,d) :: P' => bv d + 2 * dv P'
		370	end.
		372	Definition dig (x : tri) : bool := let '(_,_,d) := x in d.
		373	Definition dig0 (x : tri) : Prop := dig x = false.
		377	Lemma dv_lt P : dv P < 2 ^ length P.
		378	Proof.
		379	induction P as [\|[[p q] d] P IH]; cbn [dv length]; [cbn; lia\|].
		380	rewrite Nat.pow_succ_r'. destruct d; cbn [bv]; lia.
		381	Qed.
		383	Lemma dv_zeros Z R : Forall dig0 Z -> dv (Z ++ R) = 2 ^ length Z * dv R.
		384	Proof.
		385	induction Z as [\|[[p q] d] Z IH]; intros HZ; cbn [app dv length]; [cbn; lia\|].
		386	inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d. rewrite IH by exact HZ'.
		387	rewrite Nat.pow_succ_r'. cbn [bv]. nia.
		388	Qed.
		390	Lemma dv_tz Z R : Forall dig0 Z -> dv (map touch Z ++ R) + 1 = 2 ^ length Z + 2 ^ length Z * dv R.
		391	Proof.
		392	induction Z as [\|[[p q] d] Z IH]; intros HZ; cbn [map app dv length touch]; [cbn; lia\|].
		393	inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d. cbn [negb bv].
		394	specialize (IH HZ'). rewrite Nat.pow_succ_r'. nia.
		395	Qed.
		397	(** every element, with its 1-based index and the list to its right *)
		398	Fixpoint AllI (Pr : nat -> tri -> list tri -> Prop) (i : nat) (P : list tri) : Prop :=
		399	match P with
		400	\| [] => True
		401	\| x :: Y => Pr i x Y /\ AllI Pr (S i) Y
		402	end.
		404	Lemma AllI_app Pr Z : forall i R, AllI Pr i (Z ++ R) -> AllI Pr (i + length Z) R.
		405	Proof.
		406	induction Z as [\|x Z IH]; intros i R H; cbn [app length] in *.
		407	- rewrite Nat.add_0_r. exact H.
		408	- destruct H as [_ H]. replace (i + S (length Z)) with (S i + length Z) by lia. apply IH, H.
		409	Qed.
		411	Lemma AllI_mono (Pr Pr' : nat -> tri -> list tri -> Prop) P : forall i,
		412	(forall j x Y, i <= j -> Pr j x Y -> Pr' j x Y) -> AllI Pr i P -> AllI Pr' i P.
		413	Proof.
		414	induction P as [\|x P IH]; intros i Hm H; cbn in *; [exact I\|].
		415	destruct H as [H1 H2]. split; [apply Hm; [lia \| exact H1]\|].
		416	apply IH; [\|exact H2]. intros j y Y Hj. apply Hm. lia.
		417	Qed.
		419	Lemma AllI_shift (Pr Pr' : nat -> tri -> list tri -> Prop) P : forall i,
		420	(forall j x Y, i <= j -> Pr (S j) x Y -> Pr' j x Y) -> AllI Pr (S i) P -> AllI Pr' i P.
		421	Proof.
		422	induction P as [\|x P IH]; intros i Hm H; cbn in *; [exact I\|].
		423	destruct H as [H1 H2]. split; [apply Hm; [lia \| exact H1]\|].
		424	apply IH; [\|exact H2]. intros j y Y Hj. apply Hm. lia.
		425	Qed.
		427	(** the touched prefix Z (all digits 0) of a rule; R becomes R' *)
		428	Lemma AllI_touchZ (Pr Pr' : nat -> tri -> list tri -> Prop) R R' : forall Z i,
		429	Forall dig0 Z ->
		430	(forall j p q Zr, Forall dig0 Zr -> j + S (length Zr) = i + length Z ->
		431	Pr j (p,q,false) (Zr ++ R) -> Pr' j (S p, pred q, true) (map touch Zr ++ R')) ->
		432	AllI Pr i (Z ++ R) -> AllI Pr' (i + length Z) R' -> AllI Pr' i (map touch Z ++ R').
		433	Proof.
		434	induction Z as [\|[[p q] d] Z IH]; intros i HZ Hob HA HR; cbn [app map length] in *.
		435	- rewrite Nat.add_0_r in HR. exact HR.
		436	- inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d. destruct HA as [H1 H2].
		437	cbn [touch negb]. split.
		438	+ apply Hob; [exact HZ' \| lia \| exact H1].
		439	+ apply IH; [exact HZ' \| \| exact H2 \| ].
		440	* intros j p' q' Zr HZr Hj. apply Hob; [exact HZr \| lia].
		441	* replace (S i + length Z) with (i + S (length Z)) by lia. exact HR.
		442	Qed.
		444	(** * The per-pair clause. n = number of pairs to the right, w = 2^n, tv = value of the digits
		445	from this pair to the top (this pair least significant, so tv = d mod 2). Rt = tv + (phase
		446	term) is the number of touches the pair still gets before the next re-pairing if no merge
		447	happens; p + Rt and q - Rt are invariant under touches. *)
		449	Inductive phase := E1 \| E2 \| E1t \| E2t \| T0 \| L1 \| L2 \| LX.
		451	(** clauses that depend on n (not on the index) *)
		452	Definition PN (ph : phase) (c4 : bool) (p q n tv : nat) : Prop :=
		453	match ph with
		454	\| E1 => match n with
		455	\| 0 => q >= tv + 2 ^ n + 1 /\ p + tv + 2 ^ n >= 3
		456	\| S _ => q >= tv + 3 * 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv + 2 ^ n >= 3 * 2 ^ n
		457	end
		458	\| E2 => match n with
		459	\| 0 => q >= tv + 1 /\ p + tv >= 3
		460	\| S _ => q >= tv + 2 * 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv >= 3 * 2 ^ n
		461	end
		462	\| E1t => match n with
		463	\| 0 => q >= tv + 2 ^ n + 1 /\ p + tv + 2 ^ n = 5
		464	\| S _ => q >= tv + 2 * 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv + 2 ^ n >= 3 * 2 ^ n
		465	end
		466	\| E2t => match n with
		467	\| 0 => q >= tv + 1 /\ p + tv = 5
		468	\| S _ => q >= tv + 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv >= 3 * 2 ^ n
		469	end
		470	\| T0 => q >= tv + 7 * 2 ^ n + 1 /\ p + tv + 5 * 2 ^ n >= 6 * 2 ^ n /\
		471	match n with
		472	\| 0 => tv = 0 /\ p mod 2 = 0
		473	\| S _ => (p + tv) mod 2 = 1
		474	end
		475	\| L1 => q + 2 ^ n >= tv + 2 /\
		476	match n with
		477	\| 0 => q = tv + 2 ^ n
		478	\| 1 => p + tv + 2 ^ n >= (if c4 then 4 else 5) * 2 ^ n /\
		479	(q >= tv + 2 ^ n + 1 \/ (q + tv) mod 2 = 0) /\ (if c4 then q = tv + 2 ^ n else True)
		480	\| S (S _) => p + tv + 2 ^ n >= (if c4 then 4 else 5) * 2 ^ n /\ (q + tv) mod 2 = 0
		481	end
		482	\| LX => match n with
		483	\| 0 => q = tv + 1
		484	\| 1 => p + tv >= 4 * 2 ^ n /\ q = tv + 1
		485	\| S (S _) => p + tv >= 4 * 2 ^ n /\ (q + tv) mod 2 = 0
		486	end
		487	\| L2 => p + tv >= (if c4 then 4 else 5) * (2 * 2 ^ n) /\
		488	match n with
		489	\| 0 => (q >= tv + 1 \/ (q + tv) mod 2 = 0) /\ (if c4 then q = tv else True)
		490	\| S _ => (q + tv) mod 2 = 0
		491	end
		492	end.
		494	(** clauses for pairs 1 and 2 (h only matters for pair 1) *)
		495	Definition PI (ph : phase) (h i p q n tv : nat) : Prop :=
		496	match i with
		497	\| 1 => h mod 2 = 0 /\
		498	match ph with
		499	\| E1 \| E1t => 2 <= n /\ p + tv + 2 ^ n + 3 >= 11 * 2 ^ n /\ h + 4 * (tv + 2 ^ n) + 6 >= 12 * 2 ^ n
		500	\| E2 \| E2t => 2 <= n /\ p + tv + 3 >= 11 * 2 ^ n /\ h + 4 * tv + 6 >= 12 * 2 ^ n
		501	\| T0 => 2 <= n /\ p + tv + 5 * 2 ^ n + 3 >= 22 * 2 ^ n /\ h + 4 * (tv + 5 * 2 ^ n) + 6 >= 24 * 2 ^ n
		502	\| L1 => 2 <= n /\ q >= tv + 3 * 2 ^ n /\ h + 4 * (tv + 2 ^ n) + 6 >= 8 * 2 ^ n
		503	\| LX => 3 <= n /\ q >= tv + 2 * 2 ^ n /\ h + 4 * tv + 6 >= 8 * 2 ^ n
		504	\| L2 => 1 <= n /\ q >= tv + 4 * 2 ^ n /\ h + 4 * tv + 6 >= 16 * 2 ^ n
		505	end
		506	\| 2 => match ph with
		507	\| E1 \| E1t => p + tv + 2 ^ n + 1 >= 7 * 2 ^ n
		508	\| E2 \| E2t => p + tv + 1 >= 7 * 2 ^ n
		509	\| T0 => p + tv + 5 * 2 ^ n + 1 >= 14 * 2 ^ n
		510	\| L1 => q >= tv + 2 ^ n + 1
		511	\| LX \| L2 => q >= tv + 1
		512	end
		513	\| _ => True
		514	end.
		516	Definition PC (ph : phase) (c4 : bool) (h i p q n tv : nat) : Prop :=
		517	1 <= p /\ 1 <= q /\ PN ph c4 p q n tv /\ PI ph h i p q n tv.
		519	Definition Lift (Pr : nat -> nat -> nat -> nat -> nat -> Prop) (i : nat) (x : tri) (Y : list tri) : Prop :=
		520	let '(p,q,d) := x in Pr i p q (length Y) (dv (x :: Y)).
		522	Definition PCx (ph : phase) (c4 : bool) (h : nat) := Lift (PC ph c4 h).
		524	Ltac dP := unfold PC, PN, PI in *.
		525	Ltac unfL := unfold PCx, Lift in ; cbv beta iota in .
		526	Ltac unfLg := unfold PCx, Lift; cbv beta iota.
		527	Ltac unfLh H := unfold PCx, Lift in H; cbv beta iota in H.
		528	Ltac splitH := repeat match goal with H : _ /\ _ \|- _ => destruct H end.
		529	Ltac cr := cbn - [Nat.modulo] in *; splitH; repeat split; try lia.
		531	Lemma pow_pos n : 1 <= 2 ^ n.
		532	Proof. pose proof (Nat.pow_nonzero 2 n). lia. Qed.
		534	(** a touch (every touched pair of a Dec step) *)
		535	Lemma ob_touch ph c4 h i p q n tv : 1 <= tv -> 2 <= q ->
		536	PC ph c4 h i p q n tv -> PC ph c4 (4 + h) i (S p) (pred q) n (tv - 1).
		537	Proof.
		538	intros Ht Hq [H1 [H2 [HN HI]]]. pose proof (pow_pos n). split; [lia\|]. split; [lia\|]. split.
		539	- clear HI. unfold PN in *. destruct ph; try destruct c4; destruct n as [\|[\|n]]; cr.
		540	- clear HN. unfold PI in *. destruct i as [\|[\|[\|i]]]; try exact I; destruct ph; cr.
		541	Qed.
		543	Lemma pow_S n : 2 ^ S n = 2 * 2 ^ n.
		544	Proof. reflexivity. Qed.
		546	Ltac prePC := match goal with H : PC _ _ _ _ _ _ _ _ \|- _ => destruct H as (Hp & Hq0 & HN & HI) end;
		547	split; [lia\|]; split; [lia\|]; split.
		549	(** a pair left of a DecMerge (L phases): n+1 -> n pairs to the right,
		550	tv = u + 2U -> u - 1 + U with u = 2^a (a >= 1), U = u * H *)
		551	Lemma ob_merge ph c4 h i p q n u U :
		552	(ph = L1 \/ ph = L2 \/ ph = LX) ->
		553	1 <= n -> 2 <= u -> u mod 2 = 0 -> U mod 2 = 0 -> U + u <= 2 * 2 ^ n ->
		554	(ph = L1 -> U + u <= 2 ^ n) -> (ph = LX -> 2 <= n) -> (ph = L1 -> c4 = true -> 2 <= n) ->
		555	(i = 1 -> 2 <= n) -> (ph = LX -> i = 1 -> 3 <= n) -> 2 <= q ->
		556	PC ph c4 h i p q (S n) (u + 2 * U) -> PC ph c4 (4 + h) i (S p) (pred q) n (u - 1 + U).
		557	Proof.
		558	intros Hph Hn Hu Hu2 HU2 HUu HL1 HLX Hc4 Hi1 HiX Hq H. pose proof (pow_pos n).
		559	prePC.
		560	- clear HI. unfold PN in . repeat rewrite pow_S in .
		561	destruct Hph as [-> \| [-> \| ->]]; try destruct c4; destruct n as [\|[\|n]]; cr.
		562	- clear HN. unfold PI in . repeat rewrite pow_S in .
		563	destruct i as [\|[\|[\|i]]]; try exact I; destruct Hph as [-> \| [-> \| ->]]; cr.
		564	Qed.
		566	(** a pair left of a DecMergeTail (L2): tv = 2^(n+1) -> 2^(n+1) - 1, and c4 is cleared *)
		567	Lemma ob_mt c4 h i p q n : 2 <= q -> (i = 1 -> 1 <= n) ->
		568	PC L2 c4 h i p q (S n) (2 * 2 ^ n) -> PC L2 false (4 + h) i (S p) (pred q) n (2 * 2 ^ n - 1).
		569	Proof.
		570	intros Hq Hi1 H. pose proof (pow_pos n). prePC.
		571	- clear HI. unfold PN in . repeat rewrite pow_S in . destruct c4; destruct n as [\|n]; cr.
		572	- clear HN. unfold PI in . repeat rewrite pow_S in . destruct i as [\|[\|[\|i]]]; try exact I; cr.
		573	Qed.
		575	(** the fused pair inherits the right pair's suffix *)
		576	Lemma ob_fuse ph c4 h h' k p p' q' n tv : (ph = L1 \/ ph = L2 \/ ph = LX) -> 3 <= k ->
		577	PC ph c4 h (S k) p' q' n tv -> PC ph c4 h' k (p + p' + 3) q' n tv.
		578	Proof.
		579	intros Hph Hk H. pose proof (pow_pos n). prePC.
		580	- clear HI. unfold PN in *. destruct Hph as [-> \| [-> \| ->]]; try destruct c4; destruct n as [\|[\|n]]; cr.
		581	- unfold PI. destruct k as [\|[\|[\|k]]]; try lia; exact I.
		582	Qed.
		584	(** pairs far from the head: the index and h do not matter *)
		585	Lemma ob_far ph c4 h h' i j p q n tv : 3 <= i -> 3 <= j ->
		586	PC ph c4 h i p q n tv -> PC ph c4 h' j p q n tv.
		587	Proof.
		588	intros Hi Hj [H1 [H2 [H3 _]]]. split; [lia\|]. split; [lia\|]. split; [exact H3\|].
		589	unfold PI. destruct j as [\|[\|[\|j]]]; try lia; exact I.
		590	Qed.
		592	(** End (E1 -> E2, E1t -> E2t) *)
		593	Definition endtr (ph ph' : phase) : Prop := (ph = E1 /\ ph' = E2) \/ (ph = E1t /\ ph' = E2t).
		595	Lemma ob_end ph ph' h i p q n : endtr ph ph' -> 1 <= n -> 2 <= q ->
		596	PC ph false h i p q n 0 -> PC ph' false (4 + h) i (S p) (pred q) n (2 ^ n - 1).
		597	Proof.
		598	intros Hph Hn Hq H. pose proof (pow_pos n). prePC.
		599	- clear HI. unfold PN in *. destruct Hph as [[-> ->]\|[-> ->]]; destruct n as [\|n]; cr.
		600	- clear HN. unfold PI in *. destruct i as [\|[\|[\|i]]]; try exact I; destruct Hph as [[-> ->]\|[-> ->]]; cr.
		601	Qed.
		603	Lemma ob_end_top ph ph' h i p q : endtr ph ph' -> 3 <= i ->
		604	PC ph false h i p (S (S q)) 0 0 -> PC ph' false (4 + h) i (S p) (S q) 0 0.
		605	Proof.
		606	intros Hph Hi H. prePC.
		607	- clear HI. unfold PN in *. destruct Hph as [[-> ->]\|[-> ->]]; cr.
		608	- unfold PI. destruct i as [\|[\|[\|i]]]; try lia; exact I.
		609	Qed.
		611	(** EndLast (L1 -> L2) *)
		612	Lemma ob_endlast c4 h i p q n : 2 <= q ->
		613	PC L1 c4 h i p q (S n) 0 -> PC L2 c4 (4 + h) i (S p) (pred q) n (2 * 2 ^ n - 1).
		614	Proof.
		615	intros Hq H. pose proof (pow_pos n). prePC.
		616	- clear HI. unfold PN in . repeat rewrite pow_S in . destruct c4; destruct n as [\|n]; cr.
		617	- clear HN. unfold PI in . repeat rewrite pow_S in . destruct i as [\|[\|[\|i]]]; try exact I; cr.
		618	Qed.
		620	(** X2 (T0 -> E1t) *)
		621	Lemma ob_x2 h i p q n : 1 <= n -> 2 <= q ->
		622	PC T0 false h i p q n 0 -> PC E1t false (4 + h) i (S p) (pred q) (S n) (3 * 2 ^ n - 1).
		623	Proof.
		624	intros Hn Hq H. pose proof (pow_pos n). prePC.
		625	- clear HI. unfold PN in . repeat rewrite pow_S in . destruct n as [\|n]; cr.
		626	- clear HN. unfold PI in . repeat rewrite pow_S in . destruct i as [\|[\|[\|i]]]; try exact I; cr.
		627	Qed.
		629	Lemma ob_x2_top h i p q : 3 <= i ->
		630	PC T0 false h i p (S (S q)) 0 0 -> PC E1t false (4 + h) i (S p) (S q) 1 2.
		631	Proof.
		632	intros Hi H. prePC.
		633	- clear HI. unfold PN in *. cr.
		634	- unfold PI. destruct i as [\|[\|[\|i]]]; try lia; exact I.
		635	Qed.
		637	Lemma ob_x2_new h i k : 3 <= i -> 3 <= k -> PC E1t false h i 3 k 0 1.
		638	Proof.
		639	intros Hi Hk. split; [lia\|]. split; [lia\|]. split.
		640	- unfold PN. cr.
		641	- unfold PI. destruct i as [\|[\|[\|i]]]; try lia; exact I.
		642	Qed.
		644	(** Ov (E2 -> L1/LX, E2t -> L1 with c4, L2 -> E1). Xp: condition on the old far p (= x). *)
		645	Definition ovtr (ph ph' : phase) (c4' : bool) (Xp : nat -> Prop) : Prop :=
		646	(ph = E2 /\ ph' = L1 /\ c4' = false /\ Xp = (fun x => x <> 4)) \/
		647	(ph = E2 /\ ph' = LX /\ c4' = false /\ Xp = (fun x => x = 4)) \/
		648	(ph = E2t /\ ph' = L1 /\ c4' = true /\ Xp = (fun _ => True)) \/
		649	(ph = L2 /\ ph' = E1 /\ c4' = false /\ Xp = (fun _ => True)).
		651	Lemma ob_ov_head ph ph' c4' Xp h p1 q1 n : ovtr ph ph' c4' Xp ->
		652	PC ph false h 1 (S (S p1)) q1 n 0 -> PC ph' c4' 2 1 (h + 5) (S p1) (S n) (2 * (2 * 2 ^ n) - 2).
		653	Proof.
		654	intros Htr H. pose proof (pow_pos n). prePC.
		655	- unfold PN, PI in . repeat rewrite pow_S in .
		656	destruct Htr as [(-> & -> & -> & _)\|[(-> & -> & -> & _)\|[(-> & -> & -> & _)\|(-> & -> & -> & _)]]];
		657	destruct n as [\|[\|n]]; cr.
		658	- unfold PN, PI in . repeat rewrite pow_S in .
		659	destruct Htr as [(-> & -> & -> & _)\|[(-> & -> & -> & _)\|[(-> & -> & -> & _)\|(-> & -> & -> & _)]]];
		660	destruct n as [\|[\|n]]; cr.
		661	Qed.
		663	Lemma ob_ov_step ph ph' c4' Xp h i pp q p' q' m : ovtr ph ph' c4' Xp -> 1 <= i ->
		664	PC ph false h i pp q (S m) 0 -> PC ph false h (S i) p' q' m 0 -> (m = 0 -> Xp p') ->
		665	PC ph' c4' 2 (S i) q p' (S m) (2 * (2 * 2 ^ m) - 1).
		666	Proof.
		667	intros Htr Hi H H' HX. pose proof (pow_pos m). destruct H as (Hp & Hq & HN & HI).
		668	destruct H' as (Hp' & Hq' & HN' & HI').
		669	split; [lia\|]. split; [lia\|]. split.
		670	- clear HI HI'. unfold PN in . repeat rewrite pow_S in .
		671	destruct Htr as [(-> & -> & -> & ->)\|[(-> & -> & -> & ->)\|[(-> & -> & -> & ->)\|(-> & -> & -> & ->)]]];
		672	destruct m as [\|[\|m]]; cr.
		673	- unfold PI. destruct i as [\|[\|i]]; [lia\| \|exact I].
		674	unfold PN, PI in . repeat rewrite pow_S in .
		675	destruct Htr as [(-> & -> & -> & ->)\|[(-> & -> & -> & ->)\|[(-> & -> & -> & ->)\|(-> & -> & -> & ->)]]];
		676	destruct m as [\|[\|m]]; cr.
		677	Qed.
		679	Lemma ob_ov_base ph ph' c4' Xp h i pp q t : ovtr ph ph' c4' Xp -> 1 <= i ->
		680	(ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
		681	PC ph false h i pp q 0 0 -> PC ph' c4' 2 (S i) q (S t) 0 1.
		682	Proof.
		683	intros Htr Hi Ht1 Ht2 H. unfold PC in H. splitH. split; [lia\|]. split; [lia\|].
		684	unfold PN, PI in *.
		685	destruct Htr as [(-> & -> & -> & ->)\|[(-> & -> & -> & ->)\|[(-> & -> & -> & ->)\|(-> & -> & -> & ->)]]];
		686	destruct i as [\|[\|[\|i]]]; cr; try (specialize (Ht2 ltac:(discriminate)); lia);
		687	specialize (Ht1 eq_refl); lia.
		688	Qed.
		690	(** X1 (LX -> T0) *)
		691	Lemma ob_x1_head h p1 q1 n :
		692	PC LX false h 1 (S (S p1)) q1 (S (S n)) 0 -> PC T0 false 2 1 (h + 5) (S p1) (S n) (2 * 2 ^ n - 2).
		693	Proof.
		694	intros H. pose proof (pow_pos n). prePC; unfold PN, PI in ; repeat rewrite pow_S in ;
		695	destruct n as [\|[\|n]]; cr.
		696	Qed.
		698	Lemma ob_x1_step h i pp q p' q' m : 1 <= i ->
		699	PC LX false h i pp q (S (S (S m))) 0 -> PC LX false h (S i) p' q' (S (S m)) 0 ->
		700	PC T0 false 2 (S i) q p' (S m) (2 * 2 ^ m - 1).
		701	Proof.
		702	intros Hi H H'. pose proof (pow_pos m). unfold PC in H, H'. splitH. split; [lia\|]. split; [lia\|].
		703	unfold PN, PI in . repeat rewrite pow_S in . destruct m as [\|m]; destruct i as [\|[\|[\|i]]]; cr.
		704	Qed.
		706	Lemma ob_x1_base h i pp q pa : 1 <= i ->
		707	PC LX false h i pp q 2 0 -> PC LX false h (S i) (S pa) 1 1 0 -> PC T0 false 2 (S i) q (S pa) 0 0.
		708	Proof.
		709	intros Hi H H'. unfold PC in H, H'. splitH. split; [lia\|]. split; [lia\|].
		710	unfold PN, PI in *. destruct i as [\|[\|[\|i]]]; cr.
		711	Qed.
		713	(** * List-level preservation, one lemma per rule *)
		715	Lemma dv_zero Z : Forall dig0 Z -> dv Z = 0.
		716	Proof. intros H. pose proof (dv_zeros Z [] H). rewrite app_nil_r in H0. cbn in H0. lia. Qed.
		718	Lemma dv_tz' Z R : Forall dig0 Z -> dv (map touch Z ++ R) = 2 ^ length Z - 1 + 2 ^ length Z * dv R.
		719	Proof. intros H. pose proof (dv_tz Z R H). lia. Qed.
		721	Lemma ovp_len q Z t : length (ovp q Z t) = S (length Z).
		722	Proof. revert q. induction Z as [\|[[p q'] d] Z IH]; intros q; cbn; [reflexivity\|]. rewrite IH. reflexivity. Qed.
		724	Lemma ovp_dv q Z t : dv (ovp q Z t) + 1 = 2 ^ S (length Z).
		725	Proof.
		726	revert q. induction Z as [\|[[p q'] d] Z IH]; intros q; cbn [ovp dv bv length]; [cbn; lia\|].
		727	specialize (IH q'). rewrite (pow_S (S (length Z))). lia.
		728	Qed.
		730	Lemma ovpX_len q Z pa : length (ovpX q Z pa) = S (length Z).
		731	Proof. revert q. induction Z as [\|[[p q'] d] Z IH]; intros q; cbn; [reflexivity\|]. rewrite IH. reflexivity. Qed.
		733	Lemma ovpX_dv q Z pa : dv (ovpX q Z pa) + 1 = 2 ^ length Z.
		734	Proof.
		735	revert q. induction Z as [\|[[p q'] d] Z IH]; intros q; cbn [ovpX dv bv length]; [cbn; lia\|].
		736	specialize (IH q'). rewrite (pow_S (length Z)). lia.
		737	Qed.
		739	Fixpoint lastOK (Xp : nat -> Prop) (Z : list tri) : Prop :=
		740	match Z with
		741	\| [] => True
		742	\| [(p,_,_)] => Xp p
		743	\| _ :: Z' => lastOK Xp Z'
		744	end.
		746	Lemma lastOK_cons Xp p q d Z : lastOK Xp ((p,q,d) :: Z) -> (Z = [] -> Xp p) /\ lastOK Xp Z.
		747	Proof. destruct Z as [\|z Z]; cbn; [tauto\|]. intros H. split; [discriminate \| exact H]. Qed.
		749	Lemma lastOK_dec Z : lastOK (fun x => x = 4) Z \/ lastOK (fun x => x <> 4) Z.
		750	Proof.
		751	induction Z as [\|[[p q] d] Z IH]; [left; exact I\|].
		752	destruct Z as [\|z Z]; [cbn; lia \| exact IH].
		753	Qed.
		755	Lemma AllI_ovp ph ph' c4' Xp h t : ovtr ph ph' c4' Xp -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
		756	forall Z i pp q, 1 <= i -> Forall dig0 Z -> lastOK Xp Z -> PC ph false h i pp q (length Z) 0 ->
		757	AllI (PCx ph false h) (S i) Z -> AllI (PCx ph' c4' 2) (S i) (ovp q Z t).
		758	Proof.
		759	intros Htr Ht1 Ht2. induction Z as [\|[[p' q'] d'] Z IH]; intros i pp q Hi HZ HX H HA.
		760	- cbn [ovp AllI]. split; [\|exact I]. unfL. cbn [length dv bv].
		761	eapply ob_ov_base; eauto.
		762	- cbn [ovp AllI]. inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d'.
		763	destruct HA as [Hh HA]. apply lastOK_cons in HX. destruct HX as [HX1 HX2].
		764	unfL. cbn [length] in H. rewrite dv_zero in Hh by (constructor; [reflexivity \| exact HZ']).
3989	split.	765	split.
3990	- apply LWF_S. 2,3: cbn; lia.
		766	+ unfL. rewrite ovp_len.
3991	apply LWF_S. 2,3: cbn; lia.
		767	replace (dv ((q, p', true) :: ovp q' Z t)) with (2 * (2 * 2 ^ length Z) - 1)
3992	apply LWF_O_1.
		768	by (cbn [dv bv]; pose proof (ovp_dv q' Z t) as E; rewrite pow_S in E; lia).
3993	- lia.
		769	eapply ob_ov_step; eauto. intros E. apply HX1. destruct Z; [reflexivity \| discriminate].
3994	}
		770	+ apply (IH (S i) p'); auto.
3995	intros [[x y] z] [HP HP0].
		771	Qed.
3996	epose proof (LWF_spec _ _ (2^len x-1+z) HP _) as [x0 [k [I1 [x1 [y0 [I2 I3]]]]]].
		773	Lemma AllI_ovpX h pa pb : forall Z i pp q, 1 <= i -> Forall dig0 Z ->
3997	epose proof (LIncs_k _ _ _ I1); subst.
		774	PC LX false h i pp q (S (S (length Z))) 0 ->
3998	eapply BigStep in I1.
		775	AllI (PCx LX false h) (S i) (Z ++ [(S pa, 1, false); (pb, 1, false)]) ->
3999	2: apply I2.
		776	AllI (PCx T0 false 2) (S i) (ovpX q Z (S pa)).
4000	eexists (_,_,_); split.
		777	Proof.
4001	1: apply I1.
		778	induction Z as [\|[[p' q'] d'] Z IH]; intros i pp q Hi HZ H HA.
		779	- cbn [ovpX AllI app] in *. split; [\|exact I]. destruct HA as [Ha _].
		780	unfL. cbn [length dv bv] in *. eapply ob_x1_base; eauto.
		781	- cbn [ovpX AllI app] in *. inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d'.
		782	destruct HA as [Hh HA]. unfL.
		783	rewrite length_app in Hh. cbn [length] in Hh.
		784	rewrite dv_zero in Hh
		785	by (constructor; [reflexivity\|]; apply Forall_app; split; [exact HZ'\|]; repeat constructor).
4002	split.	786	split.
4003	1: apply I3.
		787	+ unfL. rewrite ovpX_len.
4004	lia.
		788	replace (dv ((q, p', true) :: ovpX q' Z (S pa))) with (2 * 2 ^ length Z - 1)
4005	Unshelve.
		789	by (cbn [dv bv]; pose proof (ovpX_dv q' Z (S pa)) as E; lia).
4006	apply aWF_intro; lia.
		790	eapply ob_x1_step; eauto. replace (length Z + 2) with (S (S (length Z))) in Hh by lia. exact Hh.
		791	+ apply (IH (S i) p'); auto. replace (length Z + 2) with (S (S (length Z))) in Hh by lia. exact Hh.
4007	Qed.	792	Qed.
		794	(** pass-through pairs (digit 0 below a digit 1) have q >= 2 *)
		795	Lemma passq ph c4 h i p q n tv : PC ph c4 h i p q n tv -> 2 <= tv -> tv mod 2 = 0 -> 2 <= q.
		796	Proof.
		797	intros (Hp & Hq & HN & _) Ht Ht2. pose proof (pow_pos n). unfold PN in HN.
		798	destruct ph; try destruct c4; destruct n as [\|[\|n]]; cr.
		799	Qed.
		801	Lemma Z_okL ph c4 h : forall Z i x R, Forall dig0 Z -> dig x = true ->
		802	AllI (PCx ph c4 h) i (Z ++ x :: R) -> Forall okL Z.
		803	Proof.
		804	induction Z as [\|[[p q] d] Z IH]; intros i x R HZ Hx HA; [constructor\|].
		805	inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d.
		806	cbn [app AllI] in HA. destruct HA as [Hh HA]. constructor; [\|eapply IH; eauto].
		807	cbn. split; [reflexivity\|]. unfL. eapply passq; [exact Hh\| \|].
		808	- cbn [dv bv]. rewrite dv_zeros by exact HZ'. destruct x as [[px qx] dx]. cbn in Hx. subst dx.
		809	cbn [dv bv]. pose proof (pow_pos (length Z)). nia.
		810	- cbn [dv bv]. lia.
		811	Qed.
		813	(** a digit-1 pair with q = 1 (a run-out): only in L phases, never pairs 1 and 2 *)
		814	Lemma borrow1 ph c4 h k p n tv : 1 <= k -> tv mod 2 = 1 -> PC ph c4 h k p 1 n tv ->
		815	(ph = L1 \/ ph = L2 \/ ph = LX) /\ 3 <= k /\
		816	(ph = L1 -> 1 <= n /\ tv + 1 <= 2 ^ n /\ (c4 = true -> 2 <= n)) /\ (ph = LX -> 2 <= n).
		817	Proof.
		818	intros Hk Ht (Hp & Hq & HN & HI). pose proof (pow_pos n).
		819	assert (Hph : ph = L1 \/ ph = L2 \/ ph = LX).
		820	{ clear HI. unfold PN in HN. destruct ph; try (left; reflexivity); try (right; left; reflexivity);
		821	try (right; right; reflexivity); exfalso; destruct n as [\|n]; cr. }
		822	split; [exact Hph\|]. split.
		823	- clear HN. unfold PI in HI. destruct k as [\|[\|[\|k]]]; try lia;
		824	destruct Hph as [-> \| [-> \| ->]]; cr.
		825	- clear HI. unfold PN in HN. split; intros ->; [destruct c4\|]; destruct n as [\|[\|n]]; cr; discriminate.
		826	Qed.
		828	Lemma even2 x : (2 * x) mod 2 = 0.
		829	Proof. lia. Qed.
		831	Lemma pc_len (Pr : nat -> tri -> list tri -> Prop) i P : AllI Pr i P -> True.
		832	Proof. auto. Qed.
		834	Ltac dvs := cbn [dv bv length app map] in ; repeat rewrite length_app in ; repeat rewrite length_map in *;
		835	cbn [length] in *.
		837	Lemma inv_Dec ph c4 h Z p q R : Forall dig0 Z ->
		838	AllI (PCx ph c4 h) 1 (Z ++ (p, S (S q), true) :: R) ->
		839	AllI (PCx ph c4 (4 + h)) 1 (map touch Z ++ (S p, S q, false) :: R).
		840	Proof.
		841	intros HZ HA. pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx HR].
		842	apply (AllI_touchZ (PCx ph c4 h) (PCx ph c4 (4 + h)) ((p, S (S q), true) :: R) ((S p, S q, false) :: R)); [exact HZ \| \| exact HA \| ].
		843	- intros j p0 q0 Zr HZr Hj H. unfL. dvs.
		844	rewrite dv_zeros in H by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in *.
		845	pose proof (pow_pos (length Zr)).
		846	replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * (0 + 2 * dv R)))
		847	with (2 * (2 ^ length Zr * (1 + 2 * dv R)) - 1) by nia.
		848	apply (ob_touch ph c4 h j p0 q0); [nia\| \|exact H]. eapply passq; [exact H\| nia \| apply even2].
		849	- cbn [AllI]. split.
		850	+ unfL. cbn [dv bv] in *.
		851	replace (0 + 2 * dv R) with (1 + 2 * dv R - 1) by lia.
		852	apply (ob_touch ph c4 h (1 + length Z) p (S (S q)) (length R) (1 + 2 * dv R)); [lia\|lia\|exact Hx].
		853	+ eapply AllI_mono; [\|exact HR]. intros j y Y Hj Hy. destruct y as [[py qy] dy].
		854	unfL. destruct Hy as (Hp & Hq & HN & HI). split; [lia\|]. split; [lia\|].
		855	split; [exact HN\|]. unfold PI in *. destruct j as [\|[\|[\|j]]]; try lia; try exact HI; exact I.
		856	Qed.
		858	Lemma snoc_nn (Z : list tri) y : Z ++ [y] <> [].
		859	Proof. destruct Z; discriminate. Qed.
		861	Definition minlen (ph : phase) : nat := match ph with LX => 3 \| L2 => 1 \| _ => 2 end.
		863	Lemma head_len ph c4 h x Y : PCx ph c4 h 1 x Y -> minlen ph <= length Y.
		864	Proof.
		865	destruct x as [[p q] d]. intros H. unfLh H. destruct H as (_ & _ & _ & HI). unfold PI in HI.
		866	destruct ph; cbn [minlen]; cr.
		867	Qed.
		869	Lemma AllI_len ph c4 h P : P <> [] -> AllI (PCx ph c4 h) 1 P -> S (minlen ph) <= length P.
		870	Proof.
		871	destruct P as [\|x Y]; [congruence\|]. intros _ [H _]. apply head_len in H. cbn. lia.
		872	Qed.
		874	Lemma q2_V0 ph c4 h i p q n : PC ph c4 h i p q n 0 -> 1 <= n -> (ph = LX -> 2 <= n) -> 2 <= q.
		875	Proof.
		876	intros (Hp & Hq & HN & _) Hn HX. pose proof (pow_pos n). unfold PN in HN.
		877	destruct ph; try destruct c4; destruct n as [\|[\|n]]; cr; specialize (HX eq_refl); lia.
		878	Qed.
		880	Lemma p1_V0 ph c4 h p q n : PC ph c4 h 1 p q n 0 -> (ph = E2 \/ ph = E2t \/ ph = L2 \/ ph = LX) -> 2 <= p.
		881	Proof.
		882	intros (Hp & Hq & HN & HI) Hph. pose proof (pow_pos n). unfold PN, PI in *.
		883	destruct Hph as [-> \| [-> \| [-> \| ->]]]; try destruct c4; destruct n as [\|[\|n]]; cr.
		884	Qed.
		886	Lemma L2_c4_V0 h i p q : PC L2 true h i p q 0 0 -> False.
		887	Proof. intros (Hp & Hq & HN & _). unfold PN in HN. cr. Qed.
		889	Lemma AllI_okRO ph c4 h : forall Z i, Forall dig0 Z -> AllI (PCx ph c4 h) i Z -> Forall okR Z /\ Forall okO Z.
		890	Proof.
		891	induction Z as [\|[[p q] d] Z IH]; intros i HZ HA; [split; constructor\|].
		892	inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d.
		893	destruct HA as [Hh HA]. destruct (IH (S i) HZ' HA) as [H1 H2]. unfLh Hh. destruct Hh as (Hp & Hq & _).
		894	split; constructor; auto; cbn; lia.
		895	Qed.
		897	Lemma inv_Merge ph c4 h Z p p' q' d' R0 : Forall dig0 Z ->
		898	AllI (PCx ph c4 h) 1 (Z ++ (p, 1, true) :: (p', q', d') :: R0) ->
		899	AllI (PCx ph c4 (4 + h)) 1 (map touch Z ++ (p + p' + 3, q', d') :: R0).
		900	Proof.
		901	intros HZ HA. pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx [Hy HR]].
		902	pose proof (dv_lt ((p', q', d') :: R0)) as Hlt. cbn [length] in Hlt.
		903	set (Hd := dv ((p', q', d') :: R0)) in *.
		904	assert (Hx' := Hx). unfLh Hx'. cbn [length] in Hx'.
		905	change (dv ((p, 1, true) :: (p', q', d') :: R0)) with (1 + 2 * Hd) in Hx'.
		906	destruct (borrow1 ph c4 h (1 + length Z) p (S (length R0)) (1 + 2 * Hd)) as (Hph & Hk & HL1 & HLX);
		907	[lia \| lia \| exact Hx' \|].
		908	apply (AllI_touchZ (PCx ph c4 h) (PCx ph c4 (4 + h)) ((p, 1, true) :: (p', q', d') :: R0)
		909	((p + p' + 3, q', d') :: R0)); [exact HZ \| \| exact HA \| ].
		910	- intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in . cbn [length] in . cbn [dv bv] in H0 \|- *.
		911	rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 \|- *.
		912	change (bv d' + 2 * dv R0) with Hd in H0 \|- *.
		913	set (A := 2 ^ length Zr) in . set (B := 2 ^ length R0) in .
		914	assert (HA1 : 1 <= A) by apply pow_pos. assert (HB1 : 1 <= B) by apply pow_pos.
		915	assert (Hn : 2 ^ (length Zr + S (length R0)) = A * (2 * B)) by (rewrite Nat.pow_add_r; reflexivity).
		916	rewrite pow_S in Hlt. fold B in Hlt.
		917	replace (length Zr + S (S (length R0))) with (S (length Zr + S (length R0))) in H0 by lia.
		918	replace (0 + 2 * (A * (1 + 2 * Hd))) with (2 * A + 2 * (2 * A * Hd)) in H0 by ring.
		919	replace (1 + 2 * (A - 1 + A * Hd)) with (2 * A - 1 + 2 * A * Hd) by (clear - HA1; nia).
		920	assert (Hq2 : 2 <= q0).
		921	{ eapply passq; [exact H0 \| nia \|]. replace (2 * A + 2 * (2 * A * Hd)) with (2 * (A + 2 * A * Hd)) by ring.
		922	apply even2. }
		923	eapply ob_merge; [exact Hph \| lia \| lia \| \| \| \| \| \| \| \| \| exact Hq2 \| exact H0].
		924	+ apply even2.
		925	+ replace (2 * A * Hd) with (2 * (A * Hd)) by ring. apply even2.
		926	+ rewrite Hn. nia.
		927	+ intros ->. destruct (HL1 eq_refl) as (_ & Hb & _). rewrite pow_S in Hb. fold B in Hb. rewrite Hn. nia.
		928	+ intros ->. specialize (HLX eq_refl). lia.
		929	+ intros -> Hc. destruct (HL1 eq_refl) as (_ & _ & Hc2). specialize (Hc2 Hc). lia.
		930	+ intros ->. lia.
		931	+ intros -> ->. specialize (HLX eq_refl). lia.
		932	- cbn [AllI]. split.
		933	+ unfLh Hy. unfLg. change (dv ((p + p' + 3, q', d') :: R0)) with (dv ((p', q', d') :: R0)).
		934	replace (length Z + 1) with (1 + length Z) by lia.
		935	eapply ob_fuse; [exact Hph \| lia \| exact Hy].
		936	+ eapply AllI_shift; [\|exact HR]. intros j y Y Hj Hy0. destruct y as [[py qy] dy].
		937	unfLh Hy0. unfLg. eapply ob_far; [\| \| exact Hy0]; lia.
		938	Qed.
		940	Lemma inv_MT c4 h Z p : Forall dig0 Z -> AllI (PCx L2 c4 h) 1 (Z ++ [(p, 1, true)]) ->
		941	AllI (PCx L2 false (4 + h)) 1 (map touch Z) /\ 2 <= length Z.
		942	Proof.
		943	intros HZ HA. pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx _].
		944	assert (Hx' := Hx). unfLh Hx'. cbn [length dv bv] in Hx'.
		945	destruct (borrow1 L2 c4 h (1 + length Z) p 0 (1 + 2 * 0)) as (_ & Hk & _); [lia \| lia \| exact Hx' \|].
		946	split; [\|lia]. rewrite <- (app_nil_r (map touch Z)).
		947	apply (AllI_touchZ (PCx L2 c4 h) (PCx L2 false (4 + h)) [(p, 1, true)] []); [exact HZ \| \| exact HA \| exact I].
		948	intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in . cbn [length] in . cbn [dv bv] in H0 \|- *.
		949	rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 \|- *.
		950	pose proof (pow_pos (length Zr)).
		951	replace (length Zr + 1) with (S (length Zr)) in H0 by lia. rewrite Nat.add_0_r.
		952	replace (0 + 2 * (2 ^ length Zr * (1 + 2 * 0))) with (2 * 2 ^ length Zr) in H0 by ring.
		953	replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * 0)) with (2 * 2 ^ length Zr - 1) by lia.
		954	apply (ob_mt c4); [\| lia \| exact H0].
		955	eapply passq; [exact H0 \| lia \| apply even2].
		956	Qed.
		958	Lemma inv_End ph ph' h Z p q : endtr ph ph' -> Forall dig0 Z ->
		959	AllI (PCx ph false h) 1 (Z ++ [(p, S (S q), false)]) ->
		960	AllI (PCx ph' false (4 + h)) 1 (map touch Z ++ [(S p, S q, false)]).
		961	Proof.
		962	intros Htr HZ HA. pose proof (AllI_len _ _ _ _ (snoc_nn Z _) HA) as Hlen.
		963	rewrite length_app in Hlen. cbn [length] in Hlen.
		964	assert (Hm : minlen ph = 2) by (destruct Htr as [[-> _]\|[-> _]]; reflexivity).
		965	pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx _].
		966	apply (AllI_touchZ (PCx ph false h) (PCx ph' false (4 + h)) [(p, S (S q), false)] [(S p, S q, false)]);
		967	[exact HZ \| \| exact HA \| ].
		968	- intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in . cbn [length] in . cbn [dv bv] in H0 \|- *.
		969	rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 \|- *.
		970	pose proof (pow_pos (length Zr)).
		971	replace (0 + 2 * (2 ^ length Zr * (0 + 2 * 0))) with 0 in H0 by ring.
		972	replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * (0 + 2 * 0))) with (2 ^ (length Zr + 1) - 1)
		973	by (rewrite Nat.add_1_r, pow_S; lia).
		974	apply (ob_end ph ph'); [exact Htr \| lia \| \| exact H0].
		975	eapply q2_V0; [exact H0 \| lia \| intros ->; destruct Htr as [[? _]\|[? _]]; discriminate].
		976	- cbn [AllI]. split; [\|exact I]. unfLh Hx. unfLg. cbn [length dv bv] in *.
		977	apply (ob_end_top ph ph'); [exact Htr \| lia \| exact Hx].
		978	Qed.
		980	Lemma inv_X2 h Z p q k : Forall dig0 Z -> 3 <= k ->
		981	AllI (PCx T0 false h) 1 (Z ++ [(p, S (S q), false)]) ->
		982	AllI (PCx E1t false (4 + h)) 1 (map touch Z ++ [(S p, S q, false); (3, k, true)]).
		983	Proof.
		984	intros HZ Hk HA. pose proof (AllI_len _ _ _ _ (snoc_nn Z _) HA) as Hlen.
		985	rewrite length_app in Hlen. cbn [length minlen] in Hlen.
		986	pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx _].
		987	apply (AllI_touchZ (PCx T0 false h) (PCx E1t false (4 + h)) [(p, S (S q), false)]
		988	[(S p, S q, false); (3, k, true)]); [exact HZ \| \| exact HA \| ].
		989	- intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in . cbn [length] in . cbn [dv bv] in H0 \|- *.
		990	rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 \|- *.
		991	pose proof (pow_pos (length Zr)).
		992	replace (0 + 2 * (2 ^ length Zr * (0 + 2 * 0))) with 0 in H0 by ring.
		993	replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * (0 + 2 * (1 + 2 * 0))))
		994	with (3 * 2 ^ (length Zr + 1) - 1) by (rewrite Nat.add_1_r, pow_S; lia).
		995	replace (length Zr + 2) with (S (length Zr + 1)) by lia.
		996	apply ob_x2; [lia \| \| exact H0].
		997	eapply q2_V0; [exact H0 \| lia \| discriminate].
		998	- cbn [AllI]. split; [\|split; [\|exact I]].
		999	+ unfLh Hx. unfLg. cbn [length dv bv] in *. apply ob_x2_top; [lia \| exact Hx].
		1000	+ unfLg. cbn [length dv bv]. apply ob_x2_new; lia.
		1001	Qed.
		1003	Lemma inv_EndLast c4 h Z p : Forall dig0 Z -> AllI (PCx L1 c4 h) 1 (Z ++ [(p, 1, false)]) ->
		1004	AllI (PCx L2 c4 (4 + h)) 1 (map touch Z) /\ 2 <= length Z.
		1005	Proof.
		1006	intros HZ HA. pose proof (AllI_len _ _ _ _ (snoc_nn Z _) HA) as Hlen.
		1007	rewrite length_app in Hlen. cbn [length minlen] in Hlen.
		1008	split; [\|lia]. rewrite <- (app_nil_r (map touch Z)).
		1009	apply (AllI_touchZ (PCx L1 c4 h) (PCx L2 c4 (4 + h)) [(p, 1, false)] []); [exact HZ \| \| exact HA \| exact I].
		1010	intros j p0 q0 Zr HZr Hj H0. unfLh H0. unfLg. rewrite !length_app, !length_map in . cbn [length] in . cbn [dv bv] in H0 \|- *.
		1011	rewrite dv_zeros in H0 by exact HZr. rewrite dv_tz' by exact HZr. cbn [dv bv] in H0 \|- *.
		1012	pose proof (pow_pos (length Zr)).
		1013	replace (0 + 2 * (2 ^ length Zr * (0 + 2 * 0))) with 0 in H0 by ring.
		1014	replace (length Zr + 1) with (S (length Zr)) in H0 by lia. rewrite Nat.add_0_r.
		1015	replace (1 + 2 * (2 ^ length Zr - 1 + 2 ^ length Zr * 0)) with (2 * 2 ^ length Zr - 1) by lia.
		1016	apply ob_endlast; [\| exact H0].
		1017	eapply q2_V0; [exact H0 \| lia \| discriminate].
		1018	Qed.
		1020	Lemma inv_Ov ph ph' c4' Xp h p1 q1 Z t : ovtr ph ph' c4' Xp -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) ->
		1021	Forall dig0 Z -> lastOK Xp Z ->
		1022	AllI (PCx ph false h) 1 ((S (S p1), q1, false) :: Z) ->
		1023	AllI (PCx ph' c4' 2) 1 ((h + 5, S p1, false) :: ovp q1 Z t).
		1024	Proof.
		1025	intros Htr Ht1 Ht2 HZ HX HA. cbn [AllI] in HA \|- *. destruct HA as [Hh HA].
		1026	assert (Hh' := Hh). unfLh Hh'. rewrite dv_zero in Hh' by (constructor; [reflexivity \| exact HZ]).
		1027	split.
		1028	- unfLg. rewrite ovp_len.
		1029	replace (dv ((h + 5, S p1, false) :: ovp q1 Z t)) with (2 * (2 * 2 ^ length Z) - 2)
		1030	by (cbn [dv bv]; pose proof (ovp_dv q1 Z t) as E; rewrite pow_S in E; lia).
		1031	eapply ob_ov_head; [exact Htr \| exact Hh'].
		1032	- eapply (AllI_ovp ph ph' c4' Xp h t Htr Ht1 Ht2 Z 1 (S (S p1)) q1); auto.
		1033	Qed.
		1035	Lemma inv_X1 h p1 q1 Z pa pb : Forall dig0 Z ->
		1036	AllI (PCx LX false h) 1 ((S (S p1), q1, false) :: Z ++ [(S pa, 1, false); (pb, 1, false)]) ->
		1037	AllI (PCx T0 false 2) 1 ((h + 5, S p1, false) :: ovpX q1 Z (S pa)).
		1038	Proof.
		1039	intros HZ HA. cbn [AllI] in HA \|- *. destruct HA as [Hh HA].
		1040	assert (Hh' := Hh). unfLh Hh'.
		1041	rewrite dv_zero in Hh'
		1042	by (constructor; [reflexivity\|]; apply Forall_app; split; [exact HZ\|]; repeat constructor).
		1043	rewrite length_app in Hh'. cbn [length] in Hh'. replace (length Z + 2) with (S (S (length Z))) in Hh' by lia.
		1044	split.
		1045	- unfLg. rewrite ovpX_len.
		1046	replace (dv ((h + 5, S p1, false) :: ovpX q1 Z (S pa))) with (2 * 2 ^ length Z - 2)
		1047	by (cbn [dv bv]; pose proof (ovpX_dv q1 Z (S pa)) as E; lia).
		1048	exact (ob_x1_head _ _ _ _ Hh').
		1049	- eapply (AllI_ovpX h pa pb Z 1 (S (S p1)) q1); auto.
		1050	Qed.
		1052	(** * The invariant J on abstract states, and one macro step (TM part) *)
		1054	Record st := mkst { sh : nat; sP : list (natnatbool); sT : Tl; sph : phase; sc4 : bool }.
		1056	Definition Cf (s : st) : Q * tape := K (sh s) (sP s) (sT s).
		1058	Definition TC (ph : phase) (c4 : bool) (T : Tl) : Prop :=
		1059	match ph with
		1060	\| E1 \| E1t \| LX => T = TN /\ c4 = false
		1061	\| L1 => T = TN
		1062	\| E2 \| E2t => T = TA 1 /\ c4 = false
		1063	\| T0 => (exists k, T = TB k /\ 3 <= k) /\ c4 = false
		1064	\| L2 => exists t, T = TA t /\ 2 <= t
		1065	end.
		1067	Definition J (s : st) : Prop :=
		1068	sP s <> [] /\ TC (sph s) (sc4 s) (sT s) /\ AllI (PCx (sph s) (sc4 s) (sh s)) 1 (sP s).
		1070	Lemma split1 (P : list tri) :
		1071	(exists Z x R, P = Z ++ x :: R /\ Forall dig0 Z /\ dig x = true) \/ Forall dig0 P.
		1072	Proof.
		1073	induction P as [\|[[p q] d] P IH]; [right; constructor\|].
		1074	destruct d.
		1075	- left. exists (@nil (natnatbool)), (p,q,true), P. auto.
		1076	- destruct IH as [(Z & x & R & -> & HZ & Hx) \| H].
		1077	+ left. exists ((p,q,false) :: Z), x, R. split; [reflexivity\|].
		1078	split; [constructor; [reflexivity\|exact HZ] \| exact Hx].
		1079	+ right. constructor; [reflexivity \| exact H].
		1080	Qed.
		1082	Lemma Z_okL_V0 ph c4 h y : ph <> LX -> forall Z i, Forall dig0 (Z ++ [y]) ->
		1083	AllI (PCx ph c4 h) i (Z ++ [y]) -> Forall okL Z.
		1084	Proof.
		1085	intros Hph. induction Z as [\|[[p q] d] Z IH]; intros i HZ HA; [constructor\|].
		1086	inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d.
		1087	cbn [app AllI] in HA. destruct HA as [Hh HA]. constructor; [\|eapply IH; eauto].
		1088	cbn. split; [reflexivity\|]. unfLh Hh. rewrite dv_zero in Hh by (constructor; [reflexivity \| exact HZ']).
		1089	eapply q2_V0; [exact Hh \| rewrite length_app; cbn; lia \| intros E; contradiction].
		1090	Qed.
		1092	Lemma lastOK_True Z : lastOK (fun _ => True) Z.
		1093	Proof. induction Z as [\|[[p q] d] Z IH]; [exact I\|]. destruct Z; [exact I \| exact IH]. Qed.
		1095	Lemma Forall_snoc_inv (Pr : tri -> Prop) Z y : Forall Pr (Z ++ [y]) -> Forall Pr Z /\ Pr y.
		1096	Proof. intros H. apply Forall_app in H. destruct H as [H1 H2]. inversion H2. auto. Qed.
		1098	Lemma last_pc ph c4 h Z p q d : Forall dig0 (Z ++ [(p,q,d)]) -> AllI (PCx ph c4 h) 1 (Z ++ [(p,q,d)]) ->
		1099	d = false /\ PC ph c4 h (1 + length Z) p q 0 0.
		1100	Proof.
		1101	intros HZ HA. apply Forall_snoc_inv in HZ. destruct HZ as [_ Hd]. unfold dig0, dig in Hd. subst d.
		1102	split; [reflexivity\|]. pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hy _].
		1103	unfLh Hy. exact Hy.
		1104	Qed.
		1106	Lemma first_pc ph c4 h p q d Z : Forall dig0 ((p,q,d) :: Z) -> AllI (PCx ph c4 h) 1 ((p,q,d) :: Z) ->
		1107	d = false /\ PC ph c4 h 1 p q (length Z) 0 /\ Forall dig0 Z /\ AllI (PCx ph c4 h) 2 Z.
		1108	Proof.
		1109	intros HZ [Hh HA]. inversion HZ as [\|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d.
		1110	split; [reflexivity\|]. unfLh Hh. rewrite dv_zero in Hh by (constructor; [reflexivity \| exact HZ']).
		1111	auto.
		1112	Qed.
		1114	Ltac pnc H := let H' := fresh in destruct H as (_ & _ & H' & _); unfold PN in H'; cbn - [Nat.modulo] in H'.
		1116	Lemma Jstep : forall s, J s -> exists s', Cf s -->+ Cf s' /\ J s'.
		1117	Proof.
		1118	intros [h P T ph c4] (HP & HT & HA). unfold Cf. cbn [sh sP sT sph sc4] in *.
		1119	destruct (split1 P) as [(Z & [[p q] d] & R & -> & HZ & Hd) \| H0].
		1120	- (* some digit is 1: a Dec-family step *)
		1121	cbn in Hd. subst d.
		1122	assert (HZL : Forall okL Z) by (apply (Z_okL ph c4 h Z 1 (p, q, true) R); [exact HZ \| reflexivity \| exact HA]).
		1123	pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx HR].
		1124	assert (Hx' := Hx). unfLh Hx'.
		1125	destruct q as [\|[\|q]].
		1126	+ exfalso. destruct Hx' as (_ & Hq & _). lia.
		1127	+ destruct (borrow1 ph c4 h (1 + length Z) p (length R) (dv ((p, 1, true) :: R)))
		1128	as (Hph & Hk & HL1 & HLX); [lia \| cbn [dv bv]; lia \| exact Hx' \|].
		1129	destruct R as [\|[[p' q'] d'] R0].
		1130	* destruct T as [\|t\|k].
		1131	-- exfalso. destruct Hph as [-> \| [-> \| ->]].
		1132	++ destruct (HL1 eq_refl) as (Hn & _). cbn in Hn. lia.
		1133	++ destruct HT as (t & Ht & _). discriminate.
		1134	++ specialize (HLX eq_refl). cbn in HLX. lia.
		1135	-- assert (ph = L2) as ->.
		1136	{ destruct Hph as [-> \| [-> \| ->]]; cbn in HT; try reflexivity;
		1137	try discriminate; destruct HT; discriminate. }
		1138	destruct HT as (t' & Ht & Ht2). injection Ht as <-.
		1139	destruct (inv_MT c4 h Z p HZ HA) as [HA' Hlen].
		1140	exists (mkst (4 + h) (map touch Z) (TA (p + t + 3)) L2 false). cbn [sh sP sT sph sc4]. split.
		1141	++ apply DecMergeTail. exact HZL.
		1142	++ split; [destruct Z; [cbn in Hlen; lia \| discriminate]\|].
		1143	split; [exists (p + t + 3); split; [reflexivity \| lia] \| exact HA'].
		1144	-- exfalso. destruct Hph as [-> \| [-> \| ->]]; cbn in HT;
		1145	repeat match goal with H : _ /\ _ \|- _ => destruct H \| H : exists _, _ \|- _ => destruct H end;
		1146	discriminate.
		1147	* exists (mkst (4 + h) (map touch Z ++ (p + p' + 3, q', d') :: R0) T ph c4). cbn [sh sP sT sph sc4].
		1148	split.
		1149	-- apply DecMerge. exact HZL.
		1150	-- split; [destruct Z; discriminate\|]. split; [exact HT\|]. eapply inv_Merge; eauto.
		1151	+ exists (mkst (4 + h) (map touch Z ++ (S p, S q, false) :: R) T ph c4). cbn [sh sP sT sph sc4]. split.
		1152	* apply Dec. exact HZL.
		1153	* split; [destruct Z; discriminate\|]. split; [exact HT\|]. apply inv_Dec; assumption.
		1154	- (* all digits 0 *)
		1155	destruct ph.
		1156	+ (* E1: End *)
		1157	destruct HT as [-> ->]. destruct (exists_last HP) as (Z & [[p q] d] & ->).
		1158	destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy].
		1159	assert (Hq : 2 <= q) by (pnc Hy; lia). destruct q as [\|[\|q]]; [lia\|lia\|].
		1160	assert (HZL : Forall okL Z) by (eapply Z_okL_V0; [\| exact H0 \| exact HA]; discriminate).
		1161	apply Forall_snoc_inv in H0. destruct H0 as [HZ _].
		1162	exists (mkst (4 + h) (map touch Z ++ [(S p, S q, false)]) (TA 1) E2 false). cbn [sh sP sT sph sc4].
		1163	split; [apply EndR; exact HZL\|]. split; [apply snoc_nn\|]. split; [split; reflexivity\|].
		1164	eapply inv_End; [left; split; reflexivity \| exact HZ \| exact HA].
		1165	+ (* E2: Ov *)
		1166	destruct HT as [-> ->]. destruct P as [\|[[p1 q1] d1] Z]; [congruence\|].
		1167	destruct (first_pc _ _ _ _ _ _ _ H0 HA) as (-> & Hh & HZ & HA2).
		1168	assert (Hp1 := p1_V0 _ _ _ _ _ _ Hh ltac:(left; reflexivity)).
		1169	destruct p1 as [\|[\|p1]]; [lia\|lia\|].
		1170	destruct (AllI_okRO _ _ _ Z 2 HZ HA2) as [HR HO].
		1171	assert (Hq1 : 1 <= q1) by (destruct Hh as (_ & Hq & _); exact Hq).
		1172	destruct (lastOK_dec Z) as [HX \| HX].
		1173	* exists (mkst 2 ((h + 5, S p1, false) :: ovp q1 Z 1) TN LX false). cbn [sh sP sT sph sc4].
		1174	split; [apply Ov; assumption\|]. split; [discriminate\|]. split; [split; reflexivity\|].
		1175	eapply (inv_Ov E2 LX false (fun x => x = 4)); [right; left; auto \| discriminate \| auto \| exact HZ \| exact HX \| exact HA].
		1176	* exists (mkst 2 ((h + 5, S p1, false) :: ovp q1 Z 1) TN L1 false). cbn [sh sP sT sph sc4].
		1177	split; [apply Ov; assumption\|]. split; [discriminate\|]. split; [reflexivity\|].
		1178	eapply (inv_Ov E2 L1 false (fun x => x <> 4)); [left; auto \| discriminate \| auto \| exact HZ \| exact HX \| exact HA].
		1179	+ (* E1t: End *)
		1180	destruct HT as [-> ->]. destruct (exists_last HP) as (Z & [[p q] d] & ->).
		1181	destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy].
		1182	assert (Hq : 2 <= q) by (pnc Hy; lia). destruct q as [\|[\|q]]; [lia\|lia\|].
		1183	assert (HZL : Forall okL Z) by (eapply Z_okL_V0; [\| exact H0 \| exact HA]; discriminate).
		1184	apply Forall_snoc_inv in H0. destruct H0 as [HZ _].
		1185	exists (mkst (4 + h) (map touch Z ++ [(S p, S q, false)]) (TA 1) E2t false). cbn [sh sP sT sph sc4].
		1186	split; [apply EndR; exact HZL\|]. split; [apply snoc_nn\|]. split; [split; reflexivity\|].
		1187	eapply inv_End; [right; split; reflexivity \| exact HZ \| exact HA].
		1188	+ (* E2t: Ov to an L-slot after a T2 start *)
		1189	destruct HT as [-> ->]. destruct P as [\|[[p1 q1] d1] Z]; [congruence\|].
		1190	destruct (first_pc _ _ _ _ _ _ _ H0 HA) as (-> & Hh & HZ & HA2).
		1191	assert (Hp1 := p1_V0 _ _ _ _ _ _ Hh ltac:(right; left; reflexivity)).
		1192	destruct p1 as [\|[\|p1]]; [lia\|lia\|].
		1193	destruct (AllI_okRO _ _ _ Z 2 HZ HA2) as [HR HO].
		1194	assert (Hq1 : 1 <= q1) by (destruct Hh as (_ & Hq & _); exact Hq).
		1195	exists (mkst 2 ((h + 5, S p1, false) :: ovp q1 Z 1) TN L1 true). cbn [sh sP sT sph sc4].
		1196	split; [apply Ov; assumption\|]. split; [discriminate\|]. split; [reflexivity\|].
		1197	eapply (inv_Ov E2t L1 true (fun _ => True)); [right; right; left; auto \| discriminate \| auto \| exact HZ \| apply lastOK_True \| exact HA].
		1198	+ (* T0: X2 *)
		1199	destruct HT as [(k & -> & Hk) ->]. destruct (exists_last HP) as (Z & [[p q] d] & ->).
		1200	destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy].
		1201	assert (Hq : 2 <= q) by (pnc Hy; lia). destruct q as [\|[\|q]]; [lia\|lia\|].
		1202	destruct k as [\|k]; [lia\|].
		1203	assert (HZL : Forall okL Z) by (eapply Z_okL_V0; [\| exact H0 \| exact HA]; discriminate).
		1204	apply Forall_snoc_inv in H0. destruct H0 as [HZ _].
		1205	exists (mkst (4 + h) (map touch Z ++ [(S p, S q, false); (3, S k, true)]) TN E1t false).
		1206	cbn [sh sP sT sph sc4].
		1207	split; [apply X2; exact HZL\|]. split; [destruct Z; discriminate\|]. split; [split; reflexivity\|].
		1208	apply inv_X2; [exact HZ \| lia \| exact HA].
		1209	+ (* L1: EndLast *)
		1210	cbn in HT. subst T. destruct (exists_last HP) as (Z & [[p q] d] & ->).
		1211	destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy].
		1212	assert (Hq : q = 1) by (pnc Hy; lia). subst q.
		1213	assert (HZL : Forall okL Z) by (eapply Z_okL_V0; [\| exact H0 \| exact HA]; discriminate).
		1214	apply Forall_snoc_inv in H0. destruct H0 as [HZ _].
		1215	destruct (inv_EndLast c4 h Z p HZ HA) as [HA' Hlen].
		1216	exists (mkst (4 + h) (map touch Z) (TA (p + 4)) L2 c4). cbn [sh sP sT sph sc4].
		1217	split; [apply EndLast; exact HZL\|]. split; [destruct Z; [cbn in Hlen; lia \| discriminate]\|].
		1218	split; [exists (p + 4); split; [reflexivity \| lia] \| exact HA'].
		1219	+ (* L2: Ov *)
		1220	destruct HT as (t & -> & Ht).
		1221	destruct c4.
		1222	{ exfalso. destruct (exists_last HP) as (Z & [[p q] d] & ->).
		1223	destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy]. exact (L2_c4_V0 _ _ _ _ Hy). }
		1224	destruct P as [\|[[p1 q1] d1] Z]; [congruence\|].
		1225	destruct (first_pc _ _ _ _ _ _ _ H0 HA) as (-> & Hh & HZ & HA2).
		1226	assert (Hp1 := p1_V0 _ _ _ _ _ _ Hh ltac:(right; right; left; reflexivity)).
		1227	destruct p1 as [\|[\|p1]]; [lia\|lia\|].
		1228	destruct (AllI_okRO _ _ _ Z 2 HZ HA2) as [HR HO].
		1229	assert (Hq1 : 1 <= q1) by (destruct Hh as (_ & Hq & _); exact Hq).
		1230	exists (mkst 2 ((h + 5, S p1, false) :: ovp q1 Z t) TN E1 false). cbn [sh sP sT sph sc4].
		1231	split; [apply Ov; assumption\|]. split; [discriminate\|]. split; [split; reflexivity\|].
		1232	eapply (inv_Ov L2 E1 false (fun _ => True)); [right; right; right; auto \| intros _; exact Ht \| intros E; congruence \| exact HZ \| apply lastOK_True \| exact HA].
		1233	+ (* LX: X1 *)
		1234	destruct HT as [-> ->].
		1235	pose proof (AllI_len _ _ _ _ HP HA) as Hlen. cbn [minlen] in Hlen.
		1236	destruct (exists_last HP) as (P1 & [[pb qb] db] & ->).
		1237	assert (HP1 : P1 <> []) by (destruct P1; [cbn in Hlen; lia \| discriminate]).
		1238	destruct (exists_last HP1) as (P2 & [[pa qa] da] & ->).
		1239	destruct P2 as [\|[[p1 q1] d1] Z]; [cbn in Hlen; lia\|].
		1240	rewrite <- !app_assoc in H0, HA \|- . cbn [app] in H0, HA \|- .
		1241	destruct (first_pc _ _ _ _ _ _ _ H0 HA) as (-> & Hh & HZab & HA2).
		1242	apply Forall_app in HZab. destruct HZab as [HZ Hab].
		1243	inversion Hab as [\|? ? Hda Hab']; subst. inversion Hab' as [\|? ? Hdb _]; subst.
		1244	unfold dig0, dig in Hda, Hdb. subst da db.
		1245	pose proof (AllI_app _ _ _ _ HA2) as HB. cbn [AllI] in HB. destruct HB as [Ha [Hb _]].
		1246	unfLh Ha. unfLh Hb. cbn [length dv bv] in Ha, Hb.
		1247	assert (Hqa : qa = 1) by (pnc Ha; lia). assert (Hqb : qb = 1) by (pnc Hb; lia). subst qa qb.
		1248	assert (Hpa : 1 <= pa) by (destruct Ha as (Hp & _); exact Hp). destruct pa as [\|pa]; [lia\|].
		1249	assert (Hp1 := p1_V0 _ _ _ _ _ _ Hh ltac:(right; right; right; reflexivity)).
		1250	destruct p1 as [\|[\|p1]]; [lia\|lia\|].
		1251	assert (HZab' : Forall dig0 (Z ++ [(S pa, 1, false); (pb, 1, false)]))
		1252	by (apply Forall_app; split; [exact HZ \| repeat constructor]).
		1253	destruct (AllI_okRO _ _ _ _ 2 HZab' HA2) as [HR HO].
		1254	apply Forall_app in HR. apply Forall_app in HO. destruct HR as [HR _]. destruct HO as [HO _].
		1255	assert (Hq1 : 1 <= q1) by (destruct Hh as (_ & Hq & _); exact Hq).
		1256	exists (mkst 2 ((h + 5, S p1, false) :: ovpX q1 Z (S pa)) (TB (pb + 3)) T0 false).
		1257	cbn [sh sP sT sph sc4]. split; [apply X1; assumption\|].
		1258	split; [discriminate\|]. split; [split; [exists (pb + 3); split; [reflexivity \| lia] \| reflexivity]\|].
		1259	eapply inv_X1; [exact HZ \| exact HA].
		1260	Qed.
		1262	Lemma J_base : J (mkst 2 base TN E1 false).
		1263	Proof.
		1264	unfold J, base. cbn [sh sP sT sph sc4]. split; [discriminate\|]. split; [split; reflexivity\|].
		1265	cbn [AllI]. unfold PCx, Lift, PC, PN, PI. cbn. repeat split; lia.
		1266	Qed.
		1268	Lemma nonhalt : ~ halts tm c0.
		1269	Proof.
		1270	apply multistep_nonhalt with (c' := K 2 base TN); [exact init\|].
		1271	change (K 2 base TN) with (Cf (mkst 2 base TN E1 false)).
		1272	apply progress_nonhalt_cond with (P := J); [exact Jstep \| exact J_base].
		1273	Qed.
		1275	(*
		1276	```
		1277	1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---
		1279	[p,q,d] := (10)^p (01)^q s(d), s(1) = 0001, s(0) = 0010 [RP]
		1280	K(h; P; T) := 0^inf <A (10)^h 11001 [p_1,q_1,d_1] ... [p_L,q_L,d_L] T 0^inf [K]
		1281	T in { -, (10)^t 1, (101)^2 (01)^k } [TN, TA t, TB k]
		1282	k := least j with d_j = 1; Z := pairs 1..k-1 (all d = 0, q >= 2)
		1283	touch (p,q,d) := (p+1, q-1, 1-d)
		1285	Dec K(h; Z ++ (p,q+2,1) :: R; T) -->+ K(h+4; touch Z ++ (p+1,q+1,0) :: R; T)
		1286	DecMerge K(h; Z ++ (p,1,1) :: (p',q',d') :: R; T) -->+ K(h+4; touch Z ++ (p+p'+3,q',d') :: R; T)
		1287	DecMergeTail K(h; Z ++ [(p,1,1)]; (10)^t 1) -->+ K(h+4; touch Z; (10)^(p+t+3) 1)
		1288	DecMergeEmpty K(h; Z ++ [(p,1,1)]; -) -->+ K(h+4; touch Z; (10)^(p+2) 1)
		1289	End K(h; Z ++ [(p,q+2,0)]; -) -->+ K(h+4; touch Z ++ [(p+1,q+1,0)]; (10)^1 1)
		1290	EndLast K(h; Z ++ [(p,1,0)]; -) -->+ K(h+4; touch Z; (10)^(p+4) 1)
		1291	X2 K(h; Z ++ [(p,q+2,0)]; (101)^2 (01)^(k+1))
		1292	-->+ K(h+4; touch Z ++ [(p+1,q+1,0); (3,k+1,1)]; -)
		1293	Ov K(h; (p1+2,q1,0) :: Y; (10)^t 1) -->+ K(2; (h+5,p1+1,0) :: ovp q1 Y t; -)
		1294	Y all d = 0, p,q >= 1, q1 >= 1; ovp q [] t = [(q,t+1,1)],
		1295	ovp q ((p',q',_) :: Y) t = (q,p',1) :: ovp q' Y t
		1296	X1 K(h; (p1+2,q1,0) :: Y ++ [(pa+1,1,0); (pb,1,0)]; -)
		1297	-->+ K(2; (h+5,p1+1,0) :: ovpX q1 Y (pa+1); (101)^2 (01)^(pb+3))
		1298	ovpX q [] pa = [(q,pa,0)], ovpX q ((p',q',_) :: Y) pa = (q,p',1) :: ovpX q' Y pa
		1299	invariant J (per pair, n = pairs to the right, tv = digit value from the pair up,
		1300	Rt = tv + phase term): see Definitions PN, PI, TC, J; preserved by every rule (Jstep).
		1301	start: c0 -->(956) K(2; (11,11,0); -) -->(77,754) K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); -)
		1302	```
		1303	*)

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

138 items in 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v (1303 lines): 102 Lemma, 25 Definition, 8 Fixpoint, 2 Inductive, 1 Record. 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 "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---").	L23	identicalexcept the TM string
2	Lemma	`ev_eq`	Lemma ev_eq {c1 c2 c2'} : c1 -->* c2 -> c2 = c2' -> c1 -->* c2'.	L30	new
3	Lemma	`prog_eq`	Lemma prog_eq {c1 c2 c2'} : c1 -->+ c2 -> c2 = c2' -> c1 -->+ c2'.	L33	new
4	Lemma	`Start`	Lemma Start h r : 0inf <{{A}} [1;0]^^h > [1;1;0;0;1] > r -->+ 0inf <* <[1;0]^^(4+h) <* <[1;1;1] <* [0] {{B}}> r.	L41	new
5	Lemma	`PassR`	Lemma PassR l p q r : l <* [0] {{B}}> [1;0]^^p > [0;1]^^(S q) > [0;0;1;0] > r --> l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^q <* <[1;1] <* [0] {{B}}> r.	L45	new
6	Lemma	`Borrow`	Lemma Borrow l p q r : l {{B}}> [1;0]^^p > [0;1]^^(S (S q)) > [0;0;0;1] > r --> l <{{D}} [1;0]^^(S p) > [0;1]^^(S q) > [0;0;1;0] *> r.	L49	new
7	Lemma	`PassL`	Lemma PassL l p q r : l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] <{{D}} r -->* l <* [0] <{{D}} [1;0]^^(S p) > [0;1]^^(S q) > [0;0;0;1] *> r.	L53	new
8	Lemma	`EndPh`	Lemma EndPh h r : 0inf <* <[1;0]^^(4+h) <* <[1;1;1] <* [0] <{{D}} r -->* 0inf <{{A}} [1;0]^^(4+h) > [1;1;0;0;1] > r.	L57	new
9	Lemma	`EndT`	Lemma EndT l p q : l <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] {{B}}> 0inf -->* l <{{D}} [1;0]^^(S p) > [0;1]^^(S q) > [0;0;1;0] > [1;0;1] > 0inf.	L61	new
10	Lemma	`EndLastT`	Lemma EndLastT l p : l <* <[0;1]^^p <* <[1;1;0] <* <[1;1] <* [0] {{B}}> 0inf -->* l <{{D}} [1;0]^^(p+4) > [1] > 0inf.	L65	new
11	Lemma	`MergeB`	Lemma MergeB l p p' r : l {{B}}> [1;0]^^p > [0;1] > [0;0;0;1] > [1;0]^^p' > r -->* l <{{D}} [1;0]^^(p+p'+3) *> r.	L69	new
12	Lemma	`MergeE`	Lemma MergeE l p : l {{B}}> [1;0]^^p > [0;1] > [0;0;0;1] > 0inf --> l <{{D}} [1;0]^^(p+2) > [1] > 0inf.	L73	new
13	Lemma	`OvT`	Lemma OvT l t : l <* [0] {{B}}> [1;0]^^t > [1] > 0inf -->* l <{{D}} [0;1]^^(S t) > [0;0;0;1] > 0inf.	L77	new
14	Lemma	`OvL`	Lemma OvL l p q r : l <* [0] <* <[0;1]^^(S p) <* <[1;1;0] <* <[0;1]^^q <* <[1;1] <{{D}} r -->* l <{{D}} [0;1]^^(S p) > [0;0;0;1] > [1;0]^^(S q) *> r.	L81	new
15	Lemma	`OvEnd`	Lemma OvEnd h p r : 0inf <* <[1;0]^^(4+h) <* <[1;1;1] <{{D}} [0;1]^^(S (S p)) > [0;0;0;1] > r -->* 0inf <{{A}} [1;0]^^2 > [1;1;0;0;1] > [1;0]^^(h+5) > [0;1]^^(S p) > [0;0;1;0] *> r.	L85	new
16	Lemma	`X1Sw`	Lemma X1Sw l p r : l <* [0] <* <[0;1]^^(S p) <* <[1;1;0] <* <[1;1] <* [0] <{{D}} r -->* l <{{D}} [0;1]^^(S p) > [0;0;1;0;1;0;1] > r.	L89	new
17	Lemma	`X2T`	Lemma X2T l p q k : l <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] {{B}}> [1;0;1;1;0;1] > [0;1]^^(S k) > 0inf -->* l <{{D}} [1;0]^^(S p) > [0;1]^^(S q) > [0;0;1;0] > [1;0]^^3 > [0;1]^^(S k) > [0;0;0;1] > 0inf.	L93	new
18	Definition	`sd`	Definition sd (d : bool) : list Sym := if d then [0;0;0;1] else [0;0;1;0].	L99	new
19	Fixpoint	`RP`	Fixpoint RP (P : list (natnatbool)) (r : side) : side := match P with \| [] => r \| (p,q,d) :: P' => [1;0]^^p > [0;1]^^q > sd d *> RP P' r end.	L101	new
20	Inductive	`Tl`	Inductive Tl := TN \| TA (t : nat) \| TB (k : nat).	L107	new
21	Definition	`RT`	Definition RT (T : Tl) : side := match T with \| TN => 0inf \| TA t => [1;0]^^t > [1] > 0inf \| TB k => [1;0;1;1;0;1] > [0;1]^^k > 0inf end.	L109	new
22	Definition	`K`	Definition K (h : nat) (P : list (natnatbool)) (T : Tl) : Q * tape := 0inf <{{A}} [1;0]^^h > [1;1;0;0;1] > RP P (RT T).	L116	new
23	Definition	`pre`	Definition pre (h : nat) : side := 0inf <* <[1;0]^^(4+h) <* <[1;1;1].	L119	new
24	Definition	`reg`	Definition reg (p q : nat) (l : side) : side := l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(pred q) <* <[1;1].	L122	new
25	Fixpoint	`LP`	Fixpoint LP (Z : list (natnatbool)) (l : side) : side := match Z with \| [] => l \| (p,q,d) :: Z' => LP Z' (reg p q l) end.	L125	new
26	Fixpoint	`OvR`	Fixpoint OvR (Z : list (natnatbool)) (r : side) : side := match Z with \| [] => r \| (p,q,d) :: Z' => [0;1]^^p > [0;0;0;1] > [1;0]^^q *> OvR Z' r end.	L132	new
27	Definition	`touch`	Definition touch (x : natnatbool) : natnatbool := let '(p,q,d) := x in (S p, pred q, negb d).	L138	new
28	Definition	`okR`	Definition okR (x : natnatbool) : Prop := let '(p,q,d) := x in d = false /\ 1 <= q.	L141	new
29	Definition	`okL`	Definition okL (x : natnatbool) : Prop := let '(p,q,d) := x in d = false /\ 2 <= q.	L142	new
30	Definition	`okO`	Definition okO (x : natnatbool) : Prop := let '(p,q,d) := x in 1 <= p /\ 1 <= q.	L143	new
31	Lemma	`RP_app`	Lemma RP_app Z W r : RP (Z ++ W) r = RP Z (RP W r).	L145	new
32	Lemma	`LP_app`	Lemma LP_app Z W l : LP (Z ++ W) l = LP W (LP Z l).	L150	new
33	Lemma	`PassesR`	Lemma PassesR Z : Forall okR Z -> forall l r, l <* [0] {{B}}> RP Z r -->* LP Z l <* [0] {{B}}> r.	L155	new
34	Lemma	`PassesL`	Lemma PassesL Z : Forall okL Z -> forall l r, LP Z l <* [0] <{{D}} r -->* l <* [0] <{{D}} RP (map touch Z) r.	L165	new
35	Lemma	`OvPasses`	Lemma OvPasses Z : Forall okO Z -> forall l r, LP Z l <{{D}} r -->* l <{{D}} OvR Z r.	L175	new
36	Lemma	`okL_R`	Lemma okL_R Z : Forall okL Z -> Forall okR Z.	L185	new
37	Lemma	`Dec`	Lemma Dec h Z p q R T : Forall okL Z -> K h (Z ++ (p, S (S q), true) :: R) T -->+ K (4+h) (map touch Z ++ (S p, S q, false) :: R) T.	L192	new
38	Lemma	`DecMerge`	Lemma DecMerge h Z p p' q' d' R T : Forall okL Z -> K h (Z ++ (p, 1%nat, true) :: (p', q', d') :: R) T -->+ K (4+h) (map touch Z ++ (p+p'+3, q', d') :: R) T.	L203	new
39	Lemma	`DecMergeTail`	Lemma DecMergeTail h Z p t : Forall okL Z -> K h (Z ++ [(p, 1%nat, true)]) (TA t) -->+ K (4+h) (map touch Z) (TA (p+t+3)).	L214	new
40	Lemma	`DecMergeEmpty`	Lemma DecMergeEmpty h Z p : Forall okL Z -> K h (Z ++ [(p, 1%nat, true)]) TN -->+ K (4+h) (map touch Z) (TA (p+2)).	L225	new
41	Lemma	`Forall_snoc`	Lemma Forall_snoc {A} (P : A -> Prop) Z x : Forall P Z -> P x -> Forall P (Z ++ [x]).	L236	new
42	Lemma	`EndR`	Lemma EndR h Z p q : Forall okL Z -> K h (Z ++ [(p, S (S q), false)]) TN -->+ K (4+h) (map touch Z ++ [(S p, S q, false)]) (TA 1).	L239	new
43	Lemma	`EndLast`	Lemma EndLast h Z p : Forall okL Z -> K h (Z ++ [(p, 1%nat, false)]) TN -->+ K (4+h) (map touch Z) (TA (p+4)).	L251	new
44	Lemma	`X2`	Lemma X2 h Z p q k : Forall okL Z -> K h (Z ++ [(p, S (S q), false)]) (TB (S k)) -->+ K (4+h) (map touch Z ++ [(S p, S q, false); (3%nat, S k, true)]) TN.	L263	new
45	Fixpoint	`ovp`	Fixpoint ovp (q : nat) (Z : list (natnatbool)) (t : nat) : list (natnatbool) := match Z with \| [] => [(q, S t, true)] \| (p',q',_) :: Z' => (q, p', true) :: ovp q' Z' t end.	L276	new
46	Lemma	`ovp_eq`	Lemma ovp_eq Z : forall q t, RP (ovp q Z t) 0inf = [1;0]^^q > OvR Z ([0;1]^^(S t) > [0;0;0;1] *> 0inf).	L282	new
47	Lemma	`Ov`	Lemma Ov h p1 q1 Z t : 1 <= q1 -> Forall okR Z -> Forall okO Z -> K h ((S (S p1), q1, false) :: Z) (TA t) -->+ K 2 ((h+5, S p1, false) :: ovp q1 Z t) TN.	L288	adapted
48	Fixpoint	`ovpX`	Fixpoint ovpX (q : nat) (Z : list (natnatbool)) (pa : nat) : list (natnatbool) := match Z with \| [] => [(q, pa, false)] \| (p',q',_) :: Z' => (q, p', true) :: ovpX q' Z' pa end.	L303	new
49	Lemma	`ovpX_eq`	Lemma ovpX_eq Z : forall q pa r, RP (ovpX q Z pa) r = [1;0]^^q > OvR Z ([0;1]^^pa > [0;0;1;0] *> r).	L309	new
50	Lemma	`tailB_eq`	Lemma tailB_eq n : [0;0;1;0;1;0;1] > [1;0]^^(S n) > [1] > 0inf = [0;0;1;0] > RT (TB n).	L315	new
51	Lemma	`X1`	Lemma X1 h p1 q1 Z pa pb : 1 <= q1 -> Forall okR Z -> Forall okO Z -> K h ((S (S p1), q1, false) :: Z ++ [(S pa, 1%nat, false); (pb, 1%nat, false)]) TN -->+ K 2 ((h+5, S p1, false) :: ovpX q1 Z (S pa)) (TB (pb+3)).	L323	new
52	Lemma	`init0`	Lemma init0 : c0 -->* K 2 [(11%nat, 11%nat, false)] TN.	L346	new
53	Definition	`base`	Definition base : list (natnatbool) := [(95%nat, 68%nat, false); (34%nat, 33%nat, true); (10%nat, 15%nat, true); (1%nat, 24%nat, true)].	L349	new
54	Lemma	`init`	Lemma init : c0 -->* K 2 base TN.	L352	adapted
55	Definition	`bv`	Definition bv (d : bool) : nat := if d then 1 else 0.	L364	new
56	Fixpoint	`dv`	Fixpoint dv (P : list tri) : nat := match P with \| [] => 0 \| (_,_,d) :: P' => bv d + 2 * dv P' end.	L366	new
57	Definition	`dig`	Definition dig (x : tri) : bool := let '(_,_,d) := x in d.	L372	new
58	Definition	`dig0`	Definition dig0 (x : tri) : Prop := dig x = false.	L373	new
59	Lemma	`dv_lt`	Lemma dv_lt P : dv P < 2 ^ length P.	L377	new
60	Lemma	`dv_zeros`	Lemma dv_zeros Z R : Forall dig0 Z -> dv (Z ++ R) = 2 ^ length Z * dv R.	L383	new
61	Lemma	`dv_tz`	Lemma dv_tz Z R : Forall dig0 Z -> dv (map touch Z ++ R) + 1 = 2 ^ length Z + 2 ^ length Z * dv R.	L390	new
62	Fixpoint	`AllI`	Fixpoint AllI (Pr : nat -> tri -> list tri -> Prop) (i : nat) (P : list tri) : Prop := match P with \| [] => True \| x :: Y => Pr i x Y /\ AllI Pr (S i) Y end.	L398	new
63	Lemma	`AllI_app`	Lemma AllI_app Pr Z : forall i R, AllI Pr i (Z ++ R) -> AllI Pr (i + length Z) R.	L404	new
64	Lemma	`AllI_mono`	Lemma AllI_mono (Pr Pr' : nat -> tri -> list tri -> Prop) P : forall i, (forall j x Y, i <= j -> Pr j x Y -> Pr' j x Y) -> AllI Pr i P -> AllI Pr' i P.	L411	new
65	Lemma	`AllI_shift`	Lemma AllI_shift (Pr Pr' : nat -> tri -> list tri -> Prop) P : forall i, (forall j x Y, i <= j -> Pr (S j) x Y -> Pr' j x Y) -> AllI Pr (S i) P -> AllI Pr' i P.	L419	new
66	Lemma	`AllI_touchZ`	Lemma AllI_touchZ (Pr Pr' : nat -> tri -> list tri -> Prop) R R' : forall Z i, Forall dig0 Z -> (forall j p q Zr, Forall dig0 Zr -> j + S (length Zr) = i + length Z -> Pr j (p,q,false) (Zr ++ R) -> Pr' j (S p, pred q, true) (map touch Zr ++ R')) -> AllI Pr i (Z ++ R) -> AllI Pr' (i + length Z) R' -> AllI Pr' i (map touch Z ++ R').	L428	new
67	Inductive	`phase`	Inductive phase := E1 \| E2 \| E1t \| E2t \| T0 \| L1 \| L2 \| LX.	L449	new
68	Definition	`PN`	Definition PN (ph : phase) (c4 : bool) (p q n tv : nat) : Prop := match ph with \| E1 => match n with \| 0 => q >= tv + 2 ^ n + 1 /\ p + tv + 2 ^ n >= 3 \| S _ => q >= tv + 3 * 2 ^ n + 1 /\ (p + tv) mod 2 = 1 /\ p + tv + 2 ^ n >= 3 * 2 ^ n end … +35 lines	L452	new
69	Definition	`PI`	Definition PI (ph : phase) (h i p q n tv : nat) : Prop := match i with \| 1 => h mod 2 = 0 /\ match ph with \| E1 \| E1t => 2 <= n /\ p + tv + 2 ^ n + 3 >= 11 * 2 ^ n /\ h + 4 * (tv + 2 ^ n) + 6 >= 12 * 2 ^ n \| E2 \| E2t => 2 <= n /\ p + tv + 3 >= 11 * 2 ^ n /\ h + 4 * tv + 6 >= 12 * 2 ^ n … +14 lines	L495	new
70	Definition	`PC`	Definition PC (ph : phase) (c4 : bool) (h i p q n tv : nat) : Prop := 1 <= p /\ 1 <= q /\ PN ph c4 p q n tv /\ PI ph h i p q n tv.	L516	new
71	Definition	`Lift`	Definition Lift (Pr : nat -> nat -> nat -> nat -> nat -> Prop) (i : nat) (x : tri) (Y : list tri) : Prop := let '(p,q,d) := x in Pr i p q (length Y) (dv (x :: Y)).	L519	new
72	Definition	`PCx`	Definition PCx (ph : phase) (c4 : bool) (h : nat) := Lift (PC ph c4 h).	L522	new
73	Lemma	`pow_pos`	Lemma pow_pos n : 1 <= 2 ^ n.	L531	new
74	Lemma	`ob_touch`	Lemma ob_touch ph c4 h i p q n tv : 1 <= tv -> 2 <= q -> PC ph c4 h i p q n tv -> PC ph c4 (4 + h) i (S p) (pred q) n (tv - 1).	L535	new
75	Lemma	`pow_S`	Lemma pow_S n : 2 ^ S n = 2 * 2 ^ n.	L543	new
76	Lemma	`ob_merge`	Lemma ob_merge ph c4 h i p q n u U : (ph = L1 \/ ph = L2 \/ ph = LX) -> 1 <= n -> 2 <= u -> u mod 2 = 0 -> U mod 2 = 0 -> U + u <= 2 * 2 ^ n -> (ph = L1 -> U + u <= 2 ^ n) -> (ph = LX -> 2 <= n) -> (ph = L1 -> c4 = true -> 2 <= n) -> (i = 1 -> 2 <= n) -> (ph = LX -> i = 1 -> 3 <= n) -> 2 <= q -> PC ph c4 h i p q (S n) (u + 2 * U) -> PC ph c4 (4 + h) i (S p) (pred q) n (u - 1 + U).	L551	new
77	Lemma	`ob_mt`	Lemma ob_mt c4 h i p q n : 2 <= q -> (i = 1 -> 1 <= n) -> PC L2 c4 h i p q (S n) (2 * 2 ^ n) -> PC L2 false (4 + h) i (S p) (pred q) n (2 * 2 ^ n - 1).	L567	new
78	Lemma	`ob_fuse`	Lemma ob_fuse ph c4 h h' k p p' q' n tv : (ph = L1 \/ ph = L2 \/ ph = LX) -> 3 <= k -> PC ph c4 h (S k) p' q' n tv -> PC ph c4 h' k (p + p' + 3) q' n tv.	L576	new
79	Lemma	`ob_far`	Lemma ob_far ph c4 h h' i j p q n tv : 3 <= i -> 3 <= j -> PC ph c4 h i p q n tv -> PC ph c4 h' j p q n tv.	L585	new
80	Definition	`endtr`	Definition endtr (ph ph' : phase) : Prop := (ph = E1 /\ ph' = E2) \/ (ph = E1t /\ ph' = E2t).	L593	new
81	Lemma	`ob_end`	Lemma ob_end ph ph' h i p q n : endtr ph ph' -> 1 <= n -> 2 <= q -> PC ph false h i p q n 0 -> PC ph' false (4 + h) i (S p) (pred q) n (2 ^ n - 1).	L595	new
82	Lemma	`ob_end_top`	Lemma ob_end_top ph ph' h i p q : endtr ph ph' -> 3 <= i -> PC ph false h i p (S (S q)) 0 0 -> PC ph' false (4 + h) i (S p) (S q) 0 0.	L603	new
83	Lemma	`ob_endlast`	Lemma ob_endlast c4 h i p q n : 2 <= q -> PC L1 c4 h i p q (S n) 0 -> PC L2 c4 (4 + h) i (S p) (pred q) n (2 * 2 ^ n - 1).	L612	new
84	Lemma	`ob_x2`	Lemma ob_x2 h i p q n : 1 <= n -> 2 <= q -> PC T0 false h i p q n 0 -> PC E1t false (4 + h) i (S p) (pred q) (S n) (3 * 2 ^ n - 1).	L621	new
85	Lemma	`ob_x2_top`	Lemma ob_x2_top h i p q : 3 <= i -> PC T0 false h i p (S (S q)) 0 0 -> PC E1t false (4 + h) i (S p) (S q) 1 2.	L629	new
86	Lemma	`ob_x2_new`	Lemma ob_x2_new h i k : 3 <= i -> 3 <= k -> PC E1t false h i 3 k 0 1.	L637	new
87	Definition	`ovtr`	Definition ovtr (ph ph' : phase) (c4' : bool) (Xp : nat -> Prop) : Prop := (ph = E2 /\ ph' = L1 /\ c4' = false /\ Xp = (fun x => x <> 4)) \/ (ph = E2 /\ ph' = LX /\ c4' = false /\ Xp = (fun x => x = 4)) \/ (ph = E2t /\ ph' = L1 /\ c4' = true /\ Xp = (fun _ => True)) \/ (ph = L2 /\ ph' = E1 /\ c4' = false /\ Xp = (fun _ => True)).	L645	new
88	Lemma	`ob_ov_head`	Lemma ob_ov_head ph ph' c4' Xp h p1 q1 n : ovtr ph ph' c4' Xp -> PC ph false h 1 (S (S p1)) q1 n 0 -> PC ph' c4' 2 1 (h + 5) (S p1) (S n) (2 * (2 * 2 ^ n) - 2).	L651	new
89	Lemma	`ob_ov_step`	Lemma ob_ov_step ph ph' c4' Xp h i pp q p' q' m : ovtr ph ph' c4' Xp -> 1 <= i -> PC ph false h i pp q (S m) 0 -> PC ph false h (S i) p' q' m 0 -> (m = 0 -> Xp p') -> PC ph' c4' 2 (S i) q p' (S m) (2 * (2 * 2 ^ m) - 1).	L663	new
90	Lemma	`ob_ov_base`	Lemma ob_ov_base ph ph' c4' Xp h i pp q t : ovtr ph ph' c4' Xp -> 1 <= i -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) -> PC ph false h i pp q 0 0 -> PC ph' c4' 2 (S i) q (S t) 0 1.	L679	new
91	Lemma	`ob_x1_head`	Lemma ob_x1_head h p1 q1 n : PC LX false h 1 (S (S p1)) q1 (S (S n)) 0 -> PC T0 false 2 1 (h + 5) (S p1) (S n) (2 * 2 ^ n - 2).	L691	new
92	Lemma	`ob_x1_step`	Lemma ob_x1_step h i pp q p' q' m : 1 <= i -> PC LX false h i pp q (S (S (S m))) 0 -> PC LX false h (S i) p' q' (S (S m)) 0 -> PC T0 false 2 (S i) q p' (S m) (2 * 2 ^ m - 1).	L698	new
93	Lemma	`ob_x1_base`	Lemma ob_x1_base h i pp q pa : 1 <= i -> PC LX false h i pp q 2 0 -> PC LX false h (S i) (S pa) 1 1 0 -> PC T0 false 2 (S i) q (S pa) 0 0.	L706	new
94	Lemma	`dv_zero`	Lemma dv_zero Z : Forall dig0 Z -> dv Z = 0.	L715	new
95	Lemma	`dv_tz'`	Lemma dv_tz' Z R : Forall dig0 Z -> dv (map touch Z ++ R) = 2 ^ length Z - 1 + 2 ^ length Z * dv R.	L718	new
96	Lemma	`ovp_len`	Lemma ovp_len q Z t : length (ovp q Z t) = S (length Z).	L721	new
97	Lemma	`ovp_dv`	Lemma ovp_dv q Z t : dv (ovp q Z t) + 1 = 2 ^ S (length Z).	L724	new
98	Lemma	`ovpX_len`	Lemma ovpX_len q Z pa : length (ovpX q Z pa) = S (length Z).	L730	new
99	Lemma	`ovpX_dv`	Lemma ovpX_dv q Z pa : dv (ovpX q Z pa) + 1 = 2 ^ length Z.	L733	new
100	Fixpoint	`lastOK`	Fixpoint lastOK (Xp : nat -> Prop) (Z : list tri) : Prop := match Z with \| [] => True \| [(p,_,_)] => Xp p \| _ :: Z' => lastOK Xp Z' end.	L739	new
101	Lemma	`lastOK_cons`	Lemma lastOK_cons Xp p q d Z : lastOK Xp ((p,q,d) :: Z) -> (Z = [] -> Xp p) /\ lastOK Xp Z.	L746	new
102	Lemma	`lastOK_dec`	Lemma lastOK_dec Z : lastOK (fun x => x = 4) Z \/ lastOK (fun x => x <> 4) Z.	L749	new
103	Lemma	`AllI_ovp`	Lemma AllI_ovp ph ph' c4' Xp h t : ovtr ph ph' c4' Xp -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) -> forall Z i pp q, 1 <= i -> Forall dig0 Z -> lastOK Xp Z -> PC ph false h i pp q (length Z) 0 -> AllI (PCx ph false h) (S i) Z -> AllI (PCx ph' c4' 2) (S i) (ovp q Z t).	L755	new
104	Lemma	`AllI_ovpX`	Lemma AllI_ovpX h pa pb : forall Z i pp q, 1 <= i -> Forall dig0 Z -> PC LX false h i pp q (S (S (length Z))) 0 -> AllI (PCx LX false h) (S i) (Z ++ [(S pa, 1, false); (pb, 1, false)]) -> AllI (PCx T0 false 2) (S i) (ovpX q Z (S pa)).	L773	new
105	Lemma	`passq`	Lemma passq ph c4 h i p q n tv : PC ph c4 h i p q n tv -> 2 <= tv -> tv mod 2 = 0 -> 2 <= q.	L795	new
106	Lemma	`Z_okL`	Lemma Z_okL ph c4 h : forall Z i x R, Forall dig0 Z -> dig x = true -> AllI (PCx ph c4 h) i (Z ++ x :: R) -> Forall okL Z.	L801	new
107	Lemma	`borrow1`	Lemma borrow1 ph c4 h k p n tv : 1 <= k -> tv mod 2 = 1 -> PC ph c4 h k p 1 n tv -> (ph = L1 \/ ph = L2 \/ ph = LX) /\ 3 <= k /\ (ph = L1 -> 1 <= n /\ tv + 1 <= 2 ^ n /\ (c4 = true -> 2 <= n)) /\ (ph = LX -> 2 <= n).	L814	new
108	Lemma	`even2`	Lemma even2 x : (2 * x) mod 2 = 0.	L828	new
109	Lemma	`pc_len`	Lemma pc_len (Pr : nat -> tri -> list tri -> Prop) i P : AllI Pr i P -> True.	L831	new
110	Lemma	`inv_Dec`	Lemma inv_Dec ph c4 h Z p q R : Forall dig0 Z -> AllI (PCx ph c4 h) 1 (Z ++ (p, S (S q), true) :: R) -> AllI (PCx ph c4 (4 + h)) 1 (map touch Z ++ (S p, S q, false) :: R).	L837	new
111	Lemma	`snoc_nn`	Lemma snoc_nn (Z : list tri) y : Z ++ [y] <> [].	L858	new
112	Definition	`minlen`	Definition minlen (ph : phase) : nat := match ph with LX => 3 \| L2 => 1 \| _ => 2 end.	L861	new
113	Lemma	`head_len`	Lemma head_len ph c4 h x Y : PCx ph c4 h 1 x Y -> minlen ph <= length Y.	L863	new
114	Lemma	`AllI_len`	Lemma AllI_len ph c4 h P : P <> [] -> AllI (PCx ph c4 h) 1 P -> S (minlen ph) <= length P.	L869	new
115	Lemma	`q2_V0`	Lemma q2_V0 ph c4 h i p q n : PC ph c4 h i p q n 0 -> 1 <= n -> (ph = LX -> 2 <= n) -> 2 <= q.	L874	new
116	Lemma	`p1_V0`	Lemma p1_V0 ph c4 h p q n : PC ph c4 h 1 p q n 0 -> (ph = E2 \/ ph = E2t \/ ph = L2 \/ ph = LX) -> 2 <= p.	L880	new
117	Lemma	`L2_c4_V0`	Lemma L2_c4_V0 h i p q : PC L2 true h i p q 0 0 -> False.	L886	new
118	Lemma	`AllI_okRO`	Lemma AllI_okRO ph c4 h : forall Z i, Forall dig0 Z -> AllI (PCx ph c4 h) i Z -> Forall okR Z /\ Forall okO Z.	L889	new
119	Lemma	`inv_Merge`	Lemma inv_Merge ph c4 h Z p p' q' d' R0 : Forall dig0 Z -> AllI (PCx ph c4 h) 1 (Z ++ (p, 1, true) :: (p', q', d') :: R0) -> AllI (PCx ph c4 (4 + h)) 1 (map touch Z ++ (p + p' + 3, q', d') :: R0).	L897	new
120	Lemma	`inv_MT`	Lemma inv_MT c4 h Z p : Forall dig0 Z -> AllI (PCx L2 c4 h) 1 (Z ++ [(p, 1, true)]) -> AllI (PCx L2 false (4 + h)) 1 (map touch Z) /\ 2 <= length Z.	L940	new
121	Lemma	`inv_End`	Lemma inv_End ph ph' h Z p q : endtr ph ph' -> Forall dig0 Z -> AllI (PCx ph false h) 1 (Z ++ [(p, S (S q), false)]) -> AllI (PCx ph' false (4 + h)) 1 (map touch Z ++ [(S p, S q, false)]).	L958	new
122	Lemma	`inv_X2`	Lemma inv_X2 h Z p q k : Forall dig0 Z -> 3 <= k -> AllI (PCx T0 false h) 1 (Z ++ [(p, S (S q), false)]) -> AllI (PCx E1t false (4 + h)) 1 (map touch Z ++ [(S p, S q, false); (3, k, true)]).	L980	new
123	Lemma	`inv_EndLast`	Lemma inv_EndLast c4 h Z p : Forall dig0 Z -> AllI (PCx L1 c4 h) 1 (Z ++ [(p, 1, false)]) -> AllI (PCx L2 c4 (4 + h)) 1 (map touch Z) /\ 2 <= length Z.	L1003	new
124	Lemma	`inv_Ov`	Lemma inv_Ov ph ph' c4' Xp h p1 q1 Z t : ovtr ph ph' c4' Xp -> (ph = L2 -> 2 <= t) -> (ph <> L2 -> t = 1) -> Forall dig0 Z -> lastOK Xp Z -> AllI (PCx ph false h) 1 ((S (S p1), q1, false) :: Z) -> AllI (PCx ph' c4' 2) 1 ((h + 5, S p1, false) :: ovp q1 Z t).	L1020	new
125	Lemma	`inv_X1`	Lemma inv_X1 h p1 q1 Z pa pb : Forall dig0 Z -> AllI (PCx LX false h) 1 ((S (S p1), q1, false) :: Z ++ [(S pa, 1, false); (pb, 1, false)]) -> AllI (PCx T0 false 2) 1 ((h + 5, S p1, false) :: ovpX q1 Z (S pa)).	L1035	new
126	Record	`st`	Record st := mkst { sh : nat; sP : list (natnatbool); sT : Tl; sph : phase; sc4 : bool }.	L1054	new
127	Definition	`Cf`	Definition Cf (s : st) : Q * tape := K (sh s) (sP s) (sT s).	L1056	new
128	Definition	`TC`	Definition TC (ph : phase) (c4 : bool) (T : Tl) : Prop := match ph with \| E1 \| E1t \| LX => T = TN /\ c4 = false \| L1 => T = TN \| E2 \| E2t => T = TA 1 /\ c4 = false \| T0 => (exists k, T = TB k /\ 3 <= k) /\ c4 = false … +2 lines	L1058	new
129	Definition	`J`	Definition J (s : st) : Prop := sP s <> [] /\ TC (sph s) (sc4 s) (sT s) /\ AllI (PCx (sph s) (sc4 s) (sh s)) 1 (sP s).	L1067	new
130	Lemma	`split1`	Lemma split1 (P : list tri) : (exists Z x R, P = Z ++ x :: R /\ Forall dig0 Z /\ dig x = true) \/ Forall dig0 P.	L1070	new
131	Lemma	`Z_okL_V0`	Lemma Z_okL_V0 ph c4 h y : ph <> LX -> forall Z i, Forall dig0 (Z ++ [y]) -> AllI (PCx ph c4 h) i (Z ++ [y]) -> Forall okL Z.	L1082	new
132	Lemma	`lastOK_True`	Lemma lastOK_True Z : lastOK (fun _ => True) Z.	L1092	new
133	Lemma	`Forall_snoc_inv`	Lemma Forall_snoc_inv (Pr : tri -> Prop) Z y : Forall Pr (Z ++ [y]) -> Forall Pr Z /\ Pr y.	L1095	new
134	Lemma	`last_pc`	Lemma last_pc ph c4 h Z p q d : Forall dig0 (Z ++ [(p,q,d)]) -> AllI (PCx ph c4 h) 1 (Z ++ [(p,q,d)]) -> d = false /\ PC ph c4 h (1 + length Z) p q 0 0.	L1098	new
135	Lemma	`first_pc`	Lemma first_pc ph c4 h p q d Z : Forall dig0 ((p,q,d) :: Z) -> AllI (PCx ph c4 h) 1 ((p,q,d) :: Z) -> d = false /\ PC ph c4 h 1 p q (length Z) 0 /\ Forall dig0 Z /\ AllI (PCx ph c4 h) 2 Z.	L1106	new
136	Lemma	`Jstep`	Lemma Jstep : forall s, J s -> exists s', Cf s -->+ Cf s' /\ J s'.	L1116	new
137	Lemma	`J_base`	Lemma J_base : J (mkst 2 base TN E1 false).	L1262	new
138	Lemma	`nonhalt`	Lemma nonhalt : ~ halts tm c0.	L1268	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 138: 2. Rules (macro steps; each is an exact run of at least 1 step from one K to the next)

Notation used in the rules:

Π_{j<k}[...] is a product over pairs.
R is everything to the right of the touched pairs, tail included, and it is unchanged.

The rules cover every K, except the "outside" cases listed after the table.

Let k := least j with d_j = 1 (when V > 0).

Dec_k          q_1..q_{k-1} >= 2, q_k >= 2:
  0^inf <A (10)^h 11001 Π_{j<k}[p_j,q_j,0] [p_k,q_k,1] R 0^inf
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<k}[p_j+1,q_j-1,1] [p_k+1,q_k-1,0] R 0^inf

DecMerge_k     q_1..q_{k-1} >= 2, q_k = 1, k < L:
  ... Π_{j<k}[p_j,q_j,0] [p_k,1,1] [p',q',d'] R
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<k}[p_j+1,q_j-1,1] [p_k+p'+3, q', d'] R

DecMergeTail   q_1..q_{L-1} >= 2, k = L, q_L = 1, T = T1(t):
  ... Π_{j<L}[p_j,q_j,0] [p_L,1,1] (10)^t 1 0^inf
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<L}[p_j+1,q_j-1,1] (10)^(p_L+t+3) 1 0^inf

DecMergeEmpty  as DecMergeTail but T = -:          ... [p_L,1,1] 0^inf --> ... (10)^(p_L+2) 1 0^inf

End            V = 0, T = -, all q_j >= 2:
  0^inf <A (10)^h 11001 Π_{j<L}[p_j,q_j,0] [p_L,q_L,0] 0^inf
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<L}[p_j+1,q_j-1,1] [p_L+1,q_L-1,0] (10)^1 1 0^inf

EndLast        V = 0, T = -, q_1..q_{L-1} >= 2, q_L = 1:
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<L}[p_j+1,q_j-1,1] (10)^(p_L+4) 1 0^inf

Ov             V = 0, T = T1(t), p_1 >= 2:
  0^inf <A (10)^h 11001 Π_{j<=L}[p_j,q_j,0] (10)^t 1 0^inf
  --> 0^inf <A (10)^2 11001 [h+5, p_1-1, 0] Π_{j=1..L-1}[q_j, p_{j+1}, 1] [q_L, t+1, 1] 0^inf

X1             V = 0, T = -, L >= 3, q_1..q_{L-2} >= 2, q_{L-1} = q_L = 1, p_1 >= 2:
  0^inf <A (10)^h 11001 Π_{j<=L}[p_j,q_j,0] 0^inf
  --> 0^inf <A (10)^2 11001 [h+5, p_1-1, 0] Π_{j=1..L-3}[q_j, p_{j+1}, 1] [q_{L-2}, p_{L-1}, 0] (101)^2 (01)^(p_L+3) 0^inf

X2             V = 0, T = T2(k), all q_j >= 2:
  0^inf <A (10)^h 11001 Π_{j<=L}[p_j,q_j,0] (101)^2 (01)^k 0^inf
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<L}[p_j+1,q_j-1,1] [p_L+1,q_L-1,0] [3, k, 1] 0^inf

In words:

Each Dec* subtracts 1 from V: pairs 1..k are touched.
End* and X2 touch every pair; they behave like a decrement from 0 that the tail absorbs.
Ov and X1 re-pair the blocks, so that the old splits become the new digit blocks, and they reset h to 2.

Physically, a decrement is three short bounces at the left end followed by one sweep to the borrow pair and back.

Outside cases are the K for which no rule above applies:

(o1) Some pass-through pair j < k has q_j = 1.
(o2) k = L, q_L = 1 and T = T2.
(o3) V = 0, T = -, and some q_j = 1 with j ≤ L−1, but the shape is not X1.
(o4) The X1 shape with L ≤ 2 or p_1 = 1.
(o5) Ov with p_1 = 1.
(o6) X2 with some q_j = 1.
(o7) L = 0.

At least (o1), (o3) and (o6) can halt (direct simulation):

case	configuration	halts after
(o1)	K(6; (5,1,0),(7,4,1); −)	1,480 steps
(o3)	K(2; (6,1,0),(5,8,0),(11,2,0),(12,3,0); −)	1,554 steps
(o6)	K(6; (9,1,0),(5,4,0); T2(5))	1,684 steps

In random samples, 45 of 56 (o1) instances, 24 of 35 (o3) and 27 of 44 (o6) halted. The others jump to an unrelated K.

Either way, the proof must keep the orbit out of (o1)–(o7), and it does so without using what the machine does there.

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

4 machines, 4 killed, 0 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
#3 kill 4	`1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---`	✓Killed: never halts	this kill
#25 kill 7	`1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---`	✓Killed: never halts	parent link; = #3's table, run from state C; targeting: follow-on to #3; named in #25's .v header; named in #25's proof.md; named in #25's notes.md; named in #3's notes.md · review · same machine as this kill? (same table, started in #3's C; trajectory twin; tables, pictures and numbers side by side)
#24 kill 8	`1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---`	✓Killed: never halts	parent link; = #3's table mirrored, run from state D; targeting: follow-on to #3; named in #24's .v header; named in #24's proof.md; named in #24's notes.md; named in #3's notes.md · review · same machine as this kill? (same table mirrored, started in #3's D; trajectory twin; tables, pictures and numbers side by side)
#3b kill 12	`1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---`	✓Killed: never halts	parent link; = #3's table, run from state B; named in #3b's .v header; named in #3b's proof.md; named in #3b's notes.md · review · same machine as this kill? (same table, started in #3's B; different orbit; tables, pictures and numbers side by side) · mechanism
Named in a file but not linked (not counted as family)
W7-1	`1RB1RC_1LC1LE_1RD0RA_1LB0RA_0LD1LF_1LD---`	▲Stuck	named in W7-1's proof.md; named in W7-1's notes.md · mechanism
W4-6	`1RB---_0RC0RF_0RD0RA_1RE0LB_1LF0LE_1RC0LE`	▲Stuck	named in W4-6's notes.md · mechanism
W7-2	`1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD`	○Open	named in W7-2's proof.md; named in W7-2's notes.md · mechanism
W4-3 kill 20	`1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---`	✓Killed: never halts	named in W4-3's proof.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 53 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 24.69 s
✓
.v hash matches the checked hash
.v = checked sha256 cfa603a314f6…; submission/ copy = checked sha256 cfa603a314f6…
✓
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 L86: - Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):
- notes.md L113: - 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.
- notes.md L122: ## Checkpoint B (Dennis, 2026-10-10)
- proof.md L1: # 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---: informal proof (Checkpoint B)
○
Family posted together?
3 other kill(s) in the family: #25, #24, #3b; the Discord draft names 2 of them

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

Review pages on file: review-invariant-2.md · review-invariant.md

Files

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

name	size	changed
notes.md ↓	14 KB	2026-10-10 16:56
proof.md ↓	57 KB	2026-10-10 05:55
how_proved.md ↓	1.6 KB	2026-10-14 10:51
status.json ↓	489 B	2026-10-13 06:44
observe.json ↓	18 KB	2026-10-10 17:57
1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v ↓	62 KB	2026-10-10 11:50
img/	12 items	2026-10-10 16:30
rocq/	17 items	2026-10-10 07:02
scripts/	18 items	2026-10-10 17:55
submission/	6 items	2026-10-12 12:51
work/	2 items	2026-10-12 12:41
check_proof.py ↓	46 KB	2026-10-10 05:32
review-invariant-2.md ↓	17 KB	2026-10-10 05:54
review-invariant.md ↓	12 KB	2026-10-10 05:11

status.json in full

{
 "tm": "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "pr": "https://github.com/ccz181078/busycoq/pull/15",
 "pr_file": "verify/Skelet1LikeC2_1RB0LD.v",
 "pr_state": "merged",
 "pr_opened": "2026-10-10",
 "posted": "2026-10-10 (bbchallenge Discord #bb6, by Dennis)",
 "pr_comments": 0,
 "pr_merged_at": "2026-10-13T12:25:47Z",
 "pr_merged_by": "ccz181078"
}

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

1 contract warning

diagrams: 6 (want 3-5)

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 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (the kill review: python3 -B tools/killreview.py 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, which also renders a derived kill's same-machine pictures)