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 / W5-4

`1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB`

W5-4local proof 31Kill claimedBell eats counterbbchallenge ↗Explorer

How we proved it never halts

A size bound plus a remainder that never hits zero

Most of the tape is a long row of 10 pairs, the "bell", with one 00 in it, the "wall"; at the right end sits a counter whose bits sit every third cell (a 0 means the bit is set). Each round trip of the head moves the wall two pairs right and counts the counter down by 1. When the bell ahead of the wall is used up, the wall bites the counter's low end, and usually the pairs behind the wall become the new bell. But a bite on set low bits starts smaller nested copies of the whole process on the rest of the counter.

The only way to halt is a bite on a counter with every bit set, exactly when two pairs of bell remain. At each cycle start the proof tracks two facts. The bell is long: at least 2 pairs more than a power of 2 set by the counter's width. And a certain mix of bell length, width and counter value leaves remainder 1 or 2 when divided by 3; each cycle swaps the two, so it is never 0.

Why that settles it: among long-bell starts, the ones headed for the halt all have remainder 0, apart from one small state the proof excludes separately. The nested copies, and the rest of a cycle after them, start with an odd bell when the width is not a multiple of 3, which cannot reach the halt either. Nobody knows whether nested copies always finish, so the proof shows "no halt within N steps" for every N, by induction, from the good start reached at step 327.

The Rocq proof checks every move as an exact run, the arithmetic of rounds and bites, both invariants and that induction, and runs the 327-step opening directly.

#31local proof number

1,039lines of Rocq

35 sto compile

6/6automatic checks

Overview

In one sentence

Wall walks the bell, counting a zone down; bites its low end each cycle. Halts only if an overflow hits q=4.

Submitted mechanism Counter and bell. A bell (10)^q with a wall 00, then a zone holding a binary counter whose bits sit 3 cells apart (a set bit is a 0). Each round trip from the wall moves the wall 2 pairs right and decrements the counter. At 0 an overflow resets the counter according to the zone width modulo 3 (rules O0–O2 of the write-up). (submission/README.md, Mechanism)

Upstream: Kill claimed · PR #28merged 2026-10-16 07:09 UTC by ccz181078 · PR_BEC.v · TM5 · on Submissions →
Rocq proof: check_kill PASS · first Oct 13 13:03
1,039 lines · 45 KB .v · compile 34.7 s · coqchk pass · 0 axioms · PASS Oct 13 13:03
· the .v file
Automatic review: 6 of 6 checks passtemplate: verify/BECv5.v Module TM1 (adapted from) · details in Proof →
Class: Bell eats counterours: Bell eats counter (sheet) · ours adds: two-level: a down-counting binary zone (bits 3 cells apart, anchored at the far end) bitten from its low end; W4-2's architecture mirrored · med confidence
On the list: not on BB6_holdouts_663.txt (line 525 of the previous list) · historical 740 line 525
eqv ×1sim 1e15

Your calls on file 3

funded: option: proof · date: 2026-10-13
next: post the Discord draft (submission/discord.md, not posted; fill in <LINK>, search #bb6 first); add to the next upstream PR batch
2026-10-13 · proof: Fund one more stage on W5-4 to close the two open sub-lemmas and write proof.md, then formalize, or park it at the invariant stage? (Dennis 2026-10-13: 'go with recommendations')

Mechanism

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

How it works: 3 notes

R(p,q,Z) = 0^inf (10)^p 1 C> 0 0 (10)^q Z: each round the wall 00 moves 2 pairs right (q-2) and the zone Z counts down by 1 (zeros = set bits on the lattice j = w-1-3i); at v = 0 it refills (O0/O1/O2). At q <= 2 the wall bites Z's low end (B0/B1/B2/B2') and a new cycle starts with n one or two pairs longer.
Two levels: per two calm cycles v drops by 1; near n = 2^(L+1) the zone gains a bit (level-up), sometimes through a chaotic phase of nested bites (B2'', closed as a stack of the same rules in Wave 5). The closed rules reproduce the direct run at all 4,197 cycle starts to 1e11.
Why it never halts (Wave 5): the invariant I = {d = n - 2^(cap+1) >= 2, M = n + 2v - 2^(cap+2) != 0 mod 3}. Every rule keeps M or negates it mod 3, and the only halting starts from d >= 2 have M = 0. The blank run is in I from step 327. Checked on 7.9M states; two sub-lemmas (continuation cycles, nested levels) still need a paper argument.

Figures for Checkpoint A

Fig 1 · bbchallenge default view, first 10,000 steps
The site's view. The striped middle is the bell (10)^n; the dense band at the right edge is the zone.

Fig 2 · One cycle: the wall walks rightQ1
Each thin diagonal is one round. Compare the wall's start per round and the zone width at the right edge.

Fig 3 · Counter fill per cycle, levels 3 to 21Q2
One dot per cycle. Follow one descending curve (a calm level), then look at the scatter where curves restart (level-ups).

More figures (2)Fig 4–5: One round, step by step · Nested bite (no closed form yet)

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

rule	from ⟶ to	cases	steps	checked
init	0^∞ A> 0^∞ ⟶ 0^∞ C> 0 0 1² 0^∞	= R(-1,0,11); the next cycle starts follow from the rules below (abstract run = direct run at 4,200 cycle starts)	4	✓1/1
R1 round	0^∞ (10)^p 1 C> 0 0 (10)^q Z 0^∞ ⟶ 0^∞ (10)^p+2 1 C> 0 0 (10)^q-2 dec(Z) 0^∞	q >= 3, Z has a zero, w = 0 or 2 mod 3; dec: leftmost zero j -> 1, zeros at j-3, j-6, ... >= 2	—	✓150/150
R2 round	0^∞ (10)^p 1 C> 0 0 (10)^q Z 0^∞ ⟶ 0^∞ (10)^p+2 1 C> 0 0 (10)^q-3 11 dec(Z) 0^∞	q >= 3, Z has a zero, w = 1 mod 3 (one bell pair joins the zone)	—	✓150/150
O2 overflow	0^∞ (10)^p 1 C> 0 0 (10)^q 1^w 0^∞ ⟶ 0^∞ (10)^p+2 1 C> 0 0 (10)^q-2 (110)^(w-2)/3 111 0^∞	q >= 3, w = 2 mod 3: zone + 1 cell, all bits set (v = 2^L - 1)	—	✓52/52
O1 overflow	0^∞ (10)^p 1 C> 0 0 (10)^q 1^w 0^∞ ⟶ 0^∞ (10)^p+2 1 C> 0 0 (10)^q-2 allset(w+1) 0^∞	q >= 3, w = 1 mod 3; allset(u) = every lattice position >= 2 set	—	✓53/53
O0 overflow	0^∞ (10)^p 1 C> 0 0 (10)^q 1^w 0^∞ ⟶ 0^∞ (10)^p+2 1 C> 0 0 (10)^q-3 1⁵ (0 1²)^w/3-1 0 1³ 0^∞	q >= 3, w = 0 mod 3: zone + 3 cells, v = 2^L - 2	—	✓45/45
B2 bite	0^∞ (10)^p 1 C> 0 0 (10)² 111 Y 0^∞ ⟶ 0^∞ (10)^p+2 1 C> 0 0 10 1 Y 0^∞	q = 2, zone starts 111; re-parse: a leading 10 of 1Y joins the bell	14	✓150/150
B2' bite, k=1	0^∞ (10)^p 1 C> 0 0 (10)² 110 111 Y 0^∞ ⟶ 0^∞ (10)^p+2 1 C> 0 0 (10)³ Y 0^∞	q = 2, lowest bit set, next clear; Y starts 11	32	✓150/150
H halt	0^∞ (10)^p 1 C> 0 0 (10)² (110)^k 111 0^∞ ⟶ halt	q = 2 and every bit set, k >= 1	<= 60	✓150/150
B1 bite	0^∞ (10)^p 1 C> 0 0 10 1 Y 0^∞ ⟶ 0^∞ C> 0 0 (10)^p+3 Y 0^∞	q = 1, zone 1Y starts 11; re-parse leading 10 of Y; new cycle with n = p+3	—	✓150/150
B0 bite	0^∞ (10)^p 1 C> 0 0 Z 0^∞ ⟶ 0^∞ C> 0 0 (10)^p+3 dec(Z)[3:] 0^∞	q = 0, w = 0 mod 3, Z starts 111 (f = 2: n = p+2 and zone 11 Z[3:], 30/30)	—	✓120/120
B2'' nested bite	0^∞ (10)^p 1 C> 0 0 (10)² (110)^k 1^3a+5 0 Y 0^∞ ⟶ 0^∞ (10)^p+2 1 C> 0 0 (10)^q' Z' 0^∞	q = 2, k >= 2 low bits set: an inner wall re-runs rounds on the low part; q' = 5..15, Z' a suffix of Z (top cells sometimes changed). No closed form yet; 49 of 204,953 transitions to 1e9	—	–untested

Compressed historythe tape as 0^∞ C> 0 0 (10)ⁿ Z 0^∞ (cycle start R(-1,n,Z); Z has width w, counter value v, L bits) at 37 moments: where the rules are read off

0^∞ C> 0 0 (10)ⁿ Z 0^∞ (cycle start R(-1,n,Z); Z has width w, counter value v, L bits)

step	`n`	`w`	`v`	`L`
116	3	6	0	1
244	4	8	1	1
327	6	5	0	0
675	8	6	1	1
1,167	10	6	0	1
1,875	11	9	2	2
3,712	15	9	1	2
6,281	18	9	0	2
11,559	22	11	1	2
19,917	27	12	5	3
34,268	32	12	2	3
58,430	37	15	14	4
104,530	45	15	10	4
179,487	54	15	6	4
325,977	66	15	0	4
568,494	81	18	30	5
1,015,594	98	18	17	5
1,819,792	118	18	7	5
3,217,296	141	21	58	6
5,662,179	170	21	44	6
10,090,497	206	21	26	6
17,830,518	249	21	4	6
31,972,323	316	26	126	7
56,366,707	397	18	15	5
100,571,217	493	24	57	7
177,845,615	608	29	212	8
317,209,753	754	20	15	5
562,863,502	874	27	77	8
1,002,875,795	1,014	29	6	8
1,781,927,417	1,196	30	427	9
3,167,681,311	1,426	30	312	9
5,625,645,742	1,711	30	169	9
10,005,286,011	2,072	14	7	3
17,798,996,334	2,508	33	796	10
31,649,029,640	3,024	33	538	10
56,244,128,079	3,652	35	223	10
99,952,253,520	4,417	36	1,888	11

nlast 4,417

wlast 36

vlast 1,888

Llast 11

Template comparison1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v: partly applies · the nearest solved proof, what carries over, and the transitions that differ

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

file: machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v ⚠ not at pin (W4-2 kill, from BECv5.v TM1/TM2)
module: —
machine: 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (11 transitions apart)
diff: not a near table: architecture match only (mirrored bell + counter + bite)
note: Same plan: bell with a moving defect, counter bumped per pass, low-end bite, rare nested eating, halting needs a coincidence; proof via an invariant in progress_nonhalt_cond. Different: counter counts down, bits 3 apart anchored at the far end, defect moves 2 pairs per round, two-level slow counter (v -1 per 2 cycles, level-up at n ~ 2^(L+1)). W4-2's phi/Sweep lemmas do not transfer.

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

proof.md on the invariant I: the rules, Lemma M (mod-3 sign law, proved), Lemma K (d >= 2 closure, proved for plain cycles, checked exhaustively), and the entry at step 327. Then Rocq: one lemma per rule, the nested bite by induction on depth, progress_nonhalt_cond over I (W4-2's shape).

▲Lemma K for cycles with a B2'/B2'' continuation has no paper argument yet; the data show slack (min d' = 5 where 2 is needed).
▲No halt inside nested levels from K is only checked, not argued.
▲The Rocq build of the nested bite (a recursion over walls) is the long part.

Stats & provenance10¹¹ steps simulated · 2,058 cells · the status in full · files

simulated: 10¹¹ steps
tape: 2,058 cells · 1,040 nonzeros
growth: span ~ 2058 cells at 1e9 (tools/sim.py), ~1.2·n^3 steps for bell length n; n = 4,417 at 1e11 (direct C event logger); abstract run to 3e7 cycles
status now: check_kill PASS, independently re-verified (status.json, 2026-10-13)
observer's note: Mechanism and rules validated; non-halting invariant (parity split of O2 overflows) and nested-bite closed form open.
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v

Proof & checks

6/6 automatic checks pass

Kill 31 · Bell eats counter · the kill file 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v: 1039 lines, 129 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (adapted from): verify/BECv5.v Module TM1 · 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

1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB

vs holdout list

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

Theorem

✓ Lemma nonhalt: ~halts tm c0. L1008

check_kill

✓ PASS · 17/17 checks pass · compile 34.71 s · coqchk pass (4.57 s) · assumptions: 0 (closed) · 2026-10-13 20:03:57 UTC · submission/check_kill.txt

Checked .v

sha256 f61649bdc6b6e97b…

✓	1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v	`f61649bdc6b6e97b…` = checked
✓	submission/1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v	`f61649bdc6b6e97b…` = checked

Status

✓Killed: never halts updated 2026-10-13

✓ 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`	45662 bytes, 1039 lines, 1168 sentences
✓	`framework`	HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓	`framework_build`	13 needed framework .vo files present and fresh, with native code no older than the .vo
✓	`forbidden`	none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)
✓	`structure`	5 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 23: TM_from_str "1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB" == <tm> (41 bytes)
✓	`theorem_text`	line 1008: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 (<opam-switch>/bin/coqc)
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 34.7s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---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 (4.6s); 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).

adapted from verify/BECv5.v Module TM1 · detected from 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v line 4

3%of our lines identical to the template

0changed lines

850added lines (ours only)

121template lines dropped

1 / 1 / 127items identical / adapted / new

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

Adapted from busycoq's verify/BECv5.v, Module TM1: one es lemma per low-level rule and one counter-form lemma per macro rule. Changes: a decrementing counter on a 3-cell lattice whose overflow rule depends on the zone width modulo 3; nested bites, so the left side is a stack of frames; and a bounded induction on steps with phase invariants instead of progress_nonhalt_cond. The file has 1,039 lines, every lemma top level.

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

3% identical · 0 changed · 850 added

template 144 lines

16% kept verbatim · 121 not in ours

our items 129

1 identical · 1 adapted · 127 new · 11 template-only

identicalchanged / adaptedours only (new)template only

Template part: lines 1–29 (shared header, before the first Module) + 31–165 (body of Module TM1; the Module/End lines left out). Ours: lines 15–1039 (header comment 1–14 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: highbit, LC0, R, tm', LInc0, LIncs, LIncs', RIncs, ROv, S, BigStep

Side-by-side diff: template (144 lines) vs ours (873 lines), 971 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.	16	From BusyCoq Require Import Individual62.
2	Require Import ZifyNat Lia.	17	Require Import ZifyNat Lia.
3	Require Import ZArith.	18	Require Import ZArith.
4	Require Import String.	19	Require Import String.
5	From BusyCoq Require Import BinaryCounter_v2.
6	From BusyCoq Require Import Longitudinal.
8	Open Scope list.	21	Open Scope list.
10	Ltac flia := repeat (lia\|\|f_equal).
12	Lemma highbit x:
⋯ 14 template-only lines (template 13–26), not in ours
27	cbn; lia.
28	Qed.
32	Definition tm := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB").	23	Definition tm := Eval compute in (TM_from_str "1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB").
34	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).	25	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
35	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).	26	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
37	Notation "l <\| r" :=
		28	( Low-level rules (proof.md 3.1). Left-side lists are written outward from the head. *)
38	(l <{{A}} [] *> r) (at level 30).
		30	Lemma BR k: forall l r, l {{B}}> [1]^^k > r --> [1]^^k *> l {{B}}> r.
40	Notation "l \|> r" :=
		31	Proof. es. Qed.
41	(l <* [] {{B}}> r) (at level 30).
		33	Lemma SW k: forall l r, [1;0]^^k > l <{{C}} r --> l <{{C}} [0;1]^^k *> r.
43	Definition LC0 n := BinInc <[0;1] n.
		34	Proof. es. Qed.
44	Definition R n m := [1] > [1;0]^^(1+n) > [0] > [1;0]^^(m) > const 0.
		36	Lemma TT j: forall l r, [1;1;1]^^j > l <{{C}} r --> l <{{C}} [0;1;1]^^j *> r.
46	Notation hL := (A,[]).
		37	Proof. es. Qed.
47	Notation hR := (B,[]).
		39	Lemma PS b: forall l r, [1;1;0] > l {{B}}> [1;0]^^b > r -->* [1;1] > [0;1]^^b > [0] *> l {{B}}> r.
48	Notation hLR := [(hL,hR)].
		40	Proof. es. Qed.
49	Notation hRL := [(hR,hL)].
		42	(** The round W, PS^(q-3), ZA, in three cases by f mod 3 (f = 3j+2, 3j+4, 3j+3). *)
51	Definition tm' := flip tm.
		43	Lemma RND2 q j: forall l r,
53	Lemma LInc0 r n:
		44	l {{C}}> [0;0] > [1;0]^^(q+3) > [1;1;1]^^j > [1;1;0] > r -->+
54	LC0 n <\| r -->*
		45	[1;0;1;0] > l {{C}}> [0;0] > [1;0]^^(q+1) > [1;1;0]^^j > [1;1;1] *> r.
55	LC0 (1+n) \|> r.
		46	Proof. es. Qed.
		48	Lemma RND1 q j: forall l r,
		49	l {{C}}> [0;0] > [1;0]^^(q+3) > [1;1;1]^^j > [1;1;1;1;0] > r -->+
		50	[1;0;1;0] > l {{C}}> [0;0] > [1;0]^^(q+1) > [1;1;1;1] > [0;1;1]^^j > [1] > r.
		51	Proof. es. Qed.
		53	Lemma RND0 q j: forall l r,
		54	l {{C}}> [0;0] > [1;0]^^(q+3) > [1;1;1]^^j > [1;1;1;0] > r -->+
		55	[1;0;1;0] > l {{C}}> [0;0] > [1;0]^^q > [1;1;1;1;1] > [0;1;1]^^j > [1] > r.
		56	Proof. es. Qed.
		58	(** PUSH k: the bite at q = 2 (B2 for k = 0, the nested bite N for k >= 1). *)
		59	Lemma PUSH k: forall l r,
		60	l {{C}}> [0;0] > [1;0]^^2 > [1;1;0]^^k > [1;1;1] > r -->+
		61	[1;0;0]^^k > [1;0;1;0] > l {{C}}> [0;0] > [1;0] > [1] *> r.
		62	Proof. es. Qed.
		64	(** Ending bites B1, B0, B0c: they read the left part (10)^p 1 and the 00 left of it. *)
		65	Lemma BITE1 p: forall l r,
		66	[1] > [0;1]^^p > [0;0] > l {{C}}> [0;0] > [1;0] > [1;1] > r -->+
		67	l {{C}}> [0;0] > [1;0]^^(p+3) > [1] *> r.
		68	Proof. es. Qed.
		70	Lemma BITE0 p j: forall l r,
		71	[1] > [0;1]^^p > [0;0] > l {{C}}> [0;0] > [1;1;1]^^j > [1;1;0] > r -->+
		72	l {{C}}> [0;0] > [1;0]^^(p+2) > [1] > [0;1;1]^^j > [1] *> r.
		73	Proof. es. Qed.
		75	Lemma BITE0c p j: forall l r,
		76	[1] > [0;1]^^p > [0;0] > l {{C}}> [0;0] > [1;1;1]^^j > [1;1;1;1;1;1;0] > r -->+
		77	l {{C}}> [0;0] > [1;0]^^(p+2) > [1;1;1] > [1;1;0]^^j > [1;1;1] *> r.
		78	Proof. es. Qed.
		80	Lemma BITE0c3 p: forall l r,
		81	[1] > [0;1]^^p > [0;0] > l {{C}}> [0;0] > [1;1;1;0;0] *> r -->+
		82	l {{C}}> [0;0] > [1;0]^^(p+1) > [1;1;1;1;1;1] *> r.
		83	Proof. es. Qed.
		85	( The counter zone: zone r L v = 1^r (1 1 c_0) ... (1 1 c_(L-1)) 1 1 1, width 3L+3+r,
		86	c_b = 0 iff bit b of v is set (proof.md 2: the lattice of a width-w zone). *)
		88	Definition bitc (v : nat) : sym := if Nat.odd v then 0 else 1.
		90	Fixpoint dg (L v : nat) : list sym :=
		91	match L with
		92	\| O => []
		93	\| S L' => [1;1;bitc v] ++ dg L' (Nat.div2 v)
		94	end.
		96	Definition zone (r L v : nat) : list sym := [1]^^r ++ dg L v ++ [1;1;1].
		98	Lemma bitc_even v: bitc (2*v) = 1.
		99	Proof. unfold bitc. rewrite Nat.odd_mul. reflexivity. Qed.
		101	Lemma bitc_odd v: bitc (2*v+1) = 0.
		102	Proof. unfold bitc. rewrite Nat.add_1_r, Nat.odd_succ, Nat.even_mul. reflexivity. Qed.
		104	Lemma div2_even v: Nat.div2 (2*v) = v.
		105	Proof. apply Nat.div2_double. Qed.
		107	Lemma div2_odd v: Nat.div2 (2*v+1) = v.
		108	Proof. rewrite Nat.add_1_r. apply Nat.div2_succ_double. Qed.
		110	Lemma dg_even L v: dg (S L) (2*v) = [1;1;1] ++ dg L v.
		111	Proof. cbn [dg]. rewrite bitc_even, div2_even. reflexivity. Qed.
		113	Lemma dg_odd L v: dg (S L) (2*v+1) = [1;1;0] ++ dg L v.
		114	Proof. cbn [dg]. rewrite bitc_odd, div2_odd. reflexivity. Qed.
		116	Lemma pow_pos P: 1 <= 2^P.
		117	Proof. pose proof (Nat.pow_nonzero 2 P). lia. Qed.
		119	Lemma dg_zero L: dg L 0 = [1;1;1]^^L.
56	Proof.	120	Proof.
57	unfold LC0.
		121	induction L as [\|L IH]; [reflexivity\|].
58	er.
		122	change (dg (S L) 0) with ([1;1;1] ++ dg L 0). rewrite IH. reflexivity.
59	eapply evstep_trans.
60	1: apply progress_evstep.
61	1: apply LBinInc_spec with (qL:=[]) (qR:=[]); es.
62	er.
63	Qed.	123	Qed.
65	Lemma LIncs n:
		125	Lemma dg_full L: dg L (2^L - 1) = [1;1;0]^^L.
66	sideRLs tm' (hLR^^n) (LC0 0) (LC0 n).
67	Proof.	126	Proof.
68	induction n.
		127	induction L as [\|L IH]; [reflexivity\|].
69	- esx.
		128	replace (2^(S L) - 1) with (2*(2^L-1)+1) by (rewrite Nat.pow_succ_r'; pose proof (pow_pos L); lia).
70	- replace (S n) with (n+1) by lia.
		129	rewrite dg_odd, IH. reflexivity.
71	rewrite lpow_add.
72	eapply sideRLs_trans.
⋯ 4 template-only lines (template 73–76), not in ours
77	rw_Bin.
78	esx.
79	Qed.	130	Qed.
81	Lemma LIncs' n:
		132	Lemma dg_low b L o: dg (b + S L) (2^b(2o+1)) = [1;1;1]^^b ++ [1;1;0] ++ dg L o.
82	sideRLs tm' (hLR^^(n2)) (LC0 n < [0]) (LC0 0).
83	Proof.	133	Proof.
84	unfold LC0.
		134	induction b as [\|b IH].
85	induction n using lt_wf_ind.
		135	- replace (2^0(2o+1)) with (2*o+1) by (cbn; lia). apply dg_odd.
86	divmod2_cases n.
		136	- replace (2^(S b)(2o+1)) with (2(2^b(2*o+1))) by (rewrite Nat.pow_succ_r'; lia).
87	- destruct (Nat.eqb_spec n' 0).
		137	cbn [Nat.add]. rewrite dg_even, IH. reflexivity.
88	+ subst.
89	esx.
⋯ 14 template-only lines (template 90–103), not in ours
104	replace ((n'2+1)2) with (n'22+2) by lia.
105	apply segRLs_addmul''; esx.
106	Qed.	138	Qed.
108	Lemma RIncs n m:
		140	Lemma dg_lowones k L o: dg (k + S L) (2^k - 1 + 2^(S k)*o) = [1;1;0]^^k ++ [1;1;1] ++ dg L o.
109	sideRLs tm (hRL^^n) (R n m) (R 0 (n+m)).
110	Proof.	141	Proof.
111	gen m.
		142	induction k as [\|k IH].
112	induction n; intros.
		143	- replace (2^0 - 1 + 2^1o) with (2o) by (cbn; lia). apply dg_even.
113	- esx.
		144	- replace (2^(S k) - 1 + 2^(S (S k))o) with (2(2^k - 1 + 2^(S k)*o)+1)
114	- replace (S n) with (1+n) by lia.
		145	by (rewrite !Nat.pow_succ_r'; pose proof (pow_pos k); lia).
115	rewrite lpow_add.
		146	cbn [Nat.add]. rewrite dg_odd, IH. reflexivity.
116	eapply sideRLs_trans.
117	2: applys_eq (IHn (1+m)); flia.
118	esx.
119	Qed.	147	Qed.
121	Lemma ROv k i m:
		149	Lemma lowbit (x:nat): x <> 0%nat -> exists P o, x = 2^P(2o+1).
122	LC0 ((k2+1)2^i-1) <\| R 0 m -->+
123	LC0 k <* [0] <\| R (1+i+m) 0.
124	Proof.	150	Proof.
125	unfold LC0,R.
		151	induction x as [x IH] using lt_wf_ind. intros Hx.
126	rw_Bin.
		152	destruct (Nat.Even_or_Odd x) as [[x' Hx']\|[x' Hx']]; subst x.
127	es.
		153	- destruct (IH x') as [P [o Ho]]; [lia\|lia\|].
		154	exists (S P), o. rewrite Nat.pow_succ_r'. lia.
		155	- exists 0%nat, x'. cbn. lia.
128	Qed.	156	Qed.
130	Definition S '(a,b) := LC0 a <\| R 0 b.
		158	Lemma lowbit_lt b o L: 2^b(2o+1) < 2^L -> b < L /\ o < 2^(L-b-1).
132	Lemma BigStep k i m:
133	k*2<=(1+i+m) ->
134	S ((k2+1)2^i-1,m) -->+
135	S (1+i+m-k*2,1+i+m).
136	Proof.	159	Proof.
137	unfold S.
		160	intros H.
138	intros.
		161	assert (Hb: b < L).
139	follow10 ROv.
		162	{ apply (Nat.pow_lt_mono_r_iff 2); [lia\|]. pose proof (pow_pos b). nia. }
140	replace (1+i+m) with (k2+(1+i+m-k2)) by lia.
		163	split; [exact Hb\|].
141	epose proof (sideRLs_concat_1L (RIncs _ 0)) as I1.
		164	replace L with (b + S (L-b-1)) in H by lia.
142	follow I1.
		165	rewrite Nat.pow_add_r, Nat.pow_succ_r' in H.
143	- rewrite lpow_add.
		166	pose proof (pow_pos b). nia.
144	eapply sideRLs_trans.
		167	Qed.
145	+ apply LIncs'.
		169	Lemma ones_comm b: [1;1] ++ [1;1;1]^^b = [1;1;1]^^b ++ [1;1].
146	+ apply LIncs.
		170	Proof. induction b as [\|b IH]; [reflexivity\|]. cbn [lpow]. rewrite <-List.app_assoc, <-IH. reflexivity. Qed.
147	- unfold to_DH_config.
		172	Lemma one_comm b: [1] ++ [1;1;1]^^b = [1;1;1]^^b ++ [1].
148	finish.
		173	Proof. induction b as [\|b IH]; [reflexivity\|]. cbn [lpow]. rewrite <-List.app_assoc, <-IH. reflexivity. Qed.
		175	Lemma sh110 b: [1;1] ++ [0;1;1]^^b = [1;1;0]^^b ++ [1;1].
		176	Proof. induction b as [\|b IH]; [reflexivity\|]. cbn [lpow]. rewrite <-List.app_assoc, <-IH. reflexivity. Qed.
		178	Lemma S_ones2 b s: [1;1] > [1;1;1]^^b > s = [1;1;1]^^b > [1;1] > s.
		179	Proof. rewrite <-!Str_app_assoc, ones_comm. reflexivity. Qed.
		181	Lemma S_ones1 b s: [1] > [1;1;1]^^b > s = [1;1;1]^^b > [1] > s.
		182	Proof. rewrite <-!Str_app_assoc, one_comm. reflexivity. Qed.
		184	Lemma S_sh110 b s: [1;1] > [0;1;1]^^b > s = [1;1;0]^^b > [1;1] > s.
		185	Proof. rewrite <-!Str_app_assoc, sh110. reflexivity. Qed.
		187	( Counter forms of the round (proof.md 3.2), for any left side l *)
		189	Definition RT (l : side) (q : nat) (Z : list sym) : Q * tape := l {{C}}> [0;0] > [1;0]^^q > Z *> const 0.
		191	Lemma R1z l q L v: 1 <= v -> v < 2^L ->
		192	RT l (q+3) (zone 0 L v) -->+ RT ([1;0;1;0] *> l) (q+1) (zone 0 L (v-1)).
		193	Proof.
		194	intros H1 H2. destruct (lowbit v) as [b [o ->]]; [lia\|].
		195	destruct (lowbit_lt _ _ _ H2) as [Hb Ho].
		196	remember (L-b-1) as L'. replace L with (b + S L') by lia.
		197	replace (2^b(2o+1) - 1) with (2^b - 1 + 2^(S b)*o) by (rewrite Nat.pow_succ_r'; pose proof (pow_pos b); nia).
		198	unfold RT, zone. rewrite dg_low, dg_lowones. cbn [lpow app].
		199	rewrite !Str_app_assoc. apply RND2.
		200	Qed.
		202	Lemma R1t l q L v: 1 <= v -> v < 2^L ->
		203	RT l (q+3) (zone 2 L v) -->+ RT ([1;0;1;0] *> l) (q+1) (zone 2 L (v-1)).
		204	Proof.
		205	intros H1 H2. destruct (lowbit v) as [b [o ->]]; [lia\|].
		206	destruct (lowbit_lt _ _ _ H2) as [Hb Ho].
		207	remember (L-b-1) as L'. replace L with (b + S L') by lia.
		208	replace (2^b(2o+1) - 1) with (2^b - 1 + 2^(S b)*o) by (rewrite Nat.pow_succ_r'; pose proof (pow_pos b); nia).
		209	unfold RT, zone. rewrite dg_low, dg_lowones. rewrite !Str_app_assoc.
		210	change ([1]^^2) with [1;1]. rewrite S_ones2.
		211	change ([1;1] > [1;1;0] > ?Y) with ([1;1;1;1;0] *> Y).
		212	eapply progress_evstep_trans. 1: apply RND1. apply evstep_refl'.
		213	change ([1;1;1;1] > ?X) with ([1;1] > [1;1] *> X). rewrite S_sh110. reflexivity.
		214	Qed.
		216	Lemma R2r l q L v: 1 <= v -> v < 2^L ->
		217	RT l (q+3) (zone 1 L v) -->+ RT ([1;0;1;0] > l) q (zone 0 (S L) (2v-2)).
		218	Proof.
		219	intros H1 H2. destruct (lowbit v) as [b [o ->]]; [lia\|].
		220	destruct (lowbit_lt _ _ _ H2) as [Hb Ho].
		221	remember (L-b-1) as L'. replace L with (b + S L') by lia.
		222	replace (2(2^b(2o+1))-2) with (2(2^b - 1 + 2^(S b)*o)) by (rewrite Nat.pow_succ_r'; pose proof (pow_pos b); nia).
		223	unfold RT, zone. rewrite dg_low, dg_even, dg_lowones. rewrite !Str_app_assoc.
		224	change ([1]^^1) with [1]. rewrite S_ones1.
		225	change ([1] > [1;1;0] > ?Y) with ([1;1;1;0] *> Y).
		226	eapply progress_evstep_trans. 1: apply RND0. apply evstep_refl'.
		227	change ([1;1;1;1;1] > ?X) with ([1;1;1] > [1;1] *> X). rewrite S_sh110. reflexivity.
		228	Qed.
		230	Lemma O2r l q L:
		231	RT l (q+3) (zone 2 L 0) -->+ RT ([1;0;1;0] *> l) (q+1) (zone 0 (S L) (2^(S L)-1)).
		232	Proof.
		233	unfold RT, zone. rewrite dg_zero, dg_full. rewrite !Str_app_assoc.
		234	change ([1]^^2) with [1;1]. change ([1]^^0 *> ?X) with X.
		235	assert (E: [1;1] > [1;1;1]^^L > [1;1;1] > const 0 = [1;1;1]^^(S L) > [1;1;0] *> const 0).
		236	{ rewrite S_ones2, lpow_S, Str_app_assoc, <-lpow_shift'. f_equal. cbn. repeat f_equal. apply const_unfold. }
		237	rewrite E. apply RND2.
		238	Qed.
		240	Lemma O1r l q L:
		241	RT l (q+3) (zone 1 L 0) -->+ RT ([1;0;1;0] *> l) (q+1) (zone 2 L (2^L-1)).
		242	Proof.
		243	unfold RT, zone. rewrite dg_zero, dg_full. rewrite !Str_app_assoc.
		244	change ([1]^^2) with [1;1]. change ([1]^^1) with [1].
		245	assert (E: [1] > [1;1;1]^^L > [1;1;1] > const 0 = [1;1;1]^^L > [1;1;1;1;0] *> const 0).
		246	{ rewrite S_ones1. f_equal. cbn. repeat f_equal. apply const_unfold. }
		247	rewrite E. eapply progress_evstep_trans. 1: apply RND1. apply evstep_refl'.
		248	change ([1;1;1;1] > ?X) with ([1;1] > [1;1] *> X). rewrite S_sh110. reflexivity.
		249	Qed.
		251	Lemma O0r l q L:
		252	RT l (q+3) (zone 0 L 0) -->+ RT ([1;0;1;0] *> l) q (zone 0 (S L) (2^(S L)-2)).
		253	Proof.
		254	replace (2^(S L)-2) with (2*(2^L-1)) by (rewrite Nat.pow_succ_r'; pose proof (pow_pos L); lia).
		255	unfold RT, zone. rewrite dg_zero, dg_even, dg_full. rewrite !Str_app_assoc.
		256	change ([1]^^0 *> ?X) with X.
		257	assert (E: [1;1;1]^^L > [1;1;1] > const 0 = [1;1;1]^^L > [1;1;1;0] > const 0).
		258	{ f_equal. cbn. repeat f_equal. apply const_unfold. }
		259	rewrite E. eapply progress_evstep_trans. 1: apply RND0. apply evstep_refl'.
		260	change ([1;1;1;1;1] > ?X) with ([1;1;1] > [1;1] *> X). rewrite S_sh110. reflexivity.
		261	Qed.
		263	( Counter forms of the bites (proof.md 3.3). FR p l is the frame 00 (10)^p 1 on top of l. *)
		265	Definition FR (p : nat) (l : side) : side := [1] > [0;1]^^p > [0;0] *> l.
		267	Lemma PUSHr l k L o:
		268	RT l 2 (zone 0 (k + S L) (2^k - 1 + 2^(S k)o)) -->+ RT ([1;0;0]^^k > [1;0;1;0] *> l) 1 (zone 1 L o).
		269	Proof.
		270	unfold RT, zone. rewrite dg_lowones. rewrite !Str_app_assoc.
		271	change ([1]^^0 *> ?X) with X.
		272	eapply progress_evstep_trans. 1: apply PUSH. apply evstep_refl'. reflexivity.
		273	Qed.
		275	Lemma B1z0 p l L v: RT (FR p l) 1 (zone 0 (S L) (2*v)) -->+ RT l (p+3) (zone 2 L v).
		276	Proof.
		277	unfold RT, FR, zone. rewrite dg_even. rewrite !Str_app_assoc.
		278	change ([1]^^0 > ?X) with X. change ([1;0]^^1 > [1;1;1] > ?X) with ([1;0] > [1;1] > [1] > X).
		279	eapply progress_evstep_trans. 1: apply BITE1. apply evstep_refl'. reflexivity.
		280	Qed.
		282	Lemma B1z1 p l L v: RT (FR p l) 1 (zone 0 (S L) (2*v+1)) -->+ RT l (p+4) (zone 0 L v).
		283	Proof.
		284	unfold RT, FR, zone. rewrite dg_odd. rewrite !Str_app_assoc.
		285	change ([1]^^0 > ?X) with X. change ([1;0]^^1 > [1;1;0] > ?X) with ([1;0] > [1;1] > [0] > X).
		286	eapply progress_evstep_trans. 1: apply BITE1. apply evstep_refl'.
		287	replace (p+4) with (S (p+3)) by lia. rewrite lpow_S, Str_app_assoc, <-lpow_shift'. reflexivity.
		288	Qed.
		290	Lemma B1o p l L v: RT (FR p l) 1 (zone 1 L v) -->+ RT l (p+3) (zone 0 L v).
		291	Proof.
		292	unfold RT, FR, zone. destruct L as [\|L].
		293	- cbn [dg]. change ([1;0]^^1 > ([1]^^1 ++ [] ++ [1;1;1]) > ?X) with ([1;0] > [1;1] > [1;1] *> X).
		294	eapply progress_evstep_trans. 1: apply BITE1. apply evstep_refl'. reflexivity.
		295	- cbn [dg]. rewrite !Str_app_assoc.
		296	change ([1;0]^^1 > [1]^^1 > [1;1;bitc v] > ?X) with ([1;0] > [1;1] > [1;bitc v] > X).
		297	eapply progress_evstep_trans. 1: apply BITE1. apply evstep_refl'. reflexivity.
		298	Qed.
		300	Lemma B1t p l L v: RT (FR p l) 1 (zone 2 L v) -->+ RT l (p+3) (zone 1 L v).
		301	Proof.
		302	unfold RT, FR, zone. rewrite !Str_app_assoc.
		303	change ([1;0]^^1 > [1]^^2 > ?X) with ([1;0] > [1;1] > X).
		304	eapply progress_evstep_trans. 1: apply BITE1. apply evstep_refl'. reflexivity.
		305	Qed.
		307	Lemma B0r p l b L o:
		308	RT (FR p l) 0 (zone 0 (S b + S L) (2^(S b)(2o+1))) -->+ RT l (p+3) (zone 0 (b + S L) (2^b - 1 + 2^(S b)*o)).
		309	Proof.
		310	unfold RT, FR, zone. rewrite dg_low, dg_lowones. rewrite !Str_app_assoc.
		311	change ([1]^^0 > ?X) with X. change ([1;0]^^0 > ?X) with X.
		312	eapply progress_evstep_trans. 1: apply BITE0. apply evstep_refl'.
		313	rewrite lpow_S, Str_app_assoc.
		314	change ([1] > [0;1;1] > ?X) with ([1;0] > [1;1] > X). rewrite S_sh110.
		315	replace (p+3) with (S (p+2)) by lia. rewrite (lpow_S (p+2)), Str_app_assoc, <-lpow_shift'. reflexivity.
		316	Qed.
		318	Lemma B0cr p l L: RT (FR p l) 0 (zone 0 (S L) 0) -->+ RT l (p+2) (zone 0 (S L) (2^(S L)-2)).
		319	Proof.
		320	replace (2^(S L)-2) with (2*(2^L-1)) by (rewrite Nat.pow_succ_r'; pose proof (pow_pos L); lia).
		321	unfold RT, FR, zone. rewrite dg_zero, dg_even, dg_full. rewrite !Str_app_assoc.
		322	change ([1]^^0 > ?X) with X. change ([1;0]^^0 > ?X) with X.
		323	assert (E: [1;1;1]^^(S L) > [1;1;1] > const 0 = [1;1;1]^^L > [1;1;1;1;1;1;0] > const 0).
		324	{ rewrite lpow_S, Str_app_assoc, <-lpow_shift'. f_equal. cbn. repeat f_equal. apply const_unfold. }
		325	rewrite E. apply BITE0c.
		326	Qed.
		328	Lemma B0c3r p l: RT (FR p l) 0 (zone 0 0 0) -->+ RT l (p+1) (zone 0 1 0).
		329	Proof.
		330	unfold RT, FR, zone. cbn [dg lpow app].
		331	assert (E: [1;1;1] > const 0 = [1;1;1;0;0] > const 0).
		332	{ cbn. rewrite <-!const_unfold. reflexivity. }
		333	change ([1;0]^^0 *> ?X) with X. rewrite E.
		334	eapply progress_evstep_trans. 1: apply BITE0c3. apply evstep_refl'. reflexivity.
		335	Qed.
		337	( Frames *)
		339	Lemma FR_round p l: [1;0;1;0] *> FR p l = FR (p+2) l.
		340	Proof.
		341	unfold FR. replace (p+2) with (S (S p)) by lia.
		342	cbn [lpow]. rewrite !Str_app_assoc. reflexivity.
		343	Qed.
		345	( Initial segment (proof.md 7): c0 -->(327) R(-1, 6, 11111) = (6,5,0) *)
		347	Lemma init: c0 -->* RT (const 0) 6 (zone 2 0 0).
		348	Proof. unfold RT, zone. cbn. solve_init. Qed.
		350	( Levels. lev P l is the top frame in shifted coordinates P = p+1; P = 0 is the cycle
		351	start (no frame), used only over the blank left side. *)
		353	Definition lev (P : nat) (l : side) : side :=
		354	match P with
		355	\| O => l
		356	\| S p => FR p l
		357	end.
		359	Definition okL (P : nat) (l : side) : Prop := P = 0%nat -> l = const 0.
		361	Lemma lev_round P l: okL P l -> [1;0;1;0] *> lev P l = lev (P+2) l.
		362	Proof.
		363	unfold okL. destruct P as [\|P]; intros H.
		364	- rewrite H by reflexivity. cbn. repeat f_equal. apply const_unfold.
		365	- cbn [lev]. replace (S P + 2) with (S (P+2)) by lia. apply FR_round.
		366	Qed.
		368	Lemma okL_S P l: okL (S P) l.
		369	Proof. unfold okL. intros H. discriminate H. Qed.
		371	(** The abstract round (proof.md 3.2 counter form): (q, r, L, v) -> (q', r', L', v'). *)
		372	Inductive Rnd : nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> Prop :=
		373	\| RR1z q L v: 1 <= v -> Rnd (q+3) 0 L v (q+1) 0 L (v-1)
		374	\| RR1t q L v: 1 <= v -> Rnd (q+3) 2 L v (q+1) 2 L (v-1)
		375	\| RR2 q L v: 1 <= v -> Rnd (q+3) 1 L v q 0 (S L) (2*v-2)
		376	\| RO2 q L: Rnd (q+3) 2 L 0 (q+1) 0 (S L) (2^(S L)-1)
		377	\| RO1 q L: Rnd (q+3) 1 L 0 (q+1) 2 L (2^L-1)
		378	\| RO0 q L: Rnd (q+3) 0 L 0 q 0 (S L) (2^(S L)-2).
		380	Lemma Rnd_tape q r L v q' r' L' v' P l:
		381	Rnd q r L v q' r' L' v' -> v < 2^L -> okL P l ->
		382	RT (lev P l) q (zone r L v) -->+ RT (lev (P+2) l) q' (zone r' L' v').
		383	Proof.
		384	intros H Hv Hl. rewrite <-(lev_round P l Hl).
		385	destruct H.
		386	- apply R1z; lia.
		387	- apply R1t; lia.
		388	- apply R2r; lia.
		389	- apply O2r.
		390	- apply O1r.
		391	- apply O0r.
		392	Qed.
		394	Lemma Rnd_valid q r L v q' r' L' v':
		395	Rnd q r L v q' r' L' v' -> v < 2^L -> r < 3 -> v' < 2^L' /\ r' < 3.
		396	Proof.
		397	intros H Hv Hr. destruct H; rewrite ?Nat.pow_succ_r' in *; pose proof (pow_pos L); lia.
		398	Qed.
		400	Lemma Rnd_exists q r L v: 3 <= q -> r < 3 -> exists q' r' L' v', Rnd q r L v q' r' L' v'.
		401	Proof.
		402	intros Hq Hr. replace q with ((q-3)+3) by lia.
		403	destruct (Nat.eq_dec v 0) as [->\|Hv].
		404	- destruct r as [\|[\|[\|]]]; [\| \| \|lia]; eexists _, _, _, _.
		405	+ apply RO0.
		406	+ apply RO1.
		407	+ apply RO2.
		408	- destruct r as [\|[\|[\|]]]; [\| \| \|lia]; eexists _, _, _, _.
		409	+ apply RR1z; lia.
		410	+ apply RR2; lia.
		411	+ apply RR1t; lia.
		412	Qed.
		414	Lemma okL_ge P l: 1 <= P -> okL P l.
		415	Proof. intros H. destruct P; [lia\|apply okL_S]. Qed.
		417	( The invariant (proof.md 5.1) on cycle starts t = (n, r, L, v): width w = 3L+3+r *)
		419	Definition cap (r L : nat) : nat := L + (if Nat.eqb r 1 then 1 else 0).
		421	(** K: d = n - 2^(cap+1) >= 2 *)
		422	Definition Kst (n r L : nat) : Prop := 2^(S (cap r L)) + 2 <= n.
		424	(** J: n >= 3, n odd when w = 1, 2 mod 3 *)
		425	Definition Jst (n r : nat) : Prop := 3 <= n /\ (r <> 0%nat -> n mod 2 = 1%nat).
		427	(** M (mod 3): n + 2v - 2^(cap+2) (w = 0, 2), n + v - 2^(cap+2) (w = 1); -x is written 2x *)
		428	Definition Mv (n r L v : nat) : nat :=
		429	(n + (if Nat.eqb r 1 then v else 2v) + 2 2^(cap r L + 2)) mod 3.
		431	(** The sign-law quantity Q of a frame (proof.md 5.4), P = p+1: Q = M - P = M + 2P (mod 3) *)
		432	Definition Qv (P q r L v : nat) : nat := (Mv q r L v + 2*P) mod 3.
		434	Definition Ist (n r L v : nat) : Prop :=
		435	r < 3 /\ v < 2^L /\ Kst n r L /\ Mv n r L v <> 0%nat /\ ~ (n = 6 /\ r = 1 /\ L = 0 /\ v = 0)%nat.
		437	Lemma init_I: Ist 6 2 0 0.
		438	Proof. unfold Ist, Kst, Mv, cap. cbn. repeat split; lia. Qed.
		440	Lemma Rnd_sign P q r L v q' r' L' v':
		441	Rnd q r L v q' r' L' v' -> Qv P q r L v = Qv (P+2) q' r' L' v'.
		442	Proof.
		443	intros H. unfold Qv, Mv, cap.
		444	destruct H as [q L v Hv\|q L v Hv\|q L v Hv\|q L\|q L\|q L]; pose proof (pow_pos L);
		445	cbn [Nat.eqb]; rewrite ?Nat.pow_add_r; cbn [Nat.pow]; lia.
		446	Qed.
		448	( Ending bites as one relation: from frame P = p+1 the pop is RT l (P + e) (zone r' L' v') *)
		450	Inductive EB : nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> Prop :=
		451	\| EB1z0 L v: EB 1 0 (S L) (2*v) 2 2 L v
		452	\| EB1z1 L v: EB 1 0 (S L) (2*v+1) 3 0 L v
		453	\| EB1o L v: EB 1 1 L v 2 0 L v
		454	\| EB1t L v: EB 1 2 L v 2 1 L v
		455	\| EB0 b L o: EB 0 0 (S b + S L) (2^(S b)(2o+1)) 2 0 (b + S L) (2^b - 1 + 2^(S b)*o)
		456	\| EB0c L: EB 0 0 (S L) 0 1 0 (S L) (2^(S L)-2)
		457	\| EB0c3: EB 0 0 0 0 0 0 1 0.
		459	Lemma EB_tape q r L v e r' L' v' p l:
		460	EB q r L v e r' L' v' -> RT (FR p l) q (zone r L v) -->+ RT l (S p + e) (zone r' L' v').
		461	Proof.
		462	intros H. destruct H.
		463	- replace (S p + 2) with (p+3) by lia. apply B1z0.
		464	- replace (S p + 3) with (p+4) by lia. apply B1z1.
		465	- replace (S p + 2) with (p+3) by lia. apply B1o.
		466	- replace (S p + 2) with (p+3) by lia. apply B1t.
		467	- replace (S p + 2) with (p+3) by lia. apply B0r.
		468	- replace (S p + 1) with (p+2) by lia. apply B0cr.
		469	- replace (S p + 0) with (p+1) by lia. apply B0c3r.
		470	Qed.
		472	(** Sign law for ending bites (proof.md 5.4): M(pop) = -Q(bite) (mod 3) *)
		473	Lemma EB_sign q r L v e r' L' v' P:
		474	EB q r L v e r' L' v' -> (Mv (P + e) r' L' v' + Qv P q r L v) mod 3 = 0%nat.
		475	Proof.
		476	intros H. unfold Qv, Mv, cap.
		477	destruct H as [L v\|L v\|L v\|L v\|b L o\|L\|]; cbn [Nat.eqb]; rewrite ?Nat.pow_add_r; cbn [Nat.pow].
		478	1-4,6: pose proof (pow_pos L); lia.
		479	- pose proof (pow_pos L). pose proof (pow_pos b). nia.
		480	- lia.
		481	Qed.
		483	( The bite at q = 2 on a level: PUSH k leaves k pending inner levels (frames p = 0,
		484	i.e. lev 1) over the level's own frame, now at P+2 (proof.md 3.4, the stack). *)
		486	Lemma iter_FR0 k X: [1;0;0]^^k *> X = Nat.iter k (FR 0) X.
		487	Proof.
		488	induction k as [\|k IH]; [reflexivity\|].
		489	rewrite lpow_S, Str_app_assoc, IH. reflexivity.
		490	Qed.
		492	Lemma PUSH_lev k L o P l: okL P l ->
		493	RT (lev P l) 2 (zone 0 (k + S L) (2^k - 1 + 2^(S k)*o)) -->+
		494	RT (Nat.iter k (FR 0) (lev (P+2) l)) 1 (zone 1 L o).
		495	Proof.
		496	intros Hl. rewrite <-(lev_round P l Hl), <-iter_FR0. apply PUSHr.
		497	Qed.
		499	(** The innermost level of a nested bite is a single B1 bite: it pops into the next level's
		500	start (lev 1 = the frame p = 0) with t_2 = (3, Y[3:]). *)
		501	Lemma inner1 k L o X:
		502	RT (Nat.iter (S k) (FR 0) X) 1 (zone 1 L o) -->+ RT (Nat.iter k (FR 0) X) 3 (zone 0 L o).
		503	Proof. cbn [Nat.iter]. apply (EB_tape 1 1 L o 2 0 L o 0). constructor. Qed.
		505	( Bounded safety (proof.md 6, route 3 of proof.md 9) *)
		507	Definition safe (c : Q * tape) (N : nat) : Prop := forall M, M <= N -> ~ halts_in tm c M.
		509	Lemma safe_mono c N N': safe c N -> N' <= N -> safe c N'.
		510	Proof. intros H Hle M HM. apply H. lia. Qed.
		512	Lemma safe_ev c c' N: c -->* c' -> safe c' N -> safe c N.
		513	Proof.
		514	intros H HN M HM Hh. apply with_counter in H as [n Hn].
		515	destruct (Nat.leb_spec n M).
		516	- apply (HN (M - n)); [lia\|]. eapply preceeds_halt; eauto.
		517	- eapply exceeds_halt; eauto.
		518	Qed.
		520	Lemma safe_prog c c' N: c -->+ c' -> safe c' (N - 1) -> safe c N.
		521	Proof.
		522	intros H HN M HM Hh. apply progress_multistep in H as [n Hn].
		523	destruct (Nat.leb_spec (S n) M).
		524	- apply (HN (M - S n)); [lia\|]. eapply preceeds_halt; eauto.
		525	- eapply exceeds_halt; eauto.
		526	Qed.
		528	Lemma safe_prog0 c c': c -->+ c' -> safe c 0.
		529	Proof.
		530	intros H M HM Hh. apply progress_multistep in H as [n Hn].
		531	eapply exceeds_halt; [exact Hh \| \| exact Hn]. lia.
		532	Qed.
		534	Lemma safe_RT0 l q Z: safe (RT l q Z) 0.
		535	Proof.
		536	intros M HM [ch [Hrun Hh]]. assert (M = 0%nat) by lia. subst M.
		537	inversion Hrun; subst. unfold RT in Hh. cbn in Hh. discriminate.
		538	Qed.
		540	( The phase lemma: rounds from a phase start to its bite (q <= 2), carrying any
		541	invariant that every round preserves. j is the frame offset from the level start. *)
		543	Lemma phase (Inv : nat -> nat -> nat -> nat -> nat -> Prop):
		544	(forall j q r L v q' r' L' v', Rnd q r L v q' r' L' v' -> v < 2^L ->
		545	Inv j q r L v -> Inv (j+2) q' r' L' v') ->
		546	forall q j P l r L v, okL (P + j) l -> r < 3 -> v < 2^L -> Inv j q r L v ->
		547	exists j' q' r' L' v', q' <= 2 /\ r' < 3 /\ v' < 2^L' /\ Inv j' q' r' L' v' /\
		548	j <= j' /\ (3 <= q -> j + 2 <= j') /\
		549	RT (lev (P + j) l) q (zone r L v) -->* RT (lev (P + j') l) q' (zone r' L' v').
		550	Proof.
		551	intros Hstep q. induction q as [q IH] using lt_wf_ind. intros j P l r L v Hl Hr Hv HI.
		552	destruct (Nat.le_gt_cases q 2) as [Hq\|Hq].
		553	- exists j, q, r, L, v. repeat split; try assumption; try lia. apply evstep_refl.
		554	- destruct (Rnd_exists q r L v ltac:(lia) Hr) as [q' [r' [L' [v' HR]]]].
		555	assert (Hq': q' < q) by (destruct HR; lia).
		556	destruct (Rnd_valid _ _ _ _ _ _ _ _ HR Hv Hr) as [Hv' Hr'].
		557	assert (Hl': okL (P + (j+2)) l) by (apply okL_ge; lia).
		558	destruct (IH q' Hq' (j+2) P l r' L' v' Hl' Hr' Hv' (Hstep _ _ _ _ _ _ _ _ _ HR Hv HI))
		559	as [j2 [q2 [r2 [L2 [v2 [H1 [H2 [H3 [H4 [H5 [H6 H7]]]]]]]]]]].
		560	exists j2, q2, r2, L2, v2. repeat split; try assumption; try lia.
		561	eapply evstep_trans. 2: exact H7.
		562	apply progress_evstep. replace (P + (j+2)) with ((P+j)+2) by lia. apply Rnd_tape; assumption.
		563	Qed.
		565	( Classes of level starts and the phase invariants (proof.md 5) *)
		567	Lemma cap0 L: cap 0 L = L. Proof. unfold cap. cbn. lia. Qed.
		568	Lemma cap1 L: cap 1 L = S L. Proof. unfold cap. cbn. lia. Qed.
		569	Lemma cap2 L: cap 2 L = L. Proof. unfold cap. cbn. lia. Qed.
		571	Ltac pw := rewrite ?Nat.pow_succ_r' in *.
		573	Lemma pow0 L: L = 0%nat -> 2^L = 1%nat.
		574	Proof. intros ->. reflexivity. Qed.
		576	(** K' = K minus T_c and (6,4,0) *)
		577	Definition Kx (n r L v : nat) : Prop :=
		578	Kst n r L /\ ~ (r = 2%nat /\ v = 2^L - 1 /\ n = 2^(S L) + 2) /\
		579	~ (n = 6%nat /\ r = 1%nat /\ L = 0%nat /\ v = 0%nat).
		581	Definition Pre (n r L v : nat) : Prop := Jst n r \/ Kx n r L v.
		583	(** Safety along a phase (Lemma P): no H, and every bite has a rule. *)
		584	Definition Saf (q r L v : nat) : Prop :=
		585	match r with
		586	\| O => (L = 0%nat -> 3 <= q) /\ ~ (q = 2%nat /\ v = 2^L - 1) /\ (q = 0%nat -> v mod 2 = 0%nat)
		587	\| 1%nat => 3 <= q /\ (v = 0%nat -> (q <= 2^(S L) + 2 -> q mod 2 = 1%nat) /\ q <> 2^(S L) + 4)
		588	\| _ => (q <= 2v + 2 -> q mod 2 = 1%nat) /\ q <> 2v + 4
		589	end.
		591	(** The K bound along a phase from K' (Lemma K, Lemma A1); j is the frame offset. *)
		592	Definition KI (j q r L v : nat) : Prop :=
		593	match r with
		594	\| O => 2^L <= j + q /\ (2^(S L) <= j + 2*v + 2 \/ 2^(S L) + 1 <= j + q) /\
		595	(q = 0%nat -> v <> 0%nat) /\ (L = 0%nat -> 4 <= q)
		596	\| 1%nat => 2^(S (S L)) + 2 <= q /\ (v = 0%nat -> 2^(S L) + 5 <= q)
		597	\| _ => 2^(S L) + 2 <= j + q /\ 2*v + 5 <= q
		598	end.
		600	(** The overflow bound along a phase from a zone-dominated start (Lemma Z'), target cap C. *)
		601	Definition ZI (C q r L v : nat) : Prop :=
		602	1 <= C /\
		603	match r with
		604	\| O => L <= S C /\ q + 2^(S (S L)) + C <= 2*v + L + 2^(S (S (S C))) + 1 /\
		605	(q = 0%nat -> v = 0%nat -> L <= C)
		606	\| 1%nat => S (S L) <= C /\ q <= 2^(S (S L)) + 1 /\ 3 <= q
		607	\| _ => S L <= C /\ q <= 2*v + 2^(S L) + 1
		608	end.
		610	Lemma Saf_step q r L v q' r' L' v': Rnd q r L v q' r' L' v' -> v < 2^L -> Saf q r L v -> Saf q' r' L' v'.
		611	Proof.
		612	intros H Hv HS. pose proof (pow_pos L) as HL. pose proof (pow0 L) as H0.
		613	destruct H; cbn [Saf] in *; pw; lia.
		614	Qed.
		616	Lemma KI_step j q r L v q' r' L' v': Rnd q r L v q' r' L' v' -> v < 2^L -> KI j q r L v -> KI (j+2) q' r' L' v'.
		617	Proof.
		618	intros H Hv HK. pose proof (pow_pos L) as HL. pose proof (pow0 L) as H0.
		619	destruct H; cbn [KI] in *.
		620	1-5: pw; lia.
		621	destruct L as [\|L]; cbn [Nat.pow] in *; [lia\|]. pose proof (pow_pos L). pw. lia.
		622	Qed.
		624	Lemma pow_mono a b: a <= b -> 2^a <= 2^b.
		625	Proof. intros H. apply Nat.pow_le_mono_r; lia. Qed.
		627	Lemma pow_lin a: S a <= 2^a.
		628	Proof. pose proof (Nat.pow_gt_lin_r 2 a ltac:(lia)). lia. Qed.
		630	Lemma ZI_step C q r L v q' r' L' v': Rnd q r L v q' r' L' v' -> v < 2^L -> ZI C q r L v -> ZI C q' r' L' v'.
		631	Proof.
		632	intros H Hv [HC HZ]. split; [exact HC\|]. pose proof (pow_pos L) as HL. pose proof (pow_lin C) as HlC.
		633	pose proof (pow0 L) as H0.
		634	destruct H; cbn [ZI] in *.
		635	- pw; lia.
		636	- pw; lia.
		637	- (* R2 *) pose proof (pow_mono (S (S L)) C ltac:(lia)). pw; lia.
		638	- (* O2 *) pose proof (pow_mono (S L) C ltac:(lia)). pw; lia.
		639	- (* O1 *) pw; lia.
		640	- (* O0 *) destruct (Nat.eq_dec L (S C)) as [E\|E].
		641	+ subst L. pw. lia.
		642	+ destruct L as [\|L]; cbn [Nat.pow] in *; [lia\|]. pose proof (pow_pos L). pw. lia.
		643	Qed.
		645	(** The phase invariant of a level started at t = (n, r, L, v): sign law (Qv), the U5 bound,
		646	safety, the K bound (t in K') and the overflow bound (t in J, zone-dominated). *)
		647	Definition PI (n r L v j q r' L' v' : nat) : Prop :=
		648	j mod 2 = 0%nat /\ Qv j q r' L' v' = Mv n r L v /\
		649	(r' = 1%nat -> j = 0%nat) /\ (r' = 2%nat -> L' = 0%nat -> j <= 2) /\
		650	Saf q r' L' v' /\ (Kx n r L v -> KI j q r' L' v') /\
		651	(Jst n r -> ~ Kst n r L -> ZI (S (cap r L)) q r' L' v').
		653	Lemma PI_step n r L v j q r1 L1 v1 q' r' L' v':
		654	Rnd q r1 L1 v1 q' r' L' v' -> v1 < 2^L1 -> PI n r L v j q r1 L1 v1 -> PI n r L v (j+2) q' r' L' v'.
		655	Proof.
		656	intros H Hv [H1 [H2 [H3 [H4 [H5 [H6 H7]]]]]].
		657	split; [lia\|]. split; [rewrite <-H2; symmetry; apply Rnd_sign; exact H\|].
		658	split; [intros E; subst r'; inversion H\|].
		659	split.
		660	{ intros E1 E2. inversion H; subst; try discriminate.
		661	- cbn in Hv. lia.
		662	- specialize (H3 eq_refl). lia. }
		663	split; [eapply Saf_step; eauto\|].
		664	split; [intros HK; eapply KI_step; eauto\|].
		665	intros HJ HK. eapply ZI_step; eauto.
		666	Qed.
		668	Lemma Mv_lt3 n r L v: Mv n r L v < 3.
		669	Proof. unfold Mv. apply Nat.mod_upper_bound. lia. Qed.
		671	Lemma Qv0 q r L v: Qv 0 q r L v = Mv q r L v.
		672	Proof. unfold Qv. rewrite Nat.mul_0_r, Nat.add_0_r. apply Nat.mod_small, Mv_lt3. Qed.
		674	Lemma Pre_n3 n r L v: Pre n r L v -> 3 <= n.
		675	Proof.
		676	intros [[H _]\|[H _]]; [exact H\|]. unfold Kst in H. pose proof (pow_pos (S (cap r L))). lia.
		677	Qed.
		679	Lemma Saf_start n r L v: r < 3 -> v < 2^L -> Pre n r L v -> Saf n r L v.
		680	Proof.
		681	intros Hr Hv HP. pose proof (pow_pos L) as HL. pose proof (pow0 L) as H0.
		682	destruct HP as [[Hn Hp]\|[HK [HT H6]]].
		683	- destruct r as [\|[\|[\|r]]]; cbn [Saf]; pw; lia.
		684	- unfold Kst in HK. destruct r as [\|[\|[\|r]]]; cbn [Saf]; rewrite ?cap0, ?cap1, ?cap2 in HK; pw; try lia.
		685	destruct (Nat.eq_dec L 0) as [->\|EL]; [cbn in *; lia\|].
		686	assert (2 <= 2^L) by (destruct L; [lia\|]; cbn [Nat.pow]; pose proof (pow_pos L); lia). lia.
		687	Qed.
		689	Lemma KI_start n r L v: r < 3 -> v < 2^L -> Kx n r L v -> KI 0 n r L v.
		690	Proof.
		691	intros Hr Hv [HK [HT H6]]. pose proof (pow_pos L) as HL. pose proof (pow0 L) as H0.
		692	unfold Kst in HK. destruct r as [\|[\|[\|r]]]; cbn [KI]; rewrite ?cap0, ?cap1, ?cap2 in HK; pw; try lia.
		693	destruct (Nat.eq_dec L 0) as [->\|EL]; [cbn in *; lia\|].
		694	assert (2 <= 2^L) by (destruct L; [lia\|]; cbn [Nat.pow]; pose proof (pow_pos L); lia). lia.
		695	Qed.
		697	Lemma ZI_start n r L v: r < 3 -> v < 2^L -> Jst n r -> ~ Kst n r L -> ZI (S (cap r L)) n r L v.
		698	Proof.
		699	intros Hr Hv [Hn Hp] HK. pose proof (pow_pos L) as HL. pose proof (pow0 L) as H0.
		700	unfold Kst in HK. split; [lia\|].
		701	destruct r as [\|[\|[\|r]]]; cbn [ZI]; rewrite ?cap0, ?cap1, ?cap2 in *; pw; lia.
		702	Qed.
		704	Lemma PI_start n r L v: r < 3 -> v < 2^L -> Pre n r L v -> PI n r L v 0 n r L v.
		705	Proof.
		706	intros Hr Hv HP. split; [reflexivity\|]. split; [apply Qv0\|].
		707	split; [reflexivity\|]. split; [lia\|]. split; [apply Saf_start; assumption\|].
		708	split; [intros HK; apply KI_start; assumption\|].
		709	intros HJ HK. apply ZI_start; assumption.
		710	Qed.
		712	( What a level guarantees about its pop (proof.md 6, U1-U4, plus the (6,4,0) bound U5).
		713	A level from t = (n, r, L, v) at frame P pops at RT l (P + n') (zone r' L' v'). *)
		714	Definition Post (n r L v n' r' L' v' : nat) : Prop :=
		715	r' < 3 /\ v' < 2^L' /\
		716	(Jst n r -> Jst (S n') r') /\
		717	(Kx n r L v -> Kst n' r' L') /\
		718	(Jst n r -> ~ Kst n r L -> Kst (S n') r' L' \/ cap r' L' <= S (cap r L)) /\
		719	(Mv n' r' L' v' + Mv n r L v) mod 3 = 0%nat /\
		720	(r' = 1%nat -> L' = 0%nat -> v' = 0%nat -> n' = 4%nat \/ 8 <= n').
		722	Definition U (N : nat) : Prop :=
		723	forall P l n r L v, okL P l -> r < 3 -> v < 2^L -> Pre n r L v ->
		724	(forall n' r' L' v', Post n r L v n' r' L' v' -> safe (RT l (P + n') (zone r' L' v')) (N - 1)) ->
		725	safe (RT (lev P l) n (zone r L v)) N.
		727	( Bites (proof.md 3.3, Lemma P3) *)
		729	Lemma lowones L: forall v, v < 2^L -> v <> 2^L - 1 ->
		730	exists k L' o, L = k + S L' /\ v = 2^k - 1 + 2^(S k) * o /\ o < 2^L'.
		731	Proof.
		732	induction L as [\|L IH]; intros v Hv Hne.
		733	- cbn in *. lia.
		734	- rewrite Nat.pow_succ_r' in Hv, Hne.
		735	destruct (Nat.Even_or_Odd v) as [[o Ho]\|[v' Hv']].
		736	+ exists 0%nat, L, o. cbn. lia.
		737	+ destruct (IH v') as [k [L' [o [E1 [E2 E3]]]]]; [lia\|lia\|].
		738	exists (S k), L', o. split; [lia\|]. split; [\|exact E3].
		739	subst v v'. pose proof (pow_pos k). pw. lia.
		740	Qed.
		742	Lemma bite_shape j qb rb Lb vb: qb <= 2 -> rb < 3 -> vb < 2^Lb -> Saf qb rb Lb vb -> 2 <= j ->
		743	(rb = 1%nat -> j = 0%nat) ->
		744	(exists e r' L' v', EB qb rb Lb vb e r' L' v') \/
		745	(qb = 2%nat /\ rb = 0%nat /\ exists k L' o, Lb = k + S L' /\ vb = 2^k - 1 + 2^(S k) * o /\ o < 2^L').
		746	Proof.
		747	intros Hq Hr Hv HS Hj H1.
		748	destruct rb as [\|[\|[\|rb]]]; [\| lia \| \| lia]; cbn [Saf] in HS.
		749	- destruct HS as [HS1 [HS2 HS3]].
		750	destruct qb as [\|[\|[\|qb]]]; [\| \| \|lia].
		751	+ destruct Lb as [\|Lb]; [lia\|]. left.
		752	destruct (Nat.eq_dec vb 0) as [->\|Hne].
		753	* eexists _, _, _, _. apply EB0c.
		754	* destruct (lowbit vb Hne) as [b [o ->]].
		755	destruct b as [\|b]; [rewrite Nat.pow_0_r, Nat.mul_1_l in HS3; lia\|].
		756	destruct (lowbit_lt _ _ _ Hv) as [Hb Ho].
		757	replace (S Lb) with (S b + S (Lb - b - 1)) by lia.
		758	eexists _, _, _, _. apply EB0.
		759	+ destruct Lb as [\|Lb]; [lia\|]. left.
		760	destruct (Nat.Even_or_Odd vb) as [[w ->]\|[w ->]]; eexists _, _, _, _; [apply EB1z0\|apply EB1z1].
		761	+ right. split; [reflexivity\|]. split; [reflexivity\|]. apply lowones; [exact Hv\|]. tauto.
		762	- destruct HS as [HS1 HS2]. assert (qb = 1%nat) as -> by lia.
		763	left. eexists _, _, _, _. apply EB1t.
		764	Qed.
		766	Lemma EB_valid q r L v e r' L' v': EB q r L v e r' L' v' -> v < 2^L -> r' < 3 /\ v' < 2^L'.
		767	Proof.
		768	intros H Hv. destruct H; (split; [lia\|]).
		769	- pw. lia.
		770	- pw. lia.
		771	- exact Hv.
		772	- exact Hv.
		773	- rewrite Nat.pow_add_r in *. pw. pose proof (pow_pos b). pose proof (pow_pos L).
		774	assert (o < 2^L) by nia. nia.
		775	- pose proof (pow_pos L). pw. lia.
		776	- cbn. lia.
		777	Qed.
		779	Lemma EB_lev q r L v e r' L' v' P l: 1 <= P -> EB q r L v e r' L' v' ->
		780	RT (lev P l) q (zone r L v) -->+ RT l (P + e) (zone r' L' v').
		781	Proof. intros HP H. destruct P as [\|p]; [lia\|]. cbn [lev]. apply EB_tape. exact H. Qed.
		783	Lemma Kst_mono n n' r L: Kst n r L -> n <= n' -> Kst n' r L.
		784	Proof. unfold Kst. lia. Qed.
		786	(** A plain end: the first bite of the level is an ending bite (proof.md 5.5, 5.7 plain cases). *)
		787	Lemma ending n r L v j qb rb Lb vb e r' L' v':
		788	EB qb rb Lb vb e r' L' v' -> PI n r L v j qb rb Lb vb -> 2 <= j -> vb < 2^Lb ->
		789	Post n r L v (j + e) r' L' v'.
		790	Proof.
		791	intros H [H1 [H2 [H3 [H4 [H5 [H6 H7]]]]]] Hj Hvb.
		792	destruct (EB_valid _ _ _ _ _ _ _ _ H Hvb) as [Hr' Hv'].
		793	pose proof (EB_sign _ _ _ _ _ _ _ _ j H) as HS. rewrite H2 in HS.
		794	split; [exact Hr'\|]. split; [exact Hv'\|].
		795	split.
		796	{ intros _. unfold Jst. destruct H; split; lia. }
		797	split.
		798	{ intros HK. specialize (H6 HK). unfold Kst.
		799	destruct H; cbn [KI] in H6; rewrite ?cap0, ?cap1, ?cap2; cbn [Nat.add] in *; pw; lia. }
		800	split.
		801	{ intros HJ HK. destruct (H7 HJ HK) as [HC7 HZ7]. right.
		802	destruct H; cbn [ZI] in HZ7; rewrite ?cap0, ?cap1, ?cap2; cbn [Nat.add] in *; lia. }
		803	split; [exact HS\|].
		804	intros E1 E2 E3. destruct H; try discriminate E1. subst. left. specialize (H4 eq_refl eq_refl). lia.
		805	Qed.
		807	(** B2 then B1 (PUSH with k = 0, then the B1 of zone 1). *)
		808	Lemma ending_B2 n r L v j L' o:
		809	PI n r L v j 2 0 (0 + S L') (2^0 - 1 + 2^1 * o) -> 2 <= j -> o < 2^L' ->
		810	Post n r L v (j + 4) 0 L' o.
		811	Proof.
		812	intros [H1 [H2 [H3 [H4 [H5 [H6 H7]]]]]] Hj Ho. cbn [Nat.add Nat.pow Nat.sub] in *.
		813	split; [lia\|]. split; [exact Ho\|].
		814	split; [intros _; unfold Jst; lia\|].
		815	split.
		816	{ intros HK. specialize (H6 HK). unfold Kst. cbn [KI] in H6. rewrite cap0. pw. lia. }
		817	split.
		818	{ intros HJ HK. destruct (H7 HJ HK) as [HC7 HZ7]. right. cbn [ZI] in HZ7. rewrite cap0. lia. }
		819	split.
		820	{ rewrite <-H2. unfold Qv, Mv, cap. cbn [Nat.eqb]. rewrite !Nat.pow_add_r. cbn [Nat.pow].
		821	pose proof (pow_pos L'). lia. }
		822	intros E. discriminate E.
		823	Qed.
		825	( The stack of a nested bite (proof.md 3.4): budget and sign along the inner levels *)
		827	(** Budget(t, C): d(t) >= 2, or cap(t) <= C (Lemmas Kp and Z' carry it from level to level). *)
		828	Definition Budget (n r L C : nat) : Prop := Kst n r L \/ cap r L <= C.
		830	(** Sign relation after j levels: X - 1 alternates in sign (proof.md 5.4, rule N). *)
		831	Definition SR (j a b : nat) : Prop :=
		832	(j mod 2 = 0%nat -> b = a) /\ (j mod 2 = 1%nat -> (a + b + 2) mod 3 = 0%nat).
		834	Lemma JK n r L v: Jst n r -> Kst n r L -> Kx n r L v.
		835	Proof.
		836	intros [Hn Hp] HK. split; [exact HK\|]. split.
		837	- intros [-> [_ ->]]. pw. specialize (Hp ltac:(lia)). lia.
		838	- intros [-> [-> _]]. specialize (Hp ltac:(lia)). lia.
		839	Qed.
		841	Lemma Budget_step n r L v C n' r' L' v': Jst n r -> Budget n r L C -> Post n r L v n' r' L' v' ->
		842	Budget (S n') r' L' (S C).
		843	Proof.
		844	intros HJ HB [_ [_ [_ [HU2 [HU3 _]]]]].
		845	destruct (Nat.le_gt_cases (2^(S (cap r L)) + 2) n) as [HK\|HK].
		846	- left. apply (Kst_mono n'); [apply HU2, JK; assumption \| lia].
		847	- destruct HB as [HB\|HB]; [unfold Kst in HB; lia\|].
		848	destruct (HU3 HJ ltac:(unfold Kst; lia)) as [H\|H]; [left; exact H \| right; lia].
		849	Qed.
		851	Lemma Mv_shift a n r L v: Mv (a + n) r L v = (Mv n r L v + a) mod 3.
		852	Proof. unfold Mv. generalize (if Nat.eqb r 1 then v else 2v) (2 2^(cap r L + 2)). intros x y. lia. Qed.
		854	Lemma SR_step j n r L v n' r' L' v' b: b < 3 -> Post n r L v n' r' L' v' -> SR j (Mv (S n') r' L' v') b ->
		855	SR (S j) (Mv n r L v) b.
		856	Proof.
		857	intros Hb [_ [_ [_ [_ [_ [HU4 _]]]]]] [HE HO].
		858	change (S n') with (1 + n') in HE, HO. rewrite Mv_shift in HE, HO.
		859	pose proof (Mv_lt3 n r L v). pose proof (Mv_lt3 n' r' L' v').
		860	split; intros Hj; lia.
		861	Qed.
		863	Lemma pow2_mod3 k: exists x, 2^k = 3*x + 1 + k mod 2.
		864	Proof.
		865	induction k as [\|k [x Hx]]; [exists 0%nat; reflexivity\|].
		866	exists (2*x + k mod 2). rewrite Nat.pow_succ_r', Hx. pose proof (Nat.mod_upper_bound k 2). lia.
		867	Qed.
		869	(** The sign of the bite zone (110)^k 111 Y against the zone of t_2 (proof.md 5.4, N row). *)
		870	Lemma QvN j k L o:
		871	(k mod 2 = 0%nat -> Qv j 2 0 (S k + S L) (2^(S k) - 1 + 2^(S (S k)) * o) = (Mv 3 0 L o + 1 + 2*j) mod 3) /\
		872	(k mod 2 = 1%nat -> Qv j 2 0 (S k + S L) (2^(S k) - 1 + 2^(S (S k)) * o) = (2 * (Mv 3 0 L o + 1) + 2*j) mod 3).
		873	Proof.
		874	destruct (pow2_mod3 k) as [x Hx]. pose proof (pow_pos L).
		875	unfold Qv, Mv, cap. cbn [Nat.eqb]. rewrite !Nat.pow_add_r. cbn [Nat.pow]. rewrite Hx.
		876	split; intros Hk; rewrite Hk; lia.
		877	Qed.
		879	(** The composite form of a level with a nested bite (proof.md 3.4, 5.7): the outer level
		880	resumes at t_(k+1) and its pop is that of the resumed phase, shifted by j + 2. *)
		881	Lemma compose n r L v j k L' o n1 r1 L1 v1 n3 r3 L3 v3:
		882	PI n r L v j 2 0 (S k + S L') (2^(S k) - 1 + 2^(S (S k)) * o) -> 2 <= j ->
		883	Jst n1 r1 -> Budget n1 r1 L1 (L' + k) -> SR k (Mv 3 0 L' o) (Mv n1 r1 L1 v1) ->
		884	Post n1 r1 L1 v1 n3 r3 L3 v3 -> Post n r L v (j + 2 + n3) r3 L3 v3.
		885	Proof.
		886	intros [H1 [H2 [H3 [H4 [H5 [H6 H7]]]]]] Hj HJ1 HB1 HSR HP.
		887	pose proof (Budget_step _ _ _ _ _ _ _ _ _ HJ1 HB1 HP) as HB3.
		888	destruct HP as [Hr3 [Hv3 [HU1 [HU2 [HU3 [HU4 HU5]]]]]].
		889	destruct (HU1 HJ1) as [Hn3 Hp3].
		890	split; [exact Hr3\|]. split; [exact Hv3\|].
		891	split.
		892	{ intros _. split; [lia\|]. intros E. specialize (Hp3 E). lia. }
		893	split.
		894	{ intros HK. specialize (H6 HK). cbn [KI] in H6. unfold Kst.
		895	destruct HB3 as [HB3\|HB3]; [unfold Kst in HB3; lia\|].
		896	pose proof (pow_mono (S (cap r3 L3)) (S k + S L') ltac:(lia)). lia. }
		897	split.
		898	{ intros HJ HK. destruct (H7 HJ HK) as [HC7 HZ7]. cbn [ZI] in HZ7.
		899	destruct HB3 as [HB3\|HB3]; [left; apply (Kst_mono (S n3)); [exact HB3\|lia] \| right; lia]. }
		900	split.
		901	{ rewrite (Mv_shift (j + 2) n3). destruct HSR as [HE HO]. destruct (QvN j k L' o) as [QE QO].
		902	pose proof (Mv_lt3 n3 r3 L3 v3). pose proof (Mv_lt3 n1 r1 L1 v1). pose proof (Mv_lt3 3 0 L' o).
		903	pose proof (Nat.mod_upper_bound k 2 ltac:(lia)).
		904	rewrite <-H2.
		905	destruct (Nat.eq_dec (k mod 2) 0) as [Ek\|Ek].
		906	- rewrite (QE Ek). specialize (HE Ek). lia.
		907	- assert (Ek1: k mod 2 = 1%nat) by lia. rewrite (QO Ek1). specialize (HO Ek1). lia. }
		908	intros E1 E2 E3. right. destruct (HU5 E1 E2 E3); lia.
		909	Qed.
		911	Lemma STK: forall j B, (forall B', B' <= B -> U B') -> forall n r L v C X,
		912	Jst n r -> Budget n r L C -> r < 3 -> v < 2^L ->
		913	(forall n1 r1 L1 v1, Jst n1 r1 -> Budget n1 r1 L1 (C + j) -> r1 < 3 -> v1 < 2^L1 ->
		914	SR j (Mv n r L v) (Mv n1 r1 L1 v1) -> safe (RT X n1 (zone r1 L1 v1)) (B - j)) ->
		915	safe (RT (Nat.iter j (FR 0) X) n (zone r L v)) B.
		916	Proof.
		917	induction j as [\|j IH]; intros B HU n r L v C X HJ HB Hr Hv Hk.
		918	- cbn [Nat.iter].
		919	pose proof (Hk n r L v HJ ltac:(rewrite Nat.add_0_r; exact HB) Hr Hv
		920	ltac:(split; intros; [reflexivity\|lia])) as H.
		921	rewrite Nat.sub_0_r in H. exact H.
		922	- change (Nat.iter (S j) (FR 0) X) with (lev 1 (Nat.iter j (FR 0) X)).
		923	apply (HU B (le_n B) 1%nat (Nat.iter j (FR 0) X) n r L v (okL_S 0 _) Hr Hv (or_introl HJ)).
		924	intros n' r' L' v' HP.
		925	change (1 + n') with (S n').
		926	pose proof HP as [Hr' [Hv' [HU1 _]]].
		927	apply (IH (B - 1) (fun B' HB' => HU B' ltac:(lia)) (S n') r' L' v' (S C) X (HU1 HJ)
		928	(Budget_step _ _ _ _ _ _ _ _ _ HJ HB HP) Hr' Hv').
		929	intros n1 r1 L1 v1 HJ1 HB1 Hr1 Hv1 HS1.
		930	replace (B - 1 - j) with (B - S j) by lia.
		931	apply Hk; try assumption.
		932	+ replace (C + S j) with (S C + j) by lia. exact HB1.
		933	+ eapply SR_step; [apply Mv_lt3 \| eassumption \| eassumption].
		934	Qed.
		936	( U(N) for every N (proof.md 6): strong induction on the number of steps *)
		938	Lemma U_all: forall N, U N.
		939	Proof.
		940	intros N. induction N as [N IH] using strong_induction.
		941	intros P l n r L v Hl Hr Hv Hpre Hk.
		942	pose proof (Pre_n3 _ _ _ _ Hpre) as Hn.
		943	destruct N as [\|N'].
		944	{ destruct (Rnd_exists n r L v Hn Hr) as [q' [r' [L' [v' HR]]]].
		945	eapply safe_prog0. eapply Rnd_tape; eassumption. }
		946	destruct (phase (PI n r L v) (PI_step n r L v) n 0 P l r L v)
		947	as [j [qb [rb [Lb [vb [Hqb [Hrb [Hvb [HI [_ [Hj Hrun]]]]]]]]]]].
		948	{ rewrite Nat.add_0_r. exact Hl. }
		949	{ exact Hr. } { exact Hv. } { apply PI_start; assumption. }
		950	specialize (Hj Hn). rewrite Nat.add_0_r in Hrun. cbn [Nat.add] in Hj.
		951	eapply safe_ev; [exact Hrun\|].
		952	assert (HlP: okL (P + j) l) by (apply okL_ge; lia).
		953	pose proof HI as [_ [_ [HI3 [_ [HI5 _]]]]].
		954	destruct (bite_shape j qb rb Lb vb Hqb Hrb Hvb HI5 Hj HI3)
		955	as [[e [r' [L' [v' HE]]]] \| [Eq [Er [k [L' [o [EL [Ev Ho]]]]]]]].
		956	- (* an ending bite: the pop *)
		957	eapply safe_prog. { apply EB_lev; [lia \| exact HE]. }
		958	replace (P + j + e) with (P + (j + e)) by lia.
		959	apply Hk. eapply ending; eassumption.
		960	- subst qb rb Lb vb. destruct k as [\|k].
		961	+ (* B2, then B1 *)
		962	eapply safe_prog.
		963	{ eapply progress_trans. { apply (PUSH_lev 0 L' o (P + j) l HlP). }
		964	cbn [Nat.iter]. apply (EB_lev 1 1 L' o 2 0 L' o (P + j + 2) l); [lia \| constructor]. }
		965	replace (P + j + 2 + 2) with (P + (j + 4)) by lia.
		966	apply Hk. apply ending_B2; assumption.
		967	+ (* the nested bite N: PUSH, the innermost B1, the stack, then the rest of the level *)
		968	assert (Hpush: RT (lev (P + j) l) 2 (zone 0 (S k + S L') (2^(S k) - 1 + 2^(S (S k)) * o)) -->+
		969	RT (Nat.iter k (FR 0) (lev (P + j + 2) l)) 3 (zone 0 L' o)).
		970	{ eapply progress_trans. { apply (PUSH_lev (S k) L' o (P + j) l HlP). } apply inner1. }
		971	eapply safe_prog; [exact Hpush\|].
		972	replace (S N' - 1) with N' by lia.
		973	apply (STK k N' (fun B HB => IH B ltac:(lia)) 3 0 L' o L' (lev (P + j + 2) l)).
		974	* split; [lia\|]. intros E; lia.
		975	* right. rewrite cap0. lia.
		976	* lia.
		977	* exact Ho.
		978	* intros n1 r1 L1 v1 HJ1 HB1 Hr1 Hv1 HS1.
		979	apply (IH (N' - k) ltac:(lia) (P + j + 2) l n1 r1 L1 v1 (okL_ge (P + j + 2) l ltac:(lia)) Hr1 Hv1 (or_introl HJ1)).
		980	intros n3 r3 L3 v3 HP3.
		981	replace (P + j + 2 + n3) with (P + (j + 2 + n3)) by lia.
		982	apply (safe_mono _ (S N' - 1)); [\| lia].
		983	apply Hk. eapply compose; eassumption.
		984	Qed.
		986	( Cycles from I (proof.md 5.8) and the main theorem *)
		988	Lemma Ist_Kx n r L v: Ist n r L v -> Kx n r L v.
		989	Proof.
		990	unfold Ist, Kx. intros [Hr [Hv [HK [HM H6]]]]. split; [exact HK\|]. split; [\|exact H6].
		991	intros [-> [-> ->]]. apply HM. unfold Mv, cap. cbn [Nat.eqb]. rewrite !Nat.pow_add_r. cbn [Nat.pow].
		992	pose proof (pow_pos L). lia.
		993	Qed.
		995	Lemma cycles N: forall n r L v, Ist n r L v -> safe (RT (const 0) n (zone r L v)) N.
		996	Proof.
		997	induction N as [N IH] using strong_induction. intros n r L v HI.
		998	pose proof (Ist_Kx _ _ _ _ HI) as HK. destruct HI as [Hr [Hv [HKs [HM H6]]]].
		999	apply (U_all N 0%nat (const 0) n r L v); [intros _; reflexivity \| exact Hr \| exact Hv \| right; exact HK \|].
		1000	intros n' r' L' v' [Hr' [Hv' [_ [HU2 [_ [HU4 HU5]]]]]].
		1001	destruct N as [\|N']; [apply safe_RT0\|].
		1002	replace (S N' - 1) with N' by lia.
		1003	change (0 + n')%nat with n'. apply IH; [lia\|]. unfold Ist. split; [exact Hr'\|]. split; [exact Hv'\|]. split; [apply HU2, HK\|].
		1004	pose proof (Mv_lt3 n r L v). pose proof (Mv_lt3 n' r' L' v'). split; [lia\|].
		1005	intros [E1 [E2 [E3 E4]]]. destruct (HU5 E2 E3 E4); lia.
149	Qed.	1006	Qed.
151	Lemma nonhalt: ~halts tm c0.	1008	Lemma nonhalt: ~halts tm c0.
152	Proof.	1009	Proof.
153	eapply multistep_nonhalt with (c':=S (6,6)).
		1010	intros [N HN].
154	1: unfold S; esx.
		1011	exact (safe_ev c0 _ N init (cycles N 6 2 0 0 init_I) N (le_n N) HN).
155	eapply progress_nonhalt_cond with (P:=fun '(a,b) => a<=1+b).
156	2: lia.
⋯ 5 template-only lines (template 157–161), not in ours
162	zify_le_mul_r; lia.
163	- lia.
164	Qed.	1012	Qed.
		1014	(*
		1015	1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB (only F0 is undefined)
		1017	zone(r,L,v) = 1^r (1 1 c_0) ... (1 1 c_(L-1)) 1 1 1, c_b = 0 iff bit b of v is set (width 3L+3+r)
		1018	frame p = 0 0 (10)^p 1; RT l q Z = l C> 0 0 (10)^q Z 0^inf
		1019	lev P l = frame P-1 on top of l (P >= 1); lev 0 l = l = 0^inf (the cycle start)
		1021	R1 q -> q-2, v -> v-1 q >= 3, v >= 1, r = 0, 2
		1022	R2 q -> q-3, zone(1,L,v) -> zone(0,L+1,2v-2) q >= 3, v >= 1
		1023	O2 q -> q-2, zone(2,L,0) -> zone(0,L+1,2^(L+1)-1)
		1024	O1 q -> q-2, zone(1,L,0) -> zone(2,L,2^L-1)
		1025	O0 q -> q-3, zone(0,L,0) -> zone(0,L+1,2^(L+1)-2) (every round: P -> P+2)
		1026	PUSH q = 2, zone(0,k+1+L, 2^k-1 + 2^(k+1) o) -> k new frames 0 over P+2, q = 1, zone(1,L,o)
		1027	(k = 0: B2; k >= 1: nested levels; all bits set: halts)
		1028	B1 q = 1: pop frame p, q -> p+3 (+1 if bit 0 set), zone loses its first cell
		1029	B0 q = 0, bit 0 clear: pop, q -> p+3; B0c q = 0, v = 0: pop, q -> p+2 (p+1 on 111)
		1031	level starts t = (n,r,L,v): cap = L + [r = 1], K: n >= 2^(cap+1) + 2, J: n >= 3, n odd if r <> 0
		1032	K' = K minus (2^(L+1)+2, 2, L, 2^L-1) and (6, 1, 0, 0); M = n + (r = 1 ? v : 2v) + 2^(cap+3) mod 3
		1033	phase invariants, kept by every round: Saf (no halt, every bite has a rule), KI (start in K'),
		1034	ZI (start in J with n < 2^(cap+1) + 2), Qv = M + 2P mod 3 (sign law)
		1035	U(N): a level from t in J or K' at any frame does not halt within N steps if every pop t' with
		1036	U1-U5 is safe for N-1 steps; the inner levels of a nested bite and the rest of the level after
		1037	it use U at fewer steps (STK, compose)
		1038	I = K' with M <> 0 is closed under cycles; start: c0 -->(327) q = 6, zone(2,0,0) = 11111, no frame
		1039	*)

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

129 items in 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v (1039 lines): 102 Lemma, 24 Definition, 2 Inductive, 1 Fixpoint. 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 "1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB").	L23	identicalexcept the TM string
2	Lemma	`BR`	Lemma BR k: forall l r, l {{B}}> [1]^^k > r --> [1]^^k *> l {{B}}> r.	L30	new
3	Lemma	`SW`	Lemma SW k: forall l r, [1;0]^^k > l <{{C}} r --> l <{{C}} [0;1]^^k *> r.	L33	new
4	Lemma	`TT`	Lemma TT j: forall l r, [1;1;1]^^j > l <{{C}} r --> l <{{C}} [0;1;1]^^j *> r.	L36	new
5	Lemma	`PS`	Lemma PS b: forall l r, [1;1;0] > l {{B}}> [1;0]^^b > r -->* [1;1] > [0;1]^^b > [0] *> l {{B}}> r.	L39	new
6	Lemma	`RND2`	Lemma RND2 q j: forall l r, l {{C}}> [0;0] > [1;0]^^(q+3) > [1;1;1]^^j > [1;1;0] > r -->+ [1;0;1;0] > l {{C}}> [0;0] > [1;0]^^(q+1) > [1;1;0]^^j > [1;1;1] *> r.	L43	new
7	Lemma	`RND1`	Lemma RND1 q j: forall l r, l {{C}}> [0;0] > [1;0]^^(q+3) > [1;1;1]^^j > [1;1;1;1;0] > r -->+ [1;0;1;0] > l {{C}}> [0;0] > [1;0]^^(q+1) > [1;1;1;1] > [0;1;1]^^j > [1] > r.	L48	new
8	Lemma	`RND0`	Lemma RND0 q j: forall l r, l {{C}}> [0;0] > [1;0]^^(q+3) > [1;1;1]^^j > [1;1;1;0] > r -->+ [1;0;1;0] > l {{C}}> [0;0] > [1;0]^^q > [1;1;1;1;1] > [0;1;1]^^j > [1] > r.	L53	new
9	Lemma	`PUSH`	Lemma PUSH k: forall l r, l {{C}}> [0;0] > [1;0]^^2 > [1;1;0]^^k > [1;1;1] > r -->+ [1;0;0]^^k > [1;0;1;0] > l {{C}}> [0;0] > [1;0] > [1] *> r.	L59	new
10	Lemma	`BITE1`	Lemma BITE1 p: forall l r, [1] > [0;1]^^p > [0;0] > l {{C}}> [0;0] > [1;0] > [1;1] > r -->+ l {{C}}> [0;0] > [1;0]^^(p+3) > [1] *> r.	L65	new
11	Lemma	`BITE0`	Lemma BITE0 p j: forall l r, [1] > [0;1]^^p > [0;0] > l {{C}}> [0;0] > [1;1;1]^^j > [1;1;0] > r -->+ l {{C}}> [0;0] > [1;0]^^(p+2) > [1] > [0;1;1]^^j > [1] *> r.	L70	new
12	Lemma	`BITE0c`	Lemma BITE0c p j: forall l r, [1] > [0;1]^^p > [0;0] > l {{C}}> [0;0] > [1;1;1]^^j > [1;1;1;1;1;1;0] > r -->+ l {{C}}> [0;0] > [1;0]^^(p+2) > [1;1;1] > [1;1;0]^^j > [1;1;1] *> r.	L75	new
13	Lemma	`BITE0c3`	Lemma BITE0c3 p: forall l r, [1] > [0;1]^^p > [0;0] > l {{C}}> [0;0] > [1;1;1;0;0] > r -->+ l {{C}}> [0;0] > [1;0]^^(p+1) > [1;1;1;1;1;1] > r.	L80	new
14	Definition	`bitc`	Definition bitc (v : nat) : sym := if Nat.odd v then 0 else 1.	L88	new
15	Fixpoint	`dg`	Fixpoint dg (L v : nat) : list sym := match L with \| O => [] \| S L' => [1;1;bitc v] ++ dg L' (Nat.div2 v) end.	L90	new
16	Definition	`zone`	Definition zone (r L v : nat) : list sym := [1]^^r ++ dg L v ++ [1;1;1].	L96	new
17	Lemma	`bitc_even`	Lemma bitc_even v: bitc (2*v) = 1.	L98	new
18	Lemma	`bitc_odd`	Lemma bitc_odd v: bitc (2*v+1) = 0.	L101	new
19	Lemma	`div2_even`	Lemma div2_even v: Nat.div2 (2*v) = v.	L104	new
20	Lemma	`div2_odd`	Lemma div2_odd v: Nat.div2 (2*v+1) = v.	L107	new
21	Lemma	`dg_even`	Lemma dg_even L v: dg (S L) (2*v) = [1;1;1] ++ dg L v.	L110	new
22	Lemma	`dg_odd`	Lemma dg_odd L v: dg (S L) (2*v+1) = [1;1;0] ++ dg L v.	L113	new
23	Lemma	`pow_pos`	Lemma pow_pos P: 1 <= 2^P.	L116	new
24	Lemma	`dg_zero`	Lemma dg_zero L: dg L 0 = [1;1;1]^^L.	L119	new
25	Lemma	`dg_full`	Lemma dg_full L: dg L (2^L - 1) = [1;1;0]^^L.	L125	new
26	Lemma	`dg_low`	Lemma dg_low b L o: dg (b + S L) (2^b(2o+1)) = [1;1;1]^^b ++ [1;1;0] ++ dg L o.	L132	new
27	Lemma	`dg_lowones`	Lemma dg_lowones k L o: dg (k + S L) (2^k - 1 + 2^(S k)*o) = [1;1;0]^^k ++ [1;1;1] ++ dg L o.	L140	new
28	Lemma	`lowbit`	Lemma lowbit (x:nat): x <> 0%nat -> exists P o, x = 2^P(2o+1).	L149	new
29	Lemma	`lowbit_lt`	Lemma lowbit_lt b o L: 2^b(2o+1) < 2^L -> b < L /\ o < 2^(L-b-1).	L158	new
30	Lemma	`ones_comm`	Lemma ones_comm b: [1;1] ++ [1;1;1]^^b = [1;1;1]^^b ++ [1;1].	L169	new
31	Lemma	`one_comm`	Lemma one_comm b: [1] ++ [1;1;1]^^b = [1;1;1]^^b ++ [1].	L172	new
32	Lemma	`sh110`	Lemma sh110 b: [1;1] ++ [0;1;1]^^b = [1;1;0]^^b ++ [1;1].	L175	new
33	Lemma	`S_ones2`	Lemma S_ones2 b s: [1;1] > [1;1;1]^^b > s = [1;1;1]^^b > [1;1] > s.	L178	new
34	Lemma	`S_ones1`	Lemma S_ones1 b s: [1] > [1;1;1]^^b > s = [1;1;1]^^b > [1] > s.	L181	new
35	Lemma	`S_sh110`	Lemma S_sh110 b s: [1;1] > [0;1;1]^^b > s = [1;1;0]^^b > [1;1] > s.	L184	new
36	Definition	`RT`	Definition RT (l : side) (q : nat) (Z : list sym) : Q * tape := l {{C}}> [0;0] > [1;0]^^q > Z *> const 0.	L189	new
37	Lemma	`R1z`	Lemma R1z l q L v: 1 <= v -> v < 2^L -> RT l (q+3) (zone 0 L v) -->+ RT ([1;0;1;0] *> l) (q+1) (zone 0 L (v-1)).	L191	new
38	Lemma	`R1t`	Lemma R1t l q L v: 1 <= v -> v < 2^L -> RT l (q+3) (zone 2 L v) -->+ RT ([1;0;1;0] *> l) (q+1) (zone 2 L (v-1)).	L202	new
39	Lemma	`R2r`	Lemma R2r l q L v: 1 <= v -> v < 2^L -> RT l (q+3) (zone 1 L v) -->+ RT ([1;0;1;0] > l) q (zone 0 (S L) (2v-2)).	L216	new
40	Lemma	`O2r`	Lemma O2r l q L: RT l (q+3) (zone 2 L 0) -->+ RT ([1;0;1;0] *> l) (q+1) (zone 0 (S L) (2^(S L)-1)).	L230	new
41	Lemma	`O1r`	Lemma O1r l q L: RT l (q+3) (zone 1 L 0) -->+ RT ([1;0;1;0] *> l) (q+1) (zone 2 L (2^L-1)).	L240	new
42	Lemma	`O0r`	Lemma O0r l q L: RT l (q+3) (zone 0 L 0) -->+ RT ([1;0;1;0] *> l) q (zone 0 (S L) (2^(S L)-2)).	L251	new
43	Definition	`FR`	Definition FR (p : nat) (l : side) : side := [1] > [0;1]^^p > [0;0] *> l.	L265	new
44	Lemma	`PUSHr`	Lemma PUSHr l k L o: RT l 2 (zone 0 (k + S L) (2^k - 1 + 2^(S k)o)) -->+ RT ([1;0;0]^^k > [1;0;1;0] *> l) 1 (zone 1 L o).	L267	new
45	Lemma	`B1z0`	Lemma B1z0 p l L v: RT (FR p l) 1 (zone 0 (S L) (2*v)) -->+ RT l (p+3) (zone 2 L v).	L275	new
46	Lemma	`B1z1`	Lemma B1z1 p l L v: RT (FR p l) 1 (zone 0 (S L) (2*v+1)) -->+ RT l (p+4) (zone 0 L v).	L282	new
47	Lemma	`B1o`	Lemma B1o p l L v: RT (FR p l) 1 (zone 1 L v) -->+ RT l (p+3) (zone 0 L v).	L290	new
48	Lemma	`B1t`	Lemma B1t p l L v: RT (FR p l) 1 (zone 2 L v) -->+ RT l (p+3) (zone 1 L v).	L300	new
49	Lemma	`B0r`	Lemma B0r p l b L o: RT (FR p l) 0 (zone 0 (S b + S L) (2^(S b)(2o+1))) -->+ RT l (p+3) (zone 0 (b + S L) (2^b - 1 + 2^(S b)*o)).	L307	new
50	Lemma	`B0cr`	Lemma B0cr p l L: RT (FR p l) 0 (zone 0 (S L) 0) -->+ RT l (p+2) (zone 0 (S L) (2^(S L)-2)).	L318	new
51	Lemma	`B0c3r`	Lemma B0c3r p l: RT (FR p l) 0 (zone 0 0 0) -->+ RT l (p+1) (zone 0 1 0).	L328	new
52	Lemma	`FR_round`	Lemma FR_round p l: [1;0;1;0] *> FR p l = FR (p+2) l.	L339	new
53	Lemma	`init`	Lemma init: c0 -->* RT (const 0) 6 (zone 2 0 0).	L347	new
54	Definition	`lev`	Definition lev (P : nat) (l : side) : side := match P with \| O => l \| S p => FR p l end.	L353	new
55	Definition	`okL`	Definition okL (P : nat) (l : side) : Prop := P = 0%nat -> l = const 0.	L359	new
56	Lemma	`lev_round`	Lemma lev_round P l: okL P l -> [1;0;1;0] *> lev P l = lev (P+2) l.	L361	new
57	Lemma	`okL_S`	Lemma okL_S P l: okL (S P) l.	L368	new
58	Inductive	`Rnd`	Inductive Rnd : nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> Prop := \| RR1z q L v: 1 <= v -> Rnd (q+3) 0 L v (q+1) 0 L (v-1) \| RR1t q L v: 1 <= v -> Rnd (q+3) 2 L v (q+1) 2 L (v-1) \| RR2 q L v: 1 <= v -> Rnd (q+3) 1 L v q 0 (S L) (2*v-2) \| RO2 q L: Rnd (q+3) 2 L 0 (q+1) 0 (S L) (2^(S L)-1) \| RO1 q L: Rnd (q+3) 1 L 0 (q+1) 2 L (2^L-1) … +1 lines	L372	new
59	Lemma	`Rnd_tape`	Lemma Rnd_tape q r L v q' r' L' v' P l: Rnd q r L v q' r' L' v' -> v < 2^L -> okL P l -> RT (lev P l) q (zone r L v) -->+ RT (lev (P+2) l) q' (zone r' L' v').	L380	new
60	Lemma	`Rnd_valid`	Lemma Rnd_valid q r L v q' r' L' v': Rnd q r L v q' r' L' v' -> v < 2^L -> r < 3 -> v' < 2^L' /\ r' < 3.	L394	new
61	Lemma	`Rnd_exists`	Lemma Rnd_exists q r L v: 3 <= q -> r < 3 -> exists q' r' L' v', Rnd q r L v q' r' L' v'.	L400	new
62	Lemma	`okL_ge`	Lemma okL_ge P l: 1 <= P -> okL P l.	L414	new
63	Definition	`cap`	Definition cap (r L : nat) : nat := L + (if Nat.eqb r 1 then 1 else 0).	L419	new
64	Definition	`Kst`	Definition Kst (n r L : nat) : Prop := 2^(S (cap r L)) + 2 <= n.	L422	new
65	Definition	`Jst`	Definition Jst (n r : nat) : Prop := 3 <= n /\ (r <> 0%nat -> n mod 2 = 1%nat).	L425	new
66	Definition	`Mv`	Definition Mv (n r L v : nat) : nat := (n + (if Nat.eqb r 1 then v else 2v) + 2 2^(cap r L + 2)) mod 3.	L428	new
67	Definition	`Qv`	Definition Qv (P q r L v : nat) : nat := (Mv q r L v + 2*P) mod 3.	L432	new
68	Definition	`Ist`	Definition Ist (n r L v : nat) : Prop := r < 3 /\ v < 2^L /\ Kst n r L /\ Mv n r L v <> 0%nat /\ ~ (n = 6 /\ r = 1 /\ L = 0 /\ v = 0)%nat.	L434	new
69	Lemma	`init_I`	Lemma init_I: Ist 6 2 0 0.	L437	new
70	Lemma	`Rnd_sign`	Lemma Rnd_sign P q r L v q' r' L' v': Rnd q r L v q' r' L' v' -> Qv P q r L v = Qv (P+2) q' r' L' v'.	L440	new
71	Inductive	`EB`	Inductive EB : nat -> nat -> nat -> nat -> nat -> nat -> nat -> nat -> Prop := \| EB1z0 L v: EB 1 0 (S L) (2v) 2 2 L v \| EB1z1 L v: EB 1 0 (S L) (2v+1) 3 0 L v \| EB1o L v: EB 1 1 L v 2 0 L v \| EB1t L v: EB 1 2 L v 2 1 L v \| EB0 b L o: EB 0 0 (S b + S L) (2^(S b)(2o+1)) 2 0 (b + S L) (2^b - 1 + 2^(S b)*o) … +2 lines	L450	new
72	Lemma	`EB_tape`	Lemma EB_tape q r L v e r' L' v' p l: EB q r L v e r' L' v' -> RT (FR p l) q (zone r L v) -->+ RT l (S p + e) (zone r' L' v').	L459	new
73	Lemma	`EB_sign`	Lemma EB_sign q r L v e r' L' v' P: EB q r L v e r' L' v' -> (Mv (P + e) r' L' v' + Qv P q r L v) mod 3 = 0%nat.	L473	new
74	Lemma	`iter_FR0`	Lemma iter_FR0 k X: [1;0;0]^^k *> X = Nat.iter k (FR 0) X.	L486	new
75	Lemma	`PUSH_lev`	Lemma PUSH_lev k L o P l: okL P l -> RT (lev P l) 2 (zone 0 (k + S L) (2^k - 1 + 2^(S k)*o)) -->+ RT (Nat.iter k (FR 0) (lev (P+2) l)) 1 (zone 1 L o).	L492	new
76	Lemma	`inner1`	Lemma inner1 k L o X: RT (Nat.iter (S k) (FR 0) X) 1 (zone 1 L o) -->+ RT (Nat.iter k (FR 0) X) 3 (zone 0 L o).	L501	new
77	Definition	`safe`	Definition safe (c : Q * tape) (N : nat) : Prop := forall M, M <= N -> ~ halts_in tm c M.	L507	new
78	Lemma	`safe_mono`	Lemma safe_mono c N N': safe c N -> N' <= N -> safe c N'.	L509	new
79	Lemma	`safe_ev`	Lemma safe_ev c c' N: c -->* c' -> safe c' N -> safe c N.	L512	new
80	Lemma	`safe_prog`	Lemma safe_prog c c' N: c -->+ c' -> safe c' (N - 1) -> safe c N.	L520	new
81	Lemma	`safe_prog0`	Lemma safe_prog0 c c': c -->+ c' -> safe c 0.	L528	new
82	Lemma	`safe_RT0`	Lemma safe_RT0 l q Z: safe (RT l q Z) 0.	L534	new
83	Lemma	`phase`	Lemma phase (Inv : nat -> nat -> nat -> nat -> nat -> Prop): (forall j q r L v q' r' L' v', Rnd q r L v q' r' L' v' -> v < 2^L -> Inv j q r L v -> Inv (j+2) q' r' L' v') -> forall q j P l r L v, okL (P + j) l -> r < 3 -> v < 2^L -> Inv j q r L v -> exists j' q' r' L' v', q' <= 2 /\ r' < 3 /\ v' < 2^L' /\ Inv j' q' r' L' v' /\ j <= j' /\ (3 <= q -> j + 2 <= j') /\ … +1 lines	L543	new
84	Lemma	`cap0`	Lemma cap0 L: cap 0 L = L.	L567	new
85	Lemma	`cap1`	Lemma cap1 L: cap 1 L = S L.	L568	new
86	Lemma	`cap2`	Lemma cap2 L: cap 2 L = L.	L569	new
87	Lemma	`pow0`	Lemma pow0 L: L = 0%nat -> 2^L = 1%nat.	L573	new
88	Definition	`Kx`	Definition Kx (n r L v : nat) : Prop := Kst n r L /\ ~ (r = 2%nat /\ v = 2^L - 1 /\ n = 2^(S L) + 2) /\ ~ (n = 6%nat /\ r = 1%nat /\ L = 0%nat /\ v = 0%nat).	L577	new
89	Definition	`Pre`	Definition Pre (n r L v : nat) : Prop := Jst n r \/ Kx n r L v.	L581	new
90	Definition	`Saf`	Definition Saf (q r L v : nat) : Prop := match r with \| O => (L = 0%nat -> 3 <= q) /\ ~ (q = 2%nat /\ v = 2^L - 1) /\ (q = 0%nat -> v mod 2 = 0%nat) \| 1%nat => 3 <= q /\ (v = 0%nat -> (q <= 2^(S L) + 2 -> q mod 2 = 1%nat) /\ q <> 2^(S L) + 4) \| _ => (q <= 2v + 2 -> q mod 2 = 1%nat) /\ q <> 2v + 4 end.	L584	new
91	Definition	`KI`	Definition KI (j q r L v : nat) : Prop := match r with \| O => 2^L <= j + q /\ (2^(S L) <= j + 2v + 2 \/ 2^(S L) + 1 <= j + q) /\ (q = 0%nat -> v <> 0%nat) /\ (L = 0%nat -> 4 <= q) \| 1%nat => 2^(S (S L)) + 2 <= q /\ (v = 0%nat -> 2^(S L) + 5 <= q) \| _ => 2^(S L) + 2 <= j + q /\ 2v + 5 <= q … +1 lines	L592	new
92	Definition	`ZI`	Definition ZI (C q r L v : nat) : Prop := 1 <= C /\ match r with \| O => L <= S C /\ q + 2^(S (S L)) + C <= 2*v + L + 2^(S (S (S C))) + 1 /\ (q = 0%nat -> v = 0%nat -> L <= C) \| 1%nat => S (S L) <= C /\ q <= 2^(S (S L)) + 1 /\ 3 <= q … +2 lines	L601	new
93	Lemma	`Saf_step`	Lemma Saf_step q r L v q' r' L' v': Rnd q r L v q' r' L' v' -> v < 2^L -> Saf q r L v -> Saf q' r' L' v'.	L610	new
94	Lemma	`KI_step`	Lemma KI_step j q r L v q' r' L' v': Rnd q r L v q' r' L' v' -> v < 2^L -> KI j q r L v -> KI (j+2) q' r' L' v'.	L616	new
95	Lemma	`pow_mono`	Lemma pow_mono a b: a <= b -> 2^a <= 2^b.	L624	new
96	Lemma	`pow_lin`	Lemma pow_lin a: S a <= 2^a.	L627	new
97	Lemma	`ZI_step`	Lemma ZI_step C q r L v q' r' L' v': Rnd q r L v q' r' L' v' -> v < 2^L -> ZI C q r L v -> ZI C q' r' L' v'.	L630	new
98	Definition	`PI`	Definition PI (n r L v j q r' L' v' : nat) : Prop := j mod 2 = 0%nat /\ Qv j q r' L' v' = Mv n r L v /\ (r' = 1%nat -> j = 0%nat) /\ (r' = 2%nat -> L' = 0%nat -> j <= 2) /\ Saf q r' L' v' /\ (Kx n r L v -> KI j q r' L' v') /\ (Jst n r -> ~ Kst n r L -> ZI (S (cap r L)) q r' L' v').	L647	new
99	Lemma	`PI_step`	Lemma PI_step n r L v j q r1 L1 v1 q' r' L' v': Rnd q r1 L1 v1 q' r' L' v' -> v1 < 2^L1 -> PI n r L v j q r1 L1 v1 -> PI n r L v (j+2) q' r' L' v'.	L653	new
100	Lemma	`Mv_lt3`	Lemma Mv_lt3 n r L v: Mv n r L v < 3.	L668	new
101	Lemma	`Qv0`	Lemma Qv0 q r L v: Qv 0 q r L v = Mv q r L v.	L671	new
102	Lemma	`Pre_n3`	Lemma Pre_n3 n r L v: Pre n r L v -> 3 <= n.	L674	new
103	Lemma	`Saf_start`	Lemma Saf_start n r L v: r < 3 -> v < 2^L -> Pre n r L v -> Saf n r L v.	L679	new
104	Lemma	`KI_start`	Lemma KI_start n r L v: r < 3 -> v < 2^L -> Kx n r L v -> KI 0 n r L v.	L689	new
105	Lemma	`ZI_start`	Lemma ZI_start n r L v: r < 3 -> v < 2^L -> Jst n r -> ~ Kst n r L -> ZI (S (cap r L)) n r L v.	L697	new
106	Lemma	`PI_start`	Lemma PI_start n r L v: r < 3 -> v < 2^L -> Pre n r L v -> PI n r L v 0 n r L v.	L704	new
107	Definition	`Post`	Definition Post (n r L v n' r' L' v' : nat) : Prop := r' < 3 /\ v' < 2^L' /\ (Jst n r -> Jst (S n') r') /\ (Kx n r L v -> Kst n' r' L') /\ (Jst n r -> ~ Kst n r L -> Kst (S n') r' L' \/ cap r' L' <= S (cap r L)) /\ (Mv n' r' L' v' + Mv n r L v) mod 3 = 0%nat /\ … +1 lines	L714	new
108	Definition	`U`	Definition U (N : nat) : Prop := forall P l n r L v, okL P l -> r < 3 -> v < 2^L -> Pre n r L v -> (forall n' r' L' v', Post n r L v n' r' L' v' -> safe (RT l (P + n') (zone r' L' v')) (N - 1)) -> safe (RT (lev P l) n (zone r L v)) N.	L722	new
109	Lemma	`lowones`	Lemma lowones L: forall v, v < 2^L -> v <> 2^L - 1 -> exists k L' o, L = k + S L' /\ v = 2^k - 1 + 2^(S k) * o /\ o < 2^L'.	L729	new
110	Lemma	`bite_shape`	Lemma bite_shape j qb rb Lb vb: qb <= 2 -> rb < 3 -> vb < 2^Lb -> Saf qb rb Lb vb -> 2 <= j -> (rb = 1%nat -> j = 0%nat) -> (exists e r' L' v', EB qb rb Lb vb e r' L' v') \/ (qb = 2%nat /\ rb = 0%nat /\ exists k L' o, Lb = k + S L' /\ vb = 2^k - 1 + 2^(S k) * o /\ o < 2^L').	L742	new
111	Lemma	`EB_valid`	Lemma EB_valid q r L v e r' L' v': EB q r L v e r' L' v' -> v < 2^L -> r' < 3 /\ v' < 2^L'.	L766	new
112	Lemma	`EB_lev`	Lemma EB_lev q r L v e r' L' v' P l: 1 <= P -> EB q r L v e r' L' v' -> RT (lev P l) q (zone r L v) -->+ RT l (P + e) (zone r' L' v').	L779	new
113	Lemma	`Kst_mono`	Lemma Kst_mono n n' r L: Kst n r L -> n <= n' -> Kst n' r L.	L783	new
114	Lemma	`ending`	Lemma ending n r L v j qb rb Lb vb e r' L' v': EB qb rb Lb vb e r' L' v' -> PI n r L v j qb rb Lb vb -> 2 <= j -> vb < 2^Lb -> Post n r L v (j + e) r' L' v'.	L787	new
115	Lemma	`ending_B2`	Lemma ending_B2 n r L v j L' o: PI n r L v j 2 0 (0 + S L') (2^0 - 1 + 2^1 * o) -> 2 <= j -> o < 2^L' -> Post n r L v (j + 4) 0 L' o.	L808	new
116	Definition	`Budget`	Definition Budget (n r L C : nat) : Prop := Kst n r L \/ cap r L <= C.	L828	new
117	Definition	`SR`	Definition SR (j a b : nat) : Prop := (j mod 2 = 0%nat -> b = a) /\ (j mod 2 = 1%nat -> (a + b + 2) mod 3 = 0%nat).	L831	new
118	Lemma	`JK`	Lemma JK n r L v: Jst n r -> Kst n r L -> Kx n r L v.	L834	new
119	Lemma	`Budget_step`	Lemma Budget_step n r L v C n' r' L' v': Jst n r -> Budget n r L C -> Post n r L v n' r' L' v' -> Budget (S n') r' L' (S C).	L841	new
120	Lemma	`Mv_shift`	Lemma Mv_shift a n r L v: Mv (a + n) r L v = (Mv n r L v + a) mod 3.	L851	new
121	Lemma	`SR_step`	Lemma SR_step j n r L v n' r' L' v' b: b < 3 -> Post n r L v n' r' L' v' -> SR j (Mv (S n') r' L' v') b -> SR (S j) (Mv n r L v) b.	L854	new
122	Lemma	`pow2_mod3`	Lemma pow2_mod3 k: exists x, 2^k = 3*x + 1 + k mod 2.	L863	new
123	Lemma	`QvN`	Lemma QvN j k L o: (k mod 2 = 0%nat -> Qv j 2 0 (S k + S L) (2^(S k) - 1 + 2^(S (S k)) * o) = (Mv 3 0 L o + 1 + 2j) mod 3) /\ (k mod 2 = 1%nat -> Qv j 2 0 (S k + S L) (2^(S k) - 1 + 2^(S (S k)) o) = (2 * (Mv 3 0 L o + 1) + 2*j) mod 3).	L870	new
124	Lemma	`compose`	Lemma compose n r L v j k L' o n1 r1 L1 v1 n3 r3 L3 v3: PI n r L v j 2 0 (S k + S L') (2^(S k) - 1 + 2^(S (S k)) * o) -> 2 <= j -> Jst n1 r1 -> Budget n1 r1 L1 (L' + k) -> SR k (Mv 3 0 L' o) (Mv n1 r1 L1 v1) -> Post n1 r1 L1 v1 n3 r3 L3 v3 -> Post n r L v (j + 2 + n3) r3 L3 v3.	L881	new
125	Lemma	`STK`	Lemma STK: forall j B, (forall B', B' <= B -> U B') -> forall n r L v C X, Jst n r -> Budget n r L C -> r < 3 -> v < 2^L -> (forall n1 r1 L1 v1, Jst n1 r1 -> Budget n1 r1 L1 (C + j) -> r1 < 3 -> v1 < 2^L1 -> SR j (Mv n r L v) (Mv n1 r1 L1 v1) -> safe (RT X n1 (zone r1 L1 v1)) (B - j)) -> safe (RT (Nat.iter j (FR 0) X) n (zone r L v)) B.	L911	new
126	Lemma	`U_all`	Lemma U_all: forall N, U N.	L938	new
127	Lemma	`Ist_Kx`	Lemma Ist_Kx n r L v: Ist n r L v -> Kx n r L v.	L988	new
128	Lemma	`cycles`	Lemma cycles N: forall n r L v, Ist n r L v -> safe (RT (const 0) n (zone r L v)) N.	L995	new
129	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L1008	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 92: 1. Rule table (busycoq comment-block style)

This block is a compact reference. §2 defines every symbol in it, and §3 derives every rule.

1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB            (only F0 is undefined)

lattice(w) = { j = w-1-3i : i >= 1, j >= 2 };   bit b of v (b = 0, 1, ...) sits on the b-th smallest lattice cell
enc(w,v)   = 1^w with 0 on the lattice cells of the set bits of v;   L(w) = #lattice(w) = floor(w/3) - 1
cap(w)     = L(w) + [w = 1 mod 3]                    allset(u) = enc(u, 2^L(u) - 1)
R(p,q,Z)   = 0^inf (10)^p 1 C> 0 0 (10)^q Z 0^inf  (p >= 0);   R(-1,q,Z) = 0^inf C> 0 0 (10)^q Z 0^inf  (cycle start)
             (Z never starts with 10: the bell takes every leading 10 pair; Z has no trailing 0)
R_L(p,q,Z) = L 0 0 (10)^p 1 C> 0 0 (10)^q Z 0^inf     (p >= 0, any left context L;  R = R_(0^inf))
R_L(-1,q,Z) = L C> 0 0 (10)^q Z 0^inf                  (only a name for the tape a level pops to)
             no rule is applied to R_L(-1, ..) unless L = 0^inf;  if L = L' 0 0 1 it is the tape R_L'(0, q, Z)

low-level rules (each run reads only the cells shown)
BR   B> 1^k              --> 1^k B>                                    k
S    (01)^k <C           --> <C (01)^k                                 2k       C1 D0
T    (111)^j <C          --> <C (011)^j                                5j       C1 D1 A1 C1 D0
W    C> 00 101010        --> 0101 0011 B>                              10
PS   011 B> (10)^b       --> 0 (10)^b 11 B>                            12b
ZA   00 (10)^a 11 B> 1^f 0  --> C> 0 (01)^(a+1) (011)^j 1              f = 2 mod 3, j = (f+1)/3
                            --> C> 0 (01)^(a+2) 111 (011)^(j-2) 1      f = 1 mod 3, f >= 4, j = (f+2)/3
                            --> C> 0 (01)^a 011111 (011)^(j-1) 1       f = 0 mod 3, f >= 3, j = f/3
PUSH C> 00 1010 (110)^k 111  --> 0101 (001)^k C> 00 101                14+3k   (k >= 0)
B1   00 (10)^p 1 C> 00 10 11 --> C> 00 (10)^(p+3) 1                    2p+15
B0   00 (10)^p 1 C> 00 1^f 0 --> C> 00 (10)^(p+2) 1 (011)^j 1          f = 2 mod 3, j = (f-2)/3
B0c  00 (10)^p 1 C> 00 1^w 0 --> C> 00 (10)^(p+2) 11 allset(w-2)       w = 0 mod 3, w >= 6
     00 (10)^p 1 C> 00 111 00 --> C> 00 (10)^(p+1) 111111              2p+31
Ht   C> 00 101 000       --> 0101 001 F> 0  (F0 undefined)             9

macro rules (Z = enc(w,v), f = position of the first 0 of Z, or w if v = 0; p >= 0 and any left context L;
             the five rounds also hold at p = -1 with L = 0^inf, where they give R(1, ..), §3.2)
R1   R_L(p,q,Z) --> R_L(p+2, q-2, enc(w, v-1))              q >= 3, v >= 1, w = 0,2 mod 3
R2   R_L(p,q,Z) --> R_L(p+2, q-3, enc(w+2, 2v-2))           q >= 3, v >= 1, w = 1 mod 3
O2   R_L(p,q,Z) --> R_L(p+2, q-2, enc(w+1, 2^(L+1)-1))      q >= 3, v = 0,  w = 2 mod 3
O1   R_L(p,q,Z) --> R_L(p+2, q-2, enc(w+1, 2^L-1))          q >= 3, v = 0,  w = 1 mod 3, w >= 4
O0   R_L(p,q,Z) --> R_L(p+2, q-3, enc(w+3, 2^(L+1)-2))      q >= 3, v = 0,  w = 0 mod 3
     (all five = W, PS^(q-3), ZA; 10 + 12(q-3) + f + 1 + 5j + {2(q-2) | 5+2(q-1) | 11+2(q-3)} steps)
B2   R_L(p,2,Z) --> R_L(p+2, 1, Z[2:])  re-parsed           Z starts 111, w >= 6    (PUSH k=0)
                (w = 1, bit 0 set: R_L(p+2, 2, enc(w-4, (v-1)/2)); never occurs, Lemma P)
N    R_L(p,2,(110)^k Y) --> R_L(p+2, G^(k-1)(3, Y[3:]))     k >= 1, Y starts 111, |Y| >= 6
H    R_L(p,2,(110)^k 111) --> halts                         k >= 1  (PUSH k, then Ht: 23+3k steps)
                (also k = 0, Z = 111: PUSH 0, then Ht; never occurs, since a bite zone has width >= 5, P1)
B1   R_L(p,1,Z) --> R_L(-1, p+3, Z[1:])  re-parsed          p >= 0, Z starts 11
B0   R_L(p,0,Z) --> R_L(-1, p+3, enc(w-3, (v-2)/2))         w = 0 mod 3, v >= 1 even
                --> R_L(-1, p+2, enc(w-1, (v-1)/2))         w = 0 mod 3, v odd      (never occurs, Lemma P)
B0c  R_L(p,0,1^w) --> R_L(-1, p+2, enc(w, 2^L-2))           w = 0 mod 3, w >= 6;   1^3 --> R_L(-1,p+1,1^6)
     ending bites (B1, B0, B0c) need the 0 0 left of (10)^p 1 and read nothing left of it

levels:  t = (n,w,v);  F(t) = the cycle start R(-1, F t) reached from R(-1, n, enc(w,v));
         the run from R_L(p0, n, enc(w,v)), p0 >= 0, n >= 3, pops at R_L(-1, F(t) + (p0+1, 0, 0))  (L never read);
         G(t) = F(t) + (1,0,0) = where a level started at R_L(0, n, enc(w,v)) pops
stack:   N = PUSH k, then the innermost level R_L1(0,1,Y[2:]) --B1--> (3, Y[3:]); level i pops into
         level i+1 (R_L(-1, ..) of level i = R_L'(0, ..) of level i+1); level k pops into R(p+2, ..)

invariant:  d(t) = n - 2^(cap(w)+1);  M(t) = n + 2v - 2^(cap+2) (w = 0,2) | n + v - 2^(cap+2) (w = 1)  (mod 3)
   K = { w >= 3, d >= 2 };   I = { t in K : M(t) != 0 } minus (6,4,0)
   J = { w >= 3, n >= 3, n odd if w = 1,2 mod 3 }               (inner phase starts)
   H* = { w = 2: n = 2v+4 } u { w = 1: v = 0, n = 2^(L+1)+4 }    (the phase starts that halt)
   s in I  ->  the cycle from s never halts, and if it ends, F(s) is in I   (M(F s) = -M(s))
start:  c0 -->(327) R(-1, 6, 11111) = (6,5,0),  d = 4, M = 2:  in I

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

1 machines, 1 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
W5-4 kill 31	`1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB`	✓Killed: never halts	this kill
Named in a file but not linked (not counted as family)
W4-2 kill 18	`1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF`	✓Killed: never halts	named in W5-4's proof.md; named in W5-4's notes.md · review · mechanism

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

✓
Machine string exact
the .v literal == holdout list line 558 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 4.57 s
✓
.v hash matches the checked hash
.v = checked sha256 f61649bdc6b6…; submission/ copy = checked sha256 f61649bdc6b6…
✓
No repo-local paths in the .v
comments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own verify/X.v is fine: none in the .v or the submission/ copy
✓
Public write-up is clean
tools/writeup_lint.py on submission/proof.md: 0 error(s)
○
proof.md reviewed by Dennis (Checkpoint B)
no Checkpoint B note from Dennis found
- proof.md L634: ## 12. Checkpoint B (Dennis)
- proof.md L651: - Open: Checkpoint B; a skeptic pass by a second agent; the Rocq build (§9).
○
Family posted together?
no other kill in the family

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 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB

Files

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

name	size	changed
notes.md ↓	36 KB	2026-10-13 13:16
proof.md ↓	55 KB	2026-10-13 11:53
how_proved.md ↓	1.6 KB	2026-10-14 10:51
status.json ↓	5.4 KB	2026-10-16 10:28
observe.json ↓	15 KB	2026-10-13 02:13
deepen.json ↓	3.7 KB	2026-10-13 09:30
1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v ↓	45 KB	2026-10-13 12:58
decisions/	1 item	2026-10-13 09:25
img/	7 items	2026-10-13 01:15
rocq/	3 items	2026-10-13 12:59
scripts/	17 items	2026-10-13 09:23
submission/	6 items	2026-10-15 15:49
work/	43 items	2026-10-13 11:33
check_proof.py ↓	43 KB	2026-10-13 11:22

status.json in full

{
 "tm": "1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-13",
 "reason": "check_kill PASS, independently re-verified",
 "label": "W5-4",
 "confidence": "high",
 "template": "verify/BECv5.v, Module TM1 (architecture: one es lemma per low-level rule, one counter-form lemma per macro rule; via our W4-2 kill)",
 "siblings": [],
 "family_note": "Canon over all 6 starts (renaming + mirror): only start A is on the 778/740 lists (starts B..F halt within 44 steps). No 740 entry within 2 transitions of any renamed/mirrored form. Eqv group in 2026-10-07_eqv_1590.txt is a singleton.",
 "checks": {
  "byte_exact": "data/holdouts/BB6_holdouts_740.txt line 525 (holdouts.py contains: exit 0)",
  "claims": "none (sheet results.csv row 1044: class only; no data/discord hit)",
  "upstream": "holdouts.py solved: absent from verify/ (no byte-exact, notation-only or equivalent entry)",
  "rules": "scripts/validate_rules.py seed 3, 150 per kind: all pass; B0c 180/180; nested B2'' model 252/252 + 4 halts (Y=111) vs TM brute force",
  "coverage": "closed rules + nested model on work/direct_all_events_1e9.txt: 204,951/204,953 exact (2 tiny events before step 30)",
  "abstract_vs_direct": "scripts/absim2.py (no TM simulation) = work/cycle_starts_1e11.txt at 4,197/4,197 cycle starts",
  "transients": "scripts/transient.py from T(L), L = 10..38 closed rules and 10..56 with TM fallback: all LOCK, no halt",
  "invariant": "scripts/invariant.py: Lemma K + M, 0 failures on w 3..31 n < 2^(cap+3) (6,810,622 states), w 3..16 n < 2^(cap+10) (1,132,222) and w 3..12 n < 2^(cap+14) (2,424,478); work/invariant_*.txt",
  "sign_law": "scripts/signlaw.py: TM level 7,977/7,977 random family configurations (seeds 1, 2); rule level 7.3M applications, 0 failures (work/signlaw_seed2.txt)",
  "F_vs_tm": "scripts/check_F_vs_tm.py: closed-rule cycle map = direct TM run on 300/300 random states of I (n <= 700)",
  "entry": "blank run: cycle start (6,5,0) at step 327 is in I, and so are all 304,194 later cycle starts checked (direct run to 1e11, then 300,000 closed-rule cycles)",
  "continuation_lemmas": "scripts/contlemmas.py kwin: A1 (p_c >= 2^L_c - 3, min slack 0), composite form F(s) = (p_c+2) + G^k(t_2) and A2 on 533,148 continuation cycles (w <= 27) + 151,880 (w <= 15, n < 2^(cap+10)), min d' = 5",
  "inner_levels": "scripts/contlemmas.py jwin: Lemma J (G maps J to J, no halt, no gap) on 1,920,333 + 479,621 states; Z' on 239,786 + 906; K-persistence on 1,680,547 + 478,715",
  "halting_set": "scripts/contlemmas.py hstar: the cycle from (n, w, v), w >= 3, n >= 3, halts iff it is in H* on 610,121 (w <= 24) + 606,121 (w <= 12, n < 2^(cap+12)) states",
  "nested_gform": "scripts/contlemmas.py gform: nested bite = k - 1 G-steps from (3, Z >> (k+1)), 20,000/20,000 vs scripts/nested.py",
  "random_large": "scripts/contlemmas.py random seed 2: 200,000 states, w <= 75, n up to 2^(cap+6): 0 failures (Lemma K, A1, CF, A2, J, Z', K-persistence)",
  "tm_level_shift": "scripts/contlemmas.py tm seeds 1, 2: 500 random states (151 J with d <= 1, 349 K): TM run from R(0, n, Z) pops at G(t) and from R(-1, n, Z) at F(t), 500/500 both",
  "check_proof": "check_proof.py (self-contained TM simulator + abstract model), after skeptic round 1: default seed 1 81/81 PASS in 107s (work/check_proof_seed1.log); quick seeds 1, 2 80/80 (work/check_proof_quick_seed*.log); --full seed 1 partial: T..CH 74/74 PASS (CH w <= 27, 1,527,624 K states) and INV window w <= 24, n < 2^(cap+4) PASS (610,121 states, 132,766 continuation cycles), work/check_proof_full_seed1.log + work/check_proof_full_seed1_INV.log; the second --full INV window (w <= 14, n < 2^(cap+11)), the random states and Z were stopped unfinished after 35 min (overflow_count/outer_trace step R1 rounds one at a time). New checks: MAC.round at p = -1 (450 runs, any L), SH with p0 in 0..8 (SL1 on the TM), ABS bite-zone widths, CH parts of NB and the w = 1 reductions, INV CF-J (own-frame composite form), NB as n(F s) >= n - m."
 },
 "funded": {
  "option": "proof",
  "date": "2026-10-13"
 },
 "outcome": "killed_nonhalt",
 "skeptic": [
  {
   "round": 1,
   "date": "2026-10-13",
   "verdict": "sound",
   "gaps": 5,
   "severity": "all minor",
   "result": "all fixed; proof.md Review log; no lemma changed"
  }
 ],
 "kill": {
  "file": "1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB.v",
  "sha256": "f61649bdc6b6e97b170ccd8b89a210e50f4714d06d97a352c620e62d712574fc",
  "lines": 1039,
  "check_kill": "PASS (fresh run 2026-10-13T20:03:57Z: compile 34.7 s native, coqchk pass 4.6 s, 0 assumptions; also rocq/check_kill_round2.log and the independent auditor run 2026-10-13T20:01:12Z, same sha256)",
  "route": "bounded induction on steps (U_all, CPS form) with phase invariants Saf/KI/ZI; stack of frames FR; (U5) in place of NB",
  "submission": "submission/",
  "discord": "submission/discord.md, not posted (fill in <LINK>; search #bb6 first)"
 },
 "next": "post the Discord draft (submission/discord.md, not posted; fill in <LINK>, search #bb6 first); add to the next upstream PR batch",
 "pr": "https://github.com/ccz181078/busycoq/pull/28",
 "pr_state": "merged",
 "pr_file": "verify/M_1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_HHH0RB.v",
 "pr_opened": "2026-10-15T22:48:46Z",
 "pr_comments": 0,
 "pr_head_sha": "051e8bb8e95d65bd1b0d905760f7e66e6cbf7a31",
 "posted": "2026-10-15 (Discord; user confirmed sent)",
 "pr_merged_at": "2026-10-16T07:09:19Z",
 "pr_merged_by": "ccz181078"
}

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

3 contract warnings

rank: missing
diagrams[2].window: not "cells A..B, 1 px = k cells"
template file not in the pinned tree: machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v

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