proposition: Lemma WriteB_TerminatesIn (n : nat) (c : option (Fin.t n)) : isTotal (WriteB c).
proof: Proof. destruct (@MoveM_isTotal (finType_CS bool) Lmove n) as [MoveM_c H_MoveM]. destruct (@TestLeftof_total (finType_CS bool)) as [kT HT]. red. eexists. eapply TerminatesIn_monotone. { unfold WriteB. destruct c; cbn. - instantiate (1 := ltac:(destruct c; refine _ )). cbn. apply Switch_TerminatesIn; [now auto with nocore TMdb..|]. instantiate (1 := fun x => if x then _ else _). intros []; now auto with nocore TMdb. - cbn. now auto with nocore TMdb. } cbn. intros ? ? ?. destruct c; cbn. + repeat eexists. { eapply Nat.le_refl. } { unshelve eapply (Nat.le_trans _ _ _ _ H). eapply Nat.le_refl. } intros. TMSimp. destruct yout. * cbn. repeat (rewrite !app_length, ?rev_length, ?length_encode_sym; cbn). eapply Nat.le_add_r. * repeat eexists. { eapply Nat.le_refl. } { repeat (rewrite !app_length, ?rev_length, ?length_encode_sym; cbn). eapply Nat.le_add_l. } { eapply Nat.le_refl. } { eapply Nat.le_refl. } intros. eapply Nat.le_refl. + lia. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString