Nuprl Definition : cs-archive-blocked
in state s, ws' blocks ws from archiving v in inning i ==
∃j:ℤ
(((0 ≤ j) ∧ j < i)
∧ (∃v':V
((¬(v' = v ∈ V))
∧ (∀b:{a:Id| (a ∈ A)}
(((b ∈ ws) ∧ (b ∈ ws'))
⇒ ((↑j ∈ dom(Estimate(s;b)))
∧ (Estimate(s;b)(j) = v' ∈ V)
∧ (∀k:ℤ. (((j < k ∧ k < i) ∧ (↑k ∈ dom(Estimate(s;b)))) ⇒ (Estimate(s;b)(k) = v' ∈ V)))))))))
Definitions occuring in Statement :
cs-estimate: Estimate(s;a),
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
Id: Id,
int-deq: IntDeq,
l_member: (x ∈ l),
assert: ↑b,
less_than: a < b,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
cs-archive-blocked
in state s, ws' blocks ws from archiving v in inning i ==
\mexists{}j:\mBbbZ{}
(((0 \mleq{} j) \mwedge{} j < i)
\mwedge{} (\mexists{}v':V
((\mneg{}(v' = v))
\mwedge{} (\mforall{}b:\{a:Id| (a \mmember{} A)\}
(((b \mmember{} ws) \mwedge{} (b \mmember{} ws'))
{}\mRightarrow{} ((\muparrow{}j \mmember{} dom(Estimate(s;b)))
\mwedge{} (Estimate(s;b)(j) = v')
\mwedge{} (\mforall{}k:\mBbbZ{}
(((j < k \mwedge{} k < i) \mwedge{} (\muparrow{}k \mmember{} dom(Estimate(s;b))))
{}\mRightarrow{} (Estimate(s;b)(k) = v')))))))))
Date html generated:
2015_07_17-AM-11_25_55
Last ObjectModification:
2012_02_25-AM-11_42_00
Home
Index