Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Let x0 of type ι be given.
Assume H4: x0 ∈ int.
Let x1 of type ι be given.
Assume H5: x1 ∈ int.
Let x2 of type ι be given.
Assume H6: x2 ∈ int.
Let x3 of type ι be given.
Assume H7: x3 ∈ int.
Let x4 of type ι be given.
Assume H8: x4 ∈ int.
Let x5 of type ι be given.
Assume H9: x5 ∈ int.
Assume H10: 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 H11: x6 ∈ int.
Let x7 of type ι be given.
Assume H12: x7 ∈ int.
Let x8 of type ι be given.
Assume H13: x8 ∈ int.
Let x9 of type ι be given.
Assume H14: x9 ∈ int.
Assume H15: 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_f712399f1133da8194de032e3ed497d1ec5c40bb41a197c5c3ec1ab28bc2ae11 with λ x10 . x10 ∈ int, add_SNo, mul_SNo, λ x10 . mul_SNo x10 x10, minus_SNo, λ x10 . x10 ∈ omega, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, ∀ x10 : ο . (∀ x11 . x11 ∈ omega ⟶ ∀ x12 . x12 ∈ omega ⟶ ∀ x13 . x13 ∈ omega ⟶ ∀ x14 . x14 ∈ omega ⟶ 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 29 subgoals.
Let x10 of type ι be given.
Let x11 of type ι be given.
Assume H16: x10 ∈ int.
Assume H17: x11 ∈ int.
Apply int_add_SNo with x10, x11 leaving 2 subgoals.
The subproof is completed by applying H16.
The subproof is completed by applying H17.
Let x10 of type ι be given.
Let x11 of type ι be given.
Assume H16: x10 ∈ int.
Assume H17: x11 ∈ int.
Apply int_mul_SNo with x10, x11 leaving 2 subgoals.
The subproof is completed by applying H16.
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 H16: x10 ∈ int.
Assume H17: x11 ∈ int.
Assume H18: 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 H16.
Apply L0 with x11.
The subproof is completed by applying H17.
Apply L0 with x12.
The subproof is completed by applying H18.
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 H16: x10 ∈ int.
Assume H17: x11 ∈ int.
Assume H18: x12 ∈ int.
Apply mul_SNo_distrL with x10, x11, x12 leaving 3 subgoals.
Apply L0 with x10.
The subproof is completed by applying H16.
Apply L0 with x11.
The subproof is completed by applying H17.
Apply L0 with x12.
The subproof is completed by applying H18.
Let x10 of type ι be given.
Let x11 of type ι be given.
Let x12 of type ι be given.
Assume H16: x10 ∈ int.
Assume H17: x11 ∈ int.
Assume H18: x12 ∈ int.
Apply mul_SNo_distrR with x10, x11, x12 leaving 3 subgoals.
Apply L0 with x10.
The subproof is completed by applying H16.
Apply L0 with x11.
The subproof is completed by applying H17.
Apply L0 with x12.
The subproof is completed by applying H18.
Let x10 of type ι be given.
Assume H16: x10 ∈ int.
Let x11 of type ι → ι → ο be given.
Assume H17: x11 (mul_SNo x10 x10) (mul_SNo x10 x10).
The subproof is completed by applying H17.
The subproof is completed by applying int_minus_SNo.
Let x10 of type ι be given.
Assume H16: x10 ∈ int.
Apply minus_SNo_invol with x10.
Apply L0 with x10.
The subproof is completed by applying H16.
Let x10 of type ι be given.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■