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

Definitions occuring in Statement :  es-locl: (e <loc e') hd: hd(l) length: ||as|| null: null(as) list_ind: list_ind ifthenelse: if then else 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

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

Home Index