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 / C2-552

`1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB`

C2-552local proof 19Kill claimedSkelet 1-like Class 2bbchallenge ↗Explorer

How we proved it halts

Replaying a binary counter until a digit runs out of fuel

Look at the tape each time the head reaches fresh tape on the right, and it reads as a binary counter, lowest digit on the right. Digits are fenced off by walls, runs of equal cells (usually 11). Inside each digit sit a bit marker (00 for 0, 1111 for 1), sometimes a few spare walls, and a final alternating stretch whose length is the digit's fuel. Each trip adds 1: the carry runs left past every 1 digit to the first 0, and every digit it touches burns fuel.

The key idea: spare walls are spare lives. A digit with a spare wall that runs out of fuel hands that wall to the fence on its right and takes the gap before it as new fuel; the wall later moves into the next digit. So walls drift toward the head, and a digit with no spare wall survives only if walls reach it in time. Between such events everything changes at a steady rate, so long runs of increments can be done in one batch by a formula.

Why it halts: from step 342, a checker replays the run in 107,781 moves, about half of them batches. In increment 11,631,266,794,472,450,654,093 (about 1.16 × 10^22), a carry reaches a digit with no spare wall, bit 0 and no fuel, and the machine hits its one missing instruction. Adding up every move's cost gives a 45-digit step count, about 1.77 × 10^44: exactly 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463.

In Rocq (busycoq), every carry rule and batch formula is a proved lemma, and the checker, proved correct once, runs to the halt, re-checking each proposed batch. The step count is not part of that proof; its per-move costs match direct simulation over the first 10^11 steps.

#19local proof number

1,142lines of Rocq

70 sto compile

6/6automatic checks

Overview

In one sentence

Fueled-unit binary counter, rules closed (27,813/27,813 to 1e9); halting = a k=1 unit losing the fuel race.

Submitted mechanism At each right record the tape is a binary counter of units [x, M, m_1, Q_1, …, y] cut by 11 walls. The lead M (00 or 1111) is the bit, the Q are passive walls, and the last gap y is fuel that every carry burns. (submission/README.md, Mechanism)

Upstream: Kill claimed · PR #18merged 2026-10-14 06:20 UTC by ccz181078 · Sk1Class2_v4.v · TM12 · on Submissions →
Rocq proof: check_kill PASS · first Oct 12 20:38
1,142 lines · 64 KB .v · compile 70.0 s · coqchk pass · 1 axioms · PASS Oct 12 20:38 (re-run Oct 13 10:33)
· the .v file
Automatic review: 6 of 6 checks passtemplate: verify/Sk1Machines.v (adapted from) · details in Proof →
Class: Skelet 1-like Class 2ours: sheet Skelet 1-like Class 2 ≠ ours multi-level binary counter: #11-style carry M over fueled units, walls migrate unit to unit, edge fossils = Pascal rows · med confidence
On the list: not on BB6_holdouts_663.txt (line 552 of the previous list) · historical 740 line 552 · observe.json rank #552
eqv ×1sim 1e15

Your calls on file 1

funded: option: class2_closeout · date: 2026-10-12

Mechanism

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

How it works: 3 notes

Wall view: 1-blocks of length 3g+2 (11, 1^5, ...) are unit boundaries with g glued walls; 3j+1 (1111, 1^7, ...) are passive stacks; units are x M m Q .. y (lead M = 00/1111 is the bit, y = fuel); the leftmost block is the edge. Carry M: leads 1111->00 up to the first 00->1111, every touch burns fuel.
Markers flow right: a passive wall that reaches the boundary glues, then becomes the next unit's lead (unglue S) while that unit's old lead turns passive. The edge grows by 3 per overflow and fossilizes into passive stacks that seed the Pascal rows; resets turn the tail into a new LSB unit.
Halts iff F reads a 1 after 00: only a single-marker unit running dry does that. Its margin y-(2T-bit) is constant between resets; non-halting needs the reset ratio a_{n+1}/a_n < 2 (observed 1.79-1.86). No halt to 1e11 (direct) or in 3M more macro increments.

Figures for Checkpoint A

Fig 1 · bbchallenge Default view, 10,000 stepsviewer ↗
Orientation: the run as the site shows it. Note the slowly widening left zone and the drifting walls.

Fig 2 · Carries on a built unit tapeQ1
Each leftward diagonal is one increment; its depth is the carry length. Compare the depths of successive sweeps.

Fig 3 · Edge records to 300,000 stepsQ2 viewer ↗
White diagonals are 1111 markers drifting right as x grows; the vertical stripes at the left are the fossil zone.

More figures (1)Fig 4: Left records to 3 billion steps

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

rule	from ⟶ to	cases	steps	checked
M carry (wall view)	... 11 [x 00 m P .. y] {11 [x_i 1111 m_i P .. y_i]}_i 11 t A> ⟶ ... 11 [x-1 1111 m+1 P .. y-2] {11 [x_i+3 00 m_i+1 P .. y_i-2]}_i 11 (t+2) A> (k=1 units: no m, y-1)	carry stops at the first unit with lead 00; units left of it and the prefix untouched	2t + sum_passed (20 + 16(k-1) + 2(x+sum m+y)) + (16 + 16(k-1) + 2(sum m + y))	✓30033/30033
Closed unit rules (stage 2)	E U_0 b_1 U_1 ... b_N U_N b_T [t] A> ⟶ one increment: tail t+2; per unit from the right: M pass / S unglue (boundary 1^3g+2) / leadless +2 / M stop; edge e+=3 or fossilize (e = 1 mod 3) or absorb b_1; glue G when a last gap hits -1; reset R in two increments	see notes.md stage 2 table; executable spec work/rules3.py	not modelled (the macro step count is not needed for the non-halting argument)	✓28413/28413

Compressed historythe tape as reset: ... 11 x M (a-1) 11 1 1111 (2a-1) 11 1 A> 0^∞ at 17 moments: where the rules are read off

reset: ... 11 x M (a-1) 11 1 1111 (2a-1) 11 1 A> 0^∞

step	`a`	`lo`
537	2	-10
884	4	-11
1,665	7	-14
3,132	11	-17
5,841	17	-19
11,638	28	-22
26,355	50	-25
70,210	93	-29
211,425	173	-34
677,044	317	-42
2,195,541	574	-51
7,122,972	1,036	-68
23,158,343	1,875	-95
75,751,078	3,407	-143
249,431,021	6,205	-228
824,902,774	11,304	-381
2,732,037,815	20,577	-658

alast 20,577

lolast -658

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

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

file: SBCv6.v:3702
module: TM21 (via our kill #11)
machine: 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (11 transitions apart)
diff: no close table; architecture only
note: Level 0 is #11's per-carry M (one macro step per carry, every touch burns fuel). There is no global re-pairing O: new LSB units enter at the right, old units fossilize at the left into an unbounded Pascal-triangle zone (depth ~ log t). #3's down-counter with ghost-phase J does not fit (this counter increments).

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

Stage 3: an invariant for the k=1 fuel race (margin y-(2T-bit) >= 0 for every episode), closed under all rules and tested on the macro simulator. Needs a bound on the reset ratio a_{n+1}/a_n < 2, set by the Pascal-structured arrival schedule from U_0/U_1.

▲The invariant must control future fuel-race episodes, whose start depends on the arrival schedule from an unbounded Pascal-structured fossil zone: far beyond #11's INV.
▲The reset ratio a_{n+1}/a_n oscillates slowly (1.79-1.86 observed) with no closed form; a proof needs a uniform bound below 2.
▲Rules are validated, not proved: the macro step uses shift rules over alternating stretches that a Coq proof would have to establish one by one.

Stats & provenance10¹¹ steps simulated · 556,565 cells · the status in full · files

simulated: 10¹¹ steps
tape: 556,565 cells · 283,762 nonzeros
growth: span ~ t^0.5 to the right; left edge +1 per far-left carry (-676 at 3e9, -3,671 at 1e11); walls ~ log t
status now: check_kill --halt PASS, independently re-verified (status.json, 2026-10-13)
observer's note: Rule closure done (Class 2 close-out stage 2): 27,813/27,813 increments from step 342 to 1e9; invariant (k=1 fuel race) open.
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v

Proof & checks

6/6 automatic checks pass

Kill 19 · Skelet 1-like Class 2 · the kill file 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v: 1142 lines, 234 items · the package submission/

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

1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB

vs holdout list

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

Theorem

✓ Lemma halt: halts tm c0. L1117

check_kill

✓ PASS · 17/17 checks pass · compile 69.98 s · coqchk pass (536.46 s) · assumptions: 1 (Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g) · 2026-10-13 17:33:35 UTC · submission/check_kill.txt

Checked .v

sha256 198b30225e7ccff8…

✓	1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v	`198b30225e7ccff8…` = checked
✓	submission/1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v	`198b30225e7ccff8…` = checked

Status

✓Killed: halts updated 2026-10-13

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

All 17 check_kill checks with their one-line results

✓	`args`	6x2 machine, framework module Individual62, mode halt
✓	`input`	65774 bytes, 1142 lines, 1452 sentences
✓	`framework`	HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓	`framework_build`	14 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`	10 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 37: TM_from_str "1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB" == <tm> (41 bytes)
✓	`theorem_text`	line 1117: halt : halts tm c0
✓	`coq`	coqc 8.20.1 (<opam-switch>/bin/coqc)
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 70.0s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	halt : halts (TM_from_str "1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB") c0 with absolute names (in-file and isolated)
✓	`isolation`	only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off
✓	`assumptions`	1 assumption(s), all in the baseline
✓	`coqchk`	coqchk -norec BB6Kill.Candidate ok (536.5s); 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/Sk1Machines.v · detected from 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v line 8

5%of our lines identical to the template

1changed lines

1000added lines (ours only)

1849template lines dropped

0 / 11 / 223items identical / adapted / new

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

verify/Sk1Machines.v, Module TM91 (a halting Skelet 1 machine) with Module Sk1Auto: a checker iterated by Eqb.N_iter_until and proved sound once (check_spec), with untrusted proposals certified at each use.

Kept: the checker architecture (one step function iterated by N_iter_until and proved sound with N_iter_until_spec: advance on run-length tapes there, next on unit records here), the call-segment calculus of verify/Individual.v (instantiated in verify/Individual62.v), and sideRLs_halt of verify/LongitudinalHalt.v.
Changed: the records are this machine's units (stack lists with binary-number gaps) instead of run-length tapes; the rules are unit-level lemmas rather than scans; closed-form batches replace bulk steps; and the run is split into 22 chunks so that coqchk finishes.

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

5% identical · 1 changed · 1000 added

template 1907 lines

3% kept verbatim · 1849 not in ours

our items 234

0 identical · 11 adapted · 223 new · 177 template-only

identicalchanged / adaptedours only (new)template only

Template part: whole file, lines 3–2043 (leading comment left out). Ours: lines 31–1142 (header comment 1–30 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: W, digit, word, take, give, carry, walls, prefix_rule, effect, total, total_spec, total_add, total_six, total_period, effectN, denote_effect, totalN, totalN_spec, cells, cell_word, batch, totalN_rule, batch_spec, scan, scan_valid, head, start, calls_spec, batch_root, total_seven, nil_power, t, push, push_spec, pop, pop_spec, remove, remove_spec, commute_power, skip_block …

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

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

template		ours
3	From BusyCoq Require Import Individual62 Helper LongitudinalHalt Eqb FastRev.	32	From BusyCoq Require Import Individual62 LongitudinalHalt Flip Eqb.
4	Require Import ZifyNat Lia NArith PeanoNat String List.	33	Require Import ZifyNat Lia NArith PeanoNat String List.
5	Import BusyCoq.Eqb.
6	Open Scope sym_scope.	34	Open Scope sym_scope.
8	Module Sk1Counter.
		35	Open Scope list.
9	Definition W : list Sym := [1;1;1;1;0;1;1;1;1;1].
		37	Definition tm := Eval compute in (TM_from_str "1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB").
10	Inductive digit := D0 \| D1 \| D2 \| D3 \| D4 \| D5.
		38	Definition tmf := Eval compute in (flip tm).
11	Definition word p : list Sym :=
		39	Notation "c -->* c'" := (c -[ tmf ]->* c') (at level 40).
12	match p with
		40	Notation "c -->+ c'" := (c -[ tmf ]->+ c') (at level 40).
13	\| D0 => [0;1] \| D1 => [1;1;1;1]
		42	(** * Generic composition of one-call segments *)
14	\| D2 => [0;1;1;1;1;1] \| D3 => [1;1;1;1;1;1;1;1]
		43	Lemma segRR_app {t h1 h2 h3 w1 w2 m1 m2}:
15	\| D4 => [0;1;1;1;1;1;1;1;1;1]
		44	segRR t h1 h2 w1 m1 -> segRR t h2 h3 w2 m2 -> segRR t h1 h3 (w1 ++ w2) (m2 ++ m1).
16	\| D5 => [1;1;1;1;1;1;1;1;1;1;1;1]
17	end.
⋯ 18 template-only lines (template 19–39), not in ours
40	forall k, segRLs tm (h^^t) (h^^u)
41	(W^^k ++ word p ++ W^^b) (W^^(k+a) ++ word q ++ W^^c).
42	Proof.	45	Proof.
43	intros H k. rewrite lpow_add, <-app_assoc.
		46	unfold segRR. intros H1 H2 l r. destruct h1 as [q1 v1], h2 as [q2 v2], h3 as [q3 v3].
44	eapply segRLs_concat; [apply walls\|exact H].
		47	rewrite Str_app_assoc. eapply evstep_trans. 1: apply H1.
		48	cbn in *. rewrite Str_app_assoc. apply (H2 (Str_app m1 l) r).
45	Qed.	49	Qed.
47	Record effect := Eff { phase : digit; used : nat; given : nat; sent : nat }.
		50	Lemma segLL_app {t h1 h2 h3 w1 w2 o1 o2}:
48	Fixpoint total (p:digit) (t:nat) : effect :=
		51	segLL t h1 h2 w1 o1 -> segLL t h2 h3 w2 o2 -> segLL t h1 h3 (w1 ++ w2) (o2 ++ o1).
49	match t with
50	\| O => Eff p 0 0 0
⋯ 5 template-only lines (template 51–56), not in ours
57	segRLs tm (h^^t) (h^^sent a) (word p ++ W^^(used a+n))
58	(W^^given a ++ word (phase a) ++ W^^n).
59	Proof.	52	Proof.
60	gen p n. induction t; intros p n; cbn [total phase used given sent].
		53	unfold segLL. intros H1 H2 l r. destruct h1 as [q1 v1], h2 as [q2 v2], h3 as [q3 v3].
61	- constructor.
		54	cbn in *. rewrite Str_app_assoc. eapply evstep_trans. 1: apply (H1 (Str_app w2 l) r).
62	- cbn [lpow]. rewrite <-Nat.add_assoc.
		55	rewrite Str_app_assoc. apply H2.
63	rewrite (lpow_add _ (carry p)).
64	eapply segRLs_trans.
65	+ apply one.
66	+ apply prefix_rule, IHt.
67	Qed.	56	Qed.
68	End Counter.
		57	Lemma segRR_RL_LL {t h1 h2 h3 h4 w1 w2 m w1' w2'}:
70	Lemma total_add p t u :
		58	segRR t h1 h2 w1 m -> segRL t h2 h3 w2 w2' -> segLL t h3 h4 m w1' ->
71	total p (t+u) =
		59	segRL t h1 h4 (w1 ++ w2) (w1' ++ w2').
72	let a := total p t in let b := total (phase a) u in
73	Eff (phase b) (used a+used b) (given a+given b) (sent a+sent b).
74	Proof.	60	Proof.
75	gen p. induction t; intros p; cbn [Nat.add total phase used given sent].
		61	unfold segRR,segRL,segLL. intros H1 H2 H3 l r.
76	- destruct (total p u); reflexivity.
		62	destruct h1 as [q1 v1], h2 as [q2 v2], h3 as [q3 v3], h4 as [q4 v4]. cbn in *.
77	- rewrite IHt. cbn. f_equal; lia.
		63	rewrite Str_app_assoc. eapply evstep_progress_trans. 1: apply H1.
		64	eapply progress_evstep_trans. 1: apply H2.
		65	rewrite Str_app_assoc. apply H3.
78	Qed.	66	Qed.
80	Lemma total_six p : total p 6 = Eff p 2 3 1.
		68	(** * Words (all near-first; a unit word is root-first) *)
81	Proof. destruct p; reflexivity. Qed.
		69	Definition stack j : list Sym := [1] ++ [1;1;1]^^j.
83	Lemma total_period p k r :
		70	Definition blk m j : list Sym := [0] ++ [1;0]^^m ++ stack j.
84	total p (k*6+r) = let a := total p r in
		71	Definition bmid m j : list Sym := [0;1] ++ [0;1;1]^^j ++ [0;1]^^m.
85	Eff (phase a) (k2+used a) (k3+given a) (k+sent a).
		72	Definition lbw m j : list Sym := [0;1;1]^^j ++ [0;1]^^(S m).
		73	Definition xbmid x : list Sym := [0;0;1] ++ [0;1]^^x.
		75	(** * Block lemmas (found with solve_seg) *)
		76	Lemma blkRR_F m j: segRR tmf (F,[]) (F,[]) (blk m j) (bmid m j).
		77	Proof. unfold blk,bmid,stack. solve_seg. Qed.
		78	Lemma blkRR_B m j: segRR tmf (B,[]) (F,[]) (blk m j) (bmid m j).
		79	Proof. unfold blk,bmid,stack. solve_seg. Qed.
		80	Lemma blkLL m j: segLL tmf (D,[]) (D,[]) (lbw m j) (blk m j).
		81	Proof. unfold blk,lbw,stack. solve_seg. Qed.
		82	Lemma sweepLL: segLL tmf (D,[]) (D,[]) [0;1] [0;1].
		83	Proof. solve_seg. Qed.
		84	Lemma leadLL a: segLL tmf (A,[]) (D,[]) (bmid a 1) ([0;1]^^a ++ [0;0] ++ [1;0;1]).
		85	Proof. unfold bmid. solve_seg. Qed.
		86	Lemma xbRR x: segRR tmf (F,[]) (B,[]) ([0] ++ [1;0]^^x ++ [1;1]) (xbmid x).
		87	Proof. unfold xbmid. solve_seg. Qed.
		88	Lemma xbLL x: segLL tmf (D,[]) (A,[]) (xbmid x) ([0] ++ [1;0]^^x ++ [1;1]).
		89	Proof. unfold xbmid. solve_seg. Qed.
		90	Lemma leadstopS a x: segRL tmf (F,[]) (D,[]) ([0;1]^^(S a) ++ [0;0] ++ [1;0]^^(S x))
		91	([0] ++ [1;0]^^a ++ [1;1;1;1] ++ [0] ++ [1;0]^^x).
		92	Proof. solve_seg. Qed.
		93	Lemma leadstop0 x: segRL tmf (F,[]) (D,[]) ([0;0] ++ [1;0]^^(S x)) ([1;1;1] ++ [0] ++ [1;0]^^x).
		94	Proof. solve_seg. Qed.
		95	Lemma stop1 c a: segRL tmf (B,[]) (D,[]) ([0;1]^^(S c) ++ [0;0] ++ [1;0]^^(S a))
		96	([0] ++ [1;0]^^c ++ [1;1;1;1] ++ [0] ++ [1;0]^^a).
		97	Proof. solve_seg. Qed.
		98	Lemma edge0L x f: sideRL tmf (F,[]) (D,[]) (([0] ++ [1;0]^^(S x) ++ [1;1;1]^^f) *> const 0)
		99	(([0] ++ [1;0]^^x ++ [1;1;1]^^(S f)) *> const 0).
		100	Proof. unfold sideRL. intros l. unfold to_DH_config. es. Qed.
		101	Lemma edge0E y f: sideRL tmf (B,[]) (D,[]) (([0] ++ [1;0]^^(S y) ++ [1;1;1]^^f) *> const 0)
		102	(([0] ++ [1;0]^^y ++ [1;1;1]^^(S f)) *> const 0).
		103	Proof. unfold sideRL. intros l. unfold to_DH_config. es. Qed.
		105	(** * Chains of passive blocks *)
		106	Definition blkp (p:nat*nat) := blk (fst p) (snd p).
		107	Definition bmidp (p:nat*nat) := bmid (fst p) (snd p).
		108	Definition lbwp (p:nat*nat) := lbw (fst p) (snd p).
		109	Fixpoint cw (ch:list (nat*nat)) : list Sym := match ch with [] => [] \| p::ch => blkp p ++ cw ch end.
		110	Fixpoint cmid (ch:list (nat*nat)) : list Sym := match ch with [] => [] \| p::ch => cmid ch ++ bmidp p end.
		111	Fixpoint clbw (ch:list (nat*nat)) : list Sym := match ch with [] => [] \| p::ch => clbw ch ++ lbwp p end.
		113	Lemma chainRR ch: segRR tmf (F,[]) (F,[]) (cw ch) (cmid ch).
86	Proof.	114	Proof.
87	induction k; [cbn [Nat.mul Nat.add]; destruct (total p r); reflexivity\|].
		115	induction ch as [\|p ch IH]; cbn [cw cmid].
88	replace (S k6+r) with (6+(k6+r)) by lia.
		116	- unfold segRR. intros. cbn. finish.
89	rewrite total_add,total_six. cbn [phase used given sent].
		117	- exact (segRR_app (blkRR_F (fst p) (snd p)) IH).
90	rewrite IHk. cbn. f_equal; lia.
91	Qed.	118	Qed.
93	Record effectN := EffN { phaseN : digit; usedN : N; givenN : N; sentN : N }.
		119	Lemma chainLL ch: segLL tmf (D,[]) (D,[]) (clbw ch) (cw ch).
94	Definition denote_effect a :=
95	Eff (phaseN a) (N.to_nat (usedN a)) (N.to_nat (givenN a)) (N.to_nat (sentN a)).
⋯ 4 template-only lines (template 96–99), not in ours
100	(k*3+N.of_nat (given a)) (k+N.of_nat (sent a)).
102	Lemma totalN_spec p t : denote_effect (totalN p t) = total p (N.to_nat t).
103	Proof.	120	Proof.
104	unfold totalN,denote_effect; cbn [phaseN usedN givenN sentN].
		121	induction ch as [\|p ch IH]; cbn [cw clbw].
105	rewrite !N2Nat.inj_add, !N2Nat.inj_mul, !Nat2N.id.
		122	- unfold segLL. intros. cbn. finish.
106	replace (N.to_nat t) with (N.to_nat (t/6)*6+N.to_nat (t mod 6)).
		123	- exact (segLL_app IH (blkLL (fst p) (snd p))).
107	- apply eq_sym, total_period.
108	- pose proof (N.div_mod t 6 ltac:(lia)). nia.
109	Qed.	124	Qed.
111	Definition cells := list (digit*N).
		125	Lemma bmid_shift m j: bmid m j ++ [0;1] = [0;1] ++ lbw m j.
112	Fixpoint cell_word (xs:cells) : list Sym := match xs with
		126	Proof. unfold bmid,lbw. rewrite <-!app_assoc. f_equal. f_equal. rewrite lpow_shift. reflexivity. Qed.
113	\| [] => []
		127	Lemma cmid_shift ch: cmid ch ++ [0;1] = [0;1] ++ clbw ch.
114	\| (p,n)::xs => word p ++ W^^N.to_nat n ++ cell_word xs
		128	Proof.
115	end.
		129	induction ch as [\|p ch IH]; cbn [cmid clbw]; [reflexivity\|].
117	Fixpoint batch (t:N) (xs:cells) : option (N*cells) :=
		130	unfold bmidp,lbwp. rewrite <-app_assoc, bmid_shift.
118	match xs with
		131	rewrite (app_assoc (cmid ch) [0;1]), IH. rewrite <-app_assoc. reflexivity.
119	\| [] => if (t=?0)%N then Some (0%N,[]) else None
		132	Qed.
120	\| (p,n)::xs =>
		133	Lemma bmid_S m j: bmid (S m) j = [0;1] ++ lbw m j.
121	let a := totalN p t in
		134	Proof. rewrite <-bmid_shift. unfold bmid. cbn [lpow]. rewrite <-!app_assoc. f_equal. f_equal.
122	if (usedN a<=?n)%N then
		135	rewrite lpow_shift. reflexivity. Qed.
123	match batch (sentN a) xs with
		137	(** prefix = Y block (entered in B) followed by a chain *)
124	\| Some (e,ys) => Some (givenN a,(phaseN a,(n-usedN a+e)%N)::ys)
		138	Definition pw c j ch := blk c j ++ cw ch.
125	\| None => None
		139	Lemma prefRR c j ch: segRR tmf (B,[]) (F,[]) (pw c j ch) (cmid ch ++ bmid c j).
126	end
		140	Proof. exact (segRR_app (blkRR_B c j) (chainRR ch)). Qed.
127	else None
		141	Lemma prefLL c j ch: segLL tmf (D,[]) (D,[]) (cmid ch ++ bmid (S c) j) (pw c j ch ++ [0;1]).
128	end.
		142	Proof.
130	Section BatchCorrect.
		143	rewrite bmid_S, (app_assoc (cmid ch) [0;1]), cmid_shift, <-app_assoc.
131	Variable tm : TM.
		144	unfold pw.
132	Variable h : list (DH0*DH0).
		145	refine (segLL_app sweepLL _).
133	Hypothesis wall : forall n, segRLs tm h h (W^^n) (W^^n).
		146	exact (segLL_app (chainLL ch) (blkLL c j)).
134	Hypothesis one : forall p n,
		147	Qed.
135	segRLs tm h (h^^carry p) (word p ++ W^^(take p+n))
		149	(** * Frames *)
136	(W^^give p ++ word (next p) ++ W^^n).
		150	Lemma segRL_frame {t h1 h2 w w'} u: segRL t h1 h2 w w' -> segRL t h1 h2 (w ++ u) (w' ++ u).
138	Lemma totalN_rule p t n :
		151	Proof. unfold segRL. intros H l r. rewrite !Str_app_assoc. apply H. Qed.
139	(usedN (totalN p t)<=n)%N ->
		153	(** * Digits. lead1 a x: m1 = 2a+1 cells, lead 1111, x = 2x+1 cells;
140	segRLs tm (h^^N.to_nat t) (h^^N.to_nat (sentN (totalN p t)))
		154	lead0 a x: m1 = 2a cells, lead 00, x = 2x cells. For k=1 the "m1" gap is the fuel y. *)
141	(word p ++ W^^N.to_nat n)
		155	Definition lead1 a x : list Sym := blk a 1 ++ [0] ++ [1;0]^^x.
142	(W^^N.to_nat (givenN (totalN p t)) ++ word (phaseN (totalN p t)) ++
		156	Definition lead0 a x : list Sym := [0;1]^^a ++ [0;0] ++ [1;0]^^x.
143	W^^N.to_nat (n-usedN (totalN p t))).
		157	Definition tailw g : list Sym := [1;1] ++ [1;1;1]^^g.
		159	Definition hB : DH0 := (B,[]).
		160	Definition hD : DH0 := (D,[]).
		161	Definition h : list (DH0*DH0) := [(hB,hD)].
		163	Lemma stopK c j ch a x: segRL tmf hB hD (pw (S c) j ch ++ lead0 a (S x)) (pw c j ch ++ lead1 a x).
		164	Proof.
		165	destruct a as [\|a].
		166	- pose proof (segRR_RL_LL (prefRR (S c) j ch) (leadstop0 x) (prefLL c j ch)) as H.
		167	unfold lead0,lead1. applys_eq H. cbn. rewrite <-!app_assoc. reflexivity.
		168	- pose proof (segRR_RL_LL (prefRR (S c) j ch) (leadstopS a x) (prefLL c j ch)) as H.
		169	unfold lead0,lead1. applys_eq H. unfold blk,stack. cbn. rewrite <-!app_assoc. reflexivity.
		170	Qed.
		172	Lemma stopK1 c a: segRL tmf hB hD (lead0 (S c) (S a)) (lead1 c a).
		173	Proof. unfold lead0,lead1,blk,stack. solve_seg. Qed.
		175	Definition passK_mid c j ch a x := (xbmid x ++ bmid a 1) ++ (cmid ch ++ bmid (S c) j).
		176	Lemma passK_RR c j ch a x: segRR tmf hB hB (pw (S c) j ch ++ lead1 a x ++ [1;1]) (passK_mid c j ch a x).
		177	Proof.
		178	unfold lead1, passK_mid. rewrite <-!app_assoc.
		179	pose proof (segRR_app (prefRR (S c) j ch) (segRR_app (blkRR_F a 1) (xbRR x))) as H.
		180	rewrite <-!app_assoc in H. exact H.
		181	Qed.
		182	Lemma passK_LL c j ch a x: segLL tmf hD hD (passK_mid c j ch a x) (pw c j ch ++ lead0 (S a) (S (S x)) ++ [1;1]).
		183	Proof.
		184	unfold passK_mid.
		185	pose proof (segLL_app (segLL_app (xbLL x) (leadLL a)) (prefLL c j ch)) as H.
		186	applys_eq H. unfold lead0. cbn [lpow]. rewrite <-!app_assoc. cbn. reflexivity.
		187	Qed.
		188	Lemma passK c j ch a x: segRLs tmf h h (pw (S c) j ch ++ lead1 a x ++ [1;1]) (pw c j ch ++ lead0 (S a) (S (S x)) ++ [1;1]).
		189	Proof.
		190	unfold h. applys_eq (segRLs_lrcons tmf [] [] [] _ _ _ _ _ hB hD hB hD
		191	(passK_RR c j ch a x) (passK_LL c j ch a x) (segLRs_O _ _) (segRLs_O _ _)).
		192	Qed.
		194	Definition passK1_mid c x := xbmid x ++ bmid c 1.
		195	Lemma passK1_RR c x: segRR tmf hB hB (lead1 c x ++ [1;1]) (passK1_mid c x).
		196	Proof. unfold lead1,passK1_mid. rewrite <-!app_assoc. exact (segRR_app (blkRR_B c 1) (xbRR x)). Qed.
		197	Lemma passK1_LL c x: segLL tmf hD hD (passK1_mid c x) (lead0 c (S (S x)) ++ [1;1]).
		198	Proof.
		199	unfold passK1_mid. pose proof (segLL_app (xbLL x) (leadLL c)) as H.
		200	applys_eq H. unfold lead0. cbn [lpow]. rewrite <-!app_assoc. cbn. reflexivity.
		201	Qed.
		202	Lemma passK1 c x: segRLs tmf h h (lead1 c x ++ [1;1]) (lead0 c (S (S x)) ++ [1;1]).
		203	Proof.
		204	unfold h. applys_eq (segRLs_lrcons tmf [] [] [] _ _ _ _ _ hB hD hB hD
		205	(passK1_RR c x) (passK1_LL c x) (segLRs_O _ _) (segRLs_O _ _)).
		206	Qed.
		208	(** halting call: a k=1 digit with lead 00 and no fuel *)
		209	Lemma halt0 x l r: halts tmf (l {{B}}> lead0 0 x *> r).
		210	Proof. unfold lead0. cbn. solve_halt. Qed.
		212	(** * U0 (the unit next to the edge) and the edge 1^(3f) *)
		213	Lemma edge0L0 f: sideRL tmf (F,[]) (D,[]) (([0] ++ [1;1;1]^^f) *> const 0)
		214	(([1;1] ++ [1;1;1]^^f) *> const 0).
		215	Proof. unfold sideRL. intros l. unfold to_DH_config. es. Qed.
		216	Lemma segRR_sideRL_LL {t h1 h2 h3 h4 w m w' r r'}:
		217	segRR t h1 h2 w m -> sideRL t h2 h3 r r' -> segLL t h3 h4 m w' ->
		218	sideRL t h1 h4 (w > r) (w' > r').
		219	Proof.
		220	unfold segRR,sideRL,segLL. intros H1 H2 H3 l.
		221	destruct h1 as [q1 v1], h2 as [q2 v2], h3 as [q3 v3], h4 as [q4 v4]. cbn in *.
		222	eapply evstep_progress_trans. 1: apply H1.
		223	eapply progress_evstep_trans. 1: apply H2.
		224	apply H3.
		225	Qed.
		226	Definition edgew x f : list Sym := [0] ++ [1;0]^^x ++ [1;1;1]^^f.
		227	(** leadless U0: prefix, then the gap x (2x+1 cells), then the edge *)
		228	Lemma u0L c j ch x f: sideRL tmf hB hD ((pw (S c) j ch ++ edgew x f) *> const 0)
		229	((pw c j ch ++ edgew x (S f)) *> const 0).
		230	Proof.
		231	rewrite !Str_app_assoc. destruct x as [\|x].
		232	- pose proof (segRR_sideRL_LL (prefRR (S c) j ch) (edge0L0 f) (prefLL c j ch)) as H.
		233	applys_eq H. unfold edgew. rewrite <-!Str_app_assoc. f_equal. rewrite <-!app_assoc. reflexivity.
		234	- pose proof (segRR_sideRL_LL (prefRR (S c) j ch) (edge0L x f) (prefLL c j ch)) as H.
		235	applys_eq H. unfold edgew. rewrite <-!Str_app_assoc. f_equal. rewrite <-!app_assoc. reflexivity.
		236	Qed.
		237	(** empty U0 *)
		238	Lemma u0E y f: sideRL tmf hB hD (edgew (S y) f > const 0) (edgew y (S f) > const 0).
		239	Proof. unfold edgew. exact (edge0E y f). Qed.
		241	(** * The root: tail gap 2t+1 and the tail boundary 11 *)
		242	Definition root t (X:side) : Q * tape := const 0 <{{A}} ([0;1]^^t ++ [0;1;1]) *> X.
		243	Definition wmid t : list Sym := [0] ++ [0;1]^^t ++ [0;1;0;1].
		244	Lemma root_in t X: root t X -->* wmid t *> const 0 {{B}}> X.
		245	Proof. unfold root,wmid. es. Qed.
		246	Lemma sweepA: forall l r n, l <* [0;1]^^n <{{A}} r -->* l <{{A}} [0;1]^^n *> r.
		247	Proof. apply (shift_rule_L [] tmf [0;1] [0;1] A). intros. es. Qed.
		248	Lemma root_out t X: wmid t > const 0 <{{D}} X --> root (S t) X.
		249	Proof.
		250	unfold root,wmid. simpl_tape. step. follow sweepA. do 4 step.
		251	apply evstep_refl'. cbn [lpow app Str_app].
		252	change (0 >> 1 >> 1 >> X) with ([0;1] *> 1 >> X). rewrite lpow_shift'. reflexivity.
		253	Qed.
		254	Lemma root_step t X X': sideRL tmf hB hD X X' -> root t X -->+ root (S t) X'.
144	Proof.	255	Proof.
145	intros H.	256	intros H.
146	pose proof (total_spec tm h wall one (N.to_nat t) p
		257	eapply evstep_progress_trans. 1: apply root_in.
147	(N.to_nat (n-usedN (totalN p t)))) as I.
		258	eapply progress_evstep_trans. 1: apply (H (wmid t *> const 0)).
148	rewrite <-totalN_spec in I. cbn [denote_effect phase used given sent] in I.
		259	apply root_out.
149	applys_eq I; flia.
150	Qed.	260	Qed.
152	Lemma batch_spec t xs e ys :
		261	Lemma root_steps n: forall t X X', sideRLs tmf (h^^n) X X' -> root t X -->* root (n+t) X'.
153	batch t xs = Some (e,ys) ->
154	segRLs tm (h^^N.to_nat t) [] (cell_word xs)
155	(W^^N.to_nat e ++ cell_word ys).
156	Proof.	262	Proof.
157	gen t e ys. induction xs as [\|[p n] xs IH]; intros t e ys H; cbn [batch] in H.
		263	induction n; intros t X X' H.
158	- destruct (N.eqb_spec t 0); inverts H. subst t. constructor.
		264	- inverts H. finish.
159	- destruct (N.leb_spec (usedN (totalN p t)) n); try discriminate.
		265	- cbn [lpow h app] in H. inverts H.
160	destruct (batch (sentN (totalN p t)) xs) as [[e' ys']\|] eqn:E; inverts H.
		266	eapply evstep_trans. 1: apply progress_evstep, root_step; eassumption.
161	specialize (IH _ _ _ E).
		267	replace (S n + t) with (n + S t) by lia. apply IHn. assumption.
162	pose proof (totalN_rule p t n H0) as I.
163	change (segRLs tm (h^^N.to_nat t) [] (cell_word ((p,n)::xs))
⋯ 4 template-only lines (template 164–167), not in ours
168	repeat rewrite app_assoc.
169	applys_eq (segRLs_concat I IH); repeat rewrite app_assoc; reflexivity.
170	Qed.	268	Qed.
171	End BatchCorrect.
		269	Lemma root_halt t X: sideRLs_halt tmf h X -> halts tmf (root t X).
173	Record scan := Scan { scan_q : Q; scan_dir : dir;
		270	Proof. intros H. eapply halts_evstep. 2: apply root_in. apply (sideRLs_halt_single _ _ _ _ H). Qed.
174	scan_in : list Sym; scan_out : list Sym; scan_context : list Sym }.
		273	(** * Uniform touch lemmas. A unit is [cw bs ++ leadw b a x ++ far]; every touch moves all
175	Definition scan_valid tm s := forall n l r,
		274	passive walls two cells toward the root, i.e. consumes the two root-most cells [0;1]. *)
176	match scan_dir s with
		275	Definition hF : DH0 := (F,[]).
177	\| R =>
		276	Definition leadw (b:bool) a x := if b then lead1 a x else lead0 a x.
178	l <* (rev (scan_context s)) {{scan_q s}}> (scan_in s)^^n > r -[tm]->
		277	Definition uw bs b a x (far:list Sym) := cw bs ++ leadw b a x ++ far.
179	l <* (rev (scan_out s))^^n <* (rev (scan_context s)) {{scan_q s}}> r
		278	Definition consume (bs: list (natnat)) (a:nat) : option (nat list (natnat) nat) :=
180	\| L =>
		279	match bs with
181	l <* (rev (scan_in s))^^n <{{scan_q s}} (scan_context s) > r -[tm]->
		280	\| (S c, j) :: r => Some (O, (c,j)::r, a)
182	l <{{scan_q s}} (scan_context s) > (scan_out s)^^n > r
		281	\| (O, j) :: r => Some (j, r, a)
		282	\| [] => match a with S a' => Some (O, [], a') \| O => None end
183	end.	283	end.
185	Definition head q : list (DH0*DH0) := [((q,<[1;0;1]),(q,[1]))].
		284	Lemma cw_app l1 l2: cw (l1 ++ l2) = cw l1 ++ cw l2.
186	Definition start (q:Q) (r:side) := 0inf <* <[1;0;1] {{q}}> r.
		285	Proof. induction l1 as [\|p l1 IH]; cbn; [reflexivity\|]. rewrite IH, app_assoc. reflexivity. Qed.
188	Section RootCorrect.
		287	Lemma yLL_glue j: segLL tmf (D,[]) (D,[]) ([0;1;1]^^j) ([1;1;1]^^j).
189	Variable tm : TM.
		288	Proof. solve_seg. Qed.
190	Variable q : Q.
		289	Lemma prefLL_glue j ch: segLL tmf (D,[]) (D,[]) (cmid ch ++ bmid 0 j) ([1;1;1]^^j ++ cw ch ++ [0;1]).
191	Hypothesis emit : forall r,
192	0inf <{{q}} [1] > r -[tm]-> start q r.
194	Lemma calls_spec t r r' : sideRLs tm ((head q)^^t) r r' ->
195	start q r -[tm]->* start q r'.
196	Proof.	290	Proof.
197	gen r r'. induction t; intros r r' H; cbn [lpow head app] in H.
		291	unfold bmid. cbn [lpow]. rewrite app_nil_r.
198	- inverts H. constructor.
		292	rewrite (app_assoc (cmid ch) [0;1]), cmid_shift, <-app_assoc.
199	- inverts H.
		293	pose proof (segLL_app sweepLL (segLL_app (chainLL ch) (yLL_glue j))) as H.
200	match goal with
		294	applys_eq H. rewrite <-!app_assoc. reflexivity.
201	\| Hret : sideRL _ _ _ _ _ \|- _ => follow100 Hret
		295	Qed.
		297	(** generic compositions: prefix out (B->F), a core entered in F, prefix back (D->D) *)
		298	Lemma gen_RL {ci co} (HF: segRL tmf hF hD ci co) c j ch:
		299	segRL tmf hB hD (pw (S c) j ch ++ ci) (pw c j ch ++ [0;1] ++ co).
		300	Proof.
		301	pose proof (segRR_RL_LL (prefRR (S c) j ch) HF (prefLL c j ch)) as H.
		302	applys_eq H. rewrite <-!app_assoc. reflexivity.
		303	Qed.
		304	Lemma gen_RLg {ci co} (HF: segRL tmf hF hD ci co) j ch:
		305	segRL tmf hB hD (pw 0 j ch ++ ci) ([1;1;1]^^j ++ cw ch ++ [0;1] ++ co).
		306	Proof.
		307	pose proof (segRR_RL_LL (prefRR 0 j ch) HF (prefLL_glue j ch)) as H.
		308	applys_eq H. rewrite <-!app_assoc. reflexivity.
		309	Qed.
		310	Lemma lrcons1 {w1 w2 m}: segRR tmf hB hB w1 m -> segLL tmf hD hD m w2 -> segRLs tmf h h w1 w2.
		311	Proof.
		312	intros H1 H2. unfold h.
		313	applys_eq (segRLs_lrcons tmf [] [] [] _ _ _ _ _ hB hD hB hD H1 H2 (segLRs_O _ _) (segRLs_O _ _)).
		314	Qed.
		315	Lemma gen_fwd {ci m co} (HR: segRR tmf hF hB ci m) (HL: segLL tmf hD hD m co) c j ch:
		316	segRLs tmf h h (pw (S c) j ch ++ ci) (pw c j ch ++ [0;1] ++ co).
		317	Proof.
		318	pose proof (lrcons1 (segRR_app (prefRR (S c) j ch) HR) (segLL_app HL (prefLL c j ch))) as H.
		319	applys_eq H. rewrite <-!app_assoc. reflexivity.
		320	Qed.
		321	Lemma gen_fwdg {ci m co} (HR: segRR tmf hF hB ci m) (HL: segLL tmf hD hD m co) j ch:
		322	segRLs tmf h h (pw 0 j ch ++ ci) ([1;1;1]^^j ++ cw ch ++ [0;1] ++ co).
		323	Proof.
		324	pose proof (lrcons1 (segRR_app (prefRR 0 j ch) HR) (segLL_app HL (prefLL_glue j ch))) as H.
		325	applys_eq H. rewrite <-!app_assoc. reflexivity.
		326	Qed.
		327	Lemma gen_side {ci co R R'} (HF: sideRL tmf hF hD (ci > R) (co > R')) c j ch:
		328	sideRL tmf hB hD ((pw (S c) j ch ++ ci) > R) ((pw c j ch ++ [0;1] ++ co) > R').
		329	Proof.
		330	pose proof (segRR_sideRL_LL (prefRR (S c) j ch) HF (prefLL c j ch)) as H.
		331	applys_eq H; rewrite <-!Str_app_assoc; f_equal; rewrite <-!app_assoc; reflexivity.
		332	Qed.
		333	Lemma gen_sideg {ci co R R'} (HF: sideRL tmf hF hD (ci > R) (co > R')) j ch:
		334	sideRL tmf hB hD ((pw 0 j ch ++ ci) > R) (([1;1;1]^^j ++ cw ch ++ [0;1] ++ co) > R').
		335	Proof.
		336	pose proof (segRR_sideRL_LL (prefRR 0 j ch) HF (prefLL_glue j ch)) as H.
		337	applys_eq H; rewrite <-!Str_app_assoc; f_equal; rewrite <-!app_assoc; reflexivity.
		338	Qed.
		339	Lemma segRL_side {t h1 h2 w w'} R: segRL t h1 h2 w w' -> sideRL t h1 h2 (w > R) (w' > R).
		340	Proof. unfold segRL,sideRL. intros H l. destruct h1 as [q1 v1], h2 as [q2 v2]. cbn. apply H. Qed.
		342	Ltac injE E := injection E; intros; subst; clear E.
		343	Ltac lnorm2 := unfold uw,leadw,pw; do 3 (rewrite ?cw_app; cbn [cw]); unfold blkp,lead0,lead1,blk,stack,tailw,edgew; cbn [fst snd lpow];
		344	rewrite ?app_nil_r, ?app_nil_l; repeat rewrite <-app_assoc; cbn [app];
		345	repeat (rewrite lpow_rotate_list; cbn [app]); try reflexivity.
		347	( cores *)
		348	Lemma cstopF a x far: exists co, segRL tmf hF hD (lead0 a (S x) ++ far) co /\ [0;1] ++ co = lead1 a x ++ far.
		349	Proof.
		350	destruct a as [\|a].
		351	- eexists. split. 1: exact (segRL_frame far (leadstop0 x)). lnorm2.
		352	- eexists. split. 1: exact (segRL_frame far (leadstopS a x)). lnorm2.
		353	Qed.
		354	Lemma t_stop bs a x far ov bs' a': consume bs a = Some (ov, bs', a') ->
		355	segRL tmf hB hD (uw bs false a (S x) far) ([1;1;1]^^ov ++ uw bs' true a' x far).
		356	Proof.
		357	destruct (cstopF a x far) as [co [HF HE]].
		358	destruct bs as [\|[[\|c] j] r]; cbn [consume]; intros E.
		359	- destruct a as [\|a]; [discriminate\|]. injection E as E1 E2 E3; subst ov bs' a'.
		360	pose proof (segRL_frame far (stopK1 a x)) as H. applys_eq H; lnorm2.
		361	- injection E as E1 E2 E3; subst ov bs' a'. pose proof (gen_RLg HF j r) as H. rewrite HE in H. applys_eq H; lnorm2.
		362	- injection E as E1 E2 E3; subst ov bs' a'. pose proof (gen_RL HF c j r) as H. rewrite HE in H. applys_eq H; lnorm2.
		363	Qed.
		365	Definition cpass_mid a x := xbmid x ++ bmid a 1.
		366	Lemma cpassRR a x: segRR tmf hF hB (lead1 a x ++ [1;1]) (cpass_mid a x).
		367	Proof. unfold lead1,cpass_mid. rewrite <-!app_assoc. exact (segRR_app (blkRR_F a 1) (xbRR x)). Qed.
		368	Definition cpass_co a x := ([0;1]^^a ++ [0;0] ++ [1;0;1]) ++ ([0] ++ [1;0]^^x ++ [1;1]).
		369	Lemma cpassLL a x: segLL tmf hD hD (cpass_mid a x) (cpass_co a x).
		370	Proof. unfold cpass_mid,cpass_co. exact (segLL_app (xbLL x) (leadLL a)). Qed.
		371	Lemma t_pass bs a x ov bs' a': consume bs (S a) = Some (ov, bs', a') ->
		372	segRLs tmf h h (uw bs true a x (tailw 0)) ([1;1;1]^^ov ++ uw bs' false a' (S (S x)) (tailw 0)).
		373	Proof.
		374	destruct bs as [\|[[\|c] j] r]; cbn [consume]; intros E; injection E as E1 E2 E3; subst ov bs' a'.
		375	- pose proof (passK1 a x) as H. applys_eq H; lnorm2.
		376	- pose proof (gen_fwdg (cpassRR a x) (cpassLL a x) j r) as H. applys_eq H; unfold cpass_co; lnorm2.
		377	- pose proof (gen_fwd (cpassRR a x) (cpassLL a x) c j r) as H. applys_eq H; unfold cpass_co; lnorm2.
		378	Qed.
		380	( unglue: the glued walls of the far neighbour come in; the first becomes a 00 lead *)
		381	Definition um1 a x : list Sym := [0;0;1;0;1;1;0;1;0;1] ++ [0;1]^^x ++ [1] ++ [0;1]^^a.
		382	Definition um2 a x g : list Sym := [0;0;1;0;1;1;0;1;1;0;1] ++ [1;0;1]^^g ++ [0;1] ++ [0;1]^^x ++ [1] ++ [0;1]^^a.
		383	Definition uco1 a x : list Sym := [0;1]^^a ++ [1;1;1;0;1;0] ++ [1;0]^^x ++ [0;1;0;1;1].
		384	Definition uco2 a x g : list Sym := [0;1]^^a ++ [1;1;1;0;1] ++ [0;1]^^x ++ [1;1;1] ++ [1;1;1]^^g ++ [0;0;1;0;1;1].
		385	Lemma u1RF a x: segRR tmf hF hB (lead1 a x ++ tailw 1) (um1 a x).
		386	Proof. unfold lead1,blk,stack,tailw,um1,hF,hB. solve_seg. Qed.
		387	Lemma u1RB a x: segRR tmf hB hB (lead1 a x ++ tailw 1) (um1 a x).
		388	Proof. unfold lead1,blk,stack,tailw,um1,hB. solve_seg. Qed.
		389	Lemma u1L a x: segLL tmf hD hD (um1 a x) (uco1 a x).
		390	Proof. unfold um1,uco1,hD. solve_seg. Qed.
		391	Lemma u2RF a x g: segRR tmf hF hB (lead1 a x ++ tailw (S (S g))) (um2 a x g).
		392	Proof. unfold lead1,blk,stack,tailw,um2,hF,hB. solve_seg. Qed.
		393	Lemma u2RB a x g: segRR tmf hB hB (lead1 a x ++ tailw (S (S g))) (um2 a x g).
		394	Proof. unfold lead1,blk,stack,tailw,um2,hB. solve_seg. Qed.
		395	Lemma u2L a x g: segLL tmf hD hD (um2 a x g) (uco2 a x g).
		396	Proof. unfold um2,uco2,hD. solve_seg. Qed.
		398	Lemma t_ungl1 bs a x ov bs' a': consume (bs ++ [(a,1%nat)]) (S x) = Some (ov, bs', a') ->
		399	segRLs tmf h h (uw bs true a x (tailw 1)) ([1;1;1]^^ov ++ uw bs' false a' 1 (tailw 0)).
		400	Proof.
		401	destruct bs as [\|[[\|c] j] r]; cbn [app consume].
		402	- destruct a as [\|a]; intros E; injection E as E1 E2 E3; subst ov bs' a'.
		403	+ pose proof (lrcons1 (u1RB 0 x) (u1L 0 x)) as H. applys_eq H; unfold uco1; lnorm2.
		404	+ pose proof (lrcons1 (u1RB (S a) x) (u1L (S a) x)) as H. applys_eq H; unfold uco1; lnorm2.
		405	- intros E; injection E as E1 E2 E3; subst ov bs' a'.
		406	pose proof (gen_fwdg (u1RF a x) (u1L a x) j r) as H. applys_eq H; unfold uco1; rewrite ?cw_app; lnorm2.
		407	- intros E; injection E as E1 E2 E3; subst ov bs' a'.
		408	pose proof (gen_fwd (u1RF a x) (u1L a x) c j r) as H. applys_eq H; unfold uco1; rewrite ?cw_app; lnorm2.
		409	Qed.
		410	Lemma t_ungl2 bs a x g ov bs' a': consume (bs ++ [(a,1%nat);(x,S g)]) 0%nat = Some (ov, bs', a') ->
		411	segRLs tmf h h (uw bs true a x (tailw (S (S g)))) ([1;1;1]^^ov ++ uw bs' false a' 1 (tailw 0)).
		412	Proof.
		413	destruct bs as [\|[[\|c] j] r]; cbn [app consume].
		414	- destruct a as [\|a]; intros E; injection E as E1 E2 E3; subst ov bs' a'.
		415	+ pose proof (lrcons1 (u2RB 0 x g) (u2L 0 x g)) as H. applys_eq H; unfold uco2; lnorm2.
		416	+ pose proof (lrcons1 (u2RB (S a) x g) (u2L (S a) x g)) as H. applys_eq H; unfold uco2; lnorm2.
		417	- intros E; injection E as E1 E2 E3; subst ov bs' a'.
		418	pose proof (gen_fwdg (u2RF a x g) (u2L a x g) j r) as H. applys_eq H; unfold uco2; rewrite ?cw_app; lnorm2.
		419	- intros E; injection E as E1 E2 E3; subst ov bs' a'.
		420	pose proof (gen_fwd (u2RF a x g) (u2L a x g) c j r) as H. applys_eq H; unfold uco2; rewrite ?cw_app; lnorm2.
		421	Qed.
		423	( the halting call *)
		424	Lemma t_halt x far l r: halts tmf (l {{B}}> uw [] false 0 x far *> r).
		425	Proof. unfold uw, leadw. cbn [cw app]. rewrite Str_app_assoc. apply halt0. Qed.
		427	( U0 next to the edge. Edge class 0: [1;1;1]^^f; class 1: [1] ++ [1;1;1]^^f *)
		428	Definition edge1w f : list Sym := [1] ++ [1;1;1]^^f.
		429	Lemma z_lead bs x f ov bs' a': bs <> [] -> consume bs 0%nat = Some (ov, bs', a') ->
		430	sideRL tmf hB hD ((cw bs ++ edgew x f) > const 0) (([1;1;1]^^ov ++ cw bs' ++ edgew x (S f)) > const 0).
		431	Proof.
		432	intros NE. destruct bs as [\|[[\|c] j] r]; [congruence\| \|]; cbn [consume]; intros E; injection E as E1 E2 E3; subst ov bs' a'.
		433	- destruct x as [\|x].
		434	+ pose proof (gen_sideg (edge0L0 f) j r) as H. applys_eq H; rewrite <-?Str_app_assoc; f_equal; lnorm2.
		435	+ pose proof (gen_sideg (edge0L x f) j r) as H. applys_eq H; rewrite <-?Str_app_assoc; f_equal; lnorm2.
		436	- destruct x as [\|x].
		437	+ pose proof (gen_side (edge0L0 f) c j r) as H. applys_eq H; rewrite <-?Str_app_assoc; f_equal; lnorm2.
		438	+ pose proof (gen_side (edge0L x f) c j r) as H. applys_eq H; rewrite <-?Str_app_assoc; f_equal; lnorm2.
		439	Qed.
		440	Lemma z_empty y f: sideRL tmf hB hD (edgew (S y) f > const 0) (edgew y (S f) > const 0).
		441	Proof. apply u0E. Qed.
		442	Lemma z_absorb f: sideRL tmf hB hD (edgew 0 (S f) > const 0) (([1;1] ++ [1;1;1]^^(S f)) > const 0).
		443	Proof. unfold sideRL. intros l. unfold to_DH_config, edgew, hB, hD. es. Qed.
		444	Lemma z_stop bs a x f ov bs' a': consume bs a = Some (ov, bs', a') ->
		445	sideRL tmf hB hD (uw bs false a (S x) (edge1w f) > const 0) (([1;1;1]^^ov ++ uw bs' true a' x (edge1w f)) > const 0).
		446	Proof. intros E. apply segRL_side, t_stop, E. Qed.
		447	Definition zco a x f : list Sym := [0;1]^^a ++ [1;1;1;0;1] ++ [0;1]^^x ++ [1;1;1]^^f ++ [0;1;1;1].
		448	Lemma z1F a x f: sideRL tmf hF hD ((lead1 a x ++ edge1w f) > const 0) (zco a x f > const 0).
		449	Proof. unfold sideRL. intros l. unfold to_DH_config, lead1, blk, stack, edge1w, zco, hF, hD. es. Qed.
		450	Lemma z1B a x f: sideRL tmf hB hD ((lead1 a x ++ edge1w f) > const 0) (zco a x f > const 0).
		451	Proof. unfold sideRL. intros l. unfold to_DH_config, lead1, blk, stack, edge1w, zco, hB, hD. es. Qed.
		452	Lemma z_1111 bs a x f ov bs' a': consume (bs ++ [(a,1%nat);(x,f)]) 0%nat = Some (ov, bs', a') ->
		453	sideRL tmf hB hD (uw bs true a x (edge1w f) > const 0) (([1;1;1]^^ov ++ cw bs' ++ edgew 0 1) > const 0).
		454	Proof.
		455	unfold uw, leadw. destruct bs as [\|[[\|c] j] r]; cbn [app consume].
		456	- destruct a as [\|a]; intros E; injection E as E1 E2 E3; subst ov bs' a'.
		457	+ pose proof (z1B 0 x f) as H. applys_eq H; rewrite <-?Str_app_assoc; f_equal; unfold zco; lnorm2.
		458	+ pose proof (z1B (S a) x f) as H. applys_eq H; rewrite <-?Str_app_assoc; f_equal; unfold zco; lnorm2.
		459	- intros E; injection E as E1 E2 E3; subst ov bs' a'.
		460	pose proof (gen_sideg (z1F a x f) j r) as H. applys_eq H; rewrite <-?Str_app_assoc; f_equal; unfold zco; rewrite ?cw_app; lnorm2.
		461	- intros E; injection E as E1 E2 E3; subst ov bs' a'.
		462	pose proof (gen_side (z1F a x f) c j r) as H. applys_eq H; rewrite <-?Str_app_assoc; f_equal; unfold zco; rewrite ?cw_app; lnorm2.
		463	Qed.
		465	( resets at the root *)
		466	Definition NT s g (X:side) : Q * tape := const 0 <{{A}} ([1;0]^^s ++ [1] ++ [0;0] ++ [1;0] ++ tailw g) *> X.
		467	Definition rmid t : list Sym := [0;0;1;0;1;1;0;1;0] ++ [1;0]^^t.
		468	Lemma reset1_in t X: root t ([1;1;1] > X) --> rmid t *> const 0 {{B}}> X.
		469	Proof. unfold root,rmid. es. Qed.
		470	Lemma reset1_out t X: rmid t > const 0 <{{D}} X --> NT (S t) 0 X.
		471	Proof. unfold rmid,NT,tailw. es. Qed.
		472	Lemma reset1 t X X': sideRL tmf hB hD X X' -> root t ([1;1;1] > X) --> NT (S t) 0 X'.
		473	Proof.
		474	intros H. eapply evstep_trans. 1: apply reset1_in.
		475	eapply evstep_trans. 2: apply reset1_out.
		476	apply progress_evstep. apply (H (rmid t *> const 0)).
		477	Qed.
		478	Lemma reset1_halt t X: sideRLs_halt tmf h X -> halts tmf (root t ([1;1;1] *> X)).
		479	Proof. intros H. eapply halts_evstep. 2: apply reset1_in. apply (sideRLs_halt_single _ _ _ _ H). Qed.
		480	Lemma reset2 s g X: NT (S s) g X -->* root 0 ((lead1 s 0 ++ tailw g) *> X).
		481	Proof. unfold NT,root,lead1,blk,stack,tailw. es. Qed.
		483	(** * Records with N fields (computation) and their words *)
		484	Definition cvp (p:NN) : natnat := (N.to_nat (fst p), N.to_nat (snd p)).
		485	Definition cvl (bs:list (N*N)) := map cvp bs.
		486	Record unitN := UN { ubs : list (N*N); ubit : bool; ua : N; ux : N; ug : N }.
		487	Definition uwN u := uw (cvl (ubs u)) (ubit u) (N.to_nat (ua u)) (N.to_nat (ux u)) (tailw (N.to_nat (ug u))).
		488	Fixpoint dwords (us:list unitN) : list Sym := match us with [] => [] \| u::us => uwN u ++ dwords us end.
		489	Inductive zN := Z0 (bs:list (NN)) (x f:N) \| ZD (bs:list (NN)) (b:bool) (a x f:N).
		490	Definition zside z : side := match z with
		491	\| Z0 bs x f => (cw (cvl bs) ++ edgew (N.to_nat x) (N.to_nat f)) *> const 0
		492	\| ZD bs b a x f => uw (cvl bs) b (N.to_nat a) (N.to_nat x) (edge1w (N.to_nat f)) *> const 0 end.
		493	Inductive tailN := TT (t g:N) \| NTl (s g:N).
		494	Record cfg := Cfg { ctl : tailN; cus : list unitN; cz : zN }.
		495	Definition denote c : Q * tape := match ctl c with
		496	\| TT t g => root (N.to_nat t) (([1;1;1]^^(N.to_nat g) ++ dwords (cus c)) *> zside (cz c))
		497	\| NTl s g => NT (N.to_nat s) (N.to_nat g) (dwords (cus c) *> zside (cz c)) end.
		499	Definition consumeN (bs:list (NN)) (a:N) : option (N list (NN) N) :=
		500	match bs with
		501	\| (c, j) :: r => if N.eqb c 0 then Some (j, r, a) else Some (0%N, (N.pred c, j)::r, a)
		502	\| [] => if N.eqb a 0 then None else Some (0%N, [], N.pred a)
202	end.	503	end.
203	follow emit. apply IHt; assumption.
		504	Lemma consumeN_spec bs a ov bs' a': consumeN bs a = Some (ov, bs', a') ->
		505	consume (cvl bs) (N.to_nat a) = Some (N.to_nat ov, cvl bs', N.to_nat a').
		506	Proof.
		507	destruct bs as [\|[c j] r]; cbn.
		508	- destruct (N.eqb_spec a 0); [discriminate\|]. intros E; injection E as E1 E2 E3; subst.
		509	replace (N.to_nat a) with (S (N.to_nat (N.pred a))) by lia. reflexivity.
		510	- destruct (N.eqb_spec c 0) as [Hc\|Hc]; intros E; injection E as E1 E2 E3; subst.
		511	+ reflexivity.
		512	+ unfold cvp; cbn. replace (N.to_nat c) with (S (N.to_nat (N.pred c))) by lia. reflexivity.
204	Qed.	513	Qed.
206	Hypothesis wall : forall n, segRLs tm (head q) (head q) (W^^n) (W^^n).
		514	Arguments consumeN : simpl never.
207	Hypothesis one : forall p n,
		515	Lemma cvl_app l1 l2: cvl (l1 ++ l2) = cvl l1 ++ cvl l2.
208	segRLs tm (head q) ((head q)^^carry p) (word p ++ W^^(take p+n))
		516	Proof. apply map_app. Qed.
209	(W^^give p ++ word (next p) ++ W^^n).
		518	( one touch *)
211	Lemma batch_root t xs e ys k r : batch t xs=Some (e,ys) ->
		519	Inductive tres := TStop (ov:N) (u:unitN) \| TPass (ov:N) (u:unitN) \| THalt \| TFail.
212	start q (W^^N.to_nat k > cell_word xs > r) -[tm]->*
		520	Definition touchN u : tres :=
213	start q (W^^N.to_nat (k+e) > cell_word ys > r).
		521	if ubit u then
		522	if N.eqb (ug u) 0 then
		523	match consumeN (ubs u) (N.succ (ua u)) with Some (ov,bs',a') => TPass ov (UN bs' false a' (ux u + 2) 0) \| None => TFail end
		524	else if N.eqb (ug u) 1 then
		525	match consumeN (ubs u ++ [(ua u, 1%N)]) (N.succ (ux u)) with Some (ov,bs',a') => TPass ov (UN bs' false a' 1 0) \| None => TFail end
		526	else
		527	match consumeN (ubs u ++ [(ua u, 1%N); (ux u, ug u - 1)%N]) 0%N with Some (ov,bs',a') => TPass ov (UN bs' false a' 1 0) \| None => TFail end
		528	else
		529	match ubs u, N.eqb (ua u) 0 with
		530	\| [], true => THalt
		531	\| _, _ => if N.eqb (ux u) 0 then TFail else
		532	match consumeN (ubs u) (ua u) with Some (ov,bs',a') => TStop ov (UN bs' true a' (N.pred (ux u)) (ug u)) \| None => TFail end
		533	end.
		535	Ltac nat_of := cbn [cvp fst snd]; rewrite ?N2Nat.inj_succ, ?N2Nat.inj_add, ?N2Nat.inj_pred.
		537	Lemma touchN_stop u ov u': touchN u = TStop ov u' -> segRL tmf hB hD (uwN u) ([1;1;1]^^(N.to_nat ov) ++ uwN u').
214	Proof.	538	Proof.
215	intros H. apply (calls_spec (N.to_nat t)).
		539	destruct u as [bs [] a x g]; unfold touchN; cbn [ubit ubs ua ux ug].
216	rewrite N2Nat.inj_add,lpow_add,Str_app_assoc.
		540	- destruct (N.eqb g 0); [\|destruct (N.eqb g 1)];
217	eapply segRLs_sideRLs_concat; [apply walls,wall\|].
		541	match goal with \|- context [consumeN ?b ?c] => destruct (consumeN b c) as [[[? ?] ?]\|] end; discriminate.
218	pose proof (segRLs_sideRLs_concat
		542	- intros E. assert (Hx: N.eqb x 0 = false /\ consumeN bs a = Some (ov, ubs u', ua u') /\ ubit u' = true
219	(batch_spec tm (head q) wall one t xs e ys H) (sideRLseq_O tm r)) as I.
		543	/\ ux u' = N.pred x /\ ug u' = g).
220	rewrite Str_app_assoc in I. exact I.
		544	{ destruct bs as [\|p bs]; [destruct (N.eqb a 0)\|]; cbn in E; try discriminate;
		545	destruct (N.eqb x 0); cbn in E; try discriminate;
		546	destruct (consumeN _ a) as [[[o b'] a'']\|]; try discriminate; injection E as <- <-; cbn; auto. }
		547	destruct Hx as (Hx & Hc & Hb & Hux & Hg). apply consumeN_spec in Hc.
		548	unfold uwN. rewrite Hb, Hux, Hg. cbn [ubs ubit ua ux ug].
		549	apply N.eqb_neq in Hx. replace (N.to_nat x) with (S (N.to_nat (N.pred x))) by lia.
		550	apply t_stop. exact Hc.
221	Qed.	551	Qed.
222	End RootCorrect.
		552	Lemma touchN_pass u ov u': touchN u = TPass ov u' -> segRLs tmf h h (uwN u) ([1;1;1]^^(N.to_nat ov) ++ uwN u') /\ ug u' = 0%N.
223	End Sk1Counter.
		553	Proof.
225	Module Sk1Counter7.
		554	destruct u as [bs [] a x g]; unfold touchN; cbn [ubit ubs ua ux ug].
226	Definition W : list Sym := [0;1;0;1;1;1].
		555	- destruct (N.eqb_spec g 0) as [Hg0\|Hg0]; [\|destruct (N.eqb_spec g 1) as [Hg1\|Hg1]].
227	Inductive digit := D0 \| D1 \| D2 \| D3 \| D4 \| D5 \| D6.
		556	+ destruct (consumeN bs (N.succ a)) as [[[o b'] a'']\|] eqn:Ec; [\|discriminate].
228	Definition word p : list Sym :=
		557	intros E; injection E as <- <-. split; [\|reflexivity].
229	match p with
		558	apply consumeN_spec in Ec. rewrite N2Nat.inj_succ in Ec. subst g.
230	\| D0 => [0;1;0;1;0;1] \| D1 => [1;1] \| D2 => [0;1;1;1]
		559	unfold uwN; cbn [ubs ubit ua ux ug].
231	\| D3 => [0;1;0;1;0;1;1;1;0;1;1;1] \| D4 => [1;1;1;1;0;1;1;1]
		560	replace (N.to_nat (x + 2)) with (S (S (N.to_nat x))) by lia. apply t_pass, Ec.
232	\| D5 => [0;1;0;1;0;1;1;1;1;1] \| D6 => [1;1;1;1;1;1]
		561	+ destruct (consumeN (bs ++ [(a, 1%N)]) (N.succ x)) as [[[o b'] a'']\|] eqn:Ec; [\|discriminate].
		562	intros E; injection E as <- <-. split; [\|reflexivity].
		563	apply consumeN_spec in Ec. rewrite N2Nat.inj_succ, cvl_app in Ec. subst g.
		564	cbn [cvl map] in Ec. unfold cvp in Ec; cbn [fst snd] in Ec. change (N.to_nat 1) with 1%nat in Ec.
		565	unfold uwN; cbn [ubs ubit ua ux ug]. apply t_ungl1, Ec.
		566	+ destruct (consumeN (bs ++ [(a, 1%N); (x, g-1)%N]) 0%N) as [[[o b'] a'']\|] eqn:Ec; [\|discriminate].
		567	intros E; injection E as <- <-. split; [\|reflexivity].
		568	apply consumeN_spec in Ec. rewrite cvl_app in Ec. cbn [cvl map] in Ec. unfold cvp in Ec; cbn [fst snd] in Ec.
		569	change (N.to_nat 1) with 1%nat in Ec. change (N.to_nat 0) with 0%nat in Ec.
		570	unfold uwN; cbn [ubs ubit ua ux ug].
		571	replace (N.to_nat g) with (S (S (N.to_nat (g-1) - 1))) by lia.
		572	replace (N.to_nat (g-1)) with (S (N.to_nat (g-1) - 1)) in Ec by lia.
		573	apply t_ungl2, Ec.
		574	- intros E. destruct bs as [\|p bs]; [destruct (N.eqb a 0)\|]; cbn in E; try discriminate;
		575	destruct (N.eqb x 0); cbn in E; try discriminate;
		576	destruct (consumeN _ a) as [[[o b'] a'']\|]; discriminate.
		577	Qed.
		578	Lemma touchN_halt u: touchN u = THalt -> forall l r, halts tmf (l {{B}}> uwN u *> r).
		579	Proof.
		580	destruct u as [bs [] a x g]; unfold touchN; cbn [ubit ubs ua ux ug].
		581	- destruct (N.eqb g 0); [\|destruct (N.eqb g 1)];
		582	match goal with \|- context [consumeN ?b ?c] => destruct (consumeN b c) as [[[? ?] ?]\|] end; discriminate.
		583	- destruct bs as [\|p bs]; [destruct (N.eqb_spec a 0) as [Ha\|Ha]\|].
		584	+ intros _ l r. unfold uwN; cbn [ubs ubit ua ux ug cvl map]. subst a. apply t_halt.
		585	+ intros E; cbn in E; destruct (N.eqb x 0); cbn in E; try discriminate;
		586	destruct (consumeN _ a) as [[[o b'] a'']\|]; discriminate.
		587	+ intros E; cbn in E; destruct (N.eqb x 0); cbn in E; try discriminate;
		588	destruct (consumeN _ a) as [[[o b'] a'']\|]; discriminate.
		589	Qed.
		591	( U0 touch *)
		592	Inductive zres := ZRet (ov:N) (z:zN) \| ZAbs (f:N) \| ZFail.
		593	Definition ztouch z : zres := match z with
		594	\| Z0 [] y f => if N.eqb y 0 then (if N.eqb f 0 then ZFail else ZAbs f) else ZRet 0%N (Z0 [] (N.pred y) (N.succ f))
		595	\| Z0 bs x f => match consumeN bs 0%N with Some (ov,bs',_) => ZRet ov (Z0 bs' x (N.succ f)) \| None => ZFail end
		596	\| ZD bs false a x f => if N.eqb x 0 then ZFail else
		597	match consumeN bs a with Some (ov,bs',a') => ZRet ov (ZD bs' true a' (N.pred x) f) \| None => ZFail end
		598	\| ZD bs true a x f => match consumeN (bs ++ [(a,1%N);(x,f)]) 0%N with Some (ov,bs',_) => ZRet ov (Z0 bs' 0 1) \| None => ZFail end
233	end.	599	end.
234	Definition next p := match p with
		600	Lemma ztouch_ret z ov z': ztouch z = ZRet ov z' -> sideRL tmf hB hD (zside z) ([1;1;1]^^(N.to_nat ov) *> zside z').
235	\| D0=>D1 \| D1=>D2 \| D2=>D3 \| D3=>D4 \| D4=>D5 \| D5=>D6 \| D6=>D0 end.
236	Definition take p : nat := match p with D1 \| D2=>1 \| _=>0 end.
⋯ 15 template-only lines (template 237–254), not in ours
255	forall k, segRLs tm (h^^t) (h^^u)
256	(W^^k ++ word p ++ W^^b) (W^^(k+a) ++ word q ++ W^^c).
257	Proof.	601	Proof.
258	intros H k. rewrite lpow_add, <-app_assoc.
		602	destruct z as [[\|p bs] x f\|bs [] a x f]; cbn [ztouch zside].
259	eapply segRLs_concat; [apply walls\|exact H].
		603	- destruct (N.eqb_spec x 0) as [Hx\|Hx]; [destruct (N.eqb f 0); discriminate\|].
		604	intros E; injection E as <- <-. cbn [zside cvl map cw app]. change (N.to_nat 0) with 0%nat.
		605	cbn [lpow Str_app]. rewrite N2Nat.inj_succ.
		606	replace (N.to_nat x) with (S (N.to_nat (N.pred x))) by lia. apply z_empty.
		607	- destruct (consumeN (p::bs) 0%N) as [[[o b'] a'']\|] eqn:Ec; [\|discriminate].
		608	intros E; injection E as <- <-. apply consumeN_spec in Ec. cbn [zside].
		609	rewrite <-Str_app_assoc, N2Nat.inj_succ. apply (z_lead _ _ _ _ _ (N.to_nat a'')); [discriminate\|exact Ec].
		610	- destruct (consumeN _ 0%N) as [[[o b'] a'']\|] eqn:Ec; [\|discriminate].
		611	intros E; injection E as <- <-. apply consumeN_spec in Ec. rewrite cvl_app in Ec.
		612	cbn [cvl map] in Ec. unfold cvp in Ec; cbn [fst snd] in Ec. change (N.to_nat 1) with 1%nat in Ec.
		613	cbn [zside]. rewrite <-Str_app_assoc. change (N.to_nat 0) with 0%nat. change (N.to_nat 1) with 1%nat.
		614	apply (z_1111 _ _ _ _ _ _ (N.to_nat a'')), Ec.
		615	- destruct (N.eqb_spec x 0) as [Hx\|Hx]; [discriminate\|].
		616	destruct (consumeN bs a) as [[[o b'] a'']\|] eqn:Ec; [\|discriminate].
		617	intros E; injection E as <- <-. apply consumeN_spec in Ec. cbn [zside]. rewrite <-Str_app_assoc.
		618	replace (N.to_nat x) with (S (N.to_nat (N.pred x))) by lia. apply z_stop, Ec.
260	Qed.	619	Qed.
262	Record effect := Eff { phase : digit; used : nat; given : nat; sent : nat }.
		620	Lemma ztouch_abs z f: ztouch z = ZAbs f -> sideRL tmf hB hD (zside z) (([1;1] ++ [1;1;1]^^(N.to_nat f)) *> const 0).
263	Fixpoint total (p:digit) (t:nat) : effect :=
264	match t with
⋯ 6 template-only lines (template 265–271), not in ours
272	segRLs tm (h^^t) (h^^sent a) (word p ++ W^^(used a+n))
273	(W^^given a ++ word (phase a) ++ W^^n).
274	Proof.	621	Proof.
275	gen p n. induction t; intros p n; cbn [total phase used given sent].
		622	destruct z as [[\|p bs] x f'\|bs [] a x f']; cbn [ztouch zside].
276	- constructor.
		623	- destruct (N.eqb_spec x 0) as [Hx\|Hx]; [\|discriminate]. destruct (N.eqb_spec f' 0) as [Hf\|Hf]; [discriminate\|].
277	- cbn [lpow]. rewrite <-Nat.add_assoc.
		624	intros E; injection E as <-. subst x. cbn [cvl map cw app].
278	rewrite (lpow_add _ (carry p)).
		625	replace (N.to_nat f') with (S (N.to_nat f' - 1)) by lia. apply z_absorb.
279	eapply segRLs_trans.
		626	- destruct (consumeN (p::bs) 0%N) as [[[o b'] a'']\|]; discriminate.
280	+ apply one.
		627	- destruct (consumeN _ 0%N) as [[[o b'] a'']\|]; discriminate.
281	+ apply prefix_rule, IHt.
		628	- destruct (N.eqb x 0); [discriminate\|]. destruct (consumeN bs a) as [[[o b'] a'']\|]; discriminate.
282	Qed.	629	Qed.
283	End Counter.
		631	( one call from the root through the units *)
285	Lemma total_add p t u :
		632	Inductive cres := CRet (ov:N) (us:list unitN) (z:zN) \| CHalt \| CFail.
286	total p (t+u) =
		633	Definition setg u g := UN (ubs u) (ubit u) (ua u) (ux u) g.
287	let a := total p t in let b := total (phase a) u in
		634	Fixpoint callN (us:list unitN) (z:zN) : cres := match us with
288	Eff (phase b) (used a+used b) (given a+given b) (sent a+sent b).
		635	\| [] => match ztouch z with ZRet ov z' => CRet ov [] z' \| _ => CFail end
289	Proof.
		636	\| u :: us1 => match touchN u with
290	gen p. induction t; intros p; cbn [Nat.add total phase used given sent].
		637	\| TStop ov u' => CRet ov (u' :: us1) z
291	- destruct (total p u); reflexivity.
		638	\| THalt => CHalt
292	- rewrite IHt. cbn. f_equal; lia.
		639	\| TFail => CFail
293	Qed.
		640	\| TPass ov u' => match us1 with
295	Lemma total_seven p : total p 7 = Eff p 2 4 1.
		641	\| [] => match ztouch z with
296	Proof. destruct p; reflexivity. Qed.
		642	\| ZRet ov2 z' => CRet ov [setg u' ov2] z'
298	Lemma total_period p k r :
		643	\| ZAbs f => CRet ov [] (ZD (ubs u') (ubit u') (ua u') (ux u') (ug u' + f + 1))
299	total p (k*7+r) = let a := total p r in
		644	\| ZFail => CFail end
300	Eff (phase a) (k2+used a) (k4+given a) (k+sent a).
		645	\| _ => match callN us1 z with
301	Proof.
		646	\| CRet ov2 us' z' => CRet ov (setg u' ov2 :: us') z'
302	induction k; [cbn [Nat.mul Nat.add]; destruct (total p r); reflexivity\|].
		647	\| CHalt => CHalt \| CFail => CFail end
303	replace (S k7+r) with (7+(k7+r)) by lia.
304	rewrite total_add,total_seven. cbn [phase used given sent].
⋯ 30 template-only lines (template 305–338), not in ours
339	\| Some (e,ys) => Some (givenN a,(phaseN a,(n-usedN a+e)%N)::ys)
340	\| None => None
341	end	648	end
342	else None
343	end.
⋯ 318 template-only lines (template 345–695), not in ours
696	\| Some ys => remove_fast fuel w (N.pred n) ys
697	\| None => None end
698	end	649	end
699	end.	650	end.
701	Lemma remove_fast_spec fuel w n xs ys : remove_fast fuel w n xs=Some ys ->
		652	Lemma side1 {w w' r r'}: segRLs tmf h h w w' -> sideRL tmf hB hD r r' -> sideRL tmf hB hD (w > r) (w' > r').
702	denote xs=w^^N.to_nat n *> denote ys.
703	Proof.	653	Proof.
704	gen n xs ys. induction fuel; intros n xs ys H; cbn [remove_fast] in H;
		654	intros H1 H2. assert (H3: sideRLs tmf h r r'). { unfold h. econstructor; [exact H2\|constructor]. }
705	destruct (N.eqb_spec n 0); try discriminate; subst; try solve [inverts H; reflexivity].
		655	pose proof (segRLs_sideRLs_concat H1 H3) as H. unfold h in H. inversion H; subst.
706	destruct (skip w n xs) as [[k zs]\|] eqn:E.
		656	match goal with Hs: sideRLs _ [] _ _ \|- _ => inversion Hs; subst end. assumption.
707	- destruct (skip_spec _ _ _ _ _ E) as [Hk E1].
708	rewrite E1,(IHfuel _ _ _ H),<-Str_app_assoc,<-lpow_add.
⋯ 3 template-only lines (template 709–711), not in ours
712	replace (N.to_nat n) with (1+N.to_nat (N.pred n)) by lia.
713	cbn [Nat.add lpow]. rewrite Str_app_assoc. reflexivity.
714	Qed.	657	Qed.
716	Fixpoint size (xs:t) : N := match xs with
		658	Lemma setg_word u g: ug u = 0%N -> uwN u ++ [1;1;1]^^(N.to_nat g) = uwN (setg u g).
717	\| []=>0%N \| (w,n)::xs=>(N.of_nat (length w)*n+size xs)%N end.
		659	Proof. intros E. unfold uwN, setg, uw, tailw. cbn [ubs ubit ua ux ug]. rewrite E. cbn. rewrite <-!app_assoc. reflexivity. Qed.
719	End Runs.
		660	Lemma abs_word u f: ug u = 0%N -> uwN u ++ [1;1] ++ [1;1;1]^^(N.to_nat f) =
721	Module RunMachine.
		661	uw (cvl (ubs u)) (ubit u) (N.to_nat (ua u)) (N.to_nat (ux u)) (edge1w (N.to_nat (ug u + f + 1))).
722	Record config := Cfg { left : Runs.t; right : Runs.t; state : Q; direction : dir }.
		662	Proof.
723	Definition denote c := match direction c with
		663	intros E. unfold uwN, uw, tailw, edge1w. rewrite E. rewrite <-!app_assoc. f_equal. f_equal.
724	\| L => Runs.denote (left c) <{{state c}} Runs.denote (right c)
		664	replace (N.to_nat (0 + f + 1)) with (S (N.to_nat f)) by lia. cbn. reflexivity.
725	\| R => Runs.denote (left c) {{state c}}> Runs.denote (right c)
		665	Qed.
		667	Lemma callN_ret us: forall z ov us' z', callN us z = CRet ov us' z' ->
		668	sideRL tmf hB hD (dwords us > zside z) (([1;1;1]^^(N.to_nat ov) ++ dwords us') > zside z').
		669	Proof.
		670	induction us as [\|u us1 IH]; intros z ov us' z' E; cbn [callN] in E.
		671	- destruct (ztouch z) as [o z1\|f\|] eqn:Ez; try discriminate. injection E as <- <- <-.
		672	cbn [dwords]. rewrite app_nil_r. cbn [Str_app]. apply ztouch_ret, Ez.
		673	- destruct (touchN u) as [o u1\|o u1\| \|] eqn:Et; try discriminate.
		674	+ injection E as <- <- <-. apply touchN_stop in Et. cbn [dwords].
		675	rewrite (app_assoc ([1;1;1]^^(N.to_nat o))), !(Str_app_assoc _ (dwords us1)).
		676	apply segRL_side, Et.
		677	+ apply touchN_pass in Et. destruct Et as [Ht Hg].
		678	destruct us1 as [\|v us2].
		679	* destruct (ztouch z) as [o2 z1\|f\|] eqn:Ez; try discriminate.
		680	-- injection E as <- <- <-. apply ztouch_ret in Ez. pose proof (side1 Ht Ez) as H.
		681	cbn [dwords]. rewrite !app_nil_r. applys_eq H; rewrite <-?Str_app_assoc; f_equal.
		682	rewrite <-!app_assoc, setg_word by exact Hg. reflexivity.
		683	-- injection E as <- <- <-. apply ztouch_abs in Ez. pose proof (side1 Ht Ez) as H.
		684	cbn [dwords zside]. rewrite !app_nil_r. applys_eq H; rewrite <-?Str_app_assoc; f_equal.
		685	rewrite <-!app_assoc, abs_word by exact Hg. reflexivity.
		686	* destruct (callN (v :: us2) z) as [o2 us3 z1\| \|] eqn:Ec; try discriminate.
		687	injection E as <- <- <-. apply IH in Ec. pose proof (side1 Ht Ec) as H.
		688	cbn [dwords] in *. applys_eq H; rewrite <-?Str_app_assoc; f_equal.
		689	rewrite <-!app_assoc. f_equal. rewrite app_assoc, setg_word by exact Hg. reflexivity.
		690	Qed.
		691	Lemma callN_halt us: forall z, callN us z = CHalt -> sideRLs_halt tmf h (dwords us *> zside z).
		692	Proof.
		693	induction us as [\|u us1 IH]; intros z E; cbn [callN] in E.
		694	- destruct (ztouch z); discriminate.
		695	- destruct (touchN u) as [o u1\|o u1\| \|] eqn:Et; try discriminate.
		696	+ apply touchN_pass in Et. destruct Et as [Ht Hg]. destruct us1 as [\|v us2].
		697	* destruct (ztouch z); discriminate.
		698	* destruct (callN (v :: us2) z) as [o2 us3 z1\| \|] eqn:Ec; try discriminate.
		699	apply IH in Ec. cbn [dwords]. rewrite Str_app_assoc.
		700	exact (segRLs_sideRLs_halt_concat _ _ _ _ _ _ Ht Ec).
		701	+ pose proof (touchN_halt _ Et) as Hh.
		702	cbn [dwords]. rewrite Str_app_assoc. unfold h. constructor. intros l. cbn. apply Hh.
		703	Qed.
		705	( one increment *)
		706	Inductive ires := IOk (c:cfg) \| IHalt \| IFail.
		707	Definition inc1 c : ires := match ctl c with
		708	\| TT t g =>
		709	if N.eqb g 0 then match callN (cus c) (cz c) with
		710	\| CRet ov us' z' => IOk (Cfg (TT (N.succ t) ov) us' z') \| CHalt => IHalt \| CFail => IFail end
		711	else if N.eqb g 1 then match callN (cus c) (cz c) with
		712	\| CRet ov us' z' => IOk (Cfg (NTl (N.succ t) ov) us' z') \| CHalt => IHalt \| CFail => IFail end
		713	else IFail
		714	\| NTl s g => if N.eqb s 0 then IFail else IOk (Cfg (TT 0 0) (UN [] true (N.pred s) 0 g :: cus c) (cz c))
726	end.	715	end.
728	Definition raw tm c : option config :=
		716	Lemma inc1_ok c c': inc1 c = IOk c' -> denote c -->* denote c'.
729	let '(b,l,r) := match direction c with
		717	Proof.
730	\| L => let '(b,l) := Runs.pop (left c) in (b,l,right c)
		718	destruct c as [[t g\|s g] us z]; unfold inc1, denote; cbn [ctl cus cz].
731	\| R => let '(b,r) := Runs.pop (right c) in (b,left c,r)
		719	- destruct (N.eqb_spec g 0) as [Hg\|Hg]; [\|destruct (N.eqb_spec g 1) as [Hg1\|Hg1]].
732	end in
		720	+ destruct (callN us z) as [ov us' z'\| \|] eqn:E; try discriminate. intros H; injection H as <-.
733	match tm (state c,b) with
		721	apply callN_ret in E. cbn [ctl cus cz]. subst g. cbn [N.to_nat lpow app].
734	\| None => None
		722	rewrite N2Nat.inj_succ. apply progress_evstep, root_step, E.
735	\| Some (b',L,q) => Some (Cfg l (Runs.push [b'] 1 r) q L)
		723	+ destruct (callN us z) as [ov us' z'\| \|] eqn:E; try discriminate. intros H; injection H as <-.
736	\| Some (b',R,q) => Some (Cfg (Runs.push [b'] 1 l) r q R)
		724	apply callN_ret in E. cbn [ctl cus cz]. subst g. change (N.to_nat 1) with 1%nat. cbn [lpow].
		725	rewrite app_nil_r, Str_app_assoc, N2Nat.inj_succ.
		726	eapply evstep_trans. 1: apply (reset1 _ _ _ E).
		727	unfold NT. rewrite <-!Str_app_assoc. apply evstep_refl'. f_equal. f_equal. unfold tailw.
		728	rewrite <-!app_assoc. reflexivity.
		729	+ discriminate.
		730	- destruct (N.eqb_spec s 0) as [Hs\|Hs]; [discriminate\|]. intros H; injection H as <-. cbn [ctl cus cz dwords].
		731	replace (N.to_nat s) with (S (N.to_nat (N.pred s))) by lia.
		732	eapply evstep_trans. 1: apply reset2.
		733	replace ((lead1 (N.to_nat (N.pred s)) 0 ++ tailw (N.to_nat g)) > (dwords us > zside z))
		734	with (([1;1;1]^^(N.to_nat 0) ++ dwords (UN [] true (N.pred s) 0 g :: us)) *> zside z).
		735	+ apply evstep_refl.
		736	+ cbn [dwords N.to_nat lpow app]. rewrite Str_app_assoc. reflexivity.
		737	Qed.
		738	Lemma inc1_halt c: inc1 c = IHalt -> halts tmf (denote c).
		739	Proof.
		740	destruct c as [[t g\|s g] us z]; unfold inc1, denote; cbn [ctl cus cz].
		741	- destruct (N.eqb_spec g 0) as [Hg\|Hg]; [\|destruct (N.eqb_spec g 1) as [Hg1\|Hg1]].
		742	+ destruct (callN us z) as [ov us' z'\| \|] eqn:E; try discriminate. intros _.
		743	apply callN_halt in E. subst g. cbn [N.to_nat lpow app]. apply root_halt, E.
		744	+ destruct (callN us z) as [ov us' z'\| \|] eqn:E; try discriminate. intros _.
		745	apply callN_halt in E. subst g. change (N.to_nat 1) with 1%nat. cbn [lpow]. rewrite app_nil_r, Str_app_assoc.
		746	apply reset1_halt, E.
		747	+ discriminate.
		748	- destruct (N.eqb s 0); discriminate.
		749	Qed.
		751	(** * Batches: n touches of one unit with no structural event, in closed form *)
		752	Ltac fin := try reflexivity; cbn [lpow app]; try lia; try (f_equal; lia); try (f_equal; f_equal; lia); try (f_equal; f_equal; f_equal; lia).
		753	Lemma stop1s {bs a x far ov bs' a'}: consume bs a = Some (ov, bs', a') ->
		754	segRLs tmf h [] (uw bs false a (S x) far) ([1;1;1]^^ov ++ uw bs' true a' x far).
		755	Proof. intros E. unfold h. econstructor; [apply (t_stop _ _ _ _ _ _ _ E)\|constructor]. Qed.
		756	Lemma pairK q: forall c j r a x, segRLs tmf (h^^(q*2)) (h^^q)
		757	(uw ((q*2+c, j)::r) false a (S x) (tailw 0)) (uw ((c,j)::r) false (q+a) (S (q+x)) (tailw 0)).
		758	Proof.
		759	induction q as [\|q IH]; intros c j r a x.
		760	- apply segRLs_O.
		761	- pose proof (@stop1s ((S (S (q2+c)), j)::r) a x (tailw 0) 0 ((S (q2+c), j)::r) a eq_refl) as H1.
		762	pose proof (t_pass ((S (q2+c), j)::r) a x 0 ((q2+c,j)::r) (S a) eq_refl) as H2.
		763	pose proof (IH c j r (S a) (S x)) as H3.
		764	pose proof (segRLs_trans H1 (segRLs_trans H2 H3)) as H.
		765	applys_eq H; fin.
		766	Qed.
		767	Lemma pair1 q: forall a x, segRLs tmf (h^^(q*2)) (h^^q)
		768	(uw [] false (q+a) (S x) (tailw 0)) (uw [] false a (S (q+x)) (tailw 0)).
		769	Proof.
		770	induction q as [\|q IH]; intros a x.
		771	- apply segRLs_O.
		772	- pose proof (@stop1s [] (S (q+a)) x (tailw 0) 0 [] (q+a) eq_refl) as H1.
		773	pose proof (t_pass [] (q+a) x 0 [] (q+a) eq_refl) as H2.
		774	pose proof (IH a (S x)) as H3.
		775	pose proof (segRLs_trans H1 (segRLs_trans H2 H3)) as H.
		776	applys_eq H; fin.
		777	Qed.
		778	Definition b2n (b:bool) : nat := if b then 1 else 0.
		779	Lemma clK0 q rb c j r a x: segRLs tmf (h^^(q*2 + b2n rb)) (h^^q)
		780	(uw ((q*2 + b2n rb + c, j)::r) false a (S x) (tailw 0)) (uw ((c,j)::r) rb (q+a) (q + S x - b2n rb) (tailw 0)).
		781	Proof.
		782	destruct rb; cbn [b2n].
		783	- pose proof (pairK q (S c) j r a x) as H1.
		784	pose proof (@stop1s ((S c, j)::r) (q+a) (q+x) (tailw 0) 0 ((c,j)::r) (q+a) eq_refl) as H2.
		785	pose proof (segRLs_trans H1 H2) as H. rewrite lpow_add.
		786	rewrite app_nil_r in H. applys_eq H; fin.
		787	- pose proof (pairK q c j r a x) as H. applys_eq H; fin.
		788	Qed.
		789	Lemma clK1 q rb c j r a x: segRLs tmf (h^^(S (q*2 + b2n rb))) (h^^(S q))
		790	(uw ((S (q*2 + b2n rb + c), j)::r) true a x (tailw 0)) (uw ((c,j)::r) rb (q + S a) (q + S (S x) - b2n rb) (tailw 0)).
		791	Proof.
		792	pose proof (t_pass ((S (q2 + b2n rb + c), j)::r) a x 0 ((q2 + b2n rb + c, j)::r) (S a) eq_refl) as H1.
		793	pose proof (clK0 q rb c j r (S a) (S x)) as H2.
		794	exact (segRLs_trans H1 H2).
		795	Qed.
		796	Lemma cl10 q rb a x: segRLs tmf (h^^(q*2 + b2n rb)) (h^^q)
		797	(uw [] false (q + b2n rb + a) (S x) (tailw 0)) (uw [] rb a (q + S x - b2n rb) (tailw 0)).
		798	Proof.
		799	destruct rb; cbn [b2n].
		800	- pose proof (pair1 q (S a) x) as H1.
		801	pose proof (@stop1s [] (S a) (q+x) (tailw 0) 0 [] a eq_refl) as H2.
		802	pose proof (segRLs_trans H1 H2) as H. rewrite lpow_add.
		803	rewrite app_nil_r in H. applys_eq H; fin.
		804	- pose proof (pair1 q a x) as H. applys_eq H; fin.
		805	Qed.
		806	Lemma cl11 q rb a x: segRLs tmf (h^^(S (q*2 + b2n rb))) (h^^(S q))
		807	(uw [] true (q + b2n rb + a) x (tailw 0)) (uw [] rb a (q + S (S x) - b2n rb) (tailw 0)).
		808	Proof.
		809	pose proof (t_pass [] (q + b2n rb + a) x 0 [] (q + b2n rb + a) eq_refl) as H1.
		810	pose proof (cl10 q rb a (S x)) as H2.
		811	exact (segRLs_trans H1 H2).
		812	Qed.
		814	Definition b2N (b:bool) : N := if b then 1%N else 0%N.
		815	Lemma b2N_nat b: N.to_nat (b2N b) = b2n b.
		816	Proof. destruct b; reflexivity. Qed.
		817	Lemma div2_nat n: N.to_nat n = N.to_nat (N.div2 n) * 2 + b2n (N.odd n).
		818	Proof. rewrite <-b2N_nat. pose proof (N.div2_odd n) as E. unfold b2N. destruct (N.odd n); cbn [N.b2n] in E; lia. Qed.
		820	Definition closedU (n:N) (u:unitN) : option (unitN * N) :=
		821	if N.eqb n 0 then Some (u, 0%N) else
		822	match ubs u with
		823	\| (c,j)::r =>
		824	if negb (ubit u) then
		825	if N.eqb n 1 then
		826	if N.eqb (ux u) 0 \|\| N.eqb c 0 then None
		827	else Some (UN ((N.pred c, j)::r) true (ua u) (N.pred (ux u)) (ug u), 0%N)
		828	else
		829	if negb (N.eqb (ug u) 0) \|\| N.eqb (ux u) 0 \|\| N.ltb c n then None
		830	else Some (UN (((c - n)%N, j)::r) (N.odd n) (N.div2 n + ua u) (N.div2 n + ux u - b2N (N.odd n)) 0, N.div2 n)
		831	else
		832	if negb (N.eqb (ug u) 0) \|\| N.ltb c n then None
		833	else Some (UN (((c - n)%N, j)::r) (N.odd (N.pred n)) (N.div2 (N.pred n) + N.succ (ua u))
		834	(N.div2 (N.pred n) + N.succ (N.succ (ux u)) - b2N (N.odd (N.pred n))) 0, N.succ (N.div2 (N.pred n)))
		835	\| [] =>
		836	if negb (ubit u) then
		837	if N.eqb n 1 then
		838	if N.eqb (ux u) 0 \|\| N.eqb (ua u) 0 then None
		839	else Some (UN [] true (N.pred (ua u)) (N.pred (ux u)) (ug u), 0%N)
		840	else
		841	if negb (N.eqb (ug u) 0) \|\| N.eqb (ux u) 0 \|\| N.ltb (ua u) (N.div2 n + b2N (N.odd n)) then None
		842	else Some (UN [] (N.odd n) (ua u - N.div2 n - b2N (N.odd n)) (N.div2 n + ux u - b2N (N.odd n)) 0, N.div2 n)
		843	else
		844	if negb (N.eqb (ug u) 0) \|\| N.ltb (ua u) (N.div2 (N.pred n) + b2N (N.odd (N.pred n))) then None
		845	else Some (UN [] (N.odd (N.pred n)) (ua u - N.div2 (N.pred n) - b2N (N.odd (N.pred n)))
		846	(N.div2 (N.pred n) + N.succ (N.succ (ux u)) - b2N (N.odd (N.pred n))) 0, N.succ (N.div2 (N.pred n)))
737	end.	847	end.
739	Lemma raw_spec tm c : match raw tm c with
		849	Ltac bnorm := repeat match goal with
740	\| None => halted tm (denote c)
		850	\| H: (_ \|\| _) = false \|- _ => apply Bool.orb_false_iff in H; destruct H
741	\| Some c' => denote c -[tm]-> denote c'
		851	\| H: negb _ = false \|- _ => apply Bool.negb_false_iff in H
		852	\| H: N.eqb _ _ = true \|- _ => apply N.eqb_eq in H
		853	\| H: N.eqb _ _ = false \|- _ => apply N.eqb_neq in H
		854	\| H: N.ltb _ _ = false \|- _ => apply N.ltb_ge in H
742	end.	855	end.
		856	Ltac dif := match goal with \|- context [if ?b then _ else _] => destruct b eqn:G end.
		857	Ltac weq := unfold uwN; cbn [ubs ubit ua ux ug cvl map lpow app]; try unfold cvp; cbn [fst snd]; f_equal; try f_equal; try f_equal; try lia.
		859	Lemma closedU_spec n u u' p: closedU n u = Some (u', p) ->
		860	segRLs tmf (h^^(N.to_nat n)) (h^^(N.to_nat p)) (uwN u) (uwN u').
743	Proof.	861	Proof.
744	destruct c as [l r q []]; unfold raw; cbn [left right state direction denote].
		862	unfold closedU. destruct (N.eqb_spec n 0) as [Hn\|Hn].
745	- pose proof (Runs.pop_spec l) as H. destruct (Runs.pop l) as [b l']; cbn in H.
		863	{ intros E; injection E as <- <-. subst n. apply segRLs_O. }
746	rewrite H. destruct (tm (q,b)) as [[[b' []] q']\|] eqn:E;
		864	destruct u as [[\|[c j] r] [] a x g]; cbn [ubs ubit ua ux ug negb].
747	cbn [denote left right state direction]; try rewrite Runs.push_spec;
		865	- (* k=1, bit 1 *)
748	cbn [N.to_nat Pos.to_nat lpow app Str_app];
		866	dif; [discriminate\|]. bnorm. intros E; injection E as <- <-. subst g.
749	first [solve [unfold halted; cbn; exact E] \| solve [econstructor; exact E]].
		867	pose proof (div2_nat (N.pred n)) as Hd. rewrite <-b2N_nat in Hd.
750	- pose proof (Runs.pop_spec r) as H. destruct (Runs.pop r) as [b r']; cbn in H.
		868	pose proof (cl11 (N.to_nat (N.div2 (N.pred n))) (N.odd (N.pred n))
751	rewrite H. destruct (tm (q,b)) as [[[b' []] q']\|] eqn:E;
		869	(N.to_nat (a - N.div2 (N.pred n) - b2N (N.odd (N.pred n)))) (N.to_nat x)) as HH.
752	cbn [denote left right state direction]; try rewrite Runs.push_spec;
		870	rewrite <-b2N_nat in HH. applys_eq HH; try (f_equal; lia); weq.
753	cbn [N.to_nat Pos.to_nat lpow app Str_app];
		871	- (* k=1, bit 0 *)
754	first [solve [unfold halted; cbn; exact E] \| solve [econstructor; exact E]].
		872	destruct (N.eqb_spec n 1) as [Hn1\|Hn1]; cbn [negb].
		873	+ dif; [discriminate\|]. bnorm. intros E; injection E as <- <-. subst n.
		874	assert (Ec: consume [] (N.to_nat a) = Some (0%nat, [], N.to_nat (N.pred a))).
		875	{ unfold consume. replace (N.to_nat a) with (S (N.to_nat (N.pred a))) by lia. reflexivity. }
		876	pose proof (@stop1s [] _ (N.to_nat (N.pred x)) (tailw (N.to_nat g)) _ _ _ Ec) as HH.
		877	change (h^^(N.to_nat 1)) with h. change (h^^(N.to_nat 0)) with (@nil (DH0*DH0)).
		878	applys_eq HH; weq.
		879	+ dif; [discriminate\|]. bnorm. intros E; injection E as <- <-. subst g.
		880	pose proof (div2_nat n) as Hd. rewrite <-b2N_nat in Hd.
		881	pose proof (cl10 (N.to_nat (N.div2 n)) (N.odd n) (N.to_nat (a - N.div2 n - b2N (N.odd n))) (N.to_nat (N.pred x))) as HH.
		882	rewrite <-b2N_nat in HH. applys_eq HH; try (f_equal; lia); weq.
		883	- (* k>=2, bit 1 *)
		884	dif; [discriminate\|]. bnorm. intros E; injection E as <- <-. subst g.
		885	pose proof (div2_nat (N.pred n)) as Hd. rewrite <-b2N_nat in Hd.
		886	pose proof (clK1 (N.to_nat (N.div2 (N.pred n))) (N.odd (N.pred n)) (N.to_nat (c - n)) (N.to_nat j) (cvl r)
		887	(N.to_nat a) (N.to_nat x)) as HH.
		888	rewrite <-b2N_nat in HH. applys_eq HH; try (f_equal; lia); weq.
		889	- (* k>=2, bit 0 *)
		890	destruct (N.eqb_spec n 1) as [Hn1\|Hn1]; cbn [negb].
		891	+ dif; [discriminate\|]. bnorm. intros E; injection E as <- <-. subst n.
		892	assert (Ec: consume ((N.to_nat c, N.to_nat j)::cvl r) (N.to_nat a) = Some (0%nat, (N.to_nat (N.pred c), N.to_nat j)::cvl r, N.to_nat a)).
		893	{ unfold consume. replace (N.to_nat c) with (S (N.to_nat (N.pred c))) by lia. reflexivity. }
		894	pose proof (@stop1s _ _ (N.to_nat (N.pred x)) (tailw (N.to_nat g)) _ _ _ Ec) as HH.
		895	change (h^^(N.to_nat 1)) with h. change (h^^(N.to_nat 0)) with (@nil (DH0*DH0)).
		896	applys_eq HH; weq.
		897	+ dif; [discriminate\|]. bnorm. intros E; injection E as <- <-. subst g.
		898	pose proof (div2_nat n) as Hd. rewrite <-b2N_nat in Hd.
		899	pose proof (clK0 (N.to_nat (N.div2 n)) (N.odd n) (N.to_nat (c - n)) (N.to_nat j) (cvl r) (N.to_nat a) (N.to_nat (N.pred x))) as HH.
		900	rewrite <-b2N_nat in HH. applys_eq HH; try (f_equal; lia); weq.
755	Qed.	901	Qed.
756	End RunMachine.
		903	( U0 in a batch *)
757	End Sk1Tape.
		904	Lemma zLs m: forall c j r x f, sideRLs tmf (h^^m) ((cw ((m+c,j)::r) ++ edgew x f) *> const 0)
759	Module Sk1Check.
		905	((cw ((c,j)::r) ++ edgew x (m+f)) *> const 0).
760	Import Sk1Tape Sk1Counter.
761	Module RT := Runs.
⋯ 8 template-only lines (template 762–770), not in ours
771	\| _,_ => c end.
773	Lemma orient_spec d c : denote (orient d c)=denote c.
774	Proof.	906	Proof.
775	destruct c as [l r q []],d; unfold orient; cbn [left right state direction]; try reflexivity.
		907	induction m as [\|m IH]; intros c j r x f.
776	- pose proof (RT.pop_spec l) as H. destruct (RT.pop l) as [b l']; cbn in H.
		908	- constructor.
777	cbn [denote left right state direction]. rewrite RT.push_spec,H. reflexivity.
		909	- pose proof (z_lead ((S (m+c), j)::r) x f 0 ((m+c,j)::r) 0 ltac:(discriminate) eq_refl) as H1.
778	- pose proof (RT.pop_spec r) as H. destruct (RT.pop r) as [b r']; cbn in H.
		910	cbn [lpow app] in H1. unfold h. cbn [lpow app]. econstructor. 1: exact H1.
779	cbn [denote left right state direction]. rewrite RT.push_spec,H. reflexivity.
		911	replace (S m + f) with (m + S f) by lia. apply IH.
780	Qed.	912	Qed.
781	Lemma orient_direction d c : direction (orient d c)=d.
		913	Lemma zEs m: forall y f, sideRLs tmf (h^^m) (edgew (m+y) f > const 0) (edgew y (m+f) > const 0).
782	Proof. destruct c as [l r q []],d; cbn [orient direction left right state]; try reflexivity;
		914	Proof.
783	first [solve [destruct (RT.pop l); reflexivity] \| solve [destruct (RT.pop r); reflexivity]]. Qed.
		915	induction m as [\|m IH]; intros y f.
784	Lemma orient_state d c : state (orient d c)=state c.
		916	- constructor.
785	Proof. destruct c as [l r q []],d; cbn [orient direction left right state]; try reflexivity;
		917	- unfold h. cbn [lpow app]. econstructor. 1: apply (z_empty (m+y) f).
786	first [solve [destruct (RT.pop l); reflexivity] \| solve [destruct (RT.pop r); reflexivity]]. Qed.
		918	replace (S m + f) with (m + S f) by lia. apply IH.
788	(* 32 is only a matching-work budget. Exhaustion rejects the certificate. *)
		919	Qed.
789	Definition remove_run := RT.remove_fast 32.
		920	Definition closedZ (m:N) (z:zN) : option zN :=
791	Definition scan_stacks s n l r : option (RT.t*RT.t) :=
		921	if N.eqb m 0 then Some z else
792	match scan_dir s with
		922	match z with
793	\| L => match RT.remove (scan_context s) r,
		923	\| Z0 [] y f => if N.ltb y m then None else Some (Z0 [] (y - m) (f + m))
794	remove_run (fast_rev (scan_in s)) n l with
		924	\| Z0 ((c,j)::r) x f => if N.ltb c m then None else Some (Z0 (((c - m)%N, j)::r) x (f + m))
795	\| Some r,Some l => Some (l,RT.push (scan_context s) 1 (RT.push (scan_out s) n r))
		925	\| ZD _ _ _ _ _ => None
796	\| _,_ => None end
797	\| R => match RT.remove (fast_rev (scan_context s)) l,
⋯ 2 template-only lines (template 798–799), not in ours
800	(RT.push (fast_rev (scan_out s)) n l),r)
801	\| _,_ => None end
802	end.	926	end.
804	Lemma scan_stacks_spec tm s n l r l' r' : scan_valid tm s ->
		927	Lemma closedZ_spec m z z': closedZ m z = Some z' -> sideRLs tmf (h^^(N.to_nat m)) (zside z) (zside z').
805	scan_stacks s n l r=Some (l',r') ->
806	denote (Cfg l r (scan_q s) (scan_dir s)) -[tm]->*
807	denote (Cfg l' r' (scan_q s) (scan_dir s)).
808	Proof.	928	Proof.
809	destruct s as [q d w v x]. unfold scan_valid,scan_stacks,remove_run.
		929	unfold closedZ. destruct (N.eqb_spec m 0) as [Hm\|Hm].
810	destruct d; cbn [scan_q scan_dir scan_in scan_out scan_context]; intros H E.
		930	{ intros E; injection E as <-. subst m. constructor. }
811	- destruct (RT.remove x r) as [r0\|] eqn:Er; try discriminate.
		931	destruct z as [[\|[c j] r] x f\|bs b a x f]; try discriminate.
812	destruct (RT.remove_fast 32 (fast_rev w) n l) as [l0\|] eqn:El; inverts E.
		932	- destruct (N.ltb_spec x m) as [Hx\|Hx]; [discriminate\|]. intros E; injection E as <-.
813	cbn [denote left right state direction].
		933	cbn [zside cvl map cw app]. pose proof (zEs (N.to_nat m) (N.to_nat (x - m)) (N.to_nat f)) as H.
814	rewrite !RT.push_spec,(RT.remove_spec _ _ _ Er),(RT.remove_fast_spec _ _ _ _ _ El).
		934	replace (N.to_nat x) with (N.to_nat m + N.to_nat (x - m)) by lia.
815	rewrite fast_rev_spec. change (N.to_nat 1) with 1%nat.
		935	replace (N.to_nat (f + m)) with (N.to_nat m + N.to_nat f) by lia. exact H.
816	cbn [lpow]. rewrite app_nil_r. apply H.
		936	- destruct (N.ltb_spec c m) as [Hc\|Hc]; [discriminate\|]. intros E; injection E as <-.
817	- destruct (RT.remove (fast_rev x) l) as [l0\|] eqn:El; try discriminate.
		937	cbn [zside cvl map]. unfold cvp; cbn [fst snd].
818	destruct (RT.remove_fast 32 w n r) as [r0\|] eqn:Er; inverts E.
		938	pose proof (zLs (N.to_nat m) (N.to_nat (c - m)) (N.to_nat j) (cvl r) (N.to_nat x) (N.to_nat f)) as H.
819	cbn [denote left right state direction].
		939	replace (N.to_nat c) with (N.to_nat m + N.to_nat (c - m)) by lia.
820	rewrite !RT.push_spec,(RT.remove_spec _ _ _ El),(RT.remove_fast_spec _ _ _ _ _ Er).
		940	replace (N.to_nat (f + m)) with (N.to_nat m + N.to_nat f) by lia. exact H.
821	rewrite !fast_rev_spec. change (N.to_nat 1) with 1%nat.
822	cbn [lpow]. rewrite app_nil_r. apply H.
823	Qed.	941	Qed.
825	Definition use_scan s n c : option config :=
		943	Fixpoint batchL (n:N) (us:list unitN) (z:zN) : option (list unitN * zN) := match us with
826	if eqb (state c) (scan_q s) then
		944	\| [] => match closedZ n z with Some z' => Some ([], z') \| None => None end
827	let c := orient (scan_dir s) c in
		945	\| u :: us => match closedU n u with
828	match scan_stacks s n (left c) (right c) with
		946	\| Some (u', p) => match batchL p us z with Some (us', z') => Some (u' :: us', z') \| None => None end
829	\| Some (l,r) => Some (Cfg l r (scan_q s) (scan_dir s))
		947	\| None => None end end.
830	\| None => None end
		948	Lemma batchL_spec us: forall n z us' z', batchL n us z = Some (us', z') ->
831	else None.
		949	sideRLs tmf (h^^(N.to_nat n)) (dwords us > zside z) (dwords us' > zside z').
833	Lemma use_scan_spec tm s n c c' : scan_valid tm s -> use_scan s n c=Some c' ->
834	denote c -[tm]->* denote c'.
835	Proof.	950	Proof.
836	intros H. unfold use_scan. destruct (eqb_spec (state c) (scan_q s)); try discriminate.
		951	induction us as [\|u us IH]; intros n z us' z' E; cbn [batchL] in E.
837	pose proof (orient_direction (scan_dir s) c) as Hd.
		952	- destruct (closedZ n z) as [z1\|] eqn:Ez; [\|discriminate]. injection E as <- <-. apply closedZ_spec, Ez.
838	pose proof (orient_state (scan_dir s) c) as Hq.
		953	- destruct (closedU n u) as [[u1 p]\|] eqn:Eu; [\|discriminate].
839	rewrite <-(orient_spec (scan_dir s) c).
		954	destruct (batchL p us z) as [[us1 z1]\|] eqn:Eb; [\|discriminate]. injection E as <- <-.
840	remember (orient (scan_dir s) c) as z.
		955	cbn [dwords]. rewrite !Str_app_assoc.
841	destruct z as [l r q d]; cbn [left right state direction] in *; subst.
		956	exact (segRLs_sideRLs_concat (closedU_spec _ _ _ _ Eu) (IH _ _ _ _ Eb)).
842	destruct (scan_stacks s n l r) as [[l' r']\|] eqn:E; intros Hc; inverts Hc.
843	rewrite e. eapply scan_stacks_spec; eauto.
844	Qed.	957	Qed.
846	Fixpoint zeros (xs:RT.t) := match xs with
		959	( batch-size proposal (untrusted; a port of the accelerated simulator) *)
847	\| [] => true
		960	Definition evt_unit (u:unitN) : N :=
848	\| (w,_)::xs => if forallb (fun b=>eqb b 0) w then zeros xs else false end.
		961	let own := match ubs u with (c,_)::_ => N.succ c \| [] => (2 * ua u + b2N (ubit u))%N end in
849	Lemma zero_word w : forallb (fun b=>eqb b 0) w=true -> w *> 0inf=0inf.
		962	let own := if negb (ubit u) && N.eqb (ux u) 0 then 1%N else own in
		963	if N.eqb (ug u) 0 then own else N.min own (if ubit u then 1%N else 2%N).
		964	Definition evt_z z : N := match z with Z0 [] y _ => N.succ y \| Z0 ((c,_)::_) _ _ => N.succ c \| ZD _ _ _ _ _ => 1%N end.
		965	Definition first_inc (C q n : N) : N := (n * 2^q - C mod 2^q)%N.
		966	Fixpoint cval (us:list unitN) (i:N) : N := match us with
		967	\| [] => 0%N \| u :: us => ((if ubit u then 2^i else 0) + cval us (N.succ i))%N end.
		968	Fixpoint pmin (us:list unitN) (i C:N) (z:zN) : N := match us with
		969	\| [] => first_inc C i (evt_z z)
		970	\| u :: us => N.min (first_inc C i (evt_unit u)) (pmin us (N.succ i) C z) end.
		971	Definition propose (us:list unitN) (z:zN) : N := N.pred (pmin us 0 (cval us 0) z).
		973	( the checker *)
		974	Definition batch_step c : option cfg := match ctl c with
		975	\| TT t g => if N.eqb g 0 then
		976	let d := propose (cus c) (cz c) in
		977	if N.eqb d 0 then None else
		978	match batchL d (cus c) (cz c) with Some (us', z') => Some (Cfg (TT (t + d) 0) us' z') \| None => None end
		979	else None
		980	\| NTl _ _ => None end.
		981	Lemma batch_step_spec c c': batch_step c = Some c' -> denote c -->* denote c'.
850	Proof.	982	Proof.
851	induction w as [\|b w IH]; cbn; intros H; [reflexivity\|].
		983	destruct c as [[t g\|s g] us z]; unfold batch_step; cbn [ctl cus cz]; [\|discriminate].
852	destruct b; cbn in H; try discriminate. rewrite IH by exact H. symmetry; apply const_unfold.
		984	destruct (N.eqb_spec g 0) as [Hg\|Hg]; [\|discriminate]. subst g.
		985	destruct (N.eqb (propose us z) 0); [discriminate\|].
		986	destruct (batchL (propose us z) us z) as [[us' z']\|] eqn:E; [\|discriminate]. intros H; injection H as <-.
		987	apply batchL_spec in E. unfold denote; cbn [ctl cus cz N.to_nat lpow app].
		988	replace (N.to_nat (t + propose us z)) with (N.to_nat (propose us z) + N.to_nat t) by lia.
		989	apply root_steps, E.
853	Qed.	990	Qed.
854	Lemma zeros_spec xs : zeros xs=true -> RT.denote xs=0inf.
		991	Definition next c : cfg + unit := match batch_step c with
		992	\| Some c' => inl c'
		993	\| None => match inc1 c with IOk c' => inl c' \| IHalt => inr tt \| IFail => inl c end end.
		994	Lemma next_spec c: match next c with inl c' => denote c -->* denote c' \| inr _ => halts tmf (denote c) end.
855	Proof.	995	Proof.
856	induction xs as [\|[w n] xs IH]; cbn [zeros RT.denote]; intros H; [reflexivity\|].
		996	unfold next. destruct (batch_step c) as [c'\|] eqn:Eb; [apply batch_step_spec, Eb\|].
857	destruct (forallb (fun b=>eqb b 0) w) eqn:E; try discriminate.
		997	destruct (inc1 c) as [c'\| \|] eqn:Ei.
858	rewrite IH by exact H. apply lpow_all0,zero_word,E.
		998	- apply inc1_ok, Ei.
		999	- apply inc1_halt, Ei.
		1000	- apply evstep_refl.
859	Qed.	1001	Qed.
861	Section Cells.
		1002	Definition c342 := Cfg (NTl 1 1) [] (Z0 [(0%N,3%N)] 0 1).
862	Variable digit : Type.
		1003	Definition check fuel := match N_iter_until next (inl c342) fuel with inl _ => false \| inr _ => true end.
863	Variable word : digit -> list Sym.
		1004	Theorem check_spec fuel: check fuel = true -> halts tmf (denote c342).
864	Variable W : list Sym.
865	Fixpoint cells_word (xs:list(digit*N)) : list Sym := match xs with
⋯ 12 template-only lines (template 866–878), not in ours
880	Lemma remove_cells_spec xs r r' : remove_cells xs r=Some r' ->
881	RT.denote r=cells_word xs *> RT.denote r'.
882	Proof.	1005	Proof.
883	gen r. induction xs as [\|[p n] xs IH]; intros r H; cbn [remove_cells] in H.
		1006	pose proof (@N_iter_until_spec cfg unit next (inl c342) fuel
884	- inverts H; reflexivity.
		1007	(fun c => denote c342 -->* denote c) (fun _ => halts tmf (denote c342))) as H.
885	- destruct (RT.remove (word p) r) as [s\|] eqn:E; try discriminate.
		1008	assert (Hstep: forall c, denote c342 -->* denote c ->
886	destruct (remove_run W n s) as [s'\|] eqn:E'; try discriminate.
		1009	match next c with inl c' => denote c342 -->* denote c' \| inr _ => halts tmf (denote c342) end).
887	rewrite (RT.remove_spec _ _ _ E),(RT.remove_fast_spec _ _ _ _ _ E'),(IH _ H).
		1010	{ intros c E. pose proof (next_spec c) as I. destruct (next c).
888	cbn [cells_word]; rewrite !Str_app_assoc; reflexivity.
		1011	- eapply evstep_trans; eauto.
		1012	- eapply halts_evstep; [exact I\|exact E]. }
		1013	specialize (H Hstep (evstep_refl _ _)). unfold check.
		1014	destruct (N_iter_until next (inl c342) fuel); [discriminate\|]. intros _. exact H.
889	Qed.	1015	Qed.
890	Lemma push_cells_spec xs r : RT.denote (push_cells xs r)=cells_word xs *> RT.denote r.
		1017	(** * The run, in chunks of 5000 iterations (each intermediate configuration is computed once by the VM
		1018	and stored; each chunk is then checked separately, which keeps kernel re-checking bounded) *)
		1019	Ltac vm_check_eq := match goal with \|- _ = ?a => vm_cast_no_check (eq_refl a) end.
		1020	Definition run (T:N) (c:cfg) : cfg + unit := N_iter_until next (inl c) T.
		1021	Definition unl (x:cfg + unit) : cfg := match x with inl c => c \| inr _ => c342 end.
		1022	Lemma run_ok T c c': run T c = inl c' -> denote c -->* denote c'.
891	Proof.	1023	Proof.
892	induction xs as [\|[p n] xs IH]; cbn [push_cells cells_word]; [reflexivity\|].
		1024	intros E. pose proof (@N_iter_until_spec cfg unit next (inl c) T
893	rewrite !RT.push_spec,IH. change (N.to_nat 1) with 1%nat.
		1025	(fun x => denote c -->* denote x) (fun _ => halts tmf (denote c))) as H.
894	cbn [lpow]. rewrite app_nil_r,!Str_app_assoc. reflexivity.
		1026	assert (Hstep: forall x, denote c -->* denote x ->
		1027	match next x with inl x' => denote c -->* denote x' \| inr _ => halts tmf (denote c) end).
		1028	{ intros x Ex. pose proof (next_spec x) as I. destruct (next x).
		1029	- eapply evstep_trans; eauto.
		1030	- eapply halts_evstep; [exact I\|exact Ex]. }
		1031	specialize (H Hstep (evstep_refl _ _)). unfold run in E. rewrite E in H. exact H.
895	Qed.	1032	Qed.
897	Definition bulk_stacks q (u:list Sym) t k xs c :=
		1033	Lemma run_halt T c: run T c = inr tt -> halts tmf (denote c).
898	if eqb (state c) q then
899	let c := orient R c in
⋯ 14 template-only lines (template 900–914), not in ours
916	Lemma bulk_stacks_spec t k xs c c' : bulk_stacks q u t k xs c=Some c' ->
917	denote c -[tm]->* denote c'.
918	Proof.	1034	Proof.
919	unfold bulk_stacks. destruct (eqb_spec (state c) q); try discriminate.
		1035	intros E. pose proof (@N_iter_until_spec cfg unit next (inl c) T
920	pose proof (orient_direction R c) as Hd. pose proof (orient_state R c) as Hq.
		1036	(fun x => denote c -->* denote x) (fun _ => halts tmf (denote c))) as H.
921	rewrite <-(orient_spec R c). remember (orient R c) as z.
		1037	assert (Hstep: forall x, denote c -->* denote x ->
922	destruct z as [l r q' d]; cbn [left right state direction] in *; subst.
		1038	match next x with inl x' => denote c -->* denote x' \| inr _ => halts tmf (denote c) end).
923	destruct (RT.remove (fast_rev u) l) as [l0\|] eqn:El; try discriminate.
		1039	{ intros x Ex. pose proof (next_spec x) as I. destruct (next x).
924	destruct (remove_run W k r) as [r0\|] eqn:Er; try discriminate.
		1040	- eapply evstep_trans; eauto.
925	destruct (batch t xs) as [[e ys]\|] eqn:Eb; try discriminate.
		1041	- eapply halts_evstep; [exact I\|exact Ex]. }
926	destruct (zeros l0) eqn:Ez; try discriminate.
		1042	specialize (H Hstep (evstep_refl _ _)). unfold run in E. rewrite E in H. exact H.
927	destruct (remove_cells xs r0) as [r1\|] eqn:Ec; intros H; inverts H.
928	cbn [denote left right state direction].
929	rewrite !RT.push_spec,push_cells_spec,(RT.remove_spec _ _ _ El),
930	(zeros_spec _ Ez),(RT.remove_fast_spec _ _ _ _ _ Er),(remove_cells_spec _ _ _ Ec).
931	rewrite fast_rev_spec. eapply rule; exact Eb.
932	Qed.	1043	Qed.
933	End BulkCorrect.
		1045	Definition k1 := Eval vm_compute in unl (run 5000 c342).
934	End Cells.
		1046	Lemma s1: run 5000 c342 = inl k1. Proof. vm_check_eq. Qed.
937	Definition initial := Cfg [] [] A R.
		1047	Definition k2 := Eval vm_compute in unl (run 5000 k1).
938	Lemma initial_spec : denote initial=c0.
		1048	Lemma s2: run 5000 k1 = inl k2. Proof. vm_check_eq. Qed.
939	Proof. reflexivity. Qed.
		1049	Definition k3 := Eval vm_compute in unl (run 5000 k2).
940	End Sk1Check.
		1050	Lemma s3: run 5000 k2 = inl k3. Proof. vm_check_eq. Qed.
942	Module Sk1Auto.
		1051	Definition k4 := Eval vm_compute in unl (run 5000 k3).
943	Import Sk1Check.
		1052	Lemma s4: run 5000 k3 = inl k4. Proof. vm_check_eq. Qed.
944	Import RM.
		1053	Definition k5 := Eval vm_compute in unl (run 5000 k4).
945	Local Opaque RT.remove_fast RT.remove RT.push.
		1054	Lemma s5: run 5000 k4 = inl k5. Proof. vm_check_eq. Qed.
947	(* Proposals need not be complete: the bulk/scan checkers certify each use. *)
		1055	Definition k6 := Eval vm_compute in unl (run 5000 k5).
948	Definition front_size (r:RT.t) := RT.size (firstn 2 r).
		1056	Lemma s6: run 5000 k5 = inl k6. Proof. vm_check_eq. Qed.
949	Definition periodic (w:list Sym) (r:RT.t) :=
		1057	Definition k7 := Eval vm_compute in unl (run 5000 k6).
950	let '(x,v):=match r with
		1058	Lemma s7: run 5000 k6 = inl k7. Proof. vm_check_eq. Qed.
951	\| (x,Npos xH)::(v,_)::_=>(x,v)
		1059	Definition k8 := Eval vm_compute in unl (run 5000 k7).
952	\| (v,_)::_=>([],v) \| []=>([],[]) end in
		1060	Lemma s8: run 5000 k7 = inl k8. Proof. vm_check_eq. Qed.
953	eqb (x++v^^length w) (w^^length v++x).
		1061	Definition k9 := Eval vm_compute in unl (run 5000 k8).
954	Fixpoint count_run fuel w r : N*RT.t := match fuel with
		1062	Lemma s9: run 5000 k8 = inl k9. Proof. vm_check_eq. Qed.
955	\| O=>(0%N,r)
		1063	Definition k10 := Eval vm_compute in unl (run 5000 k9).
956	\| S fuel=>match (if periodic w r then RT.skip w (front_size r) r else None) with
		1064	Lemma s10: run 5000 k9 = inl k10. Proof. vm_check_eq. Qed.
957	\| Some(k,s)=>let '(n,s):=count_run fuel w s in ((k+n)%N,s)
		1065	Definition k11 := Eval vm_compute in unl (run 5000 k10).
958	\| None=>match RT.remove w r with
		1066	Lemma s11: run 5000 k10 = inl k11. Proof. vm_check_eq. Qed.
959	\| Some s=>let '(n,s):=count_run fuel w s in ((1+n)%N,s)
		1067	Definition k12 := Eval vm_compute in unl (run 5000 k11).
960	\| None=>(0%N,r) end end end.
		1068	Lemma s12: run 5000 k11 = inl k12. Proof. vm_check_eq. Qed.
962	Section Proposal.
		1069	Definition k13 := Eval vm_compute in unl (run 5000 k12).
963	Variable digit : Type.
		1070	Lemma s13: run 5000 k12 = inl k13. Proof. vm_check_eq. Qed.
964	Variable W : list Sym.
		1071	Definition k14 := Eval vm_compute in unl (run 5000 k13).
965	Variable word : digit -> list Sym.
		1072	Lemma s14: run 5000 k13 = inl k14. Proof. vm_check_eq. Qed.
966	Variable next : digit -> digit.
		1073	Definition k15 := Eval vm_compute in unl (run 5000 k14).
967	Variable take : digit -> nat.
		1074	Lemma s15: run 5000 k14 = inl k15. Proof. vm_check_eq. Qed.
968	Variable index : digit -> N.
		1075	Definition k16 := Eval vm_compute in unl (run 5000 k15).
969	Variable period : nat.
		1076	Lemma s16: run 5000 k15 = inl k16. Proof. vm_check_eq. Qed.
970	Variable order : list digit.
		1077	Definition k17 := Eval vm_compute in unl (run 5000 k16).
971	Fixpoint first_bad fuel p n : N := match fuel with
		1078	Lemma s17: run 5000 k16 = inl k17. Proof. vm_check_eq. Qed.
972	\| O=>1%N
		1079	Definition k18 := Eval vm_compute in unl (run 5000 k17).
973	\| S fuel=>if (N.of_nat(take p)<=?n)%N
		1080	Lemma s18: run 5000 k17 = inl k18. Proof. vm_check_eq. Qed.
974	then (1+first_bad fuel (next p) (n-N.of_nat(take p)))%N else 1%N end.
		1081	Definition k19 := Eval vm_compute in unl (run 5000 k18).
975	Definition unsafe p n := (N.of_nat period*(n/2)+first_bad period p (n mod 2))%N.
		1082	Lemma s19: run 5000 k18 = inl k19. Proof. vm_check_eq. Qed.
976	Definition better (a b:option(digitNRT.t)) := match a,b with
		1083	Definition k20 := Eval vm_compute in unl (run 5000 k19).
977	\| Some(p,n,r),Some(q,m,s)=>if (n<?m)%N then b else a
		1084	Lemma s20: run 5000 k19 = inl k20. Proof. vm_check_eq. Qed.
978	\| None,_=>b \| _,None=>a end.
		1085	Definition k21 := Eval vm_compute in unl (run 5000 k20).
979	Fixpoint choose ps r : option(digitNRT.t) := match ps with
		1086	Lemma s21: run 5000 k20 = inl k21. Proof. vm_check_eq. Qed.
980	\| []=>None
		1087	Lemma s22: run 5000 k21 = inr tt. Proof. vm_check_eq. Qed.
981	\| p::ps=>let cand:=match RT.remove (word p) r with
		1088	Lemma init: c0 -[tmf]->* denote c342.
982	\| None=>None
		1089	Proof. unfold denote, c342, NT, zside; cbn. solve_init. Qed.
983	\| Some r=>let '(n,r):=count_run 32 W r in Some(p,n,r) end in
		1090	Lemma halt_tmf: halts tmf c0.
984	better cand (choose ps r) end.
985	Fixpoint propose_cells fuel r cap : Nlist(digitN) := match fuel with
⋯ 59 template-only lines (template 986–1047), not in ours
1049	Lemma auto_scan_spec s c c': Sk1Counter.scan_valid tm s -> auto_scan s c=Some c' ->
1050	denote c -[tm]->* denote c'.
1051	Proof.	1091	Proof.
1052	intros H. unfold auto_scan. destruct (N.ltb (scan_count s c) min_scan); try discriminate.
		1092	eapply halts_evstep. 2: apply init.
1053	apply use_scan_spec,H.
		1093	eapply halts_evstep. 2: apply (run_ok _ _ _ s1).
		1094	eapply halts_evstep. 2: apply (run_ok _ _ _ s2).
		1095	eapply halts_evstep. 2: apply (run_ok _ _ _ s3).
		1096	eapply halts_evstep. 2: apply (run_ok _ _ _ s4).
		1097	eapply halts_evstep. 2: apply (run_ok _ _ _ s5).
		1098	eapply halts_evstep. 2: apply (run_ok _ _ _ s6).
		1099	eapply halts_evstep. 2: apply (run_ok _ _ _ s7).
		1100	eapply halts_evstep. 2: apply (run_ok _ _ _ s8).
		1101	eapply halts_evstep. 2: apply (run_ok _ _ _ s9).
		1102	eapply halts_evstep. 2: apply (run_ok _ _ _ s10).
		1103	eapply halts_evstep. 2: apply (run_ok _ _ _ s11).
		1104	eapply halts_evstep. 2: apply (run_ok _ _ _ s12).
		1105	eapply halts_evstep. 2: apply (run_ok _ _ _ s13).
		1106	eapply halts_evstep. 2: apply (run_ok _ _ _ s14).
		1107	eapply halts_evstep. 2: apply (run_ok _ _ _ s15).
		1108	eapply halts_evstep. 2: apply (run_ok _ _ _ s16).
		1109	eapply halts_evstep. 2: apply (run_ok _ _ _ s17).
		1110	eapply halts_evstep. 2: apply (run_ok _ _ _ s18).
		1111	eapply halts_evstep. 2: apply (run_ok _ _ _ s19).
		1112	eapply halts_evstep. 2: apply (run_ok _ _ _ s20).
		1113	eapply halts_evstep. 2: apply (run_ok _ _ _ s21).
		1114	exact (run_halt _ _ s22).
1054	Qed.	1115	Qed.
1055	Lemma try_scans_spec ss c c':Forall(Sk1Counter.scan_valid tm) ss -> try_scans ss c=Some c' ->
		1117	Lemma halt: halts tm c0.
1056	denote c -[tm]->* denote c'.
		1118	Proof. apply flip_halts_iff. exact halt_tmf. Qed.
1057	Proof.
		1120	(*
1058	intros H. induction H; cbn [try_scans]; [discriminate\|].
		1121	```
1059	destruct (auto_scan x c) as [c''\|] eqn:E; [intros H'; inverts H'\|apply IHForall].
		1122	mirror tmf = flip tm; words root-first (nearest the head first)
1060	eapply auto_scan_spec; eauto.
		1123	unit uw bs b a x far = cw bs ++ leadw b a x ++ far, blk c j = [0] ++ [1;0]^^c ++ [1] ++ [1;1;1]^^j
1061	Qed.
		1124	lead leadw true a x = blk a 1 ++ [0] ++ [1;0]^^x, leadw false a x = [0;1]^^a ++ [0;0] ++ [1;0]^^x
1062	Lemma advance_spec c:match advance tm scans c with
		1125	far tailw g = [1;1] ++ [1;1;1]^^g (boundary); edgew x f = [0] ++ [1;0]^^x ++ [1;1;1]^^f; edge1w f = [1] ++ [1;1;1]^^f
1063	\| inl c'=>denote c -[tm]->* denote c' \| inr _=>halted tm (denote c) end.
		1126	consume ((S c,j)::r) a = (0, (c,j)::r, a); ((0,j)::r) a = (j, r, a) (j walls glue root-ward); [] (S a) = (0, [], a)
1064	Proof.
		1128	touch (call in B, return in D; [1;1;1]^^ov = walls glued onto the root-side boundary)
1065	unfold advance. destruct (auto_bulk c) as [c'\|] eqn:E; [eapply bulk_ok; eauto\|].
		1129	stop uw bs false a (S x) far -> [1;1;1]^^ov ++ uw bs' true a' x far (bs',a') from consume bs a
1066	destruct (try_scans scans c) as [c'\|] eqn:Es; [eapply try_scans_spec; eauto\|].
		1130	pass uw bs true a x (tailw 0) -> [1;1;1]^^ov ++ uw bs' false a' (x+2) (tailw 0), one call forwarded; consume bs (a+1)
1067	pose proof(RM.raw_spec tm c) as H. destruct(RM.raw tm c); [apply evstep_one,H\|exact H].
		1131	unglue1 uw bs true a x (tailw 1) -> [1;1;1]^^ov ++ uw bs' false a' 1 (tailw 0), forwarded; consume (bs++[(a,1)]) (x+1)
1068	Qed.
		1132	unglue2 uw bs true a x (tailw (g+2)) -> [1;1;1]^^ov ++ uw bs' false 0 1 (tailw 0), forwarded; consume (bs++[(a,1);(x,g+1)]) 0
1069	Theorem check_spec fuel:check tm scans fuel=true -> halts tm c0.
		1133	halt uw [] false 0 x far -> halts
1070	Proof.
		1134	U0 cw bs ++ edgew x f -> [1;1;1]^^ov ++ cw bs' ++ edgew x (f+1) (bs nonempty)
1071	rewrite <-initial_spec.
		1135	edgew (y+1) f -> edgew y (f+1); edgew 0 (f+1) -> [1;1] ++ [1;1;1]^^(f+1) (absorb: U1 becomes U0, edge class 1)
1072	pose proof (@N_iter_until_spec config unit (advance tm scans) (inl initial) fuel
		1136	uw bs true a x (edge1w f) -> [1;1;1]^^ov ++ cw bs' ++ edgew 0 1 consume (bs++[(a,1);(x,f)]) 0
1073	(fun c=>denote initial -[tm]->* denote c)
		1137	root root t X = 0inf <{{A}} ([0;1]^^t ++ [0;1;1]) *> X: root t X -->+ root (t+1) X' for a call X -> X'
1074	(fun _=>halts tm (denote initial))) as H.
		1138	reset1 root t ([1;1;1] > X) --> NT (t+1) 0 X' (NT s g X = 0inf <{{A}} ([1;0]^^s ++ [1;0;0;1;0] ++ tailw g) *> X)
1075	assert (Hstep:forall c,denote initial -[tm]->* denote c ->
		1139	reset2 NT (s+1) g X -->* root 0 ((leadw true s 0 ++ tailw g) *> X)
1076	match advance tm scans c with
		1140	start c0 -->* NT 1 1 ((blk 0 3 ++ edgew 0 1) *> 0inf) (342 steps)
1077	\| inl c'=>denote initial -[tm]->* denote c' \| inr _=>halts tm (denote initial) end).
		1141	```
1078	{ intros c E. pose proof(advance_spec c) as I. destruct(advance tm scans c).
		1142	*)
1079	- eapply evstep_trans; eauto.
1080	- eapply halts_evstep; [apply halted_halts,I\|exact E]. }
⋯ 927 template-only lines (template 1081–2041), not in ours
2042	Qed.
2043	End TM105.

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

234 items in 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v (1142 lines): 136 Lemma, 81 Definition, 8 Fixpoint, 6 Inductive, 2 Record, 1 Theorem. 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.


Definition tm := Eval compute in (TM_from_str "1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB").
Definition tmf := Eval compute in (flip tm).
Lemma segRR_app {t h1 h2 h3 w1 w2 m1 m2}:
segRR t h1 h2 w1 m1 -> segRR t h2 h3 w2 m2 -> segRR t h1 h3 (w1 ++ w2) (m2 ++ m1).
Lemma segLL_app {t h1 h2 h3 w1 w2 o1 o2}:
segLL t h1 h2 w1 o1 -> segLL t h2 h3 w2 o2 -> segLL t h1 h3 (w1 ++ w2) (o2 ++ o1).
Lemma segRR_RL_LL {t h1 h2 h3 h4 w1 w2 m w1' w2'}:
segRR t h1 h2 w1 m -> segRL t h2 h3 w2 w2' -> segLL t h3 h4 m w1' ->
segRL t h1 h4 (w1 ++ w2) (w1' ++ w2').
Definition stack j : list Sym := [1] ++ [1;1;1]^^j.
Definition blk m j : list Sym := [0] ++ [1;0]^^m ++ stack j.
Definition bmid m j : list Sym := [0;1] ++ [0;1;1]^^j ++ [0;1]^^m.
Definition lbw m j : list Sym := [0;1;1]^^j ++ [0;1]^^(S m).
Definition xbmid x : list Sym := [0;0;1] ++ [0;1]^^x.
Lemma blkRR_F m j: segRR tmf (F,[]) (F,[]) (blk m j) (bmid m j).
Lemma blkRR_B m j: segRR tmf (B,[]) (F,[]) (blk m j) (bmid m j).
Lemma blkLL m j: segLL tmf (D,[]) (D,[]) (lbw m j) (blk m j).
Lemma sweepLL: segLL tmf (D,[]) (D,[]) [0;1] [0;1].
Lemma leadLL a: segLL tmf (A,[]) (D,[]) (bmid a 1) ([0;1]^^a ++ [0;0] ++ [1;0;1]).
Lemma xbRR x: segRR tmf (F,[]) (B,[]) ([0] ++ [1;0]^^x ++ [1;1]) (xbmid x).
Lemma xbLL x: segLL tmf (D,[]) (A,[]) (xbmid x) ([0] ++ [1;0]^^x ++ [1;1]).
Lemma leadstopS a x: segRL tmf (F,[]) (D,[]) ([0;1]^^(S a) ++ [0;0] ++ [1;0]^^(S x))
([0] ++ [1;0]^^a ++ [1;1;1;1] ++ [0] ++ [1;0]^^x).
Lemma leadstop0 x: segRL tmf (F,[]) (D,[]) ([0;0] ++ [1;0]^^(S x)) ([1;1;1] ++ [0] ++ [1;0]^^x).
Lemma stop1 c a: segRL tmf (B,[]) (D,[]) ([0;1]^^(S c) ++ [0;0] ++ [1;0]^^(S a))
([0] ++ [1;0]^^c ++ [1;1;1;1] ++ [0] ++ [1;0]^^a).
Lemma edge0L x f: sideRL tmf (F,[]) (D,[]) (([0] ++ [1;0]^^(S x) ++ [1;1;1]^^f) *> const 0)
(([0] ++ [1;0]^^x ++ [1;1;1]^^(S f)) *> const 0).
Lemma edge0E y f: sideRL tmf (B,[]) (D,[]) (([0] ++ [1;0]^^(S y) ++ [1;1;1]^^f) *> const 0)
(([0] ++ [1;0]^^y ++ [1;1;1]^^(S f)) *> const 0).
Definition blkp (p:nat*nat) := blk (fst p) (snd p).
Definition bmidp (p:nat*nat) := bmid (fst p) (snd p).
Definition lbwp (p:nat*nat) := lbw (fst p) (snd p).
Fixpoint cw (ch:list (nat*nat)) : list Sym := match ch with [] => [] | p::ch => blkp p ++ cw ch end.
Fixpoint cmid (ch:list (nat*nat)) : list Sym := match ch with [] => [] | p::ch => cmid ch ++ bmidp p end.
Fixpoint clbw (ch:list (nat*nat)) : list Sym := match ch with [] => [] | p::ch => clbw ch ++ lbwp p end.
Lemma chainRR ch: segRR tmf (F,[]) (F,[]) (cw ch) (cmid ch).
Lemma chainLL ch: segLL tmf (D,[]) (D,[]) (clbw ch) (cw ch).
Lemma bmid_shift m j: bmid m j ++ [0;1] = [0;1] ++ lbw m j.
Lemma cmid_shift ch: cmid ch ++ [0;1] = [0;1] ++ clbw ch.
Lemma bmid_S m j: bmid (S m) j = [0;1] ++ lbw m j.
Definition pw c j ch := blk c j ++ cw ch.
Lemma prefRR c j ch: segRR tmf (B,[]) (F,[]) (pw c j ch) (cmid ch ++ bmid c j).
Lemma prefLL c j ch: segLL tmf (D,[]) (D,[]) (cmid ch ++ bmid (S c) j) (pw c j ch ++ [0;1]).
Lemma segRL_frame {t h1 h2 w w'} u: segRL t h1 h2 w w' -> segRL t h1 h2 (w ++ u) (w' ++ u).
Definition lead1 a x : list Sym := blk a 1 ++ [0] ++ [1;0]^^x.
Definition lead0 a x : list Sym := [0;1]^^a ++ [0;0] ++ [1;0]^^x.
Definition tailw g : list Sym := [1;1] ++ [1;1;1]^^g.
Definition hB : DH0 := (B,[]).
Definition hD : DH0 := (D,[]).
Definition h : list (DH0*DH0) := [(hB,hD)].
Lemma stopK c j ch a x: segRL tmf hB hD (pw (S c) j ch ++ lead0 a (S x)) (pw c j ch ++ lead1 a x).
Lemma stopK1 c a: segRL tmf hB hD (lead0 (S c) (S a)) (lead1 c a).
Definition passK_mid c j ch a x := (xbmid x ++ bmid a 1) ++ (cmid ch ++ bmid (S c) j).
Lemma passK_RR c j ch a x: segRR tmf hB hB (pw (S c) j ch ++ lead1 a x ++ [1;1]) (passK_mid c j ch a x).
Lemma passK_LL c j ch a x: segLL tmf hD hD (passK_mid c j ch a x) (pw c j ch ++ lead0 (S a) (S (S x)) ++ [1;1]).
Lemma passK c j ch a x: segRLs tmf h h (pw (S c) j ch ++ lead1 a x ++ [1;1]) (pw c j ch ++ lead0 (S a) (S (S x)) ++ [1;1]).
Definition passK1_mid c x := xbmid x ++ bmid c 1.
Lemma passK1_RR c x: segRR tmf hB hB (lead1 c x ++ [1;1]) (passK1_mid c x).
Lemma passK1_LL c x: segLL tmf hD hD (passK1_mid c x) (lead0 c (S (S x)) ++ [1;1]).
Lemma passK1 c x: segRLs tmf h h (lead1 c x ++ [1;1]) (lead0 c (S (S x)) ++ [1;1]).
Lemma halt0 x l r: halts tmf (l {{B}}> lead0 0 x *> r).
Lemma edge0L0 f: sideRL tmf (F,[]) (D,[]) (([0] ++ [1;1;1]^^f) *> const 0)
(([1;1] ++ [1;1;1]^^f) *> const 0).
Lemma segRR_sideRL_LL {t h1 h2 h3 h4 w m w' r r'}:
segRR t h1 h2 w m -> sideRL t h2 h3 r r' -> segLL t h3 h4 m w' ->
sideRL t h1 h4 (w *> r) (w' *> r').
Definition edgew x f : list Sym := [0] ++ [1;0]^^x ++ [1;1;1]^^f.
Lemma u0L c j ch x f: sideRL tmf hB hD ((pw (S c) j ch ++ edgew x f) *> const 0)
((pw c j ch ++ edgew x (S f)) *> const 0).
Lemma u0E y f: sideRL tmf hB hD (edgew (S y) f *> const 0) (edgew y (S f) *> const 0).
Definition root t (X:side) : Q * tape := const 0 <{{A}} ([0;1]^^t ++ [0;1;1]) *> X.
Definition wmid t : list Sym := [0] ++ [0;1]^^t ++ [0;1;0;1].
Lemma root_in t X: root t X -->* wmid t *> const 0 {{B}}> X.
Lemma sweepA: forall l r n, l <* [0;1]^^n <{{A}} r -->* l <{{A}} [0;1]^^n *> r.
Lemma root_out t X: wmid t *> const 0 <{{D}} X -->* root (S t) X.
Lemma root_step t X X': sideRL tmf hB hD X X' -> root t X -->+ root (S t) X'.
Lemma root_steps n: forall t X X', sideRLs tmf (h^^n) X X' -> root t X -->* root (n+t) X'.
Lemma root_halt t X: sideRLs_halt tmf h X -> halts tmf (root t X).
Definition hF : DH0 := (F,[]).
Definition leadw (b:bool) a x := if b then lead1 a x else lead0 a x.
Definition uw bs b a x (far:list Sym) := cw bs ++ leadw b a x ++ far.
Definition consume (bs: list (nat*nat)) (a:nat) : option (nat * list (nat*nat) * nat) :=
match bs with
| (S c, j) :: r => Some (O, (c,j)::r, a)
| (O, j) :: r => Some (j, r, a)
| [] => match a with S a' => Some (O, [], a') | O => None end
end.
Lemma cw_app l1 l2: cw (l1 ++ l2) = cw l1 ++ cw l2.
Lemma yLL_glue j: segLL tmf (D,[]) (D,[]) ([0;1;1]^^j) ([1;1;1]^^j).
Lemma prefLL_glue j ch: segLL tmf (D,[]) (D,[]) (cmid ch ++ bmid 0 j) ([1;1;1]^^j ++ cw ch ++ [0;1]).
Lemma gen_RL {ci co} (HF: segRL tmf hF hD ci co) c j ch:
segRL tmf hB hD (pw (S c) j ch ++ ci) (pw c j ch ++ [0;1] ++ co).
Lemma gen_RLg {ci co} (HF: segRL tmf hF hD ci co) j ch:
segRL tmf hB hD (pw 0 j ch ++ ci) ([1;1;1]^^j ++ cw ch ++ [0;1] ++ co).
Lemma lrcons1 {w1 w2 m}: segRR tmf hB hB w1 m -> segLL tmf hD hD m w2 -> segRLs tmf h h w1 w2.
Lemma gen_fwd {ci m co} (HR: segRR tmf hF hB ci m) (HL: segLL tmf hD hD m co) c j ch:
segRLs tmf h h (pw (S c) j ch ++ ci) (pw c j ch ++ [0;1] ++ co).
Lemma gen_fwdg {ci m co} (HR: segRR tmf hF hB ci m) (HL: segLL tmf hD hD m co) j ch:
segRLs tmf h h (pw 0 j ch ++ ci) ([1;1;1]^^j ++ cw ch ++ [0;1] ++ co).
Lemma gen_side {ci co R R'} (HF: sideRL tmf hF hD (ci *> R) (co *> R')) c j ch:
sideRL tmf hB hD ((pw (S c) j ch ++ ci) *> R) ((pw c j ch ++ [0;1] ++ co) *> R').
Lemma gen_sideg {ci co R R'} (HF: sideRL tmf hF hD (ci *> R) (co *> R')) j ch:
sideRL tmf hB hD ((pw 0 j ch ++ ci) *> R) (([1;1;1]^^j ++ cw ch ++ [0;1] ++ co) *> R').
Lemma segRL_side {t h1 h2 w w'} R: segRL t h1 h2 w w' -> sideRL t h1 h2 (w *> R) (w' *> R).
Lemma cstopF a x far: exists co, segRL tmf hF hD (lead0 a (S x) ++ far) co /\ [0;1] ++ co = lead1 a x ++ far.
Lemma t_stop bs a x far ov bs' a': consume bs a = Some (ov, bs', a') ->
segRL tmf hB hD (uw bs false a (S x) far) ([1;1;1]^^ov ++ uw bs' true a' x far).
Definition cpass_mid a x := xbmid x ++ bmid a 1.
Lemma cpassRR a x: segRR tmf hF hB (lead1 a x ++ [1;1]) (cpass_mid a x).
Definition cpass_co a x := ([0;1]^^a ++ [0;0] ++ [1;0;1]) ++ ([0] ++ [1;0]^^x ++ [1;1]).
Lemma cpassLL a x: segLL tmf hD hD (cpass_mid a x) (cpass_co a x).
Lemma t_pass bs a x ov bs' a': consume bs (S a) = Some (ov, bs', a') ->
segRLs tmf h h (uw bs true a x (tailw 0)) ([1;1;1]^^ov ++ uw bs' false a' (S (S x)) (tailw 0)).
Definition um1 a x : list Sym := [0;0;1;0;1;1;0;1;0;1] ++ [0;1]^^x ++ [1] ++ [0;1]^^a.
Definition um2 a x g : list Sym := [0;0;1;0;1;1;0;1;1;0;1] ++ [1;0;1]^^g ++ [0;1] ++ [0;1]^^x ++ [1] ++ [0;1]^^a.
Definition uco1 a x : list Sym := [0;1]^^a ++ [1;1;1;0;1;0] ++ [1;0]^^x ++ [0;1;0;1;1].
Definition uco2 a x g : list Sym := [0;1]^^a ++ [1;1;1;0;1] ++ [0;1]^^x ++ [1;1;1] ++ [1;1;1]^^g ++ [0;0;1;0;1;1].
Lemma u1RF a x: segRR tmf hF hB (lead1 a x ++ tailw 1) (um1 a x).
Lemma u1RB a x: segRR tmf hB hB (lead1 a x ++ tailw 1) (um1 a x).
Lemma u1L a x: segLL tmf hD hD (um1 a x) (uco1 a x).
Lemma u2RF a x g: segRR tmf hF hB (lead1 a x ++ tailw (S (S g))) (um2 a x g).
Lemma u2RB a x g: segRR tmf hB hB (lead1 a x ++ tailw (S (S g))) (um2 a x g).
Lemma u2L a x g: segLL tmf hD hD (um2 a x g) (uco2 a x g).
Lemma t_ungl1 bs a x ov bs' a': consume (bs ++ [(a,1%nat)]) (S x) = Some (ov, bs', a') ->
segRLs tmf h h (uw bs true a x (tailw 1)) ([1;1;1]^^ov ++ uw bs' false a' 1 (tailw 0)).
Lemma t_ungl2 bs a x g ov bs' a': consume (bs ++ [(a,1%nat);(x,S g)]) 0%nat = Some (ov, bs', a') ->
segRLs tmf h h (uw bs true a x (tailw (S (S g)))) ([1;1;1]^^ov ++ uw bs' false a' 1 (tailw 0)).
Lemma t_halt x far l r: halts tmf (l {{B}}> uw [] false 0 x far *> r).
Definition edge1w f : list Sym := [1] ++ [1;1;1]^^f.
Lemma z_lead bs x f ov bs' a': bs <> [] -> consume bs 0%nat = Some (ov, bs', a') ->
sideRL tmf hB hD ((cw bs ++ edgew x f) *> const 0) (([1;1;1]^^ov ++ cw bs' ++ edgew x (S f)) *> const 0).
Lemma z_empty y f: sideRL tmf hB hD (edgew (S y) f *> const 0) (edgew y (S f) *> const 0).
Lemma z_absorb f: sideRL tmf hB hD (edgew 0 (S f) *> const 0) (([1;1] ++ [1;1;1]^^(S f)) *> const 0).
Lemma z_stop bs a x f ov bs' a': consume bs a = Some (ov, bs', a') ->
sideRL tmf hB hD (uw bs false a (S x) (edge1w f) *> const 0) (([1;1;1]^^ov ++ uw bs' true a' x (edge1w f)) *> const 0).
Definition zco a x f : list Sym := [0;1]^^a ++ [1;1;1;0;1] ++ [0;1]^^x ++ [1;1;1]^^f ++ [0;1;1;1].
Lemma z1F a x f: sideRL tmf hF hD ((lead1 a x ++ edge1w f) *> const 0) (zco a x f *> const 0).
Lemma z1B a x f: sideRL tmf hB hD ((lead1 a x ++ edge1w f) *> const 0) (zco a x f *> const 0).
Lemma z_1111 bs a x f ov bs' a': consume (bs ++ [(a,1%nat);(x,f)]) 0%nat = Some (ov, bs', a') ->
sideRL tmf hB hD (uw bs true a x (edge1w f) *> const 0) (([1;1;1]^^ov ++ cw bs' ++ edgew 0 1) *> const 0).
Definition NT s g (X:side) : Q * tape := const 0 <{{A}} ([1;0]^^s ++ [1] ++ [0;0] ++ [1;0] ++ tailw g) *> X.
Definition rmid t : list Sym := [0;0;1;0;1;1;0;1;0] ++ [1;0]^^t.
Lemma reset1_in t X: root t ([1;1;1] *> X) -->* rmid t *> const 0 {{B}}> X.
Lemma reset1_out t X: rmid t *> const 0 <{{D}} X -->* NT (S t) 0 X.
Lemma reset1 t X X': sideRL tmf hB hD X X' -> root t ([1;1;1] *> X) -->* NT (S t) 0 X'.
Lemma reset1_halt t X: sideRLs_halt tmf h X -> halts tmf (root t ([1;1;1] *> X)).
Lemma reset2 s g X: NT (S s) g X -->* root 0 ((lead1 s 0 ++ tailw g) *> X).
Definition cvp (p:N*N) : nat*nat := (N.to_nat (fst p), N.to_nat (snd p)).
Definition cvl (bs:list (N*N)) := map cvp bs.
Record unitN := UN { ubs : list (N*N); ubit : bool; ua : N; ux : N; ug : N }.
Definition uwN u := uw (cvl (ubs u)) (ubit u) (N.to_nat (ua u)) (N.to_nat (ux u)) (tailw (N.to_nat (ug u))).
Fixpoint dwords (us:list unitN) : list Sym := match us with [] => [] | u::us => uwN u ++ dwords us end.
Inductive zN := Z0 (bs:list (N*N)) (x f:N) | ZD (bs:list (N*N)) (b:bool) (a x f:N).
Definition zside z : side := match z with
| Z0 bs x f => (cw (cvl bs) ++ edgew (N.to_nat x) (N.to_nat f)) *> const 0
| ZD bs b a x f => uw (cvl bs) b (N.to_nat a) (N.to_nat x) (edge1w (N.to_nat f)) *> const 0 end.
Inductive tailN := TT (t g:N) | NTl (s g:N).
Record cfg := Cfg { ctl : tailN; cus : list unitN; cz : zN }.
Definition denote c : Q * tape := match ctl c with
| TT t g => root (N.to_nat t) (([1;1;1]^^(N.to_nat g) ++ dwords (cus c)) *> zside (cz c))
| NTl s g => NT (N.to_nat s) (N.to_nat g) (dwords (cus c) *> zside (cz c)) end.
Definition consumeN (bs:list (N*N)) (a:N) : option (N * list (N*N) * N) :=
match bs with
| (c, j) :: r => if N.eqb c 0 then Some (j, r, a) else Some (0%N, (N.pred c, j)::r, a)
| [] => if N.eqb a 0 then None else Some (0%N, [], N.pred a)
end.
Lemma consumeN_spec bs a ov bs' a': consumeN bs a = Some (ov, bs', a') ->
consume (cvl bs) (N.to_nat a) = Some (N.to_nat ov, cvl bs', N.to_nat a').
Lemma cvl_app l1 l2: cvl (l1 ++ l2) = cvl l1 ++ cvl l2.
Inductive tres := TStop (ov:N) (u:unitN) | TPass (ov:N) (u:unitN) | THalt | TFail.
Definition touchN u : tres :=
if ubit u then
  if N.eqb (ug u) 0 then
    match consumeN (ubs u) (N.succ (ua u)) with Some (ov,bs',a') => TPass ov (UN bs' false a' (ux u + 2) 0) | None => TFail end
  else if N.eqb (ug u) 1 then
    match consumeN (ubs u ++ [(ua u, 1%N)]) (N.succ (ux u)) with Some (ov,bs',a') => TPass ov (UN bs' false a' 1 0) | None => TFail end
… +8 lines
Lemma touchN_stop u ov u': touchN u = TStop ov u' -> segRL tmf hB hD (uwN u) ([1;1;1]^^(N.to_nat ov) ++ uwN u').
Lemma touchN_pass u ov u': touchN u = TPass ov u' -> segRLs tmf h h (uwN u) ([1;1;1]^^(N.to_nat ov) ++ uwN u') /\ ug u' = 0%N.
Lemma touchN_halt u: touchN u = THalt -> forall l r, halts tmf (l {{B}}> uwN u *> r).
Inductive zres := ZRet (ov:N) (z:zN) | ZAbs (f:N) | ZFail.
Definition ztouch z : zres := match z with
| Z0 [] y f => if N.eqb y 0 then (if N.eqb f 0 then ZFail else ZAbs f) else ZRet 0%N (Z0 [] (N.pred y) (N.succ f))
| Z0 bs x f => match consumeN bs 0%N with Some (ov,bs',_) => ZRet ov (Z0 bs' x (N.succ f)) | None => ZFail end
| ZD bs false a x f => if N.eqb x 0 then ZFail else
    match consumeN bs a with Some (ov,bs',a') => ZRet ov (ZD bs' true a' (N.pred x) f) | None => ZFail end
| ZD bs true a x f => match consumeN (bs ++ [(a,1%N);(x,f)]) 0%N with Some (ov,bs',_) => ZRet ov (Z0 bs' 0 1) | None => ZFail end
… +1 lines
Lemma ztouch_ret z ov z': ztouch z = ZRet ov z' -> sideRL tmf hB hD (zside z) ([1;1;1]^^(N.to_nat ov) *> zside z').
Lemma ztouch_abs z f: ztouch z = ZAbs f -> sideRL tmf hB hD (zside z) (([1;1] ++ [1;1;1]^^(N.to_nat f)) *> const 0).
Inductive cres := CRet (ov:N) (us:list unitN) (z:zN) | CHalt | CFail.
Definition setg u g := UN (ubs u) (ubit u) (ua u) (ux u) g.
Fixpoint callN (us:list unitN) (z:zN) : cres := match us with
| [] => match ztouch z with ZRet ov z' => CRet ov [] z' | _ => CFail end
| u :: us1 => match touchN u with
  | TStop ov u' => CRet ov (u' :: us1) z
  | THalt => CHalt
  | TFail => CFail
… +11 lines
Lemma side1 {w w' r r'}: segRLs tmf h h w w' -> sideRL tmf hB hD r r' -> sideRL tmf hB hD (w *> r) (w' *> r').
Lemma setg_word u g: ug u = 0%N -> uwN u ++ [1;1;1]^^(N.to_nat g) = uwN (setg u g).
Lemma abs_word u f: ug u = 0%N -> uwN u ++ [1;1] ++ [1;1;1]^^(N.to_nat f) =
uw (cvl (ubs u)) (ubit u) (N.to_nat (ua u)) (N.to_nat (ux u)) (edge1w (N.to_nat (ug u + f + 1))).
Lemma callN_ret us: forall z ov us' z', callN us z = CRet ov us' z' ->
sideRL tmf hB hD (dwords us *> zside z) (([1;1;1]^^(N.to_nat ov) ++ dwords us') *> zside z').
Lemma callN_halt us: forall z, callN us z = CHalt -> sideRLs_halt tmf h (dwords us *> zside z).
Inductive ires := IOk (c:cfg) | IHalt | IFail.
Definition inc1 c : ires := match ctl c with
| TT t g =>
  if N.eqb g 0 then match callN (cus c) (cz c) with
    | CRet ov us' z' => IOk (Cfg (TT (N.succ t) ov) us' z') | CHalt => IHalt | CFail => IFail end
  else if N.eqb g 1 then match callN (cus c) (cz c) with
    | CRet ov us' z' => IOk (Cfg (NTl (N.succ t) ov) us' z') | CHalt => IHalt | CFail => IFail end
… +3 lines
Lemma inc1_ok c c': inc1 c = IOk c' -> denote c -->* denote c'.
Lemma inc1_halt c: inc1 c = IHalt -> halts tmf (denote c).
Lemma stop1s {bs a x far ov bs' a'}: consume bs a = Some (ov, bs', a') ->
segRLs tmf h [] (uw bs false a (S x) far) ([1;1;1]^^ov ++ uw bs' true a' x far).
Lemma pairK q: forall c j r a x, segRLs tmf (h^^(q*2)) (h^^q)
(uw ((q*2+c, j)::r) false a (S x) (tailw 0)) (uw ((c,j)::r) false (q+a) (S (q+x)) (tailw 0)).
Lemma pair1 q: forall a x, segRLs tmf (h^^(q*2)) (h^^q)
(uw [] false (q+a) (S x) (tailw 0)) (uw [] false a (S (q+x)) (tailw 0)).
Definition b2n (b:bool) : nat := if b then 1 else 0.
Lemma clK0 q rb c j r a x: segRLs tmf (h^^(q*2 + b2n rb)) (h^^q)
(uw ((q*2 + b2n rb + c, j)::r) false a (S x) (tailw 0)) (uw ((c,j)::r) rb (q+a) (q + S x - b2n rb) (tailw 0)).
Lemma clK1 q rb c j r a x: segRLs tmf (h^^(S (q*2 + b2n rb))) (h^^(S q))
(uw ((S (q*2 + b2n rb + c), j)::r) true a x (tailw 0)) (uw ((c,j)::r) rb (q + S a) (q + S (S x) - b2n rb) (tailw 0)).
Lemma cl10 q rb a x: segRLs tmf (h^^(q*2 + b2n rb)) (h^^q)
(uw [] false (q + b2n rb + a) (S x) (tailw 0)) (uw [] rb a (q + S x - b2n rb) (tailw 0)).
Lemma cl11 q rb a x: segRLs tmf (h^^(S (q*2 + b2n rb))) (h^^(S q))
(uw [] true (q + b2n rb + a) x (tailw 0)) (uw [] rb a (q + S (S x) - b2n rb) (tailw 0)).
Definition b2N (b:bool) : N := if b then 1%N else 0%N.
Lemma b2N_nat b: N.to_nat (b2N b) = b2n b.
Lemma div2_nat n: N.to_nat n = N.to_nat (N.div2 n) * 2 + b2n (N.odd n).
Definition closedU (n:N) (u:unitN) : option (unitN * N) :=
if N.eqb n 0 then Some (u, 0%N) else
match ubs u with
| (c,j)::r =>
  if negb (ubit u) then
    if N.eqb n 1 then
… +22 lines
Lemma closedU_spec n u u' p: closedU n u = Some (u', p) ->
segRLs tmf (h^^(N.to_nat n)) (h^^(N.to_nat p)) (uwN u) (uwN u').
Lemma zLs m: forall c j r x f, sideRLs tmf (h^^m) ((cw ((m+c,j)::r) ++ edgew x f) *> const 0)
((cw ((c,j)::r) ++ edgew x (m+f)) *> const 0).
Lemma zEs m: forall y f, sideRLs tmf (h^^m) (edgew (m+y) f *> const 0) (edgew y (m+f) *> const 0).
Definition closedZ (m:N) (z:zN) : option zN :=
if N.eqb m 0 then Some z else
match z with
| Z0 [] y f => if N.ltb y m then None else Some (Z0 [] (y - m) (f + m))
| Z0 ((c,j)::r) x f => if N.ltb c m then None else Some (Z0 (((c - m)%N, j)::r) x (f + m))
| ZD _ _ _ _ _ => None
… +1 lines
Lemma closedZ_spec m z z': closedZ m z = Some z' -> sideRLs tmf (h^^(N.to_nat m)) (zside z) (zside z').
Fixpoint batchL (n:N) (us:list unitN) (z:zN) : option (list unitN * zN) := match us with
| [] => match closedZ n z with Some z' => Some ([], z') | None => None end
| u :: us => match closedU n u with
  | Some (u', p) => match batchL p us z with Some (us', z') => Some (u' :: us', z') | None => None end
  | None => None end end.
Lemma batchL_spec us: forall n z us' z', batchL n us z = Some (us', z') ->
sideRLs tmf (h^^(N.to_nat n)) (dwords us *> zside z) (dwords us' *> zside z').
Definition evt_unit (u:unitN) : N :=
let own := match ubs u with (c,_)::_ => N.succ c | [] => (2 * ua u + b2N (ubit u))%N end in
let own := if negb (ubit u) && N.eqb (ux u) 0 then 1%N else own in
if N.eqb (ug u) 0 then own else N.min own (if ubit u then 1%N else 2%N).
Definition evt_z z : N := match z with Z0 [] y _ => N.succ y | Z0 ((c,_)::_) _ _ => N.succ c | ZD _ _ _ _ _ => 1%N end.
Definition first_inc (C q n : N) : N := (n * 2^q - C mod 2^q)%N.
Fixpoint cval (us:list unitN) (i:N) : N := match us with
| [] => 0%N | u :: us => ((if ubit u then 2^i else 0) + cval us (N.succ i))%N end.
Fixpoint pmin (us:list unitN) (i C:N) (z:zN) : N := match us with
| [] => first_inc C i (evt_z z)
| u :: us => N.min (first_inc C i (evt_unit u)) (pmin us (N.succ i) C z) end.
Definition propose (us:list unitN) (z:zN) : N := N.pred (pmin us 0 (cval us 0) z).
Definition batch_step c : option cfg := match ctl c with
| TT t g => if N.eqb g 0 then
    let d := propose (cus c) (cz c) in
    if N.eqb d 0 then None else
    match batchL d (cus c) (cz c) with Some (us', z') => Some (Cfg (TT (t + d) 0) us' z') | None => None end
  else None
… +1 lines
Lemma batch_step_spec c c': batch_step c = Some c' -> denote c -->* denote c'.
Definition next c : cfg + unit := match batch_step c with
| Some c' => inl c'
| None => match inc1 c with IOk c' => inl c' | IHalt => inr tt | IFail => inl c end end.
Lemma next_spec c: match next c with inl c' => denote c -->* denote c' | inr _ => halts tmf (denote c) end.
Definition c342 := Cfg (NTl 1 1) [] (Z0 [(0%N,3%N)] 0 1).
Definition check fuel := match N_iter_until next (inl c342) fuel with inl _ => false | inr _ => true end.
Theorem check_spec fuel: check fuel = true -> halts tmf (denote c342).
Definition run (T:N) (c:cfg) : cfg + unit := N_iter_until next (inl c) T.
Definition unl (x:cfg + unit) : cfg := match x with inl c => c | inr _ => c342 end.
Lemma run_ok T c c': run T c = inl c' -> denote c -->* denote c'.
Lemma run_halt T c: run T c = inr tt -> halts tmf (denote c).
Definition k1 := Eval vm_compute in unl (run 5000 c342).
Lemma s1: run 5000 c342 = inl k1.
Definition k2 := Eval vm_compute in unl (run 5000 k1).
Lemma s2: run 5000 k1 = inl k2.
Definition k3 := Eval vm_compute in unl (run 5000 k2).
Lemma s3: run 5000 k2 = inl k3.
Definition k4 := Eval vm_compute in unl (run 5000 k3).
Lemma s4: run 5000 k3 = inl k4.
Definition k5 := Eval vm_compute in unl (run 5000 k4).
Lemma s5: run 5000 k4 = inl k5.
Definition k6 := Eval vm_compute in unl (run 5000 k5).
Lemma s6: run 5000 k5 = inl k6.
Definition k7 := Eval vm_compute in unl (run 5000 k6).
Lemma s7: run 5000 k6 = inl k7.
Definition k8 := Eval vm_compute in unl (run 5000 k7).
Lemma s8: run 5000 k7 = inl k8.
Definition k9 := Eval vm_compute in unl (run 5000 k8).
Lemma s9: run 5000 k8 = inl k9.
Definition k10 := Eval vm_compute in unl (run 5000 k9).
Lemma s10: run 5000 k9 = inl k10.
Definition k11 := Eval vm_compute in unl (run 5000 k10).
Lemma s11: run 5000 k10 = inl k11.
Definition k12 := Eval vm_compute in unl (run 5000 k11).
Lemma s12: run 5000 k11 = inl k12.
Definition k13 := Eval vm_compute in unl (run 5000 k12).
Lemma s13: run 5000 k12 = inl k13.
Definition k14 := Eval vm_compute in unl (run 5000 k13).
Lemma s14: run 5000 k13 = inl k14.
Definition k15 := Eval vm_compute in unl (run 5000 k14).
Lemma s15: run 5000 k14 = inl k15.
Definition k16 := Eval vm_compute in unl (run 5000 k15).
Lemma s16: run 5000 k15 = inl k16.
Definition k17 := Eval vm_compute in unl (run 5000 k16).
Lemma s17: run 5000 k16 = inl k17.
Definition k18 := Eval vm_compute in unl (run 5000 k17).
Lemma s18: run 5000 k17 = inl k18.
Definition k19 := Eval vm_compute in unl (run 5000 k18).
Lemma s19: run 5000 k18 = inl k19.
Definition k20 := Eval vm_compute in unl (run 5000 k19).
Lemma s20: run 5000 k19 = inl k20.
Definition k21 := Eval vm_compute in unl (run 5000 k20).
Lemma s21: run 5000 k20 = inl k21.
Lemma s22: run 5000 k21 = inr tt.
Lemma init: c0 -[tmf]->* denote c342.
Lemma halt_tmf: halts tmf c0.
Lemma halt: halts tm c0.

#	kind	name	statement (no proof body)	line	vs template
1	Definition	`tm`	Definition tm := Eval compute in (TM_from_str "1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB").	L37	adapted
2	Definition	`tmf`	Definition tmf := Eval compute in (flip tm).	L38	new
3	Lemma	`segRR_app`	Lemma segRR_app {t h1 h2 h3 w1 w2 m1 m2}: segRR t h1 h2 w1 m1 -> segRR t h2 h3 w2 m2 -> segRR t h1 h3 (w1 ++ w2) (m2 ++ m1).	L43	new
4	Lemma	`segLL_app`	Lemma segLL_app {t h1 h2 h3 w1 w2 o1 o2}: segLL t h1 h2 w1 o1 -> segLL t h2 h3 w2 o2 -> segLL t h1 h3 (w1 ++ w2) (o2 ++ o1).	L50	new
5	Lemma	`segRR_RL_LL`	Lemma segRR_RL_LL {t h1 h2 h3 h4 w1 w2 m w1' w2'}: segRR t h1 h2 w1 m -> segRL t h2 h3 w2 w2' -> segLL t h3 h4 m w1' -> segRL t h1 h4 (w1 ++ w2) (w1' ++ w2').	L57	new
6	Definition	`stack`	Definition stack j : list Sym := [1] ++ [1;1;1]^^j.	L69	new
7	Definition	`blk`	Definition blk m j : list Sym := [0] ++ [1;0]^^m ++ stack j.	L70	new
8	Definition	`bmid`	Definition bmid m j : list Sym := [0;1] ++ [0;1;1]^^j ++ [0;1]^^m.	L71	new
9	Definition	`lbw`	Definition lbw m j : list Sym := [0;1;1]^^j ++ [0;1]^^(S m).	L72	new
10	Definition	`xbmid`	Definition xbmid x : list Sym := [0;0;1] ++ [0;1]^^x.	L73	new
11	Lemma	`blkRR_F`	Lemma blkRR_F m j: segRR tmf (F,[]) (F,[]) (blk m j) (bmid m j).	L76	new
12	Lemma	`blkRR_B`	Lemma blkRR_B m j: segRR tmf (B,[]) (F,[]) (blk m j) (bmid m j).	L78	new
13	Lemma	`blkLL`	Lemma blkLL m j: segLL tmf (D,[]) (D,[]) (lbw m j) (blk m j).	L80	new
14	Lemma	`sweepLL`	Lemma sweepLL: segLL tmf (D,[]) (D,[]) [0;1] [0;1].	L82	new
15	Lemma	`leadLL`	Lemma leadLL a: segLL tmf (A,[]) (D,[]) (bmid a 1) ([0;1]^^a ++ [0;0] ++ [1;0;1]).	L84	new
16	Lemma	`xbRR`	Lemma xbRR x: segRR tmf (F,[]) (B,[]) ([0] ++ [1;0]^^x ++ [1;1]) (xbmid x).	L86	new
17	Lemma	`xbLL`	Lemma xbLL x: segLL tmf (D,[]) (A,[]) (xbmid x) ([0] ++ [1;0]^^x ++ [1;1]).	L88	new
18	Lemma	`leadstopS`	Lemma leadstopS a x: segRL tmf (F,[]) (D,[]) ([0;1]^^(S a) ++ [0;0] ++ [1;0]^^(S x)) ([0] ++ [1;0]^^a ++ [1;1;1;1] ++ [0] ++ [1;0]^^x).	L90	new
19	Lemma	`leadstop0`	Lemma leadstop0 x: segRL tmf (F,[]) (D,[]) ([0;0] ++ [1;0]^^(S x)) ([1;1;1] ++ [0] ++ [1;0]^^x).	L93	new
20	Lemma	`stop1`	Lemma stop1 c a: segRL tmf (B,[]) (D,[]) ([0;1]^^(S c) ++ [0;0] ++ [1;0]^^(S a)) ([0] ++ [1;0]^^c ++ [1;1;1;1] ++ [0] ++ [1;0]^^a).	L95	new
21	Lemma	`edge0L`	Lemma edge0L x f: sideRL tmf (F,[]) (D,[]) (([0] ++ [1;0]^^(S x) ++ [1;1;1]^^f) > const 0) (([0] ++ [1;0]^^x ++ [1;1;1]^^(S f)) > const 0).	L98	new
22	Lemma	`edge0E`	Lemma edge0E y f: sideRL tmf (B,[]) (D,[]) (([0] ++ [1;0]^^(S y) ++ [1;1;1]^^f) > const 0) (([0] ++ [1;0]^^y ++ [1;1;1]^^(S f)) > const 0).	L101	new
23	Definition	`blkp`	Definition blkp (p:nat*nat) := blk (fst p) (snd p).	L106	new
24	Definition	`bmidp`	Definition bmidp (p:nat*nat) := bmid (fst p) (snd p).	L107	new
25	Definition	`lbwp`	Definition lbwp (p:nat*nat) := lbw (fst p) (snd p).	L108	new
26	Fixpoint	`cw`	Fixpoint cw (ch:list (nat*nat)) : list Sym := match ch with [] => [] \| p::ch => blkp p ++ cw ch end.	L109	new
27	Fixpoint	`cmid`	Fixpoint cmid (ch:list (nat*nat)) : list Sym := match ch with [] => [] \| p::ch => cmid ch ++ bmidp p end.	L110	new
28	Fixpoint	`clbw`	Fixpoint clbw (ch:list (nat*nat)) : list Sym := match ch with [] => [] \| p::ch => clbw ch ++ lbwp p end.	L111	new
29	Lemma	`chainRR`	Lemma chainRR ch: segRR tmf (F,[]) (F,[]) (cw ch) (cmid ch).	L113	new
30	Lemma	`chainLL`	Lemma chainLL ch: segLL tmf (D,[]) (D,[]) (clbw ch) (cw ch).	L119	new
31	Lemma	`bmid_shift`	Lemma bmid_shift m j: bmid m j ++ [0;1] = [0;1] ++ lbw m j.	L125	new
32	Lemma	`cmid_shift`	Lemma cmid_shift ch: cmid ch ++ [0;1] = [0;1] ++ clbw ch.	L127	new
33	Lemma	`bmid_S`	Lemma bmid_S m j: bmid (S m) j = [0;1] ++ lbw m j.	L133	new
34	Definition	`pw`	Definition pw c j ch := blk c j ++ cw ch.	L138	new
35	Lemma	`prefRR`	Lemma prefRR c j ch: segRR tmf (B,[]) (F,[]) (pw c j ch) (cmid ch ++ bmid c j).	L139	new
36	Lemma	`prefLL`	Lemma prefLL c j ch: segLL tmf (D,[]) (D,[]) (cmid ch ++ bmid (S c) j) (pw c j ch ++ [0;1]).	L141	new
37	Lemma	`segRL_frame`	Lemma segRL_frame {t h1 h2 w w'} u: segRL t h1 h2 w w' -> segRL t h1 h2 (w ++ u) (w' ++ u).	L150	new
38	Definition	`lead1`	Definition lead1 a x : list Sym := blk a 1 ++ [0] ++ [1;0]^^x.	L155	new
39	Definition	`lead0`	Definition lead0 a x : list Sym := [0;1]^^a ++ [0;0] ++ [1;0]^^x.	L156	new
40	Definition	`tailw`	Definition tailw g : list Sym := [1;1] ++ [1;1;1]^^g.	L157	new
41	Definition	`hB`	Definition hB : DH0 := (B,[]).	L159	new
42	Definition	`hD`	Definition hD : DH0 := (D,[]).	L160	new
43	Definition	`h`	Definition h : list (DH0*DH0) := [(hB,hD)].	L161	adapted
44	Lemma	`stopK`	Lemma stopK c j ch a x: segRL tmf hB hD (pw (S c) j ch ++ lead0 a (S x)) (pw c j ch ++ lead1 a x).	L163	new
45	Lemma	`stopK1`	Lemma stopK1 c a: segRL tmf hB hD (lead0 (S c) (S a)) (lead1 c a).	L172	new
46	Definition	`passK_mid`	Definition passK_mid c j ch a x := (xbmid x ++ bmid a 1) ++ (cmid ch ++ bmid (S c) j).	L175	new
47	Lemma	`passK_RR`	Lemma passK_RR c j ch a x: segRR tmf hB hB (pw (S c) j ch ++ lead1 a x ++ [1;1]) (passK_mid c j ch a x).	L176	new
48	Lemma	`passK_LL`	Lemma passK_LL c j ch a x: segLL tmf hD hD (passK_mid c j ch a x) (pw c j ch ++ lead0 (S a) (S (S x)) ++ [1;1]).	L182	new
49	Lemma	`passK`	Lemma passK c j ch a x: segRLs tmf h h (pw (S c) j ch ++ lead1 a x ++ [1;1]) (pw c j ch ++ lead0 (S a) (S (S x)) ++ [1;1]).	L188	new
50	Definition	`passK1_mid`	Definition passK1_mid c x := xbmid x ++ bmid c 1.	L194	new
51	Lemma	`passK1_RR`	Lemma passK1_RR c x: segRR tmf hB hB (lead1 c x ++ [1;1]) (passK1_mid c x).	L195	new
52	Lemma	`passK1_LL`	Lemma passK1_LL c x: segLL tmf hD hD (passK1_mid c x) (lead0 c (S (S x)) ++ [1;1]).	L197	new
53	Lemma	`passK1`	Lemma passK1 c x: segRLs tmf h h (lead1 c x ++ [1;1]) (lead0 c (S (S x)) ++ [1;1]).	L202	new
54	Lemma	`halt0`	Lemma halt0 x l r: halts tmf (l {{B}}> lead0 0 x *> r).	L209	new
55	Lemma	`edge0L0`	Lemma edge0L0 f: sideRL tmf (F,[]) (D,[]) (([0] ++ [1;1;1]^^f) > const 0) (([1;1] ++ [1;1;1]^^f) > const 0).	L213	new
56	Lemma	`segRR_sideRL_LL`	Lemma segRR_sideRL_LL {t h1 h2 h3 h4 w m w' r r'}: segRR t h1 h2 w m -> sideRL t h2 h3 r r' -> segLL t h3 h4 m w' -> sideRL t h1 h4 (w > r) (w' > r').	L216	new
57	Definition	`edgew`	Definition edgew x f : list Sym := [0] ++ [1;0]^^x ++ [1;1;1]^^f.	L226	new
58	Lemma	`u0L`	Lemma u0L c j ch x f: sideRL tmf hB hD ((pw (S c) j ch ++ edgew x f) > const 0) ((pw c j ch ++ edgew x (S f)) > const 0).	L228	new
59	Lemma	`u0E`	Lemma u0E y f: sideRL tmf hB hD (edgew (S y) f > const 0) (edgew y (S f) > const 0).	L238	new
60	Definition	`root`	Definition root t (X:side) : Q * tape := const 0 <{{A}} ([0;1]^^t ++ [0;1;1]) *> X.	L242	new
61	Definition	`wmid`	Definition wmid t : list Sym := [0] ++ [0;1]^^t ++ [0;1;0;1].	L243	new
62	Lemma	`root_in`	Lemma root_in t X: root t X -->* wmid t *> const 0 {{B}}> X.	L244	new
63	Lemma	`sweepA`	Lemma sweepA: forall l r n, l <* [0;1]^^n <{{A}} r -->* l <{{A}} [0;1]^^n *> r.	L246	new
64	Lemma	`root_out`	Lemma root_out t X: wmid t > const 0 <{{D}} X --> root (S t) X.	L248	new
65	Lemma	`root_step`	Lemma root_step t X X': sideRL tmf hB hD X X' -> root t X -->+ root (S t) X'.	L254	new
66	Lemma	`root_steps`	Lemma root_steps n: forall t X X', sideRLs tmf (h^^n) X X' -> root t X -->* root (n+t) X'.	L261	new
67	Lemma	`root_halt`	Lemma root_halt t X: sideRLs_halt tmf h X -> halts tmf (root t X).	L269	new
68	Definition	`hF`	Definition hF : DH0 := (F,[]).	L275	new
69	Definition	`leadw`	Definition leadw (b:bool) a x := if b then lead1 a x else lead0 a x.	L276	new
70	Definition	`uw`	Definition uw bs b a x (far:list Sym) := cw bs ++ leadw b a x ++ far.	L277	new
71	Definition	`consume`	Definition consume (bs: list (natnat)) (a:nat) : option (nat list (natnat) nat) := match bs with \| (S c, j) :: r => Some (O, (c,j)::r, a) \| (O, j) :: r => Some (j, r, a) \| [] => match a with S a' => Some (O, [], a') \| O => None end end.	L278	new
72	Lemma	`cw_app`	Lemma cw_app l1 l2: cw (l1 ++ l2) = cw l1 ++ cw l2.	L284	new
73	Lemma	`yLL_glue`	Lemma yLL_glue j: segLL tmf (D,[]) (D,[]) ([0;1;1]^^j) ([1;1;1]^^j).	L287	new
74	Lemma	`prefLL_glue`	Lemma prefLL_glue j ch: segLL tmf (D,[]) (D,[]) (cmid ch ++ bmid 0 j) ([1;1;1]^^j ++ cw ch ++ [0;1]).	L289	new
75	Lemma	`gen_RL`	Lemma gen_RL {ci co} (HF: segRL tmf hF hD ci co) c j ch: segRL tmf hB hD (pw (S c) j ch ++ ci) (pw c j ch ++ [0;1] ++ co).	L298	new
76	Lemma	`gen_RLg`	Lemma gen_RLg {ci co} (HF: segRL tmf hF hD ci co) j ch: segRL tmf hB hD (pw 0 j ch ++ ci) ([1;1;1]^^j ++ cw ch ++ [0;1] ++ co).	L304	new
77	Lemma	`lrcons1`	Lemma lrcons1 {w1 w2 m}: segRR tmf hB hB w1 m -> segLL tmf hD hD m w2 -> segRLs tmf h h w1 w2.	L310	new
78	Lemma	`gen_fwd`	Lemma gen_fwd {ci m co} (HR: segRR tmf hF hB ci m) (HL: segLL tmf hD hD m co) c j ch: segRLs tmf h h (pw (S c) j ch ++ ci) (pw c j ch ++ [0;1] ++ co).	L315	new
79	Lemma	`gen_fwdg`	Lemma gen_fwdg {ci m co} (HR: segRR tmf hF hB ci m) (HL: segLL tmf hD hD m co) j ch: segRLs tmf h h (pw 0 j ch ++ ci) ([1;1;1]^^j ++ cw ch ++ [0;1] ++ co).	L321	new
80	Lemma	`gen_side`	Lemma gen_side {ci co R R'} (HF: sideRL tmf hF hD (ci > R) (co > R')) c j ch: sideRL tmf hB hD ((pw (S c) j ch ++ ci) > R) ((pw c j ch ++ [0;1] ++ co) > R').	L327	new
81	Lemma	`gen_sideg`	Lemma gen_sideg {ci co R R'} (HF: sideRL tmf hF hD (ci > R) (co > R')) j ch: sideRL tmf hB hD ((pw 0 j ch ++ ci) > R) (([1;1;1]^^j ++ cw ch ++ [0;1] ++ co) > R').	L333	new
82	Lemma	`segRL_side`	Lemma segRL_side {t h1 h2 w w'} R: segRL t h1 h2 w w' -> sideRL t h1 h2 (w > R) (w' > R).	L339	new
83	Lemma	`cstopF`	Lemma cstopF a x far: exists co, segRL tmf hF hD (lead0 a (S x) ++ far) co /\ [0;1] ++ co = lead1 a x ++ far.	L348	new
84	Lemma	`t_stop`	Lemma t_stop bs a x far ov bs' a': consume bs a = Some (ov, bs', a') -> segRL tmf hB hD (uw bs false a (S x) far) ([1;1;1]^^ov ++ uw bs' true a' x far).	L354	new
85	Definition	`cpass_mid`	Definition cpass_mid a x := xbmid x ++ bmid a 1.	L365	new
86	Lemma	`cpassRR`	Lemma cpassRR a x: segRR tmf hF hB (lead1 a x ++ [1;1]) (cpass_mid a x).	L366	new
87	Definition	`cpass_co`	Definition cpass_co a x := ([0;1]^^a ++ [0;0] ++ [1;0;1]) ++ ([0] ++ [1;0]^^x ++ [1;1]).	L368	new
88	Lemma	`cpassLL`	Lemma cpassLL a x: segLL tmf hD hD (cpass_mid a x) (cpass_co a x).	L369	new
89	Lemma	`t_pass`	Lemma t_pass bs a x ov bs' a': consume bs (S a) = Some (ov, bs', a') -> segRLs tmf h h (uw bs true a x (tailw 0)) ([1;1;1]^^ov ++ uw bs' false a' (S (S x)) (tailw 0)).	L371	new
90	Definition	`um1`	Definition um1 a x : list Sym := [0;0;1;0;1;1;0;1;0;1] ++ [0;1]^^x ++ [1] ++ [0;1]^^a.	L381	new
91	Definition	`um2`	Definition um2 a x g : list Sym := [0;0;1;0;1;1;0;1;1;0;1] ++ [1;0;1]^^g ++ [0;1] ++ [0;1]^^x ++ [1] ++ [0;1]^^a.	L382	new
92	Definition	`uco1`	Definition uco1 a x : list Sym := [0;1]^^a ++ [1;1;1;0;1;0] ++ [1;0]^^x ++ [0;1;0;1;1].	L383	new
93	Definition	`uco2`	Definition uco2 a x g : list Sym := [0;1]^^a ++ [1;1;1;0;1] ++ [0;1]^^x ++ [1;1;1] ++ [1;1;1]^^g ++ [0;0;1;0;1;1].	L384	new
94	Lemma	`u1RF`	Lemma u1RF a x: segRR tmf hF hB (lead1 a x ++ tailw 1) (um1 a x).	L385	new
95	Lemma	`u1RB`	Lemma u1RB a x: segRR tmf hB hB (lead1 a x ++ tailw 1) (um1 a x).	L387	new
96	Lemma	`u1L`	Lemma u1L a x: segLL tmf hD hD (um1 a x) (uco1 a x).	L389	new
97	Lemma	`u2RF`	Lemma u2RF a x g: segRR tmf hF hB (lead1 a x ++ tailw (S (S g))) (um2 a x g).	L391	new
98	Lemma	`u2RB`	Lemma u2RB a x g: segRR tmf hB hB (lead1 a x ++ tailw (S (S g))) (um2 a x g).	L393	new
99	Lemma	`u2L`	Lemma u2L a x g: segLL tmf hD hD (um2 a x g) (uco2 a x g).	L395	new
100	Lemma	`t_ungl1`	Lemma t_ungl1 bs a x ov bs' a': consume (bs ++ [(a,1%nat)]) (S x) = Some (ov, bs', a') -> segRLs tmf h h (uw bs true a x (tailw 1)) ([1;1;1]^^ov ++ uw bs' false a' 1 (tailw 0)).	L398	new
101	Lemma	`t_ungl2`	Lemma t_ungl2 bs a x g ov bs' a': consume (bs ++ [(a,1%nat);(x,S g)]) 0%nat = Some (ov, bs', a') -> segRLs tmf h h (uw bs true a x (tailw (S (S g)))) ([1;1;1]^^ov ++ uw bs' false a' 1 (tailw 0)).	L410	new
102	Lemma	`t_halt`	Lemma t_halt x far l r: halts tmf (l {{B}}> uw [] false 0 x far *> r).	L424	new
103	Definition	`edge1w`	Definition edge1w f : list Sym := [1] ++ [1;1;1]^^f.	L428	new
104	Lemma	`z_lead`	Lemma z_lead bs x f ov bs' a': bs <> [] -> consume bs 0%nat = Some (ov, bs', a') -> sideRL tmf hB hD ((cw bs ++ edgew x f) > const 0) (([1;1;1]^^ov ++ cw bs' ++ edgew x (S f)) > const 0).	L429	new
105	Lemma	`z_empty`	Lemma z_empty y f: sideRL tmf hB hD (edgew (S y) f > const 0) (edgew y (S f) > const 0).	L440	new
106	Lemma	`z_absorb`	Lemma z_absorb f: sideRL tmf hB hD (edgew 0 (S f) > const 0) (([1;1] ++ [1;1;1]^^(S f)) > const 0).	L442	new
107	Lemma	`z_stop`	Lemma z_stop bs a x f ov bs' a': consume bs a = Some (ov, bs', a') -> sideRL tmf hB hD (uw bs false a (S x) (edge1w f) > const 0) (([1;1;1]^^ov ++ uw bs' true a' x (edge1w f)) > const 0).	L444	new
108	Definition	`zco`	Definition zco a x f : list Sym := [0;1]^^a ++ [1;1;1;0;1] ++ [0;1]^^x ++ [1;1;1]^^f ++ [0;1;1;1].	L447	new
109	Lemma	`z1F`	Lemma z1F a x f: sideRL tmf hF hD ((lead1 a x ++ edge1w f) > const 0) (zco a x f > const 0).	L448	new
110	Lemma	`z1B`	Lemma z1B a x f: sideRL tmf hB hD ((lead1 a x ++ edge1w f) > const 0) (zco a x f > const 0).	L450	new
111	Lemma	`z_1111`	Lemma z_1111 bs a x f ov bs' a': consume (bs ++ [(a,1%nat);(x,f)]) 0%nat = Some (ov, bs', a') -> sideRL tmf hB hD (uw bs true a x (edge1w f) > const 0) (([1;1;1]^^ov ++ cw bs' ++ edgew 0 1) > const 0).	L452	new
112	Definition	`NT`	Definition NT s g (X:side) : Q * tape := const 0 <{{A}} ([1;0]^^s ++ [1] ++ [0;0] ++ [1;0] ++ tailw g) *> X.	L466	new
113	Definition	`rmid`	Definition rmid t : list Sym := [0;0;1;0;1;1;0;1;0] ++ [1;0]^^t.	L467	new
114	Lemma	`reset1_in`	Lemma reset1_in t X: root t ([1;1;1] > X) --> rmid t *> const 0 {{B}}> X.	L468	new
115	Lemma	`reset1_out`	Lemma reset1_out t X: rmid t > const 0 <{{D}} X --> NT (S t) 0 X.	L470	new
116	Lemma	`reset1`	Lemma reset1 t X X': sideRL tmf hB hD X X' -> root t ([1;1;1] > X) --> NT (S t) 0 X'.	L472	new
117	Lemma	`reset1_halt`	Lemma reset1_halt t X: sideRLs_halt tmf h X -> halts tmf (root t ([1;1;1] *> X)).	L478	new
118	Lemma	`reset2`	Lemma reset2 s g X: NT (S s) g X -->* root 0 ((lead1 s 0 ++ tailw g) *> X).	L480	new
119	Definition	`cvp`	Definition cvp (p:NN) : natnat := (N.to_nat (fst p), N.to_nat (snd p)).	L484	new
120	Definition	`cvl`	Definition cvl (bs:list (N*N)) := map cvp bs.	L485	new
121	Record	`unitN`	Record unitN := UN { ubs : list (N*N); ubit : bool; ua : N; ux : N; ug : N }.	L486	new
122	Definition	`uwN`	Definition uwN u := uw (cvl (ubs u)) (ubit u) (N.to_nat (ua u)) (N.to_nat (ux u)) (tailw (N.to_nat (ug u))).	L487	new
123	Fixpoint	`dwords`	Fixpoint dwords (us:list unitN) : list Sym := match us with [] => [] \| u::us => uwN u ++ dwords us end.	L488	new
124	Inductive	`zN`	Inductive zN := Z0 (bs:list (NN)) (x f:N) \| ZD (bs:list (NN)) (b:bool) (a x f:N).	L489	new
125	Definition	`zside`	Definition zside z : side := match z with \| Z0 bs x f => (cw (cvl bs) ++ edgew (N.to_nat x) (N.to_nat f)) > const 0 \| ZD bs b a x f => uw (cvl bs) b (N.to_nat a) (N.to_nat x) (edge1w (N.to_nat f)) > const 0 end.	L490	new
126	Inductive	`tailN`	Inductive tailN := TT (t g:N) \| NTl (s g:N).	L493	new
127	Record	`cfg`	Record cfg := Cfg { ctl : tailN; cus : list unitN; cz : zN }.	L494	new
128	Definition	`denote`	Definition denote c : Q * tape := match ctl c with \| TT t g => root (N.to_nat t) (([1;1;1]^^(N.to_nat g) ++ dwords (cus c)) > zside (cz c)) \| NTl s g => NT (N.to_nat s) (N.to_nat g) (dwords (cus c) > zside (cz c)) end.	L495	adapted
129	Definition	`consumeN`	Definition consumeN (bs:list (NN)) (a:N) : option (N list (NN) N) := match bs with \| (c, j) :: r => if N.eqb c 0 then Some (j, r, a) else Some (0%N, (N.pred c, j)::r, a) \| [] => if N.eqb a 0 then None else Some (0%N, [], N.pred a) end.	L499	new
130	Lemma	`consumeN_spec`	Lemma consumeN_spec bs a ov bs' a': consumeN bs a = Some (ov, bs', a') -> consume (cvl bs) (N.to_nat a) = Some (N.to_nat ov, cvl bs', N.to_nat a').	L504	new
131	Lemma	`cvl_app`	Lemma cvl_app l1 l2: cvl (l1 ++ l2) = cvl l1 ++ cvl l2.	L515	new
132	Inductive	`tres`	Inductive tres := TStop (ov:N) (u:unitN) \| TPass (ov:N) (u:unitN) \| THalt \| TFail.	L519	new
133	Definition	`touchN`	Definition touchN u : tres := if ubit u then if N.eqb (ug u) 0 then match consumeN (ubs u) (N.succ (ua u)) with Some (ov,bs',a') => TPass ov (UN bs' false a' (ux u + 2) 0) \| None => TFail end else if N.eqb (ug u) 1 then match consumeN (ubs u ++ [(ua u, 1%N)]) (N.succ (ux u)) with Some (ov,bs',a') => TPass ov (UN bs' false a' 1 0) \| None => TFail end … +8 lines	L520	new
134	Lemma	`touchN_stop`	Lemma touchN_stop u ov u': touchN u = TStop ov u' -> segRL tmf hB hD (uwN u) ([1;1;1]^^(N.to_nat ov) ++ uwN u').	L537	new
135	Lemma	`touchN_pass`	Lemma touchN_pass u ov u': touchN u = TPass ov u' -> segRLs tmf h h (uwN u) ([1;1;1]^^(N.to_nat ov) ++ uwN u') /\ ug u' = 0%N.	L552	new
136	Lemma	`touchN_halt`	Lemma touchN_halt u: touchN u = THalt -> forall l r, halts tmf (l {{B}}> uwN u *> r).	L578	new
137	Inductive	`zres`	Inductive zres := ZRet (ov:N) (z:zN) \| ZAbs (f:N) \| ZFail.	L592	new
138	Definition	`ztouch`	Definition ztouch z : zres := match z with \| Z0 [] y f => if N.eqb y 0 then (if N.eqb f 0 then ZFail else ZAbs f) else ZRet 0%N (Z0 [] (N.pred y) (N.succ f)) \| Z0 bs x f => match consumeN bs 0%N with Some (ov,bs',_) => ZRet ov (Z0 bs' x (N.succ f)) \| None => ZFail end \| ZD bs false a x f => if N.eqb x 0 then ZFail else match consumeN bs a with Some (ov,bs',a') => ZRet ov (ZD bs' true a' (N.pred x) f) \| None => ZFail end \| ZD bs true a x f => match consumeN (bs ++ [(a,1%N);(x,f)]) 0%N with Some (ov,bs',_) => ZRet ov (Z0 bs' 0 1) \| None => ZFail end … +1 lines	L593	new
139	Lemma	`ztouch_ret`	Lemma ztouch_ret z ov z': ztouch z = ZRet ov z' -> sideRL tmf hB hD (zside z) ([1;1;1]^^(N.to_nat ov) *> zside z').	L600	new
140	Lemma	`ztouch_abs`	Lemma ztouch_abs z f: ztouch z = ZAbs f -> sideRL tmf hB hD (zside z) (([1;1] ++ [1;1;1]^^(N.to_nat f)) *> const 0).	L620	new
141	Inductive	`cres`	Inductive cres := CRet (ov:N) (us:list unitN) (z:zN) \| CHalt \| CFail.	L632	new
142	Definition	`setg`	Definition setg u g := UN (ubs u) (ubit u) (ua u) (ux u) g.	L633	new
143	Fixpoint	`callN`	Fixpoint callN (us:list unitN) (z:zN) : cres := match us with \| [] => match ztouch z with ZRet ov z' => CRet ov [] z' \| _ => CFail end \| u :: us1 => match touchN u with \| TStop ov u' => CRet ov (u' :: us1) z \| THalt => CHalt \| TFail => CFail … +11 lines	L634	new
144	Lemma	`side1`	Lemma side1 {w w' r r'}: segRLs tmf h h w w' -> sideRL tmf hB hD r r' -> sideRL tmf hB hD (w > r) (w' > r').	L652	new
145	Lemma	`setg_word`	Lemma setg_word u g: ug u = 0%N -> uwN u ++ [1;1;1]^^(N.to_nat g) = uwN (setg u g).	L658	new
146	Lemma	`abs_word`	Lemma abs_word u f: ug u = 0%N -> uwN u ++ [1;1] ++ [1;1;1]^^(N.to_nat f) = uw (cvl (ubs u)) (ubit u) (N.to_nat (ua u)) (N.to_nat (ux u)) (edge1w (N.to_nat (ug u + f + 1))).	L660	new
147	Lemma	`callN_ret`	Lemma callN_ret us: forall z ov us' z', callN us z = CRet ov us' z' -> sideRL tmf hB hD (dwords us > zside z) (([1;1;1]^^(N.to_nat ov) ++ dwords us') > zside z').	L667	new
148	Lemma	`callN_halt`	Lemma callN_halt us: forall z, callN us z = CHalt -> sideRLs_halt tmf h (dwords us *> zside z).	L691	new
149	Inductive	`ires`	Inductive ires := IOk (c:cfg) \| IHalt \| IFail.	L706	new
150	Definition	`inc1`	Definition inc1 c : ires := match ctl c with \| TT t g => if N.eqb g 0 then match callN (cus c) (cz c) with \| CRet ov us' z' => IOk (Cfg (TT (N.succ t) ov) us' z') \| CHalt => IHalt \| CFail => IFail end else if N.eqb g 1 then match callN (cus c) (cz c) with \| CRet ov us' z' => IOk (Cfg (NTl (N.succ t) ov) us' z') \| CHalt => IHalt \| CFail => IFail end … +3 lines	L707	adapted
151	Lemma	`inc1_ok`	Lemma inc1_ok c c': inc1 c = IOk c' -> denote c -->* denote c'.	L716	new
152	Lemma	`inc1_halt`	Lemma inc1_halt c: inc1 c = IHalt -> halts tmf (denote c).	L738	new
153	Lemma	`stop1s`	Lemma stop1s {bs a x far ov bs' a'}: consume bs a = Some (ov, bs', a') -> segRLs tmf h [] (uw bs false a (S x) far) ([1;1;1]^^ov ++ uw bs' true a' x far).	L753	new
154	Lemma	`pairK`	Lemma pairK q: forall c j r a x, segRLs tmf (h^^(q2)) (h^^q) (uw ((q2+c, j)::r) false a (S x) (tailw 0)) (uw ((c,j)::r) false (q+a) (S (q+x)) (tailw 0)).	L756	new
155	Lemma	`pair1`	Lemma pair1 q: forall a x, segRLs tmf (h^^(q*2)) (h^^q) (uw [] false (q+a) (S x) (tailw 0)) (uw [] false a (S (q+x)) (tailw 0)).	L767	new
156	Definition	`b2n`	Definition b2n (b:bool) : nat := if b then 1 else 0.	L778	new
157	Lemma	`clK0`	Lemma clK0 q rb c j r a x: segRLs tmf (h^^(q2 + b2n rb)) (h^^q) (uw ((q2 + b2n rb + c, j)::r) false a (S x) (tailw 0)) (uw ((c,j)::r) rb (q+a) (q + S x - b2n rb) (tailw 0)).	L779	new
158	Lemma	`clK1`	Lemma clK1 q rb c j r a x: segRLs tmf (h^^(S (q2 + b2n rb))) (h^^(S q)) (uw ((S (q2 + b2n rb + c), j)::r) true a x (tailw 0)) (uw ((c,j)::r) rb (q + S a) (q + S (S x) - b2n rb) (tailw 0)).	L789	new
159	Lemma	`cl10`	Lemma cl10 q rb a x: segRLs tmf (h^^(q*2 + b2n rb)) (h^^q) (uw [] false (q + b2n rb + a) (S x) (tailw 0)) (uw [] rb a (q + S x - b2n rb) (tailw 0)).	L796	new
160	Lemma	`cl11`	Lemma cl11 q rb a x: segRLs tmf (h^^(S (q*2 + b2n rb))) (h^^(S q)) (uw [] true (q + b2n rb + a) x (tailw 0)) (uw [] rb a (q + S (S x) - b2n rb) (tailw 0)).	L806	new
161	Definition	`b2N`	Definition b2N (b:bool) : N := if b then 1%N else 0%N.	L814	new
162	Lemma	`b2N_nat`	Lemma b2N_nat b: N.to_nat (b2N b) = b2n b.	L815	new
163	Lemma	`div2_nat`	Lemma div2_nat n: N.to_nat n = N.to_nat (N.div2 n) * 2 + b2n (N.odd n).	L817	new
164	Definition	`closedU`	Definition closedU (n:N) (u:unitN) : option (unitN * N) := if N.eqb n 0 then Some (u, 0%N) else match ubs u with \| (c,j)::r => if negb (ubit u) then if N.eqb n 1 then … +22 lines	L820	new
165	Lemma	`closedU_spec`	Lemma closedU_spec n u u' p: closedU n u = Some (u', p) -> segRLs tmf (h^^(N.to_nat n)) (h^^(N.to_nat p)) (uwN u) (uwN u').	L859	new
166	Lemma	`zLs`	Lemma zLs m: forall c j r x f, sideRLs tmf (h^^m) ((cw ((m+c,j)::r) ++ edgew x f) > const 0) ((cw ((c,j)::r) ++ edgew x (m+f)) > const 0).	L904	new
167	Lemma	`zEs`	Lemma zEs m: forall y f, sideRLs tmf (h^^m) (edgew (m+y) f > const 0) (edgew y (m+f) > const 0).	L913	new
168	Definition	`closedZ`	Definition closedZ (m:N) (z:zN) : option zN := if N.eqb m 0 then Some z else match z with \| Z0 [] y f => if N.ltb y m then None else Some (Z0 [] (y - m) (f + m)) \| Z0 ((c,j)::r) x f => if N.ltb c m then None else Some (Z0 (((c - m)%N, j)::r) x (f + m)) \| ZD _ _ _ _ _ => None … +1 lines	L920	new
169	Lemma	`closedZ_spec`	Lemma closedZ_spec m z z': closedZ m z = Some z' -> sideRLs tmf (h^^(N.to_nat m)) (zside z) (zside z').	L927	new
170	Fixpoint	`batchL`	Fixpoint batchL (n:N) (us:list unitN) (z:zN) : option (list unitN * zN) := match us with \| [] => match closedZ n z with Some z' => Some ([], z') \| None => None end \| u :: us => match closedU n u with \| Some (u', p) => match batchL p us z with Some (us', z') => Some (u' :: us', z') \| None => None end \| None => None end end.	L943	new
171	Lemma	`batchL_spec`	Lemma batchL_spec us: forall n z us' z', batchL n us z = Some (us', z') -> sideRLs tmf (h^^(N.to_nat n)) (dwords us > zside z) (dwords us' > zside z').	L948	new
172	Definition	`evt_unit`	Definition evt_unit (u:unitN) : N := let own := match ubs u with (c,_)::_ => N.succ c \| [] => (2 * ua u + b2N (ubit u))%N end in let own := if negb (ubit u) && N.eqb (ux u) 0 then 1%N else own in if N.eqb (ug u) 0 then own else N.min own (if ubit u then 1%N else 2%N).	L960	new
173	Definition	`evt_z`	Definition evt_z z : N := match z with Z0 [] y _ => N.succ y \| Z0 ((c,_)::_) _ _ => N.succ c \| ZD _ _ _ _ _ => 1%N end.	L964	new
174	Definition	`first_inc`	Definition first_inc (C q n : N) : N := (n * 2^q - C mod 2^q)%N.	L965	new
175	Fixpoint	`cval`	Fixpoint cval (us:list unitN) (i:N) : N := match us with \| [] => 0%N \| u :: us => ((if ubit u then 2^i else 0) + cval us (N.succ i))%N end.	L966	new
176	Fixpoint	`pmin`	Fixpoint pmin (us:list unitN) (i C:N) (z:zN) : N := match us with \| [] => first_inc C i (evt_z z) \| u :: us => N.min (first_inc C i (evt_unit u)) (pmin us (N.succ i) C z) end.	L968	new
177	Definition	`propose`	Definition propose (us:list unitN) (z:zN) : N := N.pred (pmin us 0 (cval us 0) z).	L971	adapted
178	Definition	`batch_step`	Definition batch_step c : option cfg := match ctl c with \| TT t g => if N.eqb g 0 then let d := propose (cus c) (cz c) in if N.eqb d 0 then None else match batchL d (cus c) (cz c) with Some (us', z') => Some (Cfg (TT (t + d) 0) us' z') \| None => None end else None … +1 lines	L974	adapted
179	Lemma	`batch_step_spec`	Lemma batch_step_spec c c': batch_step c = Some c' -> denote c -->* denote c'.	L981	new
180	Definition	`next`	Definition next c : cfg + unit := match batch_step c with \| Some c' => inl c' \| None => match inc1 c with IOk c' => inl c' \| IHalt => inr tt \| IFail => inl c end end.	L991	adapted
181	Lemma	`next_spec`	Lemma next_spec c: match next c with inl c' => denote c -->* denote c' \| inr _ => halts tmf (denote c) end.	L994	new
182	Definition	`c342`	Definition c342 := Cfg (NTl 1 1) [] (Z0 [(0%N,3%N)] 0 1).	L1002	new
183	Definition	`check`	Definition check fuel := match N_iter_until next (inl c342) fuel with inl _ => false \| inr _ => true end.	L1003	adapted
184	Theorem	`check_spec`	Theorem check_spec fuel: check fuel = true -> halts tmf (denote c342).	L1004	adapted
185	Definition	`run`	Definition run (T:N) (c:cfg) : cfg + unit := N_iter_until next (inl c) T.	L1020	new
186	Definition	`unl`	Definition unl (x:cfg + unit) : cfg := match x with inl c => c \| inr _ => c342 end.	L1021	new
187	Lemma	`run_ok`	Lemma run_ok T c c': run T c = inl c' -> denote c -->* denote c'.	L1022	new
188	Lemma	`run_halt`	Lemma run_halt T c: run T c = inr tt -> halts tmf (denote c).	L1033	new
189	Definition	`k1`	Definition k1 := Eval vm_compute in unl (run 5000 c342).	L1045	new
190	Lemma	`s1`	Lemma s1: run 5000 c342 = inl k1.	L1046	new
191	Definition	`k2`	Definition k2 := Eval vm_compute in unl (run 5000 k1).	L1047	new
192	Lemma	`s2`	Lemma s2: run 5000 k1 = inl k2.	L1048	new
193	Definition	`k3`	Definition k3 := Eval vm_compute in unl (run 5000 k2).	L1049	new
194	Lemma	`s3`	Lemma s3: run 5000 k2 = inl k3.	L1050	new
195	Definition	`k4`	Definition k4 := Eval vm_compute in unl (run 5000 k3).	L1051	new
196	Lemma	`s4`	Lemma s4: run 5000 k3 = inl k4.	L1052	new
197	Definition	`k5`	Definition k5 := Eval vm_compute in unl (run 5000 k4).	L1053	new
198	Lemma	`s5`	Lemma s5: run 5000 k4 = inl k5.	L1054	new
199	Definition	`k6`	Definition k6 := Eval vm_compute in unl (run 5000 k5).	L1055	new
200	Lemma	`s6`	Lemma s6: run 5000 k5 = inl k6.	L1056	new
201	Definition	`k7`	Definition k7 := Eval vm_compute in unl (run 5000 k6).	L1057	new
202	Lemma	`s7`	Lemma s7: run 5000 k6 = inl k7.	L1058	new
203	Definition	`k8`	Definition k8 := Eval vm_compute in unl (run 5000 k7).	L1059	new
204	Lemma	`s8`	Lemma s8: run 5000 k7 = inl k8.	L1060	new
205	Definition	`k9`	Definition k9 := Eval vm_compute in unl (run 5000 k8).	L1061	new
206	Lemma	`s9`	Lemma s9: run 5000 k8 = inl k9.	L1062	new
207	Definition	`k10`	Definition k10 := Eval vm_compute in unl (run 5000 k9).	L1063	new
208	Lemma	`s10`	Lemma s10: run 5000 k9 = inl k10.	L1064	new
209	Definition	`k11`	Definition k11 := Eval vm_compute in unl (run 5000 k10).	L1065	new
210	Lemma	`s11`	Lemma s11: run 5000 k10 = inl k11.	L1066	new
211	Definition	`k12`	Definition k12 := Eval vm_compute in unl (run 5000 k11).	L1067	new
212	Lemma	`s12`	Lemma s12: run 5000 k11 = inl k12.	L1068	new
213	Definition	`k13`	Definition k13 := Eval vm_compute in unl (run 5000 k12).	L1069	new
214	Lemma	`s13`	Lemma s13: run 5000 k12 = inl k13.	L1070	new
215	Definition	`k14`	Definition k14 := Eval vm_compute in unl (run 5000 k13).	L1071	new
216	Lemma	`s14`	Lemma s14: run 5000 k13 = inl k14.	L1072	new
217	Definition	`k15`	Definition k15 := Eval vm_compute in unl (run 5000 k14).	L1073	new
218	Lemma	`s15`	Lemma s15: run 5000 k14 = inl k15.	L1074	new
219	Definition	`k16`	Definition k16 := Eval vm_compute in unl (run 5000 k15).	L1075	new
220	Lemma	`s16`	Lemma s16: run 5000 k15 = inl k16.	L1076	new
221	Definition	`k17`	Definition k17 := Eval vm_compute in unl (run 5000 k16).	L1077	new
222	Lemma	`s17`	Lemma s17: run 5000 k16 = inl k17.	L1078	new
223	Definition	`k18`	Definition k18 := Eval vm_compute in unl (run 5000 k17).	L1079	new
224	Lemma	`s18`	Lemma s18: run 5000 k17 = inl k18.	L1080	new
225	Definition	`k19`	Definition k19 := Eval vm_compute in unl (run 5000 k18).	L1081	new
226	Lemma	`s19`	Lemma s19: run 5000 k18 = inl k19.	L1082	new
227	Definition	`k20`	Definition k20 := Eval vm_compute in unl (run 5000 k19).	L1083	new
228	Lemma	`s20`	Lemma s20: run 5000 k19 = inl k20.	L1084	new
229	Definition	`k21`	Definition k21 := Eval vm_compute in unl (run 5000 k20).	L1085	new
230	Lemma	`s21`	Lemma s21: run 5000 k20 = inl k21.	L1086	new
231	Lemma	`s22`	Lemma s22: run 5000 k21 = inr tt.	L1087	new
232	Lemma	`init`	Lemma init: c0 -[tmf]->* denote c342.	L1088	adapted
233	Lemma	`halt_tmf`	Lemma halt_tmf: halts tmf c0.	L1090	new
234	Lemma	`halt`	Lemma halt: halts tm c0.	L1117	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
proof.md (working copy) · differs from the submitted copy

submission/proof.md line 134: 3. The rules

An increment is one carry. It enters at the right end and moves left one unit at a time. Each unit it reaches is touched: it changes as below and either stops the carry or passes it on to the left.

3.1 Stop and pass

In every touch of a digit, all of its passive stacks move two cells to the right and the right end of its lead moves one cell to the right. The lead flips.

touch	when	change	the carry
stop	lead `00`, x ≥ 2	lead becomes `1111`, x decreases by 1	stops
pass	lead `1111`, left boundary `11`	lead becomes `00`, x increases by 3	goes on to the left
halt	single-marker, lead `00`, y = 0	the machine halts (§3.6)	—

The fuel changes the same way in a stop and in a pass:

digit	change
single-marker	y decreases by 1
multi-marker	m_1 increases by 1, y decreases by 2 (glue when y = 1, §3.2)

The inner gaps m_2, …, m_r do not change.

3.2 Glue

A multi-marker digit touched with y = 1 would get y = −1. Instead its last stack runs into the boundary on its right:

… m_r  1^(3j+1)  [1]  1^(3g+2) …    ->    … m_r  1^(3(g+j)+2) …

The digit loses its last stack Q_r = 1^(3j+1), and the boundary to its right now carries g + j glued walls.

The digit's new fuel is the gap that was left of the lost stack, as it stands after the touch: m_r if r ≥ 2 (the touch leaves it unchanged), and m_1 + 1 if r = 1 (the touch adds 1 to m_1).

3.3 Unglue

A digit with lead 1111 whose left boundary carries g ≥ 1 glued walls is not passed as in §3.1. The glued walls came from the left neighbour, and now they enter this digit:

1^5      [x, 1111, m_1, Q_1, …, y]   ->   11 [2, 00, x+1, 1111, m_1, Q_1, …, y−2]
1^(3g+2) [x, 1111, m_1, Q_1, …, y]   ->   11 [2, 00, 0, 1^(3g−2), x, 1111, m_1, Q_1, …, y−2]     (g ≥ 2)

The first glued wall becomes the new lead. It has just been passed, so it is 00.
For g ≥ 2 the other g − 1 glued walls follow as one stack.
The old lead 1111 becomes a passive wall.
The boundary is plain 11 again, and the carry goes on to the left.

For a single-marker digit the part m_1, Q_1, … is empty, so [x, 1111, y] becomes [2, 00, x+1, 1111, y−2]. As always, y − 2 = −1 means a glue instead (§3.2).

3.4 The unit next to the edge

An increment whose carry passes every digit U_1, …, U_n is an overflow; it touches U_0.

U_0	edge	effect
leadless `[x, Q_1, …, y]`	e ≡ 0	e grows by 3; y decreases by 2, or glue when y = 1; x and the inner gaps stay
empty `[y]`, y ≥ 3	e ≡ 0	e grows by 3; y decreases by 2
empty `[1]`	e ≡ 0	absorption: the edge and b_1 = `11` merge into a new edge `1^(e+4)`; U_1 becomes U_0
a digit, lead `00`	e ≡ 1	a stop, as in §3.1
a digit, lead `1111`	e ≡ 1	fossilization, below

Fossilization. The old edge becomes a passive stack, the old lead becomes a passive wall, and a new edge 111 starts at the left end:

1^e [x, 1111, m_1, Q_1, …, y]   ->   111 [1, 1^e, x, 1111, m_1, Q_1, …, y−2]        (e ≡ 1 mod 3)

U_0 is then leadless and the edge is ≡ 0 again. The stacks left behind by the fossilizations form the far left part of the tape.

3.5 Tail and resets

Every increment adds 2 to the tail: t becomes t + 2.

A reset takes two increments. It starts when the least significant digit has glued its last stack onto the tail boundary, so that b_T = 1^5:

… 1^5 [t] A>          ->   … 11 [2, 00, t+2] A>                   (first increment)
… b [2, 00, y] A>     ->   … b [1, 1111, y−2] 11 [1] A>           (second increment)

In the first increment the old tail becomes the fuel of a new least significant digit. Its lead is the glued wall, already passed, so the carry goes on into the digits to the left.
In the second increment the new digit stops the carry at once, and a new tail [1] appears.
The boundary b left of the new digit is 11, unless the carry of the first increment glued walls onto it.

The configuration at step 342 is the state between the two increments of a reset, with b = 1^5.

3.6 The halt

A carry that touches a single-marker digit [x, 00, 0] halts the machine. There the tape reads

… 00 11 …

the lead 00 followed at once by the digit's right boundary. By §1 this is the halting pattern: the head reaches the left 1 of 11 in state F, with 0 0 to its left.

3.7 What the rules exclude

No rule covers these shapes:

a stop with x = 0;
a tail boundary with two or more glued walls;
an absorption when there is no digit left to become U_0;
the halting shape [x, 00, 0] in U_0.

If the run ever reached such a shape, the checker of §8 would stall and never report the halt. It does report it, so these shapes never occur on the run.

The edge class always matches U_0: an absorption leaves a U_0 digit with e ≡ 1, a fossilization leaves a leadless U_0 with e ≡ 0, and edge growth keeps e mod 3.

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

No related machine found (no parent link, table twin, follow-on row or mention).

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 587 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
1 assumption(s); tools/assumptions_baseline.txt allows only functional_extensionality_dep
✓
coqchk finished (optional)
coqchk pass in 536.46 s
✓
.v hash matches the checked hash
.v = checked sha256 198b30225e7c…; submission/ copy = checked sha256 198b30225e7c…
✓
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 L564: - Checkpoint B is pending (non-blocking); there are no notes to fold in yet. Nothing posted.
- proof.md L527: - Checkpoint B is pending (non-blocking); there are no notes to fold in yet.
○
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 halts” (above), which quotes how_proved.md. Re-run: python3 -B tools/killreview.py 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB

Files

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

name	size	changed
notes.md ↓	40 KB	2026-10-12 20:47
proof.md ↓	27 KB	2026-10-12 21:04
how_proved.md ↓	1.6 KB	2026-10-14 10:51
status.json ↓	1.7 KB	2026-10-14 09:08
observe.json ↓	9.2 KB	2026-10-12 15:25
1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v ↓	64 KB	2026-10-13 10:20
img/	6 items	2026-10-12 14:50
rocq/	11 items	2026-10-13 10:49
submission/	5 items	2026-10-13 09:12
work/	67 items	2026-10-12 17:25
rocq-plan.md ↓	17 KB	2026-10-12 17:50

status.json in full

{
 "tm": "1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB",
 "label": "C2-552",
 "status": "KILLED_HALT",
 "stage": "done",
 "updated": "2026-10-13",
 "reason": "check_kill --halt PASS, independently re-verified",
 "halt_steps": {
  "exact": "176522930997643289094015905898381767890130463",
  "approx": "1.765e44",
  "convention": "steps including the halting transition (tools/sim convention); busycoq halts_in n = exact - 1",
  "busycoq_halts_in_n": "176522930997643289094015905898381767890130462",
  "proven_in_coq": false,
  "basis": "computed from per-rule step formulas summed over the same run (work/steps_exact/, exact_steps.json); formulas exact on all 276,427 increments to 1e11 and on all 53,973 single-stepped increments (reduced tapes); the .v proves halts tm c0 only",
  "lower_bound": "87364406466050439442427007228199699615332500",
  "halting_increment_after_step342": "11631266794472450654093",
  "resets_before_halt": 82
 },
 "check_kill": {
  "result": "PASS",
  "mode": "halt",
  "sha256": "198b30225e7ccff843808791746c4351a52277da10691ee5791a1cf205712805",
  "compile_s": 70.0,
  "coqchk_s": 536.5,
  "coqchk_cap_s": 600,
  "assumptions": [
   "functional_extensionality_dep"
  ],
  "log": "submission/check_kill.txt",
  "checked_at": "2026-10-13T17:33:35Z",
  "raw": [
   "rocq/check_kill_2026-10-13_fix1.out"
  ]
 },
 "funded": {
  "option": "class2_closeout",
  "date": "2026-10-12"
 },
 "pr": "https://github.com/ccz181078/busycoq/pull/18",
 "pr_state": "merged",
 "pr_comments": 0,
 "posted": "2026-10-13 (bbchallenge Discord, by Dennis)",
 "pr_file": "verify/Skelet1LikeC2Halt_1RB0RD_1LC0RA.v",
 "pr_merged_at": "2026-10-14T06:20:40Z",
 "pr_merged_by": "ccz181078",
 "pr_merge_commit": "cdaf693"
}

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