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.
Apply unknownprop_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba with x0, x1, x2, λ x3 x4 . x4 = add_CSNo x1 (add_CSNo x0 x2) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba with x1, x0, x2, λ x3 x4 . add_CSNo (add_CSNo x0 x1) x2 = x4 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
set y3 to be add_CSNo (add_CSNo x1 x0) x2
Claim L3: ∀ x4 : ι → ο . x4 y3 ⟶ x4 (add_CSNo (add_CSNo x0 x1) x2)
Let x4 of type ι → ο be given.
Apply unknownprop_6df04587a59e9b54f0549c96144213d94328d0b365474f739b895e743839c817 with x1, x2, λ x5 x6 . (λ x7 . x4) (add_CSNo x5 y3) (add_CSNo x6 y3) leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
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.
■