Built . It shows the files as they were then (ages and “working now” follow your clock). tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.

Machines / W5-1

`1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---`

W5-1local proof 23Claimed by someone elseBell eats counterbbchallenge ↗Explorer

How we proved it never halts

W4-2's proof in a mirror, with a three-step detour

W4-2 keeps a binary counter on one side of the head and two runs of 10 pairs on the other, fuel and spent. Each bounce adds 1 to the counter and moves one pair from fuel to spent; when the fuel is gone, the pairs bite off the counter's low end and a longer round starts. This machine does the same in a mirror: left of the head are the spent pairs, a gap, the fuel pairs and a single 1 (01 01 … 01 0 01 01 … 01 1), and right of it is the counter.

Mirrored and renamed, this table is W4-2's with one entry changed. In one of W4-2's two ways of stepping over a 1 while scanning the counter, this machine takes three steps instead (one back, two forward) and ends in the same place with the same tape and state. The detour needs a 1 behind the head, and one is always there, because the state that makes the detour is only entered by a step that writes that 1.

So W4-2's arithmetic carries over unchanged, including its key size bound: at every bite on a tidy counter, the counter's value is between one and about 2.5 times the length of the round just finished. New is the start: this machine acts like the mirrored table started in another state, and at step 73 it reaches such a bite inside the bound. From there W4-2's induction runs forever and never reaches the missing entry.

The Rocq proof copies W4-2's arithmetic word for word, re-proves the low-level moves on the mirrored table with the detour, and runs the 73-step opening directly; busycoq's mirror and renaming theorems carry the result over to this machine.

#23local proof number

1,278lines of Rocq

64 sto compile

6/6automatic checks

Claimed by someone else

We proved this machine locally, but our proof was still unsubmitted when we found it already covered upstream.

Submit completed proofs early. A local proof does not secure an upstream claim.

Upstream proof ↗ · Recorded timeline

What the timing evidence establishes

This describes upstream credit, not who first discovered the mathematics. The records do not establish adoption of our proof, first public push time, or whether an earlier submission would have secured credit.

Overview

In one sentence

W4-2 in a mirror, started in F, with F1 stretched into a 3-step detour; W4-2's rules and invariant cover it.

Submitted mechanism A mirrored Bell-eats-counter. On TP's side the tape is 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf. Each bounce applies one map phi to the left word w (two interleaved binary numbers, even and odd cells) and moves one 10 from the n-block to the m-block. At n = 0 the right side eats the low end of w and refills n. (submission/README.md, Mechanism)

Upstream: The blank-start machine never halts: BECv10.v.TM11 ↗. We also have a local proof. This upstream addition is separate from our merged submissions; adoption credit is not established. Recorded commit time: 2026-10-13T13:42:06Z. First public push time is not established.
Rocq proof: check_kill PASS · first Oct 13 02:13
1,278 lines · 50 KB .v · compile 64.1 s · coqchk pass · 0 axioms · PASS Oct 13 02:13
· the .v file
Automatic review: 6 of 6 checks passtemplate: verify/BECv5.v Module TM1 (adapted from) · details in Proof →
Class: Bell eats counterours: Bell eats counter (sheet) · ours adds: W4-2's counter (BECv5 family) in a mirror, started in W4-2's F; F1 = 1RC is a 3-step detour of W4-2's F1 = 1LF · high confidence
On the list: not on BB6_holdouts_663.txt (line 349 of the previous list) · historical 740 line 349
eqv ×2sim 1e15

Mechanism

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

How it works: 3 notes

349 = W4-2's table with F1 = 1RC (W4-2: 1LF), mirrored and renamed (F->A, A->B, ..., E->F); its blank run is W4-2's table started in F.
Only A1 enters F, so F always has a 1 on its right: F1 C1 A1 (3 steps) does what W4-2's F1 does in 1 (in 349's letters: 1 A> 1 -> A1 D1 B1 -> 1 1 A>). Exact lockstep over 3e7 steps, 479 detours.
So the run is W4-2's run from F: K'('',0,1) at step 14, (std,2,2) at step 73, inside W4-2's invariant I; every rule, Lemma S and Lemma C carry over (Eqv_v3 TM518 pairs them too, but imports BBinf).

Figures for Checkpoint A

Fig 1 · bbchallenge default view, first 10,000 stepsviewer ↗
The site's view. The left edge holds the (01) blocks; the right edge is the counter being eaten and rebuilt.

Fig 2 · 349 vs W4-2 (as TM518 tm), steps 106-142Q1
Same blank start and step numbers per row. Compare the two head paths row by row from the yellow mark.

Fig 3 · Counter word at each overflowQ2
One row per cycle, the counter's low end at the left. Read the colour strip, then compare rows.

Checkpoint A · 3 open

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

Q1
check One detour: the two panels agree through step 121. There 349 reads A1 and steps back (green D, then orange B) where TM518 goes straight on, and afterwards 349 runs exactly 2 rows behind on the same tape. Is that the only difference you see? see Fig 2
Q2
check Counter word at each overflow: do the rows read as W4-2's binary counter (mirrored, low end on the left), flipping between standard and packed (blue/orange strip), with rare pink dirty rows? see Fig 3
Q3
decision Proof route: copy W4-2's .v, restate TF2/TF3 and phi_spec's F-clause for the detour, add the 73-step start from F, and close with flip_halts + perm_halts as in #24. Should we go straight on to proof.md and the .v (work continues meanwhile)?

More figures (2)Fig 4–5: Right records to 2e8 steps · Every 2,000,000 steps to 2e9

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

rule	from ⟶ to	cases	steps	checked
init	0^∞ A> 0^∞ ⟶ 0^∞ 01 0 01 1 B> 0^∞	= K'('',0,1) = (std,0,1), the mirror of W4-2's K('',0,1) reached from F; then S0 gives K'(001,0,2) = (std,2,2) at step 73, inside I	14	✓2/2
detour (Lemma E)	1 A> 1 x ⟶ 1 1 A> x	349's A1 = W4-2's F1 seen in the mirror; TM518 tm (= W4-2) does it in 1 step (A1 = 1RA). Only B1 enters A from the left side, so the cell left of A is always 1	3 (A1 D1 B1)	✓958/958
R1 bounce	0^∞ (01)^m 0 (01)¹⁺ⁿ 1 B> w 0^∞ ⟶ 0^∞ (01)^m+1 0 (01)ⁿ 1 B> phi(w) 0^∞	n >= 1; phi = W4-2's phi with w read from the head rightwards; L'(w) = 1 if w starts with 0, else 2e+3+2*p11 ((e,e+1) = first 00 pair, p11 = 11 pairs before it = detours)	L'(w)+10n+7	✓1200/1200
R2 overflow, q even	0^∞ (01)^m 0 01 1 B> w 0^∞ ⟶ 0^∞ (01)⁰ 0 (01)^2+m+q/2 1 B> x 0^∞	phi(w) = 0^q 1 x, q even: K'(x, m+1+q/2, 0) (W4-2's R2 / BECv5's ROv)	L'(w)+q+8	✓1200/1200
R3 reset, q odd	0^∞ (01)^m 0 01 1 B> w 0^∞ ⟶ 0^∞ (01)^m+(q+3)/2 0 01 1 B> x' 0^∞	phi(w) = 0^q 1 00 x' (or 0^q 1 then 0^inf), q odd	L'(w)+q+14	✓1200/1200
R4 overflow halt	0^∞ (01)^m 0 01 1 B> w 0^∞ ⟶ halt	phi(w) = 0^q 1 1 x, q odd; never met inside a macro rule (W4-2 Lemma S); R5 (0^q 1 01 x) nests, also never met	L'(w)+q+8 then F1	✓1200/1200
macro S0	S(std,N,m) = K'(std(N),0,m) ⟶ S(std, b, b)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); k = 0 (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓86/86
macro S1	S(std,N,m) = K'(std(N),0,m) ⟶ S(pk, 2k+b, b)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); k >= 1, k = 2^(L-1) or 2k+b >= 2^(L+1) (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓177/177
macro S2	S(std,N,m) = K'(std(N),0,m) ⟶ S(std, b+L+3, b+L+3)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); k not a power of 2, 2k+b+1 = 2^(L+1) (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓81/81
macro S3a	S(std,N,m) = K'(std(N),0,m) ⟶ S(std, 3*2^h+n, n)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); final gap, g = 0 (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓81/81
macro S3b	S(std,N,m) = K'(std(N),0,m) ⟶ S(std, 2^h+1+2g+n, n)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); final gap, g >= 1, n >= 2^(h+1)-2g (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓86/86
macro P0	S(pk,N,m) = K'(pk(N),0,m) ⟶ S(std, b+1, b+1)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); k = 0 (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓83/83
macro P1	S(pk,N,m) = K'(pk(N),0,m) ⟶ S(std, k+b, b)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); k = 2^(L-1) (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓108/108
macro P2	S(pk,N,m) = K'(pk(N),0,m) ⟶ S(std, 2r+b, b)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); r >= 1, 2r+b >= 2^L (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓157/157
macro P3	S(pk,N,m) = K'(pk(N),0,m) ⟶ S(std, b+L+1, b+L+1)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); r >= 1, 2r+b+1 = 2^L (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓81/81
macro P4a	S(pk,N,m) = K'(pk(N),0,m) ⟶ S(pk, 3*2^h+n, n)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); final gap, g = 0 (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓81/81
macro P4b	S(pk,N,m) = K'(pk(N),0,m) ⟶ S(pk, 2^h+1+2g+n, n)	N+1 = (2k+1)2^i, b = m+1+i, L = bitlen(k), r = k-2^(L-1); final gap, g >= 1, n >= 2^(h+1)-2g (W4-2 proof.md 3.4, unchanged); runs to the first clean overflow with N' >= 1	—	✓85/85
invariant I	(std,2,2) at step 73 ⟶ I holds after every macro rule	W4-2's I (linear bounds on N vs m by class); Lemma S/C are pure arithmetic, so they carry over. Checked along 1,000,000 macro steps (m = 2.57e6) and as direct overflow states for 140 macro steps (to step 3.0e7)	—	✓4/4

Compressed historythe tape as 0^∞ (01)^m 0 01 1 B> w 0^∞, w = std(N) | pk(N) (clean overflow states; the first row is the empty word) at 40 moments: where the rules are read off

0^∞ (01)^m 0 01 1 B> w 0^∞, w = std(N) | pk(N) (clean overflow states; the first row is the empty word)

step	`type`	`N`	`m`
14	std	0	1
73	std	2	2
174	pk	5	3
395	std	6	5
686	pk	12	6
1,055	std	11	7
1,742	pk	12	10
2,535	std	15	11
4,116	std	16	16
5,855	pk	33	17
7,986	std	27	19
10,797	pk	28	22
13,842	std	35	23
17,681	pk	34	26
26,495	pk	43	29
32,180	std	34	32
38,191	pk	67	33
45,296	std	44	36
52,779	pk	81	37
61,050	std	47	39
71,499	pk	46	44
82,394	std	59	45
94,743	pk	62	48
107,590	std	79	49
123,109	pk	58	54
139,182	std	81	55
156,407	pk	97	57
174,822	std	75	59
195,117	pk	80	62
216,030	std	79	63
240,335	pk	72	68
265,314	std	77	69
291,733	pk	109	71
319,626	std	95	73
352,205	pk	81	79
386,394	std	89	81
422,249	pk	127	83
466,182	std	92	92
511,013	pk	185	93
557,760	std	123	95

typelast std

not plottable

Nlast 123

mlast 95

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

	0	1
A	1RB	1LDtpl 1RA
B	1LC	1RA
C	0LD	0LC
D	0RE	1RB
E	1RD	0RF
F	0RB	---

differs from the template

file: machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v ⚠ not at pin
module: —
machine: 1RB1RA_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (1 transition apart)
diff: A1: 1LD here vs 1RA in TM518 tm (= W4-2 mirrored, renamed F->A, A->B, ..., E->F); i.e. W4-2's F1 = 1LF becomes 1RC
note: Our kill W4-2 (check_kill PASS). On the unmirrored table TP = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC only TF2 and TF3 read F1 with an unknown right side: restate them and phi_spec's PF clause with [1] *> r on the right (every PF entry already has [1;1]). TA2, RS, OVe, OVo, all arithmetic, BS_*, I, Lemma S/C and step_I are unchanged. New: init from F;; tape0 to St (false,2,2) (73 steps), then Perm (flip tm) TP f + flip_halts + perm_halts as in #24.

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

Delta proof from W4-2: proof.md adds Lemma E (the detour), the 73-step start from F and the mirror/renaming. The .v is W4-2's with tm := TP, TF2/TF3/phi_spec restated with [1] on the right, init from F, then #24's flip/perm reduction to 349.

▲phi_spec's PF clause needs list re-association ([1;1] *> [1] *> r = [1] *> [1;1] *> r) in four branches: small but fiddly.
▲The file carries two TM_from_str strings (TP and 349); check_kill.sh accepted that shape for #24.
▲init over 73 steps from F;; tape0 by esx (W4-2's init0 is 32); fallback: 14 steps to K('',0,1), then W4-2's BS_S0 with i = 0, m = 1.

Stats & provenance10⁹ steps simulated · 2,324 cells · the status in full · files

simulated: 10⁹ steps
tape: 2,324 cells · 1,157 nonzeros
growth: span ~ steps^(1/3) like W4-2 (2,324 cells at 1e9: -457..1866); abstract rules: 1,000,000 macro steps from (std,2,2), m = 2.57e6
status now: check_kill PASS, independently re-verified (status.json, 2026-10-13)
observer's note: Observe done, confidence high: 349 is W4-2 from F with a 3-step detour; rules, macro rules and I validated on 349 directly; next: proof.md + .v
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v

Proof & checks

6/6 automatic checks pass

Kill 23 · Bell eats counter · the kill file 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v: 1278 lines, 122 items · the package submission/

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

1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---

vs holdout list

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

Theorem

✓ Lemma nonhalt: ~halts tm c0. L1230

check_kill

✓ PASS · 17/17 checks pass · compile 64.14 s · coqchk pass (27.18 s) · assumptions: 0 (closed) · 2026-10-13 09:13:45 UTC · submission/check_kill.txt

Checked .v

sha256 32cbc5c17ddb0b7e…

✓	1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v	`32cbc5c17ddb0b7e…` = checked
✓	submission/1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v	`32cbc5c17ddb0b7e…` = checked

Status

✓Killed: never halts updated 2026-10-13

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

All 17 check_kill checks with their one-line results

✓	`args`	6x2 machine, framework module Individual62, mode nonhalt
✓	`input`	51432 bytes, 1278 lines, 1357 sentences
✓	`framework`	HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓	`framework_build`	13 needed framework .vo files present and fresh, with native code no older than the .vo
✓	`forbidden`	none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)
✓	`structure`	5 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 1218: TM_from_str "1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---" == <tm> (41 bytes)
✓	`theorem_text`	line 1230: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 ([local working file]
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 64.1s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---") c0 with absolute names (in-file and isolated)
✓	`isolation`	only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off
✓	`assumptions`	0 assumption(s), all in the baseline
✓	`coqchk`	coqchk -norec BB6Kill.Candidate ok (27.2s); its context summary lists nothing of the file's own
✓	`integrity`	input sha256 and framework HEAD/cleanliness identical before and after

2Where it came fromCheck: the template is the one you expect, and the measured reuse (tiles, the reuse figure, diff) agrees with what the README says was kept and changed (quoted).

adapted from verify/BECv5.v Module TM1 · detected from 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v line 9

1%of our lines identical to the template

0changed lines

1101added lines (ours only)

131template lines dropped

2 / 1 / 119items identical / adapted / new

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

Adapted from busycoq's verify/BECv5.v, Module TM1 / Module TM2, through our proof of 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (the same table with F1 = 1LF, 1,217 lines, in its own package). Changes: tm becomes tmP with F1 = 1RC; TF2, TF3 and the PF clause of phi_spec carry [1] *> r on the right; a 73-step initF from F (solve_initF) replaces the 32-step start; nonhalt becomes nonhalt_F; tm, f349, perm_349 and nonhalt are added. Comments aside, 16 lines were replaced and 43 added. The file has 1,278 lines, every lemma top level.

Fig P1 · Reuse of the template, line by line and by name

Top two bars: non-blank lines after the TM string is replaced by <TM> and whitespace is collapsed. Bottom bar: our Definitions/Lemmas/… by name.

ours 1114 lines

1% identical · 0 changed · 1101 added

template 144 lines

9% kept verbatim · 131 not in ours

our items 122

2 identical · 1 adapted · 119 new · 10 template-only

identicalchanged / adaptedours only (new)template only

Template part: lines 1–29 (shared header, before the first Module) + 31–165 (body of Module TM1; the Module/End lines left out). Ours: lines 27–1278 (header comment 1–26 left out). Line diff: Python difflib SequenceMatcher; inside a replaced block, line pairs at least 75% alike count as changed, the rest as removed + added.

Template-only names: highbit, LC0, tm', LInc0, LIncs, LIncs', RIncs, ROv, S, BigStep

Side-by-side diff: template (144 lines) vs ours (1114 lines), 1232 lines differ; runs of identical lines and long template-only runs folded

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

template		ours
1	From BusyCoq Require Import Individual62.	28	From BusyCoq Require Import Individual62.
2	Require Import ZifyNat Lia.	29	Require Import ZifyNat Lia.
3	Require Import ZArith.	30	Require Import ZArith.
4	Require Import String.	31	Require Import String.
5	From BusyCoq Require Import BinaryCounter_v2.
6	From BusyCoq Require Import Longitudinal.
8	Open Scope list.	33	Open Scope list.
10	Ltac flia := repeat (lia\|\|f_equal).
		35	Definition tmP := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC").
12	Lemma highbit x:
		37	Notation "c -->* c'" := (c -[ tmP ]->* c') (at level 40).
13	x<>O ->
		38	Notation "c -->+ c'" := (c -[ tmP ]->+ c') (at level 40).
14	exists i, 2^i<=x<2^i*2.
		40	Definition R n m := [1] > [1;0]^^(1+n) > [0] > [1;0]^^(m) > const 0.
		42	( Words W(e,o): bit d of e on cell 2d, bit d of o on cell 2d+1 (cell 0 is read by A) *)
		44	Definition bt (x:nat) : Sym := if Nat.odd x then 1 else 0.
		46	Fixpoint wd (n e o : nat) : list Sym :=
		47	match n with
		48	\| O => []
		49	\| S n' => bt e :: bt o :: wd n' (Nat.div2 e) (Nat.div2 o)
		50	end.
		52	Definition WS e o : side := wd (e+o) e o *> const 0.
		54	Lemma bt_even e: bt (2*e) = 0.
		55	Proof. unfold bt. rewrite Nat.odd_even. reflexivity. Qed.
		57	Lemma bt_odd e: bt (2*e+1) = 1.
		58	Proof. unfold bt. rewrite Nat.odd_odd. reflexivity. Qed.
		60	Lemma div2_even e: Nat.div2 (2*e) = e.
		61	Proof. apply Nat.div2_double. Qed.
		63	Lemma div2_odd e: Nat.div2 (2*e+1) = e.
		64	Proof. rewrite Nat.add_1_r. apply Nat.div2_succ_double. Qed.
		66	Lemma wd_pad n: forall e o k,
		67	e < 2^n -> o < 2^n ->
		68	wd (n+k) e o > const 0 = wd n e o > const 0.
15	Proof.	69	Proof.
16	induction x using lt_wf_ind; intros.
		70	induction n; intros e o k He Ho.
17	divmod2_cases x.
		71	- cbn in He,Ho. assert (e=0)%nat by lia. assert (o=0)%nat by lia. subst.
18	- unshelve epose proof (H n' _ _) as [i Hi].
		72	cbn. induction k.
19	1,2: lia.
		73	+ reflexivity.
20	eexists (S i).
		74	+ change (wd (S k) 0 0) with (0 :: 0 :: wd k 0 0). cbn [Str_app]. rewrite IHk. rewrite <-!const_unfold. reflexivity.
21	cbn; lia.
		75	- cbn [wd Nat.add Str_app]. f_equal. f_equal.
22	- destruct (Nat.eqb_spec n' 0).
		76	apply IHn.
23	1: exists O; lia.
		77	+ rewrite Nat.div2_div. cbn in He. apply Nat.Div0.div_lt_upper_bound; lia.
24	unshelve epose proof (H n' _ _) as [i Hi].
		78	+ rewrite Nat.div2_div. cbn in Ho. apply Nat.Div0.div_lt_upper_bound; lia.
25	1,2: lia.
26	eexists (S i).
27	cbn; lia.
28	Qed.	79	Qed.
		81	Lemma lt_pow2_self x: x < 2^x.
		82	Proof. apply Nat.pow_gt_lin_r. lia. Qed.
		84	Lemma wd_WS n e o:
		85	e < 2^n -> o < 2^n ->
		86	wd n e o *> const 0 = WS e o.
		87	Proof.
		88	intros He Ho. unfold WS.
		89	assert (e < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). pose proof (Nat.pow_le_mono_r 2 e (e+o)). lia. }
		90	assert (o < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). lia. }
		91	destruct (Nat.le_ge_cases n (e+o)) as [H1\|H1].
		92	- replace (e+o) with (n+(e+o-n)) by lia. rewrite wd_pad; auto.
		93	- replace n with ((e+o)+(n-(e+o))) by lia. rewrite wd_pad; auto.
		94	Qed.
		96	Lemma WS_split e o:
		97	WS e o = [bt e; bt o] *> WS (Nat.div2 e) (Nat.div2 o).
		98	Proof.
		99	rewrite <-(wd_WS (S (e+o)) e o).
		100	2,3: pose proof (lt_pow2_self (e+o)); pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))); lia.
		101	cbn [wd Str_app].
		102	rewrite (wd_WS (e+o)). 1: reflexivity.
		103	- rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound.
		104	pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia.
		105	- rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound.
		106	pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia.
		107	Qed.
		109	Lemma WS_00 e o: WS (2e) (2o) = [0;0] *> WS e o.
		110	Proof. rewrite WS_split, bt_even, bt_even, div2_even, div2_even. reflexivity. Qed.
		111	Lemma WS_10 e o: WS (2e+1) (2o) = [1;0] *> WS e o.
		112	Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed.
		113	Lemma WS_01 e o: WS (2e) (2o+1) = [0;1] *> WS e o.
		114	Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed.
		115	Lemma WS_11 e o: WS (2e+1) (2o+1) = [1;1] *> WS e o.
		116	Proof. rewrite WS_split, bt_odd, bt_odd, div2_odd, div2_odd. reflexivity. Qed.
		118	Lemma WS_0x e o: WS (2e) o = [0; bt o] > WS e (Nat.div2 o).
		119	Proof. rewrite WS_split, bt_even, div2_even. reflexivity. Qed.
		120	Lemma WS_1x e o: WS (2e+1) o = [1; bt o] > WS e (Nat.div2 o).
		121	Proof. rewrite WS_split, bt_odd, div2_odd. reflexivity. Qed.
		123	( The left step phi, as a relation (A scanning an E-cell / F scanning an E-cell) *)
		125	Inductive PA : nat -> nat -> nat -> nat -> Prop :=
		126	\| PA0 e o : PA (2e) o (2e+1) o
		127	\| PA1 e o e' o' : PA e o e' o' -> PA (2e+1) (2o) (2e') (2o')
		128	\| PA2 e o e' o' : PF e o e' o' -> PA (2e+1) (2o+1) (2e') (2o')
		129	with PF : nat -> nat -> nat -> nat -> Prop :=
		130	\| PF0 e o : PF (2e) (2o) (2e) (2o+1)
		131	\| PF1 e o e' o' : PF e o e' o' -> PF (2e) (2o+1) (2e') (2o')
		132	\| PF2 e o e' o' : PA e o e' o' -> PF (2e+1) (2o) (2e') (2o')
		133	\| PF3 e o e' o' : PF e o e' o' -> PF (2e+1) (2o+1) (2e') (2o').
		135	Scheme PA_mind := Induction for PA Sort Prop
		136	with PF_mind := Induction for PF Sort Prop.
		137	Combined Scheme PAF_mind from PA_mind, PF_mind.
		139	Lemma TA0 l a r: [0;a] > l <{{A}} r -->+ [1;a] > l {{B}}> r.
		140	Proof. es. Qed.
		141	Lemma TA1 l r: [1;0] > l <{{A}} r -->+ l <{{A}} [1;1] > r.
		142	Proof. es. Qed.
		143	Lemma TA2 l r: [1;1] > l <{{A}} r -->+ l <{{F}} [1;1] > r.
		144	Proof. es. Qed.
		145	Lemma TF0 l r: [0;0] > l <{{F}} r -->+ [0;1] > l {{B}}> r.
		146	Proof. es. Qed.
		147	Lemma TF1 l r: [0;1] > l <{{F}} r -->+ l <{{F}} [1;1] > r.
		148	Proof. es. Qed.
		149	(** F reads a 1 only with a 1 on its right (the cell A1 or an earlier F step wrote); there
		150	tmP's F1 = 1RC is followed by C1 = 1LA and A1 = 1LF (the detour), and the three steps leave
		151	the tape as one left move in F. Hence the explicit [1] on the right of TF2 and TF3. *)
		152	Lemma TF2 l r: [1;0] > l <{{F}} [1] > r -->+ l <{{A}} [1;1] > [1] > r.
		153	Proof. es. Qed.
		154	Lemma TF3 l r: [1;1] > l <{{F}} [1] > r -->+ l <{{F}} [1;1] > [1] > r.
		155	Proof. es. Qed.
		156	Lemma TB l r: l {{B}}> [1;1] > r -->+ [0;0] > l {{B}}> r.
		157	Proof. es. Qed.
		159	Lemma phi_spec:
		160	(forall e o e' o', PA e o e' o' -> forall r, WS e o <{{A}} r -->+ WS e' o' {{B}}> r) /\
		161	(forall e o e' o', PF e o e' o' -> forall r, WS e o <{{F}} [1] > r -->+ WS e' o' {{B}}> [1] > r).
		162	Proof.
		163	apply PAF_mind.
		164	all: intros.
		165	all: try (rewrite WS_0x, WS_1x; apply TA0).
		166	all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TA1\|]; eapply progress_trans; [apply H\|]; apply TB).
		167	all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TA2\|]; eapply progress_trans; [apply (H ([1] *> r))\|]; apply TB).
		168	all: try (rewrite WS_00, WS_01; apply TF0).
		169	all: try (rewrite WS_01, WS_00; eapply progress_trans; [apply TF1\|]; eapply progress_trans; [apply (H ([1] > [1] > r))\|]; apply (TB _ ([1] *> r))).
		170	all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TF2\|]; eapply progress_trans; [apply H\|]; apply (TB _ ([1] *> r))).
		171	all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TF3\|]; eapply progress_trans; [apply (H ([1] > [1] > r))\|]; apply (TB _ ([1] *> r))).
		172	Qed.
		174	Definition PA_spec := proj1 phi_spec.
		176	( Iterates, shape lemmas *)
		178	Inductive PAs : nat -> nat -> nat -> nat -> nat -> Prop :=
		179	\| PAs0 e o : PAs 0 e o e o
		180	\| PAsS j e o e1 o1 e2 o2 : PA e o e1 o1 -> PAs j e1 o1 e2 o2 -> PAs (S j) e o e2 o2.
		182	Lemma PA_eq e o e' o' e2 o2 e2' o2':
		183	PA e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PA e2 o2 e2' o2'.
		184	Proof. intros; subst; auto. Qed.
		186	Lemma PF_eq e o e' o' e2 o2 e2' o2':
		187	PF e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PF e2 o2 e2' o2'.
		188	Proof. intros; subst; auto. Qed.
		190	Lemma PAs_eq j e o e' o' j2 e2 o2 e2' o2':
		191	PAs j e o e' o' -> j = j2 -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PAs j2 e2 o2 e2' o2'.
		192	Proof. intros; subst; auto. Qed.
		194	Lemma PAs_1 e o e' o': PA e o e' o' -> PAs 1 e o e' o'.
		195	Proof. intros. econstructor; eauto. constructor. Qed.
		197	Lemma PAs_trans j1 j2 e o e1 o1 e2 o2:
		198	PAs j1 e o e1 o1 -> PAs j2 e1 o1 e2 o2 -> PAs (j1+j2) e o e2 o2.
		199	Proof.
		200	induction 1; intros; cbn; auto.
		201	econstructor; eauto.
		202	Qed.
		204	Lemma PAs_split j1 j2 e o e2 o2:
		205	PAs (j1+j2) e o e2 o2 -> exists e1 o1, PAs j1 e o e1 o1 /\ PAs j2 e1 o1 e2 o2.
		206	Proof.
		207	gen e o. induction j1; intros e o H.
		208	- exists e, o. split; [constructor\|auto].
		209	- cbn in H. inversion H; subst.
		210	destruct (IHj1 _ _ H2) as [e3 [o3 [H3 H4]]].
		211	exists e3, o3. split; auto. econstructor; eauto.
		212	Qed.
		214	Lemma PAs_dbl j e o e' o':
		215	PAs j e o e' o' -> PAs (2j) (2e) (2o) (2e') (2*o').
		216	Proof.
		217	induction 1.
		218	- constructor.
		219	- replace (2 * S j) with (S (S (2*j))) by lia.
		220	econstructor. 1: apply PA0.
		221	econstructor. 1: apply PA1; eassumption.
		222	assumption.
		223	Qed.
		225	Lemma PAs_dbl1 j e o e' o':
		226	PAs (S j) e o e' o' -> PAs (2j+1) (2e+1) (2o) (2e') (2*o').
		227	Proof.
		228	intros H. inversion H; subst.
		229	replace (2j+1) with (S (2j)) by lia.
		230	econstructor. 1: apply PA1; eassumption.
		231	apply PAs_dbl; assumption.
		232	Qed.
		234	( Increments *)
		236	Lemma INC_std N: PA N 0 (N+1) 0.
		237	Proof.
		238	induction N as [N IH] using lt_wf_ind.
		239	destruct (Nat.Even_or_Odd N) as [[N' HN]\|[N' HN]]; subst N.
		240	- eapply PA_eq. 1: apply (PA0 N' 0). all: lia.
		241	- eapply PA_eq. 1: apply (PA1 N' 0 (N'+1) 0), IH. all: lia.
		242	Qed.
		244	Lemma INC_stds j N: PAs j N 0 (N+j) 0.
		245	Proof.
		246	gen N. induction j; intros N.
		247	- eapply PAs_eq. 1: apply (PAs0 N 0). all: lia.
		248	- econstructor. 1: apply INC_std.
		249	eapply PAs_eq. 1: apply (IHj (N+1)). all: lia.
		250	Qed.
		252	Lemma PF_inc0 o: PF 0 o 0 (o+1).
		253	Proof.
		254	induction o as [o IH] using lt_wf_ind.
		255	destruct (Nat.Even_or_Odd o) as [[o' Ho]\|[o' Ho]]; subst o.
		256	- eapply PF_eq. 1: apply (PF0 0 o'). all: lia.
		257	- eapply PF_eq. 1: apply (PF1 0 o' 0 (o'+1)), IH. all: lia.
		258	Qed.
		260	Lemma Gap P: forall c E o1,
		261	c+1 < 2^(S P) ->
		262	PA (c + 2^(S P)E) (2^P(2o1+1)) (c + 1 + 2^(S P)E) (2^P(2o1+1)).
		263	Proof.
		264	induction P; intros c E o1 Hc.
		265	- cbn in . eapply PA_eq. 1: apply (PA0 E (2o1+1)). all: lia.
		266	- rewrite !Nat.pow_succ_r' in *.
		267	destruct (Nat.Even_or_Odd c) as [[c' Hc']\|[c' Hc']]; subst c.
		268	+ eapply PA_eq. 1: apply (PA0 (c' + 22^PE) (22^P(2*o1+1))). all: lia.
		269	+ eapply PA_eq. 1: apply (PA1 (c' + 22^PE) (2^P(2o1+1)) (c'+1+22^PE) (2^P(2o1+1))), IHP.
		270	all: lia.
		271	Qed.
		273	Lemma Gaps P j: forall c E o1,
		274	c+j < 2^(S P) ->
		275	PAs j (c + 2^(S P)E) (2^P(2o1+1)) (c + j + 2^(S P)E) (2^P(2o1+1)).
		276	Proof.
		277	induction j; intros c E o1 Hc.
		278	- eapply PAs_eq. 1: apply (PAs0 (c + 2^(S P)E) (2^P(2*o1+1))). all: lia.
		279	- econstructor. 1: apply Gap; lia.
		280	eapply PAs_eq. 1: apply (IHj (c+1) E o1). all: lia.
		281	Qed.
		283	Lemma F_inc h: forall E o O,
		284	o + 1 < 2^h ->
		285	PF (2^hE) (o + 2^hO) (2^hE) (o + 1 + 2^hO).
		286	Proof.
		287	induction h; intros E o O Ho.
		288	- cbn in Ho. lia.
		289	- rewrite !Nat.pow_succ_r' in *.
		290	destruct (Nat.Even_or_Odd o) as [[o' Ho']\|[o' Ho']]; subst o.
		291	+ eapply PF_eq. 1: apply (PF0 (2^hE) (o' + 2^hO)). all: lia.
		292	+ eapply PF_eq. 1: apply (PF1 (2^hE) (o' + 2^hO) (2^hE) (o'+1+2^hO)), IHh.
		293	all: lia.
		294	Qed.
		296	Lemma F_carry h: forall E O E' O',
		297	PF E O E' O' ->
		298	PF (2^hE) (2^h - 1 + 2^hO) (2^hE') (2^hO').
		299	Proof.
		300	induction h; intros E O E' O' H.
		301	- cbn. eapply PF_eq. 1: apply H. all: lia.
		302	- rewrite !Nat.pow_succ_r' in *.
		303	pose proof (Nat.pow_nonzero 2 h).
		304	eapply PF_eq. 1: apply (PF1 (2^hE) (2^h - 1 + 2^hO) (2^hE') (2^hO')), IHh, H.
		305	all: lia.
		306	Qed.
		309	Lemma lowbit (x:nat): x <> 0%nat -> exists P o, x = 2^P(2o+1).
		310	Proof.
		311	induction x as [x IH] using lt_wf_ind. intros Hx.
		312	destruct (Nat.Even_or_Odd x) as [[x' Hx']\|[x' Hx']]; subst x.
		313	- destruct (IH x') as [P [o Ho]]; [lia\|lia\|].
		314	exists (S P), o. rewrite Nat.pow_succ_r'. lia.
		315	- exists 0%nat, x'. cbn. lia.
		316	Qed.
		318	Lemma pow_pos P: 1 <= 2^P.
		319	Proof. pose proof (Nat.pow_nonzero 2 P). lia. Qed.
		321	Lemma pow_odd_pos P o1: 2^P <= 2^P(2o1+1).
		322	Proof. replace (2^P) with (2^P*1) at 1 by lia. apply Nat.mul_le_mono_l. lia. Qed.
		324	Lemma pow_odd_room P o1 h: 2^P(2o1+1) < 2^h -> 2^P(2o1+1) + 2^P <= 2^h.
		325	Proof.
		326	intros H.
		327	pose proof (pow_pos P). pose proof (pow_odd_pos P o1).
		328	assert (P < h). {
		329	destruct (Nat.lt_ge_cases P h) as [\|H2]; auto.
		330	pose proof (Nat.pow_le_mono_r 2 h P ltac:(lia) H2). lia. }
		331	replace (2^h) with (2^P * 2^(h-P)) in *.
		332	2: { rewrite <-Nat.pow_add_r. f_equal. lia. }
		333	assert (2*o1+1 < 2^(h-P)). { apply (Nat.mul_lt_mono_pos_l (2^P)); lia. }
		334	replace (2^P(2o1+1) + 2^P) with (2^P(2o1+2)) by lia.
		335	apply Nat.mul_le_mono_l. lia.
		336	Qed.
		338	(** The sweep: a low part (c, o) of h digit pairs, o = 2^P(2 o1+1), c < 2^(P+1), counts its
		339	T-count 2o+c up to 2^(h+1); then the carry enters the high part (E,O) in F mode. *)
		340	Lemma Sweep h: forall P o1 c E O E' O',
		341	2^P(2o1+1) < 2^h -> c < 2^(S P) -> PF E O E' O' ->
		342	PAs (2^(S h) - 2^(S P)(2o1+1) - c) (c + 2^hE) (2^P(2o1+1) + 2^hO) (2^hE') (2^hO').
		343	Proof.
		344	induction h; intros P o1 c E O E' O' Ho Hc HF.
		345	- pose proof (pow_odd_pos P o1). cbn in Ho. lia.
		346	- destruct P as [\|P'].
		347	+ (* o odd *)
		348	cbn [Nat.pow] in . rewrite Nat.mul_1_l in .
		349	assert (H1: PAs (2^(S (S h)) - 2(2o1+1) - 1) (1 + 2^(S h)E) ((2o1+1) + 2^(S h)O) (2^(S h)E') (2^(S h)*O')).
		350	{ rewrite !Nat.pow_succ_r' in *.
		351	destruct (Nat.eq_dec (o1+1) (2^h)) as [Eo\|Eo].
		352	- apply PAs_eq with 1%nat (2(2^hE)+1)%nat (2(2^h - 1 + 2^hO)+1)%nat (2(2^hE'))%nat (2(2^hO'))%nat.
		353	+ apply PAs_1. apply PA2. apply F_carry. assumption.
		354	+ lia.
		355	+ lia.
		356	+ lia.
		357	+ lia.
		358	+ lia.
		359	- destruct (lowbit (o1+1)) as [P2 [o2 Ho2]]; [lia\|].
		360	pose proof (IHh P2 o2 0%nat E O E' O') as IH.
		361	try rewrite Nat.pow_succ_r' in IH.
		362	rewrite <-Ho2 in IH.
		363	specialize (IH ltac:(lia) ltac:(pose proof (pow_pos P2); lia) HF).
		364	apply PAs_dbl in IH.
		365	apply PAs_eq with (1 + 2 * (2 * 2 ^ h - 2 * 2 ^ P2 * (2 * o2 + 1) - 0))%nat (2(2^hE)+1)%nat (2(o1 + 2^hO)+1)%nat (2(2^hE'))%nat (2(2^hO'))%nat.
		366	+ econstructor. 1: apply PA2, F_inc; lia.
		367	eapply PAs_eq. 1: apply IH. all: lia.
		368	+ lia.
		369	+ lia.
		370	+ lia.
		371	+ lia.
		372	+ lia. }
		373	destruct (Nat.eq_dec c 1%nat) as [->\|Hc1].
		374	* exact H1.
		375	* assert (c = 0%nat) as -> by lia.
		376	apply PAs_eq with (1 + (2^(S (S h)) - 2(2o1+1) - 1))%nat (0 + 2^(S h)E)%nat (2o1+1+2^(S h)O)%nat (2^(S h)E')%nat (2^(S h)*O')%nat.
		377	-- econstructor. 2: apply H1.
		378	rewrite Nat.pow_succ_r'. eapply PA_eq. 1: apply (PA0 (2^hE) (2o1+1+22^hO)). all: lia.
		379	-- rewrite !Nat.pow_succ_r' in *. lia.
		380	-- rewrite !Nat.pow_succ_r' in *. lia.
		381	-- rewrite !Nat.pow_succ_r' in *. lia.
		382	-- rewrite !Nat.pow_succ_r' in *. lia.
		383	-- rewrite !Nat.pow_succ_r' in *. lia.
		384	+ (* o even *)
		385	rewrite (Nat.pow_succ_r' 2 (S P')) in *.
		386	rewrite (Nat.pow_succ_r' 2 P') in *.
		387	rewrite (Nat.pow_succ_r' 2 (S h)) in *.
		388	rewrite (Nat.pow_succ_r' 2 h) in *.
		389	destruct (Nat.Even_or_Odd c) as [[c' Hc']\|[c' Hc']]; subst c.
		390	* pose proof (IHh P' o1 c' E O E' O') as IH.
		391	try rewrite !Nat.pow_succ_r' in IH.
		392	specialize (IH ltac:(lia) ltac:(lia) HF).
		393	apply PAs_dbl in IH.
		394	eapply PAs_eq. 1: apply IH. all: lia.
		395	* pose proof (IHh P' o1 c' E O E' O') as IH.
		396	try rewrite !Nat.pow_succ_r' in IH.
		397	specialize (IH ltac:(lia) ltac:(lia) HF).
		398	pose proof (pow_odd_pos P' o1).
		399	pose proof (pow_odd_room P' o1 h ltac:(lia)).
		400	remember (2 * 2 ^ h - 2 * 2 ^ P' * (2 * o1 + 1) - c') as n eqn:En.
		401	destruct n as [\|n']. 1: lia.
		402	apply PAs_dbl1 in IH.
		403	eapply PAs_eq. 1: apply IH. all: lia.
		404	Qed.
		406	( The right step and the overflows *)
		408	Lemma RS l n m:
		409	l {{B}}> R (S n) m -->+ l <{{A}} R n (S m).
		410	Proof.
		411	unfold R. es.
		412	Qed.
		414	Lemma shift01 u (r:side): [0;1]^^u > [0] > r = [0] > [1;0]^^u > r.
		415	Proof.
		416	induction u.
		417	- reflexivity.
		418	- cbn [lpow]. rewrite !Str_app_assoc. rewrite IHu. reflexivity.
		419	Qed.
		421	Lemma OVe l u m:
		422	([0;0]^^u > [1] > l) {{B}}> R 0 m -->+ l <{{A}} R (1+u+m) 0.
		423	Proof.
		424	unfold R. es.
		425	Qed.
		427	Lemma OVo l u m:
		428	([0;0]^^u > [0;1;0;0] > l) {{B}}> R 0 m -->+ l <{{A}} R 0 (u+2+m).
		429	Proof.
		430	unfold R. es.
		431	Qed.
		433	Definition K e o n m := WS e o <{{A}} R n m.
		435	( Words on the tape *)
		437	Lemma WS_shift: forall n a c, a + c < n -> WS a c = [bt a] *> WS c (Nat.div2 a).
		438	Proof.
		439	induction n; intros a c Hn. 1: lia.
		440	destruct (Nat.eq_dec (a+c) 0%nat) as [E\|E].
		441	- assert (a = 0%nat) as -> by lia. assert (c = 0%nat) as -> by lia.
		442	unfold WS. cbn. rewrite <-const_unfold. reflexivity.
		443	- rewrite WS_split. rewrite (WS_split c).
		444	rewrite (IHn (Nat.div2 a) (Nat.div2 c)).
		445	+ reflexivity.
		446	+ rewrite !Nat.div2_div.
		447	pose proof (Nat.Div0.div_le_upper_bound a 2 (a/2)).
		448	pose proof (Nat.div_mod a 2). pose proof (Nat.div_mod c 2).
		449	pose proof (Nat.mod_upper_bound a 2). pose proof (Nat.mod_upper_bound c 2). lia.
		450	Qed.
		452	Lemma WS_1 a c: WS (2a+1) c = [1] > WS c a.
		453	Proof.
		454	rewrite (WS_shift (S (2*a+1+c))) by lia. rewrite bt_odd, div2_odd. reflexivity.
		455	Qed.
		457	Lemma WS_pow x y u: WS (x2^u) (y2^u) = [0;0]^^u *> WS x y.
		458	Proof.
		459	induction u.
		460	- cbn. rewrite !Nat.mul_1_r. reflexivity.
		461	- rewrite Nat.pow_succ_r'.
		462	replace (x(22^u)) with (2(x2^u)) by lia.
		463	replace (y(22^u)) with (2(y2^u)) by lia.
		464	rewrite WS_00, IHu. cbn [lpow]. rewrite Str_app_assoc. reflexivity.
		465	Qed.
		467	( Composite rules on K configurations *)
		469	Lemma bounces j e o e' o' n m:
		470	PAs j e o e' o' -> K e o (j+n) m -->* K e' o' n (j+m).
		471	Proof.
		472	intros H. gen n m. induction H; intros n m.
		473	- finish.
		474	- apply evstep_trans with (K e1 o1 (j+n) (S m)).
		475	+ apply progress_evstep. unfold K.
		476	eapply progress_trans. 1: apply PA_spec; eassumption.
		477	cbn [Nat.add]. apply RS.
		478	+ eapply evstep_trans. 1: apply IHPAs. finish.
		479	Qed.
		481	Lemma OV_even e o a c u m:
		482	PA e o ((2a+1)2^u) (c*2^u) -> K e o 0 m -->+ K c a (1+u+m) 0.
		483	Proof.
		484	intros H. unfold K.
		485	eapply progress_trans. 1: apply PA_spec, H.
		486	rewrite WS_pow, WS_1.
		487	apply OVe.
		488	Qed.
		490	Lemma OV_odd e o a c u m:
		491	PA e o (c2^(u+2)) ((4a+1)*2^u) -> K e o 0 m -->+ K c a 0 (u+2+m).
		492	Proof.
		493	intros H. unfold K.
		494	eapply progress_trans. 1: apply PA_spec, H.
		495	replace (c2^(u+2)) with ((2(2c))2^u) by (rewrite Nat.pow_add_r; cbn; lia).
		496	replace (4a+1) with (2(2*a)+1) by lia.
		497	rewrite WS_pow, WS_01, WS_00.
		498	apply OVo.
		499	Qed.
		501	( Packed counter *)
		503	Definition pkE N := N - 2^(Nat.log2 N).
		504	Definition pkO N := 2^(Nat.log2 N - 1).
		506	Lemma pk_eq P N: 2^(S P) <= N < 2^(S (S P)) -> pkE N = N - 2^(S P) /\ pkO N = 2^P.
		507	Proof.
		508	intros H. unfold pkE, pkO.
		509	rewrite (Nat.log2_unique N (S P)); [\|lia\|lia].
		510	split; [reflexivity\|]. f_equal. lia.
		511	Qed.
		513	Lemma PAs_1_inv e o e2 o2: PAs 1 e o e2 o2 -> PA e o e2 o2.
		514	Proof.
		515	intros H. inversion H as [\|j' e' o' e1 o1 e3 o3 HA HB]; subst.
		516	inversion HB; subst. assumption.
		517	Qed.
		519	Lemma PAs_last j e o e2 o2:
		520	PAs (S j) e o e2 o2 -> exists e1 o1, PAs j e o e1 o1 /\ PA e1 o1 e2 o2.
		521	Proof.
		522	intros H. replace (S j) with (j+1) in H by lia.
		523	destruct (PAs_split _ _ _ _ _ _ H) as [e1 [o1 [H1 H2]]].
		524	exists e1, o1. split; auto. apply PAs_1_inv, H2.
		525	Qed.
		527	Lemma INC_pk N: 2 <= N -> PA (pkE N) (pkO N) (pkE (S N)) (pkO (S N)).
		528	Proof.
		529	intros HN.
		530	pose proof (Nat.log2_spec N ltac:(lia)) as HL.
		531	assert (Hl1: 1 <= Nat.log2 N). { pose proof (Nat.log2_le_mono 2 N HN) as Hm. cbn in Hm. lia. }
		532	remember (Nat.log2 N - 1) as P.
		533	replace (Nat.log2 N) with (S P) in HL by lia.
		534	destruct (pk_eq P N HL) as [E1 E2]. rewrite E1, E2.
		535	rewrite (Nat.pow_succ_r' 2 (S P)) in HL.
		536	destruct (Nat.eq_dec (S N) (2^(S (S P)))) as [Ec\|Ec].
		537	- destruct (pk_eq (S P) (S N)) as [E3 E4].
		538	{ rewrite ?Nat.pow_succ_r' in *. lia. }
		539	rewrite E3, E4.
		540	pose proof (Sweep (S P) P 0 (2^(S P) - 1) 0 0 0 1) as H.
		541	specialize (H ltac:(rewrite ?Nat.pow_succ_r' in *; lia) ltac:(lia) (PF0 0 0)).
		542	apply PAs_1_inv.
		543	eapply PAs_eq. 1: apply H. all: rewrite ?Nat.pow_succ_r' in *; lia.
		544	- destruct (pk_eq P (S N)) as [E3 E4].
		545	{ rewrite ?Nat.pow_succ_r' in *. lia. }
		546	rewrite E3, E4.
		547	pose proof (Gap P (N - 2^(S P)) 0 0) as H.
		548	specialize (H ltac:(rewrite ?(Nat.pow_succ_r' 2 (S P)) in *; lia)).
		549	eapply PA_eq. 1: apply H. all: lia.
		550	Qed.
		552	Lemma INC_pks j N: 2 <= N -> PAs j (pkE N) (pkO N) (pkE (N+j)) (pkO (N+j)).
		553	Proof.
		554	gen N. induction j; intros N HN.
		555	- eapply PAs_eq. 1: apply (PAs0 (pkE N) (pkO N)). all: f_equal; lia.
		556	- econstructor. 1: apply INC_pk; lia.
		557	eapply PAs_eq. 1: apply (IHj (S N)); lia. all: f_equal; lia.
		558	Qed.
		560	( Macro rules (proof.md 3.6). l is bitlen(k)-1, b = 1+i+m. *)
		562	Lemma bounces0 j e o e' o' m:
		563	PAs j e o e' o' -> K e o j m -->* K e' o' 0 (j+m).
		564	Proof.
		565	intros H. pose proof (bounces j e o e' o' 0 m H) as H1.
		566	rewrite Nat.add_0_r in H1. exact H1.
		567	Qed.
		569	Lemma OVB e o a c u m e' o':
		570	PA e o ((2a+1)2^u) (c*2^u) ->
		571	PAs (1+u+m) c a e' o' ->
		572	K e o 0 m -->+ K e' o' 0 (1+u+m).
		573	Proof.
		574	intros H1 H2. eapply progress_evstep_trans. 1: apply OV_even, H1.
		575	eapply evstep_trans. 1: apply bounces0, H2.
		576	finish.
		577	Qed.
		579	Lemma std_ov k i: PA ((2k+1)2^i-1) 0 ((2k+1)2^i) (0*2^i).
		580	Proof.
		581	pose proof (pow_pos i).
		582	eapply PA_eq. 1: apply (INC_std ((2k+1)2^i-1)). all: nia.
		583	Qed.
		585	Lemma BS_S0 i m: K (2^i-1) 0 0 m -->+ K (1+i+m) 0 0 (1+i+m).
		586	Proof.
		587	apply OVB with (a:=0%nat) (c:=0%nat).
		588	- pose proof (std_ov 0 i). eapply PA_eq. 1: apply H. all: lia.
		589	- eapply PAs_eq. 1: apply (INC_stds (1+i+m) 0). all: lia.
		590	Qed.
		592	Lemma OVoS0 e o u m: PA e o 0 (2^u) -> K e o 0 m -->+ K (u+3+m) 0 0 (u+3+m).
		593	Proof.
		594	intros H.
		595	eapply progress_trans. 1: apply (OV_odd e o 0 0 u m).
		596	- eapply PA_eq. 1: apply H. all: lia.
		597	- pose proof (BS_S0 0 (u+2+m)) as H1. cbn in H1.
		598	eapply progress_evstep_trans. 1: apply H1. finish.
		599	Qed.
		601	Lemma BS_S1a l k i m:
		602	k = 2^l ->
		603	K ((2k+1)2^i-1) 0 0 m -->+ K (pkE (2k+(1+i+m))) (pkO (2k+(1+i+m))) 0 (1+i+m).
		604	Proof.
		605	intros Hk.
		606	apply OVB with (a:=k) (c:=0%nat).
		607	1: apply std_ov.
		608	destruct (pk_eq l (2^(S l))) as [E1 E2].
		609	{ rewrite !Nat.pow_succ_r'. pose proof (pow_pos l). lia. }
		610	eapply PAs_eq. 1: apply (INC_pks (1+i+m) (2^(S l))).
		611	- rewrite Nat.pow_succ_r'. pose proof (pow_pos l). lia.
		612	- reflexivity.
		613	- rewrite E1. lia.
		614	- rewrite E2. lia.
		615	- f_equal. rewrite Nat.pow_succ_r'. lia.
		616	- f_equal. rewrite Nat.pow_succ_r'. lia.
		617	Qed.
		619	(** sweep of W(0,k), k < 2^(l+1), into pk(2^(l+2)) *)
		620	Lemma O3_merge l k:
		621	1 <= k < 2^(S l) ->
		622	PAs (2^(S (S l)) - 2*k) 0 k (pkE (2^(S (S l)))) (pkO (2^(S (S l)))).
		623	Proof.
		624	intros Hk.
		625	destruct (lowbit k) as [P [o1 Ho]]; [lia\|].
		626	pose proof (Sweep (S l) P o1 0 0 0 0 1) as H.
		627	specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF0 0 0)).
		628	destruct (pk_eq (S l) (2^(S (S l)))) as [E1 E2].
		629	{ rewrite !(Nat.pow_succ_r' 2 (S _)). pose proof (pow_pos (S l)). lia. }
		630	rewrite E1, E2.
		631	eapply PAs_eq. 1: apply H. all: rewrite ?Nat.pow_succ_r' in *; lia.
		632	Qed.
		634	Lemma BS_S1b l k i m:
		635	2^l <= k < 2^(S l) ->
		636	2^(S (S l)) <= 2*k+(1+i+m) ->
		637	K ((2k+1)2^i-1) 0 0 m -->+ K (pkE (2k+(1+i+m))) (pkO (2k+(1+i+m))) 0 (1+i+m).
		638	Proof.
		639	intros Hk Hb.
		640	pose proof (pow_pos l).
		641	apply OVB with (a:=k) (c:=0%nat).
		642	1: apply std_ov.
		643	pose proof (O3_merge l k ltac:(lia)) as H1.
		644	pose proof (INC_pks (2*k+(1+i+m)-2^(S (S l))) (2^(S (S l)))) as H2.
		645	specialize (H2 ltac:(rewrite !Nat.pow_succ_r'; lia)).
		646	pose proof (PAs_trans _ _ _ _ _ _ _ _ H1 H2) as H3.
		647	eapply PAs_eq. 1: apply H3. all: try reflexivity.
		648	- rewrite !(Nat.pow_succ_r' 2 (S _)) in . rewrite !Nat.pow_succ_r' in . lia.
		649	- f_equal. lia.
		650	- f_equal. lia.
		651	Qed.
		653	Lemma BS_S2 l k i m:
		654	2^l <= k < 2^(S l) ->
		655	2*k+(1+i+m)+1 = 2^(S (S l)) ->
		656	K ((2k+1)2^i-1) 0 0 m -->+ K (l+4+(1+i+m)) 0 0 (l+4+(1+i+m)).
		657	Proof.
		658	intros Hk Hb.
		659	pose proof (pow_pos l).
		660	pose proof (O3_merge l k ltac:(lia)) as H1.
		661	destruct (pk_eq (S l) (2^(S (S l)))) as [E1 E2].
		662	{ rewrite !(Nat.pow_succ_r' 2 (S _)). pose proof (pow_pos (S l)). lia. }
		663	rewrite E1, E2 in H1.
		664	replace (2 ^ S (S l) - 2 * k) with (S (1+i+m)) in H1 by lia.
		665	destruct (PAs_last _ _ _ _ _ H1) as [e1 [o1 [H2 H3]]].
		666	eapply progress_trans. 1: apply OV_even with (a:=k) (c:=0%nat) (u:=i), std_ov.
		667	eapply evstep_progress_trans. 1: apply bounces0, H2.
		668	eapply progress_evstep_trans. 1: apply (OVoS0 _ _ (S l)).
		669	- eapply PA_eq. 1: apply H3. all: lia.
		670	- finish.
		671	Qed.
		673	Lemma pk_ov_full i: 2 <= i ->
		674	PA (pkE (2^i-1)) (pkO (2^i-1)) 0 (2^(i-1)).
		675	Proof.
		676	intros Hi.
		677	pose proof (INC_pk (2^i-1)) as H.
		678	assert (4 <= 2^i). { pose proof (Nat.pow_le_mono_r 2 2 i ltac:(lia) Hi). cbn in H0. lia. }
		679	specialize (H ltac:(lia)).
		680	replace (S (2^i-1)) with (2^i) in H by lia.
		681	destruct (pk_eq (i-1) (2^i)) as [E1 E2].
		682	{ replace (S (i-1)) with i by lia. split; [lia \| apply Nat.pow_lt_mono_r; lia]. }
		683	rewrite E1, E2 in H.
		684	eapply PA_eq. 1: apply H. all: try reflexivity.
		685	replace (S (i-1)) with i by lia. lia.
		686	Qed.
		688	Lemma BS_P0 i m: 2 <= i ->
		689	K (pkE (2^i-1)) (pkO (2^i-1)) 0 m -->+ K (2+i+m) 0 0 (2+i+m).
		690	Proof.
		691	intros Hi.
		692	eapply progress_evstep_trans. 1: apply (OVoS0 _ _ (i-1)), pk_ov_full, Hi.
		693	finish.
		694	Qed.
		696	(** pk(N) with N+1 = (2k+1) 2^i, 2^l <= k < 2^(l+1), k = 2^l + r: overflow gives W(2^l, r) *)
		697	Lemma pk_ov l r i:
		698	r < 2^l ->
		699	PA (pkE ((2(2^l+r)+1)2^i-1)) (pkO ((2(2^l+r)+1)2^i-1)) ((2r+1)2^i) (2^l*2^i).
		700	Proof.
		701	intros Hr.
		702	pose proof (pow_pos l). pose proof (pow_pos i).
		703	destruct (pk_eq (l+i) ((2(2^l+r)+1)2^i-1)) as [E1 E2].
		704	{ rewrite !Nat.pow_succ_r', Nat.pow_add_r. nia. }
		705	rewrite E1, E2.
		706	pose proof (Gap (l+i) ((2r+1)2^i-1) 0 0) as HG.
		707	specialize (HG ltac:(rewrite !Nat.pow_succ_r', Nat.pow_add_r; nia)).
		708	eapply PA_eq. 1: apply HG.
		709	all: rewrite ?Nat.pow_succ_r', ?Nat.pow_add_r; nia.
		710	Qed.
		712	Lemma BS_P1 l i m:
		713	K (pkE ((2(2^l+0)+1)2^i-1)) (pkO ((2(2^l+0)+1)2^i-1)) 0 m -->+ K (2^l+(1+i+m)) 0 0 (1+i+m).
		714	Proof.
		715	apply OVB with (a:=0%nat) (c:=2^l).
		716	1: apply pk_ov; apply pow_pos.
		717	eapply PAs_eq. 1: apply (INC_stds (1+i+m) (2^l)). all: lia.
		718	Qed.
		720	Lemma BS_P2 l r i m:
		721	1 <= r < 2^l ->
		722	2^(S l) <= 2*r+(1+i+m) ->
		723	K (pkE ((2(2^l+r)+1)2^i-1)) (pkO ((2(2^l+r)+1)2^i-1)) 0 m -->+ K (2*r+(1+i+m)) 0 0 (1+i+m).
		724	Proof.
		725	intros Hr Hb.
		726	apply OVB with (a:=r) (c:=2^l).
		727	1: apply pk_ov; lia.
		728	destruct (lowbit r) as [P [o1 Ho]]; [lia\|].
		729	pose proof (Sweep l P o1 0 1 0 2 0) as H.
		730	specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
		731	specialize (H (PF2 0 0 1 0 (PA0 0 0))).
		732	rewrite !Nat.mul_0_r in H.
		733	pose proof (INC_stds (2r+(1+i+m)-2^(S l)) (2^l2)) as H2.
		734	pose proof (PAs_trans _ _ _ _ _ _ _ _ H H2) as H3.
		735	eapply PAs_eq. 1: apply H3. all: rewrite ?Nat.pow_succ_r' in *; lia.
		736	Qed.
		738	Lemma BS_P3 l r i m:
		739	1 <= r < 2^l ->
		740	2*r+(1+i+m)+1 = 2^(S l) ->
		741	K (pkE ((2(2^l+r)+1)2^i-1)) (pkO ((2(2^l+r)+1)2^i-1)) 0 m -->+ K (l+2+(1+i+m)) 0 0 (l+2+(1+i+m)).
		742	Proof.
		743	intros Hr Hb.
		744	destruct (lowbit r) as [P [o1 Ho]]; [lia\|].
		745	pose proof (Sweep l P o1 0 1 0 2 0) as H.
		746	specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
		747	specialize (H (PF2 0 0 1 0 (PA0 0 0))).
		748	replace (2 ^ S l - 2 ^ S P * (2 * o1 + 1) - 0) with (S (1+i+m)) in H by (rewrite ?Nat.pow_succ_r' in *; lia).
		749	destruct (PAs_last _ _ _ _ _ H) as [e1 [o1' [H2 H3]]].
		750	eapply progress_trans. 1: apply OV_even with (a:=r) (c:=2^l) (u:=i), pk_ov; lia.
		751	eapply evstep_progress_trans.
		752	1: { eapply bounces0. eapply PAs_eq. 1: apply H2. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
		753	eapply progress_evstep_trans. 1: apply OV_even with (a:=0%nat) (c:=0%nat) (u:=S l).
		754	- eapply PA_eq. 1: apply H3. all: rewrite ?Nat.pow_succ_r' in *; lia.
		755	- eapply evstep_trans. 1: apply bounces0, (INC_stds _ 0).
		756	finish.
		757	Qed.
		759	Lemma PAs_trans_eq j1 j2 e o e1 o1 e1' o1' e2 o2:
		760	PAs j1 e o e1 o1 -> PAs j2 e1' o1' e2 o2 -> e1 = e1' -> o1 = o1' -> PAs (j1+j2) e o e2 o2.
		761	Proof. intros H1 H2 -> ->. eapply PAs_trans; eauto. Qed.
		763	(** S3 / P4: the gen-1 orbit stops in its final gap at T = 2^(l+1) + v (resp. 2^l + v),
		764	v = 2^u (2g+1), l = S (h+u); the overflow then leaves the gen-2 word *)
		765	Lemma S3_pre h u r g i m:
		766	1 <= r < 2^(h+u) -> g < 2^h ->
		767	2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2*g+1) ->
		768	K ((2(2^(S (h+u))+r)+1)2^i-1) 0 0 m -->+ K (3*2^h) g (1+u+(1+i+m)) 0.
		769	Proof.
		770	intros Hr Hg Hb.
		771	pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu.
		772	assert (E1: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r.
		773	destruct (lowbit r) as [P [o1 Ho]]; [lia\|].
		774	pose proof (Sweep (h+u) P o1 0 0 2 0 3) as H1.
		775	specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF_inc0 2)).
		776	pose proof (Gaps (h+u) (2^u(2g+1)) 0 0 1) as H2.
		777	specialize (H2 ltac:(rewrite Nat.pow_succ_r', E1; nia)).
		778	pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(lia) ltac:(lia)) as H3.
		779	assert (Hj: (2 ^ S (h+u) - 2 ^ S P * (2 * o1 + 1) - 0) + 2^u(2g+1) = S (1+i+m)).
		780	{ rewrite ?Nat.pow_succ_r' in *. lia. }
		781	rewrite Hj in H3.
		782	destruct (PAs_last _ _ _ _ _ H3) as [e1 [o2 [H4 H5]]].
		783	eapply progress_trans. 1: apply OV_even with (a:=(2^(S (h+u))+r)) (c:=0%nat) (u:=i), std_ov.
		784	eapply evstep_progress_trans.
		785	1: { eapply bounces0. eapply PAs_eq. 1: apply H4. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
		786	eapply progress_evstep_trans. 1: apply OV_even with (a:=g) (c:=3*2^h) (u:=u).
		787	- eapply PA_eq. 1: apply H5. all: rewrite ?Nat.pow_succ_r' in *; nia.
		788	- finish.
		789	Qed.
		791	Lemma BS_S3a h u r i m:
		792	1 <= r < 2^(h+u) ->
		793	2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u ->
		794	K ((2(2^(S (h+u))+r)+1)2^i-1) 0 0 m -->+ K (3*2^h+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)).
		795	Proof.
		796	intros Hr Hb.
		797	eapply progress_evstep_trans. 1: apply (S3_pre h u r 0 i m); [lia\|apply pow_pos\|lia].
		798	eapply evstep_trans. 1: apply bounces0, (INC_stds _ (3*2^h)).
		799	finish.
		800	Qed.
		802	Lemma BS_S3b h u r g i m:
		803	1 <= r < 2^(h+u) -> 1 <= g < 2^h ->
		804	2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2*g+1) ->
		805	2^(S h) <= 2*g + (1+u+(1+i+m)) ->
		806	K ((2(2^(S (h+u))+r)+1)2^i-1) 0 0 m -->+ K (2^(S h)+2*g+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)).
		807	Proof.
		808	intros Hr Hg Hb Hn.
		809	eapply progress_evstep_trans. 1: apply (S3_pre h u r g i m); lia.
		810	destruct (lowbit g) as [P [o1 Ho]]; [lia\|].
		811	pose proof (Sweep h P o1 0 3 0 4 0) as H1.
		812	specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
		813	specialize (H1 (PF_eq _ _ _ _ _ _ _ _ (PF2 1 0 2 0 (PA_eq _ _ _ _ _ _ _ _ (PA1 0 0 1 0 (PA0 0 0)) eq_refl eq_refl eq_refl eq_refl)) eq_refl eq_refl eq_refl eq_refl)).
		814	pose proof (INC_stds (2g+(1+u+(1+i+m)) - 2^(S h)) (2^h4)) as H2.
		815	pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 eq_refl ltac:(lia)) as H3.
		816	eapply evstep_trans.
		817	1: { eapply bounces0. eapply PAs_eq. 1: apply H3. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
		818	apply evstep_refl'. f_equal; rewrite ?Nat.pow_succ_r' in *; lia.
		819	Qed.
		821	Lemma P4_pre h u r g i m:
		822	1 <= r < 2^(h+u) -> g < 2^h ->
		823	2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2*g+1) ->
		824	K (pkE ((2(2^(S (h+u))+r)+1)2^i-1)) (pkO ((2(2^(S (h+u))+r)+1)2^i-1)) 0 m -->+
		825	K (2^h) (2^h+g) (1+u+(1+i+m)) 0.
		826	Proof.
		827	intros Hr Hg Hb.
		828	pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu.
		829	assert (E1: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r.
		830	destruct (lowbit r) as [P [o1 Ho]]; [lia\|].
		831	pose proof (Sweep (h+u) P o1 0 2 0 2 1) as H1.
		832	specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF0 1 0)).
		833	pose proof (Gaps (h+u) (2^u(2g+1)) 0 1 0) as H2.
		834	specialize (H2 ltac:(rewrite Nat.pow_succ_r', E1; nia)).
		835	pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(rewrite ?Nat.pow_succ_r'; lia) ltac:(lia)) as H3.
		836	assert (Hj: (2 ^ S (h+u) - 2 ^ S P * (2 * o1 + 1) - 0) + 2^u(2g+1) = S (1+i+m)).
		837	{ rewrite ?Nat.pow_succ_r' in *. lia. }
		838	rewrite Hj in H3.
		839	destruct (PAs_last _ _ _ _ _ H3) as [e1 [o2 [H4 H5]]].
		840	eapply progress_trans. 1: apply OV_even with (a:=r) (c:=2^(S (h+u))) (u:=i), pk_ov; rewrite ?Nat.pow_succ_r'; lia.
		841	eapply evstep_progress_trans.
		842	1: { eapply bounces0. eapply PAs_eq. 1: apply H4. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
		843	eapply progress_evstep_trans. 1: apply OV_even with (a:=2^h+g) (c:=2^h) (u:=u).
		844	- eapply PA_eq. 1: apply H5. all: rewrite ?Nat.pow_succ_r' in *; nia.
		845	- finish.
		846	Qed.
		848	Lemma BS_P4a h u r i m:
		849	1 <= r < 2^(h+u) ->
		850	2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u ->
		851	K (pkE ((2(2^(S (h+u))+r)+1)2^i-1)) (pkO ((2(2^(S (h+u))+r)+1)2^i-1)) 0 m -->+
		852	K (pkE (32^h+(1+u+(1+i+m)))) (pkO (32^h+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)).
		853	Proof.
		854	intros Hr Hb.
		855	pose proof (pow_pos h) as Ph.
		856	eapply progress_evstep_trans. 1: apply (P4_pre h u r 0 i m); [lia\|apply pow_pos\|lia].
		857	destruct (pk_eq h (3*2^h)) as [E1 E2]. { rewrite !Nat.pow_succ_r'. lia. }
		858	pose proof (INC_pks (1+u+(1+i+m)) (3*2^h)) as H1.
		859	specialize (H1 ltac:(lia)). rewrite E1, E2 in H1.
		860	eapply evstep_trans.
		861	1: { eapply bounces0. eapply PAs_eq. 1: apply H1. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. }
		862	finish.
		863	Qed.
		865	Lemma BS_P4b h u r g i m:
		866	1 <= r < 2^(h+u) -> 1 <= g < 2^h ->
		867	2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2*g+1) ->
		868	2^(S h) <= 2*g + (1+u+(1+i+m)) ->
		869	K (pkE ((2(2^(S (h+u))+r)+1)2^i-1)) (pkO ((2(2^(S (h+u))+r)+1)2^i-1)) 0 m -->+
		870	K (pkE (2^(S h)+2g+(1+u+(1+i+m)))) (pkO (2^(S h)+2g+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)).
		871	Proof.
		872	intros Hr Hg Hb Hn.
		873	pose proof (pow_pos h) as Ph.
		874	eapply progress_evstep_trans. 1: apply (P4_pre h u r g i m); lia.
		875	destruct (lowbit g) as [P [o1 Ho]]; [lia\|].
		876	pose proof (Sweep h P o1 0 1 1 0 2) as H1.
		877	specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
		878	specialize (H1 (PF_eq _ _ _ _ _ _ _ _ (PF3 0 0 0 1 (PF0 0 0)) eq_refl eq_refl eq_refl eq_refl)).
		879	destruct (pk_eq (S h) (2^(S (S h)))) as [E1 E2].
		880	{ rewrite !Nat.pow_succ_r'. lia. }
		881	pose proof (INC_pks (2*g+(1+u+(1+i+m)) - 2^(S h)) (2^(S (S h)))) as H2.
		882	specialize (H2 ltac:(rewrite !Nat.pow_succ_r'; lia)).
		883	rewrite E1, E2 in H2.
		884	pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(rewrite !Nat.pow_succ_r'; lia) ltac:(rewrite !Nat.pow_succ_r'; lia)) as H3.
		885	eapply evstep_trans.
		886	1: { eapply bounces0. eapply PAs_eq. 1: apply H3. 4,5: try reflexivity.
		887	all: try (f_equal; rewrite ?Nat.pow_succ_r' in *; lia).
		888	all: rewrite ?Nat.pow_succ_r' in *; lia. }
		889	apply evstep_refl'. rewrite Nat.add_0_r. f_equal; f_equal; rewrite ?Nat.pow_succ_r' in *; lia.
		890	Qed.
		892	( Invariant (proof.md 4.1) and the main induction *)
		894	Definition St (s : bool * nat * nat) : Q * tape :=
		895	let '(t, N, m) := s in if t then K (pkE N) (pkO N) 0 m else K N 0 0 m.
		897	Definition I (s : bool * nat * nat) : Prop :=
		898	let '(t, N, m) := s in
		899	1 <= m <= N /\ (t = true -> 2 <= N) /\
		900	(if Nat.even (N + m) then
		901	(if t then (if Nat.even N then N <= 2m+3 else 2N <= 5*m+6)
		902	else (if Nat.even N then 2N <= 3m+6 else N <= 2*m+3))
		903	else N <= m+3).
		905	(** The start: busycoq's solve_init, run from F instead of A (73 steps, no F1 read). *)
		906	Ltac solve_initF :=
		907	change (F, tape0) with (cconfig_to_config (nil,nil,0,F));
		908	repeat rewrite Str_cons_def;
		909	repeat rewrite <-Str_app_assoc;
		910	repeat rewrite simpl_directed_head_l;
		911	repeat rewrite simpl_directed_head_r;
		912	repeat rewrite l_const0_app_nil;
		913	repeat rewrite r_const0_app_nil;
		914	repeat rewrite config_to_cconfig;
		915	apply cconfig_evstep_dec_spec with (n:=1000000);
		916	vm_compute;
		917	reflexivity.
		919	Lemma initF: F;; tape0 -->* K 2 0 0 2.
		920	Proof.
		921	unfold K. replace (WS 2 0) with ([0;0;1] *> const 0).
		922	2: { unfold WS. cbn. rewrite <-const_unfold. reflexivity. }
		923	unfold R. cbn [lpow Str_app app]. solve_initF.
		924	Qed.
		926	( Coverage and closure (proof.md 4.2 Lemma S, 4.3 Lemma C) *)
		928	Local Open Scope nat_scope.
		930	Lemma St_std N m: St (false, N, m) = K N 0 0 m.
		931	Proof. reflexivity. Qed.
		933	Lemma St_pk N m: St (true, N, m) = K (pkE N) (pkO N) 0 m.
		934	Proof. reflexivity. Qed.
		936	Lemma even_mod x: Nat.even x = true -> x mod 2 = 0.
		937	Proof. intros H. apply Nat.even_spec in H as [q ->]. lia. Qed.
		939	Lemma odd_mod x: Nat.even x = false -> x mod 2 = 1.
		940	Proof.
		941	intros H. destruct (Nat.Even_or_Odd x) as [He\|[q ->]].
		942	- apply Nat.even_spec in He. congruence.
		943	- lia.
		944	Qed.
		946	Ltac par x := let E := fresh "E" in
		947	destruct (Nat.even x) eqn:E; [apply even_mod in E \| apply odd_mod in E].
		949	(** I in linear-arithmetic form (parities as [mod 2]) *)
		950	Lemma I_std N m: I (false, N, m) <->
		951	1 <= m <= N /\
		952	((N+m) mod 2 = 0 -> N mod 2 = 0 -> 2N <= 3m+6) /\
		953	((N+m) mod 2 = 0 -> N mod 2 = 1 -> N <= 2*m+3) /\
		954	((N+m) mod 2 = 1 -> N <= m+3).
		955	Proof.
		956	unfold I. cbv beta iota zeta. par (N+m); par N; cbv beta iota.
		957	all: split; [intros [H1 [_ H3]]; lia \| intros H; split; [lia \| split; [intros Hf; discriminate \| lia]]].
		958	Qed.
		960	Lemma I_pk N m: I (true, N, m) <->
		961	1 <= m <= N /\ 2 <= N /\
		962	((N+m) mod 2 = 0 -> N mod 2 = 0 -> N <= 2*m+3) /\
		963	((N+m) mod 2 = 0 -> N mod 2 = 1 -> 2N <= 5m+6) /\
		964	((N+m) mod 2 = 1 -> N <= m+3).
		965	Proof.
		966	unfold I. cbv beta iota zeta. par (N+m); par N; cbv beta iota.
		967	all: split; [intros [H1 [H2 H3]]; specialize (H2 eq_refl); lia \| intros H; split; [lia \| split; [intros _; lia \| lia]]].
		968	Qed.
		970	(** results N' = D + n, m' = n *)
		971	Lemma close_diag t n: 1 <= n -> (t = true -> 2 <= n) -> I (t, n, n).
		972	Proof.
		973	intros H1 H2. destruct t; [apply I_pk; specialize (H2 eq_refl) \| apply I_std]; lia.
		974	Qed.
		976	Lemma close_std D n: 1 <= n ->
		977	(D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 1 -> D <= n+3) /\ (n mod 2 = 0 -> 2*D <= n+6)) ->
		978	I (false, D+n, n).
		979	Proof. intros. apply I_std. lia. Qed.
		981	Lemma close_pk D n: 1 <= n -> 2 <= D+n ->
		982	(D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 0 -> D <= n+3) /\ (n mod 2 = 1 -> 2D <= 3n+6)) ->
		983	I (true, D+n, n).
		984	Proof. intros. apply I_pk. lia. Qed.
		986	(** N+1 = 2^i (2k+1): the three shapes of N *)
		987	Lemma Nfacts N k i: S N = 2^i(2k+1) ->
		988	(i = 0 /\ N = 2k) \/ (i = 1 /\ N = 4k+1) \/ (2 <= i /\ (S N) mod 4 = 0 /\ 8*k+4 <= S N).
		989	Proof.
		990	intros H. destruct i as [\|[\|i']].
		991	- left. rewrite Nat.pow_0_r in H. lia.
		992	- right; left. rewrite Nat.pow_1_r in H. lia.
		993	- right; right. rewrite !Nat.pow_succ_r' in H. pose proof (pow_pos i').
		994	assert (H1: S N = 4 * (2^i'(2k+1))) by lia.
		995	assert (H2: 2k+1 <= 2^i'(2*k+1)) by nia.
		996	remember (2^i'(2k+1)) as Y. clear HeqY H. lia.
		997	Qed.
		999	Ltac nfacts N k i Hk :=
		1000	destruct (Nfacts N k i Hk) as [[-> ->]\|[[-> ->]\|[?Hi [?H4 ?H8]]]]; clear Hk.
		1002	Lemma log2_facts k: 1 <= k -> exists l r, k = 2^l + r /\ r < 2^l.
		1003	Proof.
		1004	intros Hk. exists (Nat.log2 k), (k - 2^(Nat.log2 k)).
		1005	pose proof (Nat.log2_spec k ltac:(lia)) as [H1 H2].
		1006	rewrite Nat.pow_succ_r' in H2. lia.
		1007	Qed.
		1009	Lemma pow_ge2 u: 1 <= u -> 2 <= 2^u.
		1010	Proof. intros Hu. destruct u as [\|u]; [lia\|]. rewrite Nat.pow_succ_r'. pose proof (pow_pos u). lia. Qed.
		1012	Lemma pow_ge4 u: 2 <= u -> 4 <= 2^u.
		1013	Proof.
		1014	intros Hu. replace u with (S (S (u-2))) by lia. rewrite !Nat.pow_succ_r'.
		1015	pose proof (pow_pos (u-2)). lia.
		1016	Qed.
		1018	Lemma pow_par h: (h = 0 /\ 2^h = 1) \/ 2^h mod 2 = 0.
		1019	Proof. destruct h as [\|h]; [left; split; reflexivity \| right; rewrite Nat.pow_succ_r'; lia]. Qed.
		1021	(** the gen-2 exponents of S3/P4: v = 2^u (2g+1) with 1 <= v < 2^l and v even *)
		1022	Lemma split_v l v: 1 <= v -> v < 2^l -> v mod 2 = 0 ->
		1023	exists h u g, l = S (h+u) /\ v = 2^u(2g+1) /\ 1 <= u /\ g < 2^h.
		1024	Proof.
		1025	intros Hv1 Hv2 Hv3.
		1026	destruct (lowbit v) as [u [g Hv]]; [lia\|].
		1027	pose proof (pow_odd_pos u g) as Pug.
		1028	assert (Hul: u < l). { apply (Nat.pow_lt_mono_r_iff 2); lia. }
		1029	exists (l - S u), u, g.
		1030	assert (El: l = S (l - S u + u)) by lia.
		1031	split; [exact El\|]. split; [exact Hv\|].
		1032	pose proof (pow_pos u) as Pu.
		1033	split.
		1034	- destruct u as [\|u']; [\|lia]. rewrite Nat.pow_0_r in Hv. lia.
		1035	- set (h := l - S u) in *. clearbody h. subst l.
		1036	rewrite Nat.pow_succ_r', Nat.pow_add_r in Hv2.
		1037	assert (H1: 2^u(2g+1) < 2^u(22^h)) by lia.
		1038	apply Nat.mul_lt_mono_pos_l in H1; lia.
		1039	Qed.
		1041	(** closure of S1, P1, P2 (proof.md 4.3) *)
		1042	Lemma C_S1 N m i k: I (false, N, m) -> S N = 2^i(2k+1) -> 1 <= k ->
		1043	I (true, 2*k+(1+i+m), 1+i+m).
		1044	Proof.
		1045	intros HI Hk Hk1. apply I_std in HI. apply I_pk.
		1046	nfacts N k i Hk; lia.
		1047	Qed.
		1049	Lemma C_P1 N m i l: I (true, N, m) -> S N = 2^i(2(2^l+0)+1) ->
		1050	I (false, 2^l+(1+i+m), 1+i+m).
		1051	Proof.
		1052	intros HI Hk. apply I_pk in HI. apply I_std.
		1053	pose proof (pow_pos l). pose proof (pow_par l) as Hl.
		1054	rewrite Nat.add_0_r in Hk. set (Z := 2^l) in *. clearbody Z.
		1055	nfacts N Z i Hk; lia.
		1056	Qed.
		1058	Lemma C_P2 N m i l r: I (true, N, m) -> S N = 2^i(2(2^l+r)+1) -> r < 2^l ->
		1059	I (false, 2*r+(1+i+m), 1+i+m).
		1060	Proof.
		1061	intros HI Hk Hr. apply I_pk in HI. apply I_std.
		1062	set (Z := 2^l) in *. clearbody Z.
		1063	nfacts N (Z+r) i Hk; lia.
		1064	Qed.
		1066	(** coverage of S3 and P4 (proof.md 4.2): the dirty cases are i = 0 (S3), i <= 1 (P4), class P,
		1067	in the final gap, with T even *)
		1068	Lemma Cov_S3 N m i l r: I (false, N, m) -> S N = 2^i(2(2^l+r)+1) -> 1 <= r -> r < 2^l ->
		1069	2(2^l+r)+(1+i+m)+1 < 42^l ->
		1070	i = 0 /\ m mod 2 = 0 /\ 2r < 2^l /\ 32^l < 2(2^l+r)+(1+i+m)+1 /\ 4(2^l+r) <= 3*m+6.
		1071	Proof.
		1072	intros HI Hk Hr1 Hr Hlt. apply I_std in HI.
		1073	set (Z := 2^l) in *. clearbody Z.
		1074	nfacts N (Z+r) i Hk; lia.
		1075	Qed.
		1077	Lemma Cov_P4 N m i l r: I (true, N, m) -> S N = 2^i(2(2^l+r)+1) -> 1 <= r -> r < 2^l ->
		1078	2r+(1+i+m)+1 < 22^l ->
		1079	i <= 1 /\ (2r+(1+i+m)+1) mod 2 = 0 /\ 2r < 2^l /\ 2^l < 2*r+(1+i+m)+1 /\ 2^l < 1+i+m.
		1080	Proof.
		1081	intros HI Hk Hr1 Hr Hlt. apply I_pk in HI.
		1082	set (Z := 2^l) in *. clearbody Z.
		1083	nfacts N (Z+r) i Hk; lia.
		1084	Qed.
		1086	Lemma step_std N m: I (false, N, m) -> exists s', St (false, N, m) -->+ St s' /\ I s'.
		1087	Proof.
		1088	intros HI. rewrite St_std.
		1089	assert (Hm: 1 <= m <= N) by (apply I_std in HI; tauto).
		1090	destruct (lowbit (S N)) as [i [k Hk]]; [lia\|].
		1091	destruct (Nat.eq_dec k 0) as [->\|Hk0].
		1092	{ (* S0 *)
		1093	exists (false, 1+i+m, 1+i+m). rewrite St_std. split.
		1094	- replace N with (2^i-1) by lia. apply BS_S0.
		1095	- apply close_diag; [lia \| intros Hf; discriminate Hf]. }
		1096	destruct (log2_facts k ltac:(lia)) as [l [r [-> Hr]]].
		1097	replace N with ((2(2^l+r)+1)2^i-1) by lia.
		1098	pose proof (pow_pos l) as Pl.
		1099	assert (E2: 2^(S l) = 2*2^l) by apply Nat.pow_succ_r'.
		1100	assert (E4: 2^(S (S l)) = 4*2^l) by (rewrite !Nat.pow_succ_r'; lia).
		1101	destruct (Nat.eq_dec r 0) as [->\|Hr0].
		1102	{ (* S1, k = 2^l *)
		1103	exists (true, 2*(2^l+0)+(1+i+m), 1+i+m). rewrite St_pk. split.
		1104	- apply BS_S1a with (l := l). lia.
		1105	- apply (C_S1 N); [exact HI \| exact Hk \| lia]. }
		1106	destruct (lt_eq_lt_dec (2*(2^l+r)+(1+i+m)+1) (2^(S (S l)))) as [[Hlt\|Heq]\|Hgt].
		1107	3: { (* S1, T > 2^(l+2) *)
		1108	exists (true, 2*(2^l+r)+(1+i+m), 1+i+m). rewrite St_pk. split.
		1109	- clear Hk. apply BS_S1b with (l := l); lia.
		1110	- apply (C_S1 N); [exact HI \| exact Hk \| lia]. }
		1111	2: { (* S2 *)
		1112	exists (false, l+4+(1+i+m), l+4+(1+i+m)). rewrite St_std. split.
		1113	- clear Hk. apply BS_S2; lia.
		1114	- apply close_diag; [lia \| intros Hf; discriminate Hf]. }
		1115	(* S3 *)
		1116	rewrite E4 in Hlt.
		1117	destruct (Cov_S3 N m i l r HI Hk ltac:(lia) Hr Hlt) as [-> [Hm2 [Hr2 [HT3 H43]]]].
		1118	clear HI Hk Hm.
		1119	assert (HZ: 2^l mod 2 = 0).
		1120	{ destruct l as [\|l']; [rewrite Nat.pow_0_r in *; lia \| rewrite Nat.pow_succ_r'; lia]. }
		1121	destruct (split_v l (2(2^l+r)+(1+0+m)+1 - 32^l)) as [h [u [g [-> [Hv [Hu1 Hg]]]]]];
		1122	[lia\|lia\|lia\|].
		1123	assert (E1: 2^(S (h+u)) = 2(2^h2^u)) by (rewrite Nat.pow_succ_r', Nat.pow_add_r; reflexivity).
		1124	assert (E3: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r.
		1125	assert (E5: 2^(S h) = 2*2^h) by apply Nat.pow_succ_r'.
		1126	pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu.
		1127	assert (HU: 22^h <= 2^h2^u) by (pose proof (pow_ge2 u Hu1); nia).
		1128	assert (HU2: 2 <= u -> 42^h <= 2^h2^u) by (intros Hu2; pose proof (pow_ge4 u Hu2); nia).
		1129	pose proof (pow_par h) as Hh.
		1130	(* n = 1+u+(1+0+m) > 2^l >= 42^h, n odd if u = 1 )
		1131	assert (Hn: 2^(S (h+u)) < 1+u+(1+0+m)) by lia.
		1132	assert (Hv': 2r+(1+0+m)+1 = 2^(S (h+u)) + 2^u(2*g+1)) by lia.
		1133	clear Hv HZ E4 E2 Pl HT3 H43 Hlt.
		1134	destruct (Nat.eq_dec g 0) as [->\|Hg0].
		1135	- exists (false, 3*2^h+(1+u+(1+0+m)), 1+u+(1+0+m)). rewrite St_std. split.
		1136	+ apply BS_S3a; lia.
		1137	+ apply close_std; [lia\|].
		1138	destruct Hh as [[-> Hh1]\|Hh]; [left; lia \| right; lia].
		1139	- exists (false, 2^(S h)+2*g+(1+u+(1+0+m)), 1+u+(1+0+m)). rewrite St_std. split.
		1140	+ apply BS_S3b; lia.
		1141	+ apply close_std; [lia\|]. right. lia.
		1142	Qed.
		1144	Lemma step_pk N m: I (true, N, m) -> exists s', St (true, N, m) -->+ St s' /\ I s'.
		1145	Proof.
		1146	intros HI. rewrite St_pk.
		1147	assert (Hm: 1 <= m <= N /\ 2 <= N) by (apply I_pk in HI; tauto).
		1148	destruct (lowbit (S N)) as [i [k Hk]]; [lia\|].
		1149	destruct (Nat.eq_dec k 0) as [->\|Hk0].
		1150	{ (* P0 *)
		1151	assert (Hi: 2 <= i).
		1152	{ destruct (Nfacts N 0 i Hk) as [[_ HN]\|[[_ HN]\|[Hi _]]]; lia. }
		1153	exists (false, 2+i+m, 2+i+m). rewrite St_std. split.
		1154	- replace N with (2^i-1) by lia. apply BS_P0, Hi.
		1155	- apply close_diag; [lia \| intros Hf; discriminate Hf]. }
		1156	destruct (log2_facts k ltac:(lia)) as [l [r [-> Hr]]].
		1157	replace N with ((2(2^l+r)+1)2^i-1) by lia.
		1158	pose proof (pow_pos l) as Pl.
		1159	assert (E2: 2^(S l) = 2*2^l) by apply Nat.pow_succ_r'.
		1160	destruct (Nat.eq_dec r 0) as [->\|Hr0].
		1161	{ (* P1 *)
		1162	exists (false, 2^l+(1+i+m), 1+i+m). rewrite St_std. split.
		1163	- apply BS_P1.
		1164	- apply (C_P1 N); [exact HI \| exact Hk]. }
		1165	destruct (lt_eq_lt_dec (2*r+(1+i+m)+1) (2^(S l))) as [[Hlt\|Heq]\|Hgt].
		1166	3: { (* P2 *)
		1167	exists (false, 2*r+(1+i+m), 1+i+m). rewrite St_std. split.
		1168	- clear Hk. apply BS_P2; lia.
		1169	- apply (C_P2 N m i l); [exact HI \| exact Hk \| exact Hr]. }
		1170	2: { (* P3 *)
		1171	exists (false, l+2+(1+i+m), l+2+(1+i+m)). rewrite St_std. split.
		1172	- clear Hk. apply BS_P3; lia.
		1173	- apply close_diag; [lia \| intros Hf; discriminate Hf]. }
		1174	(* P4 *)
		1175	rewrite E2 in Hlt.
		1176	destruct (Cov_P4 N m i l r HI Hk ltac:(lia) Hr Hlt) as [Hi1 [HT2 [Hr2 [HT1 Hb]]]].
		1177	clear HI Hk Hm.
		1178	assert (HZ: 2^l mod 2 = 0).
		1179	{ destruct l as [\|l']; [rewrite Nat.pow_0_r in *; lia \| rewrite Nat.pow_succ_r'; lia]. }
		1180	destruct (split_v l (2*r+(1+i+m)+1 - 2^l)) as [h [u [g [-> [Hv [Hu1 Hg]]]]]];
		1181	[lia\|lia\|lia\|].
		1182	assert (E1: 2^(S (h+u)) = 2(2^h2^u)) by (rewrite Nat.pow_succ_r', Nat.pow_add_r; reflexivity).
		1183	assert (E3: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r.
		1184	assert (E5: 2^(S h) = 2*2^h) by apply Nat.pow_succ_r'.
		1185	pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu.
		1186	assert (HU: 22^h <= 2^h2^u) by (pose proof (pow_ge2 u Hu1); nia).
		1187	pose proof (pow_par h) as Hh.
		1188	assert (Hv': 2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2*g+1)) by lia.
		1189	clear Hv HZ E2 Pl HT1 HT2 Hlt.
		1190	destruct (Nat.eq_dec g 0) as [->\|Hg0].
		1191	- exists (true, 3*2^h+(1+u+(1+i+m)), 1+u+(1+i+m)). rewrite St_pk. split.
		1192	+ apply BS_P4a; lia.
		1193	+ apply close_pk; [lia\|lia\|].
		1194	destruct Hh as [[-> Hh1]\|Hh]; [left; lia \| right; lia].
		1195	- exists (true, 2^(S h)+2*g+(1+u+(1+i+m)), 1+u+(1+i+m)). rewrite St_pk. split.
		1196	+ apply BS_P4b; lia.
		1197	+ apply close_pk; [lia\|lia\|]. right. lia.
		1198	Qed.
		1200	Lemma step_I s: I s -> exists s', St s -->+ St s' /\ I s'.
		1201	Proof.
		1202	destruct s as [[[\|] N] m].
		1203	- apply step_pk.
		1204	- apply step_std.
		1205	Qed.
		1207	Lemma nonhalt_F: ~halts tmP (F;; tape0).
		1208	Proof.
		1209	eapply multistep_nonhalt. 1: apply initF.
		1210	change (K 2 0 0 2) with (St (false, 2%nat, 2%nat)).
		1211	apply progress_nonhalt_cond with (P := I).
		1212	- apply step_I.
		1213	- cbn. lia.
		1214	Qed.
		1216	( The machine and the conjugacy: [flip tm] renamed by f349 is tmP *)
32	Definition tm := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB").	1218	Definition tm := Eval compute in (TM_from_str "1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---").
34	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
		1220	Definition f349 (q : Q) : Q :=
35	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
		1221	match q with A => F \| B => A \| C => B \| D => C \| E => D \| F => E end.
37	Notation "l <\| r" :=
		1223	Lemma perm_349 : Perm (flip tm) tmP f349.
38	(l <{{A}} [] *> r) (at level 30).
40	Notation "l \|> r" :=
⋯ 9 template-only lines (template 41–53), not in ours
54	LC0 n <\| r -->*
55	LC0 (1+n) \|> r.
56	Proof.	1224	Proof.
57	unfold LC0.
		1225	split.
58	er.
		1226	- intros [] [] H; cbn in *; try discriminate; reflexivity.
59	eapply evstep_trans.
		1227	- intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
60	1: apply progress_evstep.
61	1: apply LBinInc_spec with (qL:=[]) (qR:=[]); es.
⋯ 79 template-only lines (template 62–146), not in ours
147	- unfold to_DH_config.
148	finish.
149	Qed.	1228	Qed.
151	Lemma nonhalt: ~halts tm c0.	1230	Lemma nonhalt: ~halts tm c0.
152	Proof.	1231	Proof.
153	eapply multistep_nonhalt with (c':=S (6,6)).
		1232	intros H. apply flip_halts in H.
154	1: unfold S; esx.
		1233	change (halts (flip tm) (A;; tape0)) in H.
155	eapply progress_nonhalt_cond with (P:=fun '(a,b) => a<=1+b).
		1234	exact (nonhalt_F (perm_halts _ _ _ _ _ perm_349 H)).
156	2: lia.
157	intros [a b] HP.
⋯ 4 template-only lines (template 158–161), not in ours
162	zify_le_mul_r; lia.
163	- lia.
164	Qed.	1235	Qed.
		1237	(*
		1238	1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (only F1 is undefined)
		1239	= tmP mirrored (L<->R) and renamed by f349: A->F, B->A, C->B, D->C, E->D, F->E
		1240	(state q of tm behaves as state f349 q of tmP)
		1241	tmP = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC (only E1 is undefined)
		1242	tm from 0^inf A> 0^inf = mirror of tmP from 0^inf F> 0^inf (flip_halts, Perm (flip tm) tmP f349, perm_halts)
		1244	tmP below. words: w = ... w_2 w_1 w_0, w_d = the cell at offset d (offset 0 = the cell A reads)
		1245	W(e,o): bit d of e at offset 2d, bit d of o at offset 2d+1
		1246	std(N) = W(N,0); pk(N) = W(N-2^(P+1), 2^P) for 2^(P+1) <= N < 2^(P+2)
		1247	K(w,n,m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf (= w <\| R n m); S(typ,N,m) = K(typ(N),0,m)
		1248	on tm's tape: K'(w,n,m) = 0^inf (01)^m 0 (01)^(1+n) 1 B> w~ 0^inf (w~ = w from offset 0, left to right)
		1249	phi(w): w_0 = 0 -> w_0 := 1; else (e,e+1) := lowest pair of adjacent 0 cells: w_(e+1) := 1, w_0..w_e := 0
		1251	E l 1 <F 1 r -->(3) l <F 1 1 r F1 C1 A1 (the detour); tmP enters F only by A1 (1LF)
		1252	L 0^inf w <A r --> 0^inf phi(w) B> r steps 1 if w_0 = 0, else 2e+3+2 p11(w)
		1253	p11(w) = number of d with 1 <= d <= e-1 and w_(d-1) = w_d = 1 (one detour each)
		1255	R1 K(w,n,m) --> K(phi(w), n-1, m+1) n >= 1
		1256	R2 K(w,0,m) --> K(x, m+1+u, 0) phi(w) = x 1 0^(2u)
		1257	R3 K(w,0,m) --> K(x', 0, m+u+2) phi(w) = x' 0 0 1 0^(2u+1) (x'00 may be 0^inf)
		1258	R4 K(w,0,m) --> halt (E1; on tm: F1) phi(w) = x 1 1 0^(2u+1)
		1259	R5 K(w,0,m) --> nested scan, no rule phi(w) = x 1 0 1 0^(2u+1)
		1261	N+1 = (2k+1) 2^i, b = m+1+i, L = bitlen(k), r = k - 2^(L-1)
		1262	S0 S(std,N,m) --> S(std, b, b) k = 0
		1263	S1 S(std,N,m) --> S(pk, 2k+b, b) k >= 1, and k = 2^(L-1) or 2k+b >= 2^(L+1)
		1264	S2 S(std,N,m) --> S(std, b+L+3, b+L+3) 2k+b+1 = 2^(L+1)
		1265	S3 S(std,N,m) --> S(std, D+n, n) k < 3 2^(L-2), 3 2^(L-1) < 2k+b+1 < 2^(L+1)
		1266	P0 S(pk,N,m) --> S(std, b+1, b+1) k = 0
		1267	P1 S(pk,N,m) --> S(std, k+b, b) k = 2^(L-1)
		1268	P2 S(pk,N,m) --> S(std, 2r+b, b) r >= 1, 2r+b >= 2^L
		1269	P3 S(pk,N,m) --> S(std, b+L+1, b+L+1) r >= 1, 2r+b+1 = 2^L
		1270	P4 S(pk,N,m) --> S(pk, D+n, n) 1 <= r < 2^(L-2), 2^(L-1) < 2r+b+1 < 2^L
		1272	invariant I(typ,N,m): 1 <= m <= N (pk: N >= 2), and
		1273	N = m (mod 2): std: 2N <= 3m+6 (N even), N <= 2m+3 (N odd); pk: N <= 2m+3 (N even), 2N <= 5m+6 (N odd)
		1274	N != m (mod 2): N <= m+3
		1276	start: tmP from F;; tape0 -->(73) K(std 2,0,2) = S(std,2,2), which satisfies I
		1277	(tm: c0 -->(14) K'(0^inf,0,1) -->(59, S0) S(std,2,2); the first F1 of tmP is its 122nd step)
		1278	*)

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

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

#	kind	name	statement (no proof body)	line	vs template
1	Definition	`tmP`	Definition tmP := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC").	L35	new
2	Definition	`R`	Definition R n m := [1] > [1;0]^^(1+n) > [0] > [1;0]^^(m) > const 0.	L40	identical
3	Definition	`bt`	Definition bt (x:nat) : Sym := if Nat.odd x then 1 else 0.	L44	new
4	Fixpoint	`wd`	Fixpoint wd (n e o : nat) : list Sym := match n with \| O => [] \| S n' => bt e :: bt o :: wd n' (Nat.div2 e) (Nat.div2 o) end.	L46	new
5	Definition	`WS`	Definition WS e o : side := wd (e+o) e o *> const 0.	L52	new
6	Lemma	`bt_even`	Lemma bt_even e: bt (2*e) = 0.	L54	new
7	Lemma	`bt_odd`	Lemma bt_odd e: bt (2*e+1) = 1.	L57	new
8	Lemma	`div2_even`	Lemma div2_even e: Nat.div2 (2*e) = e.	L60	new
9	Lemma	`div2_odd`	Lemma div2_odd e: Nat.div2 (2*e+1) = e.	L63	new
10	Lemma	`wd_pad`	Lemma wd_pad n: forall e o k, e < 2^n -> o < 2^n -> wd (n+k) e o > const 0 = wd n e o > const 0.	L66	new
11	Lemma	`lt_pow2_self`	Lemma lt_pow2_self x: x < 2^x.	L81	new
12	Lemma	`wd_WS`	Lemma wd_WS n e o: e < 2^n -> o < 2^n -> wd n e o *> const 0 = WS e o.	L84	new
13	Lemma	`WS_split`	Lemma WS_split e o: WS e o = [bt e; bt o] *> WS (Nat.div2 e) (Nat.div2 o).	L96	new
14	Lemma	`WS_00`	Lemma WS_00 e o: WS (2e) (2o) = [0;0] *> WS e o.	L109	new
15	Lemma	`WS_10`	Lemma WS_10 e o: WS (2e+1) (2o) = [1;0] *> WS e o.	L111	new
16	Lemma	`WS_01`	Lemma WS_01 e o: WS (2e) (2o+1) = [0;1] *> WS e o.	L113	new
17	Lemma	`WS_11`	Lemma WS_11 e o: WS (2e+1) (2o+1) = [1;1] *> WS e o.	L115	new
18	Lemma	`WS_0x`	Lemma WS_0x e o: WS (2e) o = [0; bt o] > WS e (Nat.div2 o).	L118	new
19	Lemma	`WS_1x`	Lemma WS_1x e o: WS (2e+1) o = [1; bt o] > WS e (Nat.div2 o).	L120	new
20	Inductive	`PA`	Inductive PA : nat -> nat -> nat -> nat -> Prop := \| PA0 e o : PA (2e) o (2e+1) o \| PA1 e o e' o' : PA e o e' o' -> PA (2e+1) (2o) (2e') (2o') \| PA2 e o e' o' : PF e o e' o' -> PA (2e+1) (2o+1) (2e') (2o') with PF : nat -> nat -> nat -> nat -> Prop := \| PF0 e o : PF (2e) (2o) (2e) (2o+1) … +3 lines	L125	new
21	Lemma	`TA0`	Lemma TA0 l a r: [0;a] > l <{{A}} r -->+ [1;a] > l {{B}}> r.	L139	new
22	Lemma	`TA1`	Lemma TA1 l r: [1;0] > l <{{A}} r -->+ l <{{A}} [1;1] > r.	L141	new
23	Lemma	`TA2`	Lemma TA2 l r: [1;1] > l <{{A}} r -->+ l <{{F}} [1;1] > r.	L143	new
24	Lemma	`TF0`	Lemma TF0 l r: [0;0] > l <{{F}} r -->+ [0;1] > l {{B}}> r.	L145	new
25	Lemma	`TF1`	Lemma TF1 l r: [0;1] > l <{{F}} r -->+ l <{{F}} [1;1] > r.	L147	new
26	Lemma	`TF2`	Lemma TF2 l r: [1;0] > l <{{F}} [1] > r -->+ l <{{A}} [1;1] > [1] > r.	L152	new
27	Lemma	`TF3`	Lemma TF3 l r: [1;1] > l <{{F}} [1] > r -->+ l <{{F}} [1;1] > [1] > r.	L154	new
28	Lemma	`TB`	Lemma TB l r: l {{B}}> [1;1] > r -->+ [0;0] > l {{B}}> r.	L156	new
29	Lemma	`phi_spec`	Lemma phi_spec: (forall e o e' o', PA e o e' o' -> forall r, WS e o <{{A}} r -->+ WS e' o' {{B}}> r) /\ (forall e o e' o', PF e o e' o' -> forall r, WS e o <{{F}} [1] > r -->+ WS e' o' {{B}}> [1] > r).	L159	new
30	Definition	`PA_spec`	Definition PA_spec := proj1 phi_spec.	L174	new
31	Inductive	`PAs`	Inductive PAs : nat -> nat -> nat -> nat -> nat -> Prop := \| PAs0 e o : PAs 0 e o e o \| PAsS j e o e1 o1 e2 o2 : PA e o e1 o1 -> PAs j e1 o1 e2 o2 -> PAs (S j) e o e2 o2.	L178	new
32	Lemma	`PA_eq`	Lemma PA_eq e o e' o' e2 o2 e2' o2': PA e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PA e2 o2 e2' o2'.	L182	new
33	Lemma	`PF_eq`	Lemma PF_eq e o e' o' e2 o2 e2' o2': PF e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PF e2 o2 e2' o2'.	L186	new
34	Lemma	`PAs_eq`	Lemma PAs_eq j e o e' o' j2 e2 o2 e2' o2': PAs j e o e' o' -> j = j2 -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PAs j2 e2 o2 e2' o2'.	L190	new
35	Lemma	`PAs_1`	Lemma PAs_1 e o e' o': PA e o e' o' -> PAs 1 e o e' o'.	L194	new
36	Lemma	`PAs_trans`	Lemma PAs_trans j1 j2 e o e1 o1 e2 o2: PAs j1 e o e1 o1 -> PAs j2 e1 o1 e2 o2 -> PAs (j1+j2) e o e2 o2.	L197	new
37	Lemma	`PAs_split`	Lemma PAs_split j1 j2 e o e2 o2: PAs (j1+j2) e o e2 o2 -> exists e1 o1, PAs j1 e o e1 o1 /\ PAs j2 e1 o1 e2 o2.	L204	new
38	Lemma	`PAs_dbl`	Lemma PAs_dbl j e o e' o': PAs j e o e' o' -> PAs (2j) (2e) (2o) (2e') (2*o').	L214	new
39	Lemma	`PAs_dbl1`	Lemma PAs_dbl1 j e o e' o': PAs (S j) e o e' o' -> PAs (2j+1) (2e+1) (2o) (2e') (2*o').	L225	new
40	Lemma	`INC_std`	Lemma INC_std N: PA N 0 (N+1) 0.	L236	new
41	Lemma	`INC_stds`	Lemma INC_stds j N: PAs j N 0 (N+j) 0.	L244	new
42	Lemma	`PF_inc0`	Lemma PF_inc0 o: PF 0 o 0 (o+1).	L252	new
43	Lemma	`Gap`	Lemma Gap P: forall c E o1, c+1 < 2^(S P) -> PA (c + 2^(S P)E) (2^P(2o1+1)) (c + 1 + 2^(S P)E) (2^P(2o1+1)).	L260	new
44	Lemma	`Gaps`	Lemma Gaps P j: forall c E o1, c+j < 2^(S P) -> PAs j (c + 2^(S P)E) (2^P(2o1+1)) (c + j + 2^(S P)E) (2^P(2o1+1)).	L273	new
45	Lemma	`F_inc`	Lemma F_inc h: forall E o O, o + 1 < 2^h -> PF (2^hE) (o + 2^hO) (2^hE) (o + 1 + 2^hO).	L283	new
46	Lemma	`F_carry`	Lemma F_carry h: forall E O E' O', PF E O E' O' -> PF (2^hE) (2^h - 1 + 2^hO) (2^hE') (2^hO').	L296	new
47	Lemma	`lowbit`	Lemma lowbit (x:nat): x <> 0%nat -> exists P o, x = 2^P(2o+1).	L309	new
48	Lemma	`pow_pos`	Lemma pow_pos P: 1 <= 2^P.	L318	new
49	Lemma	`pow_odd_pos`	Lemma pow_odd_pos P o1: 2^P <= 2^P(2o1+1).	L321	new
50	Lemma	`pow_odd_room`	Lemma pow_odd_room P o1 h: 2^P(2o1+1) < 2^h -> 2^P(2o1+1) + 2^P <= 2^h.	L324	new
51	Lemma	`Sweep`	Lemma Sweep h: forall P o1 c E O E' O', 2^P(2o1+1) < 2^h -> c < 2^(S P) -> PF E O E' O' -> PAs (2^(S h) - 2^(S P)(2o1+1) - c) (c + 2^hE) (2^P(2o1+1) + 2^hO) (2^hE') (2^hO').	L340	new
52	Lemma	`RS`	Lemma RS l n m: l {{B}}> R (S n) m -->+ l <{{A}} R n (S m).	L408	new
53	Lemma	`shift01`	Lemma shift01 u (r:side): [0;1]^^u > [0] > r = [0] > [1;0]^^u > r.	L414	new
54	Lemma	`OVe`	Lemma OVe l u m: ([0;0]^^u > [1] > l) {{B}}> R 0 m -->+ l <{{A}} R (1+u+m) 0.	L421	new
55	Lemma	`OVo`	Lemma OVo l u m: ([0;0]^^u > [0;1;0;0] > l) {{B}}> R 0 m -->+ l <{{A}} R 0 (u+2+m).	L427	new
56	Definition	`K`	Definition K e o n m := WS e o <{{A}} R n m.	L433	new
57	Lemma	`WS_shift`	Lemma WS_shift: forall n a c, a + c < n -> WS a c = [bt a] *> WS c (Nat.div2 a).	L437	new
58	Lemma	`WS_1`	Lemma WS_1 a c: WS (2a+1) c = [1] > WS c a.	L452	new
59	Lemma	`WS_pow`	Lemma WS_pow x y u: WS (x2^u) (y2^u) = [0;0]^^u *> WS x y.	L457	new
60	Lemma	`bounces`	Lemma bounces j e o e' o' n m: PAs j e o e' o' -> K e o (j+n) m -->* K e' o' n (j+m).	L469	new
61	Lemma	`OV_even`	Lemma OV_even e o a c u m: PA e o ((2a+1)2^u) (c*2^u) -> K e o 0 m -->+ K c a (1+u+m) 0.	L481	new
62	Lemma	`OV_odd`	Lemma OV_odd e o a c u m: PA e o (c2^(u+2)) ((4a+1)*2^u) -> K e o 0 m -->+ K c a 0 (u+2+m).	L490	new
63	Definition	`pkE`	Definition pkE N := N - 2^(Nat.log2 N).	L503	new
64	Definition	`pkO`	Definition pkO N := 2^(Nat.log2 N - 1).	L504	new
65	Lemma	`pk_eq`	Lemma pk_eq P N: 2^(S P) <= N < 2^(S (S P)) -> pkE N = N - 2^(S P) /\ pkO N = 2^P.	L506	new
66	Lemma	`PAs_1_inv`	Lemma PAs_1_inv e o e2 o2: PAs 1 e o e2 o2 -> PA e o e2 o2.	L513	new
67	Lemma	`PAs_last`	Lemma PAs_last j e o e2 o2: PAs (S j) e o e2 o2 -> exists e1 o1, PAs j e o e1 o1 /\ PA e1 o1 e2 o2.	L519	new
68	Lemma	`INC_pk`	Lemma INC_pk N: 2 <= N -> PA (pkE N) (pkO N) (pkE (S N)) (pkO (S N)).	L527	new
69	Lemma	`INC_pks`	Lemma INC_pks j N: 2 <= N -> PAs j (pkE N) (pkO N) (pkE (N+j)) (pkO (N+j)).	L552	new
70	Lemma	`bounces0`	Lemma bounces0 j e o e' o' m: PAs j e o e' o' -> K e o j m -->* K e' o' 0 (j+m).	L562	new
71	Lemma	`OVB`	Lemma OVB e o a c u m e' o': PA e o ((2a+1)2^u) (c*2^u) -> PAs (1+u+m) c a e' o' -> K e o 0 m -->+ K e' o' 0 (1+u+m).	L569	new
72	Lemma	`std_ov`	Lemma std_ov k i: PA ((2k+1)2^i-1) 0 ((2k+1)2^i) (0*2^i).	L579	new
73	Lemma	`BS_S0`	Lemma BS_S0 i m: K (2^i-1) 0 0 m -->+ K (1+i+m) 0 0 (1+i+m).	L585	new
74	Lemma	`OVoS0`	Lemma OVoS0 e o u m: PA e o 0 (2^u) -> K e o 0 m -->+ K (u+3+m) 0 0 (u+3+m).	L592	new
75	Lemma	`BS_S1a`	Lemma BS_S1a l k i m: k = 2^l -> K ((2k+1)2^i-1) 0 0 m -->+ K (pkE (2k+(1+i+m))) (pkO (2k+(1+i+m))) 0 (1+i+m).	L601	new
76	Lemma	`O3_merge`	Lemma O3_merge l k: 1 <= k < 2^(S l) -> PAs (2^(S (S l)) - 2*k) 0 k (pkE (2^(S (S l)))) (pkO (2^(S (S l)))).	L620	new
77	Lemma	`BS_S1b`	Lemma BS_S1b l k i m: 2^l <= k < 2^(S l) -> 2^(S (S l)) <= 2k+(1+i+m) -> K ((2k+1)2^i-1) 0 0 m -->+ K (pkE (2k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m).	L634	new
78	Lemma	`BS_S2`	Lemma BS_S2 l k i m: 2^l <= k < 2^(S l) -> 2k+(1+i+m)+1 = 2^(S (S l)) -> K ((2k+1)*2^i-1) 0 0 m -->+ K (l+4+(1+i+m)) 0 0 (l+4+(1+i+m)).	L653	new
79	Lemma	`pk_ov_full`	Lemma pk_ov_full i: 2 <= i -> PA (pkE (2^i-1)) (pkO (2^i-1)) 0 (2^(i-1)).	L673	new
80	Lemma	`BS_P0`	Lemma BS_P0 i m: 2 <= i -> K (pkE (2^i-1)) (pkO (2^i-1)) 0 m -->+ K (2+i+m) 0 0 (2+i+m).	L688	new
81	Lemma	`pk_ov`	Lemma pk_ov l r i: r < 2^l -> PA (pkE ((2(2^l+r)+1)2^i-1)) (pkO ((2(2^l+r)+1)2^i-1)) ((2r+1)2^i) (2^l*2^i).	L697	new
82	Lemma	`BS_P1`	Lemma BS_P1 l i m: K (pkE ((2(2^l+0)+1)2^i-1)) (pkO ((2(2^l+0)+1)2^i-1)) 0 m -->+ K (2^l+(1+i+m)) 0 0 (1+i+m).	L712	new
83	Lemma	`BS_P2`	Lemma BS_P2 l r i m: 1 <= r < 2^l -> 2^(S l) <= 2r+(1+i+m) -> K (pkE ((2(2^l+r)+1)2^i-1)) (pkO ((2(2^l+r)+1)2^i-1)) 0 m -->+ K (2r+(1+i+m)) 0 0 (1+i+m).	L720	new
84	Lemma	`BS_P3`	Lemma BS_P3 l r i m: 1 <= r < 2^l -> 2r+(1+i+m)+1 = 2^(S l) -> K (pkE ((2(2^l+r)+1)2^i-1)) (pkO ((2(2^l+r)+1)*2^i-1)) 0 m -->+ K (l+2+(1+i+m)) 0 0 (l+2+(1+i+m)).	L738	new
85	Lemma	`PAs_trans_eq`	Lemma PAs_trans_eq j1 j2 e o e1 o1 e1' o1' e2 o2: PAs j1 e o e1 o1 -> PAs j2 e1' o1' e2 o2 -> e1 = e1' -> o1 = o1' -> PAs (j1+j2) e o e2 o2.	L759	new
86	Lemma	`S3_pre`	Lemma S3_pre h u r g i m: 1 <= r < 2^(h+u) -> g < 2^h -> 2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2g+1) -> K ((2(2^(S (h+u))+r)+1)2^i-1) 0 0 m -->+ K (32^h) g (1+u+(1+i+m)) 0.	L765	new
87	Lemma	`BS_S3a`	Lemma BS_S3a h u r i m: 1 <= r < 2^(h+u) -> 2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u -> K ((2(2^(S (h+u))+r)+1)2^i-1) 0 0 m -->+ K (32^h+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)).	L791	new
88	Lemma	`BS_S3b`	Lemma BS_S3b h u r g i m: 1 <= r < 2^(h+u) -> 1 <= g < 2^h -> 2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2g+1) -> 2^(S h) <= 2g + (1+u+(1+i+m)) -> K ((2(2^(S (h+u))+r)+1)2^i-1) 0 0 m -->+ K (2^(S h)+2*g+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)).	L802	new
89	Lemma	`P4_pre`	Lemma P4_pre h u r g i m: 1 <= r < 2^(h+u) -> g < 2^h -> 2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2g+1) -> K (pkE ((2(2^(S (h+u))+r)+1)2^i-1)) (pkO ((2(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+ K (2^h) (2^h+g) (1+u+(1+i+m)) 0.	L821	new
90	Lemma	`BS_P4a`	Lemma BS_P4a h u r i m: 1 <= r < 2^(h+u) -> 2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u -> K (pkE ((2(2^(S (h+u))+r)+1)2^i-1)) (pkO ((2(2^(S (h+u))+r)+1)2^i-1)) 0 m -->+ K (pkE (32^h+(1+u+(1+i+m)))) (pkO (3*2^h+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)).	L848	new
91	Lemma	`BS_P4b`	Lemma BS_P4b h u r g i m: 1 <= r < 2^(h+u) -> 1 <= g < 2^h -> 2r+(1+i+m)+1 = 2^(S (h+u)) + 2^u(2g+1) -> 2^(S h) <= 2g + (1+u+(1+i+m)) -> K (pkE ((2(2^(S (h+u))+r)+1)2^i-1)) (pkO ((2(2^(S (h+u))+r)+1)2^i-1)) 0 m -->+ K (pkE (2^(S h)+2g+(1+u+(1+i+m)))) (pkO (2^(S h)+2g+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)).	L865	new
92	Definition	`St`	Definition St (s : bool * nat * nat) : Q * tape := let '(t, N, m) := s in if t then K (pkE N) (pkO N) 0 m else K N 0 0 m.	L894	new
93	Definition	`I`	Definition I (s : bool * nat * nat) : Prop := let '(t, N, m) := s in 1 <= m <= N /\ (t = true -> 2 <= N) /\ (if Nat.even (N + m) then (if t then (if Nat.even N then N <= 2m+3 else 2N <= 5m+6) else (if Nat.even N then 2N <= 3m+6 else N <= 2m+3)) … +1 lines	L897	new
94	Lemma	`initF`	Lemma initF: F;; tape0 -->* K 2 0 0 2.	L919	new
95	Lemma	`St_std`	Lemma St_std N m: St (false, N, m) = K N 0 0 m.	L930	new
96	Lemma	`St_pk`	Lemma St_pk N m: St (true, N, m) = K (pkE N) (pkO N) 0 m.	L933	new
97	Lemma	`even_mod`	Lemma even_mod x: Nat.even x = true -> x mod 2 = 0.	L936	new
98	Lemma	`odd_mod`	Lemma odd_mod x: Nat.even x = false -> x mod 2 = 1.	L939	new
99	Lemma	`I_std`	Lemma I_std N m: I (false, N, m) <-> 1 <= m <= N /\ ((N+m) mod 2 = 0 -> N mod 2 = 0 -> 2N <= 3m+6) /\ ((N+m) mod 2 = 0 -> N mod 2 = 1 -> N <= 2*m+3) /\ ((N+m) mod 2 = 1 -> N <= m+3).	L950	new
100	Lemma	`I_pk`	Lemma I_pk N m: I (true, N, m) <-> 1 <= m <= N /\ 2 <= N /\ ((N+m) mod 2 = 0 -> N mod 2 = 0 -> N <= 2m+3) /\ ((N+m) mod 2 = 0 -> N mod 2 = 1 -> 2N <= 5*m+6) /\ ((N+m) mod 2 = 1 -> N <= m+3).	L960	new
101	Lemma	`close_diag`	Lemma close_diag t n: 1 <= n -> (t = true -> 2 <= n) -> I (t, n, n).	L971	new
102	Lemma	`close_std`	Lemma close_std D n: 1 <= n -> (D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 1 -> D <= n+3) /\ (n mod 2 = 0 -> 2*D <= n+6)) -> I (false, D+n, n).	L976	new
103	Lemma	`close_pk`	Lemma close_pk D n: 1 <= n -> 2 <= D+n -> (D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 0 -> D <= n+3) /\ (n mod 2 = 1 -> 2D <= 3n+6)) -> I (true, D+n, n).	L981	new
104	Lemma	`Nfacts`	Lemma Nfacts N k i: S N = 2^i(2k+1) -> (i = 0 /\ N = 2k) \/ (i = 1 /\ N = 4k+1) \/ (2 <= i /\ (S N) mod 4 = 0 /\ 8*k+4 <= S N).	L987	new
105	Lemma	`log2_facts`	Lemma log2_facts k: 1 <= k -> exists l r, k = 2^l + r /\ r < 2^l.	L1002	new
106	Lemma	`pow_ge2`	Lemma pow_ge2 u: 1 <= u -> 2 <= 2^u.	L1009	new
107	Lemma	`pow_ge4`	Lemma pow_ge4 u: 2 <= u -> 4 <= 2^u.	L1012	new
108	Lemma	`pow_par`	Lemma pow_par h: (h = 0 /\ 2^h = 1) \/ 2^h mod 2 = 0.	L1018	new
109	Lemma	`split_v`	Lemma split_v l v: 1 <= v -> v < 2^l -> v mod 2 = 0 -> exists h u g, l = S (h+u) /\ v = 2^u(2g+1) /\ 1 <= u /\ g < 2^h.	L1022	new
110	Lemma	`C_S1`	Lemma C_S1 N m i k: I (false, N, m) -> S N = 2^i(2k+1) -> 1 <= k -> I (true, 2*k+(1+i+m), 1+i+m).	L1042	new
111	Lemma	`C_P1`	Lemma C_P1 N m i l: I (true, N, m) -> S N = 2^i(2(2^l+0)+1) -> I (false, 2^l+(1+i+m), 1+i+m).	L1049	new
112	Lemma	`C_P2`	Lemma C_P2 N m i l r: I (true, N, m) -> S N = 2^i(2(2^l+r)+1) -> r < 2^l -> I (false, 2*r+(1+i+m), 1+i+m).	L1058	new
113	Lemma	`Cov_S3`	Lemma Cov_S3 N m i l r: I (false, N, m) -> S N = 2^i(2(2^l+r)+1) -> 1 <= r -> r < 2^l -> 2(2^l+r)+(1+i+m)+1 < 42^l -> i = 0 /\ m mod 2 = 0 /\ 2r < 2^l /\ 32^l < 2(2^l+r)+(1+i+m)+1 /\ 4(2^l+r) <= 3*m+6.	L1068	new
114	Lemma	`Cov_P4`	Lemma Cov_P4 N m i l r: I (true, N, m) -> S N = 2^i(2(2^l+r)+1) -> 1 <= r -> r < 2^l -> 2r+(1+i+m)+1 < 22^l -> i <= 1 /\ (2r+(1+i+m)+1) mod 2 = 0 /\ 2r < 2^l /\ 2^l < 2*r+(1+i+m)+1 /\ 2^l < 1+i+m.	L1077	new
115	Lemma	`step_std`	Lemma step_std N m: I (false, N, m) -> exists s', St (false, N, m) -->+ St s' /\ I s'.	L1086	new
116	Lemma	`step_pk`	Lemma step_pk N m: I (true, N, m) -> exists s', St (true, N, m) -->+ St s' /\ I s'.	L1144	new
117	Lemma	`step_I`	Lemma step_I s: I s -> exists s', St s -->+ St s' /\ I s'.	L1200	new
118	Lemma	`nonhalt_F`	Lemma nonhalt_F: ~halts tmP (F;; tape0).	L1207	new
119	Definition	`tm`	Definition tm := Eval compute in (TM_from_str "1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---").	L1218	identicalexcept the TM string
120	Definition	`f349`	Definition f349 (q : Q) : Q := match q with A => F \| B => A \| C => B \| D => C \| E => D \| F => E end.	L1220	new
121	Lemma	`perm_349`	Lemma perm_349 : Perm (flip tm) tmP f349.	L1223	new
122	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L1230	adapted

4What a maintainer readsCheck: the rule table below is what the .v proves, and proof.md / README read cleanly for a maintainer.

submission/proof.md · informal proof (submitted copy)
submission/README.md · the package README
submission/discord.md · Discord draft (not posted)
proof.md (working copy) · differs from the submitted copy

submission/proof.md line 98: 2. Rule table (busycoq comment-block style)

This block collects the statements of §3–§6 in one place. Its symbols are defined in §1 (v, u, h, g, n and D in the block itself). The rules are proved in §3, the invariant in §4 and the start in §6.

1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---        (349; only F1 is undefined)
  = TP mirrored (L<->R) and renamed by f: A->F, B->A, C->B, D->C, E->D, F->E   (349 state q behaves as TP state f q)
TP = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC   (the 1LF machine = ..._1LA1LF: only F1 differs; only E1 undefined)
349 from 0^inf A> 0^inf  =  mirror of TP from 0^inf F> 0^inf   (flip_halts + perm_halts)

TP below.  words: w = ... w_2 w_1 w_0, w_d = the cell at offset d (offset 0 = the cell A reads)
           W(e,o): bit d of e at offset 2d, bit d of o at offset 2d+1
std(N) = W(N,0);   pk(N) = W(N-2^(P+1), 2^P) for 2^(P+1) <= N < 2^(P+2)
K(w,n,m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf;   S(typ,N,m) = K(typ(N),0,m)
   in 349's orientation: K'(w,n,m) = 0^inf (01)^m 0 (01)^(1+n) 1 B> w~ 0^inf   (w~ = w from offset 0, left to right)
phi(w): w_0 = 0 -> w_0 := 1;  else (e,e+1) := lowest pair of adjacent 0 cells: w_(e+1) := 1, w_0..w_e := 0

E   l 1 <F 1 r  -->(3)  l <F 1 1 r        F1 C1 A1  (1LF machine: l 1 <F r -->(1) l <F 1 r);  TP enters F only by A1 (1LF)
L   0^inf w <A r  -->  0^inf phi(w) B> r     steps L_TP(w) = 1 if w_0 = 0, else 2e+3+2*p11(w)
    p11(w) = #{d : 1 <= d <= e-1, w_(d-1) = w_d = 1}  (one detour per adjacent 11 pair below the 00 pair)

R1  K(w,n,m) --> K(phi(w), n-1, m+1)       n >= 1                                    steps L_TP(w) + 10n+7
R2  K(w,0,m) --> K(x, m+1+u, 0)            phi(w) = x 1 0^(2u)                       steps L_TP(w) + 2u+8
R3  K(w,0,m) --> K(x', 0, m+u+2)           phi(w) = x' 0 0 1 0^(2u+1)  (x'00 may be 0^inf)   L_TP(w) + 2u+15
R4  K(w,0,m) --> halt (E1; 349: F1)        phi(w) = x 1 1 0^(2u+1)
R5  K(w,0,m) --> nested scan, no rule      phi(w) = x 1 0 1 0^(2u+1)

N+1 = (2k+1) 2^i,  b = m+1+i,  L = bitlen(k),  r = k - 2^(L-1),  tz = number of trailing 0 bits
S0  S(std,N,m) --> S(std, b, b)                k = 0
S1  S(std,N,m) --> S(pk, 2k+b, b)              k >= 1, and k = 2^(L-1) or 2k+b >= 2^(L+1)
S2  S(std,N,m) --> S(std, b+L+3, b+L+3)        k not a power of 2, 2k+b+1 = 2^(L+1)
S3  S(std,N,m) --> S(std, D+n, n)              k not a power of 2, k < 3*2^(L-2), 3*2^(L-1) < 2k+b+1 < 2^(L+1)
P0  S(pk,N,m)  --> S(std, b+1, b+1)            k = 0
P1  S(pk,N,m)  --> S(std, k+b, b)              k >= 1, k = 2^(L-1)
P2  S(pk,N,m)  --> S(std, 2r+b, b)             r >= 1, 2r+b >= 2^L
P3  S(pk,N,m)  --> S(std, b+L+1, b+L+1)        r >= 1, 2r+b+1 = 2^L
P4  S(pk,N,m)  --> S(pk, D+n, n)               1 <= r < 2^(L-2), 2^(L-1) < 2r+b+1 < 2^L
    S3/P4: v = 2k+b+1-3*2^(L-1) (S3) or 2r+b+1-2^(L-1) (P4); u = tz(v), h = L-2-u, g = v >> (u+1), n = b+1+u;
           D = 3*2^h if g = 0 (S3a/P4a);  D = 2^(h+1)+2g if g >= 1 and n >= 2^(h+1)-2g (S3b/P4b)
    each rule runs to the FIRST overflow state K(w',0,m') with w' clean and N' >= 1;  S2 and P0 pass through
    K(0^inf,0,M) = S(std,0,M) on the way (M = b+L+2 / b; not in I), and leave it by S0

invariant I(typ,N,m):   1 <= m <= N (pk: N >= 2), and
  N = m (mod 2):   std: 2N <= 3m+6 (N even), N <= 2m+3 (N odd);   pk: N <= 2m+3 (N even), 2N <= 5m+6 (N odd)
  N != m (mod 2):  N <= m+3
I(s) -> exactly one of S0..S3, P0..P4 applies to s, and I holds at its result

start: 349 from c0 = 0^inf A> 0^inf -->(14) K'(0^inf,0,1) = S(std,0,1) -->(59, S0) S(std,2,2) at step 73, in I
       (TP: F;; tape0 -->(73) K(std 2,0,2); the first F1 is TP's 122nd transition)

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

1 machines, 1 killed, 0 not. Family links: status.json parent, same transition table with another start (tools/dashboard.py), targeting.md follow-on rows, ledger "= twin" notes. A machine string named in a .v header / proof.md / notes.md is listed but does not make a family.

who	machine	status	relation to this kill
W5-1 kill 23	`1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---`	✓Killed: never halts	this kill
Named in a file but not linked (not counted as family)
W4-2 kill 18	`1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF`	✓Killed: never halts	named in W4-2's proof.md; named in W4-2's notes.md; named in W5-1's proof.md · review · mechanism

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

✓
Machine string exact
the .v literal == holdout list line 371 byte for byte
✓
Statement is ~halts tm c0
parsed from the .v and confirmed by check_kill (theorem_text, theorem_rocq)
✓
No axioms beyond baseline
0 assumption(s); tools/assumptions_baseline.txt allows only functional_extensionality_dep
✓
coqchk finished (optional)
coqchk pass in 27.18 s
✓
.v hash matches the checked hash
.v = checked sha256 32cbc5c17ddb…; submission/ copy = checked sha256 32cbc5c17ddb…
✓
No repo-local paths in the .v
comments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own verify/X.v is fine: none in the .v or the submission/ copy
✓
Public write-up is clean
tools/writeup_lint.py on submission/proof.md: 0 error(s)
○
proof.md reviewed by Dennis (Checkpoint B)
no Checkpoint B note from Dennis found
- proof.md L520: ## 10. Checkpoint B (Dennis)
- proof.md L535: - Open: Checkpoint B; a skeptic pass by a second agent; formalization (§8).
- proof.md L542: - Open: Checkpoint B (Dennis); the formal stage (the kill-file edits listed in §8, then check_kill).
○
Family posted together?
no other kill in the family

Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.1 s from the files linked above; nothing in this review is hand-written except the box “How we proved it never halts” (above), which quotes how_proved.md. Re-run: python3 -B tools/killreview.py 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---

Files

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

name	size	changed
notes.md ↓	9.0 KB	2026-10-13 02:20
proof.md ↓	51 KB	2026-10-13 02:03
how_proved.md ↓	1.6 KB	2026-10-14 10:51
status.json ↓	2.6 KB	2026-10-13 02:19
observe.json ↓	17 KB	2026-10-13 01:07
1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v ↓	50 KB	2026-10-13 02:06
img/	6 items	2026-10-13 01:03
rocq/	6 items	2026-10-13 02:06
scripts/	2 items	2026-10-13 01:02
submission/	5 items	2026-10-13 02:19
work/	20 items	2026-10-13 01:56
check_proof.py ↓	46 KB	2026-10-13 01:59

status.json in full

{
 "tm": "1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-13",
 "reason": "check_kill PASS, independently re-verified",
 "label": "W5-1",
 "confidence": "high",
 "template": "machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v (W4-2), plus the flip_halts/perm_halts reduction of #24 (1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---)",
 "siblings": [],
 "family_note": "Canon over all 6 starts (renaming + mirror): only start A is on the 778/740 lists. Eqv groups (2026-10-07_eqv_1590): {349, TM518 tm 1RB1RA_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---} and {W4-2, TP 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC}; neither adds a 740 holdout.",
 "checks": {
  "byte_exact": "data/holdouts/BB6_holdouts_740.txt line 349 (holdouts.py contains: exit 0)",
  "claims": "none (sheet results.csv row 1038: class only; no data/discord hit)",
  "upstream": "holdouts.py solved: no completed proof; only Eqv_v3.v TM518 (tm'), which imports BBinf (not usable)",
  "observe_checks": "28/28 PASS seed 1 and seed 2 (work/observe_checks_seed{1,2}.log)"
 },
 "proof": {
  "file": "proof.md",
  "check": "check_proof.py",
  "result": "PASS 219/219 (seed 1 --full 77 s; seed 1 default 44 s; seed 2 default 44 s)",
  "logs": [
   "work/check_proof_seed1.log",
   "work/check_proof_seed2.log",
   "work/check_proof_full_seed1.log"
  ],
  "plan_check": "rocq/plan_check_phi.v compiles (1.2 s); rocq/plan_check_phi_neg_TF2.v fails as expected",
  "plan_check_full": {
   "file": "rocq/plan_check_full.v",
   "generator": "rocq/mk_plan_check_full.py",
   "sha256": "3197daf23fb5ea0ac0286cfd8c1a9a32ae92edca811cab121429374e3317fc90",
   "result": "compiles against vendor/ busycoq, coqc 8.20.1 -native-compiler no, 65.5 s; Print Assumptions nonhalt: Closed under the global context",
   "log": "work/plan_check_full.log",
   "note": "plan check, not a check_kill run: still carries W4-2's header comment and a trailing Print Assumptions line"
  },
  "date": "2026-10-13"
 },
 "review": {
  "skeptic_round_1": {
   "date": "2026-10-13",
   "sound": true,
   "gaps": 4,
   "severity": "minor, minor, minor, minor",
   "outcome": "all fixed and re-checked (proof.md review log)"
  }
 },
 "kill": {
  "file": "1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v",
  "sha256": "32cbc5c17ddb0b7e094514fe5f9130a9ef0ec09919c17838b3472134f60e4e88",
  "check_kill": "PASS (fresh run 2026-10-13T09:13:45Z: compile 64.1 s native, coqchk pass 27.2 s, 0 assumptions; also 09:08:08Z rocq/check_kill_r1.log and the auditor run 09:10:39Z, same sha256)",
  "submission": "submission/"
 }
}

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

2 contract warnings

rank: missing
template file not in the pinned tree: machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v

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