(def-language group-language (base-types gg) (constants (e"gg") (mul"[gg,gg,gg]") (inv"[gg,gg]")))

(def-theory groupsRemark: This entry is multiply defined. See: [1] [2](language group-language) (component-theories h-o-real-arithmetic) (axioms (left-mul-id"forall(x:gg, e mul x = x)"rewrite) (right-mul-id"forall(x:gg, x mul e = x)"rewrite) (left-mul-inv"forall(x:gg, inv(x) mul x = e)"rewrite) (right-mul-inv"forall(x:gg, x mul inv(x) = e)"rewrite) (mul-associativity"forall(x,y,z:gg, (x mul y) mul z = x mul (y mul z))"rewrite)))

(def-quasi-constructor group"lambda(gg%:sets[gg], mul%:[gg,gg,gg], e%:gg, inv%:[gg,gg], forall(x,y:gg, x in gg% and y in gg% implies mul%(x,y) in gg%) and e% in gg% and forall(x:gg, x in gg% implies inv%(x) in gg%) and forall(x:gg, x in gg% implies mul%(e%,x)=x) and forall(x:gg, x in gg% implies mul%(x,e%)=x) and forall(x:gg, x in gg% implies mul%(inv%(x),x)=e%) and forall(x:gg, x in gg% implies mul%(x,inv%(x))=e%) and forall(x,y,z:gg, ((x in gg%) and (y in gg%) and (z in gg%)) implies mul%(mul%(x,y),z) = mul%(x,mul%(y,z))))"(language groups))

(def-theorem mul-is-total"total_q{mul,[gg,gg,gg]}"(theory groups) (usages d-r-convergence transportable-macete) (proof ( insistent-direct-inference (instantiate-theorem mul-associativity ("x_0""x_1""x_1")) )))

(def-theorem inv-is-totalRemark: This entry is multiply defined. See: [1] [2]"total_q{inv,[gg,gg]}"(theory groups) (usages d-r-convergence transportable-macete) (proof ( insistent-direct-inference (instantiate-theorem left-mul-inv ("x_0")) )))

(def-theorem reverse-mul-associativity"forall(x,y,z:gg, x mul (y mul z) = (x mul y) mul z)"(theory groups) (usages transportable-macete) (proof (simplify)))

(def-theorem left-inv-cancellation"forall(x,y:gg, inv(x) mul (x mul y) = y)"(theory groups) (usages rewrite transportable-macete) (proof ( (apply-macete-with-minor-premises reverse-mul-associativity) (apply-macete-with-minor-premises left-mul-inv) simplify )))

(def-theorem right-inv-cancellation"forall(x,y:gg, x mul (inv(x) mul y) = y)"(theory groups) (usages rewrite transportable-macete) (proof ;; obtained by editing the previous proof script ( (apply-macete-with-minor-premises reverse-mul-associativity) (apply-macete-with-minor-premises right-mul-inv) simplify )))

(def-script inv-cancellation-script 1 ( (apply-macete-with-minor-premises reverse-mul-associativity) (apply-macete-with-minor-premises $1) simplify ))

(def-theorem inv-of-e"inv(e)=e"(theory groups) (usages rewrite transportable-macete) (proof ( (instantiate-theorem left-mul-id ("inv(e)")) (force-substitution"inv(e)""e mul inv(e)"(0)) simplify )))

(def-theorem inv-of-inv"forall(x:gg, inv(inv(x))=x)"(theory groups) (usages rewrite transportable-macete) (proof ( (instantiate-theorem mul-associativity ("inv(inv(x))""inv(x)""x")) (contrapose"with(p:prop,p)") (force-substitution"inv(inv(x)) mul inv(x)""e"(0)) (force-substitution"inv(x) mul x""e"(0)) simplify simplify simplify )))

(def-theorem push-inv"forall(g,h:gg, inv(g mul h) = inv(h) mul inv(g))"(theory groups) (usages rewrite transportable-macete) (proof ( (instantiate-theorem mul-associativity ("inv(g mul h)""g mul h""inv(h) mul inv(g)")) (contrapose"with(p:prop,p)") (force-substitution"inv(g mul h) mul (g mul h)""e"(0)) (force-substitution"(g mul h) mul (inv(h) mul inv(g))""e"(0)) simplify simplify simplify )))

(def-translation mul-reverse (source groups) (target groups) (fixed-theories h-o-real-arithmetic) (constant-pairs (mul"lambda(x,y:gg, y mul x)")) force-under-quick-load (theory-interpretation-check using-simplification))

(def-theorem left-cancellation-law"forall(x,y,z:gg, x mul y = x mul z iff y=z)"(theory groups) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem mul-associativity ("inv(x)""x""y")) (contrapose"with(y,x:gg,(inv(x) mul x) mul y=inv(x) mul (x mul y))") (force-substitution"x mul y""x mul z"(0)) (apply-macete-with-minor-premises mul-associativity) (apply-macete-with-minor-premises left-inv-cancellation) )))

(def-theorem left-trivial-cancellation-law-left"forall(x,y:gg, x = x mul y iff e=y)"(theory groups) (usages transportable-macete) (proof ( (instantiate-theorem left-cancellation-law ("x""e""y")) simplify simplify (contrapose"with(y,x:gg,not(x mul e=x mul y))") simplify )))

(def-theorem left-trivial-cancellation-law-right"forall(x,y:gg, x mul y = x iff y=e)"(theory groups) (usages transportable-macete) (proof ( (instantiate-theorem left-trivial-cancellation-law-left ("x""y")) simplify simplify )))

(def-theorem right-cancellation-law left-cancellation-law (theory groups) (usages transportable-macete) (translation mul-reverse) (proof existing-theorem))

(def-theorem right-trivial-cancellation-law-left left-trivial-cancellation-law-left (theory groups) (usages transportable-macete) (translation mul-reverse) (proof existing-theorem))

(def-theorem right-trivial-cancellation-law-right left-trivial-cancellation-law-right (theory groups) (usages transportable-macete) (translation mul-reverse) (proof existing-theorem))

(def-compound-macete group-cancellation-laws (series (repeat mul-associativity) (repeat left-cancellation-law) left-trivial-cancellation-law-left left-trivial-cancellation-law-right (repeat reverse-mul-associativity) (repeat right-cancellation-law) right-trivial-cancellation-law-left right-trivial-cancellation-law-right))