Nuprl Definition : correct-consistent-class
any x,y from X satisfy
R[x; y]
at locations i.Correct[i] ==
∀e1,e2:E. (Correct[loc(e1)] ⇒ Correct[loc(e2)] ⇒ (∀v1,v2:T. (v1 ∈ X(e1) ⇒ v2 ∈ X(e2) ⇒ R[v1; v2])))
Definitions occuring in Statement :
classrel: v ∈ X(e),
es-loc: loc(e),
es-E: E,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
correct-consistent-class
any x,y from X satisfy
R[x; y]
at locations i.Correct[i] ==
\mforall{}e1,e2:E.
(Correct[loc(e1)] {}\mRightarrow{} Correct[loc(e2)] {}\mRightarrow{} (\mforall{}v1,v2:T. (v1 \mmember{} X(e1) {}\mRightarrow{} v2 \mmember{} X(e2) {}\mRightarrow{} R[v1; v2])))
Date html generated:
2015_07_17-PM-00_17_07
Last ObjectModification:
2014_08_15-PM-03_24_59
Home
Index