Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
(
ι
→
ι
→
ι
) →
ι
→
ι
be given.
Assume H0:
∀ x1 .
80242..
x1
⟶
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
prim1
x4
(
56ded..
(
e4431..
x1
)
)
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
.
Let x1 of type
ι
be given.
Assume H1:
80242..
x1
.
Claim L2:
∀ x2 .
∀ x3 x4 :
ι →
ι →
ι → ι
.
...
⟶
(
λ x5 .
λ x6 :
ι →
ι →
ι → ι
.
If_iii
(
ordinal
x5
)
(
λ x7 .
If_ii
(
prim1
x7
(
56ded..
(
4ae4a..
x5
)
)
)
(
x0
x7
(
λ x8 .
x6
(
e4431..
x8
)
x8
)
)
...
)
...
)
...
...
=
...
...
Apply In_rec_iii_eq with
λ x2 .
λ x3 :
ι →
ι →
ι → ι
.
If_iii
(
ordinal
x2
)
(
λ x4 .
If_ii
(
prim1
x4
(
56ded..
(
4ae4a..
x2
)
)
)
(
x0
x4
(
λ x5 .
x3
(
e4431..
x5
)
x5
)
)
(
Descr_ii
(
λ x5 :
ι → ι
.
True
)
)
)
(
λ x4 .
Descr_ii
(
λ x5 :
ι → ι
.
True
)
)
,
e4431..
x1
,
λ x2 x3 :
ι →
ι → ι
.
x3
x1
=
x0
x1
(
λ x4 .
In_rec_iii
(
λ x5 .
λ x6 :
ι →
ι →
ι → ι
.
If_iii
(
ordinal
x5
)
(
λ x7 .
If_ii
(
prim1
x7
(
56ded..
(
4ae4a..
x5
)
)
)
(
x0
x7
(
λ x8 .
x6
(
e4431..
x8
)
x8
)
)
(
Descr_ii
(
λ x8 :
ι → ι
.
True
)
)
)
(
λ x7 .
Descr_ii
(
λ x8 :
ι → ι
.
True
)
)
)
(
e4431..
x4
)
x4
)
leaving 2 subgoals.
The subproof is completed by applying L2.
Claim L3:
ordinal
(
e4431..
x1
)
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with
x1
.
The subproof is completed by applying H1.
Apply If_iii_1 with
ordinal
(
e4431..
x1
)
,
λ x2 .
If_ii
(
prim1
x2
(
56ded..
(
4ae4a..
(
e4431..
x1
)
)
)
)
(
x0
x2
(
λ x3 .
In_rec_iii
(
λ x4 .
λ x5 :
ι →
ι →
ι → ι
.
If_iii
(
ordinal
x4
)
(
λ x6 .
If_ii
(
prim1
x6
(
56ded..
(
4ae4a..
x4
)
)
)
(
x0
x6
(
λ x7 .
x5
(
e4431..
x7
)
x7
)
)
(
Descr_ii
(
λ x7 :
ι → ι
.
True
)
)
)
(
λ x6 .
Descr_ii
(
λ x7 :
ι → ι
.
True
)
)
)
(
e4431..
x3
)
x3
)
)
(
Descr_ii
(
λ x3 :
ι → ι
.
True
)
)
,
λ x2 .
Descr_ii
(
λ x3 :
ι → ι
.
True
)
,
λ x2 x3 :
ι →
ι → ι
.
x3
x1
=
x0
x1
(
λ x4 .
In_rec_iii
(
λ x5 .
λ x6 :
ι →
ι →
ι → ι
.
If_iii
(
ordinal
x5
)
(
λ x7 .
If_ii
(
prim1
x7
(
56ded..
(
4ae4a..
x5
)
)
)
(
x0
x7
(
λ x8 .
x6
(
e4431..
x8
)
x8
)
)
(
Descr_ii
(
λ x8 :
ι → ι
.
True
)
)
)
(
λ x7 .
Descr_ii
(
λ x8 :
ι → ι
.
True
)
)
)
(
e4431..
x4
)
x4
)
leaving 2 subgoals.
The subproof is completed by applying L3.
Claim L4:
prim1
x1
(
56ded..
(
4ae4a..
(
e4431..
x1
)
)
)
Apply unknownprop_55be23921c8e687561ab6e9faf36ed3618fa021f01ef196ba95aa8fcda0b83ee with
x1
.
The subproof is completed by applying H1.
Apply If_ii_1 with
prim1
x1
(
56ded..
(
4ae4a..
(
e4431..
x1
)
)
)
,
x0
x1
(
λ x2 .
In_rec_iii
(
λ x3 .
λ x4 :
ι →
ι →
ι → ι
.
If_iii
(
ordinal
x3
)
(
λ x5 .
If_ii
(
prim1
x5
(
56ded..
(
4ae4a..
x3
)
)
)
(
x0
x5
(
λ x6 .
x4
(
e4431..
x6
)
x6
)
)
(
Descr_ii
(
λ x6 :
ι → ι
.
True
)
)
)
(
λ x5 .
Descr_ii
(
λ x6 :
ι → ι
.
True
)
)
)
(
e4431..
x2
)
x2
)
,
Descr_ii
(
λ x2 :
ι → ι
.
True
)
.
The subproof is completed by applying L4.
■