Claim L0: ...

...

Claim L1: ...

...

Claim L2: ...

...

Let x0 of type ι be given.

Assume H3: x0 ∈ int.

Let x1 of type ι be given.

Assume H4: x1 ∈ int.

Let x2 of type ι be given.

Assume H5: x2 ∈ int.

Let x3 of type ι be given.

Assume H6: x3 ∈ int.

Let x4 of type ι be given.

Assume H7: x4 ∈ int.

Let x5 of type ι be given.

Assume H8: x5 ∈ int.

Assume H9: x0 = add_SNo ((λ x6 . mul_SNo x6 x6) x2) (add_SNo ((λ x6 . mul_SNo x6 x6) x3) (add_SNo ((λ x6 . mul_SNo x6 x6) x4) ((λ x6 . mul_SNo x6 x6) x5))).

Let x6 of type ι be given.

Assume H10: x6 ∈ int.

Let x7 of type ι be given.

Assume H11: x7 ∈ int.

Let x8 of type ι be given.

Assume H12: x8 ∈ int.

Let x9 of type ι be given.

Assume H13: x9 ∈ int.

Assume H14: x1 = add_SNo ((λ x10 . mul_SNo x10 x10) x6) (add_SNo ((λ x10 . mul_SNo x10 x10) x7) (add_SNo ((λ x10 . mul_SNo x10 x10) x8) ((λ x10 . mul_SNo x10 x10) x9))).

Apply unknownprop_891bd8eaccd4934854a1a39a96fa375f8b43c939234e5ead477578dfa15afa04 with λ x10 . x10 ∈ int, add_SNo, mul_SNo, λ x10 . mul_SNo x10 x10, minus_SNo, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, ∀ x10 : ο . (∀ x11 . x11 ∈ int ⟶ ∀ x12 . x12 ∈ int ⟶ ∀ x13 . x13 ∈ int ⟶ ∀ x14 . x14 ∈ int ⟶ mul_SNo x0 x1 = add_SNo ((λ x15 . mul_SNo x15 x15) x11) (add_SNo ((λ x15 . mul_SNo x15 x15) x12) (add_SNo ((λ x15 . mul_SNo x15 x15) x13) ((λ x15 . mul_SNo x15 x15) x14))) ⟶ x10) ⟶ x10 leaving 28 subgoals.

Let x10 of type ι be given.

Let x11 of type ι be given.

Assume H15: x10 ∈ int.

Assume H16: x11 ∈ int.

Apply int_add_SNo with x10, x11 leaving 2 subgoals.

The subproof is completed by applying H15.

The subproof is completed by applying H16.

Let x10 of type ι be given.

Let x11 of type ι be given.

Assume H15: x10 ∈ int.

Assume H16: x11 ∈ int.

Apply int_mul_SNo with x10, x11 leaving 2 subgoals.

The subproof is completed by applying H15.

The subproof is completed by applying H16.

Let x10 of type ι be given.

Let x11 of type ι be given.

Let x12 of type ι be given.

Assume H15: x10 ∈ int.

Assume H16: x11 ∈ int.

Assume H17: x12 ∈ int.

Apply add_SNo_com_3_0_1 with x10, x11, x12 leaving 3 subgoals.

Apply L0 with x10.

The subproof is completed by applying H15.

Apply L0 with x11.

The subproof is completed by applying H16.

Apply L0 with x12.

The subproof is completed by applying H17.

The subproof is completed by applying L1.

Let x10 of type ι be given.

Let x11 of type ι be given.

Let x12 of type ι be given.

Assume H15: x10 ∈ int.

Assume H16: x11 ∈ int.

Assume H17: x12 ∈ int.

Apply mul_SNo_distrL with x10, x11, x12 leaving 3 subgoals.

Apply L0 with x10.

The subproof is completed by applying H15.

Apply L0 with x11.

The subproof is completed by applying H16.

Apply L0 with x12.

The subproof is completed by applying H17.

Let x10 of type ι be given.

Let x11 of type ι be given.

Let x12 of type ι be given.

Assume H15: x10 ∈ int.

Assume H16: x11 ∈ int.

Assume H17: x12 ∈ int.

Apply mul_SNo_distrR with x10, x11, x12 leaving 3 subgoals.

Apply L0 with x10.

The subproof is completed by applying H15.

Apply L0 with x11.

The subproof is completed by applying H16.

Apply L0 with x12.

The subproof is completed by applying H17.

Let x10 of type ι be given.

Assume H15: x10 ∈ int.

Let x11 of type ι → ι → ο be given.

Assume H16: x11 (mul_SNo x10 x10) (mul_SNo x10 x10).

The subproof is completed by applying H16.

The subproof is completed by applying int_minus_SNo.

Let x10 of type ι be given.

Assume H15: x10 ∈ int.

Apply minus_SNo_invol with x10.

Apply L0 with x10.

The subproof is completed by applying H15.

Let x10 of type ι be given.

Let x11 of type ι be given.

Assume H15: x10 ∈ int.

...

■

Proofgold Proof