Nuprl Definition : confluent-equiv
confluent-equiv(T;x,y.R[x; y]) == λa,b. ∃w:T. (R[a; w] ∧ R[b; w])
Definitions occuring in Statement :
exists: ∃x:A. B[x],
and: P ∧ Q,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
exists: ∃x:A. B[x],
and: P ∧ Q
FDL editor aliases :
confluent-equiv
Latex:
confluent-equiv(T;x,y.R[x; y]) == \mlambda{}a,b. \mexists{}w:T. (R[a; w] \mwedge{} R[b; w])
Date html generated:
2019_10_15-AM-10_24_44
Last ObjectModification:
2019_08_16-PM-03_04_47
Theory : relations2
Home
Index