---

ses-fresh-thread(s;es;f;A;thr) ==
  i:||thr||
    ((thr[i]  Sign)
     ((signer(thr[i]) = A)
        (j:i
           ((thr[j]  New)
            (isl(f signed(thr[i])))
            (outl(f signed(thr[i])) = New(thr[j]))
            (k:{j + 1..i}
                ((thr[k]  Sign)
                 (isl(f signed(thr[k])))
                 ((outl(f signed(thr[k])) = New(thr[j])))))))))

---

Definitions :  length: ||as||,  Id: Id,  ses-signer: signer(e),  exists: x:A. B[x],  and: P  Q,  all: x:A. B[x],  int_seg: {i..j},  add: n + m,  natural_number: $n,  in-eclass: e  X,  ses-sign: Sign,  implies: P  Q,  assert: b,  isl: isl(x),  not: A,  equal: s = t,  atom: Atom$n,  outl: outl(x),  apply: f a,  ses-signed: signed(e),  eclass-val: X(e),  ses-new: New,  select: l[i]
FDL editor aliases :  ses-fresh-thread

---

ses-fresh-thread(s;es;f;A;thr)  ==
    \mforall{}i:\mBbbN{}||thr||
        ((\muparrow{}thr[i]  \mmember{}\msubb{}  Sign)
        {}\mRightarrow{}  ((signer(thr[i])  =  A)
              \mwedge{}  (\mexists{}j:\mBbbN{}i
                      ((\muparrow{}thr[j]  \mmember{}\msubb{}  New)
                      \mwedge{}  (\muparrow{}isl(f  signed(thr[i])))
                      \mwedge{}  (outl(f  signed(thr[i]))  =  New(thr[j]))
                      \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}
                                ((\muparrow{}thr[k]  \mmember{}\msubb{}  Sign)
                                {}\mRightarrow{}  (\muparrow{}isl(f  signed(thr[k])))
                                {}\mRightarrow{}  (\mneg{}(outl(f  signed(thr[k]))  =  New(thr[j])))))))))


Date html generated: 2010_08_28-AM-03_14_40
Last ObjectModification: 2010_03_16-PM-02_40_14

Home Index