Search for blocks/addresses/...
Proofgold Proof
pf
Apply nat_primrec_S with
1
,
λ x0 x1 .
mul_nat
2
x1
,
3
,
λ x0 x1 .
x1
=
16
leaving 2 subgoals.
The subproof is completed by applying nat_3.
Apply unknownprop_dce43ea6d63e54501c7ce27a27a4f3799fbde66446a6152326baf4c4d41aa8a0 with
λ x0 x1 .
mul_nat
2
x1
=
16
.
The subproof is completed by applying unknownprop_36374898b358f79d17b8b2339ff8c1fbf04a96c8611bd3a9eaa03c3fcb156f33.
■