- [ [I;I], [I];
- [C;C], [C];
- [M;M], [];
- [M;C], [I;M];
- [C;M], [M;I];
-(*
-axiom leq_refl: ∀A. A ⊆ A.
-axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
-axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C.
-
-axiom i_contrattivita: ∀A. i A ⊆ A.
-axiom i_idempotenza: ∀A. i (i A) = i A.
-axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B.
-axiom c_espansivita: ∀A. A ⊆ c A.
-axiom c_idempotenza: ∀A. c (c A) = c A.
-axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B.
-axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A.
-axiom m_saturazione: ∀A. A ⊆ m (m A).
-axiom m_puntofisso: ∀A. m A = m (m (m A)).
-axiom th1: ∀A. c (m A) ⊆ m (i A).
-axiom th2: ∀A. i (m A) ⊆ m (c A).
-lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B.
-lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B.
-*)
+ [ [I], Le, [];
+ [C], Ge, [];
+ [I;I], Ge, [I];
+ [C;C], Le, [C];
+ [I], Le, [I];
+ [I], Ge, [I];
+ [C], Le, [C];
+ [C], Ge, [C];
+ [C;M], Le, [M;I];
+ [C;M;I], Le, [M;I]; (* ??? *)
+ [I;M], Le, [M;C];
+ [I;M;C], Ge, [I;M]; (* ??? *)
+ [M;M;M], Ge, [M];
+ [M;M], Ge, [];
+ [M], Le, [M];
+ [M], Ge, [M];