Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
ο
be given.
Assume H0:
∀ x1 .
x0
x1
⟶
struct_p
x1
.
Assume H1:
x0
(
pack_p
1
(
λ x1 .
True
)
)
.
Assume H2:
x0
(
pack_p
omega
(
λ x1 .
True
)
)
.
Apply and5I with
MetaCat_terminal_p
x0
UnaryPredHom
struct_id
struct_comp
(
pack_p
1
(
λ x1 .
True
)
)
(
λ x1 .
lam
(
ap
x1
0
)
(
λ x2 .
0
)
)
,
x0
(
pack_p
omega
(
λ x1 .
True
)
)
,
UnaryPredHom
(
pack_p
1
(
λ x1 .
True
)
)
(
pack_p
omega
(
λ x1 .
True
)
)
(
lam
1
(
λ x1 .
0
)
)
,
UnaryPredHom
(
pack_p
omega
(
λ x1 .
True
)
)
(
pack_p
omega
(
λ x1 .
True
)
)
(
lam
omega
(
λ x1 .
ordsucc
x1
)
)
,
∀ x1 x2 x3 .
...
⟶
UnaryPredHom
(
pack_p
1
...
)
...
...
⟶
UnaryPredHom
x1
x1
x3
⟶
and
(
and
(
and
(
UnaryPredHom
(
pack_p
omega
(
λ x4 .
True
)
)
x1
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
)
(
struct_comp
(
pack_p
1
(
λ x4 .
True
)
)
(
pack_p
omega
(
λ x4 .
True
)
)
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
)
)
(
struct_comp
(
pack_p
omega
(
λ x4 .
True
)
)
(
pack_p
omega
(
λ x4 .
True
)
)
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
)
)
=
struct_comp
(
pack_p
omega
(
λ x4 .
True
)
)
x1
x1
x3
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
)
)
(
∀ x4 .
UnaryPredHom
(
pack_p
omega
(
λ x5 .
True
)
)
x1
x4
⟶
struct_comp
(
pack_p
1
(
λ x5 .
True
)
)
(
pack_p
omega
(
λ x5 .
True
)
)
x1
x4
(
lam
1
(
λ x5 .
0
)
)
=
x2
⟶
struct_comp
(
pack_p
omega
(
λ x5 .
True
)
)
(
pack_p
omega
(
λ x5 .
True
)
)
x1
x4
(
lam
omega
(
λ x5 .
ordsucc
x5
)
)
=
struct_comp
(
pack_p
omega
(
λ x5 .
True
)
)
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.
...
...
...
...
...
■