Nuprl Definition : es-locally-ordered

es-locally-ordered(es;L) ==
  rec-case(L) of
  [] => True
  e::rest =>
   r.if null(rest) then True
  if (||rest|| =z 1) then (e <loc hd(rest))
  else (e <loc hd(rest)) ∧ r
  fi 


Definitions occuring in Statement :  es-locl: (e <loc e'),  hd: hd(l),  length: ||as||,  null: null(as),  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  and: P ∧ Q,  true: True,  natural_number: $n
FDL editor aliases :  es-locally-ordered es-locally-ordered
es-locally-ordered(es;L)  ==
    rec-case(L)  of
    []  =>  True
    e::rest  =>
      r.if  null(rest)  then  True
    if  (||rest||  =\msubz{}  1)  then  (e  <loc  hd(rest))
    else  (e  <loc  hd(rest))  \mwedge{}  r
    fi 


Date html generated: 2015_07_17-AM-08_38_07
Last ObjectModification: 2013_03_25-PM-01_46_44

Home Index