BB(6) hunt
Machines / #2

1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---

#2local proof 1Kill claimedBell eats counterbbchallenge ↗Explorer

How we proved it never halts

A known sweep recipe plus one extra +1, shown never to get stuck

Right of a short wall, 11, the tape is cut into three-cell blocks: filler 110, and binary digits 100 (a 1) and 000 (a 0). A typical moment is 11 110 110 … 110 100 000 100: the wall, mostly filler, and a few digits near the right end forming a small binary counter, lowest digit first. Over and over the head sweeps right from the wall and back, and each sweep leaves the wall one cell further left and the filler longer.

The key idea: every sweep follows a fixed recipe, almost the one busycoq already proved for a close relative, its TM7, whose table differs in one entry. Going right, the head turns blocks into filler and runs up a debt of extra passes (trips over the blocks ahead); from the first 1 digit on it pays the debt off, and any leftover is written past the right end in binary. The one difference: whenever the head steps into a filler block, this machine first runs a quick +1 over everything to its right.

Why that settles it: the proof writes the recipe as twelve exact rules and shows two things. Each rule is a real run of the machine that never uses the missing entry (state F reading a 1), because F always arrives on the last cell of a block, which is 0 in all three kinds. And the recipe never gets stuck: it applies to the first sweep and to every tape a sweep produces, which needed two extra end cases and a count of pending +1s on top of TM7's version.

The Rocq proof checks every rule by induction, the never-stuck lemma and the 16-step opening; eight rules reuse TM7's proof unchanged. busycoq has merged it as BellEatsCounter_1RB0RF.v.

#1local proof number
599lines of Rocq
5 sto compile
5/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

SOMDCv6 TM7 + one change: A1=0RF runs a +1 pass each time a 110 digit is entered. Fits 208/208 sweeps.

Submitted mechanism At each sweep boundary the tape is S(r) = 0^inf 11 D> <r> 0^inf, where r is a word over three 3-cell digits: L = 110, 0 = 000, 1 = 100. In practice r is a long L-run followed by a short binary counter. (submission/README.md, Mechanism)

Upstream
Kill claimed · PR #14merged 2026-10-10 20:47 UTC by ccz181078 · verify/BellEatsCounter_1RB0RF.v · on Submissions →
Rocq proof
check_kill PASS · first Oct 10 04:48
599 lines · 19 KB .v · compile 4.7 s · coqchk pass · 0 axioms · PASS Oct 10 04:48 (re-run Oct 14 14:27)
· the .v file
Automatic review
5 of 6 checks passtemplate: verify/SOMDCv6.v Module TM7 (adapted from) · details in Proof →
Class
Bell eats counterours: Bell eats counter (sheet) · ours adds: SOMDCv6 TM7 + a '+1 pass at each 110 entered' · high confidence
On the list
not on BB6_holdouts_663.txt (line 301 of the previous list)
#2eqv ×1sim 1e15

Mechanism

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

How it works: 3 notes
  • Tape: wall 11, then 3-cell digits L=110, 0=000, 1=100: a long run of L's, then a short counter.
  • Each sweep: the eater turns digits white until it reads a 1-digit; then k drain passes rebuild L's (k = digits eaten).
  • Only change vs SOMDCv6 TM7: each L entered (by eater or drain pass) first fires a +1 pass on the digits to its right.

Figures for Checkpoint A

Fig 1 · One eating pass: ours vs SOMDCv6 TM7✓ Q1

Same start for both. Blue boxes mark ours' extra +1 passes; compare everything outside them with TM7's run.

One eating pass: ours vs SOMDCv6 TM7
bbchallenge-defaultStart constructed: 0∞ 11 D> (110)4 100 110 100 0∞ = S(L⁴ 1L1)Rows every step: ours 0..118Window cells -4..24, 1 px = 1/12 cellColors 1 0 head after a move R/L box: ours' extra +1 pass ▶: TM7's A1 (turns back) dashes: eater stops
Start: the same for both machines · Rows: TM7 0..44 (until the eater reads the 1-digit); same scale · Window: cell 12 px wide, step 8 px tall
Fig 2 · One full sweep: ours vs TM7✓ Q2

One full sweep each. Find pass 5 (a drain pass), then compare the drain zigzags that follow it.

One full sweep: ours vs TM7
bbchallenge-defaultStart constructed: 0∞ 11 D> (110)4 100 110 100 0∞ = S(L⁴ 1L1)Rows every step: ours 0..421Window cells -4..34, 1 px = 1/10 cellColors 1 0 head after a move R/L box: ours' extra +1 pass ▶: TM7's A1 (turns back) dashes: eater stops bracket: drain passes
Start: the same for both machines · Rows: TM7 0..237 (to the next S config); same scale · Window: cell 10 px wide, step 4 px tall · Colors: white bracket: no A1: same rules in both
Fig 3 · bbchallenge default view, first 10,000 steps✓ Q3viewer ↗

The site's view from blank: watch the white bells and the right edge of the digit region.

bbchallenge default view, first 10,000 steps
bbchallenge-defaultStart blankRows 10,000 steps squeezed into 500 px rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a move R/L
Rows: 1 px row = 20 steps; the site blends steps 20y+9 and 20y+10 · Colors: red/green: blended into the squeezed rows, as on the site
More figures (2)Fig 4–5: Left/right records to 1 billion steps · Blaze, 10 million steps
Fig 4 · Left/right records to 1 billion steps

White bell waves over a steadily growing right edge; the left edge barely moves (209 vs 4,692 cells).

Left/right records to 1 billion steps
bbchallenge-defaultStart blankRows the start, then one row per new leftmost or rightmost cellWindow cells -209..4,692, 1 px = 1 cellColors 1 0 or never visited head after a move R/L
Rows: 4,902 rows (209 left, 4,692 right) up to step 1e9; rows are not evenly spaced in time · Colors: zoomed out, the L digits (110 stripes) look grey and the bell is solid white
Fig 5 · Blaze, 10 million steps

Stacked bells; the right edge grows roughly like t^(1/3).

Blaze, 10 million steps
bbchallenge-blazeStart blankRows Blaze time blocks of 16,384 stepsWindow cells -54..953, 1 px = 1.26 cellsColors 0 1 a cell that was 1 for only part of its 16,384-step block
Rows: (611 rows, each averaged), stretched to 500 px (1 px ~ 20,000 steps) · Window: 1,008 Blaze columns of 1 cell each, stretched to 800 px
Rules (6/6 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
Sweep
0∞ 11 D> r 0∞
⟶ 0∞ 11 D> eat(r) 0∞ (wall 1 cell left)
r over L=110,0=000,1=100. Eater, k=0: 0->L,k+1 | L->L,k+1,+1 rest* | 1->L, count mode. Count mode k>=1: L->L, eater again, +1 rest* | 1->L,k-1 | 0->0,(k-1)/2 if k odd; 0->1,(k-2)/2 if even. Right end: k=0->1; odd->0; even->1; repeat. *=new vs TM7—✓502/502
Eater enters L (new)
1 D> 110 X
⟶ 1 111 D> inc(X)
A1 fires here. inc = +1 on the 0/1 digits, little-endian, L skipped; overflow appends 100. TM7: 1 D> 110 X -> 1 111 D> X in 11 steps (no pass)6j+13 (j = digits before the first 000 in X)✓1393/1393
Drain pass enters L (new)
B> 1 110 X
⟶ 1 111 D> inc(X)
A1 fires here and the eater restarts after the L (115 of 208 sweeps to 1e9). TM7: B> 1 110 X -> 1 111 D> X in 10 steps (no pass)6j+12 (j as above)✓1393/1393
Eater over 0s
11 D> (000)a
⟶ 11 (111)a D>
—3a✓45/45
+1 pass: carry
B> (100)a 000
⟶ (000)a <C 100
at tape end: B> (100)^a 0^inf -> (000)^a <C 1 0^inf3a+1✓90/90
+1 pass: skip L, return
B> (110)a
⟶ (011)a B>
return: (011)^a <C -> <C (110)^a and (000)^a <C -> <C (000)^a, 3a each3a✓135/135
Compressed historythe tape as 0∞ 11 D> (110)n T 0∞ at 40 moments: where the rules are read off
0∞ 11 D> (110)n T 0∞
stepnT
501
1611
91311
31861
80980L11
1,93014111
3,971191,111
6,93221101L1
10,625231LL1L001
16,17632111
24,427381
34,85041111L11
47,929471L01101
64,518531L01101
84,5395710LL0011
436,857105111LL0101
1,355,2991591LL10L01001
2,835,01421000LL010011
5,658,65626910110L111
9,961,61232600L1111001
16,012,4323811LLL1L0011101
23,139,1834371LL11101011
33,896,5195031LLLL10101111
47,901,4395671L111L100001
65,193,5816280LL11L0011001
83,603,98668601L0L0L100101
108,594,88675001LLL0L1101101
138,455,6508160L0L01LL000011
173,399,6348840LL1LL10011011
208,657,71594111L1LLL1000111
254,952,9211,0160LLLLL101011111
308,436,9931,0800LLL0101L000001
368,117,8871,147111L10110001
426,162,8321,2011L0L01L1001001
499,947,9581,2720LLL11L00111001
582,161,1081,34110L1L10100101
673,443,4981,4091LLL0L1L10110101
761,279,3811,4720LL1LL0L10101101
871,368,5691,5561,001,000,011
992,340,7151,61910L11LL0100011
nlast 1,619
1,619059.9e8log xstep 5: n = 0step 16: n = 1step 91: n = 3step 318: n = 6step 809: n = 8step 1930: n = 14step 3971: n = 19step 6932: n = 21step 10625: n = 23step 16176: n = 32step 24427: n = 38step 34850: n = 41step 47929: n = 47step 64518: n = 53step 84539: n = 57step 436857: n = 105step 1355299: n = 159step 2835014: n = 210step 5658656: n = 269step 9961612: n = 326step 16012432: n = 381step 23139183: n = 437step 33896519: n = 503step 47901439: n = 567step 65193581: n = 628step 83603986: n = 686step 108594886: n = 750step 138455650: n = 816step 173399634: n = 884step 208657715: n = 941step 254952921: n = 1016step 308436993: n = 1080step 368117887: n = 1147step 426162832: n = 1201step 499947958: n = 1272step 582161108: n = 1341step 673443498: n = 1409step 761279381: n = 1472step 871368569: n = 1556step 992340715: n = 1619
Tlast 10L11LL0100011
1e9158.7e8log-logstep 5: T = 1step 16: T = 1step 91: T = 11step 318: T = 1step 1930: T = 111step 3971: T = 1111step 16176: T = 111step 24427: T = 1step 871368569: T = 1001000011
Template comparisonSOMDCv6.v TM7: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0RFtpl 0RC
B1LC0RE
C0LC0LD
D1RD1LB
E0RF1RA
F0RB---

differs from the template

file
SOMDCv6.v:1626
module
TM7 (line 1626); TM8 (line 1874) has the identical proof
machine
1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- (1 transition apart)
diff
A1: 0RC (TM7) / 0LC (TM8) -> 0RF; other 11 transitions equal
note
Config S(r)=0^inf 11 D> r and digits 110/000/100 carry over (no other digit to 1e9). TM7's RIncs map fits 1/208 sweeps; with '+1 to the rest at every L entered' (eater and drain clause) it fits 208/208; eater clause alone: 95/208.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Copy SOMDCv6 TM7 (S', ld/d0/d1, h/h', RIncs, BigStep, nonhalt). Add Inductive Inc (+1, L skipped) proved as one h-pass, sideRLs tm [h] (toRC r) (toRC r') (BC-style: B>000-><C100, B>100->000B>, 110<->011). Insert Inc into RIncs_hx_ld and RIncs_h1_ld, redo RIncs_nxt, then nonhalt via multistep_nonhalt + progress_nonhalt_cond exactly as TM7.

  • ▲Domain lemma (TM7's RIncs_nxt) must absorb the extra +1s; in the abstract run the pass count k in count mode gets as low as 1.
  • ▲+1 can lengthen the word (overflow appends 100), so RIncs_nxt's induction on r gets more cases.
  • ▲Twin 1RB0RA_... (A1=0RA, also open) uses extra digits 010/011/111: own rules, no free second kill.
Stats & provenance109 steps simulated · 4,902 cells · the status in full · files
simulated
109 steps
tape
4,902 cells · 4,592 nonzeros
growth
span ~t^0.34 (2,220 cells at 1e8, 4,902 at 1e9); 208 sweeps by 1e9
status now
check_kill PASS, independently re-verified (status.json, 2026-10-10)
observer's note
Mechanism found; every rule passes simulation; aligned TM7 comparison redrawn; plain counter arithmetic (not a cryptid).
files
observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v
other viewers
sweep_ours · sweep_tm7

Proof & checks

5/6 automatic checks pass

Kill 1 · Bell eats counter · the kill file 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v: 599 lines, 35 items · the package submission/

✗ 5/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (adapted from): verify/SOMDCv6.v Module TM7 · 29% of our lines identical
1What is provedCheck: the string, the theorem and every check_kill line are green, and the .v on disk is the one that was checked (same sha256).
Machine
1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---
vs holdout list
✓ byte-exact: the .v literal (L27) == 2026-10-07_778.txt line 301 (41 bytes, via tools/holdouts.py)
Theorem
✓ Lemma nonhalt: ~halts tm c0. L560
check_kill
✓ PASS · 17/17 checks pass · compile 4.65 s · coqchk pass (1.29 s) · assumptions: 0 (closed) · 2026-10-14 21:27:13 UTC · check_kill.txt · 2 runs on file
Checked .v
sha256 e434537eca67d99f…
✓1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.ve434537eca67d99f… = checked
✓submission/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.ve434537eca67d99f… = 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
✓input19434 bytes, 599 lines, 421 sentences
✓frameworkHEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓framework_build15 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)
✓structure8 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓tm_textline 27: TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---" == <tm> (41 bytes)
✓theorem_textline 560: nonhalt : ~halts tm c0
✓coqcoqc 8.20.1 ([local working file]
✓nameshalts, c0, TM_from_str resolved inside Individual62
✓compilecompiled in 4.7s with all appended checks
✓tm_rocqBB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---" by eq_refl (in-file and isolated)
✓theorem_rocqnonhalt : ~ halts (TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---") 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 (1.3s); its context summary lists nothing of the file's own
✓integrityinput sha256 and framework HEAD/cleanliness identical before and after
2Where it came fromCheck: the template is the one you expect, and the measured reuse (tiles, the reuse figure, diff) agrees with what the README says was kept and changed (quoted).
adapted from verify/SOMDCv6.v Module TM7 · detected from 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v line 2
29%of our lines identical to the template
5changed lines
370added lines (ours only)
70template lines dropped
7 / 3 / 25items identical / adapted / new
What the package README says it reused and changed (submission/README.md line 15, Template and what changed), quoted:

This extends SOMDCv6.v Module TM7 (1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---), which differs only in A1 (0RC there, 0RF here).

  1. New Inc relation (one pass = +1, L skipped), proved as sideRLs tm h.
  2. Inc premise on the two L clauses of RIncs (eater enters L, drain pass enters L). Their segment facts become [h; h'; h] (seg_hx_ld, seg_h1_ld).
  3. Two zero-pass end clauses, Z1 RIncs h1 0 [D1] [LD] and Z0 RIncs h1 0 [D0] [D1]. They add no machine behaviour (1 100 0^inf = 110 0^inf, 1 000 0^inf = 100 0^inf), but without them the sweep's domain is not closed.
  4. Domain lemma redone as key, with j pending +1 passes and a condition Inv that reduces to TM7's when j = 0. It uses the helper lemmas RIncs_Inc, End_1 and End_x.

The file is 599 lines, about 2.4 times TM7. The informal proof is proof.md.

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

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

ours 525 lines
29% identical · 5 changed · 370 added
template 225 lines
67% kept verbatim · 70 not in ours
our items 35
7 identical · 3 adapted · 25 new · 1 template-only
identicalchanged / adaptedours only (new)template only
Template part: lines 1–17 (shared header, before the first Module) + 1627–1870 (body of Module TM7; the Module/End lines left out). Ours: lines 9–599 (header comment 1–8 left out). Line diff: Python difflib SequenceMatcher; inside a replaced block, line pairs at least 75% alike count as changed, the rest as removed + added.

Template-only names: RIncs_nxt

Side-by-side diff: template (225 lines) vs ours (525 lines), 445 lines differ; runs of identical lines and long template-only runs folded
identicalequal once each TM string is <TM>changedours onlytemplate only
templateours
1From BusyCoq Require Import Individual62 Longitudinal DivModCases.10From BusyCoq Require Import Individual62 Longitudinal DivModCases.
2Require Import ZifyNat Lia.11Require Import ZifyNat Lia.
⋯ 14 identical lines (template 3–1631, ours 12–31)
1632Notation d0 := [0;0;0].32Notation d0 := [0;0;0].
1633Notation d1 := [1;0;0].33Notation d1 := [1;0;0].
34Notation w1ld := [1;1;1;0].
1634Notation hR := (B,@nil Sym).35Notation hR := (B,@nil Sym).
1635Notation hR' := (D,[1]).36Notation hR' := (D,[1]).
⋯ 20 identical lines (template 1636–1659, ours 37–60)
1660| h1 => []61| h1 => []
1661end.62end.
64(* one h pass over the digits = +1 on the little-endian binary number of the 0/1 digits, L skipped *)
65Inductive Inc: list RD -> list RD -> Prop :=
66| Inc_nil: Inc [] [D1]
67| Inc_d0 r: Inc (D0::r) (D1::r)
68| Inc_d1 r r': Inc r r' -> Inc (D1::r) (D0::r')
69| Inc_ld r r': Inc r r' -> Inc (LD::r) (LD::r').
1663Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=71Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=
1664| RIncs_hx_ld k r r':72| RIncs_hx_ld k r r1 r':
1665 RIncs hx (1+k) r r' ->
73 Inc r r1 ->
74 RIncs hx (1+k) r1 r' ->
1666 RIncs hx k (LD::r) (LD::r')75 RIncs hx k (LD::r) (LD::r')
1668| RIncs_hx_d1 k r r':77| RIncs_hx_d1 k r r':
⋯ 3 identical lines (template 1669–1672, ours 78–81)
1673 RIncs hx (1+k) r r' ->82 RIncs hx (1+k) r r' ->
1674 RIncs hx k (D0::r) (LD::r')83 RIncs hx k (D0::r) (LD::r')
1676| RIncs_h1_ld k r r':85| RIncs_h1_ld k r r1 r':
1677 RIncs hx (1+k) r r' ->
86 Inc r r1 ->
87 RIncs hx (1+k) r1 r' ->
1678 RIncs h1 (1+k) (LD::r) (LD::r')88 RIncs h1 (1+k) (LD::r) (LD::r')
1680| RIncs_h1_d1 k r r':90| RIncs_h1_d1 k r r':
⋯ 14 identical lines (template 1681–1698, ours 91–109)
1699 RIncs h1 k [] r' ->110 RIncs h1 k [] r' ->
1700 RIncs h1 (2+k*2) [] (D1::r')111 RIncs h1 (2+k*2) [] (D1::r')
113| RIncs_h1_z1:
114 RIncs h1 0 [D1] [LD]
116| RIncs_h1_z0:
117 RIncs h1 0 [D0] [D1]
1701.118.
1703Ltac cat3 :=120Ltac cat3 :=
⋯ 6 identical lines (template 1704–1711, ours 121–128)
1713Ltac tr2 :=130Ltac tr2 :=
1714 eapply sideRLs_trans; [esx | ].131 eapply sideRLs_trans; [esx | ].
133Lemma z1_eq: [1] *> d1 *> 0inf = ld *> 0inf.
134Proof.
135 cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold.
136Qed.
138Lemma z0_eq: [1] *> d0 *> 0inf = d1 *> 0inf.
139Proof.
140 cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold.
141Qed.
1716Open Scope nat.143Open Scope nat.
145Lemma Inc_spec r r':
146 Inc r r' ->
147 sideRLs tm h (toRC r) (toRC r').
148Proof.
149 intro H.
150 induction H; cbn[toRC].
151 - esc.
152 - change h with (h++[]).
153 eapply segRLs_sideRLs_concat; [esx | constructor].
154 - eapply (@segRLs_sideRLs_concat tm h h); [esx | apply IHInc].
155 - eapply (@segRLs_sideRLs_concat tm h h); [esx | apply IHInc].
156Qed.
158Lemma seg_hx_ld k:
159 segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld.
160Proof.
161 rewrite lpow_add.
162 change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
163 eapply segRLs_trans; [esx | wal].
164Qed.
166Lemma seg_h1_ld k:
167 segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) w1ld ld.
168Proof.
169 rewrite lpow_add.
170 change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
171 eapply segRLs_trans; [esx | wal].
172Qed.
1718Lemma RIncs_spec tp k r r':174Lemma RIncs_spec tp k r r':
1719 RIncs tp k r r' ->175 RIncs tp k r r' ->
⋯ 2 identical lines (template 1720–1721, ours 176–177)
1722 intro H.178 intro H.
1723 induction H; intros; cbn[toH toH' toRC] in *.179 induction H; intros; cbn[toH toH' toRC] in *.
1724 - cat3; tr1; wal.
180 - eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]).
181 1: apply seg_hx_ld.
182 eapply sideRLs_trans.
183 1: apply Inc_spec; eassumption.
184 apply IHRIncs.
1725 - tr2.185 - tr2.
1726 cat3; wal.186 cat3; wal.
1727 - cat3; tr1; wal.187 - cat3; tr1; wal.
1728 - rewrite lpow_add,app_assoc.
188 - change ([] ++ h^^(1+k)) with (h^^1 ++ h^^k).
1729 eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]); [|eauto 1].189 eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]).
1730 tr1; wal.
190 1: apply seg_h1_ld.
191 eapply sideRLs_trans.
192 1: apply Inc_spec; eassumption.
193 apply IHRIncs.
1731 - rewrite lpow_add,app_assoc.194 - rewrite lpow_add,app_assoc.
1732 tr2.195 tr2.
⋯ 21 identical lines (template 1733–1753, ours 196–216)
1754 rewrite app_nil_l.217 rewrite app_nil_l.
1755 am 2 1 k 1 0.218 am 2 1 k 1 0.
219 - cbn[lpow app]. rewrite z1_eq. constructor.
220 - cbn[lpow app]. rewrite z0_eq. constructor.
221Qed.
223(* ---------- combinatorics of the sweep relation (no machine) ---------- *)
225Lemma Inc_total r: exists r', Inc r r'.
226Proof.
227 induction r as [|d r [r' I]].
228 - eexists; apply Inc_nil.
229 - destruct d; eexists.
230 + apply Inc_ld, I.
231 + apply Inc_d0.
232 + apply Inc_d1, I.
233Qed.
235Lemma Inc_fun r r1 r2: Inc r r1 -> Inc r r2 -> r1 = r2.
236Proof.
237 intro I. gen r2.
238 induction I; intros r2 I2; inversion I2; subst; try reflexivity; f_equal; auto.
239Qed.
241Lemma RIncs_eqk tp k k' r r': RIncs tp k r r' -> k = k' -> RIncs tp k' r r'.
242Proof. intros; subst; auto. Qed.
244Ltac inc_nil :=
245 repeat match goal with
246 | J: Inc [] _ |- _ => inversion J; subst; clear J
247 end.
249(* proof.md Lemma A: one more pass after the k passes is +1 on the result *)
250Lemma RIncs_Inc tp k r r' r'':
251 RIncs tp k r r' -> Inc r' r'' -> RIncs tp (1+k) r r''.
252Proof.
253 intro I. gen r''.
254 induction I; intros r'' J; inversion J; subst; inc_nil.
255 - eapply RIncs_hx_ld; eauto.
256 - apply RIncs_hx_d1; auto.
257 - apply RIncs_hx_d0; auto.
258 - eapply (RIncs_h1_ld (1+k)); eauto.
259 - apply (RIncs_h1_d1 (1+k)); auto.
260 - eapply RIncs_eqk; [apply RIncs_h1_d0_1; eauto | lia].
261 - eapply RIncs_eqk; [apply (RIncs_h1_d0_0 (1+k)); eauto | lia].
262 - apply (RIncs_h1_rh_1 0), RIncs_h1_rh_0.
263 - eapply RIncs_eqk; [apply RIncs_h1_rh_2; eauto | lia].
264 - eapply RIncs_eqk; [apply (RIncs_h1_rh_1 (1+k)); eauto | lia].
265 - apply (RIncs_h1_d1 0), RIncs_h1_rh_0.
266 - apply (RIncs_h1_d0_0 0), RIncs_h1_rh_0.
1756Qed.267Qed.
1758Lemma RIncs_nxt_1 k:269Lemma RIncs_nxt_1 k:
⋯ 10 identical lines (template 1759–1768, ours 270–279)
1769 Unshelve. all: lia.280 Unshelve. all: lia.
1770Qed.281Qed.
1773Ltac solve_v2 :=
283Lemma End_1 m w:
1774 (epose proof (RIncs_nxt_1 _) as [r I]; repeat ec; try apply I).
284 RIncs h1 m [] w -> forall q, m <= q -> exists w', RIncs h1 q w w'.
1776Ltac solve_v1 H tp'0 k'0 H' :=
1777 eapply H with (tp':=tp'0) (k':=k'0) in H';
⋯ 12 template-only lines (template 1778–1790), not in ours
1791 exists r'',
1792 RIncs tp' k' r' r''.
1793Proof.285Proof.
1794 gen tp k r' tp' k'.
286 intro I. remember h1 as t. remember (@nil RD) as e.
1795 induction r; intros.
287 induction I; intros q Hq; try discriminate; subst.
1796 {
288 - destruct q as [|q].
1797 gen tp r' tp' k'.
289 + eexists; apply RIncs_h1_z1.
1798 induction k using lt_wf_ind.
290 + destruct (RIncs_nxt_1 q) as [w I].
1799 intros.
291 eexists; apply (RIncs_h1_d1 q), I.
1800 inverts H1; destruct tp'.
292 - specialize (IHI eq_refl eq_refl).
1801 all: try lia.
293 destruct (mod2 q) as [b Hb|b Hb]; subst q.
1802 - solve_v2.
294 + destruct b as [|b]; [lia|].
1803 - destruct (sub k' 1); [subst|lia].
295 destruct (IHI b) as [w I2]; [lia|].
1804 solve_v2.
296 eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 | lia].
1805 - solve_v1 H0 hx (1+k') H3.
297 + destruct (IHI b) as [w I2]; [lia|].
1806 - destruct (sub k' 1); [subst|lia].
298 eexists; apply RIncs_h1_d0_0, I2.
1807 destruct (mod2 c); subst.
299 - specialize (IHI eq_refl eq_refl).
1808 + solve_v1 H0 h1 (a) H3.
300 destruct q as [|q]; [lia|].
1809 + solve_v1 H0 h1 (a) H3.
301 destruct (IHI q) as [w I2]; [lia|].
1810 - solve_v1 H0 h1 (k') H3.
302 eexists; apply (RIncs_h1_d1 q), I2.
1811 - destruct (sub k' 1); [subst|lia].
303Qed.
1812 solve_v1 H0 h1 (c) H3.
305Lemma End_x m w:
1813 }
306 RIncs h1 m [] w -> forall q, m <= 2*q+2 -> exists w', RIncs hx q w w'.
1814 {
307Proof.
1815 inverts H0; destruct tp'.
308 intro I. remember h1 as t. remember (@nil RD) as e.
1816 all: try lia.
309 induction I; intros q Hq; try discriminate; subst.
1817 - solve_v1 IHr hx (1+k') H7.
310 - destruct (RIncs_nxt_1 q) as [w I].
1818 - solve_v1 IHr hx (1+k') H7.
311 eexists; apply RIncs_hx_d1, I.
1819 - solve_v1 IHr hx (1+k') H7.
312 - specialize (IHI eq_refl eq_refl).
1820 - solve_v1 IHr hx (1+k') H7.
313 destruct (IHI (1+q)) as [w I2]; [lia|].
1821 - destruct (sub k' 1); [subst|lia].
314 eexists; apply RIncs_hx_d0, I2.
1822 solve_v1 IHr hx (1+c) H7.
315 - destruct (End_1 _ _ I q) as [w I2]; [lia|].
1823 - solve_v1 IHr hx (1+k') H7.
316 eexists; apply RIncs_hx_d1, I2.
1824 - destruct (sub k' 1); [subst|lia].
317Qed.
1825 solve_v1 IHr hx (1+c) H7.
319(* inversion helpers *)
1826 - solve_v1 IHr hx (1+k') H7.
320Lemma inv_hx_ld k r rK: RIncs hx k (LD::r) rK ->
1827 - destruct (sub k' 1); [subst|lia].
321 exists r1 rK', Inc r r1 /\ RIncs hx (1+k) r1 rK' /\ rK = LD::rK'.
1828 destruct (mod2 c); subst.
322Proof. intro E; inversion E; subst; do 2 eexists; repeat split; eauto. Qed.
1829 + solve_v1 IHr h1 (a) H7.
324Lemma inv_hx_d1 k r rK: RIncs hx k (D1::r) rK ->
1830 + solve_v1 IHr h1 (a) H7.
325 exists rK', RIncs h1 k r rK' /\ rK = LD::rK'.
1831 - solve_v1 IHr h1 k' H7.
326Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.
1832 - destruct (sub k' 1); [subst|lia].
328Lemma inv_hx_d0 k r rK: RIncs hx k (D0::r) rK ->
1833 solve_v1 IHr h1 (c) H7.
329 exists rK', RIncs hx (1+k) r rK' /\ rK = LD::rK'.
1834 }
330Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.
332Lemma inv_h1_ld k r rK: RIncs h1 (1+k) (LD::r) rK ->
333 exists r1 rK', Inc r r1 /\ RIncs hx (1+k) r1 rK' /\ rK = LD::rK'.
334Proof. intro E; inversion E; subst; do 2 eexists; repeat split; eauto. Qed.
336Lemma inv_h1_d1 k r rK: RIncs h1 (1+k) (D1::r) rK ->
337 exists rK', RIncs h1 k r rK' /\ rK = LD::rK'.
338Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.
340Lemma inv_h1_d0 K r rK: RIncs h1 K (D0::r) rK ->
341 (exists A rK', K = 1+A*2 /\ RIncs h1 A r rK' /\ rK = D0::rK') \/
342 (exists A rK', K = 2+A*2 /\ RIncs h1 A r rK' /\ rK = D1::rK') \/
343 (K = 0 /\ r = [] /\ rK = [D1]).
344Proof.
345 intro E; inversion E; subst.
346 - left; do 2 eexists; repeat split; eauto.
347 - right; left; do 2 eexists; repeat split; eauto.
348 - right; right; auto.
349Qed.
351Lemma inv_z1 K rK: RIncs h1 K [D1] rK ->
352 (K = 0 /\ rK = [LD]) \/
353 (exists K0 rK', K = 1+K0 /\ RIncs h1 K0 [] rK' /\ rK = LD::rK').
354Proof.
355 intro E; inversion E; subst.
356 - right; do 2 eexists; repeat split; eauto.
357 - left; auto.
358Qed.
360(* proof.md section 3.3: the second sweep reads the first's output after j pending +1s *)
361Definition Inv tp k j tq q :=
362 match tp, tq with
363 | hx, hx => k <= q /\ j <= q
364 | h1, hx => k+1 <= q /\ j <= q
365 | h1, h1 => (j = 0 /\ 2*k+1 <= q) \/ (1 <= j /\ k+j <= q /\ 1 <= q)
366 | hx, h1 => False
367 end.
369Lemma key tp k r r1:
370 RIncs tp k r r1 ->
371 forall j rK tq q,
372 RIncs tp (k+j) r rK ->
373 Inv tp k j tq q ->
374 exists r2, RIncs tq q rK r2.
375Proof.
376 intro D.
377 induction D as [k r r1 r' Hi D IH | k r r' D IH | k r r' D IH
378 | k r r1 r' Hi D IH | k r r' D IH | a r r' D IH | a r r' D IH
379 | | a r' D IH | a r' D IH | | ];
380 intros j rK tq q E HI.
381 - (* hx_ld *)
382 destruct (inv_hx_ld _ _ _ E) as [r1' [rK' [Hi' [E' ->]]]].
383 rewrite (Inc_fun _ _ _ Hi' Hi) in E'.
384 destruct tq; cbn in HI; [|contradiction].
385 destruct (Inc_total rK') as [rK'' J].
386 destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
387 + eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
388 + cbn; lia.
389 + eexists; eapply RIncs_hx_ld; eassumption.
390 - (* hx_d1 *)
391 destruct (inv_hx_d1 _ _ _ E) as [rK' [E' ->]].
392 destruct tq; cbn in HI; [|contradiction].
393 destruct (Inc_total rK') as [rK'' J].
394 destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
395 + eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
396 + cbn; lia.
397 + eexists; eapply RIncs_hx_ld; eassumption.
398 - (* hx_d0 *)
399 destruct (inv_hx_d0 _ _ _ E) as [rK' [E' ->]].
400 destruct tq; cbn in HI; [|contradiction].
401 destruct (Inc_total rK') as [rK'' J].
402 destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
403 + eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
404 + cbn; lia.
405 + eexists; eapply RIncs_hx_ld; eassumption.
406 - (* h1_ld *)
407 destruct (inv_h1_ld (k+j) _ _ E) as [r1' [rK' [Hi' [E' ->]]]].
408 rewrite (Inc_fun _ _ _ Hi' Hi) in E'.
409 destruct (Inc_total rK') as [rK'' J].
410 destruct tq; cbn in HI.
411 + destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
412 * eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
413 * cbn; lia.
414 * eexists; eapply RIncs_hx_ld; eassumption.
415 + destruct q as [|q0]; [lia|].
416 destruct (IH (1+j) rK'' hx (S q0)) as [r2 I2].
417 * eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
418 * cbn; lia.
419 * eexists; eapply (RIncs_h1_ld q0); eassumption.
420 - (* h1_d1 *)
421 destruct (inv_h1_d1 (k+j) _ _ E) as [rK' [E' ->]].
422 destruct (Inc_total rK') as [rK'' J].
423 destruct tq; cbn in HI.
424 + destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
425 * eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
426 * cbn; lia.
427 * eexists; eapply RIncs_hx_ld; eassumption.
428 + destruct q as [|q0]; [lia|].
429 destruct (IH (1+j) rK'' hx (S q0)) as [r2 I2].
430 * eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
431 * cbn; lia.
432 * eexists; eapply (RIncs_h1_ld q0); eassumption.
433 - (* h1_d0_0 *)
434 destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]|[[A [rK' [HK [E' ->]]]]|[HK _]]]; [| |lia].
435 + (* rK = D0::rK' *)
436 assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption | lia]).
437 destruct tq; cbn in HI.
438 * destruct (IH (A-a) rK' hx (1+q) E2) as [r2 I2]; [cbn; lia|].
439 eexists; apply RIncs_hx_d0, I2.
440 * destruct (mod2 q) as [b Hb|b Hb]; subst q.
441 -- destruct b as [|b]; [lia|].
442 destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia|].
443 eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 | lia].
444 -- destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia|].
445 eexists; apply RIncs_h1_d0_0, I2.
446 + (* rK = D1::rK' *)
447 assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption | lia]).
448 destruct tq; cbn in HI.
449 * destruct (IH (A-a) rK' h1 q E2) as [r2 I2]; [cbn; lia|].
450 eexists; apply RIncs_hx_d1, I2.
451 * destruct q as [|q0]; [lia|].
452 destruct (IH (A-a) rK' h1 q0 E2) as [r2 I2]; [cbn; lia|].
453 eexists; apply (RIncs_h1_d1 q0), I2.
454 - (* h1_d0_1 *)
455 destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]|[[A [rK' [HK [E' ->]]]]|[HK _]]]; [| |lia].
456 + (* rK = D0::rK' *)
457 assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption | lia]).
458 destruct tq; cbn in HI.
459 * destruct (IH (A-a) rK' hx (1+q) E2) as [r2 I2]; [cbn; lia|].
460 eexists; apply RIncs_hx_d0, I2.
461 * destruct (mod2 q) as [b Hb|b Hb]; subst q.
462 -- destruct b as [|b]; [lia|].
463 destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia|].
464 eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 | lia].
465 -- destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia|].
466 eexists; apply RIncs_h1_d0_0, I2.
467 + (* rK = D1::rK' *)
468 assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption | lia]).
469 destruct tq; cbn in HI.
470 * destruct (IH (A-a) rK' h1 q E2) as [r2 I2]; [cbn; lia|].
471 eexists; apply RIncs_hx_d1, I2.
472 * destruct q as [|q0]; [lia|].
473 destruct (IH (A-a) rK' h1 q0 E2) as [r2 I2]; [cbn; lia|].
474 eexists; apply (RIncs_h1_d1 q0), I2.
475 - (* rh_0 *)
476 destruct tq; cbn in HI.
477 + eapply End_x; [eassumption | lia].
478 + eapply End_1; [eassumption | lia].
479 - (* rh_1 *)
480 destruct tq; cbn in HI.
481 + eapply End_x; [eassumption | lia].
482 + eapply End_1; [eassumption | lia].
483 - (* rh_2 *)
484 destruct tq; cbn in HI.
485 + eapply End_x; [eassumption | lia].
486 + eapply End_1; [eassumption | lia].
487 - (* z1 *)
488 destruct (inv_z1 _ _ E) as [[HK ->]|[K0 [rK' [HK [E' ->]]]]].
489 + destruct tq; cbn in HI.
490 * destruct (RIncs_nxt_1 (1+q)) as [w I].
491 eexists; eapply RIncs_hx_ld; [apply Inc_nil | apply RIncs_hx_d1, I].
492 * destruct q as [|q0]; [lia|].
493 destruct (RIncs_nxt_1 (1+q0)) as [w I].
494 eexists; eapply (RIncs_h1_ld q0); [apply Inc_nil | apply RIncs_hx_d1, I].
495 + destruct (Inc_total rK') as [rK'' J].
496 pose proof (RIncs_Inc _ _ _ _ _ E' J) as E''.
497 destruct tq; cbn in HI.
498 * destruct (End_x _ _ E'' (1+q)) as [w I]; [lia|].
499 eexists; eapply RIncs_hx_ld; eassumption.
500 * destruct q as [|q0]; [lia|].
501 destruct (End_x _ _ E'' (1+q0)) as [w I]; [lia|].
502 eexists; eapply (RIncs_h1_ld q0); eassumption.
503 - (* z0 *)
504 destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]|[[A [rK' [HK [E' ->]]]]|[HK [_ ->]]]].
505 + destruct tq; cbn in HI.
506 * destruct (End_x _ _ E' (1+q)) as [w I]; [lia|].
507 eexists; apply RIncs_hx_d0, I.
508 * destruct (mod2 q) as [b Hb|b Hb]; subst q.
509 -- destruct b as [|b]; [lia|].
510 destruct (End_1 _ _ E' b) as [w I]; [lia|].
511 eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I | lia].
512 -- destruct (End_1 _ _ E' b) as [w I]; [lia|].
513 eexists; apply RIncs_h1_d0_0, I.
514 + destruct tq; cbn in HI.
515 * destruct (End_1 _ _ E' q) as [w I]; [lia|].
516 eexists; apply RIncs_hx_d1, I.
517 * destruct q as [|q0]; [lia|].
518 destruct (End_1 _ _ E' q0) as [w I]; [lia|].
519 eexists; apply (RIncs_h1_d1 q0), I.
520 + destruct tq; cbn in HI.
521 * destruct (RIncs_nxt_1 q) as [w I].
522 eexists; apply RIncs_hx_d1, I.
523 * destruct q as [|q0]; [lia|].
524 destruct (RIncs_nxt_1 q0) as [w I].
525 eexists; apply (RIncs_h1_d1 q0), I.
526Qed.
528Lemma domain r r':
529 RIncs hx 0 r r' -> exists r'', RIncs hx 0 r' r''.
530Proof.
531 intro I.
532 eapply (key _ _ _ _ I 0 r' hx 0).
533 - apply I.
534 - cbn; lia.
1835Qed.535Qed.
1837Open Scope sym.538Open Scope sym.
⋯ 12 identical lines (template 1839–1852, ours 540–553)
1853 es.554 es.
1854Qed.555Qed.
557Lemma start: c0 -->* S' [LD;D1].
558Proof. esx. Qed.
1856Lemma nonhalt: ~halts tm c0.560Lemma nonhalt: ~halts tm c0.
1857Proof.561Proof.
1858 eapply multistep_nonhalt with (c':=S' [D1]).562 eapply multistep_nonhalt with (c':=S' [LD;D1]).
1859 1: esx.
563 1: apply start.
1860 eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').564 eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').
1861 2: repeat ec.
565 2: {
566 exists [LD;LD;LD;D1;D1].
567 eapply RIncs_hx_ld; [apply Inc_d1, Inc_nil |].
568 apply RIncs_hx_d0. apply RIncs_hx_d1.
569 apply (RIncs_h1_rh_2 0), RIncs_h1_rh_0.
570 }
1862 intros r [r' I1].571 intros r [r' I1].
1863 pose proof I1 as I2.
1864 eapply RIncs_nxt with (tp':=hx) (k':=O) in I2.
1865 2: lia.
1866 exists r'; split.572 exists r'; split.
1867 - apply BigStep,I1.573 - apply BigStep, I1.
1868 - apply I2.
574 - apply (domain _ _ I1).
1869Qed.575Qed.
577Close Scope sym.
579(*
580```
5811RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---
583S(r) = 0^inf 11 D> <r> 0^inf digits: L = 110, 0 = 000, 1 = 100
584start: 0^inf A> 0^inf -->* S(L1) (S(1) at step 5, S(L1) at step 16)
585sweep: S(r) -->+ S(r') if RIncs hx 0 r r'
587inc(r): +1 on the little-endian binary number of the 0/1 digits of r, L skipped,
588 a carry out of the last digit appends a 1
589eater (hx,k): L -> L, k+1, inc the rest; 0 -> L, k+1; 1 -> L, drain with k
590drain (h1,k): L -> L, eater with k, inc the rest (k >= 1); 1 -> L, k-1 (k >= 1)
591 0 -> 0, (k-1)/2 (k odd); 0 -> 1, (k-2)/2 (k even, k >= 2)
592right end (h1,k): k = 0 -> 1; k odd -> 0, (k-1)/2; k even -> 1, (k-2)/2
593last digit, drain with k = 0: 1 -> L, 0 -> 1 (1 100 0^inf = 110 0^inf, 1 000 0^inf = 100 0^inf)
595domain: RIncs hx 0 r r' -> exists r'', RIncs hx 0 r' r''
596 (key: a second sweep reading the first one's output after j pending +1 passes,
597 under Inv; with j = 0 these are TM7's RIncs_nxt conditions)
598```
599*)
3Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.

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

#kindnamestatement (no proof body)linevs template
1Definitiontm
Definition tm := Eval compute in (TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").
L27identicalexcept the TM string
2InductiveRD
Inductive RD := LD|D0|D1.
L41identical
3InductiveH
Inductive H := hx|h1.
L42identical
4FixpointtoRC
Fixpoint toRC ls :=
match ls with
| [] => 0inf
| LD::ls => ld*>toRC ls
| D0::ls => d0*>toRC ls
| D1::ls => d1*>toRC ls
… +1 lines
L44identical
5DefinitiontoH'
Definition toH' x :=
match x with
| hx => []
| h1 => [1]
end.
L52identical
6DefinitiontoH
Definition toH x :=
match x with
| hx => h'
| h1 => []
end.
L58identical
7InductiveInc
Inductive Inc: list RD -> list RD -> Prop :=
| Inc_nil: Inc [] [D1]
| Inc_d0 r: Inc (D0::r) (D1::r)
| Inc_d1 r r': Inc r r' -> Inc (D1::r) (D0::r')
| Inc_ld r r': Inc r r' -> Inc (LD::r) (LD::r').
L65new
8InductiveRIncs
Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=
| RIncs_hx_ld k r r1 r':
  Inc r r1 ->
  RIncs hx (1+k) r1 r' ->
  RIncs hx k (LD::r) (LD::r')

… +42 lines
L71adapted
9Lemmaz1_eq
Lemma z1_eq: [1] *> d1 *> 0inf = ld *> 0inf.
L133new
10Lemmaz0_eq
Lemma z0_eq: [1] *> d0 *> 0inf = d1 *> 0inf.
L138new
11LemmaInc_spec
Lemma Inc_spec r r':
Inc r r' ->
sideRLs tm h (toRC r) (toRC r').
L145new
12Lemmaseg_hx_ld
Lemma seg_hx_ld k:
segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld.
L158new
13Lemmaseg_h1_ld
Lemma seg_h1_ld k:
segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) w1ld ld.
L166new
14LemmaRIncs_spec
Lemma RIncs_spec tp k r r':
RIncs tp k r r' ->
sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').
L174adapted
15LemmaInc_total
Lemma Inc_total r: exists r', Inc r r'.
L225new
16LemmaInc_fun
Lemma Inc_fun r r1 r2: Inc r r1 -> Inc r r2 -> r1 = r2.
L235new
17LemmaRIncs_eqk
Lemma RIncs_eqk tp k k' r r': RIncs tp k r r' -> k = k' -> RIncs tp k' r r'.
L241new
18LemmaRIncs_Inc
Lemma RIncs_Inc tp k r r' r'':
RIncs tp k r r' -> Inc r' r'' -> RIncs tp (1+k) r r''.
L250new
19LemmaRIncs_nxt_1
Lemma RIncs_nxt_1 k:
exists r, RIncs h1 k [] r.
L269identical
20LemmaEnd_1
Lemma End_1 m w:
RIncs h1 m [] w -> forall q, m <= q -> exists w', RIncs h1 q w w'.
L283new
21LemmaEnd_x
Lemma End_x m w:
RIncs h1 m [] w -> forall q, m <= 2*q+2 -> exists w', RIncs hx q w w'.
L305new
22Lemmainv_hx_ld
Lemma inv_hx_ld k r rK: RIncs hx k (LD::r) rK ->
exists r1 rK', Inc r r1 /\ RIncs hx (1+k) r1 rK' /\ rK = LD::rK'.
L320new
23Lemmainv_hx_d1
Lemma inv_hx_d1 k r rK: RIncs hx k (D1::r) rK ->
exists rK', RIncs h1 k r rK' /\ rK = LD::rK'.
L324new
24Lemmainv_hx_d0
Lemma inv_hx_d0 k r rK: RIncs hx k (D0::r) rK ->
exists rK', RIncs hx (1+k) r rK' /\ rK = LD::rK'.
L328new
25Lemmainv_h1_ld
Lemma inv_h1_ld k r rK: RIncs h1 (1+k) (LD::r) rK ->
exists r1 rK', Inc r r1 /\ RIncs hx (1+k) r1 rK' /\ rK = LD::rK'.
L332new
26Lemmainv_h1_d1
Lemma inv_h1_d1 k r rK: RIncs h1 (1+k) (D1::r) rK ->
exists rK', RIncs h1 k r rK' /\ rK = LD::rK'.
L336new
27Lemmainv_h1_d0
Lemma inv_h1_d0 K r rK: RIncs h1 K (D0::r) rK ->
(exists A rK', K = 1+A*2 /\ RIncs h1 A r rK' /\ rK = D0::rK') \/
(exists A rK', K = 2+A*2 /\ RIncs h1 A r rK' /\ rK = D1::rK') \/
(K = 0 /\ r = [] /\ rK = [D1]).
L340new
28Lemmainv_z1
Lemma inv_z1 K rK: RIncs h1 K [D1] rK ->
(K = 0 /\ rK = [LD]) \/
(exists K0 rK', K = 1+K0 /\ RIncs h1 K0 [] rK' /\ rK = LD::rK').
L351new
29DefinitionInv
Definition Inv tp k j tq q :=
match tp, tq with
| hx, hx => k <= q /\ j <= q
| h1, hx => k+1 <= q /\ j <= q
| h1, h1 => (j = 0 /\ 2*k+1 <= q) \/ (1 <= j /\ k+j <= q /\ 1 <= q)
| hx, h1 => False
… +1 lines
L361new
30Lemmakey
Lemma key tp k r r1:
RIncs tp k r r1 ->
forall j rK tq q,
RIncs tp (k+j) r rK ->
Inv tp k j tq q ->
exists r2, RIncs tq q rK r2.
L369new
31Lemmadomain
Lemma domain r r':
RIncs hx 0 r r' -> exists r'', RIncs hx 0 r' r''.
L528new
32DefinitionS'
Definition S' r :=
lh {{{ (hR',R) }}} toH' hx *> toRC r.
L542new
33LemmaBigStep
Lemma BigStep r r':
RIncs hx 0 r r' ->
S' r -->+ S' r'.
L545new
34Lemmastart
Lemma start: c0 -->* S' [LD;D1].
L557new
35Lemmanonhalt
Lemma nonhalt: ~halts tm c0.
L560adapted
4What a maintainer readsCheck: the rule table below is what the .v proves, and proof.md / README read cleanly for a maintainer.
submission/proof.md line 32: 2. Rule table
1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---      (SOMDCv6 TM7 with A1 = 0RF instead of 0RC)

S(r) = 0^inf 11 D> <r> 0^inf          L = 110, 0 = 000, 1 = 100
start: 0^inf A> 0^inf  -(5)->  S(1)
sweep: S(r) -+-> S(r')  if R(hx,0,r,r')            (r' starts one cell further left)
domain P(r) := exists r', R(hx,0,r,r');   P(1);   P(r) /\ R(hx,0,r,r') -> P(r')

Inc (one h pass = +1):
  I1  Inc(1::r, 0::r')  <- Inc(r,r')         I3  Inc(L::r, L::r')  <- Inc(r,r')
  I2  Inc(0::r, 1::r)                        I4  Inc([], [1])

R (k >= 0); NEW = differs from TM7's RIncs:
  X1  R(hx,k,    L::r, L::r')  <- Inc(r,r1), R(hx,k+1,r1,r')   NEW (TM7: R(hx,k+1,r,r'))  RIncs_hx_ld
  X2  R(hx,k,    0::r, L::r')  <- R(hx,k+1,r,r')                                          RIncs_hx_d0
  X3  R(hx,k,    1::r, L::r')  <- R(h1,k,r,r')                                            RIncs_hx_d1
  C1  R(h1,k+1,  L::r, L::r')  <- Inc(r,r1), R(hx,k+1,r1,r')   NEW (TM7: R(hx,k+1,r,r'))  RIncs_h1_ld
  C2  R(h1,k+1,  1::r, L::r')  <- R(h1,k,r,r')                                            RIncs_h1_d1
  C3  R(h1,2k+1, 0::r, 0::r')  <- R(h1,k,r,r')                                            RIncs_h1_d0_0
  C4  R(h1,2k+2, 0::r, 1::r')  <- R(h1,k,r,r')                                            RIncs_h1_d0_1
  R0  R(h1,0,    [],   [1])                                                               RIncs_h1_rh_0
  R1  R(h1,2k+1, [],   0::r')  <- R(h1,k,[],r')                                           RIncs_h1_rh_1
  R2  R(h1,2k+2, [],   1::r')  <- R(h1,k,[],r')                                           RIncs_h1_rh_2
  Z1  R(h1,0,    [1],  [L])     NEW: 0 passes, 1 100 0^inf = 110 0^inf
  Z0  R(h1,0,    [0],  [1])     NEW: 0 passes, 1 000 0^inf = 100 0^inf
  (no clause: hx at the right end; h1 with 0 passes on a word other than [], [1], [0])

machine level (j = number of digits of X before its first 0 digit, or |X| if none):
  B> 100 X  -(3)->  000 B> X            B> 000 X  -(1)->  <C 100 X        B> 0^inf  -(1)->  <C 100 0^inf
  B> 110 X  -(3)->  011 B> X            011 <C  -(3)->  <C 110            000 <C  -(3)->  <C 000
     =>  B> <X> 0^inf  -(6j+1)->  <C <X+1> 0^inf                       (Inc, no A1)
  eater enters L:   1 D> 110 <X>  -(6j+13)->  1 111 D> <X+1>       TM7: -(11)-> 1 111 D> <X>
  drain enters L:   B> 1 110 <X>  -(6j+12)->  1 111 D> <X+1>       TM7: -(10)-> 1 111 D> <X>
  wall:             0^inf 1 <C <r'>  -(3)->  0^inf 11 D> <r'>      (C1, D0, D0)

In words:

  • Eater (hx). The eater turns every digit it crosses into L. It gains one pass at each L or 0, and at each L the rest of the word gets +1 (X1, NEW). It switches to draining at the first 1 (X3).
  • Drain (h1, k passes). Each 1 absorbs one pass and becomes L (C2). Each 0 keeps one bit of the count and halves it (C3, C4). At the right end the count is written in bijective binary (R0–R2). An L restarts the eater with the same count and adds +1 to the rest (C1, NEW; this is the "drain-enters-L restart"). With 0 passes left, the drain can only be at the last digit, and it leaves the stray 1 in place (Z0, Z1, NEW).

Worked example. This is the start of the Checkpoint A picture pair, S(L^4 1L1), and it is the extra 1 Dennis noticed there (checked in §7).

  • First eat. Both machines eat the 4 L's (k = 4) and stop at the 1. Ours added +1 at each L, so its rest is 1L1 + 4 = 1L11, while TM7's is still 1L1. The extra 1 digit on the right is the extra bar after the first eat.
  • Drain. The first drain pass enters the L.
  • TM7 restarts the eater on 1.
  • Ours first runs +1 pass number 5: 11 + 1 = 001. The extra 1 is not ignored: the carry turns both 1s into 0s and appends a new 1.
  • Second eat. Ours also eats the two new 0s (k = 6). TM7 stops at once (k = 4).
  • Right end. The count is written in bijective binary: 6 gives 111, 4 gives 101.
  • Result. Ours reaches S(L^9 111) and TM7 reaches S(L^7 101). Ours has two more L's on the left, and the right end differs.
5FamilyCheck: related machines are killed together or have a reason to be left open.

2 machines, 1 killed, 1 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
#2 kill 11RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---✓Killed: never haltsthis kill
#231RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---▲Stuckparent link; targeting: follow-on to #2; ledger: #23 = twin of #2; named in #23's proof.md · page
6ChecklistCheck: every ✓ is computed; the two ○ are yours to decide; an amber ! is an optional check that did not finish.
  • ✓
    Machine string exact
    the .v literal == holdout list line 301 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 1.29 s
  • ✓
    .v hash matches the checked hash
    .v = checked sha256 e434537eca67…; submission/ copy = checked sha256 e434537eca67…
  • ✓
    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: 8 error(s); L3 working-copy; L3 submission-copy; L74 checkpoint; L74 pilot-name; L263 review-log; L265 skeptic, submission/discord/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---_writeup.md: 2 error(s); L73 checkpoint; L73 pilot-name
  • ○
    proof.md reviewed by Dennis (Checkpoint B)
    no Checkpoint B note from Dennis found
    • notes.md L129: - 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 before posting.
    • notes.md L132: ## Checkpoint B (Dennis), 2026-10-10
  • ○
    Family posted together?
    no other kill in the family; 1 member(s) not killed: #23

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 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---

Review pages on file: compare.html · review.html

Files

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

namesizechanged
notes.md ↓12 KB2026-10-10 12:19
proof.md ↓24 KB2026-10-10 04:46
how_proved.md ↓1.6 KB2026-10-14 10:51
status.json ↓645 B2026-10-10 18:03
observe.json ↓12 KB2026-10-10 04:41
1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v ↓19 KB2026-10-10 11:50
check_kill.txt ↓11 KB2026-10-14 14:27
compare/4 items2026-10-10 11:15
img/8 items2026-10-10 02:14
review/14 items2026-10-13 15:48
rocq/3 items2026-10-10 04:45
rocq-scratch/3 items2026-10-10 03:53
scripts/1 item2026-10-10 02:18
submission/6 items2026-10-10 12:07
check_proof.py ↓29 KB2026-10-10 04:44
check_rules.py ↓11 KB2026-10-10 02:15
compare.html ↓498 KB2026-10-13 15:48
cov_all_1e7.txt ↓155 B2026-10-10 11:54
review.html ↓132 KB2026-10-13 15:48
rocq-plan.md ↓18 KB2026-10-10 04:11
status.json in full
{
 "tm": "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "pr": "https://github.com/ccz181078/busycoq/pull/14",
 "pr_file": "verify/BellEatsCounter_1RB0RF.v",
 "posted": "PR #14 opened and Discord post made 2026-10-10 (Dennis)",
 "pr_state": "merged",
 "merged": "2026-10-10T20:47:35Z (ccz181078, merge commit 9cf9e88; upstream file verify/BellEatsCounter_1RB0RF.v)",
 "holdouts_740": "absent (removed: solved by our PR #14)",
 "pr_merged_at": "2026-10-10T20:47:35Z",
 "pr_merged_by": "ccz181078",
 "pr_comments": 0
}