Thm* L:T List, P:(T T Prop).
Thm* ( x,y:T. Dec(P(x,y)))
Thm* 
Thm* ( x,y:T. P(x,y)  P(y,x))
Thm* 
Thm* ( L':T List.
Thm* ((L (swap adjacent[ P(x,y)]^*) L') & ( i: (||L'||-1). P(L'[i],L'[(i+1)]))) | [partial_sort] |
Thm* L:T List, P:(T T  ).
Thm* ( x,y:T. P(x,y)  P(y,x))
Thm* 
Thm* ( L':T List.
Thm* ((L guarded_permutation(T; L,i. P(L[i],L[(i+1)])) L')
Thm* (& ( i: (||L'||-1). P(L'[i],L'[(i+1)]))) | [partial_sort_exists_2] |
Thm* k: , p:( k  k). Bij( k; k; p)  ( L: (k-1) List. p = compose_flips(L)) | [permute_by_flips] |
Thm* k: , x,y: k. L: (k-1) List. (x, y) = compose_flips(L) | [flip_adjacent] |
Thm* n: , R:( n  n Prop), x,y: n. (x (R^*) y)  ( k: (n+1). x R^k y) | [rel_star_finite] |
Thm* R:(T T Prop), k: , x,y:T.
Thm* (x R^k y)
Thm* 
Thm* ( L:T List.
Thm* (||L|| = k+1 & L[0] = x & last(L) = y & ( i: k. L[i] R L[(i+1)])) | [rel_exp_list] |
Thm* P:(L:(T List)  (||L||-1)  ), m:((T List)  ).
Thm* ( L:T List, i: (||L||-1).
Thm* (P(L,i)  P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L))
Thm* 
Thm* ( L:T List.
Thm* ( L':T List.
Thm* ((L guarded_permutation(T; L,i. P(L,i)) L') & ( i: (||L'||-1). P(L',i))) | [partial_sort_exists] |
Thm* i: , L:A List.
Thm* i+1<||L||
Thm* 
Thm* ( X,Y:A List.
Thm* (L = (X @ [L[i]; L[(i+1)]] @ Y)
Thm* (& swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y)) | [swap_adjacent_decomp] |
Thm* L:T List, P:( ||L|| Prop).
Thm* ( x: ||L||. Dec(P(x)))
Thm* 
Thm* ( i: ||L||. P(i))  ( i: ||L||. P(i) & ( j: ||L||. i<j  P(j))) | [last_with_property] |
Thm* L:T List, P:( ||L|| Prop).
Thm* ( x: ||L||. Dec(P(x)))
Thm* 
Thm* ( L1,L2:T List, f1:( ||L1||  ||L||), f2:( ||L2||  ||L||).
Thm* (interleaving_occurence(T;L1;L2;L;f1;f2)
Thm* (& ( i: ||L1||. P(f1(i))) & ( i: ||L2||. P(f2(i)))
Thm* (& ( i: ||L||.
Thm* (& ((P(i)  ( j: ||L1||. f1(j) = i))
Thm* (& (& ( P(i)  ( j: ||L2||. f2(j) = i)))) | [interleaving_split] |
Thm* L:T List, n: , f:( n  ||L||).
Thm* increasing(f;n)
Thm* 
Thm* ( L1:T List. ||L1|| = n & sublist_occurence(T;L1;L;f)) | [range_sublist] |
Thm* P:(T  ), T':Type, f:({x:T| P(x) } T'), L:T List, x:T'.
Thm* (x mapfilter(f;P;L))  ( y:T. (y L) & P(y) & x = f(y)) | [member_map_filter] |
Def swap adjacent[P(x;y)](L1,L2)
Def == i: (||L1||-1). P(L1[i];L1[(i+1)]) & L2 = swap(L1;i;i+1) A List | [swap_adjacent] |
Def guarded_permutation(T;P)
Def == ( L1,L2. i: (||L1||-1). P(L1,i) & L2 = swap(L1;i;i+1) T List)^* | [guarded_permutation] |
Def disjoint_sublists(T;L1;L2;L)
Def == f1:( ||L1||  ||L||), f2:( ||L2||  ||L||).
Def == increasing(f1;||L1||) & ( j: ||L1||. L1[j] = L[(f1(j))] T)
Def == & increasing(f2;||L2||) & ( j: ||L2||. L2[j] = L[(f2(j))] T)
Def == & ( j1: ||L1||, j2: ||L2||. f1(j1) = f2(j2)) | [disjoint_sublists] |
Def ( x L.P(x)) == x:T. (x L) & P(x) | [l_exists] |