YES(O(1),O(n^1)) 555.20/148.07 YES(O(1),O(n^1)) 555.20/148.07 555.20/148.07 We are left with following problem, upon which TcT provides the 555.20/148.07 certificate YES(O(1),O(n^1)). 555.20/148.07 555.20/148.07 Strict Trs: 555.20/148.07 { second(Op(x, y)) -> y 555.20/148.07 , isOp(Op(x, y)) -> True() 555.20/148.07 , isOp(Val(n)) -> False() 555.20/148.07 , assrewrite(exp) -> rewrite(exp) 555.20/148.07 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.07 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.07 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.07 rw(Val(n), first(second(Val(n)))) 555.20/148.07 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.07 , rewrite(Val(n)) -> Val(n) 555.20/148.07 , first(Op(x, y)) -> x 555.20/148.07 , first(Val(n)) -> Val(n) 555.20/148.07 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.07 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.07 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.07 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.07 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.07 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.07 Weak Trs: 555.20/148.07 { rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.07 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.07 c, 555.20/148.07 a1, 555.20/148.07 rewrite(x)) 555.20/148.07 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.07 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) } 555.20/148.07 Obligation: 555.20/148.07 innermost runtime complexity 555.20/148.07 Answer: 555.20/148.07 YES(O(1),O(n^1)) 555.20/148.07 555.20/148.07 We add the following dependency tuples: 555.20/148.07 555.20/148.07 Strict DPs: 555.20/148.07 { second^#(Op(x, y)) -> c_1() 555.20/148.07 , isOp^#(Op(x, y)) -> c_2() 555.20/148.07 , isOp^#(Val(n)) -> c_3() 555.20/148.07 , assrewrite^#(exp) -> c_4(rewrite^#(exp)) 555.20/148.07 , rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_5(rw^#(x', x)) 555.20/148.07 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_6(rw^#(x, Val(n))) 555.20/148.07 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.07 c_7(rw^#(Val(n), first(second(Val(n)))), 555.20/148.07 first^#(second(Val(n))), 555.20/148.07 second^#(Val(n))) 555.20/148.07 , rewrite^#(Op(Val(n), y)) -> c_8() 555.20/148.07 , rewrite^#(Val(n)) -> c_9() 555.20/148.07 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.07 c_12(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.07 rewrite^#(x)) 555.20/148.07 , rw^#(Op(Op(x, y), Val(n)), c) -> 555.20/148.07 c_13(rw[Ite][True][Let]^#(Op(Op(x, y), Val(n)), c, Val(n))) 555.20/148.07 , rw^#(Op(Val(n), y), c) -> c_14(rewrite^#(c)) 555.20/148.07 , rw^#(Val(n), c) -> c_15(rewrite^#(c)) 555.20/148.07 , first^#(Op(x, y)) -> c_10() 555.20/148.07 , first^#(Val(n)) -> c_11() } 555.20/148.07 Weak DPs: 555.20/148.07 { rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.07 c_16(rewrite^#(x)) 555.20/148.07 , rw[Ite][True][Let]^#(Op(x', Op(x, Val(n))), c, a1) -> c_17() } 555.20/148.07 555.20/148.07 and mark the set of starting terms. 555.20/148.07 555.20/148.07 We are left with following problem, upon which TcT provides the 555.20/148.07 certificate YES(O(1),O(n^1)). 555.20/148.07 555.20/148.07 Strict DPs: 555.20/148.07 { second^#(Op(x, y)) -> c_1() 555.20/148.07 , isOp^#(Op(x, y)) -> c_2() 555.20/148.07 , isOp^#(Val(n)) -> c_3() 555.20/148.07 , assrewrite^#(exp) -> c_4(rewrite^#(exp)) 555.20/148.07 , rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_5(rw^#(x', x)) 555.20/148.07 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_6(rw^#(x, Val(n))) 555.20/148.07 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.07 c_7(rw^#(Val(n), first(second(Val(n)))), 555.20/148.07 first^#(second(Val(n))), 555.20/148.07 second^#(Val(n))) 555.20/148.07 , rewrite^#(Op(Val(n), y)) -> c_8() 555.20/148.07 , rewrite^#(Val(n)) -> c_9() 555.20/148.07 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.07 c_12(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.07 rewrite^#(x)) 555.20/148.07 , rw^#(Op(Op(x, y), Val(n)), c) -> 555.20/148.07 c_13(rw[Ite][True][Let]^#(Op(Op(x, y), Val(n)), c, Val(n))) 555.20/148.07 , rw^#(Op(Val(n), y), c) -> c_14(rewrite^#(c)) 555.20/148.07 , rw^#(Val(n), c) -> c_15(rewrite^#(c)) 555.20/148.07 , first^#(Op(x, y)) -> c_10() 555.20/148.07 , first^#(Val(n)) -> c_11() } 555.20/148.07 Weak DPs: 555.20/148.07 { rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.07 c_16(rewrite^#(x)) 555.20/148.07 , rw[Ite][True][Let]^#(Op(x', Op(x, Val(n))), c, a1) -> c_17() } 555.20/148.07 Weak Trs: 555.20/148.07 { second(Op(x, y)) -> y 555.20/148.07 , isOp(Op(x, y)) -> True() 555.20/148.07 , isOp(Val(n)) -> False() 555.20/148.07 , assrewrite(exp) -> rewrite(exp) 555.20/148.07 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.07 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.07 c, 555.20/148.07 a1, 555.20/148.07 rewrite(x)) 555.20/148.07 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.07 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.07 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.07 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.07 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.07 rw(Val(n), first(second(Val(n)))) 555.20/148.07 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.07 , rewrite(Val(n)) -> Val(n) 555.20/148.07 , first(Op(x, y)) -> x 555.20/148.07 , first(Val(n)) -> Val(n) 555.20/148.07 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.07 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.07 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.07 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.07 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.07 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.07 Obligation: 555.20/148.07 innermost runtime complexity 555.20/148.07 Answer: 555.20/148.07 YES(O(1),O(n^1)) 555.20/148.07 555.20/148.07 We estimate the number of application of {1,2,3,11,14,15} by 555.20/148.07 applications of Pre({1,2,3,11,14,15}) = {5,6}. Here rules are 555.20/148.07 labeled as follows: 555.20/148.07 555.20/148.07 DPs: 555.20/148.07 { 1: second^#(Op(x, y)) -> c_1() 555.20/148.07 , 2: isOp^#(Op(x, y)) -> c_2() 555.20/148.07 , 3: isOp^#(Val(n)) -> c_3() 555.20/148.07 , 4: assrewrite^#(exp) -> c_4(rewrite^#(exp)) 555.20/148.07 , 5: rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> 555.20/148.07 c_5(rw^#(x', x)) 555.20/148.07 , 6: rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> 555.20/148.07 c_6(rw^#(x, Val(n))) 555.20/148.07 , 7: rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.07 c_7(rw^#(Val(n), first(second(Val(n)))), 555.20/148.07 first^#(second(Val(n))), 555.20/148.07 second^#(Val(n))) 555.20/148.07 , 8: rewrite^#(Op(Val(n), y)) -> c_8() 555.20/148.07 , 9: rewrite^#(Val(n)) -> c_9() 555.20/148.07 , 10: rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.07 c_12(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.07 rewrite^#(x)) 555.20/148.07 , 11: rw^#(Op(Op(x, y), Val(n)), c) -> 555.20/148.07 c_13(rw[Ite][True][Let]^#(Op(Op(x, y), Val(n)), c, Val(n))) 555.20/148.07 , 12: rw^#(Op(Val(n), y), c) -> c_14(rewrite^#(c)) 555.20/148.07 , 13: rw^#(Val(n), c) -> c_15(rewrite^#(c)) 555.20/148.07 , 14: first^#(Op(x, y)) -> c_10() 555.20/148.07 , 15: first^#(Val(n)) -> c_11() 555.20/148.07 , 16: rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.07 c_16(rewrite^#(x)) 555.20/148.07 , 17: rw[Ite][True][Let]^#(Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.07 c_17() } 555.20/148.07 555.20/148.07 We are left with following problem, upon which TcT provides the 555.20/148.07 certificate YES(O(1),O(n^1)). 555.20/148.07 555.20/148.07 Strict DPs: 555.20/148.07 { assrewrite^#(exp) -> c_4(rewrite^#(exp)) 555.20/148.07 , rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_5(rw^#(x', x)) 555.20/148.07 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_6(rw^#(x, Val(n))) 555.20/148.07 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.07 c_7(rw^#(Val(n), first(second(Val(n)))), 555.20/148.07 first^#(second(Val(n))), 555.20/148.07 second^#(Val(n))) 555.20/148.07 , rewrite^#(Op(Val(n), y)) -> c_8() 555.20/148.07 , rewrite^#(Val(n)) -> c_9() 555.20/148.07 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.07 c_12(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.07 rewrite^#(x)) 555.20/148.07 , rw^#(Op(Val(n), y), c) -> c_14(rewrite^#(c)) 555.20/148.07 , rw^#(Val(n), c) -> c_15(rewrite^#(c)) } 555.20/148.07 Weak DPs: 555.20/148.07 { second^#(Op(x, y)) -> c_1() 555.20/148.07 , isOp^#(Op(x, y)) -> c_2() 555.20/148.07 , isOp^#(Val(n)) -> c_3() 555.20/148.07 , rw^#(Op(Op(x, y), Val(n)), c) -> 555.20/148.07 c_13(rw[Ite][True][Let]^#(Op(Op(x, y), Val(n)), c, Val(n))) 555.20/148.07 , first^#(Op(x, y)) -> c_10() 555.20/148.07 , first^#(Val(n)) -> c_11() 555.20/148.07 , rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.07 c_16(rewrite^#(x)) 555.20/148.07 , rw[Ite][True][Let]^#(Op(x', Op(x, Val(n))), c, a1) -> c_17() } 555.20/148.07 Weak Trs: 555.20/148.07 { second(Op(x, y)) -> y 555.20/148.07 , isOp(Op(x, y)) -> True() 555.20/148.07 , isOp(Val(n)) -> False() 555.20/148.07 , assrewrite(exp) -> rewrite(exp) 555.20/148.07 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.07 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.07 c, 555.20/148.07 a1, 555.20/148.07 rewrite(x)) 555.20/148.07 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.07 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.07 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.07 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.07 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.07 rw(Val(n), first(second(Val(n)))) 555.20/148.07 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.07 , rewrite(Val(n)) -> Val(n) 555.20/148.07 , first(Op(x, y)) -> x 555.20/148.07 , first(Val(n)) -> Val(n) 555.20/148.07 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.07 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.07 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.08 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.08 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.08 Obligation: 555.20/148.08 innermost runtime complexity 555.20/148.08 Answer: 555.20/148.08 YES(O(1),O(n^1)) 555.20/148.08 555.20/148.08 The following weak DPs constitute a sub-graph of the DG that is 555.20/148.08 closed under successors. The DPs are removed. 555.20/148.08 555.20/148.08 { second^#(Op(x, y)) -> c_1() 555.20/148.08 , isOp^#(Op(x, y)) -> c_2() 555.20/148.08 , isOp^#(Val(n)) -> c_3() 555.20/148.08 , rw^#(Op(Op(x, y), Val(n)), c) -> 555.20/148.08 c_13(rw[Ite][True][Let]^#(Op(Op(x, y), Val(n)), c, Val(n))) 555.20/148.08 , first^#(Op(x, y)) -> c_10() 555.20/148.08 , first^#(Val(n)) -> c_11() 555.20/148.08 , rw[Ite][True][Let]^#(Op(x', Op(x, Val(n))), c, a1) -> c_17() } 555.20/148.08 555.20/148.08 We are left with following problem, upon which TcT provides the 555.20/148.08 certificate YES(O(1),O(n^1)). 555.20/148.08 555.20/148.08 Strict DPs: 555.20/148.08 { assrewrite^#(exp) -> c_4(rewrite^#(exp)) 555.20/148.08 , rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_5(rw^#(x', x)) 555.20/148.08 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_6(rw^#(x, Val(n))) 555.20/148.08 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_7(rw^#(Val(n), first(second(Val(n)))), 555.20/148.08 first^#(second(Val(n))), 555.20/148.08 second^#(Val(n))) 555.20/148.08 , rewrite^#(Op(Val(n), y)) -> c_8() 555.20/148.08 , rewrite^#(Val(n)) -> c_9() 555.20/148.08 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 c_12(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.08 rewrite^#(x)) 555.20/148.08 , rw^#(Op(Val(n), y), c) -> c_14(rewrite^#(c)) 555.20/148.08 , rw^#(Val(n), c) -> c_15(rewrite^#(c)) } 555.20/148.08 Weak DPs: 555.20/148.08 { rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 c_16(rewrite^#(x)) } 555.20/148.08 Weak Trs: 555.20/148.08 { second(Op(x, y)) -> y 555.20/148.08 , isOp(Op(x, y)) -> True() 555.20/148.08 , isOp(Val(n)) -> False() 555.20/148.08 , assrewrite(exp) -> rewrite(exp) 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.08 c, 555.20/148.08 a1, 555.20/148.08 rewrite(x)) 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.08 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.08 rw(Val(n), first(second(Val(n)))) 555.20/148.08 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.08 , rewrite(Val(n)) -> Val(n) 555.20/148.08 , first(Op(x, y)) -> x 555.20/148.08 , first(Val(n)) -> Val(n) 555.20/148.08 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.08 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.08 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.08 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.08 Obligation: 555.20/148.08 innermost runtime complexity 555.20/148.08 Answer: 555.20/148.08 YES(O(1),O(n^1)) 555.20/148.08 555.20/148.08 Due to missing edges in the dependency-graph, the right-hand sides 555.20/148.08 of following rules could be simplified: 555.20/148.08 555.20/148.08 { rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_7(rw^#(Val(n), first(second(Val(n)))), 555.20/148.08 first^#(second(Val(n))), 555.20/148.08 second^#(Val(n))) } 555.20/148.08 555.20/148.08 We are left with following problem, upon which TcT provides the 555.20/148.08 certificate YES(O(1),O(n^1)). 555.20/148.08 555.20/148.08 Strict DPs: 555.20/148.08 { assrewrite^#(exp) -> c_1(rewrite^#(exp)) 555.20/148.08 , rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_2(rw^#(x', x)) 555.20/148.08 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_3(rw^#(x, Val(n))) 555.20/148.08 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.08 , rewrite^#(Op(Val(n), y)) -> c_5() 555.20/148.08 , rewrite^#(Val(n)) -> c_6() 555.20/148.08 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.08 rewrite^#(x)) 555.20/148.08 , rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.20/148.08 , rw^#(Val(n), c) -> c_9(rewrite^#(c)) } 555.20/148.08 Weak DPs: 555.20/148.08 { rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 c_10(rewrite^#(x)) } 555.20/148.08 Weak Trs: 555.20/148.08 { second(Op(x, y)) -> y 555.20/148.08 , isOp(Op(x, y)) -> True() 555.20/148.08 , isOp(Val(n)) -> False() 555.20/148.08 , assrewrite(exp) -> rewrite(exp) 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.08 c, 555.20/148.08 a1, 555.20/148.08 rewrite(x)) 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.08 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.08 rw(Val(n), first(second(Val(n)))) 555.20/148.08 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.08 , rewrite(Val(n)) -> Val(n) 555.20/148.08 , first(Op(x, y)) -> x 555.20/148.08 , first(Val(n)) -> Val(n) 555.20/148.08 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.08 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.08 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.08 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.08 Obligation: 555.20/148.08 innermost runtime complexity 555.20/148.08 Answer: 555.20/148.08 YES(O(1),O(n^1)) 555.20/148.08 555.20/148.08 We replace rewrite rules by usable rules: 555.20/148.08 555.20/148.08 Weak Usable Rules: 555.20/148.08 { second(Op(x, y)) -> y 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.08 c, 555.20/148.08 a1, 555.20/148.08 rewrite(x)) 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.08 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.08 rw(Val(n), first(second(Val(n)))) 555.20/148.08 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.08 , rewrite(Val(n)) -> Val(n) 555.20/148.08 , first(Op(x, y)) -> x 555.20/148.08 , first(Val(n)) -> Val(n) 555.20/148.08 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.08 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.08 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.08 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.08 555.20/148.08 We are left with following problem, upon which TcT provides the 555.20/148.08 certificate YES(O(1),O(n^1)). 555.20/148.08 555.20/148.08 Strict DPs: 555.20/148.08 { assrewrite^#(exp) -> c_1(rewrite^#(exp)) 555.20/148.08 , rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_2(rw^#(x', x)) 555.20/148.08 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_3(rw^#(x, Val(n))) 555.20/148.08 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.08 , rewrite^#(Op(Val(n), y)) -> c_5() 555.20/148.08 , rewrite^#(Val(n)) -> c_6() 555.20/148.08 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.08 rewrite^#(x)) 555.20/148.08 , rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.20/148.08 , rw^#(Val(n), c) -> c_9(rewrite^#(c)) } 555.20/148.08 Weak DPs: 555.20/148.08 { rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 c_10(rewrite^#(x)) } 555.20/148.08 Weak Trs: 555.20/148.08 { second(Op(x, y)) -> y 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.08 c, 555.20/148.08 a1, 555.20/148.08 rewrite(x)) 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.08 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.08 rw(Val(n), first(second(Val(n)))) 555.20/148.08 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.08 , rewrite(Val(n)) -> Val(n) 555.20/148.08 , first(Op(x, y)) -> x 555.20/148.08 , first(Val(n)) -> Val(n) 555.20/148.08 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.08 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.08 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.08 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.08 Obligation: 555.20/148.08 innermost runtime complexity 555.20/148.08 Answer: 555.20/148.08 YES(O(1),O(n^1)) 555.20/148.08 555.20/148.08 Consider the dependency graph 555.20/148.08 555.20/148.08 1: assrewrite^#(exp) -> c_1(rewrite^#(exp)) 555.20/148.08 -->_1 rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) :4 555.20/148.08 -->_1 rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> 555.20/148.08 c_3(rw^#(x, Val(n))) :3 555.20/148.08 -->_1 rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> 555.20/148.08 c_2(rw^#(x', x)) :2 555.20/148.08 -->_1 rewrite^#(Val(n)) -> c_6() :6 555.20/148.08 -->_1 rewrite^#(Op(Val(n), y)) -> c_5() :5 555.20/148.08 555.20/148.08 2: rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_2(rw^#(x', x)) 555.20/148.08 -->_1 rw^#(Val(n), c) -> c_9(rewrite^#(c)) :9 555.20/148.08 -->_1 rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) :8 555.20/148.08 -->_1 rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.08 rewrite^#(x)) :7 555.20/148.08 555.20/148.08 3: rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_3(rw^#(x, Val(n))) 555.20/148.08 -->_1 rw^#(Val(n), c) -> c_9(rewrite^#(c)) :9 555.20/148.08 -->_1 rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) :8 555.20/148.08 -->_1 rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.08 rewrite^#(x)) :7 555.20/148.08 555.20/148.08 4: rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.08 -->_1 rw^#(Val(n), c) -> c_9(rewrite^#(c)) :9 555.20/148.08 555.20/148.08 5: rewrite^#(Op(Val(n), y)) -> c_5() 555.20/148.08 555.20/148.08 6: rewrite^#(Val(n)) -> c_6() 555.20/148.08 555.20/148.08 7: rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.08 rewrite^#(x)) 555.20/148.08 -->_1 rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 c_10(rewrite^#(x)) :10 555.20/148.08 -->_2 rewrite^#(Val(n)) -> c_6() :6 555.20/148.08 -->_2 rewrite^#(Op(Val(n), y)) -> c_5() :5 555.20/148.08 -->_2 rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) :4 555.20/148.08 -->_2 rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> 555.20/148.08 c_3(rw^#(x, Val(n))) :3 555.20/148.08 -->_2 rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> 555.20/148.08 c_2(rw^#(x', x)) :2 555.20/148.08 555.20/148.08 8: rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.20/148.08 -->_1 rewrite^#(Val(n)) -> c_6() :6 555.20/148.08 -->_1 rewrite^#(Op(Val(n), y)) -> c_5() :5 555.20/148.08 -->_1 rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) :4 555.20/148.08 -->_1 rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> 555.20/148.08 c_3(rw^#(x, Val(n))) :3 555.20/148.08 -->_1 rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> 555.20/148.08 c_2(rw^#(x', x)) :2 555.20/148.08 555.20/148.08 9: rw^#(Val(n), c) -> c_9(rewrite^#(c)) 555.20/148.08 -->_1 rewrite^#(Val(n)) -> c_6() :6 555.20/148.08 -->_1 rewrite^#(Op(Val(n), y)) -> c_5() :5 555.20/148.08 -->_1 rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) :4 555.20/148.08 -->_1 rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> 555.20/148.08 c_3(rw^#(x, Val(n))) :3 555.20/148.08 -->_1 rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> 555.20/148.08 c_2(rw^#(x', x)) :2 555.20/148.08 555.20/148.08 10: rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 c_10(rewrite^#(x)) 555.20/148.08 -->_1 rewrite^#(Val(n)) -> c_6() :6 555.20/148.08 -->_1 rewrite^#(Op(Val(n), y)) -> c_5() :5 555.20/148.08 -->_1 rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) :4 555.20/148.08 -->_1 rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> 555.20/148.08 c_3(rw^#(x, Val(n))) :3 555.20/148.08 -->_1 rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> 555.20/148.08 c_2(rw^#(x', x)) :2 555.20/148.08 555.20/148.08 555.20/148.08 Following roots of the dependency graph are removed, as the 555.20/148.08 considered set of starting terms is closed under reduction with 555.20/148.08 respect to these rules (modulo compound contexts). 555.20/148.08 555.20/148.08 { assrewrite^#(exp) -> c_1(rewrite^#(exp)) } 555.20/148.08 555.20/148.08 555.20/148.08 We are left with following problem, upon which TcT provides the 555.20/148.08 certificate YES(O(1),O(n^1)). 555.20/148.08 555.20/148.08 Strict DPs: 555.20/148.08 { rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_2(rw^#(x', x)) 555.20/148.08 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_3(rw^#(x, Val(n))) 555.20/148.08 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.08 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.08 , rewrite^#(Op(Val(n), y)) -> c_5() 555.20/148.08 , rewrite^#(Val(n)) -> c_6() 555.20/148.08 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.08 rewrite^#(x)) 555.20/148.08 , rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.20/148.08 , rw^#(Val(n), c) -> c_9(rewrite^#(c)) } 555.20/148.08 Weak DPs: 555.20/148.08 { rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 c_10(rewrite^#(x)) } 555.20/148.08 Weak Trs: 555.20/148.08 { second(Op(x, y)) -> y 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.08 c, 555.20/148.08 a1, 555.20/148.08 rewrite(x)) 555.20/148.08 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.08 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.08 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.08 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.08 rw(Val(n), first(second(Val(n)))) 555.20/148.08 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.08 , rewrite(Val(n)) -> Val(n) 555.20/148.08 , first(Op(x, y)) -> x 555.20/148.08 , first(Val(n)) -> Val(n) 555.20/148.08 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.08 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.08 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.08 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.08 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.08 Obligation: 555.20/148.08 innermost runtime complexity 555.20/148.08 Answer: 555.20/148.08 YES(O(1),O(n^1)) 555.20/148.08 555.20/148.08 We use the processor 'matrix interpretation of dimension 2' to 555.20/148.08 orient following rules strictly. 555.20/148.08 555.20/148.08 DPs: 555.20/148.08 { 4: rewrite^#(Op(Val(n), y)) -> c_5() 555.20/148.08 , 5: rewrite^#(Val(n)) -> c_6() 555.20/148.08 , 7: rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) } 555.20/148.08 Trs: { first(Val(n)) -> Val(n) } 555.20/148.08 555.20/148.08 Sub-proof: 555.20/148.08 ---------- 555.20/148.08 The following argument positions are usable: 555.20/148.08 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 555.20/148.08 Uargs(c_7) = {1, 2}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, 555.20/148.08 Uargs(c_10) = {1} 555.20/148.08 555.20/148.08 TcT has computed the following constructor-based matrix 555.20/148.08 interpretation satisfying not(EDA) and not(IDA(1)). 555.20/148.08 555.20/148.08 [second](x1) = [0 1] x1 + [0] 555.20/148.08 [1 0] [0] 555.20/148.08 555.20/148.08 [Op](x1, x2) = [0 0] x1 + [0 555.20/148.08 1] x2 + [0] 555.20/148.08 [1 1] [1 555.20/148.08 0] [0] 555.20/148.08 555.20/148.08 [rw[Ite][True][Let]](x1, x2, x3) = [7 0] x2 + [0] 555.20/148.08 [7 7] [0] 555.20/148.08 555.20/148.08 [rewrite](x1) = [0] 555.20/148.08 [0] 555.20/148.08 555.20/148.08 [first](x1) = [0 4] x1 + [0] 555.20/148.08 [0 2] [0] 555.20/148.08 555.20/148.08 [rw[Ite][True][Let][Let]](x1, x2, x3, x4) = [0 0] x4 + [0] 555.20/148.08 [1 1] [0] 555.20/148.08 555.20/148.08 [rw](x1, x2) = [0] 555.20/148.08 [0] 555.20/148.08 555.20/148.08 [Val](x1) = [0] 555.20/148.08 [1] 555.20/148.08 555.20/148.08 [rewrite^#](x1) = [2 2] x1 + [0] 555.20/148.08 [0 0] [0] 555.20/148.08 555.20/148.08 [rw^#](x1, x2) = [2 2] x1 + [2 555.20/148.08 2] x2 + [0] 555.20/148.08 [0 0] [0 555.20/148.08 0] [4] 555.20/148.08 555.20/148.08 [rw[Ite][True][Let]^#](x1, x2, x3) = [0 2] x1 + [0] 555.20/148.08 [0 0] [0] 555.20/148.08 555.20/148.08 [c_2](x1) = [1 0] x1 + [0] 555.20/148.08 [0 0] [0] 555.20/148.08 555.20/148.08 [c_3](x1) = [1 0] x1 + [0] 555.20/148.08 [0 0] [0] 555.20/148.08 555.20/148.08 [c_4](x1) = [1 0] x1 + [0] 555.20/148.08 [0 0] [0] 555.20/148.08 555.20/148.08 [c_5] = [1] 555.20/148.08 [0] 555.20/148.08 555.20/148.08 [c_6] = [1] 555.20/148.08 [0] 555.20/148.08 555.20/148.08 [c_7](x1, x2) = [1 0] x1 + [1 555.20/148.08 0] x2 + [0] 555.20/148.08 [0 0] [0 555.20/148.08 0] [3] 555.20/148.08 555.20/148.08 [c_8](x1) = [1 0] x1 + [1] 555.20/148.08 [0 0] [3] 555.20/148.08 555.20/148.08 [c_9](x1) = [1 0] x1 + [2] 555.20/148.08 [0 0] [3] 555.20/148.08 555.20/148.08 [c_10](x1) = [1 0] x1 + [0] 555.20/148.08 [0 0] [0] 555.20/148.08 555.20/148.08 The order satisfies the following ordering constraints: 555.20/148.08 555.20/148.08 [second(Op(x, y))] = [1 0] y + [1 1] x + [0] 555.20/148.08 [0 1] [0 0] [0] 555.20/148.08 >= [1 0] y + [0] 555.20/148.08 [0 1] [0] 555.20/148.08 = [y] 555.20/148.08 555.20/148.08 [rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1)] = [7 0] c + [0] 555.20/148.08 [7 7] [0] 555.20/148.08 >= [0] 555.20/148.08 [0] 555.20/148.08 = [rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.08 c, 555.20/148.08 a1, 555.20/148.08 rewrite(x))] 555.20/148.08 555.20/148.08 [rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1)] = [7 0] c + [0] 555.20/148.08 [7 7] [0] 555.20/148.08 ? [0] 555.20/148.08 [1] 555.20/148.08 = [rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n))] 555.20/148.08 555.20/148.08 [rewrite(Op(Op(x', y'), Op(x', Op(x, y))))] = [0] 555.20/148.08 [0] 555.20/148.08 >= [0] 555.20/148.08 [0] 555.20/148.08 = [rw(x', x)] 555.20/148.08 555.20/148.08 [rewrite(Op(Op(x', y'), Op(x, Val(n))))] = [0] 555.20/148.08 [0] 555.20/148.08 >= [0] 555.20/148.08 [0] 555.20/148.08 = [rw(x, Val(n))] 555.20/148.08 555.20/148.08 [rewrite(Op(Op(x, y), Val(n)))] = [0] 555.20/148.08 [0] 555.20/148.08 >= [0] 555.20/148.08 [0] 555.20/148.08 = [rw(Val(n), first(second(Val(n))))] 555.20/148.08 555.20/148.08 [rewrite(Op(Val(n), y))] = [0] 555.20/148.08 [0] 555.20/148.08 ? [0 1] y + [0] 555.20/148.08 [1 0] [1] 555.20/148.08 = [Op(Val(n), y)] 555.20/148.08 555.20/148.08 [rewrite(Val(n))] = [0] 555.20/148.09 [0] 555.20/148.09 ? [0] 555.20/148.09 [1] 555.20/148.09 = [Val(n)] 555.20/148.09 555.20/148.09 [first(Op(x, y))] = [4 0] y + [4 4] x + [0] 555.20/148.09 [2 0] [2 2] [0] 555.20/148.09 >= [1 0] x + [0] 555.20/148.09 [0 1] [0] 555.20/148.09 = [x] 555.20/148.09 555.20/148.09 [first(Val(n))] = [4] 555.20/148.09 [2] 555.20/148.09 > [0] 555.20/148.09 [1] 555.20/148.09 = [Val(n)] 555.20/148.09 555.20/148.09 [rw(Op(Op(x', y'), Op(x, y)), c)] = [0] 555.20/148.09 [0] 555.20/148.09 ? [7 0] c + [0] 555.20/148.09 [7 7] [0] 555.20/148.09 = [rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x))] 555.20/148.09 555.20/148.09 [rw(Op(Op(x, y), Val(n)), c)] = [0] 555.20/148.09 [0] 555.20/148.09 ? [7 0] c + [0] 555.20/148.09 [7 7] [0] 555.20/148.09 = [rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n))] 555.20/148.09 555.20/148.09 [rw(Op(Val(n), y), c)] = [0] 555.20/148.09 [0] 555.20/148.09 ? [0 0] y + [0] 555.20/148.09 [1 1] [1] 555.20/148.09 = [Op(Op(Val(n), y), rewrite(c))] 555.20/148.09 555.20/148.09 [rw(Val(n), c)] = [0] 555.20/148.09 [0] 555.20/148.09 ? [0] 555.20/148.09 [1] 555.20/148.09 = [Op(Val(n), rewrite(c))] 555.20/148.09 555.20/148.09 [rewrite^#(Op(Op(x', y'), Op(x', Op(x, y))))] = [2 2] y + [2 2] x + [4 4] x' + [2 2] y' + [0] 555.20/148.09 [0 0] [0 0] [0 0] [0 0] [0] 555.20/148.09 >= [2 2] x + [2 2] x' + [0] 555.20/148.09 [0 0] [0 0] [0] 555.20/148.09 = [c_2(rw^#(x', x))] 555.20/148.09 555.20/148.09 [rewrite^#(Op(Op(x', y'), Op(x, Val(n))))] = [2 2] x + [2 2] x' + [2 2] y' + [2] 555.20/148.09 [0 0] [0 0] [0 0] [0] 555.20/148.09 >= [2 2] x + [2] 555.20/148.09 [0 0] [0] 555.20/148.09 = [c_3(rw^#(x, Val(n)))] 555.20/148.09 555.20/148.09 [rewrite^#(Op(Op(x, y), Val(n)))] = [2 2] y + [2 2] x + [2] 555.20/148.09 [0 0] [0 0] [0] 555.20/148.09 >= [2] 555.20/148.09 [0] 555.20/148.09 = [c_4(rw^#(Val(n), first(second(Val(n)))))] 555.20/148.09 555.20/148.09 [rewrite^#(Op(Val(n), y))] = [2 2] y + [2] 555.20/148.09 [0 0] [0] 555.20/148.09 > [1] 555.20/148.09 [0] 555.20/148.09 = [c_5()] 555.20/148.09 555.20/148.09 [rewrite^#(Val(n))] = [2] 555.20/148.09 [0] 555.20/148.09 > [1] 555.20/148.09 [0] 555.20/148.09 = [c_6()] 555.20/148.09 555.20/148.09 [rw^#(Op(Op(x', y'), Op(x, y)), c)] = [2 2] c + [2 2] y + [2 2] x + [2 2] x' + [2 2] y' + [0] 555.20/148.09 [0 0] [0 0] [0 0] [0 0] [0 0] [4] 555.20/148.09 >= [0 2] y + [2 2] x + [2 2] x' + [2 2] y' + [0] 555.20/148.09 [0 0] [0 0] [0 0] [0 0] [3] 555.20/148.09 = [c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.09 rewrite^#(x))] 555.20/148.09 555.20/148.09 [rw^#(Op(Val(n), y), c)] = [2 2] c + [2 2] y + [2] 555.20/148.09 [0 0] [0 0] [4] 555.20/148.09 > [2 2] c + [1] 555.20/148.09 [0 0] [3] 555.20/148.09 = [c_8(rewrite^#(c))] 555.20/148.09 555.20/148.09 [rw^#(Val(n), c)] = [2 2] c + [2] 555.20/148.09 [0 0] [4] 555.20/148.09 >= [2 2] c + [2] 555.20/148.09 [0 0] [3] 555.20/148.09 = [c_9(rewrite^#(c))] 555.20/148.09 555.20/148.09 [rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1)] = [2 0] y + [2 2] x + [2 2] x' + [0] 555.20/148.09 [0 0] [0 0] [0 0] [0] 555.20/148.09 >= [2 2] x + [0] 555.20/148.09 [0 0] [0] 555.20/148.09 = [c_10(rewrite^#(x))] 555.20/148.09 555.20/148.09 555.20/148.09 The strictly oriented rules are moved into the weak component. 555.20/148.09 555.20/148.09 We are left with following problem, upon which TcT provides the 555.20/148.09 certificate YES(O(1),O(n^1)). 555.20/148.09 555.20/148.09 Strict DPs: 555.20/148.09 { rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_2(rw^#(x', x)) 555.20/148.09 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_3(rw^#(x, Val(n))) 555.20/148.09 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.09 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.09 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.09 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.09 rewrite^#(x)) 555.20/148.09 , rw^#(Val(n), c) -> c_9(rewrite^#(c)) } 555.20/148.09 Weak DPs: 555.20/148.09 { rewrite^#(Op(Val(n), y)) -> c_5() 555.20/148.09 , rewrite^#(Val(n)) -> c_6() 555.20/148.09 , rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.20/148.09 , rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.09 c_10(rewrite^#(x)) } 555.20/148.09 Weak Trs: 555.20/148.09 { second(Op(x, y)) -> y 555.20/148.09 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.09 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.09 c, 555.20/148.09 a1, 555.20/148.09 rewrite(x)) 555.20/148.09 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.09 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.09 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.09 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.09 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.09 rw(Val(n), first(second(Val(n)))) 555.20/148.09 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.09 , rewrite(Val(n)) -> Val(n) 555.20/148.09 , first(Op(x, y)) -> x 555.20/148.09 , first(Val(n)) -> Val(n) 555.20/148.09 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.09 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.09 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.09 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.09 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.09 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.09 Obligation: 555.20/148.09 innermost runtime complexity 555.20/148.09 Answer: 555.20/148.09 YES(O(1),O(n^1)) 555.20/148.09 555.20/148.09 The following weak DPs constitute a sub-graph of the DG that is 555.20/148.09 closed under successors. The DPs are removed. 555.20/148.09 555.20/148.09 { rewrite^#(Op(Val(n), y)) -> c_5() 555.20/148.09 , rewrite^#(Val(n)) -> c_6() } 555.20/148.09 555.20/148.09 We are left with following problem, upon which TcT provides the 555.20/148.09 certificate YES(O(1),O(n^1)). 555.20/148.09 555.20/148.09 Strict DPs: 555.20/148.09 { rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_2(rw^#(x', x)) 555.20/148.09 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_3(rw^#(x, Val(n))) 555.20/148.09 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.09 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.09 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.09 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.09 rewrite^#(x)) 555.20/148.09 , rw^#(Val(n), c) -> c_9(rewrite^#(c)) } 555.20/148.09 Weak DPs: 555.20/148.09 { rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.20/148.09 , rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.09 c_10(rewrite^#(x)) } 555.20/148.09 Weak Trs: 555.20/148.09 { second(Op(x, y)) -> y 555.20/148.09 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.09 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.09 c, 555.20/148.09 a1, 555.20/148.09 rewrite(x)) 555.20/148.09 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.20/148.09 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.20/148.09 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.20/148.09 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.20/148.09 , rewrite(Op(Op(x, y), Val(n))) -> 555.20/148.09 rw(Val(n), first(second(Val(n)))) 555.20/148.09 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.20/148.09 , rewrite(Val(n)) -> Val(n) 555.20/148.09 , first(Op(x, y)) -> x 555.20/148.09 , first(Val(n)) -> Val(n) 555.20/148.09 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.09 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.20/148.09 , rw(Op(Op(x, y), Val(n)), c) -> 555.20/148.09 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.20/148.09 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.20/148.09 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.20/148.09 Obligation: 555.20/148.09 innermost runtime complexity 555.20/148.09 Answer: 555.20/148.09 YES(O(1),O(n^1)) 555.20/148.09 555.20/148.09 We use the processor 'matrix interpretation of dimension 2' to 555.20/148.09 orient following rules strictly. 555.20/148.09 555.20/148.09 DPs: 555.20/148.09 { 1: rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> 555.20/148.09 c_2(rw^#(x', x)) 555.20/148.09 , 2: rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> 555.20/148.09 c_3(rw^#(x, Val(n))) 555.20/148.09 , 3: rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.09 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.09 , 4: rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.09 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.09 rewrite^#(x)) 555.20/148.09 , 7: rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.09 c_10(rewrite^#(x)) } 555.20/148.09 Trs: 555.20/148.09 { second(Op(x, y)) -> y 555.20/148.09 , first(Op(x, y)) -> x } 555.20/148.09 555.20/148.09 Sub-proof: 555.20/148.09 ---------- 555.20/148.09 The following argument positions are usable: 555.20/148.09 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, 555.20/148.09 Uargs(c_7) = {1, 2}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, 555.20/148.09 Uargs(c_10) = {1} 555.20/148.09 555.20/148.09 TcT has computed the following constructor-based matrix 555.20/148.09 interpretation satisfying not(EDA) and not(IDA(1)). 555.20/148.09 555.20/148.09 [second](x1) = [0 1] x1 + [0] 555.20/148.09 [2 0] [0] 555.20/148.09 555.20/148.09 [Op](x1, x2) = [1 1] x1 + [0 555.20/148.09 1] x2 + [1] 555.20/148.09 [0 0] [1 555.20/148.09 0] [2] 555.20/148.09 555.20/148.09 [rw[Ite][True][Let]](x1, x2, x3) = [7 0] x2 + [0] 555.20/148.09 [7 7] [0] 555.20/148.09 555.20/148.09 [rewrite](x1) = [0] 555.20/148.09 [0] 555.20/148.09 555.20/148.09 [first](x1) = [4 0] x1 + [0] 555.20/148.09 [4 0] [0] 555.20/148.09 555.20/148.09 [rw[Ite][True][Let][Let]](x1, x2, x3, x4) = [0] 555.20/148.09 [0] 555.20/148.09 555.20/148.09 [rw](x1, x2) = [0] 555.20/148.09 [0] 555.20/148.09 555.20/148.09 [Val](x1) = [0] 555.20/148.09 [0] 555.20/148.09 555.20/148.09 [rewrite^#](x1) = [1 1] x1 + [0] 555.20/148.09 [0 0] [0] 555.20/148.09 555.20/148.09 [rw^#](x1, x2) = [1 1] x1 + [1 555.20/148.09 1] x2 + [0] 555.20/148.09 [0 0] [0 555.20/148.09 0] [4] 555.20/148.09 555.20/148.09 [rw[Ite][True][Let]^#](x1, x2, x3) = [1 0] x1 + [0] 555.20/148.09 [0 0] [0] 555.20/148.09 555.20/148.09 [c_2](x1) = [1 0] x1 + [1] 555.20/148.09 [0 0] [0] 555.20/148.09 555.20/148.09 [c_3](x1) = [1 0] x1 + [3] 555.20/148.09 [0 0] [0] 555.20/148.09 555.20/148.09 [c_4](x1) = [2 0] x1 + [3] 555.20/148.09 [0 0] [0] 555.20/148.09 555.20/148.09 [c_5] = [0] 555.20/148.09 [0] 555.20/148.09 555.20/148.09 [c_6] = [0] 555.20/148.09 [0] 555.20/148.09 555.20/148.09 [c_7](x1, x2) = [1 0] x1 + [1 555.20/148.09 0] x2 + [1] 555.20/148.09 [0 0] [0 555.20/148.09 0] [3] 555.20/148.09 555.20/148.09 [c_8](x1) = [1 0] x1 + [3] 555.20/148.09 [0 0] [3] 555.20/148.09 555.20/148.09 [c_9](x1) = [1 0] x1 + [0] 555.20/148.09 [0 0] [3] 555.20/148.09 555.20/148.09 [c_10](x1) = [1 0] x1 + [3] 555.20/148.09 [0 0] [0] 555.20/148.09 555.20/148.09 The order satisfies the following ordering constraints: 555.20/148.09 555.20/148.09 [second(Op(x, y))] = [1 0] y + [0 0] x + [2] 555.20/148.09 [0 2] [2 2] [2] 555.20/148.09 > [1 0] y + [0] 555.20/148.09 [0 1] [0] 555.20/148.09 = [y] 555.20/148.09 555.20/148.09 [rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1)] = [7 0] c + [0] 555.20/148.09 [7 7] [0] 555.20/148.09 >= [0] 555.20/148.09 [0] 555.20/148.09 = [rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.20/148.09 c, 555.20/148.09 a1, 555.20/148.09 rewrite(x))] 555.20/148.09 555.20/148.09 [rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1)] = [7 0] c + [0] 555.20/148.09 [7 7] [0] 555.20/148.09 >= [0] 555.20/148.09 [0] 555.20/148.09 = [rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n))] 555.20/148.09 555.20/148.09 [rewrite(Op(Op(x', y'), Op(x', Op(x, y))))] = [0] 555.20/148.09 [0] 555.20/148.09 >= [0] 555.20/148.09 [0] 555.20/148.09 = [rw(x', x)] 555.20/148.09 555.20/148.09 [rewrite(Op(Op(x', y'), Op(x, Val(n))))] = [0] 555.20/148.09 [0] 555.20/148.09 >= [0] 555.20/148.09 [0] 555.20/148.09 = [rw(x, Val(n))] 555.20/148.09 555.20/148.09 [rewrite(Op(Op(x, y), Val(n)))] = [0] 555.20/148.09 [0] 555.20/148.09 >= [0] 555.20/148.09 [0] 555.20/148.09 = [rw(Val(n), first(second(Val(n))))] 555.20/148.09 555.20/148.09 [rewrite(Op(Val(n), y))] = [0] 555.20/148.09 [0] 555.20/148.09 ? [0 1] y + [1] 555.20/148.09 [1 0] [2] 555.20/148.09 = [Op(Val(n), y)] 555.20/148.09 555.20/148.09 [rewrite(Val(n))] = [0] 555.20/148.09 [0] 555.20/148.09 >= [0] 555.20/148.09 [0] 555.20/148.09 = [Val(n)] 555.20/148.09 555.20/148.09 [first(Op(x, y))] = [0 4] y + [4 4] x + [4] 555.20/148.09 [0 4] [4 4] [4] 555.20/148.09 > [1 0] x + [0] 555.20/148.09 [0 1] [0] 555.20/148.09 = [x] 555.20/148.09 555.20/148.09 [first(Val(n))] = [0] 555.20/148.09 [0] 555.20/148.09 >= [0] 555.20/148.09 [0] 555.20/148.09 = [Val(n)] 555.20/148.09 555.20/148.09 [rw(Op(Op(x', y'), Op(x, y)), c)] = [0] 555.20/148.09 [0] 555.20/148.09 ? [7 0] c + [0] 555.20/148.09 [7 7] [0] 555.20/148.09 = [rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x))] 555.20/148.09 555.20/148.09 [rw(Op(Op(x, y), Val(n)), c)] = [0] 555.20/148.09 [0] 555.20/148.09 ? [7 0] c + [0] 555.20/148.09 [7 7] [0] 555.20/148.09 = [rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n))] 555.20/148.09 555.20/148.09 [rw(Op(Val(n), y), c)] = [0] 555.20/148.09 [0] 555.20/148.09 ? [1 1] y + [4] 555.20/148.09 [0 0] [2] 555.20/148.09 = [Op(Op(Val(n), y), rewrite(c))] 555.20/148.09 555.20/148.09 [rw(Val(n), c)] = [0] 555.20/148.09 [0] 555.20/148.09 ? [1] 555.20/148.09 [2] 555.20/148.09 = [Op(Val(n), rewrite(c))] 555.20/148.09 555.20/148.09 [rewrite^#(Op(Op(x', y'), Op(x', Op(x, y))))] = [1 1] y + [1 1] x + [2 2] x' + [1 1] y' + [12] 555.20/148.09 [0 0] [0 0] [0 0] [0 0] [0] 555.20/148.09 > [1 1] x + [1 1] x' + [1] 555.20/148.09 [0 0] [0 0] [0] 555.20/148.09 = [c_2(rw^#(x', x))] 555.20/148.09 555.20/148.09 [rewrite^#(Op(Op(x', y'), Op(x, Val(n))))] = [1 1] x + [1 1] x' + [1 1] y' + [9] 555.20/148.09 [0 0] [0 0] [0 0] [0] 555.20/148.09 > [1 1] x + [3] 555.20/148.09 [0 0] [0] 555.20/148.09 = [c_3(rw^#(x, Val(n)))] 555.20/148.09 555.20/148.09 [rewrite^#(Op(Op(x, y), Val(n)))] = [1 1] y + [1 1] x + [6] 555.20/148.09 [0 0] [0 0] [0] 555.20/148.09 > [3] 555.20/148.09 [0] 555.20/148.09 = [c_4(rw^#(Val(n), first(second(Val(n)))))] 555.20/148.09 555.20/148.09 [rw^#(Op(Op(x', y'), Op(x, y)), c)] = [1 1] c + [1 1] y + [1 1] x + [1 1] x' + [1 1] y' + [9] 555.20/148.09 [0 0] [0 0] [0 0] [0 0] [0 0] [4] 555.20/148.09 > [1 0] y + [1 1] x + [1 1] x' + [1 1] y' + [7] 555.20/148.09 [0 0] [0 0] [0 0] [0 0] [3] 555.20/148.09 = [c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.10 rewrite^#(x))] 555.20/148.10 555.20/148.10 [rw^#(Op(Val(n), y), c)] = [1 1] c + [1 1] y + [3] 555.20/148.10 [0 0] [0 0] [4] 555.20/148.10 >= [1 1] c + [3] 555.20/148.10 [0 0] [3] 555.20/148.10 = [c_8(rewrite^#(c))] 555.20/148.10 555.20/148.10 [rw^#(Val(n), c)] = [1 1] c + [0] 555.20/148.10 [0 0] [4] 555.20/148.10 >= [1 1] c + [0] 555.20/148.10 [0 0] [3] 555.20/148.10 = [c_9(rewrite^#(c))] 555.20/148.10 555.20/148.10 [rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1)] = [0 1] y + [1 1] x + [1 1] x' + [4] 555.20/148.10 [0 0] [0 0] [0 0] [0] 555.20/148.10 > [1 1] x + [3] 555.20/148.10 [0 0] [0] 555.20/148.10 = [c_10(rewrite^#(x))] 555.20/148.10 555.20/148.10 555.20/148.10 We return to the main proof. Consider the set of all dependency 555.20/148.10 pairs 555.20/148.10 555.20/148.10 : 555.20/148.10 { 1: rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> 555.20/148.10 c_2(rw^#(x', x)) 555.20/148.10 , 2: rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> 555.20/148.10 c_3(rw^#(x, Val(n))) 555.20/148.10 , 3: rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.10 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.10 , 4: rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.20/148.10 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.20/148.10 rewrite^#(x)) 555.20/148.10 , 5: rw^#(Val(n), c) -> c_9(rewrite^#(c)) 555.20/148.10 , 6: rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.20/148.10 , 7: rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.20/148.10 c_10(rewrite^#(x)) } 555.20/148.10 555.20/148.10 Processor 'matrix interpretation of dimension 2' induces the 555.20/148.10 complexity certificate YES(?,O(n^1)) on application of dependency 555.20/148.10 pairs {1,2,3,4,7}. These cover all (indirect) predecessors of 555.20/148.10 dependency pairs {1,2,3,4,5,6,7}, their number of application is 555.20/148.10 equally bounded. The dependency pairs are shifted into the weak 555.20/148.10 component. 555.20/148.10 555.20/148.10 We are left with following problem, upon which TcT provides the 555.20/148.10 certificate YES(O(1),O(1)). 555.20/148.10 555.20/148.10 Weak DPs: 555.20/148.10 { rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_2(rw^#(x', x)) 555.20/148.10 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_3(rw^#(x, Val(n))) 555.20/148.10 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.20/148.10 c_4(rw^#(Val(n), first(second(Val(n))))) 555.20/148.10 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.56/148.10 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.56/148.10 rewrite^#(x)) 555.56/148.10 , rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.56/148.10 , rw^#(Val(n), c) -> c_9(rewrite^#(c)) 555.56/148.10 , rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.56/148.10 c_10(rewrite^#(x)) } 555.56/148.10 Weak Trs: 555.56/148.10 { second(Op(x, y)) -> y 555.56/148.10 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.56/148.10 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.56/148.10 c, 555.56/148.10 a1, 555.56/148.10 rewrite(x)) 555.56/148.10 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.56/148.10 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.56/148.10 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.56/148.10 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.56/148.10 , rewrite(Op(Op(x, y), Val(n))) -> 555.56/148.10 rw(Val(n), first(second(Val(n)))) 555.56/148.10 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.56/148.10 , rewrite(Val(n)) -> Val(n) 555.56/148.10 , first(Op(x, y)) -> x 555.56/148.10 , first(Val(n)) -> Val(n) 555.56/148.10 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.56/148.10 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.56/148.10 , rw(Op(Op(x, y), Val(n)), c) -> 555.56/148.10 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.56/148.10 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.56/148.10 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.56/148.10 Obligation: 555.56/148.10 innermost runtime complexity 555.56/148.10 Answer: 555.56/148.10 YES(O(1),O(1)) 555.56/148.10 555.56/148.10 The following weak DPs constitute a sub-graph of the DG that is 555.56/148.10 closed under successors. The DPs are removed. 555.56/148.10 555.56/148.10 { rewrite^#(Op(Op(x', y'), Op(x', Op(x, y)))) -> c_2(rw^#(x', x)) 555.56/148.10 , rewrite^#(Op(Op(x', y'), Op(x, Val(n)))) -> c_3(rw^#(x, Val(n))) 555.56/148.10 , rewrite^#(Op(Op(x, y), Val(n))) -> 555.56/148.10 c_4(rw^#(Val(n), first(second(Val(n))))) 555.56/148.10 , rw^#(Op(Op(x', y'), Op(x, y)), c) -> 555.56/148.10 c_7(rw[Ite][True][Let]^#(Op(Op(x', y'), Op(x, y)), c, rewrite(x)), 555.56/148.10 rewrite^#(x)) 555.56/148.10 , rw^#(Op(Val(n), y), c) -> c_8(rewrite^#(c)) 555.56/148.10 , rw^#(Val(n), c) -> c_9(rewrite^#(c)) 555.56/148.10 , rw[Ite][True][Let]^#(Op(x', Op(x', Op(x, y))), c, a1) -> 555.56/148.10 c_10(rewrite^#(x)) } 555.56/148.10 555.56/148.10 We are left with following problem, upon which TcT provides the 555.56/148.10 certificate YES(O(1),O(1)). 555.56/148.10 555.56/148.10 Weak Trs: 555.56/148.10 { second(Op(x, y)) -> y 555.56/148.10 , rw[Ite][True][Let](Op(x', Op(x', Op(x, y))), c, a1) -> 555.56/148.10 rw[Ite][True][Let][Let](Op(x', Op(x', Op(x, y))), 555.56/148.10 c, 555.56/148.10 a1, 555.56/148.10 rewrite(x)) 555.56/148.10 , rw[Ite][True][Let](Op(x', Op(x, Val(n))), c, a1) -> 555.56/148.10 rw[Ite][True][Let][Let](Op(x', Op(x, Val(n))), c, a1, Val(n)) 555.56/148.10 , rewrite(Op(Op(x', y'), Op(x', Op(x, y)))) -> rw(x', x) 555.56/148.10 , rewrite(Op(Op(x', y'), Op(x, Val(n)))) -> rw(x, Val(n)) 555.56/148.10 , rewrite(Op(Op(x, y), Val(n))) -> 555.56/148.10 rw(Val(n), first(second(Val(n)))) 555.56/148.10 , rewrite(Op(Val(n), y)) -> Op(Val(n), y) 555.56/148.10 , rewrite(Val(n)) -> Val(n) 555.56/148.10 , first(Op(x, y)) -> x 555.56/148.10 , first(Val(n)) -> Val(n) 555.56/148.10 , rw(Op(Op(x', y'), Op(x, y)), c) -> 555.56/148.10 rw[Ite][True][Let](Op(Op(x', y'), Op(x, y)), c, rewrite(x)) 555.56/148.10 , rw(Op(Op(x, y), Val(n)), c) -> 555.56/148.10 rw[Ite][True][Let](Op(Op(x, y), Val(n)), c, Val(n)) 555.56/148.10 , rw(Op(Val(n), y), c) -> Op(Op(Val(n), y), rewrite(c)) 555.56/148.10 , rw(Val(n), c) -> Op(Val(n), rewrite(c)) } 555.56/148.10 Obligation: 555.56/148.10 innermost runtime complexity 555.56/148.10 Answer: 555.56/148.10 YES(O(1),O(1)) 555.56/148.10 555.56/148.10 No rule is usable, rules are removed from the input problem. 555.56/148.10 555.56/148.10 We are left with following problem, upon which TcT provides the 555.56/148.10 certificate YES(O(1),O(1)). 555.56/148.10 555.56/148.10 Rules: Empty 555.56/148.10 Obligation: 555.56/148.10 innermost runtime complexity 555.56/148.10 Answer: 555.56/148.10 YES(O(1),O(1)) 555.56/148.10 555.56/148.10 Empty rules are trivially bounded 555.56/148.10 555.56/148.10 Hurray, we answered YES(O(1),O(n^1)) 555.87/148.44 EOF