proposition: Lemma StateWhileCoInduction : (forall l (tin : tapes sig n) (k : nat) (HT : T l tin k), exists k1, T' l tin k1 /\ forall (ymid : F1 + F2) tmid, R l tin (ymid, tmid) -> match ymid with | inl l1 => exists k2, T l1 tmid k2 /\ 1 + k1 + k2 <= k | inr _ => k1 <= k end) -> (forall l, T l <<=2 StateWhile_T R T' l).
proof: Proof. intros. revert l. cofix IH. intros l tin k HT. specialize H with (1 := HT) as (k1&H1&H2). econstructor; eauto. - intros tmid ymid HR. specialize (H2 (inl ymid) tmid HR) as (k2&H2&Hk); cbn in *. exists k2. split. 2: lia. now apply IH. - intros tmid l2 HR. now specialize (H2 (inr l2) tmid HR). Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts