---

Step * of Lemma aa_max_w_unit_prop1

i:. wu:?.  j:. (aa_max_w_unit(inl i ;wu) = (inl j ))
BY
{ (Auto THEN RepUR ``aa_max_w_unit`` 0) }

1
1. i : @i
2. wu : ?@i
 j:. (case wu of inl(intval2) => inl imax(i;intval2)  | inr(unitval2) => inl i  = (inl j ))


\mforall{}i:\mBbbZ{}.  \mforall{}wu:\mBbbZ{}?.    \mexists{}j:\mBbbZ{}.  (aa\_max\_w\_unit(inl  i  ;wu)  =  (inl  j  ))


By

(Auto  THEN  RepUR  ``aa\_max\_w\_unit``  0)



Home Index