proposition: Lemma TestLeftof_total {Σ} : isTotal (@TestLeftof Σ).
proof: Proof. unfold TestLeftof. eexists. eapply TerminatesIn_monotone. { eapply Switch_TerminatesIn; [now auto with nocore TMdb..|]. instantiate (1 := fun x => if x then _ else ltac:(clear x; refine _)). intros []; [now auto with nocore TMdb..|]. apply Seq_TerminatesIn; [now auto with nocore TMdb..|]. eapply Switch_TerminatesIn; [now auto with nocore TMdb..|]. instantiate (1 := fun x => if x then _ else _). intros []; now auto with nocore TMdb. } intros ? ? ?. exists 1, 5. split; [apply Nat.le_refl|]. split; [apply H|]. intros tout yout. rewrite (destruct_tape tout). cbn. intros [-> <-]. destruct current; [apply Nat.le_0_l|]. exists 1, 3. split; [apply Nat.le_refl|]. split; [apply Nat.le_refl|]. intros tout' _. rewrite (destruct_tape tout'). cbn. intros ->. exists 1, 1. split; [apply Nat.le_refl|]. split; [apply Nat.le_refl|]. intros ? ? [-> ?]. destruct current; lia. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString