[apply Exy|apply Eyz] assumption.
qed.
-lemma eq_trans:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_trans_.
+lemma eq_trans:∀E:apartness.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝
+ λE,x,y,z.eq_trans_ E x z y.
+
+notation > "'Eq'≈" non associative with precedence 50 for
+ @{'eqrewrite}.
+
+interpretation "eq_rew" 'eqrewrite =
+ (cic:/matita/excedence/eq_trans.con _ _ _).
(* BUG: vedere se ricapita *)
alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con".
intro Xyz; apply Exy; apply unfold_apart; right; assumption;
qed.
+notation > "'Ex'≪" non associative with precedence 50 for
+ @{'excedencerewritel}.
+
+interpretation "exc_rewl" 'excedencerewritel =
+ (cic:/matita/excedence/exc_rewl.con _ _ _).
+
lemma le_rewr: ∀E:excedence.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
intro Xyz; apply Exy; apply unfold_apart; left; assumption;
qed.
+
+notation > "'Ex'≫" non associative with precedence 50 for
+ @{'excedencerewriter}.
+interpretation "exc_rewr" 'excedencerewriter =
+ (cic:/matita/excedence/exc_rewr.con _ _ _).
+
lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
cases (Exy (ap_symmetric ??? a));
lemma le_le_eq: ∀E:excedence.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
+qed.
+
+lemma ap_le_to_lt: ∀E:excedence.∀a,c:E.c # a → c ≤ a → c < a.
+intros; split; assumption;
qed.
\ No newline at end of file
theorem eq_opp_plus_plus_opp_opp:
∀G:abelian_group.∀x,y:G. -(x+y) ≈ -x + -y.
intros (G x y); apply (plus_cancr ??? (x+y));
-apply (eq_trans ?? 0 ? (opp_inverse ??));
-apply (eq_trans ?? (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))]
-apply (eq_trans ?? (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm]
-apply (eq_trans ?? (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;]
-apply (eq_trans ?? (-y + 0 + y));
+apply (Eq≈ 0 (opp_inverse ??));
+apply (Eq≈ (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))]
+apply (Eq≈ (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm]
+apply (Eq≈ (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;]
+apply (Eq≈ (-y + 0 + y));
[2: apply feq_plusr; apply feq_plusl; apply eq_sym; apply opp_inverse]
-apply (eq_trans ?? (-y + y));
+apply (Eq≈ (-y + y));
[2: apply feq_plusr; apply eq_sym;
- apply (eq_trans ?? (0+-y)); [apply plus_comm|apply zero_neutral]]
+ apply (Eq≈ (0+-y)); [apply plus_comm|apply zero_neutral]]
apply eq_sym; apply opp_inverse.
qed.
theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x.
intros (G x); apply (plus_cancl ??? (-x));
-apply (eq_trans ?? (--x + -x)); [apply plus_comm]
-apply (eq_trans ?? 0); [apply opp_inverse]
+apply (Eq≈ (--x + -x) (plus_comm ???));
+apply (Eq≈ 0 (opp_inverse ??));
apply eq_sym; apply opp_inverse;
qed.
theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption]
intro G; apply (plus_cancr ??? 0);
-apply (eq_trans ?? 0); [apply zero_neutral;]
+apply (Eq≈ 0); [apply zero_neutral;]
apply eq_sym; apply opp_inverse;
qed.
lemma feq_oppr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x ≈ -y → x ≈ -z.
intros (G x y z H1 H2); apply (plus_cancr ??? z);
-apply (eq_trans ?? 0 ?? (opp_inverse ?z));
-apply (eq_trans ?? (-y + z) ? H2);
-apply (eq_trans ?? (-y + y) ? H1);
-apply (eq_trans ?? 0 ? (opp_inverse ??));
+(* apply (eq_trans ??? 0 ? (opp_inverse ??)); *)
+apply (Eq≈ 0 ? (opp_inverse ??));
+apply (Eq≈ (-y + z) H2);
+apply (Eq≈ (-y + y) H1);
+apply (Eq≈ 0 (opp_inverse ??));
apply eq_reflexive;
qed.
assumption;
qed.
-(*
-lemma lt_to_dpos: ∀R.∀ml:mlattice R.∀x,y:ml.x < y → 0 < δ x y.
-intros 4; repeat (unfold in ⊢ (? % ? ?→?)); simplify; unfold excl;
-intro H; elim H (H1 H2); elim H2 (H3 H3); [cases (H1 H3)]
-split; [apply mpositive]
-*)
-
lemma meq_l: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δx y ≈ δz y.
intros (R ml x y z); apply le_le_eq;
[ apply (le_transitive ???? (mtineq ???y z));
intros; apply (eq_trans ???? (msymmetric ??y x));
apply (eq_trans ????? (msymmetric ??z y)); apply meq_l; assumption;
qed.
-
-lemma ap_le_to_lt: ∀O:ogroup.∀a,c:O.c # a → c ≤ a → c < a.
-intros (R a c A L); split; assumption;
-qed.
+
lemma dap_to_lt: ∀R.∀ml:mlattice R.∀x,y:ml. δ x y # 0 → 0 < δ x y.
intros; split [apply mpositive] apply ap_symmetric; assumption;
∀R.∀ml:mlattice R.∀x,y,z:ml. x ≤ y → y ≤ z → δ x z ≈ δ x y + δ y z.
intros (R ml x y z Lxy Lyz); apply le_le_eq; [apply mtineq]
apply (le_transitive ????? (ml_prop2 ?? ml (y) ??));
- cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
- apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
- lapply (le_to_eqm ??? Lxy) as Dxm;
- lapply (le_to_eqm ??? Lyz) as Dym;
- lapply (le_to_eqj ??? Lxy) as Dxj;
- lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy Lyz;
- apply (eq_trans ?? (δ(x∧y) y + δy z)); [apply feq_plusr; apply (meq_l ????? Dxm);]
- apply (eq_trans ?? (δ(x∧y) (y∧z) + δy z)); [apply feq_plusr; apply (meq_r ????? Dym);]
- apply (eq_trans ?? (δ(x∧y) (y∧z) + δ(x∨y) z)); [apply feq_plusl; apply (meq_l ????? Dxj);]
- apply (eq_trans ?? (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [apply feq_plusl; apply (meq_r ????? Dyj);]
- apply (eq_trans ?? ? ? (plus_comm ???));
- apply (eq_trans ?? (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z))); [apply feq_plusr; apply (meq_l ????? (join_comm ???));]
- apply feq_plusl;
- apply (eq_trans ?? (δ(y∧x) (y∧z))); [apply (meq_l ????? (meet_comm ???));]
- apply eq_reflexive;
+cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
+ apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
+lapply (le_to_eqm ??? Lxy) as Dxm; lapply (le_to_eqm ??? Lyz) as Dym;
+lapply (le_to_eqj ??? Lxy) as Dxj; lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy Lyz;
+apply (Eq≈ (δ(x∧y) y + δy z)); [apply feq_plusr; apply (meq_l ????? Dxm);]
+apply (Eq≈ (δ(x∧y) (y∧z) + δy z)); [apply feq_plusr; apply (meq_r ????? Dym);]
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z)); [apply feq_plusl; apply (meq_l ????? Dxj);]
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [apply feq_plusl; apply (meq_r ????? Dyj);]
+apply (Eq≈ ? (plus_comm ???));
+apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z))); [apply feq_plusr; apply (meq_l ????? (join_comm ???));]
+apply feq_plusl;
+apply (Eq≈ (δ(y∧x) (y∧z))); [apply (meq_l ????? (meet_comm ???));]
+apply eq_reflexive;
qed.
-
-
+(* 3.17 conclusione: δ x y ≈ 0 *)
+(* 3.20 conclusione: δ x y ≈ 0 *)
+(* 3.21 sup forte
+ strong_sup x ≝ ∀n. s n ≤ x ∧ ∀y x ≰ y → ∃n. s n ≰ y
+ strong_sup_zoli x ≝ ∀n. s n ≤ x ∧ ∄y. y#x ∧ y ≤ x
+*)
+(* 3.22 sup debole (più piccolo dei maggioranti) *)
+(* 3.23 conclusion: δ x sup(...) ≈ 0 *)
+(* 3.25 vero nel reticolo e basta (niente δ) *)
+(* 3.36 conclusion: δ x y ≈ 0 *)
\ No newline at end of file
μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).
intros (R L x y z H H1);
apply (plus_cancr ??? (μ(z∧x)));
-apply (eq_trans ?? (μz + μx) ? (modular_mjp ????));
-apply (eq_trans ?? (μz + μy) ? H); clear H;
-apply (eq_trans ?? (μ(z∨y) + μ(z∧y)) ? (modular_mjp ??z y));
+apply (Eq≈ (μz + μx) (modular_mjp ????));
+apply (Eq≈ (μz + μy) H); clear H;
+apply (Eq≈ (μ(z∨y) + μ(z∧y)) (modular_mjp ??z y));
apply (plus_cancl ??? (- μ (z ∨ y)));
-apply (eq_trans ?? ? ? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(z∧y)) ? (opp_inverse ??));
-apply (eq_trans ?? ? ? (zero_neutral ??));
-apply (eq_trans ?? (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ?? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(z∧x)) ?? (opp_inverse ??));
-apply (eq_trans ?? (μ (z ∧ x)) ?H1 (zero_neutral ??));
+apply (Eq≈ ? (plus_assoc ????));
+apply (Eq≈ (0+ μ(z∧y)) (opp_inverse ??));
+apply (Eq≈ ? (zero_neutral ??));
+apply (Eq≈ (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ? (plus_assoc ????));
+apply (Eq≈ (0+ μ(z∧x)) ? (opp_inverse ??));
+apply (Eq≈ (μ (z ∧ x)) H1 (zero_neutral ??));
qed.
lemma modularj: ∀R.∀L:wlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
intros (R L y z);
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) ?? (opp_inverse ??));
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+apply (Eq≈ ? H1); clear H1;
+apply (Eq≈ ?? (plus_assoc ????));
+apply (Eq≈ (μy+ μz + 0) ? (opp_inverse ??));
+apply (Eq≈ ?? (plus_comm ???));
+apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??)));
apply eq_reflexive.
qed.
intros (R L y z);
lapply (modular_mjp ?? y z) as H1;
apply (plus_cancl ??? (μ(y ∨ z)));
-apply (eq_trans ?? ? ? H1); clear H1;
-apply (eq_trans ????? (plus_comm ???));
-apply (eq_trans ?? ? ?? (plus_assoc ????));
-apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??));
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+apply (Eq≈ ? H1); clear H1;
+apply (Eq≈ ?? (plus_comm ???));
+apply (Eq≈ ?? (plus_assoc ????));
+apply (Eq≈ (μy+ μz + 0) ? (opp_inverse ??));
+apply (Eq≈ ?? (plus_comm ???));
+apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??)));
apply eq_reflexive.
qed.
lemma modularmj: ∀R.∀L:wlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
intros (R L x y z);
lapply (modular_mjp ?? x (y ∨ z)) as H1;
-apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ?? (feq_plusr ???? H1)); clear H1;
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ?? (plus_assoc ????));
-apply (eq_trans ?? (0+μ(x∧(y∨z))) ?? (opp_inverse ??));
-apply (eq_trans ?? (μ(x∧(y∨z))) ?? (zero_neutral ??));
+apply (Eq≈ (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ? (feq_plusr ???? H1)); clear H1;
+apply (Eq≈ ? ? (plus_comm ???));
+apply (Eq≈ (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ? (plus_assoc ????));
+apply (Eq≈ (0+μ(x∧(y∨z))) ? (opp_inverse ??));
+apply (Eq≈ (μ(x∧(y∨z))) ? (zero_neutral ??));
apply eq_reflexive.
qed.
lemma modularjm: ∀R.∀L:wlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))).
intros (R L x y z);
lapply (modular_mjp ?? x (y ∧ z)) as H1;
-apply (eq_trans ?? (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ?? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(x∨y∧z)) ?? (opp_inverse ??));
+apply (Eq≈ (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
+apply (Eq≈ ? ? (plus_comm ???));
+apply (Eq≈ (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ? (plus_assoc ????));
+apply (Eq≈ (0+ μ(x∨y∧z)) ? (opp_inverse ??));
apply eq_sym; apply zero_neutral;
qed.
lemma step1_3_57': ∀R.∀L:wlattice R.∀x,y,z:L.
μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)).
intros (R L x y z);
-apply (eq_trans ?? ? ? (modularjm ?? x y z));
-apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z))) ?); [
+apply (Eq≈ ? (modularjm ?? x y z));
+apply (Eq≈ ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z)))); [
apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);]
-apply (eq_trans ?? (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
+apply (Eq≈ (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
apply feq_plusl; apply feq_opp;
- apply (eq_trans ?? ? ? (meet_assoc ?????));
- apply (eq_trans ?? ? ? (meet_comm ????));
+ apply (Eq≈ ? (meet_assoc ?????));
+ apply (Eq≈ ? (meet_comm ????));
apply eq_reflexive;]
-apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
+apply feq_plusr; apply (Eq≈ ? (plus_assoc ????));
apply feq_plusr; apply plus_assoc;
qed.
lemma step1_3_57: ∀R.∀L:wlattice R.∀x,y,z:L.
μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
intros (R L x y z);
-apply (eq_trans ?? ? ? (modularmj ?? x y z));
-apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [
+apply (Eq≈ ? (modularmj ?? x y z));
+apply (Eq≈ ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z)))); [
apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);]
-apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
+apply (Eq≈ (μ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≈ ? (join_assoc ?????));
+ apply (Eq≈ ? (join_comm ????));
apply eq_reflexive;]
-apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
+apply feq_plusr; apply (Eq≈ ? (plus_assoc ????));
apply feq_plusr; apply plus_assoc;
qed.
apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [
apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm]
apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [
- apply feq_plusl; apply (eq_trans ?? (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [
+ apply feq_plusl; apply (Eq≈ (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [
apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [
- repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∧x)∨y)) ? (eq_opp_opp_x_x ??));
+ repeat apply feq_plusl; apply eq_sym; apply (Eq≈ (μ((z∧x)∨y)) (eq_opp_opp_x_x ??));
apply join_comm;]
apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [
apply eq_sym; apply plus_assoc;]
repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
- apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∨z))) ? (eq_sym ??? (plus_assoc ????)));
+ apply (Eq≈ ( μx+ μy+ μz+(- μy+- μ(y∨z))) (eq_sym ??? (plus_assoc ????)));
apply feq_plusl; apply plus_comm;]
apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
- apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
+ apply (Eq≈ (μx+ μy+( -μy+ μz)) (eq_sym ??? (plus_assoc ????)));
apply feq_plusl; apply plus_comm;]
apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [
apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj]
apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [
- apply feq_plusl; apply (eq_trans ?? (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [
+ apply feq_plusl; apply (Eq≈ (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [
apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [
- repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∨x)∧y)) ? (eq_opp_opp_x_x ??));
+ repeat apply feq_plusl; apply eq_sym; apply (Eq≈ (μ((z∨x)∧y)) (eq_opp_opp_x_x ??));
apply meet_comm;]
apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [
apply eq_sym; apply plus_assoc;]
repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
- apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∧z))) ? (eq_sym ??? (plus_assoc ????)));
+ apply (Eq≈ ( μx+ μy+ μz+(- μy+- μ(y∧z))) (eq_sym ??? (plus_assoc ????)));
apply feq_plusl; apply plus_comm;]
apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
- repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
- apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
+ repeat apply feq_plusr; apply (Eq≈ ?? (plus_assoc ????));
+ apply (Eq≈ (μx+ μy+( -μy+ μz)) (eq_sym ??? (plus_assoc ????)));
apply feq_plusl; apply plus_comm;]
apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
projects / helm.git / commitdiff