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: CSNo x0.
Assume H1: CSNo x1.
Assume H2: CSNo x2.
set y3 to be mul_CSNo x2 (mul_CSNo x0 x1)
Claim L3: ∀ x4 : ι → ο . x4 y3 ⟶ x4 (mul_CSNo x0 (mul_CSNo x1 x2))
Let x4 of type ι → ο be given.
Assume H3: x4 (mul_CSNo y3 (mul_CSNo x1 x2)).
set y5 to be mul_CSNo x1 (mul_CSNo y3 x2)
Claim L4: ∀ x6 : ι → ο . x6 y5 ⟶ x6 (mul_CSNo x1 (mul_CSNo x2 y3))
Let x6 of type ι → ο be given.
Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with y3, x4, λ x7 x8 . (λ x9 . x6) (mul_CSNo x2 x7) (mul_CSNo x2 x8) leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
set y6 to be λ x6 . y5
Apply L4 with λ x7 . y6 x7 y5 ⟶ y6 y5 x7 leaving 2 subgoals.
Assume H5: y6 y5 y5.
The subproof is completed by applying H5.
Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with y3, y5, x4, λ x7 . y6 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
set y7 to be mul_CSNo (mul_CSNo y5 y3) x4
Claim L5: ∀ x8 : ι → ο . x8 y7 ⟶ x8 (mul_CSNo (mul_CSNo y3 y5) x4)
Let x8 of type ι → ο be given.
Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with x4, y6, λ x9 x10 . (λ x11 . x8) (mul_CSNo x9 y5) (mul_CSNo x10 y5) leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
set y8 to be λ x8 . y7
Apply L5 with λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H6: y8 y7 y7.
The subproof is completed by applying H6.
Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with y7, y5, y6, λ x9 x10 . (λ x11 . y8) x10 x9 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying L5.
Let x4 of type ι → ι → ο be given.
Apply L3 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H4: x4 y3 y3.
The subproof is completed by applying H4.
■