proposition: Lemma Step_total q : isTotal (Step q).
proof: Proof. destruct (MoveB_total n). destruct (ReadB_total n). destruct (WriteB_total'). eexists. eapply TerminatesIn_monotone. - unfold Step. eapply Switch_TerminatesIn. { now auto with nocore TMdb. } { eassumption. } cbn. intros c_i. instantiate (1 := ltac:(intros c_i; refine _)); cbn. instantiate (1 := ltac:(destruct (halt q); refine _)); cbn. destruct halt. { now auto with nocore TMdb. } instantiate (1 := ltac:(destruct (trans (q, [| map_opt g c_i |])) as [? t], (Vector.hd t))). destruct (trans (q, [| map_opt g c_i |])); cbn. destruct (Vector.hd t). now auto with nocore TMdb. - cbn. intros ? ? ?. repeat eexists. { apply Nat.le_refl. } { eapply H2. } intros. instantiate (1 := ltac:(destruct (halt q))); cbn. destruct halt. { apply Nat.le_0_l. } rename yout into c_i. destruct (trans (q, [| map_opt g c_i |])); cbn. destruct (Vector.hd t); cbn. repeat eexists. { apply Nat.le_refl. } { apply Nat.le_refl. } { apply Nat.le_refl. } { apply Nat.le_refl. } intros. apply Nat.le_0_l. Unshelve. all: exact 0. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString