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 add_CSNo x2 (add_CSNo x0 x1)
Claim L3: ∀ x4 : ι → ο . x4 y3 ⟶ x4 (add_CSNo x0 (add_CSNo x1 x2))
Let x4 of type ι → ο be given.
Assume H3: x4 (add_CSNo y3 (add_CSNo x1 x2)).
set y5 to be add_CSNo x1 (add_CSNo y3 x2)
Claim L4: ∀ x6 : ι → ο . x6 y5 ⟶ x6 (add_CSNo x1 (add_CSNo x2 y3))
Let x6 of type ι → ο be given.
Apply unknownprop_6df04587a59e9b54f0549c96144213d94328d0b365474f739b895e743839c817 with y3, x4, λ x7 x8 . (λ x9 . x6) (add_CSNo x2 x7) (add_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_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba 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 add_CSNo (add_CSNo y5 y3) x4
Claim L5: ∀ x8 : ι → ο . x8 y7 ⟶ x8 (add_CSNo (add_CSNo y3 y5) x4)
Let x8 of type ι → ο be given.
Apply unknownprop_6df04587a59e9b54f0549c96144213d94328d0b365474f739b895e743839c817 with x4, y6, λ x9 x10 . (λ x11 . x8) (add_CSNo x9 y5) (add_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_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba 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.
■