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.
Let x3 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Assume H3: SNo x3.
set y4 to be mul_SNo (mul_SNo x0 x1) (mul_SNo x2 x3)
set y5 to be mul_SNo (mul_SNo x1 x3) (mul_SNo x2 y4)
Claim L4: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4
Let x6 of type ι → ο be given.
Assume H4: 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 H0.
The subproof is completed by applying H1.
Apply SNo_mul_SNo with y4, y5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
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 L5: ∀ x10 : ι → ο . x10 y9 ⟶ x10 y8
Let x10 of type ι → ο be given.
Assume H5: 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 H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
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 H2.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
set y12 to be mul_SNo (mul_SNo x6 y7) y8
set y13 to be mul_SNo (mul_SNo y8 y7) y9
Claim L6: ∀ x14 : ι → ο . x14 y13 ⟶ x14 y12
Let x14 of type ι → ο be given.
Assume H6: 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 H1.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Let x14 of type ι → ι → ο be given.
Apply L6 with λ x15 . x14 x15 y13 ⟶ x14 y13 x15.
Assume H7: x14 y13 y13.
The subproof is completed by applying H7.
The subproof is completed by applying H5.
set y10 to be λ x10 . y9
Apply L5 with λ x11 . y10 x11 y9 ⟶ y10 y9 x11 leaving 2 subgoals.
Assume H6: y10 y9 y9.
The subproof is completed by applying H6.
Apply mul_SNo_assoc with x6, y8, mul_SNo y7 y9, λ x11 . y10 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply SNo_mul_SNo with y7, y9 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
The subproof is completed by applying L5.
Let x6 of type ι → ι → ο be given.
Apply L4 with λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H5: x6 y5 y5.
The subproof is completed by applying H5.
■