Nuprl Definition : rel_exp
R^n == fix((λrel_exp,n. if (n =z 0) then λx,y. (x = y ∈ T) else λx,y. ∃z:T. ((x R z) ∧ (z (rel_exp (n - 1)) y)) fi )) n
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
infix_ap: x f y,
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
subtract: n - m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
fix: fix(F),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
equal: s = t ∈ T,
lambda: λx.A[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
infix_ap: x f y,
apply: f a,
subtract: n - m,
natural_number: $n
FDL editor aliases :
rel_exp
rel_exp
Latex:
rel\_exp(T; R; n) ==
fix((\mlambda{}rel$_{exp}$,n. if (n =\msubz{} 0) then \mlambda{}x,y. (x = y) else \mlambda{}x,y. \mexists{}z:T. ((x R z) \000C\mwedge{} (z (rel$_{exp}$ (n - 1)) y)) fi )) n
Date html generated:
2016_05_13-PM-04_18_41
Last ObjectModification:
2015_09_22-PM-05_46_45
Theory : relations
Home
Index