proposition: Lemma WhileInduction : (forall tin yout tout (HLastStep: R1 tin (Some yout, tout)), R2 tin (yout, tout)) -> (forall tin tmid tout yout (HStar : R1 tin (None, tmid)) (HLastStep : R2 tmid (yout, tout)), R2 tin (yout, tout)) -> While_Rel R1 <<=2 R2.
proof: Proof. intros H1 H2. intros tin tout. induction 1; eauto. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts