Beginning of Section AIM
(*** $I sig/PfgEAug2022Preamble.mgs ***)
L3
Variable X : set
L5
Variable m b s : set → set → set
L6
Variable e : set
L7
Variable K : set → set → set
L8
Variable a : set → set → set → set
L9
Variable T : set → set → set
L10
Variable L R : set → set → set → set
L11
Hypothesis He : e ∈ X
L13
Hypothesis Hm : ∀x y ∈ X, m x y ∈ X
L14
Hypothesis Hs : ∀x y ∈ X, s x y ∈ X
L15
Hypothesis Hb : ∀x y ∈ X, b x y ∈ X
L16
Hypothesis HKdef : ∀x y ∈ X, K x y = b (m y x) (m x y)
L17
Hypothesis HK : ∀x y ∈ X, K x y ∈ X
L18
Hypothesis Hadef : ∀x y z ∈ X, a x y z = b (m x (m y z)) (m (m x y) z)
L19
Hypothesis Ha : ∀x y z ∈ X, a x y z ∈ X
L20
Hypothesis HTdef : ∀u x ∈ X, T u x = b x (m u x)
L21
Hypothesis HT : ∀u x ∈ X, T u x ∈ X
L22
Hypothesis HLdef : ∀u x y ∈ X, L u x y = b (m y x) (m y (m x u))
L23
Hypothesis HL : ∀u x y ∈ X, L u x y ∈ X
L24
Hypothesis HRdef : ∀u x y ∈ X, R u x y = s (m (m u x) y) (m x y)
L25
Hypothesis HR : ∀u x y ∈ X, R u x y ∈ X
L26
Hypothesis HeL : ∀x ∈ X, m e x = x
L27
Hypothesis HeR : ∀x ∈ X, m x e = x
L28
Hypothesis Hbm : ∀x y ∈ X, b x (m x y) = y
L29
Hypothesis Hmb : ∀x y ∈ X, m x (b x y) = y
L30
Hypothesis Hsm : ∀x y ∈ X, s (m x y) y = x
L31
Hypothesis Hms : ∀x y ∈ X, m (s x y) y = x
L32
Hypothesis HTT : ∀u x y ∈ X, T (T u x) y = T (T u y) x
L33
Hypothesis HTL : ∀u x y z ∈ X, T (L u x y) z = L (T u z) x y
L34
Hypothesis HTR : ∀u x y z ∈ X, T (R u x y) z = R (T u z) x y
L35
Hypothesis HLR : ∀u x y z w ∈ X, L (R u x y) z w = R (L u z w) x y
L36
Hypothesis HLL : ∀u x y z w ∈ X, L (L u x y) z w = L (L u z w) x y
L37
Hypothesis HRR : ∀u x y z w ∈ X, R (R u x y) z w = R (R u z w) x y
L38
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:
Proof not loaded.
L41
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:
Proof not loaded.
L44
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:
Proof not loaded.
L48
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:
Proof not loaded.
L52
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:
Proof not loaded.
L57
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:
Proof not loaded.
L61
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:
Proof not loaded.
L64
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:
Proof not loaded.
L68
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:
Proof not loaded.
L71
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:
Proof not loaded.
End of Section AIM