Nuprl Definition : rel_star

R^* ==  λx,y. ∃n:ℕ(x R^n y)



Definitions occuring in Statement :  rel_exp: R^n nat: infix_ap: 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: 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