proposition: Lemma choicerule : forall k1 k2, k1 <= mu p1 Q -> k2 <= mu p2 Q -> (k1 * ([1-] k2) + k2) <= mu p Q.
proof: Proof. unfold p,Mlet,star; simpl; unfold unit; intros. apply Ole_trans with (mu p1 (fun x : A => mu p2 (fun y : A => Q x * ([1-] (Q y)) + Q y))). apply Ole_trans with (mu p1 (fun x : A => ((mu p2 (fun y : A => Q x * ([1-] (Q y)))) +(mu p2 Q)))). change (k1 * [1-] k2 + k2 <= mu p1 (fplus (fun x : A => mu p2 (fun y : A => Q x * [1-] (Q y))) (fun x => mu p2 Q))). assert (H1 : fplusok (fun x : A => mu p2 (fun y : A => Q x * [1-] (Q y))) (fun x => mu p2 Q)). repeat red; unfold finv; intros. apply Ole_trans with (mu p2 (fun y : A => [1-] (Q y))). apply (mu_monotonic p2); auto. apply (mu_stable_inv p2 Q). setoid_rewrite (mu_stable_plus p1 H1). assert (Heq1:mu p1 (fun _ : A => mu p2 Q) == mu p2 Q). exact (mu_cte_eq p1 (mu p2 Q) p1_terminates). rewrite Heq1. apply Ole_trans with (k1 * [1-] (mu p2 Q) + (mu p2 Q)); auto. Usimpl. apply Ole_trans with (mu p1 (fun x : A => (Q x) * mu p2 (finv Q))). apply Ole_trans with ((mu p1 Q) * (mu p2 (finv Q))). rewrite (mu_one_inv p2 p2_terminates Q); auto. rewrite (mu_stable_mult_right p1 (mu p2 (finv Q)) Q); auto. apply (mu_monotonic p1); intro x. rewrite <- (mu_stable_mult p2 (Q x) (finv Q)); auto. apply (mu_monotonic p1); intro x. assert (fplusok (fun y : A => Q x * [1-] (Q y)) Q). intro y; unfold finv; auto. rewrite <- (mu_stable_plus p2 H1); auto. apply (mu_monotonic p1); intro x. apply (mu_monotonic p2); intro y. apply Ole_trans with ((Q x) + (Q y)); auto. Qed.
imports: ALEA(Utheory)