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

`1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB`

#8local proof 13Kill claimedSync bouncer counterbbchallenge ↗Explorer

How we proved it never halts

A timing window that every route returns to

Right of the head is a binary counter with spread-out digits: a seven-cell mark (0110001 for a 1, 0010001 for a 0) followed by a gap of repeated 100s. Left of it is padding, and at the far right a tail: a fixed gadget holding 15 bits, plus a slowly growing end. Each bounce off the left end adds 1 to the counter and lengthens the padding.

At an overflow the tail answers in one of two ways. Either the counter just wraps to zero, or the left part of the tape freezes into a "wall", which the machine eats two counts at a time in a long pause that rebuilds the gaps. The key idea: the proof never predicts the tail's 15 bits, only its front two. At each overflow those two step through a short cycle, 10, 01, 11, 00 and back to 10, and the quiet wrap can happen only at 11, where the proof simply allows either answer.

Why that settles it: the one moment no rule covers is a pause whose wall runs out exactly as the counter overflows. At each overflow outside a pause, the proof measures how far the padding's length is from a length set by the counter. While that surplus stays in a window set by the counter's size and the two front bits, only four sequences of events can follow. Each shifts or flips the surplus by an exact amount, avoids the uncovered moment, and lands back in the window. The run enters the window at step 92,299, so the missing instruction is never used.

The Rocq proof (checked against busycoq) replays the first 92,299 steps, then checks the tape moves by running them, the counting by induction, the tail's answers through a verified model of the head's return trip, and the window by arithmetic.

#13local proof number

1,327lines of Rocq

10 sto compile

6/6automatic checks

Overview

In one sentence

Bouncer carrying a binary counter whose digits sit in its body; each overflow inserts a new digit ~4x farther out

Submitted mechanism A spread binary counter inside a bouncer. Right of the lead (001)^a 00, the tape is a counter in the tokens 00, 01, Z = 100: each digit is b Z 01 Z^g (bit b, gap g), LSB first. Every bounce off the left end adds 1 to the counter and 1 to a. (submission/README.md, Mechanism)

Upstream: Kill claimed · PR #26merged 2026-10-16 07:08 UTC by ccz181078 · PR_SBC.v · TM1 · on Submissions →
Rocq proof: check_kill PASS · first Oct 10 16:07
1,327 lines · 74 KB .v · compile 10.3 s · coqchk pass · 0 axioms · PASS Oct 10 16:07
· the .v file
Automatic review: 6 of 6 checks passtemplate: verify/CounterClass3v2.v Module TM1 (adapted from) · details in Proof →
Class: Sync bouncer counterours: Sync bouncer counter (sheet) · ours adds: spread-digit variant (binary counter whose digits sit inside the bouncer body) · med confidence
On the list: not on BB6_holdouts_663.txt (line 410 of the previous list) · historical 740 line 410
#8eqv ×1sim 1e15UBRRBA

Your calls on file 1

2026-10-10 · deepen3_oracle_free: #8's left counter and overflow pause are fully ruled. Only the right-end tail, which decides NO / emit / SILENT at each overflow, lacks a general rule. Fund a third deepen round aimed at a tail-independent proof, or park #8? (Dennis: go with all recommendations (2026-10-10))

Mechanism

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

How it works: 3 notes

Bouncer: the head shuttles from the left edge into the tape; each trip adds one (010) block to the left lead a.
The (100) body holds 7-cell digits 0b10001; each trip is a binary +1 (run to the first 0-digit, set it, clear the 1s).
Right end frozen. At overflow (all 1s) a long pause cuts a new lowest digit from the lead, ~4x farther out.

Figures for Checkpoint A

Fig 1 · One row per +1: six bit columnsQ1
One row per +1. Count the rows between colour changes in each of the six bit columns, left to right.

Fig 2 · Eight +1s up close, every stepQ2
Eight +1s, every step. Note where each right sweep turns back, against the bit cells (21, 43, 62, 78).

Fig 3 · Real run from blank, right edge pinnedQ3 viewer ↗
Real run from blank, right edge pinned. Watch for new thin vertical lines and where each one appears.

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

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

rule	from ⟶ to	cases	steps	checked
Inc (one bounce = binary +1)	0^∞ <A (010)^a 00 b0 10001 (100)^g1 0 b1 10001 ... (100)^gk 0 bk 10001 R 0^∞ ⟶ same with a+1 and bits b0..bk + 1 (b0..b(j-1): 1->0, bj: 0->1)	j = lowest 0 bit; needs some bi = 0 (else Ovf). Holds for every a>=1, gi>=1, 1-6 digits	6a + 6(g1+...+gj) + 24j + 9	✓400/400
Ovf-insert (overflow pause, long lead)	0^∞ <A (010)^a 00 1 10001 (100)^g1 0 1 10001 (100)^g2 0 1 10001 (100)^g3 R* 0^∞ ⟶ 0^∞ <A (010)^a-g'-5 00 0 10001 (100)^g' [old digits, bits reloaded] (100)^g1 ... (100)^g3 R' 0^∞	a >= g'+6, g' = 2044 - 2g1 - 4g2 - 8g3 (k=3; general 2^(2k+5)-4-sum 2^i g_i matches all 4 real inserts). R* = real R at step 114113163	—	✓30/30
Ovf-short (overflow pause, short lead)	same as Ovf-insert ⟶ 0^∞ <A (010)^a-1 [same digits and gaps, counter reloaded] R' 0^∞	a < g'+6: no insert, gaps unchanged; reloaded counter value rises by 2 per +1 in a (checked a = 100..115)	—	✓12/12

Compressed historythe tape as 0^∞ <A (010)^a 00 b0 10001 (100)^g1 0 b1 10001 ... (100)^gk 0 bk 10001 R 0^∞ at 25 moments: where the rules are read off

0^∞ <A (010)^a 00 b0 10001 (100)^g1 0 b1 10001 ... (100)^gk 0 bk 10001 R 0^∞

step	`a (lead)`	`b0..bk (LSB first)`	`g1..gk (gaps, LSB side first)`	`R (packed high digits)`
466	6	1	-	1 digits/16 cells
3,669	14	1	-	9 digits/99 cells
8,109	14	1	-	12 digits/127 cells
17,206	44	1	-	12 digits/132 cells
36,124	11	1	28	13 digits/142 cells
36,205	12	11	28	13 digits/142 cells
60,574	75	1	28	13 digits/142 cells
92,299	120	11	28	13 digits/142 cells
236,797	47	10	6,828	14 digits/152 cells
237,094	48	110	6,828	14 digits/152 cells
500,668	264	110	6,828	14 digits/152 cells
1,006,516	468	111	6,828	14 digits/152 cells
2,847,332	203	100	2,606,828	15 digits/162 cells
2,848,565	204	1,100	2,606,828	15 digits/162 cells
2,861,897	210	1,001	2,606,828	15 digits/162 cells
10,002,518	1,429	11	2,606,828	15 digits/162 cells
30,013,827	2,874	1,000	2,606,828	15 digits/162 cells
60,004,098	4,223	110	2,606,828	15 digits/162 cells
114,077,490	5,943	111	2,606,828	15 digits/162 cells
114,113,163	5,944	1,111	2,606,828	15 digits/162 cells
555,048,797	799	111,010	7.4·10¹⁵	17 digits/182 cells
555,053,606	800	1,111,010	7.4·10¹⁵	17 digits/182 cells
700,022,195	6,047	111,010	7.4·10¹⁵	17 digits/182 cells
850,053,545	8,931	100,111	7.4·10¹⁵	17 digits/182 cells
999,986,591	11,157	10,010	7.4·10¹⁵	17 digits/182 cells

a (lead)last 11,157

b0..bk (LSB first)last 10,010

g1..gk (gaps, LSB side first)last 7.4·10¹⁵

R (packed high digits)last 17 digits/182 cells

not plottable

Template comparisonSBCv2_6x2_solved.v tm108: does not apply · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	0LF
B	0RC	---
C	1RD	0RA
D	1LE	0RC
E	0LA	0LE
F	1LE	1LB

differs from the template

file: SBCv2_6x2_solved.v (Section template SBCv2.v)
module: tm108 / nonhalt108 (line 1195)
machine: 1LB0RE_0LC---_1LD0LA_1RA0LC_1RF1RB_0RA0RF (11 transitions apart)
diff: mirror + relabel E<->F gives 1RB0LF_0RC---_1RD0RA_1LA0RC_0LA0LE_1LE1LB; only D0 differs: ours 1LE, template 1LA
note: Template LInc/RInc0, mirrored: 10/10 on the template, 0/10 on ours. Same idea (binary counter + unary sync), but our digits are spread through the unary body, not packed in a 4-cell-digit counter.

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

Family proof in the SBCv2 spirit but with new shapes: (1) Inc as an ind-lemma over a 'spread counter' (digits 0b10001 between (100)^g gaps; shift rules over (100)^g via es/sideRLs); (2) map the overflow pause into exact sub-rules (insert / short-lead / R growth), not yet done; (3) multistep_nonhalt + progress_nonhalt_cond with an invariant on (a, k, gaps, counter value), like SBCv2's P(k,n).

▲Overflow pause internals are unmapped: R growth and multi-insert pauses (step 1.1e8 inserted 1028, 4097 and 7). They are most of the proof.
▲Size: nested counters plus an arithmetic invariant; expect 30-80 KB, well over the 15 KB target.
▲Only 4 real overflows exist in 1e10 steps (the next is far beyond reach), so the long-term rules rest on synthetic-config probes.

Stats & provenance10¹⁰ steps simulated · 181,589 cells · the status in full · files

simulated: 10¹⁰ steps
tape: 181,589 cells · 60,536 nonzeros
growth: span ~ t^0.5 (17.9k cells at 1e8, 50.2k at 1e9, 181.6k at 1e10); right edge fixed at 11 since step 1527
status now: check_kill PASS, independently re-verified (status.json, 2026-10-10)
observer's note: Mechanism found and core rules validated (Inc 400/400, overflow branches 30/30 and 12/12); arithmetic is linear, not Collatz-like; sheet has no notes or claims; on mxdys's UBRRBA_TODO list (Dennis: fair game).
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v

Proof & checks

6/6 automatic checks pass

Kill 13 · Sync bouncer counter · the kill file 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v: 1327 lines, 183 items · the package submission/

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

1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB

vs holdout list

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

Theorem

✓ Lemma nonhalt : ~ halts tm c0. L1284

check_kill

✓ PASS · 17/17 checks pass · compile 10.3 s · coqchk pass (3.19 s) · assumptions: 0 (closed) · 2026-10-10 23:07:05 UTC · submission/check_kill.txt

Checked .v

sha256 0ddf748799bcd23d…

✓	1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v	`0ddf748799bcd23d…` = checked
✓	submission/1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v	`0ddf748799bcd23d…` = checked

Status

✓Killed: never halts updated 2026-10-10

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

All 17 check_kill checks with their one-line results

✓	`args`	6x2 machine, framework module Individual62, mode nonhalt
✓	`input`	75561 bytes, 1327 lines, 1613 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 40: TM_from_str "1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB" == <tm> (41 bytes)
✓	`theorem_text`	line 1284: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 ([local working file]
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 10.3s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB") 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 (3.2s); 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/CounterClass3v2.v Module TM1 · detected from 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v line 10

3%of our lines identical to the template

1changed lines

1148added lines (ours only)

870template lines dropped

1 / 1 / 181items identical / adapted / new

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

Adapted from busycoq's verify/CounterClass3v2.v, Module TM1 (1RB0LC_0LC1RE_1LD1LC_1LA1RD_---1RF_0RA0RF), a hand-written multi-level counter proof. The transition tables are unrelated, so the file follows TM1's architecture, not its lemmas.

Kept: es window lemmas and shift rules, a carry lemma by induction on the carry depth (TM1's E_stmt/E_all), macro lemmas chained with follow, and multistep_nonhalt.
Changed: TM1 closes by strong induction over a trajectory family (Traj) with progress_nonhalt_simple. Here the macro state is (a, G, r1, tail), closed by the interval invariant with progress_nonhalt_cond.
New: the token layer, the retf transducer for the overflow and the tail, one IR shape KP for normal and pause mode, and the zone-rebuild induction Zones, whose no-overflow condition is stated on the final value only.

The file has 1,327 lines and imports only Individual62 from busycoq.

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

3% identical · 1 changed · 1148 added

template 903 lines

4% kept verbatim · 870 not in ours

our items 183

1 identical · 1 adapted · 181 new · 190 template-only

identicalchanged / adaptedours only (new)template only

Template part: lines 4–7 (shared header, before the first Module) + 9–985 (body of Module TM1; the Module/End lines left out). Ours: lines 33–1327 (header comment 1–32 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: lpow_snoc, lpow_snoc', lpow_app, lpow_cons_r, lpow_mul_S, sweepC, sweepD, sweepF, E_stmt, E0, Climb_of_E, X1_of_E, Climbs_of_E, E_all, Climb, Climbs, X1, FailStep, lpow_shift_str, FailChain', G_shift, FailChain, ML1, MLs, Mac_E, Mac_Fail, Mac_Climb, Mac_ML, Fail1, A4, GenStart, H, maff, mak, maadd, masub, mamul, madiv3, maeq, mage …

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

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

template		ours
4	From Coq Require Import Lia PeanoNat String ZArith List.
		34	From BusyCoq Require Import Individual62.
5	From BusyCoq Require Import Individual62 SimplTape.
		35	Require Import Lia.
6	Set Default Goal Selector "!".
		36	Require Import String.
		37	Require Import List.
		38	Require Import Arith.
9	Definition tm := Eval compute in (TM_from_str "1RB0LC_0LC1RE_1LD1LC_1LA1RD_---1RF_0RA0RF").	40	Definition tm := Eval compute in (TM_from_str "1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB").
11	Notation "c --> c'" := (c -[ tm ]-> c') (at level 40).	42	Notation "c --> c'" := (c -[ tm ]-> c') (at level 40).
12	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).	43	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
13	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).	44	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
15	( Tape algebra *)
		46	Open Scope list.
17	Lemma lpow_snoc : forall (s : Sym) n (l : side),
		48	( Tokens *)
18	l << s <* [s]^^n = l <* [s]^^(S n).
		49	Inductive tok := T0 \| T1 \| TZ.
		50	Definition tokw (t : tok) : list Sym :=
		51	match t with T0 => [0;0] \| T1 => [0;1] \| TZ => [1;0;0] end.
		52	Fixpoint tw (ts : list tok) : list Sym :=
		53	match ts with [] => [] \| t :: ts => tokw t ++ tw ts end.
		55	Inductive ptok := P \| PZ.
		56	Definition pw (p : ptok) : list Sym := match p with P => [0;1] \| PZ => [0;1;0] end.
		57	Fixpoint pl (ps : list ptok) : list Sym :=
		58	match ps with [] => [] \| p :: ps => pw p ++ pl ps end.
		59	Definition proc (t : tok) : ptok := match t with TZ => PZ \| _ => P end.
		61	Lemma tw_app xs ys : tw (xs ++ ys) = tw xs ++ tw ys.
		62	Proof. induction xs; cbn; [reflexivity\|]. rewrite IHxs, app_assoc. reflexivity. Qed.
		63	Lemma tw_cons x xs : tw (x :: xs) = tokw x ++ tw xs.
		64	Proof. reflexivity. Qed.
		65	Lemma pl_app xs ys : pl (xs ++ ys) = pl xs ++ pl ys.
		66	Proof. induction xs; cbn; [reflexivity\|]. rewrite IHxs, app_assoc. reflexivity. Qed.
		68	( Window lemmas *)
		69	Lemma AT0 l r : l {{A}}> [0;0] > r --> l <* [0;1] {{C}}> r. Proof. es. Qed.
		70	Lemma CT1 l r : l {{C}}> [0;1] > r --> l <* [0;1] {{C}}> r. Proof. es. Qed.
		71	Lemma CTZ l r : l {{C}}> [1;0;0] > r --> l <* [0;1;0] {{C}}> r. Proof. es. Qed.
		72	Lemma CT0 l r : l {{C}}> [0;0] > r --> l <{{E}} [0;1] *> r. Proof. es. Qed.
		73	Lemma EPZ l r : l <* [0;1;0] <{{E}} r -->* l <{{E}} [1;0;0] *> r. Proof. es. Qed.
		74	Lemma EP l r : l <* [0;1] <{{E}} r -->* l <{{F}} [0;0] *> r. Proof. es. Qed.
		75	Lemma FP l r : l <* [0;1] <{{F}} r -->* l <{{E}} [0;1] *> r. Proof. es. Qed.
		76	Lemma FPZP l r : l <* [0;1] <* [0;1;0] <{{F}} [0;0] > r -->
		77	l <{{E}} [0;0] > [1;0;0] > [0;1] *> r. Proof. es. Qed.
		78	Lemma ENDl l r : l <* [0;0] <{{F}} r -->* l <{{A}} [0;1] *> r. Proof. es. Qed.
		79	Lemma B1 l r : l <* [1;0] <{{F}} r -->* l <* [0;0] {{A}}> r. Proof. es. Qed.
		80	Lemma BN l r : l <* [0;1;0;0;1;0] <{{F}} [0;0] > r --> l <{{A}} [0;0;0;1;0;0;0;1] *> r. Proof. es. Qed.
		81	Lemma ENDZX l r : l <* [0;0;1;0;0;1;0;1;0;0;1;0] <{{F}} r -->* l <{{A}} [0;0;0;1;0;0;0;1;1;0;0;1] *> r. Proof. es. Qed.
		83	( C sweep over T1/TZ tokens *)
		84	Fixpoint noT0 (ts : list tok) : Prop :=
		85	match ts with [] => True \| T0 :: _ => False \| _ :: ts => noT0 ts end.
		86	Definition prc (ts : list tok) : list ptok := rev (map proc ts).
		88	Lemma Csweep ts : noT0 ts -> forall l r,
		89	l {{C}}> tw ts > r --> l <* pl (prc ts) {{C}}> r.
19	Proof.	90	Proof.
20	intros s n l. induction n as [\| n IH]; [reflexivity \|].
		91	induction ts as [\|t ts IH]; intros H l r; [finish\|].
21	cbn [lpow app Str_app] in *. rewrite IH. reflexivity.
		92	unfold prc. cbn [map rev]. rewrite pl_app. cbn [tw].
		93	rewrite Str_app_assoc.
		94	destruct t; cbn in H; [contradiction\| \|].
		95	- follow CT1. follow (IH H). cbn [pl proc]. rewrite Str_app_assoc. finish.
		96	- follow CTZ. follow (IH H). cbn [pl proc]. rewrite Str_app_assoc. finish.
22	Qed.	97	Qed.
24	Lemma lpow_snoc' : forall (s : Sym) n (l : side),
		99	( The leftward return over processed tokens *)
25	s >> [s]^^n > l = [s]^^n > s >> l.
		100	Fixpoint retf (m : Q) (ps : list ptok) (rs : list tok) {struct ps} : Q * list ptok * list tok :=
26	Proof. intros. symmetry. apply (lpow_snoc s n l). Qed.
		101	match m, ps with
28	Lemma lpow_app : forall (xs : list Sym) a b (r : side),
		102	\| E, PZ :: ps' => retf E ps' (TZ :: rs)
29	xs^^a > xs^^b > r = xs^^(a + b) *> r.
		103	\| E, P :: ps' => retf F ps' (T0 :: rs)
		104	\| F, P :: ps' => retf E ps' (T1 :: rs)
		105	\| F, PZ :: P :: ps' =>
		106	match rs with
		107	\| T0 :: rs' => retf E ps' (T0 :: TZ :: T1 :: rs')
		108	\| _ => (m, ps, rs)
		109	end
		110	\| _, _ => (m, ps, rs)
		111	end.
		113	Lemma retf_spec_n n : forall ps, length ps <= n -> forall m rs m' ps' rs',
		114	retf m ps rs = (m', ps', rs') -> forall l r,
		115	l <* pl ps <{{m}} tw rs > r --> l <* pl ps' <{{m'}} tw rs' *> r.
30	Proof.	116	Proof.
31	intros. rewrite lpow_add, Str_app_assoc. reflexivity.
		117	induction n as [\|n IH]; intros ps Hn m rs m' ps' rs' Hr l r.
		118	- destruct ps; [\|cbn in Hn; lia].
		119	destruct m; cbn in Hr; inversion Hr; subst; finish.
		120	- destruct ps as [\|p ps].
		121	{ destruct m; cbn in Hr; inversion Hr; subst; finish. }
		122	cbn in Hn.
		123	destruct m, p; cbn in Hr; try (inversion Hr; subst; solve [finish]).
		124	+ (* E, P *)
		125	cbn [pl]. rewrite Str_app_assoc. cbn [pw].
		126	follow EP. apply (IH ps ltac:(lia) _ _ _ _ _ Hr).
		127	+ (* E, PZ *)
		128	cbn [pl]. rewrite Str_app_assoc. cbn [pw].
		129	follow EPZ. apply (IH ps ltac:(lia) _ _ _ _ _ Hr).
		130	+ (* F, P *)
		131	cbn [pl]. rewrite Str_app_assoc. cbn [pw].
		132	follow FP. apply (IH ps ltac:(lia) _ _ _ _ _ Hr).
		133	+ (* F, PZ *)
		134	destruct ps as [\|[\|] ps]; try (inversion Hr; subst; solve [finish]).
		135	destruct rs as [\|[\| \|] rs]; try (inversion Hr; subst; solve [finish]).
		136	cbn [pl tw]. rewrite !Str_app_assoc. cbn [pw tokw].
		137	cbn in Hn.
		138	follow FPZP.
		139	assert (H := IH ps ltac:(lia) _ _ _ _ _ Hr l r).
		140	cbn [tw] in H. rewrite !Str_app_assoc in H. exact H.
32	Qed.	141	Qed.
34	Lemma lpow_cons_r : forall (s : Sym) n (r : side),
		143	Lemma retf_spec ps m rs m' ps' rs' :
35	[s]^^n > s >> r = [s]^^(S n) > r.
		144	retf m ps rs = (m', ps', rs') -> forall l r,
		145	l <* pl ps <{{m}} tw rs > r --> l <* pl ps' <{{m'}} tw rs' *> r.
		146	Proof. intros. eapply retf_spec_n; [apply le_n\|eassumption]. Qed.
		148	( Shift rules *)
		149	Lemma CTZ' l r : l <* [] {{C}}> [1;0;0] > r --> l <* [0;1;0] <* [] {{C}}> r. Proof. es. Qed.
		150	Definition CTZs := shift_rule_R _ _ _ _ _ CTZ'.
		151	Lemma EPZ' l r : l <* [0;1;0] <{{E}} [] > r --> l <{{E}} [] > [1;0;0] > r. Proof. es. Qed.
		152	Definition EPZs := shift_rule_L _ _ _ _ _ EPZ'.
		154	Lemma tw_Z g : tw (repeat TZ g) = [1;0;0]^^g.
		155	Proof. induction g; cbn; [reflexivity\|]. rewrite IHg. reflexivity. Qed.
		157	( The counter: digits b Z 1 Z^g, LSB first; the last digit is its bit only *)
		158	Definition bit (v : nat) : tok := if Nat.odd v then T1 else T0.
		159	Fixpoint ctr (gs : list nat) (v : nat) : list tok :=
		160	match gs with
		161	\| [] => [bit v]
		162	\| g :: gs' => bit v :: TZ :: T1 :: repeat TZ g ++ ctr gs' (Nat.div2 v)
		163	end.
		165	Lemma bit_even w : bit (2*w) = T0.
		166	Proof. unfold bit. rewrite Nat.odd_even. reflexivity. Qed.
		167	Lemma bit_odd w : bit (S (2*w)) = T1.
		168	Proof. unfold bit. replace (S (2w)) with (2w+1) by lia. rewrite Nat.odd_odd. reflexivity. Qed.
		170	Lemma ctr_even g gs w : ctr (g :: gs) (2*w) = T0 :: TZ :: T1 :: repeat TZ g ++ ctr gs w.
		171	Proof. cbn [ctr]. rewrite bit_even, Nat.div2_double. reflexivity. Qed.
		172	Lemma ctr_odd g gs w : ctr (g :: gs) (S (2*w)) = T1 :: TZ :: T1 :: repeat TZ g ++ ctr gs w.
		173	Proof. cbn [ctr]. rewrite bit_odd, Nat.div2_succ_double. reflexivity. Qed.
		175	Lemma ctr_hd_even gs w : exists rest, ctr gs (2w) = T0 :: rest /\ ctr gs (S (2w)) = T1 :: rest.
36	Proof.	176	Proof.
37	intros s n r. induction n as [\| n IH]; [reflexivity \|].
		177	destruct gs as [\|g gs].
38	cbn [lpow app Str_app] in *. rewrite IH. reflexivity.
		178	- exists (@nil tok). cbn [ctr]. rewrite bit_even, bit_odd. auto.
		179	- eexists. rewrite ctr_even, ctr_odd. split; reflexivity.
39	Qed.	180	Qed.
41	Lemma lpow_mul_S : forall (xs : list Sym) k (r : side),
		182	Lemma pow2S n : 2 ^ S n = 2 * 2 ^ n.
42	xs^^(S k) > r = xs > xs^^k *> r.
		183	Proof. apply Nat.pow_succ_r'. Qed.
43	Proof. intros. cbn [lpow]. apply Str_app_assoc. Qed.
		185	Lemma IncC gs : forall v, S v < 2 ^ S (length gs) -> forall l r t,
45	(** Replace the left-hand side of an [-->] goal by a convertible term. )
		186	l {{C}}> tw (ctr gs v ++ t) > r --> l <{{E}} tw (ctr gs (S v) ++ t) *> r.
46	Ltac lhs_raw c :=
47	lazymatch goal with
⋯ 17 template-only lines (template 48–69), not in ours
71	Lemma sweepC : forall e l r,
72	l <* [1]^^e <{{C}} r -->* l <{{C}} [1]^^e *> r.
73	Proof.	187	Proof.
74	induction e as [\| e IH]; intros l r.	188	induction gs as [\|g gs IH]; intros v Hv l r t;
75	- finish.
		189	destruct (Nat.Even_or_Odd v) as [[w ->]\|[w ->]].
76	- cbn [lpow app Str_app]. step.
		190	- cbn [ctr app tw]. rewrite bit_even. replace (S (2w)) with (2w+1) by lia.
77	follow IH. apply evstep_refl'. now rewrite lpow_cons_r.
		191	unfold bit. rewrite Nat.odd_odd. cbn [tokw]. rewrite !Str_app_assoc. apply CT0.
		192	- cbn [length] in Hv. rewrite pow2S in Hv. cbn in Hv. lia.
		193	- destruct (ctr_hd_even (g :: gs) w) as (rest & E0 & E1).
		194	rewrite E0, E1. cbn [app tw]. rewrite !Str_app_assoc. apply CT0.
		195	- replace (2w+1) with (S (2w)) by lia. rewrite ctr_odd.
		196	replace (S (S (2w))) with (2 S w) by lia. rewrite ctr_even.
		197	cbn [length] in Hv. rewrite !pow2S in Hv.
		198	cbn [app]. rewrite <- !app_assoc. cbn [tw].
		199	rewrite !(tw_app (repeat TZ g)), tw_Z, !Str_app_assoc. cbn [tokw].
		200	follow CT1. follow CTZ. follow CT1.
		201	follow CTZs.
		202	follow (IH w ltac:(rewrite pow2S; lia)).
		203	follow EPZs. follow EP. follow FPZP. finish.
78	Qed.	204	Qed.
80	Lemma sweepD : forall e l r,
		206	Lemma IncL gs v a : S v < 2 ^ S (length gs) -> forall l r t,
81	l {{D}}> [1]^^e > r --> l <* [1]^^e {{D}}> r.
		207	l {{A}}> tw (T0 :: repeat TZ a ++ ctr gs v ++ t) > r -->
		208	l <{{F}} tw (T0 :: repeat TZ a ++ ctr gs (S v) ++ t) *> r.
82	Proof.	209	Proof.
83	induction e as [\| e IH]; intros l r.
		210	intros Hv l r t.
84	- finish.
		211	cbn [tw]. rewrite !(tw_app (repeat TZ a)), tw_Z, !Str_app_assoc. cbn [tokw].
85	- cbn [lpow app Str_app]. step.
		212	follow AT0. follow CTZs.
86	follow IH. apply evstep_refl'. now rewrite lpow_snoc.
		213	follow (IncC gs v Hv).
		214	follow EPZs. follow EP. finish.
87	Qed.	215	Qed.
89	Lemma sweepF : forall e l r,
		217	( The left bounce: F at the edge adds one 100 to the lead and returns to A *)
90	l {{F}}> [1]^^e > r --> l <* [0]^^e {{F}}> r.
		218	Lemma Bnc X : (const 0) <{{F}} [0;0] > [1;0;0] > X -->*
		219	(const 0) {{A}}> [0;0] > [1;0;0] > [1;0;0] *> X.
		220	Proof. rewrite (const_unfold _ 0) at 1. es. Qed.
		222	( Normal-mode increment: one bounce, lead a -> a+1, counter v -> v+1 *)
		223	Lemma Inc gs v a : S v < 2 ^ S (length gs) -> forall t,
		224	(const 0) {{A}}> tw (T0 :: repeat TZ (S a) ++ ctr gs v ++ t) > (const 0) -->
		225	(const 0) {{A}}> tw (T0 :: repeat TZ (S (S a)) ++ ctr gs (S v) ++ t) *> (const 0).
91	Proof.	226	Proof.
92	induction e as [\| e IH]; intros l r.
		227	intros Hv t.
93	- finish.
		228	follow (IncL gs v (S a) Hv).
94	- cbn [lpow app Str_app]. step.
		229	(* 0inf <F tw(T0 :: 100^(S a) ++ ctr(Sv) ++ t) ; peel 00 100 and bounce *)
95	follow IH. apply evstep_refl'. now rewrite lpow_snoc.
		230	cbn [repeat app]. rewrite !tw_cons. cbn [tokw]. rewrite !Str_app_assoc.
		231	follow Bnc. finish.
96	Qed.	232	Qed.
98	( E(j), Climb, X1 (mutual strong induction on j) *)
		234	( Overflow return: C sweeps a T0-free word, turns at the next 0, then retf returns.
100	Definition E_stmt j := forall l r m, j <= m ->
		235	This is the whole tail table T(f) of the write-up, with no 2^14-entry table: the head
101	l << 1 <* [0]^^(1 + j3) {{A}}> 1 >> [1]^^m > 0 >> r -->*
		236	stops at the first 0 of the tail and the leftward return is the finite automaton [retf]. *)
102	l << 1 <* [1]^^(1 + j3) <{{A}} 1 >> [1]^^m > 0 >> r.
		237	Lemma OvRet w rest : noT0 w ->
104	Lemma E0 : E_stmt 0.
		238	forall m' ps' rs', retf E (prc w ++ [P]) (T1 :: rest) = (m', ps', rs') ->
105	Proof. intros l r m _. execute. Qed.
		239	forall l r,
107	Lemma Climb_of_E : forall i, E_stmt i -> forall l r n, i + 1 <= n ->
		240	l {{A}}> tw (T0 :: w ++ T0 :: rest) > r -->
108	l <* [0]^^3 {{A}}> 0 >> [1]^^(2 + i3) > 0 >> [1]^^n > 0 >> r -->
		241	l <* pl ps' <{{m'}} tw rs' *> r.
109	l {{A}}> 0 >> [1]^^(5 + i3) > 0 >> [1]^^n *> 0 >> r.
110	Proof.	242	Proof.
111	intros i HE l r n Hn.
		243	intros Hw m' ps' rs' Hr l r.
112	destruct n as [\| n]; [lia \|].
		244	rewrite tw_cons. cbn [tokw]. rewrite (tw_app w (T0 :: rest)), !Str_app_assoc.
113	execute.
		245	follow AT0.
114	follow sweepF. step.
		246	follow (Csweep w Hw).
115	follow HE; try lia.
		247	rewrite tw_cons. cbn [tokw]. rewrite Str_app_assoc.
116	step. follow sweepC. execute.
		248	follow CT0.
		249	(* now: l <* [0;1] <* pl (prc w) <{{E}} [0;1] > tw rest > r *)
		250	assert (H := retf_spec (prc w ++ [P]) E (T1 :: rest) m' ps' rs' Hr l r).
		251	rewrite pl_app in H. cbn [pl pw] in H.
		252	cbn [tw tokw] in H.
		253	rewrite !Str_app_assoc in H.
		254	follow H. finish.
117	Qed.	255	Qed.
119	Lemma X1_of_E : forall i, E_stmt i -> forall l r n, i + 1 <= n ->
		257	( Pause rules (proof.md section 3) *)
120	l << 1 << 0 {{A}}> 0 >> [1]^^(2 + i3) > 0 >> [1]^^n > 0 >> r -->
		258	Ltac tnorm := rewrite <- ?app_assoc; repeat (rewrite ?tw_cons, ?tw_app, ?tw_Z); cbn [tokw]; rewrite ?Str_app_assoc.
121	l <* [1]^^(5 + i3) <{{A}} 1 >> [1]^^n > 0 >> r.
		260	Lemma TwoInc gs v p t L r : S (S v) < 2 ^ S (length gs) ->
		261	L <* [0] <* [1;0] {{A}}> tw (T0 :: repeat TZ p ++ ctr gs v ++ t) > r -->
		262	L {{A}}> tw (T0 :: repeat TZ (S p) ++ ctr gs (S (S v)) ++ t) *> r.
122	Proof.	263	Proof.
123	intros i HE l r n Hn.
		264	intros Hv.
124	destruct n as [\| n]; [lia \|].
		265	follow (IncL gs v p ltac:(lia)).
125	execute.
		266	follow B1.
126	follow sweepF. step.
		267	follow (IncL gs (S v) p Hv).
127	follow HE; try lia.
		268	follow ENDl.
128	step. follow sweepC. execute.
		269	cbn [repeat app]. rewrite !tw_cons. cbn [tokw]. rewrite !Str_app_assoc.
129	follow sweepD. execute. fin.
130	Qed.
⋯ 727 template-only lines (template 132–905), not in ours
906	(* hit the wall *)
907	follow (H b (q m - 1) (3 * N m - 1) l ([1]^^(N m - 1) *> const 0) ltac:(lia)).
908	finish.	270	finish.
909	Qed.	271	Qed.
911	( The stage chain S(k), Climb, S(k-1), Climb, ..., S(3), Climb *)
		273	Lemma ZXg gs v p t L r : S (S v) < 2 ^ S (length gs) ->
912	Lemma Chain : forall n, (forall m, m < n -> Traj m) -> forall b l, 1 <= b ->
		274	L <* [0] <* [1;0;1;0;0;1;0;1;0;0;1;0] {{A}}> tw (T0 :: repeat TZ p ++ ctr gs v ++ t) > r -->
913	l <* [0]^^(ZC n) {{A}}> 0 >> [1]^^(2 + b3) > 0 >> [1]^^b > 0 >> [1]^^(N n - 1) > const 0 -->*
		275	L {{A}}> tw (T0 :: ctr (S (S p) :: gs) (2 * S (S v)) ++ t) *> r.
914	lm0 l (2 + (b + 3 * SN n)3) (b + 3 SN n) 67.
915	Proof.	276	Proof.
916	induction n as [\| n IH]; intros HT b l Hb.
		277	intros Hv.
917	- replace (b + 3 * SN 0) with b by (simpl; lia). unfold lm0. simpl ZC. simpl N. finish.
		278	follow (IncL gs v p ltac:(lia)).
918	- pose proof (inv n) as Hi.
		279	follow B1.
919	replace ([0]^^(ZC (S n)) *> l)
		280	follow (IncL gs (S v) p Hv).
920	with ([0]^^3 > [0]^^((3 N n - q n - 2)3) > [0]^^(ZC n) *> l).
		281	follow ENDZX.
921	2:{ rewrite !lpow_app. f_equal. f_equal. simpl ZC. lia. }
		282	rewrite ctr_even. cbn [repeat app]. tnorm.
922	follow (Stage n (HT n ltac:(lia)) b ([0]^^((3 * N n - q n - 2)3) > [0]^^(ZC n) *> l) Hb).
		283	finish.
923	unfold lm0.
924	follow (Climbs (3 * N n - q n - 2) (b + q n + 2) ([0]^^(ZC n) *> l)
925	([1]^^(N n - 1) > const 0) (b + 3 N n) ltac:(lia)).
926	follow (IH (fun m Hm => HT m ltac:(lia)) (b + 3 * N n) l ltac:(lia)).
927	unfold lm0. simpl SN. finish.
928	Qed.	284	Qed.
930	( One round: Traj(k) landmark -> Traj(k+1) landmark *)
		286	Lemma ZXP2g gs v p t L r : S v < 2 ^ S (length gs) ->
931	Lemma Step : forall n, (forall m, m <= n -> Traj m) -> forall l,
		287	L <* [0] <* [0;1;0;0;1;0] {{A}}> tw (T0 :: repeat TZ p ++ ctr gs v ++ t) > r -->
932	lm0 (l <* [0]^^(Zs n)) 8 (3 * N n - 1) (N n - 1) -->+
		288	L {{A}}> tw (T0 :: ctr (p :: gs) (2 * S v) ++ t) *> r.
933	lm0 l 8 (3 * N (S n) - 1) (N (S n) - 1).
934	Proof.	289	Proof.
935	intros n HT l. pose proof (inv n) as Hi.
		290	intros Hv.
936	unfold Zs.
		291	follow (IncL gs v p Hv).
937	replace ([0]^^(3 * (3 * N n - 3) + ZC n + 180 + 3) *> l)
		292	rewrite tw_cons. cbn [tokw]. rewrite Str_app_assoc.
938	with ([0]^^((3 * N n - 3)3) > [0]^^(ZC n) > [0]^^180 > [0]^^3 *> l).
		293	follow BN.
939	2:{ rewrite !lpow_app. f_equal. f_equal. lia. }
		294	rewrite ctr_even. cbn [app]. tnorm.
940	unfold lm0.
		295	finish.
941	follow (Climbs (3 * N n - 3) 2 ([0]^^(ZC n) > [0]^^180 > [0]^^3 *> l)
		296	Qed.
942	([1]^^(N n - 1) > const 0) (3 N n - 1) ltac:(lia)).
		298	( The tail (proof.md sections 1.2, 4.2, 4.4) *)
943	follow (Chain n (fun m Hm => HT m ltac:(lia)) (3 * N n - 1)
		299	Definition bt (b : bool) : tok := if b then T1 else T0.
944	([0]^^180 > [0]^^3 > l) ltac:(lia)).
		300	Definition tailx (y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 : bool) (e : list bool) : list tok :=
945	follow (Tail (3 * N n - 1 + 3 * SN n) ([0]^^3 *> l) ltac:(lia)).
		301	bt y :: bt z :: TZ :: T1 :: bt b4 :: bt b5 :: TZ :: T1 :: bt b6 :: TZ :: bt b7 :: TZ :: T1 ::
946	unfold lm0.
		302	bt b8 :: bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ ::
		303	bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1].
		304	Definition tailw (x y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 : bool) (e : list bool) : list tok :=
		305	bt x :: tailx y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e.
		307	(** L: x = 1, front unit (y, z); the stream is the tail followed by blank tape. )
		308	Definition Lst (y z : bool) (S : Stream Sym) : Prop :=
		309	exists b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e,
		310	S = tw (tailw true y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0.
		312	Lemma TailRet pre rest m out : noT0 pre -> retf E (prc pre) [T1] = (m, [], out) ->
		313	forall l R, l {{C}}> tw (pre ++ T0 :: rest) > R --> l <{{m}} tw (out ++ rest) *> R.
		314	Proof.
		315	intros Hn Hr l R.
		316	rewrite tw_app, Str_app_assoc, tw_cons. cbn [tokw]. rewrite Str_app_assoc.
		317	follow (Csweep pre Hn).
		318	follow CT0.
		319	assert (H := retf_spec (prc pre) E [T1] m [] out Hr l (tw rest *> R)).
		320	cbn [pl tw tokw app] in H. rewrite tw_app, Str_app_assoc. exact H.
		321	Qed.
		323	Lemma Tail10 l b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e :
		324	l {{C}}> tw (tailw true true false b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 -->
		325	l <{{E}} tw (tailw true false true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0.
		326	Proof.
		327	exact (TailRet [T1; T1] (tl (tl (tailx true true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e)))
		328	E [T1; T0; T1] I eq_refl l (const 0)).
		329	Qed.
		331	Lemma Tail0z l z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e :
		332	l {{C}}> tw (tailw true false z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 -->
		333	l <{{F}} [0;0] > tw (tailx true z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0.
		334	Proof.
		335	exact (TailRet [T1] (tl (tailx true z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e))
		336	F [T0; T1] I eq_refl l (const 0)).
		337	Qed.
		339	Definition F1 : list tok := [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1; T1; TZ; T1; TZ; T1; T1; TZ; T1; TZ; T1; TZ; T1; TZ; T1; TZ; T1].
		340	Definition F1E : list tok := [T1; T0; T0; TZ; T1; T1; T0; TZ; T1; T0; TZ; T0; TZ; T1; T1; T0; TZ; T0; TZ; T1; T0; TZ; T1; TZ; T0; TZ; T1; TZ; T0; TZ; T1].
		341	Definition F1F : list tok := [T0; T1; T0; TZ; T1; T0; T0; TZ; T1; T0; TZ; T1; TZ; T1; T0; T0; TZ; T1; TZ; T1; T0; TZ; T0; TZ; T1; TZ; T0; TZ; T1; TZ; T1].
		342	Lemma F1E_ret X : retf E (prc F1) X = (E, [], F1E ++ X). Proof. reflexivity. Qed.
		343	Lemma F1F_ret X : retf F (prc F1) X = (F, [], F1F ++ X). Proof. reflexivity. Qed.
		344	Lemma tailw_ones e : tailw true true true true true true true true true true true true true true true e = F1 ++ map bt e ++ [T1].
		345	Proof. reflexivity. Qed.
		347	Lemma prc_app xs ys : prc (xs ++ ys) = prc ys ++ prc xs.
		348	Proof. unfold prc. rewrite map_app, rev_app_distr. reflexivity. Qed.
		349	Lemma repeat_snoc {X} (x : X) n : repeat x n ++ [x] = x :: repeat x n.
		350	Proof. induction n as [\|n IH]; cbn; [\|rewrite IH]; reflexivity. Qed.
		351	Lemma prc_T1s j : prc (repeat T1 j) = repeat P j.
		352	Proof.
		353	unfold prc. induction j as [\|j IH]; [reflexivity\|].
		354	cbn [repeat map rev]. rewrite IH. apply repeat_snoc.
		355	Qed.
		356	Lemma noT0_app xs ys : noT0 xs -> noT0 ys -> noT0 (xs ++ ys).
		357	Proof. induction xs as [\|[] xs IH]; cbn; tauto. Qed.
		358	Lemma noT0_T1s j : noT0 (repeat T1 j).
		359	Proof. induction j; cbn; auto. Qed.
		360	Lemma map_bt_true j : map bt (repeat true j) = repeat T1 j.
		361	Proof. induction j; cbn; [\|rewrite IHj]; reflexivity. Qed.
		362	Lemma map_bt_alt i : map bt ([true; false]^^i) = [T1; T0]^^i.
		363	Proof. induction i; cbn; [\|rewrite IHi]; reflexivity. Qed.
		365	Lemma retf_PP i : forall ps rs, retf E (repeat P (2 * i) ++ ps) rs = retf E ps ([T1;T0]^^i ++ rs).
		366	Proof.
		367	induction i as [\|i IH]; intros ps rs; [reflexivity\|].
		368	replace (2 * S i) with (S (S (2 * i))) by lia. cbn [repeat app retf].
		369	rewrite IH. f_equal. change (T1 :: T0 :: rs) with ([T1;T0] ++ rs).
		370	rewrite app_assoc, lpow_shift. reflexivity.
		371	Qed.
		372	Lemma retf_PPP i ps rs : retf E (repeat P (S (2 * i)) ++ ps) rs = retf F ps (T0 :: [T1;T0]^^i ++ rs).
		373	Proof.
		374	replace (repeat P (S (2 * i)) ++ ps) with (repeat P (2 * i) ++ P :: ps).
		375	- rewrite retf_PP. reflexivity.
		376	- change (P :: ps) with ([P] ++ ps). rewrite app_assoc, repeat_snoc. reflexivity.
		377	Qed.
		379	Lemma e_split e : (exists j e', e = repeat true j ++ false :: e') \/ (exists m, e = repeat true m).
		380	Proof.
		381	induction e as [\|[] e IH].
		382	- right. exists O. reflexivity.
		383	- destruct IH as [(j & e' & ->)\|(m & ->)].
		384	+ left. exists (S j), e'. reflexivity.
		385	+ right. exists (S m). reflexivity.
		386	- left. exists O, e. reflexivity.
		387	Qed.
		389	Lemma Tail11_end e :
		390	(exists S', (forall l, l {{C}}> tw (tailw true true true true true true true true true true true true true true true e) > const 0 -->
		391	l <{{E}} S') /\ Lst false false S') \/
		392	(exists S', (forall l, l {{C}}> tw (tailw true true true true true true true true true true true true true true true e) > const 0 -->
		393	l <{{F}} [0;0] > S') /\ Lst true false ([0;1] > S')).
		394	Proof.
		395	rewrite tailw_ones.
		396	destruct (e_split e) as [(j & e' & ->)\|(m & ->)].
		397	- assert (Hs : F1 ++ map bt (repeat true j ++ false :: e') ++ [T1] =
		398	(F1 ++ repeat T1 j) ++ T0 :: (map bt e' ++ [T1])).
		399	{ rewrite map_app, map_bt_true. cbn [map bt app]. rewrite <- ?app_assoc. cbn [app]. reflexivity. }
		400	rewrite Hs.
		401	assert (Hn : noT0 (F1 ++ repeat T1 j)) by (apply noT0_app; [exact I \| apply noT0_T1s]).
		402	destruct (Nat.Even_or_Odd j) as [[i ->]\|[i ->]].
		403	+ left. eexists. split.
		404	* intros l. apply (TailRet _ _ E (F1E ++ [T1;T0]^^i ++ [T1]) Hn).
		405	rewrite prc_app, prc_T1s, retf_PP, F1E_ret. reflexivity.
		406	* exists true; exists false; exists false; exists false; exists true; exists false; exists false; exists false; exists true; exists false; exists true; exists false; exists ([true;false]^^i ++ true :: e').
		407	unfold tailw, tailx. rewrite map_app, map_bt_alt. cbn [map bt app]. rewrite <- ?app_assoc. cbn [app]. reflexivity.
		408	+ replace (2 * i + 1) with (S (2 * i)) in * by lia.
		409	right. exists (tw (tl F1F ++ T0 :: [T1;T0]^^i ++ [T1] ++ map bt e' ++ [T1]) *> const 0). split.
		410	* intros l. replace (tl F1F ++ T0 :: [T1;T0]^^i ++ [T1] ++ map bt e' ++ [T1]) with
		411	(tl ((F1F ++ T0 :: [T1;T0]^^i ++ [T1]) ++ map bt e' ++ [T1]))
		412	by (unfold F1F; cbn [tl app]; rewrite <- !app_assoc; reflexivity).
		413	apply (TailRet _ _ F (F1F ++ T0 :: [T1;T0]^^i ++ [T1]) Hn).
		414	rewrite prc_app, prc_T1s, retf_PPP, F1F_ret. reflexivity.
		415	* exists false; exists false; exists false; exists true; exists false; exists false; exists true; exists false; exists false; exists true; exists false; exists true; exists (false :: [true;false]^^i ++ true :: e').
		416	unfold tailw, tailx. cbn [map]. rewrite map_app, map_bt_alt. cbn [map bt app]. rewrite <- ?app_assoc. cbn [app]. reflexivity.
		417	- assert (Hs : tw (F1 ++ map bt (repeat true m) ++ [T1]) *> const 0 =
		418	tw ((F1 ++ repeat T1 (S m)) ++ T0 :: []) *> const 0).
		419	{ rewrite map_bt_true. rewrite !tw_app, !Str_app_assoc. cbn [tw tokw app].
		420	replace (repeat T1 (S m)) with (repeat T1 m ++ [T1]) by apply repeat_snoc.
		421	rewrite tw_app, Str_app_assoc. cbn [tw tokw app].
		422	rewrite (const_unfold _ 0) at 1. rewrite (const_unfold _ 0) at 1. reflexivity. }
		423	rewrite Hs.
		424	assert (Hn : noT0 (F1 ++ repeat T1 (S m))) by (apply noT0_app; [exact I \| apply noT0_T1s]).
		425	destruct (Nat.Even_or_Odd (S m)) as [[i Hi]\|[i Hi]]; rewrite Hi in *.
		426	+ left. eexists. split.
		427	* intros l. apply (TailRet _ _ E (F1E ++ [T1;T0]^^i ++ [T1]) Hn).
		428	rewrite prc_app, prc_T1s, retf_PP, F1E_ret. reflexivity.
		429	* exists true; exists false; exists false; exists false; exists true; exists false; exists false; exists false; exists true; exists false; exists true; exists false; exists ([true;false]^^i).
		430	rewrite app_nil_r. unfold tailw, tailx. rewrite map_bt_alt. cbn [map bt app]. rewrite <- ?app_assoc. cbn [app]. reflexivity.
		431	+ replace (2 * i + 1) with (S (2 * i)) in * by lia.
		432	right. exists (tw (tl F1F ++ T0 :: [T1;T0]^^i ++ [T1]) *> const 0). split.
		433	* intros l. replace (tl F1F ++ T0 :: [T1;T0]^^i ++ [T1]) with
		434	(tl ((F1F ++ T0 :: [T1;T0]^^i ++ [T1]) ++ []))
		435	by (rewrite app_nil_r; unfold F1F; reflexivity).
		436	apply (TailRet _ _ F (F1F ++ T0 :: [T1;T0]^^i ++ [T1]) Hn).
		437	rewrite prc_app, prc_T1s, retf_PPP, F1F_ret. reflexivity.
		438	* exists false; exists false; exists false; exists true; exists false; exists false; exists true; exists false; exists false; exists true; exists false; exists true; exists (false :: [true;false]^^i).
		439	unfold tailw, tailx. cbn [map]. rewrite map_bt_alt. cbn [map bt app]. rewrite <- ?app_assoc. cbn [app]. reflexivity.
		440	Qed.
		442	Lemma Tail11 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e :
		443	(exists S', (forall l, l {{C}}> tw (tailw true true true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 -->
		444	l <{{E}} S') /\ Lst false false S') \/
		445	(exists S', (forall l, l {{C}}> tw (tailw true true true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 -->
		446	l <{{F}} [0;0] > S') /\ Lst true false ([0;1] > S')).
		447	Proof.
		448	destruct b4. 2: {
		449	left. exists (tw (tailw true false false true b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0). split.
		450	- intros l; exact (TailRet [T1; T1; T1; TZ; T1] (bt b5 :: TZ :: T1 :: bt b6 :: TZ :: bt b7 :: TZ :: T1 :: bt b8 :: bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) E [T1; T0; T0; TZ; T1; T1] I eq_refl l (const 0)).
		451	- exists true; exists b5; exists b6; exists b7; exists b8; exists b9; exists b10; exists b11; exists b12; exists b13; exists b14; exists b15; exists e. reflexivity. }
		452	destruct b5. 2: {
		453	right. exists (tw ([T1; T0; TZ; T1; T0; T1] ++ (TZ :: T1 :: bt b6 :: TZ :: bt b7 :: TZ :: T1 :: bt b8 :: bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1])) *> const 0). split.
		454	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1] (TZ :: T1 :: bt b6 :: TZ :: bt b7 :: TZ :: T1 :: bt b8 :: bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) F [T0; T1; T0; TZ; T1; T0; T1] I eq_refl l (const 0)).
		455	- exists false; exists true; exists b6; exists b7; exists b8; exists b9; exists b10; exists b11; exists b12; exists b13; exists b14; exists b15; exists e. reflexivity. }
		456	destruct b6. 2: {
		457	right. exists (tw ([T1; T0; TZ; T1; T0; T0; TZ; T1; T1] ++ (TZ :: bt b7 :: TZ :: T1 :: bt b8 :: bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1])) *> const 0). split.
		458	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1] (TZ :: bt b7 :: TZ :: T1 :: bt b8 :: bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) F [T0; T1; T0; TZ; T1; T0; T0; TZ; T1; T1] I eq_refl l (const 0)).
		459	- exists false; exists false; exists true; exists b7; exists b8; exists b9; exists b10; exists b11; exists b12; exists b13; exists b14; exists b15; exists e. reflexivity. }
		460	destruct b7. 2: {
		461	left. exists (tw (tailw true false false true false false true b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0). split.
		462	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ] (TZ :: T1 :: bt b8 :: bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) E [T1; T0; T0; TZ; T1; T1; T0; TZ; T1; T0; TZ; T1] I eq_refl l (const 0)).
		463	- exists true; exists false; exists false; exists true; exists b8; exists b9; exists b10; exists b11; exists b12; exists b13; exists b14; exists b15; exists e. reflexivity. }
		464	destruct b8. 2: {
		465	left. exists (tw (tailw true false false true false false false true b9 b10 b11 b12 b13 b14 b15 e) *> const 0). split.
		466	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1] (bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) E [T1; T0; T0; TZ; T1; T1; T0; TZ; T1; T0; TZ; T0; TZ; T1; T1] I eq_refl l (const 0)).
		467	- exists true; exists false; exists false; exists false; exists true; exists b9; exists b10; exists b11; exists b12; exists b13; exists b14; exists b15; exists e. reflexivity. }
		468	destruct b9. 2: {
		469	right. exists (tw ([T1; T0; TZ; T1; T0; T0; TZ; T1; T0; TZ; T1; TZ; T1; T0; T1] ++ (TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1])) *> const 0). split.
		470	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1] (TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) F [T0; T1; T0; TZ; T1; T0; T0; TZ; T1; T0; TZ; T1; TZ; T1; T0; T1] I eq_refl l (const 0)).
		471	- exists false; exists false; exists false; exists true; exists false; exists true; exists b10; exists b11; exists b12; exists b13; exists b14; exists b15; exists e. reflexivity. }
		472	destruct b10. 2: {
		473	left. exists (tw (tailw true false false true false false false true false true b11 b12 b13 b14 b15 e) *> const 0). split.
		474	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1; T1; TZ] (TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) E [T1; T0; T0; TZ; T1; T1; T0; TZ; T1; T0; TZ; T0; TZ; T1; T1; T0; TZ; T1] I eq_refl l (const 0)).
		475	- exists true; exists false; exists false; exists false; exists true; exists false; exists true; exists b11; exists b12; exists b13; exists b14; exists b15; exists e. reflexivity. }
		476	destruct b11. 2: {
		477	left. exists (tw (tailw true false false true false false false true false false true b12 b13 b14 b15 e) *> const 0). split.
		478	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1; T1; TZ; T1; TZ; T1] (TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) E [T1; T0; T0; TZ; T1; T1; T0; TZ; T1; T0; TZ; T0; TZ; T1; T1; T0; TZ; T0; TZ; T1; T1] I eq_refl l (const 0)).
		479	- exists true; exists false; exists false; exists false; exists true; exists false; exists false; exists true; exists b12; exists b13; exists b14; exists b15; exists e. reflexivity. }
		480	destruct b12. 2: {
		481	right. exists (tw ([T1; T0; TZ; T1; T0; T0; TZ; T1; T0; TZ; T1; TZ; T1; T0; T0; TZ; T1; TZ; T1; T0; TZ; T1] ++ (TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1])) *> const 0). split.
		482	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1; T1; TZ; T1; TZ; T1; T1; TZ] (TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) F [T0; T1; T0; TZ; T1; T0; T0; TZ; T1; T0; TZ; T1; TZ; T1; T0; T0; TZ; T1; TZ; T1; T0; TZ; T1] I eq_refl l (const 0)).
		483	- exists false; exists false; exists false; exists true; exists false; exists false; exists true; exists false; exists true; exists b13; exists b14; exists b15; exists e. reflexivity. }
		484	destruct b13. 2: {
		485	left. exists (tw (tailw true false false true false false false true false false false true true b14 b15 e) *> const 0). split.
		486	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1; T1; TZ; T1; TZ; T1; T1; TZ; T1; TZ] (TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) E [T1; T0; T0; TZ; T1; T1; T0; TZ; T1; T0; TZ; T0; TZ; T1; T1; T0; TZ; T0; TZ; T1; T0; TZ; T1; TZ; T1] I eq_refl l (const 0)).
		487	- exists true; exists false; exists false; exists false; exists true; exists false; exists false; exists false; exists true; exists true; exists b14; exists b15; exists e. reflexivity. }
		488	destruct b14. 2: {
		489	right. exists (tw ([T1; T0; TZ; T1; T0; T0; TZ; T1; T0; TZ; T1; TZ; T1; T0; T0; TZ; T1; TZ; T1; T0; TZ; T0; TZ; T1; TZ; T1] ++ (TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1])) *> const 0). split.
		490	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1; T1; TZ; T1; TZ; T1; T1; TZ; T1; TZ; T1; TZ] (TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1]) F [T0; T1; T0; TZ; T1; T0; T0; TZ; T1; T0; TZ; T1; TZ; T1; T0; T0; TZ; T1; TZ; T1; T0; TZ; T0; TZ; T1; TZ; T1] I eq_refl l (const 0)).
		491	- exists false; exists false; exists false; exists true; exists false; exists false; exists true; exists false; exists false; exists true; exists true; exists b15; exists e. reflexivity. }
		492	destruct b15. 2: {
		493	left. exists (tw (tailw true false false true false false false true false false false true false true true e) *> const 0). split.
		494	- intros l; exact (TailRet [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1; T1; TZ; T1; TZ; T1; T1; TZ; T1; TZ; T1; TZ; T1; TZ] (TZ :: T1 :: map bt e ++ [T1]) E [T1; T0; T0; TZ; T1; T1; T0; TZ; T1; T0; TZ; T0; TZ; T1; T1; T0; TZ; T0; TZ; T1; T0; TZ; T1; TZ; T0; TZ; T1; TZ; T1] I eq_refl l (const 0)).
		495	- exists true; exists false; exists false; exists false; exists true; exists false; exists false; exists false; exists true; exists false; exists true; exists true; exists e. reflexivity. }
		497	apply Tail11_end.
		498	Qed.
		500	( Composition of the return automaton *)
		501	Lemma retf_app_n n : forall ps1, length ps1 <= n -> forall m ps2 rs m1 rs1,
		502	retf m ps1 rs = (m1, [], rs1) -> retf m (ps1 ++ ps2) rs = retf m1 ps2 rs1.
		503	Proof.
		504	induction n as [\|n IH]; intros ps1 Hn m ps2 rs m1 rs1 Hr.
		505	- destruct ps1; [\|cbn in Hn; lia].
		506	destruct m; cbn in Hr; inversion Hr; subst; reflexivity.
		507	- destruct ps1 as [\|p ps1].
		508	{ destruct m; cbn in Hr; inversion Hr; subst; reflexivity. }
		509	cbn in Hn.
		510	destruct m, p; cbn in Hr; try discriminate.
		511	+ cbn [app retf]. apply (IH ps1 ltac:(lia) _ _ _ _ _ Hr).
		512	+ cbn [app retf]. apply (IH ps1 ltac:(lia) _ _ _ _ _ Hr).
		513	+ cbn [app retf]. apply (IH ps1 ltac:(lia) _ _ _ _ _ Hr).
		514	+ destruct ps1 as [\|[\|] ps1]; try discriminate.
		515	destruct rs as [\|[\| \|] rs]; try discriminate.
		516	cbn [app retf]. cbn in Hn. apply (IH ps1 ltac:(lia) _ _ _ _ _ Hr).
		517	Qed.
		518	Lemma retf_app m ps1 ps2 rs m1 rs1 :
		519	retf m ps1 rs = (m1, [], rs1) -> retf m (ps1 ++ ps2) rs = retf m1 ps2 rs1.
		520	Proof. intros. eapply retf_app_n; [apply le_n\|eassumption]. Qed.
		522	( Lemma RB: the return over the R block (proof.md section 4.3) *)
		523	Lemma RB_E2 n : forall rs, retf E ([PZ;P]^^(2*n)) rs = (E, [], [T0;TZ;T1;TZ]^^n ++ rs).
		524	Proof.
		525	induction n as [\|n IH]; intros rs; [reflexivity\|].
		526	replace (2 * S n) with (S (S (2 * n))) by lia. cbn [lpow app retf].
		527	rewrite IH. f_equal. f_equal. change (T0 :: TZ :: T1 :: TZ :: rs) with ([T0;TZ;T1;TZ] ++ rs).
		528	rewrite app_assoc, lpow_shift. reflexivity.
		529	Qed.
		530	Lemma RB_F2 n : forall rs, retf F ([PZ;P]^^(2*n)) (T0 :: rs) = (F, [], T0 :: [TZ;T0;TZ;T1]^^n ++ rs).
		531	Proof.
		532	induction n as [\|n IH]; intros rs; [reflexivity\|].
		533	replace (2 * S n) with (S (S (2 * n))) by lia. cbn [lpow app retf].
		534	rewrite IH. f_equal. f_equal. f_equal. change (TZ :: T0 :: TZ :: T1 :: rs) with ([TZ;T0;TZ;T1] ++ rs).
		535	rewrite app_assoc, lpow_shift. reflexivity.
		536	Qed.
		537	Lemma RB_E1 n rs : retf E ([PZ;P]^^(S (2*n))) rs = (F, [], T0 :: [TZ;T0;TZ;T1]^^n ++ TZ :: rs).
		538	Proof. cbn [lpow app retf]. apply RB_F2. Qed.
		539	Lemma RB_F1 n rs : retf F ([PZ;P]^^(S (2*n))) (T0 :: rs) = (E, [], [T0;TZ;T1;TZ]^^n ++ T0 :: TZ :: T1 :: rs).
		540	Proof. cbn [lpow app retf]. apply RB_E2. Qed.
		542	Lemma shift4 n : [T0;TZ;T1] ++ [TZ;T0;TZ;T1]^^n = [T0;TZ;T1;TZ]^^n ++ [T0;TZ;T1].
		543	Proof.
		544	induction n as [\|n IH]; [reflexivity\|].
		545	cbn [lpow]. change ([T0;TZ;T1] ++ [TZ;T0;TZ;T1] ++ [TZ;T0;TZ;T1]^^n) with
		546	([T0;TZ;T1;TZ] ++ ([T0;TZ;T1] ++ [TZ;T0;TZ;T1]^^n)).
		547	rewrite IH, app_assoc. reflexivity.
		548	Qed.
		550	( Digits, all-ones and all-zeros counters *)
		551	Definition dig (b : tok) (g : nat) : list tok := b :: TZ :: T1 :: repeat TZ g.
		552	Fixpoint LD (b : tok) (G : list nat) : list tok :=
		553	match G with [] => [] \| g :: G' => dig b g ++ LD b G' end.
		555	Lemma LD_app b G1 G2 : LD b (G1 ++ G2) = LD b G1 ++ LD b G2.
		556	Proof. induction G1; cbn; [\|rewrite IHG1, app_assoc]; reflexivity. Qed.
		557	Lemma LD_ones b r : LD b (repeat 1%nat r) = [b;TZ;T1;TZ]^^r.
		558	Proof. induction r; cbn; [\|rewrite IHr]; reflexivity. Qed.
		560	Lemma ctr_zero gs : ctr gs 0 = LD T0 gs ++ [T0].
		561	Proof.
		562	induction gs as [\|g gs IH]; [reflexivity\|]. cbn [ctr LD dig].
		563	change (Nat.div2 O) with O. rewrite IH, <- !app_assoc. reflexivity.
		564	Qed.
		565	Lemma ctr_ones gs : ctr gs (2 ^ S (length gs) - 1) = LD T1 gs ++ [T1].
		566	Proof.
		567	induction gs as [\|g gs IH]; [reflexivity\|].
		568	cbn [length]. replace (2 ^ S (S (length gs)) - 1) with (S (2 * (2 ^ S (length gs) - 1))).
		569	2: { rewrite (pow2S (S (length gs))). assert (0 < 2 ^ S (length gs)) by (apply Nat.neq_0_lt_0, Nat.pow_nonzero; lia). lia. }
		570	rewrite ctr_odd, IH. cbn [LD dig]. rewrite <- !app_assoc. reflexivity.
		571	Qed.
		573	Lemma noT0_LD1 G : noT0 (LD T1 G).
		574	Proof.
		575	induction G as [\|g G IH]; [exact I\|]. cbn [LD dig].
		576	cbn [app noT0]. induction g; cbn; auto.
		577	Qed.
		578	Lemma noT0_U q : noT0 ([T1;TZ]^^q).
		579	Proof. induction q; cbn; auto. Qed.
		580	Lemma noT0_TZ a : noT0 (repeat TZ a).
		581	Proof. induction a; cbn; auto. Qed.
		583	Lemma prc_TZ a : prc (repeat TZ a) = repeat PZ a.
		584	Proof.
		585	unfold prc. induction a as [\|a IH]; [reflexivity\|].
		586	cbn [repeat map rev]. rewrite IH. apply repeat_snoc.
		587	Qed.
		588	Lemma prc_U q : prc ([T1;TZ]^^q) = [PZ;P]^^q.
		589	Proof.
		590	induction q as [\|q IH]; [reflexivity\|].
		591	cbn [lpow]. rewrite prc_app, IH. change (prc [T1;TZ]) with [PZ;P].
		592	rewrite lpow_shift. reflexivity.
		593	Qed.
		594	Lemma prc_dig g : prc (dig T1 g) = repeat PZ g ++ [P; PZ; P].
		595	Proof. unfold dig. change (T1 :: TZ :: T1 :: repeat TZ g) with ([T1;TZ;T1] ++ repeat TZ g).
		596	rewrite prc_app, prc_TZ. reflexivity. Qed.
		597	Lemma prc_LD G : prc (LD T1 G) = flat_map (fun g => repeat PZ g ++ [P; PZ; P]) (rev G).
		598	Proof.
		599	induction G as [\|g G IH]; [reflexivity\|].
		600	cbn [LD rev]. rewrite prc_app, IH, prc_dig, flat_map_app. cbn. rewrite app_nil_r. reflexivity.
		601	Qed.
		603	(** the S-return through the processed large digits and the lead *)
		604	Lemma retf_dig g ps rs : retf E (repeat PZ g ++ [P; PZ; P] ++ ps) rs =
		605	retf E ps (dig T0 g ++ rs).
		606	Proof.
		607	revert rs. induction g as [\|g IH]; intros rs; [reflexivity\|].
		608	cbn [repeat app retf]. rewrite IH. f_equal. unfold dig. cbn [app repeat].
		609	change (TZ :: rs) with ([TZ] ++ rs). rewrite app_assoc, repeat_snoc. reflexivity.
		610	Qed.
		611	Lemma retf_LD G : forall ps rs, retf E (prc (LD T1 G) ++ ps) rs = retf E ps (LD T0 G ++ rs).
		612	Proof.
		613	induction G as [\|g G IH]; intros ps rs; [reflexivity\|].
		614	cbn [LD]. rewrite prc_app, <- app_assoc, IH, prc_dig, <- app_assoc, retf_dig.
		615	rewrite app_assoc. reflexivity.
		616	Qed.
		617	Lemma retf_lead a rs : retf E (repeat PZ a ++ [P]) rs = (F, [], T0 :: repeat TZ a ++ rs).
		618	Proof.
		619	revert rs. induction a as [\|a IH]; intros rs; [reflexivity\|].
		620	cbn [repeat app retf]. rewrite IH. cbn [app repeat].
		621	change (TZ :: rs) with ([TZ] ++ rs). rewrite app_assoc, repeat_snoc. reflexivity.
		622	Qed.
		624	Lemma AT0p l r : l {{A}}> [0;0] > r -->+ l < [0;1] {{C}}> r. Proof. es. Qed.
		625	Lemma OvSweep w : noT0 w -> forall l S,
		626	l {{A}}> tw (T0 :: w) > S -->+ l < pl (prc w ++ [P]) {{C}}> S.
		627	Proof.
		628	intros Hw l S.
		629	rewrite tw_cons. cbn [tokw]. rewrite Str_app_assoc.
		630	eapply progress_evstep_trans; [apply AT0p\|].
		631	follow (Csweep w Hw).
		632	rewrite pl_app, Str_app_assoc. finish.
		633	Qed.
		635	( The overflow core: sweep, tail, R block, boundary (proof.md 4.1-4.3) *)
		636	Definition sfx (H : bool) : list tok := if H then [TZ] else [TZ;T1;TZ].
		637	Definition gsof (G : list nat) (r1 : nat) : list nat := G ++ 2%nat :: repeat 1%nat r1.
		638	Definition qof (H : bool) (r1 : nat) : nat := if H then S (2 * r1) else 2 * S r1.
		639	Definition ones (gs : list nat) : nat := 2 ^ S (length gs) - 1.
		641	Lemma U2 r : [T1;TZ;T1;TZ]^^r = [T1;TZ]^^(2*r).
		642	Proof.
		643	induction r as [\|r IH]; [reflexivity\|].
		644	replace (2 * S r) with (S (S (2 * r))) by lia. cbn [lpow]. rewrite IH. reflexivity.
		645	Qed.
		647	Lemma body_ones G r1 H : ctr (gsof G r1) (ones (gsof G r1)) ++ sfx H =
		648	LD T1 G ++ dig T1 2 ++ [T1;TZ]^^(qof H r1).
		649	Proof.
		650	unfold ones, gsof. rewrite ctr_ones, LD_app. cbn [LD]. rewrite LD_ones, U2.
		651	rewrite <- !app_assoc. f_equal. f_equal. destruct H; cbn [qof sfx].
		652	- replace (S (2 * r1)) with (2 * r1 + 1) by lia. rewrite lpow_add. reflexivity.
		653	- replace (2 * S r1) with (2 * r1 + 2) by lia. rewrite lpow_add. reflexivity.
		654	Qed.
		656	Lemma body_zero G r1 : ctr (gsof G r1) 0 = LD T0 G ++ dig T0 2 ++ [T0;TZ;T1;TZ]^^r1 ++ [T0].
		657	Proof. unfold gsof. rewrite ctr_zero, LD_app. cbn [LD]. rewrite LD_ones, <- !app_assoc. reflexivity. Qed.
		659	Lemma noT0_w a G q : noT0 (repeat TZ a ++ LD T1 G ++ dig T1 2 ++ [T1;TZ]^^q).
		660	Proof.
		661	repeat apply noT0_app; auto using noT0_TZ, noT0_LD1, noT0_U. exact I.
		662	Qed.
		664	Lemma prc_w a G q : prc (repeat TZ a ++ LD T1 G ++ dig T1 2 ++ [T1;TZ]^^q) ++ [P] =
		665	[PZ;P]^^q ++ [PZ;PZ;P;PZ;P] ++ (prc (LD T1 G) ++ repeat PZ a ++ [P]).
		666	Proof.
		667	rewrite !prc_app, prc_U, prc_TZ, prc_dig. rewrite <- !app_assoc. reflexivity.
		668	Qed.
		670	Lemma BNp ps l r : l <* pl ([PZ;PZ;P;PZ;P] ++ ps) <{{F}} [0;0] > r -->
		671	l <* pl ps <* [1;0;1;0;0;1] {{A}}> [0;0;0;0;1;0;0;0;1] *> r.
		672	Proof.
		673	rewrite pl_app, Str_app_assoc. cbn [pl pw app].
		674	change [0;1;0;0;1;0;0;1;0;1;0;0;1] with ([0;1;0;0;1;0] ++ [0;1;0;1;0;0;1]).
		675	rewrite Str_app_assoc. follow BN. finish.
		676	Qed.
		678	Lemma OvN1 G r1 a l St St' : (forall l', l' {{C}}> St -->* l' <{{E}} St') ->
		679	l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx true) *> St -->+
		680	l <* pl (prc (LD T1 G) ++ repeat PZ a ++ [P]) <* [1;0;1;0;0;1] {{A}}>
		681	tw (T0 :: ctr (repeat 1%nat r1) 0 ++ sfx false) *> St'.
		682	Proof.
		683	intros Ht.
		684	rewrite body_ones.
		685	eapply progress_evstep_trans; [apply (OvSweep _ (noT0_w a G (qof true r1)) l St)\|].
		686	eapply evstep_trans; [apply Ht\|].
		687	rewrite prc_w.
		688	set (X := prc (LD T1 G) ++ repeat PZ a ++ [P]).
		689	assert (Hr : retf E ([PZ;P]^^(qof true r1) ++ [PZ;PZ;P;PZ;P] ++ X) [] =
		690	(F, [PZ;PZ;P;PZ;P] ++ X, T0 :: [TZ;T0;TZ;T1]^^r1 ++ [TZ])).
		691	{ cbn [qof]. rewrite (retf_app _ _ _ _ _ _ (RB_E1 r1 [])). reflexivity. }
		692	follow (retf_spec _ _ _ _ _ _ Hr l St').
		693	rewrite tw_cons. cbn [tokw]. rewrite Str_app_assoc.
		694	follow BNp.
		695	rewrite ctr_zero, LD_ones.
		696	replace (T0 :: ([T0;TZ;T1;TZ]^^r1 ++ [T0]) ++ sfx false) with
		697	([T0;T0;TZ;T1] ++ [TZ;T0;TZ;T1]^^r1 ++ [TZ]).
		698	2: { cbn [sfx]. rewrite <- !app_assoc. change ([T0;T0;TZ;T1] ++ ([TZ;T0;TZ;T1]^^r1 ++ [TZ]))
		699	with (T0 :: ([T0;TZ;T1] ++ [TZ;T0;TZ;T1]^^r1) ++ [TZ]). rewrite shift4, <- !app_assoc. reflexivity. }
		700	rewrite !tw_app, !Str_app_assoc. finish.
		701	Qed.
		703	Lemma OvN0 G r1 a l St S0 : (forall l', l' {{C}}> St -->* l' <{{F}} [0;0] *> S0) ->
		704	l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx false) *> St -->+
		705	l <* pl (prc (LD T1 G) ++ repeat PZ a ++ [P]) <* [1;0;1;0;0;1] {{A}}>
		706	tw (T0 :: ctr (repeat 1%nat (S r1)) 0 ++ sfx true) > ([0;1] > S0).
		707	Proof.
		708	intros Ht.
		709	rewrite body_ones.
		710	eapply progress_evstep_trans; [apply (OvSweep _ (noT0_w a G (qof false r1)) l St)\|].
		711	eapply evstep_trans; [apply Ht\|].
		712	rewrite prc_w.
		713	set (X := prc (LD T1 G) ++ repeat PZ a ++ [P]).
		714	assert (Hr : retf F ([PZ;P]^^(qof false r1) ++ [PZ;PZ;P;PZ;P] ++ X) [T0] =
		715	(F, [PZ;PZ;P;PZ;P] ++ X, T0 :: [TZ;T0;TZ;T1]^^(S r1) ++ [])).
		716	{ cbn [qof]. rewrite (retf_app _ _ _ _ _ _ (RB_F2 (S r1) [])). reflexivity. }
		717	follow (retf_spec _ _ _ _ _ _ Hr l S0).
		718	rewrite tw_cons. cbn [tokw]. rewrite Str_app_assoc.
		719	follow BNp.
		720	assert (E : tw (T0 :: ctr (repeat 1%nat (S r1)) 0 ++ sfx true) > ([0;1] > S0) =
		721	tw ([T0;T0;TZ;T1] ++ [TZ;T0;TZ;T1]^^(S r1)) *> S0).
		722	{ change ([0;1] > S0) with (tw [T1] > S0). rewrite <- Str_app_assoc, <- tw_app.
		723	f_equal. f_equal. rewrite ctr_zero, LD_ones. cbn [sfx]. rewrite <- !app_assoc. cbn [app].
		724	f_equal. rewrite <- !app_assoc. cbn [app]. rewrite <- shift4. reflexivity. }
		725	rewrite E, app_nil_r, !tw_app, !Str_app_assoc. finish.
		726	Qed.
		728	Lemma OvS1 G r1 a l St S0 : (forall l', l' {{C}}> St -->* l' <{{F}} [0;0] *> S0) ->
		729	l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx true) *> St -->+
		730	l <{{F}} tw (T0 :: repeat TZ a ++ ctr (gsof G r1) 0 ++ sfx true) > ([0;1] > S0).
		731	Proof.
		732	intros Ht.
		733	rewrite body_ones.
		734	eapply progress_evstep_trans; [apply (OvSweep _ (noT0_w a G (qof true r1)) l St)\|].
		735	eapply evstep_trans; [apply Ht\|].
		736	rewrite prc_w.
		737	assert (Hr : retf F ([PZ;P]^^(qof true r1) ++ [PZ;PZ;P;PZ;P] ++ prc (LD T1 G) ++ repeat PZ a ++ [P]) [T0] =
		738	(F, [], T0 :: repeat TZ a ++ LD T0 G ++ dig T0 2 ++ [T0;TZ;T1;TZ]^^r1 ++ [T0;TZ;T1])).
		739	{ cbn [qof]. rewrite (retf_app _ _ _ _ _ _ (RB_F1 r1 [])).
		740	change [PZ;PZ;P;PZ;P] with (repeat PZ 2 ++ [P;PZ;P]). rewrite <- app_assoc, retf_dig, retf_LD, retf_lead.
		741	rewrite <- ?app_assoc. reflexivity. }
		742	assert (E : tw (T0 :: repeat TZ a ++ ctr (gsof G r1) 0 ++ sfx true) > ([0;1] > S0) =
		743	tw (T0 :: repeat TZ a ++ LD T0 G ++ dig T0 2 ++ [T0;TZ;T1;TZ]^^r1 ++ [T0;TZ;T1]) *> S0).
		744	{ change ([0;1] > S0) with (tw [T1] > S0). rewrite <- Str_app_assoc, <- tw_app.
		745	f_equal. f_equal. rewrite body_zero. cbn [sfx app]. rewrite <- !app_assoc. cbn [app]. reflexivity. }
		746	rewrite E.
		747	follow (retf_spec _ _ _ _ _ _ Hr l S0).
		748	finish.
		749	Qed.
		751	Ltac fw H := eapply evstep_trans; [exact H\|].
		753	( Macro steps: configurations IR in normal mode (W = 0inf) and pause mode *)
		754	Definition KP (W : side) (p : nat) (gs : list nat) (v : nat) (H : bool) (St : side) : Q * tape :=
		755	W {{A}}> tw (T0 :: repeat TZ p ++ ctr gs v ++ sfx H) *> St.
		756	Definition NN (gs : list nat) : nat := 2 ^ S (length gs).
		758	Lemma wall0 : (const 0 <* [1] : side) = Str_app [1;0] (Str_app [0] (const 0)).
		759	Proof. cbn. rewrite <- !const_unfold. reflexivity. Qed.
		761	Lemma P100 n l p gs v H St : S (S v) < NN gs ->
		762	KP (Str_app ([1] ++ [0;0;1]^^(S n)) l) p gs v H St -->*
		763	KP (Str_app ([1] ++ [0;0;1]^^n) l) (S p) gs (S (S v)) H St.
		764	Proof. intros Hv. exact (TwoInc gs v p (sfx H) (Str_app ([1] ++ [0;0;1]^^n) l) St Hv). Qed.
		766	Lemma P100s m : forall n l p gs v H St, 2 * m + v < NN gs ->
		767	KP (Str_app ([1] ++ [0;0;1]^^(m + n)) l) p gs v H St -->*
		768	KP (Str_app ([1] ++ [0;0;1]^^n) l) (m + p) gs (2 * m + v) H St.
		769	Proof.
		770	induction m as [\|m IH]; intros n l p gs v H St Hv; [finish\|].
		771	follow (P100 (m + n) l p gs v H St ltac:(lia)).
		772	follow (IH n l (S p) gs (S (S v)) H St ltac:(lia)).
		773	replace (m + S p) with (S m + p) by lia. replace (2 * m + S (S v)) with (2 * S m + v) by lia.
		774	finish.
		775	Qed.
		777	Lemma WX p gs v H St : S (S v) < NN gs ->
		778	KP (Str_app [1] (const 0)) p gs v H St -->* KP (const 0) (S p) gs (S (S v)) H St.
		779	Proof. intros Hv. unfold KP. rewrite wall0. exact (TwoInc gs v p (sfx H) (const 0) St Hv). Qed.
		781	Lemma Inc1 a gs v H St : S v < NN gs ->
		782	KP (const 0) (S a) gs v H St -->* KP (const 0) (S (S a)) gs (S v) H St.
		783	Proof.
		784	intros Hv. unfold KP.
		785	follow (IncL gs v (S a) Hv).
		786	cbn [repeat app]. rewrite !tw_cons. cbn [tokw]. rewrite !Str_app_assoc.
		787	follow Bnc. finish.
		788	Qed.
		790	Lemma Incs m : forall a gs v H St, m + v < NN gs ->
		791	KP (const 0) (S a) gs v H St -->* KP (const 0) (m + S a) gs (m + v) H St.
		792	Proof.
		793	induction m as [\|m IH]; intros a gs v H St Hv; [finish\|].
		794	follow (Inc1 a gs v H St ltac:(lia)).
		795	follow (IH (S a) gs (S v) H St ltac:(lia)).
		796	replace (m + S (S a)) with (S m + S a) by lia. replace (m + S v) with (S m + v) by lia.
		797	finish.
		798	Qed.
		800	(** zones: Zn(g) 1001 packed in the wall, innermost first *)
		801	Fixpoint zw (L : list nat) : list Sym :=
		802	match L with [] => [] \| g :: L' => [1;0;0;1] ++ [0;1;0]^^(S g) ++ zw L' end.
		803	Fixpoint zv (L : list nat) (v : nat) : nat :=
		804	match L with [] => v \| g :: L' => zv L' (2 * v + 2 * g) end.
		805	Fixpoint zg (L : list nat) (p : nat) (gs : list nat) : list nat :=
		806	match L with [] => gs \| g :: L' => zg L' (g - 2) (S (S p) :: gs) end.
		807	Fixpoint zp (L : list nat) (p : nat) : nat :=
		808	match L with [] => p \| g :: L' => zp L' (g - 2) end.
		810	Lemma P010s m : forall X Y p gs v H St, 2 * m + v < NN gs ->
		811	KP (Str_app ([1;0] ++ [0;1;0]^^m ++ X) Y) p gs v H St -->*
		812	KP (Str_app ([1;0] ++ X) Y) (m + p) gs (2 * m + v) H St.
		813	Proof.
		814	induction m as [\|m IH]; intros X Y p gs v H St Hv; [finish\|].
		815	follow (TwoInc gs v p (sfx H) (Str_app ([1;0] ++ [0;1;0]^^m ++ X) Y) St ltac:(unfold NN in Hv; lia)).
		816	follow (IH X Y (S p) gs (S (S v)) H St ltac:(lia)).
		817	replace (m + S p) with (S m + p) by lia. replace (2 * m + S (S v)) with (2 * S m + v) by lia.
		818	finish.
		819	Qed.
		821	Lemma Zone g L X Y p gs v H St : 2 <= g -> v + g < NN gs ->
		822	KP (Str_app ([1;0] ++ zw (g :: L) ++ X) Y) p gs v H St -->*
		823	KP (Str_app ([1;0] ++ zw L ++ X) Y) (g - 2) (S (S p) :: gs) (2 * v + 2 * g) H St.
		824	Proof.
		825	intros Hg Hv. destruct g as [\|[\|g]]; try lia. replace (S (S g) - 2) with g by lia.
		826	unfold KP at 1. cbn [zw]. rewrite <- !app_assoc.
		827	fw (ZXg gs v p (sfx H) (Str_app ([1;0] ++ [0;1;0]^^g ++ zw L ++ X) Y) St ltac:(unfold NN in *; lia)).
		828	fw (P010s g (zw L ++ X) Y 0 (S (S p) :: gs) (2 * S (S v)) H St ltac:(unfold NN in *; cbn [length]; rewrite pow2S; lia)).
		829	replace (g + 0) with g by lia. replace (2 * g + 2 * S (S v)) with (2 * v + 2 * S (S g)) by lia.
		830	finish.
		831	Qed.
		833	Lemma zv_ge L : forall v, 2 ^ length L * v <= zv L v.
		834	Proof.
		835	induction L as [\|g L IH]; intros v; cbn [zv length]; [rewrite Nat.pow_0_r; lia\|].
		836	specialize (IH (2 * v + 2 * g)). rewrite pow2S. nia.
		837	Qed.
		838	Lemma zg_len L : forall p gs, length (zg L p gs) = length L + length gs.
		839	Proof. induction L as [\|g L IH]; intros p gs; cbn [zg length]; [\|rewrite IH; cbn [length]]; lia. Qed.
		841	Lemma Zones L : Forall (le 2) L -> forall X Y p gs v H St,
		842	zv L v < 2 ^ (S (length gs) + length L) ->
		843	KP (Str_app ([1;0] ++ zw L ++ X) Y) p gs v H St -->*
		844	KP (Str_app ([1;0] ++ X) Y) (zp L p) (zg L p gs) (zv L v) H St.
		845	Proof.
		846	induction L as [\|g L IH]; intros HL X Y p gs v H St Hv; [finish\|].
		847	inversion HL as [\|? ? Hg HL']; subst.
		848	cbn [zv zg zp length] in *.
		849	assert (Hz := zv_ge L (2 * v + 2 * g)).
		850	assert (Hn : v + g < NN gs).
		851	{ unfold NN.
		852	assert (E : 2 ^ (S (length gs) + S (length L)) = 2 ^ length L * (2 * 2 ^ S (length gs))).
		853	{ rewrite Nat.add_succ_r, Nat.pow_succ_r', Nat.pow_add_r. ring. }
		854	rewrite E in Hv.
		855	assert (Hp : 0 < 2 ^ length L) by (apply Nat.neq_0_lt_0, Nat.pow_nonzero; lia).
		856	assert (H2 : 2 * v + 2 * g < 2 * 2 ^ S (length gs)).
		857	{ apply (Nat.mul_lt_mono_pos_l (2 ^ length L)); [exact Hp\|]. lia. }
		858	lia. }
		859	follow (Zone g L X Y p gs v H St Hg Hn).
		860	apply IH; [exact HL'\|]. cbn [length].
		861	replace (S (S (length gs)) + length L) with (S (length gs) + S (length L)) by lia. exact Hv.
		862	Qed.
		864	( Wall bookkeeping *)
		865	Fixpoint gval (G : list nat) : nat := match G with [] => 0 \| g :: G' => 2 * (g + gval G') end.
		867	Lemma zv_app L1 : forall L2 v, zv (L1 ++ L2) v = zv L2 (zv L1 v).
		868	Proof. induction L1; intros; cbn; auto. Qed.
		869	Lemma zp_app L1 : forall L2 p, zp (L1 ++ L2) p = zp L2 (zp L1 p).
		870	Proof. induction L1; intros; cbn; auto. Qed.
		871	Lemma zg_app L1 : forall L2 p gs, zg (L1 ++ L2) p gs = zg L2 (zp L1 p) (zg L1 p gs).
		872	Proof. induction L1; intros; cbn; auto. Qed.
		873	Lemma zw_app L1 L2 : zw (L1 ++ L2) = zw L1 ++ zw L2.
		874	Proof. induction L1; cbn; [\|rewrite IHL1, <- !app_assoc]; reflexivity. Qed.
		875	Lemma zv_rev G : zv (rev G) 0 = gval G.
		876	Proof. induction G as [\|g G IH]; [reflexivity\|]. cbn [rev gval]. rewrite zv_app, IH. cbn. lia. Qed.
		877	Lemma zg_rev G gs0 : Forall (le 2) G -> S (S (zp (rev G) 0)) :: zg (rev G) 0 gs0 = G ++ 2%nat :: gs0.
		878	Proof.
		879	induction G as [\|g G IH]; intros HG; [reflexivity\|].
		880	inversion HG; subst. cbn [rev]. rewrite zp_app, zg_app. cbn [zp zg].
		881	rewrite (IH H2). cbn [app]. f_equal. lia.
		882	Qed.
		883	Lemma zp_rev_last G p : zp (rev G ++ [p]) 0 = p - 2.
		884	Proof. rewrite zp_app. reflexivity. Qed.
		885	Lemma zv_rev_last G p : zv (rev G ++ [p]) 0 = 2 * gval G + 2 * p.
		886	Proof. rewrite zv_app, zv_rev. reflexivity. Qed.
		887	Lemma zg_rev_last G p gs0 : Forall (le 2) G -> zg (rev G ++ [p]) 0 gs0 = G ++ 2%nat :: gs0.
		888	Proof. intros HG. rewrite zg_app. cbn [zg]. apply zg_rev, HG. Qed.
		889	Lemma zg_len' L p gs : length (zg L p gs) = length L + length gs.
		890	Proof. apply zg_len. Qed.
		892	Lemma pl_lead a : pl (repeat PZ a ++ [P]) = [0;1] ++ [0;0;1]^^a.
		893	Proof. induction a as [\|a IH]; [reflexivity\|]. cbn [repeat app pl pw]. rewrite IH. reflexivity. Qed.
		895	Lemma pl_PZ g : pl (repeat PZ g) = [0;1;0]^^g.
		896	Proof. induction g; cbn; [\|rewrite IHg]; reflexivity. Qed.
		898	Lemma zw_LD_gen L : [1;0;0;1] ++ pl (flat_map (fun g => repeat PZ g ++ [P; PZ; P]) L) = zw L ++ [1;0;0;1].
		899	Proof.
		900	induction L as [\|g L IH]; [reflexivity\|].
		901	cbn [flat_map zw]. rewrite !pl_app, pl_PZ. change (pl [P;PZ;P]) with ([0;1;0] ++ [1;0;0;1]).
		902	rewrite <- !app_assoc. rewrite IH. f_equal.
		903	rewrite app_assoc, lpow_shift. reflexivity.
		904	Qed.
		906	Lemma wallOv G W l : (l <* pl (prc (LD T1 G) ++ W) <* [1;0;1;0;0;1] : side) =
		907	Str_app ([1;0] ++ zw (rev G) ++ [1;0;0;1] ++ pl W) l.
		908	Proof.
		909	rewrite <- Str_app_assoc. f_equal.
		910	rewrite pl_app, prc_LD. change [1;0;1;0;0;1] with ([1;0] ++ [1;0;0;1]).
		911	rewrite <- app_assoc, (app_assoc [1;0;0;1]), zw_LD_gen, <- !app_assoc. reflexivity.
		912	Qed.
		914	Lemma wallPO G p n l : Str_app ([1;0] ++ zw (rev G) ++ [1;0;0;1] ++ pl (repeat PZ p ++ [P]))
		915	(Str_app ([0;0;0;1] ++ [0;0;1]^^n) l) =
		916	Str_app ([1;0] ++ zw (rev G ++ [p]) ++ [0;0;1]^^(S n)) l.
		917	Proof.
		918	rewrite <- Str_app_assoc. f_equal.
		919	rewrite zw_app, pl_app, pl_PZ. cbn [zw]. rewrite app_nil_r, <- !app_assoc.
		920	f_equal. f_equal. f_equal.
		921	change (pl [P] ++ [0;0;0;1] ++ [0;0;1]^^n) with ([0;1;0] ++ [0;0;1] ++ [0;0;1]^^n).
		922	rewrite app_assoc, lpow_shift. reflexivity.
		923	Qed.
		925	(** ends of the rebuild *)
		926	Lemma ZXN a l p gs v H St : S (S v) < NN gs ->
		927	KP (Str_app ([1;0] ++ [1;0;0;1] ++ pl (repeat PZ (S (S a)) ++ [P])) l) p gs v H St -->*
		928	KP (Str_app ([1] ++ [0;0;1]^^a) l) 0 (S (S p) :: gs) (2 * S (S v)) H St.
		929	Proof.
		930	intros Hv. unfold KP at 1. rewrite pl_lead.
		931	exact (ZXg gs v p (sfx H) (Str_app ([1] ++ [0;0;1]^^a) l) St Hv).
		932	Qed.
		934	Lemma ZXP n l p gs v H St : S (S (S v)) < NN gs ->
		935	KP (Str_app ([1;0] ++ [0;0;1]^^(S (S (S n)))) l) p gs v H St -->*
		936	KP (Str_app ([1] ++ [0;0;1]^^n) l) 0 (S p :: gs) (2 * S (S (S v))) H St.
		937	Proof.
		938	intros Hv.
		939	fw (TwoInc gs v p (sfx H) (Str_app ([0;1] ++ [0;0;1]^^(S (S n))) l) St ltac:(unfold NN in Hv; lia)).
		940	exact (ZXP2g gs (S (S v)) (S p) (sfx H) (Str_app ([1] ++ [0;0;1]^^n) l) St Hv).
		941	Qed.
		943	( NO, PO, SILENT, SILENTP with their rebuilds (proof.md 4.3, 5.2) *)
		944	Definition OvNp (H : bool) (r1 : nat) (St : side) (H' : bool) (r1' : nat) (St' : side) : Prop :=
		945	forall G a l, l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx H) *> St -->+
		946	l <* pl (prc (LD T1 G) ++ repeat PZ a ++ [P]) <* [1;0;1;0;0;1] {{A}}>
		947	tw (T0 :: ctr (repeat 1%nat r1') 0 ++ sfx H') *> St'.
		948	Definition OvSp (r1 : nat) (St St' : side) : Prop :=
		949	forall G a l, l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx true) *> St -->+
		950	l <{{F}} tw (T0 :: repeat TZ a ++ ctr (gsof G r1) 0 ++ sfx true) *> St'.
		952	Lemma OvNp1 r1 St St' : (forall l', l' {{C}}> St -->* l' <{{E}} St') -> OvNp true r1 St false r1 St'.
		953	Proof. intros Ht G a l. apply OvN1, Ht. Qed.
		954	Lemma OvNp0 r1 St S0 : (forall l', l' {{C}}> St -->* l' <{{F}} [0;0] *> S0) ->
		955	OvNp false r1 St true (S r1) ([0;1] *> S0).
		956	Proof. intros Ht G a l. apply OvN0, Ht. Qed.
		957	Lemma OvSp1 r1 St S0 : (forall l', l' {{C}}> St -->* l' <{{F}} [0;0] > S0) -> OvSp r1 St ([0;1] > S0).
		958	Proof. intros Ht G a l. apply OvS1, Ht. Qed.
		960	Lemma len_gsof G r1 : length (gsof G r1) = length G + S r1.
		961	Proof. unfold gsof. rewrite length_app. cbn [length]. rewrite repeat_length. lia. Qed.
		962	Lemma pow_pos n : 0 < 2 ^ n.
		963	Proof. apply Nat.neq_0_lt_0, Nat.pow_nonzero. lia. Qed.
		965	Lemma NOrb H r1 St H' r1' St' G a : OvNp H r1 St H' r1' St' -> Forall (le 2) G ->
		966	gval G + 2 < 2 ^ (length G + S r1') ->
		967	KP (const 0) (S (S a)) (gsof G r1) (ones (gsof G r1)) H St -->+
		968	KP (Str_app ([1] ++ [0;0;1]^^a) (const 0)) 0 (gsof G r1') (2 * gval G + 4) H' St'.
		969	Proof.
		970	intros Hov HG Hv.
		971	eapply progress_evstep_trans; [exact (Hov G (S (S a)) (const 0))\|].
		972	rewrite wallOv.
		973	assert (HGr : Forall (le 2) (rev G)) by (apply Forall_rev, HG).
		974	assert (Hz : zv (rev G) 0 < 2 ^ (S (length (repeat 1%nat r1')) + length (rev G))).
		975	{ rewrite zv_rev, repeat_length, length_rev. replace (S r1' + length G) with (length G + S r1') by lia. lia. }
		976	fw (Zones (rev G) HGr ([1;0;0;1] ++ pl (repeat PZ (S (S a)) ++ [P])) (const 0) 0 (repeat 1%nat r1') 0 H' St' Hz).
		977	assert (Hx : S (S (zv (rev G) 0)) < NN (zg (rev G) 0 (repeat 1%nat r1'))).
		978	{ unfold NN. rewrite zg_len, zv_rev, repeat_length, length_rev.
		979	replace (S (length G + r1')) with (length G + S r1') by lia. lia. }
		980	fw (ZXN a (const 0) (zp (rev G) 0) (zg (rev G) 0 (repeat 1%nat r1')) (zv (rev G) 0) H' St' Hx).
		981	rewrite zg_rev by exact HG. rewrite zv_rev.
		982	replace (2 * S (S (gval G))) with (2 * gval G + 4) by lia.
		983	finish.
		984	Qed.
		986	Lemma ones_S gs : S (ones gs - 1) = ones gs.
		987	Proof. unfold ones. assert (H := pow_pos (S (length gs))). rewrite pow2S in *. lia. Qed.
		988	Lemma ones_lt gs : ones gs < NN gs.
		989	Proof. unfold ones, NN. assert (H := pow_pos (S (length gs))). lia. Qed.
		991	Lemma POrb H r1 St H' r1' St' G p n l0 : OvNp H r1 St H' r1' St' -> Forall (le 2) G -> 2 <= p ->
		992	2 * gval G + 2 * p + 3 < 2 ^ (length G + S (S r1')) ->
		993	KP (Str_app ([1] ++ [0;0;1]^^(S (S (S n)))) l0) p (gsof G r1) (ones (gsof G r1) - 1) H St -->*
		994	KP (Str_app ([1] ++ [0;0;1]^^n) l0) 0 (gsof (S (p - 2) :: G) r1') (2 * S (S (S (2 * gval G + 2 * p)))) H' St'.
		995	Proof.
		996	intros Hov HG Hp Hv.
		997	assert (HI : S (ones (gsof G r1) - 1) < 2 ^ S (length (gsof G r1))) by (rewrite ones_S; apply ones_lt).
		998	fw (IncL (gsof G r1) (ones (gsof G r1) - 1) p HI (Str_app ([1] ++ [0;0;1]^^(S (S (S n)))) l0) St (sfx H)).
		999	rewrite ones_S.
		1000	fw (B1 (Str_app ([0;1] ++ [0;0;1]^^(S (S n))) l0) (tw (T0 :: repeat TZ p ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx H) *> St)).
		1001	fw (progress_evstep _ _ _ (Hov G p (Str_app [0;0] (Str_app ([0;1] ++ [0;0;1]^^(S (S n))) l0)))).
		1002	rewrite wallOv.
		1003	replace (Str_app [0;0] (Str_app ([0;1] ++ [0;0;1]^^(S (S n))) l0)) with
		1004	(Str_app ([0;0;0;1] ++ [0;0;1]^^(S (S n))) l0) by (rewrite <- Str_app_assoc; reflexivity).
		1005	rewrite wallPO.
		1006	assert (HGr : Forall (le 2) (rev G ++ [p])) by (apply Forall_app; split; [apply Forall_rev, HG \| auto]).
		1007	assert (Hz : zv (rev G ++ [p]) 0 < 2 ^ (S (length (repeat 1%nat r1')) + length (rev G ++ [p]))).
		1008	{ rewrite zv_rev_last, repeat_length, length_app, length_rev. cbn [length].
		1009	replace (S r1' + (length G + 1)) with (length G + S (S r1')) by lia. lia. }
		1010	fw (Zones (rev G ++ [p]) HGr ([0;0;1]^^(S (S (S n)))) l0 0 (repeat 1%nat r1') 0 H' St' Hz).
		1011	assert (Hx : S (S (S (zv (rev G ++ [p]) 0))) < NN (zg (rev G ++ [p]) 0 (repeat 1%nat r1'))).
		1012	{ unfold NN. rewrite zg_len, zv_rev_last, repeat_length, length_app, length_rev. cbn [length].
		1013	replace (S (length G + 1 + r1')) with (length G + S (S r1')) by lia. lia. }
		1014	fw (ZXP n l0 (zp (rev G ++ [p]) 0) (zg (rev G ++ [p]) 0 (repeat 1%nat r1')) (zv (rev G ++ [p]) 0) H' St' Hx).
		1015	rewrite zp_rev_last, zg_rev_last, zv_rev_last by exact HG.
		1016	finish.
		1017	Qed.
		1019	Lemma SILENTP r1 St St' G p n l0 : OvSp r1 St St' ->
		1020	KP (Str_app ([1] ++ [0;0;1]^^(S n)) l0) p (gsof G r1) (ones (gsof G r1) - 1) true St -->*
		1021	KP (Str_app ([1] ++ [0;0;1]^^n) l0) (S p) (gsof G r1) 0 true St'.
		1022	Proof.
		1023	intros Hov.
		1024	assert (HI : S (ones (gsof G r1) - 1) < 2 ^ S (length (gsof G r1))) by (rewrite ones_S; apply ones_lt).
		1025	fw (IncL (gsof G r1) (ones (gsof G r1) - 1) p HI (Str_app ([1] ++ [0;0;1]^^(S n)) l0) St (sfx true)).
		1026	rewrite ones_S.
		1027	fw (B1 (Str_app ([0;1] ++ [0;0;1]^^n) l0) (tw (T0 :: repeat TZ p ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx true) *> St)).
		1028	fw (progress_evstep _ _ _ (Hov G p (Str_app [0;0] (Str_app ([0;1] ++ [0;0;1]^^n) l0)))).
		1029	fw (ENDl (Str_app ([0;1] ++ [0;0;1]^^n) l0) (tw (T0 :: repeat TZ p ++ ctr (gsof G r1) 0 ++ sfx true) *> St')).
		1030	unfold KP. cbn [repeat app]. rewrite !tw_cons. cbn [tokw]. rewrite !Str_app_assoc.
		1031	finish.
		1032	Qed.
		1034	Lemma SILENT r1 St St' G a : OvSp r1 St St' ->
		1035	KP (const 0) (S a) (gsof G r1) (ones (gsof G r1)) true St -->+ KP (const 0) (S (S a)) (gsof G r1) 0 true St'.
		1036	Proof.
		1037	intros Hov.
		1038	eapply progress_evstep_trans; [exact (Hov G (S a) (const 0))\|].
		1039	unfold KP. cbn [repeat app]. rewrite !tw_cons. cbn [tokw]. rewrite !Str_app_assoc.
		1040	follow Bnc. finish.
		1041	Qed.
		1043	( The four paths between normal-mode overflows (proof.md section 5.2) *)
		1044	Definition KX (a : nat) (G : list nat) (r1 : nat) (St : side) : Q * tape :=
		1045	KP (const 0) a (gsof G r1) (ones (gsof G r1)) true St.
		1047	Lemma pS k r : 2 ^ (k + S r) = 2 * 2 ^ (k + r).
		1048	Proof. rewrite Nat.add_succ_r. apply Nat.pow_succ_r'. Qed.
		1049	Lemma NN_gsof G r1 : NN (gsof G r1) = 4 * 2 ^ (length G + r1).
		1050	Proof. unfold NN. rewrite len_gsof, <- Nat.add_succ_r, pS, pS. lia. Qed.
		1051	Lemma ones_gsof G r1 : ones (gsof G r1) = 4 * 2 ^ (length G + r1) - 1.
		1052	Proof. rewrite <- NN_gsof. reflexivity. Qed.
		1053	Lemma Q_cons (g : nat) (G : list nat) r1 : 2 ^ (length (g :: G) + S r1) = 4 * 2 ^ (length G + r1).
		1054	Proof. cbn [length]. rewrite pS. rewrite Nat.add_succ_l, Nat.pow_succ_r'. lia. Qed.
		1056	Lemma KP_eq W p p' gs v v' H St : p = p' -> v = v' -> KP W p gs v H St = KP W p' gs v' H St.
		1057	Proof. intros -> ->. reflexivity. Qed.
		1059	Lemma pathS a G r1 St St' : OvSp r1 St St' -> 1 <= a ->
		1060	KX a G r1 St -->+ KX (a + 4 * 2 ^ (length G + r1)) G r1 St'.
		1061	Proof.
		1062	intros Hov Ha. unfold KX.
		1063	assert (HO := ones_gsof G r1). assert (HN := NN_gsof G r1). assert (HP := pow_pos (length G + r1)).
		1064	replace a with (S (a - 1)) at 1 by lia.
		1065	eapply progress_evstep_trans; [apply (SILENT r1 St St' G (a - 1) Hov)\|].
		1066	fw (Incs (ones (gsof G r1)) (S (a - 1)) (gsof G r1) 0 true St' ltac:(lia)).
		1067	rewrite (KP_eq _ _ (a + 4 * 2 ^ (length G + r1)) _ _ (ones (gsof G r1))) by lia.
		1068	finish.
		1069	Qed.
		1071	(** NO with e0, then the pause up to PO#1 and PO#1 with e1: common prefix of P1, P1S, P3 *)
		1072	Lemma pre1 a G r1 St St1 S0 kap s : let Q := 2 ^ (length G + r1) in
		1073	OvNp true r1 St false r1 St1 -> (forall l', l' {{C}}> St1 -->* l' <{{F}} [0;0] *> S0) ->
		1074	Forall (le 2) G -> gval G + 6 + kap = Q -> a = s + Q + kap -> 8 <= s ->
		1075	KX a G r1 St -->+
		1076	KP (Str_app ([1] ++ [0;0;1]^^(s - 8)) (const 0)) 0 (gsof ((Q + 2 + kap) :: G) (S r1)) (8 * Q - 6) true ([0;1] *> S0).
		1077	Proof.
		1078	intros Q Hov1 Ht2 HG HV Ha Hs. unfold KX.
		1079	assert (HO := ones_gsof G r1). assert (HN := NN_gsof G r1). assert (HP := pow_pos (length G + r1)).
		1080	fold Q in HO, HN, HP.
		1081	replace a with (S (S (a - 2))) at 1 by lia.
947	eapply progress_evstep_trans.	1082	eapply progress_evstep_trans.
948	{ apply (A4p (205 + (3 * N n - 1 + 3 * SN n)*3) l
		1083	{ apply (NOrb true r1 St false r1 St1 G (a - 2) Hov1 HG). rewrite pS. fold Q. lia. }
949	([1]^^(68 + (3 * N n - 1 + 3 * SN n)) *> const 0)). }
		1084	replace (a - 2) with ((Q + 3 + kap) + S (S (S (s - 8)))) by lia.
950	simpl N. finish.
		1085	fw (P100s (Q + 3 + kap) (S (S (S (s - 8)))) (const 0) 0 (gsof G r1) (2 * gval G + 4) false St1 ltac:(lia)).
		1086	rewrite (KP_eq _ _ (Q + 3 + kap) _ _ (ones (gsof G r1) - 1)) by lia.
		1087	fw (POrb false r1 St1 true (S r1) ([0;1] *> S0) G (Q + 3 + kap) (s - 8) (const 0) (OvNp0 r1 St1 S0 Ht2) HG
		1088	ltac:(lia) ltac:(rewrite !pS; fold Q; lia)).
		1089	replace (S (Q + 3 + kap - 2)) with (Q + 2 + kap) by lia.
		1090	rewrite (KP_eq _ _ 0 _ _ (8 * Q - 6)) by lia.
		1091	finish.
951	Qed.	1092	Qed.
953	( Traj(k) for all k, by strong induction *)
		1094	Definition TailF (St S0 : side) : Prop := forall l', l' {{C}}> St -->* l' <{{F}} [0;0] *> S0.
954	Lemma Traj_all : forall n, Traj n.
		1096	Lemma gval_cons g G : gval (g :: G) = 2 * (g + gval G).
		1097	Proof. reflexivity. Qed.
		1099	Lemma pathP1 a G r1 St St1 S0 kap s : let Q := 2 ^ (length G + r1) in
		1100	OvNp true r1 St false r1 St1 -> TailF St1 S0 ->
		1101	Forall (le 2) G -> gval G + 6 + kap = Q -> a = s + Q + kap -> 8 <= s -> s <= 4 * Q + 9 ->
		1102	KX a G r1 St -->+ KX (8 * Q + 12 - s) ((Q + 2 + kap) :: G) (S r1) ([0;1] *> S0).
955	Proof.	1103	Proof.
956	induction n as [n IH] using strong_induction.
		1104	intros Q Hov1 Ht2 HG HV Ha Hs1 Hs2.
957	destruct n as [\| n]. { apply Traj0. }
		1105	eapply progress_evstep_trans; [apply (pre1 a G r1 St St1 S0 kap s Hov1 Ht2 HG HV Ha Hs1)\|].
958	intros l. rewrite Dz_S.
		1106	fold Q. set (G' := (Q + 2 + kap) :: G).
959	rewrite <- lpow_app.
		1107	assert (HN : NN (gsof G' (S r1)) = 16 * Q) by (rewrite NN_gsof; unfold G'; rewrite Q_cons; fold Q; lia).
960	follow (IH n ltac:(lia) ([0]^^(Zs n) *> l)).
		1108	assert (HO : ones (gsof G' (S r1)) = 16 * Q - 1) by (unfold ones, NN in *; lia).
961	apply progress_evstep.
		1109	assert (HP := pow_pos (length G + r1)). fold Q in HP.
962	apply (Step n (fun m Hm => IH m ltac:(lia)) l).
		1110	replace (s - 8) with (s - 8 + 0) at 1 by lia.
		1111	fw (P100s (s - 8) 0 (const 0) 0 (gsof G' (S r1)) (8 * Q - 6) true ([0;1] *> S0) ltac:(lia)).
		1112	fw (WX (s - 8 + 0) (gsof G' (S r1)) (2 * (s - 8) + (8 * Q - 6)) true ([0;1] *> S0) ltac:(lia)).
		1113	fw (Incs (8 * Q + 19 - 2 * s) (s - 8 + 0) (gsof G' (S r1)) (S (S (2 * (s - 8) + (8 * Q - 6)))) true ([0;1] *> S0) ltac:(lia)).
		1114	unfold KX. rewrite (KP_eq _ _ (8 * Q + 12 - s) _ _ (ones (gsof G' (S r1)))) by lia.
		1115	finish.
963	Qed.	1116	Qed.
965	Lemma const_zeros : forall k, [0]^^k *> const 0 = const 0.
		1118	Lemma pathP1S a G r1 St St1 S0 St3 kap s : let Q := 2 ^ (length G + r1) in
		1119	OvNp true r1 St false r1 St1 -> TailF St1 S0 -> OvSp (S r1) ([0;1] *> S0) St3 ->
		1120	Forall (le 2) G -> gval G + 6 + kap = Q -> a = s + Q + kap -> 4 * Q + 11 <= s -> s <= 12 * Q + 9 ->
		1121	KX a G r1 St -->+ KX (24 * Q + 12 - s) ((Q + 2 + kap) :: G) (S r1) St3.
966	Proof.	1122	Proof.
967	induction k as [\| k IH]; [reflexivity \|].
		1123	intros Q Hov1 Ht2 Hov3 HG HV Ha Hs1 Hs2.
968	cbn [lpow app Str_app]. rewrite IH. symmetry. apply const_unfold.
		1124	eapply progress_evstep_trans; [apply (pre1 a G r1 St St1 S0 kap s Hov1 Ht2 HG HV Ha ltac:(lia))\|].
		1125	fold Q. set (G' := (Q + 2 + kap) :: G).
		1126	assert (HN : NN (gsof G' (S r1)) = 16 * Q) by (rewrite NN_gsof; unfold G'; rewrite Q_cons; fold Q; lia).
		1127	assert (HO : ones (gsof G' (S r1)) = 16 * Q - 1) by (unfold ones, NN in *; lia).
		1128	assert (HP := pow_pos (length G + r1)). fold Q in HP.
		1129	replace (s - 8) with ((4 * Q + 2) + S (s - 4 * Q - 11)) at 1 by lia.
		1130	fw (P100s (4 * Q + 2) (S (s - 4 * Q - 11)) (const 0) 0 (gsof G' (S r1)) (8 * Q - 6) true ([0;1] *> S0) ltac:(lia)).
		1131	rewrite (KP_eq _ _ (4 * Q + 2) _ _ (ones (gsof G' (S r1)) - 1)) by lia.
		1132	fw (SILENTP (S r1) ([0;1] > S0) St3 G' (4 Q + 2) (s - 4 * Q - 11) (const 0) Hov3).
		1133	replace (s - 4 * Q - 11) with (s - 4 * Q - 11 + 0) at 1 by lia.
		1134	fw (P100s (s - 4 * Q - 11) 0 (const 0) (S (4 * Q + 2)) (gsof G' (S r1)) 0 true St3 ltac:(lia)).
		1135	fw (WX (s - 4 * Q - 11 + S (4 * Q + 2)) (gsof G' (S r1)) (2 * (s - 4 * Q - 11) + 0) true St3 ltac:(lia)).
		1136	fw (Incs (24 * Q + 19 - 2 * s) (s - 4 * Q - 11 + S (4 * Q + 2)) (gsof G' (S r1))
		1137	(S (S (2 * (s - 4 * Q - 11) + 0))) true St3 ltac:(lia)).
		1138	unfold KX. rewrite (KP_eq _ _ (24 * Q + 12 - s) _ _ (ones (gsof G' (S r1)))) by lia.
		1139	finish.
969	Qed.	1140	Qed.
971	(** The landmarks of the actual blank-tape run. *)
		1142	Lemma pathP3 a G r1 St St1 S0 St3 S4 kap s : let Q := 2 ^ (length G + r1) in
972	Definition LM n : Q * tape := lm0 (const 0) 8 (3 * N n - 1) (N n - 1).
		1143	OvNp true r1 St false r1 St1 -> TailF St1 S0 ->
974	Theorem nonhalt : ~ halts tm c0.
		1144	OvNp true (S r1) ([0;1] *> S0) false (S r1) St3 -> TailF St3 S4 ->
		1145	Forall (le 2) G -> gval G + 6 + kap = Q -> a = s + Q + kap -> 4 * Q + 24 <= s -> s <= 36 * Q + 31 ->
		1146	KX a G r1 St -->+ KX (68 * Q + 40 - s) (7 :: (4 * Q + 1) :: (Q + 2 + kap) :: G) (S (S r1)) ([0;1] *> S4).
975	Proof.	1147	Proof.
976	apply multistep_nonhalt with (LM 0).
		1148	intros Q Hov1 Ht2 Hov3 Ht4 HG HV Ha Hs1 Hs2.
977	{ pose proof (Traj0 (const 0)) as H0.
		1149	eapply progress_evstep_trans; [apply (pre1 a G r1 St St1 S0 kap s Hov1 Ht2 HG HV Ha ltac:(lia))\|].
978	rewrite const_zeros in H0. exact H0. }
		1150	fold Q. set (G' := (Q + 2 + kap) :: G).
979	apply progress_nonhalt_simple with (C := LM). intro n. exists (S n).
		1151	assert (HP := pow_pos (length G + r1)). fold Q in HP.
980	pose proof (Step n (fun m _ => Traj_all m) (const 0)) as Hs.
		1152	assert (HN : NN (gsof G' (S r1)) = 16 * Q) by (rewrite NN_gsof; unfold G'; rewrite Q_cons; fold Q; lia).
981	rewrite const_zeros in Hs. exact Hs.
		1153	assert (HO : ones (gsof G' (S r1)) = 16 * Q - 1) by (unfold ones, NN in *; lia).
		1154	assert (HG' : Forall (le 2) G') by (constructor; [lia \| exact HG]).
		1155	assert (HV' : gval G' = 4 * Q - 8) by (unfold G'; rewrite gval_cons; lia).
		1156	assert (HL' : length G' = S (length G)) by reflexivity.
		1157	(* pause up to PO#2 *)
		1158	replace (s - 8) with ((4 * Q + 2) + S (S (S (s - 4 * Q - 13)))) at 1 by lia.
		1159	fw (P100s (4 * Q + 2) (S (S (S (s - 4 * Q - 13)))) (const 0) 0 (gsof G' (S r1)) (8 * Q - 6) true ([0;1] *> S0) ltac:(lia)).
		1160	rewrite (KP_eq _ _ (4 * Q + 2) _ _ (ones (gsof G' (S r1)) - 1)) by lia.
		1161	fw (POrb true (S r1) ([0;1] > S0) false (S r1) St3 G' (4 Q + 2) (s - 4 * Q - 13) (const 0) Hov3 HG'
		1162	ltac:(lia) ltac:(rewrite !pS, HL', Nat.add_succ_l, Nat.pow_succ_r'; fold Q; lia)).
		1163	replace (S (4 * Q + 2 - 2)) with (4 * Q + 1) by lia.
		1164	set (G'' := (4 * Q + 1) :: G').
		1165	assert (HN2 : NN (gsof G'' (S r1)) = 32 * Q).
		1166	{ rewrite NN_gsof. unfold G'', G'. cbn [length]. rewrite !Nat.add_succ_l, !Nat.pow_succ_r', !pS. fold Q. lia. }
		1167	assert (HO2 : ones (gsof G'' (S r1)) = 32 * Q - 1) by (unfold ones, NN in *; lia).
		1168	assert (HG'' : Forall (le 2) G'') by (constructor; [lia \| exact HG']).
		1169	assert (HV'' : gval G'' = 16 * Q - 14) by (unfold G''; rewrite gval_cons; lia).
		1170	assert (HL'' : length G'' = S (S (length G))) by reflexivity.
		1171	replace (s - 4 * Q - 13) with (8 + S (S (S (s - 4 * Q - 24)))) at 1 by lia.
		1172	fw (P100s 8 (S (S (S (s - 4 * Q - 24)))) (const 0) 0 (gsof G'' (S r1))
		1173	(2 * S (S (S (2 * gval G' + 2 * (4 * Q + 2))))) false St3 ltac:(lia)).
		1174	rewrite (KP_eq _ _ 8 _ _ (ones (gsof G'' (S r1)) - 1)) by lia.
		1175	fw (POrb false (S r1) St3 true (S (S r1)) ([0;1] > S4) G'' 8 (s - 4 Q - 24) (const 0) (OvNp0 (S r1) St3 S4 Ht4) HG''
		1176	ltac:(lia) ltac:(rewrite !pS, HL'', !Nat.add_succ_l, !Nat.pow_succ_r'; fold Q; lia)).
		1177	replace (S (8 - 2)) with 7 by lia.
		1178	set (G3 := 7 :: G'').
		1179	assert (HN3 : NN (gsof G3 (S (S r1))) = 128 * Q).
		1180	{ rewrite NN_gsof. unfold G3, G'', G'. cbn [length]. rewrite !Nat.add_succ_l, !Nat.pow_succ_r', !pS. fold Q. lia. }
		1181	assert (HO3 : ones (gsof G3 (S (S r1))) = 128 * Q - 1) by (unfold ones, NN in *; lia).
		1182	replace (s - 4 * Q - 24) with (s - 4 * Q - 24 + 0) at 1 by lia.
		1183	fw (P100s (s - 4 * Q - 24) 0 (const 0) 0 (gsof G3 (S (S r1))) (2 * S (S (S (2 * gval G'' + 2 * 8)))) true ([0;1] *> S4) ltac:(lia)).
		1184	fw (WX (s - 4 * Q - 24 + 0) (gsof G3 (S (S r1))) (2 * (s - 4 * Q - 24) + 2 * S (S (S (2 * gval G'' + 2 * 8)))) true ([0;1] *> S4) ltac:(lia)).
		1185	fw (Incs (72 * Q + 63 - 2 * s) (s - 4 * Q - 24 + 0) (gsof G3 (S (S r1)))
		1186	(S (S (2 * (s - 4 * Q - 24) + 2 * S (S (S (2 * gval G'' + 2 * 8)))))) true ([0;1] *> S4) ltac:(lia)).
		1187	unfold KX. rewrite (KP_eq _ _ (68 * Q + 40 - s) _ _ (ones (gsof G3 (S (S r1))))) by lia.
		1188	finish.
982	Qed.	1189	Qed.
984	Print Assumptions nonhalt.
		1191	( The invariant (proof.md section 5.3) and the induction step *)
		1192	Definition INV (a : nat) (G : list nat) (r1 : nat) (St : side) : Prop :=
		1193	Forall (le 2) G /\ 64 <= 2 ^ (length G + r1) /\
		1194	exists kap s, (kap = 2 \/ kap = 8) /\ gval G + 6 + kap = 2 ^ (length G + r1) /\
		1195	a = s + 2 ^ (length G + r1) + kap /\
		1196	((Lst true true St /\ 24 <= s <= 2 ^ (length G + r1) + 2) \/
		1197	(Lst true false St /\ ((8 <= s <= 4 * 2 ^ (length G + r1) - 14) \/
		1198	(4 * 2 ^ (length G + r1) + 24 <= s <= 8 * 2 ^ (length G + r1))))).
		1200	Lemma Lst_intro y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e :
		1201	Lst y z (tw (tailw true y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0).
		1202	Proof.
		1203	exists b4; exists b5; exists b6; exists b7; exists b8; exists b9; exists b10; exists b11;
		1204	exists b12; exists b13; exists b14; exists b15; exists e. reflexivity.
		1205	Qed.
		1207	Lemma Q1 (g : nat) G r1 : 2 ^ (length (g :: G) + S r1) = 4 * 2 ^ (length G + r1).
		1208	Proof. apply Q_cons. Qed.
		1209	Lemma Q3 (g1 g2 g3 : nat) G r1 : 2 ^ (length (g1 :: g2 :: g3 :: G) + S (S r1)) = 32 * 2 ^ (length G + r1).
		1210	Proof. cbn [length]. rewrite !Nat.add_succ_l, !Nat.pow_succ_r', !pS. lia. Qed.
		1212	Lemma step a G r1 St : INV a G r1 St ->
		1213	exists a' G' r1' St', KX a G r1 St -->+ KX a' G' r1' St' /\ INV a' G' r1' St'.
		1214	Proof.
		1215	intros (HG & HQ & kap & s & Hk & HV & Ha & Ht).
		1216	set (Q := 2 ^ (length G + r1)) in *.
		1217	destruct Ht as [(HL & Hs) \| (HL & Hs)].
		1218	- (* front unit 11 *)
		1219	destruct HL as (b4 & b5 & b6 & b7 & b8 & b9 & b10 & b11 & b12 & b13 & b14 & b15 & e & ->).
		1220	destruct (Tail11 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) as [(S' & HE & HL') \| (S0 & HF & HL')].
		1221	+ (* N: path P1 *)
		1222	destruct HL' as (c4 & c5 & c6 & c7 & c8 & c9 & c10 & c11 & c12 & c13 & c14 & c15 & e' & ->).
		1223	set (S0 := tw (tailx true false c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 e') *> const 0).
		1224	assert (Ht2 : TailF (tw (tailw true false false c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 e') *> const 0) S0)
		1225	by (intros l; apply Tail0z).
		1226	exists (8 * Q + 12 - s), ((Q + 2 + kap) :: G), (S r1), ([0;1] *> S0). split.
		1227	* apply (pathP1 a G r1 _ _ S0 kap s (OvNp1 r1 _ _ HE) Ht2 HG HV Ha); lia.
		1228	* split; [constructor; [lia\|exact HG]\|]. rewrite Q1. fold Q. split; [lia\|].
		1229	exists 2, (4 * Q + 10 - s). split; [auto\|]. rewrite gval_cons. split; [lia\|]. split; [lia\|].
		1230	right. split; [exact (Lst_intro true false c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 e')\|]. lia.
		1231	+ (* S: path S *)
		1232	exists (a + 4 * Q), G, r1, ([0;1] *> S0). split.
		1233	* apply (pathS a G r1 _ _ (OvSp1 r1 _ S0 HF)); lia.
		1234	* split; [exact HG\|]. fold Q. split; [lia\|].
		1235	exists kap, (s + 4 * Q). split; [auto\|]. split; [lia\|]. split; [lia\|].
		1236	right. split; [exact HL'\|]. lia.
		1237	- (* front unit 10 *)
		1238	destruct HL as (b4 & b5 & b6 & b7 & b8 & b9 & b10 & b11 & b12 & b13 & b14 & b15 & e & ->).
		1239	set (St1 := tw (tailw true false true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0).
		1240	assert (HE : forall l, l {{C}}> tw (tailw true true false b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 --> l <{{E}} St1)
		1241	by (intros l; apply Tail10).
		1242	set (S0 := tw (tailx true true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0).
		1243	assert (Ht2 : TailF St1 S0) by (intros l; apply Tail0z).
		1244	destruct Hs as [Hs \| Hs].
		1245	+ (* path P1 *)
		1246	exists (8 * Q + 12 - s), ((Q + 2 + kap) :: G), (S r1), ([0;1] *> S0). split.
		1247	* apply (pathP1 a G r1 _ St1 S0 kap s (OvNp1 r1 _ _ HE) Ht2 HG HV Ha); lia.
		1248	* split; [constructor; [lia\|exact HG]\|]. rewrite Q1. fold Q. split; [lia\|].
		1249	exists 2, (4 * Q + 10 - s). split; [auto\|]. rewrite gval_cons. split; [lia\|]. split; [lia\|].
		1250	left. split; [exact (Lst_intro true true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e)\|]. lia.
		1251	+ destruct (Tail11 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) as [(S3 & HE3 & HL3) \| (S3 & HF3 & HL3)].
		1252	* (* path P3 *)
		1253	destruct HL3 as (c4 & c5 & c6 & c7 & c8 & c9 & c10 & c11 & c12 & c13 & c14 & c15 & e' & ->).
		1254	set (S4 := tw (tailx true false c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 e') *> const 0).
		1255	assert (Ht4 : TailF (tw (tailw true false false c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 e') *> const 0) S4)
		1256	by (intros l; apply Tail0z).
		1257	exists (68 * Q + 40 - s), (7 :: (4 * Q + 1) :: (Q + 2 + kap) :: G), (S (S r1)), ([0;1] *> S4). split.
		1258	-- apply (pathP3 a G r1 _ St1 S0 _ S4 kap s (OvNp1 r1 _ _ HE) Ht2 (OvNp1 (S r1) _ _ HE3) Ht4 HG HV Ha); lia.
		1259	-- split; [repeat constructor; try lia; exact HG\|]. rewrite Q3. fold Q. split; [lia\|].
		1260	exists 8, (36 * Q + 32 - s). split; [auto\|]. rewrite !gval_cons. split; [lia\|]. split; [lia\|].
		1261	right. split; [exact (Lst_intro true false c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 e')\|]. lia.
		1262	* (* path P1S *)
		1263	exists (24 * Q + 12 - s), ((Q + 2 + kap) :: G), (S r1), ([0;1] *> S3). split.
		1264	-- apply (pathP1S a G r1 _ St1 S0 _ kap s (OvNp1 r1 _ _ HE) Ht2 (OvSp1 (S r1) _ S3 HF3) HG HV Ha); lia.
		1265	-- split; [constructor; [lia\|exact HG]\|]. rewrite Q1. fold Q. split; [lia\|].
		1266	exists 2, (20 * Q + 10 - s). split; [auto\|]. rewrite gval_cons. split; [lia\|]. split; [lia\|].
		1267	right. split; [exact HL3\|]. lia.
		1268	Qed.
		1270	( Initial segment and the theorem *)
		1271	Definition St0 : side :=
		1272	tw (tailw true true true true true true false true true true true false true false true [false; true; false]) *> const 0.
		1274	Lemma init : c0 -->* KX 121 [28%nat] 5 St0.
		1275	Proof. unfold KX, KP, St0. solve_init. Qed.
		1277	Lemma INV0 : INV 121 [28%nat] 5 St0.
		1278	Proof.
		1279	split; [repeat constructor; lia\|]. cbn [length]. split; [cbn; lia\|].
		1280	exists 2, 55. split; [auto\|]. cbn. split; [lia\|]. split; [lia\|].
		1281	left. split; [exact (Lst_intro true true true true true false true true true true false true false true [false; true; false])\|]. lia.
		1282	Qed.
		1284	Lemma nonhalt : ~ halts tm c0.
		1285	Proof.
		1286	apply multistep_nonhalt with (c' := KX 121 [28%nat] 5 St0); [exact init\|].
		1287	apply (progress_nonhalt_cond tm _ (121, [28%nat], 5, St0)
		1288	(fun '(a, G, r1, St) => KX a G r1 St) (fun '(a, G, r1, St) => INV a G r1 St)).
		1289	- intros [[[a G] r1] St] HI.
		1290	destruct (step a G r1 St HI) as (a' & G' & r1' & St' & Hs & HI').
		1291	exists (a', G', r1', St'). split; assumption.
		1292	- exact INV0.
		1293	Qed.
		1296	(*
		1297	```
		1298	0 1
		1299	A 1RB 0LF
		1300	B 0RC --- halting transition: B reads 1
		1301	C 1RD 0RA
		1302	D 1LE 0RC
		1303	E 0LA 0LE
		1304	F 1LE 1LB
		1306	Token view (right of the lead): T0 = 00, T1 = 01, TZ = 100 ; processed P = (10), PZ = (010).
		1307	counter ctr gs v = digits b 100 01 (100)^g with LSB leftmost (last digit = its bit only).
		1308	KP W p gs v H St := W A> 00 (100)^p <ctr gs v> <sfx H> St (W = 0^inf: normal mode)
		1309	KX a G r1 St := KP 0^inf a (G ++ 2 :: 1^r1) (all ones) 1 St (normal-mode overflow)
		1311	Inc1 KP 0^inf (a+1) gs v -->* KP 0^inf (a+2) gs (v+1) (v+1 < 2^N)
		1312	P100 (100)^(n+1) 1 \| p, v -->* (100)^n 1 \| p+1, v+2
		1313	WX 1 \| p, v -->* 0^inf \| p+1, v+2 (normal mode)
		1314	Zone g Y Zn(g) 1001 01 \| p, gs, v -->* Y 01 \| g-2, (p+2)::gs, 2v+2g
		1315	ZXN (100)^(a+2) 10100101 \| p, gs, v -->* (100)^a 1 \| 0, (p+2)::gs, 2v+4
		1316	ZXP (100)^(n+3) 01 \| p, gs, v -->* (100)^n 1 \| 0, (p+1)::gs, 2v+6
		1317	NO/PO overflow, tail answers N -->+ wall of zones, then Zones, ZXN / ZXP
		1318	SILENT overflow, tail answers S -->+ KP 0^inf (a+1) gs 0
		1319	SILENTP overflow in a pause, S -->* (100)^n 1 \| p+1, 0
		1321	pathS KX a G r1 St -->+ KX (a+M) G r1 St' front 11 -> 10
		1322	pathP1 KX a G r1 St -->+ KX (2M+12-s) ((Q+2+k)::G) (r1+1) St'' 10 -> 11, 11 -> 10
		1323	pathP1S KX a G r1 St -->+ KX (6M+12-s) ((Q+2+k)::G) (r1+1) St'' 10 -> 10
		1324	pathP3 KX a G r1 St -->+ KX (17M+40-s) (7::(4Q+1)::(Q+2+k)::G) (r1+2) St'' 10 -> 10
		1325	(Q = 2^(length G + r1), M = 4Q, k in {2,8}, a = s + Q + k)
		1326	```
		1327	*)

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

183 items in 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v (1327 lines): 142 Lemma, 28 Definition, 11 Fixpoint, 2 Inductive. Tags against the template: identical = same name and same text once each file's own TM string is <TM> (marked "except the TM string" when that is the only difference); adapted = same name, different text; new = no item of that name in the template part.

#	kind	name	statement (no proof body)	line	vs template
1	Definition	`tm`	Definition tm := Eval compute in (TM_from_str "1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB").	L40	identicalexcept the TM string
2	Inductive	`tok`	Inductive tok := T0 \| T1 \| TZ.	L49	new
3	Definition	`tokw`	Definition tokw (t : tok) : list Sym := match t with T0 => [0;0] \| T1 => [0;1] \| TZ => [1;0;0] end.	L50	new
4	Fixpoint	`tw`	Fixpoint tw (ts : list tok) : list Sym := match ts with [] => [] \| t :: ts => tokw t ++ tw ts end.	L52	new
5	Inductive	`ptok`	Inductive ptok := P \| PZ.	L55	new
6	Definition	`pw`	Definition pw (p : ptok) : list Sym := match p with P => [0;1] \| PZ => [0;1;0] end.	L56	new
7	Fixpoint	`pl`	Fixpoint pl (ps : list ptok) : list Sym := match ps with [] => [] \| p :: ps => pw p ++ pl ps end.	L57	new
8	Definition	`proc`	Definition proc (t : tok) : ptok := match t with TZ => PZ \| _ => P end.	L59	new
9	Lemma	`tw_app`	Lemma tw_app xs ys : tw (xs ++ ys) = tw xs ++ tw ys.	L61	new
10	Lemma	`tw_cons`	Lemma tw_cons x xs : tw (x :: xs) = tokw x ++ tw xs.	L63	new
11	Lemma	`pl_app`	Lemma pl_app xs ys : pl (xs ++ ys) = pl xs ++ pl ys.	L65	new
12	Lemma	`AT0`	Lemma AT0 l r : l {{A}}> [0;0] > r --> l <* [0;1] {{C}}> r.	L69	new
13	Lemma	`CT1`	Lemma CT1 l r : l {{C}}> [0;1] > r --> l <* [0;1] {{C}}> r.	L70	new
14	Lemma	`CTZ`	Lemma CTZ l r : l {{C}}> [1;0;0] > r --> l <* [0;1;0] {{C}}> r.	L71	new
15	Lemma	`CT0`	Lemma CT0 l r : l {{C}}> [0;0] > r --> l <{{E}} [0;1] *> r.	L72	new
16	Lemma	`EPZ`	Lemma EPZ l r : l <* [0;1;0] <{{E}} r -->* l <{{E}} [1;0;0] *> r.	L73	new
17	Lemma	`EP`	Lemma EP l r : l <* [0;1] <{{E}} r -->* l <{{F}} [0;0] *> r.	L74	new
18	Lemma	`FP`	Lemma FP l r : l <* [0;1] <{{F}} r -->* l <{{E}} [0;1] *> r.	L75	new
19	Lemma	`FPZP`	Lemma FPZP l r : l <* [0;1] <* [0;1;0] <{{F}} [0;0] > r --> l <{{E}} [0;0] > [1;0;0] > [0;1] *> r.	L76	new
20	Lemma	`ENDl`	Lemma ENDl l r : l <* [0;0] <{{F}} r -->* l <{{A}} [0;1] *> r.	L78	new
21	Lemma	`B1`	Lemma B1 l r : l <* [1;0] <{{F}} r -->* l <* [0;0] {{A}}> r.	L79	new
22	Lemma	`BN`	Lemma BN l r : l <* [0;1;0;0;1;0] <{{F}} [0;0] > r --> l <{{A}} [0;0;0;1;0;0;0;1] *> r.	L80	new
23	Lemma	`ENDZX`	Lemma ENDZX l r : l <* [0;0;1;0;0;1;0;1;0;0;1;0] <{{F}} r -->* l <{{A}} [0;0;0;1;0;0;0;1;1;0;0;1] *> r.	L81	new
24	Fixpoint	`noT0`	Fixpoint noT0 (ts : list tok) : Prop := match ts with [] => True \| T0 :: _ => False \| _ :: ts => noT0 ts end.	L84	new
25	Definition	`prc`	Definition prc (ts : list tok) : list ptok := rev (map proc ts).	L86	new
26	Lemma	`Csweep`	Lemma Csweep ts : noT0 ts -> forall l r, l {{C}}> tw ts > r --> l <* pl (prc ts) {{C}}> r.	L88	new
27	Fixpoint	`retf`	Fixpoint retf (m : Q) (ps : list ptok) (rs : list tok) {struct ps} : Q * list ptok * list tok := match m, ps with \| E, PZ :: ps' => retf E ps' (TZ :: rs) \| E, P :: ps' => retf F ps' (T0 :: rs) \| F, P :: ps' => retf E ps' (T1 :: rs) \| F, PZ :: P :: ps' => … +6 lines	L100	new
28	Lemma	`retf_spec_n`	Lemma retf_spec_n n : forall ps, length ps <= n -> forall m rs m' ps' rs', retf m ps rs = (m', ps', rs') -> forall l r, l <* pl ps <{{m}} tw rs > r --> l <* pl ps' <{{m'}} tw rs' *> r.	L113	new
29	Lemma	`retf_spec`	Lemma retf_spec ps m rs m' ps' rs' : retf m ps rs = (m', ps', rs') -> forall l r, l <* pl ps <{{m}} tw rs > r --> l <* pl ps' <{{m'}} tw rs' *> r.	L143	new
30	Lemma	`CTZ'`	Lemma CTZ' l r : l <* [] {{C}}> [1;0;0] > r --> l <* [0;1;0] <* [] {{C}}> r.	L149	new
31	Definition	`CTZs`	Definition CTZs := shift_rule_R _ _ _ _ _ CTZ'.	L150	new
32	Lemma	`EPZ'`	Lemma EPZ' l r : l <* [0;1;0] <{{E}} [] > r --> l <{{E}} [] > [1;0;0] > r.	L151	new
33	Definition	`EPZs`	Definition EPZs := shift_rule_L _ _ _ _ _ EPZ'.	L152	new
34	Lemma	`tw_Z`	Lemma tw_Z g : tw (repeat TZ g) = [1;0;0]^^g.	L154	new
35	Definition	`bit`	Definition bit (v : nat) : tok := if Nat.odd v then T1 else T0.	L158	new
36	Fixpoint	`ctr`	Fixpoint ctr (gs : list nat) (v : nat) : list tok := match gs with \| [] => [bit v] \| g :: gs' => bit v :: TZ :: T1 :: repeat TZ g ++ ctr gs' (Nat.div2 v) end.	L159	new
37	Lemma	`bit_even`	Lemma bit_even w : bit (2*w) = T0.	L165	new
38	Lemma	`bit_odd`	Lemma bit_odd w : bit (S (2*w)) = T1.	L167	new
39	Lemma	`ctr_even`	Lemma ctr_even g gs w : ctr (g :: gs) (2*w) = T0 :: TZ :: T1 :: repeat TZ g ++ ctr gs w.	L170	new
40	Lemma	`ctr_odd`	Lemma ctr_odd g gs w : ctr (g :: gs) (S (2*w)) = T1 :: TZ :: T1 :: repeat TZ g ++ ctr gs w.	L172	new
41	Lemma	`ctr_hd_even`	Lemma ctr_hd_even gs w : exists rest, ctr gs (2w) = T0 :: rest /\ ctr gs (S (2w)) = T1 :: rest.	L175	new
42	Lemma	`pow2S`	Lemma pow2S n : 2 ^ S n = 2 * 2 ^ n.	L182	new
43	Lemma	`IncC`	Lemma IncC gs : forall v, S v < 2 ^ S (length gs) -> forall l r t, l {{C}}> tw (ctr gs v ++ t) > r --> l <{{E}} tw (ctr gs (S v) ++ t) *> r.	L185	new
44	Lemma	`IncL`	Lemma IncL gs v a : S v < 2 ^ S (length gs) -> forall l r t, l {{A}}> tw (T0 :: repeat TZ a ++ ctr gs v ++ t) > r --> l <{{F}} tw (T0 :: repeat TZ a ++ ctr gs (S v) ++ t) *> r.	L206	new
45	Lemma	`Bnc`	Lemma Bnc X : (const 0) <{{F}} [0;0] > [1;0;0] > X -->* (const 0) {{A}}> [0;0] > [1;0;0] > [1;0;0] *> X.	L218	new
46	Lemma	`Inc`	Lemma Inc gs v a : S v < 2 ^ S (length gs) -> forall t, (const 0) {{A}}> tw (T0 :: repeat TZ (S a) ++ ctr gs v ++ t) > (const 0) --> (const 0) {{A}}> tw (T0 :: repeat TZ (S (S a)) ++ ctr gs (S v) ++ t) *> (const 0).	L223	new
47	Lemma	`OvRet`	Lemma OvRet w rest : noT0 w -> forall m' ps' rs', retf E (prc w ++ [P]) (T1 :: rest) = (m', ps', rs') -> forall l r, l {{A}}> tw (T0 :: w ++ T0 :: rest) > r --> l <* pl ps' <{{m'}} tw rs' *> r.	L237	new
48	Lemma	`TwoInc`	Lemma TwoInc gs v p t L r : S (S v) < 2 ^ S (length gs) -> L <* [0] <* [1;0] {{A}}> tw (T0 :: repeat TZ p ++ ctr gs v ++ t) > r --> L {{A}}> tw (T0 :: repeat TZ (S p) ++ ctr gs (S (S v)) ++ t) *> r.	L260	new
49	Lemma	`ZXg`	Lemma ZXg gs v p t L r : S (S v) < 2 ^ S (length gs) -> L <* [0] <* [1;0;1;0;0;1;0;1;0;0;1;0] {{A}}> tw (T0 :: repeat TZ p ++ ctr gs v ++ t) > r --> L {{A}}> tw (T0 :: ctr (S (S p) :: gs) (2 * S (S v)) ++ t) *> r.	L273	new
50	Lemma	`ZXP2g`	Lemma ZXP2g gs v p t L r : S v < 2 ^ S (length gs) -> L <* [0] <* [0;1;0;0;1;0] {{A}}> tw (T0 :: repeat TZ p ++ ctr gs v ++ t) > r --> L {{A}}> tw (T0 :: ctr (p :: gs) (2 * S v) ++ t) *> r.	L286	new
51	Definition	`bt`	Definition bt (b : bool) : tok := if b then T1 else T0.	L299	new
52	Definition	`tailx`	Definition tailx (y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 : bool) (e : list bool) : list tok := bt y :: bt z :: TZ :: T1 :: bt b4 :: bt b5 :: TZ :: T1 :: bt b6 :: TZ :: bt b7 :: TZ :: T1 :: bt b8 :: bt b9 :: TZ :: bt b10 :: TZ :: T1 :: bt b11 :: TZ :: bt b12 :: TZ :: bt b13 :: TZ :: bt b14 :: TZ :: bt b15 :: TZ :: T1 :: map bt e ++ [T1].	L300	new
53	Definition	`tailw`	Definition tailw (x y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 : bool) (e : list bool) : list tok := bt x :: tailx y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e.	L304	new
54	Definition	`Lst`	Definition Lst (y z : bool) (S : Stream Sym) : Prop := exists b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e, S = tw (tailw true y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0.	L308	new
55	Lemma	`TailRet`	Lemma TailRet pre rest m out : noT0 pre -> retf E (prc pre) [T1] = (m, [], out) -> forall l R, l {{C}}> tw (pre ++ T0 :: rest) > R --> l <{{m}} tw (out ++ rest) *> R.	L312	new
56	Lemma	`Tail10`	Lemma Tail10 l b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e : l {{C}}> tw (tailw true true false b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 --> l <{{E}} tw (tailw true false true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0.	L323	new
57	Lemma	`Tail0z`	Lemma Tail0z l z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e : l {{C}}> tw (tailw true false z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 --> l <{{F}} [0;0] > tw (tailx true z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0.	L331	new
58	Definition	`F1`	Definition F1 : list tok := [T1; T1; T1; TZ; T1; T1; T1; TZ; T1; T1; TZ; T1; TZ; T1; T1; T1; TZ; T1; TZ; T1; T1; TZ; T1; TZ; T1; TZ; T1; TZ; T1; TZ; T1].	L339	new
59	Definition	`F1E`	Definition F1E : list tok := [T1; T0; T0; TZ; T1; T1; T0; TZ; T1; T0; TZ; T0; TZ; T1; T1; T0; TZ; T0; TZ; T1; T0; TZ; T1; TZ; T0; TZ; T1; TZ; T0; TZ; T1].	L340	new
60	Definition	`F1F`	Definition F1F : list tok := [T0; T1; T0; TZ; T1; T0; T0; TZ; T1; T0; TZ; T1; TZ; T1; T0; T0; TZ; T1; TZ; T1; T0; TZ; T0; TZ; T1; TZ; T0; TZ; T1; TZ; T1].	L341	new
61	Lemma	`F1E_ret`	Lemma F1E_ret X : retf E (prc F1) X = (E, [], F1E ++ X).	L342	new
62	Lemma	`F1F_ret`	Lemma F1F_ret X : retf F (prc F1) X = (F, [], F1F ++ X).	L343	new
63	Lemma	`tailw_ones`	Lemma tailw_ones e : tailw true true true true true true true true true true true true true true true e = F1 ++ map bt e ++ [T1].	L344	new
64	Lemma	`prc_app`	Lemma prc_app xs ys : prc (xs ++ ys) = prc ys ++ prc xs.	L347	new
65	Lemma	`repeat_snoc`	Lemma repeat_snoc {X} (x : X) n : repeat x n ++ [x] = x :: repeat x n.	L349	new
66	Lemma	`prc_T1s`	Lemma prc_T1s j : prc (repeat T1 j) = repeat P j.	L351	new
67	Lemma	`noT0_app`	Lemma noT0_app xs ys : noT0 xs -> noT0 ys -> noT0 (xs ++ ys).	L356	new
68	Lemma	`noT0_T1s`	Lemma noT0_T1s j : noT0 (repeat T1 j).	L358	new
69	Lemma	`map_bt_true`	Lemma map_bt_true j : map bt (repeat true j) = repeat T1 j.	L360	new
70	Lemma	`map_bt_alt`	Lemma map_bt_alt i : map bt ([true; false]^^i) = [T1; T0]^^i.	L362	new
71	Lemma	`retf_PP`	Lemma retf_PP i : forall ps rs, retf E (repeat P (2 * i) ++ ps) rs = retf E ps ([T1;T0]^^i ++ rs).	L365	new
72	Lemma	`retf_PPP`	Lemma retf_PPP i ps rs : retf E (repeat P (S (2 * i)) ++ ps) rs = retf F ps (T0 :: [T1;T0]^^i ++ rs).	L372	new
73	Lemma	`e_split`	Lemma e_split e : (exists j e', e = repeat true j ++ false :: e') \/ (exists m, e = repeat true m).	L379	new
74	Lemma	`Tail11_end`	Lemma Tail11_end e : (exists S', (forall l, l {{C}}> tw (tailw true true true true true true true true true true true true true true true e) > const 0 --> l <{{E}} S') /\ Lst false false S') \/ (exists S', (forall l, l {{C}}> tw (tailw true true true true true true true true true true true true true true true e) > const 0 --> l <{{F}} [0;0] > S') /\ Lst true false ([0;1] > S')).	L389	new
75	Lemma	`Tail11`	Lemma Tail11 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e : (exists S', (forall l, l {{C}}> tw (tailw true true true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 --> l <{{E}} S') /\ Lst false false S') \/ (exists S', (forall l, l {{C}}> tw (tailw true true true b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) > const 0 --> l <{{F}} [0;0] > S') /\ Lst true false ([0;1] > S')).	L442	new
76	Lemma	`retf_app_n`	Lemma retf_app_n n : forall ps1, length ps1 <= n -> forall m ps2 rs m1 rs1, retf m ps1 rs = (m1, [], rs1) -> retf m (ps1 ++ ps2) rs = retf m1 ps2 rs1.	L501	new
77	Lemma	`retf_app`	Lemma retf_app m ps1 ps2 rs m1 rs1 : retf m ps1 rs = (m1, [], rs1) -> retf m (ps1 ++ ps2) rs = retf m1 ps2 rs1.	L518	new
78	Lemma	`RB_E2`	Lemma RB_E2 n : forall rs, retf E ([PZ;P]^^(2*n)) rs = (E, [], [T0;TZ;T1;TZ]^^n ++ rs).	L523	new
79	Lemma	`RB_F2`	Lemma RB_F2 n : forall rs, retf F ([PZ;P]^^(2*n)) (T0 :: rs) = (F, [], T0 :: [TZ;T0;TZ;T1]^^n ++ rs).	L530	new
80	Lemma	`RB_E1`	Lemma RB_E1 n rs : retf E ([PZ;P]^^(S (2*n))) rs = (F, [], T0 :: [TZ;T0;TZ;T1]^^n ++ TZ :: rs).	L537	new
81	Lemma	`RB_F1`	Lemma RB_F1 n rs : retf F ([PZ;P]^^(S (2*n))) (T0 :: rs) = (E, [], [T0;TZ;T1;TZ]^^n ++ T0 :: TZ :: T1 :: rs).	L539	new
82	Lemma	`shift4`	Lemma shift4 n : [T0;TZ;T1] ++ [TZ;T0;TZ;T1]^^n = [T0;TZ;T1;TZ]^^n ++ [T0;TZ;T1].	L542	new
83	Definition	`dig`	Definition dig (b : tok) (g : nat) : list tok := b :: TZ :: T1 :: repeat TZ g.	L551	new
84	Fixpoint	`LD`	Fixpoint LD (b : tok) (G : list nat) : list tok := match G with [] => [] \| g :: G' => dig b g ++ LD b G' end.	L552	new
85	Lemma	`LD_app`	Lemma LD_app b G1 G2 : LD b (G1 ++ G2) = LD b G1 ++ LD b G2.	L555	new
86	Lemma	`LD_ones`	Lemma LD_ones b r : LD b (repeat 1%nat r) = [b;TZ;T1;TZ]^^r.	L557	new
87	Lemma	`ctr_zero`	Lemma ctr_zero gs : ctr gs 0 = LD T0 gs ++ [T0].	L560	new
88	Lemma	`ctr_ones`	Lemma ctr_ones gs : ctr gs (2 ^ S (length gs) - 1) = LD T1 gs ++ [T1].	L565	new
89	Lemma	`noT0_LD1`	Lemma noT0_LD1 G : noT0 (LD T1 G).	L573	new
90	Lemma	`noT0_U`	Lemma noT0_U q : noT0 ([T1;TZ]^^q).	L578	new
91	Lemma	`noT0_TZ`	Lemma noT0_TZ a : noT0 (repeat TZ a).	L580	new
92	Lemma	`prc_TZ`	Lemma prc_TZ a : prc (repeat TZ a) = repeat PZ a.	L583	new
93	Lemma	`prc_U`	Lemma prc_U q : prc ([T1;TZ]^^q) = [PZ;P]^^q.	L588	new
94	Lemma	`prc_dig`	Lemma prc_dig g : prc (dig T1 g) = repeat PZ g ++ [P; PZ; P].	L594	new
95	Lemma	`prc_LD`	Lemma prc_LD G : prc (LD T1 G) = flat_map (fun g => repeat PZ g ++ [P; PZ; P]) (rev G).	L597	new
96	Lemma	`retf_dig`	Lemma retf_dig g ps rs : retf E (repeat PZ g ++ [P; PZ; P] ++ ps) rs = retf E ps (dig T0 g ++ rs).	L604	new
97	Lemma	`retf_LD`	Lemma retf_LD G : forall ps rs, retf E (prc (LD T1 G) ++ ps) rs = retf E ps (LD T0 G ++ rs).	L611	new
98	Lemma	`retf_lead`	Lemma retf_lead a rs : retf E (repeat PZ a ++ [P]) rs = (F, [], T0 :: repeat TZ a ++ rs).	L617	new
99	Lemma	`AT0p`	Lemma AT0p l r : l {{A}}> [0;0] > r -->+ l < [0;1] {{C}}> r.	L624	new
100	Lemma	`OvSweep`	Lemma OvSweep w : noT0 w -> forall l S, l {{A}}> tw (T0 :: w) > S -->+ l < pl (prc w ++ [P]) {{C}}> S.	L625	new
101	Definition	`sfx`	Definition sfx (H : bool) : list tok := if H then [TZ] else [TZ;T1;TZ].	L636	new
102	Definition	`gsof`	Definition gsof (G : list nat) (r1 : nat) : list nat := G ++ 2%nat :: repeat 1%nat r1.	L637	new
103	Definition	`qof`	Definition qof (H : bool) (r1 : nat) : nat := if H then S (2 * r1) else 2 * S r1.	L638	new
104	Definition	`ones`	Definition ones (gs : list nat) : nat := 2 ^ S (length gs) - 1.	L639	new
105	Lemma	`U2`	Lemma U2 r : [T1;TZ;T1;TZ]^^r = [T1;TZ]^^(2*r).	L641	new
106	Lemma	`body_ones`	Lemma body_ones G r1 H : ctr (gsof G r1) (ones (gsof G r1)) ++ sfx H = LD T1 G ++ dig T1 2 ++ [T1;TZ]^^(qof H r1).	L647	new
107	Lemma	`body_zero`	Lemma body_zero G r1 : ctr (gsof G r1) 0 = LD T0 G ++ dig T0 2 ++ [T0;TZ;T1;TZ]^^r1 ++ [T0].	L656	new
108	Lemma	`noT0_w`	Lemma noT0_w a G q : noT0 (repeat TZ a ++ LD T1 G ++ dig T1 2 ++ [T1;TZ]^^q).	L659	new
109	Lemma	`prc_w`	Lemma prc_w a G q : prc (repeat TZ a ++ LD T1 G ++ dig T1 2 ++ [T1;TZ]^^q) ++ [P] = [PZ;P]^^q ++ [PZ;PZ;P;PZ;P] ++ (prc (LD T1 G) ++ repeat PZ a ++ [P]).	L664	new
110	Lemma	`BNp`	Lemma BNp ps l r : l <* pl ([PZ;PZ;P;PZ;P] ++ ps) <{{F}} [0;0] > r --> l <* pl ps <* [1;0;1;0;0;1] {{A}}> [0;0;0;0;1;0;0;0;1] *> r.	L670	new
111	Lemma	`OvN1`	Lemma OvN1 G r1 a l St St' : (forall l', l' {{C}}> St -->* l' <{{E}} St') -> l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx true) > St -->+ l < pl (prc (LD T1 G) ++ repeat PZ a ++ [P]) <* [1;0;1;0;0;1] {{A}}> tw (T0 :: ctr (repeat 1%nat r1) 0 ++ sfx false) *> St'.	L678	new
112	Lemma	`OvN0`	Lemma OvN0 G r1 a l St S0 : (forall l', l' {{C}}> St -->* l' <{{F}} [0;0] > S0) -> l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx false) > St -->+ l <* pl (prc (LD T1 G) ++ repeat PZ a ++ [P]) <* [1;0;1;0;0;1] {{A}}> tw (T0 :: ctr (repeat 1%nat (S r1)) 0 ++ sfx true) > ([0;1] > S0).	L703	new
113	Lemma	`OvS1`	Lemma OvS1 G r1 a l St S0 : (forall l', l' {{C}}> St -->* l' <{{F}} [0;0] > S0) -> l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx true) > St -->+ l <{{F}} tw (T0 :: repeat TZ a ++ ctr (gsof G r1) 0 ++ sfx true) > ([0;1] > S0).	L728	new
114	Definition	`KP`	Definition KP (W : side) (p : nat) (gs : list nat) (v : nat) (H : bool) (St : side) : Q * tape := W {{A}}> tw (T0 :: repeat TZ p ++ ctr gs v ++ sfx H) *> St.	L754	new
115	Definition	`NN`	Definition NN (gs : list nat) : nat := 2 ^ S (length gs).	L756	new
116	Lemma	`wall0`	Lemma wall0 : (const 0 <* [1] : side) = Str_app [1;0] (Str_app [0] (const 0)).	L758	new
117	Lemma	`P100`	Lemma P100 n l p gs v H St : S (S v) < NN gs -> KP (Str_app ([1] ++ [0;0;1]^^(S n)) l) p gs v H St -->* KP (Str_app ([1] ++ [0;0;1]^^n) l) (S p) gs (S (S v)) H St.	L761	new
118	Lemma	`P100s`	Lemma P100s m : forall n l p gs v H St, 2 * m + v < NN gs -> KP (Str_app ([1] ++ [0;0;1]^^(m + n)) l) p gs v H St -->* KP (Str_app ([1] ++ [0;0;1]^^n) l) (m + p) gs (2 * m + v) H St.	L766	new
119	Lemma	`WX`	Lemma WX p gs v H St : S (S v) < NN gs -> KP (Str_app [1] (const 0)) p gs v H St -->* KP (const 0) (S p) gs (S (S v)) H St.	L777	new
120	Lemma	`Inc1`	Lemma Inc1 a gs v H St : S v < NN gs -> KP (const 0) (S a) gs v H St -->* KP (const 0) (S (S a)) gs (S v) H St.	L781	new
121	Lemma	`Incs`	Lemma Incs m : forall a gs v H St, m + v < NN gs -> KP (const 0) (S a) gs v H St -->* KP (const 0) (m + S a) gs (m + v) H St.	L790	new
122	Fixpoint	`zw`	Fixpoint zw (L : list nat) : list Sym := match L with [] => [] \| g :: L' => [1;0;0;1] ++ [0;1;0]^^(S g) ++ zw L' end.	L801	new
123	Fixpoint	`zv`	Fixpoint zv (L : list nat) (v : nat) : nat := match L with [] => v \| g :: L' => zv L' (2 * v + 2 * g) end.	L803	new
124	Fixpoint	`zg`	Fixpoint zg (L : list nat) (p : nat) (gs : list nat) : list nat := match L with [] => gs \| g :: L' => zg L' (g - 2) (S (S p) :: gs) end.	L805	new
125	Fixpoint	`zp`	Fixpoint zp (L : list nat) (p : nat) : nat := match L with [] => p \| g :: L' => zp L' (g - 2) end.	L807	new
126	Lemma	`P010s`	Lemma P010s m : forall X Y p gs v H St, 2 * m + v < NN gs -> KP (Str_app ([1;0] ++ [0;1;0]^^m ++ X) Y) p gs v H St -->* KP (Str_app ([1;0] ++ X) Y) (m + p) gs (2 * m + v) H St.	L810	new
127	Lemma	`Zone`	Lemma Zone g L X Y p gs v H St : 2 <= g -> v + g < NN gs -> KP (Str_app ([1;0] ++ zw (g :: L) ++ X) Y) p gs v H St -->* KP (Str_app ([1;0] ++ zw L ++ X) Y) (g - 2) (S (S p) :: gs) (2 * v + 2 * g) H St.	L821	new
128	Lemma	`zv_ge`	Lemma zv_ge L : forall v, 2 ^ length L * v <= zv L v.	L833	new
129	Lemma	`zg_len`	Lemma zg_len L : forall p gs, length (zg L p gs) = length L + length gs.	L838	new
130	Lemma	`Zones`	Lemma Zones L : Forall (le 2) L -> forall X Y p gs v H St, zv L v < 2 ^ (S (length gs) + length L) -> KP (Str_app ([1;0] ++ zw L ++ X) Y) p gs v H St -->* KP (Str_app ([1;0] ++ X) Y) (zp L p) (zg L p gs) (zv L v) H St.	L841	new
131	Fixpoint	`gval`	Fixpoint gval (G : list nat) : nat := match G with [] => 0 \| g :: G' => 2 * (g + gval G') end.	L865	new
132	Lemma	`zv_app`	Lemma zv_app L1 : forall L2 v, zv (L1 ++ L2) v = zv L2 (zv L1 v).	L867	new
133	Lemma	`zp_app`	Lemma zp_app L1 : forall L2 p, zp (L1 ++ L2) p = zp L2 (zp L1 p).	L869	new
134	Lemma	`zg_app`	Lemma zg_app L1 : forall L2 p gs, zg (L1 ++ L2) p gs = zg L2 (zp L1 p) (zg L1 p gs).	L871	new
135	Lemma	`zw_app`	Lemma zw_app L1 L2 : zw (L1 ++ L2) = zw L1 ++ zw L2.	L873	new
136	Lemma	`zv_rev`	Lemma zv_rev G : zv (rev G) 0 = gval G.	L875	new
137	Lemma	`zg_rev`	Lemma zg_rev G gs0 : Forall (le 2) G -> S (S (zp (rev G) 0)) :: zg (rev G) 0 gs0 = G ++ 2%nat :: gs0.	L877	new
138	Lemma	`zp_rev_last`	Lemma zp_rev_last G p : zp (rev G ++ [p]) 0 = p - 2.	L883	new
139	Lemma	`zv_rev_last`	Lemma zv_rev_last G p : zv (rev G ++ [p]) 0 = 2 * gval G + 2 * p.	L885	new
140	Lemma	`zg_rev_last`	Lemma zg_rev_last G p gs0 : Forall (le 2) G -> zg (rev G ++ [p]) 0 gs0 = G ++ 2%nat :: gs0.	L887	new
141	Lemma	`zg_len'`	Lemma zg_len' L p gs : length (zg L p gs) = length L + length gs.	L889	new
142	Lemma	`pl_lead`	Lemma pl_lead a : pl (repeat PZ a ++ [P]) = [0;1] ++ [0;0;1]^^a.	L892	new
143	Lemma	`pl_PZ`	Lemma pl_PZ g : pl (repeat PZ g) = [0;1;0]^^g.	L895	new
144	Lemma	`zw_LD_gen`	Lemma zw_LD_gen L : [1;0;0;1] ++ pl (flat_map (fun g => repeat PZ g ++ [P; PZ; P]) L) = zw L ++ [1;0;0;1].	L898	new
145	Lemma	`wallOv`	Lemma wallOv G W l : (l <* pl (prc (LD T1 G) ++ W) <* [1;0;1;0;0;1] : side) = Str_app ([1;0] ++ zw (rev G) ++ [1;0;0;1] ++ pl W) l.	L906	new
146	Lemma	`wallPO`	Lemma wallPO G p n l : Str_app ([1;0] ++ zw (rev G) ++ [1;0;0;1] ++ pl (repeat PZ p ++ [P])) (Str_app ([0;0;0;1] ++ [0;0;1]^^n) l) = Str_app ([1;0] ++ zw (rev G ++ [p]) ++ [0;0;1]^^(S n)) l.	L914	new
147	Lemma	`ZXN`	Lemma ZXN a l p gs v H St : S (S v) < NN gs -> KP (Str_app ([1;0] ++ [1;0;0;1] ++ pl (repeat PZ (S (S a)) ++ [P])) l) p gs v H St -->* KP (Str_app ([1] ++ [0;0;1]^^a) l) 0 (S (S p) :: gs) (2 * S (S v)) H St.	L926	new
148	Lemma	`ZXP`	Lemma ZXP n l p gs v H St : S (S (S v)) < NN gs -> KP (Str_app ([1;0] ++ [0;0;1]^^(S (S (S n)))) l) p gs v H St -->* KP (Str_app ([1] ++ [0;0;1]^^n) l) 0 (S p :: gs) (2 * S (S (S v))) H St.	L934	new
149	Definition	`OvNp`	Definition OvNp (H : bool) (r1 : nat) (St : side) (H' : bool) (r1' : nat) (St' : side) : Prop := forall G a l, l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx H) > St -->+ l < pl (prc (LD T1 G) ++ repeat PZ a ++ [P]) <* [1;0;1;0;0;1] {{A}}> tw (T0 :: ctr (repeat 1%nat r1') 0 ++ sfx H') *> St'.	L944	new
150	Definition	`OvSp`	Definition OvSp (r1 : nat) (St St' : side) : Prop := forall G a l, l {{A}}> tw (T0 :: repeat TZ a ++ ctr (gsof G r1) (ones (gsof G r1)) ++ sfx true) > St -->+ l <{{F}} tw (T0 :: repeat TZ a ++ ctr (gsof G r1) 0 ++ sfx true) > St'.	L948	new
151	Lemma	`OvNp1`	Lemma OvNp1 r1 St St' : (forall l', l' {{C}}> St -->* l' <{{E}} St') -> OvNp true r1 St false r1 St'.	L952	new
152	Lemma	`OvNp0`	Lemma OvNp0 r1 St S0 : (forall l', l' {{C}}> St -->* l' <{{F}} [0;0] > S0) -> OvNp false r1 St true (S r1) ([0;1] > S0).	L954	new
153	Lemma	`OvSp1`	Lemma OvSp1 r1 St S0 : (forall l', l' {{C}}> St -->* l' <{{F}} [0;0] > S0) -> OvSp r1 St ([0;1] > S0).	L957	new
154	Lemma	`len_gsof`	Lemma len_gsof G r1 : length (gsof G r1) = length G + S r1.	L960	new
155	Lemma	`pow_pos`	Lemma pow_pos n : 0 < 2 ^ n.	L962	new
156	Lemma	`NOrb`	Lemma NOrb H r1 St H' r1' St' G a : OvNp H r1 St H' r1' St' -> Forall (le 2) G -> gval G + 2 < 2 ^ (length G + S r1') -> KP (const 0) (S (S a)) (gsof G r1) (ones (gsof G r1)) H St -->+ KP (Str_app ([1] ++ [0;0;1]^^a) (const 0)) 0 (gsof G r1') (2 * gval G + 4) H' St'.	L965	new
157	Lemma	`ones_S`	Lemma ones_S gs : S (ones gs - 1) = ones gs.	L986	new
158	Lemma	`ones_lt`	Lemma ones_lt gs : ones gs < NN gs.	L988	new
159	Lemma	`POrb`	Lemma POrb H r1 St H' r1' St' G p n l0 : OvNp H r1 St H' r1' St' -> Forall (le 2) G -> 2 <= p -> 2 * gval G + 2 * p + 3 < 2 ^ (length G + S (S r1')) -> KP (Str_app ([1] ++ [0;0;1]^^(S (S (S n)))) l0) p (gsof G r1) (ones (gsof G r1) - 1) H St -->* KP (Str_app ([1] ++ [0;0;1]^^n) l0) 0 (gsof (S (p - 2) :: G) r1') (2 * S (S (S (2 * gval G + 2 * p)))) H' St'.	L991	new
160	Lemma	`SILENTP`	Lemma SILENTP r1 St St' G p n l0 : OvSp r1 St St' -> KP (Str_app ([1] ++ [0;0;1]^^(S n)) l0) p (gsof G r1) (ones (gsof G r1) - 1) true St -->* KP (Str_app ([1] ++ [0;0;1]^^n) l0) (S p) (gsof G r1) 0 true St'.	L1019	new
161	Lemma	`SILENT`	Lemma SILENT r1 St St' G a : OvSp r1 St St' -> KP (const 0) (S a) (gsof G r1) (ones (gsof G r1)) true St -->+ KP (const 0) (S (S a)) (gsof G r1) 0 true St'.	L1034	new
162	Definition	`KX`	Definition KX (a : nat) (G : list nat) (r1 : nat) (St : side) : Q * tape := KP (const 0) a (gsof G r1) (ones (gsof G r1)) true St.	L1044	new
163	Lemma	`pS`	Lemma pS k r : 2 ^ (k + S r) = 2 * 2 ^ (k + r).	L1047	new
164	Lemma	`NN_gsof`	Lemma NN_gsof G r1 : NN (gsof G r1) = 4 * 2 ^ (length G + r1).	L1049	new
165	Lemma	`ones_gsof`	Lemma ones_gsof G r1 : ones (gsof G r1) = 4 * 2 ^ (length G + r1) - 1.	L1051	new
166	Lemma	`Q_cons`	Lemma Q_cons (g : nat) (G : list nat) r1 : 2 ^ (length (g :: G) + S r1) = 4 * 2 ^ (length G + r1).	L1053	new
167	Lemma	`KP_eq`	Lemma KP_eq W p p' gs v v' H St : p = p' -> v = v' -> KP W p gs v H St = KP W p' gs v' H St.	L1056	new
168	Lemma	`pathS`	Lemma pathS a G r1 St St' : OvSp r1 St St' -> 1 <= a -> KX a G r1 St -->+ KX (a + 4 * 2 ^ (length G + r1)) G r1 St'.	L1059	new
169	Lemma	`pre1`	Lemma pre1 a G r1 St St1 S0 kap s : let Q := 2 ^ (length G + r1) in OvNp true r1 St false r1 St1 -> (forall l', l' {{C}}> St1 -->* l' <{{F}} [0;0] > S0) -> Forall (le 2) G -> gval G + 6 + kap = Q -> a = s + Q + kap -> 8 <= s -> KX a G r1 St -->+ KP (Str_app ([1] ++ [0;0;1]^^(s - 8)) (const 0)) 0 (gsof ((Q + 2 + kap) :: G) (S r1)) (8 Q - 6) true ([0;1] *> S0).	L1072	new
170	Definition	`TailF`	Definition TailF (St S0 : side) : Prop := forall l', l' {{C}}> St -->* l' <{{F}} [0;0] *> S0.	L1094	new
171	Lemma	`gval_cons`	Lemma gval_cons g G : gval (g :: G) = 2 * (g + gval G).	L1096	new
172	Lemma	`pathP1`	Lemma pathP1 a G r1 St St1 S0 kap s : let Q := 2 ^ (length G + r1) in OvNp true r1 St false r1 St1 -> TailF St1 S0 -> Forall (le 2) G -> gval G + 6 + kap = Q -> a = s + Q + kap -> 8 <= s -> s <= 4 * Q + 9 -> KX a G r1 St -->+ KX (8 * Q + 12 - s) ((Q + 2 + kap) :: G) (S r1) ([0;1] *> S0).	L1099	new
173	Lemma	`pathP1S`	Lemma pathP1S a G r1 St St1 S0 St3 kap s : let Q := 2 ^ (length G + r1) in OvNp true r1 St false r1 St1 -> TailF St1 S0 -> OvSp (S r1) ([0;1] > S0) St3 -> Forall (le 2) G -> gval G + 6 + kap = Q -> a = s + Q + kap -> 4 Q + 11 <= s -> s <= 12 * Q + 9 -> KX a G r1 St -->+ KX (24 * Q + 12 - s) ((Q + 2 + kap) :: G) (S r1) St3.	L1118	new
174	Lemma	`pathP3`	Lemma pathP3 a G r1 St St1 S0 St3 S4 kap s : let Q := 2 ^ (length G + r1) in OvNp true r1 St false r1 St1 -> TailF St1 S0 -> OvNp true (S r1) ([0;1] > S0) false (S r1) St3 -> TailF St3 S4 -> Forall (le 2) G -> gval G + 6 + kap = Q -> a = s + Q + kap -> 4 Q + 24 <= s -> s <= 36 * Q + 31 -> KX a G r1 St -->+ KX (68 * Q + 40 - s) (7 :: (4 * Q + 1) :: (Q + 2 + kap) :: G) (S (S r1)) ([0;1] *> S4).	L1142	new
175	Definition	`INV`	Definition INV (a : nat) (G : list nat) (r1 : nat) (St : side) : Prop := Forall (le 2) G /\ 64 <= 2 ^ (length G + r1) /\ exists kap s, (kap = 2 \/ kap = 8) /\ gval G + 6 + kap = 2 ^ (length G + r1) /\ a = s + 2 ^ (length G + r1) + kap /\ ((Lst true true St /\ 24 <= s <= 2 ^ (length G + r1) + 2) \/ (Lst true false St /\ ((8 <= s <= 4 * 2 ^ (length G + r1) - 14) \/ … +1 lines	L1192	new
176	Lemma	`Lst_intro`	Lemma Lst_intro y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e : Lst y z (tw (tailw true y z b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 e) *> const 0).	L1200	new
177	Lemma	`Q1`	Lemma Q1 (g : nat) G r1 : 2 ^ (length (g :: G) + S r1) = 4 * 2 ^ (length G + r1).	L1207	new
178	Lemma	`Q3`	Lemma Q3 (g1 g2 g3 : nat) G r1 : 2 ^ (length (g1 :: g2 :: g3 :: G) + S (S r1)) = 32 * 2 ^ (length G + r1).	L1209	new
179	Lemma	`step`	Lemma step a G r1 St : INV a G r1 St -> exists a' G' r1' St', KX a G r1 St -->+ KX a' G' r1' St' /\ INV a' G' r1' St'.	L1212	new
180	Definition	`St0`	Definition St0 : side := tw (tailw true true true true true true false true true true true false true false true [false; true; false]) *> const 0.	L1271	new
181	Lemma	`init`	Lemma init : c0 -->* KX 121 [28%nat] 5 St0.	L1274	new
182	Lemma	`INV0`	Lemma INV0 : INV 121 [28%nat] 5 St0.	L1277	new
183	Lemma	`nonhalt`	Lemma nonhalt : ~ halts tm c0.	L1284	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 100: 2.2 Rule Inc_L

Inc_L. For every left half-tape L, every a ≥ 0 and every counter D_G(v) with v + 1 < 2^N:

L A>(001)^a 00 D_G(v) T → L <F (001)^a 00 D_G(v+1) T, in 6a + 6S_j + 24j + 7 steps.

Here j = the number of trailing 1 bits of v (b_0..b_(j-1) = 1, b_j = 0) and S_j = g_1 + ... + g_j. The head never reads L before the last step, so L is arbitrary. T is arbitrary too, because the run never reads past d_j.

Proof, in order:

R2, R4^a.
For i = 0..j-1: R3 on d_i, then R4^(g_(i+1)).
R5 on d_j.
For i = j-1 down to 0: L1^(g_(i+1)), then L2 on the processed d_i.
L1^a, then L3.

The step total is 2 + 3a + Σ(7 + 3g) + 3 + Σ(3g + 17) + 3a + 2. The proof is by induction on the carry depth j, like Climb/E_stmt in CounterClass3v2 TM1. In the .v the counter is ctr gs v (a list of gaps, LSB first, whose last digit is its bit only, so the digits above the carry are never read), the induction is IncC (over the list gs), and IncL adds steps 1 and 5.

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
#8 kill 13	`1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB`	✓Killed: never halts	this kill
Named in a file but not linked (not counted as family)
W6-8	`1RB1RC_0LC1RE_1RA0LD_1LB0RD_0RF---_0RA0RF`	▲Stuck	named in W6-8's notes.md · 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 437 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 3.19 s
✓
.v hash matches the checked hash
.v = checked sha256 0ddf748799bc…; submission/ copy = checked sha256 0ddf748799bc…
✓
No repo-local paths in the .v
comments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own verify/X.v is fine: none in the .v or the submission/ copy
✓
Public write-up is clean
tools/writeup_lint.py on submission/proof.md: 0 error(s)
○
proof.md reviewed by Dennis (Checkpoint B)
no Checkpoint B note from Dennis found
- notes.md L106: - Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):
- notes.md L344: - No Checkpoint B notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
- proof.md L1: # 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB: never halts (informal proof, Checkpoint B)
- proof.md L415: - Open: the formalisation route for T(f) (§9 step 5). Checkpoint B not yet reviewed (see the next entry).
○
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 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB

Files

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

name	size	changed
notes.md ↓	30 KB	2026-10-10 16:18
proof.md ↓	42 KB	2026-10-10 14:39
how_proved.md ↓	1.6 KB	2026-10-14 10:51
status.json ↓	575 B	2026-10-16 10:28
observe.json ↓	12 KB	2026-10-10 04:41
deepen.json ↓	17 KB	2026-10-10 13:25
1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v ↓	74 KB	2026-10-10 16:02
decisions/	1 item	2026-10-10 13:24
img/	6 items	2026-10-10 01:56
rocq/	5 items	2026-10-10 15:57
scripts/	44 items	2026-10-10 14:22
submission/	6 items	2026-10-15 15:49
work/	28 items	2026-10-10 16:19
check_proof.py ↓	53 KB	2026-10-10 14:31

status.json in full

{
 "tm": "1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "pr": "https://github.com/ccz181078/busycoq/pull/26",
 "pr_state": "merged",
 "pr_file": "verify/M_1RB0LF_0RCHHH_1RD0RA_1LE0RC_0LA0LE_1LE1LB.v",
 "pr_opened": "2026-10-15T22:46:55Z",
 "pr_comments": 0,
 "pr_head_sha": "c12a4d3727231fa0aefd58b42335e33b2ecb9352",
 "posted": "2026-10-15 (Discord; user confirmed sent)",
 "pr_merged_at": "2026-10-16T07:08:21Z",
 "pr_merged_by": "ccz181078"
}

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