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