Nuprl Definition : es-pstar-q
[e1;e2]~([a,b].p[a; b])*[a,b].q[a; b] ==
∃m:ℕ+
∃f:ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id}
((((f 0) = e1 ∈ E) ∧ f (m - 1) ≤loc e2 )
∧ ((∀i:ℕm - 1. (f i <loc f (i + 1))) ∧ (∀i:ℕm - 1. p[f i; pred(f (i + 1))]))
∧ q[f (m - 1); e2])
Definitions occuring in Statement :
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-pred: pred(e),
es-loc: loc(e),
es-E: E,
Id: Id,
nat_plus: ℕ+,
int_seg: {i..j-},
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x],
subtract: n - m,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
FDL editor aliases :
es-pstar-q
es-pstar-q
[e1;e2]\msim{}([a,b].p[a; b])*[a,b].q[a; b] ==
\mexists{}m:\mBbbN{}\msupplus{}
\mexists{}f:\mBbbN{}m {}\mrightarrow{} \{e:E| loc(e) = loc(e1)\}
((((f 0) = e1) \mwedge{} f (m - 1) \mleq{}loc e2 )
\mwedge{} ((\mforall{}i:\mBbbN{}m - 1. (f i <loc f (i + 1))) \mwedge{} (\mforall{}i:\mBbbN{}m - 1. p[f i; pred(f (i + 1))]))
\mwedge{} q[f (m - 1); e2])
Date html generated:
2015_07_17-AM-08_53_32
Last ObjectModification:
2013_03_25-PM-01_52_28
Home
Index