Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιιο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2x0 x2 x1.
Assume H1: ∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3).
Assume H2: ∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)).
Let x1 of type ι be given.
Assume H3: x1u18.
Let x2 of type ι be given.
Assume H4: x2DirGraphOutNeighbors u18 x0 x1.
Apply unknownprop_997b324045b1165b0cf38788927ff324ddb3a505c8b91e290586e4dd5480f2bd with DirGraphOutNeighbors u18 x0 x2, u4, x1 leaving 2 subgoals.
Apply unknownprop_426b271b8453605fe796f284fb15405fbff198d07b0c3dc7b8c218dee82a5c65 with u18, x0, x1, x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_942eb02a74c10f16602e1ae1f344c3023e05004e91bcaa34f489f7c49867be93 with x0, x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply SepE1 with u18, λ x3 . and (x1 = x3∀ x4 : ο . x4) (x0 x1 x3), x2.
The subproof is completed by applying H4.