The kill file, 599 lines, sha256 e434537eca67d99f… (same file as submission/). Right column: one note per item, with its tag, the proof.md section it formalizes and TM7's counterpart in SOMDCv6.v. Tags are computed: copied = same text as TM7, adapted = TM7's text with edits (edited lines shaded), new = no TM7 text. Raw file: 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 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. *)
10From BusyCoq Require Import Individual62 Longitudinal DivModCases.11Require Import ZifyNat Lia.12Require Import ZArith.13Require Import String.14Require Import List.
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]).
22Ltac ec := econstructor.27Definition tm := Eval compute in (TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").28Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).29Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
34Notation w1ld := [1;1;1;0].35Notation hR := (B,@nil Sym).36Notation hR' := (D,[1]).37Notation hL := (C,@nil Sym).38Notation h := [(hR,hL)].39Notation h' := [(hR',hL)].
44Fixpoint toRC ls :=45match ls with46| [] => 0inf47| LD::ls => ld*>toRC ls48| D0::ls => d0*>toRC ls49| D1::ls => d1*>toRC ls50end.
64(* one h pass over the digits = +1 on the little-endian binary number of the 0/1 digits, 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').
71Inductive RIncs: H->nat->(list RD)->(list RD)->Prop :=72| RIncs_hx_ld k r r1 r':73 Inc r r1 ->74 RIncs hx (1+k) r1 r' ->75 RIncs hx k (LD::r) (LD::r')7677| RIncs_hx_d1 k r r':78 RIncs h1 k r r' ->79 RIncs hx k (D1::r) (LD::r')8081| RIncs_hx_d0 k r r':82 RIncs hx (1+k) r r' ->83 RIncs hx k (D0::r) (LD::r')8485| RIncs_h1_ld k r r1 r':86 Inc r r1 ->87 RIncs hx (1+k) r1 r' ->88 RIncs h1 (1+k) (LD::r) (LD::r')8990| RIncs_h1_d1 k r r':91 RIncs h1 k r r' ->92 RIncs h1 (1+k) (D1::r) (LD::r')9394| RIncs_h1_d0_0 k r r':95 RIncs h1 k r r' ->96 RIncs h1 (1+k*2) (D0::r) (D0::r')9798| RIncs_h1_d0_1 k r r':99 RIncs h1 k r r' ->100 RIncs h1 (2+k*2) (D0::r) (D1::r')101102| RIncs_h1_rh_0:103 RIncs h1 0 [] [D1]104105| RIncs_h1_rh_1 k r':106 RIncs h1 k [] r' ->107 RIncs h1 (1+k*2) [] (D0::r')108109| RIncs_h1_rh_2 k r':110 RIncs h1 k [] r' ->111 RIncs h1 (2+k*2) [] (D1::r')112113| RIncs_h1_z1:114 RIncs h1 0 [D1] [LD]115116| RIncs_h1_z0:117 RIncs h1 0 [D0] [D1]118.
120Ltac cat3 :=121 eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]); [|eauto 1].122123Ltac tr1 :=124 rewrite lpow_add,app_assoc;125 eapply segRLs_trans; [esx | ].126127Ltac wal :=128 eapply segRLs_wall''; esx.129130Ltac tr2 :=131 eapply sideRLs_trans; [esx | ].
133Lemma z1_eq: [1] *> d1 *> 0inf = ld *> 0inf.134Proof.135 cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold.136Qed.
138Lemma z0_eq: [1] *> d0 *> 0inf = d1 *> 0inf.139Proof.140 cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold.141Qed.
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.
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.
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.
174Lemma RIncs_spec tp k r r':175 RIncs tp k r r' ->176 sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').177Proof.178 intro H.179 induction H; intros; cbn[toH toH' toRC] in *.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.185 - tr2.186 cat3; wal.187 - cat3; 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.194 - rewrite lpow_add,app_assoc.195 tr2.196 cat3; wal.197 - cat3.198 rewrite app_nil_l.199 am 2 1 k 1 1.200 rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.201 tr2; eauto 1.202 - cat3.203 rewrite Nat.add_comm.204 am 2 1 k 2 1.205 rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.206 tr2; eauto 1.207 - esc.208 - rewrite lpow_add,app_assoc.209 tr2.210 cat3.211 rewrite app_nil_l.212 am 2 1 k 0 0.213 - change (2+k*2) with (1+(1+k*2)).214 rewrite lpow_add,app_assoc.215 tr2.216 cat3.217 rewrite app_nil_l.218 am 2 1 k 1 0.219 - cbn[lpow app]. rewrite z1_eq. constructor.220 - cbn[lpow app]. rewrite z0_eq. constructor.221Qed.
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.
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.
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.
244Ltac inc_nil :=245 repeat match goal with246 | J: Inc [] _ |- _ => inversion J; subst; clear J247 end.
249(* proof.md Lemma A: one more pass after the k passes is +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.
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.
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.
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.
319(* inversion helpers *)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.323324Lemma 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.327328Lemma 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.331332Lemma 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.335336Lemma 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.339340Lemma 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.350351Lemma 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.
360(* proof.md section 3.3: the second sweep reads the first's output after j pending +1s *)361Definition 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.
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 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.526Qed.
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.
540Notation lh := (0inf<*<[1]).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.
560Lemma nonhalt: ~halts tm c0.561Proof.562 eapply multistep_nonhalt with (c':=S' [LD;D1]).563 1: apply start.564 eapply progress_nonhalt_cond with (P:=fun r => exists r', RIncs hx 0 r r').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 }571 intros r [r' I1].572 exists r'; split.573 - apply BigStep, I1.574 - apply (domain _ _ I1).575Qed.
579(*580```5811RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---582583S(r) = 0^inf 11 D> <r> 0^inf digits: L = 110, 0 = 000, 1 = 100584start: 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'586587inc(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 1589eater (hx,k): L -> L, k+1, inc the rest; 0 -> L, k+1; 1 -> L, drain with k590drain (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)/2593last digit, drain with k = 0: 1 -> L, 0 -> 1 (1 100 0^inf = 110 0^inf, 1 000 0^inf = 100 0^inf)594595domain: 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*)