Search for blocks/addresses/...
Proofgold Proof
pf
Apply nat_primrec_S with
1
,
λ x0 x1 .
mul_nat
2
x1
,
4
,
λ x0 x1 .
x1
=
32
leaving 2 subgoals.
The subproof is completed by applying nat_4.
Apply unknownprop_18dab10013860d442d73fc2b55cfee57e61b2e3044d2d0c29767dba9e5eb2112 with
λ x0 x1 .
mul_nat
2
x1
=
32
.
The subproof is completed by applying unknownprop_0ea4d9117f5e04c7f1289250df7ab43a5ad0c6cef376e453fd3c5c502e8be6da.
■