- downarrow: unary_morphism1 (form bp) (form bp);
- downarrow_is_sat: is_o_saturation ? downarrow;
- converges: ∀q1,q2.
- (Ext⎽bp q1 ∧ (Ext⎽bp q2)) = (Ext⎽bp ((downarrow q1) ∧ (downarrow q2)));
- all_covered: Ext⎽bp (oa_one (form bp)) = oa_one (concr bp);
- il2: ∀I:SET.∀p:arrows2 SET1 I (form bp).
- downarrow (∨ { x ∈ I | downarrow (p x) | down_p ???? }) =
- ∨ { x ∈ I | downarrow (p x) | down_p ???? };
- il1: ∀q.downarrow (A ? q) = A ? q
+ Odownarrow: unary_morphism1 (Oform Obp) (Oform Obp);
+ Odownarrow_is_sat: is_o_saturation ? Odownarrow;
+ Oconverges: ∀q1,q2.
+ (Ext⎽Obp q1 ∧ (Ext⎽Obp q2)) = (Ext⎽Obp ((Odownarrow q1) ∧ (Odownarrow q2)));
+ Oall_covered: Ext⎽Obp (oa_one (Oform Obp)) = oa_one (Oconcr Obp);
+ Oil2: ∀I:SET.∀p:arrows2 SET1 I (Oform Obp).
+ Odownarrow (∨ { x ∈ I | Odownarrow (p x) | down_p ???? }) =
+ ∨ { x ∈ I | Odownarrow (p x) | down_p ???? };
+ Oil1: ∀q.Odownarrow (A ? q) = A ? q