p,q. p o q;x.x;L)
T:Type, L:(T
T) List. compose_list(L) 
TTA,B,C:Type, f:(BC), g:(AB). f o g AC
k ; a.as' f(a,reduce(f;k;as')) (recursive)A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B| Who Cites compose list? | |
| compose_list | Def compose_list(L) == reduce(p,q. p o q;x.x;L) |
| Thm* T:Type, L:(TT) List. compose_list(L) TT | |
| compose | Def (f o g)(x) == f(g(x)) |
| Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC | |
| reduce | Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive) |
| Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B |
About:
 |  |  |  |
 |  |  |  |  |  |