Nuprl Definition : es-with-internal

es-with-internal(es;k;X) ==
  mk-extended-eo(type: e:E × ℕ||X map(λe.info(e);≤loc(e))|| + 1;
                 domain: λp.(es-dom(es) (fst(p)));
                 loc: λp.loc(fst(p));
                 info: λp.let e,n = p 
                          in if (n =z 0) then info(e) else X map(λe.info(e);≤loc(e))[n - 1] fi ;
                 causal: λe1,e2. ((fst(e1) < fst(e2)) ∨ (((fst(e1)) = (fst(e2)) ∈ E) ∧ snd(e1) < snd(e2)));
                 local: λe1,e2. (es-blocl(es;fst(e1);fst(e2))
                               ∨b((¬bes-blocl(es;fst(e2);fst(e1))) ∧b snd(e1) <z snd(e2)));
                 pred: λp.if snd(p)=0
                             then if first(fst(p))
                                  then p
                                  else let e' = pred(fst(p)) in
                                        let extra = X map(λe.info(e);≤loc(e')) in
                                        <e', ||extra||>
                                  fi 
                             else <fst(p), (snd(p)) - 1>;
                 rank: λp.((k * es-rank(es;fst(p))) + (snd(p))))


Definitions occuring in Statement :  mk-extended-eo: mk-extended-eo,  es-info: info(e),  es-le-before: ≤loc(e),  es-blocl: es-blocl(es;e1;e2),  es-first: first(e),  es-pred: pred(e),  es-rank: es-rank(es;e),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  es-dom: es-dom(es),  select: L[n],  map: map(f;as),  length: ||as||,  bor: p ∨bq,  band: p ∧b q,  int_seg: {i..j-},  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  less_than: a < b,  let: let,  pi1: fst(t),  pi2: snd(t),  or: P ∨ Q,  and: P ∧ Q,  int_eq: if a=b  then c  else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  product: x:A × B[x],  multiply: n * m,  subtract: n - m,  add: n + m,  natural_number: $n,  equal: s = t ∈ T
FDL editor aliases :  es-with-internal
Latex:
es-with-internal(es;k;X)  ==
    mk-extended-eo(type:  e:E  \mtimes{}  \mBbbN{}||X  map(\mlambda{}e.info(e);\mleq{}loc(e))||  +  1;
                                  domain:  \mlambda{}p.(es-dom(es)  (fst(p)));
                                  loc:  \mlambda{}p.loc(fst(p));
                                  info:  \mlambda{}p.let  e,n  =  p 
                                                    in  if  (n  =\msubz{}  0)  then  info(e)  else  X  map(\mlambda{}e.info(e);\mleq{}loc(e))[n  -  1]  fi  ;
                                  causal:  \mlambda{}e1,e2.  ((fst(e1)  <  fst(e2))
                                                                \mvee{}  (((fst(e1))  =  (fst(e2)))  \mwedge{}  snd(e1)  <  snd(e2)));
                                  local:  \mlambda{}e1,e2.  (es-blocl(es;fst(e1);fst(e2))
                                                              \mvee{}\msubb{}((\mneg{}\msubb{}es-blocl(es;fst(e2);fst(e1)))  \mwedge{}\msubb{}  snd(e1)  <z  snd(e2)));
                                  pred:  \mlambda{}p.if  snd(p)=0
                                                          then  if  first(fst(p))
                                                                    then  p
                                                                    else  let  e'  =  pred(fst(p))  in
                                                                                let  extra  =  X  map(\mlambda{}e.info(e);\mleq{}loc(e'))  in
                                                                                <e',  ||extra||>
                                                                    fi 
                                                          else  <fst(p),  (snd(p))  -  1>
                                  rank:  \mlambda{}p.((k  *  es-rank(es;fst(p)))  +  (snd(p))))


Date html generated: 2015_07_21-PM-04_46_23
Last ObjectModification: 2014_08_18-PM-05_31_53

Home Index