Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Claim L1: ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3mul_SNo (mul_SNo x0 x1) (mul_SNo x2 x3) = mul_SNo (mul_SNo x0 x2) (mul_SNo x1 x3)
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H1: SNo x0.
Assume H2: SNo x1.
Assume H3: SNo x2.
Assume H4: SNo x3.
set y4 to be mul_SNo ... ...
set y5 to be mul_SNo (mul_SNo x1 x3) (mul_SNo x2 y4)
Claim L5: ∀ x6 : ι → ο . x6 y5x6 y4
Let x6 of type ιο be given.
Assume H5: x6 (mul_SNo (mul_SNo x2 y4) (mul_SNo x3 y5)).
set y7 to be λ x7 . x6
Apply mul_SNo_assoc with x2, x3, mul_SNo y4 y5, λ x8 x9 . y7 x9 x8 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply SNo_mul_SNo with y4, y5 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
set y8 to be mul_SNo x3 (mul_SNo y4 (mul_SNo y5 x6))
set y9 to be mul_SNo y4 (mul_SNo x6 (mul_SNo y5 y7))
Claim L6: ∀ x10 : ι → ο . x10 y9x10 y8
Let x10 of type ιο be given.
Assume H6: x10 (mul_SNo y5 (mul_SNo y7 (mul_SNo x6 y8))).
set y11 to be λ x11 . x10
Apply mul_SNo_assoc with x6, y7, y8, λ x12 x13 . x13 = mul_SNo y7 (mul_SNo x6 y8), λ x12 x13 . y11 (mul_SNo y5 x12) (mul_SNo y5 x13) leaving 5 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply mul_SNo_assoc with y7, x6, y8, λ x12 x13 . mul_SNo (mul_SNo x6 y7) y8 = x13 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
set y12 to be mul_SNo (mul_SNo x6 y7) y8
set y13 to be mul_SNo (mul_SNo y8 y7) y9
Claim L7: ∀ x14 : ι → ο . x14 y13x14 y12
Let x14 of type ιο be given.
Assume H7: x14 (mul_SNo (mul_SNo y9 y8) x10).
set y15 to be λ x15 . x14
Apply mul_SNo_com with y8, y9, λ x16 x17 . y15 (mul_SNo x16 x10) (mul_SNo x17 x10) leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
Let x14 of type ιιο be given.
Apply L7 with λ x15 . x14 x15 y13x14 y13 x15.
Assume H8: x14 y13 y13.
The subproof is completed by applying H8.
The subproof is completed by applying H6.
set y10 to be λ x10 . y9
Apply L6 with λ x11 . y10 x11 y9y10 y9 x11 leaving 2 subgoals.
Assume H7: y10 y9 y9.
The subproof is completed by applying H7.
Apply mul_SNo_assoc with x6, y8, mul_SNo y7 y9, λ x11 . y10 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply SNo_mul_SNo with y7, y9 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L6.
Let x6 of type ιιο be given.
Apply L5 with λ x7 . x6 x7 y5x6 y5 x7.
Assume H6: x6 y5 y5.
The subproof is completed by applying H6.
Apply unknownprop_891bd8eaccd4934854a1a39a96fa375f8b43c939234e5ead477578dfa15afa04 with SNo, add_SNo, mul_SNo, λ x0 . mul_SNo x0 x0, minus_SNo leaving 15 subgoals.
The subproof is completed by applying SNo_add_SNo.
The subproof is completed by applying SNo_mul_SNo.
The subproof is completed by applying add_SNo_com_3_0_1.
The subproof is completed by applying L0.
The subproof is completed by applying mul_SNo_distrL.
The subproof is completed by applying mul_SNo_distrR.
Let x0 of type ι be given.
Assume H2: SNo x0.
Let x1 of type ιιο be given.
Assume H3: x1 (mul_SNo x0 x0) (mul_SNo x0 x0).
The subproof is completed by applying H3.
The subproof is completed by applying SNo_minus_SNo.
The subproof is completed by applying minus_SNo_invol.
The subproof is completed by applying add_SNo_minus_L2.
The subproof is completed by applying add_SNo_minus_SNo_prop2.
The subproof is completed by applying mul_SNo_minus_distrL.
The subproof is completed by applying mul_SNo_minus_distrR.
The subproof is completed by applying mul_SNo_com.
The subproof is completed by applying L1.