proposition: Theorem Prob_or_indep : forall (c1 c2 : Comp bool), well_formed_comp c2 -> Pr[b1 <-$ c1; b2 <-$ c2; ret (b1 || b2)] == Pr[c1] + (evalDist c1 false) * Pr[c2].
proof: Proof. intuition. rewrite bool_Comp_seq. assert (Pr [b2 <-$ c2; ret true || b2 ] == 1). comp_irr_l. rewrite evalDist_ret_1; simpl; intuition. rewrite H0. clear H0. assert (Pr [b2 <-$ c2; ret false || b2 ] == Pr[c2]). rewrite bool_Comp_seq. rewrite evalDist_ret_1. rewrite evalDist_ret_0. rewrite ratMult_0_r. rewrite <- ratAdd_0_r. eapply ratMult_1_r. simpl. intuition. simpl; intuition. rewrite H0. clear H0. rewrite ratMult_1_r. intuition. Qed.
imports: FCF.FCF FCF.CompFold