Search for blocks/addresses/...
Proofgold Proof
pf
Apply CD_add_F_eq with
Sing
2
,
SNo
,
add_SNo
leaving 3 subgoals.
The subproof is completed by applying complex_tag_fresh.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with
0
.
The subproof is completed by applying SNo_0.
■