Beginning of Section Conj_mul_SNo_assoc_lem1__26__21

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g x y + g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__26__21)

SNo (g (g x y + g u x2) y2) → w < g (g x y) z

In Proofgold the corresponding term root is 5821fa... and proposition id is bb8dfc...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__26__21

Beginning of Section Conj_mul_SNo_assoc_lem1__27__27

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Hypothesis H30 : SNo (g x y + g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__27__27)

SNo (g (g u y + g x x2) y2) → w < g (g x y) z

In Proofgold the corresponding term root is 48f51a... and proposition id is e7121f...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__27__27

Beginning of Section Conj_mul_SNo_assoc_lem1__27__30

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Theorem. (Conj_mul_SNo_assoc_lem1__27__30)

SNo (g (g u y + g x x2) y2) → w < g (g x y) z

In Proofgold the corresponding term root is c6f350... and proposition id is abd44a...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__27__30

Beginning of Section Conj_mul_SNo_assoc_lem1__28__4

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Hypothesis H30 : SNo (g x y + g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__28__4)

SNo (g (g x y + g u x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is 7f288d... and proposition id is c230ba...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__28__4

Beginning of Section Conj_mul_SNo_assoc_lem1__28__7

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Hypothesis H30 : SNo (g x y + g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__28__7)

SNo (g (g x y + g u x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is bfaa45... and proposition id is a597a0...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__28__7

Beginning of Section Conj_mul_SNo_assoc_lem1__28__8

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Hypothesis H30 : SNo (g x y + g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__28__8)

SNo (g (g x y + g u x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is 2234a6... and proposition id is 2c6af1...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__28__8

Beginning of Section Conj_mul_SNo_assoc_lem1__28__22

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Hypothesis H30 : SNo (g x y + g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__28__22)

SNo (g (g x y + g u x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is 0d0563... and proposition id is 541ead...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__28__22

Beginning of Section Conj_mul_SNo_assoc_lem1__28__27

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Hypothesis H30 : SNo (g x y + g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__28__27)

SNo (g (g x y + g u x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is ef4b3a... and proposition id is a9a00f...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__28__27

Beginning of Section Conj_mul_SNo_assoc_lem1__28__30

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Theorem. (Conj_mul_SNo_assoc_lem1__28__30)

SNo (g (g x y + g u x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is 36422c... and proposition id is 8b6e3b...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__28__30

Beginning of Section Conj_mul_SNo_assoc_lem1__29__14

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Hypothesis H30 : SNo (g x y + g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__29__14)

SNo (g (g u y + g x x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is fec08d... and proposition id is 7a69fe...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__29__14

Beginning of Section Conj_mul_SNo_assoc_lem1__30__0

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Theorem. (Conj_mul_SNo_assoc_lem1__30__0)

SNo (g x y + g u x2) → w < g (g x y) z

In Proofgold the corresponding term root is 045849... and proposition id is 7cf689...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__30__0

Beginning of Section Conj_mul_SNo_assoc_lem1__30__4

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Hypothesis H29 : SNo (g u y + g x x2)

Theorem. (Conj_mul_SNo_assoc_lem1__30__4)

SNo (g x y + g u x2) → w < g (g x y) z

In Proofgold the corresponding term root is 292c9c... and proposition id is 633da2...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__30__4

Beginning of Section Conj_mul_SNo_assoc_lem1__31__23

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__31__23)

SNo (g u y + g x x2) → w < g (g x y) z

In Proofgold the corresponding term root is d92b1d... and proposition id is 1531d7...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__31__23

Beginning of Section Conj_mul_SNo_assoc_lem1__31__27

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g x (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__31__27)

SNo (g u y + g x x2) → w < g (g x y) z

In Proofgold the corresponding term root is 978465... and proposition id is 8ca155...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__31__27

Beginning of Section Conj_mul_SNo_assoc_lem1__33__4

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Hypothesis H29 : SNo (g u (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__33__4)

SNo (g u v + g u (g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is c4bfe6... and proposition id is 6d2973...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__33__4

Beginning of Section Conj_mul_SNo_assoc_lem1__33__24

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Hypothesis H29 : SNo (g u (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__33__24)

SNo (g u v + g u (g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is f5211b... and proposition id is c257bf...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__33__24

Beginning of Section Conj_mul_SNo_assoc_lem1__34__8

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__34__8)

SNo (g u (g x2 z + g y y2)) → w < g (g x y) z

In Proofgold the corresponding term root is a4ad9e... and proposition id is 9eb95d...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__34__8

Beginning of Section Conj_mul_SNo_assoc_lem1__34__9

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__34__9)

SNo (g u (g x2 z + g y y2)) → w < g (g x y) z

In Proofgold the corresponding term root is ebdbd6... and proposition id is 45d75f...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__34__9

Beginning of Section Conj_mul_SNo_assoc_lem1__35__4

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Hypothesis H26 : SNo (v + g x2 y2)

Hypothesis H27 : SNo (g x (v + g x2 y2))

Hypothesis H28 : SNo (g u (v + g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__35__4)

SNo (g u (g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is fb9f35... and proposition id is 1fb085...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__35__4

Beginning of Section Conj_mul_SNo_assoc_lem1__36__3

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Hypothesis H26 : SNo (v + g x2 y2)

Hypothesis H27 : SNo (g x (v + g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__36__3)

SNo (g u (v + g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 0c2c0b... and proposition id is e08854...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__36__3

Beginning of Section Conj_mul_SNo_assoc_lem1__36__11

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Hypothesis H26 : SNo (v + g x2 y2)

Hypothesis H27 : SNo (g x (v + g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__36__11)

SNo (g u (v + g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is bdc4a6... and proposition id is f5488c...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__36__11

Beginning of Section Conj_mul_SNo_assoc_lem1__36__23

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Hypothesis H26 : SNo (v + g x2 y2)

Hypothesis H27 : SNo (g x (v + g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__36__23)

SNo (g u (v + g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is a029ae... and proposition id is 2855e8...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__36__23

Beginning of Section Conj_mul_SNo_assoc_lem1__36__27

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Hypothesis H26 : SNo (v + g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__36__27)

SNo (g u (v + g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 6eb7dd... and proposition id is a6d6fb...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__36__27

Beginning of Section Conj_mul_SNo_assoc_lem1__37__11

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Hypothesis H26 : SNo (v + g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__37__11)

SNo (g x (v + g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 1aa07c... and proposition id is 0c790e...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__37__11

Beginning of Section Conj_mul_SNo_assoc_lem1__38__11

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__38__11)

SNo (v + g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 7b7b12... and proposition id is c92dd4...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__38__11

Beginning of Section Conj_mul_SNo_assoc_lem1__38__13

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__38__13)

SNo (v + g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 2fc98b... and proposition id is ba3bd3...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__38__13

Beginning of Section Conj_mul_SNo_assoc_lem1__40__19

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z)

Hypothesis H25 : SNo (g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__40__19)

SNo (g x2 z + g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is be48c1... and proposition id is ee6363...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__40__19

Beginning of Section Conj_mul_SNo_assoc_lem1__40__25

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z)

Theorem. (Conj_mul_SNo_assoc_lem1__40__25)

SNo (g x2 z + g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is d17bb2... and proposition id is c394a2...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__40__25

Beginning of Section Conj_mul_SNo_assoc_lem1__41__17

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z)

Theorem. (Conj_mul_SNo_assoc_lem1__41__17)

SNo (g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is cea3ef... and proposition id is 130018...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__41__17

Beginning of Section Conj_mul_SNo_assoc_lem1__43__3

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__43__3)

SNo (g x x2) → w < g (g x y) z

In Proofgold the corresponding term root is c15325... and proposition id is 361f69...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__43__3

Beginning of Section Conj_mul_SNo_assoc_lem1__43__6

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H19 : SNo y2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__43__6)

SNo (g x x2) → w < g (g x y) z

In Proofgold the corresponding term root is e0a2d1... and proposition id is fa1c3b...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__43__6

Beginning of Section Conj_mul_SNo_assoc_lem1__43__19

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoR y

Hypothesis H15 : y2 ∈ SNoL z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : y < x2

Hypothesis H20 : y2 < z

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__43__19)

SNo (g x x2) → w < g (g x y) z

In Proofgold the corresponding term root is 3fa025... and proposition id is b44bb1...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__43__19

Beginning of Section Conj_mul_SNo_assoc_lem1__46__0

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H7 : u ∈ SNoR x

Hypothesis H8 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H9 : SNo u

Hypothesis H10 : x < u

Hypothesis H11 : SNo v

Hypothesis H12 : x2 ∈ SNoL y

Hypothesis H13 : y2 ∈ SNoR z

Hypothesis H14 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H15 : SNo x2

Hypothesis H16 : x2 < y

Hypothesis H17 : SNo y2

Hypothesis H18 : z < y2

Hypothesis H19 : SNo (g x2 z + g y y2)

Hypothesis H20 : SNo (v + g x2 y2)

Hypothesis H21 : SNo (g x (v + g x2 y2))

Hypothesis H22 : SNo (g u (v + g x2 y2))

Hypothesis H23 : SNo (g u (g x2 z + g y y2))

Hypothesis H24 : SNo (g x (g x2 z + g y y2))

Hypothesis H25 : SNo (g u y + g x x2)

Hypothesis H26 : SNo (g x y + g u x2)

Hypothesis H27 : SNo (g (g u y + g x x2) z)

Hypothesis H28 : SNo (g (g x y + g u x2) z)

Hypothesis H29 : SNo (g (g u y + g x x2) y2)

Theorem. (Conj_mul_SNo_assoc_lem1__46__0)

SNo (g (g x y + g u x2) y2) → w < g (g x y) z

In Proofgold the corresponding term root is 1cc964... and proposition id is f39a11...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__46__0

Beginning of Section Conj_mul_SNo_assoc_lem1__47__5

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H6 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H7 : u ∈ SNoR x

Hypothesis H8 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H9 : SNo u

Hypothesis H10 : x < u

Hypothesis H11 : SNo v

Hypothesis H12 : x2 ∈ SNoL y

Hypothesis H13 : y2 ∈ SNoR z

Hypothesis H14 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H15 : SNo x2

Hypothesis H16 : x2 < y

Hypothesis H17 : SNo y2

Hypothesis H18 : z < y2

Hypothesis H19 : SNo (g x2 z + g y y2)

Hypothesis H20 : SNo (v + g x2 y2)

Hypothesis H21 : SNo (g x (v + g x2 y2))

Hypothesis H22 : SNo (g u (v + g x2 y2))

Hypothesis H23 : SNo (g u (g x2 z + g y y2))

Hypothesis H24 : SNo (g x (g x2 z + g y y2))

Hypothesis H25 : SNo (g u y + g x x2)

Hypothesis H26 : SNo (g x y + g u x2)

Hypothesis H27 : SNo (g (g u y + g x x2) z)

Hypothesis H28 : SNo (g (g x y + g u x2) z)

Theorem. (Conj_mul_SNo_assoc_lem1__47__5)

SNo (g (g u y + g x x2) y2) → w < g (g x y) z

In Proofgold the corresponding term root is 934560... and proposition id is 4a86ce...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__47__5

Beginning of Section Conj_mul_SNo_assoc_lem1__48__1

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H7 : u ∈ SNoR x

Hypothesis H8 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H9 : SNo u

Hypothesis H10 : x < u

Hypothesis H11 : SNo v

Hypothesis H12 : x2 ∈ SNoL y

Hypothesis H13 : y2 ∈ SNoR z

Hypothesis H14 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H15 : SNo x2

Hypothesis H16 : x2 < y

Hypothesis H17 : SNo y2

Hypothesis H18 : z < y2

Hypothesis H19 : SNo (g x2 z + g y y2)

Hypothesis H20 : SNo (v + g x2 y2)

Hypothesis H21 : SNo (g x (v + g x2 y2))

Hypothesis H22 : SNo (g u (v + g x2 y2))

Hypothesis H23 : SNo (g u (g x2 z + g y y2))

Hypothesis H24 : SNo (g x (g x2 z + g y y2))

Hypothesis H25 : SNo (g u y + g x x2)

Hypothesis H26 : SNo (g x y + g u x2)

Hypothesis H27 : SNo (g (g u y + g x x2) z)

Theorem. (Conj_mul_SNo_assoc_lem1__48__1)

SNo (g (g x y + g u x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is e6b7c0... and proposition id is c331ef...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__48__1

Beginning of Section Conj_mul_SNo_assoc_lem1__48__22

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H7 : u ∈ SNoR x

Hypothesis H8 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H9 : SNo u

Hypothesis H10 : x < u

Hypothesis H11 : SNo v

Hypothesis H12 : x2 ∈ SNoL y

Hypothesis H13 : y2 ∈ SNoR z

Hypothesis H14 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H15 : SNo x2

Hypothesis H16 : x2 < y

Hypothesis H17 : SNo y2

Hypothesis H18 : z < y2

Hypothesis H19 : SNo (g x2 z + g y y2)

Hypothesis H20 : SNo (v + g x2 y2)

Hypothesis H21 : SNo (g x (v + g x2 y2))

Hypothesis H23 : SNo (g u (g x2 z + g y y2))

Hypothesis H24 : SNo (g x (g x2 z + g y y2))

Hypothesis H25 : SNo (g u y + g x x2)

Hypothesis H26 : SNo (g x y + g u x2)

Hypothesis H27 : SNo (g (g u y + g x x2) z)

Theorem. (Conj_mul_SNo_assoc_lem1__48__22)

SNo (g (g x y + g u x2) z) → w < g (g x y) z

In Proofgold the corresponding term root is 9bf01f... and proposition id is 2eb556...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__48__22

Beginning of Section Conj_mul_SNo_assoc_lem1__50__11

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u x2)

Hypothesis H21 : SNo (g x2 z + g y y2)

Hypothesis H22 : SNo (v + g x2 y2)

Hypothesis H23 : SNo (g x (v + g x2 y2))

Hypothesis H24 : SNo (g u (v + g x2 y2))

Hypothesis H25 : SNo (g u (g x2 z + g y y2))

Hypothesis H26 : SNo (g x (g x2 z + g y y2))

Hypothesis H27 : SNo (g u y + g x x2)

Theorem. (Conj_mul_SNo_assoc_lem1__50__11)

SNo (g x y + g u x2) → w < g (g x y) z

In Proofgold the corresponding term root is 1141e6... and proposition id is 2e775e...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__50__11

Beginning of Section Conj_mul_SNo_assoc_lem1__52__3

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__52__3)

SNo (g x (g x2 z + g y y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 8891dc... and proposition id is 976c93...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__52__3

Beginning of Section Conj_mul_SNo_assoc_lem1__52__10

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H25 : SNo (g x (v + g x2 y2))

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__52__10)

SNo (g x (g x2 z + g y y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 358d81... and proposition id is 9c7fb3...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__52__10

Beginning of Section Conj_mul_SNo_assoc_lem1__52__25

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g u (v + g x2 y2))

Hypothesis H27 : SNo (g u (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__52__25)

SNo (g x (g x2 z + g y y2)) → w < g (g x y) z

In Proofgold the corresponding term root is c9ac54... and proposition id is 6cf6f3...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__52__25

Beginning of Section Conj_mul_SNo_assoc_lem1__53__6

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Hypothesis H29 : SNo (g u (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__53__6)

SNo (g u v + g u (g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 587546... and proposition id is 9ae5ea...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__53__6

Beginning of Section Conj_mul_SNo_assoc_lem1__53__23

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Hypothesis H29 : SNo (g u (g x2 z + g y y2))

Theorem. (Conj_mul_SNo_assoc_lem1__53__23)

SNo (g u v + g u (g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is a2730d... and proposition id is 3d0157...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__53__23

Beginning of Section Conj_mul_SNo_assoc_lem1__54__13

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__54__13)

SNo (g u (g x2 z + g y y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 61284d... and proposition id is 885e11...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__54__13

Beginning of Section Conj_mul_SNo_assoc_lem1__54__20

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__54__20)

SNo (g u (g x2 z + g y y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 7274ec... and proposition id is aed699...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__54__20

Beginning of Section Conj_mul_SNo_assoc_lem1__54__23

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (v + g x2 y2)

Hypothesis H26 : SNo (g x (v + g x2 y2))

Hypothesis H27 : SNo (g u (v + g x2 y2))

Hypothesis H28 : SNo (g u (g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__54__23)

SNo (g u (g x2 z + g y y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 00273c... and proposition id is 2770ad...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__54__23

Beginning of Section Conj_mul_SNo_assoc_lem1__55__8

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Hypothesis H26 : SNo (v + g x2 y2)

Hypothesis H27 : SNo (g x (v + g x2 y2))

Hypothesis H28 : SNo (g u (v + g x2 y2))

Theorem. (Conj_mul_SNo_assoc_lem1__55__8)

SNo (g u (g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 77236f... and proposition id is 9d009c...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__55__8

Beginning of Section Conj_mul_SNo_assoc_lem1__57__15

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Hypothesis H26 : SNo (v + g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__57__15)

SNo (g x (v + g x2 y2)) → w < g (g x y) z

In Proofgold the corresponding term root is 068121... and proposition id is c4280e...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__57__15

Beginning of Section Conj_mul_SNo_assoc_lem1__58__7

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__58__7)

SNo (v + g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 4f2880... and proposition id is 44e496...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__58__7

Beginning of Section Conj_mul_SNo_assoc_lem1__58__9

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Hypothesis H25 : SNo (g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__58__9)

SNo (v + g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 88217e... and proposition id is c9dbcf...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__58__9

Beginning of Section Conj_mul_SNo_assoc_lem1__59__2

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__59__2)

SNo (g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 57f44f... and proposition id is f6aaf0...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__59__2

Beginning of Section Conj_mul_SNo_assoc_lem1__59__7

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__59__7)

SNo (g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 4b416f... and proposition id is f0df65...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__59__7

Beginning of Section Conj_mul_SNo_assoc_lem1__59__18

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z + g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__59__18)

SNo (g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is c3fad3... and proposition id is dda03d...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__59__18

Beginning of Section Conj_mul_SNo_assoc_lem1__60__6

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z)

Hypothesis H25 : SNo (g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__60__6)

SNo (g x2 z + g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 0407e3... and proposition id is 9faafb...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__60__6

Beginning of Section Conj_mul_SNo_assoc_lem1__61__1

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Hypothesis H24 : SNo (g x2 z)

Theorem. (Conj_mul_SNo_assoc_lem1__61__1)

SNo (g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 6db43e... and proposition id is 71aabd...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__61__1

Beginning of Section Conj_mul_SNo_assoc_lem1__62__1

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Hypothesis H22 : SNo (g u x2)

Hypothesis H23 : SNo (g x x2)

Theorem. (Conj_mul_SNo_assoc_lem1__62__1)

SNo (g x2 z) → w < g (g x y) z

In Proofgold the corresponding term root is 34b54d... and proposition id is cd6d07...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__62__1

Beginning of Section Conj_mul_SNo_assoc_lem1__64__15

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Hypothesis H21 : SNo (g u y)

Theorem. (Conj_mul_SNo_assoc_lem1__64__15)

SNo (g u x2) → w < g (g x y) z

In Proofgold the corresponding term root is 57f9d0... and proposition id is dd89cc...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__64__15

Beginning of Section Conj_mul_SNo_assoc_lem1__65__9

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoR x

Hypothesis H10 : SNo u

Hypothesis H11 : x < u

Hypothesis H12 : SNo v

Hypothesis H13 : SNo (g u v)

Hypothesis H14 : x2 ∈ SNoL y

Hypothesis H15 : y2 ∈ SNoR z

Hypothesis H16 : (g x2 z + g y y2) ≤ v + g x2 y2

Hypothesis H17 : SNo x2

Hypothesis H18 : x2 < y

Hypothesis H19 : SNo y2

Hypothesis H20 : z < y2

Theorem. (Conj_mul_SNo_assoc_lem1__65__9)

SNo (g u y) → w < g (g x y) z

In Proofgold the corresponding term root is 2fa438... and proposition id is 8160b3...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__65__9

Beginning of Section Conj_mul_SNo_assoc_lem1__67__4

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → SNo (g x2 y2))

Hypothesis H1 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → (∀z2 : set, z2 ∈ SNoR (g x2 y2) → (∀P : prop, (∀w2 : set, w2 ∈ SNoL x2 → (∀u2 : set, u2 ∈ SNoR y2 → (g w2 y2 + g x2 u2) ≤ z2 + g w2 u2 → P)) → (∀w2 : set, w2 ∈ SNoR x2 → (∀u2 : set, u2 ∈ SNoL y2 → (g w2 y2 + g x2 u2) ≤ z2 + g w2 u2 → P)) → P)))

Hypothesis H2 : (∀x2 : set, ∀y2 : set, ∀z2 : set, ∀w2 : set, SNo x2 → SNo y2 → SNo z2 → SNo w2 → z2 < x2 → w2 < y2 → (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2)

Hypothesis H3 : (∀x2 : set, ∀y2 : set, ∀z2 : set, ∀w2 : set, SNo x2 → SNo y2 → SNo z2 → SNo w2 → z2 ≤ x2 → w2 ≤ y2 → (g z2 y2 + g x2 w2) ≤ g x2 y2 + g z2 w2)

Hypothesis H5 : SNo y

Hypothesis H6 : SNo z

Hypothesis H7 : SNo (g x y)

Hypothesis H8 : SNo (g y z)

Hypothesis H9 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev x) → (∀y2 : set, SNo y2 → (∀z2 : set, z2 ∈ SNoS_ (SNoLev y) → (∀w2 : set, w2 ∈ SNoS_ (SNoLev z) → w = g x2 (g y z) + g x y2 + - (g x2 y2) → (g x2 (g z2 z + g y w2) + g x (y2 + g z2 w2)) ≤ g x (g z2 z + g y w2) + g x2 (y2 + g z2 w2) → (g (g x2 y + g x z2) z + g (g x y + g x2 z2) w2) < g (g x y + g x2 z2) z + g (g x2 y + g x z2) w2 → w < g (g x y) z))))

Hypothesis H10 : u ∈ SNoR x

Hypothesis H11 : v ∈ SNoR (g y z)

Hypothesis H12 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H13 : SNo u

Hypothesis H14 : x < u

Theorem. (Conj_mul_SNo_assoc_lem1__67__4)

SNo v → w < g (g x y) z

In Proofgold the corresponding term root is 8613cc... and proposition id is 0fff95...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__67__4

Beginning of Section Conj_mul_SNo_assoc_lem1__70__6

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → SNo (g x2 y2))

Hypothesis H1 : (∀x2 : set, ∀y2 : set, ∀z2 : set, ∀w2 : set, SNo x2 → SNo y2 → SNo z2 → SNo w2 → z2 < x2 → w2 < y2 → (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2)

Hypothesis H2 : SNo x

Hypothesis H3 : SNo y

Hypothesis H4 : SNo z

Hypothesis H5 : SNo (g x y)

Hypothesis H7 : w < x

Hypothesis H8 : SNo u

Hypothesis H9 : y < u

Hypothesis H10 : SNo v

Hypothesis H11 : z < v

Hypothesis H12 : SNo (g w y)

Hypothesis H13 : SNo (g w u)

Hypothesis H14 : SNo (g x u)

Hypothesis H15 : SNo (g w y + g x u)

Hypothesis H16 : SNo (g x y + g w u)

Hypothesis H17 : SNo (g (g w y + g x u) z)

Theorem. (Conj_mul_SNo_assoc_lem1__70__6)

SNo (g (g x y + g w u) z) → (g (g w y + g x u) z + g (g x y + g w u) v) < g (g x y + g w u) z + g (g w y + g x u) v

In Proofgold the corresponding term root is cfa8f6... and proposition id is 740991...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__70__6

Beginning of Section Conj_mul_SNo_assoc_lem1__72__7

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → SNo (g x2 y2))

Hypothesis H1 : (∀x2 : set, ∀y2 : set, ∀z2 : set, ∀w2 : set, SNo x2 → SNo y2 → SNo z2 → SNo w2 → z2 < x2 → w2 < y2 → (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2)

Hypothesis H2 : SNo x

Hypothesis H3 : SNo y

Hypothesis H4 : SNo z

Hypothesis H5 : SNo (g x y)

Hypothesis H6 : SNo w

Hypothesis H8 : SNo u

Hypothesis H9 : y < u

Hypothesis H10 : SNo v

Hypothesis H11 : z < v

Hypothesis H12 : SNo (g w y)

Hypothesis H13 : SNo (g w u)

Hypothesis H14 : SNo (g x u)

Hypothesis H15 : SNo (g w y + g x u)

Theorem. (Conj_mul_SNo_assoc_lem1__72__7)

SNo (g x y + g w u) → (g (g w y + g x u) z + g (g x y + g w u) v) < g (g x y + g w u) z + g (g w y + g x u) v

In Proofgold the corresponding term root is 12a983... and proposition id is 8783fd...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__72__7

Beginning of Section Conj_mul_SNo_assoc_lem1__73__3

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → SNo (g x2 y2))

Hypothesis H1 : (∀x2 : set, ∀y2 : set, ∀z2 : set, ∀w2 : set, SNo x2 → SNo y2 → SNo z2 → SNo w2 → z2 < x2 → w2 < y2 → (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2)

Hypothesis H2 : SNo x

Hypothesis H4 : SNo z

Hypothesis H5 : SNo (g x y)

Hypothesis H6 : SNo w

Hypothesis H7 : w < x

Hypothesis H8 : SNo u

Hypothesis H9 : y < u

Hypothesis H10 : SNo v

Hypothesis H11 : z < v

Hypothesis H12 : SNo (g w y)

Hypothesis H13 : SNo (g w u)

Hypothesis H14 : SNo (g x u)

Theorem. (Conj_mul_SNo_assoc_lem1__73__3)

SNo (g w y + g x u) → (g (g w y + g x u) z + g (g x y + g w u) v) < g (g x y + g w u) z + g (g w y + g x u) v

In Proofgold the corresponding term root is b2e076... and proposition id is 3632d3...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__73__3

Beginning of Section Conj_mul_SNo_assoc_lem1__74__8

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Hypothesis H24 : SNo (g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__74__8)

SNo (v + g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is d9ad13... and proposition id is 3d8aec...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__74__8

Beginning of Section Conj_mul_SNo_assoc_lem1__75__0

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__75__0)

SNo (g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is a98402... and proposition id is 581454...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__75__0

Beginning of Section Conj_mul_SNo_assoc_lem1__75__9

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z + g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__75__9)

SNo (g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 5f487d... and proposition id is 86d7c6...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__75__9

Beginning of Section Conj_mul_SNo_assoc_lem1__76__10

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z)

Hypothesis H24 : SNo (g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__76__10)

SNo (g x2 z + g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 8df412... and proposition id is 4e7fe9...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__76__10

Beginning of Section Conj_mul_SNo_assoc_lem1__77__7

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z)

Theorem. (Conj_mul_SNo_assoc_lem1__77__7)

SNo (g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 9fd6f5... and proposition id is 93adb0...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__77__7

Beginning of Section Conj_mul_SNo_assoc_lem1__77__13

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z)

Theorem. (Conj_mul_SNo_assoc_lem1__77__13)

SNo (g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 54c247... and proposition id is 19caf4...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__77__13

Beginning of Section Conj_mul_SNo_assoc_lem1__77__19

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Hypothesis H22 : SNo (g x x2)

Hypothesis H23 : SNo (g x2 z)

Theorem. (Conj_mul_SNo_assoc_lem1__77__19)

SNo (g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 3d4667... and proposition id is 6af766...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__77__19

Beginning of Section Conj_mul_SNo_assoc_lem1__79__14

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Hypothesis H21 : SNo (g u x2)

Theorem. (Conj_mul_SNo_assoc_lem1__79__14)

SNo (g x x2) → w < g (g x y) z

In Proofgold the corresponding term root is a6ddf5... and proposition id is 94c5b7...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__79__14

Beginning of Section Conj_mul_SNo_assoc_lem1__80__7

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Hypothesis H20 : SNo (g u y)

Theorem. (Conj_mul_SNo_assoc_lem1__80__7)

SNo (g u x2) → w < g (g x y) z

In Proofgold the corresponding term root is d8d9da... and proposition id is 315b19...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__80__7

Beginning of Section Conj_mul_SNo_assoc_lem1__81__0

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoR y

Hypothesis H14 : y2 ∈ SNoR z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : y < x2

Hypothesis H18 : SNo y2

Hypothesis H19 : z < y2

Theorem. (Conj_mul_SNo_assoc_lem1__81__0)

SNo (g u y) → w < g (g x y) z

In Proofgold the corresponding term root is 5850a3... and proposition id is 4d5ea7...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__81__0

Beginning of Section Conj_mul_SNo_assoc_lem1__82__1

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g x2 z + g y y2)

Hypothesis H21 : SNo (g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__82__1)

SNo (v + g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 9ca4bb... and proposition id is 6db841...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__82__1

Beginning of Section Conj_mul_SNo_assoc_lem1__82__14

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g x2 z + g y y2)

Hypothesis H21 : SNo (g x2 y2)

Theorem. (Conj_mul_SNo_assoc_lem1__82__14)

SNo (v + g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is cd4402... and proposition id is db3818...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__82__14

Beginning of Section Conj_mul_SNo_assoc_lem1__83__9

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g x2 z + g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__83__9)

SNo (g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is e18f40... and proposition id is e9f6b8...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__83__9

Beginning of Section Conj_mul_SNo_assoc_lem1__83__13

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g x2 z + g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__83__13)

SNo (g x2 y2) → w < g (g x y) z

In Proofgold the corresponding term root is 548fa5... and proposition id is 278285...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__83__13

Beginning of Section Conj_mul_SNo_assoc_lem1__84__13

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g x2 z)

Hypothesis H21 : SNo (g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__84__13)

SNo (g x2 z + g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 2617ed... and proposition id is 7aafa3...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__84__13

Beginning of Section Conj_mul_SNo_assoc_lem1__84__20

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H21 : SNo (g y y2)

Theorem. (Conj_mul_SNo_assoc_lem1__84__20)

SNo (g x2 z + g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 1fb660... and proposition id is ebb2c7...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__84__20

Beginning of Section Conj_mul_SNo_assoc_lem1__85__0

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g x2 z)

Theorem. (Conj_mul_SNo_assoc_lem1__85__0)

SNo (g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is c59a01... and proposition id is 327c35...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__85__0

Beginning of Section Conj_mul_SNo_assoc_lem1__85__3

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Variable x2 : set

Variable y2 : set

Hypothesis H0 : (∀z2 : set, ∀w2 : set, SNo z2 → SNo w2 → SNo (g z2 w2))

Hypothesis H1 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 < z2 → v2 < w2 → (g u2 w2 + g z2 v2) < g z2 w2 + g u2 v2)

Hypothesis H2 : (∀z2 : set, ∀w2 : set, ∀u2 : set, ∀v2 : set, SNo z2 → SNo w2 → SNo u2 → SNo v2 → u2 ≤ z2 → v2 ≤ w2 → (g u2 w2 + g z2 v2) ≤ g z2 w2 + g u2 v2)

Hypothesis H4 : SNo y

Hypothesis H5 : SNo z

Hypothesis H6 : SNo (g x y)

Hypothesis H7 : (∀z2 : set, z2 ∈ SNoS_ (SNoLev x) → (∀w2 : set, SNo w2 → (∀u2 : set, u2 ∈ SNoS_ (SNoLev y) → (∀v2 : set, v2 ∈ SNoS_ (SNoLev z) → w = g z2 (g y z) + g x w2 + - (g z2 w2) → (g z2 (g u2 z + g y v2) + g x (w2 + g u2 v2)) ≤ g x (g u2 z + g y v2) + g z2 (w2 + g u2 v2) → (g (g z2 y + g x u2) z + g (g x y + g z2 u2) v2) < g (g x y + g z2 u2) z + g (g z2 y + g x u2) v2 → w < g (g x y) z))))

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H10 : SNo u

Hypothesis H11 : u < x

Hypothesis H12 : SNo v

Hypothesis H13 : x2 ∈ SNoL y

Hypothesis H14 : y2 ∈ SNoL z

Hypothesis H15 : (v + g x2 y2) ≤ g x2 z + g y y2

Hypothesis H16 : SNo x2

Hypothesis H17 : x2 < y

Hypothesis H18 : SNo y2

Hypothesis H19 : y2 < z

Hypothesis H20 : SNo (g x2 z)

Theorem. (Conj_mul_SNo_assoc_lem1__85__3)

SNo (g y y2) → w < g (g x y) z

In Proofgold the corresponding term root is 90abbe... and proposition id is e4cf77...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__85__3

Beginning of Section Conj_mul_SNo_assoc_lem1__87__3

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → SNo (g x2 y2))

Hypothesis H1 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → (∀z2 : set, z2 ∈ SNoL (g x2 y2) → (∀P : prop, (∀w2 : set, w2 ∈ SNoL x2 → (∀u2 : set, u2 ∈ SNoL y2 → (z2 + g w2 u2) ≤ g w2 y2 + g x2 u2 → P)) → (∀w2 : set, w2 ∈ SNoR x2 → (∀u2 : set, u2 ∈ SNoR y2 → (z2 + g w2 u2) ≤ g w2 y2 + g x2 u2 → P)) → P)))

Hypothesis H2 : (∀x2 : set, ∀y2 : set, ∀z2 : set, ∀w2 : set, SNo x2 → SNo y2 → SNo z2 → SNo w2 → z2 < x2 → w2 < y2 → (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2)

Hypothesis H4 : SNo x

Hypothesis H5 : SNo y

Hypothesis H6 : SNo z

Hypothesis H7 : SNo (g x y)

Hypothesis H8 : SNo (g y z)

Hypothesis H9 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev x) → (∀y2 : set, SNo y2 → (∀z2 : set, z2 ∈ SNoS_ (SNoLev y) → (∀w2 : set, w2 ∈ SNoS_ (SNoLev z) → w = g x2 (g y z) + g x y2 + - (g x2 y2) → (g x2 (g z2 z + g y w2) + g x (y2 + g z2 w2)) ≤ g x (g z2 z + g y w2) + g x2 (y2 + g z2 w2) → (g (g x2 y + g x z2) z + g (g x y + g x2 z2) w2) < g (g x y + g x2 z2) z + g (g x2 y + g x z2) w2 → w < g (g x y) z))))

Hypothesis H10 : u ∈ SNoL x

Hypothesis H11 : v ∈ SNoL (g y z)

Hypothesis H12 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H13 : SNo u

Hypothesis H14 : u < x

Theorem. (Conj_mul_SNo_assoc_lem1__87__3)

SNo v → w < g (g x y) z

In Proofgold the corresponding term root is 3da978... and proposition id is 0eed71...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__87__3

Beginning of Section Conj_mul_SNo_assoc_lem1__87__9

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → SNo (g x2 y2))

Hypothesis H1 : (∀x2 : set, ∀y2 : set, SNo x2 → SNo y2 → (∀z2 : set, z2 ∈ SNoL (g x2 y2) → (∀P : prop, (∀w2 : set, w2 ∈ SNoL x2 → (∀u2 : set, u2 ∈ SNoL y2 → (z2 + g w2 u2) ≤ g w2 y2 + g x2 u2 → P)) → (∀w2 : set, w2 ∈ SNoR x2 → (∀u2 : set, u2 ∈ SNoR y2 → (z2 + g w2 u2) ≤ g w2 y2 + g x2 u2 → P)) → P)))

Hypothesis H2 : (∀x2 : set, ∀y2 : set, ∀z2 : set, ∀w2 : set, SNo x2 → SNo y2 → SNo z2 → SNo w2 → z2 < x2 → w2 < y2 → (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2)

Hypothesis H3 : (∀x2 : set, ∀y2 : set, ∀z2 : set, ∀w2 : set, SNo x2 → SNo y2 → SNo z2 → SNo w2 → z2 ≤ x2 → w2 ≤ y2 → (g z2 y2 + g x2 w2) ≤ g x2 y2 + g z2 w2)

Hypothesis H4 : SNo x

Hypothesis H5 : SNo y

Hypothesis H6 : SNo z

Hypothesis H7 : SNo (g x y)

Hypothesis H8 : SNo (g y z)

Hypothesis H10 : u ∈ SNoL x

Hypothesis H11 : v ∈ SNoL (g y z)

Hypothesis H12 : w = g u (g y z) + g x v + - (g u v)

Hypothesis H13 : SNo u

Hypothesis H14 : u < x

Theorem. (Conj_mul_SNo_assoc_lem1__87__9)

SNo v → w < g (g x y) z

In Proofgold the corresponding term root is 9d46bf... and proposition id is 488de5...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__87__9

Beginning of Section Conj_mul_SNo_assoc_lem1__88__0

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H1 : (∀v : set, ∀x2 : set, ∀y2 : set, SNo v → SNo x2 → SNo y2 → g v (x2 + y2) = g v x2 + g v y2)

Hypothesis H2 : (∀v : set, ∀x2 : set, ∀y2 : set, SNo v → SNo x2 → SNo y2 → g (v + x2) y2 = g v y2 + g x2 y2)

Hypothesis H3 : (∀v : set, ∀x2 : set, SNo v → SNo x2 → (∀y2 : set, y2 ∈ SNoL (g v x2) → (∀P : prop, (∀z2 : set, z2 ∈ SNoL v → (∀w2 : set, w2 ∈ SNoL x2 → (y2 + g z2 w2) ≤ g z2 x2 + g v w2 → P)) → (∀z2 : set, z2 ∈ SNoR v → (∀w2 : set, w2 ∈ SNoR x2 → (y2 + g z2 w2) ≤ g z2 x2 + g v w2 → P)) → P)))

Hypothesis H4 : (∀v : set, ∀x2 : set, SNo v → SNo x2 → (∀y2 : set, y2 ∈ SNoR (g v x2) → (∀P : prop, (∀z2 : set, z2 ∈ SNoL v → (∀w2 : set, w2 ∈ SNoR x2 → (g z2 x2 + g v w2) ≤ y2 + g z2 w2 → P)) → (∀z2 : set, z2 ∈ SNoR v → (∀w2 : set, w2 ∈ SNoL x2 → (g z2 x2 + g v w2) ≤ y2 + g z2 w2 → P)) → P)))

Hypothesis H5 : (∀v : set, ∀x2 : set, ∀y2 : set, ∀z2 : set, SNo v → SNo x2 → SNo y2 → SNo z2 → y2 < v → z2 < x2 → (g y2 x2 + g v z2) < g v x2 + g y2 z2)

Hypothesis H6 : (∀v : set, ∀x2 : set, ∀y2 : set, ∀z2 : set, SNo v → SNo x2 → SNo y2 → SNo z2 → y2 ≤ v → z2 ≤ x2 → (g y2 x2 + g v z2) ≤ g v x2 + g y2 z2)

Hypothesis H7 : SNo x

Hypothesis H8 : SNo y

Hypothesis H9 : SNo z

Hypothesis H10 : (∀v : set, v ∈ SNoS_ (SNoLev x) → g v (g y z) = g (g v y) z)

Hypothesis H11 : (∀v : set, v ∈ SNoS_ (SNoLev y) → g x (g v z) = g (g x v) z)

Hypothesis H12 : (∀v : set, v ∈ SNoS_ (SNoLev z) → g x (g y v) = g (g x y) v)

Hypothesis H13 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → g v (g x2 z) = g (g v x2) z))

Hypothesis H14 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev z) → g v (g y x2) = g (g v y) x2))

Hypothesis H15 : (∀v : set, v ∈ SNoS_ (SNoLev y) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev z) → g x (g v x2) = g (g x v) x2))

Hypothesis H16 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → (∀y2 : set, y2 ∈ SNoS_ (SNoLev z) → g v (g x2 y2) = g (g v x2) y2)))

Hypothesis H17 : (∀v : set, v ∈ w → (∀P : prop, (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL (g y z) → v = g x2 (g y z) + g x y2 + - (g x2 y2) → P)) → (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoR (g y z) → v = g x2 (g y z) + g x y2 + - (g x2 y2) → P)) → P))

Hypothesis H18 : u ∈ w

Hypothesis H19 : SNo (g x y)

Hypothesis H20 : SNo (g y z)

Hypothesis H21 : SNo (g (g x y) z)

Theorem. (Conj_mul_SNo_assoc_lem1__88__0)

(∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, SNo x2 → (∀y2 : set, y2 ∈ SNoS_ (SNoLev y) → (∀z2 : set, z2 ∈ SNoS_ (SNoLev z) → u = g v (g y z) + g x x2 + - (g v x2) → (g v (g y2 z + g y z2) + g x (x2 + g y2 z2)) ≤ g x (g y2 z + g y z2) + g v (x2 + g y2 z2) → (g (g v y + g x y2) z + g (g x y + g v y2) z2) < g (g x y + g v y2) z + g (g v y + g x y2) z2 → u < g (g x y) z)))) → u < g (g x y) z

In Proofgold the corresponding term root is 90711e... and proposition id is 9e7273...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__88__0

Beginning of Section Conj_mul_SNo_assoc_lem1__88__17

Variable g : (set → (set → set))

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo v → SNo x2 → SNo (g v x2))

Hypothesis H1 : (∀v : set, ∀x2 : set, ∀y2 : set, SNo v → SNo x2 → SNo y2 → g v (x2 + y2) = g v x2 + g v y2)

Hypothesis H2 : (∀v : set, ∀x2 : set, ∀y2 : set, SNo v → SNo x2 → SNo y2 → g (v + x2) y2 = g v y2 + g x2 y2)

Hypothesis H3 : (∀v : set, ∀x2 : set, SNo v → SNo x2 → (∀y2 : set, y2 ∈ SNoL (g v x2) → (∀P : prop, (∀z2 : set, z2 ∈ SNoL v → (∀w2 : set, w2 ∈ SNoL x2 → (y2 + g z2 w2) ≤ g z2 x2 + g v w2 → P)) → (∀z2 : set, z2 ∈ SNoR v → (∀w2 : set, w2 ∈ SNoR x2 → (y2 + g z2 w2) ≤ g z2 x2 + g v w2 → P)) → P)))

Hypothesis H4 : (∀v : set, ∀x2 : set, SNo v → SNo x2 → (∀y2 : set, y2 ∈ SNoR (g v x2) → (∀P : prop, (∀z2 : set, z2 ∈ SNoL v → (∀w2 : set, w2 ∈ SNoR x2 → (g z2 x2 + g v w2) ≤ y2 + g z2 w2 → P)) → (∀z2 : set, z2 ∈ SNoR v → (∀w2 : set, w2 ∈ SNoL x2 → (g z2 x2 + g v w2) ≤ y2 + g z2 w2 → P)) → P)))

Hypothesis H5 : (∀v : set, ∀x2 : set, ∀y2 : set, ∀z2 : set, SNo v → SNo x2 → SNo y2 → SNo z2 → y2 < v → z2 < x2 → (g y2 x2 + g v z2) < g v x2 + g y2 z2)

Hypothesis H6 : (∀v : set, ∀x2 : set, ∀y2 : set, ∀z2 : set, SNo v → SNo x2 → SNo y2 → SNo z2 → y2 ≤ v → z2 ≤ x2 → (g y2 x2 + g v z2) ≤ g v x2 + g y2 z2)

Hypothesis H7 : SNo x

Hypothesis H8 : SNo y

Hypothesis H9 : SNo z

Hypothesis H10 : (∀v : set, v ∈ SNoS_ (SNoLev x) → g v (g y z) = g (g v y) z)

Hypothesis H11 : (∀v : set, v ∈ SNoS_ (SNoLev y) → g x (g v z) = g (g x v) z)

Hypothesis H12 : (∀v : set, v ∈ SNoS_ (SNoLev z) → g x (g y v) = g (g x y) v)

Hypothesis H13 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → g v (g x2 z) = g (g v x2) z))

Hypothesis H14 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev z) → g v (g y x2) = g (g v y) x2))

Hypothesis H15 : (∀v : set, v ∈ SNoS_ (SNoLev y) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev z) → g x (g v x2) = g (g x v) x2))

Hypothesis H16 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → (∀y2 : set, y2 ∈ SNoS_ (SNoLev z) → g v (g x2 y2) = g (g v x2) y2)))

Hypothesis H18 : u ∈ w

Hypothesis H19 : SNo (g x y)

Hypothesis H20 : SNo (g y z)

Hypothesis H21 : SNo (g (g x y) z)

Theorem. (Conj_mul_SNo_assoc_lem1__88__17)

(∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, SNo x2 → (∀y2 : set, y2 ∈ SNoS_ (SNoLev y) → (∀z2 : set, z2 ∈ SNoS_ (SNoLev z) → u = g v (g y z) + g x x2 + - (g v x2) → (g v (g y2 z + g y z2) + g x (x2 + g y2 z2)) ≤ g x (g y2 z + g y z2) + g v (x2 + g y2 z2) → (g (g v y + g x y2) z + g (g x y + g v y2) z2) < g (g x y + g v y2) z + g (g v y + g x y2) z2 → u < g (g x y) z)))) → u < g (g x y) z

In Proofgold the corresponding term root is 0390ba... and proposition id is f1c5cc...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_assoc_lem1__88__17

Beginning of Section Conj_mul_SNo_assoc_lem1__89__7