Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
x0
∈
setexp
real
omega
.
Let x1 of type
ι
be given.
Assume H1:
x1
∈
setexp
real
omega
.
Assume H2:
∀ x2 .
x2
∈
omega
⟶
and
(
and
(
SNoLe
(
ap
x0
x2
)
(
ap
x1
x2
)
)
(
SNoLe
(
ap
x0
x2
)
(
ap
x0
(
ordsucc
x2
)
)
)
)
(
SNoLe
(
ap
x1
(
ordsucc
x2
)
)
(
ap
x1
x2
)
)
.
Apply dneg with
∃ x2 .
and
(
x2
∈
real
)
(
∀ x3 .
x3
∈
omega
⟶
and
(
SNoLe
(
ap
x0
x3
)
x2
)
(
SNoLe
x2
(
ap
x1
x3
)
)
)
.
Assume H3:
not
(
∃ x2 .
and
(
x2
∈
real
)
(
∀ x3 .
x3
∈
omega
⟶
and
(
SNoLe
(
ap
x0
x3
)
x2
)
(
SNoLe
x2
(
ap
x1
x3
)
)
)
)
.
Claim L4:
...
...
Claim L5:
...
...
Claim L6:
...
...
Claim L7:
...
...
Apply SNoCutP_SNoCut_impred with
{x2 ∈
SNoS_
omega
|
∃ x3 .
and
(
x3
∈
omega
)
(
SNoLt
x2
(
ap
x0
x3
)
)
}
,
{x2 ∈
SNoS_
omega
|
∃ x3 .
and
(
x3
∈
omega
)
(
SNoLt
(
ap
x1
x3
)
x2
)
}
,
False
leaving 2 subgoals.
The subproof is completed by applying L7.
Assume H8:
SNo
(
SNoCut
{x2 ∈
SNoS_
omega
|
∃ x3 .
and
(
x3
∈
omega
)
(
SNoLt
x2
(
ap
x0
x3
)
)
}
{x2 ∈
SNoS_
omega
|
∃ x3 .
and
(
x3
∈
omega
)
(
SNoLt
(
ap
x1
x3
)
x2
)
}
)
.
Assume H9:
SNoLev
(
SNoCut
{x2 ∈
SNoS_
omega
|
∃ x3 .
and
(
x3
∈
omega
)
(
SNoLt
x2
(
ap
x0
x3
)
)
}
{x2 ∈
SNoS_
omega
|
∃ x3 .
and
(
x3
∈
omega
)
(
SNoLt
(
ap
x1
x3
)
x2
)
}
)
∈
ordsucc
(
binunion
(
famunion
{x2 ∈
SNoS_
omega
|
∃ x3 .
and
(
x3
∈
omega
)
(
SNoLt
x2
(
ap
x0
x3
)
)
}
(
λ x2 .
ordsucc
(
SNoLev
x2
)
)
)
(
famunion
{x2 ∈
SNoS_
omega
|
∃ x3 .
and
(
x3
∈
omega
)
(
SNoLt
(
ap
x1
x3
)
x2
)
}
(
λ x2 .
ordsucc
(
SNoLev
x2
)
)
)
)
.
Assume H10:
∀ x2 .
x2
∈
{x3 ∈
SNoS_
omega
|
∃ x4 .
and
(
x4
∈
omega
)
(
SNoLt
x3
(
ap
x0
x4
)
)
}
⟶
SNoLt
x2
(
SNoCut
{x3 ∈
SNoS_
omega
|
∃ x4 .
and
(
x4
∈
omega
)
(
SNoLt
x3
(
ap
x0
x4
)
)
}
{x3 ∈
SNoS_
omega
|
∃ x4 .
and
(
x4
∈
omega
)
(
SNoLt
(
ap
x1
x4
)
x3
)
}
)
.
Assume H11:
∀ x2 .
...
⟶
SNoLt
(
SNoCut
{x3 ∈
SNoS_
omega
|
∃ x4 .
and
(
x4
∈
omega
)
(
SNoLt
x3
(
ap
x0
x4
)
)
}
...
)
...
.
...
■