Implicative Group Axioms
Input Files and Proofs
These proofs were found by
Otter 3.0.4.
Abelian Group Axioms
x+y = z+u -> (y´+z)+u = x
- First proof (derive known equational axiom):
input, proof.
- Second proof (derive standard axioms):
input, proof.
x-y = z-u -> u-(z-x) = y
Group Axioms
(x·y)·z = (x·u)·w -> u·(w·z´) = y
- First proof (derive known equational axiom):
input, proof.
- Second proof (derive standard axioms):
input, proof.
x/y=z/u -> y/(((z/z)/z)/((x/x)/x))=u
Back to
Single Implicative Axioms for Groups and for Abelian Groups.