WORST_CASE(?,O(n^2)) Solution: --------- #0 :: [] -(0)-> A(0, 0) #EQ :: [] -(0)-> A(3, 3) #EQ :: [] -(0)-> A(10, 10) #GT :: [] -(0)-> A(3, 3) #GT :: [] -(0)-> A(10, 10) #LT :: [] -(0)-> A(3, 3) #LT :: [] -(0)-> A(10, 10) #and :: [A(1, 1) x A(1, 1)] -(0)-> A(12, 4) #cklt :: [A(3, 3)] -(0)-> A(7, 7) #compare :: [A(0, 0) x A(0, 0)] -(0)-> A(4, 4) #eq :: [A(0, 0) x A(0, 0)] -(0)-> A(12, 4) #equal :: [A(0, 0) x A(1, 0)] -(1)-> A(11, 3) #false :: [] -(0)-> A(0, 1) #false :: [] -(0)-> A(1, 1) #false :: [] -(0)-> A(7, 0) #false :: [] -(0)-> A(15, 15) #false :: [] -(0)-> A(15, 11) #false :: [] -(0)-> A(13, 13) #less :: [A(0, 0) x A(2, 0)] -(1)-> A(7, 7) #neg :: [A(0, 0)] -(0)-> A(0, 0) #or :: [A(1, 1) x A(7, 0)] -(0)-> A(15, 15) #pos :: [A(0, 0)] -(0)-> A(0, 0) #s :: [A(0, 0)] -(0)-> A(0, 0) #true :: [] -(0)-> A(0, 1) #true :: [] -(0)-> A(1, 1) #true :: [] -(0)-> A(7, 0) #true :: [] -(0)-> A(15, 15) #true :: [] -(0)-> A(15, 11) #true :: [] -(0)-> A(13, 13) :: :: [A(7, 0) x A(7, 0)] -(7)-> A(7, 0) :: :: [A(7, 0) x A(15, 8)] -(7)-> A(7, 8) :: :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) :: :: [A(1, 0) x A(7, 6)] -(1)-> A(1, 6) and :: [A(9, 1) x A(12, 12)] -(1)-> A(12, 4) insert :: [A(6, 0) x A(7, 0)] -(4)-> A(0, 0) insert#1 :: [A(7, 0) x A(6, 0)] -(3)-> A(0, 0) insert#2 :: [A(0, 1) x A(6, 0) x A(0, 0) x A(7, 0)] -(5)-> A(0, 0) isortlist :: [A(15, 8)] -(4)-> A(7, 0) isortlist#1 :: [A(7, 8)] -(3)-> A(0, 0) leq :: [A(0, 0) x A(7, 0)] -(3)-> A(9, 10) leq#1 :: [A(0, 0) x A(7, 0)] -(2)-> A(8, 9) leq#2 :: [A(7, 0) x A(0, 0) x A(0, 0)] -(1)-> A(8, 8) nil :: [] -(0)-> A(7, 0) nil :: [] -(0)-> A(7, 8) nil :: [] -(0)-> A(0, 0) nil :: [] -(0)-> A(15, 15) nil :: [] -(0)-> A(7, 7) or :: [A(1, 1) x A(8, 0)] -(1)-> A(13, 13) Cost Free Signatures: --------------------- #0 :: [] -(0)-> A_cf(0, 0) #EQ :: [] -(0)-> A_cf(0, 0) #EQ :: [] -(0)-> A_cf(14, 14) #GT :: [] -(0)-> A_cf(0, 0) #GT :: [] -(0)-> A_cf(14, 14) #LT :: [] -(0)-> A_cf(0, 0) #LT :: [] -(0)-> A_cf(14, 14) #and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #and :: [A_cf(3, 0) x A_cf(3, 3)] -(0)-> A_cf(10, 8) #and :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #and :: [A_cf(0, 1) x A_cf(0, 1)] -(0)-> A_cf(14, 14) #and :: [A_cf(7, 7) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 14) #and :: [A_cf(0, 7) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #and :: [A_cf(3, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 14) #and :: [A_cf(3, 0) x A_cf(3, 4)] -(0)-> A_cf(14, 14) #and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 8) #cklt :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #cklt :: [A_cf(0, 0)] -(0)-> A_cf(15, 15) #compare :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #compare :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(10, 8) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 10) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 12) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 8) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(4, 8) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(9, 4) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(10, 10) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(4, 9) #false :: [] -(0)-> A_cf(0, 0) #false :: [] -(0)-> A_cf(0, 1) #false :: [] -(0)-> A_cf(15, 15) #false :: [] -(0)-> A_cf(11, 11) #false :: [] -(0)-> A_cf(3, 0) #false :: [] -(0)-> A_cf(3, 3) #false :: [] -(0)-> A_cf(1, 3) #false :: [] -(0)-> A_cf(7, 0) #false :: [] -(0)-> A_cf(15, 11) #false :: [] -(0)-> A_cf(7, 7) #false :: [] -(0)-> A_cf(11, 15) #false :: [] -(0)-> A_cf(0, 7) #false :: [] -(0)-> A_cf(11, 14) #false :: [] -(0)-> A_cf(3, 4) #false :: [] -(0)-> A_cf(15, 14) #false :: [] -(0)-> A_cf(14, 14) #false :: [] -(0)-> A_cf(2, 10) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 12) #neg :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #or :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #or :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #pos :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #true :: [] -(0)-> A_cf(0, 0) #true :: [] -(0)-> A_cf(0, 1) #true :: [] -(0)-> A_cf(15, 15) #true :: [] -(0)-> A_cf(11, 11) #true :: [] -(0)-> A_cf(3, 3) #true :: [] -(0)-> A_cf(3, 0) #true :: [] -(0)-> A_cf(1, 3) #true :: [] -(0)-> A_cf(7, 0) #true :: [] -(0)-> A_cf(15, 11) #true :: [] -(0)-> A_cf(7, 7) #true :: [] -(0)-> A_cf(0, 7) #true :: [] -(0)-> A_cf(11, 14) #true :: [] -(0)-> A_cf(3, 4) #true :: [] -(0)-> A_cf(15, 14) #true :: [] -(0)-> A_cf(14, 14) #true :: [] -(0)-> A_cf(2, 10) :: :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) :: :: [A_cf(0, 0) x A_cf(9, 9)] -(0)-> A_cf(0, 9) :: :: [A_cf(8, 0) x A_cf(8, 0)] -(8)-> A_cf(8, 0) :: :: [A_cf(7, 0) x A_cf(7, 0)] -(7)-> A_cf(7, 0) :: :: [A_cf(7, 0) x A_cf(15, 8)] -(7)-> A_cf(7, 8) and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) and :: [A_cf(4, 4) x A_cf(12, 9)] -(0)-> A_cf(12, 12) and :: [A_cf(8, 4) x A_cf(8, 8)] -(0)-> A_cf(12, 12) and :: [A_cf(8, 8) x A_cf(0, 0)] -(0)-> A_cf(12, 12) and :: [A_cf(0, 8) x A_cf(0, 0)] -(0)-> A_cf(12, 12) and :: [A_cf(4, 8) x A_cf(0, 4)] -(0)-> A_cf(12, 12) insert :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) insert :: [A_cf(8, 0) x A_cf(7, 0)] -(7)-> A_cf(7, 0) insert#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) insert#1 :: [A_cf(7, 0) x A_cf(8, 0)] -(7)-> A_cf(7, 0) insert#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) insert#2 :: [A_cf(0, 1) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) insert#2 :: [A_cf(1, 3) x A_cf(8, 0) x A_cf(7, 0) x A_cf(7, 0)] -(14)-> A_cf(7, 0) isortlist :: [A_cf(8, 0)] -(0)-> A_cf(7, 0) isortlist :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) isortlist#1 :: [A_cf(8, 0)] -(0)-> A_cf(7, 0) isortlist#1 :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 12) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(10, 10) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 1) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(4, 4) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 12) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(1, 1) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 1) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 14) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 15) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 1) nil :: [] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(15, 11) nil :: [] -(0)-> A_cf(8, 0) nil :: [] -(0)-> A_cf(7, 0) nil :: [] -(0)-> A_cf(11, 2) or :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) or :: [A_cf(4, 4) x A_cf(4, 4)] -(0)-> A_cf(14, 14) or :: [A_cf(4, 4) x A_cf(4, 4)] -(0)-> A_cf(12, 12) or :: [A_cf(4, 4) x A_cf(4, 4)] -(0)-> A_cf(14, 15) Base Constructors: ------------------ #0_A :: [] -(0)-> A(0) #EQ_A :: [] -(0)-> A(0) #GT_A :: [] -(0)-> A(0) #LT_A :: [] -(0)-> A(0) #false_A :: [] -(0)-> A(0) #neg_A :: [A(0)] -(0)-> A(0) #pos_A :: [A(0)] -(0)-> A(0) #s_A :: [A(0)] -(0)-> A(0) #true_A :: [] -(0)-> A(0) ::_A :: [A(0) x A(0)] -(0)-> A(0) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1)