Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
ο
be given.
Assume H0:
∀ x1 .
x0
x1
⟶
struct_r
x1
.
Assume H1:
∀ x1 x2 .
x0
x1
⟶
x0
x2
⟶
x0
(
BinReln_product
x1
x2
)
.
Assume H2:
∀ x1 x2 .
x0
x1
⟶
x0
x2
⟶
x0
(
BinReln_exp
x1
x2
)
.
Apply andI with
MetaCat_product_constr_p
x0
BinRelnHom
struct_id
struct_comp
(
λ x1 x2 .
unpack_r_i
x1
(
λ x3 .
λ x4 :
ι →
ι → ο
.
unpack_r_i
x2
(
λ x5 .
λ x6 :
ι →
ι → ο
.
pack_r
(
setprod
x3
x5
)
(
λ x7 x8 .
and
(
x4
(
ap
x7
0
)
(
ap
x8
0
)
)
(
x6
(
ap
x7
1
)
(
ap
x8
1
)
)
)
)
)
)
(
λ x1 x2 .
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x3 .
ap
x3
0
)
)
(
λ x1 x2 .
lam
(
setprod
(
ap
x1
0
)
(
ap
x2
0
)
)
(
λ x3 .
ap
x3
1
)
)
(
λ x1 x2 x3 x4 x5 .
lam
(
ap
x3
0
)
(
λ x6 .
lam
2
(
λ x7 .
If_i
(
x7
=
0
)
(
ap
x4
x6
)
(
ap
x5
x6
)
)
)
)
,
∀ x1 x2 .
x0
x1
⟶
x0
x2
⟶
MetaCat_exp_p
x0
BinRelnHom
struct_id
struct_comp
BinReln_product
(
λ x3 x4 .
lam
(
setprod
(
ap
x3
0
)
(
ap
x4
0
)
)
(
λ x5 .
ap
x5
0
)
)
(
λ x3 x4 .
lam
(
setprod
(
ap
x3
0
)
(
ap
x4
0
)
)
(
λ x5 .
ap
x5
1
)
)
(
λ x3 x4 x5 x6 x7 .
lam
(
ap
x5
0
)
(
λ x8 .
lam
2
(
λ x9 .
If_i
(
x9
=
0
)
(
ap
x6
x8
)
(
ap
x7
x8
)
)
)
)
x1
x2
(
BinReln_exp
x1
x2
)
(
lam
(
setprod
(
setexp
(
ap
x2
0
)
(
ap
x1
0
)
)
(
ap
x1
0
)
)
(
λ x3 .
ap
(
ap
x3
0
)
(
ap
x3
1
)
)
)
(
λ x3 x4 .
lam
(
ap
x3
0
)
(
λ x5 .
lam
(
ap
x1
0
)
(
λ x6 .
ap
x4
(
lam
2
(
λ x7 .
If_i
(
x7
=
0
)
x5
x6
)
)
)
)
)
leaving 2 subgoals.
Apply unknownprop_5f5149dc445b1bf6ca4a7f60e27b87771b4704fa8e9610ac4ab806ac27b93c0b with
x0
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x1 of type
ι
be given.
Let x2 of type
ι
be given.
Assume H3:
x0
x1
.
Assume H4:
x0
x2
.
Apply and5I with
x0
x1
,
x0
x2
,
x0
(
BinReln_exp
x1
x2
)
,
BinRelnHom
(
BinReln_product
(
BinReln_exp
x1
x2
)
x1
)
x2
(
lam
(
setprod
(
setexp
(
ap
x2
0
)
(
ap
x1
0
)
)
(
ap
x1
0
)
)
(
λ x3 .
ap
(
ap
x3
0
)
(
ap
x3
1
)
)
)
,
∀ x3 .
...
⟶
∀ x4 .
...
⟶
and
(
and
(
BinRelnHom
...
...
...
)
...
)
...
leaving 5 subgoals.
...
...
...
...
...
■