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.
Assume H0:
SNoCutP
x0
x1
.
Assume H1:
SNoCutP
x2
x3
.
Claim L2:
...
...
Claim L3:
...
...
Claim L4:
...
...
Apply H0 with
SNoCutP
(
binunion
{
add_SNo
x4
(
SNoCut
x2
x3
)
|x4 ∈
x0
}
{
add_SNo
(
SNoCut
x0
x1
)
x4
|x4 ∈
x2
}
)
(
binunion
{
add_SNo
x4
(
SNoCut
x2
x3
)
|x4 ∈
x1
}
{
add_SNo
(
SNoCut
x0
x1
)
x4
|x4 ∈
x3
}
)
.
Assume H5:
and
(
∀ x4 .
x4
∈
x0
⟶
SNo
x4
)
(
∀ x4 .
x4
∈
x1
⟶
SNo
x4
)
.
Apply H5 with
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x1
⟶
SNoLt
x4
x5
)
⟶
SNoCutP
(
binunion
{
add_SNo
x4
(
SNoCut
x2
x3
)
|x4 ∈
x0
}
{
add_SNo
(
SNoCut
x0
x1
)
x4
|x4 ∈
x2
}
)
(
binunion
{
add_SNo
x4
(
SNoCut
x2
x3
)
|x4 ∈
x1
}
{
add_SNo
(
SNoCut
x0
x1
)
x4
|x4 ∈
x3
}
)
.
Assume H6:
∀ x4 .
x4
∈
x0
⟶
SNo
x4
.
Assume H7:
∀ x4 .
x4
∈
x1
⟶
SNo
x4
.
Assume H8:
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x1
⟶
SNoLt
x4
x5
.
Apply H1 with
SNoCutP
(
binunion
{
add_SNo
x4
(
SNoCut
x2
x3
)
|x4 ∈
x0
}
{
add_SNo
(
SNoCut
x0
x1
)
x4
|x4 ∈
x2
}
)
(
binunion
{
add_SNo
x4
(
SNoCut
x2
x3
)
|x4 ∈
x1
}
{
add_SNo
(
SNoCut
x0
x1
)
x4
|x4 ∈
x3
}
)
.
Assume H9:
and
(
∀ x4 .
x4
∈
x2
⟶
SNo
x4
)
(
∀ x4 .
x4
∈
x3
⟶
SNo
x4
)
.
Apply H9 with
(
∀ x4 .
x4
∈
x2
⟶
∀ x5 .
x5
∈
x3
⟶
SNoLt
x4
x5
)
⟶
SNoCutP
(
binunion
{
add_SNo
x4
(
SNoCut
x2
x3
)
|x4 ∈
x0
}
{
add_SNo
(
SNoCut
x0
x1
)
x4
|x4 ∈
x2
}
)
(
binunion
{
add_SNo
x4
(
SNoCut
x2
x3
)
|x4 ∈
x1
}
{
add_SNo
(
SNoCut
x0
x1
)
x4
|x4 ∈
x3
}
)
.
Assume H10:
∀ x4 .
x4
∈
x2
⟶
SNo
x4
.
Assume H11:
∀ x4 .
x4
∈
x3
⟶
SNo
x4
.
Assume H12:
∀ x4 .
x4
∈
x2
⟶
∀ x5 .
x5
∈
x3
⟶
SNoLt
x4
x5
.
Apply and3I with
∀ x4 .
x4
∈
binunion
{
add_SNo
x5
(
SNoCut
x2
x3
)
|x5 ∈
x0
}
{
add_SNo
(
SNoCut
x0
x1
)
x5
|x5 ∈
x2
}
⟶
SNo
x4
,
∀ x4 .
x4
∈
binunion
{
add_SNo
x5
(
SNoCut
x2
x3
)
|x5 ∈
x1
}
{
add_SNo
(
SNoCut
x0
x1
)
...
|x5 ∈
x3
}
⟶
SNo
x4
,
...
leaving 3 subgoals.
...
...
...
■