Built . It shows the files as they were then (ages and “working now” follow your clock).
tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.Machines / W5-7
1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
How we proved it halts
An exploding counter whose carry finally runs off its end
Left of the head is a binary counter, lowest digit next to the head, each digit six cells long: 111111 for a 1, 001111 for a 0, with lone 001s as spacers here and there. Right of the head is a tally, a row of 011 blocks. Every bounce of the head adds 1 to the counter, like an odometer clicking, and one block to the tally.
The key idea is what happens when the counter is all 1s. The head walks to its far end and rewrites it on the way back, shifted by three cells, while the tally turns into new low digits: a block of 0s, about one per two tally blocks, plus a single 1. Filling n zeros back up takes at least 2^n − 1 bounces, each adding a tally block, so every new block of zeros is roughly 2 to the power of the previous one: the first three overflows add 2, 25 and 654,311,423 zeros.
Why it halts: after the first 38,573 steps, simulated directly, the proof records each block only as "at least so many digits" (the rules work the same on any longer block) and pushes that through 192 more cycles. In the 195th overflow, the rewrite near the far end must add 1 to a stretch of all-1 digits with nothing beyond them, so the carry falls off the end. The machine then reads a 1 in state F, the one case its table leaves undefined, 1,368 steps after the head reached the last 63 cells of the counter. The step count is unknown; a rough estimate is a tower of 2s about 195 levels high.
The table is busycoq's TM3 with the states renamed, so TM3's rules are re-proved with its own scripts. Rocq also checks the new lower-bound rules, the 192 cycles and the final 1,368 steps; it proves halting, not the step count.
#25local proof number
838lines of Rocq
26 sto compile
6/6automatic checks
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
Claimed by someone else
We proved this machine locally, but our proof was still unsubmitted when we found it already covered upstream.
Submit completed proofs early. A local proof does not secure an upstream claim.
Upstream proof ↗ · Recorded timeline
What the timing evidence establishes
This describes upstream credit, not who first discovered the mathematics. The records do not establish adoption of our proof, first public push time, or whether an earlier submission would have secured credit.
Overview
In one sentence
SOBCv6 TM3's table from TM3's B: 194 shift-overflow cycles, then a far-end carry halts it (tower ~195).
Submitted mechanism Counter and register. Left of the head is a binary counter in the words W0 = 001 and W1 = 111 (W1 W0 = digit 0, W1 W1 = digit 1, a lone W0 a separator). Right of the head is the register 1 (011)^n 01. Each increment is one bounce and adds one 011. (submission/README.md, Mechanism)
- Upstream
- The blank-start machine halts: PR_SOBC.v.TM2 ↗. We also have a local proof. This upstream addition is separate from our merged submissions; adoption credit is not established.
- Rocq proof
- check_kill PASS · first Oct 13 04:35838 lines · 23 KB .v · compile 25.6 s · coqchk pass · 1 axioms · PASS Oct 13 04:35· the .v file
- Automatic review
- 6 of 6 checks passtemplate: verify/SOBCv6.v Module TM3 (adapted from) · details in Proof →
- Class
- Shift-overflow bouncer counterours: Shift-overflow bouncer counter (sheet) · ours adds: SOBCv6 TM3's table started in TM3's B; halts after 194 cycles · high confidence
- On the list
- not on
BB6_holdouts_663.txt(line 700 of the previous list) · historical 740 line 700 · observe.json rank #700
Mechanism
What to check here: the pictures show the mechanism that the rule table describes.
How it works: 3 notes
- Same table as SOBCv6.v TM3 (ours A,B,C,D,E,F = TM3 B,C,A,E,D,F), blank start = TM3 started in B. Left = binary counter of words 001/111 (W0 separator, W1 b = digit b, LSB at the head); right = RC n = 1 (011)^n 01. TM3's proved rules apply verbatim: Incs fills the counter while RC grows by the fill count c; Ov turns RC(2m+2) into m new zero digits and re-reads the old counter with a shift (LOv).
- From blank the chain starts at step 847 (x = 1000111011): counts 5, 51, 1,308,622,847, then each count is about 2 to the previous one (shift overflow). Near the head the list freezes into segments between huge (10)^k blocks; the far tail (100-200 symbols) keeps changing.
- In the 195th overflow (cycle 194) LOv must increment 0^11 11 11 11 at the far end: the carry runs off the tape and the machine halts (F reads 1). Direct sims of the instantiated tape halt 64 cells from the far end for every block size tried; no earlier cycle hits any failure case.
Figures for Checkpoint A
Fig 1 · Two counter cycles from blank
Rows every 40 steps. The fan is RC growing per bounce; watch the bottom rows near step 37,000.
bbchallenge-defaultStart blankRows every 40 stepsWindow cells -13..246, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: 0..40,000 (1,001 rows); P-configs at steps 847, 2,136 and 38,573
Top: walk into the full counter and back. Middle: RC is cleared. Bottom zigzag: RC becomes new digits.
bbchallenge-defaultStart mid-run: step 37,120Rows every step, 37,120..38,580Window cells -46..183, 1 px = 0.5 cellsColors 1 0 or unvisited head (last move right/left)
Start: tape rebuilt from the run: full counter <D 010 1 (011)52 01 · Rows: (1,461 rows, 2 px each); the next P-config is the row for step 38,573 · Window: (each cell 2x2 px); cell 0 = the head's start cell (run cell 40)
Only the far 25 tokens of the cycle-194 counter, filled. Follow the last leftward run to the left edge.
bbchallenge-defaultStart constructed tape (below)Rows every step 0..1,541Window cells -126..12, 1 px = 0.5 cellsColors 1 0 or unvisited head (last move right/left)
Start: 0∞ 118 02 17 02 17 02 17 02 17 02 125 02 17 02 125 02 1 02 1 <D 0 1 0 1 0 12 0 12 0 1 0∞ · Rows: (1,542 rows, 2 px each); the last row is the halt · Window: (each cell 2x2 px); cell 0 = the head's start cell, the counter's far end is cell -122
More figures (1)Fig 4: bbchallenge Default view, 10,000 steps
Orientation: the counter sits at the left edge; the right part grows with each bounce.
bbchallenge-defaultStart blankRows every step 0..9,999Window cells -200..199, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: squeezed into 500 px by the site's bilinear filter (about one sample per 20 steps)
Rules (4/4 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| Incs (TM3, proved) | Lmp x <D 010 1 011 01 0∞ ⟶ Lmp ones(x) <D 010 1 (011)c+1 01 0∞ | c = 2^D - 1 - value(x), must be odd (lowest digit 0) | — | ✓278/278 |
| Ov (TM3, proved) | Lmp ones(x) <D 010 1 (011)2m+2 01 0∞ ⟶ Lmp ((W1 W0)m W1 W1 v[1:]) <D 010 1 011 01 0∞ | v = LOv(ones(x)) must start with W0; LOv's increments must not carry off the far end | — | ✓63/63 |
| chain from blank | P x at step 847, x = 1000111011 ⟶ P-configs at steps 2,136 and 38,573 (exact tape match) | then counts 1,308,622,847 and towers; model cycles 2..193 checked by sim on instantiated tapes | — | ✓2/2 |
| far-end halt (cycle 194) | Lmp ones(x_193) <D 010 1 (011)2m+2 01 0∞ ⟶ halt | LOv at far token 10 must increment 0^11 11 11 11: carry off the far end, F reads 1 | — | ✓12/12 |
Compressed historythe tape as P-config: 0∞ Lmp(x) <D 010 1 011 01 0∞ (x = counter, D digit pairs) at 3 moments: where the rules are read off
P-config: 0∞ Lmp(x) <D 010 1 011 01 0∞ (x = counter, D digit pairs)
| step | D | c | n0 |
|---|---|---|---|
| 847 | 4 | 5 | 2 |
| 2,136 | 7 | 51 | 25 |
| 38,573 | 32 | 1,308,622,847 | 654,311,423 |
Dlast 32clast 1,308,622,847n0last 654,311,423Template comparisonSOBCv6.v TM3: partly applies · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | 0RD |
| B | 1LC | 1RE |
| C | 1LA | 0LD |
| D | 0RE | 0RF |
| E | 1LC | 1RA |
| F | 0LE | --- |
- file
SOBCv6.v:1164- module
TM3- machine
1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD---(10 transitions apart)- diff
same table after renaming (ours A,B,C,D,E,F = TM3 B,C,A,E,D,F); only the start state differs- note
- All of TM3's rule lemmas carry over (rename E->D, B->A). New: init (blank -> P x at step 847), 194 step_recs instead of 2, LInc_rec through (10) blocks with a lower bound, explicit pairs on the far side of abstract blocks (TM3's layout breaks at our cycle 4), and a far-end 'overflow halts' predicate instead of TM3's near-head direct run.
Proof strategy & riskshow the formal proof will go · 3 risks to watch
HALT proof from TM3's module: new init by solve_init to step 847, a lower-bounded block representation, 194 step_recs by vm_compute, then an inductive 'overflow halts' predicate (deep part halts => whole halts) with a far-end base case.
- ▲194 vm_compute step_recs on lists up to ~38.5k items may be slow; fallback: compress the frozen near-head segments.
- ▲The block representation must carry lower bounds (k >= 2) for LInc through (10) blocks; get the layout wrong and LOv_rec fails as TM3's did at our cycle 4.
- ▲The final halt needs a new predicate over the whole counter (~190 abstract blocks); TM3's near-head step1 tail does not reach the far end.
Stats & provenance109 steps simulated · 28,806 cells · the status in full · files
- simulated
- 109 steps
- tape
- 28,806 cells · 18,608 nonzeros
- growth
- cycle k+1 has about 2^(cycle k count) bounces: power tower; halting time a tower of height about 195
- status now
- check_kill --halt PASS, independently re-verified (status.json, 2026-10-13)
- observer's note
- Mechanism = SOBCv6 TM3's proved rules; model predicts a halt in cycle 194, reproduced by direct simulation of instantiated tapes. Next: formal HALT proof.
- files
- observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v
Proof & checks
6/6 automatic checks pass
Kill 25 · Shift-overflow bouncer counter · the kill file 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v: 838 lines, 59 items · the package submission/
✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (adapted from): verify/SOBCv6.v Module TM3 · 57% of our lines identical
1What is provedCheck: the string, the theorem and every check_kill line are green, and the .v on disk is the one that was checked (same sha256).
Machine
1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---vs holdout list
Theorem
check_kill
✓ PASS
· 17/17 checks pass
· compile 25.61 s · coqchk pass
(43.32 s) · assumptions: 1
(Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g)
· 2026-10-13 11:35:43 UTC
· submission/check_kill.txt
Checked .v
sha256 30ba969372712e44…
| ✓ | 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v | 30ba969372712e44… = checked |
| ✓ | submission/1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v | 30ba969372712e44… = checked |
Status
✓Killed: halts
updated 2026-10-13
✓ args✓ input✓ framework✓ framework_build✓ forbidden✓ structure✓ tm_text✓ theorem_text✓ coq✓ names✓ compile✓ tm_rocq✓ theorem_rocq✓ isolation✓ assumptions✓ coqchk✓ integrity
All 17 check_kill checks with their one-line results
| ✓ | args | 6x2 machine, framework module Individual62, mode halt |
| ✓ | input | 23312 bytes, 838 lines, 470 sentences |
| ✓ | framework | HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/ |
| ✓ | framework_build | 19 needed framework .vo files present and fresh, with native code no older than the .vo |
| ✓ | forbidden | none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token) |
| ✓ | structure | 11 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced |
| ✓ | tm_text | line 39: TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---" == <tm> (41 bytes) |
| ✓ | theorem_text | line 797: halt : halts tm c0 |
| ✓ | coq | coqc 8.20.1 ([local working file] |
| ✓ | names | halts, c0, TM_from_str resolved inside Individual62 |
| ✓ | compile | compiled in 25.6s with all appended checks |
| ✓ | tm_rocq | BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---" by eq_refl (in-file and isolated) |
| ✓ | theorem_rocq | halt : halts (TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---") c0 with absolute names (in-file and isolated) |
| ✓ | isolation | only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off |
| ✓ | assumptions | 1 assumption(s), all in the baseline |
| ✓ | coqchk | coqchk -norec BB6Kill.Candidate ok (43.3s); its context summary lists nothing of the file's own |
| ✓ | integrity | input sha256 and framework HEAD/cleanliness identical before and after |
2Where it came fromCheck: the template is the one you expect, and the measured reuse (tiles, the reuse figure, diff) agrees with what the README says was kept and changed (quoted).
adapted from
verify/SOBCv6.v Module TM3
· detected from 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v line 5
57%of our lines identical to the template
30changed lines
282added lines (ours only)
77template lines dropped
20 / 13 / 26items identical / adapted / new
What the package README says it reused and changed (submission/README.md line 21, Template), quoted:
verify/SOBCv6.v, Module TM3 (1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD---, halts): the same table under ours A B C D E F = TM3 B C A E D F, no mirror, started in TM3's state B.
- Kept: the words, the counter, all rules, and the abstract-list checker (
LInc_rec,LIncs_rec,LOv_rec,step_rec,P). - Changed: a new start; 192 abstract cycles instead of 2; lower bounds in the blocks, so an increment can stop inside a
(W1 W0)block; a peel case inLOv_recthat splits the far pair off a block on demand (LOv_peel); a binary count bound saturating at 256; and a far-end halting predicate (Doomed,doom_rec) in place of TM3's short direct run near the head.
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.
identicalchanged / adaptedours only (new)template only
Template part: lines 1–13 (shared header, before the first Module) + 1165–1735 (body of Module TM3; the Module/End lines left out). Ours: lines 24–838 (header comment 1–23 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: init_x, Lmp'_lpow, init1
Side-by-side diff: template (529 lines) vs ours (734 lines), 389 lines differ; runs of identical lines and long template-only runs folded
identicalequal once each TM string is <TM>changedours onlytemplate only
| template | ours | ||
|---|---|---|---|
| 1 | From BusyCoq Require Import Individual62. | 25 | From BusyCoq Require Import Individual62. |
| 2 | Require Import Lia. | 26 | Require Import Lia. |
| 3 | Require Import ZArith. | 27 | Require Import ZArith. |
| 28 | Require Import NArith. | ||
| 4 | Require Import String. | 29 | Require Import String. |
| 5 | Require Import List. | 30 | Require Import List. |
| 6 | From BusyCoq Require Import BinaryCounter_v2. | 31 | From BusyCoq Require Import BinaryCounter_v2. |
| 7 | From BusyCoq Require Import NatMod. | 32 | From BusyCoq Require Import NatMod. |
| 8 | From BusyCoq Require Import SimplTape. | 33 | From BusyCoq Require Import SimplTape. |
| 34 | From BusyCoq Require Import Longitudinal. | ||
| 35 | From BusyCoq Require Import Eqb. | ||
| 10 | Open Scope list. | 37 | Open Scope list. |
| 12 | From BusyCoq Require Import Longitudinal. | ||
| 1166 | Definition tm := Eval compute in (TM_from_str "1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD---"). | 39 | Definition tm := Eval compute in (TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---"). |
| 1168 | Definition tm' := flip tm. | 41 | Definition tm' := flip tm. |
| ⋯ 2 identical lines (template 1170–1171, ours 43–44) | |||
| 1173 | Notation w0 := <[0;0;1]. | 46 | Notation w0 := <[0;0;1]. |
| 1174 | Notation w1 := <[1;1;1]. | 47 | Notation w1 := <[1;1;1]. |
| 1175 | Notation "l <| r" := (l <{{E}} [0;1;0] *> r) (at level 30). | 48 | Notation "l <| r" := (l <{{D}} [0;1;0] *> r) (at level 30). |
| 1176 | Notation "l |> r" := (l {{B}}> r) (at level 30). | 49 | Notation "l |> r" := (l {{A}}> r) (at level 30). |
| 1178 | Inductive LD := W0 | W1. | 51 | Inductive LD := W0 | W1. |
| 1180 | Fixpoint Lmp(ls:list LD):side := | 53 | Fixpoint Lmp(ls:list LD):side := |
| ⋯ 60 identical lines (template 1181–1246, ours 54–119) | |||
| 1247 | LIncs (W1::W1::x) (W1::W1::x') (n*2+0) | 120 | LIncs (W1::W1::x) (W1::W1::x') (n*2+0) |
| 1248 | . | 121 | . |
| 1250 | Notation hR := (B,<[0;0;1]). | 123 | Notation hR := (A,<[0;0;1]). |
| 1251 | Notation hL := (E,[0;1;0]). | 124 | Notation hL := (D,[0;1;0]). |
| 1252 | Notation hLR := [(hL,hR)]. | 125 | Notation hLR := [(hL,hR)]. |
| 1253 | Notation hRL := [(hR,hL)]. | 126 | Notation hRL := [(hR,hL)]. |
| ⋯ 37 identical lines (template 1255–1293, ours 128–166) | |||
| 1294 | solve_sideRLs. | 167 | solve_sideRLs. |
| 1295 | Qed. | 168 | Qed. |
| 1297 | Definition init_x := | ||
| 1298 | (<[W1;W1;W1;W1;W0;W0;W0;W1;W1;W0;W0;W1;W1;W0;W0;W0;W0;W1;W1;W0;W0;W0;W1] <+ <[W0;W1]^^18). | ||
| 1300 | Lemma Incs x x' n0: | 170 | Lemma Incs x x' n0: |
| 1301 | LIncs x x' (n0*2+1) -> | 171 | LIncs x x' (n0*2+1) -> |
| ⋯ 64 identical lines (template 1302–1371, ours 172–241) | |||
| 1372 | - econstructor; eassumption. | 242 | - econstructor; eassumption. |
| 1373 | Qed. | 243 | Qed. |
| 245 | (* New (L4 of the write-up): the far pair of a (W1 W1) block, seen by a deeper | ||
| 246 | result W1 v, is split off and handled by LOv_d1_1; the rest is LOv_lpow. *) | ||
| 247 | Lemma LOv_peel x v v' k: | ||
| 248 | LOv x (W1::v) -> | ||
| 249 | LInc v v' -> | ||
| 250 | LOv ([W1;W1]^^(1+k)++x) (W0::W0::[W1;W0]^^k++W0::v'). | ||
| 251 | Proof. | ||
| 252 | intros H1 H2. | ||
| 253 | replace ([W1;W1]^^(1+k)++x) with ([W1;W1]^^k++(W1::W1::x)). | ||
| 254 | 2: { | ||
| 255 | change (W1::W1::x) with ([W1;W1]++x). | ||
| 256 | rewrite app_assoc, lpow_shift. | ||
| 257 | reflexivity. | ||
| 258 | } | ||
| 259 | apply (LOv_lpow (W1::W1::x) (W0::v') k). | ||
| 260 | eapply LOv_d1_1; eauto. | ||
| 261 | Qed. | ||
| 264 | (* Abstract lists: blocks with a lower bound l on their length. *) | ||
| 1376 | Inductive LD' := | 265 | Inductive LD' := |
| 1377 | | W0' | W1' | W10 | W11. | 266 | | W0' | W1' | W10 (l:nat) | W11 (l:nat). |
| 1379 | Inductive Lmp': list LD' -> list LD -> Prop := | 268 | Inductive Lmp': list LD' -> list LD -> Prop := |
| 1380 | | Lmp'_W0' x x': | 269 | | Lmp'_W0' x x': |
| ⋯ 3 identical lines (template 1381–1383, ours 270–272) | |||
| 1384 | Lmp' x x' -> | 273 | Lmp' x x' -> |
| 1385 | Lmp' (W1'::x) (W1::x') | 274 | Lmp' (W1'::x) (W1::x') |
| 1386 | | Lmp'_W10 x x' n: | 275 | | Lmp'_W10 x x' l n: |
| 1387 | Lmp' x x' -> | 276 | Lmp' x x' -> |
| 1388 | Lmp' (W10::x) ([W1;W0]^^(1+n)++x') | 277 | Lmp' (W10 l::x) ([W1;W0]^^(1+l+n)++x') |
| 1389 | | Lmp'_W11 x x' n: | 278 | | Lmp'_W11 x x' l n: |
| 1390 | Lmp' x x' -> | 279 | Lmp' x x' -> |
| 1391 | Lmp' (W11::x) ([W1;W1]^^(1+n)++x') | 280 | Lmp' (W11 l::x) ([W1;W1]^^(1+l+n)++x') |
| 1392 | | Lmp'_O: | 281 | | Lmp'_O: |
| 1393 | Lmp' [] [] | 282 | Lmp' [] [] |
| 1394 | . | 283 | . |
| 1397 | From BusyCoq Require Import Eqb. | ||
| 1399 | Fixpoint LInc_rec(x:list LD')(T:nat){struct T}:option (list LD') := | 285 | Fixpoint LInc_rec(x:list LD')(T:nat){struct T}:option (list LD') := |
| 1400 | match T with | 286 | match T with |
| ⋯ 7 identical lines (template 1401–1407, ours 287–293) | |||
| 1408 | | W1'::W0'::t => | 294 | | W1'::W0'::t => |
| 1409 | Some (W1'::W1'::t) | 295 | Some (W1'::W1'::t) |
| 296 | | W10 (S l)::t => | ||
| 297 | Some (W1'::W1'::W10 l::t) | ||
| 1410 | | _ => None | 298 | | _ => None |
| 1411 | end | 299 | end |
| 1412 | end. | 300 | end. |
| 1414 | Definition maxv:nat := 4. | ||
| 302 | (* The lower bound on the count is kept in binary (N) and saturates at maxv. *) | ||
| 1416 | Fixpoint LIncs_rec(x:list LD')(T:nat){struct T}:option ((list LD')*nat*nat) := | ||
| 303 | Definition maxv:N := 256%N. | ||
| 305 | Definition upd (n:N) (m:nat) : N := N.min maxv (2*n + N.of_nat m)%N. | ||
| 307 | Lemma upd_le n m: N.to_nat (upd n m) <= N.to_nat n * 2 + m. | ||
| 308 | Proof. unfold upd. lia. Qed. | ||
| 310 | Fixpoint LIncs_rec(x:list LD')(T:nat){struct T}:option ((list LD')*N*nat) := | ||
| 1417 | match T with | 311 | match T with |
| 1418 | | O => None | 312 | | O => None |
| ⋯ 3 identical lines (template 1419–1421, ours 313–315) | |||
| 1422 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W0'::v,n,m)) | 316 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W0'::v,n,m)) |
| 1423 | | W1'::W1'::t => | 317 | | W1'::W1'::t => |
| 1424 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W1'::W1'::v,Nat.min maxv (n*2+m),0)%nat) | 318 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W1'::W1'::v,upd n m,0%nat)) |
| 1425 | | W1'::W0'::t => | 319 | | W1'::W0'::t => |
| 1426 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W1'::W1'::v,Nat.min maxv (n*2+m),1)%nat) | 320 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W1'::W1'::v,upd n m,1%nat)) |
| 1427 | | W11::t => | 321 | | W11 l::t => |
| 1428 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W11::v,Nat.min maxv (n*2+m),0)%nat) | 322 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W11 l::v,upd n m,0%nat)) |
| 1429 | | W10::t => | 323 | | W10 l::t => |
| 1430 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W11::v,Nat.min maxv (n*2+m),1)%nat) | 324 | LIncs_rec t T0 &&& (fun '(v,n,m) => Some (W11 l::v,upd n m,1%nat)) |
| 1431 | | [] => Some ([],0,0)%nat | 325 | | [] => Some ([],0%N,0%nat) |
| 1432 | | _ => None | 326 | | _ => None |
| 1433 | end | 327 | end |
| ⋯ 15 identical lines (template 1434–1449, ours 328–343) | |||
| 1450 | | _ => None | 344 | | _ => None |
| 1451 | end) | 345 | end) |
| 1452 | | W11::t => | 346 | | W11 l::t => |
| 1453 | LOv_rec t T0 &&& (fun v => | 347 | LOv_rec t T0 &&& (fun v => |
| 1454 | match v with | 348 | match v with |
| 1455 | | W0'::W0'::v0 => Some (W0'::W0'::W10::v0) | 349 | | W0'::W0'::v0 => Some (W0'::W0'::W10 l::v0) |
| 350 | | W1'::v0 => | ||
| 351 | match l with | ||
| 352 | | O => None | ||
| 353 | | S l0 => LInc_rec v0 T &&& (fun v1 => Some (W0'::W0'::W10 l0::W0'::v1)) | ||
| 354 | end | ||
| 1456 | | _ => None | 355 | | _ => None |
| 1457 | end) | 356 | end) |
| ⋯ 40 identical lines (template 1458–1501, ours 357–400) | |||
| 1502 | specialize (IHT _ _ _ E H0) as [x0' [I1 I2]]. | 401 | specialize (IHT _ _ _ E H0) as [x0' [I1 I2]]. |
| 1503 | eic; eauto. | 402 | eic; eauto. |
| 403 | - destruct l as [|l]... | ||
| 404 | invs. | ||
| 405 | exists (W1::W1::[W1;W0]^^(1+l+n)++x'0). | ||
| 406 | split. | ||
| 407 | + cbn. apply LInc_d0. | ||
| 408 | + do 2 constructor. | ||
| 409 | apply Lmp'_W10. | ||
| 410 | assumption. | ||
| 1504 | Qed. | 411 | Qed. |
| 1506 | Opaque LInc_rec. | 413 | Opaque LInc_rec. |
| ⋯ 32 identical lines (template 1508–1539, ours 415–446) | |||
| 1540 | + destruct (LOv_rec x T) eqn:E... | 447 | + destruct (LOv_rec x T) eqn:E... |
| 1541 | invs. | 448 | invs. |
| 1542 | specialize (IHT _ _ _ E H2) as [x0' [I1 I2]]. | ||
| 449 | match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ E HL) as [x0' [I1 I2]] end. | ||
| 1543 | destruct l as [|w l]... | 450 | destruct l0 as [|w l0]... |
| 1544 | destruct w... | 451 | destruct w... |
| 1545 | destruct l as [|w l]... | 452 | * destruct l0 as [|w l0]... |
| 1546 | destruct w... | 453 | destruct w... |
| 1547 | invs. | 454 | invs. |
| 1548 | eic. | 455 | eic. |
| 1549 | * eapply LOv_lpow; eauto. | 456 | -- eapply LOv_lpow; eauto. |
| 1550 | * repeat econstructor; eauto. | 457 | -- repeat econstructor; eauto. |
| 458 | * destruct l as [|l]... | ||
| 459 | destruct (LInc_rec l0 (S T)) eqn:E1... | ||
| 460 | invs. | ||
| 461 | match goal with HL: Lmp' l0 _ |- _ => epose proof (LInc_rec_spec _ _ _ _ E1 HL) as [x1' [I3 I4]] end. | ||
| 462 | exists (W0::W0::[W1;W0]^^(1+l+n)++W0::x1'). | ||
| 463 | split. | ||
| 464 | -- apply (LOv_peel _ _ _ (1+l+n) I1 I3). | ||
| 465 | -- do 2 constructor. | ||
| 466 | apply Lmp'_W10. | ||
| 467 | constructor. | ||
| 468 | assumption. | ||
| 1551 | Qed. | 469 | Qed. |
| 1553 | Transparent LInc_rec. | 471 | Transparent LInc_rec. |
| 1555 | Opaque maxv. | ||
| 473 | Opaque upd. | ||
| 1557 | Lemma LIncs_rec_spec x T x0 x' n m: | 475 | Lemma LIncs_rec_spec x T x0 x' n m: |
| 1558 | LIncs_rec x T = Some (x0,n,m) -> | 476 | LIncs_rec x T = Some (x0,n,m) -> |
| ⋯ 2 identical lines (template 1559–1560, ours 477–478) | |||
| 1561 | LIncs x' x0' (n'*2+m) /\ | 479 | LIncs x' x0' (n'*2+m) /\ |
| 1562 | Lmp' x0 x0' /\ | 480 | Lmp' x0 x0' /\ |
| 1563 | n'>=n. | ||
| 481 | n'>=N.to_nat n. | ||
| 1564 | Proof with try congruence. | 482 | Proof with try congruence. |
| 1565 | gen x x0 x' n m. | 483 | gen x x0 x' n m. |
| ⋯ 2 identical lines (template 1566–1567, ours 484–485) | |||
| 1568 | destruct x as [|w x]... | 486 | destruct x as [|w x]... |
| 1569 | - invs. | 487 | - invs. |
| 1570 | eic; eauto; eauto. | ||
| 488 | exists (@nil LD), 0%nat. | ||
| 489 | split; [constructor|split; [constructor|cbn; lia]]. | ||
| 1571 | - destruct w... | 490 | - destruct w... |
| 1572 | + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... | 491 | + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... |
| 1573 | invs. | 492 | invs. |
| 1574 | specialize (IHT _ _ _ _ _ E H1) as [x0' [n' [I1 [I2 I3]]]]. | ||
| 493 | match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end. | ||
| 1575 | eic; eauto. | 494 | eic; eauto. |
| 1576 | + destruct x as [|w x]... | 495 | + destruct x as [|w x]... |
| 1577 | destruct w... | 496 | destruct w... |
| 1578 | * destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... | 497 | * destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... |
| 1579 | invs. | 498 | invs. |
| 1580 | specialize (IHT _ _ _ _ _ E H0) as [x0' [n' [I1 [I2 I3]]]]. | ||
| 499 | match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end. | ||
| 500 | pose proof (upd_le n1 m1). | ||
| 1581 | eic; eauto; lia. | 501 | eic; eauto; lia. |
| 1582 | * destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... | 502 | * destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... |
| 1583 | invs. | 503 | invs. |
| 1584 | specialize (IHT _ _ _ _ _ E H0) as [x0' [n' [I1 [I2 I3]]]]. | ||
| 504 | match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end. | ||
| 505 | pose proof (upd_le n1 m1). | ||
| 1585 | eic; eauto; lia. | 506 | eic; eauto; lia. |
| 1586 | + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... | 507 | + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... |
| 1587 | invs. | 508 | invs. |
| 1588 | specialize (IHT _ _ _ _ _ E H1) as [x0' [n' [I1 [I2 I3]]]]. | ||
| 509 | match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end. | ||
| 510 | match goal with |- context [ _^^(1+l+?k) ] => | ||
| 511 | replace (1+l+k) with (1+(l+k)) by lia; set (j:=l+k) end. | ||
| 512 | pose proof (upd_le n1 m1). | ||
| 1589 | eic. | 513 | eic. |
| 1590 | * rewrite lpow_add; cbn. | 514 | * rewrite lpow_add; cbn. |
| 1591 | econstructor. | 515 | econstructor. |
| 1592 | eapply LIncs_lpow; eauto. | 516 | eapply LIncs_lpow; eauto. |
| 1593 | * econstructor; eauto. | 517 | * econstructor; eauto. |
| 1594 | * pose proof (Nat.pow_nonzero 2 n). | 518 | * pose proof (Nat.pow_nonzero 2 j). |
| 1595 | rewrite Nat.mul_add_distr_r. | 519 | rewrite Nat.mul_add_distr_r. |
| 1596 | pose proof (Nat.mul_le_mono_l 1 (2^n) (n'*2+m1)). | 520 | pose proof (Nat.mul_le_mono_l 1 (2^j) (n'*2+m1)). |
| 1597 | lia. | 521 | lia. |
| 1598 | + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... | 522 | + destruct (LIncs_rec x T) as [[[v1 n1] m1]|] eqn:E... |
| 1599 | invs. | 523 | invs. |
| 1600 | specialize (IHT _ _ _ _ _ E H1) as [x0' [n' [I1 [I2 I3]]]]. | ||
| 524 | match goal with HL: Lmp' x _ |- _ => specialize (IHT _ _ _ _ _ E HL) as [x0' [n' [I1 [I2 I3]]]] end. | ||
| 525 | match goal with |- context [ _^^(1+l+?k) ] => | ||
| 526 | replace (1+l+k) with (1+(l+k)) by lia; set (j:=l+k) end. | ||
| 527 | pose proof (upd_le n1 m1). | ||
| 1601 | eic. | 528 | eic. |
| 1602 | * rewrite lpow_add; cbn. | 529 | * rewrite lpow_add; cbn. |
| 1603 | econstructor. | 530 | econstructor. |
| 1604 | eapply LIncs_lpow'; eauto. | 531 | eapply LIncs_lpow'; eauto. |
| 1605 | * econstructor; eauto. | 532 | * econstructor; eauto. |
| 1606 | * pose proof (Nat.pow_nonzero 2 n). | 533 | * pose proof (Nat.pow_nonzero 2 j). |
| 1607 | pose proof (Nat.mul_le_mono_l 1 (2^n) (n'*2+m1)). | 534 | pose proof (Nat.mul_le_mono_l 1 (2^j) (n'*2+m1)). |
| 1608 | lia. | 535 | lia. |
| 1609 | Qed. | 536 | Qed. |
| 1611 | Transparent maxv. | 538 | Transparent upd. |
| 540 | (* One counter cycle on abstract lists. The new block of (W1 W0) pairs made by the | ||
| 541 | overflow is one abstract token W10 (n-1). *) | ||
| 1613 | Definition step_rec(x:list LD'):option (list LD') := | 542 | Definition step_rec(x:list LD'):option (list LD') := |
| 1614 | LIncs_rec x (S(length x)) &&& (fun '(x0,n,m) => | 543 | LIncs_rec x (S(length x)) &&& (fun '(x0,n,m) => |
| 1615 | if m =? 1 then | 544 | if m =? 1 then |
| 1616 | match n with | ||
| 545 | match N.to_nat n with | ||
| 1617 | | O => None | 546 | | O => None |
| 1618 | | S n0 => | 547 | | S n0 => |
| 1619 | LOv_rec x0 (S(length x0)) &&& (fun x1 => | 548 | LOv_rec x0 (S(length x0)) &&& (fun x1 => |
| 1620 | match x1 with | 549 | match x1 with |
| 1621 | | W0'::x2 => | 550 | | W0'::x2 => |
| 1622 | Some ([W1';W0']^^(n0-n0/2)++W10::[W1';W0']^^(n0/2)++W1'::W1'::x2) | ||
| 551 | Some (W10 n0::W1'::W1'::x2) | ||
| 1623 | | _ => None | 552 | | _ => None |
| 1624 | end) | 553 | end) |
| 1625 | end | 554 | end |
| 1626 | else None). | 555 | else None). |
| 1628 | Lemma Lmp'_lpow x x' n: | ||
| 1629 | Lmp' x x' -> | ||
| ⋯ 3 template-only lines (template 1630–1632), not in ours | |||
| 1633 | induction n; cbn; eauto. | ||
| 1634 | Qed. | ||
| 1636 | Inductive P: (list LD')->Prop := | 557 | Inductive P: (list LD')->Prop := |
| 1637 | | P_intro x x': | 558 | | P_intro x x': |
| ⋯ 14 identical lines (template 1638–1652, ours 559–573) | |||
| 1653 | destruct (Nat.eqb_spec m 1)... | 574 | destruct (Nat.eqb_spec m 1)... |
| 1654 | subst. | 575 | subst. |
| 1655 | destruct n as [|n]... | ||
| 576 | destruct (N.to_nat n) as [|n0] eqn:En... | ||
| 1656 | destruct (LOv_rec v (S(length v))) eqn:E0... | 577 | destruct (LOv_rec v (S(length v))) eqn:E0... |
| 1657 | destruct l as [|w l]... | 578 | destruct l as [|w l]... |
| 1658 | destruct w... | 579 | destruct w... |
| 1659 | remember (n/2) as n1. | ||
| 1660 | invs. | 580 | invs. |
| 1661 | epose proof (LIncs_rec_spec _ _ _ _ _ _ E H0) as [x0' [n' [I1 [I2 I3]]]]. | 581 | epose proof (LIncs_rec_spec _ _ _ _ _ _ E H0) as [x0' [n' [I1 [I2 I3]]]]. |
| 1662 | epose proof (LOv_rec_spec _ _ _ _ E0 I2) as [x1' [I4 I5]]. | 582 | epose proof (LOv_rec_spec _ _ _ _ E0 I2) as [x1' [I4 I5]]. |
| 1663 | invs. | 583 | invs. |
| 1664 | epose proof (Nat.Div0.div_mod n 2). | ||
| 1665 | eapply P_intro with (x':=[W1;W0]^^(n')++[W1;W1]++x'). | 584 | eapply P_intro with (x':=[W1;W0]^^(n')++[W1;W1]++x'). |
| 1666 | - replace (n') with (n-n1+(1+(n'-S n))+n1) by lia. | 585 | - replace n' with (1+n0+(n'-S n0)) by lia. |
| 1667 | do 2 rewrite lpow_add. | ||
| 586 | apply Lmp'_W10. | ||
| 1668 | do 2 rewrite <-app_assoc. | ||
| 1669 | eapply Lmp'_lpow. | ||
| 1670 | econstructor. | ||
| 1671 | eapply Lmp'_lpow. | ||
| 1672 | cbn. | 587 | cbn. |
| 1673 | eauto. | 588 | eauto. |
| ⋯ 3 identical lines (template 1674–1676, ours 589–591) | |||
| 1677 | finish. | 592 | finish. |
| 1678 | Qed. | 593 | Qed. |
| 1680 | Lemma init: | ||
| 595 | Fixpoint iter (k:nat) (x:list LD') : option (list LD') := | ||
| 1681 | P (map (fun x => match x with W0 => W0' | W1 => W1' end) (init_x)). | ||
| 596 | match k with | ||
| 597 | | O => Some x | ||
| 598 | | S k0 => step_rec x &&& (fun y => iter k0 y) | ||
| 599 | end. | ||
| 601 | Lemma iter_spec k: | ||
| 602 | forall x y, | ||
| 603 | iter k x = Some y -> | ||
| 604 | P x -> | ||
| 605 | P y. | ||
| 1682 | Proof. | 606 | Proof. |
| 1683 | econstructor. | ||
| 607 | induction k; cbn; intros x y H HP. | ||
| 1684 | 1: cbn; repeat econstructor. | ||
| 608 | - inverts H. exact HP. | ||
| 1685 | cbn; solve_init. | ||
| 609 | - unfold if_Some in H. | ||
| 610 | destruct (step_rec x) as [x1|] eqn:E; [|discriminate]. | ||
| 611 | eapply IHk. | ||
| 612 | 1: exact H. | ||
| 613 | eapply step_rec_spec; eauto. | ||
| 1686 | Qed. | 614 | Qed. |
| 1688 | Lemma init1: | ||
| 617 | (* The start: P x2 after 38,573 steps from the blank tape (two exact cycles from the | ||
| 1689 | P [W1'; W0'; W1'; W0'; W10; W1'; W0'; W1'; W1'; W0'; W1'; W0'; W1'; W0'; W10; | ||
| 618 | counter 1000111011 reached after 847 steps). *) | ||
| 1690 | W1'; W0'; W0'; W0'; W0'; W1'; W1'; W1'; W0'; W1'; W0'; W1'; W0'; W1'; W0'; | ||
| 619 | Definition x2 : list LD := | ||
| 1691 | W1'; W0'; W1'; W0'; W1'; W0'; W1'; W0'; W1'; W0'; W1'; W0'; W1'; W0'; W1'; | 620 | [W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; |
| 1692 | W0'; W1'; W0'; W1'; W0'; W1'; W0'; W1'; W0'; W0'; W0'; W0'; W0'; W1'; W0'; | 621 | W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; |
| 1693 | W0'; W1'; W1'; W0'; W1'; W1'; W0'; W0'; W1'; W1'; W0'; W0'; W1'; W1'; W0'; | ||
| 622 | W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W1; W0; W1; W0; W1; W0; W0; W1; W1; | ||
| 1694 | W1'; W0'; W1'; W1']. | ||
| 623 | W0; W0; W0; W0; W1; W1; W1; W0; W1; W1]. | ||
| 625 | Definition x2' : list LD' := | ||
| 626 | map (fun x => match x with W0 => W0' | W1 => W1' end) x2. | ||
| 628 | Lemma init: P x2'. | ||
| 1695 | Proof. | 629 | Proof. |
| 1696 | eapply step_rec_spec. | ||
| 630 | apply P_intro with (x':=x2). | ||
| 1697 | 2: eapply step_rec_spec. | ||
| 631 | - unfold x2', x2. cbn. repeat constructor. | ||
| 1698 | 3: apply init. | ||
| 632 | - unfold x2. cbn. solve_init. | ||
| 1699 | 2: vm_compute; reflexivity. | ||
| 1700 | 1: vm_compute; reflexivity. | ||
| 1701 | Qed. | 633 | Qed. |
| 1703 | Ltac solve_L := | ||
| 636 | (* The halt. A list x is doomed if the overflow run started on it halts. *) | ||
| 1704 | solve [(econstructor || | ||
| 637 | Definition Doomed (x:list LD) := forall r, halts tm (Lmp x <| [1] *> r). | ||
| 1705 | eapply LIncs_lpow || | ||
| 639 | Lemma walk0 x r: | ||
| 1706 | eapply LOv_lpow); solve_L]. | ||
| 640 | Lmp x <* w0 <| [1] *> r -->* | ||
| 641 | Lmp x <| [1] *> [0;1;1] *> r. | ||
| 642 | Proof. es. Qed. | ||
| 644 | Lemma walk1 x r: | ||
| 645 | Lmp x <* w1 <* w1 <| [1] *> r -->* | ||
| 646 | Lmp x <| [1] *> [0;1;0;1;0;1] *> r. | ||
| 647 | Proof. es. Qed. | ||
| 649 | Lemma doomed_w0 x: Doomed x -> Doomed (W0::x). | ||
| 650 | Proof. | ||
| 651 | intros H r. cbn [Lmp]. | ||
| 652 | eapply halts_evstep. | ||
| 653 | 2: apply walk0. | ||
| 654 | apply H. | ||
| 655 | Qed. | ||
| 657 | Lemma doomed_w1 x: Doomed x -> Doomed (W1::W1::x). | ||
| 658 | Proof. | ||
| 659 | intros H r. cbn [Lmp]. | ||
| 660 | eapply halts_evstep. | ||
| 661 | 2: apply walk1. | ||
| 662 | apply H. | ||
| 663 | Qed. | ||
| 665 | Lemma doomed_pow k x: Doomed x -> Doomed ([W1;W1]^^k++x). | ||
| 666 | Proof. | ||
| 667 | intros H. | ||
| 668 | induction k; cbn; auto. | ||
| 669 | apply doomed_w1. exact IHk. | ||
| 670 | Qed. | ||
| 672 | Definition x_far : list LD := | ||
| 673 | [W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W1;W1;W1;W1]. | ||
| 675 | Lemma far_halt: Doomed x_far. | ||
| 676 | Proof. | ||
| 677 | intros r. | ||
| 678 | unfold x_far. cbn [Lmp]. | ||
| 679 | solve_halt. | ||
| 680 | Qed. | ||
| 682 | Definition x_far' : list LD' := | ||
| 683 | [W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W1';W1';W1';W1']. | ||
| 685 | Definition tok_eqb (a b: LD') : bool := | ||
| 686 | match a, b with | ||
| 687 | | W0', W0' => true | ||
| 688 | | W1', W1' => true | ||
| 689 | | _, _ => false | ||
| 690 | end. | ||
| 692 | Fixpoint ltok_eqb (a b: list LD') : bool := | ||
| 693 | match a, b with | ||
| 694 | | [], [] => true | ||
| 695 | | x::a0, y::b0 => tok_eqb x y && ltok_eqb a0 b0 | ||
| 696 | | _, _ => false | ||
| 697 | end. | ||
| 699 | Lemma ltok_eqb_spec a b: ltok_eqb a b = true -> a = b. | ||
| 700 | Proof. | ||
| 701 | gen b. | ||
| 702 | induction a as [|x a IH]; intros b H; destruct b as [|y b]; cbn in H; try congruence. | ||
| 703 | apply and_true_iff in H as [H1 H2]. | ||
| 704 | destruct x, y; cbn in H1; try congruence; f_equal; auto. | ||
| 705 | Qed. | ||
| 707 | Fixpoint doom_rec (X: list LD') : bool := | ||
| 708 | if ltok_eqb X x_far' then true else | ||
| 709 | match X with | ||
| 710 | | W0' :: t => doom_rec t | ||
| 711 | | W1' :: W1' :: t => doom_rec t | ||
| 712 | | W11 _ :: t => doom_rec t | ||
| 713 | | _ => false | ||
| 714 | end. | ||
| 716 | Lemma doom_rec_eq X: | ||
| 717 | doom_rec X = | ||
| 718 | if ltok_eqb X x_far' then true else | ||
| 719 | match X with | ||
| 720 | | W0' :: t => doom_rec t | ||
| 721 | | W1' :: W1' :: t => doom_rec t | ||
| 722 | | W11 _ :: t => doom_rec t | ||
| 723 | | _ => false | ||
| 724 | end. | ||
| 725 | Proof. destruct X; reflexivity. Qed. | ||
| 727 | Lemma doom_rec_spec n: | ||
| 728 | forall X x, | ||
| 729 | length X <= n -> | ||
| 730 | doom_rec X = true -> | ||
| 731 | Lmp' X x -> | ||
| 732 | Doomed x. | ||
| 733 | Proof. | ||
| 734 | induction n; intros X x Hl H HL. | ||
| 735 | - destruct X; cbn in Hl; [|lia]. | ||
| 736 | cbn in H. congruence. | ||
| 737 | - rewrite doom_rec_eq in H. | ||
| 738 | destruct (ltok_eqb X x_far') eqn:E. | ||
| 739 | + apply ltok_eqb_spec in E. subst X. | ||
| 740 | unfold x_far' in HL. | ||
| 741 | invs. | ||
| 742 | apply far_halt. | ||
| 743 | + destruct X as [|a X]; [discriminate|]. | ||
| 744 | cbn in Hl. | ||
| 745 | destruct a. | ||
| 746 | * invs. apply doomed_w0. eapply IHn; eauto; lia. | ||
| 747 | * destruct X as [|a X]; [discriminate|]. | ||
| 748 | destruct a; try discriminate. | ||
| 749 | invs. apply doomed_w1. cbn in Hl. eapply IHn; eauto; lia. | ||
| 750 | * discriminate. | ||
| 751 | * invs. apply doomed_pow. eapply IHn; eauto; lia. | ||
| 752 | Qed. | ||
| 754 | Definition final_check (k:nat) : bool := | ||
| 755 | match iter k x2' with | ||
| 756 | | Some y => | ||
| 757 | match LIncs_rec y (S(length y)) with | ||
| 758 | | Some (z,n,m) => if m =? 1 then doom_rec z else false | ||
| 759 | | None => false | ||
| 760 | end | ||
| 761 | | None => false | ||
| 762 | end. | ||
| 764 | Lemma final_check_ok: final_check 192 = true. | ||
| 765 | Proof. vm_compute. reflexivity. Qed. | ||
| 767 | Lemma final_check_spec k: | ||
| 768 | final_check k = true -> | ||
| 769 | exists y z n, | ||
| 770 | iter k x2' = Some y /\ | ||
| 771 | LIncs_rec y (S(length y)) = Some (z,n,1%nat) /\ | ||
| 772 | doom_rec z = true. | ||
| 773 | Proof. | ||
| 774 | unfold final_check. | ||
| 775 | destruct (iter k x2') as [y|] eqn:E1; [|discriminate]. | ||
| 776 | destruct (LIncs_rec y (S(length y))) as [[[z n] m]|] eqn:E2; [|discriminate]. | ||
| 777 | destruct (Nat.eqb_spec m 1); [|discriminate]. | ||
| 778 | subst m. intros H. exists y, z, n. | ||
| 779 | split; [reflexivity|split; [exact E2|exact H]]. | ||
| 780 | Qed. | ||
| 782 | Lemma halt_from k: final_check k = true -> halts tm c0. | ||
| 783 | Proof. | ||
| 784 | intros Hk. | ||
| 785 | destruct (final_check_spec k Hk) as (y & z & n & E1 & E2 & H). | ||
| 786 | pose proof (iter_spec _ _ _ E1 init) as HP. | ||
| 787 | inverts HP as HL Hc. | ||
| 788 | destruct (LIncs_rec_spec _ _ _ _ _ _ E2 HL) as [z' [n' [I1 [I2 I3]]]]. | ||
| 789 | pose proof (doom_rec_spec _ _ _ (le_n _) H I2) as HD. | ||
| 790 | eapply halts_evstep with (c' := Lmp z' <| RC ((n'+1)*2)). | ||
| 791 | - unfold RC. apply HD. | ||
| 792 | - eapply evstep_trans. | ||
| 793 | 1: exact Hc. | ||
| 794 | apply Incs. exact I1. | ||
| 795 | Qed. | ||
| 1708 | Lemma halt: halts tm c0. | 797 | Lemma halt: halts tm c0. |
| 1709 | Proof. | ||
| 798 | Proof. exact (halt_from 192 final_check_ok). Qed. | ||
| 1710 | epose proof init1 as H. | ||
| 800 | (* | ||
| 1711 | inverts H. | ||
| 801 | ``` | ||
| 1712 | invs. | ||
| 802 | 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE--- | ||
| 1713 | eapply halts_evstep. | ||
| 803 | = SOBCv6 TM3 1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD--- with ours A B C D E F = TM3 B C A E D F | ||
| 1714 | 2:{ | ||
| 805 | words (paper order) W0 = 001 W1 = 111 | ||
| 1715 | follow H1. | ||
| 806 | lists head first: x = x_0 x_1 ... x_(k-1), x_0 next to the head | ||
| 1716 | follow Incs. | ||
| 807 | Lmp(x) 0^inf w(x_(k-1)) ... w(x_1) w(x_0) | ||
| 1717 | 1: solve_L. | ||
| 808 | RC(n) 1 (011)^n 01 0^inf | ||
| 1718 | finish. | ||
| 809 | P(x) Lmp(x) <D 010 RC(1) | ||
| 1719 | } | ||
| 810 | digits W1 W0 = 0, W1 W1 = 1, a lone W0 = separator; lowest digit next to the head | ||
| 1720 | clear H1. | ||
| 811 | count(x) sum over the digit pairs p (p = 0 next to the head) of (1 - b_p) 2^p | ||
| 1721 | match goal with | ||
| 812 | ones(x) x with every digit pair set to W1 W1 | ||
| 1722 | | |- halts tm (_ <| RC ((?a+1)*2)) => | ||
| 814 | LInc Lmp(x) <D 010 r --> Lmp(LInc x) 001 A> r | ||
| 1723 | remember a as m | ||
| 815 | LOv Lmp(x) <D 010 1 r --> Lmp(LOv x) A> r x in {W0, W1 W1}^n | ||
| 1724 | end. | ||
| 816 | Incs Lmp(x) <D 010 RC(1) --> Lmp(ones x) <D 010 RC(c+1) c = count(x) odd | ||
| 1725 | clear Heqm. | ||
| 817 | Ov Lmp(x) <D 010 RC(2m+2) --> Lmp((W1 W0)^m W1 W1 x') <D 010 RC(1) LOv(x) = W0 x' | ||
| 1726 | eapply halts_evstep. | ||
| 818 | walk0 Lmp(x) 001 <D 010 1 r --> Lmp(x) <D 010 1 011 r (19 steps) | ||
| 1727 | 2:{ | ||
| 819 | walk1 Lmp(x) 111 111 <D 010 1 r --> Lmp(x) <D 010 1 010101 r (12 steps) | ||
| 1728 | repeat (cbn || rewrite Lmp_d1). | ||
| 820 | far Lmp(x_far) <D 010 1 r --> F reads 1 (halt) x_far = (W1 W1 W0)^5 (W1 W1)^3 | ||
| 1729 | time repeat (step1 || sr). | ||
| 822 | LInc(W0 t) = W0 LInc(t) LInc(W1 W0 t) = W1 W1 t LInc(W1 W1 t) = W1 W0 LInc(t) | ||
| 1730 | finish. | ||
| 823 | LOv([]) = W0 W1 LOv(W0 t) = W1 LOv(t) | ||
| 1731 | } | ||
| 824 | LOv(W1 W1 t) = W0 W0 W1 v' if LOv(t) = W0 v' | ||
| 1732 | eapply halted_halts. | ||
| 825 | LOv(W1 W1 t) = W0 W0 W0 LInc(v') if LOv(t) = W1 v' | ||
| 1733 | constructor. | ||
| 827 | blocks W10 l = (W1 W0)^(1+l+n), W11 l = (W1 W1)^(1+l+n), n >= 0 free for each block | ||
| 1734 | Qed. | ||
| 828 | LInc_rec W10 (l+1) t -> W1 W1 W10 l t | ||
| 829 | LOv_rec W11 l t -> W0 W0 W10 l v' if LOv_rec(t) = W0 W0 v' (keep) | ||
| 830 | W11 (l+1) t -> W0 W0 W10 l W0 LInc(v') if LOv_rec(t) = W1 v' (peel) | ||
| 831 | step_rec x -> W10 (n-1) W1 W1 x2 where LIncs_rec x = (x0, n, 1), n >= 1, LOv_rec x0 = W0 x2 | ||
| 833 | init c0 -->(38,573) P(x2), x2 = (W1 W0)^25 W1 W1 W0 W1 W0 W1 W0 W0 W1 W1 W0 W0 W0 W0 W1 W1 W1 W0 W1 W1 | ||
| 834 | chain x2 --(192 step_rec, bound 256)--> x194 (38,120 tokens) | ||
| 835 | halt P(x194) --Incs--> Lmp(z) <D 010 RC(2N+2), z = prefix ++ x_far, prefix in {W0, W1 W1, W11 l}^n; | ||
| 836 | walk0 / walk1 through the prefix, then far: F reads 1 | ||
| 837 | ``` | ||
| 838 | *) | ||
3Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.
59 items in 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v (838 lines): 32 Lemma, 13 Definition, 7 Inductive, 7 Fixpoint. Tags against the template: identical = same name and same text once each file's own TM string is <TM> (marked "except the TM string" when that is the only difference); adapted = same name, different text; new = no item of that name in the template part.
| # | kind | name | statement (no proof body) | line | vs template |
|---|---|---|---|---|---|
| 1 | Definition | tm | Definition tm := Eval compute in (TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---"). | L39 | identicalexcept the TM string |
| 2 | Definition | tm' | Definition tm' := flip tm. | L41 | identical |
| 3 | Inductive | LD | Inductive LD := W0 | W1. | L51 | identical |
| 4 | Fixpoint | Lmp | Fixpoint Lmp(ls:list LD):side := match ls with | [] => 0inf | W0::t => Lmp t <* w0 | W1::t => Lmp t <* w1 end. | L53 | identical |
| 5 | Inductive | LInc | Inductive LInc: (list LD)->(list LD)->Prop := | LInc_w0 x x': LInc x x' -> LInc (W0::x) (W0::x') | LInc_d0 x: LInc (W1::W0::x) (W1::W1::x) … +4 lines | L60 | identical |
| 6 | Lemma | LInc_spec | Lemma LInc_spec [x x']: LInc x x' -> forall r, Lmp x <| r -->* Lmp x' <* w0 |> r. | L71 | identical |
| 7 | Inductive | LOv | Inductive LOv: (list LD)->(list LD)->Prop := | LOv_O: LOv [] [W0;W1] | LOv_d1_0 x x': LOv x (W0::x') -> LOv (W1::W1::x) (W0::W0::W1::x') | LOv_d1_1 x x' x'': … +7 lines | L82 | identical |
| 8 | Lemma | LOv_spec | Lemma LOv_spec [x x']: LOv x x' -> forall r, Lmp x <| [1] *> r -->* Lmp x' |> r. | L96 | identical |
| 9 | Inductive | LIncs | Inductive LIncs: (list LD)->(list LD)->nat->Prop := | LIncs_O: LIncs [] [] O | LIncs_w0 x x' n: LIncs x x' n -> LIncs (W0::x) (W0::x') n … +7 lines | L109 | identical |
| 10 | Lemma | LIncs_spec | Lemma LIncs_spec [x x' n]: LIncs x x' n -> sideRLs tm' (hLR^^n) (Lmp x) (Lmp x'). | L128 | identical |
| 11 | Definition | RC | Definition RC n := [1] *> [0;1;1]^^n *> [0;1] *> 0inf. | L154 | identical |
| 12 | Lemma | RIncs | Lemma RIncs n m: sideRLs tm (hRL^^n) (RC m) (RC (n+m)). | L156 | identical |
| 13 | Lemma | Incs | Lemma Incs x x' n0: LIncs x x' (n0*2+1) -> Lmp x <| RC 1 -->* Lmp x' <| RC ((n0+1)*2). | L170 | identical |
| 14 | Lemma | Lmp_d0 | Lemma Lmp_d0 x n: Lmp (x <+ <[W0;W1]^^n) = Lmp x <* (w0<+w1)^^n. | L182 | identical |
| 15 | Lemma | Lmp_d1 | Lemma Lmp_d1 x n: Lmp (x <+ <[W1;W1]^^n) = Lmp x <* (w1<+w1)^^n. | L190 | identical |
| 16 | Lemma | Ov | Lemma Ov x x' m: LOv x (W0::x') -> Lmp x <| RC ((m+1)*2) -->* Lmp (x' <+ <[W1;W1] <+ <[W0;W1]^^m) <| RC 1. | L198 | identical |
| 17 | Lemma | LIncs_lpow | Lemma LIncs_lpow [x x' n0] n: LIncs x x' n0 -> LIncs (x <+ <[W0;W1]^^n) (x' <+ <[W1;W1]^^n) ((n0+1)*2^n-1). | L209 | identical |
| 18 | Lemma | LIncs_lpow' | Lemma LIncs_lpow' [x x' n0] n: LIncs x x' n0 -> LIncs (x <+ <[W1;W1]^^n) (x' <+ <[W1;W1]^^n) ((n0)*2^n). | L222 | identical |
| 19 | Lemma | LOv_lpow | Lemma LOv_lpow x x' n: LOv x (W0::W0::x') -> LOv (x <+ <[W1;W1]^^n) (x' <+ <[W0;W1]^^n <+ <[W0;W0]). | L235 | identical |
| 20 | Lemma | LOv_peel | Lemma LOv_peel x v v' k: LOv x (W1::v) -> LInc v v' -> LOv ([W1;W1]^^(1+k)++x) (W0::W0::[W1;W0]^^k++W0::v'). | L247 | new |
| 21 | Inductive | LD' | Inductive LD' := | W0' | W1' | W10 (l:nat) | W11 (l:nat). | L265 | adapted |
| 22 | Inductive | Lmp' | Inductive Lmp': list LD' -> list LD -> Prop := | Lmp'_W0' x x': Lmp' x x' -> Lmp' (W0'::x) (W0::x') | Lmp'_W1' x x': Lmp' x x' -> … +10 lines | L268 | adapted |
| 23 | Fixpoint | LInc_rec | Fixpoint LInc_rec(x:list LD')(T:nat){struct T}:option (list LD') :=
match T with
| O => None
| S T0 =>
match x with
| W0'::t =>
… +10 lines | L285 | adapted |
| 24 | Definition | maxv | Definition maxv:N := 256%N. | L303 | adapted |
| 25 | Definition | upd | Definition upd (n:N) (m:nat) : N := N.min maxv (2*n + N.of_nat m)%N. | L305 | new |
| 26 | Lemma | upd_le | Lemma upd_le n m: N.to_nat (upd n m) <= N.to_nat n * 2 + m. | L307 | new |
| 27 | Fixpoint | LIncs_rec | Fixpoint LIncs_rec(x:list LD')(T:nat){struct T}:option ((list LD')*N*nat) :=
match T with
| O => None
| S T0 =>
match x with
| W0'::t =>
… +13 lines | L310 | adapted |
| 28 | Fixpoint | LOv_rec | Fixpoint LOv_rec(x:list LD')(T:nat){struct T}:option (list LD') :=
match T with
| O => None
| S T0 =>
match x with
| [] => Some [W0';W1']
… +24 lines | L330 | adapted |
| 29 | Lemma | LInc_rec_spec | Lemma LInc_rec_spec x T x0 x': LInc_rec x T = Some x0 -> Lmp' x x' -> exists x0', LInc x' x0' /\ Lmp' x0 x0'. | L379 | adapted |
| 30 | Lemma | LOv_rec_spec | Lemma LOv_rec_spec x T x0 x': LOv_rec x T = Some x0 -> Lmp' x x' -> exists x0', LOv x' x0' /\ Lmp' x0 x0'. | L415 | adapted |
| 31 | Lemma | LIncs_rec_spec | Lemma LIncs_rec_spec x T x0 x' n m: LIncs_rec x T = Some (x0,n,m) -> Lmp' x x' -> exists x0' n', LIncs x' x0' (n'*2+m) /\ Lmp' x0 x0' /\ … +1 lines | L475 | adapted |
| 32 | Definition | step_rec | Definition step_rec(x:list LD'):option (list LD') := LIncs_rec x (S(length x)) &&& (fun '(x0,n,m) => if m =? 1 then match N.to_nat n with | O => None | S n0 => … +8 lines | L542 | adapted |
| 33 | Inductive | P | Inductive P: (list LD')->Prop := | P_intro x x': Lmp' x x' -> c0 -->* Lmp x' <| RC 1 -> P x. | L557 | identical |
| 34 | Lemma | step_rec_spec | Lemma step_rec_spec x x': step_rec x = Some x' -> P x -> P x'. | L563 | adapted |
| 35 | Fixpoint | iter | Fixpoint iter (k:nat) (x:list LD') : option (list LD') := match k with | O => Some x | S k0 => step_rec x &&& (fun y => iter k0 y) end. | L595 | new |
| 36 | Lemma | iter_spec | Lemma iter_spec k: forall x y, iter k x = Some y -> P x -> P y. | L601 | new |
| 37 | Definition | x2 | Definition x2 : list LD := [W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W0; W1; W1; W0; W1; W0; W1; W0; W0; W1; W1; W0; W0; W0; W0; W1; W1; W1; W0; W1; W1]. | L619 | new |
| 38 | Definition | x2' | Definition x2' : list LD' := map (fun x => match x with W0 => W0' | W1 => W1' end) x2. | L625 | new |
| 39 | Lemma | init | Lemma init: P x2'. | L628 | adapted |
| 40 | Definition | Doomed | Definition Doomed (x:list LD) := forall r, halts tm (Lmp x <| [1] *> r). | L637 | new |
| 41 | Lemma | walk0 | Lemma walk0 x r: Lmp x <* w0 <| [1] *> r -->* Lmp x <| [1] *> [0;1;1] *> r. | L639 | new |
| 42 | Lemma | walk1 | Lemma walk1 x r: Lmp x <* w1 <* w1 <| [1] *> r -->* Lmp x <| [1] *> [0;1;0;1;0;1] *> r. | L644 | new |
| 43 | Lemma | doomed_w0 | Lemma doomed_w0 x: Doomed x -> Doomed (W0::x). | L649 | new |
| 44 | Lemma | doomed_w1 | Lemma doomed_w1 x: Doomed x -> Doomed (W1::W1::x). | L657 | new |
| 45 | Lemma | doomed_pow | Lemma doomed_pow k x: Doomed x -> Doomed ([W1;W1]^^k++x). | L665 | new |
| 46 | Definition | x_far | Definition x_far : list LD := [W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W0;W1;W1;W1;W1;W1;W1]. | L672 | new |
| 47 | Lemma | far_halt | Lemma far_halt: Doomed x_far. | L675 | new |
| 48 | Definition | x_far' | Definition x_far' : list LD' := [W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W0';W1';W1';W1';W1';W1';W1']. | L682 | new |
| 49 | Definition | tok_eqb | Definition tok_eqb (a b: LD') : bool := match a, b with | W0', W0' => true | W1', W1' => true | _, _ => false end. | L685 | new |
| 50 | Fixpoint | ltok_eqb | Fixpoint ltok_eqb (a b: list LD') : bool := match a, b with | [], [] => true | x::a0, y::b0 => tok_eqb x y && ltok_eqb a0 b0 | _, _ => false end. | L692 | new |
| 51 | Lemma | ltok_eqb_spec | Lemma ltok_eqb_spec a b: ltok_eqb a b = true -> a = b. | L699 | new |
| 52 | Fixpoint | doom_rec | Fixpoint doom_rec (X: list LD') : bool := if ltok_eqb X x_far' then true else match X with | W0' :: t => doom_rec t | W1' :: W1' :: t => doom_rec t | W11 _ :: t => doom_rec t … +2 lines | L707 | new |
| 53 | Lemma | doom_rec_eq | Lemma doom_rec_eq X: doom_rec X = if ltok_eqb X x_far' then true else match X with | W0' :: t => doom_rec t | W1' :: W1' :: t => doom_rec t … +3 lines | L716 | new |
| 54 | Lemma | doom_rec_spec | Lemma doom_rec_spec n: forall X x, length X <= n -> doom_rec X = true -> Lmp' X x -> Doomed x. | L727 | new |
| 55 | Definition | final_check | Definition final_check (k:nat) : bool := match iter k x2' with | Some y => match LIncs_rec y (S(length y)) with | Some (z,n,m) => if m =? 1 then doom_rec z else false | None => false … +3 lines | L754 | new |
| 56 | Lemma | final_check_ok | Lemma final_check_ok: final_check 192 = true. | L764 | new |
| 57 | Lemma | final_check_spec | Lemma final_check_spec k: final_check k = true -> exists y z n, iter k x2' = Some y /\ LIncs_rec y (S(length y)) = Some (z,n,1%nat) /\ doom_rec z = true. | L767 | new |
| 58 | Lemma | halt_from | Lemma halt_from k: final_check k = true -> halts tm c0. | L782 | new |
| 59 | Lemma | halt | Lemma halt: halts tm c0. | L797 | adapted |
4What a maintainer readsCheck: the rule table below is what the .v proves, and proof.md / README read cleanly for a maintainer.
- submission/proof.md · informal proof (submitted copy)
- submission/README.md · the package README
- submission/discord.md · Discord draft (not posted)
- proof.md (working copy) · differs from the submitted copy
submission/proof.md line 63: 1. The rules at a glance
This block is in the style of a busycoq closing comment, in this machine's state names. Each item is defined and argued in §2–§8.
1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
= SOBCv6.v TM3 "1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD---" with ours A B C D E F = TM3 B C A E D F
0 1
A 1RB 0RD
B 1LC 1RE
C 1LA 0LD
D 0RE 0RF
E 1LC 1RA
F 0LE ---
words (paper order) W0 = 001 W1 = 111
lists head first: x = x_0 x_1 ... x_(k-1), x_0 next to the head
Lmp(x) 0^inf w(x_(k-1)) ... w(x_1) w(x_0)
RC(n) 1 (011)^n 01 0^inf
P(x) Lmp(x) <D 010 RC(1)
TM3 notation l <| r = l <D 010 r l |> r = l A> r
digits W1 W0 = digit 0, W1 W1 = digit 1, a lone W0 = separator; lowest digit next to the head
count(x) sum over digit pairs p (p = 0 next to the head) of (1 - b_p) 2^p
ones(x) x with every digit pair set to W1 W1
LInc Lmp(x) <D 010 r -->* Lmp(LInc x) 001 A> r r never read
LOv Lmp(x) <D 010 1 r -->* Lmp(LOv x) A> r x in {W0, W1 W1}*, r never read
Incs Lmp(x) <D 010 RC(1) -->* Lmp(ones x) <D 010 RC(c+1) c = count(x), c odd
Ov Lmp(x) <D 010 RC(2m+2) -->* Lmp((W1 W0)^m W1 W1 x') <D 010 RC(1) LOv(x) = W0 x'
cycle P(x) -->+ P((W1 W0)^((c-1)/2) W1 W1 x') c = count(x) odd, LOv(ones x) = W0 x'
walk0 Lmp(x) 001 <D 010 1 r -->(19) Lmp(x) <D 010 1 011 r Lmp(x) and r never read
walk1 Lmp(x) 111 111 <D 010 1 r -->(12) Lmp(x) <D 010 1 010101 r Lmp(x) and r never read
far Lmp(x_far) <D 010 1 r -->(1368) F reads 1 (halt) x_far = (W1 W1 W0)^5 (W1 W1)^3, r never read
LInc(W0 t) = W0 LInc(t) LInc(W1 W0 t) = W1 W1 t LInc(W1 W1 t) = W1 W0 LInc(t) LInc([]) undefined
LOv([]) = W0 W1 LOv(W0 t) = W1 LOv(t)
LOv(W1 W1 t) = W0 W0 W1 v' if LOv(t) = W0 v'
LOv(W1 W1 t) = W0 W0 W0 LInc(v') if LOv(t) = W1 v'
blocks (abstract) W10(l) = (W1 W0)^(1+l+n) W11(l) = (W1 W1)^(1+l+n) n >= 0 free for each block
step_rec x -> W10(n-1) W1 W1 x2 where LIncs_rec(x) = (x0, n, 1), n >= 1, LOv_rec(x0) = W0 x2
init c0 -->(847) P(x0) -->(1289) P(x1) -->(36437) P(x2) x0 = 1000111011, count 5, then count 51
chain x2 --(192 step_rec, maxv = 256)--> x194 (all succeed; smallest block bound 62)
halt P(x194) --Incs--> Lmp(z) <D 010 RC(2N+2), z = prefix ++ x_far, prefix in {W0, W1 W1, (W1 W1)^k}*
walk0 / walk1 through the prefix, then far: halts
5FamilyCheck: related machines are killed together or have a reason to be left open.
1 machines, 1 killed, 0 not. Family links: status.json parent, same transition table with another start (tools/dashboard.py), targeting.md follow-on rows, ledger "= twin" notes. A machine string named in a .v header / proof.md / notes.md is listed but does not make a family.
| who | machine | status | relation to this kill |
|---|---|---|---|
| W5-7 kill 25 | 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE--- | ✓Killed: halts | this kill |
| Named in a file but not linked (not counted as family) | |||
| off the list | 1RB---_1LC1RE_1LA0LD_0RE1LC_1LC1RF_1RB0RD | untouched | named in W5-7's notes.md |
| off the list | 1RB0RF_0RC1RD_0LD---_1LE1RA_1LA0LF_0RD0RC | untouched | named in W5-7's notes.md |
6ChecklistCheck: every ✓ is computed; the two ○ are yours to decide; an amber ! is an optional check that did not finish.
- ✓Machine string exactthe .v literal == holdout list line 738 byte for byte
- ✓Statement is
halts tm c0parsed from the .v and confirmed by check_kill (theorem_text, theorem_rocq) - ✓No axioms beyond baseline1 assumption(s); tools/assumptions_baseline.txt allows only functional_extensionality_dep
- ✓coqchk finished (optional)coqchk pass in 43.32 s
- ✓.v hash matches the checked hash.v = checked sha256 30ba96937271…; submission/ copy = checked sha256 30ba96937271…
- ✓No repo-local paths in the .vcomments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own
verify/X.vis fine: none in the .v or the submission/ copy - ✓Public write-up is cleantools/writeup_lint.py on
submission/proof.md: 0 error(s) - ○proof.md reviewed by Dennis (Checkpoint B)no Checkpoint B note from Dennis found
- ○Family posted together?no other kill in the family
Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.1 s from the files linked above; nothing in this review is hand-written except the box “How we proved it halts” (above), which quotes how_proved.md. Re-run: python3 -B tools/killreview.py 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
Files
machines/<tm>/: 11 entries · raw notes, status, scripts, images
| name | size | changed |
|---|---|---|
| notes.md ↓ | 9.2 KB | 2026-10-13 04:42 |
| proof.md ↓ | 38 KB | 2026-10-13 03:50 |
| how_proved.md ↓ | 1.7 KB | 2026-10-14 10:51 |
| status.json ↓ | 2.0 KB | 2026-10-13 04:42 |
| observe.json ↓ | 8.3 KB | 2026-10-13 03:01 |
| 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v ↓ | 23 KB | 2026-10-13 04:28 |
| img/ | 6 items | 2026-10-13 03:00 |
| rocq/ | 4 items | 2026-10-13 04:30 |
| submission/ | 5 items | 2026-10-14 09:18 |
| work/ | 5 items | 2026-10-13 03:21 |
| check_proof.py ↓ | 43 KB | 2026-10-13 03:48 |
status.json in full
{
"tm": "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---",
"label": "W5-7",
"status": "KILLED_HALT",
"stage": "done",
"updated": "2026-10-13",
"reason": "check_kill --halt PASS, independently re-verified",
"status_note": "The computed task asked for KILLED_NONHALT; the machine halts (the kill proves `Lemma halt: halts tm c0.`), so the status is KILLED_HALT, as for C2-552.",
"confidence": "high",
"template": "verify/SOBCv6.v Module TM3 (same table renamed: ours A B C D E F = TM3 B C A E D F, no mirror; started in TM3's B)",
"halt_steps": {
"approx": "power tower of height about 195",
"proven_in_coq": false,
"basis": "estimate from the cycle law (each count about 2^previous); not computed; the .v proves halts tm c0 only"
},
"eqv_partners": [
"1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LB---",
"1RB0RE_0LB1RC_1LD1RA_1LA0LE_0RC0RF_0LC---",
"1RB0RF_0RC1RD_0LD---_1LE1RA_1LA0LF_0RD0RC",
"1RB---_1LC1RE_1LA0LD_0RE1LC_1LC1RF_1RB0RD"
],
"eqv_note": "Settled through busycoq equivalences: Eqv_v3 TM637 (1RB0RE_0LB1RC_...) and TM636 (..._0LB---) at the pinned commit; Eqv_RegularPairs TM101 and Eqv_WordPairs TM98 at upstream HEAD. None is on the 740 list.",
"proof": {
"file": "proof.md",
"checker": "check_proof.py",
"checks": "46/46 PASS (full and --quick), work/check_proof.out"
},
"kill": {
"file": "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v",
"theorem": "halt : halts tm c0",
"sha256": "30ba969372712e441c93cb004872c9f78e9361ea47fb3e8e96c66957fc076786",
"lines": 838,
"check_kill": {
"result": "PASS",
"mode": "halt",
"checked_at": "2026-10-13T11:35:43Z",
"compile_s": 25.6,
"coqchk": "pass",
"coqchk_s": 43.3,
"coqchk_cap_s": 600,
"assumptions": [
"functional_extensionality_dep"
],
"log": "submission/check_kill.txt",
"earlier_runs": "rocq/check_kill.out (formalizer) and the independent audit run, same sha256"
},
"submission": "submission/",
"discord": "submission/discord.md, not posted (fill in <LINK>)"
}
}