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