proposition: Lemma While_Realise : pM ⊨ R -> While ⊨ While_Rel.
proof: Proof. intros HRel. hnf in HRel; hnf. intros t k; revert t. apply complete_induction with (x := k); clear k; intros k IH. intros tin c3 HLoop. apply While_split in HLoop as (k1&k2&c2&HLoop1&HLoop2&Hk). destruct (projT2 pM (cstate c2)) as [ f | ] eqn:E; cbn in *; [ clear IH | ]. - apply While_split_term with (f := f) in HLoop2 as ->; auto. 2: apply (loop_fulfills HLoop1). unfold While_part. rewrite E. constructor 1. specialize HRel with (1 := HLoop1). now rewrite E in HRel. - apply While_split_repeat in HLoop2 as (k2'&->&HLoop2); auto. 2: apply (loop_fulfills HLoop1). specialize IH with (2 := HLoop2); spec_assert IH by lia. econstructor 2. + specialize HRel with (1 := HLoop1). rewrite E in HRel. eassumption. + apply IH. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts