Nuprl Definition : cs-knowledge-precondition
may consider v in inning i based on knowledge (s) ==
(∃ws:{a:Id| (a ∈ A)} List
((ws ∈ W)
∧ (∀b:{a:Id| (a ∈ A)} . ((b ∈ ws) ⇒ ((↑b ∈ dom(s)) ∧ (i = (fst(s(b))) ∈ ℤ))))
∧ (∀ws':{a:Id| (a ∈ A)} List
((ws' ∈ W)
⇒ (∃b:{a:Id| (a ∈ A)} . ((b ∈ ws) ∧ (b ∈ ws') ∧ ((↑isl(snd(s(b)))) ⇒ ((snd(outl(snd(s(b))))) = v ∈ V))))))))
∨ (∃b:{a:Id| (a ∈ A)}
((↑b ∈ dom(s))
∧ let j,z = s(b)
in case z of inl(p) => let j',v' = p in (j' = i ∈ ℤ) ∧ (v' = v ∈ V) | inr(x) => False))
Definitions occuring in Statement :
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
id-deq: IdDeq,
Id: Id,
l_member: (x ∈ l),
list: T List,
outl: outl(x),
assert: ↑b,
isl: isl(x),
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
false: False,
set: {x:A| B[x]} ,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
cs-knowledge-precondition
may consider v in inning i based on knowledge (s) ==
(\mexists{}ws:\{a:Id| (a \mmember{} A)\} List
((ws \mmember{} W)
\mwedge{} (\mforall{}b:\{a:Id| (a \mmember{} A)\} . ((b \mmember{} ws) {}\mRightarrow{} ((\muparrow{}b \mmember{} dom(s)) \mwedge{} (i = (fst(s(b)))))))
\mwedge{} (\mforall{}ws':\{a:Id| (a \mmember{} A)\} List
((ws' \mmember{} W)
{}\mRightarrow{} (\mexists{}b:\{a:Id| (a \mmember{} A)\}
((b \mmember{} ws) \mwedge{} (b \mmember{} ws') \mwedge{} ((\muparrow{}isl(snd(s(b)))) {}\mRightarrow{} ((snd(outl(snd(s(b))))) = v))))))))
\mvee{} (\mexists{}b:\{a:Id| (a \mmember{} A)\}
((\muparrow{}b \mmember{} dom(s))
\mwedge{} let j,z = s(b)
in case z of inl(p) => let j',v' = p in (j' = i) \mwedge{} (v' = v) | inr(x) => False))
Date html generated:
2015_07_17-AM-11_40_00
Last ObjectModification:
2012_02_25-AM-11_45_50
Home
Index