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.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H0: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 : ο . (∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x3 ⟶ x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11))) ⟶ x9) ⟶ (∀ x10 . x10 ∈ x4 ⟶ ∀ x11 . x11 ∈ x5 ⟶ x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11))) ⟶ x9) ⟶ x9.

Assume H1: ∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x3 ⟶ add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9))) ∈ x7.

Assume H2: ∀ x8 . x8 ∈ x4 ⟶ ∀ x9 . x9 ∈ x5 ⟶ add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9))) ∈ x7.

Let x8 of type ι be given.

Assume H3: x8 ∈ x6.

Apply H0 with x8, x8 ∈ x7 leaving 3 subgoals.

The subproof is completed by applying H3.

Let x9 of type ι be given.

Assume H4: x9 ∈ x2.

Let x10 of type ι be given.

Assume H5: x10 ∈ x3.

Assume H6: x8 = add_SNo (mul_SNo x9 x1) (add_SNo (mul_SNo x0 x10) (minus_SNo (mul_SNo x9 x10))).

Apply H6 with λ x11 x12 . x12 ∈ x7.

Apply H1 with x9, x10 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

Let x9 of type ι be given.

Assume H4: x9 ∈ x4.

Let x10 of type ι be given.

Assume H5: x10 ∈ x5.

Assume H6: x8 = add_SNo (mul_SNo x9 x1) (add_SNo (mul_SNo x0 x10) (minus_SNo (mul_SNo x9 x10))).

Apply H6 with λ x11 x12 . x12 ∈ x7.

Apply H2 with x9, x10 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

■

Proofgold Proof