oa_zero_bot: ∀p:oa_P.𝟘 ≤ p;
oa_one_top: ∀p:oa_P.p ≤ 𝟙;
oa_overlap_preserves_meet_: ∀p,q:oa_P.p >< q →
- p >< (⋀ { x ∈ BOOL | If x then p else q(*match x with [ true ⇒ p | false ⇒ q ]*) | IF_THEN_ELSE_p oa_P p q });
+ p >< (⋀ { x ∈ BOOL | If x then p else q | IF_THEN_ELSE_p oa_P p q });
oa_join_split: ∀I:SET.∀p.∀q:I ⇒_2 oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
(*oa_base : setoid;
1) enum non e' il nome giusto perche' non e' suriettiva
qed.
coercion arrows1_of_ORelation_setoid.
-notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
-notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
-
-notation "r \sup (⎻* )" non associative with precedence 90 for @{'OR_f_minus_star $r}.
-notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r}.
-
-notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
-notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
-
interpretation "o-relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (or_f_minus_star ? ?) r).
interpretation "o-relation f⎻" 'OR_f_minus r = (fun12 ?? (or_f_minus ? ?) r).
interpretation "o-relation f*" 'OR_f_star r = (fun12 ?? (or_f_star ? ?) r).
definition or_prop1 : ∀P,Q:OAlgebra.∀F:ORelation_setoid P Q.∀p,q.
- (F p ≤ q) = (p ≤ F* q).
+ (F p ≤ q) =_1 (p ≤ F* q).
intros; apply (or_prop1_ ?? F p q);
qed.