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.
Let x3 of type ι → ο be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Apply unknownprop_ebe9a576a5cc888449e31325d3aa9514ef05d3ea8aa75a74baad2877bbba6245 with x2, x3, binintersect x0 x1, or (or (PNoLt x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3))) (PNoLt x1 x3 x0 x2) leaving 4 subgoals.
The subproof is completed by applying L4.
Assume H5: PNoLt_ (binintersect x0 x1) x2 x3.
Apply unknownprop_0e1ba7291a295ea3c1979b40483f7544221790d53d76aadba99638689b88d9d1 with PNoLt x0 x2 x1 x3, and (x0 = x1) (PNoEq_ x0 x2 x3), PNoLt x1 x3 x0 x2.
Apply unknownprop_2a38d5561acb46bf4581f375c3fb301a06d08a93dee7d2c06138bdaa38452584 with x0, x1, x2, x3.
The subproof is completed by applying H5.
Assume H5: PNoEq_ (binintersect x0 x1) x2 x3.
Apply unknownprop_497ef0b809178e9ac674acf0f41f994a7e76b824de0430efd934f6540a71daab with x0, x1, or (or (PNoLt x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3))) (PNoLt x1 x3 x0 x2) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H6: In x0 x1.
Claim L7: binintersect x0 x1 = x0
Apply unknownprop_5afda972c78302d86ad70171f9367780fa0c3403baf81f9e7aa674a8a6ec4541 with x0, x1.
Apply L3 with x0.
The subproof is completed by applying H6.
Claim L8: PNoEq_ x0 x2 x3
Apply L7 with λ x4 x5 . PNoEq_ x4 x2 x3.
The subproof is completed by applying H5.
Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with x3 x0, or (or (PNoLt x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3))) (PNoLt x1 x3 x0 x2) leaving 2 subgoals.
Assume H9: x3 x0.
Apply unknownprop_0e1ba7291a295ea3c1979b40483f7544221790d53d76aadba99638689b88d9d1 with PNoLt x0 x2 x1 x3, and (x0 = x1) (PNoEq_ x0 x2 x3), PNoLt x1 x3 x0 x2.
Apply unknownprop_b3cbc8d84fae88a28c0902044988016197816c898f2ca1bfc7fbe4f41daf82f2 with x0, x1, x2, x3 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L8.
The subproof is completed by applying H9.
Assume H9: not (x3 x0).
Apply unknownprop_c33a8518d3fc8314286e0e0f7acdb4e408d0225cb1257a73db3a51552718bbdd with PNoLt x0 x2 x1 x3, and (x0 = x1) (PNoEq_ x0 x2 x3), PNoLt x1 x3 x0 x2.
Apply unknownprop_16a890d80e582f5663abfcfb5f5942164bae0e65476988fa667ed9ca882547fe with x1, x0, x3, x2 leaving 3 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_411872d9e62a7c55d0c5668a8fef0b88345bdb1b66aba80c7c02082fd86432f5 with x0, x2, x3.
The subproof is completed by applying L8.
The subproof is completed by applying H9.
Assume H6: x0 = x1.
Claim L7: binintersect x0 x1 = x0
Apply H6 with λ x4 x5 . binintersect x0 x4 = x0.
Apply unknownprop_5afda972c78302d86ad70171f9367780fa0c3403baf81f9e7aa674a8a6ec4541 with x0, x0.
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with x0.
Claim L8: PNoEq_ x0 x2 x3
Apply L7 with λ x4 x5 . PNoEq_ x4 x2 x3.
The subproof is completed by applying H5.
Apply unknownprop_55d33d10f6a09aaaea8e002117cf1820d9dc4418a57f04c18d4ec79694021a99 with PNoLt x0 x2 x1 x3, and (x0 = x1) (PNoEq_ x0 x2 x3), PNoLt x1 x3 x0 x2.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with x0 = x1, PNoEq_ x0 x2 x3 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L8.
Assume H6: In x1 x0.
Claim L7: ...
...
Claim L8: ...
...
Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with x2 x1, or (or (PNoLt x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3))) ... leaving 2 subgoals.
...
...
...
■