Nuprl Definition : rel_plus
R+ == λx,y. ∃n:ℕ+. (x R^n y)
Definitions occuring in Statement :
rel_exp: R^n,
nat_plus: ℕ+,
infix_ap: x f y,
exists: ∃x:A. B[x],
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
exists: ∃x:A. B[x],
nat_plus: ℕ+,
infix_ap: x f y,
rel_exp: R^n
FDL editor aliases :
rel_plus
Latex:
R\msupplus{} == \mlambda{}x,y. \mexists{}n:\mBbbN{}\msupplus{}. (x rel\_exp(T; R; n) y)
Date html generated:
2016_05_14-PM-03_51_25
Last ObjectModification:
2015_09_22-PM-06_01_46
Theory : relations2
Home
Index