Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
→
ι
→
ο
be given.
Assume H0:
∀ x2 x3 .
x1
x2
x3
⟶
x1
x3
x2
.
Let x2 of type
ι
be given.
Let x3 of type
ι
be given.
Assume H1:
x2
∈
x0
.
Let x4 of type
ι
be given.
Assume H2:
nat_p
x4
.
Assume H3:
∀ x5 .
x5
∈
x0
⟶
(
x5
=
x2
⟶
∀ x6 : ο .
x6
)
⟶
not
(
x1
x5
x2
)
⟶
or
(
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
x4
)
(
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
(
ordsucc
x4
)
)
.
Assume H4:
∀ x5 .
x5
∈
{x6 ∈
setminus
x0
(
binunion
(
DirGraphOutNeighbors
x0
x1
x2
)
(
Sing
x2
)
)
|
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x6
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
x4
}
⟶
not
(
x1
x3
x5
)
.
Assume H5:
∀ x5 .
x5
∈
setminus
(
DirGraphOutNeighbors
x0
x1
x3
)
(
Sing
x2
)
⟶
not
(
x1
x2
x5
)
.
Let x5 of type
ι
be given.
Assume H6:
x5
∈
setminus
(
DirGraphOutNeighbors
x0
x1
x3
)
(
Sing
x2
)
.
Apply setminusE with
DirGraphOutNeighbors
x0
x1
x3
,
Sing
x2
,
x5
,
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
(
ordsucc
x4
)
leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7:
x5
∈
DirGraphOutNeighbors
x0
x1
x3
.
Assume H8:
nIn
x5
(
Sing
x2
)
.
Apply SepE with
x0
,
λ x6 .
and
(
x3
=
x6
⟶
∀ x7 : ο .
x7
)
(
x1
x3
x6
)
,
x5
,
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
(
ordsucc
x4
)
leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H9:
x5
∈
x0
.
Assume H10:
and
(
x3
=
x5
⟶
∀ x6 : ο .
x6
)
(
x1
x3
x5
)
.
Apply H10 with
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
(
ordsucc
x4
)
.
Assume H11:
x3
=
x5
⟶
∀ x6 : ο .
x6
.
Assume H12:
x1
x3
x5
.
Claim L13:
...
...
Claim L14:
...
...
Apply H3 with
x5
,
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
(
ordsucc
x4
)
leaving 5 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
Assume H15:
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
x4
.
Apply FalseE with
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
(
ordsucc
x4
)
.
Apply H4 with
x5
leaving 2 subgoals.
Apply SepI with
setminus
x0
(
binunion
(
DirGraphOutNeighbors
x0
x1
x2
)
(
Sing
x2
)
)
,
λ x6 .
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x6
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
x4
,
x5
leaving 2 subgoals.
Apply setminusI with
x0
,
binunion
(
DirGraphOutNeighbors
x0
...
...
)
...
,
...
leaving 2 subgoals.
...
...
...
...
...
■