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

(def-theory groups 
  Remark: 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-total 
  Remark: 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))