Search for blocks/addresses/...
Proofgold Proof
pf
Claim L0:
...
...
Let x0 of type
ο
be given.
Assume H1:
∀ x1 .
(
∃ x2 .
and
(
and
(
4f2b4..
x2
)
(
69b7e..
x1
x2
)
)
(
not
(
21582..
x1
x2
)
)
)
⟶
x0
.
Apply H1 with
dae85..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
4a7ef..
)
.
Let x1 of type
ο
be given.
Assume H2:
∀ x2 .
and
(
and
(
4f2b4..
x2
)
(
69b7e..
(
dae85..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
4a7ef..
)
)
x2
)
)
(
not
(
21582..
(
dae85..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
4a7ef..
)
)
x2
)
)
⟶
x1
.
Apply H2 with
c7794..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
.
Claim L3:
...
...
Claim L4:
...
...
Apply and3I with
4f2b4..
(
c7794..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
,
69b7e..
(
dae85..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
4a7ef..
)
)
(
c7794..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
,
not
(
21582..
(
dae85..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
4a7ef..
)
)
(
c7794..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
)
leaving 3 subgoals.
The subproof is completed by applying L3.
Apply unknownprop_89251a15ed6aeaee20808be140e4e7049bb7edf6c27d8ca099532dd443d98c58 with
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
,
4ae4a..
4a7ef..
.
The subproof is completed by applying L0.
Assume H5:
21582..
(
987b2..
(
1216a..
(
b5c9f..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
λ x2 .
and
(
bij
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
λ x3 .
f482f..
x2
x3
)
)
(
∀ x3 .
prim1
x3
(
4ae4a..
4a7ef..
)
⟶
f482f..
x2
x3
=
x3
)
)
)
(
λ x2 x3 .
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
λ x4 .
f482f..
x3
(
f482f..
x2
x4
)
)
)
)
(
987b2..
(
1216a..
(
b5c9f..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
λ x2 .
bij
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
λ x3 .
f482f..
x2
x3
)
)
)
(
λ x2 x3 .
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
λ x4 .
f482f..
x3
(
f482f..
x2
x4
)
)
)
)
.
Apply H5 with
False
.
Assume H6:
69b7e..
(
987b2..
(
1216a..
(
b5c9f..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
λ x2 .
and
(
bij
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
λ x3 .
f482f..
x2
x3
)
)
(
∀ x3 .
prim1
x3
(
4ae4a..
4a7ef..
)
⟶
f482f..
x2
x3
=
x3
)
)
)
(
λ x2 x3 .
0fc90..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
λ x4 .
f482f..
x3
(
f482f..
x2
x4
)
)
)
)
(
987b2..
(
1216a..
(
b5c9f..
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
)
(
λ x2 .
bij
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
4ae4a..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
λ x3 .
f482f..
x2
...
)
)
)
...
)
.
...
■