proposition: Lemma While_TerminatesIn_ind : pM ⊨ R -> projT1 pM ↓ T' -> (forall (tin : tapes sig n) (k : nat), T tin k -> exists k1, T' tin k1 /\ (forall ymid tmid, R tin (Some ymid, tmid) -> k1 <= k) /\ (forall tmid, R tin (None, tmid) -> exists k2, T tmid k2 /\ 1 + k1 + k2 <= k)) -> WhileTM ↓T.
proof: Proof. intros Realise_M Term_M Hyp tin i. revert tin. apply complete_induction with (x:=i); clear i; intros i IH tin. intros (i1&HT1&HT2&HT3) % Hyp. pose proof (Term_M _ _ HT1) as (oconf&Hloop). specialize (Realise_M _ _ _ Hloop). destruct (projT2 pM (cstate oconf)) as [ ymid | ] eqn:E1. - specialize HT2 with (1 := Realise_M). exists oconf. eapply loop_monotone; eauto. eapply While_merge_term; eauto. - specialize HT3 with (1 := Realise_M) as (i2&HT3&Hi). specialize (IH i2 ltac:(lia) _ HT3) as (oconf2&Hloop2). exists oconf2. apply loop_monotone with (k1 := i1 + (1 + i2)). 2: lia. eapply While_merge_repeat; eauto. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts