proposition: Lemma ReadB_total n : isTotal (ReadB n).
proof: Proof. induction n. - cbn. exists 0. eapply TerminatesIn_monotone. { now auto with nocore TMdb. } intros ? ? H. exact H. - destruct IHn as [c IH]. eexists. eapply TerminatesIn_monotone. { cbn. eapply Switch_TerminatesIn; [now auto with nocore TMdb..|]. intros []. { instantiate (1 := fun f => if f then _ else _). cbn. instantiate (1 := ltac:(clear f; refine _)). eapply Seq_TerminatesIn; [now auto with nocore TMdb..|]. eapply Switch_TerminatesIn; [now auto with nocore TMdb..|]. intros []. { instantiate (1 := fun f => match f with Some true => _ | Some false => _ | None => _ end). cbn. destruct b0 as [ | ]. + cbn. instantiate (1 := ltac:(clear f b0; refine _)). now auto with nocore TMdb. + instantiate (1 := ltac:(clear f b0; refine _)). eapply Switch_TerminatesIn. { eapply ReadB_Realise. } { eassumption. } intros []. { cbn. instantiate (1 := fun f => if f then _ else _). cbn. now auto with nocore TMdb. } now auto with nocore TMdb. } cbn. instantiate (1 := ltac:(clear f; refine _)). now auto with nocore TMdb. } cbn. instantiate (1 := ltac:(clear f; refine _)). now auto with nocore TMdb. } cbn. intros ? ? ?. exists 1. eexists. split. { lia. } split. 2:{ intros. TMSimp. destruct (current _). * exists 1. eexists. split. { lia. } split. 2:{ intros. TMSimp. exists 1. eexists. split. { lia. } split. 2:{ intros. TMSimp. destruct current. { destruct b0. { instantiate (1 := S _). lia. } exists c. eexists. split. { lia. } split. 2:{ intros. destruct yout; apply Nat.le_refl. } apply Nat.le_refl. } lia. } apply Nat.le_refl. } apply Nat.le_refl. * lia. } eapply H. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators