Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with setsum x0 x1, lam 2 (λ x2 . If_i (x2 = 0) x0 x1) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H0: In x2 (setsum x0 x1).
Apply unknownprop_976b9ed71c1ec1f277c9c37a01879b51c2de3497fe82149802bec54f853970e6 with x0, x1, x2, λ x3 . In x3 (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) leaving 3 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H1: In x3 x0.
Apply unknownprop_1633a25a08ee627a1613041ad1ebe0a4535d0c6ce109cb609e7d9a519dad2f25 with 2, λ x4 . If_i (x4 = 0) x0 x1, 0, x3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_7630054952f4bd54be6e25e2e786a4db7b90ee782d6b1031afa63aeb6d55b595.
Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with 0 = 0, x0, x1, λ x4 x5 . In x3 x5 leaving 2 subgoals.
Let x4 of type ι → ι → ο be given.
Assume H2: x4 0 0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H1: In x3 x1.
Apply unknownprop_1633a25a08ee627a1613041ad1ebe0a4535d0c6ce109cb609e7d9a519dad2f25 with 2, λ x4 . If_i (x4 = 0) x0 x1, 1, x3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_85e7394990c25c8874e39b4ca1ac83bc7d22390df4a86e0ba0fa73d0ca7d5d30.
Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with 1 = 0, x0, x1, λ x4 x5 . In x3 x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_698eb914d3aabc70ca0bb946b6907a27e3cce6e39040426b924e77df3507fbcf.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H0: In x2 (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)).
Claim L1: ...
...
Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with λ x3 . In x3 2, λ x3 . ∃ x4 . and (In x4 (If_i (x3 = 0) x0 x1)) (x2 = setsum x3 x4), In x2 (setsum x0 x1) leaving 2 subgoals.
The subproof is completed by applying L1.
Let x3 of type ι be given.
Assume H2: In x3 2.
Assume H3: ∃ x4 . and (In x4 (If_i (x3 = 0) x0 x1)) (x2 = setsum x3 x4).
Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with λ x4 . In x4 (If_i (x3 = 0) x0 x1), λ x4 . x2 = setsum x3 x4, In x2 (setsum x0 x1) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Assume H4: In x4 (If_i (x3 = 0) x0 x1).
Assume H5: x2 = setsum x3 x4.
Apply H5 with λ x5 x6 . In x6 (setsum x0 x1).
Claim L6: In ... ...
...
Apply unknownprop_75ddf832b1631756e4bbf96a65e15fca654982aa51c8799a97b68da7b8a2da12 with x3, 0, 1, In (setsum x3 x4) (setsum x0 x1) leaving 3 subgoals.
The subproof is completed by applying L6.
Assume H7: x3 = 0.
Apply H7 with λ x5 x6 . In (setsum x6 x4) (setsum x0 x1).
Apply unknownprop_a381a34f160abaf2788d778fb7e511fe432033da3c71a8dc7ca4fe2a805729af with x0, x1, x4.
Claim L8: If_i (x3 = 0) x0 x1 = x0
Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with x3 = 0, x0, x1.
The subproof is completed by applying H7.
Apply L8 with λ x5 x6 . In x4 x5.
The subproof is completed by applying H4.
Assume H7: x3 = 1.
Apply H7 with λ x5 x6 . In (setsum x6 x4) (setsum x0 x1).
Apply unknownprop_ba4ceb4cfc28d9d20da4c7556dd8a911f49892fbf59d2c31799f1fb1cd51e58b with x0, x1, x4.
Claim L8: If_i (x3 = 0) x0 x1 = x1
Apply H7 with λ x5 x6 . If_i (x6 = 0) x0 x1 = x1.
Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with 1 = 0, x0, x1.
The subproof is completed by applying unknownprop_698eb914d3aabc70ca0bb946b6907a27e3cce6e39040426b924e77df3507fbcf.
Apply L8 with λ x5 x6 . In x4 x5.
The subproof is completed by applying H4.
■