proposition: Lemma Loop_Realise q : Loop q ⊨ Loop_Rel q.
proof: Proof. eapply Realise_monotone. { unfold Loop. now auto with nocore TMdb. } { apply StateWhileInduction; intros; intros T HEncT; TMSimp. - specialize (HLastStep _ HEncT). destruct (halt l) eqn:E. + destruct HLastStep as [HLastStep [= HLastStep']]. eexists _, 0. cbn. unfold haltConf. cbn. rewrite E. repeat split; auto. + destruct (step _). destruct HLastStep as [_ [= ?]]. - specialize (HStar _ HEncT). destruct (halt l) eqn:E. + destruct HStar as [HStar [= HStar']]. + destruct (step _) as [q' T'] eqn:E'. destruct HStar as [HStar [= HStar']]. specialize (HLastStep _ HStar). destruct HLastStep as (c'&k&HLastStep&HLastStep'&->). eexists _, (S k). cbn. unfold haltConf. cbn. rewrite E, E'. subst. repeat split; 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)