Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: int_lin_comb x0 x1 x2.

Let x3 of type ο be given.

Assume H1: x0 ∈ int ⟶ x1 ∈ int ⟶ x2 ∈ int ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ add_SNo (mul_SNo x4 x0) (mul_SNo x5 x1) = x2 ⟶ x3.

Apply H0 with x3.

Assume H2: and (and (x0 ∈ int) (x1 ∈ int)) (x2 ∈ int).

Apply H2 with (∃ x4 . and (x4 ∈ int) (∃ x5 . and (x5 ∈ int) (add_SNo (mul_SNo x4 x0) (mul_SNo x5 x1) = x2))) ⟶ x3.

Assume H3: and (x0 ∈ int) (x1 ∈ int).

Apply H3 with x2 ∈ int ⟶ (∃ x4 . and (x4 ∈ int) (∃ x5 . and (x5 ∈ int) (add_SNo (mul_SNo x4 x0) (mul_SNo x5 x1) = x2))) ⟶ x3.

Assume H4: x0 ∈ int.

Assume H5: x1 ∈ int.

Assume H6: x2 ∈ int.

Assume H7: ∃ x4 . and (x4 ∈ int) (∃ x5 . and (x5 ∈ int) (add_SNo (mul_SNo x4 x0) (mul_SNo x5 x1) = x2)).

Apply H7 with x3.

Let x4 of type ι be given.

Assume H8: (λ x5 . and (x5 ∈ int) (∃ x6 . and (x6 ∈ int) (add_SNo (mul_SNo x5 x0) (mul_SNo x6 x1) = x2))) x4.

Apply H8 with x3.

Assume H9: x4 ∈ int.

Assume H10: ∃ x5 . and (x5 ∈ int) (add_SNo (mul_SNo x4 x0) (mul_SNo x5 x1) = x2).

Apply H10 with x3.

Let x5 of type ι be given.

Assume H11: (λ x6 . and (x6 ∈ int) (add_SNo (mul_SNo x4 x0) (mul_SNo x6 x1) = x2)) x5.

Apply H11 with x3.

Apply H1 with x4, x5 leaving 4 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

The subproof is completed by applying H9.

■

Proofgold Proof