proposition: Lemma TestLeftof_Realise {Σ : finType} : @TestLeftof Σ ⊨ fun t '(b, t') => t = t' /\ match t with [| leftof _ _ |] => b = true | _ => b = false end.
proof: Proof. eapply Realise_monotone. { unfold TestLeftof. apply Switch_Realise; [now auto with nocore TMdb|]. instantiate (1 := fun x => if x then _ else _). intros []. - now auto with nocore TMdb. - apply Switch_Realise; [now auto with nocore TMdb|]. intros ?. instantiate (1 := fun x => _). apply Switch_Realise; [now auto with nocore TMdb|]. instantiate (1 := fun x => if x then _ else _). intros []; now auto with nocore TMdb. } intros t (b, t') ?. TMSimp. rename t_0 into t. destruct t; cbn in *; TMSimp; eauto. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString