WORST_CASE(?,O(n^2)) * Step 1: Desugar WORST_CASE(?,O(n^2)) + Considered Problem: type bool = True | False ;; type 'a option = None | Some of 'a ;; type 'a list = Nil | Cons of 'a * 'a list ;; type Unit = Unit ;; let ifz n th el = match n with | 0 -> th 0 | S(x) -> el x ;; let ite b th el = match b with | True()-> th | False()-> el ;; let minus n m = let rec minus' m n = match m with | 0 -> 0 | S(x) -> match n with | 0 -> m | S(y) -> minus' x y in Pair(minus' n m,m) ;; let rec plus n m = match m with | 0 -> n | S(x) -> S(plus n x) ;; type ('a,'b,'c) triple = Triple of 'a * 'b * 'c ;; let rec div_mod n m = match (minus n m) with | Pair(res,m) -> match res with | 0 -> Triple (0,n,m) | S(x) -> match (div_mod res m) with | Triple(a,rest,unusedM) -> Triple(plus S(0) a,rest,m) ;; type ('a,'b) pair = Pair of 'a * 'b (* * * * * * * * * * * * Resource Aware ML * * * * * * * * * * * * * * * * Use Cases * * * * File: * example/calculator.raml * * Author: * Jan Hoffmann (S(S(0))015) * * Description: * An evaluator for simple arithmetic expressions. * *) ;; type nat = Zero | Succ of nat ;; type expr = Nat of nat | Add of expr * expr | Sub of expr * expr ;; let rec add n1 n2 = match n1 with | Zero()-> n2 | Succ(n) -> Succ(add n n2) ;; let rec sub n1 n2 = match n2 with | Zero()-> n1 | Succ(n2') -> match n1 with | Zero()-> Zero | Succ(n1') -> sub n1' n2' ;; let rec mult n1 n2 = match n1 with | Zero()-> Zero | Succ(n) -> add n (mult n n2) ;; let rec eval expr = match expr with | Nat(n) -> n | Add(e1,e2) -> (let n1 = eval e1 in match n1 with | Zero()-> eval e2 | Succ(n) -> Succ(eval (Add (Nat(n), e2)) )) | Sub(e1,e2) -> let n2 = eval e2 in match n2 with | Zero()-> eval e1 | Succ(m) -> let n1 = eval e1 in match n1 with | Zero()-> Zero | Succ(n) -> eval (Sub (Nat(n), Nat(m))) ;; (* let rec nat_to_int n = * match n with * | Zero()-> Zero * | Succ(n) -> * let i = nat_to_int n in * plus i Succ(Zero) * * ;; * let main = * let one = Nat (Succ(Zero)) in * let two1 = Nat (Succ (Succ (Zero))) in * let two2 = Nat (Succ (Succ (Zero))) in * let two3 = Nat (Succ (Succ (Zero))) in * let two4 = Nat (Succ (Succ (Zero))) in * let n = eval (Sub ((Add (Add (two1,two2), Add (two3, one))), two4)) in * nat_to_int n * ;; *) + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^2)) + Considered Problem: λexpr : expr. (λeval : expr -> nat. eval expr) (μeval : expr -> nat. λexpr : expr. case expr of | Nat -> λn : nat. n | Add -> λe1 : expr. λe2 : expr. (λn1 : nat. case n1 of | Zero -> eval e2 | Succ -> λn : nat. Succ(eval Add(Nat(n),e2))) (eval e1) | Sub -> λe1 : expr. λe2 : expr. (λn2 : nat. case n2 of | Zero -> eval e1 | Succ -> λm : nat. (λn1 : nat. case n1 of | Zero -> Zero | Succ -> λn : nat. eval Sub(Nat(n),Nat(m))) (eval e1)) (eval e2)) : expr -> nat where Add :: expr -> expr -> expr Cons :: 'a -> 'a list -> 'a list False :: bool Nat :: nat -> expr Nil :: 'a list None :: 'a option Pair :: 'a -> 'b -> ('a,'b) pair Some :: 'a -> 'a option Sub :: expr -> expr -> expr Succ :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple True :: bool Unit :: Unit Zero :: nat + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_1(x0) x1 -> x1 x0 2: cond_eval_expr_1(Zero(), x3) -> eval() x3 3: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval() Add(Nat(x5), x3)) 4: eval_expr_3(x3) x4 -> cond_eval_expr_1(x4, x3) 5: cond_eval_expr_3(Zero(), x5) -> Zero() 6: cond_eval_expr_3(Succ(x7), x5) -> eval() Sub(Nat(x7), Nat(x5)) 7: eval_expr_9(x5) x6 -> cond_eval_expr_3(x6, x5) 8: cond_eval_expr_2(Zero(), x2) -> eval() x2 9: cond_eval_expr_2(Succ(x5), x2) -> eval_expr_9(x5) (eval() x2) 10: eval_expr_7(x2) x4 -> cond_eval_expr_2(x4, x2) 11: cond_eval_expr(Nat(x2)) -> x2 12: cond_eval_expr(Add(x2, x3)) -> eval_expr_3(x3) (eval() x2) 13: cond_eval_expr(Sub(x2, x3)) -> eval_expr_7(x2) (eval() x3) 14: eval_1() x1 -> cond_eval_expr(x1) 15: eval() x0 -> eval_1() x0 16: main(x0) -> main_1(x0) eval() where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat eval_1 :: expr -> nat main_1 :: expr -> (expr -> nat) -> nat eval_expr_3 :: expr -> nat -> nat eval_expr_7 :: expr -> nat -> nat eval_expr_9 :: nat -> nat -> nat cond_eval_expr :: expr -> nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval :: expr -> nat main :: expr -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_1(x0) x1 -> x1 x0 2: cond_eval_expr_1(Zero(), x3) -> eval() x3 3: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval() Add(Nat(x5), x3)) 4: eval_expr_3(x3) x4 -> cond_eval_expr_1(x4, x3) 5: cond_eval_expr_3(Zero(), x5) -> Zero() 6: cond_eval_expr_3(Succ(x7), x5) -> eval() Sub(Nat(x7), Nat(x5)) 7: eval_expr_9(x5) x6 -> cond_eval_expr_3(x6, x5) 8: cond_eval_expr_2(Zero(), x2) -> eval() x2 9: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval() x5, x10) 10: eval_expr_7(x2) x4 -> cond_eval_expr_2(x4, x2) 11: cond_eval_expr(Nat(x2)) -> x2 12: cond_eval_expr(Add(x5, x6)) -> cond_eval_expr_1(eval() x5, x6) 13: cond_eval_expr(Sub(x4, x7)) -> cond_eval_expr_2(eval() x7, x4) 14: eval_1() x1 -> cond_eval_expr(x1) 15: eval() x2 -> cond_eval_expr(x2) 16: main(x0) -> eval() x0 where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat eval_1 :: expr -> nat main_1 :: expr -> (expr -> nat) -> nat eval_expr_3 :: expr -> nat -> nat eval_expr_7 :: expr -> nat -> nat eval_expr_9 :: nat -> nat -> nat cond_eval_expr :: expr -> nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval :: expr -> nat main :: expr -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 5: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_1(x0) x1 -> x1 x0 2: cond_eval_expr_1(Zero(), x3) -> eval() x3 3: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval() Add(Nat(x5), x3)) 4: eval_expr_3(x6) Zero() -> eval() x6 5: eval_expr_3(x6) Succ(x10) -> Succ(eval() Add(Nat(x10), x6)) 6: cond_eval_expr_3(Zero(), x5) -> Zero() 7: cond_eval_expr_3(Succ(x7), x5) -> eval() Sub(Nat(x7), Nat(x5)) 8: eval_expr_9(x10) Zero() -> Zero() 9: eval_expr_9(x10) Succ(x14) -> eval() Sub(Nat(x14), Nat(x10)) 10: cond_eval_expr_2(Zero(), x2) -> eval() x2 11: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval() x5, x10) 12: eval_expr_7(x4) Zero() -> eval() x4 13: eval_expr_7(x10) Succ(x20) -> cond_eval_expr_3(eval() x10, x20) 14: cond_eval_expr(Nat(x2)) -> x2 15: cond_eval_expr(Add(x5, x6)) -> cond_eval_expr_1(eval() x5, x6) 16: cond_eval_expr(Sub(x4, x7)) -> cond_eval_expr_2(eval() x7, x4) 17: eval_1() Nat(x4) -> x4 18: eval_1() Add(x10, x12) -> cond_eval_expr_1(eval() x10, x12) 19: eval_1() Sub(x8, x14) -> cond_eval_expr_2(eval() x14, x8) 20: eval() Nat(x4) -> x4 21: eval() Add(x10, x12) -> cond_eval_expr_1(eval() x10, x12) 22: eval() Sub(x8, x14) -> cond_eval_expr_2(eval() x14, x8) 23: main(x0) -> eval() x0 where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat eval_1 :: expr -> nat main_1 :: expr -> (expr -> nat) -> nat eval_expr_3 :: expr -> nat -> nat eval_expr_7 :: expr -> nat -> nat eval_expr_9 :: nat -> nat -> nat cond_eval_expr :: expr -> nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval :: expr -> nat main :: expr -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 6: UncurryATRS WORST_CASE(?,O(n^2)) + Considered Problem: 2: cond_eval_expr_1(Zero(), x3) -> eval() x3 3: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval() Add(Nat(x5), x3)) 6: cond_eval_expr_3(Zero(), x5) -> Zero() 7: cond_eval_expr_3(Succ(x7), x5) -> eval() Sub(Nat(x7), Nat(x5)) 10: cond_eval_expr_2(Zero(), x2) -> eval() x2 11: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval() x5, x10) 20: eval() Nat(x4) -> x4 21: eval() Add(x10, x12) -> cond_eval_expr_1(eval() x10, x12) 22: eval() Sub(x8, x14) -> cond_eval_expr_2(eval() x14, x8) 23: main(x0) -> eval() x0 where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval :: expr -> nat main :: expr -> nat + Applied Processor: UncurryATRS + Details: none * Step 7: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: cond_eval_expr_1(Zero(), x3) -> eval#1(x3) 2: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval#1(Add(Nat(x5), x3))) 3: cond_eval_expr_3(Zero(), x5) -> Zero() 4: cond_eval_expr_3(Succ(x7), x5) -> eval#1(Sub(Nat(x7), Nat(x5))) 5: cond_eval_expr_2(Zero(), x2) -> eval#1(x2) 6: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval#1(x5), x10) 7: eval#1(Nat(x4)) -> x4 8: eval#1(Add(x10, x12)) -> cond_eval_expr_1(eval#1(x10), x12) 9: eval#1(Sub(x8, x14)) -> cond_eval_expr_2(eval#1(x14), x8) 10: main(x0) -> eval#1(x0) where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval#1 :: expr -> nat main :: expr -> nat + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 8: Compression WORST_CASE(?,O(n^2)) + Considered Problem: 1: cond_eval_expr_1(Zero(), x3) -> eval#1(x3) 2: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval#1(Add(Nat(x5), x3))) 3: cond_eval_expr_3(Zero(), x5) -> Zero() 4: cond_eval_expr_3(Succ(x7), x5) -> eval#1(Sub(Nat(x7), Nat(x5))) 5: cond_eval_expr_2(Zero(), x2) -> eval#1(x2) 6: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval#1(x5), x10) 7: eval#1(Nat(x4)) -> x4 8: eval#1(Add(x10, x12)) -> cond_eval_expr_1(eval#1(x10), x12) 9: eval#1(Sub(x8, x14)) -> cond_eval_expr_2(eval#1(x14), x8) 10: main(x0) -> eval#1(x0) where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval#1 :: expr -> nat main :: expr -> nat + Applied Processor: Compression + Details: none * Step 9: ToTctProblem WORST_CASE(?,O(n^2)) + Considered Problem: 1: cond_eval_expr_1(Zero(), x3) -> eval#1(x3) 2: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval#1(Add(Nat(x5), x3))) 3: cond_eval_expr_3(Zero(), x5) -> Zero() 4: cond_eval_expr_3(Succ(x7), x5) -> eval#1(Sub(Nat(x7), Nat(x5))) 5: cond_eval_expr_2(Zero(), x2) -> eval#1(x2) 6: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval#1(x5), x10) 7: eval#1(Nat(x4)) -> x4 8: eval#1(Add(x10, x12)) -> cond_eval_expr_1(eval#1(x10), x12) 9: eval#1(Sub(x8, x14)) -> cond_eval_expr_2(eval#1(x14), x8) 10: main(x0) -> eval#1(x0) where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval#1 :: expr -> nat main :: expr -> nat + Applied Processor: ToTctProblem + Details: none * Step 10: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1} / {Add/2,Nat/1,Sub/2,Succ/1 ,Zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) cond_eval_expr_3#(Zero(),x5) -> c_6() eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Nat(x4)) -> c_8() eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) Weak DPs and mark the set of starting terms. * Step 11: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) cond_eval_expr_3#(Zero(),x5) -> c_6() eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Nat(x4)) -> c_8() eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {6,8} by application of Pre({6,8}) = {2,3,4,7,9,10}. Here rules are labelled as follows: 1: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) 2: cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) 3: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) 4: cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) 5: cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) 6: cond_eval_expr_3#(Zero(),x5) -> c_6() 7: eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) 8: eval#1#(Nat(x4)) -> c_8() 9: eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) 10: main#(x0) -> c_10(eval#1#(x0)) * Step 12: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) - Weak DPs: cond_eval_expr_3#(Zero(),x5) -> c_6() eval#1#(Nat(x4)) -> c_8() - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 2:S:cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 eval#1#(Nat(x4)) -> c_8():10 3:S:cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))):5 -->_2 eval#1#(Nat(x4)) -> c_8():10 -->_1 cond_eval_expr_3#(Zero(),x5) -> c_6():9 4:S:cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 eval#1#(Nat(x4)) -> c_8():10 5:S:cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 6:S:eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Nat(x4)) -> c_8():10 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)):2 -->_1 cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))):1 7:S:eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) -->_2 eval#1#(Nat(x4)) -> c_8():10 -->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 -->_1 cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)):4 -->_1 cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)):3 8:S:main#(x0) -> c_10(eval#1#(x0)) -->_1 eval#1#(Nat(x4)) -> c_8():10 -->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7 -->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6 9:W:cond_eval_expr_3#(Zero(),x5) -> c_6() 10:W:eval#1#(Nat(x4)) -> c_8() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: cond_eval_expr_3#(Zero(),x5) -> c_6() 10: eval#1#(Nat(x4)) -> c_8() * Step 13: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) * Step 14: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + 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(c_1) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1,2}, uargs(c_10) = {1} Following symbols are considered usable: {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#,eval#1#,main#} TcT has computed the following interpretation: p(Add) = [1] x1 + [1] x2 + [0] p(Nat) = [1] x1 + [0] p(Sub) = [1] x1 + [1] x2 + [0] p(Succ) = [1] x1 + [0] p(Zero) = [0] p(cond_eval_expr_1) = [0] p(cond_eval_expr_2) = [0] p(cond_eval_expr_3) = [0] p(eval#1) = [0] p(main) = [0] p(cond_eval_expr_1#) = [0] p(cond_eval_expr_2#) = [0] p(cond_eval_expr_3#) = [0] p(eval#1#) = [0] p(main#) = [2] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [4] x1 + [4] x2 + [0] p(c_4) = [2] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [2] x1 + [2] x2 + [0] p(c_8) = [0] p(c_9) = [1] x1 + [1] x2 + [0] p(c_10) = [1] x1 + [1] Following rules are strictly oriented: main#(x0) = [2] > [1] = c_10(eval#1#(x0)) Following rules are (at-least) weakly oriented: cond_eval_expr_1#(Succ(x5),x3) = [0] >= [0] = c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) = [0] >= [0] = c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) = [0] >= [0] = c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) = [0] >= [0] = c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) = [0] >= [0] = c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) = [0] >= [0] = c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) = [0] >= [0] = c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) * Step 15: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak DPs: main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + 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(c_1) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1,2}, uargs(c_10) = {1} Following symbols are considered usable: {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#,eval#1#,main#} TcT has computed the following interpretation: p(Add) = [1] x1 + [1] x2 + [1] p(Nat) = [0] p(Sub) = [1] x1 + [1] x2 + [0] p(Succ) = [1] x1 + [0] p(Zero) = [2] p(cond_eval_expr_1) = [1] x1 + [0] p(cond_eval_expr_2) = [5] x1 + [0] p(cond_eval_expr_3) = [6] p(eval#1) = [0] p(main) = [2] x1 + [0] p(cond_eval_expr_1#) = [4] x2 + [4] p(cond_eval_expr_2#) = [4] x2 + [0] p(cond_eval_expr_3#) = [0] p(eval#1#) = [4] x1 + [0] p(main#) = [4] x1 + [4] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [1] p(c_3) = [4] x1 + [1] x2 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [2] x1 + [0] p(c_6) = [1] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [2] p(c_9) = [1] x1 + [1] x2 + [0] p(c_10) = [1] x1 + [4] Following rules are strictly oriented: cond_eval_expr_1#(Zero(),x3) = [4] x3 + [4] > [4] x3 + [1] = c_2(eval#1#(x3)) Following rules are (at-least) weakly oriented: cond_eval_expr_1#(Succ(x5),x3) = [4] x3 + [4] >= [4] x3 + [4] = c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_2#(Succ(x10),x5) = [4] x5 + [0] >= [4] x5 + [0] = c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) = [4] x2 + [0] >= [4] x2 + [0] = c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) = [0] >= [0] = c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) = [4] x10 + [4] x12 + [4] >= [4] x10 + [4] x12 + [4] = c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) = [4] x14 + [4] x8 + [0] >= [4] x14 + [4] x8 + [0] = c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) = [4] x0 + [4] >= [4] x0 + [4] = c_10(eval#1#(x0)) * Step 16: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak DPs: cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + 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(c_1) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1,2}, uargs(c_10) = {1} Following symbols are considered usable: {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#,eval#1#,main#} TcT has computed the following interpretation: p(Add) = [1] x1 + [1] x2 + [0] p(Nat) = [0] p(Sub) = [1] x1 + [1] x2 + [1] p(Succ) = [0] p(Zero) = [3] p(cond_eval_expr_1) = [3] x1 + [1] p(cond_eval_expr_2) = [2] p(cond_eval_expr_3) = [1] x2 + [5] p(eval#1) = [0] p(main) = [1] x1 + [0] p(cond_eval_expr_1#) = [4] x2 + [0] p(cond_eval_expr_2#) = [4] x2 + [4] p(cond_eval_expr_3#) = [4] p(eval#1#) = [4] x1 + [0] p(main#) = [4] x1 + [5] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [1] x2 + [0] p(c_4) = [1] x1 + [2] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [1] p(c_9) = [1] x1 + [1] x2 + [0] p(c_10) = [1] x1 + [1] Following rules are strictly oriented: cond_eval_expr_2#(Zero(),x2) = [4] x2 + [4] > [4] x2 + [2] = c_4(eval#1#(x2)) Following rules are (at-least) weakly oriented: cond_eval_expr_1#(Succ(x5),x3) = [4] x3 + [0] >= [4] x3 + [0] = c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) = [4] x3 + [0] >= [4] x3 + [0] = c_2(eval#1#(x3)) cond_eval_expr_2#(Succ(x10),x5) = [4] x5 + [4] >= [4] x5 + [4] = c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_3#(Succ(x7),x5) = [4] >= [4] = c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) = [4] x10 + [4] x12 + [0] >= [4] x10 + [4] x12 + [0] = c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) = [4] x14 + [4] x8 + [4] >= [4] x14 + [4] x8 + [4] = c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) = [4] x0 + [5] >= [4] x0 + [1] = c_10(eval#1#(x0)) * Step 17: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak DPs: cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Add") :: ["A"(8, 8) x "A"(8, 8)] -(0)-> "A"(0, 8) F (TrsFun "Add") :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0) F (TrsFun "Nat") :: ["A"(8, 0)] -(0)-> "A"(8, 0) F (TrsFun "Nat") :: ["A"(8, 0)] -(0)-> "A"(8, 10) F (TrsFun "Nat") :: ["A"(8, 0)] -(0)-> "A"(8, 9) F (TrsFun "Nat") :: ["A"(8, 0)] -(0)-> "A"(8, 8) F (TrsFun "Nat") :: ["A"(8, 0)] -(0)-> "A"(8, 13) F (TrsFun "Nat") :: ["A"(8, 0)] -(0)-> "A"(8, 2) F (TrsFun "Sub") :: ["A"(8, 8) x "A"(8, 8)] -(0)-> "A"(0, 8) F (TrsFun "Sub") :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0) F (TrsFun "Succ") :: ["A"(8, 0)] -(8)-> "A"(8, 0) F (TrsFun "Zero") :: [] -(0)-> "A"(8, 0) F (TrsFun "Zero") :: [] -(0)-> "A"(8, 8) F (TrsFun "cond_eval_expr_1") :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0) F (TrsFun "cond_eval_expr_2") :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0) F (TrsFun "cond_eval_expr_3") :: ["A"(8, 0) x "A"(8, 0)] -(8)-> "A"(8, 0) F (TrsFun "eval#1") :: ["A"(8, 0)] -(0)-> "A"(8, 0) F (DpFun "cond_eval_expr_1") :: ["A"(8, 0) x "A"(8, 8)] -(0)-> "A"(1, 9) F (DpFun "cond_eval_expr_2") :: ["A"(8, 0) x "A"(8, 8)] -(0)-> "A"(10, 9) F (DpFun "cond_eval_expr_3") :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(11, 13) F (DpFun "eval#1") :: ["A"(0, 8)] -(0)-> "A"(9, 8) F (DpFun "main") :: ["A"(14, 14)] -(15)-> "A"(0, 0) F (ComFun 1) :: ["A"(0, 0)] -(0)-> "A"(4, 12) F (ComFun 2) :: ["A"(0, 0)] -(0)-> "A"(5, 11) F (ComFun 3) :: ["A"(10, 0) x "A"(0, 0)] -(0)-> "A"(10, 10) F (ComFun 4) :: ["A"(0, 0)] -(0)-> "A"(13, 15) F (ComFun 5) :: ["A"(0, 0)] -(0)-> "A"(11, 13) F (ComFun 7) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(11, 10) F (ComFun 9) :: ["A"(10, 0) x "A"(0, 0)] -(0)-> "A"(11, 10) F (ComFun 10) :: ["A"(0, 0)] -(3)-> "A"(3, 14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 10)_A" :: ["A"(0, 0)] -(1)-> "A"(1, 0) "F (ComFun 10)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 3)_A" :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 3)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 4)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 4)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 7)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 7)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 9)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 9)_A" :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Add\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Add\")_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Nat\")_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Nat\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Sub\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Sub\")_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Succ\")_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Succ\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Zero\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"Zero\")_A" :: [] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) 2. Weak: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) * Step 18: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Add") :: ["A"(3, 3) x "A"(0, 3)] -(3)-> "A"(0, 3) F (TrsFun "Add") :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0) F (TrsFun "Nat") :: ["A"(3, 0)] -(0)-> "A"(3, 0) F (TrsFun "Nat") :: ["A"(3, 0)] -(0)-> "A"(3, 15) F (TrsFun "Nat") :: ["A"(3, 0)] -(0)-> "A"(3, 6) F (TrsFun "Nat") :: ["A"(3, 0)] -(0)-> "A"(3, 14) F (TrsFun "Nat") :: ["A"(3, 0)] -(0)-> "A"(3, 13) F (TrsFun "Nat") :: ["A"(3, 0)] -(0)-> "A"(3, 3) F (TrsFun "Nat") :: ["A"(3, 0)] -(0)-> "A"(3, 8) F (TrsFun "Sub") :: ["A"(3, 3) x "A"(3, 3)] -(0)-> "A"(0, 3) F (TrsFun "Sub") :: ["A"(3, 0) x "A"(3, 0)] -(3)-> "A"(3, 0) F (TrsFun "Succ") :: ["A"(3, 0)] -(3)-> "A"(3, 0) F (TrsFun "Succ") :: ["A"(3, 0)] -(3)-> "A"(3, 7) F (TrsFun "Zero") :: [] -(0)-> "A"(3, 0) F (TrsFun "Zero") :: [] -(0)-> "A"(11, 8) F (TrsFun "cond_eval_expr_1") :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0) F (TrsFun "cond_eval_expr_2") :: ["A"(3, 0) x "A"(3, 0)] -(3)-> "A"(3, 0) F (TrsFun "cond_eval_expr_3") :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0) F (TrsFun "eval#1") :: ["A"(3, 0)] -(0)-> "A"(3, 0) F (DpFun "cond_eval_expr_1") :: ["A"(3, 0) x "A"(0, 3)] -(0)-> "A"(5, 12) F (DpFun "cond_eval_expr_2") :: ["A"(3, 0) x "A"(3, 3)] -(0)-> "A"(1, 8) F (DpFun "cond_eval_expr_3") :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(0, 13) F (DpFun "eval#1") :: ["A"(0, 3)] -(0)-> "A"(12, 12) F (DpFun "main") :: ["A"(14, 13)] -(15)-> "A"(0, 4) F (ComFun 1) :: ["A"(0, 0)] -(0)-> "A"(6, 15) F (ComFun 2) :: ["A"(12, 0)] -(0)-> "A"(9, 12) F (ComFun 3) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(4, 12) F (ComFun 4) :: ["A"(0, 0)] -(0)-> "A"(4, 10) F (ComFun 5) :: ["A"(0, 0)] -(0)-> "A"(0, 13) F (ComFun 7) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(15, 13) F (ComFun 9) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(12, 12) F (ComFun 10) :: ["A"(1, 0)] -(1)-> "A"(1, 11) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 10)_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "F (ComFun 10)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 2)_A" :: ["A"(1, 0)] -(0)-> "A"(0, 1) "F (ComFun 3)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 3)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 4)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 4)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 7)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 7)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 9)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 9)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Add\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Add\")_A" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1) "F (TrsFun \"Nat\")_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Nat\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Sub\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Sub\")_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Succ\")_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Succ\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Zero\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"Zero\")_A" :: [] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) 2. Weak: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) * Step 19: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) - Weak DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Add") :: ["A"(14, 0) x "A"(14, 0)] -(0)-> "A"(14, 0) F (TrsFun "Add") :: ["A"(14, 14) x "A"(0, 14)] -(0)-> "A"(0, 14) F (TrsFun "Nat") :: ["A"(14, 0)] -(0)-> "A"(14, 0) F (TrsFun "Nat") :: ["A"(14, 0)] -(0)-> "A"(14, 8) F (TrsFun "Nat") :: ["A"(14, 0)] -(0)-> "A"(14, 4) F (TrsFun "Nat") :: ["A"(14, 0)] -(0)-> "A"(14, 2) F (TrsFun "Nat") :: ["A"(14, 0)] -(0)-> "A"(14, 14) F (TrsFun "Sub") :: ["A"(14, 14) x "A"(14, 14)] -(14)-> "A"(0, 14) F (TrsFun "Sub") :: ["A"(14, 0) x "A"(14, 0)] -(14)-> "A"(14, 0) F (TrsFun "Succ") :: ["A"(14, 0)] -(14)-> "A"(14, 0) F (TrsFun "Succ") :: ["A"(14, 0)] -(14)-> "A"(14, 14) F (TrsFun "Zero") :: [] -(0)-> "A"(14, 0) F (TrsFun "Zero") :: [] -(0)-> "A"(14, 8) F (TrsFun "cond_eval_expr_1") :: ["A"(14, 0) x "A"(14, 0)] -(0)-> "A"(14, 0) F (TrsFun "cond_eval_expr_2") :: ["A"(14, 0) x "A"(14, 0)] -(10)-> "A"(14, 0) F (TrsFun "cond_eval_expr_3") :: ["A"(14, 0) x "A"(14, 0)] -(9)-> "A"(14, 0) F (TrsFun "eval#1") :: ["A"(14, 0)] -(0)-> "A"(14, 0) F (DpFun "cond_eval_expr_1") :: ["A"(14, 0) x "A"(0, 14)] -(0)-> "A"(0, 0) F (DpFun "cond_eval_expr_2") :: ["A"(14, 0) x "A"(14, 14)] -(13)-> "A"(0, 0) F (DpFun "cond_eval_expr_3") :: ["A"(14, 0) x "A"(14, 0)] -(7)-> "A"(0, 12) F (DpFun "eval#1") :: ["A"(0, 14)] -(0)-> "A"(4, 12) F (DpFun "main") :: ["A"(14, 14)] -(14)-> "A"(0, 0) F (ComFun 1) :: ["A"(0, 0)] -(0)-> "A"(4, 12) F (ComFun 2) :: ["A"(1, 0)] -(0)-> "A"(1, 0) F (ComFun 3) :: ["A"(0, 0) x "A"(0, 10)] -(4)-> "A"(4, 10) F (ComFun 4) :: ["A"(0, 0)] -(0)-> "A"(0, 2) F (ComFun 5) :: ["A"(0, 0)] -(2)-> "A"(2, 12) F (ComFun 7) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(11, 13) F (ComFun 9) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(6, 12) F (ComFun 10) :: ["A"(4, 0)] -(0)-> "A"(2, 2) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 10)_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "F (ComFun 10)_A" :: ["A"(1, 0)] -(0)-> "A"(0, 1) "F (ComFun 2)_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 3)_A" :: ["A"(0, 0) x "A"(0, 0)] -(1)-> "A"(1, 0) "F (ComFun 3)_A" :: ["A"(0, 0) x "A"(0, 1)] -(0)-> "A"(0, 1) "F (ComFun 4)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 4)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 5)_A" :: ["A"(0, 0)] -(1)-> "A"(1, 0) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 7)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 7)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 9)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 9)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Add\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Add\")_A" :: ["A"(1, 1) x "A"(0, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Nat\")_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Nat\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Sub\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Sub\")_A" :: ["A"(1, 1) x "A"(1, 1)] -(1)-> "A"(0, 1) "F (TrsFun \"Succ\")_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Succ\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Zero\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"Zero\")_A" :: [] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) 2. Weak: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) * Step 20: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) - Weak DPs: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))) cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)) cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)) cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))) eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)) eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)) main#(x0) -> c_10(eval#1#(x0)) - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2 ,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1 ,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Add") :: ["A"(2, 0) x "A"(2, 0)] -(2)-> "A"(2, 0) F (TrsFun "Add") :: ["A"(2, 2) x "A"(0, 2)] -(0)-> "A"(0, 2) F (TrsFun "Nat") :: ["A"(2, 0)] -(0)-> "A"(2, 0) F (TrsFun "Nat") :: ["A"(2, 0)] -(0)-> "A"(2, 1) F (TrsFun "Nat") :: ["A"(2, 0)] -(0)-> "A"(2, 7) F (TrsFun "Nat") :: ["A"(2, 0)] -(0)-> "A"(2, 6) F (TrsFun "Nat") :: ["A"(2, 0)] -(0)-> "A"(2, 9) F (TrsFun "Sub") :: ["A"(2, 0) x "A"(2, 0)] -(2)-> "A"(2, 0) F (TrsFun "Sub") :: ["A"(2, 2) x "A"(2, 2)] -(0)-> "A"(0, 2) F (TrsFun "Succ") :: ["A"(2, 0)] -(2)-> "A"(2, 0) F (TrsFun "Succ") :: ["A"(2, 0)] -(2)-> "A"(2, 3) F (TrsFun "Zero") :: [] -(0)-> "A"(2, 0) F (TrsFun "Zero") :: [] -(0)-> "A"(10, 0) F (TrsFun "cond_eval_expr_1") :: ["A"(2, 0) x "A"(2, 0)] -(2)-> "A"(2, 0) F (TrsFun "cond_eval_expr_2") :: ["A"(2, 0) x "A"(2, 0)] -(2)-> "A"(2, 0) F (TrsFun "cond_eval_expr_3") :: ["A"(2, 0) x "A"(2, 0)] -(3)-> "A"(2, 0) F (TrsFun "eval#1") :: ["A"(2, 0)] -(0)-> "A"(2, 0) F (DpFun "cond_eval_expr_1") :: ["A"(2, 0) x "A"(0, 2)] -(0)-> "A"(0, 0) F (DpFun "cond_eval_expr_2") :: ["A"(2, 0) x "A"(2, 2)] -(0)-> "A"(0, 1) F (DpFun "cond_eval_expr_3") :: ["A"(2, 0) x "A"(2, 0)] -(0)-> "A"(4, 13) F (DpFun "eval#1") :: ["A"(0, 2)] -(0)-> "A"(0, 0) F (DpFun "main") :: ["A"(14, 12)] -(15)-> "A"(0, 0) F (ComFun 1) :: ["A"(0, 0)] -(0)-> "A"(4, 4) F (ComFun 2) :: ["A"(0, 0)] -(0)-> "A"(4, 12) F (ComFun 3) :: ["A"(0, 13) x "A"(0, 0)] -(0)-> "A"(4, 13) F (ComFun 4) :: ["A"(0, 0)] -(0)-> "A"(4, 4) F (ComFun 5) :: ["A"(0, 0)] -(0)-> "A"(4, 13) F (ComFun 7) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) F (ComFun 9) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(13, 12) F (ComFun 10) :: ["A"(0, 0)] -(3)-> "A"(3, 14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 10)_A" :: ["A"(0, 0)] -(1)-> "A"(1, 0) "F (ComFun 10)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 3)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 3)_A" :: ["A"(0, 1) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 4)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 4)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 7)_A" :: ["A"(0, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "F (ComFun 7)_A" :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 9)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 9)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Add\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Add\")_A" :: ["A"(1, 1) x "A"(0, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Nat\")_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Nat\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Sub\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Sub\")_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Succ\")_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Succ\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"Zero\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"Zero\")_A" :: [] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)) 2. Weak: WORST_CASE(?,O(n^2))