-lapply (meet_join_plus ? ? x (y ∨ z)) as H;
-lapply (meet_join_plus ? ? y z) as H1;
- (*CSC: A questo punto ti servono dei lemmi sui gruppi che non sono ancora
- stati dimostrati. E una valanga di passi di riscrittura :-)
- *)
-
+cut (μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z)))); [2:
+ lapply (modular_mjp ?? x (y ∨ z)) as H1;
+ apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ?? H1); clear H1;
+ apply (eq_trans ?? ? ?? (plus_comm ???));
+ (* apply (eq_trans ?? (0+μ(x∧(y∧z))) ?? (opp_inverse ??)); ASSERT FALSE *)
+ apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z)))); [2: apply eq_sym; apply plus_assoc;]
+ apply (eq_trans ?? (0+μ(x∧(y∨z)))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse;]
+ (* apply (eq_trans ?? ? ? (eq_refl ??) (zero_neutral ??)); ASSERT FALSE *)
+ apply (eq_trans ?? (μ(x∧(y∨z)))); [apply eq_reflexive| apply eq_sym; apply zero_neutral]]
+apply (eq_trans ?? ? ? Hcut); clear Hcut;
+cut ( μ(y∨z) ≈ μy + μz + -μ (y ∧ z)); [2:
+ lapply (modular_mjp ?? y z) as H1;
+ apply (plus_cancr ??? (μ(y ∧ z)));
+ apply (eq_trans ?? ? ? H1); clear H1;
+ apply (eq_trans ?? ? ?? (plus_assoc ????));
+ apply (eq_trans ?? (μy+ μz + 0)); [2: apply feq_plusl; apply eq_sym; apply opp_inverse]
+ apply (eq_trans ?? ? ?? (plus_comm ???));
+ apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+ apply eq_reflexive;]
+apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [
+ apply feq_plusr; apply feq_plusl; apply Hcut] clear Hcut;
+apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
+ apply feq_plusl; apply feq_opp;
+ apply (eq_trans ?? ? ? (join_assoc ?????));
+ apply (eq_trans ?? ? ? (join_comm ????));
+ apply eq_reflexive;]
+apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
+apply feq_plusr; apply plus_assoc;
+qed.