| 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= j i else x fi |
| | Thm* k: , i,j: k. (i, j) k  k |
|
map | Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')]
Def (recursive) |
| | Thm* A,B:Type, f:(A B), l:A List. map(f;l) B List |
| | Thm* A,B:Type, f:(A B), 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:(T T) List. compose_list(L) T T |
|
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:(B C), g:(A B). f o g A C |
|
reduce | Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as'))
Def (recursive) |
| | Thm* A,B:Type, f:(A B B), k:B, as:A List. reduce(f;k;as) B |