| | Who Cites compose flips? |
|
| compose_flips | Def compose_flips(L) == compose_list(map( i.(i, i+1);L)) |
| | | Thm*  k: , L:(k-1) List. compose_flips(L)  k  k |
|
| flip | Def (i, j)(x) == if x= i j ;x=ji else x fi |
| | | Thm* k:, i,j:k. (i, j) kk |
|
| map | Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')] (recursive) |
| | | Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List |
| | | Thm* A,B:Type, f:(AB), l:A List . map(f;l) B 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 |
|
| eq_int | Def i=j == if i=j true ; false fi |
| | | Thm* i,j: . (i=j)  |
|
| 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 |
