Search for blocks/addresses/...
Proofgold Proof
pf
Apply nat_complete_ind with
λ x0 .
add_SNo
(
eps_
(
ordsucc
x0
)
)
(
eps_
(
ordsucc
x0
)
)
=
eps_
x0
.
Let x0 of type
ι
be given.
Assume H0:
nat_p
x0
.
Assume H1:
∀ x1 .
x1
∈
x0
⟶
add_SNo
(
eps_
(
ordsucc
x1
)
)
(
eps_
(
ordsucc
x1
)
)
=
eps_
x1
.
Claim L2:
...
...
Apply eps_SNoCut with
x0
,
λ x1 x2 .
add_SNo
(
eps_
(
ordsucc
x0
)
)
(
eps_
(
ordsucc
x0
)
)
=
x2
leaving 2 subgoals.
The subproof is completed by applying L2.
Claim L3:
...
...
Claim L4:
...
...
Apply add_SNo_eq with
eps_
(
ordsucc
x0
)
,
eps_
(
ordsucc
x0
)
,
λ x1 x2 .
x2
=
SNoCut
(
Sing
0
)
(
prim5
x0
eps_
)
leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
Apply SNoCut_ext with
binunion
{
add_SNo
x1
(
eps_
(
ordsucc
x0
)
)
|x1 ∈
SNoL
(
eps_
(
ordsucc
x0
)
)
}
{
add_SNo
(
eps_
(
ordsucc
x0
)
)
x1
|x1 ∈
SNoL
(
eps_
(
ordsucc
x0
)
)
}
,
binunion
{
add_SNo
x1
(
eps_
(
ordsucc
x0
)
)
|x1 ∈
SNoR
(
eps_
(
ordsucc
x0
)
)
}
{
add_SNo
(
eps_
(
ordsucc
x0
)
)
x1
|x1 ∈
SNoR
(
eps_
(
ordsucc
x0
)
)
}
,
Sing
0
,
{
eps_
x1
|x1 ∈
x0
}
leaving 6 subgoals.
Apply add_SNo_SNoCutP with
eps_
(
ordsucc
x0
)
,
eps_
(
ordsucc
x0
)
leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
Apply eps_SNoCutP with
x0
.
The subproof is completed by applying L2.
Claim L5:
...
...
Let x1 of type
ι
be given.
Assume H6:
x1
∈
binunion
{
add_SNo
x2
(
eps_
(
ordsucc
x0
)
)
|x2 ∈
SNoL
(
eps_
(
ordsucc
x0
)
)
}
{
add_SNo
(
eps_
(
ordsucc
x0
)
)
x2
|x2 ∈
SNoL
(
eps_
(
ordsucc
x0
)
)
}
.
Apply eps_SNoCut with
x0
,
λ x2 x3 .
SNoLt
x1
x2
leaving 2 subgoals.
The subproof is completed by applying L2.
Apply binunionE with
{
add_SNo
x2
(
eps_
(
ordsucc
x0
)
)
|x2 ∈
SNoL
(
eps_
(
ordsucc
x0
)
)
}
,
{
add_SNo
(
eps_
(
ordsucc
x0
)
)
x2
|x2 ∈
SNoL
(
eps_
(
ordsucc
x0
)
)
}
,
x1
,
SNoLt
x1
(
eps_
x0
)
leaving 3 subgoals.
The subproof is completed by applying H6.
Assume H7:
x1
∈
{
add_SNo
x2
(
eps_
(
ordsucc
x0
)
)
|x2 ∈
SNoL
(
eps_
(
ordsucc
x0
)
)
}
.
Apply ReplE_impred with
SNoL
(
eps_
(
ordsucc
x0
)
)
,
λ x2 .
add_SNo
x2
(
eps_
(
ordsucc
x0
)
)
,
x1
,
SNoLt
x1
(
eps_
x0
)
leaving 2 subgoals.
The subproof is completed by applying H7.
Let x2 of type
ι
be given.
Assume H8:
x2
∈
SNoL
(
eps_
(
ordsucc
x0
)
)
.
Assume H9:
x1
=
add_SNo
x2
(
eps_
(
ordsucc
x0
)
)
.
Apply H9 with
λ x3 x4 .
SNoLt
x4
(
eps_
x0
)
.
Apply andEL with
SNoLt
(
add_SNo
x2
(
eps_
(
ordsucc
x0
)
)
)
(
eps_
x0
)
,
SNoLt
(
add_SNo
(
eps_
(
ordsucc
x0
)
)
x2
)
(
eps_
x0
)
.
Apply L5 with
x2
.
The subproof is completed by applying H8.
Assume H7:
x1
∈
{
add_SNo
(
eps_
(
ordsucc
x0
)
)
x2
|x2 ∈
SNoL
(
eps_
(
ordsucc
x0
)
)
}
.
Apply ReplE_impred with
SNoL
(
eps_
(
ordsucc
x0
)
)
,
λ x2 .
add_SNo
(
eps_
(
ordsucc
x0
)
)
x2
,
x1
,
SNoLt
x1
(
eps_
x0
)
leaving 2 subgoals.
The subproof is completed by applying H7.
Let x2 of type
ι
be given.
Assume H8:
x2
∈
SNoL
(
eps_
(
ordsucc
x0
)
)
.
Assume H9:
...
.
...
...
...
...
■