Our proof vs its template, SOMDCv6.v Module TM7

1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- was proved by extending mxdys's TM7 from vendor/busycoq/verify/SOMDCv6.v, a machine that differs in one transition. This page measures how much of TM7's proof text we kept, and shows every difference.

1The machines

What to notice: one cell of 12 differs: A1 is 0RC in TM7 and 0RF in #2. TM8 differs in the same cell (0LC) and uses TM7's proof text.

#2 (ours)the holdout we proved

	read 0	read 1
A	1RB	0RF
B	1LC	0RE
C	0LC	0LD
D	1RD	1LB
E	0RF	1RA
F	0RB	halt

TM7SOMDCv6.v, our template

	read 0	read 1
A	1RB	0RC
B	1LC	0RE
C	0LC	0LD
D	1RD	1LB
E	0RF	1RA
F	0RB	halt

TM8SOMDCv6.v, same proof text as TM7

	read 0	read 1
A	1RB	0LC
B	1LC	0RE
C	0LC	0LD
D	1RD	1LB
E	0RF	1RA
F	0RB	halt

Machine strings (A1 marked)

1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- #2

1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- TM7

1RB0LC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- TM8

A1 = state A reading a 1

#2 0RF: write 0, move right, go to F
TM7 0RC: write 0, move right, go to C
TM8 0LC: write 0, move left, go to C

Cells that differ (of 12)

#2 vs TM7: 1 (A1) · #2 vs TM8: 1 (A1) · TM7 vs TM8: 1 (A1)
TM8's module body differs from TM7's in 1 of 244 lines: the tm line. So everything below holds for TM8 too, except the TM string.

Open #2 vs TM7 in the explorer → preset p2-vs-tm7: both machines from the same start; the dashed line is A1's first firing. d = diff view.

2Similarity at a glance

What to notice: 150 of TM7's 225 non-blank lines (67%) appear unchanged in ours. Ours is 2.3× longer, almost all of it added lines (376), not edits (7).

599

lines in ours
533 non-blank

246

lines in Module TM7
SOMDCv6.v 1626–1871

261

TM7 body + shared header
225 non-blank; what we diff against

150/225

TM7 lines kept verbatim (67%)
they are 28% of ours

2.3×

longer than TM7 + header
2.4× the module alone

Non-blank lines by diff status (same scale)

TM7 + shared header225 non-blank of 261 lines

150 identical

68 TM7 only

150 identical 7 changed 68 TM7 only (removed)

#2 (ours)533 non-blank of 599 lines

150 identical

376 ours only

150 identical 7 changed 376 ours only (added)

2 of the 150 identical lines are a Proof. and a Qed. that difflib matched across different lemmas (TM7 RIncs_nxt L1793 ↔ ours End_x L307; TM7 RIncs_nxt L1835 ↔ ours inv_h1_d0 L349). The Definition tm line counts as identical because the TM string is replaced by <TM> before diffing (section 1 shows the real difference). 1 of the 7 changed lines differ only in whitespace.

Where the identical lines are (each file drawn to the same scale, all lines; hover or click a band)

Hover a band: grey = identical run, amber = changed, red = TM7 only, green = ours only. Click to jump to it in section 4.

Items by tag and kind

	Lemma	Definition	Inductive	Ltac	Notation	other	all
identical	2	4	2	7	11	3	29
adapted	2	1	1	·	·	·	4
new	21	1	1	1	1	8	33
TM7-only	1	·	·	2	·	·	3
rows	26	6	4	10	12	11	69

"other" = imports, Open/Close Scope and comments; Definition includes Fixpoint (toRC). Lemmas: TM7 5, ours 25. Named items (Lemma, Definition, Fixpoint, Inductive, Ltac, Notation): TM7 33, ours 55.

How the numbers are computed

TM7 side = SOMDCv6.v lines 1–17 (shared header) + 1627–1870 (Module TM7 body). The Module TM7. / End TM7. lines are left out.
That is byte-identical to rocq-scratch/TM7_toplevel.v: yes (sha256 642086b1c911…).
Line diff: Python difflib.ndiff on lines with trailing spaces trimmed, blank lines treated as junk, and the TM string replaced by <TM> in both files. A removed line and an added line count as one changed line when ndiff pairs them (similarity cutoff 0.75).
Items: every top-level sentence starting with Lemma / Definition / Fixpoint / Inductive / Ltac / Notation, plus imports, scopes and comments. Paired by name; RIncs_nxt is paired by role with key. identical = the same text (trailing spaces and blank lines ignored, TM string not normalized, so tm is adapted).
Built by compare/build.py; all numbers also in compare/stats.json.

3Item by item

What to notice: 29 items are identical and only 4 are adapted (tm, RIncs, RIncs_spec, nonhalt). The bulk is 33 new items. Open a row for its word diff or code.

tagkindTM7 (SOMDCv6.v line)ours (.v line)what it is / what changed

newcomment—(* header comment *) L1 8 linescomment (ours only)

1(* 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- never halts.
2   Bell eats counter. Adapted from verify/SOMDCv6.v, Module TM7
3   (1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---), which differs only in A1 (0RC there, 0RF here).
4   Here every L digit that a sweep enters fires one extra h pass, a +1 on the digits to its right.
5   Informal proof: the accompanying write-up (proof.md).
6   Formalized with Claude Code (AI-assisted).
7   Checked: compiles against unmodified busycoq (commit 0940bb9) with Coq 8.20.1;
8   Print Assumptions nonhalt: Closed under the global context. *)

identicalimportsimports L1 5 linesimports L10 5 linesIndividual62 (machine + segment machinery), Longitudinal, DivModCases, stdlib.

Identical text in both files: TM7 L1–5, ours L10–14.

10From BusyCoq Require Import Individual62 Longitudinal DivModCases.
11Require Import ZifyNat Lia.
12Require Import ZArith.
13Require Import String.
14Require Import List.

identicalLtacesc L8 4 linesesc L17 4 linesproves a concrete segRLs / sideRLs goal by computation

Identical text in both files: TM7 L8–11, ours L17–20.

17Ltac esc :=
18  (apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) ||
19  (apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) ||
20  (eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity | st; reflexivity]).

identicalLtacec L13 1 lineec L22 1 lineeconstructor

Identical text in both files: TM7 L13–13, ours L22–22.

22Ltac ec := econstructor.

identicalLtacam L15 2 linesam L24 2 linessegRLs over h^^(k*a+b) from two concrete facts (binary-counter digits)

Identical text in both files: TM7 L15–16, ours L24–25.

24Ltac am a a' k b b' :=
25  applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc.

adaptedDefinitiontm L1627 1 linetm L27 1 linethe only difference between the machines: A1 = 0RC (TM7) vs 0RF (ours)

Word diff, TM7 L1627–1627 → ours L27–27: 29 of TM7's 30 tokens kept, ours has 30. ~~struck red~~ = TM7 only, green = ours only. Line by line in section 4 ↓

Definition tm := Eval compute in (TM_from_str "1RB0RC0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").

identicalNotation"c -->* c'" L1628 1 line"c -->* c'" L28 1 linec reaches c' in zero or more steps of tm

Identical text in both files: TM7 L1628–1628, ours L28–28.

28Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).

identicalNotation"c -->+ c'" L1629 1 line"c -->+ c'" L29 1 linec reaches c' in one or more steps of tm

Identical text in both files: TM7 L1629–1629, ours L29–29.

29Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

identicalNotationld L1631 1 lineld L31 1 linedigit L = 110

Identical text in both files: TM7 L1631–1631, ours L31–31.

31Notation ld := [1;1;0].

identicalNotationd0 L1632 1 lined0 L32 1 linedigit 0 = 000

Identical text in both files: TM7 L1632–1632, ours L32–32.

32Notation d0 := [0;0;0].

identicalNotationd1 L1633 1 lined1 L33 1 linedigit 1 = 100

Identical text in both files: TM7 L1633–1633, ours L33–33.

33Notation d1 := [1;0;0].

newNotation—w1ld L34 1 linethe word 1110 (the drain pass enters an L with a stray 1 in front); declared before Open Scope nat

34Notation w1ld := [1;1;1;0].

identicalNotationhR L1634 1 linehR L35 1 linea visit entering from the left in state B

Identical text in both files: TM7 L1634–1634, ours L35–35.

35Notation hR := (B,@nil Sym).

identicalNotationhR' L1635 1 linehR' L36 1 linea visit entering in state D with a 1 on its left

Identical text in both files: TM7 L1635–1635, ours L36–36.

36Notation hR' := (D,[1]).

identicalNotationhL L1636 1 linehL L37 1 linea visit leaving to the left in state C

Identical text in both files: TM7 L1636–1636, ours L37–37.

37Notation hL := (C,@nil Sym).

identicalNotationh L1637 1 lineh L38 1 linethe drain-pass visit (in as B, out as C); in ours also the +1 pass

Identical text in both files: TM7 L1637–1637, ours L38–38.

38Notation h := [(hR,hL)].

identicalNotationh' L1638 1 lineh' L39 1 linethe eater visit (in as D after a 1, out as C)

Identical text in both files: TM7 L1638–1638, ours L39–39.

39Notation h' := [(hR',hL)].

identicalInductiveRD L1640 1 lineRD L41 1 linethe three digits

Identical text in both files: TM7 L1640–1640, ours L41–41.

41Inductive RD := LD|D0|D1.

identicalInductiveH L1641 1 lineH L42 1 linesweep modes: hx = eater, h1 = drain (count mode)

Identical text in both files: TM7 L1641–1641, ours L42–42.

42Inductive H := hx|h1.

identicalFixpointtoRC L1643 7 linestoRC L44 7 linesdigit list -> right half of the tape

Identical text in both files: TM7 L1643–1649, ours L44–50.

44Fixpoint toRC ls :=
45match ls with
46| [] => 0inf
47| LD::ls => ld*>toRC ls
48| D0::ls => d0*>toRC ls
49| D1::ls => d1*>toRC ls
50end.

identicalDefinitiontoH' L1651 5 linestoH' L52 5 linesthe extra cell in front of the digits (h1: a stray 1)

Identical text in both files: TM7 L1651–1655, ours L52–56.

52Definition toH' x :=
53match x with
54| hx => []
55| h1 => [1]
56end.

identicalDefinitiontoH L1657 5 linestoH L58 5 linesthe first visit of each mode

Identical text in both files: TM7 L1657–1661, ours L58–62.

58Definition toH x :=
59match x with
60| hx => h'
61| h1 => []
62end.

newcomment—(* one h pass over the digits = +1 on t… *) L64 1 linecomment (ours only)

64(* one h pass over the digits = +1 on the little-endian binary number of the 0/1 digits, L skipped *)

newInductive—Inc L65 5 linesnew: one h pass = +1 on the 0/1 digits (little-endian binary, L skipped)

65Inductive Inc: list RD -> list RD -> Prop :=
66| Inc_nil: Inc [] [D1]
67| Inc_d0 r: Inc (D0::r) (D1::r)
68| Inc_d1 r r': Inc r r' -> Inc (D1::r) (D0::r')
69| Inc_ld r r': Inc r r' -> Inc (LD::r) (LD::r').

adaptedInductiveRIncs L1663 31 linesRIncs L71 37 linesthe sweep as a relation. 2 L clauses gain an Inc premise; 2 new end clauses Z1, Z0

Word diff, TM7 L1663–1701 → ours L71–118: 322 of TM7's 324 tokens kept, ours has 360. ~~struck red~~ = TM7 only, green = ours only. Line by line in section 4 ↓

Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=
| RIncs_hx_ld k r r1 r':
  Inc r r1 ->
  RIncs hx (1+k) rr1 r' ->
  RIncs hx k (LD::r) (LD::r')

| RIncs_hx_d1 k r r':
  RIncs h1 k r r' ->
  RIncs hx k (D1::r) (LD::r')

| RIncs_hx_d0 k r r':
  RIncs hx (1+k) r r' ->
  RIncs hx k (D0::r) (LD::r')

| RIncs_h1_ld k r r1 r':
  Inc r r1 ->
  RIncs hx (1+k) rr1 r' ->
  RIncs h1 (1+k) (LD::r) (LD::r')

| RIncs_h1_d1 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (1+k) (D1::r) (LD::r')

| RIncs_h1_d0_0 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (1+k*2) (D0::r) (D0::r')

| RIncs_h1_d0_1 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (2+k*2) (D0::r) (D1::r')

| RIncs_h1_rh_0:
  RIncs h1 0 [] [D1]

| RIncs_h1_rh_1 k r':
  RIncs h1 k [] r' ->
  RIncs h1 (1+k*2) [] (D0::r')


| RIncs_h1_rh_2 k r':
  RIncs h1 k [] r' ->
  RIncs h1 (2+k*2) [] (D1::r')

| RIncs_h1_z1:
  RIncs h1 0 [D1] [LD]

| RIncs_h1_z0:
  RIncs h1 0 [D0] [D1]
.

identicalLtaccat3 L1703 2 linescat3 L120 2 linespeel one 3-cell digit off the side

Identical text in both files: TM7 L1703–1704, ours L120–121.

120Ltac cat3 :=
121  eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]); [|eauto 1].

identicalLtactr1 L1706 3 linestr1 L123 3 linessplit h^^(1+k): first visit by computation

Identical text in both files: TM7 L1706–1708, ours L123–125.

123Ltac tr1 :=
124  rewrite lpow_add,app_assoc;
125  eapply segRLs_trans; [esx | ].

identicalLtacwal L1710 2 lineswal L127 2 linesk identical visits through a wall word

Identical text in both files: TM7 L1710–1711, ours L127–128.

127Ltac wal :=
128  eapply segRLs_wall''; esx.

identicalLtactr2 L1713 2 linestr2 L130 2 linesa leading sideRLs step

Identical text in both files: TM7 L1713–1714, ours L130–131.

130Ltac tr2 :=
131  eapply sideRLs_trans; [esx | ].

newLemma—z1_eq L133 4 linestape identity 1 100 0^inf = 110 0^inf, used by clause Z1

133Lemma z1_eq: [1] *> d1 *> 0inf = ld *> 0inf.
134Proof.
135  cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold.
136Qed.

newLemma—z0_eq L138 4 linestape identity 1 000 0^inf = 100 0^inf, used by clause Z0

138Lemma z0_eq: [1] *> d0 *> 0inf = d1 *> 0inf.
139Proof.
140  cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold.
141Qed.

identicalscopeOpen Scope nat L1716 1 lineOpen Scope nat L143 1 line

Identical text in both files: TM7 L1716–1716, ours L143–143.

143Open Scope nat.

newLemma—Inc_spec L145 12 linesnew: Inc is what one h pass does on the tape (sideRLs tm h)

145Lemma Inc_spec r r':
146  Inc r r' ->
147  sideRLs tm h (toRC r) (toRC r').
148Proof.
149  intro H.
150  induction H; cbn[toRC].
151  - esc.
152  - change h with (h++[]).
153    eapply segRLs_sideRLs_concat; [esx | constructor].
154  - eapply (@segRLs_sideRLs_concat tm h h); [esx | apply IHInc].
155  - eapply (@segRLs_sideRLs_concat tm h h); [esx | apply IHInc].
156Qed.

newLemma—seg_hx_ld L158 7 linesnew segment fact: the eater entering an L now emits h ++ h' ++ h^^(1+k)

158Lemma seg_hx_ld k:
159  segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld.
160Proof.
161  rewrite lpow_add.
162  change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
163  eapply segRLs_trans; [esx | wal].
164Qed.

newLemma—seg_h1_ld L166 7 linesnew segment fact: a drain pass entering an L (word 1110) emits h ++ h' ++ h^^(1+k)

166Lemma seg_h1_ld k:
167  segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) w1ld ld.
168Proof.
169  rewrite lpow_add.
170  change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
171  eapply segRLs_trans; [esx | wal].
172Qed.

adaptedLemmaRIncs_spec L1718 39 linesRIncs_spec L174 48 linessoundness of RIncs. 8 bullets verbatim, the 2 L bullets rewritten, 2 bullets added (Z1, Z0)

Word diff, TM7 L1718–1756 → ours L174–221: 248 of TM7's 264 tokens kept, ours has 361. ~~struck red~~ = TM7 only, green = ours only. Line by line in section 4 ↓

Lemma RIncs_spec tp k r r':
  RIncs tp k r r' ->
  sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').
Proof.
  intro H.
  induction H; intros; cbn[toH toH' toRC] in *.
  - cat3eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]).
    1: apply seg_hx_ld.
    eapply sideRLs_trans.
    1: apply Inc_spec; tr1;eassumption.
    apply walIHRIncs.
  - tr2.
    cat3; wal.
  - cat3; tr1; wal.
  - rewritechange lpow_add,app_assoc([] ++ h^^(1+k)) with (h^^1 ++ h^^k).
    eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]).
    1: apply seg_h1_ld.
    eapply sideRLs_trans.
    1: apply Inc_spec; [|eauto 1]eassumption.
    tr1;apply walIHRIncs.
  - rewrite lpow_add,app_assoc.
    tr2.
    cat3; wal.
  - cat3.
    rewrite app_nil_l.
    am 2 1 k 1 1.
    rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.
    tr2; eauto 1.
  - cat3.
    rewrite Nat.add_comm.
    am 2 1 k 2 1.
    rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.
    tr2; eauto 1.
  - esc.
  - rewrite lpow_add,app_assoc.
    tr2.
    cat3.
    rewrite app_nil_l.
    am 2 1 k 0 0.
  - change (2+k*2) with (1+(1+k*2)).
    rewrite lpow_add,app_assoc.
    tr2.
    cat3.
    rewrite app_nil_l.
    am 2 1 k 1 0.
  - cbn[lpow app]. rewrite z1_eq. constructor.
  - cbn[lpow app]. rewrite z0_eq. constructor.
Qed.

newcomment—(* combinatorics of the sweep relation … *) L223 1 linecomment (ours only)

223(* ---------- combinatorics of the sweep relation (no machine) ---------- *)

newLemma—Inc_total L225 9 linesnew: Inc is total

225Lemma Inc_total r: exists r', Inc r r'.
226Proof.
227  induction r as [|d r [r' I]].
228  - eexists; apply Inc_nil.
229  - destruct d; eexists.
230    + apply Inc_ld, I.
231    + apply Inc_d0.
232    + apply Inc_d1, I.
233Qed.

newLemma—Inc_fun L235 5 linesnew: Inc is deterministic

235Lemma Inc_fun r r1 r2: Inc r r1 -> Inc r r2 -> r1 = r2.
236Proof.
237  intro I. gen r2.
238  induction I; intros r2 I2; inversion I2; subst; try reflexivity; f_equal; auto.
239Qed.

newLemma—RIncs_eqk L241 2 linesnew: rewrite the pass count (k = k')

241Lemma RIncs_eqk tp k k' r r': RIncs tp k r r' -> k = k' -> RIncs tp k' r r'.
242Proof. intros; subst; auto. Qed.

newLtac—inc_nil L244 4 linesnew Ltac: invert hypotheses Inc [] _

244Ltac inc_nil :=
245  repeat match goal with
246  | J: Inc [] _ |- _ => inversion J; subst; clear J
247  end.

newcomment—(* proof.md Lemma A: one more pass afte… *) L249 1 linecomment (ours only)

249(* proof.md Lemma A: one more pass after the k passes is +1 on the result *)

newLemma—RIncs_Inc L250 18 linesnew (proof.md Lemma A): one more pass after the k passes = +1 on the result

250Lemma RIncs_Inc tp k r r' r'':
251  RIncs tp k r r' -> Inc r' r'' -> RIncs tp (1+k) r r''.
252Proof.
253  intro I. gen r''.
254  induction I; intros r'' J; inversion J; subst; inc_nil.
255  - eapply RIncs_hx_ld; eauto.
256  - apply RIncs_hx_d1; auto.
257  - apply RIncs_hx_d0; auto.
258  - eapply (RIncs_h1_ld (1+k)); eauto.
259  - apply (RIncs_h1_d1 (1+k)); auto.
260  - eapply RIncs_eqk; [apply RIncs_h1_d0_1; eauto | lia].
261  - eapply RIncs_eqk; [apply (RIncs_h1_d0_0 (1+k)); eauto | lia].
262  - apply (RIncs_h1_rh_1 0), RIncs_h1_rh_0.
263  - eapply RIncs_eqk; [apply RIncs_h1_rh_2; eauto | lia].
264  - eapply RIncs_eqk; [apply (RIncs_h1_rh_1 (1+k)); eauto | lia].
265  - apply (RIncs_h1_d1 0), RIncs_h1_rh_0.
266  - apply (RIncs_h1_d0_0 0), RIncs_h1_rh_0.
267Qed.

identicalLemmaRIncs_nxt_1 L1758 13 linesRIncs_nxt_1 L269 13 linesthe right end always succeeds in count mode

Identical text in both files: TM7 L1758–1770, ours L269–281.

269Lemma RIncs_nxt_1 k:
270  exists r, RIncs h1 k [] r.
271Proof.
272  induction k using lt_wf_ind.
273  destruct k.
274  + ec. ec.
275  + destruct (mod2 k); subst.
276    * epose proof (H0 _ _) as [r I].
277      ec. ec. apply I.
278    * epose proof (H0 _ _) as [r I].
279      ec. ec. apply I.
280  Unshelve. all: lia.
281Qed.

newLemma—End_1 L283 21 linesnew: right-end cases; TM7 did r = [] inside RIncs_nxt by an inner induction on k

283Lemma End_1 m w:
284  RIncs h1 m [] w -> forall q, m <= q -> exists w', RIncs h1 q w w'.
285Proof.
286  intro I. remember h1 as t. remember (@nil RD) as e.
287  induction I; intros q Hq; try discriminate; subst.
288  - destruct q as [|q].
289    + eexists; apply RIncs_h1_z1.
290    + destruct (RIncs_nxt_1 q) as [w I].
291      eexists; apply (RIncs_h1_d1 q), I.
292  - specialize (IHI eq_refl eq_refl).
293    destruct (mod2 q) as [b Hb|b Hb]; subst q.
294    + destruct b as [|b]; [lia|].
295      destruct (IHI b) as [w I2]; [lia|].
296      eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 | lia].
297    + destruct (IHI b) as [w I2]; [lia|].
298      eexists; apply RIncs_h1_d0_0, I2.
299  - specialize (IHI eq_refl eq_refl).
300    destruct q as [|q]; [lia|].
301    destruct (IHI q) as [w I2]; [lia|].
302    eexists; apply (RIncs_h1_d1 q), I2.
303Qed.

newLemma—End_x L305 13 linesnew: as End_1, ending in eater mode

305Lemma End_x m w:
306  RIncs h1 m [] w -> forall q, m <= 2*q+2 -> exists w', RIncs hx q w w'.
307Proof.
308  intro I. remember h1 as t. remember (@nil RD) as e.
309  induction I; intros q Hq; try discriminate; subst.
310  - destruct (RIncs_nxt_1 q) as [w I].
311    eexists; apply RIncs_hx_d1, I.
312  - specialize (IHI eq_refl eq_refl).
313    destruct (IHI (1+q)) as [w I2]; [lia|].
314    eexists; apply RIncs_hx_d0, I2.
315  - destruct (End_1 _ _ I q) as [w I2]; [lia|].
316    eexists; apply RIncs_hx_d1, I2.
317Qed.

newcomment—(* inversion helpers *) L319 1 linecomment (ours only)

319(* inversion helpers *)

newLemma—inv_hx_ld L320 3 linesnew: inversion helper used by key (TM7's RIncs_nxt used solve_v1/solve_v2 instead)

320Lemma inv_hx_ld k r rK: RIncs hx k (LD::r) rK ->
321  exists r1 rK', Inc r r1 /\ RIncs hx (1+k) r1 rK' /\ rK = LD::rK'.
322Proof. intro E; inversion E; subst; do 2 eexists; repeat split; eauto. Qed.

newLemma—inv_hx_d1 L324 3 linesnew: inversion helper used by key (TM7's RIncs_nxt used solve_v1/solve_v2 instead)

324Lemma inv_hx_d1 k r rK: RIncs hx k (D1::r) rK ->
325  exists rK', RIncs h1 k r rK' /\ rK = LD::rK'.
326Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.

newLemma—inv_hx_d0 L328 3 linesnew: inversion helper used by key (TM7's RIncs_nxt used solve_v1/solve_v2 instead)

328Lemma inv_hx_d0 k r rK: RIncs hx k (D0::r) rK ->
329  exists rK', RIncs hx (1+k) r rK' /\ rK = LD::rK'.
330Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.

newLemma—inv_h1_ld L332 3 linesnew: inversion helper used by key (TM7's RIncs_nxt used solve_v1/solve_v2 instead)

332Lemma inv_h1_ld k r rK: RIncs h1 (1+k) (LD::r) rK ->
333  exists r1 rK', Inc r r1 /\ RIncs hx (1+k) r1 rK' /\ rK = LD::rK'.
334Proof. intro E; inversion E; subst; do 2 eexists; repeat split; eauto. Qed.

newLemma—inv_h1_d1 L336 3 linesnew: inversion helper used by key (TM7's RIncs_nxt used solve_v1/solve_v2 instead)

336Lemma inv_h1_d1 k r rK: RIncs h1 (1+k) (D1::r) rK ->
337  exists rK', RIncs h1 k r rK' /\ rK = LD::rK'.
338Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.

newLemma—inv_h1_d0 L340 10 linesnew: inversion helper used by key (TM7's RIncs_nxt used solve_v1/solve_v2 instead)

340Lemma inv_h1_d0 K r rK: RIncs h1 K (D0::r) rK ->
341  (exists A rK', K = 1+A*2 /\ RIncs h1 A r rK' /\ rK = D0::rK') \/
342  (exists A rK', K = 2+A*2 /\ RIncs h1 A r rK' /\ rK = D1::rK') \/
343  (K = 0 /\ r = [] /\ rK = [D1]).
344Proof.
345  intro E; inversion E; subst.
346  - left; do 2 eexists; repeat split; eauto.
347  - right; left; do 2 eexists; repeat split; eauto.
348  - right; right; auto.
349Qed.

newLemma—inv_z1 L351 8 linesnew: inversion helper used by key (TM7's RIncs_nxt used solve_v1/solve_v2 instead)

351Lemma inv_z1 K rK: RIncs h1 K [D1] rK ->
352  (K = 0 /\ rK = [LD]) \/
353  (exists K0 rK', K = 1+K0 /\ RIncs h1 K0 [] rK' /\ rK = LD::rK').
354Proof.
355  intro E; inversion E; subst.
356  - right; do 2 eexists; repeat split; eauto.
357  - left; auto.
358Qed.

newcomment—(* proof.md section 3.3: the second swe… *) L360 1 linecomment (ours only)

360(* proof.md section 3.3: the second sweep reads the first's output after j pending +1s *)

newDefinition—Inv L361 7 linesnew: the case condition of the domain lemma; with j = 0 it is TM7's RIncs_nxt condition

361Definition Inv tp k j tq q :=
362  match tp, tq with
363  | hx, hx => k <= q /\ j <= q
364  | h1, hx => k+1 <= q /\ j <= q
365  | h1, h1 => (j = 0 /\ 2*k+1 <= q) \/ (1 <= j /\ k+j <= q /\ 1 <= q)
366  | hx, h1 => False
367  end.

TM7-onlyLtacsolve_v2 L1773 2 lines—TM7 automation for RIncs_nxt's case list; ours writes key's cases out

1773Ltac solve_v2 :=
1774  (epose proof (RIncs_nxt_1 _) as [r I]; repeat ec; try apply I).

TM7-onlyLtacsolve_v1 L1776 6 lines—TM7 automation for RIncs_nxt's case list; ours writes key's cases out

1776Ltac solve_v1 H tp'0 k'0 H' :=
1777  eapply H with (tp':=tp'0) (k':=k'0) in H';
1778  try lia;
1779  try (
1780  destruct H' as [r'' I1];
1781  repeat ec; try apply I1).

TM7-onlyLemmaRIncs_nxt L1783 53 lines—TM7's domain lemma; replaced by key (next row)

1783Lemma RIncs_nxt tp k r r' tp' k':
1784  RIncs tp k r r' ->
1785  match tp,tp' with
1786  | hx,hx => k<=k'
1787  | h1,h1 => k*2+1<=k'
1788  | h1,hx => k+1<=k'
1789  | _,_ => False
1790  end ->
1791  exists r'',
1792  RIncs tp' k' r' r''.
1793Proof.
1794  gen tp k r' tp' k'.
1795  induction r; intros.
1796  {
1797    gen tp r' tp' k'.
1798    induction k using lt_wf_ind.
1799    intros.
1800    inverts H1; destruct tp'.
1801    all: try lia.
1802    - solve_v2.
1803    - destruct (sub k' 1); [subst|lia].
1804      solve_v2.
1805    - solve_v1 H0 hx (1+k') H3.
1806    - destruct (sub k' 1); [subst|lia].
1807      destruct (mod2 c); subst.
1808      + solve_v1 H0 h1 (a) H3.
1809      + solve_v1 H0 h1 (a) H3.
1810    - solve_v1 H0 h1 (k') H3.
1811    - destruct (sub k' 1); [subst|lia].
1812      solve_v1 H0 h1 (c) H3.
1813  }
1814  {
1815    inverts H0; destruct tp'.
1816    all: try lia.
1817    - solve_v1 IHr hx (1+k') H7.
1818    - solve_v1 IHr hx (1+k') H7.
1819    - solve_v1 IHr hx (1+k') H7.
1820    - solve_v1 IHr hx (1+k') H7.
1821    - destruct (sub k' 1); [subst|lia].
1822      solve_v1 IHr hx (1+c) H7.
1823    - solve_v1 IHr hx (1+k') H7.
1824    - destruct (sub k' 1); [subst|lia].
1825      solve_v1 IHr hx (1+c) H7.
1826    - solve_v1 IHr hx (1+k') H7.
1827    - destruct (sub k' 1); [subst|lia].
1828      destruct (mod2 c); subst.
1829      + solve_v1 IHr h1 (a) H7.
1830      + solve_v1 IHr h1 (a) H7.
1831    - solve_v1 IHr h1 k' H7.
1832    - destruct (sub k' 1); [subst|lia].
1833      solve_v1 IHr h1 (c) H7.
1834  }
1835Qed.

newLemma—key L369 158 linestakes over RIncs_nxt's job (proof.md 3.3 calls it RIncs_nxt'): adds j pending +1 passes; induction on the derivation, not on r

Statements side by side: TM7's RIncs_nxt (with its case condition inline) vs ours key (case condition in Inv). With j = 0, Inv is exactly TM7's condition.

1783Lemma RIncs_nxt tp k r r' tp' k':
1784  RIncs tp k r r' ->
1785  match tp,tp' with
1786  | hx,hx => k<=k'
1787  | h1,h1 => k*2+1<=k'
1788  | h1,hx => k+1<=k'
1789  | _,_ => False
1790  end ->
1791  exists r'',
1792  RIncs tp' k' r' r''.

361Definition Inv tp k j tq q :=
362  match tp, tq with
363  | hx, hx => k <= q /\ j <= q
364  | h1, hx => k+1 <= q /\ j <= q
365  | h1, h1 => (j = 0 /\ 2*k+1 <= q) \/ (1 <= j /\ k+j <= q /\ 1 <= q)
366  | hx, h1 => False
367  end.

369Lemma key tp k r r1:
370  RIncs tp k r r1 ->
371  forall j rK tq q,
372  RIncs tp (k+j) r rK ->
373  Inv tp k j tq q ->
374  exists r2, RIncs tq q rK r2.

Full text of key (158 lines):

369Lemma key tp k r r1:
370  RIncs tp k r r1 ->
371  forall j rK tq q,
372  RIncs tp (k+j) r rK ->
373  Inv tp k j tq q ->
374  exists r2, RIncs tq q rK r2.
375Proof.
376  intro D.
377  induction D as [k r r1 r' Hi D IH | k r r' D IH | k r r' D IH
378                 | k r r1 r' Hi D IH | k r r' D IH | a r r' D IH | a r r' D IH
379                 | | a r' D IH | a r' D IH | | ];
380    intros j rK tq q E HI.
381  - (* hx_ld *)
382    destruct (inv_hx_ld _ _ _ E) as [r1' [rK' [Hi' [E' ->]]]].
383    rewrite (Inc_fun _ _ _ Hi' Hi) in E'.
384    destruct tq; cbn in HI; [|contradiction].
385    destruct (Inc_total rK') as [rK'' J].
386    destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
387    + eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
388    + cbn; lia.
389    + eexists; eapply RIncs_hx_ld; eassumption.
390  - (* hx_d1 *)
391    destruct (inv_hx_d1 _ _ _ E) as [rK' [E' ->]].
392    destruct tq; cbn in HI; [|contradiction].
393    destruct (Inc_total rK') as [rK'' J].
394    destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
395    + eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
396    + cbn; lia.
397    + eexists; eapply RIncs_hx_ld; eassumption.
398  - (* hx_d0 *)
399    destruct (inv_hx_d0 _ _ _ E) as [rK' [E' ->]].
400    destruct tq; cbn in HI; [|contradiction].
401    destruct (Inc_total rK') as [rK'' J].
402    destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
403    + eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
404    + cbn; lia.
405    + eexists; eapply RIncs_hx_ld; eassumption.
406  - (* h1_ld *)
407    destruct (inv_h1_ld (k+j) _ _ E) as [r1' [rK' [Hi' [E' ->]]]].
408    rewrite (Inc_fun _ _ _ Hi' Hi) in E'.
409    destruct (Inc_total rK') as [rK'' J].
410    destruct tq; cbn in HI.
411    + destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
412      * eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
413      * cbn; lia.
414      * eexists; eapply RIncs_hx_ld; eassumption.
415    + destruct q as [|q0]; [lia|].
416      destruct (IH (1+j) rK'' hx (S q0)) as [r2 I2].
417      * eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
418      * cbn; lia.
419      * eexists; eapply (RIncs_h1_ld q0); eassumption.
420  - (* h1_d1 *)
421    destruct (inv_h1_d1 (k+j) _ _ E) as [rK' [E' ->]].
422    destruct (Inc_total rK') as [rK'' J].
423    destruct tq; cbn in HI.
424    + destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
425      * eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
426      * cbn; lia.
427      * eexists; eapply RIncs_hx_ld; eassumption.
428    + destruct q as [|q0]; [lia|].
429      destruct (IH (1+j) rK'' hx (S q0)) as [r2 I2].
430      * eapply RIncs_eqk; [eapply RIncs_Inc; eassumption | lia].
431      * cbn; lia.
432      * eexists; eapply (RIncs_h1_ld q0); eassumption.
433  - (* h1_d0_0 *)
434    destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]|[[A [rK' [HK [E' ->]]]]|[HK _]]]; [| |lia].
435    + (* rK = D0::rK' *)
436      assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption | lia]).
437      destruct tq; cbn in HI.
438      * destruct (IH (A-a) rK' hx (1+q) E2) as [r2 I2]; [cbn; lia|].
439        eexists; apply RIncs_hx_d0, I2.
440      * destruct (mod2 q) as [b Hb|b Hb]; subst q.
441        -- destruct b as [|b]; [lia|].
442           destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia|].
443           eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 | lia].
444        -- destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia|].
445           eexists; apply RIncs_h1_d0_0, I2.
446    + (* rK = D1::rK' *)
447      assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption | lia]).
448      destruct tq; cbn in HI.
449      * destruct (IH (A-a) rK' h1 q E2) as [r2 I2]; [cbn; lia|].
450        eexists; apply RIncs_hx_d1, I2.
451      * destruct q as [|q0]; [lia|].
452        destruct (IH (A-a) rK' h1 q0 E2) as [r2 I2]; [cbn; lia|].
453        eexists; apply (RIncs_h1_d1 q0), I2.
454  - (* h1_d0_1 *)
455    destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]|[[A [rK' [HK [E' ->]]]]|[HK _]]]; [| |lia].
456    + (* rK = D0::rK' *)
457      assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption | lia]).
458      destruct tq; cbn in HI.
459      * destruct (IH (A-a) rK' hx (1+q) E2) as [r2 I2]; [cbn; lia|].
460        eexists; apply RIncs_hx_d0, I2.
461      * destruct (mod2 q) as [b Hb|b Hb]; subst q.
462        -- destruct b as [|b]; [lia|].
463           destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia|].
464           eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 | lia].
465        -- destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia|].
466           eexists; apply RIncs_h1_d0_0, I2.
467    + (* rK = D1::rK' *)
468      assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption | lia]).
469      destruct tq; cbn in HI.
470      * destruct (IH (A-a) rK' h1 q E2) as [r2 I2]; [cbn; lia|].
471        eexists; apply RIncs_hx_d1, I2.
472      * destruct q as [|q0]; [lia|].
473        destruct (IH (A-a) rK' h1 q0 E2) as [r2 I2]; [cbn; lia|].
474        eexists; apply (RIncs_h1_d1 q0), I2.
475  - (* rh_0 *)
476    destruct tq; cbn in HI.
477    + eapply End_x; [eassumption | lia].
478    + eapply End_1; [eassumption | lia].
479  - (* rh_1 *)
480    destruct tq; cbn in HI.
481    + eapply End_x; [eassumption | lia].
482    + eapply End_1; [eassumption | lia].
483  - (* rh_2 *)
484    destruct tq; cbn in HI.
485    + eapply End_x; [eassumption | lia].
486    + eapply End_1; [eassumption | lia].
487  - (* z1 *)
488    destruct (inv_z1 _ _ E) as [[HK ->]|[K0 [rK' [HK [E' ->]]]]].
489    + destruct tq; cbn in HI.
490      * destruct (RIncs_nxt_1 (1+q)) as [w I].
491        eexists; eapply RIncs_hx_ld; [apply Inc_nil | apply RIncs_hx_d1, I].
492      * destruct q as [|q0]; [lia|].
493        destruct (RIncs_nxt_1 (1+q0)) as [w I].
494        eexists; eapply (RIncs_h1_ld q0); [apply Inc_nil | apply RIncs_hx_d1, I].
495    + destruct (Inc_total rK') as [rK'' J].
496      pose proof (RIncs_Inc _ _ _ _ _ E' J) as E''.
497      destruct tq; cbn in HI.
498      * destruct (End_x _ _ E'' (1+q)) as [w I]; [lia|].
499        eexists; eapply RIncs_hx_ld; eassumption.
500      * destruct q as [|q0]; [lia|].
501        destruct (End_x _ _ E'' (1+q0)) as [w I]; [lia|].
502        eexists; eapply (RIncs_h1_ld q0); eassumption.
503  - (* z0 *)
504    destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]|[[A [rK' [HK [E' ->]]]]|[HK [_ ->]]]].
505    + destruct tq; cbn in HI.
506      * destruct (End_x _ _ E' (1+q)) as [w I]; [lia|].
507        eexists; apply RIncs_hx_d0, I.
508      * destruct (mod2 q) as [b Hb|b Hb]; subst q.
509        -- destruct b as [|b]; [lia|].
510           destruct (End_1 _ _ E' b) as [w I]; [lia|].
511           eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I | lia].
512        -- destruct (End_1 _ _ E' b) as [w I]; [lia|].
513           eexists; apply RIncs_h1_d0_0, I.
514    + destruct tq; cbn in HI.
515      * destruct (End_1 _ _ E' q) as [w I]; [lia|].
516        eexists; apply RIncs_hx_d1, I.
517      * destruct q as [|q0]; [lia|].
518        destruct (End_1 _ _ E' q0) as [w I]; [lia|].
519        eexists; apply (RIncs_h1_d1 q0), I.
520    + destruct tq; cbn in HI.
521      * destruct (RIncs_nxt_1 q) as [w I].
522        eexists; apply RIncs_hx_d1, I.
523      * destruct q as [|q0]; [lia|].
524        destruct (RIncs_nxt_1 q0) as [w I].
525        eexists; apply (RIncs_h1_d1 q0), I.
526Qed.

newLemma—domain L528 8 linesnew: key at j = 0, the form nonhalt needs

528Lemma domain r r':
529  RIncs hx 0 r r' -> exists r'', RIncs hx 0 r' r''.
530Proof.
531  intro I.
532  eapply (key _ _ _ _ I 0 r' hx 0).
533  - apply I.
534  - cbn; lia.
535Qed.

identicalscopeOpen Scope sym L1837 1 lineOpen Scope sym L538 1 line

Identical text in both files: TM7 L1837–1837, ours L538–538.

538Open Scope sym.

identicalNotationlh L1839 1 linelh L540 1 lineleft part of the boundary configuration

Identical text in both files: TM7 L1839–1839, ours L540–540.

540Notation lh := (0inf<*<[1]).

identicalDefinitionS' L1841 2 linesS' L542 2 linesthe sweep boundary 0^inf 11 D> r 0^inf

Identical text in both files: TM7 L1841–1842, ours L542–543.

542Definition S' r :=
543  lh {{{ (hR',R) }}} toH' hx *> toRC r.

identicalLemmaBigStep L1844 11 linesBigStep L545 11 linesone sweep: S' r -->+ S' r'

Identical text in both files: TM7 L1844–1854, ours L545–555.

545Lemma BigStep r r':
546  RIncs hx 0 r r' ->
547  S' r -->+ S' r'.
548Proof.
549  intros H.
550  apply RIncs_spec in H.
551  unfold S'.
552  eapply sideRLs_1 in H.
553  follow10 H.
554  es.
555Qed.

newLemma—start L557 2 linesnew: c0 -->* S' [LD;D1] by esx (TM7 does its start, to S' [D1], inline inside nonhalt)

557Lemma start: c0 -->* S' [LD;D1].
558Proof. esx. Qed.

adaptedLemmanonhalt L1856 14 linesnonhalt L560 16 linessame statement; start S' [LD;D1], domain instead of RIncs_nxt, explicit witness

Word diff, TM7 L1856–1869 → ours L560–575: 73 of TM7's 105 tokens kept, ours has 122. ~~struck red~~ = TM7 only, green = ours only. Line by line in section 4 ↓

Lemma nonhalt: ~halts tm c0.
Proof.
  eapply multistep_nonhalt with (c':=S' [LD;D1]).
  1: esxapply start.
  eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').
  2: repeat{
    exists ec[LD;LD;LD;D1;D1].
    eapply RIncs_hx_ld; [apply Inc_d1, Inc_nil |].
    apply RIncs_hx_d0. apply RIncs_hx_d1.
    apply (RIncs_h1_rh_2 0), RIncs_h1_rh_0.
  }
  intros r [r' I1].
  pose proof I1 as I2.
  eapply RIncs_nxt with (tp':=hx) (k':=O) in I2.
  2: lia.
  exists r'; split.
  - apply BigStep, I1.
  - apply I2(domain _ _ I1).
Qed.

newscope—Close Scope sym L577 1 linenew; TM7 leaves the scope open

577Close Scope sym.

newcomment—(* rule-table comment *) L579 18 linescomment (ours only)

579(*
580```
5811RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---
582
583S(r) = 0^inf 11 D> <r> 0^inf          digits: L = 110, 0 = 000, 1 = 100
584start: 0^inf A> 0^inf  -->*  S(L1)    (S(1) at step 5, S(L1) at step 16)
585sweep: S(r) -->+ S(r')  if RIncs hx 0 r r'
586
587inc(r): +1 on the little-endian binary number of the 0/1 digits of r, L skipped,
588        a carry out of the last digit appends a 1
589eater (hx,k):  L -> L, k+1, inc the rest;   0 -> L, k+1;   1 -> L, drain with k
590drain (h1,k):  L -> L, eater with k, inc the rest (k >= 1);   1 -> L, k-1 (k >= 1)
591               0 -> 0, (k-1)/2 (k odd);   0 -> 1, (k-2)/2 (k even, k >= 2)
592right end (h1,k):  k = 0 -> 1;   k odd -> 0, (k-1)/2;   k even -> 1, (k-2)/2
593last digit, drain with k = 0:  1 -> L,  0 -> 1   (1 100 0^inf = 110 0^inf, 1 000 0^inf = 100 0^inf)
594
595domain: RIncs hx 0 r r' -> exists r'', RIncs hx 0 r' r''
596  (key: a second sweep reading the first one's output after j pending +1 passes,
597   under Inv; with j = 0 these are TM7's RIncs_nxt conditions)
598```
599*)

Rows follow our file's order; TM7-only rows sit next to the row that took over their job. The shaded group (solve_v2, solve_v1, RIncs_nxt → key) is the one role pairing: TM7's domain lemma and its automation, replaced by ours. "n lines" counts non-blank lines. Line links open the highlighted files (ours via the local server, TM7 in compare/TM7.html with SOMDCv6.v line numbers).

4Full side-by-side diff

What to notice: long folded grey runs are TM7 kept verbatim. The colored stretches are where ours departs: the two RIncs L clauses, two RIncs_spec bullets, the new lemmas, and nonhalt.

changed (~)TM7 only (−) ours only (+)equal after normalizing the TM string (≈)

TM7 · SOMDCv6.v lines 1–17 + 1627–1870 (highlighted copy)			#2 (ours) · 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v
		+	1	(* 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- never halts.
		+	2	Bell eats counter. Adapted from verify/SOMDCv6.v, Module TM7
		+	3	(1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---), which differs only in A1 (0RC there, 0RF here).
		+	4	Here every L digit that a sweep enters fires one extra h pass, a +1 on the digits to its right.
		+	5	Informal proof: the accompanying write-up (proof.md).
		+	6	Formalized with Claude Code (AI-assisted).
		+	7	Checked: compiles against unmodified busycoq (commit 0940bb9) with Coq 8.20.1;
		+	8	Print Assumptions nonhalt: Closed under the global context. *)
		+	9
1	From BusyCoq Require Import Individual62 Longitudinal DivModCases.		10	From BusyCoq Require Import Individual62 Longitudinal DivModCases.
2	Require Import ZifyNat Lia.		11	Require Import ZifyNat Lia.
3	Require Import ZArith.		12	Require Import ZArith.

4	Require Import String.		13	Require Import String.
5	Require Import List.		14	Require Import List.
6			15
7			16
8	Ltac esc :=		17	Ltac esc :=
9	(apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) \|\|		18	(apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) \|\|
10	(apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) \|\|		19	(apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) \|\|
11	(eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity \| st; reflexivity]).		20	(eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity \| st; reflexivity]).
12			21
13	Ltac ec := econstructor.		22	Ltac ec := econstructor.
14			23
15	Ltac am a a' k b b' :=		24	Ltac am a a' k b b' :=
16	applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc.		25	applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc.
17			26
1627	Definition tm := Eval compute in (TM_from_str "1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").	≈	27	Definition tm := Eval compute in (TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").
1628	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).		28	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
1629	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).		29	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
1630			30
1631	Notation ld := [1;1;0].		31	Notation ld := [1;1;0].
1632	Notation d0 := [0;0;0].		32	Notation d0 := [0;0;0].
1633	Notation d1 := [1;0;0].		33	Notation d1 := [1;0;0].
		+	34	Notation w1ld := [1;1;1;0].
1634	Notation hR := (B,@nil Sym).		35	Notation hR := (B,@nil Sym).
1635	Notation hR' := (D,[1]).		36	Notation hR' := (D,[1]).
1636	Notation hL := (C,@nil Sym).		37	Notation hL := (C,@nil Sym).

1637	Notation h := [(hR,hL)].		38	Notation h := [(hR,hL)].
1638	Notation h' := [(hR',hL)].		39	Notation h' := [(hR',hL)].
1639			40
1640	Inductive RD := LD\|D0\|D1.		41	Inductive RD := LD\|D0\|D1.
1641	Inductive H := hx\|h1.		42	Inductive H := hx\|h1.
1642			43
1643	Fixpoint toRC ls :=		44	Fixpoint toRC ls :=
1644	match ls with		45	match ls with
1645	\| [] => 0inf		46	\| [] => 0inf
1646	\| LD::ls => ld*>toRC ls		47	\| LD::ls => ld*>toRC ls
1647	\| D0::ls => d0*>toRC ls		48	\| D0::ls => d0*>toRC ls
1648	\| D1::ls => d1*>toRC ls		49	\| D1::ls => d1*>toRC ls
1649	end.		50	end.
1650			51
1651	Definition toH' x :=		52	Definition toH' x :=
1652	match x with		53	match x with
1653	\| hx => []		54	\| hx => []
1654	\| h1 => [1]		55	\| h1 => [1]
1655	end.		56	end.
1656			57
1657	Definition toH x :=		58	Definition toH x :=
1658	match x with		59	match x with
1659	\| hx => h'		60	\| hx => h'
1660	\| h1 => []		61	\| h1 => []
1661	end.		62	end.
1662			63
		+	64	(* one h pass over the digits = +1 on the little-endian binary number of the 0/1 digits, L skipped *)
		+	65	Inductive Inc: list RD -> list RD -> Prop :=
		+	66	\| Inc_nil: Inc [] [D1]
		+	67	\| Inc_d0 r: Inc (D0::r) (D1::r)
		+	68	\| Inc_d1 r r': Inc r r' -> Inc (D1::r) (D0::r')
		+	69	\| Inc_ld r r': Inc r r' -> Inc (LD::r) (LD::r').
		+	70
1663	Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=		71	Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=
1664	\| RIncs_hx_ld k r r':	~	72	\| RIncs_hx_ld k r r1 r':
		+	73	Inc r r1 ->
1665	RIncs hx (1+k) r r' ->	~	74	RIncs hx (1+k) r1 r' ->
1666	RIncs hx k (LD::r) (LD::r')		75	RIncs hx k (LD::r) (LD::r')
1667			76
1668	\| RIncs_hx_d1 k r r':		77	\| RIncs_hx_d1 k r r':

1669	RIncs h1 k r r' ->		78	RIncs h1 k r r' ->
1670	RIncs hx k (D1::r) (LD::r')		79	RIncs hx k (D1::r) (LD::r')
1671			80
1672	\| RIncs_hx_d0 k r r':		81	\| RIncs_hx_d0 k r r':
1673	RIncs hx (1+k) r r' ->		82	RIncs hx (1+k) r r' ->
1674	RIncs hx k (D0::r) (LD::r')		83	RIncs hx k (D0::r) (LD::r')
1675			84
1676	\| RIncs_h1_ld k r r':	~	85	\| RIncs_h1_ld k r r1 r':
		+	86	Inc r r1 ->
1677	RIncs hx (1+k) r r' ->	~	87	RIncs hx (1+k) r1 r' ->
1678	RIncs h1 (1+k) (LD::r) (LD::r')		88	RIncs h1 (1+k) (LD::r) (LD::r')
1679			89
1680	\| RIncs_h1_d1 k r r':		90	\| RIncs_h1_d1 k r r':

1681	RIncs h1 k r r' ->		91	RIncs h1 k r r' ->
1682	RIncs h1 (1+k) (D1::r) (LD::r')		92	RIncs h1 (1+k) (D1::r) (LD::r')
1683			93
1684	\| RIncs_h1_d0_0 k r r':		94	\| RIncs_h1_d0_0 k r r':
1685	RIncs h1 k r r' ->		95	RIncs h1 k r r' ->
1686	RIncs h1 (1+k*2) (D0::r) (D0::r')		96	RIncs h1 (1+k*2) (D0::r) (D0::r')
1687			97
1688	\| RIncs_h1_d0_1 k r r':		98	\| RIncs_h1_d0_1 k r r':
1689	RIncs h1 k r r' ->		99	RIncs h1 k r r' ->
1690	RIncs h1 (2+k*2) (D0::r) (D1::r')		100	RIncs h1 (2+k*2) (D0::r) (D1::r')
1691			101
1692	\| RIncs_h1_rh_0:		102	\| RIncs_h1_rh_0:
1693	RIncs h1 0 [] [D1]		103	RIncs h1 0 [] [D1]
1694			104
1695	\| RIncs_h1_rh_1 k r':		105	\| RIncs_h1_rh_1 k r':
1696	RIncs h1 k [] r' ->		106	RIncs h1 k [] r' ->
1697	RIncs h1 (1+k*2) [] (D0::r')		107	RIncs h1 (1+k*2) [] (D0::r')
		+	108
1698	\| RIncs_h1_rh_2 k r':		109	\| RIncs_h1_rh_2 k r':
1699	RIncs h1 k [] r' ->		110	RIncs h1 k [] r' ->
1700	RIncs h1 (2+k*2) [] (D1::r')		111	RIncs h1 (2+k*2) [] (D1::r')
		+	112
		+	113	\| RIncs_h1_z1:
		+	114	RIncs h1 0 [D1] [LD]
		+	115
		+	116	\| RIncs_h1_z0:
		+	117	RIncs h1 0 [D0] [D1]
1701	.		118	.
1702			119
1703	Ltac cat3 :=		120	Ltac cat3 :=

1704	eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]); [\|eauto 1].		121	eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]); [\|eauto 1].
1705			122
1706	Ltac tr1 :=		123	Ltac tr1 :=
1707	rewrite lpow_add,app_assoc;		124	rewrite lpow_add,app_assoc;
1708	eapply segRLs_trans; [esx \| ].		125	eapply segRLs_trans; [esx \| ].
1709			126
1710	Ltac wal :=		127	Ltac wal :=
1711	eapply segRLs_wall''; esx.		128	eapply segRLs_wall''; esx.
1712			129
1713	Ltac tr2 :=		130	Ltac tr2 :=
1714	eapply sideRLs_trans; [esx \| ].		131	eapply sideRLs_trans; [esx \| ].
1715			132
		+	133	Lemma z1_eq: [1] > d1 > 0inf = ld *> 0inf.
		+	134	Proof.
		+	135	cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold.
		+	136	Qed.
		+	137
		+	138	Lemma z0_eq: [1] > d0 > 0inf = d1 *> 0inf.
		+	139	Proof.
		+	140	cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold.
		+	141	Qed.
		+	142
1716	Open Scope nat.		143	Open Scope nat.
		+	144
		+	145	Lemma Inc_spec r r':
		+	146	Inc r r' ->
		+	147	sideRLs tm h (toRC r) (toRC r').
		+	148	Proof.
		+	149	intro H.
		+	150	induction H; cbn[toRC].
		+	151	- esc.
		+	152	- change h with (h++[]).
		+	153	eapply segRLs_sideRLs_concat; [esx \| constructor].
		+	154	- eapply (@segRLs_sideRLs_concat tm h h); [esx \| apply IHInc].
		+	155	- eapply (@segRLs_sideRLs_concat tm h h); [esx \| apply IHInc].
		+	156	Qed.
		+	157
		+	158	Lemma seg_hx_ld k:
		+	159	segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld.
		+	160	Proof.
		+	161	rewrite lpow_add.
		+	162	change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
		+	163	eapply segRLs_trans; [esx \| wal].
		+	164	Qed.
		+	165
		+	166	Lemma seg_h1_ld k:
		+	167	segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) w1ld ld.
		+	168	Proof.
		+	169	rewrite lpow_add.
		+	170	change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k).
		+	171	eapply segRLs_trans; [esx \| wal].
		+	172	Qed.
1717			173
1718	Lemma RIncs_spec tp k r r':		174	Lemma RIncs_spec tp k r r':
1719	RIncs tp k r r' ->		175	RIncs tp k r r' ->
1720	sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').		176	sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').
1721	Proof.		177	Proof.
1722	intro H.		178	intro H.
1723	induction H; intros; cbn[toH toH' toRC] in *.		179	induction H; intros; cbn[toH toH' toRC] in *.
1724	- cat3; tr1; wal.	−
		+	180	- eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]).
		+	181	1: apply seg_hx_ld.
		+	182	eapply sideRLs_trans.
		+	183	1: apply Inc_spec; eassumption.
		+	184	apply IHRIncs.
1725	- tr2.		185	- tr2.
1726	cat3; wal.		186	cat3; wal.
1727	- cat3; tr1; wal.		187	- cat3; tr1; wal.
1728	- rewrite lpow_add,app_assoc.	−
		+	188	- change ([] ++ h^^(1+k)) with (h^^1 ++ h^^k).
1729	eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]); [\|eauto 1].	~	189	eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]).
1730	tr1; wal.	−
		+	190	1: apply seg_h1_ld.
		+	191	eapply sideRLs_trans.
		+	192	1: apply Inc_spec; eassumption.
		+	193	apply IHRIncs.
1731	- rewrite lpow_add,app_assoc.		194	- rewrite lpow_add,app_assoc.
1732	tr2.		195	tr2.
1733	cat3; wal.		196	cat3; wal.

1734	- cat3.		197	- cat3.
1735	rewrite app_nil_l.		198	rewrite app_nil_l.
1736	am 2 1 k 1 1.		199	am 2 1 k 1 1.
1737	rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.		200	rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.
1738	tr2; eauto 1.		201	tr2; eauto 1.
1739	- cat3.		202	- cat3.
1740	rewrite Nat.add_comm.		203	rewrite Nat.add_comm.
1741	am 2 1 k 2 1.		204	am 2 1 k 2 1.
1742	rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.		205	rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.
1743	tr2; eauto 1.		206	tr2; eauto 1.
1744	- esc.		207	- esc.
1745	- rewrite lpow_add,app_assoc.		208	- rewrite lpow_add,app_assoc.
1746	tr2.		209	tr2.
1747	cat3.		210	cat3.
1748	rewrite app_nil_l.		211	rewrite app_nil_l.
1749	am 2 1 k 0 0.		212	am 2 1 k 0 0.
1750	- change (2+k2) with (1+(1+k2)).		213	- change (2+k2) with (1+(1+k2)).
1751	rewrite lpow_add,app_assoc.		214	rewrite lpow_add,app_assoc.
1752	tr2.		215	tr2.
1753	cat3.		216	cat3.
1754	rewrite app_nil_l.		217	rewrite app_nil_l.
1755	am 2 1 k 1 0.		218	am 2 1 k 1 0.
		+	219	- cbn[lpow app]. rewrite z1_eq. constructor.
		+	220	- cbn[lpow app]. rewrite z0_eq. constructor.
1756	Qed.		221	Qed.
		+	222
		+	223	(* ---------- combinatorics of the sweep relation (no machine) ---------- *)
		+	224
		+	225	Lemma Inc_total r: exists r', Inc r r'.
		+	226	Proof.
		+	227	induction r as [\|d r [r' I]].
		+	228	- eexists; apply Inc_nil.
		+	229	- destruct d; eexists.
		+	230	+ apply Inc_ld, I.
		+	231	+ apply Inc_d0.
		+	232	+ apply Inc_d1, I.
		+	233	Qed.
		+	234
		+	235	Lemma Inc_fun r r1 r2: Inc r r1 -> Inc r r2 -> r1 = r2.
		+	236	Proof.
		+	237	intro I. gen r2.
		+	238	induction I; intros r2 I2; inversion I2; subst; try reflexivity; f_equal; auto.
		+	239	Qed.
		+	240
		+	241	Lemma RIncs_eqk tp k k' r r': RIncs tp k r r' -> k = k' -> RIncs tp k' r r'.
		+	242	Proof. intros; subst; auto. Qed.
		+	243
		+	244	Ltac inc_nil :=
		+	245	repeat match goal with
		+	246	\| J: Inc [] _ \|- _ => inversion J; subst; clear J
		+	247	end.
		+	248
		+	249	(* proof.md Lemma A: one more pass after the k passes is +1 on the result *)
		+	250	Lemma RIncs_Inc tp k r r' r'':
		+	251	RIncs tp k r r' -> Inc r' r'' -> RIncs tp (1+k) r r''.
		+	252	Proof.
		+	253	intro I. gen r''.
		+	254	induction I; intros r'' J; inversion J; subst; inc_nil.
		+	255	- eapply RIncs_hx_ld; eauto.
		+	256	- apply RIncs_hx_d1; auto.
		+	257	- apply RIncs_hx_d0; auto.
		+	258	- eapply (RIncs_h1_ld (1+k)); eauto.
		+	259	- apply (RIncs_h1_d1 (1+k)); auto.
		+	260	- eapply RIncs_eqk; [apply RIncs_h1_d0_1; eauto \| lia].
		+	261	- eapply RIncs_eqk; [apply (RIncs_h1_d0_0 (1+k)); eauto \| lia].
		+	262	- apply (RIncs_h1_rh_1 0), RIncs_h1_rh_0.
		+	263	- eapply RIncs_eqk; [apply RIncs_h1_rh_2; eauto \| lia].
		+	264	- eapply RIncs_eqk; [apply (RIncs_h1_rh_1 (1+k)); eauto \| lia].
		+	265	- apply (RIncs_h1_d1 0), RIncs_h1_rh_0.
		+	266	- apply (RIncs_h1_d0_0 0), RIncs_h1_rh_0.
		+	267	Qed.
1757			268
1758	Lemma RIncs_nxt_1 k:		269	Lemma RIncs_nxt_1 k:
1759	exists r, RIncs h1 k [] r.		270	exists r, RIncs h1 k [] r.

1760	Proof.		271	Proof.
1761	induction k using lt_wf_ind.		272	induction k using lt_wf_ind.
1762	destruct k.		273	destruct k.
1763	+ ec. ec.		274	+ ec. ec.
1764	+ destruct (mod2 k); subst.		275	+ destruct (mod2 k); subst.
1765	* epose proof (H0 _ _) as [r I].		276	* epose proof (H0 _ _) as [r I].
1766	ec. ec. apply I.		277	ec. ec. apply I.
1767	* epose proof (H0 _ _) as [r I].		278	* epose proof (H0 _ _) as [r I].
1768	ec. ec. apply I.		279	ec. ec. apply I.
1769	Unshelve. all: lia.		280	Unshelve. all: lia.
1770	Qed.		281	Qed.
1771			282
1772		−
1773	Ltac solve_v2 :=	−
1774	(epose proof (RIncs_nxt_1 _) as [r I]; repeat ec; try apply I).	−
1775		−
1776	Ltac solve_v1 H tp'0 k'0 H' :=	−
1777	eapply H with (tp':=tp'0) (k':=k'0) in H';	−
1778	try lia;	−
1779	try (	−
1780	destruct H' as [r'' I1];	−
1781	repeat ec; try apply I1).	−
1782		−
1783	Lemma RIncs_nxt tp k r r' tp' k':	−
1784	RIncs tp k r r' ->	−
1785	match tp,tp' with	−
1786	\| hx,hx => k<=k'	−
1787	\| h1,h1 => k*2+1<=k'	−
1788	\| h1,hx => k+1<=k'	−
1789	\| _,_ => False	−
1790	end ->	−
1791	exists r'',	−
1792	RIncs tp' k' r' r''.	−
		+	283	Lemma End_1 m w:
		+	284	RIncs h1 m [] w -> forall q, m <= q -> exists w', RIncs h1 q w w'.
		+	285	Proof.
		+	286	intro I. remember h1 as t. remember (@nil RD) as e.
		+	287	induction I; intros q Hq; try discriminate; subst.
		+	288	- destruct q as [\|q].
		+	289	+ eexists; apply RIncs_h1_z1.
		+	290	+ destruct (RIncs_nxt_1 q) as [w I].
		+	291	eexists; apply (RIncs_h1_d1 q), I.
		+	292	- specialize (IHI eq_refl eq_refl).
		+	293	destruct (mod2 q) as [b Hb\|b Hb]; subst q.
		+	294	+ destruct b as [\|b]; [lia\|].
		+	295	destruct (IHI b) as [w I2]; [lia\|].
		+	296	eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 \| lia].
		+	297	+ destruct (IHI b) as [w I2]; [lia\|].
		+	298	eexists; apply RIncs_h1_d0_0, I2.
		+	299	- specialize (IHI eq_refl eq_refl).
		+	300	destruct q as [\|q]; [lia\|].
		+	301	destruct (IHI q) as [w I2]; [lia\|].
		+	302	eexists; apply (RIncs_h1_d1 q), I2.
		+	303	Qed.
		+	304
		+	305	Lemma End_x m w:
		+	306	RIncs h1 m [] w -> forall q, m <= 2*q+2 -> exists w', RIncs hx q w w'.
1793	Proof.		307	Proof.
1794	gen tp k r' tp' k'.	−
1795	induction r; intros.	−
1796	{	−
1797	gen tp r' tp' k'.	−
1798	induction k using lt_wf_ind.	−
1799	intros.	−
1800	inverts H1; destruct tp'.	−
1801	all: try lia.	−
1802	- solve_v2.	−
1803	- destruct (sub k' 1); [subst\|lia].	−
1804	solve_v2.	−
1805	- solve_v1 H0 hx (1+k') H3.	−
1806	- destruct (sub k' 1); [subst\|lia].	−
1807	destruct (mod2 c); subst.	−
1808	+ solve_v1 H0 h1 (a) H3.	−
1809	+ solve_v1 H0 h1 (a) H3.	−
1810	- solve_v1 H0 h1 (k') H3.	−
1811	- destruct (sub k' 1); [subst\|lia].	−
1812	solve_v1 H0 h1 (c) H3.	−
1813	}	−
1814	{	−
1815	inverts H0; destruct tp'.	−
1816	all: try lia.	−
1817	- solve_v1 IHr hx (1+k') H7.	−
1818	- solve_v1 IHr hx (1+k') H7.	−
1819	- solve_v1 IHr hx (1+k') H7.	−
1820	- solve_v1 IHr hx (1+k') H7.	−
1821	- destruct (sub k' 1); [subst\|lia].	−
1822	solve_v1 IHr hx (1+c) H7.	−
1823	- solve_v1 IHr hx (1+k') H7.	−
1824	- destruct (sub k' 1); [subst\|lia].	−
1825	solve_v1 IHr hx (1+c) H7.	−
1826	- solve_v1 IHr hx (1+k') H7.	−
1827	- destruct (sub k' 1); [subst\|lia].	−
1828	destruct (mod2 c); subst.	−
1829	+ solve_v1 IHr h1 (a) H7.	−
1830	+ solve_v1 IHr h1 (a) H7.	−
1831	- solve_v1 IHr h1 k' H7.	−
1832	- destruct (sub k' 1); [subst\|lia].	−
1833	solve_v1 IHr h1 (c) H7.	−
1834	}	−
		+	308	intro I. remember h1 as t. remember (@nil RD) as e.
		+	309	induction I; intros q Hq; try discriminate; subst.
		+	310	- destruct (RIncs_nxt_1 q) as [w I].
		+	311	eexists; apply RIncs_hx_d1, I.
		+	312	- specialize (IHI eq_refl eq_refl).
		+	313	destruct (IHI (1+q)) as [w I2]; [lia\|].
		+	314	eexists; apply RIncs_hx_d0, I2.
		+	315	- destruct (End_1 _ _ I q) as [w I2]; [lia\|].
		+	316	eexists; apply RIncs_hx_d1, I2.
		+	317	Qed.
		+	318
		+	319	(* inversion helpers *)
		+	320	Lemma inv_hx_ld k r rK: RIncs hx k (LD::r) rK ->
		+	321	exists r1 rK', Inc r r1 /\ RIncs hx (1+k) r1 rK' /\ rK = LD::rK'.
		+	322	Proof. intro E; inversion E; subst; do 2 eexists; repeat split; eauto. Qed.
		+	323
		+	324	Lemma inv_hx_d1 k r rK: RIncs hx k (D1::r) rK ->
		+	325	exists rK', RIncs h1 k r rK' /\ rK = LD::rK'.
		+	326	Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.
		+	327
		+	328	Lemma inv_hx_d0 k r rK: RIncs hx k (D0::r) rK ->
		+	329	exists rK', RIncs hx (1+k) r rK' /\ rK = LD::rK'.
		+	330	Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.
		+	331
		+	332	Lemma inv_h1_ld k r rK: RIncs h1 (1+k) (LD::r) rK ->
		+	333	exists r1 rK', Inc r r1 /\ RIncs hx (1+k) r1 rK' /\ rK = LD::rK'.
		+	334	Proof. intro E; inversion E; subst; do 2 eexists; repeat split; eauto. Qed.
		+	335
		+	336	Lemma inv_h1_d1 k r rK: RIncs h1 (1+k) (D1::r) rK ->
		+	337	exists rK', RIncs h1 k r rK' /\ rK = LD::rK'.
		+	338	Proof. intro E; inversion E; subst; eexists; repeat split; eauto. Qed.
		+	339
		+	340	Lemma inv_h1_d0 K r rK: RIncs h1 K (D0::r) rK ->
		+	341	(exists A rK', K = 1+A*2 /\ RIncs h1 A r rK' /\ rK = D0::rK') \/
		+	342	(exists A rK', K = 2+A*2 /\ RIncs h1 A r rK' /\ rK = D1::rK') \/
		+	343	(K = 0 /\ r = [] /\ rK = [D1]).
		+	344	Proof.
		+	345	intro E; inversion E; subst.
		+	346	- left; do 2 eexists; repeat split; eauto.
		+	347	- right; left; do 2 eexists; repeat split; eauto.
		+	348	- right; right; auto.
1835	Qed.		349	Qed.
		+	350
		+	351	Lemma inv_z1 K rK: RIncs h1 K [D1] rK ->
		+	352	(K = 0 /\ rK = [LD]) \/
		+	353	(exists K0 rK', K = 1+K0 /\ RIncs h1 K0 [] rK' /\ rK = LD::rK').
		+	354	Proof.
		+	355	intro E; inversion E; subst.
		+	356	- right; do 2 eexists; repeat split; eauto.
		+	357	- left; auto.
		+	358	Qed.
		+	359
		+	360	(* proof.md section 3.3: the second sweep reads the first's output after j pending +1s *)
		+	361	Definition Inv tp k j tq q :=
		+	362	match tp, tq with
		+	363	\| hx, hx => k <= q /\ j <= q
		+	364	\| h1, hx => k+1 <= q /\ j <= q
		+	365	\| h1, h1 => (j = 0 /\ 2*k+1 <= q) \/ (1 <= j /\ k+j <= q /\ 1 <= q)
		+	366	\| hx, h1 => False
		+	367	end.
		+	368
		+	369	Lemma key tp k r r1:
		+	370	RIncs tp k r r1 ->
		+	371	forall j rK tq q,
		+	372	RIncs tp (k+j) r rK ->
		+	373	Inv tp k j tq q ->
		+	374	exists r2, RIncs tq q rK r2.
		+	375	Proof.
		+	376	intro D.
		+	377	induction D as [k r r1 r' Hi D IH \| k r r' D IH \| k r r' D IH
		+	378	\| k r r1 r' Hi D IH \| k r r' D IH \| a r r' D IH \| a r r' D IH
		+	379	\| \| a r' D IH \| a r' D IH \| \| ];
		+	380	intros j rK tq q E HI.
		+	381	- (* hx_ld *)
		+	382	destruct (inv_hx_ld _ _ _ E) as [r1' [rK' [Hi' [E' ->]]]].
		+	383	rewrite (Inc_fun _ _ _ Hi' Hi) in E'.
		+	384	destruct tq; cbn in HI; [\|contradiction].
		+	385	destruct (Inc_total rK') as [rK'' J].
		+	386	destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
		+	387	+ eapply RIncs_eqk; [eapply RIncs_Inc; eassumption \| lia].
		+	388	+ cbn; lia.
		+	389	+ eexists; eapply RIncs_hx_ld; eassumption.
		+	390	- (* hx_d1 *)
		+	391	destruct (inv_hx_d1 _ _ _ E) as [rK' [E' ->]].
		+	392	destruct tq; cbn in HI; [\|contradiction].
		+	393	destruct (Inc_total rK') as [rK'' J].
		+	394	destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
		+	395	+ eapply RIncs_eqk; [eapply RIncs_Inc; eassumption \| lia].
		+	396	+ cbn; lia.
		+	397	+ eexists; eapply RIncs_hx_ld; eassumption.
		+	398	- (* hx_d0 *)
		+	399	destruct (inv_hx_d0 _ _ _ E) as [rK' [E' ->]].
		+	400	destruct tq; cbn in HI; [\|contradiction].
		+	401	destruct (Inc_total rK') as [rK'' J].
		+	402	destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
		+	403	+ eapply RIncs_eqk; [eapply RIncs_Inc; eassumption \| lia].
		+	404	+ cbn; lia.
		+	405	+ eexists; eapply RIncs_hx_ld; eassumption.
		+	406	- (* h1_ld *)
		+	407	destruct (inv_h1_ld (k+j) _ _ E) as [r1' [rK' [Hi' [E' ->]]]].
		+	408	rewrite (Inc_fun _ _ _ Hi' Hi) in E'.
		+	409	destruct (Inc_total rK') as [rK'' J].
		+	410	destruct tq; cbn in HI.
		+	411	+ destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
		+	412	* eapply RIncs_eqk; [eapply RIncs_Inc; eassumption \| lia].
		+	413	* cbn; lia.
		+	414	* eexists; eapply RIncs_hx_ld; eassumption.
		+	415	+ destruct q as [\|q0]; [lia\|].
		+	416	destruct (IH (1+j) rK'' hx (S q0)) as [r2 I2].
		+	417	* eapply RIncs_eqk; [eapply RIncs_Inc; eassumption \| lia].
		+	418	* cbn; lia.
		+	419	* eexists; eapply (RIncs_h1_ld q0); eassumption.
		+	420	- (* h1_d1 *)
		+	421	destruct (inv_h1_d1 (k+j) _ _ E) as [rK' [E' ->]].
		+	422	destruct (Inc_total rK') as [rK'' J].
		+	423	destruct tq; cbn in HI.
		+	424	+ destruct (IH (1+j) rK'' hx (1+q)) as [r2 I2].
		+	425	* eapply RIncs_eqk; [eapply RIncs_Inc; eassumption \| lia].
		+	426	* cbn; lia.
		+	427	* eexists; eapply RIncs_hx_ld; eassumption.
		+	428	+ destruct q as [\|q0]; [lia\|].
		+	429	destruct (IH (1+j) rK'' hx (S q0)) as [r2 I2].
		+	430	* eapply RIncs_eqk; [eapply RIncs_Inc; eassumption \| lia].
		+	431	* cbn; lia.
		+	432	* eexists; eapply (RIncs_h1_ld q0); eassumption.
		+	433	- (* h1_d0_0 *)
		+	434	destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]\|[[A [rK' [HK [E' ->]]]]\|[HK _]]]; [\| \|lia].
		+	435	+ (* rK = D0::rK' *)
		+	436	assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption \| lia]).
		+	437	destruct tq; cbn in HI.
		+	438	* destruct (IH (A-a) rK' hx (1+q) E2) as [r2 I2]; [cbn; lia\|].
		+	439	eexists; apply RIncs_hx_d0, I2.
		+	440	* destruct (mod2 q) as [b Hb\|b Hb]; subst q.
		+	441	-- destruct b as [\|b]; [lia\|].
		+	442	destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia\|].
		+	443	eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 \| lia].
		+	444	-- destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia\|].
		+	445	eexists; apply RIncs_h1_d0_0, I2.
		+	446	+ (* rK = D1::rK' *)
		+	447	assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption \| lia]).
		+	448	destruct tq; cbn in HI.
		+	449	* destruct (IH (A-a) rK' h1 q E2) as [r2 I2]; [cbn; lia\|].
		+	450	eexists; apply RIncs_hx_d1, I2.
		+	451	* destruct q as [\|q0]; [lia\|].
		+	452	destruct (IH (A-a) rK' h1 q0 E2) as [r2 I2]; [cbn; lia\|].
		+	453	eexists; apply (RIncs_h1_d1 q0), I2.
		+	454	- (* h1_d0_1 *)
		+	455	destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]\|[[A [rK' [HK [E' ->]]]]\|[HK _]]]; [\| \|lia].
		+	456	+ (* rK = D0::rK' *)
		+	457	assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption \| lia]).
		+	458	destruct tq; cbn in HI.
		+	459	* destruct (IH (A-a) rK' hx (1+q) E2) as [r2 I2]; [cbn; lia\|].
		+	460	eexists; apply RIncs_hx_d0, I2.
		+	461	* destruct (mod2 q) as [b Hb\|b Hb]; subst q.
		+	462	-- destruct b as [\|b]; [lia\|].
		+	463	destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia\|].
		+	464	eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I2 \| lia].
		+	465	-- destruct (IH (A-a) rK' h1 b E2) as [r2 I2]; [cbn; lia\|].
		+	466	eexists; apply RIncs_h1_d0_0, I2.
		+	467	+ (* rK = D1::rK' *)
		+	468	assert (E2: RIncs h1 (a+(A-a)) r rK') by (eapply RIncs_eqk; [eassumption \| lia]).
		+	469	destruct tq; cbn in HI.
		+	470	* destruct (IH (A-a) rK' h1 q E2) as [r2 I2]; [cbn; lia\|].
		+	471	eexists; apply RIncs_hx_d1, I2.
		+	472	* destruct q as [\|q0]; [lia\|].
		+	473	destruct (IH (A-a) rK' h1 q0 E2) as [r2 I2]; [cbn; lia\|].
		+	474	eexists; apply (RIncs_h1_d1 q0), I2.
		+	475	- (* rh_0 *)
		+	476	destruct tq; cbn in HI.
		+	477	+ eapply End_x; [eassumption \| lia].
		+	478	+ eapply End_1; [eassumption \| lia].
		+	479	- (* rh_1 *)
		+	480	destruct tq; cbn in HI.
		+	481	+ eapply End_x; [eassumption \| lia].
		+	482	+ eapply End_1; [eassumption \| lia].
		+	483	- (* rh_2 *)
		+	484	destruct tq; cbn in HI.
		+	485	+ eapply End_x; [eassumption \| lia].
		+	486	+ eapply End_1; [eassumption \| lia].
		+	487	- (* z1 *)
		+	488	destruct (inv_z1 _ _ E) as [[HK ->]\|[K0 [rK' [HK [E' ->]]]]].
		+	489	+ destruct tq; cbn in HI.
		+	490	* destruct (RIncs_nxt_1 (1+q)) as [w I].
		+	491	eexists; eapply RIncs_hx_ld; [apply Inc_nil \| apply RIncs_hx_d1, I].
		+	492	* destruct q as [\|q0]; [lia\|].
		+	493	destruct (RIncs_nxt_1 (1+q0)) as [w I].
		+	494	eexists; eapply (RIncs_h1_ld q0); [apply Inc_nil \| apply RIncs_hx_d1, I].
		+	495	+ destruct (Inc_total rK') as [rK'' J].
		+	496	pose proof (RIncs_Inc _ _ _ _ _ E' J) as E''.
		+	497	destruct tq; cbn in HI.
		+	498	* destruct (End_x _ _ E'' (1+q)) as [w I]; [lia\|].
		+	499	eexists; eapply RIncs_hx_ld; eassumption.
		+	500	* destruct q as [\|q0]; [lia\|].
		+	501	destruct (End_x _ _ E'' (1+q0)) as [w I]; [lia\|].
		+	502	eexists; eapply (RIncs_h1_ld q0); eassumption.
		+	503	- (* z0 *)
		+	504	destruct (inv_h1_d0 _ _ _ E) as [[A [rK' [HK [E' ->]]]]\|[[A [rK' [HK [E' ->]]]]\|[HK [_ ->]]]].
		+	505	+ destruct tq; cbn in HI.
		+	506	* destruct (End_x _ _ E' (1+q)) as [w I]; [lia\|].
		+	507	eexists; apply RIncs_hx_d0, I.
		+	508	* destruct (mod2 q) as [b Hb\|b Hb]; subst q.
		+	509	-- destruct b as [\|b]; [lia\|].
		+	510	destruct (End_1 _ _ E' b) as [w I]; [lia\|].
		+	511	eexists; eapply RIncs_eqk; [apply RIncs_h1_d0_1, I \| lia].
		+	512	-- destruct (End_1 _ _ E' b) as [w I]; [lia\|].
		+	513	eexists; apply RIncs_h1_d0_0, I.
		+	514	+ destruct tq; cbn in HI.
		+	515	* destruct (End_1 _ _ E' q) as [w I]; [lia\|].
		+	516	eexists; apply RIncs_hx_d1, I.
		+	517	* destruct q as [\|q0]; [lia\|].
		+	518	destruct (End_1 _ _ E' q0) as [w I]; [lia\|].
		+	519	eexists; apply (RIncs_h1_d1 q0), I.
		+	520	+ destruct tq; cbn in HI.
		+	521	* destruct (RIncs_nxt_1 q) as [w I].
		+	522	eexists; apply RIncs_hx_d1, I.
		+	523	* destruct q as [\|q0]; [lia\|].
		+	524	destruct (RIncs_nxt_1 q0) as [w I].
		+	525	eexists; apply (RIncs_h1_d1 q0), I.
		+	526	Qed.
		+	527
		+	528	Lemma domain r r':
		+	529	RIncs hx 0 r r' -> exists r'', RIncs hx 0 r' r''.
		+	530	Proof.
		+	531	intro I.
		+	532	eapply (key _ _ _ _ I 0 r' hx 0).
		+	533	- apply I.
		+	534	- cbn; lia.
		+	535	Qed.
		+	536
1836			537
1837	Open Scope sym.		538	Open Scope sym.
1838			539

1839	Notation lh := (0inf<*<[1]).		540	Notation lh := (0inf<*<[1]).
1840			541
1841	Definition S' r :=		542	Definition S' r :=
1842	lh {{{ (hR',R) }}} toH' hx *> toRC r.		543	lh {{{ (hR',R) }}} toH' hx *> toRC r.
1843			544
1844	Lemma BigStep r r':		545	Lemma BigStep r r':
1845	RIncs hx 0 r r' ->		546	RIncs hx 0 r r' ->
1846	S' r -->+ S' r'.		547	S' r -->+ S' r'.
1847	Proof.		548	Proof.
1848	intros H.		549	intros H.
1849	apply RIncs_spec in H.		550	apply RIncs_spec in H.
1850	unfold S'.		551	unfold S'.
1851	eapply sideRLs_1 in H.		552	eapply sideRLs_1 in H.
1852	follow10 H.		553	follow10 H.
1853	es.		554	es.
1854	Qed.		555	Qed.
1855			556
		+	557	Lemma start: c0 -->* S' [LD;D1].
		+	558	Proof. esx. Qed.
		+	559
1856	Lemma nonhalt: ~halts tm c0.		560	Lemma nonhalt: ~halts tm c0.
1857	Proof.		561	Proof.
1858	eapply multistep_nonhalt with (c':=S' [D1]).	~	562	eapply multistep_nonhalt with (c':=S' [LD;D1]).
1859	1: esx.	−
		+	563	1: apply start.
1860	eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').		564	eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').
1861	2: repeat ec.	−
		+	565	2: {
		+	566	exists [LD;LD;LD;D1;D1].
		+	567	eapply RIncs_hx_ld; [apply Inc_d1, Inc_nil \|].
		+	568	apply RIncs_hx_d0. apply RIncs_hx_d1.
		+	569	apply (RIncs_h1_rh_2 0), RIncs_h1_rh_0.
		+	570	}
1862	intros r [r' I1].		571	intros r [r' I1].
1863	pose proof I1 as I2.	−
1864	eapply RIncs_nxt with (tp':=hx) (k':=O) in I2.	−
1865	2: lia.	−
1866	exists r'; split.		572	exists r'; split.
1867	- apply BigStep,I1.	~	573	- apply BigStep, I1.
1868	- apply I2.	−
		+	574	- apply (domain _ _ I1).
1869	Qed.		575	Qed.
1870			576
		+	577	Close Scope sym.
		+	578
		+	579	(*
		+	580	```
		+	581	1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---
		+	582
		+	583	S(r) = 0^inf 11 D> <r> 0^inf digits: L = 110, 0 = 000, 1 = 100
		+	584	start: 0^inf A> 0^inf -->* S(L1) (S(1) at step 5, S(L1) at step 16)
		+	585	sweep: S(r) -->+ S(r') if RIncs hx 0 r r'
		+	586
		+	587	inc(r): +1 on the little-endian binary number of the 0/1 digits of r, L skipped,
		+	588	a carry out of the last digit appends a 1
		+	589	eater (hx,k): L -> L, k+1, inc the rest; 0 -> L, k+1; 1 -> L, drain with k
		+	590	drain (h1,k): L -> L, eater with k, inc the rest (k >= 1); 1 -> L, k-1 (k >= 1)
		+	591	0 -> 0, (k-1)/2 (k odd); 0 -> 1, (k-2)/2 (k even, k >= 2)
		+	592	right end (h1,k): k = 0 -> 1; k odd -> 0, (k-1)/2; k even -> 1, (k-2)/2
		+	593	last digit, drain with k = 0: 1 -> L, 0 -> 1 (1 100 0^inf = 110 0^inf, 1 000 0^inf = 100 0^inf)
		+	594
		+	595	domain: RIncs hx 0 r r' -> exists r'', RIncs hx 0 r' r''
		+	596	(key: a second sweep reading the first one's output after j pending +1 passes,
		+	597	under Inv; with j = 0 these are TM7's RIncs_nxt conditions)
		+	598	```
		+	599	*)

8 identical runs longer than 9 lines are folded to 3 lines of context on each side. Inside changed lines the differing tokens are marked. Line numbers link to the highlighted files.

5Proof structure

What to notice: the machine-facing half (encoding, tactics, RIncs_spec, BigStep) is reused; the domain argument is what grew, because A1's extra +1 pass breaks TM7's domain lemma.

Block height = non-blank lines (1 px each, at least 18 px so the label fits; the number after each label is the count). The fill inside a block splits its lines by diff status: grey identical, amber changed, green ours only, red TM7 only, blue the tm line (equal once the TM string is normalized). Grey bands join blocks with the same job; the dashed band is the replaced domain lemma. Each TM7 block is drawn level with its match. Click a block to open its first line. The thin grey slivers at the left of “End_1, End_x” and “inv_* (7 inversion helpers)” (ours) and of “solve_v2, solve_v1, RIncs_nxt” (TM7) are the 2 coincidental Proof./Qed. matches noted in section 2, not reused proof text.

Why it grew: A1 at run time

One eating pass: ours runs a +1 pass at each L, TM7 turns straight back

From scripts/compare_tm7.py: same start S(L⁴1L1). Each time ours fires A1 (0RF) it runs one extra pass (blue boxes) that adds +1 to the digits on its right; TM7's A1 (0RC) turns straight back.

What changed, and why

New relation Inc for that +1 (on the 0/1 digits, little-endian binary, L skipped), and Inc_spec, which proves it is one h pass on the tape.
The two L clauses of RIncs (RIncs_hx_ld: the eater enters an L; RIncs_h1_ld: a drain pass enters an L) get an Inc premise and recurse on the incremented rest. Their RIncs_spec bullets now use seg_hx_ld / seg_h1_ld: the segment emits h ++ h' ++ h^^(1+k) instead of TM7's h' ++ h^^(1+k).
Two zero-pass end clauses, Z1 and Z0 (RIncs_h1_z1, RIncs_h1_z0). They add no machine behaviour (z1_eq, z0_eq are tape identities). proof.md §3.3: without them LLLL10LL1L1 is in the domain but its sweep LLLLL1LLLLLLL111 is not.
The domain lemma is redone. TM7's RIncs_nxt (induction on r, automation solve_v1/solve_v2) becomes key: a second sweep reads the first one's output with j pending +1 passes, under the condition Inv, by induction on the derivation. At j = 0, Inv is TM7's condition. Helpers: RIncs_Inc (one more pass = +1 on the result), End_1/End_x (the right end, which TM7 handled inside RIncs_nxt), seven inv_* inversions, Inc_total/Inc_fun.
Reused verbatim: the header tactics, the digit encoding and notations, toRC/toH, the segment tactics, RIncs_nxt_1, lh, S', BigStep. nonhalt keeps its shape (multistep_nonhalt then progress_nonhalt_cond, same invariant) but starts from S' [LD;D1] (lemma start) instead of S' [D1].

Clause by clause: `RIncs` and its `RIncs_spec` bullet

clause (ours, in order)	RIncs clause	RIncs_spec bullet
`RIncs_hx_ld`	adapted	adapted
`RIncs_hx_d1`	identical	identical
`RIncs_hx_d0`	identical	identical
`RIncs_h1_ld`	adapted	adapted
`RIncs_h1_d1`	identical	identical
`RIncs_h1_d0_0`	identical	identical
`RIncs_h1_d0_1`	identical	identical
`RIncs_h1_rh_0`	identical	identical
`RIncs_h1_rh_1`	identical	identical
`RIncs_h1_rh_2`	identical	identical
`RIncs_h1_z1`	new	new
`RIncs_h1_z0`	new	new

RIncs: 8 identical, 2 adapted, 2 new (TM7 has 10). RIncs_spec bullets: 8 identical, 2 adapted, 2 new. Bullet n proves clause n in both files.

6Submission comparison

What to notice: ours follows upstream's single-machine-file layout (top-level tm, trailing rule comment), but adds a header comment and a much longer, unfactored domain lemma.

	TM7 upstream	#2 (our submission)
Where it lives	One of 8 modules (TM1, TM2, TM3, TM4, TM5, TM6, TM7, TM8) in `SOMDCv6.v` (2121 lines), lines 1626–1871.	Its own file named by the machine string, 599 lines, everything top level (no `Module`).
Shared header	17 lines at the top of the file (imports, `esc`, `ec`, `am`), used by all 8 modules.	The same 17 lines copied verbatim at lines 10–26.
Comments	None: 0 comments in all 2121 lines of SOMDCv6.v.	7 top-level comments (34 lines) and 16 inline ones (mostly the case labels in `key`).
Header comment	none	Lines 1–8: machine, template and the A1 difference, mechanism in one line, informal-proof path, AI disclosure.
Rule table	none	Lines 579–599: machine string, `S(r)`, the sweep rules, in a ``` block inside `(* *)`.
Names	Shared skeleton names, counted over the 8 modules: `RIncs_spec` ×8, `RIncs_nxt` ×8, `nonhalt` ×8, `BigStep` ×4, `RIncs_nxt_1` ×2.	Keeps every TM7 name except `solve_v2`, `solve_v1`, `RIncs_nxt`. 25 new names: `w1ld`, `Inc`, `z1_eq`, `z0_eq`, `Inc_spec`, `seg_hx_ld`, `seg_h1_ld`, `Inc_total`, `Inc_fun`, `RIncs_eqk`, `inc_nil`, `RIncs_Inc`, `End_1`, `End_x`, `inv_*` (7), `Inv`, `key`, `domain`, `start`.
Domain lemma	`RIncs_nxt`, 53 lines; the cases are closed by two Ltacs (`solve_v1`, `solve_v2`).	`key`, 158 lines (26% of the file); every case written out.
Final theorem	`Lemma nonhalt: ~halts tm c0.` inside `Module TM7`.	The same statement at top level (L560), as `tools/check_kill.sh` requires.

Upstream also has single-machine files: 8 .v files under verify/ are named by their machine string (182–1029 lines). 7 of them are top level and 1 wraps its proof in a Module. They have 0–2 comments each, 6 end with a comment, and 3 put rules in a ``` block inside it (e.g. 1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC.v). Our layout (top-level tm, trailing rule comment) follows that convention. The header comment has no upstream counterpart.

Our header comment

1(* 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- never halts.
2   Bell eats counter. Adapted from verify/SOMDCv6.v, Module TM7
3   (1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---), which differs only in A1 (0RC there, 0RF here).
4   Here every L digit that a sweep enters fires one extra h pass, a +1 on the digits to its right.
5   Informal proof: the accompanying write-up (proof.md).
6   Formalized with Claude Code (AI-assisted).
7   Checked: compiles against unmodified busycoq (commit 0940bb9) with Coq 8.20.1;
8   Print Assumptions nonhalt: Closed under the global context. *)

What a maintainer might raise

No repo-local paths in the header comment. It names the template as verify/SOMDCv6.v (busycoq's own layout), the informal proof as the accompanying write-up (proof.md), and the check by busycoq commit, Coq version and the Print Assumptions result. Until the comment-only edit of 2026-10-10 it named vendor/busycoq/verify/SOMDCv6.v, machines/…/proof.md and tools/check_kill.sh.
Repeated case text in key. Byte-identical bullets: h1_d0_0 = h1_d0_1 (21 lines each, only the case-label comment differs); rh_0 = rh_1 = rh_2 (4 lines each, only the case-label comment differs). Also hx_ld, hx_d1, hx_d0 end in the same 6 lines, and h1_ld, h1_d1 end in the same 11 lines (they differ only in the label and their first one or two lines, the inversion step). TM7 folds its repeated cases into solve_v1/solve_v2; a local Ltac could do the same here.
Length. 599 lines against TM7's 246-line module (261 with the shared header). key alone is 158 lines. The 376 added non-blank lines are marked in section 4; section 3 lists the 33 new items they make up.
AI disclosure inside the file (L8). Upstream proofs carry no authorship or AI line: of the 548 .v files under verify/ (436 at the top, the rest in subfolders), a search for author / written by / Claude / GPT / LLM / AI-assisted matches only LibTactics.v (a third-party library's license note). The same disclosure is in submission/README.md and discord.md, so it could live only there if a maintainer prefers.
Generic names. key, Inv, domain, start are fine in a single file but say less than the template's style. proof.md calls key RIncs_nxt'.
Cosmetic drift from TM7, which makes the diff a little noisier: 1 whitespace-only change (apply BigStep,I1 → apply BigStep, I1), 1 blank line added between two lines kept from TM7 (RIncs L108), and a final Close Scope sym. that TM7 does not have.

Generated by compare/build.py from machines/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v (sha256 e434537eca67…) and vendor/busycoq/verify/SOMDCv6.v (sha256 cff0e865a73c…). Numbers: compare/stats.json.