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:
2019_06_20-PM-00_56_11
Last ObjectModification:
2019_01_02-PM-01_32_52
Theory : co-recursion-2
Home
Index