Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιιο be given.
Assume H0: ∀ x1 . x1u12atleastp u5 x1not (∀ x2 . x2x1∀ x3 . x3x1not (x0 x2 x3)).
Let x1 of type ι be given.
Assume H1: x1u16.
Assume H2: atleastp u6 x1.
Assume H3: ∀ x2 . x2x1∀ x3 . x3x1not (x0 x2 x3).
Claim L4: ...
...
Claim L5: x1 = binunion (setminus x1 u12) (binintersect x1 u12)
Apply set_ext with x1, binunion (setminus x1 u12) (binintersect x1 u12) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H5: x2x1.
Apply xm with x2u12, x2binunion (setminus x1 u12) (binintersect x1 u12) leaving 2 subgoals.
Assume H6: x2u12.
Apply binunionI2 with setminus x1 u12, binintersect x1 u12, x2.
Apply binintersectI with x1, u12, x2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Assume H6: nIn x2 u12.
Apply binunionI1 with setminus x1 u12, binintersect x1 u12, x2.
Apply setminusI with x1, u12, x2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Let x2 of type ι be given.
Assume H5: x2binunion (setminus x1 u12) (binintersect ... ...).
...
Claim L6: binintersect x1 u12u12
The subproof is completed by applying binintersect_Subq_2 with x1, u12.
Claim L7: not (atleastp u5 (binintersect x1 u12))
Assume H7: atleastp u5 (binintersect x1 u12).
Apply H0 with binintersect x1 u12 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H7.
Let x2 of type ι be given.
Assume H8: x2binintersect x1 u12.
Let x3 of type ι be given.
Assume H9: x3binintersect x1 u12.
Apply H3 with x2, x3 leaving 2 subgoals.
Apply binintersectE1 with x1, u12, x2.
The subproof is completed by applying H8.
Apply binintersectE1 with x1, u12, x3.
The subproof is completed by applying H9.
Claim L8: atleastp (binintersect x1 u12) u4
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with u4, binintersect x1 u12, atleastp (binintersect x1 u12) u4 leaving 3 subgoals.
The subproof is completed by applying nat_4.
Assume H8: atleastp (binintersect x1 u12) u4.
The subproof is completed by applying H8.
Assume H8: atleastp u5 (binintersect x1 u12).
Apply FalseE with atleastp (binintersect x1 u12) u4.
Apply L7.
The subproof is completed by applying H8.
Claim L9: not (atleastp (setminus x1 u12) u1)
Assume H9: atleastp (setminus x1 u12) u1.
Claim L10: atleastp x1 u5
Apply L5 with λ x2 x3 . atleastp x3 u5.
Apply nat_setsum_ordsucc with u4, λ x2 x3 . atleastp (binunion (setminus x1 u12) (binintersect x1 u12)) x2 leaving 2 subgoals.
The subproof is completed by applying nat_4.
Apply unknownprop_94b237fc7b7d3bf1a0a078f7d057802d281bf3c46c36fd56a85d339ac0f07170 with setminus x1 u12, binintersect x1 u12, u1, u4 leaving 3 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying L8.
The subproof is completed by applying L4.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with u5 leaving 2 subgoals.
The subproof is completed by applying nat_5.
Apply atleastp_tra with u6, x1, u5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying L10.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with u1, setminus x1 u12, atleastp u2 (setminus x1 u12) leaving 3 subgoals.
The subproof is completed by applying nat_1.
Assume H10: atleastp (setminus x1 u12) u1.
Apply FalseE with atleastp u2 (setminus x1 u12).
Apply L9.
The subproof is completed by applying H10.
Assume H10: atleastp u2 (setminus x1 u12).
The subproof is completed by applying H10.