Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: atleastp u13 x0.
Let x1 of type ιιο be given.
Assume H1: ∀ x2 x3 . x1 x2 x3x1 x3 x2.
Assume H2: ∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4).
Assume H3: ∀ x2 . x2x0atleastp u5 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)not (x1 x3 x4)).
Let x2 of type ι be given.
Assume H4: x2x0.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with u3, DirGraphOutNeighbors x0 x1 x2, atleastp u4 (DirGraphOutNeighbors x0 x1 x2) leaving 3 subgoals.
The subproof is completed by applying nat_3.
Assume H5: atleastp (DirGraphOutNeighbors x0 x1 x2) u3.
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Apply FalseE with atleastp u4 (DirGraphOutNeighbors x0 x1 x2).
Apply L8 with x1, False leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H9: ∃ x3 . and (x3setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))) (and (equip u3 x3) (∀ x4 . x4x3∀ x5 . x5x3(x4 = x5∀ x6 : ο . x6)x1 x4 x5)).
Apply H9 with False.
Let x3 of type ι be given.
Assume H10: (λ x4 . and (x4setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))) (and (equip u3 x4) (∀ x5 . x5x4∀ x6 . x6x4(x5 = x6∀ x7 : ο . x7)x1 x5 x6))) x3.
Apply H10 with False.
Assume H11: x3setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2)).
Assume H12: and (equip u3 x3) (∀ x4 . x4x3∀ x5 . x5x3(x4 = x5∀ x6 : ο . x6)x1 x4 x5).
Apply H12 with False.
Assume H13: equip u3 x3.
Assume H14: ∀ x4 . x4x3∀ x5 . x5x3(x4 = x5∀ x6 : ο . x6)x1 x4 x5.
Claim L15: x3x0
Apply Subq_tra with x3, setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2)), x0 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying setminus_Subq with x0, binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2).
Claim L16: atleastp u3 x3
Apply equip_atleastp with u3, x3.
The subproof is completed by applying H13.
Apply H2 with x3 leaving 3 subgoals.
The subproof is completed by applying L15.
The subproof is completed by applying L16.
The subproof is completed by applying H14.
Assume H9: ∃ x3 . and (x3setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))) (and (equip ... ...) ...).
...
...