Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
prim1
(
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
(
91630..
(
91630..
(
4ae4a..
4a7ef..
)
)
)
.
Claim L1:
prim1
(
4ae4a..
4a7ef..
)
(
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
)
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
91630..
(
4ae4a..
4a7ef..
)
,
91630..
(
4ae4a..
(
4ae4a..
4a7ef..
)
)
,
λ x0 x1 .
prim1
(
4ae4a..
4a7ef..
)
x1
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with
4ae4a..
4a7ef..
.
Apply unknownprop_a40b1b0e53a6f2e95bf15bb70ac30a639fc92aae5523aaa9454c636e67101929.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
4ae4a..
(
4ae4a..
4a7ef..
)
,
4ae4a..
4a7ef..
.
The subproof is completed by applying L1.
■