---

ses-fresh-sequence(f;A;pas) ==
  i:||pas||
    (((fst(pas[i])) = "sign")
     (((fst(snd(snd(pas[i])))) = A)
        (j:i
           (((fst(pas[j])) = "new")
            ((isl(f (fst(snd(pas[i])))))
              (outl(f (fst(snd(pas[i])))) = (snd(pas[j]))))
            (k:{j + 1..i}
                (((fst(pas[k])) = "sign")
                 (isl(f (fst(snd(pas[k])))))
                 ((outl(f (fst(snd(pas[k])))) = (snd(pas[j]))))))))))

---

Definitions :  length: ||as||,  Id: Id,  exists: x:A. B[x],  and: P  Q,  all: x:A. B[x],  int_seg: {i..j},  add: n + m,  natural_number: $n,  atom: Atom,  token: "$token",  implies: P  Q,  assert: b,  isl: isl(x),  not: A,  equal: s = t,  atom: Atom$n,  outl: outl(x),  apply: f a,  pi1: fst(t),  pi2: snd(t),  select: l[i]
FDL editor aliases :  ses-fresh-sequence

---

ses-fresh-sequence(f;A;pas)  ==
    \mforall{}i:\mBbbN{}||pas||
        (((fst(pas[i]))  =  "sign")
        {}\mRightarrow{}  (((fst(snd(snd(pas[i]))))  =  A)
              \mwedge{}  (\mexists{}j:\mBbbN{}i
                      (((fst(pas[j]))  =  "new")
                      \mwedge{}  ((\muparrow{}isl(f  (fst(snd(pas[i])))))  \mwedge{}  (outl(f  (fst(snd(pas[i]))))  =  (snd(pas[j]))))
                      \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}
                                (((fst(pas[k]))  =  "sign")
                                {}\mRightarrow{}  (\muparrow{}isl(f  (fst(snd(pas[k])))))
                                {}\mRightarrow{}  (\mneg{}(outl(f  (fst(snd(pas[k]))))  =  (snd(pas[j]))))))))))


Date html generated: 2010_08_28-AM-02_46_54
Last ObjectModification: 2010_03_16-PM-01_13_59

Home Index