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: SNoLe x0 0.
Assume H2: SNo x1.
Assume H3: SNo x2.
Assume H4: SNoLe x2 x1.
Claim L5: add_SNo (mul_SNo x0 x1) (mul_SNo 0 x2) = mul_SNo x0 x1
set y3 to be ...
set y4 to be mul_SNo ... ...
Claim L5: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Assume H5: x5 (mul_SNo x2 y3).
set y6 to be add_SNo (mul_SNo x2 y3) (mul_SNo 0 y4)
set y7 to be add_SNo (mul_SNo y3 y4) 0
Claim L6: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
Assume H6: x8 (add_SNo (mul_SNo y4 x5) 0).
set y9 to be λ x9 . x8
Apply mul_SNo_zeroL with y6, λ x10 x11 . y9 (add_SNo (mul_SNo y4 x5) x10) (add_SNo (mul_SNo y4 x5) x11) 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 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H7: y8 y7 y7.
The subproof is completed by applying H7.
Apply add_SNo_0R 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 y4 ⟶ x5 y4 x6.
Assume H6: x5 y4 y4.
The subproof is completed by applying H6.
Claim L6: add_SNo (mul_SNo 0 x1) (mul_SNo x0 x2) = mul_SNo x0 x2
set y3 to be add_SNo (mul_SNo 0 x1) (mul_SNo x0 x2)
set y4 to be mul_SNo x1 y3
Claim L6: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Assume H6: x5 (mul_SNo x2 y4).
set y6 to be add_SNo (mul_SNo 0 y3) (mul_SNo x2 y4)
set y7 to be add_SNo 0 (mul_SNo y3 x5)
Claim L7: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
Assume H7: x8 (add_SNo 0 (mul_SNo y4 y6)).
set y9 to be λ x9 . x8
Apply mul_SNo_zeroL with x5, λ x10 x11 . y9 (add_SNo x10 (mul_SNo y4 y6)) (add_SNo x11 (mul_SNo y4 y6)) 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 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H8: y8 y7 y7.
The subproof is completed by applying H8.
Apply add_SNo_0L 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 y4 ⟶ x5 y4 x6.
Assume H7: x5 y4 y4.
The subproof is completed by applying H7.
Apply L5 with λ x3 x4 . SNoLe x3 (mul_SNo x0 x2).
Apply L6 with λ x3 x4 . SNoLe (add_SNo (mul_SNo x0 x1) (mul_SNo 0 x2)) x3.
Apply mul_SNo_Le with 0, x1, x0, x2 leaving 6 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
■