Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Assume H1: ∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3).
Assume H2: ∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)).
Let x1 of type ι be given.
Assume H3: x1 ∈ u18.
Apply unknownprop_e218ed8cf74f73d11b13279ecb43db2e902573ebd411cc1f7c1f71620f4a5da3 with DirGraphOutNeighbors u18 x0 x1, u5 leaving 2 subgoals.
Apply unknownprop_7fc58161c06ac759b74ed554400e74038cd0a5c3177ca714d699b1cb30814d29 with u18, x0, u5, x1 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying nat_5.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with u4, DirGraphOutNeighbors u18 x0 x1, atleastp u5 (DirGraphOutNeighbors u18 x0 x1) leaving 3 subgoals.
The subproof is completed by applying nat_4.
Assume H4: atleastp (DirGraphOutNeighbors u18 x0 x1) u4.
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Apply L9 with atleastp u5 (DirGraphOutNeighbors u18 x0 x1).
Let x2 of type ι be given.
Assume H10: x2 ∈ DirGraphOutNeighbors u18 x0 x1.
Apply SepE with u18, λ x3 . and (x1 = x3 ⟶ ∀ x4 : ο . x4) (x0 x1 x3), x2, atleastp u5 (DirGraphOutNeighbors u18 x0 x1) leaving 2 subgoals.
The subproof is completed by applying H10.
Assume H11: x2 ∈ u18.
Assume H12: and (x1 = x2 ⟶ ∀ x3 : ο . x3) (x0 x1 x2).
Apply H12 with atleastp u5 (DirGraphOutNeighbors u18 x0 x1).
Assume H13: x1 = x2 ⟶ ∀ x3 : ο . x3.
Assume H14: x0 x1 x2.
Claim L15: ...
...
Claim L16: ...
...
Apply L16 with atleastp u5 (DirGraphOutNeighbors u18 x0 x1).
Let x3 of type ι be given.
Assume H17: (λ x4 . and (x4 ⊆ DirGraphOutNeighbors u18 x0 x2) (and (nIn x1 x4) (equip x4 u3))) x3.
Apply H17 with atleastp u5 (DirGraphOutNeighbors u18 x0 x1).
Assume H18: x3 ⊆ DirGraphOutNeighbors u18 x0 x2.
Assume H19: and (nIn x1 x3) (equip x3 u3).
Apply H19 with atleastp u5 (DirGraphOutNeighbors u18 x0 x1).
Assume H20: nIn x1 x3.
Assume H21: equip x3 u3.
Claim L22: ...
...
Claim L23: ...
...
Apply H2 with binunion (setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2)) x3, atleastp u5 (DirGraphOutNeighbors u18 x0 x1) leaving 3 subgoals.
Apply binunion_Subq_min with setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2), x3, u18 leaving 2 subgoals.
Apply Subq_tra with setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2), DirGraphOutNeighbors u18 x0 x1, u18 leaving 2 subgoals.
The subproof is completed by applying setminus_Subq with DirGraphOutNeighbors u18 x0 x1, Sing x2.
The subproof is completed by applying Sep_Subq with u18, λ x4 . and (x1 = x4 ⟶ ∀ x5 : ο . x5) (x0 x1 x4).
Apply Subq_tra with x3, DirGraphOutNeighbors u18 x0 x2, u18 leaving 2 subgoals.
The subproof is completed by applying H18.
The subproof is completed by applying Sep_Subq with u18, ....
...
...
...
■