Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: Subq x1 x0.
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setsum x1 (setminus x0 x1), x0, combine_funcs x1 (setminus x0 x1) (λ x2 . x2) (λ x2 . x2).
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setsum x1 (setminus x0 x1), x0, combine_funcs x1 (setminus x0 x1) (λ x2 . x2) (λ x2 . x2) leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setsum x1 (setminus x0 x1), x0, combine_funcs x1 (setminus x0 x1) (λ x2 . x2) (λ x2 . x2) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H4: In x2 (setsum x1 (setminus x0 x1)).
Apply L1 with x2, λ x3 . In (combine_funcs x1 (setminus x0 x1) (λ x4 . x4) (λ x4 . x4) x3) x0 leaving 3 subgoals.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Assume H5: In x3 x1.
Apply L2 with x3, λ x4 x5 . In x5 x0.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with x1, x0, x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
Let x3 of type ι be given.
Assume H5: In x3 x0.
Assume H6: nIn x3 x1.
Apply L3 with x3, λ x4 x5 . In x5 x0.
The subproof is completed by applying H5.
Let x2 of type ι be given.
Assume H4: In x2 (setsum x1 (setminus x0 x1)).
Apply L1 with x2, λ x3 . ∀ x4 . In x4 (setsum x1 (setminus x0 x1)) ⟶ combine_funcs x1 (setminus x0 x1) (λ x5 . x5) (λ x5 . x5) x3 = combine_funcs x1 (setminus x0 x1) (λ x5 . x5) (λ x5 . x5) x4 ⟶ x3 = x4 leaving 3 subgoals.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Assume H5: In x3 x1.
Let x4 of type ι be given.
Assume H6: In x4 (setsum x1 (setminus x0 x1)).
Apply L2 with x3, λ x5 x6 . x6 = combine_funcs x1 (setminus x0 x1) (λ x7 . x7) (λ x7 . x7) x4 ⟶ Inj0 x3 = x4.
Apply L1 with x4, λ x5 . x3 = combine_funcs x1 (setminus x0 x1) (λ x6 . x6) (λ x6 . x6) x5 ⟶ Inj0 x3 = x5 leaving 3 subgoals.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Assume H7: In x5 x1.
Apply L2 with x5, λ x6 x7 . x3 = x7 ⟶ Inj0 x3 = Inj0 x5.
Assume H8: x3 = x5.
Apply H8 with λ x6 x7 . Inj0 x7 = Inj0 x5.
Let x6 of type ι → ι → ο be given.
Assume H9: x6 (Inj0 x5) (Inj0 x5).
The subproof is completed by applying H9.
Let x5 of type ι be given.
Assume H7: In x5 x0.
Assume H8: nIn x5 x1.
Apply L3 with x5, λ x6 x7 . x3 = x7 ⟶ Inj0 x3 = Inj1 x5.
Assume H9: x3 = x5.
Apply FalseE with Inj0 x3 = Inj1 x5.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with x5, x1 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply H9 with λ x6 x7 . In x6 x1.
The subproof is completed by applying H5.
Let x3 of type ι be given.
Assume H5: In x3 x0.
...
...
■