---

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

---

Definitions :  list_ind: rec-case(a) of [] => s | x::y => z.t[x; y; z],  null: null(as),  true: True,  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  length: ||as||,  natural_number: $n,  and: P  Q,  es-locl: (e <loc e'),  hd: hd(l)
FDL editor aliases :  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: 2010_08_27-AM-01_09_18
Last ObjectModification: 2009_12_16-AM-12_41_25

Home Index