proposition: Theorem fcf_oracle_eq_until_bad : forall {S1 S2 : Set}(bad1 : S1 -> bool) (bad2 : S2 -> bool)(inv : S1 -> S2 -> Prop)(A B C : Set) (c : OracleComp A B C), well_formed_oc c -> forall (eqdb : EqDec B) (eqdc : EqDec C) (o1 : S1 -> A -> Comp (B * S1)) (o2 : S2 -> A -> Comp (B * S2)) (eqds1 : EqDec S1) (eqds2 : EqDec S2), (forall (a : S1) (b : A), bad1 a = true -> well_formed_comp (o1 a b)) -> (forall (a : S2) (b : A), bad2 a = true -> well_formed_comp (o2 a b)) -> (forall (x1 : S1) (x2 : S2) (a : A), inv x1 x2 -> bad1 x1 = bad2 x2 -> comp_spec (fun (y1 : B * S1) (y2 : B * S2) => bad1 (snd y1) = bad2 (snd y2) /\ (bad1 (snd y1) = false -> inv (snd y1) (snd y2) /\ fst y1 = fst y2)) (o1 x1 a) (o2 x2 a)) -> (forall (a : B) (b c0 : S1) (d : A), bad1 c0 = true -> In (a, b) (getSupport (o1 c0 d)) -> bad1 b = true) -> (forall (a : B) (b c0 : S2) (d : A), bad2 c0 = true -> In (a, b) (getSupport (o2 c0 d)) -> bad2 b = true) -> forall (s1 : S1) (s2 : S2), inv s1 s2 -> bad1 s1 = bad2 s2 -> comp_spec (fun (y1 : C * S1) (y2 : C * S2) => bad1 (snd y1) = bad2 (snd y2) /\ (bad1 (snd y1) = false -> inv (snd y1) (snd y2) /\ fst y1 = fst y2)) (c S1 eqds1 o1 s1) (c S2 eqds2 o2 s2).
proof: Proof. intuition. eapply oc_comp_spec_eq_until_bad; intuition. Qed.
imports: FCF.Crypto FCF.DistTacs FCF.ProgTacs FCF.GenTacs FCF.ProgramLogic