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.

Apply int_lin_comb_E with x0, x1, x2, int_lin_comb x1 x0 x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: x0 ∈ int.

Assume H2: x1 ∈ int.

Assume H3: x2 ∈ int.

Let x3 of type ι be given.

Assume H4: x3 ∈ int.

Let x4 of type ι be given.

Assume H5: x4 ∈ int.

Assume H6: add_SNo (mul_SNo x3 x0) (mul_SNo x4 x1) = x2.

Apply int_lin_comb_I with x1, x0, x2 leaving 4 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

Let x5 of type ο be given.

Assume H7: ∀ x6 . and (x6 ∈ int) (∃ x7 . and (x7 ∈ int) (add_SNo (mul_SNo x6 x1) (mul_SNo x7 x0) = x2)) ⟶ x5.

Apply H7 with x4.

Apply andI with x4 ∈ int, ∃ x6 . and (x6 ∈ int) (add_SNo (mul_SNo x4 x1) (mul_SNo x6 x0) = x2) leaving 2 subgoals.

The subproof is completed by applying H5.

Let x6 of type ο be given.

Assume H8: ∀ x7 . and (x7 ∈ int) (add_SNo (mul_SNo x4 x1) (mul_SNo x7 x0) = x2) ⟶ x6.

Apply H8 with x3.

Apply andI with x3 ∈ int, add_SNo (mul_SNo x4 x1) (mul_SNo x3 x0) = x2 leaving 2 subgoals.

The subproof is completed by applying H4.

Apply add_SNo_com with mul_SNo x4 x1, mul_SNo x3 x0, λ x7 x8 . x8 = x2 leaving 3 subgoals.

Apply SNo_mul_SNo with x4, x1 leaving 2 subgoals.

Apply int_SNo with x4.

The subproof is completed by applying H5.

Apply int_SNo with x1.

The subproof is completed by applying H2.

Apply SNo_mul_SNo with x3, x0 leaving 2 subgoals.

Apply int_SNo with x3.

The subproof is completed by applying H4.

Apply int_SNo with x0.

The subproof is completed by applying H1.

The subproof is completed by applying H6.

■

Proofgold Proof