Nuprl Definition : coPath
coPath(a.B[a];w;n) == if (n =z 0) then Top else t:coW-dom(a.B[a];w) × coPath(a.B[a];coW-item(w;t);n - 1) fi
Definitions occuring in Statement :
coW-item: coW-item(w;b),
coW-dom: coW-dom(a.B[a];w),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
top: Top,
product: x:A × B[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
top: Top,
product: x:A × B[x],
coW-dom: coW-dom(a.B[a];w),
coW-item: coW-item(w;b),
subtract: n - m,
natural_number: $n
FDL editor aliases :
coPath
Latex:
coPath(a.B[a];w;n) ==
if (n =\msubz{} 0) then Top else t:coW-dom(a.B[a];w) \mtimes{} coPath(a.B[a];coW-item(w;t);n - 1) fi
Date html generated:
2018_07_25-PM-01_37_44
Last ObjectModification:
2018_06_01-AM-09_51_43
Theory : co-recursion
Home
Index