proposition: Theorem DM_RC_G1_equiv : forall c x, (forall a s_A, In (a, s_A) (getSupport A1) -> well_formed_comp (c a)) -> (forall a s_A, In (a, s_A) (getSupport A1) -> exists b, In b (filter P (getSupport (c a)))) -> evalDist (RepeatCore_G P A1 A2 c) x == evalDist (DM_RC_G1 c) x.
proof: Proof. intuition. unfold RepeatCore_G, DM_RC_G1. comp_skip. comp_simp. assert (evalDist (b0 <-$ Repeat (c a) P; A2 a0 b0) x == evalDist (p <-$ (b0 <-$ Repeat (c a) P; b <-$ A2 a0 b0; ret (b0, b)); ret (snd p)) x). inline_first. comp_skip. inline_first. rewrite <- evalDist_right_ident. comp_skip. comp_simp. simpl. reflexivity. rewrite H2. comp_skip. eapply repeat_fission; intuition. eauto. eauto. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid