WORST_CASE(?,O(n^2)) * Step 1: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(add(N,X),Y) -> add(N,append(X,Y)) append(nil(),Y) -> Y f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z) f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) -> true() lt(s(X),0()) -> false() lt(s(X),s(Y)) -> lt(X,Y) qsort(add(N,X)) -> f_3(split(N,X),N,X) qsort(nil()) -> nil() split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) split(N,nil()) -> pair(nil(),nil()) - Signature: {append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0,add/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,f_1,f_2,f_3,lt,qsort,split} and constructors {0 ,add,false,nil,pair,s,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(append) = {1,2}, uargs(f_1) = {1}, uargs(f_2) = {1}, uargs(f_3) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] p(add) = [1] x2 + [2] p(append) = [1] x1 + [1] x2 + [0] p(f_1) = [1] x1 + [4] p(f_2) = [1] x1 + [1] x5 + [0] p(f_3) = [1] x1 + [4] p(false) = [0] p(lt) = [5] p(nil) = [6] p(pair) = [1] x1 + [1] p(qsort) = [1] p(s) = [1] p(split) = [0] p(true) = [2] Following rules are strictly oriented: append(nil(),Y) = [1] Y + [6] > [1] Y + [0] = Y f_2(true(),N,M,Y,X,Z) = [1] X + [2] > [1] X + [1] = pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) = [1] Y + [5] > [4] = append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) = [5] > [2] = true() lt(s(X),0()) = [5] > [0] = false() Following rules are (at-least) weakly oriented: append(add(N,X),Y) = [1] X + [1] Y + [2] >= [1] X + [1] Y + [2] = add(N,append(X,Y)) f_1(pair(X,Z),N,M,Y) = [1] X + [5] >= [1] X + [5] = f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) = [1] X + [0] >= [1] X + [3] = pair(add(M,X),Z) lt(s(X),s(Y)) = [5] >= [5] = lt(X,Y) qsort(add(N,X)) = [1] >= [4] = f_3(split(N,X),N,X) qsort(nil()) = [1] >= [6] = nil() split(N,add(M,Y)) = [0] >= [4] = f_1(split(N,Y),N,M,Y) split(N,nil()) = [0] >= [7] = pair(nil(),nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(add(N,X),Y) -> add(N,append(X,Y)) f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z) lt(s(X),s(Y)) -> lt(X,Y) qsort(add(N,X)) -> f_3(split(N,X),N,X) qsort(nil()) -> nil() split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) split(N,nil()) -> pair(nil(),nil()) - Weak TRS: append(nil(),Y) -> Y f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) -> true() lt(s(X),0()) -> false() - Signature: {append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0,add/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,f_1,f_2,f_3,lt,qsort,split} and constructors {0 ,add,false,nil,pair,s,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(append) = {1,2}, uargs(f_1) = {1}, uargs(f_2) = {1}, uargs(f_3) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(add) = [1] x2 + [1] p(append) = [1] x1 + [1] x2 + [1] p(f_1) = [1] x1 + [1] p(f_2) = [1] x1 + [2] p(f_3) = [1] x1 + [6] p(false) = [0] p(lt) = [1] p(nil) = [0] p(pair) = [3] p(qsort) = [3] p(s) = [1] p(split) = [7] p(true) = [1] Following rules are strictly oriented: f_1(pair(X,Z),N,M,Y) = [4] > [3] = f_2(lt(N,M),N,M,Y,X,Z) qsort(nil()) = [3] > [0] = nil() split(N,nil()) = [7] > [3] = pair(nil(),nil()) Following rules are (at-least) weakly oriented: append(add(N,X),Y) = [1] X + [1] Y + [2] >= [1] X + [1] Y + [2] = add(N,append(X,Y)) append(nil(),Y) = [1] Y + [1] >= [1] Y + [0] = Y f_2(false(),N,M,Y,X,Z) = [2] >= [3] = pair(add(M,X),Z) f_2(true(),N,M,Y,X,Z) = [3] >= [3] = pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) = [9] >= [8] = append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) = [1] >= [1] = true() lt(s(X),0()) = [1] >= [0] = false() lt(s(X),s(Y)) = [1] >= [1] = lt(X,Y) qsort(add(N,X)) = [3] >= [13] = f_3(split(N,X),N,X) split(N,add(M,Y)) = [7] >= [8] = f_1(split(N,Y),N,M,Y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(add(N,X),Y) -> add(N,append(X,Y)) f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z) lt(s(X),s(Y)) -> lt(X,Y) qsort(add(N,X)) -> f_3(split(N,X),N,X) split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) - Weak TRS: append(nil(),Y) -> Y f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z) f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) -> true() lt(s(X),0()) -> false() qsort(nil()) -> nil() split(N,nil()) -> pair(nil(),nil()) - Signature: {append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0,add/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,f_1,f_2,f_3,lt,qsort,split} and constructors {0 ,add,false,nil,pair,s,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(append) = {1,2}, uargs(f_1) = {1}, uargs(f_2) = {1}, uargs(f_3) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(add) = [1] x2 + [0] p(append) = [1] x1 + [1] x2 + [1] p(f_1) = [1] x1 + [1] p(f_2) = [1] x1 + [1] x5 + [2] p(f_3) = [1] x1 + [0] p(false) = [1] p(lt) = [1] p(nil) = [0] p(pair) = [1] x1 + [2] p(qsort) = [0] p(s) = [1] x1 + [0] p(split) = [2] p(true) = [1] Following rules are strictly oriented: f_2(false(),N,M,Y,X,Z) = [1] X + [3] > [1] X + [2] = pair(add(M,X),Z) Following rules are (at-least) weakly oriented: append(add(N,X),Y) = [1] X + [1] Y + [1] >= [1] X + [1] Y + [1] = add(N,append(X,Y)) append(nil(),Y) = [1] Y + [1] >= [1] Y + [0] = Y f_1(pair(X,Z),N,M,Y) = [1] X + [3] >= [1] X + [3] = f_2(lt(N,M),N,M,Y,X,Z) f_2(true(),N,M,Y,X,Z) = [1] X + [3] >= [1] X + [2] = pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) = [1] Y + [2] >= [1] = append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) = [1] >= [1] = true() lt(s(X),0()) = [1] >= [1] = false() lt(s(X),s(Y)) = [1] >= [1] = lt(X,Y) qsort(add(N,X)) = [0] >= [2] = f_3(split(N,X),N,X) qsort(nil()) = [0] >= [0] = nil() split(N,add(M,Y)) = [2] >= [3] = f_1(split(N,Y),N,M,Y) split(N,nil()) = [2] >= [2] = pair(nil(),nil()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(add(N,X),Y) -> add(N,append(X,Y)) lt(s(X),s(Y)) -> lt(X,Y) qsort(add(N,X)) -> f_3(split(N,X),N,X) split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) - Weak TRS: append(nil(),Y) -> Y f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z) f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) -> true() lt(s(X),0()) -> false() qsort(nil()) -> nil() split(N,nil()) -> pair(nil(),nil()) - Signature: {append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0,add/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,f_1,f_2,f_3,lt,qsort,split} and constructors {0 ,add,false,nil,pair,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(append) = {1,2}, uargs(f_1) = {1}, uargs(f_2) = {1}, uargs(f_3) = {1} Following symbols are considered usable: {append,f_1,f_2,f_3,lt,qsort,split} TcT has computed the following interpretation: p(0) = [1] p(add) = [1] x2 + [6] p(append) = [1] x1 + [1] x2 + [0] p(f_1) = [1] x1 + [6] p(f_2) = [4] x1 + [1] x5 + [1] x6 + [2] p(f_3) = [4] x1 + [15] p(false) = [1] p(lt) = [1] p(nil) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(qsort) = [4] x1 + [4] p(s) = [1] x1 + [0] p(split) = [1] x2 + [0] p(true) = [1] Following rules are strictly oriented: qsort(add(N,X)) = [4] X + [28] > [4] X + [15] = f_3(split(N,X),N,X) Following rules are (at-least) weakly oriented: append(add(N,X),Y) = [1] X + [1] Y + [6] >= [1] X + [1] Y + [6] = add(N,append(X,Y)) append(nil(),Y) = [1] Y + [0] >= [1] Y + [0] = Y f_1(pair(X,Z),N,M,Y) = [1] X + [1] Z + [6] >= [1] X + [1] Z + [6] = f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) = [1] X + [1] Z + [6] >= [1] X + [1] Z + [6] = pair(add(M,X),Z) f_2(true(),N,M,Y,X,Z) = [1] X + [1] Z + [6] >= [1] X + [1] Z + [6] = pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) = [4] Y + [4] Z + [15] >= [4] Y + [4] Z + [14] = append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) = [1] >= [1] = true() lt(s(X),0()) = [1] >= [1] = false() lt(s(X),s(Y)) = [1] >= [1] = lt(X,Y) qsort(nil()) = [4] >= [0] = nil() split(N,add(M,Y)) = [1] Y + [6] >= [1] Y + [6] = f_1(split(N,Y),N,M,Y) split(N,nil()) = [0] >= [0] = pair(nil(),nil()) * Step 5: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(add(N,X),Y) -> add(N,append(X,Y)) lt(s(X),s(Y)) -> lt(X,Y) split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) - Weak TRS: append(nil(),Y) -> Y f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z) f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) -> true() lt(s(X),0()) -> false() qsort(add(N,X)) -> f_3(split(N,X),N,X) qsort(nil()) -> nil() split(N,nil()) -> pair(nil(),nil()) - Signature: {append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0,add/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,f_1,f_2,f_3,lt,qsort,split} and constructors {0 ,add,false,nil,pair,s,true} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0, 0) 0 :: [] -(0)-> A(1, 0) add :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) add :: [A(4, 0) x A(9, 5)] -(4)-> A(4, 5) add :: [A(1, 0) x A(6, 5)] -(1)-> A(1, 5) append :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) f_1 :: [A(6, 5) x A(0, 0) x A(4, 0) x A(0, 0)] -(1)-> A(1, 5) f_2 :: [A(5, 5) x A(0, 0) x A(1, 0) x A(0, 0) x A(6, 5) x A(6, 5)] -(1)-> A(1, 5) f_3 :: [A(1, 5) x A(0, 0) x A(0, 0)] -(0)-> A(0, 0) false :: [] -(0)-> A(5, 5) false :: [] -(0)-> A(15, 15) lt :: [A(0, 0) x A(1, 0)] -(0)-> A(13, 13) nil :: [] -(0)-> A(0, 0) nil :: [] -(0)-> A(1, 5) nil :: [] -(0)-> A(4, 5) nil :: [] -(0)-> A(7, 7) nil :: [] -(0)-> A(15, 15) pair :: [A(6, 5) x A(6, 5)] -(0)-> A(6, 5) pair :: [A(1, 5) x A(1, 5)] -(0)-> A(1, 5) pair :: [A(7, 6) x A(7, 6)] -(0)-> A(7, 6) qsort :: [A(1, 5)] -(0)-> A(0, 0) s :: [A(0, 0)] -(0)-> A(0, 0) s :: [A(1, 0)] -(1)-> A(1, 0) split :: [A(0, 0) x A(4, 5)] -(0)-> A(1, 5) true :: [] -(0)-> A(5, 5) true :: [] -(0)-> A(15, 15) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) add :: [A_cf(5, 0) x A_cf(5, 0)] -(5)-> A_cf(5, 0) append :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_1 :: [A_cf(5, 0) x A_cf(0, 0) x A_cf(5, 0) x A_cf(0, 0)] -(5)-> A_cf(5, 0) f_1 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(5, 0) x A_cf(0, 0) x A_cf(5, 0) x A_cf(5, 0)] -(5)-> A_cf(5, 0) f_2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_3 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) false :: [] -(0)-> A_cf(0, 0) false :: [] -(0)-> A_cf(10, 10) lt :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) lt :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 8) nil :: [] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(5, 0) nil :: [] -(0)-> A_cf(15, 15) pair :: [A_cf(5, 0) x A_cf(5, 0)] -(0)-> A_cf(5, 0) pair :: [A_cf(14, 13) x A_cf(14, 13)] -(0)-> A_cf(14, 13) pair :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) qsort :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) split :: [A_cf(0, 0) x A_cf(5, 0)] -(1)-> A_cf(5, 0) split :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) true :: [] -(0)-> A_cf(0, 0) true :: [] -(0)-> A_cf(10, 10) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1, 0) 0_A :: [] -(0)-> A(0, 1) add_A :: [A(1, 0) x A(1, 0)] -(1)-> A(1, 0) add_A :: [A(0, 0) x A(1, 1)] -(0)-> A(0, 1) false_A :: [] -(0)-> A(1, 0) false_A :: [] -(0)-> A(0, 1) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) pair_A :: [A(1, 0) x A(1, 0)] -(0)-> A(1, 0) pair_A :: [A(0, 1) x A(0, 1)] -(0)-> A(0, 1) s_A :: [A(1, 0)] -(1)-> A(1, 0) s_A :: [A(0, 0)] -(0)-> A(0, 1) true_A :: [] -(0)-> A(1, 0) true_A :: [] -(0)-> A(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: lt(s(X),s(Y)) -> lt(X,Y) 2. Weak: append(add(N,X),Y) -> add(N,append(X,Y)) split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) * Step 6: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(add(N,X),Y) -> add(N,append(X,Y)) split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) - Weak TRS: append(nil(),Y) -> Y f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z) f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) -> true() lt(s(X),0()) -> false() lt(s(X),s(Y)) -> lt(X,Y) qsort(add(N,X)) -> f_3(split(N,X),N,X) qsort(nil()) -> nil() split(N,nil()) -> pair(nil(),nil()) - Signature: {append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0,add/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,f_1,f_2,f_3,lt,qsort,split} and constructors {0 ,add,false,nil,pair,s,true} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0, 0) add :: [A(0, 0) x A(3, 0)] -(3)-> A(3, 0) add :: [A(4, 0) x A(12, 4)] -(8)-> A(8, 4) add :: [A(4, 0) x A(8, 4)] -(4)-> A(4, 4) add :: [A(4, 0) x A(9, 4)] -(5)-> A(5, 4) append :: [A(3, 0) x A(3, 0)] -(0)-> A(3, 0) f_1 :: [A(9, 4) x A(0, 0) x A(4, 0) x A(0, 0)] -(6)-> A(5, 4) f_2 :: [A(3, 0) x A(0, 0) x A(4, 0) x A(0, 0) x A(9, 4) x A(9, 4)] -(9)-> A(5, 4) f_3 :: [A(4, 4) x A(0, 0) x A(0, 0)] -(0)-> A(3, 0) false :: [] -(0)-> A(3, 0) false :: [] -(0)-> A(10, 6) lt :: [A(0, 0) x A(0, 0)] -(0)-> A(4, 0) nil :: [] -(0)-> A(3, 0) nil :: [] -(0)-> A(4, 4) nil :: [] -(0)-> A(8, 4) nil :: [] -(0)-> A(5, 7) nil :: [] -(0)-> A(15, 15) pair :: [A(9, 4) x A(9, 4)] -(4)-> A(9, 4) pair :: [A(4, 4) x A(4, 4)] -(4)-> A(4, 4) pair :: [A(5, 4) x A(5, 4)] -(4)-> A(5, 4) pair :: [A(6, 4) x A(6, 4)] -(4)-> A(6, 4) qsort :: [A(4, 4)] -(0)-> A(3, 0) s :: [A(0, 0)] -(0)-> A(0, 0) split :: [A(0, 0) x A(8, 4)] -(4)-> A(5, 4) true :: [] -(0)-> A(3, 0) true :: [] -(0)-> A(10, 6) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(4, 0)] -(4)-> A_cf(4, 0) add :: [A_cf(0, 0) x A_cf(1, 0)] -(1)-> A_cf(1, 0) append :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_1 :: [A_cf(4, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(4)-> A_cf(4, 0) f_1 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_1 :: [A_cf(1, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(1)-> A_cf(1, 0) f_2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(4, 0) x A_cf(4, 0)] -(4)-> A_cf(4, 0) f_2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(1, 0) x A_cf(1, 0)] -(1)-> A_cf(1, 0) f_3 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_3 :: [A_cf(1, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) false :: [] -(0)-> A_cf(0, 0) false :: [] -(0)-> A_cf(10, 14) false :: [] -(0)-> A_cf(10, 10) lt :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 12) lt :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) lt :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 8) nil :: [] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(4, 0) nil :: [] -(0)-> A_cf(11, 11) nil :: [] -(0)-> A_cf(15, 11) nil :: [] -(0)-> A_cf(1, 0) nil :: [] -(0)-> A_cf(3, 3) nil :: [] -(0)-> A_cf(3, 2) pair :: [A_cf(4, 0) x A_cf(4, 0)] -(0)-> A_cf(4, 0) pair :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) pair :: [A_cf(1, 0) x A_cf(1, 0)] -(0)-> A_cf(1, 0) pair :: [A_cf(4, 1) x A_cf(4, 1)] -(1)-> A_cf(4, 1) pair :: [A_cf(12, 1) x A_cf(12, 1)] -(1)-> A_cf(12, 1) qsort :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) qsort :: [A_cf(1, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) split :: [A_cf(0, 0) x A_cf(4, 0)] -(0)-> A_cf(4, 0) split :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) split :: [A_cf(0, 0) x A_cf(1, 0)] -(1)-> A_cf(1, 0) true :: [] -(0)-> A_cf(0, 0) true :: [] -(0)-> A_cf(10, 14) true :: [] -(0)-> A_cf(8, 10) true :: [] -(0)-> A_cf(10, 10) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1, 0) 0_A :: [] -(0)-> A(0, 1) add_A :: [A(0, 0) x A(1, 0)] -(1)-> A(1, 0) add_A :: [A(1, 0) x A(1, 1)] -(0)-> A(0, 1) false_A :: [] -(0)-> A(1, 0) false_A :: [] -(0)-> A(0, 1) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) pair_A :: [A(1, 0) x A(1, 0)] -(0)-> A(1, 0) pair_A :: [A(0, 1) x A(0, 1)] -(1)-> A(0, 1) s_A :: [A(0, 0)] -(0)-> A(1, 0) s_A :: [A(0, 1)] -(1)-> A(0, 1) true_A :: [] -(0)-> A(1, 0) true_A :: [] -(0)-> A(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) 2. Weak: append(add(N,X),Y) -> add(N,append(X,Y)) * Step 7: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(add(N,X),Y) -> add(N,append(X,Y)) - Weak TRS: append(nil(),Y) -> Y f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z) f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) -> true() lt(s(X),0()) -> false() lt(s(X),s(Y)) -> lt(X,Y) qsort(add(N,X)) -> f_3(split(N,X),N,X) qsort(nil()) -> nil() split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) split(N,nil()) -> pair(nil(),nil()) - Signature: {append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0,add/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,f_1,f_2,f_3,lt,qsort,split} and constructors {0 ,add,false,nil,pair,s,true} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(0, 0) add :: [A(0, 0) x A(1, 0)] -(1)-> A(1, 0) add :: [A(0, 0) x A(11, 4)] -(7)-> A(7, 4) add :: [A(0, 0) x A(15, 4)] -(11)-> A(11, 4) add :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) append :: [A(1, 0) x A(0, 0)] -(1)-> A(0, 0) f_1 :: [A(11, 4) x A(0, 0) x A(0, 0) x A(0, 0)] -(11)-> A(7, 4) f_2 :: [A(3, 3) x A(0, 0) x A(0, 0) x A(0, 0) x A(15, 4) x A(11, 4)] -(11)-> A(7, 4) f_3 :: [A(7, 4) x A(0, 0) x A(0, 0)] -(8)-> A(0, 0) false :: [] -(0)-> A(3, 3) false :: [] -(0)-> A(10, 11) lt :: [A(0, 0) x A(0, 0)] -(0)-> A(4, 4) nil :: [] -(0)-> A(1, 0) nil :: [] -(0)-> A(7, 4) nil :: [] -(0)-> A(11, 4) nil :: [] -(0)-> A(7, 7) nil :: [] -(0)-> A(15, 13) pair :: [A(15, 4) x A(11, 4)] -(0)-> A(11, 4) pair :: [A(11, 4) x A(7, 4)] -(0)-> A(7, 4) pair :: [A(15, 8) x A(7, 8)] -(0)-> A(7, 8) qsort :: [A(7, 4)] -(1)-> A(0, 0) s :: [A(0, 0)] -(0)-> A(0, 0) split :: [A(0, 0) x A(11, 4)] -(0)-> A(7, 4) true :: [] -(0)-> A(3, 3) true :: [] -(0)-> A(10, 11) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) add :: [A_cf(0, 0) x A_cf(4, 0)] -(4)-> A_cf(4, 0) add :: [A_cf(0, 0) x A_cf(1, 0)] -(1)-> A_cf(1, 0) append :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) append :: [A_cf(1, 0) x A_cf(1, 0)] -(0)-> A_cf(1, 0) f_1 :: [A_cf(4, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(4)-> A_cf(4, 0) f_1 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(4, 0) x A_cf(4, 0)] -(4)-> A_cf(4, 0) f_2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) f_2 :: [A_cf(0, 1) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(4, 0) x A_cf(4, 0)] -(4)-> A_cf(4, 0) f_3 :: [A_cf(4, 0) x A_cf(0, 0) x A_cf(0, 0)] -(1)-> A_cf(1, 0) f_3 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) false :: [] -(0)-> A_cf(0, 0) false :: [] -(0)-> A_cf(10, 11) false :: [] -(0)-> A_cf(0, 1) false :: [] -(0)-> A_cf(10, 2) lt :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 8) lt :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) lt :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 2) nil :: [] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(4, 0) nil :: [] -(0)-> A_cf(1, 0) nil :: [] -(0)-> A_cf(15, 11) nil :: [] -(0)-> A_cf(3, 3) pair :: [A_cf(4, 0) x A_cf(4, 0)] -(0)-> A_cf(4, 0) pair :: [A_cf(14, 10) x A_cf(4, 10)] -(0)-> A_cf(4, 10) pair :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) pair :: [A_cf(13, 3) x A_cf(10, 3)] -(0)-> A_cf(10, 3) qsort :: [A_cf(4, 0)] -(0)-> A_cf(1, 0) qsort :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) split :: [A_cf(0, 0) x A_cf(4, 0)] -(3)-> A_cf(4, 0) split :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) split :: [A_cf(0, 0) x A_cf(4, 0)] -(0)-> A_cf(4, 0) true :: [] -(0)-> A_cf(0, 0) true :: [] -(0)-> A_cf(10, 11) true :: [] -(0)-> A_cf(0, 1) true :: [] -(0)-> A_cf(10, 2) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1, 0) 0_A :: [] -(0)-> A(0, 1) add_A :: [A(0, 0) x A(1, 0)] -(1)-> A(1, 0) add_A :: [A(0, 0) x A(1, 1)] -(0)-> A(0, 1) false_A :: [] -(0)-> A(1, 0) false_A :: [] -(0)-> A(0, 1) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) pair_A :: [A(1, 0) x A(1, 0)] -(0)-> A(1, 0) pair_A :: [A(1, 1) x A(0, 1)] -(0)-> A(0, 1) s_A :: [A(0, 0)] -(1)-> A(1, 0) s_A :: [A(0, 0)] -(0)-> A(0, 1) true_A :: [] -(0)-> A(1, 0) true_A :: [] -(0)-> A(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: append(add(N,X),Y) -> add(N,append(X,Y)) 2. Weak: * Step 8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: append(add(N,X),Y) -> add(N,append(X,Y)) append(nil(),Y) -> Y f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z) f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z) f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z)) f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z))) lt(0(),s(X)) -> true() lt(s(X),0()) -> false() lt(s(X),s(Y)) -> lt(X,Y) qsort(add(N,X)) -> f_3(split(N,X),N,X) qsort(nil()) -> nil() split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y) split(N,nil()) -> pair(nil(),nil()) - Signature: {append/2,f_1/4,f_2/6,f_3/3,lt/2,qsort/1,split/2} / {0/0,add/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,f_1,f_2,f_3,lt,qsort,split} and constructors {0 ,add,false,nil,pair,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))