Nuprl Definition : transitive-closure
TC(R) == λx,y. {L:(a:A × b:A × (R a b)) List| rel_path(A;L;x;y) ∧ 0 < ||L||}
Definitions occuring in Statement :
rel_path: rel_path(A;L;x;y),
length: ||as||,
list: T List,
less_than: a < b,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
set: {x:A| B[x]} ,
list: T List,
product: x:A × B[x],
apply: f a,
and: P ∧ Q,
rel_path: rel_path(A;L;x;y),
less_than: a < b,
natural_number: $n,
length: ||as||
FDL editor aliases :
transitive-closure
Latex:
TC(R) == \mlambda{}x,y. \{L:(a:A \mtimes{} b:A \mtimes{} (R a b)) List| rel\_path(A;L;x;y) \mwedge{} 0 < ||L||\}
Date html generated:
2016_05_14-PM-03_51_06
Last ObjectModification:
2015_09_22-PM-06_01_46
Theory : relations2
Home
Index