proposition: Lemma StateWhile_TerminatesIn_ind l : (forall l, pM l ⊨ R l) -> (forall l, projT1 (pM l) ↓ T' l) -> (forall l (tin : tapes sig n) (k : nat), T l tin k -> exists k1, T' l tin k1 /\ (forall tmid l2, R l tin (inr l2, tmid) -> k1 <= k) /\ (forall tmid l1, R l tin (inl l1, tmid) -> exists k2, T l1 tmid k2 /\ 1 + k1 + k2 <= k)) -> StateWhileTM l ↓ T l.
proof: Proof. intros Realise_M Term_M Hyp tin k. revert tin l. apply complete_induction with (x:=k); clear k; intros k IH tin l. intros (k1&HT1&HT2&HT3) % Hyp. pose proof (Term_M _ _ _ HT1) as (oconf&Hloop). specialize (Realise_M _ _ _ _ Hloop). destruct (projT2 (pM l) (cstate oconf)) as [ l1 | l2 ] eqn:E1. - specialize HT3 with (1 := Realise_M) as (k2&HT3&Hi). specialize (IH k2 ltac:(lia) _ _ HT3) as (oconf2&Hloop2). exists oconf2. apply loop_monotone with (k1 := k1 + (1 + k2)). 2: lia. cbn -[plus]. rewrite lift_init. refine (StateWhile_merge_repeat Hloop _ _ Hloop2); auto. unfold loopM in *; now apply loop_fulfills in Hloop. - specialize HT2 with (1 := Realise_M). exists (lift oconf). eapply loop_monotone; eauto. refine (StateWhile_merge_break (l2 := l2) Hloop _ _); auto. unfold loopM in *; now apply loop_fulfills in Hloop. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts