Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
ο
be given.
Assume H0:
∀ x1 .
x0
x1
⟶
struct_p
x1
.
Assume H1:
∀ x1 x2 .
x0
x1
⟶
x0
x2
⟶
x0
(
b0670..
x1
x2
)
.
Let x1 of type
ι
be given.
Let x2 of type
ι
be given.
Assume H2:
x0
x1
.
Assume H3:
x0
x2
.
Claim L4:
...
...
Apply L4 with
and
(
and
(
and
(
and
(
and
(
x0
x1
)
(
x0
x2
)
)
(
x0
(
b0670..
x1
x2
)
)
)
(
UnaryPredHom
(
b0670..
x1
x2
)
x1
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x3 .
ap
x3
0
)
)
)
)
(
UnaryPredHom
(
b0670..
x1
x2
)
x2
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x3 .
ap
x3
1
)
)
)
)
(
∀ x3 .
...
⟶
∀ x4 x5 .
...
⟶
...
⟶
and
(
and
(
and
(
UnaryPredHom
x3
(
b0670..
x1
x2
)
(
(
λ x6 x7 x8 .
lam
(
ap
x6
0
)
(
λ x9 .
lam
2
(
λ x10 .
If_i
(
x10
=
0
)
(
ap
x7
x9
)
(
ap
x8
x9
)
)
)
)
x3
x4
x5
)
)
(
struct_comp
x3
(
b0670..
x1
x2
)
x1
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x6 .
ap
x6
0
)
)
(
(
λ x6 x7 x8 .
lam
(
ap
x6
0
)
(
λ x9 .
lam
2
(
λ x10 .
If_i
(
x10
=
0
)
(
ap
x7
x9
)
(
ap
x8
x9
)
)
)
)
x3
x4
x5
)
=
x4
)
)
(
struct_comp
x3
(
b0670..
x1
x2
)
x2
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x6 .
ap
x6
1
)
)
(
(
λ x6 x7 x8 .
lam
(
ap
x6
0
)
(
λ x9 .
lam
2
(
λ x10 .
If_i
(
x10
=
0
)
(
ap
x7
x9
)
(
ap
x8
x9
)
)
)
)
x3
x4
x5
)
=
x5
)
)
(
∀ x6 .
UnaryPredHom
x3
(
b0670..
x1
...
)
...
⟶
struct_comp
x3
(
b0670..
x1
x2
)
x1
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x7 .
ap
x7
0
)
)
x6
=
x4
⟶
struct_comp
x3
(
b0670..
x1
x2
)
x2
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x7 .
ap
x7
1
)
)
x6
=
x5
⟶
x6
=
(
λ x7 x8 x9 .
lam
(
ap
x7
0
)
(
λ x10 .
lam
2
(
λ x11 .
If_i
(
x11
=
0
)
(
ap
x8
x10
)
(
ap
x9
x10
)
)
)
)
x3
x4
x5
)
)
.
...
■