Some theorems about sorted lists, based on the above implementation of permutations.
** Module lib_list_sorted Imports lib_list_PermII * lengthisahomomorphismcons = ... : {A|Type}{l|list A}{n|nat}(Eq (suc n) (length l))-> Ex ([a:A]Eq l (cons a (tail l))) Rlist = ... : {A|Type}(Rel A A)->A->Pred (list A) Sorted = ... : {A|Type}(Rel A A)->Pred (list A) SortSpec = ... : {A|Type}(Rel A A)->Rel (list A) (list A) * sortedlistinduction = ... : {A|Type}{R:Rel A A}{B|Type}{phi:Rel (list A) B}{n|B} {c|A->(list A)->B->B}(phi (nil A) n)-> ({a|A}{l|list A}{b|B}(Sorted R (cons a l))->(phi l b)-> phi (cons a l) (c a l b))->{l:list A}(Sorted R l)-> phi l (list_rec n ([a:A][l'12:list A][b:B]c a l'12 b) l) * nilSorted = ... : {A|Type}{R:Rel A A}Sorted R (nil A) * nilRlist = ... : {A|Type}{R:Rel A A}{c|A}Rlist R c (nil A) * heredSortedlemma = ... : {A|Type}{R:Rel A A}{b|A}{n|list A}(Sorted R (cons b n))->Sorted R n * SortedImpliesRlist = ... : {A|Type}{R:Rel A A}{b|A}{n|list A}(Sorted R (cons b n))->Rlist R b n * heredRlistlemma = ... : {A|Type}{R:Rel A A}{b,c|A}{n|list A}(Rlist R c (cons b n))-> Rlist R c n * heredRlist1 = ... : {A|Type}{R:Rel A A}{c|A}{m,n|list A}(Rlist R c (append m n))-> Rlist R c n * heredRlist2 = ... : {A|Type}{R:Rel A A}{c|A}{m,n|list A}(Rlist R c (append m n))-> Rlist R c m * appclRlist = ... : {A|Type}{R:Rel A A}{c|A}{m,n|list A}(Rlist R c m)->(Rlist R c n)-> Rlist R c (append m n) * heredSorted = ... : {A|Type}{R:Rel A A}{m,n|list A}(Sorted R (append m n))-> and (Sorted R m) (Sorted R n) * RlistIsMonotone = ... : {A|Type}{R:Rel A A}(trans R)->{b,c|A}{m|list A}(R c b)-> (Rlist R b m)->Rlist R c m * PermPreservesRlist = ... : {A|Type}{R:Rel A A}{c|A}{m,n|list A}(Perm m n)->(Rlist R c m)-> Rlist R c n * SortedPermsHaveRHeads = ... : {A|Type}{R:Rel A A}(refl R)->{b,c|A}{m,n|list A} (Sorted R (cons b m))->(Sorted R (cons c n))-> (Perm (cons b m) (cons c n))->R b c * SortedPermsHaveEqualHeads = ... : {A|Type}{R:Rel A A}(refl R)->({a,b|A}(R a b)->(R b a)->Eq a b)-> {b,c|A}{m,n|list A}(Sorted R (cons b m))->(Sorted R (cons c n))-> (Perm (cons b m) (cons c n))->Eq b c * SortedPermsAreEqual = ... : {A|Type}{R:Rel A A}(refl R)->({a,b|A}(R a b)->(R b a)->Eq a b)-> {l,m|list A}(Sorted R l)->(Sorted R m)->(Perm l m)->Eq l m