Left numbers: rocq-scratch/TM7_toplevel.v (SOMDCv6.v lines 1–17 plus 1627–1870, i.e. TM7 without its Module lines; 261 lines; it passes check_kill with TM7's string). Right numbers: our file (599 lines, links to the annotated view). 9 hunks, +415 / −77 lines, as printed by the command below (GNU diffutils 3.12).
cd ~/projects/bb6-hunt && T=1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---
diff -u "machines/$T/rocq-scratch/TM7_toplevel.v" "machines/$T/$T.v" | less
added in oursTM7 only
@@ -1,3 +1,12 @@1+(* 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- never halts.2+ Bell eats counter. Adapted from verify/SOMDCv6.v, Module TM73+ (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+110 From BusyCoq Require Import Individual62 Longitudinal DivModCases.211 Require Import ZifyNat Lia.312 Require Import ZArith.@@ -15,13 +24,14 @@1524 Ltac am a a' k b b' :=1625 applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc.172618-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---").1928 Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).2029 Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).21302231 Notation ld := [1;1;0].2332 Notation d0 := [0;0;0].2433 Notation d1 := [1;0;0].34+Notation w1ld := [1;1;1;0].2535 Notation hR := (B,@nil Sym).2636 Notation hR' := (D,[1]).2737 Notation hL := (C,@nil Sym).@@ -51,9 +61,17 @@5161 | h1 => []5262 end.536364+(* 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+5471 Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=55-| RIncs_hx_ld k r r':56- RIncs hx (1+k) r r' ->72+| RIncs_hx_ld k r r1 r':73+ Inc r r1 ->74+ RIncs hx (1+k) r1 r' ->5775 RIncs hx k (LD::r) (LD::r')58765977 | RIncs_hx_d1 k r r':@@ -64,8 +82,9 @@6482 RIncs hx (1+k) r r' ->6583 RIncs hx k (D0::r) (LD::r')668467-| RIncs_h1_ld k r r':68- RIncs hx (1+k) r r' ->85+| RIncs_h1_ld k r r1 r':86+ Inc r r1 ->87+ RIncs hx (1+k) r1 r' ->6988 RIncs h1 (1+k) (LD::r) (LD::r')70897190 | RIncs_h1_d1 k r r':@@ -86,9 +105,16 @@86105 | RIncs_h1_rh_1 k r':87106 RIncs h1 k [] r' ->88107 RIncs h1 (1+k*2) [] (D0::r')108+89109 | RIncs_h1_rh_2 k r':90110 RIncs h1 k [] r' ->91111 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]92118 .9311994120 Ltac cat3 :=@@ -104,21 +130,67 @@104130 Ltac tr2 :=105131 eapply sideRLs_trans; [esx | ].106132133+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+107143 Open Scope nat.108144145+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.173+109174 Lemma RIncs_spec tp k r r':110175 RIncs tp k r r' ->111176 sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').112177 Proof.113178 intro H.114179 induction H; intros; cbn[toH toH' toRC] in *.115- - 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.116185 - tr2.117186 cat3; wal.118187 - cat3; tr1; wal.119- - rewrite lpow_add,app_assoc.120- eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]); [|eauto 1].121- tr1; wal.188+ - change ([] ++ h^^(1+k)) with (h^^1 ++ h^^k).189+ eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]).190+ 1: apply seg_h1_ld.191+ eapply sideRLs_trans.192+ 1: apply Inc_spec; eassumption.193+ apply IHRIncs.122194 - rewrite lpow_add,app_assoc.123195 tr2.124196 cat3; wal.@@ -144,6 +216,54 @@144216 cat3.145217 rewrite app_nil_l.146218 am 2 1 k 1 0.219+ - cbn[lpow app]. rewrite z1_eq. constructor.220+ - cbn[lpow app]. rewrite z0_eq. constructor.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 with246+ | J: Inc [] _ |- _ => inversion J; subst; clear J247+ 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.147267 Qed.148268149269 Lemma RIncs_nxt_1 k:@@ -160,71 +280,261 @@160280 Unshelve. all: lia.161281 Qed.162282283+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'.307+Proof.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.349+Qed.163350164-Ltac solve_v2 :=165- (epose proof (RIncs_nxt_1 _) as [r I]; repeat ec; try apply I).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.166359167-Ltac solve_v1 H tp'0 k'0 H' :=168- eapply H with (tp':=tp'0) (k':=k'0) in H';169- try lia;170- try (171- destruct H' as [r'' I1];172- repeat ec; try apply I1).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 with363+ | hx, hx => k <= q /\ j <= q364+ | h1, hx => k+1 <= q /\ j <= q365+ | h1, h1 => (j = 0 /\ 2*k+1 <= q) \/ (1 <= j /\ k+j <= q /\ 1 <= q)366+ | hx, h1 => False367+ 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 IH378+ | k r r1 r' Hi D IH | k r r' D IH | a r r' D IH | a r r' D IH379+ | | 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.173527174-Lemma RIncs_nxt tp k r r' tp' k':175- RIncs tp k r r' ->176- match tp,tp' with177- | hx,hx => k<=k'178- | h1,h1 => k*2+1<=k'179- | h1,hx => k+1<=k'180- | _,_ => False181- end ->182- exists r'',183- RIncs tp' k' r' r''.184-Proof.185- gen tp k r' tp' k'.186- induction r; intros.187- {188- gen tp r' tp' k'.189- induction k using lt_wf_ind.190- intros.191- inverts H1; destruct tp'.192- all: try lia.193- - solve_v2.194- - destruct (sub k' 1); [subst|lia].195- solve_v2.196- - solve_v1 H0 hx (1+k') H3.197- - destruct (sub k' 1); [subst|lia].198- destruct (mod2 c); subst.199- + solve_v1 H0 h1 (a) H3.200- + solve_v1 H0 h1 (a) H3.201- - solve_v1 H0 h1 (k') H3.202- - destruct (sub k' 1); [subst|lia].203- solve_v1 H0 h1 (c) H3.204- }205- {206- inverts H0; destruct tp'.207- all: try lia.208- - solve_v1 IHr hx (1+k') H7.209- - solve_v1 IHr hx (1+k') H7.210- - solve_v1 IHr hx (1+k') H7.211- - solve_v1 IHr hx (1+k') H7.212- - destruct (sub k' 1); [subst|lia].213- solve_v1 IHr hx (1+c) H7.214- - solve_v1 IHr hx (1+k') H7.215- - destruct (sub k' 1); [subst|lia].216- solve_v1 IHr hx (1+c) H7.217- - solve_v1 IHr hx (1+k') H7.218- - destruct (sub k' 1); [subst|lia].219- destruct (mod2 c); subst.220- + solve_v1 IHr h1 (a) H7.221- + solve_v1 IHr h1 (a) H7.222- - solve_v1 IHr h1 k' H7.223- - destruct (sub k' 1); [subst|lia].224- solve_v1 IHr h1 (c) H7.225- }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.226535 Qed.227536537+228538 Open Scope sym.229539230540 Notation lh := (0inf<*<[1]).@@ -244,18 +554,46 @@244554 es.245555 Qed.246556557+Lemma start: c0 -->* S' [LD;D1].558+Proof. esx. Qed.559+247560 Lemma nonhalt: ~halts tm c0.248561 Proof.249- eapply multistep_nonhalt with (c':=S' [D1]).250- 1: esx.562+ eapply multistep_nonhalt with (c':=S' [LD;D1]).563+ 1: apply start.251564 eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').252- 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+ }253571 intros r [r' I1].254- pose proof I1 as I2.255- eapply RIncs_nxt with (tp':=hx) (k':=O) in I2.256- 2: lia.257572 exists r'; split.258- - apply BigStep,I1.259- - apply I2.573+ - apply BigStep, I1.574+ - apply (domain _ _ I1).260575 Qed.261576577+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 = 100584+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 1589+eater (hx,k): L -> L, k+1, inc the rest; 0 -> L, k+1; 1 -> L, drain with k590+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)/2593+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+*)