Nuprl Definition : pv11_p1_valid-proposal
pv11_p1_valid-proposal(Cmd;es;e;p;f) == ↓∃e':E. (e' c≤ e ∧ p ∈ pv11_p1_propose'base(Cmd;f)(e'))
Definitions occuring in Statement :
pv11_p1_propose'base: pv11_p1_propose'base(Cmd;mf),
classrel: v ∈ X(e),
es-causle: e c≤ e',
es-E: E,
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
product: x:A × B[x],
int: ℤ
FDL editor aliases :
pv11_p1_valid-proposal
Latex:
pv11\_p1\_valid-proposal(Cmd;es;e;p;f) == \mdownarrow{}\mexists{}e':E. (e' c\mleq{} e \mwedge{} p \mmember{} pv11\_p1\_propose'base(Cmd;f)(e'))
Date html generated:
2015_07_23-PM-05_03_12
Last ObjectModification:
2013_12_18-PM-06_17_49
Home
Index