Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2.
Assume H1: atleastp u8 x0.
Assume H2: 4402e.. x0 x1.
Assume H3: cf2df.. x0 x1.
Apply unknownprop_5af272e668d2d4cb72a765ba9a805ccc7fcec5ab9afe42c7f545b5c5a9294852 with u7, x0, 2426f.. x0 x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H4: (λ x3 . and (x3 ∈ x0) (atleastp u7 (setminus x0 (Sing x3)))) x2.
Apply H4 with 2426f.. x0 x1.
Assume H5: x2 ∈ x0.
Assume H6: atleastp u7 (setminus x0 (Sing x2)).
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply unknownprop_8943e38544e4b3d2b57c8c11b227c9428aebdef7c8a11d7eeadb3d3e0c07b51b with setminus x0 (Sing x2), x1, 2426f.. x0 x1 leaving 75 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying H6.
The subproof is completed by applying L8.
The subproof is completed by applying L9.
Apply unknownprop_14fd977f9d49fdc31325589d4fd4871675e1b8644efb5fa4452159818f3052df with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_519380bf5e700579b8bba06459ffb26f102d5176741d2b30518ea4fc278f9c2f with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_2ae0e70f5cbcf0faa8f049540c6a88b78bbe8edaee08c8f443d17461beed8f7c with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_c215c1e5c8db9a494c68832673ae159e31b497dd30b9cd5a06bf90b2dc622027 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_d52e44eac2717dee318b61da9407034839e0c1f3506fa8a2bb81063955a6794e with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_ba72885e1c8f93469ca1423ea1b55f2bd3ff94e3d12a7fcd3a357fd4886d594b with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_451f02faf6d322d6d76ffa47096fadaa7a104aa60602216495fcd330d20fdae7 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_c743d4a2def8d24688ab1760000e97c9ff290fc2288f898e04fbc305f352f8e5 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_6abf5cbfecdcc086d2501154cf6bd22c29c72f71d83ce4bd4f360714cf142d04 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_70620a076eeb7e009bbf696fc3b55b6fb5a9dd47ac651b610df1a080476489d2 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_b02f3b1df042581958d2e3840ceb00ed9425f938d16034e6f826b011d25f2f78 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_fbf09b883e1a1f4202592bec1132aa8b6614eb4531a0f561f3c2bf5bd1691f42 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_8739ca73df7ce8fbfdcfb423d914c5f8472b986a344e14a98b84f6792899c25a with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_ffc828c80b3b9452182cbae7b23771ea936205e8d6dd5d8d6bf8edb5e2290cd7 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_aafd5247c0709fa92dd924bfa603d5fdf261dd7d8768b7de5a73fd0b2f68f60e with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_71e8ac59792b068dc35880f4f6a312a337647a837feff4d999dfcda74f8562f6 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_accd7db684bac68cee89d43656b994929df22c5e1eaf91fb72e7c53bef39aead with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_a1333c6dec5b19f801d52c628b4a4ac7134f17034b34fe5bd11510f9d903f0df with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_39b1baacfdbf7477ec9094a8ed896870ab723ea278e4e6f3c578375425fa0696 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_aef1ae00f4d44fcc9d1329c1a9814b8e67ad8f881c2ac52fc989abe2dd6be514 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_a80e8e045e89520db9d3c1dbff0875d07aea5fbda9a8d0e436c420b624781e6d with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_17ab8152e28bccd713c63a99b81b6bf3ac1e3f46c00b7a7f697ffef92dc841e7 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_cb6e194cc3113cb500f9acc0f4c6e79589929f83e883e553ec86ad3a425ea347 with x0, x1, x2, setminus x0 (Sing x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L10.
Apply unknownprop_7bff4c44de67f1b5ae68c7c31d5afcc913e59ee93b4ec37d4975bf6dac976166 with x0, x1, x2, setminus ... ... leaving 5 subgoals.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■