Nuprl Definition : ses-fresh-sequence
ses-fresh-sequence(f;A;pas) ==
∀i:ℕ||pas||
(((fst(pas[i])) = "sign" ∈ Atom)
⇒ (((fst(snd(snd(pas[i])))) = A ∈ Id)
∧ (∃j:ℕi
(((fst(pas[j])) = "new" ∈ Atom)
∧ ((↑isl(f (fst(snd(pas[i]))))) ∧ (outl(f (fst(snd(pas[i])))) = (snd(pas[j])) ∈ Atom1))
∧ (∀k:{j + 1..i-}
(((fst(pas[k])) = "sign" ∈ Atom)
⇒ (↑isl(f (fst(snd(pas[k])))))
⇒ (¬(outl(f (fst(snd(pas[k])))) = (snd(pas[j])) ∈ Atom1))))))))
Definitions occuring in Statement :
Id: Id,
select: L[n],
length: ||as||,
int_seg: {i..j-},
atom: Atom$n,
outl: outl(x),
assert: ↑b,
isl: isl(x),
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
add: n + m,
natural_number: $n,
token: "$token",
atom: Atom,
equal: s = t ∈ T
FDL editor aliases :
ses-fresh-sequence
Latex:
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:
2015_07_23-PM-00_14_23
Last ObjectModification:
2012_08_30-PM-04_30_39
Home
Index