Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Apply unknownprop_712520f713b96d5afd10321cea9a3c978868fc53aa35a29461e902d5b5a4ba79 with λ x0 . True, HomSet, λ x0 . lam_id x0, λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4, 9f253.., UnaryFuncHom, struct_id, struct_comp, 47c33.., 2e027.., λ x0 . ap x0 0, λ x0 x1 x2 . x2, f3f54.., daacd.. leaving 5 subgoals.
Apply unknownprop_3d05796578cdc17ebd2096167db48ecef934256d250d1637eb5dd67225cdfe05 with λ x0 . True, HomSet, λ x0 . lam_id x0, λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4, 9f253.., UnaryFuncHom, struct_id, struct_comp, λ x0 . pack_u (setsum x0 x0) (combine_funcs x0 x0 Inj1 Inj1), λ x0 x1 x2 . lam (setsum x0 x0) (λ x3 . combine_funcs x0 x0 (λ x4 . Inj0 (ap x2 x4)) (λ x4 . Inj1 (ap x2 x4)) x3) leaving 3 subgoals.
The subproof is completed by applying unknownprop_dcf5739aa5fe0adc626fd983737b233fe68652dff14c53b3d75823dcf2542d41.
The subproof is completed by applying unknownprop_2568db697e5888ec2fd1f1bf9456b9508292ed4b824e8582b40e4f025f149e68.
Apply unknownprop_795e291855a044d4d636c961caa1600704603cc02e33a7b37aa66e8d7f6512db with λ x0 . True, HomSet, λ x0 . lam_id x0, λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4, 9f253.., UnaryFuncHom, struct_id, struct_comp, λ x0 . pack_u (setsum x0 x0) (combine_funcs x0 x0 Inj1 Inj1), λ x0 x1 x2 . lam (setsum x0 x0) (λ x3 . combine_funcs x0 x0 (λ x4 . Inj0 (ap x2 x4)) (λ x4 . Inj1 (ap x2 x4)) x3) leaving 4 subgoals.
Let x0 of type ι be given.
Assume H8: (λ x1 . True) x0.
Apply andI with struct_u ((λ x1 . pack_u (setsum x1 x1) (combine_funcs x1 x1 Inj1 Inj1)) x0), unpack_u_o ((λ x1 . pack_u (setsum x1 x1) (combine_funcs x1 x1 Inj1 Inj1)) x0) (λ x1 . λ x2 : ι → ι . ∀ x3 . x3 ∈ x1 ⟶ x2 (x2 x3) = x2 x3) leaving 2 subgoals.
Apply pack_struct_u_I with setsum x0 x0, combine_funcs x0 x0 Inj1 Inj1.
The subproof is completed by applying L0 with x0.
Claim L9: ...
...
Apply unpack_u_o_eq with λ x1 . λ x2 : ι → ι . ∀ x3 . x3 ∈ x1 ⟶ x2 (x2 x3) = x2 x3, setsum x0 x0, combine_funcs x0 x0 Inj1 Inj1, λ x1 x2 : ο . x2 leaving 2 subgoals.
The subproof is completed by applying L9.
Let x1 of type ι be given.
Assume H10: x1 ∈ setsum x0 x0.
Apply setsum_Inj_inv with x0, x0, x1, combine_funcs x0 x0 Inj1 Inj1 (combine_funcs x0 x0 Inj1 Inj1 x1) = combine_funcs x0 x0 Inj1 Inj1 x1 leaving 3 subgoals.
The subproof is completed by applying H10.
Assume H11: ∃ x2 . and (x2 ∈ x0) (x1 = Inj0 x2).
Apply H11 with combine_funcs x0 x0 Inj1 Inj1 (combine_funcs x0 x0 Inj1 Inj1 x1) = combine_funcs x0 x0 Inj1 Inj1 x1.
Let x2 of type ι be given.
Assume H12: (λ x3 . and (x3 ∈ x0) (x1 = Inj0 x3)) x2.
Apply H12 with combine_funcs x0 x0 Inj1 Inj1 (combine_funcs x0 x0 Inj1 Inj1 x1) = combine_funcs x0 x0 Inj1 Inj1 x1.
Assume H13: x2 ∈ x0.
Assume H14: ... = ....
...
...
...
...
...
...
...
...
...
■