proposition: Lemma MoveB_total (n : nat) : exists c, forall m, projT1 (MoveB m n) ↓ fun t k => c <= k.
proof: Proof. destruct (@TestLeftof_total (finType_CS bool)) as [c Hlo]. destruct (@MoveM_isTotal (finType_CS bool) Lmove n) as [c1 H1]. destruct (@MoveM_isTotal (finType_CS bool) Nmove n) as [c2 H2]. destruct (@MoveM_isTotal (finType_CS bool) Rmove n) as [c3 H3]. assert (forall m, projT1 (MoveM m n) ↓ (fun (_ : tapes (finType_CS bool) 1) (k : nat) => c1+c2+c3 <= k)) as HMoveM. { intros []; eapply TerminatesIn_monotone; try eassumption. all: intros ??; lia. } eexists. intros m. specialize (HMoveM m). eapply TerminatesIn_monotone. { unfold MoveB. eapply Switch_TerminatesIn; [now auto with nocore TMdb..|]. intros f. instantiate (1 := fun f => if f then _ else _). destruct f. - destruct m. { instantiate (1 := ltac:(destruct m, f; refine _)). all: cbn. all: now auto with nocore TMdb. } all: cbn; now auto with nocore TMdb. - instantiate (1 := ltac:(destruct f; refine _)); cbn. now auto with nocore TMdb. } intros ? ? ?. repeat eexists. { eapply Nat.le_refl. } { unshelve eapply (Nat.le_trans _ _ _ _ H). { eapply Nat.le_refl. } } intros. cbn. TMSimp. destruct yout. + destruct m; cbn. * repeat eexists. all: intros; (try apply Nat.le_refl); lia. * lia. * repeat eexists. all: intros; (try apply Nat.le_refl); lia. + repeat eexists. all: intros; (try apply Nat.le_refl); lia. Unshelve. all: exact (fun _ _ => True). Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString