Search for blocks/addresses/...
Proofgold Proof
pf
Apply mul_nat_SR with
u6
,
u4
,
λ x0 x1 .
x1
=
u30
leaving 2 subgoals.
The subproof is completed by applying nat_4.
Apply add_nat_com with
u6
,
mul_nat
u6
u4
,
λ x0 x1 .
x1
=
u30
leaving 3 subgoals.
The subproof is completed by applying nat_6.
Apply mul_nat_p with
u6
,
u4
leaving 2 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying nat_4.
Apply unknownprop_5739bd2c30c42b1cef616b7ab0141364fc0bacb1d7cf0df36fca5d0d1b298c8e with
λ x0 x1 .
add_nat
x1
u6
=
u30
.
The subproof is completed by applying unknownprop_53b5d6a493506e855393f47f611cdb01725e1da6599106a059647b3426c60f8b.
■