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: x2lam 2 (λ x3 . If_i (x3 = 0) x0 x1).
Claim L1: ∃ x3 . and (x32) (∃ x4 . and (x4If_i (x3 = 0) x0 x1) (x2 = setsum x3 x4))
Apply lamE with 2, λ x3 . If_i (x3 = 0) x0 x1, x2.
The subproof is completed by applying H0.
Apply exandE_i with λ x3 . x32, λ x3 . ∃ x4 . and (x4If_i (x3 = 0) x0 x1) (x2 = setsum x3 x4), ∃ x3 . and (x32) (∃ x4 . x2 = setsum x3 x4) leaving 2 subgoals.
The subproof is completed by applying L1.
Let x3 of type ι be given.
Assume H2: x32.
Assume H3: ∃ x4 . and (x4If_i (x3 = 0) x0 x1) (x2 = setsum x3 x4).
Apply exandE_i with λ x4 . x4If_i (x3 = 0) x0 x1, λ x4 . x2 = setsum x3 x4, ∃ x4 . and (x42) (∃ x5 . x2 = setsum x4 x5) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Assume H4: x4If_i (x3 = 0) x0 x1.
Assume H5: x2 = setsum x3 x4.
Let x5 of type ο be given.
Assume H6: ∀ x6 . and (x62) (∃ x7 . x2 = setsum x6 x7)x5.
Apply H6 with x3.
Apply andI with x32, ∃ x6 . x2 = setsum x3 x6 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x6 of type ο be given.
Assume H7: ∀ x7 . x2 = setsum x3 x7x6.
Apply H7 with x4.
The subproof is completed by applying H5.