BB(6) hunt
Machines / #4b

1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA

#4blocal proof 11Kill claimedSync bouncer counterbbchallenge ↗Explorerparent: #4

How we proved it never halts

#4's proof, from a different start

#4 keeps a binary counter at the left end of the tape and a row of five-cell blocks to its right, "A" blocks 00111 and "B" blocks 10111. Each time the counter rolls over, a marker walks right through the A blocks and then turns all the B blocks into A blocks. #4b is #4's table with its state letters shuffled, started in the state that is #4's F instead of A, so watching it you see the same picture with different numbers.

Renaming states changes nothing the machine does to the tape, so all of #4's proof holds here as it stands. That includes the two formulas that take the block counts from one cycle start to the next (one for an even A count, one for odd), and the six-sided safe region that both formulas map into itself.

What is new is the opening. After 16,590 steps #4b is at a cycle start with 14 A blocks ahead of the marker and 4 B blocks beyond them, where #4 has 16 and 0 after 17,215 steps. That point is also inside the safe region, so from there the region argument keeps the run on the rails forever and the missing transition is never used. The two runs are not copies of each other: their even/odd choices already differ in the second cycle.

The Rocq proof is #4's file with the states renamed and the opening replaced. Every tape move is re-proved on #4b's own table by running it, and the first 16,590 steps are replayed exactly.

#11local proof number
510lines of Rocq
7 sto compile
6/6automatic checks
space-time diagram, first 10,000 steps from blank
The first 10,000 steps from a blank tape. Time runs down; white is 1.
About this picture

The standard picture (bbchallenge.org's Default view): each row is the whole tape at one step, time runs downward, and the head's path draws the pattern.

bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited

Overview

In one sentence

Kill #4's table renamed EDBCFA, started in #4's F: same rules and hexagon; new base S(6,14,4) at step 16,590

Submitted mechanism #4's table, different start. Renaming the states by σ = EDBCFA (A→E, B→D, C→B, D→C, E→F, F→A), with no mirror, turns #4's table into this one. σ is the only one of the 720 × 2 maps that does. This machine starts in A = σ(F), so it runs #4's machine from 0^inf F> 0^inf. That is a different orbit of the same macro map, not #4's own run. (submission/README.md, Mechanism)

parent 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC--- (#4)

Upstream
Kill claimed · PR #24merged 2026-10-16 07:07 UTC by ccz181078 · SBCv13.v · TM2 · on Submissions →
Rocq proof
check_kill PASS · first Oct 10 12:25
510 lines · 21 KB .v · compile 7.0 s · coqchk pass · 0 axioms · PASS Oct 10 12:25
· the .v file
Automatic review
6 of 6 checks passtemplate: #4's kill file (kill 2) (twin: parent kill's .v) · details in Proof →
Class
Sync bouncer counterours: Sync bouncer counter (sheet) · ours adds: kill #4's table renamed EDBCFA (no mirror), started in #4's F · high confidence
On the list
not on BB6_holdouts_663.txt (line 14 of the previous list) · historical 740 line 14
eqv ×2sim 1e15UBRRBAlongit.
Derived from
1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---#4 Kill claimed

Mechanism

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

How it works: 3 notes
  • Same machine as kill #4 up to state names (A->E, B->D, C->B, D->C, E->F, F->A); it starts in #4's F, so its orbit differs.
  • Same words and rules as #4: binary counter (1010/0010) on the left, A/B blocks 00111/10111 and a front 111 on the right; R1-R5o.
  • From blank it reaches S(6,14,4) = Q(7,65,1,14,4) at step 16,590, inside #4's hexagon (facet 4Y+2Z >= N tight); #4's cycle lemma does the rest.

Figures for Checkpoint A

Fig 1 · Left/right records to 2.7M stepsQ1

Same view as the first figure on #4's card. Overflow resets are record rows 78, 122, 306, 390, 1,139.

Left/right records to 2.7M steps
bbchallenge-defaultStart blankRows left/right recordsWindow cells -20..1385, 1 px = 0.5 cellsColors 1 0 or never visited head just moved right/left
Rows: the start, then one row each time the head reaches a new leftmost or rightmost cell (1,406 rows, steps 0..2,700,000; rows are not equal time) · Window: each cell is 2x2 px
Fig 2 · One cycle from the base, every 50 stepsQ2

Starts at the base S(6,14,4). Top: front steps; middle: conversion; then bounces until the overflow at the bottom.

One cycle from the base, every 50 steps
bbchallenge-defaultStart mid-run: step 16,590Rows every 50 stepsWindow cells -130..177, 1 px = 0.5 cellsColors 1 0 or never visited head just moved right/left
Start: the real tape there is exactly Q(7,65,1,14,4) with head B; rebuilt from that formula and checked identical · Rows: (1,166 rows: steps 16,590..74,840; S(7,25,29) follows at step 74,884), so one bounce spans many rows · Window: (each cell is 2x2 px); cell 0 = the head cell at step 16,590, i.e. real cells -16..291
More figures (2)Fig 3–4: Initial segment, every 16 steps · bbchallenge default view, first 10,000 steps
Fig 3 · Initial segment, every 16 steps

Steps 0 to 16,576: the run before the base. Rule-governed from step 1,711 (about row 107).

Initial segment, every 16 steps
bbchallenge-defaultStart blankRows every 16 stepsWindow cells -14..112, 1 px = 0.5 cellsColors 1 0 or never visited head just moved right/left
Rows: 1,037 rows: steps 0..16,576; the base follows at step 16,590 · Window: each cell is 2x2 px
Fig 4 · bbchallenge default view, first 10,000 steps

The site's view: a bouncer growing to the right from an almost fixed left end.

bbchallenge default view, first 10,000 steps
bbchallenge-defaultStart blankRows every step 0..10,000Window cells -200..199, 1 px = 1 cellColors 1 0 or never visited head just moved right/left
Rows: squeezed 20:1 into 500 px as on bbchallenge.org (px row y blends steps 20y+9 and 20y+10)
Rules (7/7 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
R1 P-bounce
0∞ C_k(n) (00111)X (10111)z 00 B> 0∞
⟶ 0∞ C_k(n+1) (00111)X (10111)z+1 00 B> 0∞
n+1 <= 2^k-132X+32z+16t(n)+47, t(n) = trailing 1-bits of n✓40/40
R2 overflow
0∞ C_k(2k-1) (00111)X (10111)z 00 B> 0∞
⟶ 0∞ C_(k+1)(2k+1) 00111 111 (00111)X-2 (10111)z+1 00 B> 0∞
X >= 232X+32z+16k+61✓40/40
R3 front step
0∞ C_k(n) (00111)x 111 (00111)y+2 (10111)z 00 B> 0∞
⟶ 0∞ C_k(n+3) (00111)x+2 111 (00111)y (10111)z+1 00 B> 0∞
n+3 <= 2^k-1, x >= 196x+32y+32z+16(t(n)+t(n+1)+t(n+2))+197✓40/40
R4 even conversion
0∞ C_k(n) (00111)x 111 (10111)z 00 B> 0∞
⟶ 0∞ C_k(n+z+2) (00111)x+z+1 00 B> 0∞
n+z+2 <= 2^k-1—✓40/40
R5 odd conversion
0∞ C_k(n) (00111)x 111 00111 (10111)z 00 B> 0∞
⟶ 0∞ C_k(n+2z+7) (00111)x+z+4 00 B> 0∞
n+2z+7 <= 2^k-1—✓40/40
R5o odd conversion + overflow
0∞ C_k(n) (00111)x 111 00111 (10111)z 00 B> 0∞
⟶ 0∞ C_(k+1)(2k+1+3m) (00111)1+2m 111 (00111)x+z+2-2m 00 B> 0∞
m = n+2z+7-2^k >= 0, x+z+2-2m >= 1, 3m <= 2^k-2—✓40/40
R4o (remark, never used)
0∞ C_k(n) (00111)x 111 (10111)z 00 B> 0∞
⟶ 0∞ C_(k+1)(2k+1+3m) (00111)1+2m 111 (00111)x+z-1-2m 00 B> 0∞
m = n+z+2-2^k >= 0, x+z-1-2m >= 1, 3m <= 2^k-2—✓40/40
Compressed historythe tape as 0∞ C_k(n) (00111)x [111 (00111)y] (10111)z 00 B> 0∞ at 38 moments: where the rules are read off
0∞ C_k(n) (00111)x [111 (00111)y] (10111)z 00 B> 0∞
stepphaseknxyz
1,711Q520310
3,047P5277-0
4,371P5317-4
4,864Q633155
6,186Q639517
14,036P66016-0
15,825P66316-3
16,590Q7651144
25,889Q78615011
34,947P79927-0
72,951P712727-28
74,884Q812912529
109,472Q816525141
248,150P825470-0
250,437P825570-1
252,898Q92571682
428,172Q935969036
535,510P9397106-0
1,135,428P9511106-114
1,142,673Q105131104115
1,733,589Q106691050167
2,759,783P10838273-0
4,932,158P101,023273-185
4,947,035Q111,0251271186
8,405,806Q111,4302711321
17,498,220Q122,142635320
29,322,686Q122,9405950266
35,576,808P123,208862-0
72,673,681P124,095862-887
72,729,902Q134,0971860888
111,659,028Q135,38786101,318
175,916,622P136,7072,180-0
314,746,210P138,1912,180-1,484
314,863,727Q148,19312,1781,485
537,600,100Q1411,4602,17902,574
823,412,430P1414,0364,754-0
1,268,701,603P1416,3834,754-2,347
1,268,929,120Q1516,38514,7522,348
phaselast Q
not plottable
klast 15
1551,7111.3e9log xstep 1711: k = 5step 3047: k = 5step 4371: k = 5step 4864: k = 6step 6186: k = 6step 14036: k = 6step 15825: k = 6step 16590: k = 7step 25889: k = 7step 34947: k = 7step 72951: k = 7step 74884: k = 8step 109472: k = 8step 248150: k = 8step 250437: k = 8step 252898: k = 9step 428172: k = 9step 535510: k = 9step 1135428: k = 9step 1142673: k = 10step 1733589: k = 10step 2759783: k = 10step 4932158: k = 10step 4947035: k = 11step 8405806: k = 11step 17498220: k = 12step 29322686: k = 12step 35576808: k = 12step 72673681: k = 12step 72729902: k = 13step 111659028: k = 13step 175916622: k = 13step 314746210: k = 13step 314863727: k = 14step 537600100: k = 14step 823412430: k = 14step 1268701603: k = 14step 1268929120: k = 15
nlast 16,385
16,385201,7111.3e9log xstep 1711: n = 20step 3047: n = 27step 4371: n = 31step 4864: n = 33step 6186: n = 39step 14036: n = 60step 15825: n = 63step 16590: n = 65step 25889: n = 86step 34947: n = 99step 72951: n = 127step 74884: n = 129step 109472: n = 165step 248150: n = 254step 250437: n = 255step 252898: n = 257step 428172: n = 359step 535510: n = 397step 1135428: n = 511step 1142673: n = 513step 1733589: n = 669step 2759783: n = 838step 4932158: n = 1023step 4947035: n = 1025step 8405806: n = 1430step 17498220: n = 2142step 29322686: n = 2940step 35576808: n = 3208step 72673681: n = 4095step 72729902: n = 4097step 111659028: n = 5387step 175916622: n = 6707step 314746210: n = 8191step 314863727: n = 8193step 537600100: n = 11460step 823412430: n = 14036step 1268701603: n = 16383step 1268929120: n = 16385
xlast 1
4,75411,7111.3e9log xstep 1711: x = 3step 3047: x = 7step 4371: x = 7step 4864: x = 1step 6186: x = 5step 14036: x = 16step 15825: x = 16step 16590: x = 1step 25889: x = 15step 34947: x = 27step 72951: x = 27step 74884: x = 1step 109472: x = 25step 248150: x = 70step 250437: x = 70step 252898: x = 1step 428172: x = 69step 535510: x = 106step 1135428: x = 106step 1142673: x = 1step 1733589: x = 105step 2759783: x = 273step 4932158: x = 273step 4947035: x = 1step 8405806: x = 271step 17498220: x = 63step 29322686: x = 595step 35576808: x = 862step 72673681: x = 862step 72729902: x = 1step 111659028: x = 861step 175916622: x = 2180step 314746210: x = 2180step 314863727: x = 1step 537600100: x = 2179step 823412430: x = 4754step 1268701603: x = 4754step 1268929120: x = 1
ylast 4,752
4,75201,7111.3e9log xstep 1711: y = 1step 4864: y = 5step 6186: y = 1step 16590: y = 14step 25889: y = 0step 74884: y = 25step 109472: y = 1step 252898: y = 68step 428172: y = 0step 1142673: y = 104step 1733589: y = 0step 4947035: y = 271step 8405806: y = 1step 17498220: y = 532step 29322686: y = 0step 72729902: y = 860step 111659028: y = 0step 314863727: y = 2178step 537600100: y = 0step 1268929120: y = 4752
zlast 2,348
2,57401,7111.3e9log xstep 1711: z = 0step 3047: z = 0step 4371: z = 4step 4864: z = 5step 6186: z = 7step 14036: z = 0step 15825: z = 3step 16590: z = 4step 25889: z = 11step 34947: z = 0step 72951: z = 28step 74884: z = 29step 109472: z = 41step 248150: z = 0step 250437: z = 1step 252898: z = 2step 428172: z = 36step 535510: z = 0step 1135428: z = 114step 1142673: z = 115step 1733589: z = 167step 2759783: z = 0step 4932158: z = 185step 4947035: z = 186step 8405806: z = 321step 17498220: z = 0step 29322686: z = 266step 35576808: z = 0step 72673681: z = 887step 72729902: z = 888step 111659028: z = 1318step 175916622: z = 0step 314746210: z = 1484step 314863727: z = 1485step 537600100: z = 2574step 823412430: z = 0step 1268701603: z = 2347step 1268929120: z = 2348
Template comparisontemplate: applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB---
B0LC1RF
C1LE0RD
D0RB1RC
E1RD0LE
F0RC1RA
file
—
module
—
machine
1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC--- (11 transitions apart)
diff
none after renaming states by EDBCFA (no mirror); without renaming every cell differs. Start = #4's F
note
Template = kill #4's passing .v (machines/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---, sha256 51e3dea1...). Delta: TM string, {{A}}->{{E}}, {{C}}->{{B}}, {{E}}->{{F}}, a 16,590-step esx init to CfgF 5 0 14 4; cycle_step/Inv verbatim. rocq/plan_check.v compiles (6.7 s, closed).
Proof strategy & riskshow the formal proof will go · 2 risks to watch

Delta of kill #4 (proof.md section 5): #4's .v with state names renamed by EDBCFA and a new init (one 16,590-step esx to CfgF 5 0 14 4). cycle_step, Inv and all macro lemmas verbatim. rocq/plan_check.v already compiles; next: clean kill file + check_kill.

  • ▲None found in the argument: the base sits on the hexagon facet 4Y+2Z >= N (tight, 64 = 64), which Inv allows (<=); #4's base is tight on the same facet.
  • ▲On mxdys's UBRRBA_TODO and dyuan01's longitudinal lists (fair game per Dennis); re-read those threads before posting.
Stats & provenance3·109 steps simulated · 47,451 cells · the status in full · files
simulated
3·109 steps
tape
47,451 cells · 18,841 nonzeros
growth
span ~ t^0.5 (cycle k: ~2^k blocks in ~4^k steps); left edge -2 cells per cycle; 29,054 cells at 1e9 vs #4's 23,607
status now
check_kill PASS, independently re-verified (status.json, 2026-10-10)
observer's note
Relation to kill #4 established by simulation (unique renaming EDBCFA, lockstep, rules on the twin's table, base in the hexagon, orbit 9/9 cycle states to 5.04e9); delta proof.md validated (live status in status.json: CHECKPOINT_B).
files
observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v

Proof & checks

6/6 automatic checks pass

Kill 11 · Sync bouncer counter · the kill file 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v: 510 lines, 73 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (twin: parent kill's .v): #4's kill file (kill 2) · 87% of our lines identical · vs #4: same table, started in #4's F; 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
1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA
vs holdout list
✓ byte-exact: the .v literal (L23) == 2026-10-07_778.txt line 17 (41 bytes, via tools/holdouts.py)
Theorem
✓ Lemma nonhalt: ~halts tm c0. L471
check_kill
✓ PASS · 17/17 checks pass · compile 6.96 s · coqchk pass (2.11 s) · assumptions: 0 (closed) · 2026-10-10 19:25:15 UTC · submission/check_kill.txt
Checked .v
sha256 0c89b5109f87c793…
✓1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v0c89b5109f87c793… = checked
✓submission/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v0c89b5109f87c793… = checked
Status
✓Killed: never halts updated 2026-10-10
✓ args✓ input✓ framework✓ framework_build✓ forbidden✓ structure✓ tm_text✓ theorem_text✓ coq✓ names✓ compile✓ tm_rocq✓ theorem_rocq✓ isolation✓ assumptions✓ coqchk✓ integrity
All 17 check_kill checks with their one-line results
✓args6x2 machine, framework module Individual62, mode nonhalt
✓input21411 bytes, 510 lines, 532 sentences
✓frameworkHEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓framework_build13 needed framework .vo files present and fresh, with native code no older than the .vo
✓forbiddennone of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)
✓structure4 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓tm_textline 23: TM_from_str "1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA" == <tm> (41 bytes)
✓theorem_textline 471: nonhalt : ~halts tm c0
✓coqcoqc 8.20.1 ([local working file]
✓nameshalts, c0, TM_from_str resolved inside Individual62
✓compilecompiled in 7.0s with all appended checks
✓tm_rocqBB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA" by eq_refl (in-file and isolated)
✓theorem_rocqnonhalt : ~ halts (TM_from_str "1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA") c0 with absolute names (in-file and isolated)
✓isolationonly stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off
✓assumptions0 assumption(s), all in the baseline
✓coqchkcoqchk -norec BB6Kill.Candidate ok (2.1s); its context summary lists nothing of the file's own
✓integrityinput sha256 and framework HEAD/cleanliness identical before and after
2Same machine as #4?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 #4 as the parent (1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---); label: “#4b”; relation: “same transition table as #4 (states renamed), started in a different state; found by the family sweep”; parent_note: “1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC--- (#4)”. Everything below is computed from the two machine strings, not read from notes.

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

#4#4's row (read 0, read 1)σpredicted row: renamed by σthis machine's actual row
A1RB 0LA→ E1RD 0LE1RD 0LE✓start of #4
B0RC 1RD→ D0RB 1RC0RB 1RC✓
C0LD 1RE→ B0LC 1RF0LC 1RF✓
D1LA 0RB→ C1LE 0RD1LE 0RD✓
E0RD 1RF→ F0RC 1RA0RC 1RA✓
F1RC ---→ A1RB ---1RB ---✓start of this machine

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

Fig P1 · bbchallenge default view: #4 and this machine, first 10,000 steps

Same view, same settings on both sides. Look for the same band structure: it starts in #4's state F, not A, so the first steps differ; the numbers below read: different orbit, so expect the same kind of bands, not the same picture.

#4 (parent), from blank in its A
default view of 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---
this machine (#4b), from blank in its A = #4's F
default view of 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA
bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited
tools/diagram.py <tm> --as-site (the site's 400×500 canvas)
Fig P2 · Long run, Blaze (speed): #4 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.

#4 (parent), from blank in its A
blaze view of 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---
763 rows of 131,072 steps · 1,301 columns, every 8th cell · nonzeros 3,580 at 1e8
this machine (#4b), from blank in its A = #4's F
blaze view of 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA
763 rows of 131,072 steps · 1,308 columns, every 8th cell · nonzeros 3,210 at 1e8
bbchallenge-blazeStart blankRows steps 0 → 1e8Window the visited spanColors 1 0 at the sampled cell
Rows: one snapshot per row (Blaze time blocks), stretched to 500 px · Window: every k-th cell sampled, stretched to 800 px
tools/diagram.py <tm> --mode blaze --speed --as-site --steps 1e8

Trajectory numbers, from blank (C core)

○ different orbit: 23% wider at 1e9 (29,054 vs 23,607 cells; nonzeros 12,016 vs 11,358); not a fixed offset: the cell gap reaches +5,447

stepscells visited (hi − lo + 1)nonzeros
#4thisratio (Δ)#4thisratio (Δ)
1e53533581.0142 (+5)1201160.9667 (-4)
1e67721,0341.3394 (+262)4296941.6177 (+265)
1e72,6773,0151.1263 (+338)1,3711,1740.8563 (-197)
1e810,40310,4531.0048 (+50)3,5793,2090.8966 (-370)
1e923,60729,0541.2307 (+5,447)11,35812,0161.0579 (+658)

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:28 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 #4's kill file (kill 2) machines/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v · detected from status.json
87%of our lines identical to the template
52changed lines
2added lines (ours only)
1template lines dropped
28 / 45 / 0items identical / adapted / new
What the package README says it reused and changed (submission/README.md line 17, Template and what changed), quoted:

It extends kill #4's .v (504 lines; in #4's own package), which extends SBCv7.v Module TM4. A script applied proof.md §5, with every substitution count asserted:

  • the TM string;
  • σ applied to every state name {{X}}: {{A}}→{{E}} 37 times, {{C}}→{{B}} 6, {{E}}→{{F}} 35;
  • init0/init (16,590 steps to CfgF 5 0 14 4) and the start index (5,0,14,4);
  • the header and the rule-table comment.

After the renaming, 4 code lines differ from #4's .v. The counter, the Gad conversion gadget (R4/R5/R5o), Inv and cycle_step are #4's text. It compiled and passed check_kill on the first attempt. 510 lines, imports only Individual62.

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 429 lines
87% identical · 52 changed · 2 added
template 428 lines
88% kept verbatim · 1 not in ours
our items 73
28 identical · 45 adapted · 0 new · 0 template-only
identicalchanged / adaptedours only (new)template only
Template part: whole file, lines 13–504 (leading comment left out). Ours: lines 18–510 (header comment 1–17 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:

Side-by-side diff: template (428 lines) vs ours (429 lines), 55 lines differ; runs of identical lines and long template-only runs folded
identicalequal once each TM string is <TM>changedours onlytemplate only
templateours
14From BusyCoq Require Import Individual62.19From BusyCoq Require Import Individual62.
15Require Import Arith Lia.20Require Import Arith Lia.
⋯ 16 identical lines (template 16–38, ours 21–43)
39Proof. intros H E. subst. exact H. Qed.44Proof. intros H E. subst. exact H. Qed.
41(** * Shift rules (proof.md 3.1) *)46(** * Shift rules (proof.md 3.1) *)
43Lemma ENDL l : l <* <[0;0] {{C}}> 0inf -->+ l <{{A}} [0;0;1] *> 0inf. Proof. es. Qed.48Lemma ENDL l : l <* <[0;0] {{B}}> 0inf -->+ l <{{E}} [0;0;1] *> 0inf. Proof. es. Qed.
44Lemma AL l r : l <* bA <{{A}} [0;0;1] *> r -->* l <{{A}} [0;0;1] *> bAr *> r. Proof. es. Qed.49Lemma AL l r : l <* bA <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> bAr *> r. Proof. es. Qed.
45Lemma BL l r : l <* bB <{{A}} [0;0;1] *> r -->* l <{{A}} [0;0;1] *> bBr *> r. Proof. es. Qed.50Lemma BL l r : l <* bB <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> bBr *> r. Proof. es. Qed.
46Lemma AR l r : l <* <[0;0;1] {{E}}> bAr *> r -->* l <* bA <* <[0;0;1] {{E}}> r. Proof. es. Qed.51Lemma AR l r : l <* <[0;0;1] {{F}}> bAr *> r -->* l <* bA <* <[0;0;1] {{F}}> r. Proof. es. Qed.
47Lemma BR l r : l <* <[0;0;1] {{E}}> bBr *> r -->* l <* bB <* <[0;0;1] {{E}}> r. Proof. es. Qed.52Lemma BR l r : l <* <[0;0;1] {{F}}> bBr *> r -->* l <* bB <* <[0;0;1] {{F}}> r. Proof. es. Qed.
48Lemma ENDR l : l <* <[0;0;1] {{E}}> 0inf -->* l <* bB <* <[0;0] {{C}}> 0inf. Proof. es. Qed.53Lemma ENDR l : l <* <[0;0;1] {{F}}> 0inf -->* l <* bB <* <[0;0] {{B}}> 0inf. Proof. es. Qed.
49Lemma D1L l r : l <* d1 <{{A}} [0;0;1] *> r -->* l <{{A}} [0;0;1] *> [0;1;0;1] *> r. Proof. es. Qed.54Lemma D1L l r : l <* d1 <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> [0;1;0;1] *> r. Proof. es. Qed.
50Lemma FLIP l r : l <* d0 <{{A}} [0;0;1] *> r -->* l <* d1 <* <[0;0;1] {{E}}> r. Proof. es. Qed.55Lemma FLIP l r : l <* d0 <{{E}} [0;0;1] *> r -->* l <* d1 <* <[0;0;1] {{F}}> r. Proof. es. Qed.
51Lemma D0R l r : l <* <[0;0;1] {{E}}> [0;1;0;1] *> r -->* l <* d0 <* <[0;0;1] {{E}}> r. Proof. es. Qed.56Lemma D0R l r : l <* <[0;0;1] {{F}}> [0;1;0;1] *> r -->* l <* d0 <* <[0;0;1] {{F}}> r. Proof. es. Qed.
52Lemma D0R' l r : l <* <[0;0;1] {{E}}> [0;1] *> [0;1;0;1] *> r -->* l <* d0 <* <[0;0;1] {{E}}> [0;1] *> r.57Lemma D0R' l r : l <* <[0;0;1] {{F}}> [0;1] *> [0;1;0;1] *> r -->* l <* d0 <* <[0;0;1] {{F}}> [0;1] *> r.
53Proof. es. Qed.58Proof. es. Qed.
54Lemma OVL r : 0inf <{{A}} [0;0;1] *> [0;1;0;1] *> r -->* 0inf <* d1 <* <[0;0;1] {{E}}> [0;1] *> r.59Lemma OVL r : 0inf <{{E}} [0;0;1] *> [0;1;0;1] *> r -->* 0inf <* d1 <* <[0;0;1] {{F}}> [0;1] *> r.
55Proof. es. Qed.60Proof. es. Qed.
56Lemma OVR l r : l <* <[0;0;1] {{E}}> [0;1] *> bAr *> r -->* l <* d0 <{{A}} [0;0;1] *> [1;0;1] *> r.61Lemma OVR l r : l <* <[0;0;1] {{F}}> [0;1] *> bAr *> r -->* l <* d0 <{{E}} [0;0;1] *> [1;0;1] *> r.
57Proof. es. Qed.62Proof. es. Qed.
58Lemma FL l r : l <* bA <* <[1;1;1] <{{A}} [0;0;1] *> r -->* l <{{A}} [0;0;1] *> [0;0;1] *> bBr *> r.63Lemma FL l r : l <* bA <* <[1;1;1] <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> [0;0;1] *> bBr *> r.
59Proof. es. Qed.64Proof. es. Qed.
60Lemma FR1 l r : l <* <[0;0;1] {{E}}> [0;0;1] *> bBr *> r -->* l <* bA <{{A}} [0;0;1] *> [0;0;1] *> r.65Lemma FR1 l r : l <* <[0;0;1] {{F}}> [0;0;1] *> bBr *> r -->* l <* bA <{{E}} [0;0;1] *> [0;0;1] *> r.
61Proof. es. Qed.66Proof. es. Qed.
62Lemma FR2 l r : l <* <[0;0;1] {{E}}> [0;0;1] *> bAr *> r -->* l <* bA <{{A}} [0;0;1] *> [1;0;1] *> r.67Lemma FR2 l r : l <* <[0;0;1] {{F}}> [0;0;1] *> bAr *> r -->* l <* bA <{{E}} [0;0;1] *> [1;0;1] *> r.
63Proof. es. Qed.68Proof. es. Qed.
64Lemma FR3 l r : l <* <[0;0;1] {{E}}> [1;0;1] *> bAr *> r -->* l <* bA <* <[1;1;1] <* <[0;0;1] {{E}}> r.69Lemma FR3 l r : l <* <[0;0;1] {{F}}> [1;0;1] *> bAr *> r -->* l <* bA <* <[1;1;1] <* <[0;0;1] {{F}}> r.
65Proof. es. Qed.70Proof. es. Qed.
66Lemma FR4 l r : l <* <[0;0;1] {{E}}> [1;0;1] *> bBr *> r -->* l <{{A}} [0;0;1] *> [0;0;1] *> bAr *> r.71Lemma FR4 l r : l <* <[0;0;1] {{F}}> [1;0;1] *> bBr *> r -->* l <{{E}} [0;0;1] *> [0;0;1] *> bAr *> r.
67Proof. es. Qed.72Proof. es. Qed.
68Lemma FE0 l : l <* <[0;0;1] {{E}}> [0;0;1] *> 0inf -->* l <* bA <* <[0;0] {{C}}> 0inf.73Lemma FE0 l : l <* <[0;0;1] {{F}}> [0;0;1] *> 0inf -->* l <* bA <* <[0;0] {{B}}> 0inf.
69Proof. es. Qed.74Proof. es. Qed.
70Lemma FE1 l : l <* <[0;0;1] {{E}}> [1;0;1] *> 0inf -->* l <{{A}} [0;0;1] *> [0;0;1] *> [0;0;1] *> 0inf.75Lemma FE1 l : l <* <[0;0;1] {{F}}> [1;0;1] *> 0inf -->* l <{{E}} [0;0;1] *> [0;0;1] *> [0;0;1] *> 0inf.
71Proof. es. Qed.76Proof. es. Qed.
72Lemma FE2 l : l <* <[0;0;1] {{E}}> [0;0;1] *> [0;0;1] *> 0inf -->* l <* bA <{{A}} [0;0;1] *> [1] *> 0inf.77Lemma FE2 l : l <* <[0;0;1] {{F}}> [0;0;1] *> [0;0;1] *> 0inf -->* l <* bA <{{E}} [0;0;1] *> [1] *> 0inf.
73Proof. es. Qed.78Proof. es. Qed.
74Lemma FE3 l : l <* <[0;0;1] {{E}}> [1] *> 0inf -->* l <{{A}} [0;0;1] *> [0;0;1;1] *> 0inf.79Lemma FE3 l : l <* <[0;0;1] {{F}}> [1] *> 0inf -->* l <{{E}} [0;0;1] *> [0;0;1;1] *> 0inf.
75Proof. es. Qed.80Proof. es. Qed.
76Lemma FE4 l : l <* <[0;0;1] {{E}}> [0;0;1;1] *> 0inf -->* l <* bA <{{A}} [0;0;1] *> [0;0;1] *> 0inf.81Lemma FE4 l : l <* <[0;0;1] {{F}}> [0;0;1;1] *> 0inf -->* l <* bA <{{E}} [0;0;1] *> [0;0;1] *> 0inf.
77Proof. es. Qed.82Proof. es. Qed.
79(** * Repeated rules (proof.md 3.2) *)84(** * Repeated rules (proof.md 3.2) *)
81Lemma ALs a : forall l r, l <* bA^^a <{{A}} [0;0;1] *> r -->* l <{{A}} [0;0;1] *> bAr^^a *> r.86Lemma ALs a : forall l r, l <* bA^^a <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> bAr^^a *> r.
82Proof.87Proof.
83 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow AL; follow IH; rewrite lpow_shift'; finish].88 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow AL; follow IH; rewrite lpow_shift'; finish].
84Qed.89Qed.
85Lemma BLs a : forall l r, l <* bB^^a <{{A}} [0;0;1] *> r -->* l <{{A}} [0;0;1] *> bBr^^a *> r.90Lemma BLs a : forall l r, l <* bB^^a <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> bBr^^a *> r.
86Proof.91Proof.
87 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow BL; follow IH; rewrite lpow_shift'; finish].92 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow BL; follow IH; rewrite lpow_shift'; finish].
88Qed.93Qed.
89Lemma ARs a : forall l r, l <* <[0;0;1] {{E}}> bAr^^a *> r -->* l <* bA^^a <* <[0;0;1] {{E}}> r.94Lemma ARs a : forall l r, l <* <[0;0;1] {{F}}> bAr^^a *> r -->* l <* bA^^a <* <[0;0;1] {{F}}> r.
90Proof.95Proof.
91 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow AR; follow IH; rewrite <-lpow_shift'; finish].96 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow AR; follow IH; rewrite <-lpow_shift'; finish].
92Qed.97Qed.
93Lemma BRs a : forall l r, l <* <[0;0;1] {{E}}> bBr^^a *> r -->* l <* bB^^a <* <[0;0;1] {{E}}> r.98Lemma BRs a : forall l r, l <* <[0;0;1] {{F}}> bBr^^a *> r -->* l <* bB^^a <* <[0;0;1] {{F}}> r.
94Proof.99Proof.
95 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow BR; follow IH; rewrite <-lpow_shift'; finish].100 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow BR; follow IH; rewrite <-lpow_shift'; finish].
96Qed.101Qed.
97Lemma D1Ls a : forall l r, l <* d1^^a <{{A}} [0;0;1] *> r -->* l <{{A}} [0;0;1] *> [0;1;0;1]^^a *> r.102Lemma D1Ls a : forall l r, l <* d1^^a <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> [0;1;0;1]^^a *> r.
98Proof.103Proof.
99 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow D1L; follow IH; rewrite lpow_shift'; finish].104 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow D1L; follow IH; rewrite lpow_shift'; finish].
100Qed.105Qed.
101Lemma D0R's a : forall l r, l <* <[0;0;1] {{E}}> [0;1] *> [0;1;0;1]^^a *> r -->* l <* d0^^a <* <[0;0;1] {{E}}> [0;1] *> r.106Lemma D0R's a : forall l r, l <* <[0;0;1] {{F}}> [0;1] *> [0;1;0;1]^^a *> r -->* l <* d0^^a <* <[0;0;1] {{F}}> [0;1] *> r.
102Proof.107Proof.
103 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow D0R'; follow IH; rewrite <-lpow_shift'; finish].108 induction a as [|a IH]; intros; [finish | rewrite !lpow_S, !Str_app_assoc; follow D0R'; follow IH; rewrite <-lpow_shift'; finish].
⋯ 13 identical lines (template 104–121, ours 109–126)
123(** CTR: one increment, n+1 <= 2^k - 1 *)128(** CTR: one increment, n+1 <= 2^k - 1 *)
124Lemma CTR k : forall n r, S n < 2^k ->129Lemma CTR k : forall n r, S n < 2^k ->
125 ctr k n <{{A}} [0;0;1] *> r -->* ctr k (S n) <* <[0;0;1] {{E}}> r.130 ctr k n <{{E}} [0;0;1] *> r -->* ctr k (S n) <* <[0;0;1] {{F}}> r.
126Proof.131Proof.
127 induction k as [|k IH]; intros n r H.132 induction k as [|k IH]; intros n r H.
⋯ 29 identical lines (template 128–159, ours 133–164)
161(** OV: the counter overflows; it gains a digit and a new front 111 appears *)166(** OV: the counter overflows; it gains a digit and a new front 111 appears *)
162Lemma OV k r :167Lemma OV k r :
163 ctr (S k) (2^(S k) - 1) <{{A}} [0;0;1] *> bAr *> bAr *> r -->*168 ctr (S k) (2^(S k) - 1) <{{E}} [0;0;1] *> bAr *> bAr *> r -->*
164 ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* <[0;0;1] {{E}}> r.169 ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* <[0;0;1] {{F}}> r.
165Proof.170Proof.
166 rewrite ctr_ones, ctr_ov.171 rewrite ctr_ones, ctr_ov.
⋯ 3 identical lines (template 167–169, ours 172–174)
171(** RT: a round trip of the head through the counter (no overflow) *)176(** RT: a round trip of the head through the counter (no overflow) *)
172Lemma RT K n a r : S n < 2^K ->177Lemma RT K n a r : S n < 2^K ->
173 ctr K n <* bA^^a <{{A}} [0;0;1] *> r -->* ctr K (S n) <* bA^^a <* <[0;0;1] {{E}}> r.178 ctr K n <* bA^^a <{{E}} [0;0;1] *> r -->* ctr K (S n) <* bA^^a <* <[0;0;1] {{F}}> r.
174Proof.179Proof.
175 intros H. fw ALs. fw CTR. fw ARs. finish.180 intros H. fw ALs. fw CTR. fw ARs. finish.
176Qed.181Qed.
178(** OVRT: a round trip that overflows the counter *)183(** OVRT: a round trip that overflows the counter *)
179Lemma OVRT k a r :184Lemma OVRT k a r :
180 ctr (S k) (2^(S k) - 1) <* bA^^(S (S a)) <{{A}} [0;0;1] *> r -->*185 ctr (S k) (2^(S k) - 1) <* bA^^(S (S a)) <{{E}} [0;0;1] *> r -->*
181 ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* bA^^a <* <[0;0;1] {{E}}> r.186 ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* bA^^a <* <[0;0;1] {{F}}> r.
182Proof.187Proof.
183 fw ALs. rewrite !lpow_S, !Str_app_assoc. fw OV. fw ARs. finish.188 fw ALs. rewrite !lpow_S, !Str_app_assoc. fw OV. fw ARs. finish.
184Qed.189Qed.
186(** QC: one step of the front (3 round trips, the front moves 2 blocks right) *)191(** QC: one step of the front (3 round trips, the front moves 2 blocks right) *)
187Lemma QC K n x y r : 3 + n < 2^K ->192Lemma QC K n x y r : 3 + n < 2^K ->
188 ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^(S (S y)) <{{A}} [0;0;1] *> r -->*193 ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^(S (S y)) <{{E}} [0;0;1] *> r -->*
189 ctr K (3 + n) <* bA^^(S (S (S x))) <* <[1;1;1] <* bA^^y <* <[0;0;1] {{E}}> r.194 ctr K (3 + n) <* bA^^(S (S (S x))) <* <[1;1;1] <* bA^^y <* <[0;0;1] {{F}}> r.
190Proof.195Proof.
191 intros H.196 intros H.
⋯ 10 identical lines (template 192–201, ours 197–206)
202Qed.207Qed.
204(** * Configurations at the right edge (proof.md 1) *)209(** * Configurations at the right edge (proof.md 1) *)
206Definition Pc K n X z := ctr K n <* bA^^X <* bB^^z <* <[0;0] {{C}}> 0inf.211Definition Pc K n X z := ctr K n <* bA^^X <* bB^^z <* <[0;0] {{B}}> 0inf.
207Definition Qc K n x y z := ctr K n <* bA^^x <* <[1;1;1] <* bA^^y <* bB^^z <* <[0;0] {{C}}> 0inf.212Definition Qc K n x y z := ctr K n <* bA^^x <* <[1;1;1] <* bA^^y <* bB^^z <* <[0;0] {{B}}> 0inf.
209Lemma R1 K n X z : S n < 2^K -> Pc K n X z -->+ Pc K (S n) X (S z).214Lemma R1 K n X z : S n < 2^K -> Pc K n X z -->+ Pc K (S n) X (S z).
210Proof.215Proof.
⋯ 36 identical lines (template 211–252, ours 216–257)
253 the head, with 0 or 1 new A block (Hit0 / Hit1), or ends at the right edge (FE0).258 the head, with 0 or 1 new A block (Hit0 / Hit1), or ends at the right edge (FE0).
254 Gad G T D: G takes T rounds in all, which add D A blocks. *)259 Gad G T D: G takes T rounds in all, which add D A blocks. *)
256Definition Hit0 (G G' : side) := forall l, l <* <[0;0;1] {{E}}> G -->* l <{{A}} [0;0;1] *> G'.261Definition Hit0 (G G' : side) := forall l, l <* <[0;0;1] {{F}}> G -->* l <{{E}} [0;0;1] *> G'.
257Definition Hit1 (G G' : side) := forall l, l <* <[0;0;1] {{E}}> G -->* l <* bA <{{A}} [0;0;1] *> G'.262Definition Hit1 (G G' : side) := forall l, l <* <[0;0;1] {{F}}> G -->* l <* bA <{{E}} [0;0;1] *> G'.
259Inductive Gad : side -> nat -> nat -> Prop :=264Inductive Gad : side -> nat -> nat -> Prop :=
260 | Gad_end : Gad ([0;0;1] *> 0inf) 1%nat 1%nat265 | Gad_end : Gad ([0;0;1] *> 0inf) 1%nat 1%nat
⋯ 38 identical lines (template 261–304, ours 266–309)
306(** All T rounds without overflow (R4, R5) *)311(** All T rounds without overflow (R4, R5) *)
307Lemma ConvNo K : forall G T D, Gad G T D -> forall n a, n + T < 2^K ->312Lemma ConvNo K : forall G T D, Gad G T D -> forall n a, n + T < 2^K ->
308 ctr K n <* bA^^a <{{A}} [0;0;1] *> G -->* Pc K (n + T) (a + D) 0.313 ctr K n <* bA^^a <{{E}} [0;0;1] *> G -->* Pc K (n + T) (a + D) 0.
309Proof.314Proof.
310 induction 1 as [|G G' T D HH HG IH|G G' T D HH HG IH]; intros n a Hn.315 induction 1 as [|G G' T D HH HG IH|G G' T D HH HG IH]; intros n a Hn.
⋯ 6 identical lines (template 311–317, ours 316–322)
318Lemma PostOV K : forall G T D, Gad G T D -> forall n x b y,323Lemma PostOV K : forall G T D, Gad G T D -> forall n x b y,
319 b + D = 2*T + y -> 1 <= y -> 3*T + n < 2^K ->324 b + D = 2*T + y -> 1 <= y -> 3*T + n < 2^K ->
320 ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^b <{{A}} [0;0;1] *> G -->*325 ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^b <{{E}} [0;0;1] *> G -->*
321 Qc K (3*T + n) (2*T + S x) y 0.326 Qc K (3*T + n) (2*T + S x) y 0.
322Proof.327Proof.
⋯ 17 identical lines (template 323–340, ours 328–345)
341 n + T = 2^(S k) + m -> n < 2^(S k) -> a + D = 2 + 2*m + y -> 1 <= y ->346 n + T = 2^(S k) + m -> n < 2^(S k) -> a + D = 2 + 2*m + y -> 1 <= y ->
342 3*m + (2^(S k) + 1) < 2^(S (S k)) ->347 3*m + (2^(S k) + 1) < 2^(S (S k)) ->
343 ctr (S k) n <* bA^^a <{{A}} [0;0;1] *> G -->*348 ctr (S k) n <* bA^^a <{{E}} [0;0;1] *> G -->*
344 Qc (S (S k)) (3*m + (2^(S k) + 1)) (1 + 2*m) y 0.349 Qc (S (S k)) (3*m + (2^(S k) + 1)) (1 + 2*m) y 0.
345Proof.350Proof.
⋯ 26 identical lines (template 346–371, ours 351–376)
373(** From a Q configuration with y in {0,1}: the front meets the B blocks *)378(** From a Q configuration with y in {0,1}: the front meets the B blocks *)
374Lemma QG0 K n x z : Qc K n (S x) 0 z -->+379Lemma QG0 K n x z : Qc K n (S x) 0 z -->+
375 ctr K n <* bA^^x <{{A}} [0;0;1] *> [0;0;1] *> bBr^^(S z) *> 0inf.380 ctr K n <* bA^^x <{{E}} [0;0;1] *> [0;0;1] *> bBr^^(S z) *> 0inf.
376Proof.381Proof.
377 unfold Qc. fp ENDL. fw BLs. fw (FL (ctr K n <* bA^^x) (bBr^^z *> 0inf)). finish.382 unfold Qc. fp ENDL. fw BLs. fw (FL (ctr K n <* bA^^x) (bBr^^z *> 0inf)). finish.
378Qed.383Qed.
380Lemma QG1 K n x z : Qc K n (S x) 1 z -->+385Lemma QG1 K n x z : Qc K n (S x) 1 z -->+
381 ctr K n <* bA^^x <{{A}} [0;0;1] *> [0;0;1] *> bBr *> bAr *> bBr^^z *> 0inf.386 ctr K n <* bA^^x <{{E}} [0;0;1] *> [0;0;1] *> bBr *> bAr *> bBr^^z *> 0inf.
382Proof.387Proof.
383 unfold Qc. fp ENDL. fw BLs.388 unfold Qc. fp ENDL. fw BLs.
⋯ 63 identical lines (template 384–454, ours 389–459)
455 f_equal; lia.460 f_equal; lia.
456Qed.461Qed.
458(** * Start: c0 reaches Q(7,65,1,16,0) = CfgF 5 0 16 0 in 17,215 steps *)463(** * Start: c0 reaches Q(7,65,1,14,4) = CfgF 5 0 14 4 in 16,590 steps *)
460Lemma init0 : c0 -->* 0inf <* d1 <* d0^^5 <* d1 <* bA <* <[1;1;1] <* bA^^16 <* <[0;0] {{C}}> 0inf.465Lemma init0 : c0 -->* 0inf <* d1 <* d0^^5 <* d1 <* bA <* <[1;1;1] <* bA^^14 <* bB^^4 <* <[0;0] {{B}}> 0inf.
461Proof. esx. Qed.466Proof. esx. Qed.
463Lemma init : c0 -->* CfgF 5 0 16 0.468Lemma init : c0 -->* CfgF 5 0 14 4.
464Proof. apply init0. Qed.469Proof. apply init0. Qed.
466Lemma nonhalt: ~halts tm c0.471Lemma nonhalt: ~halts tm c0.
467Proof.472Proof.
468 eapply multistep_nonhalt. { apply init. }473 eapply multistep_nonhalt. { apply init. }
469 apply (progress_nonhalt_cond tm _ (5,0,16,0)%nat474 apply (progress_nonhalt_cond tm _ (5,0,14,4)%nat
470 (fun '(k,i,y,z) => CfgF k i y z) (fun '(k,i,y,z) => Inv k i y z)).475 (fun '(k,i,y,z) => CfgF k i y z) (fun '(k,i,y,z) => Inv k i y z)).
471 - intros [[[k i] y] z] HI.476 - intros [[[k i] y] z] HI.
⋯ 5 identical lines (template 472–477, ours 477–482)
478```483```
4791RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---4841RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA
485(= sigma of 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---, sigma = EDBCFA, no mirror)
481C_k(n): n in k bits MSB first, digit 1 -> 1010 (d1), digit 0 -> 0010 (d0) [ctr k n]487C_k(n): n in k bits MSB first, digit 1 -> 1010 (d1), digit 0 -> 0010 (d0) [ctr k n]
482A = 00111, B = 10111 left of the head; A' = 00101, B' = 00001 right of the head488A = 00111, B = 10111 left of the head; A' = 00101, B' = 00001 right of the head
483moving head: <A 001 / 001 E> (TM4's hL / hR)489moving head: <E 001 / 001 F> (sigma of TM4's hL / hR)
485P(k,n,X,z) := 0^inf C_k(n) A^X B^z 00 C> 0^inf [Pc]491P(k,n,X,z) := 0^inf C_k(n) A^X B^z 00 B> 0^inf [Pc]
486Q(k,n,x,y,z) := 0^inf C_k(n) A^x 111 A^y B^z 00 C> 0^inf [Qc]492Q(k,n,x,y,z) := 0^inf C_k(n) A^x 111 A^y B^z 00 B> 0^inf [Qc]
488R1 P(k,n,X,z) -->+ P(k,n+1,X,z+1) n+1 < 2^k494R1 P(k,n,X,z) -->+ P(k,n+1,X,z+1) n+1 < 2^k
489R2 P(k,2^k-1,X+2,z) -->+ Q(k+1,2^k+1,1,X,z+1)495R2 P(k,2^k-1,X+2,z) -->+ Q(k+1,2^k+1,1,X,z+1)
⋯ 9 identical lines (template 490–499, ours 496–505)
500 R5o, m = 3i+2z+8-N -> (k+1, m, 2i+z+3-2m, 0) overflow506 R5o, m = 3i+2z+8-N -> (k+1, m, 2i+z+3-2m, 0) overflow
501invariant: N >= 64, 8Y >= N, 8Y <= 3N, 3Z <= N, 8Z >= -N, 4Y+2Z >= N, 20Y+16Z <= 9N507invariant: N >= 64, 8Y >= N, 8Y <= 3N, 3Z <= N, 8Z >= -N, 4Y+2Z >= N, 20Y+16Z <= 9N
502start: c0 -->(17215) Q(7,65,1,16,0), index (5,0,16,0)
508start: c0 -->(16590) Q(7,65,1,14,4), index (5,0,14,4) [#4: c0 -->(17215) Q(7,65,1,16,0)]
503```509```
504*)510*)
4Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.

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

#kindnamestatement (no proof body)linevs template
1Definitiontm
Definition tm := Eval compute in (TM_from_str "1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA").
L23identicalexcept the TM string
2Lemmaev_eq
Lemma ev_eq {c1 c2 c2'} : c1 -->* c2 -> c2 = c2' -> c1 -->* c2'.
L40identical
3Lemmaprog_eq
Lemma prog_eq {c1 c2 c2'} : c1 -->+ c2 -> c2 = c2' -> c1 -->+ c2'.
L43identical
4LemmaENDL
Lemma ENDL l : l <* <[0;0] {{B}}> 0inf -->+ l <{{E}} [0;0;1] *> 0inf.
L48adapted
5LemmaAL
Lemma AL l r : l <* bA <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> bAr *> r.
L49adapted
6LemmaBL
Lemma BL l r : l <* bB <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> bBr *> r.
L50adapted
7LemmaAR
Lemma AR l r : l <* <[0;0;1] {{F}}> bAr *> r -->* l <* bA <* <[0;0;1] {{F}}> r.
L51adapted
8LemmaBR
Lemma BR l r : l <* <[0;0;1] {{F}}> bBr *> r -->* l <* bB <* <[0;0;1] {{F}}> r.
L52adapted
9LemmaENDR
Lemma ENDR l : l <* <[0;0;1] {{F}}> 0inf -->* l <* bB <* <[0;0] {{B}}> 0inf.
L53adapted
10LemmaD1L
Lemma D1L l r : l <* d1 <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> [0;1;0;1] *> r.
L54adapted
11LemmaFLIP
Lemma FLIP l r : l <* d0 <{{E}} [0;0;1] *> r -->* l <* d1 <* <[0;0;1] {{F}}> r.
L55adapted
12LemmaD0R
Lemma D0R l r : l <* <[0;0;1] {{F}}> [0;1;0;1] *> r -->* l <* d0 <* <[0;0;1] {{F}}> r.
L56adapted
13LemmaD0R'
Lemma D0R' l r : l <* <[0;0;1] {{F}}> [0;1] *> [0;1;0;1] *> r -->* l <* d0 <* <[0;0;1] {{F}}> [0;1] *> r.
L57adapted
14LemmaOVL
Lemma OVL r : 0inf <{{E}} [0;0;1] *> [0;1;0;1] *> r -->* 0inf <* d1 <* <[0;0;1] {{F}}> [0;1] *> r.
L59adapted
15LemmaOVR
Lemma OVR l r : l <* <[0;0;1] {{F}}> [0;1] *> bAr *> r -->* l <* d0 <{{E}} [0;0;1] *> [1;0;1] *> r.
L61adapted
16LemmaFL
Lemma FL l r : l <* bA <* <[1;1;1] <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> [0;0;1] *> bBr *> r.
L63adapted
17LemmaFR1
Lemma FR1 l r : l <* <[0;0;1] {{F}}> [0;0;1] *> bBr *> r -->* l <* bA <{{E}} [0;0;1] *> [0;0;1] *> r.
L65adapted
18LemmaFR2
Lemma FR2 l r : l <* <[0;0;1] {{F}}> [0;0;1] *> bAr *> r -->* l <* bA <{{E}} [0;0;1] *> [1;0;1] *> r.
L67adapted
19LemmaFR3
Lemma FR3 l r : l <* <[0;0;1] {{F}}> [1;0;1] *> bAr *> r -->* l <* bA <* <[1;1;1] <* <[0;0;1] {{F}}> r.
L69adapted
20LemmaFR4
Lemma FR4 l r : l <* <[0;0;1] {{F}}> [1;0;1] *> bBr *> r -->* l <{{E}} [0;0;1] *> [0;0;1] *> bAr *> r.
L71adapted
21LemmaFE0
Lemma FE0 l : l <* <[0;0;1] {{F}}> [0;0;1] *> 0inf -->* l <* bA <* <[0;0] {{B}}> 0inf.
L73adapted
22LemmaFE1
Lemma FE1 l : l <* <[0;0;1] {{F}}> [1;0;1] *> 0inf -->* l <{{E}} [0;0;1] *> [0;0;1] *> [0;0;1] *> 0inf.
L75adapted
23LemmaFE2
Lemma FE2 l : l <* <[0;0;1] {{F}}> [0;0;1] *> [0;0;1] *> 0inf -->* l <* bA <{{E}} [0;0;1] *> [1] *> 0inf.
L77adapted
24LemmaFE3
Lemma FE3 l : l <* <[0;0;1] {{F}}> [1] *> 0inf -->* l <{{E}} [0;0;1] *> [0;0;1;1] *> 0inf.
L79adapted
25LemmaFE4
Lemma FE4 l : l <* <[0;0;1] {{F}}> [0;0;1;1] *> 0inf -->* l <* bA <{{E}} [0;0;1] *> [0;0;1] *> 0inf.
L81adapted
26LemmaALs
Lemma ALs a : forall l r, l <* bA^^a <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> bAr^^a *> r.
L86adapted
27LemmaBLs
Lemma BLs a : forall l r, l <* bB^^a <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> bBr^^a *> r.
L90adapted
28LemmaARs
Lemma ARs a : forall l r, l <* <[0;0;1] {{F}}> bAr^^a *> r -->* l <* bA^^a <* <[0;0;1] {{F}}> r.
L94adapted
29LemmaBRs
Lemma BRs a : forall l r, l <* <[0;0;1] {{F}}> bBr^^a *> r -->* l <* bB^^a <* <[0;0;1] {{F}}> r.
L98adapted
30LemmaD1Ls
Lemma D1Ls a : forall l r, l <* d1^^a <{{E}} [0;0;1] *> r -->* l <{{E}} [0;0;1] *> [0;1;0;1]^^a *> r.
L102adapted
31LemmaD0R's
Lemma D0R's a : forall l r, l <* <[0;0;1] {{F}}> [0;1] *> [0;1;0;1]^^a *> r -->* l <* d0^^a <* <[0;0;1] {{F}}> [0;1] *> r.
L106adapted
32Fixpointctr
Fixpoint ctr (k n : nat) : side :=
match k with
| O => 0inf
| S k => ctr k (Nat.div2 n) <* (if Nat.odd n then d1 else d0)
end.
L113identical
33Lemmactr_even
Lemma ctr_even k q : ctr (S k) (2*q) = ctr k q <* d0.
L119identical
34Lemmactr_odd
Lemma ctr_odd k q : ctr (S k) (S (2*q)) = ctr k q <* d1.
L122identical
35Lemmapow2_pos
Lemma pow2_pos k : 1 <= 2^k.
L125identical
36LemmaCTR
Lemma CTR k : forall n r, S n < 2^k ->
ctr k n <{{E}} [0;0;1] *> r -->* ctr k (S n) <* <[0;0;1] {{F}}> r.
L129adapted
37Lemmactr_ones
Lemma ctr_ones k : ctr k (2^k - 1) = 0inf <* d1^^k.
L144identical
38Lemmactr_pow
Lemma ctr_pow k : ctr (S k) (2^k) = 0inf <* d1 <* d0^^k.
L153identical
39Lemmactr_ov
Lemma ctr_ov k : ctr (S (S k)) (2^(S k) + 1) = 0inf <* d1 <* d0^^k <* d1.
L160identical
40LemmaOV
Lemma OV k r :
ctr (S k) (2^(S k) - 1) <{{E}} [0;0;1] *> bAr *> bAr *> r -->*
ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* <[0;0;1] {{F}}> r.
L167adapted
41LemmaRT
Lemma RT K n a r : S n < 2^K ->
ctr K n <* bA^^a <{{E}} [0;0;1] *> r -->* ctr K (S n) <* bA^^a <* <[0;0;1] {{F}}> r.
L177adapted
42LemmaOVRT
Lemma OVRT k a r :
ctr (S k) (2^(S k) - 1) <* bA^^(S (S a)) <{{E}} [0;0;1] *> r -->*
ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* bA^^a <* <[0;0;1] {{F}}> r.
L184adapted
43LemmaQC
Lemma QC K n x y r : 3 + n < 2^K ->
ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^(S (S y)) <{{E}} [0;0;1] *> r -->*
ctr K (3 + n) <* bA^^(S (S (S x))) <* <[1;1;1] <* bA^^y <* <[0;0;1] {{F}}> r.
L192adapted
44DefinitionPc
Definition Pc K n X z := ctr K n <* bA^^X <* bB^^z <* <[0;0] {{B}}> 0inf.
L211adapted
45DefinitionQc
Definition Qc K n x y z := ctr K n <* bA^^x <* <[1;1;1] <* bA^^y <* bB^^z <* <[0;0] {{B}}> 0inf.
L212adapted
46LemmaR1
Lemma R1 K n X z : S n < 2^K -> Pc K n X z -->+ Pc K (S n) X (S z).
L214identical
47LemmaR1s
Lemma R1s K c : forall n X z, c + n < 2^K -> Pc K n X z -->* Pc K (c + n) X (c + z).
L220identical
48LemmaR2
Lemma R2 k X z : Pc (S k) (2^(S k) - 1) (S (S X)) z -->+ Qc (S (S k)) (2^(S k) + 1) 1 X (S z).
L229identical
49LemmaPfin
Lemma Pfin (k n X z n' x' X' z' : nat) :
n < 2^(S k) -> X = 2 + X' -> n' = 2^(S k) + 1 -> x' = 1%nat -> z' = z + 2^(S k) - n ->
Pc (S k) n X z -->+ Qc (S (S k)) n' x' X' z'.
L236identical
50LemmaR3
Lemma R3 K n x y z : 3 + n < 2^K ->
Qc K n (S x) (S (S y)) z -->+ Qc K (3 + n) (S (S (S x))) y (S z).
L247identical
51DefinitionHit0
Definition Hit0 (G G' : side) := forall l, l <* <[0;0;1] {{F}}> G -->* l <{{E}} [0;0;1] *> G'.
L261adapted
52DefinitionHit1
Definition Hit1 (G G' : side) := forall l, l <* <[0;0;1] {{F}}> G -->* l <* bA <{{E}} [0;0;1] *> G'.
L262adapted
53InductiveGad
Inductive Gad : side -> nat -> nat -> Prop :=
| Gad_end : Gad ([0;0;1] *> 0inf) 1%nat 1%nat
| Gad_h0 G G' T D : Hit0 G G' -> Gad G' T D -> Gad G (S T) D
| Gad_h1 G G' T D : Hit1 G G' -> Gad G' T D -> Gad G (S T) (S D).
L264identical
54LemmaGad_DT
Lemma Gad_DT G T D : Gad G T D -> D <= T.
L269identical
55LemmaGad_eq
Lemma Gad_eq {G T D T' D'} : T = T' -> D = D' -> Gad G T D -> Gad G T' D'.
L272identical
56Lemmagad_even
Lemma gad_even z : Gad ([0;0;1] *> bBr^^z *> 0inf) (S z) (S z).
L276identical
57Lemmagad_tail
Lemma gad_tail : Gad ([1;0;1] *> 0inf) 5 3.
L284identical
58Lemmagad_mid
Lemma gad_mid z : Gad ([1;0;1] *> bBr^^z *> 0inf) (5 + 2*z) (3 + z).
L293identical
59Lemmagad_odd
Lemma gad_odd z : Gad ([0;0;1] *> bBr *> bAr *> bBr^^z *> 0inf) (7 + 2*z) (5 + z).
L303identical
60LemmaConvNo
Lemma ConvNo K : forall G T D, Gad G T D -> forall n a, n + T < 2^K ->
ctr K n <* bA^^a <{{E}} [0;0;1] *> G -->* Pc K (n + T) (a + D) 0.
L312adapted
61LemmaPostOV
Lemma PostOV K : forall G T D, Gad G T D -> forall n x b y,
b + D = 2*T + y -> 1 <= y -> 3*T + n < 2^K ->
ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^b <{{E}} [0;0;1] *> G -->*
Qc K (3*T + n) (2*T + S x) y 0.
L323adapted
62LemmaConvOV
Lemma ConvOV k : forall G T D, Gad G T D -> forall n a m y,
n + T = 2^(S k) + m -> n < 2^(S k) -> a + D = 2 + 2*m + y -> 1 <= y ->
3*m + (2^(S k) + 1) < 2^(S (S k)) ->
ctr (S k) n <* bA^^a <{{E}} [0;0;1] *> G -->*
Qc (S (S k)) (3*m + (2^(S k) + 1)) (1 + 2*m) y 0.
L345adapted
63LemmaQG0
Lemma QG0 K n x z : Qc K n (S x) 0 z -->+
ctr K n <* bA^^x <{{E}} [0;0;1] *> [0;0;1] *> bBr^^(S z) *> 0inf.
L379adapted
64LemmaQG1
Lemma QG1 K n x z : Qc K n (S x) 1 z -->+
ctr K n <* bA^^x <{{E}} [0;0;1] *> [0;0;1] *> bBr *> bAr *> bBr^^z *> 0inf.
L385adapted
65LemmaConv0
Lemma Conv0 K n x z : n + z + 2 < 2^K ->
Qc K n (S x) 0 z -->+ Pc K (n + z + 2) (x + z + 2) 0.
L394identical
66LemmaConv1
Lemma Conv1 K n x z : n + 2*z + 7 < 2^K ->
Qc K n (S x) 1 z -->+ Pc K (n + 2*z + 7) (x + z + 5) 0.
L403identical
67LemmaConv1o
Lemma Conv1o (k m n x z n' x' y : nat) :
n + 2*z + 7 = 2^(S k) + m -> n < 2^(S k) -> x + z + 5 = 2 + 2*m + y -> 1 <= y ->
3*m + (2^(S k) + 1) < 2^(S (S k)) -> n' = 3*m + (2^(S k) + 1) -> x' = 1 + 2*m ->
Qc (S k) n (S x) 1 z -->+ Qc (S (S k)) n' x' y 0.
L412identical
68DefinitionCfgF
Definition CfgF (k i y z : nat) := Qc (S (S k)) (3*i + (2^(S k) + 1)) (1 + 2*i) y z.
L429identical
69DefinitionInv
Definition Inv (k i y z : nat) : Prop :=
64 <= 2^(S k) /\ 2^(S k) <= 8*(y + 2*i) /\ 8*(y + 2*i) <= 3 * 2^(S k) /\
3*z <= 2^(S k) + 3*i /\ 8*i <= 8*z + 2^(S k) /\
2^(S k) <= 4*y + 6*i + 2*z /\ 20*y + 24*i + 16*z <= 9 * 2^(S k).
L431identical
70Lemmacycle_step
Lemma cycle_step k i y z : Inv k i y z ->
exists k' i' y' z', CfgF k i y z -->+ CfgF k' i' y' z' /\ Inv k' i' y' z'.
L436identical
71Lemmainit0
Lemma init0 : c0 -->* 0inf <* d1 <* d0^^5 <* d1 <* bA <* <[1;1;1] <* bA^^14 <* bB^^4 <* <[0;0] {{B}}> 0inf.
L465adapted
72Lemmainit
Lemma init : c0 -->* CfgF 5 0 14 4.
L468adapted
73Lemmanonhalt
Lemma nonhalt: ~halts tm c0.
L471adapted
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 line 50: 1. What carries over unchanged (no heading names the rules; this is the first section on what carries over)
parent item here reason
parent §1 words and families: C_k(n), A/B blocks, P(k,n,X,z), Q(k,n,x,y,z) the same words; the right-edge head state is B = σ(C), and the moving head is <E 001 / 001 F> (σ of <A 001 / 001 E>) Lemma R
parent §3.1, the 21 shift rules identical, with the head states renamed; same step counts Lemma R; in the .v each is re-proved by es on this machine's table
parent §3.2 repeated rules (AL^a … D0R^t, CTR, OV, QC) and parent §3.3 macro rules R1, R2, R3, R4, R5, R5o (R4o as a remark) identical, with the same step formulas and domains Lemma R; the .v re-proves them on this table with the parent's proof scripts
parent §4 cycle states S(k,Y,Z), the cycle lemma with hypotheses (a)–(d), the hexagon R_N, (i)/(ii) and the parity remark identical the statements and proofs read only the rules and (k,Y,Z), never the start
parent §4 progress (every macro rule contains ENDL) identical Lemma R
parent §5 initial segment changed: §2 different start

The rules in busycoq comment style, for this machine:

1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA     (= sigma of 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---, sigma = EDBCFA)

C_k(n): n in k bits MSB first, 1 -> 1010, 0 -> 0010;   A = 00111, B = 10111;  moving head <E 001 / 001 F>
P(k,n,X,z)   := 0^inf C_k(n) A^X B^z 00 B> 0^inf
Q(k,n,x,y,z) := 0^inf C_k(n) A^x 111 A^y B^z 00 B> 0^inf                    (x >= 1)

R1  P(k,n,X,z)      --> P(k,n+1,X,z+1)                     n+1 <= 2^k-1
R2  P(k,2^k-1,X,z)  --> Q(k+1,2^k+1,1,X-2,z+1)             X >= 2
R3  Q(k,n,x,y+2,z)  --> Q(k,n+3,x+2,y,z+1)                 n+3 <= 2^k-1
R4  Q(k,n,x,0,z)    --> P(k,n+z+2,x+z+1,0)                 n+z+2  <= 2^k-1
R5  Q(k,n,x,1,z)    --> P(k,n+2z+7,x+z+4,0)                n+2z+7 <= 2^k-1
R5o Q(k,n,x,1,z)    --> Q(k+1,2^k+1+3m,1+2m,x+z+2-2m,0)    m := n+2z+7-2^k >= 0,  x+z+2-2m >= 1,  3m <= 2^k-2
steps: R1 32X+32z+16t(n)+47,  R2 32X+32z+16k+61,  R3 96x+32y+32z+16(t(n)+t(n+1)+t(n+2))+197

cycle (N = 2^k):  S(k,Y,Z) := Q(k+1, N+1+3m, 1+2m, Y-2m, Z+m),  m = max(0,-Z)
  S(k,2j,Z)   -->+ S(k+1, 3j+Z,   N-3-4j-Z)
  S(k,2j+1,Z) -->+ S(k+1, 3j+3+Z, N-8-5j-2Z)
invariant (N >= 64):  8Y >= N, 8Y <= 3N, 3Z <= N, 8Z >= -N, 4Y+2Z >= N, 20Y+16Z <= 9N
start: c0 -->(16590) S(6,14,4) = Q(7,65,1,14,4)        [parent: c0 -->(17215) S(6,16,0)]
6FamilyCheck: related machines are killed together or have a reason to be left open.

2 machines, 2 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.

whomachinestatusrelation to this kill
#4 kill 21RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---✓Killed: never haltsparent link; = #4b's table, run from state E; named in #4b's .v header; named in #4b's proof.md; named in #4b's notes.md · review · compared side by side above · mechanism
#4b kill 111RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA✓Killed: never haltsthis 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 17 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 2.11 s
  • ✓
    .v hash matches the checked hash
    .v = checked sha256 0c89b5109f87…; submission/ copy = checked sha256 0c89b5109f87…
  • ✓
    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 L79: - No Checkpoint B notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
    • proof.md L1: # 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA: delta proof from kill #4 (Checkpoint B)
    • proof.md L192: ## 7. Checkpoint B notes (Dennis)
  • ○
    Family posted together?
    1 other kill(s) in the family: #4; the Discord draft names 1 of them

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 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA

Files

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

namesizechanged
notes.md ↓8.4 KB2026-10-10 12:30
proof.md ↓17 KB2026-10-10 12:17
how_proved.md ↓1.4 KB2026-10-14 10:51
status.json ↓832 B2026-10-16 10:28
observe.json ↓12 KB2026-10-10 16:32
1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v ↓21 KB2026-10-10 12:21
img/9 items2026-10-16 10:28
rocq/9 items2026-10-10 12:27
submission/6 items2026-10-14 10:10
work/9 items2026-10-10 15:58
check_proof.out ↓5.7 KB2026-10-10 12:16
check_proof.py ↓22 KB2026-10-10 12:16
check_proof_k15.out ↓5.8 KB2026-10-10 12:17
status.json in full
{
 "tm": "1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "parent": "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---",
 "parent_note": "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC--- (#4)",
 "label": "#4b",
 "relation": "same transition table as #4 (states renamed), started in a different state; found by the family sweep",
 "pr": "https://github.com/ccz181078/busycoq/pull/24",
 "pr_state": "merged",
 "pr_file": "verify/M_1RBHHH_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v",
 "pr_opened": "2026-10-15T22:46:17Z",
 "pr_comments": 0,
 "pr_head_sha": "1b57cbac0ccf590232647c1b29389f2efe7f26a4",
 "posted": "2026-10-15 (Discord; user confirmed sent)",
 "pr_merged_at": "2026-10-16T07:07:18Z",
 "pr_merged_by": "ccz181078"
}
observe.json contract (tools/README-card.md):
1 contract warning
  • rank: missing