Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNoLt 0 x0.
Assume H2: SNo x1.
Assume H3: SNo x2.
Assume H4: SNoLt x1 x2.
Claim L5: add_SNo (mul_SNo 0 x2) (mul_SNo x0 x1) = mul_SNo x0 x1
set y3 to be ...
set y4 to be mul_SNo ... ...
Claim L5: ∀ x5 : ι → ο . x5 y4x5 y3
Let x5 of type ιο be given.
Assume H5: x5 (mul_SNo x2 y3).
set y6 to be add_SNo (mul_SNo 0 y4) (mul_SNo x2 y3)
set y7 to be add_SNo 0 (mul_SNo y3 y4)
Claim L6: ∀ x8 : ι → ο . x8 y7x8 y6
Let x8 of type ιο be given.
Assume H6: x8 (add_SNo 0 (mul_SNo y4 x5)).
set y9 to be λ x9 . x8
Apply mul_SNo_zeroL with y6, λ x10 x11 . y9 (add_SNo x10 (mul_SNo y4 x5)) (add_SNo x11 (mul_SNo y4 x5)) leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
set y8 to be λ x8 . y7
Apply L6 with λ x9 . y8 x9 y7y8 y7 x9 leaving 2 subgoals.
Assume H7: y8 y7 y7.
The subproof is completed by applying H7.
Apply add_SNo_0L with mul_SNo x5 y6, λ x9 . y8 leaving 2 subgoals.
Apply SNo_mul_SNo with x5, y6 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying L6.
Let x5 of type ιιο be given.
Apply L5 with λ x6 . x5 x6 y4x5 y4 x6.
Assume H6: x5 y4 y4.
The subproof is completed by applying H6.
Claim L6: add_SNo (mul_SNo x0 x2) (mul_SNo 0 x1) = mul_SNo x0 x2
set y3 to be add_SNo (mul_SNo x0 x2) (mul_SNo 0 x1)
set y4 to be mul_SNo x1 y3
Claim L6: ∀ x5 : ι → ο . x5 y4x5 y3
Let x5 of type ιο be given.
Assume H6: x5 (mul_SNo x2 y4).
set y6 to be add_SNo (mul_SNo x2 y4) (mul_SNo 0 y3)
set y7 to be add_SNo (mul_SNo y3 x5) 0
Claim L7: ∀ x8 : ι → ο . x8 y7x8 y6
Let x8 of type ιο be given.
Assume H7: x8 (add_SNo (mul_SNo y4 y6) 0).
set y9 to be λ x9 . x8
Apply mul_SNo_zeroL with x5, λ x10 x11 . y9 (add_SNo (mul_SNo y4 y6) x10) (add_SNo (mul_SNo y4 y6) x11) leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H7.
set y8 to be λ x8 . y7
Apply L7 with λ x9 . y8 x9 y7y8 y7 x9 leaving 2 subgoals.
Assume H8: y8 y7 y7.
The subproof is completed by applying H8.
Apply add_SNo_0R with mul_SNo x5 y7, λ x9 . y8 leaving 2 subgoals.
Apply SNo_mul_SNo with x5, y7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying L7.
Let x5 of type ιιο be given.
Apply L6 with λ x6 . x5 x6 y4x5 y4 x6.
Assume H7: x5 y4 y4.
The subproof is completed by applying H7.
Apply L5 with λ x3 x4 . SNoLt x3 (mul_SNo x0 x2).
Apply L6 with λ x3 x4 . SNoLt (add_SNo (mul_SNo 0 x2) (mul_SNo x0 x1)) x3.
Apply mul_SNo_Lt with x0, x2, 0, x1 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H4.