Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
(
ι
→
ι
) →
ι
be given.
Assume H0:
∀ x1 .
SNo
x1
⟶
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
.
Let x1 of type
ι
be given.
Assume H1:
SNo
x1
.
Claim L2:
∀ x2 .
∀ x3 x4 :
ι →
ι → ι
.
...
⟶
(
λ x5 .
λ x6 :
ι →
ι → ι
.
If_ii
(
ordinal
x5
)
(
λ x7 .
If_i
(
x7
∈
SNoS_
(
ordsucc
x5
)
)
(
x0
x7
(
λ x8 .
x6
(
SNoLev
x8
)
x8
)
)
(
prim0
(
λ x8 .
True
)
)
)
(
λ x7 .
prim0
...
)
)
...
...
=
...
...
Apply In_rec_ii_eq with
λ x2 .
λ x3 :
ι →
ι → ι
.
If_ii
(
ordinal
x2
)
(
λ x4 .
If_i
(
x4
∈
SNoS_
(
ordsucc
x2
)
)
(
x0
x4
(
λ x5 .
x3
(
SNoLev
x5
)
x5
)
)
(
prim0
(
λ x5 .
True
)
)
)
(
λ x4 .
prim0
(
λ x5 .
True
)
)
,
SNoLev
x1
,
λ x2 x3 :
ι → ι
.
x3
x1
=
x0
x1
(
λ x4 .
In_rec_ii
(
λ x5 .
λ x6 :
ι →
ι → ι
.
If_ii
(
ordinal
x5
)
(
λ x7 .
If_i
(
x7
∈
SNoS_
(
ordsucc
x5
)
)
(
x0
x7
(
λ x8 .
x6
(
SNoLev
x8
)
x8
)
)
(
prim0
(
λ x8 .
True
)
)
)
(
λ x7 .
prim0
(
λ x8 .
True
)
)
)
(
SNoLev
x4
)
x4
)
leaving 2 subgoals.
The subproof is completed by applying L2.
Claim L3:
ordinal
(
SNoLev
x1
)
Apply SNoLev_ordinal with
x1
.
The subproof is completed by applying H1.
Apply If_ii_1 with
ordinal
(
SNoLev
x1
)
,
λ x2 .
If_i
(
x2
∈
SNoS_
(
ordsucc
(
SNoLev
x1
)
)
)
(
x0
x2
(
λ x3 .
In_rec_ii
(
λ x4 .
λ x5 :
ι →
ι → ι
.
If_ii
(
ordinal
x4
)
(
λ x6 .
If_i
(
x6
∈
SNoS_
(
ordsucc
x4
)
)
(
x0
x6
(
λ x7 .
x5
(
SNoLev
x7
)
x7
)
)
(
prim0
(
λ x7 .
True
)
)
)
(
λ x6 .
prim0
(
λ x7 .
True
)
)
)
(
SNoLev
x3
)
x3
)
)
(
prim0
(
λ x3 .
True
)
)
,
λ x2 .
prim0
(
λ x3 .
True
)
,
λ x2 x3 :
ι → ι
.
x3
x1
=
x0
x1
(
λ x4 .
In_rec_ii
(
λ x5 .
λ x6 :
ι →
ι → ι
.
If_ii
(
ordinal
x5
)
(
λ x7 .
If_i
(
x7
∈
SNoS_
(
ordsucc
x5
)
)
(
x0
x7
(
λ x8 .
x6
(
SNoLev
x8
)
x8
)
)
(
prim0
(
λ x8 .
True
)
)
)
(
λ x7 .
prim0
(
λ x8 .
True
)
)
)
(
SNoLev
x4
)
x4
)
leaving 2 subgoals.
The subproof is completed by applying L3.
Claim L4:
x1
∈
SNoS_
(
ordsucc
(
SNoLev
x1
)
)
Apply SNoS_SNoLev with
x1
.
The subproof is completed by applying H1.
Apply If_i_1 with
x1
∈
SNoS_
(
ordsucc
(
SNoLev
x1
)
)
,
x0
x1
(
λ x2 .
In_rec_ii
(
λ x3 .
λ x4 :
ι →
ι → ι
.
If_ii
(
ordinal
x3
)
(
λ x5 .
If_i
(
x5
∈
SNoS_
(
ordsucc
x3
)
)
(
x0
x5
(
λ x6 .
x4
(
SNoLev
x6
)
x6
)
)
(
prim0
(
λ x6 .
True
)
)
)
(
λ x5 .
prim0
(
λ x6 .
True
)
)
)
(
SNoLev
x2
)
x2
)
,
prim0
(
λ x2 .
True
)
.
The subproof is completed by applying L4.
■