Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
SNo
x0
.
Assume H1:
∀ x1 .
x1
∈
SNoS_
omega
⟶
(
∀ x2 .
x2
∈
omega
⟶
SNoLt
(
abs_SNo
(
add_SNo
x1
(
minus_SNo
x0
)
)
)
(
eps_
x2
)
)
⟶
x1
=
x0
.
Assume H2:
∀ x1 .
x1
∈
omega
⟶
∃ x2 .
and
(
x2
∈
SNoS_
omega
)
(
and
(
SNoLt
x2
x0
)
(
SNoLt
x0
(
add_SNo
x2
(
eps_
x1
)
)
)
)
.
Claim L3:
...
...
Let x1 of type
ο
be given.
Assume H4:
∀ x2 .
and
(
x2
∈
setexp
(
SNoS_
omega
)
omega
)
(
∀ x3 .
x3
∈
omega
⟶
and
(
and
(
SNoLt
(
ap
x2
x3
)
x0
)
(
SNoLt
x0
(
add_SNo
(
ap
x2
x3
)
(
eps_
x3
)
)
)
)
(
∀ x4 .
x4
∈
x3
⟶
SNoLt
(
ap
x2
x4
)
(
ap
x2
x3
)
)
)
⟶
x1
.
Apply H4 with
lam
omega
(
λ x2 .
nat_primrec
(
prim0
(
λ x3 .
and
(
and
(
x3
∈
SNoS_
omega
)
(
SNoLt
x3
x0
)
)
(
SNoLt
x0
(
add_SNo
x3
(
eps_
0
)
)
)
)
)
(
λ x3 x4 .
prim0
(
λ x5 .
and
(
and
(
and
(
x5
∈
SNoS_
omega
)
(
SNoLt
x5
x0
)
)
(
SNoLt
x0
(
add_SNo
x5
(
eps_
(
ordsucc
x3
)
)
)
)
)
(
SNoLt
x4
x5
)
)
)
x2
)
.
Apply andI with
lam
omega
(
λ x2 .
nat_primrec
(
prim0
(
λ x3 .
and
(
and
(
x3
∈
SNoS_
omega
)
(
SNoLt
x3
x0
)
)
(
SNoLt
x0
(
add_SNo
x3
(
eps_
0
)
)
)
)
)
(
λ x3 x4 .
prim0
(
λ x5 .
and
(
and
(
and
(
x5
∈
SNoS_
omega
)
(
SNoLt
x5
x0
)
)
(
SNoLt
x0
(
add_SNo
x5
(
eps_
(
ordsucc
x3
)
)
)
)
)
(
SNoLt
x4
x5
)
)
)
x2
)
∈
setexp
(
SNoS_
omega
)
omega
,
∀ x2 .
...
⟶
and
(
and
(
SNoLt
(
ap
(
lam
omega
(
λ x3 .
nat_primrec
(
prim0
(
λ x4 .
and
(
and
(
x4
∈
SNoS_
omega
)
(
SNoLt
x4
x0
)
)
(
SNoLt
x0
(
add_SNo
x4
(
eps_
0
)
)
)
)
)
(
λ x4 x5 .
prim0
(
λ x6 .
and
(
and
(
and
(
x6
∈
SNoS_
omega
)
(
SNoLt
x6
x0
)
)
(
SNoLt
x0
(
add_SNo
x6
(
eps_
(
ordsucc
x4
)
)
)
)
)
(
SNoLt
x5
x6
)
)
)
x3
)
)
x2
)
x0
)
(
SNoLt
x0
(
add_SNo
(
ap
(
lam
omega
(
λ x3 .
nat_primrec
(
prim0
(
λ x4 .
and
(
and
(
x4
∈
SNoS_
omega
)
(
SNoLt
x4
x0
)
)
(
SNoLt
x0
(
add_SNo
x4
(
eps_
0
)
)
)
)
)
(
λ x4 x5 .
prim0
(
λ x6 .
and
...
...
)
)
...
)
)
...
)
...
)
)
)
...
leaving 2 subgoals.
...
...
■