BB(6) hunt
Machines / #30

1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC

#30local proof 15Kill claimedBell eats counterbbchallenge ↗Explorer

How we proved it never halts

Each epoch's cleanup costs only about the square root of its budget

Left of the head the tape reads 110 110 … 110 0 011 011 … 011: used blocks, a 0 marker, and budget blocks. Right of the head is a binary counter. On each bounce the head runs into the counter to add 1, comes back, and moves the marker one block right, usually turning a budget block into a used one. When one budget block is left, the machine eats the counter's lowest digit; sometimes that buys more budget, otherwise the head sweeps left and a new epoch starts with a larger budget, set by the length of the used run.

The eat leaves the counter messy, and the first bounces of the next epoch tidy it up. The tidying is recursive: at some digits a single bounce runs a whole mini-epoch on the rest of the counter, leaving its own mess one level deeper. The missing table entry (state D reading 0) can only come up if the budget runs out while the counter is still messy.

The key estimate: tidying a counter of k digit blocks costs about 2^(k/2) bounces, while the budget is at least about 2^(k+3), so the cleanup needs only about the square root of the budget. The proof bounds the cost with a weighted score over the counter's digits and carries an invariant from epoch to epoch, which works once the budget reaches 17,705. The 691 epochs before that (epochs 3 to 694, ending at budget 17,713) are computed exactly.

The Rocq proof checks every rule as an exact machine run, the cost bounds and the invariant from budget 17,705 up, and the opening by verified simulation. A verified model of the rules computes the 691 epochs, and a soundness proof turns that computation into a real machine run.

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

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

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

Overview

In one sentence

Marker bounce feeds a 3-cell binary counter; the bell eats only its low digit, so residue seeds the next epoch

Submitted mechanism A marker bounce feeding a counter. The hub is 0^inf (110)^a 0 (011)^b C> X 0^inf. Each bounce moves the 0 marker one block to the right, adds 1 to the counter word X and spends one 011 of the budget b. X is binary, LSB first: 3-cell blocks d01 (001)^e separated by 000, ending in a 4-stage tail. (submission/README.md, Mechanism)

Upstream
Kill claimed · PR #25merged 2026-10-16 07:08 UTC by ccz181078 · PR_BEC.v · TM4 · on Submissions →
Rocq proof
check_kill PASS · first Oct 10 18:31
1,726 lines · 86 KB .v · compile 15.5 s · coqchk pass · 0 axioms · PASS Oct 10 18:31
· the .v file
Automatic review
6 of 6 checks passtemplate: verify/FractalBEC.v (adapted from) · details in Proof →
Class
Bell eats counterours: Bell eats counter (sheet) · ours adds: partial eat with residue (sibling of #10) · med confidence
On the list
not on BB6_holdouts_663.txt (line 710 of the previous list) · historical 740 line 710
#30eqv ×1sim 1e15
Your calls on file 2
2026-10-10 · deepen
Fund one deepen stage on #30 (exact digestion rules, abstract epoch map checked against the TM, and a proof idea for 'eat after digestion'), or park it as STUCK next to #10? (auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.)
2026-10-10 · nest
Fund one more stage on #30's D6 nesting step (exact recursive rule plus a proof of the doubling law for digestion), or park it as STUCK? (auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.)

Mechanism

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

How it works: 3 notes
  • Hub K(a,b,X) = (110)^a 0 (011)^b C> X: each bounce moves the 0-marker one block and adds 1 to counter X.
  • Clean counter D(k,s,v): digits ?01 split by 001000, 4-stage tail; when b runs out only the low digit is eaten (E1/E2).
  • The rest seeds the next epoch as residue; forcing an eat during its digestion can halt, so we need eat time > digestion time.

Figures for Checkpoint A

Fig 1 · bbchallenge default view, 10,000 steps

The site's view. Find the diagonal stripes inside the bell and the busy right edge.

bbchallenge default view, 10,000 steps
bbchallenge-defaultStart blankRows every step: steps 0..9,999 squeezed into 500 px rows as on bbchallenge.orgWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: each px row blends steps 20y+9 and 20y+10, so 1 px row = 20 steps · Colors: red/green: pale = blended by the squeeze
Fig 2 · Epochs: marker diagonals and the counterQ1

Each down-right diagonal is one epoch (the 0-marker crossing the blocks); the counter is the right-edge strip.

Epochs: marker diagonals and the counter
bbchallenge-defaultStart blankRows one row per entry into state C moving rightWindow cells -425..0, 1 px = 1 cellColors 1 0 or never visited head (just moved right)
Rows: steps 0..300,000 (1,485 rows); not evenly spaced in time · Window: counted from the right edge (each row's rightmost visited cell is pinned to the last column)
Fig 3 · One residue epoch: counter word per bounceQ2

Rows are bounces. Compare the left strip's colour with the grey wedge: where does red appear?

One residue epoch: counter word per bounce
customStart blankRows one row per hub K(a,b,X)Window cells 0..63, 1 px = 1/4 cellColors 1 0 cells already absorbed into the (011) block region forcing the eat at this hub (b:=1) halts safe
Rows: (C moving right after (011)^b) from the left record at step 28,266 (k=47) to the next one at step 43,094: 61 rows, steps not evenly spaced · Window: (4x4 px per cell), counted from the epoch's first counter cell (absolute, so the word stays put as b shrinks), plus a 6 px strip on the left · Colors: left strip
More figures (4)Fig 4–7: Left and right records to 100M steps · Blaze, 10 million steps · Digestion share per epoch to 1e11 steps · Digestion cost / sqrt(N), model orbit
Fig 4 · Left and right records to 100M steps

One row per new edge cell. The left edge moves 2 cells per epoch; the right edge carries the counter.

Left and right records to 100M steps
bbchallenge-defaultStart blankRows the start, then one per new leftmost or rightmost cellWindow cells -146..3,283, 1 px = 1 cellColors 1 0 or never visited head on a new right/left cell
Rows: (3,430 rows, steps 0..100,000,000); not evenly spaced in time
Fig 5 · Blaze, 10 million steps

The bell's outline over 1e7 steps; no chaotic edge.

Blaze, 10 million steps
bbchallenge-blazeStart blankRows time blocks of 16,384 stepsWindow cells -80..1,468, 1 px = ~1.9 cellsColors 0 1
Rows: averaged (611 blocks, steps 0..10,000,000), stretched to 500 px: 1 px ~ 20,000 steps · Window: Blaze's 1,549 columns stretched to 800 px · Colors: in-between shades = both mixed inside the pixel's block (averaged); no head
Fig 6 · Digestion share per epoch to 1e11 steps

Dots sit far below the yellow budget line and under the blue curve, and they sink as N grows.

Digestion share per epoch to 1e11 steps
customStart blankRows no rows: one dot per epoch of the blank-tape orbit to step 100,000,000,000Window x = log10 N from 1 to 4.2Colors one epoch budget beta = N (the eat) 8/sqrt(N) ticks: N = 10
Rows: 517 epochs with N >= 10 and a digestion phase · Window: (N = b at the epoch's first hub), y = beta/N from 0 (bottom) to 1 (top), 420 x 220 px · Colors: white: beta = b used until the hub word is back in grammar G; blue: exhaustive clean-residue maximum; 100, 1000, 10,000
Fig 7 · Digestion cost / sqrt(N), model orbit

Green dots are TM-checked epochs, white ones the model beyond. Compare their height with the blue line.

Digestion cost / sqrt(N), model orbit
customStart blankRows no rows: one dot per epoch of the rules-only model orbitWindow x = log10 N from 1 to 6.2Colors epoch checked against the TM log later model epoch budget beta = N (y = sqrt N) 7.95 ticks: N = 10 .
Rows: epochs 3..80,585; epochs 3..519 equal the TM log to 1e11 steps · Window: (N = b at the epoch start), y = beta/sqrt(N) from 0 (bottom) to 10 (top), 420 x 220 px · Colors: blue: clean-residue maximum with 2^(k+3) <= N; 10^6
Rules (6/7 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
R restart
0∞ <A 101 (001)k 000 Y 0∞
⟶ 0∞ 110 0 (011)k+1 C> Y 0∞
any Y not starting with 011; k <= 30003k+7✓600/600
B bounce
0∞ (110)a 0 (011)b+1 C> X 0∞
⟶ 0∞ (110)a+1 0 (011)b+d C> inc(X) 0∞
b >= 1; X = any of 9,730 orbit hub words; inc(X), d in {0,1} and c(X) do not depend on a, b8b+c(X)✓600/600
W clean counter
0∞ (110)a 0 (011)b+1 C> D(n) 0∞
⟶ 0∞ (110)a+1 0 (011)b+[n=3] C> D(n+1) 0∞
D(n) = (v0 01 001000)...(v_(k-1) 01) tail_s, n = 2^(k+2)-4+s*2^k+v, tails '',0001,000010001,000110001; D(1..3)=1,010001,110001; n <= 1e5—✓600/600
E2 odd eat
0∞ (110)a 0 011 C> 101 E(j,s,u) 0∞
⟶ 0∞ <A 101 (001)a 000 11 E(j,s,u+1) 0∞
E(0,s,0)=tail_s, E(j,s,u)=001000 D(j,s,u); u+1=2^j overflows to s+1; j <= 9—✓600/600
E1 even eat
0∞ (110)a 0 011 C> (001)i 000 Y 0∞
⟶ 0∞ (110)a+2 0 (011)i C> Y 0∞
i >= 1 (i <= 40 tested), Y random / orbit / clean words not starting with 011—✓600/600
E0 empty
0∞ (110)a 0 011 C> 0∞
⟶ 0∞ <A 101 (001)a+1 0001 0∞
a <= 3000—✓200/200
digestion (open)
0∞ 110 0 (011)N C> 11 E(j,s,u) 0∞
⟶ clean counter after O(len) bounces
not exact yet: inc on words with extra 001 groups; forced eats halt at 1-2 bounce counts inside this window—–untested
Compressed historythe tape as 0∞ <A 101 (001)k T 0∞ at 40 moments: where the rules are read off
0∞ <A 101 (001)k T 0∞
stepk (left record; next epoch has b = k+1)len T (residue cells)T (residue word)
28141
1242131,000,010,001
3047910,001
8881541
2,45817181.1·1014
4,8983141
10,19033231.1·1019
17,49644231.1·1019
28,2664739000110010010010010010...
123,0649327000110010000010010001...
361,03214132000110010000010010001...
860,62419165000110010010010010010...
1,681,59625432000110010001010010001...
3,011,45631545000110010001010010001...
5,070,53038166000110010010010010010...
7,976,35244965000110010010010010010...
11,910,01652347000110010010010001010...
17,123,68860450000110010001010010000...
23,784,45066596000110010010010010010...
32,098,26074884000110010010010010010...
42,062,39881289000110010010010010010...
54,178,78289774000110010010010010010...
68,368,956959101000110010010010010010...
84,929,7401,03983000110010010010010000...
104,187,5421,13850000110010001010010001...
126,702,1441,213101000110010010010010010...
152,598,7181,31445000110010001010010001...
182,046,3361,377129000110010010010010010...
215,153,6201,48445000110010000010010000...
252,476,6781,547111000110010010010010010...
293,968,0941,66232000110010001010010001...
340,352,8941,717143000110010010010010010...
391,125,5621,82859000110010000010010000...
447,163,9121,889125000110010010010010010...
508,490,5661,983101000110010010010010010...
575,132,5582,08568000110010000010010000...
648,268,7662,165119000110010010010010010...
728,156,3082,261128000110010010010010010...
814,752,4182,37550000110010001010010000...
908,922,6822,46674000110010010010001010...
k (left record; next epoch has b = k+1)last 2,466
2,4661289.1e8log xstep 28: k (left record; next epoch has b = k+1) = 1step 124: k (left record; next epoch has b = k+1) = 2step 304: k (left record; next epoch has b = k+1) = 7step 888: k (left record; next epoch has b = k+1) = 15step 2458: k (left record; next epoch has b = k+1) = 17step 4898: k (left record; next epoch has b = k+1) = 31step 10190: k (left record; next epoch has b = k+1) = 33step 17496: k (left record; next epoch has b = k+1) = 44step 28266: k (left record; next epoch has b = k+1) = 47step 123064: k (left record; next epoch has b = k+1) = 93step 361032: k (left record; next epoch has b = k+1) = 141step 860624: k (left record; next epoch has b = k+1) = 191step 1681596: k (left record; next epoch has b = k+1) = 254step 3011456: k (left record; next epoch has b = k+1) = 315step 5070530: k (left record; next epoch has b = k+1) = 381step 7976352: k (left record; next epoch has b = k+1) = 449step 11910016: k (left record; next epoch has b = k+1) = 523step 17123688: k (left record; next epoch has b = k+1) = 604step 23784450: k (left record; next epoch has b = k+1) = 665step 32098260: k (left record; next epoch has b = k+1) = 748step 42062398: k (left record; next epoch has b = k+1) = 812step 54178782: k (left record; next epoch has b = k+1) = 897step 68368956: k (left record; next epoch has b = k+1) = 959step 84929740: k (left record; next epoch has b = k+1) = 1039step 104187542: k (left record; next epoch has b = k+1) = 1138step 126702144: k (left record; next epoch has b = k+1) = 1213step 152598718: k (left record; next epoch has b = k+1) = 1314step 182046336: k (left record; next epoch has b = k+1) = 1377step 215153620: k (left record; next epoch has b = k+1) = 1484step 252476678: k (left record; next epoch has b = k+1) = 1547step 293968094: k (left record; next epoch has b = k+1) = 1662step 340352894: k (left record; next epoch has b = k+1) = 1717step 391125562: k (left record; next epoch has b = k+1) = 1828step 447163912: k (left record; next epoch has b = k+1) = 1889step 508490566: k (left record; next epoch has b = k+1) = 1983step 575132558: k (left record; next epoch has b = k+1) = 2085step 648268766: k (left record; next epoch has b = k+1) = 2165step 728156308: k (left record; next epoch has b = k+1) = 2261step 814752418: k (left record; next epoch has b = k+1) = 2375step 908922682: k (left record; next epoch has b = k+1) = 2466
len T (residue cells)last 74
1434289.1e8log xstep 28: len T (residue cells) = 4step 124: len T (residue cells) = 13step 304: len T (residue cells) = 9step 888: len T (residue cells) = 4step 2458: len T (residue cells) = 18step 4898: len T (residue cells) = 4step 10190: len T (residue cells) = 23step 17496: len T (residue cells) = 23step 28266: len T (residue cells) = 39step 123064: len T (residue cells) = 27step 361032: len T (residue cells) = 32step 860624: len T (residue cells) = 65step 1681596: len T (residue cells) = 32step 3011456: len T (residue cells) = 45step 5070530: len T (residue cells) = 66step 7976352: len T (residue cells) = 65step 11910016: len T (residue cells) = 47step 17123688: len T (residue cells) = 50step 23784450: len T (residue cells) = 96step 32098260: len T (residue cells) = 84step 42062398: len T (residue cells) = 89step 54178782: len T (residue cells) = 74step 68368956: len T (residue cells) = 101step 84929740: len T (residue cells) = 83step 104187542: len T (residue cells) = 50step 126702144: len T (residue cells) = 101step 152598718: len T (residue cells) = 45step 182046336: len T (residue cells) = 129step 215153620: len T (residue cells) = 45step 252476678: len T (residue cells) = 111step 293968094: len T (residue cells) = 32step 340352894: len T (residue cells) = 143step 391125562: len T (residue cells) = 59step 447163912: len T (residue cells) = 125step 508490566: len T (residue cells) = 101step 575132558: len T (residue cells) = 68step 648268766: len T (residue cells) = 119step 728156308: len T (residue cells) = 128step 814752418: len T (residue cells) = 50step 908922682: len T (residue cells) = 74
T (residue word)last 000110010010010001010...
1.1e1912817,496log ystep 28: T (residue word) = 1step 124: T (residue word) = 1000010001step 304: T (residue word) = 10001step 888: T (residue word) = 1step 2458: T (residue word) = 110010001010001step 4898: T (residue word) = 1step 10190: T (residue word) = 11001000101001000101step 17496: T (residue word) = 11001000101000010001
Template comparisonFractalBEC.v: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0RF
B1RC1RF
C1LD0REtpl 1RB
D---0LE
E1LA0LE
F0RA0LC

differs from the template

file
FractalBEC.v:269
module
—
machine
1RB0RF_1RC1RF_1LD1RB_---0LE_1LA0LE_0RA0LC (1 transition apart)
diff
C1: template (tm10 mirrored) 1RB, ours 0RE; #10 has 1RA
note
RInc (marker bounce) = our B. LInc (2-cell counter) and Ov/P0 (whole counter eaten, fractal doubling k -> 2k+3) do not hold: our counter has 3-cell digits + 4-stage tail and the eat is partial (E1/E2), leaving residue. Same hub as #10 (STUCK on Lemma X).
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Deepen: exact rules for digestion and for counters with extra 001 groups, then an abstract epoch map (N, residue) -> (N', residue') checked against the TM, then prove 'digestion < N' as an inductive size invariant; proof shaped like FractalBEC/BECv7.

  • ▲Digestion may not close into a short rule list (as #10's Lemma X).
  • ▲Safety is not regular (random eat times halt), so no CTL shortcut.
  • ▲Non-clean counters (75/138 eats) may hide further cases.
Stats & provenance109 steps simulated · 7,720 cells · the status in full · files
simulated
109 steps
tape
7,720 cells · 4,642 nonzeros
growth
left edge +2 cells/epoch; 137 epochs to 1e9; k = 2,497 at step 983,786,092; right edge ~t^0.36
status now
check_kill PASS, independently re-verified (status.json, 2026-10-10)
observer's note
Rules R/B/W/E0/E1/E2 exact and validated; residue digestion and the size invariant (eat after digestion) are open, so confidence med.
files
observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v

Proof & checks

6/6 automatic checks pass

Kill 15 · Bell eats counter · the kill file 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v: 1726 lines, 219 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (adapted from): verify/FractalBEC.v · 3% 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_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC
vs holdout list
✓ byte-exact: the .v literal (L33) == 2026-10-07_778.txt line 748 (41 bytes, via tools/holdouts.py)
Theorem
✓ Lemma nonhalt: ~halts tm c0. L1706
check_kill
✓ PASS · 17/17 checks pass · compile 15.47 s · coqchk pass (67.68 s) · assumptions: 0 (closed) · 2026-10-11 01:31:40 UTC · submission/check_kill.txt
Checked .v
sha256 93a493f553118578…
✓1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v93a493f553118578… = checked
✓submission/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v93a493f553118578… = 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
✓input88034 bytes, 1726 lines, 2012 sentences
✓frameworkHEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓framework_build13 needed framework .vo files present and fresh, with native code no older than the .vo
✓forbiddennone of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)
✓structure5 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓tm_textline 33: TM_from_str "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC" == <tm> (41 bytes)
✓theorem_textline 1706: nonhalt : ~halts tm c0
✓coqcoqc 8.20.1 ([local working file]
✓nameshalts, c0, TM_from_str resolved inside Individual62
✓compilecompiled in 15.5s with all appended checks
✓tm_rocqBB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC" by eq_refl (in-file and isolated)
✓theorem_rocqnonhalt : ~ halts (TM_from_str "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC") 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 (67.7s); 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/FractalBEC.v · detected from 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v line 21
3%of our lines identical to the template
0changed lines
1469added lines (ours only)
186template lines dropped
0 / 1 / 218items identical / adapted / new
What the package README says it reused and changed (submission/README.md line 17, Template and what changed), quoted:

Adapted from busycoq's verify/FractalBEC.v, tm10 (1LB0LF_1LC1LF_1RD1LB_---0RE_1RA0RE_0LA0RC). Mirrored, tm10 differs from this machine only in C1 (1RB there, 0RE here).

  • Kept: tm10's marker bounce RInc, mirrored, as the region pass RP0/RP1; es for every finite run; multistep_nonhalt from an exact start.
  • Changed: tm10's counter (LInc, 2-cell digits) and its whole-counter eat (Ov) do not occur here, and neither does its induction on the epoch number with progress_nonhalt_simple. Everything above the bounce is new: the word syntax, LP/Phi with the nested sub-epoch, counter words and their potentials, the epoch invariant with progress_nonhalt_cond, and the fuel model for the finite part.

The file has 1,726 lines, every lemma top level, and imports only Individual62 from busycoq.

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 1511 lines
3% identical · 0 changed · 1469 added
template 228 lines
18% kept verbatim · 186 not in ours
our items 219
0 identical · 1 adapted · 218 new · 36 template-only
identicalchanged / adaptedours only (new)template only
Template part: whole file. Ours: lines 26–1726 (header comment 1–25 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: BinaryCounter_0_full, L, R, Incs, f, P0, P1, nxtP1, P0nxt, P0_0, P0_spec, config, config_S, Cert, tm1, nonhalt1, tm2, nonhalt2, tm3, nonhalt3, tm4, nonhalt4, tm5, nonhalt5, tm6, nonhalt6, tm7, nonhalt7, tm8, nonhalt8, tm9, nonhalt9, tm10, nonhalt10, tm11, nonhalt11

Side-by-side diff: template (228 lines) vs ours (1511 lines), 1655 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.27From BusyCoq Require Import Individual62.
2Require Import Lia.28Require Import Lia.
3Require Import ZArith.
4Require Import String.29Require Import String.
5From BusyCoq Require Import BinaryCounter.
30Require Import List.
6From BusyCoq Require Import BinaryCounterFull.
31Require Import Arith.
8Open Scope list.
33Definition tm := Eval compute in (TM_from_str "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC").
10Ltac er := execute_with_rotate.
35Notation "c --> c'" := (c -[ tm ]-> c') (at level 40).
11Ltac sr := use_shift_rule; simpl_rotate.
13Ltac es :=
⋯ 20 template-only lines (template 14–35), not in ours
36Hypothesis QL QR:Q.
37Hypothesis qL qR d1 w1 w0:list sym.
39Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).36Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
40Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).37Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
42Notation "l <| r" :=
39Open Scope list.
43 (l <{{QL}} qL *> r) (at level 30).
41(* ===================================================================== *)
45Notation "l |> r" :=
42(* Section 1. Finite runs (write-up 3.1-3.7), each one plain es. *)
46 (l <* qR {{QR}}> r) (at level 30).
43(* Left sides are written nearest-cell-first (<[...] reverses a literal). *)
48Definition L n := BinaryCounter_0 d1 n.
44(* ===================================================================== *)
50Definition R n m r := w1^^n *> w0 *> w1^^m *> r.
46(* LP0: 011 C> 0 r -> <A 100 1 r *)
52Hypothesis LInc:
47Lemma LP0 l r : l <* <[0;1;1] {{C}}> [0] *> r -->+ l <{{A}} [1;0;0;1] *> r.
53 forall r n,
48Proof. es. Qed.
54 L n <| r -->+
50Lemma LP0z l : l <* <[0;1;1] {{C}}> 0inf -->+ l <{{A}} [1;0;0;1] *> 0inf.
55 L (N.succ n) |> r.
51Proof. es. Qed.
57Hypothesis RInc:
53(* LP11: 011 C> 110 r -> <A 101 000 r *)
58 forall l r n m,
54Lemma LP11 l r : l <* <[0;1;1] {{C}}> [1;1;0] *> r -->+ l <{{A}} [1;0;1;0;0;0] *> r.
59 l |> R (1+n) m r -->+
55Proof. es. Qed.
60 l <| R n (1+m) r.
57(* LPC (carry), right pass: 011 C> 101 (001)^e 000 r -> 011 111 (011)^e 011 C> r *)
62Lemma Incs k n m r:
58Lemma LPCr l e r : l <* <[0;1;1] {{C}}> [1;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
63 L (N.of_nat k) <| R n m r -->+
59 l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <* <[0;1;1] {{C}}> r.
64 L (N.of_nat (1+k+n)) |> R 0 (n+m) r.
60Proof. es. Qed.
62(* LPC, left pass after an exit with d = 0 / d = 1 *)
63Lemma LPCl0 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;0] *> r -->+
64 l <{{A}} [1;0;0;0;0;1] *> [0;0;1]^^e *> [0;0;0] *> r.
65Proof. es. Qed.
67Lemma LPCl1 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;1;0;0;0] *> r -->+
68 l <{{A}} [1;0;0;0;0;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.
69Proof. es. Qed.
71(* LP5 (D5): 011 C> 10 001 (001)^e 000 r -> 011 11 (011)^(e+1) 011 C> r, and back *)
72Lemma LP5r l e r : l <* <[0;1;1] {{C}}> [1;0;0;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
73 l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <* <[0;1;1] {{C}}> r.
74Proof. es. Qed.
76Lemma LP5l0 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{A}} [1;0;0] *> r -->+
77 l <{{A}} [1;0;0;0;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.
78Proof. es. Qed.
80Lemma LP5l1 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{A}} [1;0;1;0;0;0] *> r -->+
81 l <{{A}} [1;0;0;0;1] *> [0;0;1]^^(S (S e)) *> [0;0;0] *> r.
82Proof. es. Qed.
84(* LP6 (D6), right pass: builds the sub-hub 011 1 . 110 0 (011)^(e+1) C> r *)
85Lemma LP6r l e r : l <* <[0;1;1] {{C}}> [1;0;1;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
86 l <* <[0;1;1;1] <* <[1;1;0] <* [0] <* <[0;1;1]^^(S e) {{C}}> r.
87Proof. es. Qed.
89(* W10, the D6 exit: 011 E> 1 r -> <A 100 0 r *)
90Lemma W10 l r : l <* <[0;1;1;1] <{{E}} r -->+ l <{{A}} [1;0;0;0] *> r.
91Proof. es. Qed.
93(* RP0 / RP1: the region pass (FractalBEC's RInc) *)
94Lemma RP0 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{A}} [1;0;0] *> r -->+
95 l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S n) {{C}}> r.
96Proof. es. Qed.
98Lemma RP1 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{A}} [1;0;1;0;0;0] *> r -->+
99 l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S (S n)) {{C}}> r.
100Proof. es. Qed.
102(* Eats at b = 1 *)
103Lemma E1r l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [0;0;1]^^(S e) *> [0;0;0] *> r -->+
104 l <* <[1;1;0]^^(S (S a)) <* [0] <* <[0;1;1]^^(S e) {{C}}> r.
105Proof. es. Qed.
107Lemma E2l0 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;0] *> r -->+
108 l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;1] *> [0;0;1]^^e *> [0;0;0] *> r.
109Proof. es. Qed.
111Lemma E2l1 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;1;0;0;0] *> r -->+
112 l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.
113Proof. es. Qed.
115Lemma Et0 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> 0inf -->+
116 l <{{E}} [0;1] *> [0;0;1]^^(S a) *> [0;0;0;1] *> 0inf.
117Proof. es. Qed.
119Lemma Et1 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [1] *> 0inf -->+
120 l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.
121Proof. es. Qed.
123Lemma Et2 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [0;1;0;0;0;1] *> 0inf -->+
124 l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
125Proof. es. Qed.
127Lemma Et3 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [1;1;0;0;0;1] *> 0inf -->+
128 l <* <[1;1;0]^^(S a) <* [0] <* <[0;1;1] {{C}}> [0;0;1] *> 0inf.
129Proof. es. Qed.
131(* Restart from a pre-record (write-up 3.7, plus the step L' -> L) *)
132Lemma Rst k r : const 0 <{{E}} [0;1] *> [0;0;1]^^k *> [0;0;0] *> r -->+
133 const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^(S k) {{C}}> r.
134Proof. rewrite (const_unfold _ S0) at 1. es. Qed.
136(* LPT: the constant end words *)
137Lemma LPT1 l : l <* <[0;1;1] {{C}}> [1] *> 0inf -->+ l <{{A}} [1;0;0;0;1;0;0;0;1] *> 0inf.
138Proof. es. Qed.
140Lemma LPT2 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;0;1] *> 0inf -->+
141 l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.
142Proof. es. Qed.
144Lemma LPT3 l : l <* <[0;1;1] {{C}}> [1;0;1;1;0;0;0;1] *> 0inf -->+
145 l <{{A}} [1;0;0] *> [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
146Proof. es. Qed.
148Lemma LPT4 l : l <* <[0;1;1] {{C}}> [1;0;0;0;0;1;0;0;0;1] *> 0inf -->+
149 l <{{A}} [1;0;0] *> [0;1;0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.
150Proof. es. Qed.
152Lemma LPT5 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf -->+
153 l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
154Proof. es. Qed.
156Lemma LPT6 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;1;0;0;0;1] *> 0inf -->+
157 l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
158Proof. es. Qed.
160Lemma z3 : [0;0;0] *> const 0 = const 0.
161Proof. cbn. rewrite <- !const_unfold. reflexivity. Qed.
163(* ===================================================================== *)
164(* Section 2. Words, the local pass LP and the epoch map Phi. *)
165(* ===================================================================== *)
167(* blk d e w = d01 (001)^e 000 w; p11 x w = 11 (001)^x 000 w; p01 x w = 01 (001)^x 000 w;
168 p00 w = 00 w; p10 w = 10 w; tails t0 = '', t1 = 1, t2 = 010001, t3 = 110001. *)
169Inductive word : Type :=
170| t0 | t1 | t2 | t3
171| blk (d : bool) (e : nat) (w : word)
172| p11 (x : nat) (w : word)
173| p01 (x : nat) (w : word)
174| p00 (w : word)
175| p10 (w : word).
177Definition dsym (d : bool) : Sym := if d then S1 else S0.
179Fixpoint enc (w : word) : side :=
180 match w with
181 | t0 => const 0
182 | t1 => [1] *> const 0
183 | t2 => [0;1;0;0;0;1] *> const 0
184 | t3 => [1;1;0;0;0;1] *> const 0
185 | blk d e w => [dsym d; 0; 1] *> [0;0;1]^^e *> [0;0;0] *> enc w
186 | p11 x w => [1;1] *> [0;0;1]^^x *> [0;0;0] *> enc w
187 | p01 x w => [0;1] *> [0;0;1]^^x *> [0;0;0] *> enc w
188 | p00 w => [0;0] *> enc w
189 | p10 w => [1;0] *> enc w
190 end.
192Definition addb (e : nat) (d : bool) : nat := if d then S e else e.
194(* LP w w' d: the local pass maps w to w', d = true if it absorbs one 011 block.
195 Phi a b w k y: the epoch map from the hub (110)^a 0 (011)^b C> w to the pre-record
196 E> . 01 (001)^k 000 y (write-up 3.8). *)
197Inductive LP : word -> word -> bool -> Prop :=
198| LP_a e w : LP (blk false e w) (blk true e w) false
199| LP_b e w w' d : LP w w' d -> LP (blk true e w) (blk false (addb e d) w') false
200| LP_t0 : LP t0 t1 false
201| LP_t1 : LP t1 t2 false
202| LP_t2 : LP t2 t3 false
203| LP_t3 : LP t3 (blk false 0 t0) true
204| LP_11S x w : LP (p11 (S x) w) (p01 x w) true
205| LP_110 w : LP (p11 0 w) (p00 w) true
206| LP_01 x w : LP (p01 x w) (p11 x w) false
207| LP_00 w : LP (p00 w) (p10 w) false
208| LP_5 e w w' d : LP w w' d -> LP (p10 (blk false e w)) (p01 (S (addb e d)) w') false
209| LP_6 e w k y : Phi 1 (S e) w k y -> LP (p10 (blk true e w)) (blk false k y) false
210| LP_T2 : LP (p10 t2) (p01 1 (p01 1 t1)) false
211| LP_T3 : LP (p10 t3) (p00 (p01 0 t2)) false
212| LP_T4 : LP (p10 (p00 t2)) (p01 0 (p01 1 t1)) false
213| LP_T5 : LP (p10 (p01 0 t2)) (p01 1 (p10 (p00 t2))) false
214| LP_T6 : LP (p10 (p01 1 t1)) (p01 2 (p10 (p00 t2))) false
215| LP_eq w1 w2 w' d : enc w1 = enc w2 -> LP w2 w' d -> LP w1 w' d
216with Phi : nat -> nat -> word -> nat -> word -> Prop :=
217| Phi_B a b w w' d k y : LP w w' d -> Phi (S a) (addb (S b) d) w' k y -> Phi a (S (S b)) w k y
218| Phi_E1 a e w k y : Phi (S (S a)) (S e) w k y -> Phi a 1 (blk false e w) k y
219| Phi_E2 a e w w' d : LP w w' d -> Phi a 1 (blk true e w) a (p11 (addb e d) w')
220| Phi_E0 a : Phi a 1 t0 (S a) t1
221| Phi_Et1 a : Phi a 1 t1 a (p01 1 t1)
222| Phi_Et2 a : Phi a 1 t2 a (p10 (p00 t2))
223| Phi_Et3 a k y : Phi (S a) 1 (blk false 0 t0) k y -> Phi a 1 t3 k y
224| Phi_eq a b w1 w2 k y : enc w1 = enc w2 -> Phi a b w2 k y -> Phi a b w1 k y.
226Scheme LP_mind := Induction for LP Sort Prop
227with Phi_mind := Induction for Phi Sort Prop.
228Combined Scheme LP_Phi_mind from LP_mind, Phi_mind.
230Definition outp (d : bool) (r : side) : side :=
231 if d then [1;0;1;0;0;0] *> r else [1;0;0] *> r.
233Definition LPspec (w w' : word) (d : bool) : Prop :=
234 forall l, l <* <[0;1;1] {{C}}> enc w -->+ l <{{A}} outp d (enc w').
236Definition Phispec (a b : nat) (w : word) (k : nat) (y : word) : Prop :=
237 forall l, l <* <[1;1;0]^^a <* [0] <* <[0;1;1]^^b {{C}}> enc w -->+
238 l <{{E}} [0;1] *> [0;0;1]^^k *> [0;0;0] *> enc y.
240Lemma enc_a0 : enc (blk false 0 t0) = [0;0;1] *> const 0.
241Proof. cbn [enc]. rewrite z3. reflexivity. Qed.
243(* ===================================================================== *)
244(* Section 3. Soundness: every LP / Phi derivation is a TM run. *)
245(* ===================================================================== *)
247Theorem sound :
248 (forall w w' d, LP w w' d -> LPspec w w' d) /\
249 (forall a b w k y, Phi a b w k y -> Phispec a b w k y).
65Proof.250Proof.
66 follow10 LInc.
251 apply LP_Phi_mind; unfold LPspec, Phispec.
67 gen k m.
252 - (* LP_a *) intros e w l. exact (LP0 l ([0;1] *> [0;0;1]^^e *> [0;0;0] *> enc w)).
68 induction n; intros.
253 - (* LP_b *) intros e w w' d H IH l. destruct d.
69 - finish.
254 + eapply progress_trans. { exact (LPCr l e (enc w)). }
70 - follow100 RInc.
255 eapply progress_trans. { exact (IH (l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e)). }
71 follow100 LInc.
256 exact (LPCl1 l e (enc w')).
72 follow (IHn (1+k) (1+m)).
257 + eapply progress_trans. { exact (LPCr l e (enc w)). }
73 finish.
258 eapply progress_trans. { exact (IH (l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e)). }
259 exact (LPCl0 l e (enc w')).
260 - (* LP_t0 *) intros l. exact (LP0z l).
261 - (* LP_t1 *) intros l. exact (LPT1 l).
262 - (* LP_t2 *) intros l. exact (LP0 l ([1;0;0;0;1] *> const 0)).
263 - (* LP_t3 *) intros l. unfold outp. rewrite enc_a0. exact (LP11 l ([0;0;1] *> const 0)).
264 - (* LP_11S *) intros x w l. exact (LP11 l ([0;1] *> [0;0;1]^^x *> [0;0;0] *> enc w)).
265 - (* LP_110 *) intros w l. exact (LP11 l ([0;0] *> enc w)).
266 - (* LP_01 *) intros x w l. exact (LP0 l ([1] *> [0;0;1]^^x *> [0;0;0] *> enc w)).
267 - (* LP_00 *) intros w l. exact (LP0 l ([0] *> enc w)).
268 - (* LP_5 *) intros e w w' d H IH l. destruct d.
269 + eapply progress_trans. { exact (LP5r l e (enc w)). }
270 eapply progress_trans. { exact (IH (l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e))). }
271 exact (LP5l1 l e (enc w')).
272 + eapply progress_trans. { exact (LP5r l e (enc w)). }
273 eapply progress_trans. { exact (IH (l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e))). }
274 exact (LP5l0 l e (enc w')).
275 - (* LP_6 *) intros e w k y H IH l.
276 eapply progress_trans. { exact (LP6r l e (enc w)). }
277 eapply progress_trans. { exact (IH (l <* <[0;1;1;1])). }
278 exact (W10 l ([0;1] *> [0;0;1]^^k *> [0;0;0] *> enc y)).
279 - (* LP_T2 *) intros l. exact (LPT2 l).
280 - (* LP_T3 *) intros l. exact (LPT3 l).
281 - (* LP_T4 *) intros l. exact (LPT4 l).
282 - (* LP_T5 *) intros l. exact (LPT5 l).
283 - (* LP_T6 *) intros l. exact (LPT6 l).
284 - (* LP_eq *) intros w1 w2 w' d E H IH l. rewrite E. apply IH.
285 - (* Phi_B *) intros a b w w' d k y H IH H2 IH2 l. destruct d.
286 + eapply progress_trans. { exact (IH (l <* <[1;1;0]^^a <* [0] <* <[0;1;1]^^(S b))). }
287 eapply progress_trans. { exact (RP1 (l <* <[1;1;0]^^a) b (enc w')). }
288 exact (IH2 l).
289 + eapply progress_trans. { exact (IH (l <* <[1;1;0]^^a <* [0] <* <[0;1;1]^^(S b))). }
290 eapply progress_trans. { exact (RP0 (l <* <[1;1;0]^^a) b (enc w')). }
291 exact (IH2 l).
292 - (* Phi_E1 *) intros a e w k y H IH l.
293 eapply progress_trans. { exact (E1r l a e (enc w)). }
294 exact (IH l).
295 - (* Phi_E2 *) intros a e w w' d H IH l. destruct d.
296 + eapply progress_trans. { exact (LPCr (l <* <[1;1;0]^^a <* [0]) e (enc w)). }
297 eapply progress_trans. { exact (IH (l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e)). }
298 exact (E2l1 l a e (enc w')).
299 + eapply progress_trans. { exact (LPCr (l <* <[1;1;0]^^a <* [0]) e (enc w)). }
300 eapply progress_trans. { exact (IH (l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e)). }
301 exact (E2l0 l a e (enc w')).
302 - (* Phi_E0 *) intros a l. exact (Et0 l a).
303 - (* Phi_Et1 *) intros a l. exact (Et1 l a).
304 - (* Phi_Et2 *) intros a l. exact (Et2 l a).
305 - (* Phi_Et3 *) intros a k y H IH l.
306 eapply progress_trans. { exact (Et3 l a). }
307 specialize (IH l). rewrite enc_a0 in IH. exact IH.
308 - (* Phi_eq *) intros a b w1 w2 k y E H IH l. rewrite E. apply IH.
74Qed.309Qed.
76Hypothesis Ov:
311(* ===================================================================== *)
77 forall r n m,
312(* Section 4. Epochs and the start. *)
78 L (Npos (pow2' n)) |> R 0 m r -->*
313(* ===================================================================== *)
79 const 0 <| (w0^^n *> w1^^(2+m) *> r).
315Definition K (N : nat) (y : word) : Q * tape :=
81Definition f i :=
316 const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^N {{C}}> enc y.
82 (N.to_nat (Npos (pow2' i) - 1)).
318Lemma epoch_tm N y k y' : Phi 1 N y k y' -> K N y -->+ K (S k) y'.
84Definition P0 i :=
85 forall r,
⋯ 7 template-only lines (template 86–94), not in ours
95 P0 i ->
96 P1 i.
97Proof.319Proof.
98 unfold P0,P1,f.
320 intros H. eapply progress_trans.
99 intros HP0 r.
321 - exact (proj2 sound _ _ _ _ _ H (const 0)).
100 remember (N.to_nat (N.pos (pow2' i) - 1)) as n.
322 - apply Rst.
101 follow10 (Incs 0 n 0 r).
102 replace (N.of_nat (1+0+n)) with (Npos (pow2' i)) by lia.
⋯ 5 template-only lines (template 103–107), not in ours
108 simpl_tape.
109 finish.
110Qed.323Qed.
112Lemma P0nxt i:
325(* The blank tape reaches L(7, 000 010001) at step 304, then the restart gives K(1,8,t2). *)
113 P0 i ->
326Lemma init : c0 -->* K 8 t2.
114 P0 (1+i).
327Proof. unfold K. cbn. solve_init. Qed.
329(* ===================================================================== *)
330(* Section 5. A computable model (fuel), sound for LP / Phi. *)
331(* ===================================================================== *)
333Fixpoint lpf (n : nat) (w : word) {struct n} : option (word * bool) :=
334 match n with
335 | O => None
336 | S n' =>
337 match w with
338 | t0 => Some (t1, false)
339 | t1 => Some (t2, false)
340 | t2 => Some (t3, false)
341 | t3 => Some (blk false 0 t0, true)
342 | blk false e w => Some (blk true e w, false)
343 | blk true e w =>
344 match lpf n' w with Some (w', d) => Some (blk false (addb e d) w', false) | None => None end
345 | p11 (S x) w => Some (p01 x w, true)
346 | p11 O w => Some (p00 w, true)
347 | p01 x w => Some (p11 x w, false)
348 | p00 w => Some (p10 w, false)
349 | p10 w =>
350 match w with
351 | t0 => Some (t2, false)
352 | t1 => Some (blk false 0 t1, false)
353 | t2 => Some (p01 1 (p01 1 t1), false)
354 | t3 => Some (p00 (p01 0 t2), false)
355 | blk false e w =>
356 match lpf n' w with Some (w', d) => Some (p01 (S (addb e d)) w', false) | None => None end
357 | blk true e w =>
358 match phif n' 1 (S e) w with Some (k, y) => Some (blk false k y, false) | None => None end
359 | p00 t0 => Some (t2, false)
360 | p00 t1 => Some (p01 1 t1, false)
361 | p00 t2 => Some (p01 0 (p01 1 t1), false)
362 | p01 0 t2 => Some (p01 1 (p10 (p00 t2)), false)
363 | p01 1 t1 => Some (p01 2 (p10 (p00 t2)), false)
364 | p10 (p00 t2) => Some (blk false 0 t3, false)
365 | _ => None
366 end
367 end
368 end
369with phif (n : nat) (a b : nat) (w : word) {struct n} : option (nat * word) :=
370 match n with
371 | O => None
372 | S n' =>
373 match b with
374 | O => None
375 | S O =>
376 match w with
377 | blk false e w => phif n' (S (S a)) (S e) w
378 | blk true e w =>
379 match lpf n' w with Some (w', d) => Some (a, p11 (addb e d) w') | None => None end
380 | t0 => Some (S a, t1)
381 | t1 => Some (a, p01 1 t1)
382 | t2 => Some (a, p10 (p00 t2))
383 | t3 => phif n' (S a) 1 (blk false 0 t0)
384 | p10 t0 => Some (a, p01 1 t1)
385 | p10 t1 => Some (a, p11 0 t1)
386 | p00 t0 => Some (S a, t1)
387 | p00 t1 => phif n' (S (S a)) 1 t0
388 | _ => None
389 end
390 | S (S b') =>
391 match lpf n' w with
392 | Some (w', d) => phif n' (S a) (addb (S b') d) w'
393 | None => None
394 end
395 end
396 end.
398Lemma enc_p10t0 : enc (p10 t0) = enc t1.
399Proof. cbn. rewrite <- const_unfold. reflexivity. Qed.
401Lemma enc_p10t1 : enc (p10 t1) = enc (blk true 0 t0).
402Proof. cbn [enc lpow dsym]. rewrite z3. reflexivity. Qed.
404Lemma enc_p00t0 : enc (p00 t0) = enc t0.
405Proof. cbn. rewrite <- !const_unfold. reflexivity. Qed.
407Lemma enc_p00t1 : enc (p00 t1) = enc (blk false 0 t0).
408Proof. cbn [enc lpow dsym]. rewrite z3. reflexivity. Qed.
410Lemma enc_p10p00t0 : enc (p10 (p00 t0)) = enc t1.
411Proof. cbn. rewrite <- !const_unfold. reflexivity. Qed.
413Lemma enc_p10p00t1 : enc (p10 (p00 t1)) = enc (p10 (blk false 0 t0)).
414Proof. cbn [enc lpow dsym]. rewrite z3. reflexivity. Qed.
416Lemma model_sound n :
417 (forall w w' d, lpf n w = Some (w', d) -> LP w w' d) /\
418 (forall a b w k y, phif n a b w = Some (k, y) -> Phi a b w k y).
115Proof.419Proof.
116 unfold P0.
420 induction n as [|n [IHl IHp]]; [split; intros; discriminate|].
117 intros HP0 r.
421 split.
118 replace (1+i) with (i+1) by lia.
422 - intros w w' d H. cbn [lpf] in H.
119 rewrite lpow_add,Str_app_assoc.
423 destruct w as [| | | |[|] e w|[|x] w|x w|w|w]; try (inversion H; subst; constructor; fail).
120 follow HP0.
424 + destruct (lpf n w) as [[w1 d1]|] eqn:E; inversion H; subst. constructor. apply IHl, E.
121 pose proof (nxtP1 i HP0) as HP1.
425 + destruct w as [| | | |[|] e w|[|x] w|x w|w|w]; try discriminate.
122 unfold P1 in HP1.
426 * inversion H; subst. eapply LP_eq; [apply enc_p10t0 | constructor].
123 simpl_tape.
427 * inversion H; subst. eapply LP_eq; [apply enc_p10t1 | ]. apply (LP_b 0 t0 t1 false). constructor.
124 follow100 HP1.
428 * inversion H; subst. constructor.
125 finish.
429 * inversion H; subst. constructor.
430 * destruct (phif n 1 (S e) w) as [[k y]|] eqn:E; inversion H; subst. constructor. apply IHp, E.
431 * destruct (lpf n w) as [[w1 d1]|] eqn:E; inversion H; subst. constructor. apply IHl, E.
432 * destruct x as [|[|x]]; try discriminate; destruct w; try discriminate;
433 inversion H; subst; constructor.
434 * destruct w; try discriminate; inversion H; subst.
435 -- eapply LP_eq; [apply enc_p10p00t0 | constructor].
436 -- eapply LP_eq; [apply enc_p10p00t1 | ]. apply (LP_5 0 t0 t1 false). constructor.
437 -- constructor.
438 * destruct w; try discriminate. destruct w; try discriminate. inversion H; subst.
439 apply (LP_eq _ (blk true 0 t2)); [reflexivity | ]. apply (LP_b 0 t2 t3 false). constructor.
440 - intros a b w k y H. cbn [phif] in H.
441 destruct b as [|[|b]]; try discriminate.
442 + destruct w as [| | | |[|] e w|[|x] w|x w|w|w]; try discriminate.
443 * inversion H; subst. constructor.
444 * inversion H; subst. constructor.
445 * inversion H; subst. constructor.
446 * constructor. apply IHp, H.
447 * destruct (lpf n w) as [[w1 d1]|] eqn:E; inversion H; subst. constructor. apply IHl, E.
448 * constructor. apply IHp, H.
449 * destruct w; try discriminate; inversion H; subst.
450 -- eapply Phi_eq; [apply enc_p00t0 | constructor].
451 -- eapply Phi_eq; [apply enc_p00t1 | ]. constructor. apply IHp, H.
452 * destruct w; try discriminate; inversion H; subst.
453 -- eapply Phi_eq; [apply enc_p10t0 | constructor].
454 -- eapply Phi_eq; [apply enc_p10t1 | ]. apply (Phi_E2 _ 0 t0 t1 false). constructor.
455 + destruct (lpf n w) as [[w1 d1]|] eqn:E; try discriminate.
456 eapply Phi_B; [apply IHl, E | apply IHp, H].
126Qed.457Qed.
128Lemma P0_0:
460(* ===================================================================== *)
129 P0 0.
461(* Section 6. Counter words G, their value, and the counting phase. *)
462(* ===================================================================== *)
464Open Scope nat_scope.
466Definition tl_of (s : nat) : word :=
467 match s with O => t0 | 1 => t1 | 2 => t2 | _ => t3 end.
469Fixpoint gw (bs : list (bool * nat)) (s : nat) : word :=
470 match bs with [] => tl_of s | (d, e) :: bs => blk d e (gw bs s) end.
472Fixpoint ginc (bs : list (bool * nat)) (s : nat) : list (bool * nat) * nat * bool :=
473 match bs with
474 | [] => match s with O => ([], 1, false) | 1 => ([], 2, false) | 2 => ([], 3, false)
475 | _ => ([(false, 0)], O, true) end
476 | (false, e) :: bs => ((true, e) :: bs, s, false)
477 | (true, e) :: bs => let '(bs', s', d) := ginc bs s in ((false, addb e d) :: bs', s', false)
478 end.
480Fixpoint gval (bs : list (bool * nat)) (s : nat) : nat :=
481 match bs with [] => 4 + s | (d, _) :: bs => (if d then 1 else 0) + 2 * gval bs s end.
483Fixpoint gsum (bs : list (bool * nat)) : nat :=
484 match bs with [] => O | (_, e) :: bs => e + gsum bs end.
486Lemma ginc_LP bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) -> LP (gw bs s) (gw bs' s') d.
130Proof.487Proof.
131 unfold P0.
488 intros Hs. induction bs as [|[[|] e] bs IH]; intros bs' s' d E; cbn in E.
132 es.
489 - destruct s as [|[|[|[|s]]]]; inversion E; subst; cbn; try constructor; lia.
490 - destruct (ginc bs s) as [[b1 s1] d1] eqn:E1. inversion E; subst. cbn. constructor. apply IH; reflexivity.
491 - inversion E; subst. constructor.
133Qed.492Qed.
135Lemma P0_spec i:
494Lemma ginc_val bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) ->
136 P0 i.
495 gval bs' s' = S (gval bs s) /\ s' <= 3 /\
496 gsum bs' + length bs + (if d then 1 else 0) = gsum bs + length bs' /\
497 (d = true -> bs = []) /\ length bs <= length bs'.
137Proof.498Proof.
138 induction i.
499 intros Hs. induction bs as [|[[|] e] bs IH]; intros bs' s' d E; cbn in E.
139 - apply P0_0.
500 - destruct s as [|[|[|[|s]]]]; inversion E; subst; cbn; repeat split; try lia; auto.
140 - apply P0nxt,IHi.
501 - destruct (ginc bs s) as [[b1 s1] d1] eqn:E1. inversion E; subst.
502 destruct (IH _ _ _ eq_refl) as (H1 & H2 & H3 & H4 & H5). cbn.
503 destruct d1; cbn [addb]; [specialize (H4 eq_refl); subst bs; cbn in *|]; repeat split; try lia; discriminate.
504 - inversion E; subst. cbn. repeat split; try lia; discriminate.
141Qed.505Qed.
143Definition config i :=
507Lemma gval_ge bs s : 4 <= gval bs s.
144 const 0 <| w1^^f i *> const 0.
508Proof. induction bs as [|[d e] bs IH]; cbn; lia. Qed.
146Hypothesis w0_all0:
510Lemma gval_len bs s : length bs <= gval bs s.
147 w0 *> const 0 = const 0.
511Proof. induction bs as [|[d e] bs IH]; cbn; [lia|]. pose proof (gval_ge bs s). lia. Qed.
149Lemma config_S i:
513(* Psi = value + budget + sum of exponents - number of blocks: no bounce raises it, every
150 config i -->+ config (S i).
514 E1g lowers it by value - 1 >= 3. So every counting phase ends (gcount below; cf. the
515 write-up's D.0). *)
516Definition Psi (bs : list (bool * nat)) (s b : nat) : nat := gval bs s + b + gsum bs - length bs.
518Import ListNotations.
520(* ===================================================================== *)
521(* Section 7. The epoch map on counter words, multi-step LP, digestion. *)
522(* ===================================================================== *)
524Definition blks := list (bool * nat).
525Definition b2n (d : bool) : nat := if d then 1 else 0.
526Lemma addb_b2n e d : addb e d = e + b2n d.
527Proof. destruct d; cbn; lia. Qed.
529Inductive GRes : Type := RE2 (k x : nat) (bs : blks) (s : nat) | RSp (k : nat) (y : word).
530Definition rk (r : GRes) : nat := match r with RE2 k _ _ _ => k | RSp k _ => k end.
531Definition ry (r : GRes) : word := match r with RE2 _ x bs s => p11 x (gw bs s) | RSp _ y => y end.
533(* GPhi a b bs s r: the epoch map Phi on a counter word, bounce by bounce (write-up 3.6, 3.8). *)
534Inductive GPhi : nat -> nat -> blks -> nat -> GRes -> Prop :=
535| GB a b bs s bs' s' d r : ginc bs s = (bs', s', d) -> GPhi (S a) (addb (S b) d) bs' s' r ->
536 GPhi a (S (S b)) bs s r
537| GE1 a e bs s r : GPhi (S (S a)) (S e) bs s r -> GPhi a 1 ((false, e) :: bs) s r
538| GE2 a e bs s bs' s' d : ginc bs s = (bs', s', d) ->
539 GPhi a 1 ((true, e) :: bs) s (RE2 a (addb e d) bs' s')
540| GE0 a : GPhi a 1 [] 0 (RSp (S a) t1)
541| GEt1 a : GPhi a 1 [] 1 (RSp a (p01 1 t1))
542| GEt2 a : GPhi a 1 [] 2 (RSp a (p10 (p00 t2)))
543| GEt3 a r : GPhi (S a) 1 [(false, 0)] 0 r -> GPhi a 1 [] 3 r.
545Lemma ginc_s3 bs s bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> s' <= 3.
546Proof. intros Hs E. destruct (ginc_val bs s Hs _ _ _ E) as (_ & H & _). exact H. Qed.
548Lemma GPhi_sound a b bs s r : GPhi a b bs s r -> s <= 3 -> Phi a b (gw bs s) (rk r) (ry r).
151Proof.549Proof.
152 unfold config.
550 induction 1; intros Hs; cbn [gw rk ry tl_of] in *.
153 epose proof (nxtP1 i (P0_spec i) (const 0)) as HP1.
551 - eapply Phi_B. { apply (ginc_LP bs s Hs _ _ _ H). } apply IHGPhi. eapply ginc_s3; eauto.
154 rewrite w0_all0 in HP1.
552 - apply Phi_E1. apply IHGPhi. exact Hs.
155 follow10 HP1.
553 - apply Phi_E2. apply (ginc_LP bs s Hs _ _ _ H).
156 finish.
554 - apply Phi_E0.
555 - apply Phi_Et1.
556 - apply Phi_Et2.
557 - apply Phi_Et3. apply IHGPhi. lia.
157Qed.558Qed.
159Hypothesis init:
560Lemma GPhi_s3 a b bs s r : GPhi a b bs s r -> s <= 3 ->
160 c0 -->*
561 match r with RE2 _ _ _ s2 => s2 <= 3 | RSp _ y => y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2) end.
161 config 0.
163Lemma nonhalt:~halts tm c0.
164Proof.562Proof.
165 eapply multistep_nonhalt.
563 induction 1; intros Hs; auto; try (apply IHGPhi; first [lia | eapply ginc_s3; eauto]).
166 1: apply init.
564 eapply ginc_s3; eauto.
167 eapply progress_nonhalt_simple.
168 intro i. eexists.
169 apply config_S.
170Qed.565Qed.
172End FractalBEC.
567Lemma GPhi_rk a b bs s r : GPhi a b bs s r -> a + b <= S (rk r).
175Inductive Cert :=
568Proof. induction 1; try destruct d; cbn [rk addb] in *; lia. Qed.
176| cert1
570Lemma gcount : forall P bs s a b, s <= 3 -> 1 <= b -> Psi bs s b <= P -> exists r, GPhi a b bs s r.
177 (QL QR : Q)
571Proof.
178 (qL qR d1 w1 w0 : list Sym).
572 induction P as [P IHP] using lt_wf_ind.
180Ltac solve_cert cert :=
573 intros bs s a b. revert bs s a. induction b as [b IHb] using lt_wf_ind. intros bs s a Hs Hb HP.
181match cert with
574 destruct b as [|[|b]]; [lia| |].
182 (cert1
575 - destruct bs as [|[[|] e] bs].
183 ?QL ?QR
576 + destruct s as [|[|[|[|s]]]]; try lia.
184 ?qL ?qR ?d1 ?w1 ?w0) =>
577 * eexists. apply GE0.
185 eapply (nonhalt _
578 * eexists. apply GEt1.
186 QL QR
579 * eexists. apply GEt2.
187 qL qR d1 w1 w0);
580 * eexists. apply GEt3. apply (GE1 _ 0 []). apply GE0.
188 [ intros;
581 + destruct (ginc bs s) as [[b1 s1] d1] eqn:E1. eexists. eapply GE2. exact E1.
189 apply LInc_0;
582 + assert (Hlt : Psi bs s (S e) < P).
190 try (es; fail)
583 { unfold Psi in *. cbn [gval gsum length] in HP. pose proof (gval_ge bs s). pose proof (gval_len bs s). lia. }
191 | unfold R;
584 destruct (IHP _ Hlt bs s (S (S a)) (S e) Hs ltac:(lia) (le_n _)) as (r & H).
192 intros;
585 exists r. apply GE1, H.
193 try (es; fail)
586 - destruct (ginc bs s) as [[b1 s1] d1] eqn:E1.
194 | intros;
587 destruct (ginc_val bs s Hs _ _ _ E1) as (V1 & S1 & M1 & D1 & L1).
195 unfold L,R;
588 destruct d1.
196 rewrite BinaryCounter_0_full;
589 + specialize (D1 eq_refl). subst bs. cbn in E1.
197 try (es; fail)
590 destruct s as [|[|[|[|s]]]]; inversion E1; subst; try lia.
198 | solve_const0_eq
591 assert (Hlt : S b < S (S b)) by lia.
199 | unfold config,f;
592 destruct (IHb _ Hlt [(true, 0)] 0 (S (S a)) ltac:(lia) ltac:(lia)) as (r & H).
200 cbn;
593 { unfold Psi in *. cbn in HP |- *. lia. }
201 try (es; fail)
594 exists r. eapply GB. { exact E1. }
202 ]
595 cbn [addb]. eapply GB. { reflexivity. } exact H.
596 + assert (Hlt : S b < S (S b)) by lia.
597 destruct (IHb _ Hlt b1 s1 (S a) S1 ltac:(lia)) as (r & H).
598 { unfold Psi in *. lia. }
599 exists r. eapply GB. { exact E1. } exact H.
600Qed.
602(* Multi-step local pass: n LP steps, c absorptions. *)
603Inductive LPs : word -> word -> nat -> nat -> Prop :=
604| LPs_eq w w' : enc w = enc w' -> LPs w w' 0 0
605| LPs_step w w1 w2 d n c : LP w w1 d -> LPs w1 w2 n c -> LPs w w2 (S n) (c + b2n d).
607Lemma LPs_step' w w1 w2 d n c c' : LP w w1 d -> LPs w1 w2 n c -> c' = c + b2n d -> LPs w w2 (S n) c'.
608Proof. intros H1 H2 ->. econstructor; eauto. Qed.
610Lemma LPs_eql w0 w1 w2 n c : enc w0 = enc w1 -> LPs w1 w2 n c -> LPs w0 w2 n c.
611Proof.
612 intros E H. inversion H; subst.
613 - apply LPs_eq. congruence.
614 - eapply LPs_step; [apply (LP_eq _ _ _ _ E); eassumption | eassumption].
615Qed.
617Lemma LPs_trans w1 w2 w3 n c n' c' : LPs w1 w2 n c -> LPs w2 w3 n' c' -> LPs w1 w3 (n + n') (c + c').
618Proof.
619 intros H. revert n' c' w3. induction H; intros n' c' w3 H'.
620 - cbn. eapply LPs_eql; eassumption.
621 - eapply LPs_step'; [eassumption | apply IHLPs, H' | ]. destruct d; cbn; lia.
622Qed.
624Lemma LPs_cn w w' n c : LPs w w' n c -> c <= n.
625Proof. induction 1; [lia | destruct d; cbn; lia]. Qed.
627Lemma LPs_hub w w' n c : LPs w w' n c -> forall a B k y, n + 2 <= B + c ->
628 Phi (a + n) (B + c - n) w' k y -> Phi a B w k y.
629Proof.
630 induction 1 as [w w' E | w w1 w2 d n c H1 H2 IH]; intros a B k y Hb HP.
631 - rewrite Nat.add_0_r in HP. replace (B + 0 - 0) with B in HP by lia. eapply Phi_eq; eassumption.
632 - pose proof (LPs_cn _ _ _ _ H2) as Hc.
633 destruct B as [|[|B]]; [destruct d; cbn in Hb; lia | destruct d; cbn in Hb; lia |].
634 eapply Phi_B; [exact H1|]. apply IH.
635 + rewrite addb_b2n. destruct d; unfold b2n in *; lia.
636 + rewrite addb_b2n. replace (S a + n) with (a + S n) by lia.
637 replace (S B + b2n d + c - n) with (S (S B) + (c + b2n d) - S n) by (destruct d; unfold b2n; lia).
638 exact HP.
639Qed.
641Lemma LPs_nest y y' n c : LPs y y' n c -> forall k, LPs (blk false k y) (blk false (k + c) y') (2 * n) 0.
642Proof.
643 induction 1 as [y y' E | y y1 y2 d n c H1 H2 IH]; intros k.
644 - rewrite Nat.add_0_r. apply LPs_eq. cbn [enc]. rewrite E. reflexivity.
645 - replace (2 * S n) with (S (S (2 * n))) by lia.
646 replace (k + (c + b2n d)) with (addb k d + c) by (rewrite addb_b2n; lia).
647 eapply LPs_step'; [apply LP_a | eapply LPs_step'; [apply (LP_b k y y1 d H1) | apply IH | reflexivity] | reflexivity].
648Qed.
650(* The end words of a digestion (the end words of write-up 3.4), as explicit finite chains. *)
651Inductive DigE : word -> nat -> nat -> blks -> nat -> Prop :=
652| DE0 : DigE (p10 t0) 0 0 [] 1
653| DE1 : DigE (p10 t1) 0 0 [(true, 0)] 0
654| DE2 : DigE (p10 t2) 13 5 [(false, 0)] 2
655| DE3 : DigE (p10 t3) 7 2 [(false, 0)] 2
656| DEs0 : DigE t1 0 0 [] 1
657| DEs1 : DigE (p01 1 t1) 2 1 [] 2
658| DEs2 : DigE (p10 (p00 t2)) 11 4 [(false, 0)] 2.
660Ltac lps := first [ apply LPs_eq; first [reflexivity | apply enc_p10t0 | apply enc_p10t1]
661 | eapply LPs_step'; [ constructor | lps | reflexivity ] ].
663Lemma DigE_sound y n c bs s : DigE y n c bs s -> LPs y (gw bs s) n c.
664Proof. destruct 1; cbn [gw tl_of]; lps. Qed.
666Lemma DigE_props y n c bs s : DigE y n c bs s ->
667 n <= 13 /\ c <= 5 /\ length bs <= 1 /\ s <= 3 /\ Forall (fun e => e = 0) (map snd bs).
668Proof. destruct 1; cbn; repeat split; auto; lia. Qed.
670(* Digestion of a residue: DigP x bs s = digestion of 11 (001)^x 000 W, DigT = of 10 W, with W the
671 counter word gw bs s. n LP steps (own level), c absorptions, result gw bsp sp. A b-block runs a
672 sub-epoch (GPhi) and the next level is nested inside the new block (LPs_nest). *)
673Inductive DigP : nat -> blks -> nat -> nat -> nat -> blks -> nat -> Prop :=
674| DP x bs s n c bsp sp : DigT bs s n c bsp sp -> DigP x bs s (2 * x + 2 + n) (S x + c) bsp sp
675with DigT : blks -> nat -> nat -> nat -> blks -> nat -> Prop :=
676| DTa e bs s bs' s' d n c bsp sp : ginc bs s = (bs', s', d) ->
677 DigP (S (addb e d)) bs' s' n c bsp sp -> DigT ((false, e) :: bs) s (S (S n)) c bsp sp
678| DTb e bs s k x bs2 s2 n c bsp sp : GPhi 1 (S e) bs s (RE2 k x bs2 s2) ->
679 DigP x bs2 s2 n c bsp sp -> DigT ((true, e) :: bs) s (S (2 * n)) 0 ((false, k + c) :: bsp) sp
680| DTs e bs s k y n c bsp sp : GPhi 1 (S e) bs s (RSp k y) ->
681 DigE y n c bsp sp -> DigT ((true, e) :: bs) s (S (2 * n)) 0 ((false, k + c) :: bsp) sp
682| DTt s n c bsp sp : DigE (p10 (tl_of s)) n c bsp sp -> DigT [] s n c bsp sp.
684Scheme DigP_mind := Induction for DigP Sort Prop
685with DigT_mind := Induction for DigT Sort Prop.
686Combined Scheme Dig_mind from DigP_mind, DigT_mind.
688Lemma prefix_LPs x w : LPs (p11 x w) (p10 w) (2 * x + 2) (S x).
689Proof.
690 induction x as [|x IH].
691 - eapply LPs_step'; [apply LP_110 | eapply LPs_step'; [apply LP_00 | apply LPs_eq; reflexivity | reflexivity] | reflexivity].
692 - replace (2 * S x + 2) with (S (S (2 * x + 2))) by lia.
693 eapply LPs_step'; [apply LP_11S | eapply LPs_step'; [apply LP_01 | exact IH | reflexivity] | cbn; lia].
694Qed.
696Lemma Dig_sound :
697 (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> LPs (p11 x (gw bs s)) (gw bsp sp) n c) /\
698 (forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> LPs (p10 (gw bs s)) (gw bsp sp) n c).
699Proof.
700 apply Dig_mind.
701 - intros x bs s n c bsp sp H IH Hs.
702 exact (LPs_trans _ _ _ _ _ _ _ (prefix_LPs x (gw bs s)) (IH Hs)).
703 - intros e bs s bs' s' d n c bsp sp E H IH Hs. cbn [gw].
704 eapply LPs_step'; [apply LP_5, (ginc_LP bs s Hs _ _ _ E) |
705 eapply LPs_step'; [apply LP_01 | apply IH; eapply ginc_s3; eauto | reflexivity] | cbn; lia].
706 - intros e bs s k x bs2 s2 n c bsp sp HG H IH Hs. cbn [gw].
707 pose proof (GPhi_s3 _ _ _ _ _ HG Hs) as Hs2. cbn in Hs2.
708 eapply LPs_step'; [apply LP_6; exact (GPhi_sound _ _ _ _ _ HG Hs) |
709 exact (LPs_nest _ _ _ _ (IH Hs2) k) | reflexivity].
710 - intros e bs s k y n c bsp sp HG H Hs. cbn [gw].
711 eapply LPs_step'; [apply LP_6; exact (GPhi_sound _ _ _ _ _ HG Hs) |
712 exact (LPs_nest _ _ _ _ (DigE_sound _ _ _ _ _ H) k) | reflexivity].
713 - intros s n c bsp sp H Hs. cbn [gw]. exact (DigE_sound _ _ _ _ _ H).
714Qed.
716Lemma Dig_sp :
717 (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> sp <= 3) /\
718 (forall bs s n c bsp sp, DigT bs s n c bsp sp -> sp <= 3).
719Proof.
720 apply Dig_mind; intros; auto; eapply DigE_props; eassumption.
721Qed.
723(* One epoch from an ordinary residue: digestion (n bounces), then counting (GPhi). *)
724Lemma epoch_ord N x bs s n c bsp sp r : s <= 3 -> DigP x bs s n c bsp sp -> n + 2 <= N ->
725 GPhi (1 + n) (N + c - n) bsp sp r -> Phi 1 N (p11 x (gw bs s)) (rk r) (ry r).
726Proof.
727 intros Hs HD Hn HG.
728 apply (LPs_hub _ _ _ _ (proj1 Dig_sound _ _ _ _ _ _ _ HD Hs) 1 N); [lia|].
729 apply GPhi_sound; [exact HG | exact (proj1 Dig_sp _ _ _ _ _ _ _ HD)].
730Qed.
732Lemma epoch_spec N y n c bsp sp r : DigE y n c bsp sp -> n + 2 <= N ->
733 GPhi (1 + n) (N + c - n) bsp sp r -> Phi 1 N y (rk r) (ry r).
734Proof.
735 intros HD Hn HG.
736 apply (LPs_hub _ _ _ _ (DigE_sound _ _ _ _ _ HD) 1 N); [lia|].
737 apply GPhi_sound; [exact HG | apply (DigE_props _ _ _ _ _ HD)].
738Qed.
740(* ===================================================================== *)
741(* Section 8. Positions and potentials (write-up D.0, Lemma C, D.7). *)
742(* ===================================================================== *)
744Definition exs (bs : blks) : list nat := map snd bs.
746Fixpoint bumpl (l : list nat) : list nat :=
747 match l with [] => [] | e :: l' => match l' with [] => [S e] | _ => e :: bumpl l' end end.
749Lemma length_bumpl l : length (bumpl l) = length l.
750Proof. induction l as [|e l IH]; [reflexivity|]. destruct l; cbn in *; [reflexivity|]. rewrite IH. reflexivity. Qed.
752Lemma length_exs bs : length (exs bs) = length bs.
753Proof. apply length_map. Qed.
755(* inc on G: the exponents stay, or (overflow) the last one gets +1 and a new 0 is appended. *)
756Lemma ginc_exps bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) ->
757 (exs bs' = exs bs /\ d = false) \/
758 (exs bs' = bumpl (exs bs) ++ [0] /\ d = match bs with [] => true | _ => false end).
759Proof.
760 intros Hs. induction bs as [|[[|] e] bs IH]; intros bs' s' d E; cbn in E.
761 - destruct s as [|[|[|[|s]]]]; inversion E; subst; cbn; auto; lia.
762 - destruct (ginc bs s) as [[b1 s1] d1] eqn:E1. inversion E; subst.
763 destruct (IH _ _ _ eq_refl) as [[H1 H2] | [H1 H2]]; subst; unfold exs in *; cbn [map snd].
764 + left. rewrite H1. auto.
765 + right. rewrite H1. destruct bs as [|b bs]; cbn in *; subst; cbn; auto.
766 - inversion E; subst. left. auto.
767Qed.
769(* ---------- the Q potential: bounds the number of positions ---------- *)
771Fixpoint qsum (l : list nat) : nat := match l with [] => 0 | e :: l => S e + 2 * qsum l end.
772Definition Qp (f : nat) (bs : blks) (s p : nat) : nat := 2 ^ f * (gval bs s + 2 * qsum (exs bs) + p).
773Definition QI (Q0 f : nat) (bs : blks) (s p : nat) : Prop := Qp f bs s p <= Q0 + 3 * 2 ^ (f + length bs).
775Lemma qsum_app0 l : qsum (l ++ [0]) = qsum l + 2 ^ length l.
776Proof. induction l as [|e l IH]; cbn [qsum app length]; [reflexivity|]. rewrite IH. cbn. lia. Qed.
778Lemma qsum_bumpl l : l <> [] -> 2 * qsum (bumpl l) = 2 * qsum l + 2 ^ length l.
779Proof.
780 induction l as [|e l IH]; intros Hne; [congruence|].
781 destruct l as [|e' l]; [cbn; lia|].
782 change (bumpl (e :: e' :: l)) with (e :: bumpl (e' :: l)).
783 cbn [qsum length]. rewrite Nat.pow_succ_r'. specialize (IH ltac:(discriminate)). cbn [qsum length] in IH. lia.
784Qed.
786Lemma gval_lb bs s : 4 * 2 ^ length bs <= gval bs s.
787Proof. induction bs as [|[d e] bs IH]; cbn [gval length]; [cbn; lia|]. rewrite Nat.pow_succ_r'. lia. Qed.
789Lemma gval_ub bs s : s <= 3 -> gval bs s < 8 * 2 ^ length bs.
790Proof. intros Hs. induction bs as [|[d e] bs IH]; cbn [gval length]; [cbn; lia|]. rewrite Nat.pow_succ_r'. destruct d; lia. Qed.
792Lemma QI_low Q0 f bs s p : QI Q0 f bs s p -> 2 ^ (f + length bs) <= Q0.
793Proof.
794 unfold QI, Qp. intros H. pose proof (gval_lb bs s) as G. rewrite Nat.pow_add_r in *.
795 assert (2 ^ f * (4 * 2 ^ length bs) <= 2 ^ f * (gval bs s + 2 * qsum (exs bs) + p)) by (apply Nat.mul_le_mono_l; lia).
796 lia.
797Qed.
799Lemma QI_Ps Q0 Ps f bs s p : QI Q0 f bs s p -> Q0 < 2 ^ (Ps + 1) -> f + length bs <= Ps.
800Proof.
801 intros H HP. apply QI_low in H. destruct (Nat.le_gt_cases (f + length bs) Ps) as [|Hc]; [assumption|].
802 assert (2 ^ (Ps + 1) <= 2 ^ (f + length bs)) by (apply Nat.pow_le_mono_r; lia). lia.
803Qed.
805Lemma QI_drop Q0 f bs s p : QI Q0 f bs s p -> QI Q0 f bs s 0.
806Proof. unfold QI, Qp. intros H. assert (2 ^ f * (gval bs s + 2 * qsum (exs bs) + 0) <= 2 ^ f * (gval bs s + 2 * qsum (exs bs) + p)) by (apply Nat.mul_le_mono_l; lia). lia. Qed.
808Lemma QI_cons Q0 f dd e bs s p : QI Q0 f ((dd, e) :: bs) s 0 -> p <= S e -> QI Q0 (S f) bs s p.
809Proof.
810 unfold QI, Qp, exs. cbn [map snd qsum gval length]. intros H Hp.
811 replace (S f + length bs) with (f + S (length bs)) by lia.
812 rewrite Nat.pow_succ_r'.
813 set (F := 2 ^ f) in *. set (G := gval bs s) in *. set (Q := qsum (map snd bs)) in *.
814 assert (F * p <= F * S e) by (apply Nat.mul_le_mono_l; lia).
815 assert (E1 : 2 * F * (G + 2 * Q + p) = 2 * (F * G) + 4 * (F * Q) + 2 * (F * p)) by ring.
816 assert (E2 : F * ((if dd then 1 else 0) + 2 * G + 2 * (S e + 2 * Q) + 0) =
817 F * (if dd then 1 else 0) + 2 * (F * G) + 2 * (F * S e) + 4 * (F * Q)) by ring.
818 rewrite E1. rewrite E2 in H. lia.
819Qed.
821Lemma QI_inc Q0 f bs s p bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) ->
822 QI Q0 f bs s (S p) -> QI Q0 f bs' s' (p + b2n d).
823Proof.
824 intros Hs E H. unfold QI, Qp in *.
825 destruct (ginc_val bs s Hs _ _ _ E) as (V & _).
826 destruct (ginc_exps bs s Hs _ _ _ E) as [[E1 E2] | [E1 E2]]; subst d.
827 - assert (L : length bs' = length bs) by (rewrite <- !length_exs, E1; reflexivity).
828 rewrite E1, V, L. cbn [b2n]. replace (S (gval bs s) + 2 * qsum (exs bs) + (p + 0)) with
829 (gval bs s + 2 * qsum (exs bs) + S p) by lia. exact H.
830 - assert (L : length bs' = S (length bs))
831 by (rewrite <- !length_exs, E1, length_app, length_bumpl; cbn; lia).
832 rewrite E1, V, L, qsum_app0, length_bumpl, length_exs.
833 replace (f + S (length bs)) with (S (f + length bs)) by lia.
834 rewrite Nat.pow_succ_r'. rewrite Nat.pow_add_r in *.
835 destruct bs as [|b bs0].
836 + cbn [bumpl exs map qsum length b2n] in *. rewrite Nat.pow_0_r in *.
837 rewrite !Nat.mul_add_distr_l in *. lia.
838 + cbn [b2n]. pose proof (qsum_bumpl (exs (b :: bs0)) ltac:(cbn; discriminate)) as QB.
839 rewrite length_exs in QB.
840 set (F := 2 ^ f) in *. set (X := 2 ^ length (b :: bs0)) in *.
841 set (G := gval (b :: bs0) s) in *. set (Q := qsum (exs (b :: bs0))) in *.
842 set (Q' := qsum (bumpl (exs (b :: bs0)))) in *.
843 rewrite !Nat.mul_add_distr_l in *.
844 assert (F * (2 * (Q' + X)) = 2 * (F * Q) + 3 * (F * X)) by nia.
845 lia.
846Qed.
848Lemma QI_et3 Q0 f : QI Q0 f [] 3 0 -> QI Q0 f [(false, 0)] 0 0.
849Proof. unfold QI, Qp. cbn. rewrite !Nat.add_0_r. rewrite Nat.add_1_r, Nat.pow_succ_r'. lia. Qed.
851(* ---------- generic weighted potentials over positions ---------- *)
853Fixpoint wpot (v : nat -> nat) (al be f : nat) (l : list nat) : nat :=
854 match l with [] => 0 | e :: l => v f * (al * e + be) + wpot v al be (S f) l end.
856Fixpoint vsum (v : nat -> nat) (f m : nat) : nat :=
857 match m with 0 => 0 | S m => v f + vsum v (S f) m end.
859Definition Pot (v : nat -> nat) (al be ga Ps f : nat) (l : list nat) : nat :=
860 wpot v al be f l + ga * vsum v (f + length l) (Ps - (f + length l)).
862Definition mono (v : nat -> nat) : Prop := forall i j, i <= j -> v i <= v j.
864Lemma Pot_cons v al be ga Ps f e l :
865 Pot v al be ga Ps f (e :: l) = v f * (al * e + be) + Pot v al be ga Ps (S f) l.
866Proof. unfold Pot. cbn [wpot length]. replace (f + S (length l)) with (S f + length l) by lia. lia. Qed.
868Lemma wpot_app1 v al be f l x : wpot v al be f (l ++ [x]) = wpot v al be f l + v (f + length l) * (al * x + be).
869Proof.
870 revert f. induction l as [|e l IH]; intros f; cbn [wpot app length].
871 - rewrite !Nat.add_0_r. reflexivity.
872 - rewrite IH. replace (S f + length l) with (f + S (length l)) by lia. lia.
873Qed.
875Lemma wpot_bumpl v al be f l : mono v -> wpot v al be f (bumpl l) <= wpot v al be f l + al * v (f + length l).
876Proof.
877 intros Hv. revert f. induction l as [|e l IH]; intros f; [cbn; lia|].
878 destruct l as [|e' l].
879 - cbn [bumpl wpot length]. pose proof (Hv f (f + 1) ltac:(lia)). nia.
880 - change (bumpl (e :: e' :: l)) with (e :: bumpl (e' :: l)). cbn [wpot length].
881 specialize (IH (S f)). cbn [wpot length] in IH. replace (S f + S (length l)) with (f + S (S (length l))) in IH by lia.
882 lia.
883Qed.
885Lemma Pot_ov v al be ga Ps f l : mono v -> al + be + 1 <= ga -> f + length l + 1 <= Ps ->
886 Pot v al be ga Ps f (bumpl l ++ [0]) + v (f + length l) <= Pot v al be ga Ps f l.
887Proof.
888 intros Hv Hg HP. unfold Pot. rewrite wpot_app1, length_app, length_bumpl. cbn [length].
889 pose proof (wpot_bumpl v al be f l Hv) as B.
890 replace (Ps - (f + length l)) with (S (Ps - (f + (length l + 1)))) by lia.
891 cbn [vsum]. replace (S (f + length l)) with (f + (length l + 1)) by lia.
892 set (V := v (f + length l)) in *. set (R := vsum v (f + (length l + 1)) (Ps - (f + (length l + 1)))).
893 assert ((al + be + 1) * V <= ga * V) by (apply Nat.mul_le_mono_r; lia).
894 rewrite Nat.mul_0_r, Nat.add_0_l, Nat.mul_add_distr_l. rewrite !Nat.mul_add_distr_r in *. lia.
895Qed.
897Lemma Pot_inc v al be ga Ps Q0 f bs s p bs' s' d : mono v -> al + be + 1 <= ga -> Q0 < 2 ^ (Ps + 1) -> s <= 3 ->
898 ginc bs s = (bs', s', d) -> QI Q0 f bs s (S p) ->
899 Pot v al be ga Ps f (exs bs') + b2n d * v f <= Pot v al be ga Ps f (exs bs).
900Proof.
901 intros Hv Hg HP Hs E HQ.
902 pose proof (QI_inc _ _ _ _ _ _ _ _ Hs E HQ) as HQ'. apply (QI_Ps _ Ps) in HQ'; [|exact HP].
903 destruct (ginc_exps bs s Hs _ _ _ E) as [[E1 E2] | [E1 E2]]; subst.
904 - rewrite E1. cbn. lia.
905 - rewrite E1. assert (length bs' = S (length bs)) as L
906 by (rewrite <- !length_exs, E1, length_app, length_bumpl; cbn; lia).
907 pose proof (Pot_ov v al be ga Ps f (exs bs) Hv Hg) as O. rewrite length_exs in O.
908 specialize (O ltac:(lia)). destruct bs; cbn [b2n] in *; [rewrite Nat.add_0_r in O; lia | lia].
909Qed.
911(* The epoch map consumes positions from the front; the potential pays for each one. *)
912Lemma GPhi_pot v al be ga Ps Q0 : mono v -> al + be + 1 <= ga -> 1 <= al -> 2 <= be -> Q0 < 2 ^ (Ps + 1) ->
913 forall a b bs s r, GPhi a b bs s r -> s <= 3 -> forall f U, QI Q0 f bs s (b - 1) ->
914 (forall q, f <= q -> U <= v q) ->
915 match r with
916 | RE2 k x bs2 s2 => exists h, QI Q0 (f + S h) bs2 s2 0 /\
917 U * k + Pot v al be ga Ps (f + S h) (exs bs2) + v (f + h) * (al * x + be) <=
918 Pot v al be ga Ps f (exs bs) + U * (a + b - 1) + al * v (f + h)
919 | RSp k y => U * k <= Pot v al be ga Ps f (exs bs) + U * (a + b)
203end.920 end.
206Definition tm1 := Eval compute in (TM_from_str "1LB0LF_1LC0LE_1RD1LB_1RA0RD_1LA---_0LA0RB").
207Lemma nonhalt1: ~halts tm1 c0.
208Proof.921Proof.
209 solve_cert (cert1 B D [1] [0] [0;1] [1;0;1] [0;0]).
922 intros Hv Hg Ha Hb HP.
923 induction 1 as [a b bs s bs' s' d r E H IH | a e bs s r H IH | a e bs s bs' s' d E | a | a | a | a r H IH];
924 intros Hs f U HQ HU.
925 - (* bounce *)
926 replace (S (S b) - 1) with (S b) in HQ by lia.
927 pose proof (Pot_inc v al be ga Ps Q0 f bs s b bs' s' d Hv Hg HP Hs E HQ) as PI.
928 pose proof (QI_inc _ _ _ _ _ _ _ _ Hs E HQ) as HQ'.
929 specialize (IH (ginc_s3 _ _ _ _ _ Hs E) f U).
930 rewrite addb_b2n in IH. replace (S b + b2n d - 1) with (b + b2n d) in IH by lia.
931 specialize (IH HQ' HU). pose proof (HU f (le_n _)) as Uf.
932 destruct r as [k x bs2 s2 | k y].
933 + destruct IH as (h & H1 & H2). exists h. split; [exact H1|].
934 assert (U * b2n d <= b2n d * v f) by (destruct d; cbn; lia). nia.
935 + assert (U * b2n d <= b2n d * v f) by (destruct d; cbn; lia). nia.
936 - (* E1g *)
937 pose proof (QI_cons _ _ _ _ _ _ e HQ (le_S _ _ (le_n _))) as HQ'.
938 specialize (IH Hs (S f) U). replace (S e - 1) with e in IH by lia. specialize (IH HQ').
939 specialize (IH (fun q Hq => HU q ltac:(lia))). pose proof (HU f (le_n _)) as Uf.
940 change (exs ((false, e) :: bs)) with (e :: exs bs). rewrite Pot_cons.
941 assert (U * (e + 2) <= v f * (al * e + be)).
942 { apply (Nat.le_trans _ (v f * (e + 2))); [apply Nat.mul_le_mono_r; exact Uf|].
943 apply Nat.mul_le_mono_l. assert (e <= al * e) by nia. lia. }
944 destruct r as [k x bs2 s2 | k y].
945 + destruct IH as (h & H1 & H2). exists (S h).
946 replace (f + S (S h)) with (S f + S h) by lia. replace (f + S h) with (S f + h) by lia.
947 split; [exact H1|].
948 replace (S (S a) + S e - 1) with (a + (e + 2)) in H2 by lia. rewrite (Nat.mul_add_distr_l U a (e + 2)) in H2.
949 replace (a + 1 - 1) with a by lia. lia.
950 + replace (S (S a) + S e) with ((a + 1) + (e + 2)) in IH by lia. rewrite (Nat.mul_add_distr_l U (a + 1) (e + 2)) in IH. lia.
951 - (* E2g *)
952 exists 0. pose proof (QI_cons _ _ _ _ _ _ 1 HQ ltac:(lia)) as HQ1.
953 pose proof (QI_inc _ _ _ _ _ _ _ _ Hs E HQ1) as HQ2.
954 pose proof (Pot_inc v al be ga Ps Q0 (S f) bs s 0 bs' s' d Hv Hg HP Hs E HQ1) as PI.
955 replace (f + 1) with (S f) by lia. rewrite Nat.add_0_r.
956 split; [eapply QI_drop; exact HQ2|].
957 change (exs ((true, e) :: bs)) with (e :: exs bs). rewrite Pot_cons, addb_b2n.
958 assert (v f * (al * (e + b2n d) + be) <= v f * (al * e + be) + al * v f) by (destruct d; cbn; nia).
959 replace (a + 1 - 1) with a by lia. lia.
960 - nia.
961 - nia.
962 - nia.
963 - (* Et3 *)
964 pose proof (QI_et3 _ _ HQ) as HQ'.
965 pose proof (QI_Ps _ Ps _ _ _ _ HQ' HP) as HPs. cbn [length] in HPs.
966 pose proof (Pot_ov v al be ga Ps f [] Hv Hg ltac:(cbn; lia)) as O. cbn [bumpl app length] in O.
967 rewrite Nat.add_0_r in O.
968 specialize (IH ltac:(lia) f U HQ' HU). pose proof (HU f (le_n _)) as Uf.
969 destruct r as [k x bs2 s2 | k y].
970 + destruct IH as (h & H1 & H2). exists h. split; [exact H1|]. cbn [exs map snd] in *.
971 replace (S a + 1 - 1) with (a + 1) in H2 by lia. rewrite (Nat.mul_add_distr_l U a 1) in H2.
972 replace (a + 1 - 1) with a by lia. lia.
973 + cbn [exs map snd] in *. replace (S a + 1) with (a + 1 + 1) in IH by lia.
974 rewrite (Nat.mul_add_distr_l U (a + 1) 1) in IH. lia.
210Qed.975Qed.
213Definition tm2 := Eval compute in (TM_from_str "1RB0LF_1LC---_1RE0LD_0LC1LF_0RE1RA_0LA0RC").
977(* ===================================================================== *)
214Lemma nonhalt2: ~halts tm2 c0.
978(* Section 9. Digestion bounds: cost, merged exponents, length; existence. *)
979(* ===================================================================== *)
981Definition w (q : nat) : nat := 2 ^ ((q + 1) / 2).
983Lemma w_mono : mono w.
984Proof. intros i j H. unfold w. apply Nat.pow_le_mono_r; [lia|]. apply Nat.Div0.div_le_mono; lia. Qed.
986Lemma w_lev l q : 2 * l <= q -> 2 ^ l <= w q.
215Proof.987Proof.
216 solve_cert (cert1 D A [0;1] [1;0] [0;1] [1;0;1] [0;0]).
988 intros H. unfold w. apply Nat.pow_le_mono_r; [lia|].
989 replace l with ((2 * l) / 2) at 1 by (rewrite Nat.mul_comm, Nat.div_mul; lia).
990 apply Nat.Div0.div_le_mono; lia.
217Qed.991Qed.
220Definition tm3 := Eval compute in (TM_from_str "1LB0LC_1RB1LC_0LA0RD_1RF1LE_1LD---_1RA0RF").
993Lemma w_lev1 l q : 2 * l + 1 <= q -> 2 ^ S l <= w q.
221Lemma nonhalt3: ~halts tm3 c0.
222Proof.994Proof.
223 solve_cert (cert1 D A [1;1;0] [1;0;0] [1;0] [1;1;0] [0;0]).
995 intros H. unfold w. apply Nat.pow_le_mono_r; [lia|].
996 replace (S l) with ((2 * S l) / 2) at 1 by (rewrite Nat.mul_comm, Nat.div_mul; lia).
997 apply Nat.Div0.div_le_mono; lia.
224Qed.998Qed.
227Definition tm4 := Eval compute in (TM_from_str "1LB0LE_1LC1LE_1RD1LB_1RA0RD_0LA0RF_1RD---").
1000Lemma GPhi_QI Q0 Ps a b bs s k x bs2 s2 f : Q0 < 2 ^ (Ps + 1) -> GPhi a b bs s (RE2 k x bs2 s2) -> s <= 3 ->
228Lemma nonhalt4: ~halts tm4 c0.
1001 QI Q0 f bs s (b - 1) -> exists h, QI Q0 (f + S h) bs2 s2 0.
229Proof.1002Proof.
230 solve_cert (cert1 C A [1;1;0] [1;0;0] [1;0] [1;1;0] [0;0]).
1003 intros HP HG Hs HQ.
1004 pose proof (GPhi_pot (fun _ => 0) 1 2 4 Ps Q0 ltac:(intros ? ? ?; lia) ltac:(lia) ltac:(lia) ltac:(lia) HP
1005 _ _ _ _ _ HG Hs f 0 HQ ltac:(intros; lia)) as G.
1006 destruct G as (h & G & _). eauto.
231Qed.1007Qed.
234Definition tm5 := Eval compute in (TM_from_str "1LB0LE_1LC1LE_1RD0LF_1RA0RD_0LA0RC_0RA---").
1009Lemma Dig_cost Q0 Ps : Q0 < 2 ^ (Ps + 1) ->
235Lemma nonhalt5: ~halts tm5 c0.
1010 (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
1011 2 ^ l * n <= Pot w 2 8 11 Ps f (exs bs) + 2 ^ l * (2 * x + 2) + 13 * w Ps) /\
1012 (forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
1013 2 ^ l * n <= Pot w 2 8 11 Ps f (exs bs) + 13 * w Ps).
236Proof.1014Proof.
237 solve_cert (cert1 C A [1;1;0] [1;0;0] [1;0] [1;1;0] [0;0]).
1015 intros HP. apply Dig_mind.
1016 - intros x bs s n c bsp sp H IH Hs l f Hl HQ. specialize (IH Hs l f Hl HQ).
1017 rewrite Nat.mul_add_distr_l. lia.
1018 - intros e bs s bs' s' d n c bsp sp E H IH Hs l f Hl HQ.
1019 pose proof (QI_cons _ _ _ _ _ _ 1 HQ ltac:(lia)) as HQ1.
1020 pose proof (QI_inc _ _ _ _ _ _ _ _ Hs E HQ1) as HQ2. apply QI_drop in HQ2.
1021 specialize (IH (ginc_s3 _ _ _ _ _ Hs E) l (S f) ltac:(lia) HQ2).
1022 pose proof (Pot_inc w 2 8 11 Ps Q0 (S f) bs s 0 bs' s' d w_mono ltac:(lia) HP Hs E HQ1) as PI.
1023 change (exs ((false, e) :: bs)) with (e :: exs bs). rewrite Pot_cons.
1024 pose proof (w_lev l f Hl) as Wf. set (L := 2 ^ l) in *.
1025 assert (E1 : L * S (S n) = L * n + 2 * L) by ring.
1026 assert (E2 : L * (2 * S (addb e d) + 2) + 2 * L <= w f * (2 * e + 8)).
1027 { rewrite addb_b2n. assert (L * (2 * S (e + b2n d) + 2) + 2 * L <= L * (2 * e + 8)) by (destruct d; cbn [b2n]; nia).
1028 assert (L * (2 * e + 8) <= w f * (2 * e + 8)) by (apply Nat.mul_le_mono_r; exact Wf). lia. }
1029 lia.
1030 - intros e bs s k x bs2 s2 n c bsp sp HG H IH Hs l f Hl HQ.
1031 pose proof (QI_cons _ _ _ _ _ _ e HQ (le_S _ _ (le_n _))) as HQ1.
1032 pose proof (GPhi_pot w 2 8 11 Ps Q0 w_mono ltac:(lia) ltac:(lia) ltac:(lia) HP _ _ _ _ _ HG Hs (S f) 0) as G.
1033 replace (S e - 1) with e in G by lia. specialize (G HQ1 (fun _ _ => Nat.le_0_l _)).
1034 destruct G as (h & G1 & G2).
1035 pose proof (GPhi_s3 _ _ _ _ _ HG Hs) as Hs2. cbn in Hs2.
1036 specialize (IH Hs2 (S l) (S f + S h) ltac:(lia) G1).
1037 change (exs ((true, e) :: bs)) with (e :: exs bs). rewrite Pot_cons.
1038 pose proof (w_lev l f Hl) as Wf. pose proof (w_lev1 l (S f + h) ltac:(lia)) as Wh.
1039 rewrite Nat.pow_succ_r' in IH, Wh. set (L := 2 ^ l) in *. set (W' := w (S f + h)) in *.
1040 assert (E1 : L * S (2 * n) = L + 2 * L * n) by ring.
1041 assert (E2 : 2 * L * (2 * x + 2) <= W' * (2 * x + 2)) by (apply Nat.mul_le_mono_r; exact Wh).
1042 assert (E3 : W' * (2 * x + 8) = W' * (2 * x + 2) + 6 * W') by ring.
1043 assert (E4 : L <= w f * (2 * e + 8)) by nia.
1044 rewrite Nat.mul_0_l in G2. lia.
1045 - intros e bs s k y n c bsp sp HG H Hs l f Hl HQ.
1046 destruct (DigE_props _ _ _ _ _ H) as (Hn & _).
1047 pose proof (QI_Ps _ Ps _ _ _ _ HQ HP) as HPs. cbn [length] in HPs.
1048 change (exs ((true, e) :: bs)) with (e :: exs bs). rewrite Pot_cons.
1049 pose proof (w_lev l f Hl) as Wf. pose proof (w_lev1 l Ps ltac:(lia)) as Wh.
1050 rewrite Nat.pow_succ_r' in Wh. set (L := 2 ^ l) in *.
1051 assert (E1 : L * S (2 * n) = L + 2 * L * n) by ring.
1052 assert (E2 : 2 * L * n <= 13 * w Ps) by nia.
1053 assert (E4 : L <= w f * (2 * e + 8)) by nia.
1054 lia.
1055 - intros s n c bsp sp H Hs l f Hl HQ.
1056 destruct (DigE_props _ _ _ _ _ H) as (Hn & _).
1057 pose proof (QI_Ps _ Ps _ _ _ _ HQ HP) as HPs. cbn [length] in HPs.
1058 pose proof (w_lev l Ps ltac:(lia)) as Wf. nia.
238Qed.1059Qed.
241Definition tm6 := Eval compute in (TM_from_str "1LB0LE_1LC1LE_1RD1LF_1RA0RD_0LA0RC_1LC---").
1061Fixpoint MO (u : nat -> nat) (l : nat) (es : list nat) : nat :=
242Lemma nonhalt6: ~halts tm6 c0.
1062 match es with [] => 0 | e :: es => u l * e + MO u (S l) es end.
1064Definition pu (u : nat -> nat) (l : nat) : nat := match l with 0 => 0 | S l' => u l' end.
1066Lemma pu_le u l : mono u -> pu u l <= u l.
1067Proof. intros Hu. destruct l; cbn; [lia | apply Hu; lia]. Qed.
1069Lemma MO_zero u l es : Forall (fun e => e = 0) es -> MO u l es = 0.
1070Proof. intros H. revert l. induction H as [|e es He H IH]; intros l; cbn; [reflexivity|]. rewrite IH, He. lia. Qed.
1072(* The merged blocks (write-up D.3): any level weights u that the position weights v dominate. *)
1073Lemma Dig_mass u v Q0 Ps : mono v -> mono u -> (forall l q, 2 * l <= q -> u l <= v q) -> Q0 < 2 ^ (Ps + 1) ->
1074 (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
1075 pu u l * c + MO u l (exs bsp) <= Pot v 1 3 5 Ps f (exs bs) + pu u l * S x + 6 * v Ps) /\
1076 (forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
1077 pu u l * c + MO u l (exs bsp) <= Pot v 1 3 5 Ps f (exs bs) + 6 * v Ps).
243Proof.1078Proof.
244 solve_cert (cert1 C A [1;1;0] [1;0;0] [1;0] [1;1;0] [0;0]).
1079 intros Hv Hu Huv HP. apply Dig_mind.
1080 - intros x bs s n c bsp sp H IH Hs l f Hl HQ. specialize (IH Hs l f Hl HQ).
1081 rewrite Nat.mul_add_distr_l. lia.
1082 - intros e bs s bs' s' d n c bsp sp E H IH Hs l f Hl HQ.
1083 pose proof (QI_cons _ _ _ _ _ _ 1 HQ ltac:(lia)) as HQ1.
1084 pose proof (QI_inc _ _ _ _ _ _ _ _ Hs E HQ1) as HQ2. apply QI_drop in HQ2.
1085 specialize (IH (ginc_s3 _ _ _ _ _ Hs E) l (S f) ltac:(lia) HQ2).
1086 pose proof (Pot_inc v 1 3 5 Ps Q0 (S f) bs s 0 bs' s' d Hv ltac:(lia) HP Hs E HQ1) as PI.
1087 change (exs ((false, e) :: bs)) with (e :: exs bs). rewrite Pot_cons.
1088 pose proof (Nat.le_trans _ _ _ (pu_le u l Hu) (Huv l f Hl)) as Pf.
1089 assert (pu u l * S (S (addb e d)) <= v f * (1 * e + 3)).
1090 { rewrite addb_b2n. apply Nat.mul_le_mono; [exact Pf | destruct d; cbn; lia]. }
1091 lia.
1092 - intros e bs s k x bs2 s2 n c bsp sp HG H IH Hs l f Hl HQ.
1093 pose proof (QI_cons _ _ _ _ _ _ e HQ (le_S _ _ (le_n _))) as HQ1.
1094 pose proof (GPhi_pot v 1 3 5 Ps Q0 Hv ltac:(lia) ltac:(lia) ltac:(lia) HP _ _ _ _ _ HG Hs (S f) (u l)) as G.
1095 replace (S e - 1) with e in G by lia. specialize (G HQ1 (fun q Hq => Huv l q ltac:(lia))).
1096 destruct G as (h & G1 & G2).
1097 pose proof (GPhi_s3 _ _ _ _ _ HG Hs) as Hs2. cbn in Hs2.
1098 specialize (IH Hs2 (S l) (S f + S h) ltac:(lia) G1). cbn [pu] in IH.
1099 change (exs ((true, e) :: bs)) with (e :: exs bs). rewrite Pot_cons.
1100 change (exs ((false, k + c) :: bsp)) with ((k + c) :: exs bsp). cbn [MO].
1101 pose proof (Huv l f Hl) as Uf. pose proof (Huv l (S f + h) ltac:(lia)) as Uh.
1102 set (U := u l) in *. set (V' := v (S f + h)) in *.
1103 assert (E1 : U * S x <= V' * (x + 2)) by (apply Nat.mul_le_mono; lia).
1104 assert (E2 : V' * (1 * x + 3) = V' * (x + 2) + V') by ring.
1105 assert (E3 : U * (1 + S e - 1) <= v f * (1 * e + 3)) by (apply Nat.mul_le_mono; lia).
1106 assert (E4 : U * (k + c) = U * k + U * c) by ring.
1107 rewrite Nat.mul_0_r. lia.
1108 - intros e bs s k y n c bsp sp HG H Hs l f Hl HQ.
1109 destruct (DigE_props _ _ _ _ _ H) as (_ & Hc & _ & _ & Hz).
1110 pose proof (QI_cons _ _ _ _ _ _ e HQ (le_S _ _ (le_n _))) as HQ1.
1111 pose proof (GPhi_pot v 1 3 5 Ps Q0 Hv ltac:(lia) ltac:(lia) ltac:(lia) HP _ _ _ _ _ HG Hs (S f) (u l)) as G.
1112 replace (S e - 1) with e in G by lia. specialize (G HQ1 (fun q Hq => Huv l q ltac:(lia))). cbn beta iota in G.
1113 pose proof (QI_Ps _ Ps _ _ _ _ HQ HP) as HPs. cbn [length] in HPs.
1114 change (exs ((true, e) :: bs)) with (e :: exs bs). rewrite Pot_cons.
1115 change (exs ((false, k + c) :: bsp)) with ((k + c) :: exs bsp). cbn [MO]. rewrite (MO_zero _ _ _ Hz).
1116 pose proof (Huv l f Hl) as Uf. pose proof (Huv l Ps ltac:(lia)) as Up.
1117 set (U := u l) in *.
1118 assert (E3 : U * (1 + S e) <= v f * (1 * e + 3)) by (apply Nat.mul_le_mono; lia).
1119 assert (E4 : U * (k + c) = U * k + U * c) by ring.
1120 assert (E5 : U * c <= 6 * v Ps) by nia.
1121 rewrite Nat.mul_0_r. lia.
1122 - intros s n c bsp sp H Hs l f Hl HQ.
1123 destruct (DigE_props _ _ _ _ _ H) as (_ & Hc & _ & _ & Hz). rewrite (MO_zero _ _ _ Hz).
1124 pose proof (QI_Ps _ Ps _ _ _ _ HQ HP) as HPs. cbn [length] in HPs.
1125 pose proof (Nat.le_trans _ _ _ (pu_le u l Hu) (Huv l Ps ltac:(lia))) as Pf. nia.
245Qed.1126Qed.
248Definition tm7 := Eval compute in (TM_from_str "1LB0LF_0RC1LF_1RE1LD_1LC---_1RA0RE_0LA0RC").
1128Lemma Dig_len Q0 Ps : Q0 < 2 ^ (Ps + 1) ->
249Lemma nonhalt7: ~halts tm7 c0.
1129 (forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
1130 2 * (l + length bsp) <= Ps + 3) /\
1131 (forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
1132 2 * (l + length bsp) <= Ps + 3).
250Proof.1133Proof.
251 solve_cert (cert1 C A [1;1;0] [1;0;0] [1;0] [1;1;0] [0;0]).
1134 intros HP. apply Dig_mind.
1135 - intros x bs s n c bsp sp H IH Hs l f Hl HQ. exact (IH Hs l f Hl HQ).
1136 - intros e bs s bs' s' d n c bsp sp E H IH Hs l f Hl HQ.
1137 pose proof (QI_cons _ _ _ _ _ _ 1 HQ ltac:(lia)) as HQ1.
1138 pose proof (QI_inc _ _ _ _ _ _ _ _ Hs E HQ1) as HQ2. apply QI_drop in HQ2.
1139 exact (IH (ginc_s3 _ _ _ _ _ Hs E) l (S f) ltac:(lia) HQ2).
1140 - intros e bs s k x bs2 s2 n c bsp sp HG H IH Hs l f Hl HQ.
1141 pose proof (QI_cons _ _ _ _ _ _ e HQ (le_S _ _ (le_n _))) as HQ1.
1142 destruct (GPhi_QI Q0 Ps _ _ _ _ _ _ _ _ (S f) HP HG Hs ltac:(replace (S e - 1) with e by lia; exact HQ1)) as (h & G1).
1143 pose proof (GPhi_s3 _ _ _ _ _ HG Hs) as Hs2. cbn in Hs2.
1144 specialize (IH Hs2 (S l) (S f + S h) ltac:(lia) G1). cbn [length]. lia.
1145 - intros e bs s k y n c bsp sp HG H Hs l f Hl HQ.
1146 destruct (DigE_props _ _ _ _ _ H) as (_ & _ & Hb & _).
1147 pose proof (QI_Ps _ Ps _ _ _ _ HQ HP) as HPs. cbn [length] in *. lia.
1148 - intros s n c bsp sp H Hs l f Hl HQ.
1149 destruct (DigE_props _ _ _ _ _ H) as (_ & _ & Hb & _).
1150 pose proof (QI_Ps _ Ps _ _ _ _ HQ HP) as HPs. cbn [length] in *. lia.
252Qed.1151Qed.
255Definition tm8 := Eval compute in (TM_from_str "1LB0LF_0LC1LF_1RD0LB_0RD0RE_1RA---_0LA0RC").
1153Lemma pow_gt_self n : n < 2 ^ (n + 1).
256Lemma nonhalt8: ~halts tm8 c0.
1154Proof. induction n as [|n IH]; cbn; [lia|]. rewrite Nat.add_0_r. lia. Qed.
1156Lemma DigE_ex y : y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2) -> exists n c bsp sp, DigE y n c bsp sp.
1157Proof. intros [-> | [-> | ->]]; do 4 eexists; constructor. Qed.
1159(* Every residue 11 (001)^x 000 W with W a counter word has a digestion. *)
1160Lemma DigT_exists Q0 : forall D f bs s, s <= 3 -> QI Q0 f bs s 0 -> Q0 + 1 - 2 ^ f <= D ->
1161 exists n c bsp sp, DigT bs s n c bsp sp.
257Proof.1162Proof.
258 solve_cert (cert1 C A [0;1;0] [1;0;0] [1;0] [1;1;0] [0;0]).
1163 induction D as [D IHD] using lt_wf_ind. intros f bs s Hs HQ HD.
1164 pose proof (pow_gt_self Q0) as HP.
1165 destruct bs as [|[[|] e] bs].
1166 - destruct s as [|[|[|[|s]]]]; try lia; do 4 eexists; apply DTt; constructor.
1167 - destruct (gcount (Psi bs s (S e)) bs s 1 (S e) Hs ltac:(lia) (le_n _)) as (r & HG).
1168 pose proof (QI_cons _ _ _ _ _ _ e HQ (le_S _ _ (le_n _))) as HQ1.
1169 pose proof (GPhi_s3 _ _ _ _ _ HG Hs) as Hr.
1170 destruct r as [k x bs2 s2 | k y].
1171 + destruct (GPhi_QI Q0 Q0 _ _ _ _ _ _ _ _ (S f) HP HG Hs ltac:(replace (S e - 1) with e by lia; exact HQ1)) as (h & G1).
1172 pose proof (QI_low _ _ _ _ _ G1) as L1. rewrite Nat.pow_add_r in L1.
1173 assert (2 ^ f < 2 ^ (S f + S h)) by (apply Nat.pow_lt_mono_r; lia).
1174 assert (1 <= 2 ^ length bs2) by (apply Nat.neq_0_lt_0, Nat.pow_nonzero; lia).
1175 assert (2 ^ (S f + S h) <= Q0) by nia.
1176 destruct (IHD (Q0 + 1 - 2 ^ (S f + S h)) ltac:(lia) (S f + S h) bs2 s2 Hr G1 (le_n _)) as (n & c & bsp & sp & HT).
1177 do 4 eexists. eapply DTb; [exact HG | apply DP; exact HT].
1178 + destruct (DigE_ex y Hr) as (n & c & bsp & sp & HE).
1179 do 4 eexists. eapply DTs; [exact HG | exact HE].
1180 - destruct (ginc bs s) as [[bs' s'] d] eqn:E.
1181 pose proof (QI_cons _ _ _ _ _ _ 1 HQ ltac:(lia)) as HQ1.
1182 pose proof (QI_inc _ _ _ _ _ _ _ _ Hs E HQ1) as HQ2. apply QI_drop in HQ2.
1183 pose proof (QI_low _ _ _ _ _ HQ2) as L1. rewrite Nat.pow_add_r in L1.
1184 assert (2 ^ f < 2 ^ S f) by (apply Nat.pow_lt_mono_r; lia).
1185 assert (1 <= 2 ^ length bs') by (apply Nat.neq_0_lt_0, Nat.pow_nonzero; lia).
1186 assert (2 ^ S f <= Q0) by nia.
1187 destruct (IHD (Q0 + 1 - 2 ^ S f) ltac:(lia) (S f) bs' s' (ginc_s3 _ _ _ _ _ Hs E) HQ2 (le_n _))
1188 as (n & c & bsp & sp & HT).
1189 do 4 eexists. eapply DTa; [exact E | apply DP; exact HT].
259Qed.1190Qed.
262Definition tm9 := Eval compute in (TM_from_str "1LB0LF_1LC1LE_1RD1LB_1RA0RD_0LA---_0LA0RC").
1192(* ---------- the counting phase: exponents and value ---------- *)
263Lemma nonhalt9: ~halts tm9 c0.
1194Definition Rel (orig cur : list nat) : Prop :=
1195 (forall i, S i < length cur -> nth i cur 0 <= nth i orig 0 + 1) /\
1196 (forall i, length cur <= S i -> nth i cur 0 <= nth i orig 0).
1198Lemma nth_bumpl l i : nth i (bumpl l) 0 = nth i l 0 + (if Nat.eqb (S i) (length l) then 1 else 0).
264Proof.1199Proof.
265 solve_cert (cert1 C A [1;1;0] [1;0;0] [1;0] [1;1;0] [0;0]).
1200 revert i. induction l as [|e l IH]; intros i; [destruct i; reflexivity|].
1201 destruct l as [|e' l].
1202 - destruct i as [|[|i]]; cbn; lia.
1203 - change (bumpl (e :: e' :: l)) with (e :: bumpl (e' :: l)).
1204 destruct i as [|i]; cbn [nth length]; [cbn; lia|]. rewrite IH. reflexivity.
266Qed.1205Qed.
269Definition tm10 := Eval compute in (TM_from_str "1LB0LF_1LC1LF_1RD1LB_---0RE_1RA0RE_0LA0RC").
1207Lemma nth_app0 l i : nth i (l ++ [0]) 0 = nth i l 0.
270Lemma nonhalt10: ~halts tm10 c0.
1208Proof. revert i. induction l as [|e l IH]; intros [|i]; cbn; auto. destruct i; reflexivity. Qed.
1210Lemma Rel_ov orig l : Rel orig l -> Rel orig (bumpl l ++ [0]).
271Proof.1211Proof.
272 solve_cert (cert1 C A [1;1;0] [1;0;0] [1;0] [1;1;0] [0;0]).
1212 intros [R1 R2]. unfold Rel. rewrite length_app, length_bumpl. cbn [length]. split; intros i Hi; rewrite nth_app0, nth_bumpl.
1213 - destruct (Nat.eqb_spec (S i) (length l)).
1214 + specialize (R2 i ltac:(lia)). lia.
1215 + destruct (Nat.lt_ge_cases (S i) (length l)) as [H|H]; [specialize (R1 i H); lia|].
1216 rewrite nth_overflow by lia. lia.
1217 - destruct (Nat.eqb_spec (S i) (length l)); [lia|]. rewrite nth_overflow by lia. lia.
273Qed.1218Qed.
276Definition tm11 := Eval compute in (TM_from_str "1LB1LF_1RC1LA_0RD0RC_1RE---_0LA0LF_0LE0RB").
1220Lemma Rel_inc orig bs s bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> Rel orig (exs bs) -> Rel orig (exs bs').
277Lemma nonhalt11: ~halts tm11 c0.
278Proof.1221Proof.
279 solve_cert (cert1 B E [1;0;0] [1;0;0] [1;0] [1;0;0] [0;0]).
1222 intros Hs E R. destruct (ginc_exps bs s Hs _ _ _ E) as [[E1 _] | [E1 _]]; rewrite E1; [exact R|].
1223 apply Rel_ov, R.
280Qed.1224Qed.
1226Lemma Rel_tl orig cur : Rel orig cur -> Rel (tl orig) (tl cur).
1227Proof.
1228 intros [R1 R2]. split; intros i Hi.
1229 - destruct cur as [|c cur]; cbn in Hi; [lia|]. specialize (R1 (S i) ltac:(cbn; lia)).
1230 destruct orig as [|o orig]; destruct i; cbn in *; lia.
1231 - destruct cur as [|c cur]; [destruct i; cbn; lia|]. cbn [length tl] in Hi |- *.
1232 specialize (R2 (S i) ltac:(cbn; lia)).
1233 destruct orig as [|o orig]; destruct i; cbn in *; lia.
1234Qed.
1236Lemma Rel_refl l : Rel l l.
1237Proof. split; intros; lia. Qed.
1239Lemma GPhi_rel a b bs s r : GPhi a b bs s r -> s <= 3 -> forall orig, Rel orig (exs bs) ->
1240 match r with
1241 | RE2 k x bs2 s2 => exists h, Rel (skipn (S h) orig) (exs bs2) /\ x <= nth h orig 0 + 1
1242 | RSp _ _ => True
1243 end.
1244Proof.
1245 induction 1 as [a b bs s bs' s' d r E H IH | a e bs s r H IH | a e bs s bs' s' d E | a | a | a | a r H IH];
1246 intros Hs orig R; auto.
1247 - apply IH; [eapply ginc_s3; eauto | eapply Rel_inc; eauto].
1248 - specialize (IH Hs (tl orig) (Rel_tl _ _ R)). destruct r as [k x bs2 s2|]; [|exact I].
1249 destruct IH as (h & R1 & R2). exists (S h). split.
1250 + destruct orig; [destruct h|]; exact R1.
1251 + destruct orig; cbn in *; [destruct h|]; auto.
1252 - exists 0. split.
1253 + apply (Rel_inc _ bs s bs' s' d Hs E). exact (Rel_tl _ _ R).
1254 + destruct R as [R1 R2]. destruct (ginc_exps bs s Hs _ _ _ E) as [[_ ->] | [_ Ed]].
1255 * cbn [addb]. destruct bs as [|b bs].
1256 -- specialize (R2 0 ltac:(cbn; lia)). cbn in R2. lia.
1257 -- specialize (R1 0 ltac:(cbn; lia)). cbn in R1. lia.
1258 * destruct bs as [|b bs]; subst d; cbn [addb].
1259 -- specialize (R2 0 ltac:(cbn; lia)). cbn in R2. lia.
1260 -- specialize (R1 0 ltac:(cbn; lia)). cbn in R1. lia.
1261 - apply IH; [lia|]. destruct R as [R1 R2]. split; intros i Hi; cbn in Hi; [lia|].
1262 destruct i as [|[|i]]; cbn; apply Nat.le_0_l.
1263Qed.
1265Lemma GPhi_val a b bs s r : GPhi a b bs s r -> s <= 3 ->
1266 match r with RE2 k x bs2 s2 => 2 * gval bs2 s2 + a <= gval bs s + k + 2 | RSp _ _ => True end.
1267Proof.
1268 induction 1 as [a b bs s bs' s' d r E H IH | a e bs s r H IH | a e bs s bs' s' d E | a | a | a | a r H IH];
1269 intros Hs; auto.
1270 - destruct (ginc_val bs s Hs _ _ _ E) as (V & S1 & _). specialize (IH S1). destruct r; [rewrite V in IH; lia | exact I].
1271 - specialize (IH Hs). destruct r; [cbn [gval]; lia | exact I].
1272 - destruct (ginc_val bs s Hs _ _ _ E) as (V & _). cbn [gval]. rewrite V. lia.
1273 - specialize (IH ltac:(lia)). destruct r; [cbn [gval] in *; lia | exact I].
1274Qed.
1276(* ===================================================================== *)
1277(* Section 10. Weights, masses, the threshold, the orbit invariant. *)
1278(* ===================================================================== *)
1280Definition v2 (q : nat) : nat := 2 ^ (q / 2).
1281Definition p2 (q : nat) : nat := 2 ^ S q.
1282Definition cst1 (q : nat) : nat := 1.
1283Definition u1 (l : nat) : nat := match l with 0 => 0 | S l' => 2 * w l' end.
1284Definition u2 (l : nat) : nat := match l with 0 => 0 | S l' => 2 ^ S l' end.
1286Lemma v2_mono : mono v2.
1287Proof. intros i j H. unfold v2. apply Nat.pow_le_mono_r; [lia|]. apply Nat.Div0.div_le_mono; lia. Qed.
1288Lemma p2_mono : mono p2.
1289Proof. intros i j H. unfold p2. apply Nat.pow_le_mono_r; lia. Qed.
1290Lemma cst1_mono : mono cst1.
1291Proof. intros i j H. unfold cst1. lia. Qed.
1292Lemma v2_le_w q : v2 q <= w q.
1293Proof. unfold v2, w. apply Nat.pow_le_mono_r; [lia|]. apply Nat.Div0.div_le_mono; lia. Qed.
1294Lemma cst1_le_w q : cst1 q <= w q.
1295Proof. unfold cst1, w. apply Nat.neq_0_lt_0, Nat.pow_nonzero. lia. Qed.
1297Lemma u1_mono : mono u1.
1298Proof. intros [|i] [|j] H; cbn [u1]; try lia. pose proof (w_mono i j ltac:(lia)). lia. Qed.
1299Lemma u1_w l q : 2 * l <= q -> u1 l <= w q.
1300Proof.
1301 destruct l as [|l]; intros H; cbn [u1]; [lia|].
1302 pose proof (w_lev1 l q ltac:(lia)) as W. unfold w at 1.
1303 rewrite <- Nat.pow_succ_r'.
1304 apply (Nat.le_trans _ (2 ^ S l)); [|exact W].
1305 apply Nat.pow_le_mono_r; [lia|].
1306 destruct l as [|l]; [cbn; lia|].
1307 assert ((S l + 1) / 2 <= (2 * S l) / 2) by (apply Nat.Div0.div_le_mono; lia).
1308 rewrite (Nat.mul_comm 2 (S l)), Nat.div_mul in H0 by lia. lia.
1309Qed.
1310Lemma u2_mono : mono u2.
1311Proof. intros [|i] [|j] H; cbn [u2]; try lia. apply Nat.pow_le_mono_r; lia. Qed.
1312Lemma u2_v2 l q : 2 * l <= q -> u2 l <= v2 q.
1313Proof.
1314 destruct l as [|l]; intros H; cbn [u2]; [lia|]. unfold v2. apply Nat.pow_le_mono_r; [lia|].
1315 replace (S l) with ((2 * S l) / 2) at 1 by (rewrite Nat.mul_comm, Nat.div_mul; lia).
1316 apply Nat.Div0.div_le_mono; lia.
1317Qed.
1319Lemma MO_u1 l es : MO u1 (S l) es = 2 * wpot w 1 0 l es.
1320Proof. revert l. induction es as [|e es IH]; intros l; cbn [MO wpot]; [reflexivity|]. rewrite IH. cbn [u1]. lia. Qed.
1321Lemma MO_u1_0 es : MO u1 0 es = 2 * wpot w 1 0 0 (tl es).
1322Proof. destruct es as [|e es]; cbn [MO tl]; [reflexivity|]. rewrite MO_u1. cbn [u1]. lia. Qed.
1323Lemma MO_u2 l es : MO u2 (S l) es = wpot p2 1 0 l es.
1324Proof. revert l. induction es as [|e es IH]; intros l; cbn [MO wpot]; [reflexivity|]. rewrite IH. cbn [u2]. unfold p2. lia. Qed.
1325Lemma MO_u2_0 es : MO u2 0 es = wpot p2 1 0 0 (tl es).
1326Proof. destruct es as [|e es]; cbn [MO tl]; [reflexivity|]. rewrite MO_u2. cbn [u2]. lia. Qed.
1327Lemma nth_le_MO h es : forall l, nth h es 0 <= MO cst1 l es.
1328Proof.
1329 revert h. induction es as [|e es IH]; intros h l; [destruct h; cbn; lia|].
1330 destruct h as [|h]; cbn [nth MO]; unfold cst1 at 1; [lia|]. specialize (IH h (S l)). lia.
1331Qed.
1333Lemma wpot_shift v al be f f' l : mono v -> f <= f' -> wpot v al be f l <= wpot v al be f' l.
1334Proof.
1335 intros Hv. revert f f'. induction l as [|e l IH]; intros f f' H; cbn [wpot]; [lia|].
1336 pose proof (Hv f f' H). specialize (IH (S f) (S f') ltac:(lia)).
1337 assert (v f * (al * e + be) <= v f' * (al * e + be)) by (apply Nat.mul_le_mono_r; lia). lia.
1338Qed.
1339Lemma wpot_drop v al be f h l : wpot v al be (f + h) (skipn h l) <= wpot v al be f l.
1340Proof.
1341 revert f l. induction h as [|h IH]; intros f l; [rewrite Nat.add_0_r; reflexivity|].
1342 destruct l as [|e l]; cbn [skipn wpot]; [lia|]. specialize (IH (S f) l).
1343 replace (f + S h) with (S f + h) by lia. lia.
1344Qed.
1345Lemma wpot_skipn_tl v h l : mono v -> wpot v 1 0 0 (skipn (S h) l) <= wpot v 1 0 0 (tl l).
1346Proof.
1347 intros Hv. replace (skipn (S h) l) with (skipn h (tl l)) by (destruct l; [destruct h|]; reflexivity).
1348 apply (Nat.le_trans _ (wpot v 1 0 (0 + h) (skipn h (tl l)))); [apply wpot_shift; [exact Hv | lia]|].
1349 apply wpot_drop.
1350Qed.
1351Lemma wpot_le_nth v l1 : mono v -> forall l2 f, (forall i, nth i l1 0 <= nth i l2 0 + 1) ->
1352 wpot v 1 0 f l1 <= wpot v 1 0 f l2 + vsum v f (length l1).
1353Proof.
1354 intros Hv. induction l1 as [|e1 l1 IH]; intros l2 f H; cbn [wpot length vsum]; [lia|].
1355 destruct l2 as [|e2 l2].
1356 - assert (H' : forall i, nth i l1 0 <= nth i [] 0 + 1) by (intros i; specialize (H (S i)); destruct i; cbn in *; lia).
1357 specialize (IH [] (S f) H'). cbn [wpot] in IH |- *.
1358 pose proof (H 0) as H0. cbn in H0. assert (v f * (1 * e1 + 0) <= v f) by nia. lia.
1359 - specialize (IH l2 (S f) (fun i => H (S i))). cbn [wpot].
1360 pose proof (H 0) as H0. cbn in H0. assert (v f * (1 * e1 + 0) <= v f * (1 * e2 + 0) + v f) by nia. lia.
1361Qed.
1362Lemma Rel_nth orig cur : Rel orig cur -> forall i, nth i cur 0 <= nth i orig 0 + 1.
1363Proof. intros [R1 R2] i. destruct (Nat.lt_ge_cases (S i) (length cur)); [apply R1 | specialize (R2 i)]; lia. Qed.
1364Lemma wpot_split v al be f l : wpot v al be f l = wpot v al 0 f l + be * vsum v f (length l).
1365Proof. revert f. induction l as [|e l IH]; intros f; cbn [wpot vsum length]; [lia|]. rewrite IH. ring. Qed.
1366Lemma wpot_scale2 v f l : wpot v 2 0 f l = 2 * wpot v 1 0 f l.
1367Proof. revert f. induction l as [|e l IH]; intros f; cbn [wpot]; [lia|]. rewrite IH. ring. Qed.
1368Lemma wpot_le_v v v' al be f l : (forall q, v q <= v' q) -> wpot v al be f l <= wpot v' al be f l.
1369Proof.
1370 intros H. revert f. induction l as [|e l IH]; intros f; cbn [wpot]; [lia|].
1371 specialize (IH (S f)). assert (v f * (al * e + be) <= v' f * (al * e + be)) by (apply Nat.mul_le_mono_r, H). lia.
1372Qed.
1373Lemma vsum_add v f m m' : vsum v f (m + m') = vsum v f m + vsum v (f + m) m'.
1374Proof. revert f. induction m as [|m IH]; intros f; cbn [vsum Nat.add]; [rewrite Nat.add_0_r; lia|]. rewrite IH. replace (S f + m) with (f + S m) by lia. lia. Qed.
1375Lemma vsum_mono_m v f m m' : m <= m' -> vsum v f m <= vsum v f m'.
1376Proof. intros H. replace m' with (m + (m' - m)) by lia. rewrite vsum_add. lia. Qed.
1377Lemma vsum_cst1 f m : vsum cst1 f m = m.
1378Proof. revert f. induction m as [|m IH]; intros f; cbn; [reflexivity|]. rewrite IH. unfold cst1. lia. Qed.
1379Lemma vsum_p2 f m : vsum p2 f m + 2 ^ S f = 2 ^ S (f + m).
1380Proof.
1381 revert f. induction m as [|m IH]; intros f; cbn [vsum]; [rewrite Nat.add_0_r; lia|].
1382 specialize (IH (S f)). replace (f + S m) with (S f + m) by lia. unfold p2 in *. rewrite (Nat.pow_succ_r' 2 (S f)) in IH. lia.
1383Qed.
1384Lemma wpot_p2_S f l : wpot p2 1 0 (S f) l = 2 * wpot p2 1 0 f l.
1385Proof. revert f. induction l as [|e l IH]; intros f; cbn [wpot]; [lia|]. rewrite IH. unfold p2. rewrite (Nat.pow_succ_r' 2 (S f)). ring. Qed.
1386Lemma qsum_p2 l : 2 * qsum l + 2 = 2 ^ S (length l) + wpot p2 1 0 0 l.
1387Proof.
1388 induction l as [|e l IH]; cbn [qsum length wpot]; [cbn; lia|]. rewrite wpot_p2_S.
1389 change (p2 0) with 2. rewrite (Nat.pow_succ_r' 2 (S (length l))). lia.
1390Qed.
1391Lemma wpot_zero v f l : Forall (fun e => e = 0) l -> wpot v 1 0 f l = 0.
1392Proof. intros H. revert f. induction H as [|e l He H IH]; intros f; cbn; [reflexivity|]. rewrite IH, He. lia. Qed.
1393Lemma Pot_top v al be ga Ps l : be <= ga -> length l <= Ps ->
1394 Pot v al be ga Ps 0 l <= wpot v al 0 0 l + ga * vsum v 0 Ps.
1395Proof.
1396 intros Hb Hl. unfold Pot. rewrite wpot_split. cbn [Nat.add].
1397 pose proof (vsum_add v 0 (length l) (Ps - length l)) as E. replace (length l + (Ps - length l)) with Ps in E by lia.
1398 cbn [Nat.add] in E. rewrite E.
1399 assert (be * vsum v 0 (length l) <= ga * vsum v 0 (length l)) by (apply Nat.mul_le_mono_r; lia).
1400 rewrite Nat.mul_add_distr_l. lia.
1401Qed.
1403(* ---------- the bound functions (all nondecreasing in kappa) ---------- *)
1405Definition Ws (P : nat) : nat := vsum w 0 P.
1406Definition V2s (P : nat) : nat := vsum v2 0 P.
1407Definition Pf (k : nat) : nat := Nat.max 12 (k + 3).
1408Definition Af (k : nat) : nat := 5 * Ws (Pf k) + 6 * w (Pf k) + 2 * Ws k.
1409Definition Bf (k : nat) : nat := Af k + 5 * V2s (Pf k) + 6 * v2 (Pf k) + 2 ^ (k + 1).
1410Definition Xf (k : nat) : nat := Af k + 5 * Pf k + 7.
1411Definition Costf (k : nat) : nat := 2 * Xf k + 2 + 2 * Af k + 11 * Ws (Pf k) + 13 * w (Pf k).
1412Definition Nlo (k : nat) : nat := 2 ^ (k + 3) - 8 * 2 ^ ((Pf k + 3) / 2).
1413Definition Nstar : nat := 17705.
1415Lemma Pf_mono k k' : k <= k' -> Pf k <= Pf k'.
1416Proof. unfold Pf. lia. Qed.
1417Lemma Ws_mono P P' : P <= P' -> Ws P <= Ws P'.
1418Proof. apply vsum_mono_m. Qed.
1419Lemma V2s_mono P P' : P <= P' -> V2s P <= V2s P'.
1420Proof. apply vsum_mono_m. Qed.
1421Lemma Af_mono k k' : k <= k' -> Af k <= Af k'.
1422Proof.
1423 intros H. unfold Af. pose proof (Pf_mono _ _ H).
1424 pose proof (Ws_mono _ _ H0). pose proof (w_mono _ _ H0). pose proof (Ws_mono _ _ H). lia.
1425Qed.
1427Lemma w_SS q : w (S (S q)) = 2 * w q.
1428Proof.
1429 unfold w. replace (S (S q) + 1) with ((q + 1) + 1 * 2) by lia. rewrite Nat.div_add by lia.
1430 rewrite Nat.pow_add_r. cbn. lia.
1431Qed.
1432Lemma v2_SS q : v2 (S (S q)) = 2 * v2 q.
1433Proof.
1434 unfold v2. replace (S (S q)) with (q + 1 * 2) by lia. rewrite Nat.div_add by lia.
1435 rewrite Nat.pow_add_r. cbn. lia.
1436Qed.
1437Lemma vsum_SS_w f m : vsum w (S (S f)) m = 2 * vsum w f m.
1438Proof. revert f. induction m as [|m IH]; intros f; cbn [vsum]; [lia|]. rewrite w_SS, IH. lia. Qed.
1439Lemma vsum_SS_v2 f m : vsum v2 (S (S f)) m = 2 * vsum v2 f m.
1440Proof. revert f. induction m as [|m IH]; intros f; cbn [vsum]; [lia|]. rewrite v2_SS, IH. lia. Qed.
1441Lemma Ws_SS P : Ws (S (S P)) = 2 * Ws P + 3.
1442Proof. unfold Ws. cbn [vsum]. rewrite vsum_SS_w. cbn. lia. Qed.
1443Lemma V2s_SS P : V2s (S (S P)) = 2 * V2s P + 2.
1444Proof. unfold V2s. cbn [vsum]. rewrite vsum_SS_v2. cbn. lia. Qed.
1445Lemma Pf_big k : 9 <= k -> Pf k = k + 3.
1446Proof. unfold Pf. lia. Qed.
1447Lemma Af_SS k : 9 <= k -> Af (S (S k)) = 2 * Af k + 21.
1448Proof.
1449 intros H. unfold Af. rewrite !Pf_big by lia.
1450 replace (S (S k) + 3) with (S (S (k + 3))) by lia. rewrite !Ws_SS, w_SS. lia.
1451Qed.
1453Definition gB (k : nat) : nat := Af k + 5 * V2s (k + 3) + 6 * v2 (k + 3).
1454Lemma gB_SS k : 9 <= k -> gB (S (S k)) = 2 * gB k + 31.
1455Proof.
1456 intros H. unfold gB. rewrite Af_SS by lia.
1457 replace (S (S k) + 3) with (S (S (k + 3))) by lia. rewrite V2s_SS, v2_SS. lia.
1458Qed.
1460Lemma gB_all m : gB (10 + 2 * m) + 31 < 7 * 2 ^ (10 + 2 * m) /\ gB (11 + 2 * m) + 31 < 7 * 2 ^ (11 + 2 * m).
1461Proof.
1462 induction m as [|m [IH1 IH2]].
1463 - split; apply Nat.ltb_lt; vm_compute; reflexivity.
1464 - replace (10 + 2 * S m) with (S (S (10 + 2 * m))) by lia.
1465 replace (11 + 2 * S m) with (S (S (11 + 2 * m))) by lia.
1466 rewrite !gB_SS by lia. rewrite !(Nat.pow_succ_r' 2 (S _)), !Nat.pow_succ_r'. lia.
1467Qed.
1469Lemma gB_ge k : 10 <= k -> gB k + 31 < 7 * 2 ^ k.
1470Proof.
1471 intros H. destruct (Nat.Even_or_Odd (k - 10)) as [[m Hm] | [m Hm]].
1472 - replace k with (10 + 2 * m) by lia. exact (proj1 (gB_all m)).
1473 - replace k with (11 + 2 * m) by lia. exact (proj2 (gB_all m)).
1474Qed.
1476(* (N1) the Q potential fits below 2^(Pf+1): created positions stay below Pf. *)
1477Lemma N1 k : 7 * 2 ^ k + Bf k < 2 ^ (Pf k + 1).
1478Proof.
1479 destruct (le_lt_dec k 11) as [Hk|Hk].
1480 - assert (H : forallb (fun k => 7 * 2 ^ k + Bf k <? 2 ^ (Pf k + 1)) (seq 0 12) = true) by (vm_compute; reflexivity).
1481 rewrite forallb_forall in H. specialize (H k (proj2 (in_seq 12 0 k) ltac:(lia))). apply Nat.ltb_lt, H.
1482 - pose proof (gB_ge k ltac:(lia)) as G. unfold Bf. fold (gB k) in *.
1483 unfold gB in G. rewrite Pf_big in * by lia. unfold gB in *.
1484 replace (k + 3 + 1) with (k + 4) by lia. rewrite (Nat.pow_add_r 2 k 4), (Nat.pow_add_r 2 k 1).
1485 cbn [Nat.pow]. lia.
1486Qed.
1488Lemma Costf_SS k : 9 <= k -> Costf (S (S k)) + 10 * (k + 3) = 2 * Costf k + 121.
1489Proof.
1490 intros H. unfold Costf, Xf. rewrite Af_SS by lia. rewrite !Pf_big by lia.
1491 replace (S (S k) + 3) with (S (S (k + 3))) by lia. rewrite Ws_SS, w_SS. generalize (Af k) (Ws (k + 3)) (w (k + 3)). intros. lia.
1492Qed.
1494Lemma Nlo_SS k : 9 <= k -> Nlo (S (S k)) = 4 * 2 ^ (k + 3) - 16 * 2 ^ ((k + 6) / 2) /\
1495 Nlo k = 2 ^ (k + 3) - 8 * 2 ^ ((k + 6) / 2).
1496Proof.
1497 intros H. unfold Nlo. rewrite !Pf_big by lia. split.
1498 - replace ((S (S k) + 3 + 3) / 2) with ((k + 6) / 2 + 1)
1499 by (replace (S (S k) + 3 + 3) with ((k + 6) + 1 * 2) by lia; rewrite Nat.div_add by lia; lia).
1500 replace (S (S k) + 3) with (k + 3 + 2) by lia.
1501 rewrite (Nat.pow_add_r 2 (k + 3) 2), (Nat.pow_add_r 2 ((k + 6) / 2) 1).
1502 generalize (2 ^ (k + 3)) (2 ^ ((k + 6) / 2)). intros. cbn. lia.
1503 - replace (k + 3 + 3) with (k + 6) by lia. reflexivity.
1504Qed.
1506Lemma D_all m : Costf (12 + 2 * m) + 123 <= Nlo (12 + 2 * m) /\ Costf (13 + 2 * m) + 123 <= Nlo (13 + 2 * m).
1507Proof.
1508 induction m as [|m [IH1 IH2]].
1509 - split; apply Nat.leb_le; vm_compute; reflexivity.
1510 - replace (12 + 2 * S m) with (S (S (12 + 2 * m))) by lia.
1511 replace (13 + 2 * S m) with (S (S (13 + 2 * m))) by lia.
1512 pose proof (Costf_SS (12 + 2 * m) ltac:(lia)). pose proof (Costf_SS (13 + 2 * m) ltac:(lia)).
1513 destruct (Nlo_SS (12 + 2 * m) ltac:(lia)) as [E1 E2]. destruct (Nlo_SS (13 + 2 * m) ltac:(lia)) as [E3 E4].
1514 rewrite E1, E3. rewrite E2 in IH1. rewrite E4 in IH2. lia.
1515Qed.
1517(* (N2) the digestion cost fits in the budget: below N* for kappa <= 11, below Nlo above. *)
1518Lemma N2 k : Costf k + 2 <= Nstar \/ Costf k + 2 <= Nlo k.
1519Proof.
1520 destruct (le_lt_dec k 11) as [Hk|Hk].
1521 - left. assert (H : forallb (fun k => Costf k + 2 <=? Nstar) (seq 0 12) = true) by (vm_compute; reflexivity).
1522 rewrite forallb_forall in H. specialize (H k (proj2 (in_seq 12 0 k) ltac:(lia))). apply Nat.leb_le, H.
1523 - right. destruct (Nat.Even_or_Odd (k - 12)) as [[m Hm] | [m Hm]].
1524 + replace k with (12 + 2 * m) by lia. pose proof (proj1 (D_all m)). lia.
1525 + replace k with (13 + 2 * m) by lia. pose proof (proj2 (D_all m)). lia.
1526Qed.
1528(* ===================================================================== *)
1529(* Section 11. The orbit invariant, one epoch, the finite part, nonhalt. *)
1530(* ===================================================================== *)
1532Lemma Nstar_ge : 15 <= Nstar.
1533Proof. apply Nat.leb_le. vm_compute. reflexivity. Qed.
1535Ltac opq t := let x := fresh "o" in set (x := t) in *; clearbody x.
1537Definition Mw (bs : blks) : nat := wpot w 1 0 0 (exs bs).
1538Definition M2 (bs : blks) : nat := wpot p2 1 0 0 (exs bs).
1540(* Inv k N y: epoch K(1,N,y), k bounds the number of blocks seen so far (write-up D.6). *)
1541Definition Inv (k N : nat) (y : word) : Prop :=
1542 Nstar <= N /\ Nlo k <= N /\
1543 ((exists x bs s, y = p11 x (gw bs s) /\ s <= 3 /\ length bs <= k /\
1544 Mw bs <= Af k /\ M2 bs <= Bf k /\ x <= Xf k)
1545 \/ y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2)).
1547Lemma next_inv k N n c bsp sp r :
1548 GPhi (1 + n) (N + c - n) bsp sp r -> sp <= 3 -> n + 2 <= N -> Nstar <= N -> Nlo k <= N ->
1549 MO u1 0 (exs bsp) <= Af k + 5 * Ws (Pf k) + 6 * w (Pf k) ->
1550 MO u2 0 (exs bsp) <= Af k + 5 * V2s (Pf k) + 6 * v2 (Pf k) ->
1551 MO cst1 0 (exs bsp) + 1 <= Xf k ->
1552 2 * length bsp <= Pf k + 3 ->
1553 exists k', Inv k' (S (rk r)) (ry r).
1554Proof.
1555 intros HG Hs Hn HN HL H1 H2 H3 H4.
1556 pose proof (GPhi_rk _ _ _ _ _ HG) as Hrk.
1557 pose proof (GPhi_s3 _ _ _ _ _ HG Hs) as Hr.
1558 pose proof (GPhi_rel _ _ _ _ _ HG Hs (exs bsp) (Rel_refl _)) as HR.
1559 pose proof (GPhi_val _ _ _ _ _ HG Hs) as HV.
1560 destruct r as [kk x bs2 s2 | kk y]; cbn [rk ry] in *.
1561 - destruct HR as (h & R1 & R2).
1562 exists (Nat.max k (length bs2)).
1563 assert (Hk : k <= Nat.max k (length bs2)) by lia.
1564 assert (Hk2 : length bs2 <= Nat.max k (length bs2)) by lia.
1565 set (k' := Nat.max k (length bs2)) in *.
1566 split; [lia|]. split.
1567 + destruct (le_lt_dec (length bs2) k) as [Hle|Hgt].
1568 * replace k' with k by lia. lia.
1569 * replace k' with (length bs2) by lia.
1570 pose proof (gval_lb bs2 s2). pose proof (gval_ub bsp sp Hs).
1571 assert (2 ^ length bsp <= 2 ^ ((Pf (length bs2) + 3) / 2)).
1572 { apply Nat.pow_le_mono_r; [lia|]. pose proof (Pf_mono k (length bs2) ltac:(lia)).
1573 apply Nat.div_le_lower_bound; lia. }
1574 unfold Nlo. rewrite Nat.pow_add_r.
1575 generalize dependent (2 ^ length bs2). generalize dependent (2 ^ length bsp).
1576 generalize dependent (2 ^ ((Pf (length bs2) + 3) / 2)). intros. cbn [Nat.pow] in *. lia.
1577 + left. exists x, bs2, s2. split; [reflexivity|]. split; [exact Hr|]. split; [lia|].
1578 pose proof (Pf_mono _ _ Hk) as HPf.
1579 split; [|split].
1580 * unfold Mw.
1581 pose proof (wpot_le_nth w (exs bs2) w_mono _ 0 (Rel_nth _ _ R1)) as A1. rewrite length_exs in A1.
1582 pose proof (wpot_skipn_tl w h (exs bsp) w_mono) as A2.
1583 rewrite MO_u1_0 in H1.
1584 pose proof (Ws_mono _ _ Hk2). pose proof (Ws_mono _ _ Hk). pose proof (Ws_mono _ _ HPf).
1585 pose proof (w_mono _ _ HPf).
1586 unfold Af in *. fold (Ws (length bs2)) in A1.
1587 generalize dependent (wpot w 1 0 0 (exs bs2)). generalize dependent (wpot w 1 0 0 (skipn (S h) (exs bsp))).
1588 generalize dependent (wpot w 1 0 0 (tl (exs bsp))). intros. lia.
1589 * unfold M2.
1590 pose proof (wpot_le_nth p2 (exs bs2) p2_mono _ 0 (Rel_nth _ _ R1)) as A1. rewrite length_exs in A1.
1591 pose proof (wpot_skipn_tl p2 h (exs bsp) p2_mono) as A2.
1592 rewrite MO_u2_0 in H2.
1593 pose proof (vsum_p2 0 (length bs2)) as A3. cbn [Nat.add] in A3.
1594 assert (2 ^ S (length bs2) <= 2 ^ (k' + 1)) by (apply Nat.pow_le_mono_r; lia).
1595 pose proof (Af_mono _ _ Hk). pose proof (V2s_mono _ _ HPf). pose proof (v2_mono _ _ HPf).
1596 unfold Bf.
1597 generalize dependent (wpot p2 1 0 0 (exs bs2)). generalize dependent (wpot p2 1 0 0 (skipn (S h) (exs bsp))).
1598 generalize dependent (wpot p2 1 0 0 (tl (exs bsp))). intros. lia.
1599 * pose proof (nth_le_MO h (exs bsp) 0).
1600 assert (Xf k <= Xf k') by (unfold Xf; pose proof (Af_mono _ _ Hk); lia). lia.
1601 - exists k. split; [lia|]. split; [lia|]. right. exact Hr.
1602Qed.
1604Lemma inv_step k N y : Inv k N y -> exists kk y', Phi 1 N y kk y' /\ exists k', Inv k' (S kk) y'.
1605Proof.
1606 intros (HN & HL & Hy).
1607 pose proof (N2 k) as HC.
1608 destruct Hy as [(x & bs & s & -> & Hs & Hk & HM & HM2 & Hx) | Hsp].
1609 - set (Ps := Pf k).
1610 set (Q0 := Qp 0 bs s 0 - 3 * 2 ^ length bs).
1611 assert (HQ0 : 4 * 2 ^ length bs <= Qp 0 bs s 0).
1612 { unfold Qp. rewrite Nat.pow_0_r. pose proof (gval_lb bs s). lia. }
1613 assert (HQ : QI Q0 0 bs s 0).
1614 { unfold QI, Q0. cbn [Nat.add]. clear - HQ0. lia. }
1615 assert (HP : Q0 < 2 ^ (Ps + 1)).
1616 { pose proof (N1 k) as N1k. unfold Q0, Qp. rewrite Nat.pow_0_r, Nat.mul_1_l.
1617 pose proof (qsum_p2 (exs bs)) as QP. rewrite length_exs in QP. pose proof (gval_ub bs s Hs).
1618 assert (2 ^ length bs <= 2 ^ k) by (apply Nat.pow_le_mono_r; lia). unfold M2 in HM2.
1619 rewrite Nat.pow_succ_r' in QP. fold Ps in N1k. lia. }
1620 destruct (DigT_exists Q0 (Q0 + 1) 0 bs s Hs HQ ltac:(lia)) as (n0 & c0 & bsp & sp & HT).
1621 pose proof (DP x _ _ _ _ _ _ HT) as HD.
1622 set (n := 2 * x + 2 + n0) in *. set (c := S x + c0) in *.
1623 pose proof (proj1 (Dig_cost Q0 Ps HP) _ _ _ _ _ _ _ HD Hs 0 0 (le_n _) HQ) as Hcost.
1624 rewrite Nat.pow_0_r, !Nat.mul_1_l in Hcost.
1625 pose proof (QI_Ps _ Ps _ _ _ _ HQ HP) as HPs. cbn [Nat.add] in HPs.
1626 assert (HPs' : length (exs bs) <= Ps) by (rewrite length_exs; exact HPs).
1627 pose proof (Pot_top w 2 8 11 Ps (exs bs) ltac:(lia) HPs') as PT. rewrite wpot_scale2 in PT.
1628 assert (Hn : n + 2 <= N).
1629 { unfold Costf in HC. fold Ps in HC. unfold Mw in HM. fold (Ws Ps) in PT.
1630 opq (w Ps). opq (Ws Ps). opq (Pot w 2 8 11 Ps 0 (exs bs)). opq (wpot w 1 0 0 (exs bs)). lia. }
1631 pose proof (proj1 Dig_sp _ _ _ _ _ _ _ HD) as Hsp.
1632 destruct (gcount (Psi bsp sp (N + c - n)) bsp sp (1 + n) (N + c - n) Hsp ltac:(lia) (le_n _)) as (r & HG).
1633 exists (rk r), (ry r). split; [exact (epoch_ord N x bs s n c bsp sp r Hs HD Hn HG)|].
1634 apply (next_inv k N n c bsp sp r HG Hsp Hn HN HL).
1635 + pose proof (proj1 (Dig_mass u1 w Q0 Ps w_mono u1_mono u1_w HP) _ _ _ _ _ _ _ HD Hs 0 0 (le_n _) HQ) as Hm.
1636 cbn [pu] in Hm. pose proof (Pot_top w 1 3 5 Ps (exs bs) ltac:(lia) HPs') as PT1.
1637 unfold Mw in HM. fold Ps. fold (Ws Ps) in PT1.
1638 opq (w Ps). opq (Ws Ps). opq (Pot w 1 3 5 Ps 0 (exs bs)). opq (wpot w 1 0 0 (exs bs)). opq (MO u1 0 (exs bsp)). lia.
1639 + pose proof (proj1 (Dig_mass u2 v2 Q0 Ps v2_mono u2_mono u2_v2 HP) _ _ _ _ _ _ _ HD Hs 0 0 (le_n _) HQ) as Hm.
1640 cbn [pu] in Hm. pose proof (Pot_top v2 1 3 5 Ps (exs bs) ltac:(lia) HPs') as PT1.
1641 pose proof (wpot_le_v v2 w 1 0 0 (exs bs) v2_le_w).
1642 unfold Mw in HM. fold Ps. fold (V2s Ps) in PT1.
1643 opq (v2 Ps). opq (V2s Ps). opq (Pot v2 1 3 5 Ps 0 (exs bs)). opq (wpot w 1 0 0 (exs bs)).
1644 opq (wpot v2 1 0 0 (exs bs)). opq (MO u2 0 (exs bsp)). lia.
1645 + pose proof (proj1 (Dig_mass cst1 cst1 Q0 Ps cst1_mono cst1_mono ltac:(intros; unfold cst1; lia) HP)
1646 _ _ _ _ _ _ _ HD Hs 0 0 (le_n _) HQ) as Hm.
1647 cbn [pu] in Hm. pose proof (Pot_top cst1 1 3 5 Ps (exs bs) ltac:(lia) HPs') as PT1.
1648 rewrite vsum_cst1 in PT1. pose proof (wpot_le_v cst1 w 1 0 0 (exs bs) cst1_le_w).
1649 unfold Mw in HM. unfold Xf. fold Ps. unfold cst1 at 3 in Hm.
1650 opq (Pot cst1 1 3 5 Ps 0 (exs bs)). opq (wpot w 1 0 0 (exs bs)). opq (wpot cst1 1 0 0 (exs bs)).
1651 opq (MO cst1 0 (exs bsp)). lia.
1652 + pose proof (proj1 (Dig_len Q0 Ps HP) _ _ _ _ _ _ _ HD Hs 0 0 (le_n _) HQ). fold Ps. lia.
1653 - destruct (DigE_ex y Hsp) as (n & c & bsp & sp & HE).
1654 destruct (DigE_props _ _ _ _ _ HE) as (Hn13 & Hc5 & Hb1 & Hs3 & Hz).
1655 assert (Hn : n + 2 <= N) by (pose proof Nstar_ge; lia).
1656 destruct (gcount (Psi bsp sp (N + c - n)) bsp sp (1 + n) (N + c - n) Hs3 ltac:(lia) (le_n _)) as (r & HG).
1657 exists (rk r), (ry r). split; [exact (epoch_spec N y n c bsp sp r HE Hn HG)|].
1658 apply (next_inv k N n c bsp sp r HG Hs3 Hn HN HL); rewrite ?(MO_zero _ _ _ Hz); unfold Xf, Pf; lia.
1659Qed.
1661(* ---------- the finite part: the computable model from K(1,8,t2) to epoch 694 ---------- *)
1663Fixpoint orbit (f n N : nat) (y : word) : option (nat * word) :=
1664 match n with
1665 | O => Some (N, y)
1666 | S n => match phif f 1 N y with Some (k, y') => orbit f n (S k) y' | None => None end
1667 end.
1669Lemma orbit_sound f n : forall N y N' y', orbit f n N y = Some (N', y') -> K N y -->* K N' y'.
1670Proof.
1671 induction n as [|n IH]; intros N y N' y' H; cbn [orbit] in H.
1672 - inversion H; subst. apply evstep_refl.
1673 - destruct (phif f 1 N y) as [[k y1]|] eqn:E; [|discriminate].
1674 eapply evstep_trans; [apply progress_evstep, epoch_tm, (proj2 (model_sound f) _ _ _ _ _ E) | exact (IH _ _ _ _ H)].
1675Qed.
1677Definition B694 : blks := [(false, 17); (true, 1); (true, 1); (true, 1); (true, 1);
1678 (false, 1); (false, 1); (false, 1); (true, 1); (false, 0)].
1679Definition Y694 : word := p11 7 (gw B694 0).
1681Lemma fin694 : orbit 100000 691 8 t2 = Some (17713, Y694).
1682Proof. vm_compute. reflexivity. Qed.
1684Lemma inv694 : Inv 10 17713 Y694.
1685Proof.
1686 unfold Inv. split; [apply Nat.leb_le; vm_compute; reflexivity|]. split; [apply Nat.leb_le; vm_compute; reflexivity|].
1687 left. exists 7, B694, 0. split; [reflexivity|]. split; [lia|]. split; [cbn; lia|].
1688 split; [|split]; [apply Nat.leb_le; vm_compute; reflexivity | apply Nat.leb_le; vm_compute; reflexivity |].
1689 apply Nat.leb_le; vm_compute; reflexivity.
1690Qed.
1692Lemma nonhalt_from N0 y0 (P : nat -> word -> Prop) :
1693 c0 -->* K N0 y0 -> P N0 y0 ->
1694 (forall N y, P N y -> exists k y', Phi 1 N y k y' /\ P (S k) y') ->
1695 ~ halts tm c0.
1696Proof.
1697 intros H0 HP0 Hstep.
1698 eapply multistep_nonhalt. { exact H0. }
1699 apply (progress_nonhalt_cond tm (nat * word) (N0, y0) (fun i => K (fst i) (snd i))
1700 (fun i => P (fst i) (snd i))); [| exact HP0].
1701 intros [N y] HP. cbn in HP.
1702 destruct (Hstep N y HP) as (k & y' & HPhi & HP').
1703 exists (S k, y'). split; [apply epoch_tm, HPhi | exact HP'].
1704Qed.
1706Lemma nonhalt: ~halts tm c0.
1707Proof.
1708 apply (nonhalt_from 17713 Y694 (fun N y => exists k, Inv k N y)).
1709 - eapply evstep_trans; [exact init | exact (orbit_sound _ _ _ _ _ _ fin694)].
1710 - exists 10. exact inv694.
1711 - intros N y [k Hk]. destruct (inv_step k N y Hk) as (kk & y' & H1 & H2). exists kk, y'. split; [exact H1 | exact H2].
1712Qed.
1714(*
1715 0 1
1716 A 1RB 0RF
1717 B 1RC 1RF
1718 C 1LD 0RE
1719 D --- 0LE
1720 E 1LA 0LE
1721 F 0RA 0LC
1723 hub K(a,b,X) = 0^inf (110)^a 0 (011)^b C> X 0^inf
1724 pre-record L'(k,T) = 0^inf E> 0 01 (001)^k T 0^inf (E0 = 1LA, then the restart)
1725 start c0 -->* K(1,8,010001)
1726*)
3Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.

219 items in 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v (1726 lines): 158 Lemma, 41 Definition, 12 Fixpoint, 7 Inductive, 1 Theorem. 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_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC").
L33new
2LemmaLP0
Lemma LP0 l r : l <* <[0;1;1] {{C}}> [0] *> r -->+ l <{{A}} [1;0;0;1] *> r.
L47new
3LemmaLP0z
Lemma LP0z l : l <* <[0;1;1] {{C}}> 0inf -->+ l <{{A}} [1;0;0;1] *> 0inf.
L50new
4LemmaLP11
Lemma LP11 l r : l <* <[0;1;1] {{C}}> [1;1;0] *> r -->+ l <{{A}} [1;0;1;0;0;0] *> r.
L54new
5LemmaLPCr
Lemma LPCr l e r : l <* <[0;1;1] {{C}}> [1;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <* <[0;1;1] {{C}}> r.
L58new
6LemmaLPCl0
Lemma LPCl0 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;0] *> r -->+
l <{{A}} [1;0;0;0;0;1] *> [0;0;1]^^e *> [0;0;0] *> r.
L63new
7LemmaLPCl1
Lemma LPCl1 l e r : l <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;1;0;0;0] *> r -->+
l <{{A}} [1;0;0;0;0;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.
L67new
8LemmaLP5r
Lemma LP5r l e r : l <* <[0;1;1] {{C}}> [1;0;0;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <* <[0;1;1] {{C}}> r.
L72new
9LemmaLP5l0
Lemma LP5l0 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{A}} [1;0;0] *> r -->+
l <{{A}} [1;0;0;0;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.
L76new
10LemmaLP5l1
Lemma LP5l1 l e r : l <* <[0;1;1;1;1] <* <[0;1;1]^^(S e) <{{A}} [1;0;1;0;0;0] *> r -->+
l <{{A}} [1;0;0;0;1] *> [0;0;1]^^(S (S e)) *> [0;0;0] *> r.
L80new
11LemmaLP6r
Lemma LP6r l e r : l <* <[0;1;1] {{C}}> [1;0;1;0;1] *> [0;0;1]^^e *> [0;0;0] *> r -->+
l <* <[0;1;1;1] <* <[1;1;0] <* [0] <* <[0;1;1]^^(S e) {{C}}> r.
L85new
12LemmaW10
Lemma W10 l r : l <* <[0;1;1;1] <{{E}} r -->+ l <{{A}} [1;0;0;0] *> r.
L90new
13LemmaRP0
Lemma RP0 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{A}} [1;0;0] *> r -->+
l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S n) {{C}}> r.
L94new
14LemmaRP1
Lemma RP1 l n r : l <* [0] <* <[0;1;1]^^(S n) <{{A}} [1;0;1;0;0;0] *> r -->+
l <* <[1;1;0] <* [0] <* <[0;1;1]^^(S (S n)) {{C}}> r.
L98new
15LemmaE1r
Lemma E1r l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [0;0;1]^^(S e) *> [0;0;0] *> r -->+
l <* <[1;1;0]^^(S (S a)) <* [0] <* <[0;1;1]^^(S e) {{C}}> r.
L103new
16LemmaE2l0
Lemma E2l0 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;0] *> r -->+
l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;1] *> [0;0;1]^^e *> [0;0;0] *> r.
L107new
17LemmaE2l1
Lemma E2l1 l a e r : l <* <[1;1;0]^^a <* [0] <* <[0;1;1;1;1;1] <* <[0;1;1]^^e <{{A}} [1;0;1;0;0;0] *> r -->+
l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;1] *> [0;0;1]^^(S e) *> [0;0;0] *> r.
L111new
18LemmaEt0
Lemma Et0 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> 0inf -->+
l <{{E}} [0;1] *> [0;0;1]^^(S a) *> [0;0;0;1] *> 0inf.
L115new
19LemmaEt1
Lemma Et1 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [1] *> 0inf -->+
l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.
L119new
20LemmaEt2
Lemma Et2 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [0;1;0;0;0;1] *> 0inf -->+
l <{{E}} [0;1] *> [0;0;1]^^a *> [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
L123new
21LemmaEt3
Lemma Et3 l a : l <* <[1;1;0]^^a <* [0] <* <[0;1;1] {{C}}> [1;1;0;0;0;1] *> 0inf -->+
l <* <[1;1;0]^^(S a) <* [0] <* <[0;1;1] {{C}}> [0;0;1] *> 0inf.
L127new
22LemmaRst
Lemma Rst k r : const 0 <{{E}} [0;1] *> [0;0;1]^^k *> [0;0;0] *> r -->+
const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^(S k) {{C}}> r.
L132new
23LemmaLPT1
Lemma LPT1 l : l <* <[0;1;1] {{C}}> [1] *> 0inf -->+ l <{{A}} [1;0;0;0;1;0;0;0;1] *> 0inf.
L137new
24LemmaLPT2
Lemma LPT2 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.
L140new
25LemmaLPT3
Lemma LPT3 l : l <* <[0;1;1] {{C}}> [1;0;1;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
L144new
26LemmaLPT4
Lemma LPT4 l : l <* <[0;1;1] {{C}}> [1;0;0;0;0;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;1;0;0;0;0;1;0;0;1;0;0;0;1] *> 0inf.
L148new
27LemmaLPT5
Lemma LPT5 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
L152new
28LemmaLPT6
Lemma LPT6 l : l <* <[0;1;1] {{C}}> [1;0;0;1;0;0;1;0;0;0;1] *> 0inf -->+
l <{{A}} [1;0;0] *> [0;1;0;0;1;0;0;1;0;0;0;1;0;0;0;0;1;0;0;0;1] *> 0inf.
L156new
29Lemmaz3
Lemma z3 : [0;0;0] *> const 0 = const 0.
L160new
30Inductiveword
Inductive word : Type :=
| t0 | t1 | t2 | t3
| blk (d : bool) (e : nat) (w : word)
| p11 (x : nat) (w : word)
| p01 (x : nat) (w : word)
| p00 (w : word)
… +1 lines
L169new
31Definitiondsym
Definition dsym (d : bool) : Sym := if d then S1 else S0.
L177new
32Fixpointenc
Fixpoint enc (w : word) : side :=
match w with
| t0 => const 0
| t1 => [1] *> const 0
| t2 => [0;1;0;0;0;1] *> const 0
| t3 => [1;1;0;0;0;1] *> const 0
… +6 lines
L179new
33Definitionaddb
Definition addb (e : nat) (d : bool) : nat := if d then S e else e.
L192new
34InductiveLP
Inductive LP : word -> word -> bool -> Prop :=
| LP_a e w : LP (blk false e w) (blk true e w) false
| LP_b e w w' d : LP w w' d -> LP (blk true e w) (blk false (addb e d) w') false
| LP_t0 : LP t0 t1 false
| LP_t1 : LP t1 t2 false
| LP_t2 : LP t2 t3 false
… +22 lines
L197new
35Definitionoutp
Definition outp (d : bool) (r : side) : side :=
if d then [1;0;1;0;0;0] *> r else [1;0;0] *> r.
L230new
36DefinitionLPspec
Definition LPspec (w w' : word) (d : bool) : Prop :=
forall l, l <* <[0;1;1] {{C}}> enc w -->+ l <{{A}} outp d (enc w').
L233new
37DefinitionPhispec
Definition Phispec (a b : nat) (w : word) (k : nat) (y : word) : Prop :=
forall l, l <* <[1;1;0]^^a <* [0] <* <[0;1;1]^^b {{C}}> enc w -->+
          l <{{E}} [0;1] *> [0;0;1]^^k *> [0;0;0] *> enc y.
L236new
38Lemmaenc_a0
Lemma enc_a0 : enc (blk false 0 t0) = [0;0;1] *> const 0.
L240new
39Theoremsound
Theorem sound :
(forall w w' d, LP w w' d -> LPspec w w' d) /\
(forall a b w k y, Phi a b w k y -> Phispec a b w k y).
L247new
40DefinitionK
Definition K (N : nat) (y : word) : Q * tape :=
const 0 <* <[1;1;0] <* [0] <* <[0;1;1]^^N {{C}}> enc y.
L315new
41Lemmaepoch_tm
Lemma epoch_tm N y k y' : Phi 1 N y k y' -> K N y -->+ K (S k) y'.
L318new
42Lemmainit
Lemma init : c0 -->* K 8 t2.
L326new
43Fixpointlpf
Fixpoint lpf (n : nat) (w : word) {struct n} : option (word * bool) :=
  match n with
  | O => None
  | S n' =>
    match w with
    | t0 => Some (t1, false)
… +58 lines
L333new
44Lemmaenc_p10t0
Lemma enc_p10t0 : enc (p10 t0) = enc t1.
L398new
45Lemmaenc_p10t1
Lemma enc_p10t1 : enc (p10 t1) = enc (blk true 0 t0).
L401new
46Lemmaenc_p00t0
Lemma enc_p00t0 : enc (p00 t0) = enc t0.
L404new
47Lemmaenc_p00t1
Lemma enc_p00t1 : enc (p00 t1) = enc (blk false 0 t0).
L407new
48Lemmaenc_p10p00t0
Lemma enc_p10p00t0 : enc (p10 (p00 t0)) = enc t1.
L410new
49Lemmaenc_p10p00t1
Lemma enc_p10p00t1 : enc (p10 (p00 t1)) = enc (p10 (blk false 0 t0)).
L413new
50Lemmamodel_sound
Lemma model_sound n :
(forall w w' d, lpf n w = Some (w', d) -> LP w w' d) /\
(forall a b w k y, phif n a b w = Some (k, y) -> Phi a b w k y).
L416new
51Definitiontl_of
Definition tl_of (s : nat) : word :=
match s with O => t0 | 1 => t1 | 2 => t2 | _ => t3 end.
L466new
52Fixpointgw
Fixpoint gw (bs : list (bool * nat)) (s : nat) : word :=
match bs with [] => tl_of s | (d, e) :: bs => blk d e (gw bs s) end.
L469new
53Fixpointginc
Fixpoint ginc (bs : list (bool * nat)) (s : nat) : list (bool * nat) * nat * bool :=
match bs with
| [] => match s with O => ([], 1, false) | 1 => ([], 2, false) | 2 => ([], 3, false)
        | _ => ([(false, 0)], O, true) end
| (false, e) :: bs => ((true, e) :: bs, s, false)
| (true, e) :: bs => let '(bs', s', d) := ginc bs s in ((false, addb e d) :: bs', s', false)
… +1 lines
L472new
54Fixpointgval
Fixpoint gval (bs : list (bool * nat)) (s : nat) : nat :=
match bs with [] => 4 + s | (d, _) :: bs => (if d then 1 else 0) + 2 * gval bs s end.
L480new
55Fixpointgsum
Fixpoint gsum (bs : list (bool * nat)) : nat :=
match bs with [] => O | (_, e) :: bs => e + gsum bs end.
L483new
56Lemmaginc_LP
Lemma ginc_LP bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) -> LP (gw bs s) (gw bs' s') d.
L486new
57Lemmaginc_val
Lemma ginc_val bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) ->
gval bs' s' = S (gval bs s) /\ s' <= 3 /\
gsum bs' + length bs + (if d then 1 else 0) = gsum bs + length bs' /\
(d = true -> bs = []) /\ length bs <= length bs'.
L494new
58Lemmagval_ge
Lemma gval_ge bs s : 4 <= gval bs s.
L507new
59Lemmagval_len
Lemma gval_len bs s : length bs <= gval bs s.
L510new
60DefinitionPsi
Definition Psi (bs : list (bool * nat)) (s b : nat) : nat := gval bs s + b + gsum bs - length bs.
L516new
61Definitionblks
Definition blks := list (bool * nat).
L524new
62Definitionb2n
Definition b2n (d : bool) : nat := if d then 1 else 0.
L525new
63Lemmaaddb_b2n
Lemma addb_b2n e d : addb e d = e + b2n d.
L526new
64InductiveGRes
Inductive GRes : Type := RE2 (k x : nat) (bs : blks) (s : nat) | RSp (k : nat) (y : word).
L529new
65Definitionrk
Definition rk (r : GRes) : nat := match r with RE2 k _ _ _ => k | RSp k _ => k end.
L530new
66Definitionry
Definition ry (r : GRes) : word := match r with RE2 _ x bs s => p11 x (gw bs s) | RSp _ y => y end.
L531new
67InductiveGPhi
Inductive GPhi : nat -> nat -> blks -> nat -> GRes -> Prop :=
| GB a b bs s bs' s' d r : ginc bs s = (bs', s', d) -> GPhi (S a) (addb (S b) d) bs' s' r ->
    GPhi a (S (S b)) bs s r
| GE1 a e bs s r : GPhi (S (S a)) (S e) bs s r -> GPhi a 1 ((false, e) :: bs) s r
| GE2 a e bs s bs' s' d : ginc bs s = (bs', s', d) ->
    GPhi a 1 ((true, e) :: bs) s (RE2 a (addb e d) bs' s')
… +4 lines
L534new
68Lemmaginc_s3
Lemma ginc_s3 bs s bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> s' <= 3.
L545new
69LemmaGPhi_sound
Lemma GPhi_sound a b bs s r : GPhi a b bs s r -> s <= 3 -> Phi a b (gw bs s) (rk r) (ry r).
L548new
70LemmaGPhi_s3
Lemma GPhi_s3 a b bs s r : GPhi a b bs s r -> s <= 3 ->
match r with RE2 _ _ _ s2 => s2 <= 3 | RSp _ y => y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2) end.
L560new
71LemmaGPhi_rk
Lemma GPhi_rk a b bs s r : GPhi a b bs s r -> a + b <= S (rk r).
L567new
72Lemmagcount
Lemma gcount : forall P bs s a b, s <= 3 -> 1 <= b -> Psi bs s b <= P -> exists r, GPhi a b bs s r.
L570new
73InductiveLPs
Inductive LPs : word -> word -> nat -> nat -> Prop :=
| LPs_eq w w' : enc w = enc w' -> LPs w w' 0 0
| LPs_step w w1 w2 d n c : LP w w1 d -> LPs w1 w2 n c -> LPs w w2 (S n) (c + b2n d).
L603new
74LemmaLPs_step'
Lemma LPs_step' w w1 w2 d n c c' : LP w w1 d -> LPs w1 w2 n c -> c' = c + b2n d -> LPs w w2 (S n) c'.
L607new
75LemmaLPs_eql
Lemma LPs_eql w0 w1 w2 n c : enc w0 = enc w1 -> LPs w1 w2 n c -> LPs w0 w2 n c.
L610new
76LemmaLPs_trans
Lemma LPs_trans w1 w2 w3 n c n' c' : LPs w1 w2 n c -> LPs w2 w3 n' c' -> LPs w1 w3 (n + n') (c + c').
L617new
77LemmaLPs_cn
Lemma LPs_cn w w' n c : LPs w w' n c -> c <= n.
L624new
78LemmaLPs_hub
Lemma LPs_hub w w' n c : LPs w w' n c -> forall a B k y, n + 2 <= B + c ->
Phi (a + n) (B + c - n) w' k y -> Phi a B w k y.
L627new
79LemmaLPs_nest
Lemma LPs_nest y y' n c : LPs y y' n c -> forall k, LPs (blk false k y) (blk false (k + c) y') (2 * n) 0.
L641new
80InductiveDigE
Inductive DigE : word -> nat -> nat -> blks -> nat -> Prop :=
| DE0 : DigE (p10 t0) 0 0 [] 1
| DE1 : DigE (p10 t1) 0 0 [(true, 0)] 0
| DE2 : DigE (p10 t2) 13 5 [(false, 0)] 2
| DE3 : DigE (p10 t3) 7 2 [(false, 0)] 2
| DEs0 : DigE t1 0 0 [] 1
… +2 lines
L651new
81LemmaDigE_sound
Lemma DigE_sound y n c bs s : DigE y n c bs s -> LPs y (gw bs s) n c.
L663new
82LemmaDigE_props
Lemma DigE_props y n c bs s : DigE y n c bs s ->
n <= 13 /\ c <= 5 /\ length bs <= 1 /\ s <= 3 /\ Forall (fun e => e = 0) (map snd bs).
L666new
83InductiveDigP
Inductive DigP : nat -> blks -> nat -> nat -> nat -> blks -> nat -> Prop :=
| DP x bs s n c bsp sp : DigT bs s n c bsp sp -> DigP x bs s (2 * x + 2 + n) (S x + c) bsp sp
with DigT : blks -> nat -> nat -> nat -> blks -> nat -> Prop :=
| DTa e bs s bs' s' d n c bsp sp : ginc bs s = (bs', s', d) ->
    DigP (S (addb e d)) bs' s' n c bsp sp -> DigT ((false, e) :: bs) s (S (S n)) c bsp sp
| DTb e bs s k x bs2 s2 n c bsp sp : GPhi 1 (S e) bs s (RE2 k x bs2 s2) ->
… +4 lines
L673new
84Lemmaprefix_LPs
Lemma prefix_LPs x w : LPs (p11 x w) (p10 w) (2 * x + 2) (S x).
L688new
85LemmaDig_sound
Lemma Dig_sound :
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> LPs (p11 x (gw bs s)) (gw bsp sp) n c) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> LPs (p10 (gw bs s)) (gw bsp sp) n c).
L696new
86LemmaDig_sp
Lemma Dig_sp :
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> sp <= 3) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> sp <= 3).
L716new
87Lemmaepoch_ord
Lemma epoch_ord N x bs s n c bsp sp r : s <= 3 -> DigP x bs s n c bsp sp -> n + 2 <= N ->
GPhi (1 + n) (N + c - n) bsp sp r -> Phi 1 N (p11 x (gw bs s)) (rk r) (ry r).
L724new
88Lemmaepoch_spec
Lemma epoch_spec N y n c bsp sp r : DigE y n c bsp sp -> n + 2 <= N ->
GPhi (1 + n) (N + c - n) bsp sp r -> Phi 1 N y (rk r) (ry r).
L732new
89Definitionexs
Definition exs (bs : blks) : list nat := map snd bs.
L744new
90Fixpointbumpl
Fixpoint bumpl (l : list nat) : list nat :=
match l with [] => [] | e :: l' => match l' with [] => [S e] | _ => e :: bumpl l' end end.
L746new
91Lemmalength_bumpl
Lemma length_bumpl l : length (bumpl l) = length l.
L749new
92Lemmalength_exs
Lemma length_exs bs : length (exs bs) = length bs.
L752new
93Lemmaginc_exps
Lemma ginc_exps bs s : s <= 3 -> forall bs' s' d, ginc bs s = (bs', s', d) ->
(exs bs' = exs bs /\ d = false) \/
(exs bs' = bumpl (exs bs) ++ [0] /\ d = match bs with [] => true | _ => false end).
L756new
94Fixpointqsum
Fixpoint qsum (l : list nat) : nat := match l with [] => 0 | e :: l => S e + 2 * qsum l end.
L771new
95DefinitionQp
Definition Qp (f : nat) (bs : blks) (s p : nat) : nat := 2 ^ f * (gval bs s + 2 * qsum (exs bs) + p).
L772new
96DefinitionQI
Definition QI (Q0 f : nat) (bs : blks) (s p : nat) : Prop := Qp f bs s p <= Q0 + 3 * 2 ^ (f + length bs).
L773new
97Lemmaqsum_app0
Lemma qsum_app0 l : qsum (l ++ [0]) = qsum l + 2 ^ length l.
L775new
98Lemmaqsum_bumpl
Lemma qsum_bumpl l : l <> [] -> 2 * qsum (bumpl l) = 2 * qsum l + 2 ^ length l.
L778new
99Lemmagval_lb
Lemma gval_lb bs s : 4 * 2 ^ length bs <= gval bs s.
L786new
100Lemmagval_ub
Lemma gval_ub bs s : s <= 3 -> gval bs s < 8 * 2 ^ length bs.
L789new
101LemmaQI_low
Lemma QI_low Q0 f bs s p : QI Q0 f bs s p -> 2 ^ (f + length bs) <= Q0.
L792new
102LemmaQI_Ps
Lemma QI_Ps Q0 Ps f bs s p : QI Q0 f bs s p -> Q0 < 2 ^ (Ps + 1) -> f + length bs <= Ps.
L799new
103LemmaQI_drop
Lemma QI_drop Q0 f bs s p : QI Q0 f bs s p -> QI Q0 f bs s 0.
L805new
104LemmaQI_cons
Lemma QI_cons Q0 f dd e bs s p : QI Q0 f ((dd, e) :: bs) s 0 -> p <= S e -> QI Q0 (S f) bs s p.
L808new
105LemmaQI_inc
Lemma QI_inc Q0 f bs s p bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) ->
QI Q0 f bs s (S p) -> QI Q0 f bs' s' (p + b2n d).
L821new
106LemmaQI_et3
Lemma QI_et3 Q0 f : QI Q0 f [] 3 0 -> QI Q0 f [(false, 0)] 0 0.
L848new
107Fixpointwpot
Fixpoint wpot (v : nat -> nat) (al be f : nat) (l : list nat) : nat :=
match l with [] => 0 | e :: l => v f * (al * e + be) + wpot v al be (S f) l end.
L853new
108Fixpointvsum
Fixpoint vsum (v : nat -> nat) (f m : nat) : nat :=
match m with 0 => 0 | S m => v f + vsum v (S f) m end.
L856new
109DefinitionPot
Definition Pot (v : nat -> nat) (al be ga Ps f : nat) (l : list nat) : nat :=
wpot v al be f l + ga * vsum v (f + length l) (Ps - (f + length l)).
L859new
110Definitionmono
Definition mono (v : nat -> nat) : Prop := forall i j, i <= j -> v i <= v j.
L862new
111LemmaPot_cons
Lemma Pot_cons v al be ga Ps f e l :
Pot v al be ga Ps f (e :: l) = v f * (al * e + be) + Pot v al be ga Ps (S f) l.
L864new
112Lemmawpot_app1
Lemma wpot_app1 v al be f l x : wpot v al be f (l ++ [x]) = wpot v al be f l + v (f + length l) * (al * x + be).
L868new
113Lemmawpot_bumpl
Lemma wpot_bumpl v al be f l : mono v -> wpot v al be f (bumpl l) <= wpot v al be f l + al * v (f + length l).
L875new
114LemmaPot_ov
Lemma Pot_ov v al be ga Ps f l : mono v -> al + be + 1 <= ga -> f + length l + 1 <= Ps ->
Pot v al be ga Ps f (bumpl l ++ [0]) + v (f + length l) <= Pot v al be ga Ps f l.
L885new
115LemmaPot_inc
Lemma Pot_inc v al be ga Ps Q0 f bs s p bs' s' d : mono v -> al + be + 1 <= ga -> Q0 < 2 ^ (Ps + 1) -> s <= 3 ->
ginc bs s = (bs', s', d) -> QI Q0 f bs s (S p) ->
Pot v al be ga Ps f (exs bs') + b2n d * v f <= Pot v al be ga Ps f (exs bs).
L897new
116LemmaGPhi_pot
Lemma GPhi_pot v al be ga Ps Q0 : mono v -> al + be + 1 <= ga -> 1 <= al -> 2 <= be -> Q0 < 2 ^ (Ps + 1) ->
forall a b bs s r, GPhi a b bs s r -> s <= 3 -> forall f U, QI Q0 f bs s (b - 1) ->
(forall q, f <= q -> U <= v q) ->
match r with
| RE2 k x bs2 s2 => exists h, QI Q0 (f + S h) bs2 s2 0 /\
    U * k + Pot v al be ga Ps (f + S h) (exs bs2) + v (f + h) * (al * x + be) <=
… +3 lines
L912new
117Definitionw
Definition w (q : nat) : nat := 2 ^ ((q + 1) / 2).
L981new
118Lemmaw_mono
Lemma w_mono : mono w.
L983new
119Lemmaw_lev
Lemma w_lev l q : 2 * l <= q -> 2 ^ l <= w q.
L986new
120Lemmaw_lev1
Lemma w_lev1 l q : 2 * l + 1 <= q -> 2 ^ S l <= w q.
L993new
121LemmaGPhi_QI
Lemma GPhi_QI Q0 Ps a b bs s k x bs2 s2 f : Q0 < 2 ^ (Ps + 1) -> GPhi a b bs s (RE2 k x bs2 s2) -> s <= 3 ->
QI Q0 f bs s (b - 1) -> exists h, QI Q0 (f + S h) bs2 s2 0.
L1000new
122LemmaDig_cost
Lemma Dig_cost Q0 Ps : Q0 < 2 ^ (Ps + 1) ->
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  2 ^ l * n <= Pot w 2 8 11 Ps f (exs bs) + 2 ^ l * (2 * x + 2) + 13 * w Ps) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  2 ^ l * n <= Pot w 2 8 11 Ps f (exs bs) + 13 * w Ps).
L1009new
123FixpointMO
Fixpoint MO (u : nat -> nat) (l : nat) (es : list nat) : nat :=
match es with [] => 0 | e :: es => u l * e + MO u (S l) es end.
L1061new
124Definitionpu
Definition pu (u : nat -> nat) (l : nat) : nat := match l with 0 => 0 | S l' => u l' end.
L1064new
125Lemmapu_le
Lemma pu_le u l : mono u -> pu u l <= u l.
L1066new
126LemmaMO_zero
Lemma MO_zero u l es : Forall (fun e => e = 0) es -> MO u l es = 0.
L1069new
127LemmaDig_mass
Lemma Dig_mass u v Q0 Ps : mono v -> mono u -> (forall l q, 2 * l <= q -> u l <= v q) -> Q0 < 2 ^ (Ps + 1) ->
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  pu u l * c + MO u l (exs bsp) <= Pot v 1 3 5 Ps f (exs bs) + pu u l * S x + 6 * v Ps) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  pu u l * c + MO u l (exs bsp) <= Pot v 1 3 5 Ps f (exs bs) + 6 * v Ps).
L1073new
128LemmaDig_len
Lemma Dig_len Q0 Ps : Q0 < 2 ^ (Ps + 1) ->
(forall x bs s n c bsp sp, DigP x bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  2 * (l + length bsp) <= Ps + 3) /\
(forall bs s n c bsp sp, DigT bs s n c bsp sp -> s <= 3 -> forall l f, 2 * l <= f -> QI Q0 f bs s 0 ->
  2 * (l + length bsp) <= Ps + 3).
L1128new
129Lemmapow_gt_self
Lemma pow_gt_self n : n < 2 ^ (n + 1).
L1153new
130LemmaDigE_ex
Lemma DigE_ex y : y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2) -> exists n c bsp sp, DigE y n c bsp sp.
L1156new
131LemmaDigT_exists
Lemma DigT_exists Q0 : forall D f bs s, s <= 3 -> QI Q0 f bs s 0 -> Q0 + 1 - 2 ^ f <= D ->
exists n c bsp sp, DigT bs s n c bsp sp.
L1160new
132DefinitionRel
Definition Rel (orig cur : list nat) : Prop :=
(forall i, S i < length cur -> nth i cur 0 <= nth i orig 0 + 1) /\
(forall i, length cur <= S i -> nth i cur 0 <= nth i orig 0).
L1194new
133Lemmanth_bumpl
Lemma nth_bumpl l i : nth i (bumpl l) 0 = nth i l 0 + (if Nat.eqb (S i) (length l) then 1 else 0).
L1198new
134Lemmanth_app0
Lemma nth_app0 l i : nth i (l ++ [0]) 0 = nth i l 0.
L1207new
135LemmaRel_ov
Lemma Rel_ov orig l : Rel orig l -> Rel orig (bumpl l ++ [0]).
L1210new
136LemmaRel_inc
Lemma Rel_inc orig bs s bs' s' d : s <= 3 -> ginc bs s = (bs', s', d) -> Rel orig (exs bs) -> Rel orig (exs bs').
L1220new
137LemmaRel_tl
Lemma Rel_tl orig cur : Rel orig cur -> Rel (tl orig) (tl cur).
L1226new
138LemmaRel_refl
Lemma Rel_refl l : Rel l l.
L1236new
139LemmaGPhi_rel
Lemma GPhi_rel a b bs s r : GPhi a b bs s r -> s <= 3 -> forall orig, Rel orig (exs bs) ->
match r with
| RE2 k x bs2 s2 => exists h, Rel (skipn (S h) orig) (exs bs2) /\ x <= nth h orig 0 + 1
| RSp _ _ => True
end.
L1239new
140LemmaGPhi_val
Lemma GPhi_val a b bs s r : GPhi a b bs s r -> s <= 3 ->
match r with RE2 k x bs2 s2 => 2 * gval bs2 s2 + a <= gval bs s + k + 2 | RSp _ _ => True end.
L1265new
141Definitionv2
Definition v2 (q : nat) : nat := 2 ^ (q / 2).
L1280new
142Definitionp2
Definition p2 (q : nat) : nat := 2 ^ S q.
L1281new
143Definitioncst1
Definition cst1 (q : nat) : nat := 1.
L1282new
144Definitionu1
Definition u1 (l : nat) : nat := match l with 0 => 0 | S l' => 2 * w l' end.
L1283new
145Definitionu2
Definition u2 (l : nat) : nat := match l with 0 => 0 | S l' => 2 ^ S l' end.
L1284new
146Lemmav2_mono
Lemma v2_mono : mono v2.
L1286new
147Lemmap2_mono
Lemma p2_mono : mono p2.
L1288new
148Lemmacst1_mono
Lemma cst1_mono : mono cst1.
L1290new
149Lemmav2_le_w
Lemma v2_le_w q : v2 q <= w q.
L1292new
150Lemmacst1_le_w
Lemma cst1_le_w q : cst1 q <= w q.
L1294new
151Lemmau1_mono
Lemma u1_mono : mono u1.
L1297new
152Lemmau1_w
Lemma u1_w l q : 2 * l <= q -> u1 l <= w q.
L1299new
153Lemmau2_mono
Lemma u2_mono : mono u2.
L1310new
154Lemmau2_v2
Lemma u2_v2 l q : 2 * l <= q -> u2 l <= v2 q.
L1312new
155LemmaMO_u1
Lemma MO_u1 l es : MO u1 (S l) es = 2 * wpot w 1 0 l es.
L1319new
156LemmaMO_u1_0
Lemma MO_u1_0 es : MO u1 0 es = 2 * wpot w 1 0 0 (tl es).
L1321new
157LemmaMO_u2
Lemma MO_u2 l es : MO u2 (S l) es = wpot p2 1 0 l es.
L1323new
158LemmaMO_u2_0
Lemma MO_u2_0 es : MO u2 0 es = wpot p2 1 0 0 (tl es).
L1325new
159Lemmanth_le_MO
Lemma nth_le_MO h es : forall l, nth h es 0 <= MO cst1 l es.
L1327new
160Lemmawpot_shift
Lemma wpot_shift v al be f f' l : mono v -> f <= f' -> wpot v al be f l <= wpot v al be f' l.
L1333new
161Lemmawpot_drop
Lemma wpot_drop v al be f h l : wpot v al be (f + h) (skipn h l) <= wpot v al be f l.
L1339new
162Lemmawpot_skipn_tl
Lemma wpot_skipn_tl v h l : mono v -> wpot v 1 0 0 (skipn (S h) l) <= wpot v 1 0 0 (tl l).
L1345new
163Lemmawpot_le_nth
Lemma wpot_le_nth v l1 : mono v -> forall l2 f, (forall i, nth i l1 0 <= nth i l2 0 + 1) ->
wpot v 1 0 f l1 <= wpot v 1 0 f l2 + vsum v f (length l1).
L1351new
164LemmaRel_nth
Lemma Rel_nth orig cur : Rel orig cur -> forall i, nth i cur 0 <= nth i orig 0 + 1.
L1362new
165Lemmawpot_split
Lemma wpot_split v al be f l : wpot v al be f l = wpot v al 0 f l + be * vsum v f (length l).
L1364new
166Lemmawpot_scale2
Lemma wpot_scale2 v f l : wpot v 2 0 f l = 2 * wpot v 1 0 f l.
L1366new
167Lemmawpot_le_v
Lemma wpot_le_v v v' al be f l : (forall q, v q <= v' q) -> wpot v al be f l <= wpot v' al be f l.
L1368new
168Lemmavsum_add
Lemma vsum_add v f m m' : vsum v f (m + m') = vsum v f m + vsum v (f + m) m'.
L1373new
169Lemmavsum_mono_m
Lemma vsum_mono_m v f m m' : m <= m' -> vsum v f m <= vsum v f m'.
L1375new
170Lemmavsum_cst1
Lemma vsum_cst1 f m : vsum cst1 f m = m.
L1377new
171Lemmavsum_p2
Lemma vsum_p2 f m : vsum p2 f m + 2 ^ S f = 2 ^ S (f + m).
L1379new
172Lemmawpot_p2_S
Lemma wpot_p2_S f l : wpot p2 1 0 (S f) l = 2 * wpot p2 1 0 f l.
L1384new
173Lemmaqsum_p2
Lemma qsum_p2 l : 2 * qsum l + 2 = 2 ^ S (length l) + wpot p2 1 0 0 l.
L1386new
174Lemmawpot_zero
Lemma wpot_zero v f l : Forall (fun e => e = 0) l -> wpot v 1 0 f l = 0.
L1391new
175LemmaPot_top
Lemma Pot_top v al be ga Ps l : be <= ga -> length l <= Ps ->
Pot v al be ga Ps 0 l <= wpot v al 0 0 l + ga * vsum v 0 Ps.
L1393new
176DefinitionWs
Definition Ws (P : nat) : nat := vsum w 0 P.
L1405new
177DefinitionV2s
Definition V2s (P : nat) : nat := vsum v2 0 P.
L1406new
178DefinitionPf
Definition Pf (k : nat) : nat := Nat.max 12 (k + 3).
L1407new
179DefinitionAf
Definition Af (k : nat) : nat := 5 * Ws (Pf k) + 6 * w (Pf k) + 2 * Ws k.
L1408new
180DefinitionBf
Definition Bf (k : nat) : nat := Af k + 5 * V2s (Pf k) + 6 * v2 (Pf k) + 2 ^ (k + 1).
L1409new
181DefinitionXf
Definition Xf (k : nat) : nat := Af k + 5 * Pf k + 7.
L1410new
182DefinitionCostf
Definition Costf (k : nat) : nat := 2 * Xf k + 2 + 2 * Af k + 11 * Ws (Pf k) + 13 * w (Pf k).
L1411new
183DefinitionNlo
Definition Nlo (k : nat) : nat := 2 ^ (k + 3) - 8 * 2 ^ ((Pf k + 3) / 2).
L1412new
184DefinitionNstar
Definition Nstar : nat := 17705.
L1413new
185LemmaPf_mono
Lemma Pf_mono k k' : k <= k' -> Pf k <= Pf k'.
L1415new
186LemmaWs_mono
Lemma Ws_mono P P' : P <= P' -> Ws P <= Ws P'.
L1417new
187LemmaV2s_mono
Lemma V2s_mono P P' : P <= P' -> V2s P <= V2s P'.
L1419new
188LemmaAf_mono
Lemma Af_mono k k' : k <= k' -> Af k <= Af k'.
L1421new
189Lemmaw_SS
Lemma w_SS q : w (S (S q)) = 2 * w q.
L1427new
190Lemmav2_SS
Lemma v2_SS q : v2 (S (S q)) = 2 * v2 q.
L1432new
191Lemmavsum_SS_w
Lemma vsum_SS_w f m : vsum w (S (S f)) m = 2 * vsum w f m.
L1437new
192Lemmavsum_SS_v2
Lemma vsum_SS_v2 f m : vsum v2 (S (S f)) m = 2 * vsum v2 f m.
L1439new
193LemmaWs_SS
Lemma Ws_SS P : Ws (S (S P)) = 2 * Ws P + 3.
L1441new
194LemmaV2s_SS
Lemma V2s_SS P : V2s (S (S P)) = 2 * V2s P + 2.
L1443new
195LemmaPf_big
Lemma Pf_big k : 9 <= k -> Pf k = k + 3.
L1445new
196LemmaAf_SS
Lemma Af_SS k : 9 <= k -> Af (S (S k)) = 2 * Af k + 21.
L1447new
197DefinitiongB
Definition gB (k : nat) : nat := Af k + 5 * V2s (k + 3) + 6 * v2 (k + 3).
L1453new
198LemmagB_SS
Lemma gB_SS k : 9 <= k -> gB (S (S k)) = 2 * gB k + 31.
L1454new
199LemmagB_all
Lemma gB_all m : gB (10 + 2 * m) + 31 < 7 * 2 ^ (10 + 2 * m) /\ gB (11 + 2 * m) + 31 < 7 * 2 ^ (11 + 2 * m).
L1460new
200LemmagB_ge
Lemma gB_ge k : 10 <= k -> gB k + 31 < 7 * 2 ^ k.
L1469new
201LemmaN1
Lemma N1 k : 7 * 2 ^ k + Bf k < 2 ^ (Pf k + 1).
L1477new
202LemmaCostf_SS
Lemma Costf_SS k : 9 <= k -> Costf (S (S k)) + 10 * (k + 3) = 2 * Costf k + 121.
L1488new
203LemmaNlo_SS
Lemma Nlo_SS k : 9 <= k -> Nlo (S (S k)) = 4 * 2 ^ (k + 3) - 16 * 2 ^ ((k + 6) / 2) /\
Nlo k = 2 ^ (k + 3) - 8 * 2 ^ ((k + 6) / 2).
L1494new
204LemmaD_all
Lemma D_all m : Costf (12 + 2 * m) + 123 <= Nlo (12 + 2 * m) /\ Costf (13 + 2 * m) + 123 <= Nlo (13 + 2 * m).
L1506new
205LemmaN2
Lemma N2 k : Costf k + 2 <= Nstar \/ Costf k + 2 <= Nlo k.
L1518new
206LemmaNstar_ge
Lemma Nstar_ge : 15 <= Nstar.
L1532new
207DefinitionMw
Definition Mw (bs : blks) : nat := wpot w 1 0 0 (exs bs).
L1537new
208DefinitionM2
Definition M2 (bs : blks) : nat := wpot p2 1 0 0 (exs bs).
L1538new
209DefinitionInv
Definition Inv (k N : nat) (y : word) : Prop :=
Nstar <= N /\ Nlo k <= N /\
((exists x bs s, y = p11 x (gw bs s) /\ s <= 3 /\ length bs <= k /\
    Mw bs <= Af k /\ M2 bs <= Bf k /\ x <= Xf k)
 \/ y = t1 \/ y = p01 1 t1 \/ y = p10 (p00 t2)).
L1541new
210Lemmanext_inv
Lemma next_inv k N n c bsp sp r :
GPhi (1 + n) (N + c - n) bsp sp r -> sp <= 3 -> n + 2 <= N -> Nstar <= N -> Nlo k <= N ->
MO u1 0 (exs bsp) <= Af k + 5 * Ws (Pf k) + 6 * w (Pf k) ->
MO u2 0 (exs bsp) <= Af k + 5 * V2s (Pf k) + 6 * v2 (Pf k) ->
MO cst1 0 (exs bsp) + 1 <= Xf k ->
2 * length bsp <= Pf k + 3 ->
… +1 lines
L1547new
211Lemmainv_step
Lemma inv_step k N y : Inv k N y -> exists kk y', Phi 1 N y kk y' /\ exists k', Inv k' (S kk) y'.
L1604new
212Fixpointorbit
Fixpoint orbit (f n N : nat) (y : word) : option (nat * word) :=
match n with
| O => Some (N, y)
| S n => match phif f 1 N y with Some (k, y') => orbit f n (S k) y' | None => None end
end.
L1663new
213Lemmaorbit_sound
Lemma orbit_sound f n : forall N y N' y', orbit f n N y = Some (N', y') -> K N y -->* K N' y'.
L1669new
214DefinitionB694
Definition B694 : blks := [(false, 17); (true, 1); (true, 1); (true, 1); (true, 1);
(false, 1); (false, 1); (false, 1); (true, 1); (false, 0)].
L1677new
215DefinitionY694
Definition Y694 : word := p11 7 (gw B694 0).
L1679new
216Lemmafin694
Lemma fin694 : orbit 100000 691 8 t2 = Some (17713, Y694).
L1681new
217Lemmainv694
Lemma inv694 : Inv 10 17713 Y694.
L1684new
218Lemmanonhalt_from
Lemma nonhalt_from N0 y0 (P : nat -> word -> Prop) :
c0 -->* K N0 y0 -> P N0 y0 ->
(forall N y, P N y -> exists k y', Phi 1 N y k y' /\ P (S k) y') ->
~ halts tm c0.
L1692new
219Lemmanonhalt
Lemma nonhalt: ~halts tm c0.
L1706adapted
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 51: 3. Rules

3.1 Window rules (finite runs; each is one es)

In each rule, every executed transition reads a cell inside the shown window. So each rule holds in every context.

# statement steps
W1 1 F> 1 → 1 1 F> 5
W2 F> 001 → 011 F> 3
W3 F> 000 → 011 C> 3
W4 C> 101 → 111 F> 9
W5 011 E> 0 → E> 0 010 5
W6 0 E> 0 → 1 1 F> (marker turn) 3
W7 F> 01 → 00 F> 2
W8 011 <A 100 → E> 001 000 4
W9 011 <A 101 → E> 001 001 4
W10 011 E> 1 → <A 100 0 (D6 exit) 4
W11 C> 10 → 11 F> 4

3.2 Shift rules (induction on n, one IH use each)

# statement steps proof
S1 (SL) (011)^n E> 0 → E> 0 (010)^n 5n ind n: [W5, IH]
S2 (SR) F> (001)^n → (011)^n F> 3n ind n: [W2, IH]
S3 1 F> 1^n → 1^(n+1) F> 5n ind n: [W1, IH]

3.3 Region pass (any left context l)

# statement domain steps proof
RP0 l 0 (011)^n <A 100 X → l 110 0 (011)^n C> X n ≥ 1, any l, X 8n+4 W8, S1(n−1), W6, W7, S2(n−1), W3
RP1 l 0 (011)^n <A 101 000 X → l 110 0 (011)^(n+1) C> X n ≥ 1 8n+7 W9, S1(n−1), W6, W7, S2(n), W3

The region pass reads nothing to the left of the marker. That is why a bounce works in any left context (used in D6).

3.4 Local pass LP

Definition. LP(X) is the run from 011 C> X 0^inf until the head first enters the cell left of that 011, which is cell x0-4. LP never reads cell x0-4 or anything to its left. Every rule below ends in one of two exit forms:

  • d = 0: <A 100 X';
  • d = 1: <A 101 000 X'.

We write LP(X) = (X', d).

# statement domain steps proof
LP0 011 C> 0 r → <A 100 1 r any r (incl. X = '') 4 C0, D1, E1, E0
LP11 011 C> 110 r → <A 101 000 r any r 8 C1, E1, E0, A1, F1, C0, D1, E0
LPC (carry) 011 C> 101 a^e z R → <A 100 001 a^(e+d_R) z R' with (R', d_R) = LP(R) e ≥ 0, R with an LP rule (R = '' allowed) s(R)+8e+20 right (3e+12): W4, S2(e), W3; then LP(R), whose exit reads the last cell of (011)^e or of 111; left (5e+8): for e ≥ 1, W8 or W9, S1(e−1), then 9 fixed steps through 111 and the old 011; for e = 0, 8 fixed steps
LP5 (D5) 011 C> 10 001 a^e z R → <A 100 01 001 a^(e+d) z inc R R ∈ G (R = '' allowed) by execution right: 4 + W1-type step + S2; LP(R) = GI; left as in LPC
LP6 (D6) 011 C> 10 101 a^e z R → <A 100 a^(k+1) z Y, where Φ(1, e+1, R) = L'(k, 000 Y) R ∈ G (R = '' allowed) (3e+14) + sub-epoch + 4 section 3.8
LPT six constant words, by execution (steps in brackets): 1 → 010001 [18]; 10010001 → 01001000010010001 [70]; 10110001 → 0001000010001 [44]; 1000010001 → 01000010010001 [40]; 1001000010001 → 010010001000010001 [62]; 10010010001 → 010010010001000010001 [100] (all d = 0) — 18–100 es

GI (inc on G) is a corollary. Write inc W for the LP result on a G word. It is a binary +1, LSB first:

  • An a-block toggles to a b-block (LP0).
  • A b-block carries (LPC): it becomes an a-block, and the rest is incremented.
  • Tails step '' → 1 → 010001 → 110001 (LP0, LPT, LP0).
  • 110001 → 001 with d = 1 (LP11). This is an overflow: a new block, and the absorbed 001 goes into the block in front of it (LPC with d_R = 1), or into the hub when the word is a bare tail.

G is closed under inc. For a word with at least one block, inc returns d = 0. Positions are stable: inc changes digits, and on an overflow it adds +1 to the last block and appends a new last block with e = 0. It never changes any other exponent.

Other names used below:

  • HT (toggle), D2 ('01' V → '11' V), D4 ('00' V → '10' V) and the tail steps are LP0.
  • D1 ('11' a V → '01' V, d = 1), D3 ('11' z V → '00' V, d = 1) and '11' → '' are LP11.
  • HC (carry into a nested word) is LPC with any rest that has an LP rule.
  • D5 is LP5, D6 is LP6, and T is LPT.

End words E is the closure of the LPT outputs and of 010010001 under LP until G (23 words, computed by direct enumeration). Its largest own-level cost until G is τ = 13* bounces.

3.5 Bounce

B. K(a, b+1, X) → K(a+1, b+d, X') for b ≥ 1, a ≥ 0 and LP(X) = (X', d). Steps: s_LP(X) + 8b + 4 (d = 0) or + 8b + 7 (d = 1).

  • Proof: LP(X), then RP0 or RP1 with n = b.
  • The run never reads left of the marker, so B also holds with any l in place of 0^inf (110)^a.

3.6 Eats (b = 1; the LP exit then meets the marker, A reads 0)

# statement context fact
E1g K(a, 1, a^(e+1) z R) → K(a+2, e+1, R), R ∈ G never reads left of the marker
E2g K(a, 1, 101 a^e z R) →* L'(a, 000 11 a^(e+d') z R'), (R', d') = inc R, R ∈ G the sweep 110 → 010 through (110)^a reaches cell first−1 only at the last step
E0 K(a, 1, '') →* L'(a+1, 0001) same
Et1 K(a, 1, 1) →* L'(a, 000 01 a z 1) same
Et2 K(a, 1, 010001) →* L'(a, 000 10 00 010001) same
Et3 K(a, 1, 110001) → K(a+1, 1, 001), then E1g gives K(a+3, 1, ''), then E0 never reads left of the marker

These cover every G word at b = 1. A G word is '', a tail, an a-block first, or a b-block first. Here first is the first cell of (110)^a. L'(k,T) → L(k,T) takes one step (E0 = 1LA on a blank).

3.7 Restart

R. L(k, 000 Y) → K(1, k+1, Y) in 3k + 7 steps, for any Y. The run never moves left of the A cell.

3.8 D6, the nested bounce

Epoch map. For N ≥ 1 and a word R, Φ(a, N, R) is the deterministic sequence:

  • B while b ≥ 2;
  • the eats of 3.6 at b = 1;
  • it stops at the first pre-record L'(k, T).

Φ is defined when every eat it meets is at a G word. Inside D6 this holds: R ∈ G and G is closed under inc and under E1g.

Φ terminates for every R ∈ G (D.0, Lemma P): only E1g moves the front, finitely many positions are ever created, and between two eats the budget falls by 1 per bounce except for at most one bare-tail absorption. So Φ reaches E2g, E0, Et1, Et2 or the Et3 chain after finitely many steps, and LP6 below is a total rule. The same argument shows that the counting phase of every epoch (after its digestion) ends.

LP6 proof. Write x0 for the first cell of X.

  1. Right pass (3e + 14 steps). It goes W11 (C> 10 → 11 F>), then W1, then F0 and A1, then S2(e), then W3: - from 011 C> 10 101 a^e z R - to 011 1 · 110 0 (011)^(e+1) C> R.

The part after · is the hub K(1, e+1, R) whose 0^inf has been replaced by … 011 1. Its first cell is x0+1, so first−1 = x0 holds a 1. 2. Sub-epoch. By 3.5 and 3.6, every bounce and every E1g of Φ(1, e+1, R) reads only cells at or right of its marker. Its final eat (E2g, E0, Et1, Et2, or the Et3 chain) reaches cell first−1 for the first time in state E, exactly when the standalone run reaches L'(k, T). So, cell for cell, the run in context equals the standalone run up to that moment, except that cell first−1 holds 1 instead of 0. 3. Exit (W10, 4 steps). 011 E> 1 01 (001)^k T → <A 100 0 01 (001)^k T = <A 100 a^(k+1) T. Every pre-record has T = 000 Y, so X' = a^(k+1) z Y and d = 0.

The sub-residue Y is one of:

  • '11' a^x z W' with W' ∈ G (from E2g);
  • '1' (from E0 and from the Et3 chain);
  • '01' a z 1 (from Et1);
  • '10 00 010001' (from Et2).

All of these are in O ∪ G.

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

6 machines, 3 killed, 3 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
#30 kill 151RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC✓Killed: never haltsthis kill
#7 kill 161RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA✓Killed: never haltsparent link; = #30's table mirrored, run from state E; named in #30's notes.md; named in #7's .v header; named in #7's proof.md; named in #7's notes.md · review · same machine as this kill? (same table mirrored, started in #30's E; different orbit; tables, pictures and numbers side by side) · mechanism
#31 kill 171RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB✓Killed: never haltsparent link; = #30's table, run from state B; named in #30's notes.md; named in #31's .v header; named in #31's proof.md; named in #31's notes.md · review · same machine as this kill? (same table, started in #30's B; different orbit; tables, pictures and numbers side by side) · mechanism
#101RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC⚠Cryptid candidatetargeting: follow-on to #10; named in #30's notes.md · mechanism
#151RB1RF_1LC1RE_---0LD_1LE0LD_1RA0RF_0RE0LB⚠Cryptid candidatevia #31: targeting: follow-on to #15 · mechanism
#281RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA⚠Cryptid candidatevia #7: targeting: follow-on to #7 · mechanism
6ChecklistCheck: every ✓ is computed; the two ○ are yours to decide; an amber ! is an optional check that did not finish.
  • ✓
    Machine string exact
    the .v literal == holdout list line 748 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 67.68 s
  • ✓
    .v hash matches the checked hash
    .v = checked sha256 93a493f55311…; submission/ copy = checked sha256 93a493f55311…
  • ✓
    No repo-local paths in the .v
    comments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own verify/X.v is fine: none in the .v or the submission/ copy
  • ✓
    Public write-up is clean
    tools/writeup_lint.py on submission/proof.md: 0 error(s)
  • ○
    proof.md reviewed by Dennis (Checkpoint B)
    no Checkpoint B note from Dennis found
    • notes.md L241: ## Checkpoint B, skeptic round 1 (2026-10-10)
    • notes.md L267: - proof.md: a public write-up built by `rocq/submission_src/build.py` (`python3 -B rocq/submission_src/build.py proof.md rocq/submission_src submission/proof.md`; header + working §0-§7 with 17 one-match asserted scrubs
    • notes.md L277: - No Checkpoint A or B notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
    • proof.md L259: - A deep trigger with a large exponent in front of a short all-ones suffix can push c to about `log2(excess)`. This is the effect of the Checkpoint B examples, which reach c = 2 to 6 inside the old invariant.
    • proof.md L518: - **Adversarial residues (Checkpoint B round 1):** 1,504 per seed, plus 2 × 12,004 in a stand-alone stress run (`check_proof.py --adv N`, seeds 11 and 12; `data/check_proof_adv_seed{11,12}.txt`). Two thirds come from ins
    • proof.md L538: - Confidence: high for sections 3–4 and for the mechanism; **medium-high** for Lemma D as written (one open link, and the D.3/D.4 bookkeeping deserves a careful second read at Checkpoint B).
  • ○
    Family posted together?
    2 other kill(s) in the family: #7, #31; the Discord draft names 0 of them; 3 member(s) not killed: #10, #15, #28

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

Files

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

namesizechanged
notes.md ↓32 KB2026-10-11 00:36
proof.md ↓43 KB2026-10-10 16:50
how_proved.md ↓1.6 KB2026-10-14 10:51
status.json ↓575 B2026-10-16 10:28
observe.json ↓15 KB2026-10-10 15:19
deepen.json ↓5.9 KB2026-10-10 15:19
1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v ↓86 KB2026-10-10 18:17
data/32 items2026-10-10 16:50
decisions/2 items2026-10-10 15:19
img/9 items2026-10-10 15:04
rocq/8 items2026-10-10 18:41
scripts/20 items2026-10-10 15:18
submission/6 items2026-10-15 15:49
work/1 item2026-10-10 18:43
check_proof.py ↓43 KB2026-10-10 16:50
compress_track.txt ↓2.4 KB2026-10-10 13:03
data_val_rules_1.json ↓359 B2026-10-10 13:11
data_val_rules_2.json ↓359 B2026-10-10 13:11
qsim.err ↓0 B2026-10-10 13:03
qsim.jsonl ↓5.7 KB2026-10-10 13:03
sim_1e9.jsonl ↓149 B2026-10-10 12:55
status.json in full
{
 "tm": "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "pr": "https://github.com/ccz181078/busycoq/pull/25",
 "pr_state": "merged",
 "pr_file": "verify/M_1RB0RF_1RC1RF_1LD0RE_HHH0LE_1LA0LE_0RA0LC.v",
 "pr_opened": "2026-10-15T22:46:50Z",
 "pr_comments": 0,
 "pr_head_sha": "b5060df30aabdde3b1eacd4a2cfa932557b0b53d",
 "posted": "2026-10-15 (Discord; user confirmed sent)",
 "pr_merged_at": "2026-10-16T07:08:02Z",
 "pr_merged_by": "ccz181078"
}
observe.json contract (tools/README-card.md):
3 contract warnings
  • diagrams: 7 (want 3-5)
  • diagrams[5].window: not "cells A..B, 1 px = k cells"
  • diagrams[6].window: not "cells A..B, 1 px = k cells"