proposition: Lemma WhileCoInduction : (forall (tin : tapes sig n) (k : nat) (HT : T tin k), exists k1, T' tin k1 /\ forall (ymid : option F) tmid, R tin (ymid, tmid) -> match ymid with | Some _ => k1 <= k | None => exists k2, T tmid k2 /\ 1 + k1 + k2 <= k end) -> T <<=2 While_T R T'.
proof: Proof. intros. cofix IH. intros tin k HT. specialize H with (1 := HT) as (k1&H1&H2). econstructor; eauto. - intros tmid ymid HR. specialize (H2 (Some ymid) tmid); cbn in *. auto. - intros tmid HR. specialize (H2 None tmid) as (k2&H3&H4); eauto. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts