Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Let x1 of type
ι
be given.
Let x2 of type
ι
be given.
Let x3 of type
ι
be given.
Let x4 of type
ι
be given.
Let x5 of type
ι
be given.
Let x6 of type
ι
be given.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
)
,
λ x7 .
If_i
(
x7
=
4a7ef..
)
x0
(
If_i
(
x7
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
x7
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
)
,
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
,
λ x7 x8 .
x8
=
x3
leaving 2 subgoals.
The subproof is completed by applying unknownprop_f03b01fb6a71e75b6194b561dc943c125bed733672eaa73961f8ab4995d7e9b8.
Apply If_i_0 with
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4a7ef..
,
x0
,
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
4a7ef..
)
x1
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
)
,
λ x7 x8 .
x8
=
x3
leaving 2 subgoals.
The subproof is completed by applying unknownprop_39c68f59201a24e05d494df554b752ed6bfbdb14109c09811c3da46652b4b359.
Apply If_i_0 with
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
4a7ef..
,
x1
,
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
)
x2
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
)
,
λ x7 x8 .
x8
=
x3
leaving 2 subgoals.
The subproof is completed by applying unknownprop_660d518b3f18494e3056984097a0917e4ddb34b7d7ca0e50c6808ad2c4676ba8.
Apply If_i_0 with
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
4a7ef..
)
,
x2
,
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
x3
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
x5
x6
)
)
,
λ x7 x8 .
x8
=
x3
leaving 2 subgoals.
The subproof is completed by applying unknownprop_73033d4e951667af4b4a387afc6dabb25c26071ba21f7aaa1e5a3c5c21a42316.
Apply If_i_1 with
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
,
x3
,
If_i
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
=
4ae4a..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
x4
(
If_i
(
4ae4a..
(
4ae4a..
...
)
=
...
)
...
...
)
.
...
■