Thm* P:(A A Prop), f:(B A), x,y:B List.
Thm* (x swap adjacent[P(f(x),f(y))] y)
Thm* 
Thm* (map(f;x) swap adjacent[P(x,y)] map(f;y)) | [swap_adjacent_map] |
Thm* P:(A A Prop), f:(A  ), L1,L2:A List.
Thm* (L1 swap adjacent[P(x,y)] L2)
Thm* 
Thm* (filter(f;L1) swap adjacent[P(x,y)] filter(f;L2))
Thm* filter(f;L1) = filter(f;L2) | [filter_swap_adjacent] |
Thm* P:(A A Prop), X,Y:A List, a,b:A.
Thm* P(a,b)  ((X @ [a; b] @ Y) swap adjacent[P(x,y)] (X @ [b; a] @ Y)) | [swap_adjacent_instance] |
Thm* P:(A A Prop).
Thm* (Sym x,y:A. P(x,y))  (Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2) | [symmetric_swap_adjacent] |
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* n: , R:( n  n Prop). ( i,j: n. Dec(i R j))  ( i,j: n. Dec(i (R^*) j)) | [decidable__rel_star] |
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) Prop).
Thm* Trans(T List)(_1 guarded_permutation(T;P) _2) | [guarded_permutation_transitivity] |
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* F:(A Prop), L:A List. ( k:A. Dec(F(k)))  Dec(( k L.F(k))) | [decidable__l_exists] |
Thm* P:(T Prop), x:T, L:T List. ( y [x / L].P(y))  P(x) ( y L.P(y)) | [l_exists_cons] |
Thm* P:(T Prop). ( x nil.P(x))  False | [l_exists_nil] |
Thm* F:(A Prop), L:A List. ( k:A. Dec(F(k)))  Dec(( k L.F(k))) | [decidable__l_all] |
Thm* P:(T Prop). ( x nil.P(x)) | [l_all_nil] |
Thm* f:(A B), L:A List, P:(B Prop). ( x map(f;L).P(x))  ( x L.P(f(x))) | [l_all_map] |
Thm* L:T List, P:(T Prop). ( x L.P(x))  L {x:T| P(x) } List | [list_set_type] |
Thm* P:(T Prop), x:T, L:T List. ( y [x / L].P(y))  P(x) & ( y L.P(y)) | [l_all_cons] |