Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
ο
be given.
Assume H0:
∀ x1 .
x0
x1
⟶
struct_u
x1
.
Assume H1:
∀ x1 x2 .
x0
x1
⟶
x0
x2
⟶
x0
(
5a1fb..
x1
x2
)
.
Let x1 of type
ι
be given.
Let x2 of type
ι
be given.
Assume H2:
x0
x1
.
Assume H3:
x0
x2
.
Apply H0 with
x1
,
λ x3 .
(
λ x4 x5 x6 x7 x8 .
λ x9 :
ι →
ι →
ι → ι
.
and
(
and
(
UnaryFuncHom
x6
x4
x7
)
(
UnaryFuncHom
x6
x5
x8
)
)
(
∀ x10 .
x0
x10
⟶
∀ x11 x12 .
UnaryFuncHom
x10
x4
x11
⟶
UnaryFuncHom
x10
x5
x12
⟶
and
(
and
(
and
(
UnaryFuncHom
x10
x6
(
x9
x10
x11
x12
)
)
(
struct_comp
x10
x6
x4
x7
(
x9
x10
x11
x12
)
=
x11
)
)
(
struct_comp
x10
x6
x5
x8
(
x9
x10
x11
x12
)
=
x12
)
)
(
∀ x13 .
UnaryFuncHom
x10
x6
x13
⟶
struct_comp
x10
x6
x4
x7
x13
=
x11
⟶
struct_comp
x10
x6
x5
x8
x13
=
x12
⟶
x13
=
x9
x10
x11
x12
)
)
)
x3
x2
(
5a1fb..
x3
x2
)
(
lam
(
setprod
(
ap
x3
0
)
(
ap
x2
0
)
)
(
λ x4 .
ap
x4
0
)
)
(
lam
(
setprod
(
ap
x3
0
)
(
ap
x2
0
)
)
(
λ x4 .
ap
x4
1
)
)
(
λ x4 x5 x6 .
lam
(
ap
x4
0
)
(
λ x7 .
lam
2
(
λ x8 .
If_i
(
x8
=
0
)
(
ap
x5
x7
)
(
ap
x6
x7
)
)
)
)
,
and
(
and
(
and
(
and
(
and
(
x0
x1
)
(
x0
x2
)
)
(
x0
(
5a1fb..
x1
x2
)
)
)
(
UnaryFuncHom
(
5a1fb..
x1
x2
)
x1
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x3 .
ap
x3
0
)
)
)
)
(
UnaryFuncHom
(
5a1fb..
x1
x2
)
x2
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x3 .
ap
x3
1
)
)
)
)
(
∀ x3 .
...
⟶
∀ x4 x5 .
...
⟶
...
⟶
and
(
and
(
and
(
UnaryFuncHom
x3
(
5a1fb..
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
(
5a1fb..
x1
x2
)
x1
(
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x6 .
ap
x6
0
)
)
(
(
λ x6 x7 x8 .
lam
(
ap
x6
0
)
...
)
...
...
...
)
=
...
)
)
...
)
...
)
leaving 3 subgoals.
...
...
...
■