Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
ο
be given.
Assume H0:
x0
1
.
Assume H1:
x0
omega
.
Claim L2:
...
...
Claim L3:
...
...
Apply and5I with
MetaCat_terminal_p
x0
HomSet
(
λ x1 .
lam_id
x1
)
(
λ x1 x2 x3 x4 x5 .
lam_comp
x1
x4
x5
)
1
(
λ x1 .
lam
x1
(
λ x2 .
0
)
)
,
x0
omega
,
HomSet
1
omega
(
lam
1
(
λ x1 .
0
)
)
,
HomSet
omega
omega
(
lam
omega
(
λ x1 .
ordsucc
x1
)
)
,
∀ x1 x2 x3 .
x0
x1
⟶
HomSet
1
x1
x2
⟶
HomSet
x1
x1
x3
⟶
and
(
and
(
and
(
HomSet
omega
x1
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
)
(
(
λ x4 x5 x6 x7 x8 .
lam_comp
x4
x7
x8
)
1
omega
x1
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
(
lam
1
(
λ x4 .
0
)
)
=
x2
)
)
(
(
λ x4 x5 x6 x7 x8 .
lam_comp
x4
x7
x8
)
omega
omega
x1
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
(
lam
omega
(
λ x4 .
ordsucc
x4
)
)
=
(
λ x4 x5 x6 x7 x8 .
lam_comp
x4
x7
x8
)
omega
x1
x1
x3
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
)
)
(
∀ x4 .
HomSet
omega
x1
x4
⟶
(
λ x5 x6 x7 x8 x9 .
lam_comp
x5
x8
x9
)
1
omega
x1
x4
(
lam
1
(
λ x5 .
0
)
)
=
x2
⟶
(
λ x5 x6 x7 x8 x9 .
lam_comp
x5
x8
x9
)
omega
omega
x1
x4
(
lam
omega
(
λ x5 .
ordsucc
x5
)
)
=
(
λ x5 x6 x7 x8 x9 .
lam_comp
x5
x8
x9
)
omega
x1
x1
x3
x4
⟶
x4
=
(
λ x5 x6 x7 .
lam
omega
(
λ x8 .
nat_primrec
(
ap
x6
0
)
(
λ x9 x10 .
ap
x7
x10
)
x8
)
)
x1
x2
x3
)
leaving 5 subgoals.
Apply unknownprop_c631805605639f54c3b6adaa8399cc634c2b0463b565cc1047a5bbf1a7fef49e with
x0
.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply lam_Pi with
1
,
λ x1 .
omega
,
λ x1 .
0
.
Let x1 of type
ι
be given.
Assume H4:
x1
∈
1
.
The subproof is completed by applying L3.
Apply lam_Pi with
omega
,
λ x1 .
omega
,
λ x1 .
ordsucc
x1
.
Let x1 of type
ι
be given.
Assume H4:
x1
∈
omega
.
Apply omega_ordsucc with
x1
.
The subproof is completed by applying H4.
Let x1 of type
ι
be given.
Let x2 of type
ι
be given.
Let x3 of type
ι
be given.
Assume H4:
x0
x1
.
Assume H5:
x2
∈
setexp
x1
1
.
Assume H6:
x3
∈
setexp
...
...
.
...
■