Step
*
of Lemma
test-omega-auto-split
∀n:ℤ. (if 2 <z n then if 1 <z n then 1 else 2 fi  if n ≤z 3 then 3 else 4 fi  ~ if 2 <z n then 1 else 3 fi )
BY
{ ((D 0 THENA Auto) THEN (AutoSplit THENA Auto)) }
Latex:
Latex:
\mforall{}n:\mBbbZ{}
    (if  2  <z  n  then  if  1  <z  n  then  1  else  2  fi 
    if  n  \mleq{}z  3  then  3
    else  4
    fi    \msim{}  if  2  <z  n  then  1  else  3  fi  )
By
Latex:
((D  0  THENA  Auto)  THEN  (AutoSplit  THENA  Auto))
Home
Index