Proofgold Proof

pf

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, x1 ∈ int 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.

The subproof is completed by applying H2.

■