proposition: Theorem expected_poly_time_if_f : forall (A B: nat -> Type)(f_b : forall n, (A n) -> bool)(f_so f_not : forall n, A n -> B n), efficient _ f_b -> efficient _ f_so -> efficient _ f_not -> efficient _ (fun n (a : A n) => if (f_b n a) then (f_so n a) else (f_not n a)).
proof: Proof. intuition. eapply (@expected_poly_time_compose _ _ _ _ _ _ (fun n a (b : bool) => if b then (f_so n a) else (f_not n a))); eauto. eapply expected_poly_time_pair_arg. eapply (@expected_poly_time_compose _ _ _ _ _ _ (fun n (a : A n * bool) b => if (snd a) then b else (f_not n (fst a)))); eauto. apply (@expected_poly_time_compose_simp _ _ _ _ f_so); eauto. eapply expected_poly_time_fst. eapply expected_poly_time_pair_arg. eapply (@expected_poly_time_compose _ _ _ _ _ _ (fun n (a : A n * bool * B n) b => if (snd (fst a)) then (snd a) else b)); eauto. apply (@expected_poly_time_compose_simp _ _ _ _ f_not); eauto. apply (@expected_poly_time_compose_simp _ _ _ _ (fun n a => fst a)); eauto. eapply expected_poly_time_fst. eapply expected_poly_time_fst. eapply expected_poly_time_unpair_arg. eapply expected_poly_time_unpair_arg. simpl. eapply expected_poly_time_const. eapply expected_poly_time_if. Qed.
imports: FCF.Crypto FCF.Asymptotic FCF.FCF