proposition: Theorem ifthenelse_continuous : forall (A:Type) t F G, continuous (f_order' A) (f_order' A) F -> continuous (f_order' A) (f_order' A) G -> continuous (f_order' A) (f_order' A) (fun f x => 'IF (t x) 'THEN (F f x) 'ELSE (G f x)).
proof: Proof. intros A t F G HF HG c Hc l Hl. apply (lift_lub A (option A) (@option_cpo A)). intros x; destruct (t x) as [[ | ] | ]; simpl. apply lub_lift_reverse with (l := F l)(c:= fun n => F (c n)); apply HF; auto. apply lub_lift_reverse with (l := G l)(c:= fun n => G (c n)); apply HG; auto. split; intro; auto. Qed.
imports: Relations Classical ClassicalEpsilon Zwf function_cpo