Built . It shows the files as they were then (ages and “working now” follow your clock).
tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.Machines / W4-2
1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF
How we proved it never halts
A size bound tying the counter to the length of the last round
The head sits between a binary counter on its left and, on its right, 1 10 10 … 10 0 10 10 … 10: a single 1, a run of fuel pairs, a gap, and a run of spent pairs. Each bounce moves one pair from fuel to spent and adds 1 to the counter. When the fuel is gone, the right side bites off the counter's low end and refills the fuel for a longer round. The counter is normally tidy, its number written on every other cell (or packed, with the top two bits sharing a pair), but a bite can leave it messy for a while.
The machine can halt only at a bite on a messy counter whose low end has one particular bad shape. The key is a size bound: at every bite on a tidy counter, the counter's value is at least the length of the round just finished and at most about 2.5 times it, the exact cap depending on parities and layout.
Why that settles it: the proof sorts tidy bites into eleven cases and follows each to the next tidy bite. In every case the bound keeps any messy bite on the way away from the bad shape and makes the round after it long enough to tidy the counter, and the bound holds again at the end. The run reaches a tidy bite inside the bound at step 32, so it never halts.
The Rocq proof builds on busycoq's BECv5, whose two machines differ from this one in one table entry. It proves each low-level move as an exact run, derives the eleven cases, checks the bound's closure by arithmetic, and runs the 32-step opening directly.
#18local proof number
1,217lines of Rocq
66 sto compile
6/6automatic checks
About this picture
The standard picture (bbchallenge.org's Default view): each row is the whole tape at one step, time runs downward, and the head's path draws the pattern.
bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited
Claimed by someone else
We proved this machine locally, but our proof was still unsubmitted when we found it already covered upstream.
Submit completed proofs early. A local proof does not secure an upstream claim.
Upstream proof ↗ · Recorded timeline
What the timing evidence establishes
This describes upstream credit, not who first discovered the mathematics. The records do not establish adoption of our proof, first public push time, or whether an earlier submission would have secured credit.
Overview
In one sentence
BECv5 TM1/TM2 counter; F1=1LF packs the top pair. Halting only at rare dirty overflows, avoided by >= 0.29 m.
Submitted mechanism Bounce counter. The tape is 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf, BECv5's w <| R n m. Each bounce applies one map phi to the left word w (read as two interleaved binary numbers, even and odd cells) and moves one 10 from the n-block to the m-block. (submission/README.md, Mechanism)
- Upstream
- The blank-start machine never halts: BECv10.v.TM12 ↗. We also have a local proof. This upstream addition is separate from our merged submissions; adoption credit is not established. Recorded commit time: 2026-10-13T13:42:06Z. First public push time is not established.
- Rocq proof
- check_kill PASS · first Oct 11 10:591,217 lines · 47 KB .v · compile 65.8 s · coqchk pass · 0 axioms · PASS Oct 11 10:59· the .v file
- Automatic review
- 6 of 6 checks passtemplate: verify/BECv5.v Module TM1 (adapted from) · details in Proof →
- Class
- Bell eats counterours: Bell eats counter (sheet) · ours adds: BECv5 TM1/TM2's counter with F1 = 1LF; the counter alternates std / packed encodings, with dirty transients · med confidence
- On the list
- not on
BB6_holdouts_663.txt(line 224 of the previous list) · historical 740 line 224
Your calls on file 2
- funded
- option: hunt · date: 2026-10-11
- 2026-10-11 · hunt
- Fund one 2 h stage to find an invariant on (type, N, m) that keeps every overflow off the halting points, start proof.md with it open, or park? (Dennis: go with recommendations (2026-10-11))
Mechanism
What to check here: the pictures show the mechanism that the rule table describes.
How it works: 3 notes
- K(w,n,m) = w <A 1(10)^(1+n)0(10)^m. Each bounce applies phi to w (last 00 -> 1, zeros to its right; F1 = 1LF lets a carry pass 11) and moves one 10 from n to m. At n = 0 the right side eats the counter's low end (template ROv).
- The counter comes back shifted one cell and recounts, so it alternates encodings: std(N) -> pk(2k+b) -> std(2r+b) ... In 2.8% of cycles the overflow sees a dirty word, still shifted.
- Halting needs an odd landing at a dirty overflow ending 01/11 (or 10, nested). None in 17M cycles (~5e22 steps), gap >= 0.29 m. No 740 holdout shares the table; 349 is equivalent (TM518) to it started in F.
Figures for Checkpoint A
The site's view. The right edge holds the (10) block; the left edge is the counter being eaten and rebuilt.
bbchallenge-defaultStart blankRows 10,000 steps squeezed into 500 px rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1 px row = 20 steps; the site blends steps 20y+9 and 20y+10
One row per cycle. Read the colour strip on the right, then compare the leftmost lit cells row to row.
customStart blankRows one per overflow configuration K(w,0,m) = w <A 1100 (10)^m 0^infWindow cells -27..0, 1 px = 0.25 cellsColors 1 0 a 1 in the top pair of a packed counter a 1 in a dirty word standard counter packed counter dirty word
Rows: cycles 1..400 (steps 32..604,697,267, not evenly spaced), 2 px per row · Window: counted from the counter's right end, the cell A reads; that cell moves left over time · Colors: right strip
Same start and steps, columns aligned. Follow the cyan F head down both panels; find the first differing row.
bbchallenge-exploreStart constructed: 0∞ 10100 <A 1100 (10)6 0∞Rows every step, steps 0..368Window cells -6..17, 1 px = 1/3 cellColors 0 1
Rows: (= blank-tape steps 430..798, from overflow std(6), m = 6 to the next overflow), 3 px per row · Window: (left panel); right panel: TM1 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB, cells -4..17 shifted to the same columns (slate filler at its left) · Colors: head colour = state: red A, orange B, blue C, green D, magenta E, cyan F
More figures (3)Fig 4–6: Left records to 2e8 steps · Every 2,000,000 steps to 2e9 · N/m by counter class vs invariant
Fig 4 · Left records to 2e8 steps
One row per new leftmost cell. The green diagonal is the head eating left; bands are the (10)/(01) blocks.
bbchallenge-defaultStart blankRows the start, then one row per new leftmost cellWindow cells -1046..280, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1,047 rows, steps 0..200,000,000; not evenly spaced in time
Fig 5 · Every 2,000,000 steps to 2e9
Overall growth: both edges grow like the cube root of time. The 1010 tape reads as grey at this scale.
bbchallenge-defaultStart blankRows every 2,000,000 stepsWindow cells -2313..591, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1,001 rows, steps 0..2,000,000,000 · Colors: black: alternating 1010 cells look grey
Fig 6 · N/m by counter class vs invariant
One band per class: bars stay left of the white tick; the dotted grey tick is where halting becomes possible.
customStart blankRows 5 bands, top to bottomWindow x = (N-m)/m from 0 to 1.6, 1 px = 0.004Colors std counter std N odd pk N even pk N odd parity broken tick: bound of invariant I band background
Rows: std N even, std N odd, pk N even, pk N odd (N = m mod 2), then N != m mod 2; clean overflow states of cycles 1..1,000,000 with N > 100 (abstract rules), bar height = sqrt of count · Colors: light; grey dotted tick = N = 2m+4 (halting possible for N even)
Rules (8/8 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| init | 0∞ A> 0∞ ⟶ 0∞ 1 <A 1100 10 0∞ | via K('',0,0) at step 5 and K('',1,0) at step 14; = std(1), m = 1 | 32 | ✓1/1 |
| R1 bounce | 0∞ w <A 1 (10)1+n 0 (10)m 0∞ ⟶ 0∞ phi(w) <A 1 (10)n 0 (10)m+1 0∞ | n >= 1; phi(w): last cell 0 -> 1, else the last 00 pair (0^inf counts) -> left cell 1, all cells right of it 0 (random w up to 14 cells) | — | ✓200/200 |
| R2 overflow, q even | 0∞ w <A 1100 (10)m 0∞ ⟶ 0∞ x <A 1 (10)2+m+q/2 0 0∞ | phi(w) = x 1 0^q with q even (the template's ROv when w = std((2k+1)2^i-1): q = 2i, x = std(k)0) | — | ✓200/200 |
| R3 overflow reset, q odd | 0∞ w <A 1100 (10)m 0∞ ⟶ 0∞ x' <A 1100 (10)m+(q+3)/2 0∞ | phi(w) = x 1 0^q, q odd, x = x' 00 or x empty | — | ✓200/200 |
| R4 overflow halt | 0∞ w <A 1100 (10)m 0∞ ⟶ halt | phi(w) = x 1 0^q, q odd, x ends in 01 or 11; never reached from blank (17M cycles) | — | ✓200/200 |
| B std -> pk | 0∞ std(N) <A 1100 (10)m 0∞ ⟶ 0∞ pk(2k+b) <A 1100 (10)b 0∞ | N = (2k+1)2^i - 1, b = 1+i+m, L = bitlen(k); clean iff k a power of 2 or 2k+b >= 2^(L+1); k = 0: std(b); else dirty phi^b(std(k)0) | — | ✓200/200 |
| B pk -> std | 0∞ pk(N) <A 1100 (10)m 0∞ ⟶ 0∞ std(2r+b) <A 1100 (10)b 0∞ | k = 2^(L-1)+r, r > 0, clean iff 2r+b >= 2^L; k a power of 2: std(k+b); k = 0 (all ones): reset, then std(b+1), m = b+1; else dirty phi^b(pk(k)0) | — | ✓200/200 |
| phi^j acceleration | w ⟶ phi^j(w) | cells below the lowest 1 at an odd offset count in binary on their even offsets; when full, the next step lands above | — | ✓200/200 |
Compressed historythe tape as 0∞ w <A 1100 (10)m 0∞, w = std(N) | pk(N) | dirty word at 27 moments: where the rules are read off
0∞ w <A 1100 (10)m 0∞, w = std(N) | pk(N) | dirty word
| step | type | N | m |
|---|---|---|---|
| 32 | std | 1 | 1 |
| 135 | std | 3 | 3 |
| 430 | std | 6 | 6 |
| 797 | pk | 13 | 7 |
| 1,362 | std | 11 | 9 |
| 2,295 | pk | 14 | 12 |
| 3,366 | std | 19 | 13 |
| 4,931 | pk | 20 | 16 |
| 6,664 | std | 21 | 17 |
| 8,795 | pk | 29 | 19 |
| 11,364 | std | 27 | 21 |
| 14,661 | pk | 30 | 24 |
| 18,216 | std | 39 | 25 |
| 22,931 | pk | 33 | 29 |
| 179,620 | std | 66 | 60 |
| 199,243 | dirty | 101,101,010,101 | 61 |
| 199,297 | std | 0 | 69 |
| 224,984 | std | 70 | 70 |
| 1,150,500 | std | 132 | 116 |
| 1,220,919 | dirty | 1.01·1013 | 117 |
| 9,121,201 | pk | 265 | 233 |
| 74,292,260 | std | 475 | 469 |
| 251,944,630 | std | 1,163 | 705 |
| 609,476,754 | std | 1,212 | 976 |
| 2,118,660,118 | pk | 2,653 | 1,465 |
| 5,070,324,706 | pk | 2,472 | 1,954 |
| 9,968,287,008 | pk | 3,953 | 2,451 |
typelast pknot plottable
Nlast 3,953mlast 2,451Template comparisonBECv5.v TM1: partly applies · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | 1LF |
| B | 0RC | 0RB |
| C | 0LD | 1LA |
| D | 1LC | 0LE |
| E | 0LA | --- |
| F | 1LA | 1LFtpl 0RB |
differs from the template
- file
BECv5.v:30- module
TM1- machine
1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB(1 transition apart)- diff
F1: 1LF here vs 0RB (TM1) / 1LB (TM2)- note
- Kept: LC0, R n m, LInc0, LIncs, RIncs, ROv for std counters. New: a packed counter pk with its own ROv/increments, the shifted-counter orbit (replaces LIncs': H0 -> pk(2k+j) / std), dirty transients, reset R3, and the invariant.
Proof strategy & riskshow the formal proof will go · 3 risks to watch
Find an invariant on (type, N, m) at overflow, plus the dirty state, that keeps b' off the odd landings ending 01/11/10 (measured gap >= 0.29 m). Then copy BECv5 TM1's LC0/R/RIncs/ROv, add pk lemmas and the dirty-orbit lemma, and close with progress_nonhalt_cond.
- ▲No invariant yet: the halting branch is real in the abstract system, so a proof must pin down N vs m tightly enough.
- ▲Dirty orbits need a recursive word description (binary sub-counters on even offsets) that is heavier to formalize than BinInc.
- ▲R3 resets (hit once, near misses at distance 2) put non-standard words into the next overflow; the invariant must cover them.
Stats & provenance1010 steps simulated · 4,934 cells · the status in full · files
- simulated
- 1010 steps
- tape
- 4,934 cells · 2,462 nonzeros
- growth
- span ~ 2.3·steps^(1/3) cells (4,934 at 1e10); m ~ 1.14·steps^(1/3); abstract rules: 17,000,000 cycles (m = 4.25e7, ~5e22 steps)
- status now
- check_kill PASS, independently re-verified (status.json, 2026-10-11)
- observer's note
- Observe done, confidence med: rules closed and validated, non-halting invariant open (decision.json)
- files
- observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v
Proof & checks
6/6 automatic checks pass
Kill 18 · Bell eats counter · the kill file 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v: 1217 lines, 118 items · the package submission/
✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (adapted from): verify/BECv5.v Module TM1 · 2% 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
1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LFvs holdout list
Theorem
check_kill
✓ PASS
· 17/17 checks pass
· compile 65.79 s · coqchk pass
(29.58 s) · assumptions: 0
(closed)
· 2026-10-11 17:59:26 UTC
· submission/check_kill.txt
Checked .v
sha256 20521ad7e5287240…
| ✓ | 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v | 20521ad7e5287240… = checked |
| ✓ | submission/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v | 20521ad7e5287240… = checked |
Status
✓Killed: never halts
updated 2026-10-11
✓ args✓ input✓ framework✓ framework_build✓ forbidden✓ structure✓ tm_text✓ theorem_text✓ coq✓ names✓ compile✓ tm_rocq✓ theorem_rocq✓ isolation✓ assumptions✓ coqchk✓ integrity
All 17 check_kill checks with their one-line results
| ✓ | args | 6x2 machine, framework module Individual62, mode nonhalt |
| ✓ | input | 48027 bytes, 1217 lines, 1340 sentences |
| ✓ | framework | HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/ |
| ✓ | framework_build | 13 needed framework .vo files present and fresh, with native code no older than the .vo |
| ✓ | forbidden | none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token) |
| ✓ | structure | 5 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced |
| ✓ | tm_text | line 23: TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF" == <tm> (41 bytes) |
| ✓ | theorem_text | line 1178: nonhalt : ~halts tm c0 |
| ✓ | coq | coqc 8.20.1 ([local working file] |
| ✓ | names | halts, c0, TM_from_str resolved inside Individual62 |
| ✓ | compile | compiled in 65.8s with all appended checks |
| ✓ | tm_rocq | BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF" by eq_refl (in-file and isolated) |
| ✓ | theorem_rocq | nonhalt : ~ halts (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF") c0 with absolute names (in-file and isolated) |
| ✓ | isolation | only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off |
| ✓ | assumptions | 0 assumption(s), all in the baseline |
| ✓ | coqchk | coqchk -norec BB6Kill.Candidate ok (29.6s); its context summary lists nothing of the file's own |
| ✓ | integrity | input sha256 and framework HEAD/cleanliness identical before and after |
2Where it came fromCheck: the template is the one you expect, and the measured reuse (tiles, the reuse figure, diff) agrees with what the README says was kept and changed (quoted).
adapted from
verify/BECv5.v Module TM1
· detected from 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v line 4
2%of our lines identical to the template
1changed lines
1046added lines (ours only)
118template lines dropped
2 / 1 / 115items 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/BECv5.v, Module TM1 / Module TM2, which differ from this machine only in F1. Kept: the right side R n m and its right step, the standard counter, and the architecture (big-step lemma per rule, start by esx, progress_nonhalt_cond). New: E/O words with phi as the relations PA/PF, the lemma Sweep, the packed counter, eleven macro rules in place of TM1's one and TM2's two, and the invariant I with its coverage and closure arithmetic. The file has 1,217 lines, every lemma top level.
Top two bars: non-blank lines after the TM string is replaced by <TM> and whitespace is collapsed. Bottom bar: our Definitions/Lemmas/… by name.
identicalchanged / adaptedours only (new)template only
Template part: lines 1–29 (shared header, before the first Module) + 31–165 (body of Module TM1; the Module/End lines left out). Ours: lines 15–1217 (header comment 1–14 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: highbit, LC0, tm', LInc0, LIncs, LIncs', RIncs, ROv, S, BigStep
Side-by-side diff: template (144 lines) vs ours (1072 lines), 1165 lines differ; runs of identical lines and long template-only runs folded
identicalequal once each TM string is <TM>changedours onlytemplate only
| template | ours | ||
|---|---|---|---|
| 1 | From BusyCoq Require Import Individual62. | 16 | From BusyCoq Require Import Individual62. |
| 2 | Require Import ZifyNat Lia. | 17 | Require Import ZifyNat Lia. |
| 3 | Require Import ZArith. | 18 | Require Import ZArith. |
| 4 | Require Import String. | 19 | Require Import String. |
| 5 | From BusyCoq Require Import BinaryCounter_v2. | ||
| 6 | From BusyCoq Require Import Longitudinal. | ||
| 8 | Open Scope list. | 21 | Open Scope list. |
| 10 | Ltac flia := repeat (lia||f_equal). | ||
| 12 | Lemma highbit x: | ||
| ⋯ 14 template-only lines (template 13–26), not in ours | |||
| 27 | cbn; lia. | ||
| 28 | Qed. | ||
| 32 | Definition tm := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB"). | 23 | Definition tm := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF"). |
| 34 | Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40). | 25 | Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40). |
| 35 | Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40). | 26 | Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40). |
| 37 | Notation "l <| r" := | ||
| 38 | (l <{{A}} [] *> r) (at level 30). | ||
| 40 | Notation "l |> r" := | ||
| 41 | (l <* [] {{B}}> r) (at level 30). | ||
| 43 | Definition LC0 n := BinInc <[0;1] n. | ||
| 44 | Definition R n m := [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^(m) *> const 0. | 28 | Definition R n m := [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^(m) *> const 0. |
| 46 | Notation hL := (A,[]). | ||
| 30 | (** ** Words W(e,o): bit d of e on cell 2d, bit d of o on cell 2d+1 (cell 0 is read by A) *) | ||
| 47 | Notation hR := (B,[]). | ||
| 32 | Definition bt (x:nat) : Sym := if Nat.odd x then 1 else 0. | ||
| 48 | Notation hLR := [(hL,hR)]. | ||
| 34 | Fixpoint wd (n e o : nat) : list Sym := | ||
| 49 | Notation hRL := [(hR,hL)]. | ||
| 35 | match n with | ||
| 51 | Definition tm' := flip tm. | ||
| 36 | | O => [] | ||
| 53 | Lemma LInc0 r n: | ||
| 37 | | S n' => bt e :: bt o :: wd n' (Nat.div2 e) (Nat.div2 o) | ||
| 54 | LC0 n <| r -->* | ||
| 38 | end. | ||
| 55 | LC0 (1+n) |> r. | ||
| 40 | Definition WS e o : side := wd (e+o) e o *> const 0. | ||
| 42 | Lemma bt_even e: bt (2*e) = 0. | ||
| 43 | Proof. unfold bt. rewrite Nat.odd_even. reflexivity. Qed. | ||
| 45 | Lemma bt_odd e: bt (2*e+1) = 1. | ||
| 46 | Proof. unfold bt. rewrite Nat.odd_odd. reflexivity. Qed. | ||
| 48 | Lemma div2_even e: Nat.div2 (2*e) = e. | ||
| 49 | Proof. apply Nat.div2_double. Qed. | ||
| 51 | Lemma div2_odd e: Nat.div2 (2*e+1) = e. | ||
| 52 | Proof. rewrite Nat.add_1_r. apply Nat.div2_succ_double. Qed. | ||
| 54 | Lemma wd_pad n: forall e o k, | ||
| 55 | e < 2^n -> o < 2^n -> | ||
| 56 | wd (n+k) e o *> const 0 = wd n e o *> const 0. | ||
| 56 | Proof. | 57 | Proof. |
| 57 | unfold LC0. | ||
| 58 | induction n; intros e o k He Ho. | ||
| 58 | er. | ||
| 59 | - cbn in He,Ho. assert (e=0)%nat by lia. assert (o=0)%nat by lia. subst. | ||
| 60 | cbn. induction k. | ||
| 61 | + reflexivity. | ||
| 62 | + change (wd (S k) 0 0) with (0 :: 0 :: wd k 0 0). cbn [Str_app]. rewrite IHk. rewrite <-!const_unfold. reflexivity. | ||
| 63 | - cbn [wd Nat.add Str_app]. f_equal. f_equal. | ||
| 64 | apply IHn. | ||
| 65 | + rewrite Nat.div2_div. cbn in He. apply Nat.Div0.div_lt_upper_bound; lia. | ||
| 66 | + rewrite Nat.div2_div. cbn in Ho. apply Nat.Div0.div_lt_upper_bound; lia. | ||
| 67 | Qed. | ||
| 69 | Lemma lt_pow2_self x: x < 2^x. | ||
| 70 | Proof. apply Nat.pow_gt_lin_r. lia. Qed. | ||
| 72 | Lemma wd_WS n e o: | ||
| 73 | e < 2^n -> o < 2^n -> | ||
| 74 | wd n e o *> const 0 = WS e o. | ||
| 75 | Proof. | ||
| 76 | intros He Ho. unfold WS. | ||
| 77 | assert (e < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). pose proof (Nat.pow_le_mono_r 2 e (e+o)). lia. } | ||
| 78 | assert (o < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). lia. } | ||
| 79 | destruct (Nat.le_ge_cases n (e+o)) as [H1|H1]. | ||
| 80 | - replace (e+o) with (n+(e+o-n)) by lia. rewrite wd_pad; auto. | ||
| 81 | - replace n with ((e+o)+(n-(e+o))) by lia. rewrite wd_pad; auto. | ||
| 82 | Qed. | ||
| 84 | Lemma WS_split e o: | ||
| 85 | WS e o = [bt e; bt o] *> WS (Nat.div2 e) (Nat.div2 o). | ||
| 86 | Proof. | ||
| 87 | rewrite <-(wd_WS (S (e+o)) e o). | ||
| 88 | 2,3: pose proof (lt_pow2_self (e+o)); pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))); lia. | ||
| 89 | cbn [wd Str_app]. | ||
| 90 | rewrite (wd_WS (e+o)). 1: reflexivity. | ||
| 91 | - rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound. | ||
| 92 | pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia. | ||
| 93 | - rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound. | ||
| 94 | pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia. | ||
| 95 | Qed. | ||
| 97 | Lemma WS_00 e o: WS (2*e) (2*o) = [0;0] *> WS e o. | ||
| 98 | Proof. rewrite WS_split, bt_even, bt_even, div2_even, div2_even. reflexivity. Qed. | ||
| 99 | Lemma WS_10 e o: WS (2*e+1) (2*o) = [1;0] *> WS e o. | ||
| 100 | Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed. | ||
| 101 | Lemma WS_01 e o: WS (2*e) (2*o+1) = [0;1] *> WS e o. | ||
| 102 | Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed. | ||
| 103 | Lemma WS_11 e o: WS (2*e+1) (2*o+1) = [1;1] *> WS e o. | ||
| 104 | Proof. rewrite WS_split, bt_odd, bt_odd, div2_odd, div2_odd. reflexivity. Qed. | ||
| 106 | Lemma WS_0x e o: WS (2*e) o = [0; bt o] *> WS e (Nat.div2 o). | ||
| 107 | Proof. rewrite WS_split, bt_even, div2_even. reflexivity. Qed. | ||
| 108 | Lemma WS_1x e o: WS (2*e+1) o = [1; bt o] *> WS e (Nat.div2 o). | ||
| 109 | Proof. rewrite WS_split, bt_odd, div2_odd. reflexivity. Qed. | ||
| 111 | (** ** The left step phi, as a relation (A scanning an E-cell / F scanning an E-cell) *) | ||
| 113 | Inductive PA : nat -> nat -> nat -> nat -> Prop := | ||
| 114 | | PA0 e o : PA (2*e) o (2*e+1) o | ||
| 115 | | PA1 e o e' o' : PA e o e' o' -> PA (2*e+1) (2*o) (2*e') (2*o') | ||
| 116 | | PA2 e o e' o' : PF e o e' o' -> PA (2*e+1) (2*o+1) (2*e') (2*o') | ||
| 117 | with PF : nat -> nat -> nat -> nat -> Prop := | ||
| 118 | | PF0 e o : PF (2*e) (2*o) (2*e) (2*o+1) | ||
| 119 | | PF1 e o e' o' : PF e o e' o' -> PF (2*e) (2*o+1) (2*e') (2*o') | ||
| 120 | | PF2 e o e' o' : PA e o e' o' -> PF (2*e+1) (2*o) (2*e') (2*o') | ||
| 121 | | PF3 e o e' o' : PF e o e' o' -> PF (2*e+1) (2*o+1) (2*e') (2*o'). | ||
| 123 | Scheme PA_mind := Induction for PA Sort Prop | ||
| 124 | with PF_mind := Induction for PF Sort Prop. | ||
| 125 | Combined Scheme PAF_mind from PA_mind, PF_mind. | ||
| 127 | Lemma TA0 l a r: [0;a] *> l <{{A}} r -->+ [1;a] *> l {{B}}> r. | ||
| 128 | Proof. es. Qed. | ||
| 129 | Lemma TA1 l r: [1;0] *> l <{{A}} r -->+ l <{{A}} [1;1] *> r. | ||
| 130 | Proof. es. Qed. | ||
| 131 | Lemma TA2 l r: [1;1] *> l <{{A}} r -->+ l <{{F}} [1;1] *> r. | ||
| 132 | Proof. es. Qed. | ||
| 133 | Lemma TF0 l r: [0;0] *> l <{{F}} r -->+ [0;1] *> l {{B}}> r. | ||
| 134 | Proof. es. Qed. | ||
| 135 | Lemma TF1 l r: [0;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r. | ||
| 136 | Proof. es. Qed. | ||
| 137 | Lemma TF2 l r: [1;0] *> l <{{F}} r -->+ l <{{A}} [1;1] *> r. | ||
| 138 | Proof. es. Qed. | ||
| 139 | Lemma TF3 l r: [1;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r. | ||
| 140 | Proof. es. Qed. | ||
| 141 | Lemma TB l r: l {{B}}> [1;1] *> r -->+ [0;0] *> l {{B}}> r. | ||
| 142 | Proof. es. Qed. | ||
| 144 | Lemma phi_spec: | ||
| 145 | (forall e o e' o', PA e o e' o' -> forall r, WS e o <{{A}} r -->+ WS e' o' {{B}}> r) /\ | ||
| 146 | (forall e o e' o', PF e o e' o' -> forall r, WS e o <{{F}} r -->+ WS e' o' {{B}}> r). | ||
| 147 | Proof. | ||
| 148 | apply PAF_mind. | ||
| 149 | all: intros. | ||
| 150 | all: try (rewrite WS_0x, WS_1x; apply TA0). | ||
| 151 | all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TA1|]; eapply progress_trans; [apply H|]; apply TB). | ||
| 152 | all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TA2|]; eapply progress_trans; [apply H|]; apply TB). | ||
| 153 | all: try (rewrite WS_00, WS_01; apply TF0). | ||
| 154 | all: try (rewrite WS_01, WS_00; eapply progress_trans; [apply TF1|]; eapply progress_trans; [apply H|]; apply TB). | ||
| 155 | all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TF2|]; eapply progress_trans; [apply H|]; apply TB). | ||
| 156 | all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TF3|]; eapply progress_trans; [apply H|]; apply TB). | ||
| 157 | Qed. | ||
| 159 | Definition PA_spec := proj1 phi_spec. | ||
| 161 | (** ** Iterates, shape lemmas *) | ||
| 163 | Inductive PAs : nat -> nat -> nat -> nat -> nat -> Prop := | ||
| 164 | | PAs0 e o : PAs 0 e o e o | ||
| 165 | | PAsS j e o e1 o1 e2 o2 : PA e o e1 o1 -> PAs j e1 o1 e2 o2 -> PAs (S j) e o e2 o2. | ||
| 167 | Lemma PA_eq e o e' o' e2 o2 e2' o2': | ||
| 168 | PA e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PA e2 o2 e2' o2'. | ||
| 169 | Proof. intros; subst; auto. Qed. | ||
| 171 | Lemma PF_eq e o e' o' e2 o2 e2' o2': | ||
| 172 | PF e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PF e2 o2 e2' o2'. | ||
| 173 | Proof. intros; subst; auto. Qed. | ||
| 175 | Lemma PAs_eq j e o e' o' j2 e2 o2 e2' o2': | ||
| 176 | PAs j e o e' o' -> j = j2 -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PAs j2 e2 o2 e2' o2'. | ||
| 177 | Proof. intros; subst; auto. Qed. | ||
| 179 | Lemma PAs_1 e o e' o': PA e o e' o' -> PAs 1 e o e' o'. | ||
| 180 | Proof. intros. econstructor; eauto. constructor. Qed. | ||
| 182 | Lemma PAs_trans j1 j2 e o e1 o1 e2 o2: | ||
| 183 | PAs j1 e o e1 o1 -> PAs j2 e1 o1 e2 o2 -> PAs (j1+j2) e o e2 o2. | ||
| 184 | Proof. | ||
| 185 | induction 1; intros; cbn; auto. | ||
| 186 | econstructor; eauto. | ||
| 187 | Qed. | ||
| 189 | Lemma PAs_split j1 j2 e o e2 o2: | ||
| 190 | PAs (j1+j2) e o e2 o2 -> exists e1 o1, PAs j1 e o e1 o1 /\ PAs j2 e1 o1 e2 o2. | ||
| 191 | Proof. | ||
| 192 | gen e o. induction j1; intros e o H. | ||
| 193 | - exists e, o. split; [constructor|auto]. | ||
| 194 | - cbn in H. inversion H; subst. | ||
| 195 | destruct (IHj1 _ _ H2) as [e3 [o3 [H3 H4]]]. | ||
| 196 | exists e3, o3. split; auto. econstructor; eauto. | ||
| 197 | Qed. | ||
| 199 | Lemma PAs_dbl j e o e' o': | ||
| 200 | PAs j e o e' o' -> PAs (2*j) (2*e) (2*o) (2*e') (2*o'). | ||
| 201 | Proof. | ||
| 202 | induction 1. | ||
| 203 | - constructor. | ||
| 204 | - replace (2 * S j) with (S (S (2*j))) by lia. | ||
| 205 | econstructor. 1: apply PA0. | ||
| 206 | econstructor. 1: apply PA1; eassumption. | ||
| 207 | assumption. | ||
| 208 | Qed. | ||
| 210 | Lemma PAs_dbl1 j e o e' o': | ||
| 211 | PAs (S j) e o e' o' -> PAs (2*j+1) (2*e+1) (2*o) (2*e') (2*o'). | ||
| 212 | Proof. | ||
| 213 | intros H. inversion H; subst. | ||
| 214 | replace (2*j+1) with (S (2*j)) by lia. | ||
| 215 | econstructor. 1: apply PA1; eassumption. | ||
| 216 | apply PAs_dbl; assumption. | ||
| 217 | Qed. | ||
| 219 | (** ** Increments *) | ||
| 221 | Lemma INC_std N: PA N 0 (N+1) 0. | ||
| 222 | Proof. | ||
| 223 | induction N as [N IH] using lt_wf_ind. | ||
| 224 | destruct (Nat.Even_or_Odd N) as [[N' HN]|[N' HN]]; subst N. | ||
| 225 | - eapply PA_eq. 1: apply (PA0 N' 0). all: lia. | ||
| 226 | - eapply PA_eq. 1: apply (PA1 N' 0 (N'+1) 0), IH. all: lia. | ||
| 227 | Qed. | ||
| 229 | Lemma INC_stds j N: PAs j N 0 (N+j) 0. | ||
| 230 | Proof. | ||
| 231 | gen N. induction j; intros N. | ||
| 232 | - eapply PAs_eq. 1: apply (PAs0 N 0). all: lia. | ||
| 233 | - econstructor. 1: apply INC_std. | ||
| 234 | eapply PAs_eq. 1: apply (IHj (N+1)). all: lia. | ||
| 235 | Qed. | ||
| 237 | Lemma PF_inc0 o: PF 0 o 0 (o+1). | ||
| 238 | Proof. | ||
| 239 | induction o as [o IH] using lt_wf_ind. | ||
| 240 | destruct (Nat.Even_or_Odd o) as [[o' Ho]|[o' Ho]]; subst o. | ||
| 241 | - eapply PF_eq. 1: apply (PF0 0 o'). all: lia. | ||
| 242 | - eapply PF_eq. 1: apply (PF1 0 o' 0 (o'+1)), IH. all: lia. | ||
| 243 | Qed. | ||
| 245 | Lemma Gap P: forall c E o1, | ||
| 246 | c+1 < 2^(S P) -> | ||
| 247 | PA (c + 2^(S P)*E) (2^P*(2*o1+1)) (c + 1 + 2^(S P)*E) (2^P*(2*o1+1)). | ||
| 248 | Proof. | ||
| 249 | induction P; intros c E o1 Hc. | ||
| 250 | - cbn in *. eapply PA_eq. 1: apply (PA0 E (2*o1+1)). all: lia. | ||
| 251 | - rewrite !Nat.pow_succ_r' in *. | ||
| 252 | destruct (Nat.Even_or_Odd c) as [[c' Hc']|[c' Hc']]; subst c. | ||
| 253 | + eapply PA_eq. 1: apply (PA0 (c' + 2*2^P*E) (2*2^P*(2*o1+1))). all: lia. | ||
| 254 | + eapply PA_eq. 1: apply (PA1 (c' + 2*2^P*E) (2^P*(2*o1+1)) (c'+1+2*2^P*E) (2^P*(2*o1+1))), IHP. | ||
| 255 | all: lia. | ||
| 256 | Qed. | ||
| 258 | Lemma Gaps P j: forall c E o1, | ||
| 259 | c+j < 2^(S P) -> | ||
| 260 | PAs j (c + 2^(S P)*E) (2^P*(2*o1+1)) (c + j + 2^(S P)*E) (2^P*(2*o1+1)). | ||
| 261 | Proof. | ||
| 262 | induction j; intros c E o1 Hc. | ||
| 263 | - eapply PAs_eq. 1: apply (PAs0 (c + 2^(S P)*E) (2^P*(2*o1+1))). all: lia. | ||
| 264 | - econstructor. 1: apply Gap; lia. | ||
| 265 | eapply PAs_eq. 1: apply (IHj (c+1) E o1). all: lia. | ||
| 266 | Qed. | ||
| 268 | Lemma F_inc h: forall E o O, | ||
| 269 | o + 1 < 2^h -> | ||
| 270 | PF (2^h*E) (o + 2^h*O) (2^h*E) (o + 1 + 2^h*O). | ||
| 271 | Proof. | ||
| 272 | induction h; intros E o O Ho. | ||
| 273 | - cbn in Ho. lia. | ||
| 274 | - rewrite !Nat.pow_succ_r' in *. | ||
| 275 | destruct (Nat.Even_or_Odd o) as [[o' Ho']|[o' Ho']]; subst o. | ||
| 276 | + eapply PF_eq. 1: apply (PF0 (2^h*E) (o' + 2^h*O)). all: lia. | ||
| 277 | + eapply PF_eq. 1: apply (PF1 (2^h*E) (o' + 2^h*O) (2^h*E) (o'+1+2^h*O)), IHh. | ||
| 278 | all: lia. | ||
| 279 | Qed. | ||
| 281 | Lemma F_carry h: forall E O E' O', | ||
| 282 | PF E O E' O' -> | ||
| 283 | PF (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O'). | ||
| 284 | Proof. | ||
| 285 | induction h; intros E O E' O' H. | ||
| 286 | - cbn. eapply PF_eq. 1: apply H. all: lia. | ||
| 287 | - rewrite !Nat.pow_succ_r' in *. | ||
| 288 | pose proof (Nat.pow_nonzero 2 h). | ||
| 289 | eapply PF_eq. 1: apply (PF1 (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O')), IHh, H. | ||
| 290 | all: lia. | ||
| 291 | Qed. | ||
| 294 | Lemma lowbit (x:nat): x <> 0%nat -> exists P o, x = 2^P*(2*o+1). | ||
| 295 | Proof. | ||
| 296 | induction x as [x IH] using lt_wf_ind. intros Hx. | ||
| 297 | destruct (Nat.Even_or_Odd x) as [[x' Hx']|[x' Hx']]; subst x. | ||
| 298 | - destruct (IH x') as [P [o Ho]]; [lia|lia|]. | ||
| 299 | exists (S P), o. rewrite Nat.pow_succ_r'. lia. | ||
| 300 | - exists 0%nat, x'. cbn. lia. | ||
| 301 | Qed. | ||
| 303 | Lemma pow_pos P: 1 <= 2^P. | ||
| 304 | Proof. pose proof (Nat.pow_nonzero 2 P). lia. Qed. | ||
| 306 | Lemma pow_odd_pos P o1: 2^P <= 2^P*(2*o1+1). | ||
| 307 | Proof. replace (2^P) with (2^P*1) at 1 by lia. apply Nat.mul_le_mono_l. lia. Qed. | ||
| 309 | Lemma pow_odd_room P o1 h: 2^P*(2*o1+1) < 2^h -> 2^P*(2*o1+1) + 2^P <= 2^h. | ||
| 310 | Proof. | ||
| 311 | intros H. | ||
| 312 | pose proof (pow_pos P). pose proof (pow_odd_pos P o1). | ||
| 313 | assert (P < h). { | ||
| 314 | destruct (Nat.lt_ge_cases P h) as [|H2]; auto. | ||
| 315 | pose proof (Nat.pow_le_mono_r 2 h P ltac:(lia) H2). lia. } | ||
| 316 | replace (2^h) with (2^P * 2^(h-P)) in *. | ||
| 317 | 2: { rewrite <-Nat.pow_add_r. f_equal. lia. } | ||
| 318 | assert (2*o1+1 < 2^(h-P)). { apply (Nat.mul_lt_mono_pos_l (2^P)); lia. } | ||
| 319 | replace (2^P*(2*o1+1) + 2^P) with (2^P*(2*o1+2)) by lia. | ||
| 320 | apply Nat.mul_le_mono_l. lia. | ||
| 321 | Qed. | ||
| 323 | (** The sweep: a low part (c, o) of h digit pairs, o = 2^P(2 o1+1), c < 2^(P+1), counts its | ||
| 324 | T-count 2o+c up to 2^(h+1); then the carry enters the high part (E,O) in F mode. *) | ||
| 325 | Lemma Sweep h: forall P o1 c E O E' O', | ||
| 326 | 2^P*(2*o1+1) < 2^h -> c < 2^(S P) -> PF E O E' O' -> | ||
| 327 | PAs (2^(S h) - 2^(S P)*(2*o1+1) - c) (c + 2^h*E) (2^P*(2*o1+1) + 2^h*O) (2^h*E') (2^h*O'). | ||
| 328 | Proof. | ||
| 329 | induction h; intros P o1 c E O E' O' Ho Hc HF. | ||
| 330 | - pose proof (pow_odd_pos P o1). cbn in Ho. lia. | ||
| 331 | - destruct P as [|P']. | ||
| 332 | + (* o odd *) | ||
| 333 | cbn [Nat.pow] in *. rewrite Nat.mul_1_l in *. | ||
| 334 | assert (H1: PAs (2^(S (S h)) - 2*(2*o1+1) - 1) (1 + 2^(S h)*E) ((2*o1+1) + 2^(S h)*O) (2^(S h)*E') (2^(S h)*O')). | ||
| 335 | { rewrite !Nat.pow_succ_r' in *. | ||
| 336 | destruct (Nat.eq_dec (o1+1) (2^h)) as [Eo|Eo]. | ||
| 337 | - apply PAs_eq with 1%nat (2*(2^h*E)+1)%nat (2*(2^h - 1 + 2^h*O)+1)%nat (2*(2^h*E'))%nat (2*(2^h*O'))%nat. | ||
| 338 | + apply PAs_1. apply PA2. apply F_carry. assumption. | ||
| 339 | + lia. | ||
| 340 | + lia. | ||
| 341 | + lia. | ||
| 342 | + lia. | ||
| 343 | + lia. | ||
| 344 | - destruct (lowbit (o1+1)) as [P2 [o2 Ho2]]; [lia|]. | ||
| 345 | pose proof (IHh P2 o2 0%nat E O E' O') as IH. | ||
| 346 | try rewrite Nat.pow_succ_r' in IH. | ||
| 347 | rewrite <-Ho2 in IH. | ||
| 348 | specialize (IH ltac:(lia) ltac:(pose proof (pow_pos P2); lia) HF). | ||
| 349 | apply PAs_dbl in IH. | ||
| 350 | apply PAs_eq with (1 + 2 * (2 * 2 ^ h - 2 * 2 ^ P2 * (2 * o2 + 1) - 0))%nat (2*(2^h*E)+1)%nat (2*(o1 + 2^h*O)+1)%nat (2*(2^h*E'))%nat (2*(2^h*O'))%nat. | ||
| 351 | + econstructor. 1: apply PA2, F_inc; lia. | ||
| 352 | eapply PAs_eq. 1: apply IH. all: lia. | ||
| 353 | + lia. | ||
| 354 | + lia. | ||
| 355 | + lia. | ||
| 356 | + lia. | ||
| 357 | + lia. } | ||
| 358 | destruct (Nat.eq_dec c 1%nat) as [->|Hc1]. | ||
| 359 | * exact H1. | ||
| 360 | * assert (c = 0%nat) as -> by lia. | ||
| 361 | apply PAs_eq with (1 + (2^(S (S h)) - 2*(2*o1+1) - 1))%nat (0 + 2^(S h)*E)%nat (2*o1+1+2^(S h)*O)%nat (2^(S h)*E')%nat (2^(S h)*O')%nat. | ||
| 362 | -- econstructor. 2: apply H1. | ||
| 363 | rewrite Nat.pow_succ_r'. eapply PA_eq. 1: apply (PA0 (2^h*E) (2*o1+1+2*2^h*O)). all: lia. | ||
| 364 | -- rewrite !Nat.pow_succ_r' in *. lia. | ||
| 365 | -- rewrite !Nat.pow_succ_r' in *. lia. | ||
| 366 | -- rewrite !Nat.pow_succ_r' in *. lia. | ||
| 367 | -- rewrite !Nat.pow_succ_r' in *. lia. | ||
| 368 | -- rewrite !Nat.pow_succ_r' in *. lia. | ||
| 369 | + (* o even *) | ||
| 370 | rewrite (Nat.pow_succ_r' 2 (S P')) in *. | ||
| 371 | rewrite (Nat.pow_succ_r' 2 P') in *. | ||
| 372 | rewrite (Nat.pow_succ_r' 2 (S h)) in *. | ||
| 373 | rewrite (Nat.pow_succ_r' 2 h) in *. | ||
| 374 | destruct (Nat.Even_or_Odd c) as [[c' Hc']|[c' Hc']]; subst c. | ||
| 375 | * pose proof (IHh P' o1 c' E O E' O') as IH. | ||
| 376 | try rewrite !Nat.pow_succ_r' in IH. | ||
| 377 | specialize (IH ltac:(lia) ltac:(lia) HF). | ||
| 378 | apply PAs_dbl in IH. | ||
| 379 | eapply PAs_eq. 1: apply IH. all: lia. | ||
| 380 | * pose proof (IHh P' o1 c' E O E' O') as IH. | ||
| 381 | try rewrite !Nat.pow_succ_r' in IH. | ||
| 382 | specialize (IH ltac:(lia) ltac:(lia) HF). | ||
| 383 | pose proof (pow_odd_pos P' o1). | ||
| 384 | pose proof (pow_odd_room P' o1 h ltac:(lia)). | ||
| 385 | remember (2 * 2 ^ h - 2 * 2 ^ P' * (2 * o1 + 1) - c') as n eqn:En. | ||
| 386 | destruct n as [|n']. 1: lia. | ||
| 387 | apply PAs_dbl1 in IH. | ||
| 388 | eapply PAs_eq. 1: apply IH. all: lia. | ||
| 389 | Qed. | ||
| 391 | (** ** The right step and the overflows *) | ||
| 393 | Lemma RS l n m: | ||
| 394 | l {{B}}> R (S n) m -->+ l <{{A}} R n (S m). | ||
| 395 | Proof. | ||
| 396 | unfold R. es. | ||
| 397 | Qed. | ||
| 399 | Lemma shift01 u (r:side): [0;1]^^u *> [0] *> r = [0] *> [1;0]^^u *> r. | ||
| 400 | Proof. | ||
| 401 | induction u. | ||
| 402 | - reflexivity. | ||
| 403 | - cbn [lpow]. rewrite !Str_app_assoc. rewrite IHu. reflexivity. | ||
| 404 | Qed. | ||
| 406 | Lemma OVe l u m: | ||
| 407 | ([0;0]^^u *> [1] *> l) {{B}}> R 0 m -->+ l <{{A}} R (1+u+m) 0. | ||
| 408 | Proof. | ||
| 409 | unfold R. es. | ||
| 410 | Qed. | ||
| 412 | Lemma OVo l u m: | ||
| 413 | ([0;0]^^u *> [0;1;0;0] *> l) {{B}}> R 0 m -->+ l <{{A}} R 0 (u+2+m). | ||
| 414 | Proof. | ||
| 415 | unfold R. es. | ||
| 416 | Qed. | ||
| 418 | Definition K e o n m := WS e o <{{A}} R n m. | ||
| 420 | (** ** Words on the tape *) | ||
| 422 | Lemma WS_shift: forall n a c, a + c < n -> WS a c = [bt a] *> WS c (Nat.div2 a). | ||
| 423 | Proof. | ||
| 424 | induction n; intros a c Hn. 1: lia. | ||
| 425 | destruct (Nat.eq_dec (a+c) 0%nat) as [E|E]. | ||
| 426 | - assert (a = 0%nat) as -> by lia. assert (c = 0%nat) as -> by lia. | ||
| 427 | unfold WS. cbn. rewrite <-const_unfold. reflexivity. | ||
| 428 | - rewrite WS_split. rewrite (WS_split c). | ||
| 429 | rewrite (IHn (Nat.div2 a) (Nat.div2 c)). | ||
| 430 | + reflexivity. | ||
| 431 | + rewrite !Nat.div2_div. | ||
| 432 | pose proof (Nat.Div0.div_le_upper_bound a 2 (a/2)). | ||
| 433 | pose proof (Nat.div_mod a 2). pose proof (Nat.div_mod c 2). | ||
| 434 | pose proof (Nat.mod_upper_bound a 2). pose proof (Nat.mod_upper_bound c 2). lia. | ||
| 435 | Qed. | ||
| 437 | Lemma WS_1 a c: WS (2*a+1) c = [1] *> WS c a. | ||
| 438 | Proof. | ||
| 439 | rewrite (WS_shift (S (2*a+1+c))) by lia. rewrite bt_odd, div2_odd. reflexivity. | ||
| 440 | Qed. | ||
| 442 | Lemma WS_pow x y u: WS (x*2^u) (y*2^u) = [0;0]^^u *> WS x y. | ||
| 443 | Proof. | ||
| 444 | induction u. | ||
| 445 | - cbn. rewrite !Nat.mul_1_r. reflexivity. | ||
| 446 | - rewrite Nat.pow_succ_r'. | ||
| 447 | replace (x*(2*2^u)) with (2*(x*2^u)) by lia. | ||
| 448 | replace (y*(2*2^u)) with (2*(y*2^u)) by lia. | ||
| 449 | rewrite WS_00, IHu. cbn [lpow]. rewrite Str_app_assoc. reflexivity. | ||
| 450 | Qed. | ||
| 452 | (** ** Composite rules on K configurations *) | ||
| 454 | Lemma bounces j e o e' o' n m: | ||
| 455 | PAs j e o e' o' -> K e o (j+n) m -->* K e' o' n (j+m). | ||
| 456 | Proof. | ||
| 457 | intros H. gen n m. induction H; intros n m. | ||
| 458 | - finish. | ||
| 459 | - apply evstep_trans with (K e1 o1 (j+n) (S m)). | ||
| 460 | + apply progress_evstep. unfold K. | ||
| 461 | eapply progress_trans. 1: apply PA_spec; eassumption. | ||
| 462 | cbn [Nat.add]. apply RS. | ||
| 463 | + eapply evstep_trans. 1: apply IHPAs. finish. | ||
| 464 | Qed. | ||
| 466 | Lemma OV_even e o a c u m: | ||
| 467 | PA e o ((2*a+1)*2^u) (c*2^u) -> K e o 0 m -->+ K c a (1+u+m) 0. | ||
| 468 | Proof. | ||
| 469 | intros H. unfold K. | ||
| 470 | eapply progress_trans. 1: apply PA_spec, H. | ||
| 471 | rewrite WS_pow, WS_1. | ||
| 472 | apply OVe. | ||
| 473 | Qed. | ||
| 475 | Lemma OV_odd e o a c u m: | ||
| 476 | PA e o (c*2^(u+2)) ((4*a+1)*2^u) -> K e o 0 m -->+ K c a 0 (u+2+m). | ||
| 477 | Proof. | ||
| 478 | intros H. unfold K. | ||
| 479 | eapply progress_trans. 1: apply PA_spec, H. | ||
| 480 | replace (c*2^(u+2)) with ((2*(2*c))*2^u) by (rewrite Nat.pow_add_r; cbn; lia). | ||
| 481 | replace (4*a+1) with (2*(2*a)+1) by lia. | ||
| 482 | rewrite WS_pow, WS_01, WS_00. | ||
| 483 | apply OVo. | ||
| 484 | Qed. | ||
| 486 | (** ** Packed counter *) | ||
| 488 | Definition pkE N := N - 2^(Nat.log2 N). | ||
| 489 | Definition pkO N := 2^(Nat.log2 N - 1). | ||
| 491 | Lemma pk_eq P N: 2^(S P) <= N < 2^(S (S P)) -> pkE N = N - 2^(S P) /\ pkO N = 2^P. | ||
| 492 | Proof. | ||
| 493 | intros H. unfold pkE, pkO. | ||
| 494 | rewrite (Nat.log2_unique N (S P)); [|lia|lia]. | ||
| 495 | split; [reflexivity|]. f_equal. lia. | ||
| 496 | Qed. | ||
| 498 | Lemma PAs_1_inv e o e2 o2: PAs 1 e o e2 o2 -> PA e o e2 o2. | ||
| 499 | Proof. | ||
| 500 | intros H. inversion H as [|j' e' o' e1 o1 e3 o3 HA HB]; subst. | ||
| 501 | inversion HB; subst. assumption. | ||
| 502 | Qed. | ||
| 504 | Lemma PAs_last j e o e2 o2: | ||
| 505 | PAs (S j) e o e2 o2 -> exists e1 o1, PAs j e o e1 o1 /\ PA e1 o1 e2 o2. | ||
| 506 | Proof. | ||
| 507 | intros H. replace (S j) with (j+1) in H by lia. | ||
| 508 | destruct (PAs_split _ _ _ _ _ _ H) as [e1 [o1 [H1 H2]]]. | ||
| 509 | exists e1, o1. split; auto. apply PAs_1_inv, H2. | ||
| 510 | Qed. | ||
| 512 | Lemma INC_pk N: 2 <= N -> PA (pkE N) (pkO N) (pkE (S N)) (pkO (S N)). | ||
| 513 | Proof. | ||
| 514 | intros HN. | ||
| 515 | pose proof (Nat.log2_spec N ltac:(lia)) as HL. | ||
| 516 | assert (Hl1: 1 <= Nat.log2 N). { pose proof (Nat.log2_le_mono 2 N HN) as Hm. cbn in Hm. lia. } | ||
| 517 | remember (Nat.log2 N - 1) as P. | ||
| 518 | replace (Nat.log2 N) with (S P) in HL by lia. | ||
| 519 | destruct (pk_eq P N HL) as [E1 E2]. rewrite E1, E2. | ||
| 520 | rewrite (Nat.pow_succ_r' 2 (S P)) in HL. | ||
| 521 | destruct (Nat.eq_dec (S N) (2^(S (S P)))) as [Ec|Ec]. | ||
| 522 | - destruct (pk_eq (S P) (S N)) as [E3 E4]. | ||
| 523 | { rewrite ?Nat.pow_succ_r' in *. lia. } | ||
| 524 | rewrite E3, E4. | ||
| 525 | pose proof (Sweep (S P) P 0 (2^(S P) - 1) 0 0 0 1) as H. | ||
| 526 | specialize (H ltac:(rewrite ?Nat.pow_succ_r' in *; lia) ltac:(lia) (PF0 0 0)). | ||
| 527 | apply PAs_1_inv. | ||
| 528 | eapply PAs_eq. 1: apply H. all: rewrite ?Nat.pow_succ_r' in *; lia. | ||
| 529 | - destruct (pk_eq P (S N)) as [E3 E4]. | ||
| 530 | { rewrite ?Nat.pow_succ_r' in *. lia. } | ||
| 531 | rewrite E3, E4. | ||
| 532 | pose proof (Gap P (N - 2^(S P)) 0 0) as H. | ||
| 533 | specialize (H ltac:(rewrite ?(Nat.pow_succ_r' 2 (S P)) in *; lia)). | ||
| 534 | eapply PA_eq. 1: apply H. all: lia. | ||
| 535 | Qed. | ||
| 537 | Lemma INC_pks j N: 2 <= N -> PAs j (pkE N) (pkO N) (pkE (N+j)) (pkO (N+j)). | ||
| 538 | Proof. | ||
| 539 | gen N. induction j; intros N HN. | ||
| 540 | - eapply PAs_eq. 1: apply (PAs0 (pkE N) (pkO N)). all: f_equal; lia. | ||
| 541 | - econstructor. 1: apply INC_pk; lia. | ||
| 542 | eapply PAs_eq. 1: apply (IHj (S N)); lia. all: f_equal; lia. | ||
| 543 | Qed. | ||
| 545 | (** ** Macro rules (proof.md 3.4). l is bitlen(k)-1, b = 1+i+m. *) | ||
| 547 | Lemma bounces0 j e o e' o' m: | ||
| 548 | PAs j e o e' o' -> K e o j m -->* K e' o' 0 (j+m). | ||
| 549 | Proof. | ||
| 550 | intros H. pose proof (bounces j e o e' o' 0 m H) as H1. | ||
| 551 | rewrite Nat.add_0_r in H1. exact H1. | ||
| 552 | Qed. | ||
| 554 | Lemma OVB e o a c u m e' o': | ||
| 555 | PA e o ((2*a+1)*2^u) (c*2^u) -> | ||
| 556 | PAs (1+u+m) c a e' o' -> | ||
| 557 | K e o 0 m -->+ K e' o' 0 (1+u+m). | ||
| 558 | Proof. | ||
| 559 | intros H1 H2. eapply progress_evstep_trans. 1: apply OV_even, H1. | ||
| 560 | eapply evstep_trans. 1: apply bounces0, H2. | ||
| 561 | finish. | ||
| 562 | Qed. | ||
| 564 | Lemma std_ov k i: PA ((2*k+1)*2^i-1) 0 ((2*k+1)*2^i) (0*2^i). | ||
| 565 | Proof. | ||
| 566 | pose proof (pow_pos i). | ||
| 567 | eapply PA_eq. 1: apply (INC_std ((2*k+1)*2^i-1)). all: nia. | ||
| 568 | Qed. | ||
| 570 | Lemma BS_S0 i m: K (2^i-1) 0 0 m -->+ K (1+i+m) 0 0 (1+i+m). | ||
| 571 | Proof. | ||
| 572 | apply OVB with (a:=0%nat) (c:=0%nat). | ||
| 573 | - pose proof (std_ov 0 i). eapply PA_eq. 1: apply H. all: lia. | ||
| 574 | - eapply PAs_eq. 1: apply (INC_stds (1+i+m) 0). all: lia. | ||
| 575 | Qed. | ||
| 577 | Lemma OVoS0 e o u m: PA e o 0 (2^u) -> K e o 0 m -->+ K (u+3+m) 0 0 (u+3+m). | ||
| 578 | Proof. | ||
| 579 | intros H. | ||
| 580 | eapply progress_trans. 1: apply (OV_odd e o 0 0 u m). | ||
| 581 | - eapply PA_eq. 1: apply H. all: lia. | ||
| 582 | - pose proof (BS_S0 0 (u+2+m)) as H1. cbn in H1. | ||
| 583 | eapply progress_evstep_trans. 1: apply H1. finish. | ||
| 584 | Qed. | ||
| 586 | Lemma BS_S1a l k i m: | ||
| 587 | k = 2^l -> | ||
| 588 | K ((2*k+1)*2^i-1) 0 0 m -->+ K (pkE (2*k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m). | ||
| 589 | Proof. | ||
| 590 | intros Hk. | ||
| 591 | apply OVB with (a:=k) (c:=0%nat). | ||
| 592 | 1: apply std_ov. | ||
| 593 | destruct (pk_eq l (2^(S l))) as [E1 E2]. | ||
| 594 | { rewrite !Nat.pow_succ_r'. pose proof (pow_pos l). lia. } | ||
| 595 | eapply PAs_eq. 1: apply (INC_pks (1+i+m) (2^(S l))). | ||
| 596 | - rewrite Nat.pow_succ_r'. pose proof (pow_pos l). lia. | ||
| 597 | - reflexivity. | ||
| 598 | - rewrite E1. lia. | ||
| 599 | - rewrite E2. lia. | ||
| 600 | - f_equal. rewrite Nat.pow_succ_r'. lia. | ||
| 601 | - f_equal. rewrite Nat.pow_succ_r'. lia. | ||
| 602 | Qed. | ||
| 604 | (** sweep of W(0,k), k < 2^(l+1), into pk(2^(l+2)) *) | ||
| 605 | Lemma O3_merge l k: | ||
| 606 | 1 <= k < 2^(S l) -> | ||
| 607 | PAs (2^(S (S l)) - 2*k) 0 k (pkE (2^(S (S l)))) (pkO (2^(S (S l)))). | ||
| 608 | Proof. | ||
| 609 | intros Hk. | ||
| 610 | destruct (lowbit k) as [P [o1 Ho]]; [lia|]. | ||
| 611 | pose proof (Sweep (S l) P o1 0 0 0 0 1) as H. | ||
| 612 | specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF0 0 0)). | ||
| 613 | destruct (pk_eq (S l) (2^(S (S l)))) as [E1 E2]. | ||
| 614 | { rewrite !(Nat.pow_succ_r' 2 (S _)). pose proof (pow_pos (S l)). lia. } | ||
| 615 | rewrite E1, E2. | ||
| 616 | eapply PAs_eq. 1: apply H. all: rewrite ?Nat.pow_succ_r' in *; lia. | ||
| 617 | Qed. | ||
| 619 | Lemma BS_S1b l k i m: | ||
| 620 | 2^l <= k < 2^(S l) -> | ||
| 621 | 2^(S (S l)) <= 2*k+(1+i+m) -> | ||
| 622 | K ((2*k+1)*2^i-1) 0 0 m -->+ K (pkE (2*k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m). | ||
| 623 | Proof. | ||
| 624 | intros Hk Hb. | ||
| 625 | pose proof (pow_pos l). | ||
| 626 | apply OVB with (a:=k) (c:=0%nat). | ||
| 627 | 1: apply std_ov. | ||
| 628 | pose proof (O3_merge l k ltac:(lia)) as H1. | ||
| 629 | pose proof (INC_pks (2*k+(1+i+m)-2^(S (S l))) (2^(S (S l)))) as H2. | ||
| 630 | specialize (H2 ltac:(rewrite !Nat.pow_succ_r'; lia)). | ||
| 631 | pose proof (PAs_trans _ _ _ _ _ _ _ _ H1 H2) as H3. | ||
| 632 | eapply PAs_eq. 1: apply H3. all: try reflexivity. | ||
| 633 | - rewrite !(Nat.pow_succ_r' 2 (S _)) in *. rewrite !Nat.pow_succ_r' in *. lia. | ||
| 634 | - f_equal. lia. | ||
| 635 | - f_equal. lia. | ||
| 636 | Qed. | ||
| 638 | Lemma BS_S2 l k i m: | ||
| 639 | 2^l <= k < 2^(S l) -> | ||
| 640 | 2*k+(1+i+m)+1 = 2^(S (S l)) -> | ||
| 641 | K ((2*k+1)*2^i-1) 0 0 m -->+ K (l+4+(1+i+m)) 0 0 (l+4+(1+i+m)). | ||
| 642 | Proof. | ||
| 643 | intros Hk Hb. | ||
| 644 | pose proof (pow_pos l). | ||
| 645 | pose proof (O3_merge l k ltac:(lia)) as H1. | ||
| 646 | destruct (pk_eq (S l) (2^(S (S l)))) as [E1 E2]. | ||
| 647 | { rewrite !(Nat.pow_succ_r' 2 (S _)). pose proof (pow_pos (S l)). lia. } | ||
| 648 | rewrite E1, E2 in H1. | ||
| 649 | replace (2 ^ S (S l) - 2 * k) with (S (1+i+m)) in H1 by lia. | ||
| 650 | destruct (PAs_last _ _ _ _ _ H1) as [e1 [o1 [H2 H3]]]. | ||
| 651 | eapply progress_trans. 1: apply OV_even with (a:=k) (c:=0%nat) (u:=i), std_ov. | ||
| 652 | eapply evstep_progress_trans. 1: apply bounces0, H2. | ||
| 653 | eapply progress_evstep_trans. 1: apply (OVoS0 _ _ (S l)). | ||
| 654 | - eapply PA_eq. 1: apply H3. all: lia. | ||
| 655 | - finish. | ||
| 656 | Qed. | ||
| 658 | Lemma pk_ov_full i: 2 <= i -> | ||
| 659 | PA (pkE (2^i-1)) (pkO (2^i-1)) 0 (2^(i-1)). | ||
| 660 | Proof. | ||
| 661 | intros Hi. | ||
| 662 | pose proof (INC_pk (2^i-1)) as H. | ||
| 663 | assert (4 <= 2^i). { pose proof (Nat.pow_le_mono_r 2 2 i ltac:(lia) Hi). cbn in H0. lia. } | ||
| 664 | specialize (H ltac:(lia)). | ||
| 665 | replace (S (2^i-1)) with (2^i) in H by lia. | ||
| 666 | destruct (pk_eq (i-1) (2^i)) as [E1 E2]. | ||
| 667 | { replace (S (i-1)) with i by lia. split; [lia | apply Nat.pow_lt_mono_r; lia]. } | ||
| 668 | rewrite E1, E2 in H. | ||
| 669 | eapply PA_eq. 1: apply H. all: try reflexivity. | ||
| 670 | replace (S (i-1)) with i by lia. lia. | ||
| 671 | Qed. | ||
| 673 | Lemma BS_P0 i m: 2 <= i -> | ||
| 674 | K (pkE (2^i-1)) (pkO (2^i-1)) 0 m -->+ K (2+i+m) 0 0 (2+i+m). | ||
| 675 | Proof. | ||
| 676 | intros Hi. | ||
| 677 | eapply progress_evstep_trans. 1: apply (OVoS0 _ _ (i-1)), pk_ov_full, Hi. | ||
| 678 | finish. | ||
| 679 | Qed. | ||
| 681 | (** pk(N) with N+1 = (2k+1) 2^i, 2^l <= k < 2^(l+1), k = 2^l + r: overflow gives W(2^l, r) *) | ||
| 682 | Lemma pk_ov l r i: | ||
| 683 | r < 2^l -> | ||
| 684 | PA (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) ((2*r+1)*2^i) (2^l*2^i). | ||
| 685 | Proof. | ||
| 686 | intros Hr. | ||
| 687 | pose proof (pow_pos l). pose proof (pow_pos i). | ||
| 688 | destruct (pk_eq (l+i) ((2*(2^l+r)+1)*2^i-1)) as [E1 E2]. | ||
| 689 | { rewrite !Nat.pow_succ_r', Nat.pow_add_r. nia. } | ||
| 690 | rewrite E1, E2. | ||
| 691 | pose proof (Gap (l+i) ((2*r+1)*2^i-1) 0 0) as HG. | ||
| 692 | specialize (HG ltac:(rewrite !Nat.pow_succ_r', Nat.pow_add_r; nia)). | ||
| 693 | eapply PA_eq. 1: apply HG. | ||
| 694 | all: rewrite ?Nat.pow_succ_r', ?Nat.pow_add_r; nia. | ||
| 695 | Qed. | ||
| 697 | Lemma BS_P1 l i m: | ||
| 698 | K (pkE ((2*(2^l+0)+1)*2^i-1)) (pkO ((2*(2^l+0)+1)*2^i-1)) 0 m -->+ K (2^l+(1+i+m)) 0 0 (1+i+m). | ||
| 699 | Proof. | ||
| 700 | apply OVB with (a:=0%nat) (c:=2^l). | ||
| 701 | 1: apply pk_ov; apply pow_pos. | ||
| 702 | eapply PAs_eq. 1: apply (INC_stds (1+i+m) (2^l)). all: lia. | ||
| 703 | Qed. | ||
| 705 | Lemma BS_P2 l r i m: | ||
| 706 | 1 <= r < 2^l -> | ||
| 707 | 2^(S l) <= 2*r+(1+i+m) -> | ||
| 708 | K (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) 0 m -->+ K (2*r+(1+i+m)) 0 0 (1+i+m). | ||
| 709 | Proof. | ||
| 710 | intros Hr Hb. | ||
| 711 | apply OVB with (a:=r) (c:=2^l). | ||
| 712 | 1: apply pk_ov; lia. | ||
| 713 | destruct (lowbit r) as [P [o1 Ho]]; [lia|]. | ||
| 714 | pose proof (Sweep l P o1 0 1 0 2 0) as H. | ||
| 715 | specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)). | ||
| 716 | specialize (H (PF2 0 0 1 0 (PA0 0 0))). | ||
| 717 | rewrite !Nat.mul_0_r in H. | ||
| 718 | pose proof (INC_stds (2*r+(1+i+m)-2^(S l)) (2^l*2)) as H2. | ||
| 719 | pose proof (PAs_trans _ _ _ _ _ _ _ _ H H2) as H3. | ||
| 720 | eapply PAs_eq. 1: apply H3. all: rewrite ?Nat.pow_succ_r' in *; lia. | ||
| 721 | Qed. | ||
| 723 | Lemma BS_P3 l r i m: | ||
| 724 | 1 <= r < 2^l -> | ||
| 725 | 2*r+(1+i+m)+1 = 2^(S l) -> | ||
| 726 | K (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) 0 m -->+ K (l+2+(1+i+m)) 0 0 (l+2+(1+i+m)). | ||
| 727 | Proof. | ||
| 728 | intros Hr Hb. | ||
| 729 | destruct (lowbit r) as [P [o1 Ho]]; [lia|]. | ||
| 730 | pose proof (Sweep l P o1 0 1 0 2 0) as H. | ||
| 731 | specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)). | ||
| 732 | specialize (H (PF2 0 0 1 0 (PA0 0 0))). | ||
| 733 | replace (2 ^ S l - 2 ^ S P * (2 * o1 + 1) - 0) with (S (1+i+m)) in H by (rewrite ?Nat.pow_succ_r' in *; lia). | ||
| 734 | destruct (PAs_last _ _ _ _ _ H) as [e1 [o1' [H2 H3]]]. | ||
| 735 | eapply progress_trans. 1: apply OV_even with (a:=r) (c:=2^l) (u:=i), pk_ov; lia. | ||
| 736 | eapply evstep_progress_trans. | ||
| 737 | 1: { eapply bounces0. eapply PAs_eq. 1: apply H2. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. } | ||
| 738 | eapply progress_evstep_trans. 1: apply OV_even with (a:=0%nat) (c:=0%nat) (u:=S l). | ||
| 739 | - eapply PA_eq. 1: apply H3. all: rewrite ?Nat.pow_succ_r' in *; lia. | ||
| 740 | - eapply evstep_trans. 1: apply bounces0, (INC_stds _ 0). | ||
| 741 | finish. | ||
| 742 | Qed. | ||
| 744 | Lemma PAs_trans_eq j1 j2 e o e1 o1 e1' o1' e2 o2: | ||
| 745 | PAs j1 e o e1 o1 -> PAs j2 e1' o1' e2 o2 -> e1 = e1' -> o1 = o1' -> PAs (j1+j2) e o e2 o2. | ||
| 746 | Proof. intros H1 H2 -> ->. eapply PAs_trans; eauto. Qed. | ||
| 748 | (** S3 / P4: the gen-1 orbit stops in its final gap at T = 2^(l+1) + v (resp. 2^l + v), | ||
| 749 | v = 2^u (2g+1), l = S (h+u); the overflow then leaves the gen-2 word *) | ||
| 750 | Lemma S3_pre h u r g i m: | ||
| 751 | 1 <= r < 2^(h+u) -> g < 2^h -> | ||
| 752 | 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) -> | ||
| 753 | K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (3*2^h) g (1+u+(1+i+m)) 0. | ||
| 754 | Proof. | ||
| 755 | intros Hr Hg Hb. | ||
| 756 | pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu. | ||
| 757 | assert (E1: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r. | ||
| 758 | destruct (lowbit r) as [P [o1 Ho]]; [lia|]. | ||
| 759 | pose proof (Sweep (h+u) P o1 0 0 2 0 3) as H1. | ||
| 760 | specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF_inc0 2)). | ||
| 761 | pose proof (Gaps (h+u) (2^u*(2*g+1)) 0 0 1) as H2. | ||
| 762 | specialize (H2 ltac:(rewrite Nat.pow_succ_r', E1; nia)). | ||
| 763 | pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(lia) ltac:(lia)) as H3. | ||
| 764 | assert (Hj: (2 ^ S (h+u) - 2 ^ S P * (2 * o1 + 1) - 0) + 2^u*(2*g+1) = S (1+i+m)). | ||
| 765 | { rewrite ?Nat.pow_succ_r' in *. lia. } | ||
| 766 | rewrite Hj in H3. | ||
| 767 | destruct (PAs_last _ _ _ _ _ H3) as [e1 [o2 [H4 H5]]]. | ||
| 768 | eapply progress_trans. 1: apply OV_even with (a:=(2^(S (h+u))+r)) (c:=0%nat) (u:=i), std_ov. | ||
| 769 | eapply evstep_progress_trans. | ||
| 770 | 1: { eapply bounces0. eapply PAs_eq. 1: apply H4. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. } | ||
| 771 | eapply progress_evstep_trans. 1: apply OV_even with (a:=g) (c:=3*2^h) (u:=u). | ||
| 772 | - eapply PA_eq. 1: apply H5. all: rewrite ?Nat.pow_succ_r' in *; nia. | ||
| 773 | - finish. | ||
| 774 | Qed. | ||
| 776 | Lemma BS_S3a h u r i m: | ||
| 777 | 1 <= r < 2^(h+u) -> | ||
| 778 | 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u -> | ||
| 779 | K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (3*2^h+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)). | ||
| 780 | Proof. | ||
| 781 | intros Hr Hb. | ||
| 782 | eapply progress_evstep_trans. 1: apply (S3_pre h u r 0 i m); [lia|apply pow_pos|lia]. | ||
| 783 | eapply evstep_trans. 1: apply bounces0, (INC_stds _ (3*2^h)). | ||
| 784 | finish. | ||
| 785 | Qed. | ||
| 787 | Lemma BS_S3b h u r g i m: | ||
| 788 | 1 <= r < 2^(h+u) -> 1 <= g < 2^h -> | ||
| 789 | 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) -> | ||
| 790 | 2^(S h) <= 2*g + (1+u+(1+i+m)) -> | ||
| 791 | K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (2^(S h)+2*g+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)). | ||
| 792 | Proof. | ||
| 793 | intros Hr Hg Hb Hn. | ||
| 794 | eapply progress_evstep_trans. 1: apply (S3_pre h u r g i m); lia. | ||
| 795 | destruct (lowbit g) as [P [o1 Ho]]; [lia|]. | ||
| 796 | pose proof (Sweep h P o1 0 3 0 4 0) as H1. | ||
| 797 | specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)). | ||
| 798 | specialize (H1 (PF_eq _ _ _ _ _ _ _ _ (PF2 1 0 2 0 (PA_eq _ _ _ _ _ _ _ _ (PA1 0 0 1 0 (PA0 0 0)) eq_refl eq_refl eq_refl eq_refl)) eq_refl eq_refl eq_refl eq_refl)). | ||
| 799 | pose proof (INC_stds (2*g+(1+u+(1+i+m)) - 2^(S h)) (2^h*4)) as H2. | ||
| 800 | pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 eq_refl ltac:(lia)) as H3. | ||
| 59 | eapply evstep_trans. | 801 | eapply evstep_trans. |
| 60 | 1: apply progress_evstep. | ||
| 802 | 1: { eapply bounces0. eapply PAs_eq. 1: apply H3. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. } | ||
| 61 | 1: apply LBinInc_spec with (qL:=[]) (qR:=[]); es. | ||
| 803 | apply evstep_refl'. f_equal; rewrite ?Nat.pow_succ_r' in *; lia. | ||
| 62 | er. | ||
| 63 | Qed. | 804 | Qed. |
| 65 | Lemma LIncs n: | ||
| 806 | Lemma P4_pre h u r g i m: | ||
| 66 | sideRLs tm' (hLR^^n) (LC0 0) (LC0 n). | ||
| 807 | 1 <= r < 2^(h+u) -> g < 2^h -> | ||
| 808 | 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) -> | ||
| 809 | K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+ | ||
| 810 | K (2^h) (2^h+g) (1+u+(1+i+m)) 0. | ||
| 67 | Proof. | 811 | Proof. |
| 68 | induction n. | ||
| 812 | intros Hr Hg Hb. | ||
| 69 | - esx. | ||
| 813 | pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu. | ||
| 70 | - replace (S n) with (n+1) by lia. | ||
| 814 | assert (E1: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r. | ||
| 71 | rewrite lpow_add. | ||
| 815 | destruct (lowbit r) as [P [o1 Ho]]; [lia|]. | ||
| 72 | eapply sideRLs_trans. | ||
| 816 | pose proof (Sweep (h+u) P o1 0 2 0 2 1) as H1. | ||
| 73 | 1: apply IHn. | ||
| 817 | specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF0 1 0)). | ||
| 74 | lowbitS_cases n. | ||
| 818 | pose proof (Gaps (h+u) (2^u*(2*g+1)) 0 1 0) as H2. | ||
| 75 | rewrite Nat.sub_add by lia. | ||
| 819 | specialize (H2 ltac:(rewrite Nat.pow_succ_r', E1; nia)). | ||
| 76 | unfold LC0. | ||
| 820 | pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(rewrite ?Nat.pow_succ_r'; lia) ltac:(lia)) as H3. | ||
| 77 | rw_Bin. | ||
| 821 | assert (Hj: (2 ^ S (h+u) - 2 ^ S P * (2 * o1 + 1) - 0) + 2^u*(2*g+1) = S (1+i+m)). | ||
| 78 | esx. | ||
| 822 | { rewrite ?Nat.pow_succ_r' in *. lia. } | ||
| 823 | rewrite Hj in H3. | ||
| 824 | destruct (PAs_last _ _ _ _ _ H3) as [e1 [o2 [H4 H5]]]. | ||
| 825 | eapply progress_trans. 1: apply OV_even with (a:=r) (c:=2^(S (h+u))) (u:=i), pk_ov; rewrite ?Nat.pow_succ_r'; lia. | ||
| 826 | eapply evstep_progress_trans. | ||
| 827 | 1: { eapply bounces0. eapply PAs_eq. 1: apply H4. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. } | ||
| 828 | eapply progress_evstep_trans. 1: apply OV_even with (a:=2^h+g) (c:=2^h) (u:=u). | ||
| 829 | - eapply PA_eq. 1: apply H5. all: rewrite ?Nat.pow_succ_r' in *; nia. | ||
| 830 | - finish. | ||
| 79 | Qed. | 831 | Qed. |
| 81 | Lemma LIncs' n: | ||
| 833 | Lemma BS_P4a h u r i m: | ||
| 82 | sideRLs tm' (hLR^^(n*2)) (LC0 n <* [0]) (LC0 0). | ||
| 834 | 1 <= r < 2^(h+u) -> | ||
| 835 | 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u -> | ||
| 836 | K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+ | ||
| 837 | K (pkE (3*2^h+(1+u+(1+i+m)))) (pkO (3*2^h+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)). | ||
| 83 | Proof. | 838 | Proof. |
| 84 | unfold LC0. | ||
| 839 | intros Hr Hb. | ||
| 85 | induction n using lt_wf_ind. | ||
| 840 | pose proof (pow_pos h) as Ph. | ||
| 86 | divmod2_cases n. | ||
| 841 | eapply progress_evstep_trans. 1: apply (P4_pre h u r 0 i m); [lia|apply pow_pos|lia]. | ||
| 87 | - destruct (Nat.eqb_spec n' 0). | ||
| 842 | destruct (pk_eq h (3*2^h)) as [E1 E2]. { rewrite !Nat.pow_succ_r'. lia. } | ||
| 88 | + subst. | ||
| 843 | pose proof (INC_pks (1+u+(1+i+m)) (3*2^h)) as H1. | ||
| 89 | esx. | ||
| 844 | specialize (H1 ltac:(lia)). rewrite E1, E2 in H1. | ||
| 90 | + unshelve epose proof (H n' _) as H. | ||
| 845 | eapply evstep_trans. | ||
| 91 | 1: lia. | ||
| 846 | 1: { eapply bounces0. eapply PAs_eq. 1: apply H1. 4,5: reflexivity. all: rewrite ?Nat.pow_succ_r' in *; lia. } | ||
| 92 | rw_Bin. | ||
| 847 | finish. | ||
| 93 | replace 0inf with ([0;0]*>0inf) by solve_const0_eq. | ||
| 94 | eapply @segRLs_sideRLs_concat with (w1:=[0;0]). | ||
| ⋯ 9 template-only lines (template 95–103), not in ours | |||
| 104 | replace ((n'*2+1)*2) with (n'*2*2+2) by lia. | ||
| 105 | apply segRLs_addmul''; esx. | ||
| 106 | Qed. | 848 | Qed. |
| 108 | Lemma RIncs n m: | ||
| 850 | Lemma BS_P4b h u r g i m: | ||
| 109 | sideRLs tm (hRL^^n) (R n m) (R 0 (n+m)). | ||
| 851 | 1 <= r < 2^(h+u) -> 1 <= g < 2^h -> | ||
| 852 | 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) -> | ||
| 853 | 2^(S h) <= 2*g + (1+u+(1+i+m)) -> | ||
| 854 | K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+ | ||
| 855 | K (pkE (2^(S h)+2*g+(1+u+(1+i+m)))) (pkO (2^(S h)+2*g+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)). | ||
| 110 | Proof. | 856 | Proof. |
| 111 | gen m. | ||
| 857 | intros Hr Hg Hb Hn. | ||
| 112 | induction n; intros. | ||
| 858 | pose proof (pow_pos h) as Ph. | ||
| 113 | - esx. | ||
| 859 | eapply progress_evstep_trans. 1: apply (P4_pre h u r g i m); lia. | ||
| 114 | - replace (S n) with (1+n) by lia. | ||
| 860 | destruct (lowbit g) as [P [o1 Ho]]; [lia|]. | ||
| 115 | rewrite lpow_add. | ||
| 861 | pose proof (Sweep h P o1 0 1 1 0 2) as H1. | ||
| 116 | eapply sideRLs_trans. | ||
| 862 | specialize (H1 ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)). | ||
| 117 | 2: applys_eq (IHn (1+m)); flia. | ||
| 863 | specialize (H1 (PF_eq _ _ _ _ _ _ _ _ (PF3 0 0 0 1 (PF0 0 0)) eq_refl eq_refl eq_refl eq_refl)). | ||
| 118 | esx. | ||
| 864 | destruct (pk_eq (S h) (2^(S (S h)))) as [E1 E2]. | ||
| 865 | { rewrite !Nat.pow_succ_r'. lia. } | ||
| 866 | pose proof (INC_pks (2*g+(1+u+(1+i+m)) - 2^(S h)) (2^(S (S h)))) as H2. | ||
| 867 | specialize (H2 ltac:(rewrite !Nat.pow_succ_r'; lia)). | ||
| 868 | rewrite E1, E2 in H2. | ||
| 869 | pose proof (PAs_trans_eq _ _ _ _ _ _ _ _ _ _ H1 H2 ltac:(rewrite !Nat.pow_succ_r'; lia) ltac:(rewrite !Nat.pow_succ_r'; lia)) as H3. | ||
| 870 | eapply evstep_trans. | ||
| 871 | 1: { eapply bounces0. eapply PAs_eq. 1: apply H3. 4,5: try reflexivity. | ||
| 872 | all: try (f_equal; rewrite ?Nat.pow_succ_r' in *; lia). | ||
| 873 | all: rewrite ?Nat.pow_succ_r' in *; lia. } | ||
| 874 | apply evstep_refl'. rewrite Nat.add_0_r. f_equal; f_equal; rewrite ?Nat.pow_succ_r' in *; lia. | ||
| 119 | Qed. | 875 | Qed. |
| 121 | Lemma ROv k i m: | ||
| 877 | (** ** Invariant (proof.md 4.1) and the main induction *) | ||
| 122 | LC0 ((k*2+1)*2^i-1) <| R 0 m -->+ | ||
| 879 | Definition St (s : bool * nat * nat) : Q * tape := | ||
| 123 | LC0 k <* [0] <| R (1+i+m) 0. | ||
| 880 | let '(t, N, m) := s in if t then K (pkE N) (pkO N) 0 m else K N 0 0 m. | ||
| 882 | Definition I (s : bool * nat * nat) : Prop := | ||
| 883 | let '(t, N, m) := s in | ||
| 884 | 1 <= m <= N /\ (t = true -> 2 <= N) /\ | ||
| 885 | (if Nat.even (N + m) then | ||
| 886 | (if t then (if Nat.even N then N <= 2*m+3 else 2*N <= 5*m+6) | ||
| 887 | else (if Nat.even N then 2*N <= 3*m+6 else N <= 2*m+3)) | ||
| 888 | else N <= m+3). | ||
| 890 | Lemma init0: c0 -->* K 1 0 0 1. | ||
| 124 | Proof. | 891 | Proof. |
| 125 | unfold LC0,R. | ||
| 892 | unfold K. replace (WS 1 0) with ([1] *> const 0). | ||
| 126 | rw_Bin. | ||
| 893 | 2: { unfold WS. cbn. rewrite <-const_unfold. reflexivity. } | ||
| 127 | es. | ||
| 894 | unfold R. esx. | ||
| 128 | Qed. | 895 | Qed. |
| 130 | Definition S '(a,b) := LC0 a <| R 0 b. | ||
| 897 | (** ** Coverage and closure (proof.md 4.2 Lemma S, 4.3 Lemma C) *) | ||
| 132 | Lemma BigStep k i m: | ||
| 899 | Local Open Scope nat_scope. | ||
| 133 | k*2<=(1+i+m) -> | ||
| 901 | Lemma St_std N m: St (false, N, m) = K N 0 0 m. | ||
| 134 | S ((k*2+1)*2^i-1,m) -->+ | ||
| 902 | Proof. reflexivity. Qed. | ||
| 135 | S (1+i+m-k*2,1+i+m). | ||
| 904 | Lemma St_pk N m: St (true, N, m) = K (pkE N) (pkO N) 0 m. | ||
| 905 | Proof. reflexivity. Qed. | ||
| 907 | Lemma even_mod x: Nat.even x = true -> x mod 2 = 0. | ||
| 908 | Proof. intros H. apply Nat.even_spec in H as [q ->]. lia. Qed. | ||
| 910 | Lemma odd_mod x: Nat.even x = false -> x mod 2 = 1. | ||
| 136 | Proof. | 911 | Proof. |
| 137 | unfold S. | ||
| 912 | intros H. destruct (Nat.Even_or_Odd x) as [He|[q ->]]. | ||
| 138 | intros. | ||
| 913 | - apply Nat.even_spec in He. congruence. | ||
| 139 | follow10 ROv. | ||
| 914 | - lia. | ||
| 140 | replace (1+i+m) with (k*2+(1+i+m-k*2)) by lia. | ||
| 915 | Qed. | ||
| 141 | epose proof (sideRLs_concat_1L (RIncs _ 0)) as I1. | ||
| 917 | Ltac par x := let E := fresh "E" in | ||
| 142 | follow I1. | ||
| 918 | destruct (Nat.even x) eqn:E; [apply even_mod in E | apply odd_mod in E]. | ||
| 143 | - rewrite lpow_add. | ||
| 920 | (** I in linear-arithmetic form (parities as [mod 2]) *) | ||
| 144 | eapply sideRLs_trans. | ||
| 921 | Lemma I_std N m: I (false, N, m) <-> | ||
| 145 | + apply LIncs'. | ||
| 922 | 1 <= m <= N /\ | ||
| 146 | + apply LIncs. | ||
| 923 | ((N+m) mod 2 = 0 -> N mod 2 = 0 -> 2*N <= 3*m+6) /\ | ||
| 147 | - unfold to_DH_config. | ||
| 924 | ((N+m) mod 2 = 0 -> N mod 2 = 1 -> N <= 2*m+3) /\ | ||
| 148 | finish. | ||
| 925 | ((N+m) mod 2 = 1 -> N <= m+3). | ||
| 926 | Proof. | ||
| 927 | unfold I. cbv beta iota zeta. par (N+m); par N; cbv beta iota. | ||
| 928 | all: split; [intros [H1 [_ H3]]; lia | intros H; split; [lia | split; [intros Hf; discriminate | lia]]]. | ||
| 929 | Qed. | ||
| 931 | Lemma I_pk N m: I (true, N, m) <-> | ||
| 932 | 1 <= m <= N /\ 2 <= N /\ | ||
| 933 | ((N+m) mod 2 = 0 -> N mod 2 = 0 -> N <= 2*m+3) /\ | ||
| 934 | ((N+m) mod 2 = 0 -> N mod 2 = 1 -> 2*N <= 5*m+6) /\ | ||
| 935 | ((N+m) mod 2 = 1 -> N <= m+3). | ||
| 936 | Proof. | ||
| 937 | unfold I. cbv beta iota zeta. par (N+m); par N; cbv beta iota. | ||
| 938 | all: split; [intros [H1 [H2 H3]]; specialize (H2 eq_refl); lia | intros H; split; [lia | split; [intros _; lia | lia]]]. | ||
| 939 | Qed. | ||
| 941 | (** results N' = D + n, m' = n *) | ||
| 942 | Lemma close_diag t n: 1 <= n -> (t = true -> 2 <= n) -> I (t, n, n). | ||
| 943 | Proof. | ||
| 944 | intros H1 H2. destruct t; [apply I_pk; specialize (H2 eq_refl) | apply I_std]; lia. | ||
| 945 | Qed. | ||
| 947 | Lemma close_std D n: 1 <= n -> | ||
| 948 | (D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 1 -> D <= n+3) /\ (n mod 2 = 0 -> 2*D <= n+6)) -> | ||
| 949 | I (false, D+n, n). | ||
| 950 | Proof. intros. apply I_std. lia. Qed. | ||
| 952 | Lemma close_pk D n: 1 <= n -> 2 <= D+n -> | ||
| 953 | (D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 0 -> D <= n+3) /\ (n mod 2 = 1 -> 2*D <= 3*n+6)) -> | ||
| 954 | I (true, D+n, n). | ||
| 955 | Proof. intros. apply I_pk. lia. Qed. | ||
| 957 | (** N+1 = 2^i (2k+1): the three shapes of N *) | ||
| 958 | Lemma Nfacts N k i: S N = 2^i*(2*k+1) -> | ||
| 959 | (i = 0 /\ N = 2*k) \/ (i = 1 /\ N = 4*k+1) \/ (2 <= i /\ (S N) mod 4 = 0 /\ 8*k+4 <= S N). | ||
| 960 | Proof. | ||
| 961 | intros H. destruct i as [|[|i']]. | ||
| 962 | - left. rewrite Nat.pow_0_r in H. lia. | ||
| 963 | - right; left. rewrite Nat.pow_1_r in H. lia. | ||
| 964 | - right; right. rewrite !Nat.pow_succ_r' in H. pose proof (pow_pos i'). | ||
| 965 | assert (H1: S N = 4 * (2^i'*(2*k+1))) by lia. | ||
| 966 | assert (H2: 2*k+1 <= 2^i'*(2*k+1)) by nia. | ||
| 967 | remember (2^i'*(2*k+1)) as Y. clear HeqY H. lia. | ||
| 968 | Qed. | ||
| 970 | Ltac nfacts N k i Hk := | ||
| 971 | destruct (Nfacts N k i Hk) as [[-> ->]|[[-> ->]|[?Hi [?H4 ?H8]]]]; clear Hk. | ||
| 973 | Lemma log2_facts k: 1 <= k -> exists l r, k = 2^l + r /\ r < 2^l. | ||
| 974 | Proof. | ||
| 975 | intros Hk. exists (Nat.log2 k), (k - 2^(Nat.log2 k)). | ||
| 976 | pose proof (Nat.log2_spec k ltac:(lia)) as [H1 H2]. | ||
| 977 | rewrite Nat.pow_succ_r' in H2. lia. | ||
| 978 | Qed. | ||
| 980 | Lemma pow_ge2 u: 1 <= u -> 2 <= 2^u. | ||
| 981 | Proof. intros Hu. destruct u as [|u]; [lia|]. rewrite Nat.pow_succ_r'. pose proof (pow_pos u). lia. Qed. | ||
| 983 | Lemma pow_ge4 u: 2 <= u -> 4 <= 2^u. | ||
| 984 | Proof. | ||
| 985 | intros Hu. replace u with (S (S (u-2))) by lia. rewrite !Nat.pow_succ_r'. | ||
| 986 | pose proof (pow_pos (u-2)). lia. | ||
| 987 | Qed. | ||
| 989 | Lemma pow_par h: (h = 0 /\ 2^h = 1) \/ 2^h mod 2 = 0. | ||
| 990 | Proof. destruct h as [|h]; [left; split; reflexivity | right; rewrite Nat.pow_succ_r'; lia]. Qed. | ||
| 992 | (** the gen-2 exponents of S3/P4: v = 2^u (2g+1) with 1 <= v < 2^l and v even *) | ||
| 993 | Lemma split_v l v: 1 <= v -> v < 2^l -> v mod 2 = 0 -> | ||
| 994 | exists h u g, l = S (h+u) /\ v = 2^u*(2*g+1) /\ 1 <= u /\ g < 2^h. | ||
| 995 | Proof. | ||
| 996 | intros Hv1 Hv2 Hv3. | ||
| 997 | destruct (lowbit v) as [u [g Hv]]; [lia|]. | ||
| 998 | pose proof (pow_odd_pos u g) as Pug. | ||
| 999 | assert (Hul: u < l). { apply (Nat.pow_lt_mono_r_iff 2); lia. } | ||
| 1000 | exists (l - S u), u, g. | ||
| 1001 | assert (El: l = S (l - S u + u)) by lia. | ||
| 1002 | split; [exact El|]. split; [exact Hv|]. | ||
| 1003 | pose proof (pow_pos u) as Pu. | ||
| 1004 | split. | ||
| 1005 | - destruct u as [|u']; [|lia]. rewrite Nat.pow_0_r in Hv. lia. | ||
| 1006 | - set (h := l - S u) in *. clearbody h. subst l. | ||
| 1007 | rewrite Nat.pow_succ_r', Nat.pow_add_r in Hv2. | ||
| 1008 | assert (H1: 2^u*(2*g+1) < 2^u*(2*2^h)) by lia. | ||
| 1009 | apply Nat.mul_lt_mono_pos_l in H1; lia. | ||
| 1010 | Qed. | ||
| 1012 | (** closure of S1, P1, P2 (proof.md 4.3) *) | ||
| 1013 | Lemma C_S1 N m i k: I (false, N, m) -> S N = 2^i*(2*k+1) -> 1 <= k -> | ||
| 1014 | I (true, 2*k+(1+i+m), 1+i+m). | ||
| 1015 | Proof. | ||
| 1016 | intros HI Hk Hk1. apply I_std in HI. apply I_pk. | ||
| 1017 | nfacts N k i Hk; lia. | ||
| 1018 | Qed. | ||
| 1020 | Lemma C_P1 N m i l: I (true, N, m) -> S N = 2^i*(2*(2^l+0)+1) -> | ||
| 1021 | I (false, 2^l+(1+i+m), 1+i+m). | ||
| 1022 | Proof. | ||
| 1023 | intros HI Hk. apply I_pk in HI. apply I_std. | ||
| 1024 | pose proof (pow_pos l). pose proof (pow_par l) as Hl. | ||
| 1025 | rewrite Nat.add_0_r in Hk. set (Z := 2^l) in *. clearbody Z. | ||
| 1026 | nfacts N Z i Hk; lia. | ||
| 1027 | Qed. | ||
| 1029 | Lemma C_P2 N m i l r: I (true, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> r < 2^l -> | ||
| 1030 | I (false, 2*r+(1+i+m), 1+i+m). | ||
| 1031 | Proof. | ||
| 1032 | intros HI Hk Hr. apply I_pk in HI. apply I_std. | ||
| 1033 | set (Z := 2^l) in *. clearbody Z. | ||
| 1034 | nfacts N (Z+r) i Hk; lia. | ||
| 1035 | Qed. | ||
| 1037 | (** coverage of S3 and P4 (proof.md 4.2): the dirty cases are i = 0 (S3), i <= 1 (P4), class P, | ||
| 1038 | in the final gap, with T even *) | ||
| 1039 | Lemma Cov_S3 N m i l r: I (false, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> 1 <= r -> r < 2^l -> | ||
| 1040 | 2*(2^l+r)+(1+i+m)+1 < 4*2^l -> | ||
| 1041 | i = 0 /\ m mod 2 = 0 /\ 2*r < 2^l /\ 3*2^l < 2*(2^l+r)+(1+i+m)+1 /\ 4*(2^l+r) <= 3*m+6. | ||
| 1042 | Proof. | ||
| 1043 | intros HI Hk Hr1 Hr Hlt. apply I_std in HI. | ||
| 1044 | set (Z := 2^l) in *. clearbody Z. | ||
| 1045 | nfacts N (Z+r) i Hk; lia. | ||
| 1046 | Qed. | ||
| 1048 | Lemma Cov_P4 N m i l r: I (true, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> 1 <= r -> r < 2^l -> | ||
| 1049 | 2*r+(1+i+m)+1 < 2*2^l -> | ||
| 1050 | i <= 1 /\ (2*r+(1+i+m)+1) mod 2 = 0 /\ 2*r < 2^l /\ 2^l < 2*r+(1+i+m)+1 /\ 2^l < 1+i+m. | ||
| 1051 | Proof. | ||
| 1052 | intros HI Hk Hr1 Hr Hlt. apply I_pk in HI. | ||
| 1053 | set (Z := 2^l) in *. clearbody Z. | ||
| 1054 | nfacts N (Z+r) i Hk; lia. | ||
| 1055 | Qed. | ||
| 1057 | Lemma step_std N m: I (false, N, m) -> exists s', St (false, N, m) -->+ St s' /\ I s'. | ||
| 1058 | Proof. | ||
| 1059 | intros HI. rewrite St_std. | ||
| 1060 | assert (Hm: 1 <= m <= N) by (apply I_std in HI; tauto). | ||
| 1061 | destruct (lowbit (S N)) as [i [k Hk]]; [lia|]. | ||
| 1062 | destruct (Nat.eq_dec k 0) as [->|Hk0]. | ||
| 1063 | { (* S0 *) | ||
| 1064 | exists (false, 1+i+m, 1+i+m). rewrite St_std. split. | ||
| 1065 | - replace N with (2^i-1) by lia. apply BS_S0. | ||
| 1066 | - apply close_diag; [lia | intros Hf; discriminate Hf]. } | ||
| 1067 | destruct (log2_facts k ltac:(lia)) as [l [r [-> Hr]]]. | ||
| 1068 | replace N with ((2*(2^l+r)+1)*2^i-1) by lia. | ||
| 1069 | pose proof (pow_pos l) as Pl. | ||
| 1070 | assert (E2: 2^(S l) = 2*2^l) by apply Nat.pow_succ_r'. | ||
| 1071 | assert (E4: 2^(S (S l)) = 4*2^l) by (rewrite !Nat.pow_succ_r'; lia). | ||
| 1072 | destruct (Nat.eq_dec r 0) as [->|Hr0]. | ||
| 1073 | { (* S1, k = 2^l *) | ||
| 1074 | exists (true, 2*(2^l+0)+(1+i+m), 1+i+m). rewrite St_pk. split. | ||
| 1075 | - apply BS_S1a with (l := l). lia. | ||
| 1076 | - apply (C_S1 N); [exact HI | exact Hk | lia]. } | ||
| 1077 | destruct (lt_eq_lt_dec (2*(2^l+r)+(1+i+m)+1) (2^(S (S l)))) as [[Hlt|Heq]|Hgt]. | ||
| 1078 | 3: { (* S1, T > 2^(l+2) *) | ||
| 1079 | exists (true, 2*(2^l+r)+(1+i+m), 1+i+m). rewrite St_pk. split. | ||
| 1080 | - clear Hk. apply BS_S1b with (l := l); lia. | ||
| 1081 | - apply (C_S1 N); [exact HI | exact Hk | lia]. } | ||
| 1082 | 2: { (* S2 *) | ||
| 1083 | exists (false, l+4+(1+i+m), l+4+(1+i+m)). rewrite St_std. split. | ||
| 1084 | - clear Hk. apply BS_S2; lia. | ||
| 1085 | - apply close_diag; [lia | intros Hf; discriminate Hf]. } | ||
| 1086 | (* S3 *) | ||
| 1087 | rewrite E4 in Hlt. | ||
| 1088 | destruct (Cov_S3 N m i l r HI Hk ltac:(lia) Hr Hlt) as [-> [Hm2 [Hr2 [HT3 H43]]]]. | ||
| 1089 | clear HI Hk Hm. | ||
| 1090 | assert (HZ: 2^l mod 2 = 0). | ||
| 1091 | { destruct l as [|l']; [rewrite Nat.pow_0_r in *; lia | rewrite Nat.pow_succ_r'; lia]. } | ||
| 1092 | destruct (split_v l (2*(2^l+r)+(1+0+m)+1 - 3*2^l)) as [h [u [g [-> [Hv [Hu1 Hg]]]]]]; | ||
| 1093 | [lia|lia|lia|]. | ||
| 1094 | assert (E1: 2^(S (h+u)) = 2*(2^h*2^u)) by (rewrite Nat.pow_succ_r', Nat.pow_add_r; reflexivity). | ||
| 1095 | assert (E3: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r. | ||
| 1096 | assert (E5: 2^(S h) = 2*2^h) by apply Nat.pow_succ_r'. | ||
| 1097 | pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu. | ||
| 1098 | assert (HU: 2*2^h <= 2^h*2^u) by (pose proof (pow_ge2 u Hu1); nia). | ||
| 1099 | assert (HU2: 2 <= u -> 4*2^h <= 2^h*2^u) by (intros Hu2; pose proof (pow_ge4 u Hu2); nia). | ||
| 1100 | pose proof (pow_par h) as Hh. | ||
| 1101 | (* n = 1+u+(1+0+m) > 2^l >= 4*2^h, n odd if u = 1 *) | ||
| 1102 | assert (Hn: 2^(S (h+u)) < 1+u+(1+0+m)) by lia. | ||
| 1103 | assert (Hv': 2*r+(1+0+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1)) by lia. | ||
| 1104 | clear Hv HZ E4 E2 Pl HT3 H43 Hlt. | ||
| 1105 | destruct (Nat.eq_dec g 0) as [->|Hg0]. | ||
| 1106 | - exists (false, 3*2^h+(1+u+(1+0+m)), 1+u+(1+0+m)). rewrite St_std. split. | ||
| 1107 | + apply BS_S3a; lia. | ||
| 1108 | + apply close_std; [lia|]. | ||
| 1109 | destruct Hh as [[-> Hh1]|Hh]; [left; lia | right; lia]. | ||
| 1110 | - exists (false, 2^(S h)+2*g+(1+u+(1+0+m)), 1+u+(1+0+m)). rewrite St_std. split. | ||
| 1111 | + apply BS_S3b; lia. | ||
| 1112 | + apply close_std; [lia|]. right. lia. | ||
| 1113 | Qed. | ||
| 1115 | Lemma step_pk N m: I (true, N, m) -> exists s', St (true, N, m) -->+ St s' /\ I s'. | ||
| 1116 | Proof. | ||
| 1117 | intros HI. rewrite St_pk. | ||
| 1118 | assert (Hm: 1 <= m <= N /\ 2 <= N) by (apply I_pk in HI; tauto). | ||
| 1119 | destruct (lowbit (S N)) as [i [k Hk]]; [lia|]. | ||
| 1120 | destruct (Nat.eq_dec k 0) as [->|Hk0]. | ||
| 1121 | { (* P0 *) | ||
| 1122 | assert (Hi: 2 <= i). | ||
| 1123 | { destruct (Nfacts N 0 i Hk) as [[_ HN]|[[_ HN]|[Hi _]]]; lia. } | ||
| 1124 | exists (false, 2+i+m, 2+i+m). rewrite St_std. split. | ||
| 1125 | - replace N with (2^i-1) by lia. apply BS_P0, Hi. | ||
| 1126 | - apply close_diag; [lia | intros Hf; discriminate Hf]. } | ||
| 1127 | destruct (log2_facts k ltac:(lia)) as [l [r [-> Hr]]]. | ||
| 1128 | replace N with ((2*(2^l+r)+1)*2^i-1) by lia. | ||
| 1129 | pose proof (pow_pos l) as Pl. | ||
| 1130 | assert (E2: 2^(S l) = 2*2^l) by apply Nat.pow_succ_r'. | ||
| 1131 | destruct (Nat.eq_dec r 0) as [->|Hr0]. | ||
| 1132 | { (* P1 *) | ||
| 1133 | exists (false, 2^l+(1+i+m), 1+i+m). rewrite St_std. split. | ||
| 1134 | - apply BS_P1. | ||
| 1135 | - apply (C_P1 N); [exact HI | exact Hk]. } | ||
| 1136 | destruct (lt_eq_lt_dec (2*r+(1+i+m)+1) (2^(S l))) as [[Hlt|Heq]|Hgt]. | ||
| 1137 | 3: { (* P2 *) | ||
| 1138 | exists (false, 2*r+(1+i+m), 1+i+m). rewrite St_std. split. | ||
| 1139 | - clear Hk. apply BS_P2; lia. | ||
| 1140 | - apply (C_P2 N m i l); [exact HI | exact Hk | exact Hr]. } | ||
| 1141 | 2: { (* P3 *) | ||
| 1142 | exists (false, l+2+(1+i+m), l+2+(1+i+m)). rewrite St_std. split. | ||
| 1143 | - clear Hk. apply BS_P3; lia. | ||
| 1144 | - apply close_diag; [lia | intros Hf; discriminate Hf]. } | ||
| 1145 | (* P4 *) | ||
| 1146 | rewrite E2 in Hlt. | ||
| 1147 | destruct (Cov_P4 N m i l r HI Hk ltac:(lia) Hr Hlt) as [Hi1 [HT2 [Hr2 [HT1 Hb]]]]. | ||
| 1148 | clear HI Hk Hm. | ||
| 1149 | assert (HZ: 2^l mod 2 = 0). | ||
| 1150 | { destruct l as [|l']; [rewrite Nat.pow_0_r in *; lia | rewrite Nat.pow_succ_r'; lia]. } | ||
| 1151 | destruct (split_v l (2*r+(1+i+m)+1 - 2^l)) as [h [u [g [-> [Hv [Hu1 Hg]]]]]]; | ||
| 1152 | [lia|lia|lia|]. | ||
| 1153 | assert (E1: 2^(S (h+u)) = 2*(2^h*2^u)) by (rewrite Nat.pow_succ_r', Nat.pow_add_r; reflexivity). | ||
| 1154 | assert (E3: 2^(h+u) = 2^h*2^u) by apply Nat.pow_add_r. | ||
| 1155 | assert (E5: 2^(S h) = 2*2^h) by apply Nat.pow_succ_r'. | ||
| 1156 | pose proof (pow_pos h) as Ph. pose proof (pow_pos u) as Pu. | ||
| 1157 | assert (HU: 2*2^h <= 2^h*2^u) by (pose proof (pow_ge2 u Hu1); nia). | ||
| 1158 | pose proof (pow_par h) as Hh. | ||
| 1159 | assert (Hv': 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1)) by lia. | ||
| 1160 | clear Hv HZ E2 Pl HT1 HT2 Hlt. | ||
| 1161 | destruct (Nat.eq_dec g 0) as [->|Hg0]. | ||
| 1162 | - exists (true, 3*2^h+(1+u+(1+i+m)), 1+u+(1+i+m)). rewrite St_pk. split. | ||
| 1163 | + apply BS_P4a; lia. | ||
| 1164 | + apply close_pk; [lia|lia|]. | ||
| 1165 | destruct Hh as [[-> Hh1]|Hh]; [left; lia | right; lia]. | ||
| 1166 | - exists (true, 2^(S h)+2*g+(1+u+(1+i+m)), 1+u+(1+i+m)). rewrite St_pk. split. | ||
| 1167 | + apply BS_P4b; lia. | ||
| 1168 | + apply close_pk; [lia|lia|]. right. lia. | ||
| 1169 | Qed. | ||
| 1171 | Lemma step_I s: I s -> exists s', St s -->+ St s' /\ I s'. | ||
| 1172 | Proof. | ||
| 1173 | destruct s as [[[|] N] m]. | ||
| 1174 | - apply step_pk. | ||
| 1175 | - apply step_std. | ||
| 149 | Qed. | 1176 | Qed. |
| 151 | Lemma nonhalt: ~halts tm c0. | 1178 | Lemma nonhalt: ~halts tm c0. |
| 152 | Proof. | 1179 | Proof. |
| 153 | eapply multistep_nonhalt with (c':=S (6,6)). | ||
| 1180 | eapply multistep_nonhalt. 1: apply init0. | ||
| 154 | 1: unfold S; esx. | ||
| 1181 | change (K 1 0 0 1) with (St (false, 1%nat, 1%nat)). | ||
| 155 | eapply progress_nonhalt_cond with (P:=fun '(a,b) => a<=1+b). | 1182 | apply progress_nonhalt_cond with (P := I). |
| 156 | 2: lia. | ||
| 1183 | - apply step_I. | ||
| 157 | intros [a b] HP. | ||
| 1184 | - cbn. lia. | ||
| 158 | lowbitS_cases a. | ||
| 159 | eexists (_,_). | ||
| ⋯ 2 template-only lines (template 160–161), not in ours | |||
| 162 | zify_le_mul_r; lia. | ||
| 163 | - lia. | ||
| 164 | Qed. | 1185 | Qed. |
| 1187 | (* | ||
| 1188 | 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (only E1 is undefined) | ||
| 1190 | words: W(e,o): bit d of e at offset 2d, bit d of o at offset 2d+1 (offset 0 = the cell A reads) | ||
| 1191 | std(N) = W(N,0); pk(N) = W(N-2^(P+1), 2^P) for 2^(P+1) <= N < 2^(P+2) | ||
| 1192 | K(w,n,m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf (= w <| R n m); S(typ,N,m) = K(typ(N),0,m) | ||
| 1193 | phi(w): last cell 0 -> 1; else (e,e+1) := lowest pair of adjacent 0 cells: cell e+1 := 1, cells 0..e := 0 | ||
| 1195 | R1 K(w,n,m) --> K(phi(w), n-1, m+1) n >= 1 | ||
| 1196 | R2 K(w,0,m) --> K(x, m+1+u, 0) phi(w) = x 1 0^(2u) | ||
| 1197 | R3 K(w,0,m) --> K(x', 0, m+u+2) phi(w) = x' 0 0 1 0^(2u+1) (x'00 may be 0^inf) | ||
| 1198 | R4 K(w,0,m) --> halt (E1) phi(w) = x 1 1 0^(2u+1) | ||
| 1199 | R5 K(w,0,m) --> nested scan, no rule phi(w) = x 1 0 1 0^(2u+1) | ||
| 1201 | N+1 = (2k+1) 2^i, b = m+1+i, L = bitlen(k), r = k - 2^(L-1) | ||
| 1202 | S0 S(std,N,m) --> S(std, b, b) k = 0 | ||
| 1203 | S1 S(std,N,m) --> S(pk, 2k+b, b) k >= 1, and k = 2^(L-1) or 2k+b >= 2^(L+1) | ||
| 1204 | S2 S(std,N,m) --> S(std, b+L+3, b+L+3) 2k+b+1 = 2^(L+1) | ||
| 1205 | S3 S(std,N,m) --> S(std, D+n, n) k < 3*2^(L-2), 3*2^(L-1) < 2k+b+1 < 2^(L+1) | ||
| 1206 | P0 S(pk,N,m) --> S(std, b+1, b+1) k = 0 | ||
| 1207 | P1 S(pk,N,m) --> S(std, k+b, b) k = 2^(L-1) | ||
| 1208 | P2 S(pk,N,m) --> S(std, 2r+b, b) r >= 1, 2r+b >= 2^L | ||
| 1209 | P3 S(pk,N,m) --> S(std, b+L+1, b+L+1) r >= 1, 2r+b+1 = 2^L | ||
| 1210 | P4 S(pk,N,m) --> S(pk, D+n, n) 1 <= r < 2^(L-2), 2^(L-1) < 2r+b+1 < 2^L | ||
| 1212 | invariant I(typ,N,m): 1 <= m <= N (pk: N >= 2), and | ||
| 1213 | N = m (mod 2): std: 2N <= 3m+6 (N even), N <= 2m+3 (N odd); pk: N <= 2m+3 (N even), 2N <= 5m+6 (N odd) | ||
| 1214 | N != m (mod 2): N <= m+3 | ||
| 1216 | start: c0 -->(32) K(1,0,1) = S(std,1,1), which satisfies I | ||
| 1217 | *) | ||
3Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.
118 items in 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v (1217 lines): 105 Lemma, 10 Definition, 2 Inductive, 1 Fixpoint. Tags against the template: identical = same name and same text once each file's own TM string is <TM> (marked "except the TM string" when that is the only difference); adapted = same name, different text; new = no item of that name in the template part.
| # | kind | name | statement (no proof body) | line | vs template |
|---|---|---|---|---|---|
| 1 | Definition | tm | Definition tm := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF"). | L23 | identicalexcept the TM string |
| 2 | Definition | R | Definition R n m := [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^(m) *> const 0. | L28 | identical |
| 3 | Definition | bt | Definition bt (x:nat) : Sym := if Nat.odd x then 1 else 0. | L32 | new |
| 4 | Fixpoint | wd | Fixpoint wd (n e o : nat) : list Sym := match n with | O => [] | S n' => bt e :: bt o :: wd n' (Nat.div2 e) (Nat.div2 o) end. | L34 | new |
| 5 | Definition | WS | Definition WS e o : side := wd (e+o) e o *> const 0. | L40 | new |
| 6 | Lemma | bt_even | Lemma bt_even e: bt (2*e) = 0. | L42 | new |
| 7 | Lemma | bt_odd | Lemma bt_odd e: bt (2*e+1) = 1. | L45 | new |
| 8 | Lemma | div2_even | Lemma div2_even e: Nat.div2 (2*e) = e. | L48 | new |
| 9 | Lemma | div2_odd | Lemma div2_odd e: Nat.div2 (2*e+1) = e. | L51 | new |
| 10 | Lemma | wd_pad | Lemma wd_pad n: forall e o k, e < 2^n -> o < 2^n -> wd (n+k) e o *> const 0 = wd n e o *> const 0. | L54 | new |
| 11 | Lemma | lt_pow2_self | Lemma lt_pow2_self x: x < 2^x. | L69 | new |
| 12 | Lemma | wd_WS | Lemma wd_WS n e o: e < 2^n -> o < 2^n -> wd n e o *> const 0 = WS e o. | L72 | new |
| 13 | Lemma | WS_split | Lemma WS_split e o: WS e o = [bt e; bt o] *> WS (Nat.div2 e) (Nat.div2 o). | L84 | new |
| 14 | Lemma | WS_00 | Lemma WS_00 e o: WS (2*e) (2*o) = [0;0] *> WS e o. | L97 | new |
| 15 | Lemma | WS_10 | Lemma WS_10 e o: WS (2*e+1) (2*o) = [1;0] *> WS e o. | L99 | new |
| 16 | Lemma | WS_01 | Lemma WS_01 e o: WS (2*e) (2*o+1) = [0;1] *> WS e o. | L101 | new |
| 17 | Lemma | WS_11 | Lemma WS_11 e o: WS (2*e+1) (2*o+1) = [1;1] *> WS e o. | L103 | new |
| 18 | Lemma | WS_0x | Lemma WS_0x e o: WS (2*e) o = [0; bt o] *> WS e (Nat.div2 o). | L106 | new |
| 19 | Lemma | WS_1x | Lemma WS_1x e o: WS (2*e+1) o = [1; bt o] *> WS e (Nat.div2 o). | L108 | new |
| 20 | Inductive | PA | Inductive PA : nat -> nat -> nat -> nat -> Prop := | PA0 e o : PA (2*e) o (2*e+1) o | PA1 e o e' o' : PA e o e' o' -> PA (2*e+1) (2*o) (2*e') (2*o') | PA2 e o e' o' : PF e o e' o' -> PA (2*e+1) (2*o+1) (2*e') (2*o') with PF : nat -> nat -> nat -> nat -> Prop := | PF0 e o : PF (2*e) (2*o) (2*e) (2*o+1) … +3 lines | L113 | new |
| 21 | Lemma | TA0 | Lemma TA0 l a r: [0;a] *> l <{{A}} r -->+ [1;a] *> l {{B}}> r. | L127 | new |
| 22 | Lemma | TA1 | Lemma TA1 l r: [1;0] *> l <{{A}} r -->+ l <{{A}} [1;1] *> r. | L129 | new |
| 23 | Lemma | TA2 | Lemma TA2 l r: [1;1] *> l <{{A}} r -->+ l <{{F}} [1;1] *> r. | L131 | new |
| 24 | Lemma | TF0 | Lemma TF0 l r: [0;0] *> l <{{F}} r -->+ [0;1] *> l {{B}}> r. | L133 | new |
| 25 | Lemma | TF1 | Lemma TF1 l r: [0;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r. | L135 | new |
| 26 | Lemma | TF2 | Lemma TF2 l r: [1;0] *> l <{{F}} r -->+ l <{{A}} [1;1] *> r. | L137 | new |
| 27 | Lemma | TF3 | Lemma TF3 l r: [1;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r. | L139 | new |
| 28 | Lemma | TB | Lemma TB l r: l {{B}}> [1;1] *> r -->+ [0;0] *> l {{B}}> r. | L141 | new |
| 29 | Lemma | phi_spec | Lemma phi_spec:
(forall e o e' o', PA e o e' o' -> forall r, WS e o <{{A}} r -->+ WS e' o' {{B}}> r) /\
(forall e o e' o', PF e o e' o' -> forall r, WS e o <{{F}} r -->+ WS e' o' {{B}}> r). | L144 | new |
| 30 | Definition | PA_spec | Definition PA_spec := proj1 phi_spec. | L159 | new |
| 31 | Inductive | PAs | Inductive PAs : nat -> nat -> nat -> nat -> nat -> Prop := | PAs0 e o : PAs 0 e o e o | PAsS j e o e1 o1 e2 o2 : PA e o e1 o1 -> PAs j e1 o1 e2 o2 -> PAs (S j) e o e2 o2. | L163 | new |
| 32 | Lemma | PA_eq | Lemma PA_eq e o e' o' e2 o2 e2' o2': PA e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PA e2 o2 e2' o2'. | L167 | new |
| 33 | Lemma | PF_eq | Lemma PF_eq e o e' o' e2 o2 e2' o2': PF e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PF e2 o2 e2' o2'. | L171 | new |
| 34 | Lemma | PAs_eq | Lemma PAs_eq j e o e' o' j2 e2 o2 e2' o2': PAs j e o e' o' -> j = j2 -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PAs j2 e2 o2 e2' o2'. | L175 | new |
| 35 | Lemma | PAs_1 | Lemma PAs_1 e o e' o': PA e o e' o' -> PAs 1 e o e' o'. | L179 | new |
| 36 | Lemma | PAs_trans | Lemma PAs_trans j1 j2 e o e1 o1 e2 o2: PAs j1 e o e1 o1 -> PAs j2 e1 o1 e2 o2 -> PAs (j1+j2) e o e2 o2. | L182 | new |
| 37 | Lemma | PAs_split | Lemma PAs_split j1 j2 e o e2 o2: PAs (j1+j2) e o e2 o2 -> exists e1 o1, PAs j1 e o e1 o1 /\ PAs j2 e1 o1 e2 o2. | L189 | new |
| 38 | Lemma | PAs_dbl | Lemma PAs_dbl j e o e' o': PAs j e o e' o' -> PAs (2*j) (2*e) (2*o) (2*e') (2*o'). | L199 | new |
| 39 | Lemma | PAs_dbl1 | Lemma PAs_dbl1 j e o e' o': PAs (S j) e o e' o' -> PAs (2*j+1) (2*e+1) (2*o) (2*e') (2*o'). | L210 | new |
| 40 | Lemma | INC_std | Lemma INC_std N: PA N 0 (N+1) 0. | L221 | new |
| 41 | Lemma | INC_stds | Lemma INC_stds j N: PAs j N 0 (N+j) 0. | L229 | new |
| 42 | Lemma | PF_inc0 | Lemma PF_inc0 o: PF 0 o 0 (o+1). | L237 | new |
| 43 | Lemma | Gap | Lemma Gap P: forall c E o1, c+1 < 2^(S P) -> PA (c + 2^(S P)*E) (2^P*(2*o1+1)) (c + 1 + 2^(S P)*E) (2^P*(2*o1+1)). | L245 | new |
| 44 | Lemma | Gaps | Lemma Gaps P j: forall c E o1, c+j < 2^(S P) -> PAs j (c + 2^(S P)*E) (2^P*(2*o1+1)) (c + j + 2^(S P)*E) (2^P*(2*o1+1)). | L258 | new |
| 45 | Lemma | F_inc | Lemma F_inc h: forall E o O, o + 1 < 2^h -> PF (2^h*E) (o + 2^h*O) (2^h*E) (o + 1 + 2^h*O). | L268 | new |
| 46 | Lemma | F_carry | Lemma F_carry h: forall E O E' O', PF E O E' O' -> PF (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O'). | L281 | new |
| 47 | Lemma | lowbit | Lemma lowbit (x:nat): x <> 0%nat -> exists P o, x = 2^P*(2*o+1). | L294 | new |
| 48 | Lemma | pow_pos | Lemma pow_pos P: 1 <= 2^P. | L303 | new |
| 49 | Lemma | pow_odd_pos | Lemma pow_odd_pos P o1: 2^P <= 2^P*(2*o1+1). | L306 | new |
| 50 | Lemma | pow_odd_room | Lemma pow_odd_room P o1 h: 2^P*(2*o1+1) < 2^h -> 2^P*(2*o1+1) + 2^P <= 2^h. | L309 | new |
| 51 | Lemma | Sweep | Lemma Sweep h: forall P o1 c E O E' O', 2^P*(2*o1+1) < 2^h -> c < 2^(S P) -> PF E O E' O' -> PAs (2^(S h) - 2^(S P)*(2*o1+1) - c) (c + 2^h*E) (2^P*(2*o1+1) + 2^h*O) (2^h*E') (2^h*O'). | L325 | new |
| 52 | Lemma | RS | Lemma RS l n m:
l {{B}}> R (S n) m -->+ l <{{A}} R n (S m). | L393 | new |
| 53 | Lemma | shift01 | Lemma shift01 u (r:side): [0;1]^^u *> [0] *> r = [0] *> [1;0]^^u *> r. | L399 | new |
| 54 | Lemma | OVe | Lemma OVe l u m:
([0;0]^^u *> [1] *> l) {{B}}> R 0 m -->+ l <{{A}} R (1+u+m) 0. | L406 | new |
| 55 | Lemma | OVo | Lemma OVo l u m:
([0;0]^^u *> [0;1;0;0] *> l) {{B}}> R 0 m -->+ l <{{A}} R 0 (u+2+m). | L412 | new |
| 56 | Definition | K | Definition K e o n m := WS e o <{{A}} R n m. | L418 | new |
| 57 | Lemma | WS_shift | Lemma WS_shift: forall n a c, a + c < n -> WS a c = [bt a] *> WS c (Nat.div2 a). | L422 | new |
| 58 | Lemma | WS_1 | Lemma WS_1 a c: WS (2*a+1) c = [1] *> WS c a. | L437 | new |
| 59 | Lemma | WS_pow | Lemma WS_pow x y u: WS (x*2^u) (y*2^u) = [0;0]^^u *> WS x y. | L442 | new |
| 60 | Lemma | bounces | Lemma bounces j e o e' o' n m: PAs j e o e' o' -> K e o (j+n) m -->* K e' o' n (j+m). | L454 | new |
| 61 | Lemma | OV_even | Lemma OV_even e o a c u m: PA e o ((2*a+1)*2^u) (c*2^u) -> K e o 0 m -->+ K c a (1+u+m) 0. | L466 | new |
| 62 | Lemma | OV_odd | Lemma OV_odd e o a c u m: PA e o (c*2^(u+2)) ((4*a+1)*2^u) -> K e o 0 m -->+ K c a 0 (u+2+m). | L475 | new |
| 63 | Definition | pkE | Definition pkE N := N - 2^(Nat.log2 N). | L488 | new |
| 64 | Definition | pkO | Definition pkO N := 2^(Nat.log2 N - 1). | L489 | new |
| 65 | Lemma | pk_eq | Lemma pk_eq P N: 2^(S P) <= N < 2^(S (S P)) -> pkE N = N - 2^(S P) /\ pkO N = 2^P. | L491 | new |
| 66 | Lemma | PAs_1_inv | Lemma PAs_1_inv e o e2 o2: PAs 1 e o e2 o2 -> PA e o e2 o2. | L498 | new |
| 67 | Lemma | PAs_last | Lemma PAs_last j e o e2 o2: PAs (S j) e o e2 o2 -> exists e1 o1, PAs j e o e1 o1 /\ PA e1 o1 e2 o2. | L504 | new |
| 68 | Lemma | INC_pk | Lemma INC_pk N: 2 <= N -> PA (pkE N) (pkO N) (pkE (S N)) (pkO (S N)). | L512 | new |
| 69 | Lemma | INC_pks | Lemma INC_pks j N: 2 <= N -> PAs j (pkE N) (pkO N) (pkE (N+j)) (pkO (N+j)). | L537 | new |
| 70 | Lemma | bounces0 | Lemma bounces0 j e o e' o' m: PAs j e o e' o' -> K e o j m -->* K e' o' 0 (j+m). | L547 | new |
| 71 | Lemma | OVB | Lemma OVB e o a c u m e' o': PA e o ((2*a+1)*2^u) (c*2^u) -> PAs (1+u+m) c a e' o' -> K e o 0 m -->+ K e' o' 0 (1+u+m). | L554 | new |
| 72 | Lemma | std_ov | Lemma std_ov k i: PA ((2*k+1)*2^i-1) 0 ((2*k+1)*2^i) (0*2^i). | L564 | new |
| 73 | Lemma | BS_S0 | Lemma BS_S0 i m: K (2^i-1) 0 0 m -->+ K (1+i+m) 0 0 (1+i+m). | L570 | new |
| 74 | Lemma | OVoS0 | Lemma OVoS0 e o u m: PA e o 0 (2^u) -> K e o 0 m -->+ K (u+3+m) 0 0 (u+3+m). | L577 | new |
| 75 | Lemma | BS_S1a | Lemma BS_S1a l k i m: k = 2^l -> K ((2*k+1)*2^i-1) 0 0 m -->+ K (pkE (2*k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m). | L586 | new |
| 76 | Lemma | O3_merge | Lemma O3_merge l k: 1 <= k < 2^(S l) -> PAs (2^(S (S l)) - 2*k) 0 k (pkE (2^(S (S l)))) (pkO (2^(S (S l)))). | L605 | new |
| 77 | Lemma | BS_S1b | Lemma BS_S1b l k i m: 2^l <= k < 2^(S l) -> 2^(S (S l)) <= 2*k+(1+i+m) -> K ((2*k+1)*2^i-1) 0 0 m -->+ K (pkE (2*k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m). | L619 | new |
| 78 | Lemma | BS_S2 | Lemma BS_S2 l k i m: 2^l <= k < 2^(S l) -> 2*k+(1+i+m)+1 = 2^(S (S l)) -> K ((2*k+1)*2^i-1) 0 0 m -->+ K (l+4+(1+i+m)) 0 0 (l+4+(1+i+m)). | L638 | new |
| 79 | Lemma | pk_ov_full | Lemma pk_ov_full i: 2 <= i -> PA (pkE (2^i-1)) (pkO (2^i-1)) 0 (2^(i-1)). | L658 | new |
| 80 | Lemma | BS_P0 | Lemma BS_P0 i m: 2 <= i -> K (pkE (2^i-1)) (pkO (2^i-1)) 0 m -->+ K (2+i+m) 0 0 (2+i+m). | L673 | new |
| 81 | Lemma | pk_ov | Lemma pk_ov l r i: r < 2^l -> PA (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) ((2*r+1)*2^i) (2^l*2^i). | L682 | new |
| 82 | Lemma | BS_P1 | Lemma BS_P1 l i m: K (pkE ((2*(2^l+0)+1)*2^i-1)) (pkO ((2*(2^l+0)+1)*2^i-1)) 0 m -->+ K (2^l+(1+i+m)) 0 0 (1+i+m). | L697 | new |
| 83 | Lemma | BS_P2 | Lemma BS_P2 l r i m: 1 <= r < 2^l -> 2^(S l) <= 2*r+(1+i+m) -> K (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) 0 m -->+ K (2*r+(1+i+m)) 0 0 (1+i+m). | L705 | new |
| 84 | Lemma | BS_P3 | Lemma BS_P3 l r i m: 1 <= r < 2^l -> 2*r+(1+i+m)+1 = 2^(S l) -> K (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) 0 m -->+ K (l+2+(1+i+m)) 0 0 (l+2+(1+i+m)). | L723 | new |
| 85 | Lemma | PAs_trans_eq | Lemma PAs_trans_eq j1 j2 e o e1 o1 e1' o1' e2 o2: PAs j1 e o e1 o1 -> PAs j2 e1' o1' e2 o2 -> e1 = e1' -> o1 = o1' -> PAs (j1+j2) e o e2 o2. | L744 | new |
| 86 | Lemma | S3_pre | Lemma S3_pre h u r g i m: 1 <= r < 2^(h+u) -> g < 2^h -> 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) -> K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (3*2^h) g (1+u+(1+i+m)) 0. | L750 | new |
| 87 | Lemma | BS_S3a | Lemma BS_S3a h u r i m: 1 <= r < 2^(h+u) -> 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u -> K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (3*2^h+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)). | L776 | new |
| 88 | Lemma | BS_S3b | Lemma BS_S3b h u r g i m: 1 <= r < 2^(h+u) -> 1 <= g < 2^h -> 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) -> 2^(S h) <= 2*g + (1+u+(1+i+m)) -> K ((2*(2^(S (h+u))+r)+1)*2^i-1) 0 0 m -->+ K (2^(S h)+2*g+(1+u+(1+i+m))) 0 0 (1+u+(1+i+m)). | L787 | new |
| 89 | Lemma | P4_pre | Lemma P4_pre h u r g i m: 1 <= r < 2^(h+u) -> g < 2^h -> 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) -> K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+ K (2^h) (2^h+g) (1+u+(1+i+m)) 0. | L806 | new |
| 90 | Lemma | BS_P4a | Lemma BS_P4a h u r i m: 1 <= r < 2^(h+u) -> 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u -> K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+ K (pkE (3*2^h+(1+u+(1+i+m)))) (pkO (3*2^h+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)). | L833 | new |
| 91 | Lemma | BS_P4b | Lemma BS_P4b h u r g i m: 1 <= r < 2^(h+u) -> 1 <= g < 2^h -> 2*r+(1+i+m)+1 = 2^(S (h+u)) + 2^u*(2*g+1) -> 2^(S h) <= 2*g + (1+u+(1+i+m)) -> K (pkE ((2*(2^(S (h+u))+r)+1)*2^i-1)) (pkO ((2*(2^(S (h+u))+r)+1)*2^i-1)) 0 m -->+ K (pkE (2^(S h)+2*g+(1+u+(1+i+m)))) (pkO (2^(S h)+2*g+(1+u+(1+i+m)))) 0 (1+u+(1+i+m)). | L850 | new |
| 92 | Definition | St | Definition St (s : bool * nat * nat) : Q * tape := let '(t, N, m) := s in if t then K (pkE N) (pkO N) 0 m else K N 0 0 m. | L879 | new |
| 93 | Definition | I | Definition I (s : bool * nat * nat) : Prop :=
let '(t, N, m) := s in
1 <= m <= N /\ (t = true -> 2 <= N) /\
(if Nat.even (N + m) then
(if t then (if Nat.even N then N <= 2*m+3 else 2*N <= 5*m+6)
else (if Nat.even N then 2*N <= 3*m+6 else N <= 2*m+3))
… +1 lines | L882 | new |
| 94 | Lemma | init0 | Lemma init0: c0 -->* K 1 0 0 1. | L890 | new |
| 95 | Lemma | St_std | Lemma St_std N m: St (false, N, m) = K N 0 0 m. | L901 | new |
| 96 | Lemma | St_pk | Lemma St_pk N m: St (true, N, m) = K (pkE N) (pkO N) 0 m. | L904 | new |
| 97 | Lemma | even_mod | Lemma even_mod x: Nat.even x = true -> x mod 2 = 0. | L907 | new |
| 98 | Lemma | odd_mod | Lemma odd_mod x: Nat.even x = false -> x mod 2 = 1. | L910 | new |
| 99 | Lemma | I_std | Lemma I_std N m: I (false, N, m) <-> 1 <= m <= N /\ ((N+m) mod 2 = 0 -> N mod 2 = 0 -> 2*N <= 3*m+6) /\ ((N+m) mod 2 = 0 -> N mod 2 = 1 -> N <= 2*m+3) /\ ((N+m) mod 2 = 1 -> N <= m+3). | L921 | new |
| 100 | Lemma | I_pk | Lemma I_pk N m: I (true, N, m) <-> 1 <= m <= N /\ 2 <= N /\ ((N+m) mod 2 = 0 -> N mod 2 = 0 -> N <= 2*m+3) /\ ((N+m) mod 2 = 0 -> N mod 2 = 1 -> 2*N <= 5*m+6) /\ ((N+m) mod 2 = 1 -> N <= m+3). | L931 | new |
| 101 | Lemma | close_diag | Lemma close_diag t n: 1 <= n -> (t = true -> 2 <= n) -> I (t, n, n). | L942 | new |
| 102 | Lemma | close_std | Lemma close_std D n: 1 <= n -> (D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 1 -> D <= n+3) /\ (n mod 2 = 0 -> 2*D <= n+6)) -> I (false, D+n, n). | L947 | new |
| 103 | Lemma | close_pk | Lemma close_pk D n: 1 <= n -> 2 <= D+n -> (D <= 3 /\ D mod 2 = 1) \/ (D mod 2 = 0 /\ (n mod 2 = 0 -> D <= n+3) /\ (n mod 2 = 1 -> 2*D <= 3*n+6)) -> I (true, D+n, n). | L952 | new |
| 104 | Lemma | Nfacts | Lemma Nfacts N k i: S N = 2^i*(2*k+1) -> (i = 0 /\ N = 2*k) \/ (i = 1 /\ N = 4*k+1) \/ (2 <= i /\ (S N) mod 4 = 0 /\ 8*k+4 <= S N). | L958 | new |
| 105 | Lemma | log2_facts | Lemma log2_facts k: 1 <= k -> exists l r, k = 2^l + r /\ r < 2^l. | L973 | new |
| 106 | Lemma | pow_ge2 | Lemma pow_ge2 u: 1 <= u -> 2 <= 2^u. | L980 | new |
| 107 | Lemma | pow_ge4 | Lemma pow_ge4 u: 2 <= u -> 4 <= 2^u. | L983 | new |
| 108 | Lemma | pow_par | Lemma pow_par h: (h = 0 /\ 2^h = 1) \/ 2^h mod 2 = 0. | L989 | new |
| 109 | Lemma | split_v | Lemma split_v l v: 1 <= v -> v < 2^l -> v mod 2 = 0 -> exists h u g, l = S (h+u) /\ v = 2^u*(2*g+1) /\ 1 <= u /\ g < 2^h. | L993 | new |
| 110 | Lemma | C_S1 | Lemma C_S1 N m i k: I (false, N, m) -> S N = 2^i*(2*k+1) -> 1 <= k -> I (true, 2*k+(1+i+m), 1+i+m). | L1013 | new |
| 111 | Lemma | C_P1 | Lemma C_P1 N m i l: I (true, N, m) -> S N = 2^i*(2*(2^l+0)+1) -> I (false, 2^l+(1+i+m), 1+i+m). | L1020 | new |
| 112 | Lemma | C_P2 | Lemma C_P2 N m i l r: I (true, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> r < 2^l -> I (false, 2*r+(1+i+m), 1+i+m). | L1029 | new |
| 113 | Lemma | Cov_S3 | Lemma Cov_S3 N m i l r: I (false, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> 1 <= r -> r < 2^l -> 2*(2^l+r)+(1+i+m)+1 < 4*2^l -> i = 0 /\ m mod 2 = 0 /\ 2*r < 2^l /\ 3*2^l < 2*(2^l+r)+(1+i+m)+1 /\ 4*(2^l+r) <= 3*m+6. | L1039 | new |
| 114 | Lemma | Cov_P4 | Lemma Cov_P4 N m i l r: I (true, N, m) -> S N = 2^i*(2*(2^l+r)+1) -> 1 <= r -> r < 2^l -> 2*r+(1+i+m)+1 < 2*2^l -> i <= 1 /\ (2*r+(1+i+m)+1) mod 2 = 0 /\ 2*r < 2^l /\ 2^l < 2*r+(1+i+m)+1 /\ 2^l < 1+i+m. | L1048 | new |
| 115 | Lemma | step_std | Lemma step_std N m: I (false, N, m) -> exists s', St (false, N, m) -->+ St s' /\ I s'. | L1057 | new |
| 116 | Lemma | step_pk | Lemma step_pk N m: I (true, N, m) -> exists s', St (true, N, m) -->+ St s' /\ I s'. | L1115 | new |
| 117 | Lemma | step_I | Lemma step_I s: I s -> exists s', St s -->+ St s' /\ I s'. | L1171 | new |
| 118 | Lemma | nonhalt | Lemma nonhalt: ~halts tm c0. | L1178 | adapted |
4What a maintainer readsCheck: the rule table below is what the .v proves, and proof.md / README read cleanly for a maintainer.
- submission/proof.md · informal proof (submitted copy)
- submission/README.md · the package README
- submission/discord.md · Discord draft (not posted)
- proof.md (working copy) · differs from the submitted copy
submission/proof.md line 37: 1. Rule table (busycoq comment-block style)
1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (only E1 is undefined)
words: w = ... c2 c1 c0 (offset 0 = the cell A reads); W(e,o): bit d of e at offset 2d, bit d of o at offset 2d+1
std(N) = W(N,0); pk(N) = W(N-2^(P+1), 2^P) for 2^(P+1) <= N < 2^(P+2)
K(w,n,m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf (= BECv5's w <| R n m); S(typ,N,m) = K(typ(N),0,m)
phi(w): last cell 0 -> 1; else (e,e+1) := lowest pair of adjacent 0 cells: cell e+1 := 1, cells 0..e := 0
R1 K(w,n,m) --> K(phi(w), n-1, m+1) n >= 1 steps L(w) + 10n+7
R2 K(w,0,m) --> K(x, m+1+u, 0) phi(w) = x 1 0^(2u) steps L(w) + 2u+8
R3 K(w,0,m) --> K(x', 0, m+u+2) phi(w) = x' 0 0 1 0^(2u+1) (x'00 may be 0^inf) L(w) + 2u+15
R4 K(w,0,m) --> halt (E1) phi(w) = x 1 1 0^(2u+1)
R5 K(w,0,m) --> nested scan, no rule phi(w) = x 1 0 1 0^(2u+1)
L(w) = 1 if c0 = 0, else 2e+3 with (e,e+1) as in phi
N+1 = (2k+1) 2^i, b = m+1+i, L = bitlen(k), r = k - 2^(L-1), tz = number of trailing 0 bits
S0 S(std,N,m) --> S(std, b, b) k = 0
S1 S(std,N,m) --> S(pk, 2k+b, b) k >= 1, and k = 2^(L-1) or 2k+b >= 2^(L+1)
S2 S(std,N,m) --> S(std, b+L+3, b+L+3) k not a power of 2, 2k+b+1 = 2^(L+1)
S3 S(std,N,m) --> S(std, D+n, n) k not a power of 2, k < 3*2^(L-2), 3*2^(L-1) < 2k+b+1 < 2^(L+1)
P0 S(pk,N,m) --> S(std, b+1, b+1) k = 0
P1 S(pk,N,m) --> S(std, k+b, b) k >= 1, k = 2^(L-1)
P2 S(pk,N,m) --> S(std, 2r+b, b) r >= 1, 2r+b >= 2^L
P3 S(pk,N,m) --> S(std, b+L+1, b+L+1) r >= 1, 2r+b+1 = 2^L
P4 S(pk,N,m) --> S(pk, D+n, n) 1 <= r < 2^(L-2), 2^(L-1) < 2r+b+1 < 2^L
S3/P4: v = 2k+b+1-3*2^(L-1) (S3) or 2r+b+1-2^(L-1) (P4); u = tz(v), h = L-2-u, g = v >> (u+1), n = b+1+u;
D = 3*2^h if g = 0 (S3a/P4a); D = 2^(h+1)+2g if g >= 1 and n >= 2^(h+1)-2g (S3b/P4b)
each rule runs to the FIRST overflow state K(w',0,m') with w' clean and N' >= 1; S2 and P0 pass through
K(0^inf,0,M) = S(std,0,M) on the way (M = b+L+2 / b; not in I), and leave it by S0
invariant I(typ,N,m): 1 <= m <= N (pk: N >= 2), and
N = m (mod 2): std: 2N <= 3m+6 (N even), N <= 2m+3 (N odd); pk: N <= 2m+3 (N even), 2N <= 5m+6 (N odd)
N != m (mod 2): N <= m+3
I(s) -> exactly one of S0..S3, P0..P4 applies to s, and I holds at its result
start: c0 -->(32) K(1,0,1) = S(std,1,1), which satisfies I
5FamilyCheck: related machines are killed together or have a reason to be left open.
1 machines, 1 killed, 0 not. Family links: status.json parent, same transition table with another start (tools/dashboard.py), targeting.md follow-on rows, ledger "= twin" notes. A machine string named in a .v header / proof.md / notes.md is listed but does not make a family.
| who | machine | status | relation to this kill |
|---|---|---|---|
| W4-2 kill 18 | 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF | ✓Killed: never halts | this kill |
| Named in a file but not linked (not counted as family) | |||
| W5-1 kill 23 | 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- | ✓Killed: never halts | named in W4-2's proof.md; named in W4-2's notes.md; named in W5-1's proof.md · review · mechanism |
| W5-4 kill 31 | 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB | ✓Killed: never halts | named in W5-4's proof.md; named in W5-4's notes.md · review · mechanism |
6ChecklistCheck: every ✓ is computed; the two ○ are yours to decide; an amber ! is an optional check that did not finish.
- ✓Machine string exactthe .v literal == holdout list line 240 byte for byte
- ✓Statement is
~halts tm c0parsed from the .v and confirmed by check_kill (theorem_text, theorem_rocq) - ✓No axioms beyond baseline0 assumption(s); tools/assumptions_baseline.txt allows only functional_extensionality_dep
- ✓coqchk finished (optional)coqchk pass in 29.58 s
- ✓.v hash matches the checked hash.v = checked sha256 20521ad7e528…; submission/ copy = checked sha256 20521ad7e528…
- ✓No repo-local paths in the .vcomments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own
verify/X.vis fine: none in the .v or the submission/ copy - ✓Public write-up is cleantools/writeup_lint.py on
submission/proof.md: 0 error(s) - ○proof.md reviewed by Dennis (Checkpoint B)no Checkpoint B note from Dennis found
- notes.md L130: - proof.md has had no skeptic review yet (Checkpoint B, non-blocking).
- notes.md L134: proof.md is now a complete informal proof (Checkpoint B pending, non-blocking). check_proof.py is new and self-contained: 133/133 PASS with seed 1 `--full` and seed 2 default. Logs: `work/check_proof_full_seed1.log`, `wo
- notes.md L187: - Still open: 349 `1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---` (740 line 349, sheet row 1038) is covered by the same mathematics (proof.md §7.3) but not formalized; route in status.json `family_note`. Checkpoint B had no
- proof.md L387: ## 10. Checkpoint B (Dennis)
- proof.md L414: - Open: Checkpoint B; a skeptic pass by a second agent; formalization (§8).
- proof.md L427: - **Open.** Checkpoint B (Dennis); formalization (§8), including a solo timing of TM518's `solve_eqv` for 349.
- ○Family posted together?no other kill in the family
Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.0 s from the files linked above; nothing in this review is hand-written except the box “How we proved it never halts” (above), which quotes how_proved.md. Re-run: python3 -B tools/killreview.py 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF
Files
machines/<tm>/: 14 entries · raw notes, status, scripts, images
| name | size | changed |
|---|---|---|
| notes.md ↓ | 18 KB | 2026-10-11 11:04 |
| proof.md ↓ | 41 KB | 2026-10-11 09:58 |
| how_proved.md ↓ | 1.5 KB | 2026-10-14 10:51 |
| status.json ↓ | 1.3 KB | 2026-10-11 11:04 |
| observe.json ↓ | 13 KB | 2026-10-11 09:02 |
| deepen.json ↓ | 4.7 KB | 2026-10-11 09:30 |
| 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v ↓ | 47 KB | 2026-10-11 10:52 |
| decisions/ | 1 item | 2026-10-11 09:02 |
| img/ | 9 items | 2026-10-11 08:56 |
| rocq/ | 22 items | 2026-10-11 11:02 |
| scripts/ | 5 items | 2026-10-11 08:23 |
| submission/ | 5 items | 2026-10-11 11:03 |
| work/ | 22 items | 2026-10-11 11:05 |
| check_proof.py ↓ | 56 KB | 2026-10-11 09:55 |
status.json in full
{
"tm": "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF",
"status": "KILLED_NONHALT",
"stage": "done",
"updated": "2026-10-11",
"reason": "check_kill PASS, independently re-verified",
"label": "W4-2",
"template": "verify/BECv5.v, Module TM1 / Module TM2 (same table except F1)",
"kill": {
"file": "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v",
"sha256": "20521ad7e52872407bf6a03250bdd5064676def5b770fd65ab06eb49026238f1",
"check_kill": "PASS (fresh run 2026-10-11T17:59:26Z: compile 65.8 s native, coqchk pass 29.6 s, 0 assumptions)",
"submission": "submission/"
},
"family_note": "349 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (740 line 349, sheet row 1038) is Eqv_v3 TM518 tm'; TM518 tm is this table mirrored and renamed, started in F; the same mathematics covers it (proof.md 7.3), not formalized. Route: TM518.eqv + flip_halts_c0 + perm_nonhalt + 73-step start from F + step_I.",
"funded": {
"option": "hunt",
"date": "2026-10-11"
},
"proof": {
"file": "proof.md",
"check": "check_proof.py",
"result": "PASS 147/147 (seed 1 --full; seed 1 default; seed 2 default)",
"date": "2026-10-11"
},
"review": {
"skeptic_round_1": {
"date": "2026-10-11",
"sound": true,
"gaps": 2,
"severity": "minor, minor",
"outcome": "both fixed and re-checked"
}
}
}observe.json contract (tools/README-card.md):
3 contract warnings
- rank: missing
- diagrams: 6 (want 3-5)
- diagrams[5].window: not "cells A..B, 1 px = k cells"