Beginning of Section AIM
Variable X : set
Variable m b s : set → set → set
Variable e : set
Variable K : set → set → set
Variable a : set → set → set → set
Variable T : set → set → set
Variable L R : set → set → set → set
Hypothesis He : e ∈ X
Hypothesis Hm : ∀x y ∈ X, m x y ∈ X
Hypothesis Hs : ∀x y ∈ X, s x y ∈ X
Hypothesis Hb : ∀x y ∈ X, b x y ∈ X
Hypothesis HKdef : ∀x y ∈ X, K x y = b (m y x) (m x y)
Hypothesis HK : ∀x y ∈ X, K x y ∈ X
Hypothesis Hadef : ∀x y z ∈ X, a x y z = b (m x (m y z)) (m (m x y) z)
Hypothesis Ha : ∀x y z ∈ X, a x y z ∈ X
Hypothesis HTdef : ∀u x ∈ X, T u x = b x (m u x)
Hypothesis HT : ∀u x ∈ X, T u x ∈ X
Hypothesis HLdef : ∀u x y ∈ X, L u x y = b (m y x) (m y (m x u))
Hypothesis HL : ∀u x y ∈ X, L u x y ∈ X
Hypothesis HRdef : ∀u x y ∈ X, R u x y = s (m (m u x) y) (m x y)
Hypothesis HR : ∀u x y ∈ X, R u x y ∈ X
Hypothesis HeL : ∀x ∈ X, m e x = x
Hypothesis HeR : ∀x ∈ X, m x e = x
Hypothesis Hbm : ∀x y ∈ X, b x (m x y) = y
Hypothesis Hmb : ∀x y ∈ X, m x (b x y) = y
Hypothesis Hsm : ∀x y ∈ X, s (m x y) y = x
Hypothesis Hms : ∀x y ∈ X, m (s x y) y = x
Hypothesis HTT : ∀u x y ∈ X, T (T u x) y = T (T u y) x
Hypothesis HTL : ∀u x y z ∈ X, T (L u x y) z = L (T u z) x y
Hypothesis HTR : ∀u x y z ∈ X, T (R u x y) z = R (T u z) x y
Hypothesis HLR : ∀u x y z w ∈ X, L (R u x y) z w = R (L u z w) x y
Hypothesis HLL : ∀u x y z w ∈ X, L (L u x y) z w = L (L u z w) x y
Hypothesis HRR : ∀u x y z w ∈ X, R (R u x y) z w = R (R u z w) x y
Theorem. (aK1)
∀x y z u ∈ X, a (K x y) z u = e
In Proofgold the corresponding term root is f0413a... and proposition id is 42fc46...
Proof:
The rest of the proof is missing.

Theorem. (aa1)
∀x y z u w ∈ X, a (a x y z) u w = e
In Proofgold the corresponding term root is 86bed2... and proposition id is eac1ec...
Proof:
The rest of the proof is missing.

Theorem. (com__aa1)
(∀x y ∈ X, m x y = m y x) → ∀x y z u w ∈ X, a (a x y z) u w = e
In Proofgold the corresponding term root is 6534c5... and proposition id is 975e10...
Proof:
The rest of the proof is missing.

Theorem. (middle_Bol__aa1)
(∀x y z ∈ X, m x (b (m y z) x) = m (s x z) (b y x)) → ∀x y z u w ∈ X, a (a x y z) u w = e
In Proofgold the corresponding term root is 547440... and proposition id is 79b0e8...
Proof:
The rest of the proof is missing.

Theorem. (KK_Kcom__aa1)
(∀x y z ∈ X, K (K x y) z = e) → (∀x y ∈ X, K x y = K y x) → ∀x y z u w ∈ X, a (a x y z) u w = e
In Proofgold the corresponding term root is 58773a... and proposition id is edea9f...
Proof:
The rest of the proof is missing.

Theorem. (T1dist__aa1)
(∀x y z ∈ X, m (T x y) (T z y) = T (m x z) y) → ∀x y z u w ∈ X, a (a x y z) u w = e
In Proofgold the corresponding term root is 128a2b... and proposition id is 6fb887...
Proof:
The rest of the proof is missing.

Theorem. (nil3_24)
∀x y z u w v5 v6 ∈ X, a (a (a x y z) u w) v5 v6 = e
In Proofgold the corresponding term root is 2d0c7b... and proposition id is 76b60f...
Proof:
The rest of the proof is missing.

Theorem. (com__nil3_24)
(∀x y ∈ X, m x y = m y x) → ∀x y z u w v5 v6 ∈ X, a (a (a x y z) u w) v5 v6 = e
In Proofgold the corresponding term root is fc3da9... and proposition id is 6793d3...
Proof:
The rest of the proof is missing.

Theorem. (aa1_45)
∀x y z u w ∈ X, a (a x y z) u w = a (a x y z) w u
In Proofgold the corresponding term root is 5271bc... and proposition id is 203c25...
Proof:
The rest of the proof is missing.

Theorem. (nil3_24__aa1)
(∀x y z u w v5 v6 ∈ X, a (a (a x y z) u w) v5 v6 = e) → ∀x y z u w ∈ X, a (a x y z) u w = e
In Proofgold the corresponding term root is 7dfd2b... and proposition id is bd8610...
Proof:
The rest of the proof is missing.

End of Section AIM