Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: atleastp u3 (binintersect x0 x1).
Assume H1: atleastp x0 u5.
Assume H2: atleastp x1 u5.
Apply unknownprop_9a1a966f8c8e7afed78247e44fc56ee0d1da4c414d7d3d1e95e0c6b106051621 with x0, x1, λ x2 x3 . atleastp x3 u7.
Apply atleastp_tra with binunion x0 (setminus x1 x0), setsum u5 u2, u7 leaving 2 subgoals.
Apply unknownprop_94b237fc7b7d3bf1a0a078f7d057802d281bf3c46c36fd56a85d339ac0f07170 with x0, setminus x1 x0, u5, u2 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with u2, setminus x1 x0, atleastp (setminus x1 x0) u2 leaving 3 subgoals.
The subproof is completed by applying nat_2.
Assume H3: atleastp (setminus x1 x0) u2.
The subproof is completed by applying H3.
Assume H3: atleastp u3 (setminus x1 x0).
Apply FalseE with atleastp (setminus x1 x0) u2.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with u5 leaving 2 subgoals.
The subproof is completed by applying nat_5.
Apply atleastp_tra with u6, binunion (binintersect x0 x1) (setminus x1 x0), u5 leaving 2 subgoals.
Apply atleastp_tra with u6, setsum u3 u3, binunion (binintersect x0 x1) (setminus x1 x0) leaving 2 subgoals.
Apply equip_atleastp with u6, setsum u3 u3.
Apply unknownprop_0081651aea3d6f1c927139f33dafe364a67f12ece85830970354f85e4fe4a0a7 with λ x2 x3 . equip x2 (setsum u3 u3).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with u3, u3, u3, u3 leaving 4 subgoals.
The subproof is completed by applying nat_3.
The subproof is completed by applying nat_3.
The subproof is completed by applying equip_ref with u3.
The subproof is completed by applying equip_ref with u3.
Apply unknownprop_f59d6b770984c869c1e5c6fa6c966bf2e7f31a21d93561635565b3e8dc0de299 with u3, u3, binintersect x0 x1, setminus x1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: x2 ∈ binintersect x0 x1.
Assume H5: x2 ∈ setminus x1 x0.
Apply setminusE2 with x1, x0, x2 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply binintersectE1 with x0, x1, x2.
The subproof is completed by applying H4.
Apply binunion_com with binintersect x0 x1, setminus x1 x0, λ x2 x3 . atleastp x3 u5.
Apply binintersect_com with x0, x1, λ x2 x3 . atleastp (binunion (setminus x1 x0) x3) u5.
Apply unknownprop_d80a5cdd35aff682e6edc37d56782355ff9ceaa0a69a0eeabe526b6102deafb2 with x1, x0, λ x2 x3 . atleastp x2 u5.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Assume H4: x2 ∈ setminus x1 x0.
Apply setminusE2 with x1, x0, x2 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Apply equip_atleastp with setsum u5 u2, u7.
Apply equip_sym with u7, setsum u5 u2.
Apply unknownprop_f535b7e55315533489247ef446da714ae119b4416908c171a0f36b33b8dd4dc1 with λ x2 x3 . equip x2 (setsum u5 u2).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with u5, u2, u5, u2 leaving 4 subgoals.
The subproof is completed by applying nat_5.
The subproof is completed by applying nat_2.
The subproof is completed by applying equip_ref with u5.
The subproof is completed by applying equip_ref with u2.
■