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.
Let x4 of type ι be given.
Assume H0: binunion x0 x1 = x2.
Assume H1: ∀ x5 . x5 ∈ x0 ⟶ nIn x5 x1.
Assume H2: nat_p x3.
Assume H3: nat_p x4.
Assume H4: equip x0 x3.
Assume H5: equip x2 (add_nat x3 x4).
Apply unknownprop_e218ed8cf74f73d11b13279ecb43db2e902573ebd411cc1f7c1f71620f4a5da3 with x1, x4 leaving 2 subgoals.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with x4, x1, atleastp x1 x4 leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H6: atleastp x1 x4.
The subproof is completed by applying H6.
Assume H6: atleastp (ordsucc x4) x1.
Apply FalseE with atleastp x1 x4.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with add_nat x3 x4 leaving 2 subgoals.
Apply add_nat_p with x3, x4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply atleastp_tra with ordsucc (add_nat x3 x4), binunion x0 x1, add_nat x3 x4 leaving 2 subgoals.
Apply atleastp_tra with ordsucc (add_nat x3 x4), setsum x3 (ordsucc x4), binunion x0 x1 leaving 2 subgoals.
Apply add_nat_SR with x3, x4, λ x5 x6 . atleastp x5 (setsum x3 (ordsucc x4)) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply equip_atleastp with add_nat x3 (ordsucc x4), setsum x3 (ordsucc x4).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with x3, ordsucc x4, x3, ordsucc x4 leaving 4 subgoals.
The subproof is completed by applying H2.
Apply nat_ordsucc with x4.
The subproof is completed by applying H3.
The subproof is completed by applying equip_ref with x3.
The subproof is completed by applying equip_ref with ordsucc x4.
Apply unknownprop_f59d6b770984c869c1e5c6fa6c966bf2e7f31a21d93561635565b3e8dc0de299 with x3, ordsucc x4, x0, x1 leaving 3 subgoals.
Apply equip_atleastp with x3, x0.
Apply equip_sym with x0, x3.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H1.
Apply H0 with λ x5 x6 . atleastp x6 (add_nat x3 x4).
Apply equip_atleastp with x2, add_nat x3 x4.
The subproof is completed by applying H5.
Apply nat_inv with x4, atleastp x4 x1 leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H6: x4 = 0.
Apply H6 with λ x5 x6 . atleastp x6 x1.
The subproof is completed by applying unknownprop_b7030c4d179dca75b1c0a5a2dab6748493aebd2d7f37d4cf7a0d3bf2081224c9 with x1.
Assume H6: ∃ x5 . and (nat_p x5) (x4 = ordsucc x5).
Apply H6 with atleastp x4 x1.
Let x5 of type ι be given.
Assume H7: (λ x6 . and (nat_p x6) (x4 = ordsucc x6)) x5.
Apply H7 with atleastp x4 x1.
Assume H8: nat_p x5.
Assume H9: x4 = ordsucc x5.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with x5, x1, atleastp x4 x1 leaving 3 subgoals.
The subproof is completed by applying H8.
Assume H10: atleastp x1 x5.
Apply FalseE with atleastp x4 x1.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with add_nat x3 x5 leaving 2 subgoals.
Apply add_nat_p with x3, x5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H8.
Apply atleastp_tra with ordsucc (add_nat x3 x5), binunion x0 x1, add_nat x3 x5 leaving 2 subgoals.
Apply equip_atleastp with ordsucc (add_nat x3 x5), binunion x0 x1.
Apply equip_sym with binunion x0 x1, ordsucc (add_nat x3 x5).
Apply add_nat_SR with x3, x5, λ x6 x7 . equip (binunion x0 x1) x6 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply H9 with λ x6 x7 . equip (binunion x0 x1) (add_nat x3 x6).
Apply H0 with λ x6 x7 . equip x7 (add_nat x3 x4).
The subproof is completed by applying H5.
Apply atleastp_tra with binunion x0 x1, setsum x3 x5, add_nat x3 x5 leaving 2 subgoals.
Apply unknownprop_8805a75f81012de0423e9173532fc074fb73b80e451597fde52287a4721fb204 with x0, x1, x3, x5 leaving 2 subgoals.
Apply equip_atleastp with x0, x3.
The subproof is completed by applying H4.
The subproof is completed by applying H10.
Apply equip_atleastp with setsum x3 x5, add_nat x3 x5.
Apply equip_sym with add_nat x3 x5, setsum x3 x5.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with x3, x5, x3, x5 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H8.
The subproof is completed by applying equip_ref with x3.
The subproof is completed by applying equip_ref with x5.
Assume H10: atleastp (ordsucc ...) ....
...
■