Search for blocks/addresses/...
Proofgold Proof
pf
Claim L0:
∀ x0 .
...
⟶
∀ x1 .
...
⟶
∀ x2 x3 :
ι →
ι → ι
.
...
⟶
...
⟶
(
λ x4 x5 .
λ x6 :
ι →
ι → ι
.
SNoCut
(
binunion
{
add_SNo
(
x6
(
ap
x7
0
)
x5
)
(
add_SNo
(
x6
x4
(
ap
x7
1
)
)
(
minus_SNo
(
x6
(
ap
x7
0
)
(
ap
x7
1
)
)
)
)
|x7 ∈
setprod
(
SNoL
x4
)
(
SNoL
x5
)
}
{
add_SNo
(
x6
(
ap
x7
0
)
x5
)
(
add_SNo
(
x6
x4
(
ap
x7
1
)
)
(
minus_SNo
(
x6
(
ap
x7
0
)
(
ap
x7
1
)
)
)
)
|x7 ∈
setprod
(
SNoR
x4
)
(
SNoR
x5
)
}
)
(
binunion
{
add_SNo
(
x6
(
ap
x7
0
)
x5
)
(
add_SNo
(
x6
x4
(
ap
x7
1
)
)
(
minus_SNo
(
x6
(
ap
x7
0
)
(
ap
x7
1
)
)
)
)
|x7 ∈
setprod
(
SNoL
x4
)
(
SNoR
x5
)
}
{
add_SNo
(
x6
(
ap
x7
0
)
x5
)
(
add_SNo
(
x6
x4
(
ap
x7
1
)
)
(
minus_SNo
(
x6
(
ap
x7
0
)
(
ap
x7
1
)
)
)
)
|x7 ∈
setprod
(
SNoR
x4
)
(
SNoL
x5
)
}
)
)
x0
x1
x2
=
(
λ x4 x5 .
λ x6 :
ι →
ι → ι
.
SNoCut
(
binunion
{
add_SNo
(
x6
(
ap
x7
0
)
x5
)
(
add_SNo
(
x6
x4
(
ap
x7
1
)
)
(
minus_SNo
(
x6
(
ap
x7
0
)
(
ap
x7
1
)
)
)
)
|x7 ∈
setprod
(
SNoL
x4
)
(
SNoL
x5
)
}
{
...
|x7 ∈
setprod
...
...
}
)
...
)
...
...
...
...
Apply SNo_rec2_eq with
λ x0 x1 .
λ x2 :
ι →
ι → ι
.
SNoCut
(
binunion
{
add_SNo
(
x2
(
ap
x3
0
)
x1
)
(
add_SNo
(
x2
x0
(
ap
x3
1
)
)
(
minus_SNo
(
x2
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoL
x0
)
(
SNoL
x1
)
}
{
add_SNo
(
x2
(
ap
x3
0
)
x1
)
(
add_SNo
(
x2
x0
(
ap
x3
1
)
)
(
minus_SNo
(
x2
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoR
x0
)
(
SNoR
x1
)
}
)
(
binunion
{
add_SNo
(
x2
(
ap
x3
0
)
x1
)
(
add_SNo
(
x2
x0
(
ap
x3
1
)
)
(
minus_SNo
(
x2
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoL
x0
)
(
SNoR
x1
)
}
{
add_SNo
(
x2
(
ap
x3
0
)
x1
)
(
add_SNo
(
x2
x0
(
ap
x3
1
)
)
(
minus_SNo
(
x2
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoR
x0
)
(
SNoL
x1
)
}
)
.
The subproof is completed by applying L0.
■