Nuprl Definition : ses-fresh-thread
ses-fresh-thread(s;es;f;A;thr) ==
∀i:ℕ||thr||
((↑thr[i] ∈b Sign)
⇒ ((signer(thr[i]) = A ∈ Id)
∧ (∃j:ℕi
((↑thr[j] ∈b New)
∧ (↑isl(f signed(thr[i])))
∧ (outl(f signed(thr[i])) = New(thr[j]) ∈ Atom1)
∧ (∀k:{j + 1..i-}
((↑thr[k] ∈b Sign)
⇒ (↑isl(f signed(thr[k])))
⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1))))))))
Definitions occuring in Statement :
ses-signed: signed(e),
ses-signer: signer(e),
ses-sign: Sign,
ses-new: New,
eclass-val: X(e),
in-eclass: e ∈b X,
Id: Id,
select: L[n],
length: ||as||,
int_seg: {i..j-},
atom: Atom$n,
outl: outl(x),
assert: ↑b,
isl: isl(x),
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,
equal: s = t ∈ T
FDL editor aliases :
ses-fresh-thread
Latex:
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:
2015_07_23-PM-00_16_56
Last ObjectModification:
2012_08_30-PM-04_33_42
Home
Index