(VAR IL L M N V1 V2 V ) (STRATEGY CONTEXTSENSITIVE (cons-Nat-NatIList 1) (cons-Nat-NatList 1) (cons-Nat-os-osb-NatIList-os-csb 1) (cons-os-osb-Nat-os-csb-NatIList 1) (cons-os-osb-Nat-os-csb-NatList 1) (cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb 1) ) (RULES zeros -> cons-Nat-NatIList (0 ,zeros ) cons-Nat-NatIList (V1 ,V2 )-> cons-Nat-NatList (V1 ,V2 ) cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> cons-Nat-NatIList ( V1 ,V2 ) cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> cons-Nat-NatList (V1 ,V2 ) cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> cons-Nat-os-osb-NatIList-os-csb (V1 ,V2 ) cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> cons-os-osb-Nat-os-csb-NatIList (V1 ,V2 ) cons-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> cons-os-osb-Nat-os-csb-NatList (V1 ,V2 ) is'Nat-Nat (V )-> tt is'Nat-os-osb-Nat-os-csb (V1 )-> is'Nat-Nat (V1 ) is'NatIList-NatIList (V )-> tt is'NatIList-NatList (V )-> tt is'NatIList-os-osb-NatIList-os-csb (V1 )-> is'NatIList-NatIList (V1 ) is'NatIList-os-osb-NatIList-os-csb (V1 )-> is'NatIList-NatList (V1 ) is'NatList-NatList (V )-> tt is'NatList-os-osb-NatIList-os-csb (V1 )-> is'NatList-NatIList (V1 ) is'NatList-os-osb-NatIList-os-csb (V1 )-> is'NatList-NatList (V1 ) is'Thruth-Thruth (V )-> tt is'Thruth-os-osb-Thruth-os-csb (V1 )-> is'Thruth-Thruth (V1 ) length-NatList (nil )-> 0 length-NatList (cons-Nat-NatList (N ,L ))-> s-Nat (length-NatList (L )) length-os-osb-NatIList-os-csb (V1 )-> length-NatIList (V1 ) length-os-osb-NatIList-os-csb (V1 )-> length-NatList (V1 ) s-os-osb-Nat-os-csb (V1 )-> s-Nat (V1 ) take-Nat-NatIList (0 ,IL )-> nil take-Nat-NatIList (V1 ,V2 )-> take-Nat-NatList (V1 ,V2 ) take-Nat-NatIList (s-Nat (M ),cons-Nat-NatIList (N ,IL ))-> cons-Nat-NatList ( N ,take-Nat-NatIList (M ,IL )) take-Nat-NatList (0 ,IL )-> nil take-Nat-NatList (s-Nat (M ),cons-Nat-NatList (N ,IL ))-> cons-Nat-NatList (N ,take-Nat-NatList (M ,IL )) take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> take-Nat-NatIList ( V1 ,V2 ) take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> take-Nat-NatList (V1 ,V2 ) take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> take-Nat-os-osb-NatIList-os-csb (V1 ,V2 ) take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> take-os-osb-Nat-os-csb-NatIList (V1 ,V2 ) take-os-osb-Nat-os-csb-os-osb-NatIList-os-csb (V1 ,V2 )-> take-os-osb-Nat-os-csb-NatList (V1 ,V2 ) )