Nuprl Definition : rel-confluent
rel-confluent(T;x,y.R[x; y]) == ∀x,y,z:T. (R[x; y] ⇒ R[x; z] ⇒ (∃w:T. (R[y; w] ∧ R[z; w])))
Definitions occuring in Statement :
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
and: P ∧ Q
FDL editor aliases :
rel-confluent
Latex:
rel-confluent(T;x,y.R[x; y]) == \mforall{}x,y,z:T. (R[x; y] {}\mRightarrow{} R[x; z] {}\mRightarrow{} (\mexists{}w:T. (R[y; w] \mwedge{} R[z; w])))
Date html generated:
2019_10_15-AM-10_24_33
Last ObjectModification:
2019_08_16-PM-02_32_26
Theory : relations2
Home
Index