- oa_leq_refl: ∀a:oa_P. oa_leq a a;
- oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
- oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
- oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
- oa_meet_inf:
- ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.
- oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i);
- oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = ∀i:I.oa_leq (p_i i) p;
- oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
- oa_one_top: ∀p:oa_P.oa_leq p oa_one;
- oa_overlap_preserves_meet_:
- ∀p,q:oa_P.oa_overlap p q → oa_overlap p
- (oa_meet ? { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
- oa_join_split:
- ∀I:SET.∀p.∀q:I ⇒ oa_P.
- oa_overlap p (oa_join I q) = ∃i:I.oa_overlap p (q i);
+ oa_leq_refl: ∀a:oa_P. a ≤ a;
+ oa_leq_antisym: ∀a,b:oa_P.a ≤ b → b ≤ a → a = b;
+ oa_leq_trans: ∀a,b,c:oa_P.a ≤ b → b ≤ c → a ≤ c;
+ oa_overlap_sym: ∀a,b:oa_P.a >< b → b >< a;
+ oa_meet_inf: ∀I:SET.∀p_i:I ⇒_2 oa_P.∀p:oa_P.p ≤ (⋀ p_i) = (∀i:I.p ≤ (p_i i));
+ oa_join_sup: ∀I:SET.∀p_i:I ⇒_2 oa_P.∀p:oa_P.(⋁ p_i) ≤ p = (∀i:I.p_i i ≤ p);
+ 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 });
+ oa_join_split: ∀I:SET.∀p.∀q:I ⇒_2 oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));