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

Latex:
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: 2016_05_16-AM-09_21_17 Last ObjectModification: 2013_03_25-PM-01_46_44 Theory : new!event-ordering Home Index