Step
*
1
of Lemma
radd_list_nil_lemma
radd-list([]) ~ r0
BY
{ Try (RW (AddrC [1] (TagC (mk_tag_term 100))) 0)⋅ }
1
λk.(2 * k * 0) ~ r0
Latex:
Latex:
radd-list([]) \msim{} r0
By
Latex:
Try (RW (AddrC [1] (TagC (mk\_tag\_term 100))) 0)\mcdot{}
Home
Index