Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H0: SNoCutP x0 x1.

Assume H1: SNoCutP x2 x3.

Assume H2: x4 = SNoCut x0 x1.

Assume H3: x5 = SNoCut x2 x3.

Apply mul_SNoCutP_lem with x0, x1, x2, x3, x4, x5, ∀ x6 : ο . (∀ x7 x8 x9 x10 . (∀ x11 . ... ⟶ ∀ x12 : ο . (∀ x13 . ... ⟶ ∀ x14 . ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) ...) ⟶ x12) ⟶ x12) ⟶ (∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x2 ⟶ add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12))) ∈ x7) ⟶ (∀ x11 . x11 ∈ x8 ⟶ ∀ x12 : ο . (∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x3 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNoLt x4 x13 ⟶ SNoLt x5 x14 ⟶ x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14))) ⟶ x12) ⟶ x12) ⟶ (∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x3 ⟶ add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12))) ∈ x8) ⟶ (∀ x11 . x11 ∈ x9 ⟶ ∀ x12 : ο . (∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x3 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNoLt x13 x4 ⟶ SNoLt x5 x14 ⟶ x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14))) ⟶ x12) ⟶ x12) ⟶ (∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x3 ⟶ add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12))) ∈ x9) ⟶ (∀ x11 . x11 ∈ x10 ⟶ ∀ x12 : ο . (∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x2 ⟶ SNo x13 ⟶ SNo x14 ⟶ SNoLt x4 x13 ⟶ SNoLt x14 x5 ⟶ x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14))) ⟶ x12) ⟶ x12) ⟶ (∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x2 ⟶ add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12))) ∈ x10) ⟶ SNoCutP (binunion x7 x8) (binunion x9 x10) ⟶ mul_SNo x4 x5 = SNoCut (binunion x7 x8) (binunion x9 x10) ⟶ x6) ⟶ x6 leaving 5 subgoals.

...

■

Proofgold Proof