Nuprl Definition : rel_star
R^* == λx,y. ∃n:ℕ. (x R^n y)
Definitions occuring in Statement :
rel_exp: R^n,
nat: ℕ,
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: ℕ,
infix_ap: x f y,
rel_exp: R^n
FDL editor aliases :
rel_star
Latex:
rel\_star(T; R) == \mlambda{}x,y. \mexists{}n:\mBbbN{}. (x rel\_exp(T; R; n) y)
Date html generated:
2016_05_13-PM-04_19_10
Last ObjectModification:
2015_09_22-PM-05_46_46
Theory : relations
Home
Index