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-8c

`1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA`

W5-8clocal proof 29Kill claimedBouncer + Chaotic Edgebbchallenge ↗Explorer parent: W5-8

How we proved it never halts

W5-8's proof, from a different start

W5-8's tape is mostly five long blocks of 1s with short words between them; their lengths follow exact rules through 12-trip stretches and collisions of the short words, into a double cycle that repeats forever. W5-8c is W5-8's table with its state letters renamed (no mirror), started in the state that is W5-8's E instead of A. So it shows W5-8's picture the right way round: the same 43-cell pattern at the left end, the same blocks, short words and collisions.

New state names change nothing about what the machine does, so every rule of W5-8 holds here unchanged. What is new is the opening. After 6,950,830 steps the run falls into the five-block pattern with lengths 2,583, 70, 76, 43 and 18. From there its collisions come in an order of their own: nine collisions, with 12-trip stretches between them, each inside the range where its rule is proved.

They reach a start of W5-8's double cycle at step 163,638,058, with a second block of 220 cells where W5-8's run has 212. The cycle's conditions (an odd first block, and a second block of at least 52 that leaves remainder 4 when divided by 8, with the other three blocks set by it) hold there. So the cycle repeats forever, the second block growing 220, 252, 284 and so on, and the missing transition is never used.

The Rocq proof keeps W5-8's rules and double cycle word for word, for W5-8's table. It replays that table's 6,950,830-step opening from state E in ten pieces, chains the nine collisions, and uses busycoq's renaming lemma to turn a halt of W5-8c into a halt of that run.

#29local proof number

458lines of Rocq

8 sto compile

6/6automatic checks

Overview

In one sentence

Bouncer. Every round trip starts at a fixed 43-cell gadget G. Beyond it are five 1-blocks n, a, b, c, d with four short particles between them, and a particle turns the head back. (submission/README.md, Mechanism)

parent W5-8 (740 line 214), KILLED_NONHALT 2026-10-13 (check_kill PASS, sha256 beef54a5..cf48, independently re-verified); mirrored sibling W5-8b (740 line 418) also KILLED_NONHALT

Upstream: Kill claimed · PR #27merged 2026-10-16 07:09 UTC by ccz181078 · PR_BouncerChaoticEdge.v · TM2 · on Submissions →
Rocq proof: check_kill PASS · first Oct 13 06:33
458 lines · 15 KB .v · compile 7.8 s · coqchk pass · 0 axioms · PASS Oct 13 06:33
· the .v file
Automatic review: 6 of 6 checks passtemplate: W5-8's kill file (kill 27) (twin: parent kill's .v) · details in Proof →
Class: Bouncer + Chaotic Edge
On the list: not on BB6_holdouts_663.txt (line 636 of the previous list) · historical 740 line 636
eqv ×1sim 1e15UBRRBA
Derived from: 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LFW5-8 Kill claimed

Your calls on file 1

next: post (Dennis): after W5-8 (214) and W5-8b (418), as a reply; first fix their drafts' '636 not formalized' sentences

Mechanism

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

Figures

Fig 1 · bbchallenge default view, 10,000 steps
The site's view. A bouncer: the head sweeps the whole tape, and the right side is ragged from the start.

Fig 2 · One double cycle: Even(212) to Even(244)Q1
Rows go down in time. Follow the dotted diagonal to the wall at left; compare the two halves.

Fig 3 · Right edge to 1e10 stepsQ2
One row per 12 trips. Each tooth is one run; look for any tooth that breaks the two-kind alternation.

More figures (1)Fig 4: Default view, 99,999 steps, wide window

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

rule	from ⟶ to	cases	steps	checked
Sea, right pass	C> 1^2k ⟶ (10)^k C>	any k >= 0	2k	✓200/200
Sea, left pass (composite 11 C>0)	0 (10)^k 1 1 C> 0 ⟶ 0 1 1 C> 0 1^2k	any k >= 0; the cell left of the block is 0	12k	✓200/200
Sea, left pass (composite B>000)	0 (10)^k B> 0 0 0 ⟶ 0 B> 0 0 0 1^2k	any k >= 0; used on the other trip phase	12k	✓200/200
S: 12 round trips	0^∞ <F G 1ⁿ 0 1^a 0 1² 0 1^b 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞ ⟶ 0^∞ <F G 1ⁿ⁺⁴⁸ 0 1^a-8 0 1² 0 1^b+4 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d+4 0 1² 0² 1² 0 1³ 0^∞	n odd >= 1; a even >= 10; b even >= 6; c odd >= 7; d even >= 2 (each bound is the smallest value that works; tested up to 2,000)	84n+84a+77b+70c+63d+13628	✓300/300
TE: P1 hits the wall (even to odd run)	0^∞ <F G 1ⁿ 0 1⁴ 0 1² 0 1^b 0⁶ 1³⁵ 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞ ⟶ 0^∞ <F G 1ⁿ⁺⁵⁵⁶ 0 1^b-86 0 1² 0 1⁸² 0⁶ 1^d+51 0 1² 0 1⁴ 0⁶ 1¹⁸ 0 1² 0² 1² 0 1³ 0^∞	n odd; b even, 88..3,000; d even, 20..2,000 (plus a 25 x 32 grid over b 100..676, d 20..392)	966n+952b+812d+455332 (138 round trips)	✓150/150
TO: P1 hits the wall (odd to even run)	0^∞ <F G 1ⁿ 0 1² 0 1² 0 1^b 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞ ⟶ 0^∞ <F G 1ⁿ⁺⁵⁸⁸ 0 1^b+c-91 0 1² 0 1^d+62 0⁶ 1³⁵ 0 1² 0 1⁴ 0⁶ 1¹⁸ 0 1² 0² 1² 0 1³ 0^∞	n odd; b even >= 82; c odd >= 37; d even >= 18 (half the tests on the reachable line c = b+11, d = b-64, half random)	1029n+1001b+987c+882d+458476 (147 round trips)	✓150/150
Double cycle	Even(n, x) = 0^∞ <F G 1ⁿ 0 1^x 0 1² 0 1^(x+76)/2 0⁶ 1³⁵ 0 1² 0 1⁴ 0⁶ 1¹⁸ 0 1² 0² 1² 0 1³ 0^∞ ⟶ Even(n+12x+808, x+32)	x = 4 mod 8, x >= 52, n odd. Tested: every x in 52..252, 16 random x up to 5,620, and all 16 even-run starts of the real run up to 1e10	S^((x-4)/8), TE, S^((x-52)/8), TO: 3x+201 round trips	✓42/42
Opening	blank tape, state A ⟶ Even(12863, 212) = 0^∞ <F G 1¹²⁸⁶³ 0 1²¹² 0 1² 0 1¹⁴⁴ 0⁶ 1³⁵ 0 1² 0 1⁴ 0⁶ 1¹⁸ 0 1² 0² 1² 0 1³ 0^∞	direct simulation; it is the first left record of round trip 3,209	153126993	✓1/1

Compressed historythe tape as 0^∞ <F 0² 1² 0 1⁴ 0 1² 0 1⁶ 0 1² 0 1⁵ 0² 1² 0 1⁵ 0 1² 0² 1ⁿ 0 1^a 0 1² 0 1^b 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞ at 35 moments: where the rules are read off

0^∞ <F 0² 1² 0 1⁴ 0 1² 0 1⁶ 0 1² 0 1⁵ 0² 1² 0 1⁵ 0 1² 0² 1ⁿ 0 1^a 0 1² 0 1^b 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞

step	`n`	`a`	`b`	`c`	`d`
4,097,897	1,959	34	68	45	18
18,629,265	4,351	46	86	89	18
70,933,037	8,675	110	86	133	18
123,039,285	11,503	134	82	157	18
153,126,993	12,863	212	144	35	18
198,114,311	14,667	162	82	173	18
241,393,559	16,215	244	160	35	18
303,350,077	18,211	194	82	189	18
363,208,093	19,951	276	176	35	18
445,948,083	22,139	226	82	205	18
526,157,923	24,071	308	192	35	18
633,882,729	26,451	258	82	221	18
738,604,521	28,575	340	208	35	18
875,902,559	31,147	290	82	237	18
1,009,683,503	33,463	372	224	35	18
1,181,530,261	36,227	322	82	253	18
1,349,304,629	38,735	404	240	35	18
1,561,062,667	41,691	354	82	269	18
1,768,151,803	44,391	436	256	35	18
2,025,570,753	47,539	386	82	285	18
2,277,683,073	50,431	468	272	35	18
2,586,899,639	53,771	418	82	301	18
2,890,130,631	56,855	500	288	35	18
3,257,668,589	60,387	450	82	317	18
3,618,500,813	63,663	532	304	35	18
4,051,271,011	67,387	482	82	333	18
4,476,574,099	70,855	564	320	35	18
4,981,874,457	74,771	514	82	349	18
5,478,905,113	78,431	596	336	35	18
6,064,420,623	82,539	546	82	365	18
6,640,822,623	86,391	628	352	35	18
7,314,625,349	90,691	578	82	381	18
7,978,429,541	94,735	660	368	35	18
8,748,978,619	99,227	610	82	397	18
9,508,602,923	103,463	692	384	35	18

nlast 103,463

alast 692

blast 384

clast 35

dlast 18

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

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

file: TranslatedBellv5.v:9
module: TM1
machine: 1RB0LA_1LC1LA_0RD0LB_0RE1RC_1LB0RF_1RD--- (11 transitions apart)
diff: different table, same proof architecture. The nearest proved table by transitions is 1RB0LA_1LC1RD_0RB0LC_1LA1RE_1LF0RD_---1LE (distance 3, RWL_mod_v5.v, a decider certificate with no macro rules to reuse)
note: TranslatedBellv5 TM1 proves block-macro rules with ES_v3's symbolic executor (es' a b c d e over word^^n tapes), repeats them with ind, chains them with follow, and ends with progress_nonhalt_cond. Ours needs the same tools for different rules: es' for S (5 variables), TE (3) and TO (4); ind for S^m; follow for the double cycle. The final step is progress_nonhalt_simple over x, since no extra invariant is needed. Bouncer_v2 TM1 shows es' handling a one-variable bouncer BigStep; Bouncer_v3's multistep_c' runs a long opening with nested small counters. New here: the es' calls must cover 12-, 138- and 147-trip stretches.

Proof & checks

6/6 automatic checks pass

Kill 29 · Bouncer + Chaotic Edge · the kill file 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v: 458 lines, 51 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (twin: parent kill's .v): W5-8's kill file (kill 27) · 64% of our lines identical · vs W5-8: same table, started in W5-8's E; different orbit

1What is provedCheck: the string, the theorem and every check_kill line are green, and the .v on disk is the one that was checked (same sha256).

Machine

1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA

vs holdout list

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

Theorem

✓ Lemma nonhalt: ~halts tm c0. L415

check_kill

✓ PASS · 17/17 checks pass · compile 7.84 s · coqchk pass (64.86 s) · assumptions: 0 (closed) · 2026-10-13 13:33:44 UTC · submission/check_kill.txt

Checked .v

sha256 8c597d875a112513…

✓	1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v	`8c597d875a112513…` = checked
✓	submission/1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v	`8c597d875a112513…` = 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`	15468 bytes, 458 lines, 251 sentences
✓	`framework`	HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓	`framework_build`	17 needed framework .vo files present and fresh, with native code no older than the .vo
✓	`forbidden`	none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)
✓	`structure`	6 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 35: TM_from_str "1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA" == <tm> (41 bytes)
✓	`theorem_text`	line 415: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 (<opam-switch>/bin/coqc)
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 7.8s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA") 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 (64.9s); its context summary lists nothing of the file's own
✓	`integrity`	input sha256 and framework HEAD/cleanliness identical before and after

2Same machine as W5-8?Check: every row of the table is ✓ under the computed renaming (or the listed differences are what status.json's relation says), the two pictures show the same bands, and the trajectory numbers agree with the claimed relation (a twin keeps a fixed small offset; a sibling's gap grows).

status.json names W5-8 as the parent (1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF); label: “W5-8c”; relation: “sibling of W5-8: W5-8's table with states renamed sigma = A->E, B->C, C->D, D->F, E->A, F->B (no mirror; the only map of 720 x 2), started in W5-8's state E; this run = sigma of the parent's table run from 0^inf E> 0^inf on the same tape (Lemma R)”; parent_note: “W5-8 (740 line 214), KILLED_NONHALT 2026-10-13 (check_kill PASS, sha256 beef54a5..cf48, independently re-verified); mirrored sibling W5-8b (740 line 418) also KILLED_NONHALT”. Everything below is computed from the two machine strings, not read from notes.

✓ Identical to W5-8's table under the renaming A→E, B→C, C→D, D→F, E→A, F→B (W5-8's state → this machine's), no mirror. This machine starts in W5-8's state E (W5-8 itself starts in A). The only such map.

W5-8	W5-8's row (read 0, read 1)	σ	predicted row: renamed by σ	this machine's actual row
A	`1RB` `1LD`	→ E	`1RC` `1LF`	`1RC` `1LF`	✓	start of W5-8
B	`0RC` `1RC`	→ C	`0RD` `1RD`	`0RD` `1RD`	✓
C	`1LA` `1RE`	→ D	`1LE` `1RA`	`1LE` `1RA`	✓
D	`---` `1LE`	→ F	`---` `1LA`	`---` `1LA`	✓
E	`1RF` `0RC`	→ A	`1RB` `0RD`	`1RB` `0RD`	✓	start of this machine
F	`0RB` `0LF`	→ B	`0RC` `0LB`	`0RC` `0LB`	✓

Rows aligned by σ: each of W5-8's states X sits next to this machine's state σ(X). ✓ = the actual row equals W5-8's row with every target state renamed by σ; --- (halt) must stay ---. Searched: all 720 renamings × with/without mirror.

default view of 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF — Fig P1 · **bbchallenge default view: W5-8 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: it starts in W5-8's state E, not A, so the first steps differ; the numbers below read: different orbit, so expect the same kind of bands, not the same picture.

default view of 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA — Fig P1 · **bbchallenge default view: W5-8 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: it starts in W5-8's state E, not A, so the first steps differ; the numbers below read: different orbit, so expect the same kind of bands, not the same picture.

blaze view of 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF — Fig P2 · **Long run, Blaze (speed): W5-8 and this machine, 100 million steps**
The macro behaviour, identical settings on both sides: each picture is its machine's own visited span stretched to 800 px, so compare the shape and order of the bands, not their absolute width. Speed mode samples one cell per column, so a one-cell shift can swap orange and white inside a band; compare band edges, not colours.

blaze view of 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA — Fig P2 · **Long run, Blaze (speed): W5-8 and this machine, 100 million steps**
The macro behaviour, identical settings on both sides: each picture is its machine's own visited span stretched to 800 px, so compare the shape and order of the bands, not their absolute width. Speed mode samples one cell per column, so a one-cell shift can swap orange and white inside a band; compare band edges, not colours.

Trajectory numbers, from blank (C core)

○ different orbit: 0.056% narrower at 1e9 (34,023 vs 34,042 cells; nonzeros 20,452 vs 23,290); not a fixed offset: the cell gap reaches -19

steps	cells visited (hi − lo + 1)			nonzeros
steps	W5-8	this	ratio (Δ)	W5-8	this	ratio (Δ)
1e5	315	331	1.0508 (+16)	285	203	0.7123 (-82)
1e6	1,078	1,087	1.0083 (+9)	591	932	1.5770 (+341)
1e7	3,442	3,429	0.9962 (-13)	2,350	3,381	1.4387 (+1,031)
1e8	10,784	10,794	1.0009 (+10)	6,620	9,227	1.3938 (+2,607)
1e9	34,042	34,023	0.9994 (-19)	23,290	20,452	0.8781 (-2,838)

Each machine from blank in its own start state, sim.py C core. Trajectory twin = cells and nonzeros stay within 16 of the parent's at every checkpoint (a fixed offset from a different start, not a growing gap). Cached in img/vs-parent.json (2026-10-16 10:29 PDT); --force recomputes.

3Where 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).

twin: parent kill's .v W5-8's kill file (kill 27) machines/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v · detected from status.json

64%of our lines identical to the template

31changed lines

101added lines (ours only)

25template lines dropped

23 / 16 / 12items identical / adapted / new

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

The template is the parent's kill file (adapted from busycoq's verify/TranslatedBellv5.v, Module TM1, ending with progress_nonhalt_simple as in verify/Bouncer_v2.v). Its macro rules, S_iter and DC are kept word for word on the parent's table, renamed tmP. New here: the opening init from E;; tape0 (ten cconfig_step pieces cut at left records), opening with its own 18 follows, and the renaming bridge of verify/Skelet15.v: perm : Perm tm tmP phi with busycoq's perm_halts (no flip, since there is no mirror). The file has 458 lines, every lemma top level.

Fig P3 · 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 364 lines

64% identical · 31 changed · 101 added

template 288 lines

81% kept verbatim · 25 not in ours

our items 51

23 identical · 16 adapted · 12 new · 0 template-only

identicalchanged / adaptedours only (new)template only

Template part: whole file, lines 21–361 (leading comment left out). Ours: lines 27–458 (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.

Other references found:

adapted from vendor/busycoq/verify/TranslatedBellv5.v Module TM1 (named in 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v line 12)

Side-by-side diff: template (288 lines) vs ours (364 lines), 157 lines differ; runs of identical lines and long template-only runs folded

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

template		ours
22	From BusyCoq Require Import Individual62.	28	From BusyCoq Require Import Individual62.
24	Require Import ZArith Lia.	30	Require Import ZArith Lia.
⋯ 2 identical lines (template 25–26, ours 31–32)
27	From BusyCoq Require Import ES_v3.	33	From BusyCoq Require Import ES_v3.
29	Definition tm := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").	35	Definition tm := Eval compute in (TM_from_str "1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA").
31	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
		37	(** tmP: the parent table. All configurations below are tmP's, in its coordinates. *)
32	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
		38	Definition tmP := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").
		40	Notation "c -->* c'" := (c -[ tmP ]->* c') (at level 40).
		41	Notation "c -->+ c'" := (c -[ tmP ]->+ c') (at level 40).
34	(** G: the fixed 43-cell gadget at the left end.	43	(** G: the fixed 43-cell gadget at the left end.
35	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d): F reads the 0 just left of G. *)	44	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d): F reads the 0 just left of G. *)
⋯ 80 identical lines (template 36–133, ours 45–142)
134	all: lia_refl.	143	all: lia_refl.
135	Qed.	144	Qed.
137	( Opening (write-up 5)	146	( Opening (write-up 2)
139	4,097,897 steps from the blank tape to K(1959,34,68,45,18), then 20 macro steps
		148	tmP from E;; tape0: 6,950,830 steps to K(2583,70,76,43,18) = Kr 1291 35 38 21 9,
140	to Even(12863,212) = Ev 6431 20.
		149	then 18 macro steps to Even(13299,220) = Ev 6649 21 (its own chain, write-up 2.2).
142	The direct run is cut at five left records (where the tape is short in run-length	151	The direct run is cut at nine left records (where the tape is short in run-length
143	form), so that no single computation is too large for the kernel. cc_steps runs	152	form), so that no single computation is too large for the kernel. cc_steps runs
144	busycoq's list configurations (cconfig_step); cc_steps' nests two counters as	153	busycoq's list configurations (cconfig_step); cc_steps' nests two counters as
⋯ 3 identical lines (template 145–147, ours 154–156)
148	\| O => Some x	157	\| O => Some x
149	\| S n0 =>	158	\| S n0 =>
150	match cconfig_step tm x with	159	match cconfig_step tmP x with
151	\| Some x0 => cc_steps n0 x0	160	\| Some x0 => cc_steps n0 x0
152	\| None => None	161	\| None => None
⋯ 6 identical lines (template 153–159, ours 162–168)
160	induction n; cbn[cc_steps]; intros x H.	169	induction n; cbn[cc_steps]; intros x H.
161	- inverts H. apply evstep_refl.	170	- inverts H. apply evstep_refl.
162	- pose proof (cconfig_step_spec tm x) as HE.	171	- pose proof (cconfig_step_spec tmP x) as HE.
163	destruct (cconfig_step tm x) as [x0\|]. 2: congruence.	172	destruct (cconfig_step tmP x) as [x0\|]. 2: congruence.
164	eapply evstep_step; eauto.	173	eapply evstep_step; eauto.
165	Qed.	174	Qed.
⋯ 36 identical lines (template 167–207, ours 176–216)
208	cbn [Str_app]. rewrite !Str_app_assoc. reflexivity.	217	cbn [Str_app]. rewrite !Str_app_assoc. reflexivity.
209	Qed.	218	Qed.
211	(** Left record at step 694,884. *)	220	(** Left record at step 694,787. *)
212	Definition W1 : list (nat*nat) :=	221	Definition W1 : list (nat*nat) :=
213	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,746);(2,20);(12,47);(1,20);(6,2);(2,4);(6,2);(1,2)])%nat.
		222	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,750);(1,2);(2,18);(2,34);(2,6);(1,2);(1,18);(1,2);(1,20)])%nat.
215	(** Left record at step 1,397,500. *)	224	(** Left record at step 1,378,765. *)
216	Definition W2 : list (nat*nat) :=	225	Definition W2 : list (nat*nat) :=
217	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1102);(1,2);(1,38);(1,2);(7,35);(1,22);(2,4);(1,2);(2,2);(2,4);(1,2)])%nat.	226	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1094);(3,50);(2,4);(1,49);(1,20)])%nat.
219	(** Left record at step 2,099,620. *)	228	(** Left record at step 2,077,151. *)
220	Definition W3 : list (nat*nat) :=	229	Definition W3 : list (nat*nat) :=
221	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1374);(2,132);(6,2);(2,4);(6,7);(1,2);(1,2);(1,2)])%nat.	230	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1362);(1,2);(2,4);(2,4);(6,71);(1,2);(1,54);(2,20);(1,2);(1,4);(1,2);(3,4);(1,2)])%nat.
223	(** Left record at step 2,790,296. *)	232	(** Left record at step 2,768,045. *)
224	Definition W4 : list (nat*nat) :=	233	Definition W4 : list (nat*nat) :=
225	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1599);(1,94);(1,2);(7,35);(1,20);(2,20);(1,2);(1,4);(1,2);(3,4);(1,2)])%nat.	234	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1586);(3,48);(2,4);(1,103);(1,29);(1,2);(1,7)])%nat.
227	(** Left record at step 3,493,040. *)	236	(** Left record at step 3,469,055. *)
228	Definition W5 : list (nat*nat) :=	237	Definition W5 : list (nat*nat) :=
229	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1798);(1,2);(2,58);(2,60);(2,44);(1,2);(1,4);(1,2);(1,4);(6,8);(3,6);(1,2)])%nat.	238	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1787);(2,14);(2,126);(2,58);(1,2);(1,4);(1,2);(1,4);(6,4);(11,4);(1,2)])%nat.
		240	(** Left record at step 4,155,515. *)
		241	Definition W6 : list (nat*nat) :=
		242	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1971);(2,170);(2,4);(6,19);(1,6);(1,2);(2,2);(2,8);(1,2)])%nat.
		244	(** Left record at step 4,854,845. *)
		245	Definition W7 : list (nat*nat) :=
		246	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,2139);(2,142);(2,44);(2,26);(1,2);(1,7)])%nat.
		248	(** Left record at step 5,552,637. *)
		249	Definition W8 : list (nat*nat) :=
		250	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,2295);(1,118);(1,2);(1,52);(6,43);(1,2);(1,4);(6,4);(11,4);(1,2)])%nat.
		252	(** Left record at step 6,254,851. *)
		253	Definition W9 : list (nat*nat) :=
		254	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,2442);(3,92);(6,62);(2,2);(2,46);(3,2);(2,2);(2,10);(1,2);(1,6);(2,2);(2,4);(1,2)])%nat.
231	Lemma init1:	256	Lemma init1:
232	c0 -->* LR W1.
		257	E;; tape0 -->* LR W1.
233	Proof.	258	Proof.
234	change c0 with (cconfig_to_config ([], [], 0, A)).	259	change (E;; tape0) with (cconfig_to_config ([], [], 0, E)).
235	unfold LR.	260	unfold LR.
236	apply (cc_steps'_spec 694 1000 884).	261	apply (cc_steps'_spec 694 1000 787).
237	vm_compute.	262	vm_compute.
238	reflexivity.	263	reflexivity.
⋯ 3 identical lines (template 239–242, ours 264–267)
243	Proof.	268	Proof.
244	unfold LR.	269	unfold LR.
245	apply (cc_steps'_spec 702 1000 616).	270	apply (cc_steps'_spec 683 1000 978).
246	vm_compute.	271	vm_compute.
247	reflexivity.	272	reflexivity.
⋯ 3 identical lines (template 248–251, ours 273–276)
252	Proof.	277	Proof.
253	unfold LR.	278	unfold LR.
254	apply (cc_steps'_spec 702 1000 120).	279	apply (cc_steps'_spec 698 1000 386).
255	vm_compute.	280	vm_compute.
256	reflexivity.	281	reflexivity.
⋯ 3 identical lines (template 257–260, ours 282–285)
261	Proof.	286	Proof.
262	unfold LR.	287	unfold LR.
263	apply (cc_steps'_spec 690 1000 676).	288	apply (cc_steps'_spec 690 1000 894).
264	vm_compute.	289	vm_compute.
265	reflexivity.	290	reflexivity.
⋯ 3 identical lines (template 266–269, ours 291–294)
270	Proof.	295	Proof.
271	unfold LR.	296	unfold LR.
272	apply (cc_steps'_spec 702 1000 744).	297	apply (cc_steps'_spec 701 1000 10).
273	vm_compute.	298	vm_compute.
274	reflexivity.	299	reflexivity.
275	Qed.	300	Qed.
277	Lemma init6:	302	Lemma init6:
278	LR W5 -->* Kr 979 17 34 22 9.
		303	LR W5 -->* LR W6.
		304	Proof.
		305	unfold LR.
		306	apply (cc_steps'_spec 686 1000 460).
		307	vm_compute.
		308	reflexivity.
		309	Qed.
		311	Lemma init7:
		312	LR W6 -->* LR W7.
		313	Proof.
		314	unfold LR.
		315	apply (cc_steps'_spec 699 1000 330).
		316	vm_compute.
		317	reflexivity.
		318	Qed.
		320	Lemma init8:
		321	LR W7 -->* LR W8.
		322	Proof.
		323	unfold LR.
		324	apply (cc_steps'_spec 697 1000 792).
		325	vm_compute.
		326	reflexivity.
		327	Qed.
		329	Lemma init9:
		330	LR W8 -->* LR W9.
		331	Proof.
		332	unfold LR.
		333	apply (cc_steps'_spec 702 1000 214).
		334	vm_compute.
		335	reflexivity.
		336	Qed.
		338	Lemma init10:
		339	LR W9 -->* Kr 1291 35 38 21 9.
279	Proof.	340	Proof.
280	unfold LR.	341	unfold LR.
281	rewrite Kr_cc.	342	rewrite Kr_cc.
282	apply (cc_steps'_spec 604 1000 857).	343	apply (cc_steps'_spec 695 1000 979).
283	vm_compute.	344	vm_compute.
284	reflexivity.	345	reflexivity.
285	Qed.	346	Qed.
287	Lemma init:	348	Lemma init:
288	c0 -->* Kr 979 17 34 22 9.
		349	E;; tape0 -->* Kr 1291 35 38 21 9.
289	Proof.	350	Proof.
290	follow init1.	351	follow init1.
⋯ 2 identical lines (template 291–292, ours 352–353)
293	follow init4.	354	follow init4.
294	follow init5.	355	follow init5.
295	apply init6.
		356	follow init6.
		357	follow init7.
		358	follow init8.
		359	follow init9.
		360	apply init10.
296	Qed.	361	Qed.
298	Lemma opening:	363	Lemma opening:
299	Kr 979 17 34 22 9 -->* Ev 6431 20.
		364	Kr 1291 35 38 21 9 -->* Ev 6649 21.
300	Proof.	365	Proof.
301	unfold Ev.	366	unfold Ev.
302	follow (S_iter 4 979 0 31 19 8).	367	follow (S_iter 8 1291 2 35 18 8).
303	follow (TO' 1075 1 4 8).	368	follow (T6' 1483 13 4 16).
304	follow (S_iter 4 1369 2 45 14 8).	369	follow (S_iter 7 1779 1 53 14 8).
305	follow (T6' 1465 15 0 8).
		370	follow (TE' 1947 26 13).
306	follow (S_iter 6 1761 3 45 14 8).	371	follow (S_iter 6 2225 2 38 45 8).
307	follow (T8' 1905 16 11).
		372	follow (T6' 2369 12 31 12).
308	follow (S_iter 5 2175 2 40 41 8).
		373	follow (S_iter 13 2665 3 49 14 8).
309	follow (T6' 2295 12 27 10).
		374	follow (T8' 2977 34 25).
310	follow (S_iter 12 2591 3 47 14 8).	375	follow (S_iter 10 3247 0 40 55 8).
311	follow (T8' 2879 30 23).
		376	follow (TO' 3487 22 40 20).
312	follow (S_iter 9 3149 0 40 53 8).
		377	follow (S_iter 18 3781 3 57 14 8).
313	follow (TO' 3365 20 38 18).
		378	follow (T8' 4213 52 35).
314	follow (S_iter 17 3659 3 55 14 8).
		379	follow (S_iter 14 4483 2 40 65 8).
315	follow (T8' 4067 48 33).
		380	follow (T6' 4819 30 51 28).
316	follow (S_iter 13 4337 2 40 63 8).
		381	follow (S_iter 23 5115 1 65 14 8).
317	follow (T6' 4649 28 49 26).
		382	follow (TE' 5667 70 45).
318	follow (S_iter 22 4945 1 63 14 8).	383	follow (S_iter 17 5945 2 38 77 8).
319	follow (TE' 5473 66 43).
		384	follow (T6' 6353 34 63 34).
320	follow (S_iter 16 5751 2 38 75 8).
321	follow (T6' 6135 32 61 32).
322	finish.	385	finish.
323	Qed.	386	Qed.
325	Lemma nonhalt: ~halts tm c0.	388	Lemma nonhaltP: ~halts tmP (E;; tape0).
326	Proof.	389	Proof.
327	eapply multistep_nonhalt.	390	eapply multistep_nonhalt.
328	1: { follow init. apply opening. }	391	1: { follow init. apply opening. }
329	apply (progress_nonhalt_simple tm (nat*nat) (fun p => Ev (fst p) (snd p)) (6431,20)).	392	apply (progress_nonhalt_simple tmP (nat*nat) (fun p => Ev (fst p) (snd p)) (6649,21)).
330	intros [N X].	393	intros [N X].
331	exists (48*X+716+N, 4+X).	394	exists (48*X+716+N, 4+X).
332	apply DC.	395	apply DC.
333	Qed.	396	Qed.
		398	( The relation (write-up 1)
		400	phi = sigma^-1 maps this machine's states to tmP's. Every cell (q, s) of tm is
		401	tmP's cell (phi q, s) with every target state t replaced by phi t (same symbol,
		402	same move), so tm and tmP are equal up to renaming, and phi A = E. *)
		403	Definition phi (q : Q) : Q :=
		404	match q with
		405	\| A => E \| B => F \| C => B \| D => C \| E => A \| F => D
		406	end.
		408	Lemma perm: Perm tm tmP phi.
		409	Proof.
		410	split.
		411	- intros [] [] H; cbn in *; try discriminate; reflexivity.
		412	- intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
		413	Qed.
		415	Lemma nonhalt: ~halts tm c0.
		416	Proof.
		417	intros H.
		418	change (halts tm (A;; tape0)) in H.
		419	exact (nonhaltP (perm_halts _ _ _ _ _ perm H)).
		420	Qed.
335	(*	422	(*
336	1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (only D0 undefined; D is entered only by A1 = 1LD)	423	1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA (only F0 undefined; F is entered only by E1 = 1LF)
		424	= tmP 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF with its states renamed (no mirror)
		425	sigma = A->E, B->C, C->D, D->F, E->A, F->B (phi = sigma^-1); start A = sigma(E)
		427	relation c --tmP--> c' iff sigma c --tm--> sigma c' (same tape and head, state q -> sigma q)
		428	sigma (E;; tape0) = c0, so tm's run is sigma of tmP's run from E;; tape0
		430	below, configurations are tmP's (left records); tm sees the same tapes with state sigma q (K: B instead of F)
338	G = 0^2 1^2 0 1^4 0 1^2 0 1^6 0 1^2 0 1^5 0^2 1^2 0 1^5 0 1^2 0^2 (43 cells)	432	G = 0^2 1^2 0 1^4 0 1^2 0 1^6 0 1^2 0 1^5 0^2 1^2 0 1^5 0 1^2 0^2 (43 cells)
339	K(n,a,b,c,d) = 0^inf <F G 1^n 0 1^a 0110 1^b 0^6 1^c 0110 1111 0^6 1^d 0110 0110 111 0^inf	433	K(n,a,b,c,d) = 0^inf <F G 1^n 0 1^a 0110 1^b 0^6 1^c 0110 1111 0^6 1^d 0110 0110 111 0^inf
		434	sigma K = 0^inf <B G 1^n 0 1^a 0110 1^b 0^6 1^c 0110 1111 0^6 1^d 0110 0110 111 0^inf
340	Even(n,x) = K(n, x, (x+76)/2, 35, 18)	435	Even(n,x) = K(n, x, (x+76)/2, 35, 18)
341	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d) Ev N X = Even(2N+1, 8X+52)	436	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d) Ev N X = Even(2N+1, 8X+52)
		438	tmP's rules (tmP's coordinates):
343	R1 C> 1 1 --> 1 0 C> 2 steps C1 E1	439	R1 C> 1 1 --> 1 0 C> 2 steps C1 E1
344	R2b 0 1 0 B> 0 0 0 --> 0 B> 0 0 0 1 1 12 steps B0 C0 A0 B1 C0 A1 D1 E0 F1 F1 F1 F0	440	R2b 0 1 0 B> 0 0 0 --> 0 B> 0 0 0 1 1 12 steps B0 C0 A0 B1 C0 A1 D1 E0 F1 F1 F1 F0
⋯ 9 identical lines (template 345–355, ours 441–451)
356	n odd, x = 4 mod 8, x >= 52; 3x+201 trips	452	n odd, x = 4 mod 8, x >= 52; 3x+201 trips
357	(Rocq: Ev N X -->+ Ev (48X+716+N) (X+4))	453	(Rocq: Ev N X -->+ Ev (48X+716+N) (X+4))
359	start c0 -->(4,097,897) K(1959,34,68,45,18) --(S^4 TO S^4 T6 S^6 T8 S^5 T6 S^12 T8 S^9 TO S^17 T8 S^13 T6 S^22 TE S^16 T6)-->
		455	start E;; tape0 -(6,950,830)-> K(2583,70,76,43,18) --(S^8 T6 S^7 TE S^6 T6 S^13 T8 S^10 TO S^18 T8 S^14 T6 S^23 TE S^17 T6)-->
360	Even(12863,212) at step 153,126,993; then DC forever (x = 212, 244, 276, ...)	456	Even(13299,220) at step 163,638,058; then DC forever (x = 220, 252, 284, ...)
		457	(the same for tm from c0, through sigma)
361	*)	458	*)

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

51 items in 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v (458 lines): 31 Lemma, 17 Definition, 3 Fixpoint. Tags against the template: identical = same name and same text once each file's own TM string is <TM> (marked "except the TM string" when that is the only difference); adapted = same name, different text; new = no item of that name in the template part.

#	kind	name	statement (no proof body)	line	vs template
1	Definition	`tm`	Definition tm := Eval compute in (TM_from_str "1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA").	L35	identicalexcept the TM string
2	Definition	`tmP`	Definition tmP := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").	L38	new
3	Definition	`G`	Definition G : list sym := [0;0;1;1;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;0;1;1;0;1;1;1;1;1;0;0;1;1;0;1;1;1;1;1;0;1;1;0;0].	L45	identical
4	Definition	`Kr`	Definition Kr n a b c d := 0inf <{{F}} G > [1] > [1;1]^^n > [0] > [1;1]^^a > [0;1;1;0] > [1;1]^^b > [0;0;0;0;0;0] > [1] > [1;1]^^c > [0;1;1;0;1;1;1;1;0;0;0;0;0;0] > [1;1]^^d > [0;1;1;0;0;1;1;0;1;1;1] *> 0inf.	L48	identical
5	Lemma	`S_step`	Lemma S_step n a b c d: Kr n (5+a) (3+b) (3+c) (1+d) -->+ Kr (24+n) (1+a) (5+b) (3+c) (3+d).	L59	identical
6	Lemma	`TE`	Lemma TE n b d: Kr n 2 (44+b) 17 (10+d) -->+ Kr (278+n) (1+b) 41 (35+d) 9.	L66	identical
7	Lemma	`TO`	Lemma TO n b c d: Kr n 1 (41+b) (18+c) (9+d) -->+ Kr (294+n) (14+b+c) (40+d) 17 9.	L73	identical
8	Lemma	`T6`	Lemma T6 n b c d: Kr n 3 (41+b) (17+c) (9+d) -->+ Kr (296+n) (13+b+c) (40+d) 17 9.	L80	identical
9	Lemma	`T8`	Lemma T8 n b d: Kr n 4 (44+b) 17 (10+d) -->+ Kr (270+n) (7+b) 43 (33+d) 9.	L87	identical
10	Lemma	`S_step'`	Lemma S_step' n a b c d: Kr n (5+a) (3+b) (3+c) (1+d) -->* Kr (24+n) (1+a) (5+b) (3+c) (3+d).	L93	identical
11	Lemma	`TE'`	Lemma TE' n b d: Kr n 2 (44+b) 17 (10+d) -->* Kr (278+n) (1+b) 41 (35+d) 9.	L97	identical
12	Lemma	`TO'`	Lemma TO' n b c d: Kr n 1 (41+b) (18+c) (9+d) -->* Kr (294+n) (14+b+c) (40+d) 17 9.	L101	identical
13	Lemma	`T6'`	Lemma T6' n b c d: Kr n 3 (41+b) (17+c) (9+d) -->* Kr (296+n) (13+b+c) (40+d) 17 9.	L105	identical
14	Lemma	`T8'`	Lemma T8' n b d: Kr n 4 (44+b) 17 (10+d) -->* Kr (270+n) (7+b) 43 (33+d) 9.	L109	identical
15	Lemma	`S_iter`	Lemma S_iter k: forall n a b c d, Kr n (4k+1+a) (3+b) (3+c) (1+d) --> Kr (24k+n) (1+a) (2k+3+b) (3+c) (2*k+1+d).	L114	identical
16	Definition	`Ev`	Definition Ev N X := Kr N (4X+26) (2X+32) 17 9.	L128	identical
17	Lemma	`prog_eq`	Lemma prog_eq c1 c2 c1' c2': c1 -->+ c2 -> c1 = c1' -> c2 = c2' -> c1' -->+ c2'.	L130	identical
18	Lemma	`DC`	Lemma DC N X: Ev N X -->+ Ev (48*X+716+N) (4+X).	L134	identical
19	Fixpoint	`cc_steps`	Fixpoint cc_steps (n:nat) (x:cconfig) : option cconfig := match n with \| O => Some x \| S n0 => match cconfig_step tmP x with \| Some x0 => cc_steps n0 x0 … +3 lines	L155	adapted
20	Lemma	`cc_steps_spec`	Lemma cc_steps_spec n x y: cc_steps n x = Some y -> cconfig_to_config x -->* cconfig_to_config y.	L165	adapted
21	Fixpoint	`cc_steps'`	Fixpoint cc_steps' (n1 n2 n3:nat) (x:cconfig) : option cconfig := match n1 with \| O => cc_steps n3 x \| S n1 => match cc_steps n2 x with \| Some x0 => cc_steps' n1 n2 n3 x0 … +3 lines	L176	identical
22	Lemma	`cc_steps'_spec`	Lemma cc_steps'_spec n1 n2 n3 x y: cc_steps' n1 n2 n3 x = Some y -> cconfig_to_config x -->* cconfig_to_config y.	L186	identical
23	Fixpoint	`rl`	Fixpoint rl (xs : list (nat*nat)) : list sym := match xs with \| [] => [] \| (z,o)::t => [0]^^z ++ [1]^^o ++ rl t end.	L199	identical
24	Definition	`LR`	Definition LR (xs : list (natnat)) : Q tape := cconfig_to_config ([], rl xs, 0, F).	L206	identical
25	Definition	`Kr_list`	Definition Kr_list n a b c d : list sym := G ++ [1] ++ [1;1]^^n ++ [0] ++ [1;1]^^a ++ [0;1;1;0] ++ [1;1]^^b ++ [0;0;0;0;0;0] ++ [1] ++ [1;1]^^c ++ [0;1;1;0;1;1;1;1;0;0;0;0;0;0] ++ [1;1]^^d ++ [0;1;1;0;0;1;1;0;1;1;1].	L208	identical
26	Lemma	`Kr_cc`	Lemma Kr_cc n a b c d: Kr n a b c d = cconfig_to_config ([], Kr_list n a b c d, 0, F).	L213	identical
27	Definition	`W1`	Definition W1 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,750);(1,2);(2,18);(2,34);(2,6);(1,2);(1,18);(1,2);(1,20)])%nat.	L221	adapted
28	Definition	`W2`	Definition W2 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1094);(3,50);(2,4);(1,49);(1,20)])%nat.	L225	adapted
29	Definition	`W3`	Definition W3 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1362);(1,2);(2,4);(2,4);(6,71);(1,2);(1,54);(2,20);(1,2);(1,4);(1,2);(3,4);(1,2)])%nat.	L229	adapted
30	Definition	`W4`	Definition W4 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1586);(3,48);(2,4);(1,103);(1,29);(1,2);(1,7)])%nat.	L233	adapted
31	Definition	`W5`	Definition W5 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1787);(2,14);(2,126);(2,58);(1,2);(1,4);(1,2);(1,4);(6,4);(11,4);(1,2)])%nat.	L237	adapted
32	Definition	`W6`	Definition W6 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1971);(2,170);(2,4);(6,19);(1,6);(1,2);(2,2);(2,8);(1,2)])%nat.	L241	new
33	Definition	`W7`	Definition W7 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,2139);(2,142);(2,44);(2,26);(1,2);(1,7)])%nat.	L245	new
34	Definition	`W8`	Definition W8 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,2295);(1,118);(1,2);(1,52);(6,43);(1,2);(1,4);(6,4);(11,4);(1,2)])%nat.	L249	new
35	Definition	`W9`	Definition W9 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,2442);(3,92);(6,62);(2,2);(2,46);(3,2);(2,2);(2,10);(1,2);(1,6);(2,2);(2,4);(1,2)])%nat.	L253	new
36	Lemma	`init1`	Lemma init1: E;; tape0 -->* LR W1.	L256	adapted
37	Lemma	`init2`	Lemma init2: LR W1 -->* LR W2.	L266	adapted
38	Lemma	`init3`	Lemma init3: LR W2 -->* LR W3.	L275	adapted
39	Lemma	`init4`	Lemma init4: LR W3 -->* LR W4.	L284	adapted
40	Lemma	`init5`	Lemma init5: LR W4 -->* LR W5.	L293	adapted
41	Lemma	`init6`	Lemma init6: LR W5 -->* LR W6.	L302	adapted
42	Lemma	`init7`	Lemma init7: LR W6 -->* LR W7.	L311	new
43	Lemma	`init8`	Lemma init8: LR W7 -->* LR W8.	L320	new
44	Lemma	`init9`	Lemma init9: LR W8 -->* LR W9.	L329	new
45	Lemma	`init10`	Lemma init10: LR W9 -->* Kr 1291 35 38 21 9.	L338	new
46	Lemma	`init`	Lemma init: E;; tape0 -->* Kr 1291 35 38 21 9.	L348	adapted
47	Lemma	`opening`	Lemma opening: Kr 1291 35 38 21 9 -->* Ev 6649 21.	L363	adapted
48	Lemma	`nonhaltP`	Lemma nonhaltP: ~halts tmP (E;; tape0).	L388	new
49	Definition	`phi`	Definition phi (q : Q) : Q := match q with \| A => E \| B => F \| C => B \| D => C \| E => A \| F => D end.	L403	new
50	Lemma	`perm`	Lemma perm: Perm tm tmP phi.	L408	new
51	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L415	adapted

5What 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)
submission/parent-proof.md · the parent's proof, as shipped
proof.md (working copy) · differs from the submitted copy

submission/proof.md line 123: 1.4 The parent's rules carry over

Each rule of the parent is an exact run of the parent's table: the shift rules R1 and R2b, the macro rules S, TE, TO, T6 and T8 (P§1, P§3). By Lemma R each is an exact run of this machine too, with the same domain and the same step count.

In particular the double cycle (P§4) holds here in the form

sigma Even(n, x)  -->  sigma Even(n + 12x + 808, x + 32)        (n odd, x = 4 mod 8, x >= 52)

From here on, configurations are written in the parent's coordinates, as members K(...) of the parent's table run from E. On this machine they are read through σ.

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

3 machines, 3 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-8 kill 27	`1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF`	✓Killed: never halts	parent link; = W5-8c's table, run from state E; named in W5-8c's .v header; named in W5-8c's proof.md; named in W5-8c's notes.md · review · compared side by side above · mechanism
W5-8b kill 28	`1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF`	✓Killed: never halts	= W5-8c's table mirrored, run from state D; named in W5-8c's proof.md; named in W5-8b's notes.md · review
W5-8c kill 29	`1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA`	✓Killed: never halts	this kill

7ChecklistCheck: 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 672 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 64.86 s
✓
.v hash matches the checked hash
.v = checked sha256 8c597d875a11…; submission/ copy = checked sha256 8c597d875a11…
✓
No repo-local paths in the .v
comments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own verify/X.v is fine: none in the .v or the submission/ copy
✓
Public write-up is clean
tools/writeup_lint.py on submission/proof.md: 0 error(s)
○
proof.md reviewed by Dennis (Checkpoint B)
no Checkpoint B note from Dennis found
- notes.md L61: - Checkpoint B (Dennis, non-blocking).
- proof.md L286: ## 8. Checkpoint B (Dennis)
○
Family posted together?
2 other kill(s) in the family: W5-8, W5-8b; the Discord draft names 2 of them

Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.0 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 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA

Files

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

name	size	changed
notes.md ↓	9.0 KB	2026-10-13 06:39
proof.md ↓	17 KB	2026-10-13 06:23
how_proved.md ↓	1.6 KB	2026-10-14 10:51
status.json ↓	5.3 KB	2026-10-16 10:28
1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v ↓	15 KB	2026-10-13 06:27
img/	5 items	2026-10-16 10:29
rocq/	12 items	2026-10-13 06:32
scripts/	7 items	2026-10-13 06:18
submission/	6 items	2026-10-14 09:18
work/	13 items	2026-10-13 06:23
check_proof.py ↓	33 KB	2026-10-13 06:13

status.json in full

{
 "tm": "1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA",
 "label": "W5-8c",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-13",
 "reason": "check_kill PASS, independently re-verified",
 "confidence": "high",
 "parent": "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF",
 "parent_note": "W5-8 (740 line 214), KILLED_NONHALT 2026-10-13 (check_kill PASS, sha256 beef54a5..cf48, independently re-verified); mirrored sibling W5-8b (740 line 418) also KILLED_NONHALT",
 "relation": "sibling of W5-8: W5-8's table with states renamed sigma = A->E, B->C, C->D, D->F, E->A, F->B (no mirror; the only map of 720 x 2), started in W5-8's state E; this run = sigma of the parent's table run from 0^inf E> 0^inf on the same tape (Lemma R)",
 "holdout_line_740": 636,
 "checks": {
  "byte_exact_740": "line 636, exactly once, no CR",
  "claims": "none: sheet Results row = class 'Bouncer + Chaotic Edge' only (no status/notes/sources/done-by), level-0 row status '-', classifications only in the 'Bouncer + Chaotic Edge' column; Discord only mxdys's UBRRBA_TODO list (data/discord/2026-08-24_mxdys_ubrrba_86.txt line 87, next to W5-8b (85) and W5-8 (86)), an acceleration to-do list, not a claim",
  "upstream_9cf9e88": "not proved: no .v in the 9cf9e88 verify tree contains any of the 1,440 renaming/mirror variants of the table; tools/holdouts.py solved: absent from verify/",
  "canon": "canon(this, start A) == canon(parent, start E) (check_proof REL and the scratchpad starts.py canon: 1LB0LC_0LD0RB_1RE1LA_0LC1LC_1LD1RF_---1RA for both)",
  "eqv_1590": "singleton group (line 1879 of 2026-10-07_eqv_1590.txt)"
 },
 "opening": "blank --(6,950,830 direct steps)--> sigma K(2583,70,76,43,18) (state B; first K-shaped left record, any state), then 18 macro steps by the parent's rules S^8 T6 S^7 TE S^6 T6 S^13 T8 S^10 TO S^18 T8 S^14 T6 S^23 TE S^17 T6 (own chain, not the parent's) -> sigma Even(13299,220) at step 163,638,058; from there the parent's double cycle (x = 220 + 32j; no adjusted invariant)",
 "proof_md": "proof.md (working delta proof); public write-up submission/proof.md (writeup_lint 0/0) + submission/parent-proof.md",
 "check_proof": {
  "result": "PASS",
  "claims": "83/83 seed 1 default (105 s), 83/83 seed 2 default (106 s), 83/83 seed 1 --full (373 s; orbit to 1e10: 30 even/odd run starts, 1,606 K-shaped left records all predicted); each re-ran the parent's check_proof.py in the same mode (196/196); DOC/OPEN/INV/PLAN re-run 39/39 after the last prose pass",
  "out": [
   "work/check_proof_seed1.log",
   "work/check_proof_seed2.log",
   "work/check_proof_full_seed1.log",
   "work/parent_check_proof_default_seed1.log",
   "work/parent_check_proof_default_seed2.log",
   "work/parent_check_proof_full_seed1.log",
   "work/check_proof_doc_after_prose.log"
  ],
  "teeth": "n=2585 in the opening start -> 9 checks FAIL (OPEN, PLAN, DOC); wrong sigma -> REL (4) + DOC fail; S^7 instead of S^8 in row 1 -> 6 OPEN checks fail; one wrong step number in proof.md -> DOC fails; one wrong follow argument -> PLAN fails",
  "cross_check": "C K-scanner (scripts/kscan.c) and an independent regex scan (lrec.c + Python) give the same 126 K-shaped left records up to 163,638,058 for the parent's table from E and for this machine from A; tools/sim.py events: first K-shaped left record at 6,950,830"
 },
 "open_lemmas": [],
 "next": "post (Dennis): after W5-8 (214) and W5-8b (418), as a reply; first fix their drafts' '636 not formalized' sentences",
 "workflow_name": "W5-8c",
 "template": "W5-8b's kill file (parent development on tmP + Perm bridge as verify/Skelet15.v), without flip",
 "kill": {
  "file": "1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v",
  "lines": 458,
  "sha256": "8c597d875a1125131e6a9f88fe63fc994b55df1ccecaba84b2c1d29909d00584",
  "route": "parent's kill file with its table as tmP; init E;; tape0 -->* Kr 1291 35 38 21 9 (6,950,830 steps, ten cconfig_step pieces at left records); opening = 18 follows to Ev 6649 21; nonhaltP by progress_nonhalt_simple; perm : Perm tm tmP phi + perm_halts (no flip)",
  "check_kill": "PASS round 1 (2026-10-13T13:28:27Z, rocq/check_kill_r1.log); audit PASS (2026-10-13T13:30:46Z); fresh PASS 2026-10-13T13:33:44Z (rocq/check_kill_final.log): compile 7.84 s native, coqchk -norec pass 64.86 s, 0 assumptions",
  "submission": "submission/ (.v, proof.md, parent-proof.md, check_kill.txt, README.md, discord.md; not posted)"
 },
 "alias_labels": [
  "W5-8e"
 ],
 "redispatch_2026-10-13": "re-dispatched as W5-8e (delta-proof task); already KILLED_NONHALT as W5-8c, nothing redone. Re-checked: byte-exact 740 line 636 (once, no CR); canon(this,A)==canon(parent,E)=1LB0LC_0LD0RB_1RE1LA_0LC1LC_1LD1RF_---1RA (E the only parent start that matches); .v sha256 8c597d87..0584 unchanged (= submission copy = rocq/check_kill_final.log PASS); check_proof logs 83/83 (seeds 1,2 default; seed 1 --full); upstream 9cf9e88 verify tree has no file with this string, the parent's or W5-8b's; no sheet/Discord snapshot newer than this status (newest 2026-10-09)",
 "pr": "https://github.com/ccz181078/busycoq/pull/27",
 "pr_state": "merged",
 "pr_file": "verify/M_1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_HHH1LA.v",
 "pr_opened": "2026-10-15T22:48:31Z",
 "pr_comments": 0,
 "pr_head_sha": "94903f626ae503be6be39ac40e53038ab98ac4d8",
 "posted": "2026-10-15 (Discord; user confirmed sent)",
 "pr_merged_at": "2026-10-16T07:09:03Z",
 "pr_merged_by": "ccz181078"
}

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