Step
*
of Lemma
aa_max_w_unit_wf
u1,u2:
?.
(aa_max_w_unit(u1;u2)
?)
BY
{
ProveWfLemma
}
\mforall{}u1,u2:\mBbbZ{}?. (aa\_max\_w\_unit(u1;u2) \mmember{} \mBbbZ{}?)
By
ProveWfLemma
Home
Index
u1,u2:
?. (aa_max_w_unit(u1;u2) 
?)