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 x1.
Assume H1: SNo x2.
Assume H2: SNo x3.
set y4 to be mul_SNo x0 (mul_SNo x2 (mul_SNo x1 x3))
Claim L3: ∀ x5 : ι → ο . x5 y4x5 (mul_SNo x0 (mul_SNo x1 (mul_SNo x2 x3)))
Let x5 of type ιο be given.
Apply mul_SNo_com_3_0_1 with x2, x3, y4, λ x6 x7 . (λ x8 . x5) (mul_SNo x1 x6) (mul_SNo x1 x7) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x5 of type ιιο be given.
Apply L3 with λ x6 . x5 x6 y4x5 y4 x6.
Assume H4: x5 y4 y4.
The subproof is completed by applying H4.