proposition: Lemma IsCons_Sem : IsCons ⊨c(IsCons_steps) IsCons_Rel.
proof: Proof. unfold IsCons_steps. eapply RealiseIn_monotone. { unfold IsCons. now auto with nocore TMdb. } { reflexivity. } { intros tin (yout, tout) H. split. { intros tps1 tps2 tp HCons. unfold atCons in *. TMSimp. auto. } { intros tps HNil. unfold atNil in *. TMSimp. auto. } } Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)