Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
be given.
Assume H0:
Subq
x1
x0
.
Apply and3I with
30750..
(
987b2..
(
1216a..
(
b5c9f..
x0
x0
)
(
λ x2 .
bij
x0
x0
(
λ x3 .
f482f..
x2
x3
)
)
)
(
λ x2 x3 .
0fc90..
x0
(
λ x4 .
f482f..
x3
(
f482f..
x2
x4
)
)
)
)
,
30750..
(
987b2..
(
1216a..
(
b5c9f..
x0
x0
)
(
λ x2 .
and
(
bij
x0
x0
(
λ x3 .
f482f..
x2
x3
)
)
(
∀ x3 .
prim1
x3
x1
⟶
f482f..
x2
x3
=
x3
)
)
)
(
λ x2 x3 .
0fc90..
x0
(
λ x4 .
f482f..
x3
(
f482f..
x2
x4
)
)
)
)
,
93c99..
(
987b2..
(
1216a..
(
b5c9f..
x0
x0
)
(
λ x2 .
bij
x0
x0
(
λ x3 .
f482f..
x2
x3
)
)
)
(
λ x2 x3 .
0fc90..
x0
(
λ x4 .
f482f..
x3
(
f482f..
x2
x4
)
)
)
)
(
λ x2 .
λ x3 :
ι →
ι → ι
.
93c99..
(
987b2..
(
1216a..
(
b5c9f..
x0
x0
)
(
λ x4 .
and
(
bij
x0
x0
(
λ x5 .
f482f..
x4
x5
)
)
(
∀ x5 .
prim1
x5
x1
⟶
f482f..
x4
x5
=
x5
)
)
)
(
λ x4 x5 .
0fc90..
x0
(
λ x6 .
f482f..
x5
(
f482f..
x4
x6
)
)
)
)
(
λ x4 .
λ x5 :
ι →
ι → ι
.
and
(
and
(
987b2..
(
1216a..
(
b5c9f..
x0
x0
)
(
λ x6 .
and
(
bij
x0
x0
(
λ x7 .
f482f..
x6
x7
)
)
(
∀ x7 .
prim1
x7
x1
⟶
f482f..
x6
x7
=
x7
)
)
)
(
λ x6 x7 .
0fc90..
x0
(
λ x8 .
f482f..
x7
(
f482f..
x6
x8
)
)
)
=
987b2..
x4
x3
)
(
4f2b4..
(
987b2..
x4
x3
)
)
)
(
Subq
x4
x2
)
)
)
leaving 3 subgoals.
Apply unknownprop_10272f9d8a272cf914054010d8c3a4593cfbbcb7954b0a903e2d867e85e26e68 with
1216a..
(
b5c9f..
x0
x0
)
(
λ x2 .
bij
x0
x0
(
λ x3 .
f482f..
x2
x3
)
)
,
λ x2 x3 .
0fc90..
x0
(
λ x4 .
f482f..
x3
(
f482f..
x2
x4
)
)
.
The subproof is completed by applying unknownprop_fa05ec58213d1b0cffa4f336539515d7ea4c1904e33786a57aa3d93e90546a62 with
x0
.
Apply unknownprop_10272f9d8a272cf914054010d8c3a4593cfbbcb7954b0a903e2d867e85e26e68 with
1216a..
(
b5c9f..
x0
x0
)
(
λ x2 .
and
(
bij
x0
x0
(
λ x3 .
f482f..
x2
x3
)
)
(
∀ x3 .
prim1
x3
x1
⟶
f482f..
x2
x3
=
x3
)
)
,
λ x2 x3 .
0fc90..
x0
(
λ x4 .
f482f..
x3
(
f482f..
x2
x4
)
)
.
Apply unknownprop_303ef75292a7bd9ed5b0c013e4f57cfe7915f538d6e5ad2c3b57bf918b912190 with
x0
,
x1
.
The subproof is completed by applying H0.
Apply unknownprop_cd20f7dbc591f4f87c87c35509dc2db382cd96f4518c628ca9882a10b2d1671d with
1216a..
(
b5c9f..
x0
x0
)
(
λ x2 .
and
(
bij
x0
x0
(
λ x3 .
f482f..
x2
x3
)
)
(
∀ x3 .
prim1
x3
x1
⟶
f482f..
x2
x3
=
x3
)
)
,
1216a..
(
b5c9f..
x0
x0
)
(
λ x2 .
bij
x0
x0
(
λ x3 .
f482f..
x2
x3
)
)
,
λ x2 x3 .
0fc90..
...
...
,
...
,
...
.
...
■