Search for blocks/addresses/...
Proofgold Proof
pf
Apply nat_primrec_S with
1
,
λ x0 x1 .
mul_nat
2
x1
,
2
,
λ x0 x1 .
x1
=
8
leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply unknownprop_c2aa62c368a47ae018ac0952ff3137b0b6dc17b9b871ce9eb89fc53a8a9f308f with
λ x0 x1 .
mul_nat
2
x1
=
8
.
The subproof is completed by applying unknownprop_82b4ca10eb7ca03c2ab8db9622e8ff501b1df3632d9b511d2313d8304ef45b38.
■