---

Legal(thr)@A ==
  i:||thr||
    UsedAtoms(thr[i])  [Private(A) / 
                         concat(map(j.UseableAtoms(thr[j]);[0, i)))]

---

Definitions :  all: x:A. B[x],  int_seg: {i..j},  length: ||as||,  l_contains: A  B,  atom: Atom$n,  ses-used-atoms: UsedAtoms(e),  cons: [car / cdr],  ses-private: Private(A),  concat: concat(ll),  map: map(f;as),  lambda: x.A[x],  ses-useable-atoms: UseableAtoms(e),  select: l[i],  from-upto: [n, m),  natural_number: $n
FDL editor aliases :  ses-legal-thread

---

Legal(thr)@A  ==
    \mforall{}i:\mBbbN{}||thr||.  UsedAtoms(thr[i])  \msubseteq{}  [Private(A)  /  concat(map(\mlambda{}j.UseableAtoms(thr[j]);[0,  i)))]


Date html generated: 2010_08_28-AM-02_43_45
Last ObjectModification: 2010_02_22-PM-11_55_20

Home Index