YES(O(1),O(n^1)) 96.16/24.88 YES(O(1),O(n^1)) 96.16/24.88 96.16/24.88 We are left with following problem, upon which TcT provides the 96.16/24.88 certificate YES(O(1),O(n^1)). 96.16/24.88 96.16/24.88 Strict Trs: 96.16/24.88 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.16/24.88 , l5(x, y, res, tmp, mtmp, False()) -> 96.16/24.88 l7(x, y, res, tmp, mtmp, False()) 96.16/24.88 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.16/24.88 , l13(x, y, res, tmp, True(), t) -> 96.16/24.88 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.16/24.88 , l13(x, y, res, tmp, False(), t) -> 96.16/24.88 l16(x, y, gcd(0(), y), tmp, False(), t) 96.16/24.88 , help1(S(S(x))) -> True() 96.16/24.88 , help1(S(0())) -> False() 96.16/24.88 , help1(0()) -> False() 96.16/24.88 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.16/24.88 , e7(a, b, res, t) -> False() 96.16/24.88 , m3(S(S(x)), b, res, t) -> True() 96.16/24.88 , m3(S(0()), b, res, t) -> False() 96.16/24.88 , m3(0(), b, res, t) -> False() 96.16/24.88 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.16/24.88 , e2(a, b, res, False()) -> False() 96.16/24.88 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.16/24.88 , e6(a, b, res, t) -> False() 96.16/24.88 , l14(x, y, res, tmp, mtmp, t) -> 96.16/24.88 l15(x, y, res, tmp, monus(x, y), t) 96.16/24.88 , l9(res, y, res', tmp, mtmp, t) -> res 96.16/24.88 , bool2Nat(True()) -> S(0()) 96.16/24.88 , bool2Nat(False()) -> 0() 96.16/24.88 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.16/24.88 , l8(res, y, res', True(), mtmp, t) -> res 96.16/24.88 , l8(x, y, res, False(), mtmp, t) -> 96.16/24.88 l10(x, y, res, False(), mtmp, t) 96.16/24.88 , m5(a, b, res, t) -> res 96.16/24.88 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.16/24.88 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.16/24.88 , equal0(a, b) -> e1(a, b, False(), False()) 96.16/24.88 , l12(x, y, res, tmp, mtmp, t) -> 96.16/24.88 l13(x, y, res, tmp, monus(x, y), t) 96.16/24.88 , e8(a, b, res, t) -> res 96.16/24.88 , l7(x, y, res, tmp, mtmp, t) -> 96.16/24.88 l8(x, y, res, equal0(x, y), mtmp, t) 96.16/24.88 , l11(x, y, res, tmp, mtmp, True()) -> 96.16/24.88 l12(x, y, res, tmp, mtmp, True()) 96.16/24.88 , l11(x, y, res, tmp, mtmp, False()) -> 96.16/24.88 l14(x, y, res, tmp, mtmp, False()) 96.16/24.88 , e5(a, b, res, t) -> True() 96.16/24.88 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.16/24.88 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.16/24.88 , m2(S(S(x)), b, res, True()) -> True() 96.16/24.88 , m2(S(0()), b, res, True()) -> False() 96.16/24.88 , m2(0(), b, res, True()) -> False() 96.16/24.88 , monus(a, b) -> m1(a, b, False(), False()) 96.16/24.88 , l2(x, y, res, tmp, mtmp, True()) -> res 96.16/24.88 , l2(x, y, res, tmp, mtmp, False()) -> 96.16/24.88 l3(x, y, res, tmp, mtmp, False()) 96.16/24.88 , l4(x', x, res, tmp, mtmp, t) -> 96.16/24.88 l5(x', x, res, tmp, mtmp, False()) 96.16/24.88 , l10(x, y, res, tmp, mtmp, t) -> 96.16/24.88 l11(x, y, res, tmp, mtmp, <(x, y)) 96.16/24.88 , l15(x, y, res, tmp, True(), t) -> 96.16/24.88 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.16/24.88 , l15(x, y, res, tmp, False(), t) -> 96.16/24.88 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.16/24.88 , l16(x, y, res, tmp, mtmp, t) -> res 96.16/24.88 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.16/24.88 , e4(a, b, res, True()) -> True() 96.16/24.88 , e4(a, b, res, False()) -> False() } 96.16/24.88 Weak Trs: 96.16/24.88 { <(x, 0()) -> False() 96.16/24.88 , <(S(x), S(y)) -> <(x, y) 96.16/24.88 , <(0(), S(y)) -> True() } 96.16/24.88 Obligation: 96.16/24.88 innermost runtime complexity 96.16/24.88 Answer: 96.16/24.88 YES(O(1),O(n^1)) 96.16/24.88 96.16/24.88 We add the following dependency tuples: 96.16/24.88 96.16/24.88 Strict DPs: 96.16/24.88 { l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.16/24.88 , l5^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.88 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.16/24.88 , l7^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.16/24.88 , l1^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.16/24.88 , l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.16/24.88 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.88 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.16/24.88 , l13^#(x, y, res, tmp, True(), t) -> 96.16/24.88 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.16/24.88 , l13^#(x, y, res, tmp, False(), t) -> 96.16/24.88 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.16/24.88 , l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.16/24.88 , gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.16/24.88 , help1^#(S(S(x))) -> c_6() 96.16/24.88 , help1^#(S(0())) -> c_7() 96.16/24.88 , help1^#(0()) -> c_8() 96.16/24.88 , e7^#(a, b, res, t) -> c_10() 96.16/24.88 , m3^#(S(S(x)), b, res, t) -> c_11() 96.16/24.88 , m3^#(S(0()), b, res, t) -> c_12() 96.16/24.88 , m3^#(0(), b, res, t) -> c_13() 96.16/24.88 , e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.16/24.88 , e2^#(a, b, res, False()) -> c_15() 96.16/24.88 , e3^#(a, b, res, t) -> 96.16/24.88 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.16/24.88 , e4^#(a, b, res, True()) -> c_49() 96.16/24.88 , e4^#(a, b, res, False()) -> c_50() 96.16/24.88 , e6^#(a, b, res, t) -> c_17() 96.16/24.88 , l14^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.88 , l15^#(x, y, res, tmp, True(), t) -> 96.16/24.88 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.16/24.88 , l15^#(x, y, res, tmp, False(), t) -> 96.16/24.88 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.16/24.88 , monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.16/24.88 , l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.16/24.88 , bool2Nat^#(True()) -> c_20() 96.16/24.88 , bool2Nat^#(False()) -> c_21() 96.16/24.88 , l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.16/24.88 , l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.16/24.88 , l8^#(x, y, res, False(), mtmp, t) -> 96.16/24.88 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.16/24.88 , l10^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.16/24.88 , m5^#(a, b, res, t) -> c_25() 96.16/24.88 , e1^#(a, b, res, t) -> 96.16/24.88 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.16/24.88 , m4^#(S(x'), S(x), res, t) -> 96.16/24.88 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.16/24.88 , equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.16/24.88 , l12^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.88 , e8^#(a, b, res, t) -> c_30() 96.16/24.88 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.16/24.88 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.16/24.88 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.88 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.16/24.88 , e5^#(a, b, res, t) -> c_34() 96.16/24.88 , l3^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.16/24.88 , l4^#(x', x, res, tmp, mtmp, t) -> 96.16/24.88 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.16/24.88 , m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.16/24.88 , m2^#(S(S(x)), b, res, True()) -> c_37() 96.16/24.88 , m2^#(S(0()), b, res, True()) -> c_38() 96.16/24.88 , m2^#(0(), b, res, True()) -> c_39() 96.16/24.88 , m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) } 96.16/24.88 Weak DPs: 96.16/24.88 { <^#(x, 0()) -> c_51() 96.16/24.88 , <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.16/24.88 , <^#(0(), S(y)) -> c_53() } 96.16/24.88 96.16/24.88 and mark the set of starting terms. 96.16/24.88 96.16/24.88 We are left with following problem, upon which TcT provides the 96.16/24.88 certificate YES(O(1),O(n^1)). 96.16/24.88 96.16/24.88 Strict DPs: 96.16/24.88 { l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.16/24.88 , l5^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.88 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.16/24.88 , l7^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.16/24.88 , l1^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.16/24.88 , l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.16/24.88 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.88 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.16/24.88 , l13^#(x, y, res, tmp, True(), t) -> 96.16/24.88 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.16/24.88 , l13^#(x, y, res, tmp, False(), t) -> 96.16/24.88 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.16/24.88 , l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.16/24.88 , gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.16/24.88 , help1^#(S(S(x))) -> c_6() 96.16/24.88 , help1^#(S(0())) -> c_7() 96.16/24.88 , help1^#(0()) -> c_8() 96.16/24.88 , e7^#(a, b, res, t) -> c_10() 96.16/24.88 , m3^#(S(S(x)), b, res, t) -> c_11() 96.16/24.88 , m3^#(S(0()), b, res, t) -> c_12() 96.16/24.88 , m3^#(0(), b, res, t) -> c_13() 96.16/24.88 , e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.16/24.88 , e2^#(a, b, res, False()) -> c_15() 96.16/24.88 , e3^#(a, b, res, t) -> 96.16/24.88 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.16/24.88 , e4^#(a, b, res, True()) -> c_49() 96.16/24.88 , e4^#(a, b, res, False()) -> c_50() 96.16/24.88 , e6^#(a, b, res, t) -> c_17() 96.16/24.88 , l14^#(x, y, res, tmp, mtmp, t) -> 96.16/24.88 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.88 , l15^#(x, y, res, tmp, True(), t) -> 96.16/24.88 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.16/24.88 , l15^#(x, y, res, tmp, False(), t) -> 96.16/24.88 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.16/24.88 , monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.16/24.88 , l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.16/24.88 , bool2Nat^#(True()) -> c_20() 96.16/24.88 , bool2Nat^#(False()) -> c_21() 96.16/24.89 , l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.16/24.89 , l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.16/24.89 , l8^#(x, y, res, False(), mtmp, t) -> 96.16/24.89 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.16/24.89 , l10^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.16/24.89 , m5^#(a, b, res, t) -> c_25() 96.16/24.89 , e1^#(a, b, res, t) -> 96.16/24.89 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.16/24.89 , m4^#(S(x'), S(x), res, t) -> 96.16/24.89 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.16/24.89 , equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.16/24.89 , l12^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.89 , e8^#(a, b, res, t) -> c_30() 96.16/24.89 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.16/24.89 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.16/24.89 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , e5^#(a, b, res, t) -> c_34() 96.16/24.89 , l3^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.16/24.89 , l4^#(x', x, res, tmp, mtmp, t) -> 96.16/24.89 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.16/24.89 , m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.16/24.89 , m2^#(S(S(x)), b, res, True()) -> c_37() 96.16/24.89 , m2^#(S(0()), b, res, True()) -> c_38() 96.16/24.89 , m2^#(0(), b, res, True()) -> c_39() 96.16/24.89 , m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) } 96.16/24.89 Weak DPs: 96.16/24.89 { <^#(x, 0()) -> c_51() 96.16/24.89 , <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.16/24.89 , <^#(0(), S(y)) -> c_53() } 96.16/24.89 Weak Trs: 96.16/24.89 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.16/24.89 , l5(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 l7(x, y, res, tmp, mtmp, False()) 96.16/24.89 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.16/24.89 , l13(x, y, res, tmp, True(), t) -> 96.16/24.89 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.16/24.89 , l13(x, y, res, tmp, False(), t) -> 96.16/24.89 l16(x, y, gcd(0(), y), tmp, False(), t) 96.16/24.89 , help1(S(S(x))) -> True() 96.16/24.89 , help1(S(0())) -> False() 96.16/24.89 , help1(0()) -> False() 96.16/24.89 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.16/24.89 , e7(a, b, res, t) -> False() 96.16/24.89 , m3(S(S(x)), b, res, t) -> True() 96.16/24.89 , m3(S(0()), b, res, t) -> False() 96.16/24.89 , m3(0(), b, res, t) -> False() 96.16/24.89 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.16/24.89 , e2(a, b, res, False()) -> False() 96.16/24.89 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.16/24.89 , e6(a, b, res, t) -> False() 96.16/24.89 , l14(x, y, res, tmp, mtmp, t) -> 96.16/24.89 l15(x, y, res, tmp, monus(x, y), t) 96.16/24.89 , l9(res, y, res', tmp, mtmp, t) -> res 96.16/24.89 , bool2Nat(True()) -> S(0()) 96.16/24.89 , bool2Nat(False()) -> 0() 96.16/24.89 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.16/24.89 , l8(res, y, res', True(), mtmp, t) -> res 96.16/24.89 , l8(x, y, res, False(), mtmp, t) -> 96.16/24.89 l10(x, y, res, False(), mtmp, t) 96.16/24.89 , m5(a, b, res, t) -> res 96.16/24.89 , <(x, 0()) -> False() 96.16/24.89 , <(S(x), S(y)) -> <(x, y) 96.16/24.89 , <(0(), S(y)) -> True() 96.16/24.89 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.16/24.89 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.16/24.89 , equal0(a, b) -> e1(a, b, False(), False()) 96.16/24.89 , l12(x, y, res, tmp, mtmp, t) -> 96.16/24.89 l13(x, y, res, tmp, monus(x, y), t) 96.16/24.89 , e8(a, b, res, t) -> res 96.16/24.89 , l7(x, y, res, tmp, mtmp, t) -> 96.16/24.89 l8(x, y, res, equal0(x, y), mtmp, t) 96.16/24.89 , l11(x, y, res, tmp, mtmp, True()) -> 96.16/24.89 l12(x, y, res, tmp, mtmp, True()) 96.16/24.89 , l11(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 l14(x, y, res, tmp, mtmp, False()) 96.16/24.89 , e5(a, b, res, t) -> True() 96.16/24.89 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.16/24.89 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.16/24.89 , m2(S(S(x)), b, res, True()) -> True() 96.16/24.89 , m2(S(0()), b, res, True()) -> False() 96.16/24.89 , m2(0(), b, res, True()) -> False() 96.16/24.89 , monus(a, b) -> m1(a, b, False(), False()) 96.16/24.89 , l2(x, y, res, tmp, mtmp, True()) -> res 96.16/24.89 , l2(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 l3(x, y, res, tmp, mtmp, False()) 96.16/24.89 , l4(x', x, res, tmp, mtmp, t) -> 96.16/24.89 l5(x', x, res, tmp, mtmp, False()) 96.16/24.89 , l10(x, y, res, tmp, mtmp, t) -> 96.16/24.89 l11(x, y, res, tmp, mtmp, <(x, y)) 96.16/24.89 , l15(x, y, res, tmp, True(), t) -> 96.16/24.89 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.16/24.89 , l15(x, y, res, tmp, False(), t) -> 96.16/24.89 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.16/24.89 , l16(x, y, res, tmp, mtmp, t) -> res 96.16/24.89 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.16/24.89 , e4(a, b, res, True()) -> True() 96.16/24.89 , e4(a, b, res, False()) -> False() } 96.16/24.89 Obligation: 96.16/24.89 innermost runtime complexity 96.16/24.89 Answer: 96.16/24.89 YES(O(1),O(n^1)) 96.16/24.89 96.16/24.89 We estimate the number of application of 96.16/24.89 {1,5,9,11,12,13,14,15,16,17,19,21,22,23,28,29,30,31,32,35,40,43,47,48,49} 96.16/24.89 by applications of 96.16/24.89 Pre({1,5,9,11,12,13,14,15,16,17,19,21,22,23,28,29,30,31,32,35,40,43,47,48,49}) 96.16/24.89 = {3,7,8,20,25,26,36,37}. Here rules are labeled as follows: 96.16/24.89 96.16/24.89 DPs: 96.16/24.89 { 1: l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.16/24.89 , 2: l5^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , 3: l7^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.16/24.89 , 4: l1^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , 5: l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.16/24.89 , 6: l2^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , 7: l13^#(x, y, res, tmp, True(), t) -> 96.16/24.89 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.16/24.89 , 8: l13^#(x, y, res, tmp, False(), t) -> 96.16/24.89 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.16/24.89 , 9: l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.16/24.89 , 10: gcd^#(x, y) -> 96.16/24.89 c_9(l1^#(x, y, 0(), False(), False(), False())) 96.16/24.89 , 11: help1^#(S(S(x))) -> c_6() 96.16/24.89 , 12: help1^#(S(0())) -> c_7() 96.16/24.89 , 13: help1^#(0()) -> c_8() 96.16/24.89 , 14: e7^#(a, b, res, t) -> c_10() 96.16/24.89 , 15: m3^#(S(S(x)), b, res, t) -> c_11() 96.16/24.89 , 16: m3^#(S(0()), b, res, t) -> c_12() 96.16/24.89 , 17: m3^#(0(), b, res, t) -> c_13() 96.16/24.89 , 18: e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.16/24.89 , 19: e2^#(a, b, res, False()) -> c_15() 96.16/24.89 , 20: e3^#(a, b, res, t) -> 96.16/24.89 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.16/24.89 , 21: e4^#(a, b, res, True()) -> c_49() 96.16/24.89 , 22: e4^#(a, b, res, False()) -> c_50() 96.16/24.89 , 23: e6^#(a, b, res, t) -> c_17() 96.16/24.89 , 24: l14^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.89 , 25: l15^#(x, y, res, tmp, True(), t) -> 96.16/24.89 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.16/24.89 , 26: l15^#(x, y, res, tmp, False(), t) -> 96.16/24.89 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.16/24.89 , 27: monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.16/24.89 , 28: l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.16/24.89 , 29: bool2Nat^#(True()) -> c_20() 96.16/24.89 , 30: bool2Nat^#(False()) -> c_21() 96.16/24.89 , 31: l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.16/24.89 , 32: l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.16/24.89 , 33: l8^#(x, y, res, False(), mtmp, t) -> 96.16/24.89 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.16/24.89 , 34: l10^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.16/24.89 , 35: m5^#(a, b, res, t) -> c_25() 96.16/24.89 , 36: e1^#(a, b, res, t) -> 96.16/24.89 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.16/24.89 , 37: m4^#(S(x'), S(x), res, t) -> 96.16/24.89 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.16/24.89 , 38: equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.16/24.89 , 39: l12^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.89 , 40: e8^#(a, b, res, t) -> c_30() 96.16/24.89 , 41: l11^#(x, y, res, tmp, mtmp, True()) -> 96.16/24.89 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.16/24.89 , 42: l11^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , 43: e5^#(a, b, res, t) -> c_34() 96.16/24.89 , 44: l3^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.16/24.89 , 45: l4^#(x', x, res, tmp, mtmp, t) -> 96.16/24.89 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.16/24.89 , 46: m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.16/24.89 , 47: m2^#(S(S(x)), b, res, True()) -> c_37() 96.16/24.89 , 48: m2^#(S(0()), b, res, True()) -> c_38() 96.16/24.89 , 49: m2^#(0(), b, res, True()) -> c_39() 96.16/24.89 , 50: m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) 96.16/24.89 , 51: <^#(x, 0()) -> c_51() 96.16/24.89 , 52: <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.16/24.89 , 53: <^#(0(), S(y)) -> c_53() } 96.16/24.89 96.16/24.89 We are left with following problem, upon which TcT provides the 96.16/24.89 certificate YES(O(1),O(n^1)). 96.16/24.89 96.16/24.89 Strict DPs: 96.16/24.89 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , l7^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.16/24.89 , l1^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , l13^#(x, y, res, tmp, True(), t) -> 96.16/24.89 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.16/24.89 , l13^#(x, y, res, tmp, False(), t) -> 96.16/24.89 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.16/24.89 , gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.16/24.89 , e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.16/24.89 , e3^#(a, b, res, t) -> 96.16/24.89 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.16/24.89 , l14^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.89 , l15^#(x, y, res, tmp, True(), t) -> 96.16/24.89 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.16/24.89 , l15^#(x, y, res, tmp, False(), t) -> 96.16/24.89 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.16/24.89 , monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.16/24.89 , l8^#(x, y, res, False(), mtmp, t) -> 96.16/24.89 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.16/24.89 , l10^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.16/24.89 , e1^#(a, b, res, t) -> 96.16/24.89 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.16/24.89 , m4^#(S(x'), S(x), res, t) -> 96.16/24.89 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.16/24.89 , equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.16/24.89 , l12^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.89 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.16/24.89 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.16/24.89 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , l3^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.16/24.89 , l4^#(x', x, res, tmp, mtmp, t) -> 96.16/24.89 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.16/24.89 , m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.16/24.89 , m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) } 96.16/24.89 Weak DPs: 96.16/24.89 { l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.16/24.89 , l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.16/24.89 , l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.16/24.89 , help1^#(S(S(x))) -> c_6() 96.16/24.89 , help1^#(S(0())) -> c_7() 96.16/24.89 , help1^#(0()) -> c_8() 96.16/24.89 , e7^#(a, b, res, t) -> c_10() 96.16/24.89 , m3^#(S(S(x)), b, res, t) -> c_11() 96.16/24.89 , m3^#(S(0()), b, res, t) -> c_12() 96.16/24.89 , m3^#(0(), b, res, t) -> c_13() 96.16/24.89 , e2^#(a, b, res, False()) -> c_15() 96.16/24.89 , e4^#(a, b, res, True()) -> c_49() 96.16/24.89 , e4^#(a, b, res, False()) -> c_50() 96.16/24.89 , <^#(x, 0()) -> c_51() 96.16/24.89 , <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.16/24.89 , <^#(0(), S(y)) -> c_53() 96.16/24.89 , e6^#(a, b, res, t) -> c_17() 96.16/24.89 , l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.16/24.89 , bool2Nat^#(True()) -> c_20() 96.16/24.89 , bool2Nat^#(False()) -> c_21() 96.16/24.89 , l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.16/24.89 , l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.16/24.89 , m5^#(a, b, res, t) -> c_25() 96.16/24.89 , e8^#(a, b, res, t) -> c_30() 96.16/24.89 , e5^#(a, b, res, t) -> c_34() 96.16/24.89 , m2^#(S(S(x)), b, res, True()) -> c_37() 96.16/24.89 , m2^#(S(0()), b, res, True()) -> c_38() 96.16/24.89 , m2^#(0(), b, res, True()) -> c_39() } 96.16/24.89 Weak Trs: 96.16/24.89 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.16/24.89 , l5(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 l7(x, y, res, tmp, mtmp, False()) 96.16/24.89 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.16/24.89 , l13(x, y, res, tmp, True(), t) -> 96.16/24.89 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.16/24.89 , l13(x, y, res, tmp, False(), t) -> 96.16/24.89 l16(x, y, gcd(0(), y), tmp, False(), t) 96.16/24.89 , help1(S(S(x))) -> True() 96.16/24.89 , help1(S(0())) -> False() 96.16/24.89 , help1(0()) -> False() 96.16/24.89 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.16/24.89 , e7(a, b, res, t) -> False() 96.16/24.89 , m3(S(S(x)), b, res, t) -> True() 96.16/24.89 , m3(S(0()), b, res, t) -> False() 96.16/24.89 , m3(0(), b, res, t) -> False() 96.16/24.89 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.16/24.89 , e2(a, b, res, False()) -> False() 96.16/24.89 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.16/24.89 , e6(a, b, res, t) -> False() 96.16/24.89 , l14(x, y, res, tmp, mtmp, t) -> 96.16/24.89 l15(x, y, res, tmp, monus(x, y), t) 96.16/24.89 , l9(res, y, res', tmp, mtmp, t) -> res 96.16/24.89 , bool2Nat(True()) -> S(0()) 96.16/24.89 , bool2Nat(False()) -> 0() 96.16/24.89 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.16/24.89 , l8(res, y, res', True(), mtmp, t) -> res 96.16/24.89 , l8(x, y, res, False(), mtmp, t) -> 96.16/24.89 l10(x, y, res, False(), mtmp, t) 96.16/24.89 , m5(a, b, res, t) -> res 96.16/24.89 , <(x, 0()) -> False() 96.16/24.89 , <(S(x), S(y)) -> <(x, y) 96.16/24.89 , <(0(), S(y)) -> True() 96.16/24.89 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.16/24.89 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.16/24.89 , equal0(a, b) -> e1(a, b, False(), False()) 96.16/24.89 , l12(x, y, res, tmp, mtmp, t) -> 96.16/24.89 l13(x, y, res, tmp, monus(x, y), t) 96.16/24.89 , e8(a, b, res, t) -> res 96.16/24.89 , l7(x, y, res, tmp, mtmp, t) -> 96.16/24.89 l8(x, y, res, equal0(x, y), mtmp, t) 96.16/24.89 , l11(x, y, res, tmp, mtmp, True()) -> 96.16/24.89 l12(x, y, res, tmp, mtmp, True()) 96.16/24.89 , l11(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 l14(x, y, res, tmp, mtmp, False()) 96.16/24.89 , e5(a, b, res, t) -> True() 96.16/24.89 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.16/24.89 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.16/24.89 , m2(S(S(x)), b, res, True()) -> True() 96.16/24.89 , m2(S(0()), b, res, True()) -> False() 96.16/24.89 , m2(0(), b, res, True()) -> False() 96.16/24.89 , monus(a, b) -> m1(a, b, False(), False()) 96.16/24.89 , l2(x, y, res, tmp, mtmp, True()) -> res 96.16/24.89 , l2(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 l3(x, y, res, tmp, mtmp, False()) 96.16/24.89 , l4(x', x, res, tmp, mtmp, t) -> 96.16/24.89 l5(x', x, res, tmp, mtmp, False()) 96.16/24.89 , l10(x, y, res, tmp, mtmp, t) -> 96.16/24.89 l11(x, y, res, tmp, mtmp, <(x, y)) 96.16/24.89 , l15(x, y, res, tmp, True(), t) -> 96.16/24.89 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.16/24.89 , l15(x, y, res, tmp, False(), t) -> 96.16/24.89 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.16/24.89 , l16(x, y, res, tmp, mtmp, t) -> res 96.16/24.89 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.16/24.89 , e4(a, b, res, True()) -> True() 96.16/24.89 , e4(a, b, res, False()) -> False() } 96.16/24.89 Obligation: 96.16/24.89 innermost runtime complexity 96.16/24.89 Answer: 96.16/24.89 YES(O(1),O(n^1)) 96.16/24.89 96.16/24.89 We estimate the number of application of {9} by applications of 96.16/24.89 Pre({9}) = {8}. Here rules are labeled as follows: 96.16/24.89 96.16/24.89 DPs: 96.16/24.89 { 1: l5^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , 2: l7^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.16/24.89 , 3: l1^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , 4: l2^#(x, y, res, tmp, mtmp, False()) -> 96.16/24.89 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.16/24.89 , 5: l13^#(x, y, res, tmp, True(), t) -> 96.16/24.89 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.16/24.89 , 6: l13^#(x, y, res, tmp, False(), t) -> 96.16/24.89 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.16/24.89 , 7: gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.16/24.89 , 8: e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.16/24.89 , 9: e3^#(a, b, res, t) -> 96.16/24.89 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.16/24.89 , 10: l14^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.16/24.89 , 11: l15^#(x, y, res, tmp, True(), t) -> 96.16/24.89 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.16/24.89 , 12: l15^#(x, y, res, tmp, False(), t) -> 96.16/24.89 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.16/24.89 , 13: monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.16/24.89 , 14: l8^#(x, y, res, False(), mtmp, t) -> 96.16/24.89 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.16/24.89 , 15: l10^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.16/24.89 , 16: e1^#(a, b, res, t) -> 96.16/24.89 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.16/24.89 , 17: m4^#(S(x'), S(x), res, t) -> 96.16/24.89 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.16/24.89 , 18: equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.16/24.89 , 19: l12^#(x, y, res, tmp, mtmp, t) -> 96.16/24.89 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.90 , 20: l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.90 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.90 , 21: l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , 22: l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.90 , 23: l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.90 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.90 , 24: m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.90 , 25: m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) 96.44/24.90 , 26: l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.90 , 27: l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.90 , 28: l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.90 , 29: help1^#(S(S(x))) -> c_6() 96.44/24.90 , 30: help1^#(S(0())) -> c_7() 96.44/24.90 , 31: help1^#(0()) -> c_8() 96.44/24.90 , 32: e7^#(a, b, res, t) -> c_10() 96.44/24.90 , 33: m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.90 , 34: m3^#(S(0()), b, res, t) -> c_12() 96.44/24.90 , 35: m3^#(0(), b, res, t) -> c_13() 96.44/24.90 , 36: e2^#(a, b, res, False()) -> c_15() 96.44/24.90 , 37: e4^#(a, b, res, True()) -> c_49() 96.44/24.90 , 38: e4^#(a, b, res, False()) -> c_50() 96.44/24.90 , 39: <^#(x, 0()) -> c_51() 96.44/24.90 , 40: <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.90 , 41: <^#(0(), S(y)) -> c_53() 96.44/24.90 , 42: e6^#(a, b, res, t) -> c_17() 96.44/24.90 , 43: l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.90 , 44: bool2Nat^#(True()) -> c_20() 96.44/24.90 , 45: bool2Nat^#(False()) -> c_21() 96.44/24.90 , 46: l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.90 , 47: l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.90 , 48: m5^#(a, b, res, t) -> c_25() 96.44/24.90 , 49: e8^#(a, b, res, t) -> c_30() 96.44/24.90 , 50: e5^#(a, b, res, t) -> c_34() 96.44/24.90 , 51: m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.90 , 52: m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.90 , 53: m2^#(0(), b, res, True()) -> c_39() } 96.44/24.90 96.44/24.90 We are left with following problem, upon which TcT provides the 96.44/24.90 certificate YES(O(1),O(n^1)). 96.44/24.90 96.44/24.90 Strict DPs: 96.44/24.90 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.90 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , l13^#(x, y, res, tmp, True(), t) -> 96.44/24.90 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.90 , l13^#(x, y, res, tmp, False(), t) -> 96.44/24.90 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.90 , gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.90 , e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.44/24.90 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.90 , l15^#(x, y, res, tmp, True(), t) -> 96.44/24.90 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.90 , l15^#(x, y, res, tmp, False(), t) -> 96.44/24.90 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.90 , monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.44/24.90 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.90 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.90 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.90 , e1^#(a, b, res, t) -> 96.44/24.90 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.44/24.90 , m4^#(S(x'), S(x), res, t) -> 96.44/24.90 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.44/24.90 , equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.44/24.90 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.90 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.90 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.90 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.90 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.90 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.90 , m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.90 , m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) } 96.44/24.90 Weak DPs: 96.44/24.90 { l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.90 , l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.90 , l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.90 , help1^#(S(S(x))) -> c_6() 96.44/24.90 , help1^#(S(0())) -> c_7() 96.44/24.90 , help1^#(0()) -> c_8() 96.44/24.90 , e7^#(a, b, res, t) -> c_10() 96.44/24.90 , m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.90 , m3^#(S(0()), b, res, t) -> c_12() 96.44/24.90 , m3^#(0(), b, res, t) -> c_13() 96.44/24.90 , e2^#(a, b, res, False()) -> c_15() 96.44/24.90 , e3^#(a, b, res, t) -> 96.44/24.90 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.44/24.90 , e4^#(a, b, res, True()) -> c_49() 96.44/24.90 , e4^#(a, b, res, False()) -> c_50() 96.44/24.90 , <^#(x, 0()) -> c_51() 96.44/24.90 , <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.90 , <^#(0(), S(y)) -> c_53() 96.44/24.90 , e6^#(a, b, res, t) -> c_17() 96.44/24.90 , l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.90 , bool2Nat^#(True()) -> c_20() 96.44/24.90 , bool2Nat^#(False()) -> c_21() 96.44/24.90 , l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.90 , l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.90 , m5^#(a, b, res, t) -> c_25() 96.44/24.90 , e8^#(a, b, res, t) -> c_30() 96.44/24.90 , e5^#(a, b, res, t) -> c_34() 96.44/24.90 , m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.90 , m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.90 , m2^#(0(), b, res, True()) -> c_39() } 96.44/24.90 Weak Trs: 96.44/24.90 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.44/24.90 , l5(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 l7(x, y, res, tmp, mtmp, False()) 96.44/24.90 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.44/24.90 , l13(x, y, res, tmp, True(), t) -> 96.44/24.90 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.44/24.90 , l13(x, y, res, tmp, False(), t) -> 96.44/24.90 l16(x, y, gcd(0(), y), tmp, False(), t) 96.44/24.90 , help1(S(S(x))) -> True() 96.44/24.90 , help1(S(0())) -> False() 96.44/24.90 , help1(0()) -> False() 96.44/24.90 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.44/24.90 , e7(a, b, res, t) -> False() 96.44/24.90 , m3(S(S(x)), b, res, t) -> True() 96.44/24.90 , m3(S(0()), b, res, t) -> False() 96.44/24.90 , m3(0(), b, res, t) -> False() 96.44/24.90 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.90 , e2(a, b, res, False()) -> False() 96.44/24.90 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.90 , e6(a, b, res, t) -> False() 96.44/24.90 , l14(x, y, res, tmp, mtmp, t) -> 96.44/24.90 l15(x, y, res, tmp, monus(x, y), t) 96.44/24.90 , l9(res, y, res', tmp, mtmp, t) -> res 96.44/24.90 , bool2Nat(True()) -> S(0()) 96.44/24.90 , bool2Nat(False()) -> 0() 96.44/24.90 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.44/24.90 , l8(res, y, res', True(), mtmp, t) -> res 96.44/24.90 , l8(x, y, res, False(), mtmp, t) -> 96.44/24.90 l10(x, y, res, False(), mtmp, t) 96.44/24.90 , m5(a, b, res, t) -> res 96.44/24.90 , <(x, 0()) -> False() 96.44/24.90 , <(S(x), S(y)) -> <(x, y) 96.44/24.90 , <(0(), S(y)) -> True() 96.44/24.90 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.90 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.90 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.90 , l12(x, y, res, tmp, mtmp, t) -> 96.44/24.90 l13(x, y, res, tmp, monus(x, y), t) 96.44/24.90 , e8(a, b, res, t) -> res 96.44/24.90 , l7(x, y, res, tmp, mtmp, t) -> 96.44/24.90 l8(x, y, res, equal0(x, y), mtmp, t) 96.44/24.90 , l11(x, y, res, tmp, mtmp, True()) -> 96.44/24.90 l12(x, y, res, tmp, mtmp, True()) 96.44/24.90 , l11(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 l14(x, y, res, tmp, mtmp, False()) 96.44/24.90 , e5(a, b, res, t) -> True() 96.44/24.90 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.44/24.90 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.90 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.90 , m2(S(0()), b, res, True()) -> False() 96.44/24.90 , m2(0(), b, res, True()) -> False() 96.44/24.90 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.90 , l2(x, y, res, tmp, mtmp, True()) -> res 96.44/24.90 , l2(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 l3(x, y, res, tmp, mtmp, False()) 96.44/24.90 , l4(x', x, res, tmp, mtmp, t) -> 96.44/24.90 l5(x', x, res, tmp, mtmp, False()) 96.44/24.90 , l10(x, y, res, tmp, mtmp, t) -> 96.44/24.90 l11(x, y, res, tmp, mtmp, <(x, y)) 96.44/24.90 , l15(x, y, res, tmp, True(), t) -> 96.44/24.90 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.44/24.90 , l15(x, y, res, tmp, False(), t) -> 96.44/24.90 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.44/24.90 , l16(x, y, res, tmp, mtmp, t) -> res 96.44/24.90 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.90 , e4(a, b, res, True()) -> True() 96.44/24.90 , e4(a, b, res, False()) -> False() } 96.44/24.90 Obligation: 96.44/24.90 innermost runtime complexity 96.44/24.90 Answer: 96.44/24.90 YES(O(1),O(n^1)) 96.44/24.90 96.44/24.90 We estimate the number of application of {8} by applications of 96.44/24.90 Pre({8}) = {15}. Here rules are labeled as follows: 96.44/24.90 96.44/24.90 DPs: 96.44/24.90 { 1: l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , 2: l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.90 , 3: l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , 4: l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , 5: l13^#(x, y, res, tmp, True(), t) -> 96.44/24.90 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.90 , 6: l13^#(x, y, res, tmp, False(), t) -> 96.44/24.90 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.90 , 7: gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.90 , 8: e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.44/24.90 , 9: l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.90 , 10: l15^#(x, y, res, tmp, True(), t) -> 96.44/24.90 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.90 , 11: l15^#(x, y, res, tmp, False(), t) -> 96.44/24.90 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.90 , 12: monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.44/24.90 , 13: l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.90 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.90 , 14: l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.90 , 15: e1^#(a, b, res, t) -> 96.44/24.90 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.44/24.90 , 16: m4^#(S(x'), S(x), res, t) -> 96.44/24.90 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.44/24.90 , 17: equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.44/24.90 , 18: l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.90 , 19: l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.90 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.90 , 20: l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , 21: l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.90 , 22: l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.90 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.90 , 23: m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.90 , 24: m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) 96.44/24.90 , 25: l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.90 , 26: l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.90 , 27: l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.90 , 28: help1^#(S(S(x))) -> c_6() 96.44/24.90 , 29: help1^#(S(0())) -> c_7() 96.44/24.90 , 30: help1^#(0()) -> c_8() 96.44/24.90 , 31: e7^#(a, b, res, t) -> c_10() 96.44/24.90 , 32: m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.90 , 33: m3^#(S(0()), b, res, t) -> c_12() 96.44/24.90 , 34: m3^#(0(), b, res, t) -> c_13() 96.44/24.90 , 35: e2^#(a, b, res, False()) -> c_15() 96.44/24.90 , 36: e3^#(a, b, res, t) -> 96.44/24.90 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.44/24.90 , 37: e4^#(a, b, res, True()) -> c_49() 96.44/24.90 , 38: e4^#(a, b, res, False()) -> c_50() 96.44/24.90 , 39: <^#(x, 0()) -> c_51() 96.44/24.90 , 40: <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.90 , 41: <^#(0(), S(y)) -> c_53() 96.44/24.90 , 42: e6^#(a, b, res, t) -> c_17() 96.44/24.90 , 43: l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.90 , 44: bool2Nat^#(True()) -> c_20() 96.44/24.90 , 45: bool2Nat^#(False()) -> c_21() 96.44/24.90 , 46: l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.90 , 47: l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.90 , 48: m5^#(a, b, res, t) -> c_25() 96.44/24.90 , 49: e8^#(a, b, res, t) -> c_30() 96.44/24.90 , 50: e5^#(a, b, res, t) -> c_34() 96.44/24.90 , 51: m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.90 , 52: m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.90 , 53: m2^#(0(), b, res, True()) -> c_39() } 96.44/24.90 96.44/24.90 We are left with following problem, upon which TcT provides the 96.44/24.90 certificate YES(O(1),O(n^1)). 96.44/24.90 96.44/24.90 Strict DPs: 96.44/24.90 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.90 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , l13^#(x, y, res, tmp, True(), t) -> 96.44/24.90 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.90 , l13^#(x, y, res, tmp, False(), t) -> 96.44/24.90 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.90 , gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.90 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.90 , l15^#(x, y, res, tmp, True(), t) -> 96.44/24.90 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.90 , l15^#(x, y, res, tmp, False(), t) -> 96.44/24.90 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.90 , monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.44/24.90 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.90 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.90 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.90 , e1^#(a, b, res, t) -> 96.44/24.90 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.44/24.90 , m4^#(S(x'), S(x), res, t) -> 96.44/24.90 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.44/24.90 , equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.44/24.90 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.90 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.90 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.90 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.90 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.90 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.90 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.90 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.90 , m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.90 , m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) } 96.44/24.90 Weak DPs: 96.44/24.90 { l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.90 , l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.90 , l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.90 , help1^#(S(S(x))) -> c_6() 96.44/24.90 , help1^#(S(0())) -> c_7() 96.44/24.90 , help1^#(0()) -> c_8() 96.44/24.90 , e7^#(a, b, res, t) -> c_10() 96.44/24.90 , m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.90 , m3^#(S(0()), b, res, t) -> c_12() 96.44/24.90 , m3^#(0(), b, res, t) -> c_13() 96.44/24.90 , e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.44/24.90 , e2^#(a, b, res, False()) -> c_15() 96.44/24.90 , e3^#(a, b, res, t) -> 96.44/24.90 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.44/24.90 , e4^#(a, b, res, True()) -> c_49() 96.44/24.90 , e4^#(a, b, res, False()) -> c_50() 96.44/24.90 , <^#(x, 0()) -> c_51() 96.44/24.90 , <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.90 , <^#(0(), S(y)) -> c_53() 96.44/24.90 , e6^#(a, b, res, t) -> c_17() 96.44/24.90 , l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.90 , bool2Nat^#(True()) -> c_20() 96.44/24.90 , bool2Nat^#(False()) -> c_21() 96.44/24.90 , l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.90 , l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.90 , m5^#(a, b, res, t) -> c_25() 96.44/24.90 , e8^#(a, b, res, t) -> c_30() 96.44/24.90 , e5^#(a, b, res, t) -> c_34() 96.44/24.90 , m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.90 , m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.90 , m2^#(0(), b, res, True()) -> c_39() } 96.44/24.90 Weak Trs: 96.44/24.90 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.44/24.90 , l5(x, y, res, tmp, mtmp, False()) -> 96.44/24.90 l7(x, y, res, tmp, mtmp, False()) 96.44/24.90 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.44/24.90 , l13(x, y, res, tmp, True(), t) -> 96.44/24.90 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.44/24.90 , l13(x, y, res, tmp, False(), t) -> 96.44/24.90 l16(x, y, gcd(0(), y), tmp, False(), t) 96.44/24.90 , help1(S(S(x))) -> True() 96.44/24.90 , help1(S(0())) -> False() 96.44/24.90 , help1(0()) -> False() 96.44/24.90 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.44/24.90 , e7(a, b, res, t) -> False() 96.44/24.90 , m3(S(S(x)), b, res, t) -> True() 96.44/24.90 , m3(S(0()), b, res, t) -> False() 96.44/24.90 , m3(0(), b, res, t) -> False() 96.44/24.90 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.90 , e2(a, b, res, False()) -> False() 96.44/24.90 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.90 , e6(a, b, res, t) -> False() 96.44/24.90 , l14(x, y, res, tmp, mtmp, t) -> 96.44/24.90 l15(x, y, res, tmp, monus(x, y), t) 96.44/24.90 , l9(res, y, res', tmp, mtmp, t) -> res 96.44/24.90 , bool2Nat(True()) -> S(0()) 96.44/24.90 , bool2Nat(False()) -> 0() 96.44/24.90 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.44/24.90 , l8(res, y, res', True(), mtmp, t) -> res 96.44/24.90 , l8(x, y, res, False(), mtmp, t) -> 96.44/24.90 l10(x, y, res, False(), mtmp, t) 96.44/24.90 , m5(a, b, res, t) -> res 96.44/24.90 , <(x, 0()) -> False() 96.44/24.90 , <(S(x), S(y)) -> <(x, y) 96.44/24.91 , <(0(), S(y)) -> True() 96.44/24.91 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.91 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.91 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.91 , l12(x, y, res, tmp, mtmp, t) -> 96.44/24.91 l13(x, y, res, tmp, monus(x, y), t) 96.44/24.91 , e8(a, b, res, t) -> res 96.44/24.91 , l7(x, y, res, tmp, mtmp, t) -> 96.44/24.91 l8(x, y, res, equal0(x, y), mtmp, t) 96.44/24.91 , l11(x, y, res, tmp, mtmp, True()) -> 96.44/24.91 l12(x, y, res, tmp, mtmp, True()) 96.44/24.91 , l11(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 l14(x, y, res, tmp, mtmp, False()) 96.44/24.91 , e5(a, b, res, t) -> True() 96.44/24.91 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.44/24.91 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.91 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.91 , m2(S(0()), b, res, True()) -> False() 96.44/24.91 , m2(0(), b, res, True()) -> False() 96.44/24.91 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.91 , l2(x, y, res, tmp, mtmp, True()) -> res 96.44/24.91 , l2(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 l3(x, y, res, tmp, mtmp, False()) 96.44/24.91 , l4(x', x, res, tmp, mtmp, t) -> 96.44/24.91 l5(x', x, res, tmp, mtmp, False()) 96.44/24.91 , l10(x, y, res, tmp, mtmp, t) -> 96.44/24.91 l11(x, y, res, tmp, mtmp, <(x, y)) 96.44/24.91 , l15(x, y, res, tmp, True(), t) -> 96.44/24.91 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.44/24.91 , l15(x, y, res, tmp, False(), t) -> 96.44/24.91 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.44/24.91 , l16(x, y, res, tmp, mtmp, t) -> res 96.44/24.91 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.91 , e4(a, b, res, True()) -> True() 96.44/24.91 , e4(a, b, res, False()) -> False() } 96.44/24.91 Obligation: 96.44/24.91 innermost runtime complexity 96.44/24.91 Answer: 96.44/24.91 YES(O(1),O(n^1)) 96.44/24.91 96.44/24.91 We estimate the number of application of {14} by applications of 96.44/24.91 Pre({14}) = {16}. Here rules are labeled as follows: 96.44/24.91 96.44/24.91 DPs: 96.44/24.91 { 1: l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , 2: l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.91 , 3: l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , 4: l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , 5: l13^#(x, y, res, tmp, True(), t) -> 96.44/24.91 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.91 , 6: l13^#(x, y, res, tmp, False(), t) -> 96.44/24.91 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.91 , 7: gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.91 , 8: l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.91 , 9: l15^#(x, y, res, tmp, True(), t) -> 96.44/24.91 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.91 , 10: l15^#(x, y, res, tmp, False(), t) -> 96.44/24.91 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.91 , 11: monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.44/24.91 , 12: l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.91 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.91 , 13: l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.91 , 14: e1^#(a, b, res, t) -> 96.44/24.91 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.44/24.91 , 15: m4^#(S(x'), S(x), res, t) -> 96.44/24.91 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.44/24.91 , 16: equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.44/24.91 , 17: l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.91 , 18: l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.91 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.91 , 19: l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , 20: l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.91 , 21: l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.91 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.91 , 22: m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.91 , 23: m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) 96.44/24.91 , 24: l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.91 , 25: l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.91 , 26: l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.91 , 27: help1^#(S(S(x))) -> c_6() 96.44/24.91 , 28: help1^#(S(0())) -> c_7() 96.44/24.91 , 29: help1^#(0()) -> c_8() 96.44/24.91 , 30: e7^#(a, b, res, t) -> c_10() 96.44/24.91 , 31: m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.91 , 32: m3^#(S(0()), b, res, t) -> c_12() 96.44/24.91 , 33: m3^#(0(), b, res, t) -> c_13() 96.44/24.91 , 34: e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.44/24.91 , 35: e2^#(a, b, res, False()) -> c_15() 96.44/24.91 , 36: e3^#(a, b, res, t) -> 96.44/24.91 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.44/24.91 , 37: e4^#(a, b, res, True()) -> c_49() 96.44/24.91 , 38: e4^#(a, b, res, False()) -> c_50() 96.44/24.91 , 39: <^#(x, 0()) -> c_51() 96.44/24.91 , 40: <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.91 , 41: <^#(0(), S(y)) -> c_53() 96.44/24.91 , 42: e6^#(a, b, res, t) -> c_17() 96.44/24.91 , 43: l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.91 , 44: bool2Nat^#(True()) -> c_20() 96.44/24.91 , 45: bool2Nat^#(False()) -> c_21() 96.44/24.91 , 46: l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.91 , 47: l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.91 , 48: m5^#(a, b, res, t) -> c_25() 96.44/24.91 , 49: e8^#(a, b, res, t) -> c_30() 96.44/24.91 , 50: e5^#(a, b, res, t) -> c_34() 96.44/24.91 , 51: m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.91 , 52: m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.91 , 53: m2^#(0(), b, res, True()) -> c_39() } 96.44/24.91 96.44/24.91 We are left with following problem, upon which TcT provides the 96.44/24.91 certificate YES(O(1),O(n^1)). 96.44/24.91 96.44/24.91 Strict DPs: 96.44/24.91 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.91 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , l13^#(x, y, res, tmp, True(), t) -> 96.44/24.91 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.91 , l13^#(x, y, res, tmp, False(), t) -> 96.44/24.91 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.91 , gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.91 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.91 , l15^#(x, y, res, tmp, True(), t) -> 96.44/24.91 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.91 , l15^#(x, y, res, tmp, False(), t) -> 96.44/24.91 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.91 , monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.44/24.91 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.91 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.91 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.91 , m4^#(S(x'), S(x), res, t) -> 96.44/24.91 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.44/24.91 , equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.44/24.91 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.91 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.91 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.91 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.91 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.91 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.91 , m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.91 , m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) } 96.44/24.91 Weak DPs: 96.44/24.91 { l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.91 , l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.91 , l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.91 , help1^#(S(S(x))) -> c_6() 96.44/24.91 , help1^#(S(0())) -> c_7() 96.44/24.91 , help1^#(0()) -> c_8() 96.44/24.91 , e7^#(a, b, res, t) -> c_10() 96.44/24.91 , m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.91 , m3^#(S(0()), b, res, t) -> c_12() 96.44/24.91 , m3^#(0(), b, res, t) -> c_13() 96.44/24.91 , e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.44/24.91 , e2^#(a, b, res, False()) -> c_15() 96.44/24.91 , e3^#(a, b, res, t) -> 96.44/24.91 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.44/24.91 , e4^#(a, b, res, True()) -> c_49() 96.44/24.91 , e4^#(a, b, res, False()) -> c_50() 96.44/24.91 , <^#(x, 0()) -> c_51() 96.44/24.91 , <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.91 , <^#(0(), S(y)) -> c_53() 96.44/24.91 , e6^#(a, b, res, t) -> c_17() 96.44/24.91 , l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.91 , bool2Nat^#(True()) -> c_20() 96.44/24.91 , bool2Nat^#(False()) -> c_21() 96.44/24.91 , l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.91 , l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.91 , m5^#(a, b, res, t) -> c_25() 96.44/24.91 , e1^#(a, b, res, t) -> 96.44/24.91 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.44/24.91 , e8^#(a, b, res, t) -> c_30() 96.44/24.91 , e5^#(a, b, res, t) -> c_34() 96.44/24.91 , m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.91 , m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.91 , m2^#(0(), b, res, True()) -> c_39() } 96.44/24.91 Weak Trs: 96.44/24.91 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.44/24.91 , l5(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 l7(x, y, res, tmp, mtmp, False()) 96.44/24.91 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.44/24.91 , l13(x, y, res, tmp, True(), t) -> 96.44/24.91 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.44/24.91 , l13(x, y, res, tmp, False(), t) -> 96.44/24.91 l16(x, y, gcd(0(), y), tmp, False(), t) 96.44/24.91 , help1(S(S(x))) -> True() 96.44/24.91 , help1(S(0())) -> False() 96.44/24.91 , help1(0()) -> False() 96.44/24.91 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.44/24.91 , e7(a, b, res, t) -> False() 96.44/24.91 , m3(S(S(x)), b, res, t) -> True() 96.44/24.91 , m3(S(0()), b, res, t) -> False() 96.44/24.91 , m3(0(), b, res, t) -> False() 96.44/24.91 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.91 , e2(a, b, res, False()) -> False() 96.44/24.91 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.91 , e6(a, b, res, t) -> False() 96.44/24.91 , l14(x, y, res, tmp, mtmp, t) -> 96.44/24.91 l15(x, y, res, tmp, monus(x, y), t) 96.44/24.91 , l9(res, y, res', tmp, mtmp, t) -> res 96.44/24.91 , bool2Nat(True()) -> S(0()) 96.44/24.91 , bool2Nat(False()) -> 0() 96.44/24.91 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.44/24.91 , l8(res, y, res', True(), mtmp, t) -> res 96.44/24.91 , l8(x, y, res, False(), mtmp, t) -> 96.44/24.91 l10(x, y, res, False(), mtmp, t) 96.44/24.91 , m5(a, b, res, t) -> res 96.44/24.91 , <(x, 0()) -> False() 96.44/24.91 , <(S(x), S(y)) -> <(x, y) 96.44/24.91 , <(0(), S(y)) -> True() 96.44/24.91 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.91 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.91 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.91 , l12(x, y, res, tmp, mtmp, t) -> 96.44/24.91 l13(x, y, res, tmp, monus(x, y), t) 96.44/24.91 , e8(a, b, res, t) -> res 96.44/24.91 , l7(x, y, res, tmp, mtmp, t) -> 96.44/24.91 l8(x, y, res, equal0(x, y), mtmp, t) 96.44/24.91 , l11(x, y, res, tmp, mtmp, True()) -> 96.44/24.91 l12(x, y, res, tmp, mtmp, True()) 96.44/24.91 , l11(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 l14(x, y, res, tmp, mtmp, False()) 96.44/24.91 , e5(a, b, res, t) -> True() 96.44/24.91 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.44/24.91 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.91 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.91 , m2(S(0()), b, res, True()) -> False() 96.44/24.91 , m2(0(), b, res, True()) -> False() 96.44/24.91 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.91 , l2(x, y, res, tmp, mtmp, True()) -> res 96.44/24.91 , l2(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 l3(x, y, res, tmp, mtmp, False()) 96.44/24.91 , l4(x', x, res, tmp, mtmp, t) -> 96.44/24.91 l5(x', x, res, tmp, mtmp, False()) 96.44/24.91 , l10(x, y, res, tmp, mtmp, t) -> 96.44/24.91 l11(x, y, res, tmp, mtmp, <(x, y)) 96.44/24.91 , l15(x, y, res, tmp, True(), t) -> 96.44/24.91 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.44/24.91 , l15(x, y, res, tmp, False(), t) -> 96.44/24.91 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.44/24.91 , l16(x, y, res, tmp, mtmp, t) -> res 96.44/24.91 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.91 , e4(a, b, res, True()) -> True() 96.44/24.91 , e4(a, b, res, False()) -> False() } 96.44/24.91 Obligation: 96.44/24.91 innermost runtime complexity 96.44/24.91 Answer: 96.44/24.91 YES(O(1),O(n^1)) 96.44/24.91 96.44/24.91 We estimate the number of application of {15} by applications of 96.44/24.91 Pre({15}) = {2}. Here rules are labeled as follows: 96.44/24.91 96.44/24.91 DPs: 96.44/24.91 { 1: l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , 2: l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.91 , 3: l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , 4: l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , 5: l13^#(x, y, res, tmp, True(), t) -> 96.44/24.91 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.91 , 6: l13^#(x, y, res, tmp, False(), t) -> 96.44/24.91 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.91 , 7: gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.91 , 8: l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.91 , 9: l15^#(x, y, res, tmp, True(), t) -> 96.44/24.91 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.91 , 10: l15^#(x, y, res, tmp, False(), t) -> 96.44/24.91 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.91 , 11: monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.44/24.91 , 12: l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.91 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.91 , 13: l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.91 , 14: m4^#(S(x'), S(x), res, t) -> 96.44/24.91 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.44/24.91 , 15: equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.44/24.91 , 16: l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.91 , 17: l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.91 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.91 , 18: l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , 19: l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.91 , 20: l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.91 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.91 , 21: m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.91 , 22: m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) 96.44/24.91 , 23: l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.91 , 24: l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.91 , 25: l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.91 , 26: help1^#(S(S(x))) -> c_6() 96.44/24.91 , 27: help1^#(S(0())) -> c_7() 96.44/24.91 , 28: help1^#(0()) -> c_8() 96.44/24.91 , 29: e7^#(a, b, res, t) -> c_10() 96.44/24.91 , 30: m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.91 , 31: m3^#(S(0()), b, res, t) -> c_12() 96.44/24.91 , 32: m3^#(0(), b, res, t) -> c_13() 96.44/24.91 , 33: e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.44/24.91 , 34: e2^#(a, b, res, False()) -> c_15() 96.44/24.91 , 35: e3^#(a, b, res, t) -> 96.44/24.91 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.44/24.91 , 36: e4^#(a, b, res, True()) -> c_49() 96.44/24.91 , 37: e4^#(a, b, res, False()) -> c_50() 96.44/24.91 , 38: <^#(x, 0()) -> c_51() 96.44/24.91 , 39: <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.91 , 40: <^#(0(), S(y)) -> c_53() 96.44/24.91 , 41: e6^#(a, b, res, t) -> c_17() 96.44/24.91 , 42: l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.91 , 43: bool2Nat^#(True()) -> c_20() 96.44/24.91 , 44: bool2Nat^#(False()) -> c_21() 96.44/24.91 , 45: l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.91 , 46: l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.91 , 47: m5^#(a, b, res, t) -> c_25() 96.44/24.91 , 48: e1^#(a, b, res, t) -> 96.44/24.91 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.44/24.91 , 49: e8^#(a, b, res, t) -> c_30() 96.44/24.91 , 50: e5^#(a, b, res, t) -> c_34() 96.44/24.91 , 51: m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.91 , 52: m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.91 , 53: m2^#(0(), b, res, True()) -> c_39() } 96.44/24.91 96.44/24.91 We are left with following problem, upon which TcT provides the 96.44/24.91 certificate YES(O(1),O(n^1)). 96.44/24.91 96.44/24.91 Strict DPs: 96.44/24.91 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.91 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.91 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.91 , l13^#(x, y, res, tmp, True(), t) -> 96.44/24.91 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.91 , l13^#(x, y, res, tmp, False(), t) -> 96.44/24.91 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.91 , gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.91 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.91 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.91 , l15^#(x, y, res, tmp, True(), t) -> 96.44/24.91 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.91 , l15^#(x, y, res, tmp, False(), t) -> 96.44/24.91 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.92 , monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.44/24.92 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.92 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.92 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.92 , m4^#(S(x'), S(x), res, t) -> 96.44/24.92 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.44/24.92 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.92 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.92 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.92 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.92 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.92 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.92 , m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.92 , m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) } 96.44/24.92 Weak DPs: 96.44/24.92 { l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.92 , l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.92 , l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.92 , help1^#(S(S(x))) -> c_6() 96.44/24.92 , help1^#(S(0())) -> c_7() 96.44/24.92 , help1^#(0()) -> c_8() 96.44/24.92 , e7^#(a, b, res, t) -> c_10() 96.44/24.92 , m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.92 , m3^#(S(0()), b, res, t) -> c_12() 96.44/24.92 , m3^#(0(), b, res, t) -> c_13() 96.44/24.92 , e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.44/24.92 , e2^#(a, b, res, False()) -> c_15() 96.44/24.92 , e3^#(a, b, res, t) -> 96.44/24.92 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.44/24.92 , e4^#(a, b, res, True()) -> c_49() 96.44/24.92 , e4^#(a, b, res, False()) -> c_50() 96.44/24.92 , <^#(x, 0()) -> c_51() 96.44/24.92 , <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.92 , <^#(0(), S(y)) -> c_53() 96.44/24.92 , e6^#(a, b, res, t) -> c_17() 96.44/24.92 , l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.92 , bool2Nat^#(True()) -> c_20() 96.44/24.92 , bool2Nat^#(False()) -> c_21() 96.44/24.92 , l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.92 , l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.92 , m5^#(a, b, res, t) -> c_25() 96.44/24.92 , e1^#(a, b, res, t) -> 96.44/24.92 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.44/24.92 , equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.44/24.92 , e8^#(a, b, res, t) -> c_30() 96.44/24.92 , e5^#(a, b, res, t) -> c_34() 96.44/24.92 , m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.92 , m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.92 , m2^#(0(), b, res, True()) -> c_39() } 96.44/24.92 Weak Trs: 96.44/24.92 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.44/24.92 , l5(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l7(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l13(x, y, res, tmp, True(), t) -> 96.44/24.92 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.44/24.92 , l13(x, y, res, tmp, False(), t) -> 96.44/24.92 l16(x, y, gcd(0(), y), tmp, False(), t) 96.44/24.92 , help1(S(S(x))) -> True() 96.44/24.92 , help1(S(0())) -> False() 96.44/24.92 , help1(0()) -> False() 96.44/24.92 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.44/24.92 , e7(a, b, res, t) -> False() 96.44/24.92 , m3(S(S(x)), b, res, t) -> True() 96.44/24.92 , m3(S(0()), b, res, t) -> False() 96.44/24.92 , m3(0(), b, res, t) -> False() 96.44/24.92 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.92 , e2(a, b, res, False()) -> False() 96.44/24.92 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.92 , e6(a, b, res, t) -> False() 96.44/24.92 , l14(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l15(x, y, res, tmp, monus(x, y), t) 96.44/24.92 , l9(res, y, res', tmp, mtmp, t) -> res 96.44/24.92 , bool2Nat(True()) -> S(0()) 96.44/24.92 , bool2Nat(False()) -> 0() 96.44/24.92 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.44/24.92 , l8(res, y, res', True(), mtmp, t) -> res 96.44/24.92 , l8(x, y, res, False(), mtmp, t) -> 96.44/24.92 l10(x, y, res, False(), mtmp, t) 96.44/24.92 , m5(a, b, res, t) -> res 96.44/24.92 , <(x, 0()) -> False() 96.44/24.92 , <(S(x), S(y)) -> <(x, y) 96.44/24.92 , <(0(), S(y)) -> True() 96.44/24.92 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.92 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.92 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.92 , l12(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l13(x, y, res, tmp, monus(x, y), t) 96.44/24.92 , e8(a, b, res, t) -> res 96.44/24.92 , l7(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l8(x, y, res, equal0(x, y), mtmp, t) 96.44/24.92 , l11(x, y, res, tmp, mtmp, True()) -> 96.44/24.92 l12(x, y, res, tmp, mtmp, True()) 96.44/24.92 , l11(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l14(x, y, res, tmp, mtmp, False()) 96.44/24.92 , e5(a, b, res, t) -> True() 96.44/24.92 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.44/24.92 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.92 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.92 , m2(S(0()), b, res, True()) -> False() 96.44/24.92 , m2(0(), b, res, True()) -> False() 96.44/24.92 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.92 , l2(x, y, res, tmp, mtmp, True()) -> res 96.44/24.92 , l2(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l3(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l4(x', x, res, tmp, mtmp, t) -> 96.44/24.92 l5(x', x, res, tmp, mtmp, False()) 96.44/24.92 , l10(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l11(x, y, res, tmp, mtmp, <(x, y)) 96.44/24.92 , l15(x, y, res, tmp, True(), t) -> 96.44/24.92 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.44/24.92 , l15(x, y, res, tmp, False(), t) -> 96.44/24.92 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.44/24.92 , l16(x, y, res, tmp, mtmp, t) -> res 96.44/24.92 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.92 , e4(a, b, res, True()) -> True() 96.44/24.92 , e4(a, b, res, False()) -> False() } 96.44/24.92 Obligation: 96.44/24.92 innermost runtime complexity 96.44/24.92 Answer: 96.44/24.92 YES(O(1),O(n^1)) 96.44/24.92 96.44/24.92 The following weak DPs constitute a sub-graph of the DG that is 96.44/24.92 closed under successors. The DPs are removed. 96.44/24.92 96.44/24.92 { l5^#(x, y, res, tmp, mtmp, True()) -> c_1() 96.44/24.92 , l2^#(x, y, res, tmp, mtmp, True()) -> c_41() 96.44/24.92 , l16^#(x, y, res, tmp, mtmp, t) -> c_47() 96.44/24.92 , help1^#(S(S(x))) -> c_6() 96.44/24.92 , help1^#(S(0())) -> c_7() 96.44/24.92 , help1^#(0()) -> c_8() 96.44/24.92 , e7^#(a, b, res, t) -> c_10() 96.44/24.92 , m3^#(S(S(x)), b, res, t) -> c_11() 96.44/24.92 , m3^#(S(0()), b, res, t) -> c_12() 96.44/24.92 , m3^#(0(), b, res, t) -> c_13() 96.44/24.92 , e2^#(a, b, res, True()) -> c_14(e3^#(a, b, res, True())) 96.44/24.92 , e2^#(a, b, res, False()) -> c_15() 96.44/24.92 , e3^#(a, b, res, t) -> 96.44/24.92 c_16(e4^#(a, b, res, <(b, a)), <^#(b, a)) 96.44/24.92 , e4^#(a, b, res, True()) -> c_49() 96.44/24.92 , e4^#(a, b, res, False()) -> c_50() 96.44/24.92 , <^#(x, 0()) -> c_51() 96.44/24.92 , <^#(S(x), S(y)) -> c_52(<^#(x, y)) 96.44/24.92 , <^#(0(), S(y)) -> c_53() 96.44/24.92 , e6^#(a, b, res, t) -> c_17() 96.44/24.92 , l9^#(res, y, res', tmp, mtmp, t) -> c_19() 96.44/24.92 , bool2Nat^#(True()) -> c_20() 96.44/24.92 , bool2Nat^#(False()) -> c_21() 96.44/24.92 , l6^#(x, y, res, tmp, mtmp, t) -> c_22() 96.44/24.92 , l8^#(res, y, res', True(), mtmp, t) -> c_23() 96.44/24.92 , m5^#(a, b, res, t) -> c_25() 96.44/24.92 , e1^#(a, b, res, t) -> 96.44/24.92 c_26(e2^#(a, b, res, <(a, b)), <^#(a, b)) 96.44/24.92 , equal0^#(a, b) -> c_28(e1^#(a, b, False(), False())) 96.44/24.92 , e8^#(a, b, res, t) -> c_30() 96.44/24.92 , e5^#(a, b, res, t) -> c_34() 96.44/24.92 , m2^#(S(S(x)), b, res, True()) -> c_37() 96.44/24.92 , m2^#(S(0()), b, res, True()) -> c_38() 96.44/24.92 , m2^#(0(), b, res, True()) -> c_39() } 96.44/24.92 96.44/24.92 We are left with following problem, upon which TcT provides the 96.44/24.92 certificate YES(O(1),O(n^1)). 96.44/24.92 96.44/24.92 Strict DPs: 96.44/24.92 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_2(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.92 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_42(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l13^#(x, y, res, tmp, True(), t) -> 96.44/24.92 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.92 , l13^#(x, y, res, tmp, False(), t) -> 96.44/24.92 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.92 , gcd^#(x, y) -> c_9(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.92 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_18(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.92 , l15^#(x, y, res, tmp, True(), t) -> 96.44/24.92 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.92 , l15^#(x, y, res, tmp, False(), t) -> 96.44/24.92 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.92 , monus^#(a, b) -> c_40(m1^#(a, b, False(), False())) 96.44/24.92 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.92 c_24(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.92 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.92 , m4^#(S(x'), S(x), res, t) -> 96.44/24.92 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) 96.44/24.92 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_29(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.92 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.92 c_32(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.92 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_33(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_35(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.92 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.92 c_43(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.92 , m2^#(a, b, res, False()) -> c_36(m4^#(a, b, res, False())) 96.44/24.92 , m1^#(a, x, res, t) -> c_48(m2^#(a, x, res, False())) } 96.44/24.92 Weak Trs: 96.44/24.92 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.44/24.92 , l5(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l7(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l13(x, y, res, tmp, True(), t) -> 96.44/24.92 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.44/24.92 , l13(x, y, res, tmp, False(), t) -> 96.44/24.92 l16(x, y, gcd(0(), y), tmp, False(), t) 96.44/24.92 , help1(S(S(x))) -> True() 96.44/24.92 , help1(S(0())) -> False() 96.44/24.92 , help1(0()) -> False() 96.44/24.92 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.44/24.92 , e7(a, b, res, t) -> False() 96.44/24.92 , m3(S(S(x)), b, res, t) -> True() 96.44/24.92 , m3(S(0()), b, res, t) -> False() 96.44/24.92 , m3(0(), b, res, t) -> False() 96.44/24.92 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.92 , e2(a, b, res, False()) -> False() 96.44/24.92 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.92 , e6(a, b, res, t) -> False() 96.44/24.92 , l14(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l15(x, y, res, tmp, monus(x, y), t) 96.44/24.92 , l9(res, y, res', tmp, mtmp, t) -> res 96.44/24.92 , bool2Nat(True()) -> S(0()) 96.44/24.92 , bool2Nat(False()) -> 0() 96.44/24.92 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.44/24.92 , l8(res, y, res', True(), mtmp, t) -> res 96.44/24.92 , l8(x, y, res, False(), mtmp, t) -> 96.44/24.92 l10(x, y, res, False(), mtmp, t) 96.44/24.92 , m5(a, b, res, t) -> res 96.44/24.92 , <(x, 0()) -> False() 96.44/24.92 , <(S(x), S(y)) -> <(x, y) 96.44/24.92 , <(0(), S(y)) -> True() 96.44/24.92 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.92 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.92 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.92 , l12(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l13(x, y, res, tmp, monus(x, y), t) 96.44/24.92 , e8(a, b, res, t) -> res 96.44/24.92 , l7(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l8(x, y, res, equal0(x, y), mtmp, t) 96.44/24.92 , l11(x, y, res, tmp, mtmp, True()) -> 96.44/24.92 l12(x, y, res, tmp, mtmp, True()) 96.44/24.92 , l11(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l14(x, y, res, tmp, mtmp, False()) 96.44/24.92 , e5(a, b, res, t) -> True() 96.44/24.92 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.44/24.92 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.92 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.92 , m2(S(0()), b, res, True()) -> False() 96.44/24.92 , m2(0(), b, res, True()) -> False() 96.44/24.92 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.92 , l2(x, y, res, tmp, mtmp, True()) -> res 96.44/24.92 , l2(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l3(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l4(x', x, res, tmp, mtmp, t) -> 96.44/24.92 l5(x', x, res, tmp, mtmp, False()) 96.44/24.92 , l10(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l11(x, y, res, tmp, mtmp, <(x, y)) 96.44/24.92 , l15(x, y, res, tmp, True(), t) -> 96.44/24.92 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.44/24.92 , l15(x, y, res, tmp, False(), t) -> 96.44/24.92 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.44/24.92 , l16(x, y, res, tmp, mtmp, t) -> res 96.44/24.92 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.92 , e4(a, b, res, True()) -> True() 96.44/24.92 , e4(a, b, res, False()) -> False() } 96.44/24.92 Obligation: 96.44/24.92 innermost runtime complexity 96.44/24.92 Answer: 96.44/24.92 YES(O(1),O(n^1)) 96.44/24.92 96.44/24.92 Due to missing edges in the dependency-graph, the right-hand sides 96.44/24.92 of following rules could be simplified: 96.44/24.92 96.44/24.92 { l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_31(l8^#(x, y, res, equal0(x, y), mtmp, t), equal0^#(x, y)) 96.44/24.92 , l13^#(x, y, res, tmp, True(), t) -> 96.44/24.92 c_4(l16^#(x, y, gcd(S(0()), y), tmp, True(), t), gcd^#(S(0()), y)) 96.44/24.92 , l13^#(x, y, res, tmp, False(), t) -> 96.44/24.92 c_5(l16^#(x, y, gcd(0(), y), tmp, False(), t), gcd^#(0(), y)) 96.44/24.92 , l15^#(x, y, res, tmp, True(), t) -> 96.44/24.92 c_45(l16^#(x, y, gcd(y, S(0())), tmp, True(), t), gcd^#(y, S(0()))) 96.44/24.92 , l15^#(x, y, res, tmp, False(), t) -> 96.44/24.92 c_46(l16^#(x, y, gcd(y, 0()), tmp, False(), t), gcd^#(y, 0())) 96.44/24.92 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_44(l11^#(x, y, res, tmp, mtmp, <(x, y)), <^#(x, y)) 96.44/24.92 , m4^#(S(x'), S(x), res, t) -> 96.44/24.92 c_27(m5^#(S(x'), S(x), monus(x', x), t), monus^#(x', x)) } 96.44/24.92 96.44/24.92 We are left with following problem, upon which TcT provides the 96.44/24.92 certificate YES(O(1),O(n^1)). 96.44/24.92 96.44/24.92 Strict DPs: 96.44/24.92 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_1(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_2(l8^#(x, y, res, equal0(x, y), mtmp, t)) 96.44/24.92 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_4(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l13^#(x, y, res, tmp, True(), t) -> c_5(gcd^#(S(0()), y)) 96.44/24.92 , l13^#(x, y, res, tmp, False(), t) -> c_6(gcd^#(0(), y)) 96.44/24.92 , gcd^#(x, y) -> c_7(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.92 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_8(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.92 , l15^#(x, y, res, tmp, True(), t) -> c_9(gcd^#(y, S(0()))) 96.44/24.92 , l15^#(x, y, res, tmp, False(), t) -> c_10(gcd^#(y, 0())) 96.44/24.92 , monus^#(a, b) -> c_11(m1^#(a, b, False(), False())) 96.44/24.92 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.92 c_12(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.92 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_13(l11^#(x, y, res, tmp, mtmp, <(x, y))) 96.44/24.92 , m4^#(S(x'), S(x), res, t) -> c_14(monus^#(x', x)) 96.44/24.92 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_15(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.92 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.92 c_16(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.92 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_17(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_18(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.92 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.92 c_19(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.92 , m2^#(a, b, res, False()) -> c_20(m4^#(a, b, res, False())) 96.44/24.92 , m1^#(a, x, res, t) -> c_21(m2^#(a, x, res, False())) } 96.44/24.92 Weak Trs: 96.44/24.92 { l5(x, y, res, tmp, mtmp, True()) -> 0() 96.44/24.92 , l5(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l7(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l1(x, y, res, tmp, mtmp, t) -> l2(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l13(x, y, res, tmp, True(), t) -> 96.44/24.92 l16(x, y, gcd(S(0()), y), tmp, True(), t) 96.44/24.92 , l13(x, y, res, tmp, False(), t) -> 96.44/24.92 l16(x, y, gcd(0(), y), tmp, False(), t) 96.44/24.92 , help1(S(S(x))) -> True() 96.44/24.92 , help1(S(0())) -> False() 96.44/24.92 , help1(0()) -> False() 96.44/24.92 , gcd(x, y) -> l1(x, y, 0(), False(), False(), False()) 96.44/24.92 , e7(a, b, res, t) -> False() 96.44/24.92 , m3(S(S(x)), b, res, t) -> True() 96.44/24.92 , m3(S(0()), b, res, t) -> False() 96.44/24.92 , m3(0(), b, res, t) -> False() 96.44/24.92 , e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.92 , e2(a, b, res, False()) -> False() 96.44/24.92 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.92 , e6(a, b, res, t) -> False() 96.44/24.92 , l14(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l15(x, y, res, tmp, monus(x, y), t) 96.44/24.92 , l9(res, y, res', tmp, mtmp, t) -> res 96.44/24.92 , bool2Nat(True()) -> S(0()) 96.44/24.92 , bool2Nat(False()) -> 0() 96.44/24.92 , l6(x, y, res, tmp, mtmp, t) -> 0() 96.44/24.92 , l8(res, y, res', True(), mtmp, t) -> res 96.44/24.92 , l8(x, y, res, False(), mtmp, t) -> 96.44/24.92 l10(x, y, res, False(), mtmp, t) 96.44/24.92 , m5(a, b, res, t) -> res 96.44/24.92 , <(x, 0()) -> False() 96.44/24.92 , <(S(x), S(y)) -> <(x, y) 96.44/24.92 , <(0(), S(y)) -> True() 96.44/24.92 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.92 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.92 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.92 , l12(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l13(x, y, res, tmp, monus(x, y), t) 96.44/24.92 , e8(a, b, res, t) -> res 96.44/24.92 , l7(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l8(x, y, res, equal0(x, y), mtmp, t) 96.44/24.92 , l11(x, y, res, tmp, mtmp, True()) -> 96.44/24.92 l12(x, y, res, tmp, mtmp, True()) 96.44/24.92 , l11(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l14(x, y, res, tmp, mtmp, False()) 96.44/24.92 , e5(a, b, res, t) -> True() 96.44/24.92 , l3(x, y, res, tmp, mtmp, t) -> l4(x, y, 0(), tmp, mtmp, t) 96.44/24.92 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.92 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.92 , m2(S(0()), b, res, True()) -> False() 96.44/24.92 , m2(0(), b, res, True()) -> False() 96.44/24.92 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.92 , l2(x, y, res, tmp, mtmp, True()) -> res 96.44/24.92 , l2(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 l3(x, y, res, tmp, mtmp, False()) 96.44/24.92 , l4(x', x, res, tmp, mtmp, t) -> 96.44/24.92 l5(x', x, res, tmp, mtmp, False()) 96.44/24.92 , l10(x, y, res, tmp, mtmp, t) -> 96.44/24.92 l11(x, y, res, tmp, mtmp, <(x, y)) 96.44/24.92 , l15(x, y, res, tmp, True(), t) -> 96.44/24.92 l16(x, y, gcd(y, S(0())), tmp, True(), t) 96.44/24.92 , l15(x, y, res, tmp, False(), t) -> 96.44/24.92 l16(x, y, gcd(y, 0()), tmp, False(), t) 96.44/24.92 , l16(x, y, res, tmp, mtmp, t) -> res 96.44/24.92 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.92 , e4(a, b, res, True()) -> True() 96.44/24.92 , e4(a, b, res, False()) -> False() } 96.44/24.92 Obligation: 96.44/24.92 innermost runtime complexity 96.44/24.92 Answer: 96.44/24.92 YES(O(1),O(n^1)) 96.44/24.92 96.44/24.92 We replace rewrite rules by usable rules: 96.44/24.92 96.44/24.92 Weak Usable Rules: 96.44/24.92 { e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.92 , e2(a, b, res, False()) -> False() 96.44/24.92 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.92 , m5(a, b, res, t) -> res 96.44/24.92 , <(x, 0()) -> False() 96.44/24.92 , <(S(x), S(y)) -> <(x, y) 96.44/24.92 , <(0(), S(y)) -> True() 96.44/24.92 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.92 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.92 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.92 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.92 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.92 , m2(S(0()), b, res, True()) -> False() 96.44/24.92 , m2(0(), b, res, True()) -> False() 96.44/24.92 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.92 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.92 , e4(a, b, res, True()) -> True() 96.44/24.92 , e4(a, b, res, False()) -> False() } 96.44/24.92 96.44/24.92 We are left with following problem, upon which TcT provides the 96.44/24.92 certificate YES(O(1),O(n^1)). 96.44/24.92 96.44/24.92 Strict DPs: 96.44/24.92 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_1(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_2(l8^#(x, y, res, equal0(x, y), mtmp, t)) 96.44/24.92 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_4(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l13^#(x, y, res, tmp, True(), t) -> c_5(gcd^#(S(0()), y)) 96.44/24.92 , l13^#(x, y, res, tmp, False(), t) -> c_6(gcd^#(0(), y)) 96.44/24.92 , gcd^#(x, y) -> c_7(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.92 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_8(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.92 , l15^#(x, y, res, tmp, True(), t) -> c_9(gcd^#(y, S(0()))) 96.44/24.92 , l15^#(x, y, res, tmp, False(), t) -> c_10(gcd^#(y, 0())) 96.44/24.92 , monus^#(a, b) -> c_11(m1^#(a, b, False(), False())) 96.44/24.92 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.92 c_12(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.92 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_13(l11^#(x, y, res, tmp, mtmp, <(x, y))) 96.44/24.92 , m4^#(S(x'), S(x), res, t) -> c_14(monus^#(x', x)) 96.44/24.92 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_15(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.92 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.92 c_16(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.92 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.92 c_17(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.92 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.92 c_18(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.92 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.92 c_19(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.92 , m2^#(a, b, res, False()) -> c_20(m4^#(a, b, res, False())) 96.44/24.92 , m1^#(a, x, res, t) -> c_21(m2^#(a, x, res, False())) } 96.44/24.92 Weak Trs: 96.44/24.92 { e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.92 , e2(a, b, res, False()) -> False() 96.44/24.92 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.92 , m5(a, b, res, t) -> res 96.44/24.92 , <(x, 0()) -> False() 96.44/24.92 , <(S(x), S(y)) -> <(x, y) 96.44/24.92 , <(0(), S(y)) -> True() 96.44/24.92 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.92 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.92 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.92 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.92 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.92 , m2(S(0()), b, res, True()) -> False() 96.44/24.92 , m2(0(), b, res, True()) -> False() 96.44/24.92 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.92 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.92 , e4(a, b, res, True()) -> True() 96.44/24.92 , e4(a, b, res, False()) -> False() } 96.44/24.92 Obligation: 96.44/24.92 innermost runtime complexity 96.44/24.92 Answer: 96.44/24.92 YES(O(1),O(n^1)) 96.44/24.92 96.44/24.92 We use the processor 'matrix interpretation of dimension 1' to 96.44/24.92 orient following rules strictly. 96.44/24.92 96.44/24.92 DPs: 96.44/24.92 { 5: l13^#(x, y, res, tmp, True(), t) -> c_5(gcd^#(S(0()), y)) 96.44/24.92 , 9: l15^#(x, y, res, tmp, True(), t) -> c_9(gcd^#(y, S(0()))) 96.44/24.92 , 14: m4^#(S(x'), S(x), res, t) -> c_14(monus^#(x', x)) } 96.44/24.92 Trs: 96.44/24.92 { m2(S(S(x)), b, res, True()) -> True() 96.44/24.92 , m2(S(0()), b, res, True()) -> False() 96.44/24.92 , m2(0(), b, res, True()) -> False() } 96.44/24.92 96.44/24.92 Sub-proof: 96.44/24.92 ---------- 96.44/24.92 The following argument positions are usable: 96.44/24.92 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 96.44/24.92 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 96.44/24.92 Uargs(c_7) = {1}, Uargs(c_8) = {1, 2}, Uargs(c_9) = {1}, 96.44/24.92 Uargs(c_10) = {1}, Uargs(c_11) = {1}, Uargs(c_12) = {1}, 96.44/24.92 Uargs(c_13) = {1}, Uargs(c_14) = {1}, Uargs(c_15) = {1, 2}, 96.44/24.92 Uargs(c_16) = {1}, Uargs(c_17) = {1}, Uargs(c_18) = {1}, 96.44/24.92 Uargs(c_19) = {1}, Uargs(c_20) = {1}, Uargs(c_21) = {1} 96.44/24.92 96.44/24.92 TcT has computed the following constructor-based matrix 96.44/24.92 interpretation satisfying not(EDA). 96.44/24.92 96.44/24.92 [True] = [2] 96.44/24.92 96.44/24.92 [e2](x1, x2, x3, x4) = [7] x3 + [0] 96.44/24.92 96.44/24.92 [e3](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [0] 96.44/24.92 96.44/24.92 [m5](x1, x2, x3, x4) = [4] x3 + [7] x4 + [0] 96.44/24.92 96.44/24.92 [<](x1, x2) = [0] 96.44/24.92 96.44/24.92 [e1](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] 96.44/24.92 96.44/24.92 [m4](x1, x2, x3, x4) = [7] x3 + [7] x4 + [0] 96.44/24.92 96.44/24.92 [equal0](x1, x2) = [0] 96.44/24.92 96.44/24.92 [False] = [0] 96.44/24.92 96.44/24.92 [m2](x1, x2, x3, x4) = [7] x3 + [2] x4 + [0] 96.44/24.92 96.44/24.92 [monus](x1, x2) = [0] 96.44/24.92 96.44/24.92 [S](x1) = [1] x1 + [3] 96.44/24.92 96.44/24.92 [0] = [0] 96.44/24.92 96.44/24.92 [m1](x1, x2, x3, x4) = [7] x3 + [7] x4 + [0] 96.44/24.92 96.44/24.92 [e4](x1, x2, x3, x4) = [3] x1 + [7] x2 + [7] x3 + [0] 96.44/24.92 96.44/24.92 [l5^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.92 96.44/24.92 [l7^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.92 96.44/24.92 [l1^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.92 96.44/24.92 [l2^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.92 96.44/24.92 [l13^#](x1, x2, x3, x4, x5, x6) = [3] x2 + [5] x5 + [0] 96.44/24.92 96.44/24.92 [gcd^#](x1, x2) = [3] x1 + [3] x2 + [0] 96.44/24.92 96.44/24.92 [l14^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.93 96.44/24.93 [l15^#](x1, x2, x3, x4, x5, x6) = [3] x2 + [6] x5 + [0] 96.44/24.93 96.44/24.93 [monus^#](x1, x2) = [3] x1 + [0] 96.44/24.93 96.44/24.93 [l8^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.93 96.44/24.93 [l10^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.93 96.44/24.93 [m4^#](x1, x2, x3, x4) = [3] x1 + [0] 96.44/24.93 96.44/24.93 [l12^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.93 96.44/24.93 [l11^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.93 96.44/24.93 [l3^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.93 96.44/24.93 [l4^#](x1, x2, x3, x4, x5, x6) = [3] x1 + [3] x2 + [0] 96.44/24.93 96.44/24.93 [m2^#](x1, x2, x3, x4) = [3] x1 + [0] 96.44/24.93 96.44/24.93 [m1^#](x1, x2, x3, x4) = [3] x1 + [0] 96.44/24.93 96.44/24.93 [c_1](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_2](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_3](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_4](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_5](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_6](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_7](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_8](x1, x2) = [1] x1 + [1] x2 + [0] 96.44/24.93 96.44/24.93 [c_9](x1) = [1] x1 + [1] 96.44/24.93 96.44/24.93 [c_10](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_11](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_12](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_13](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_14](x1) = [1] x1 + [1] 96.44/24.93 96.44/24.93 [c_15](x1, x2) = [1] x1 + [1] x2 + [0] 96.44/24.93 96.44/24.93 [c_16](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_17](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_18](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_19](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_20](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 [c_21](x1) = [1] x1 + [0] 96.44/24.93 96.44/24.93 The order satisfies the following ordering constraints: 96.44/24.93 96.44/24.93 [e2(a, b, res, True())] = [7] res + [0] 96.44/24.93 ? [7] b + [7] res + [7] a + [0] 96.44/24.93 = [e3(a, b, res, True())] 96.44/24.93 96.44/24.93 [e2(a, b, res, False())] = [7] res + [0] 96.44/24.93 >= [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [e3(a, b, res, t)] = [7] b + [7] res + [7] a + [0] 96.44/24.93 >= [7] b + [7] res + [3] a + [0] 96.44/24.93 = [e4(a, b, res, <(b, a))] 96.44/24.93 96.44/24.93 [m5(a, b, res, t)] = [4] res + [7] t + [0] 96.44/24.93 >= [1] res + [0] 96.44/24.93 = [res] 96.44/24.93 96.44/24.93 [<(x, 0())] = [0] 96.44/24.93 >= [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [<(S(x), S(y))] = [0] 96.44/24.93 >= [0] 96.44/24.93 = [<(x, y)] 96.44/24.93 96.44/24.93 [<(0(), S(y))] = [0] 96.44/24.93 ? [2] 96.44/24.93 = [True()] 96.44/24.93 96.44/24.93 [e1(a, b, res, t)] = [7] b + [7] res + [7] t + [7] a + [0] 96.44/24.93 >= [7] res + [0] 96.44/24.93 = [e2(a, b, res, <(a, b))] 96.44/24.93 96.44/24.93 [m4(S(x'), S(x), res, t)] = [7] res + [7] t + [0] 96.44/24.93 >= [7] t + [0] 96.44/24.93 = [m5(S(x'), S(x), monus(x', x), t)] 96.44/24.93 96.44/24.93 [equal0(a, b)] = [0] 96.44/24.93 ? [7] b + [7] a + [0] 96.44/24.93 = [e1(a, b, False(), False())] 96.44/24.93 96.44/24.93 [m2(a, b, res, False())] = [7] res + [0] 96.44/24.93 >= [7] res + [0] 96.44/24.93 = [m4(a, b, res, False())] 96.44/24.93 96.44/24.93 [m2(S(S(x)), b, res, True())] = [7] res + [4] 96.44/24.93 > [2] 96.44/24.93 = [True()] 96.44/24.93 96.44/24.93 [m2(S(0()), b, res, True())] = [7] res + [4] 96.44/24.93 > [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [m2(0(), b, res, True())] = [7] res + [4] 96.44/24.93 > [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [monus(a, b)] = [0] 96.44/24.93 >= [0] 96.44/24.93 = [m1(a, b, False(), False())] 96.44/24.93 96.44/24.93 [m1(a, x, res, t)] = [7] res + [7] t + [0] 96.44/24.93 >= [7] res + [0] 96.44/24.93 = [m2(a, x, res, False())] 96.44/24.93 96.44/24.93 [e4(a, b, res, True())] = [7] b + [7] res + [3] a + [0] 96.44/24.93 ? [2] 96.44/24.93 = [True()] 96.44/24.93 96.44/24.93 [e4(a, b, res, False())] = [7] b + [7] res + [3] a + [0] 96.44/24.93 >= [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [l5^#(x, y, res, tmp, mtmp, False())] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_1(l7^#(x, y, res, tmp, mtmp, False()))] 96.44/24.93 96.44/24.93 [l7^#(x, y, res, tmp, mtmp, t)] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_2(l8^#(x, y, res, equal0(x, y), mtmp, t))] 96.44/24.93 96.44/24.93 [l1^#(x, y, res, tmp, mtmp, t)] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_3(l2^#(x, y, res, tmp, mtmp, False()))] 96.44/24.93 96.44/24.93 [l2^#(x, y, res, tmp, mtmp, False())] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_4(l3^#(x, y, res, tmp, mtmp, False()))] 96.44/24.93 96.44/24.93 [l13^#(x, y, res, tmp, True(), t)] = [3] y + [10] 96.44/24.93 > [3] y + [9] 96.44/24.93 = [c_5(gcd^#(S(0()), y))] 96.44/24.93 96.44/24.93 [l13^#(x, y, res, tmp, False(), t)] = [3] y + [0] 96.44/24.93 >= [3] y + [0] 96.44/24.93 = [c_6(gcd^#(0(), y))] 96.44/24.93 96.44/24.93 [gcd^#(x, y)] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_7(l1^#(x, y, 0(), False(), False(), False()))] 96.44/24.93 96.44/24.93 [l14^#(x, y, res, tmp, mtmp, t)] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_8(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y))] 96.44/24.93 96.44/24.93 [l15^#(x, y, res, tmp, True(), t)] = [3] y + [12] 96.44/24.93 > [3] y + [10] 96.44/24.93 = [c_9(gcd^#(y, S(0())))] 96.44/24.93 96.44/24.93 [l15^#(x, y, res, tmp, False(), t)] = [3] y + [0] 96.44/24.93 >= [3] y + [0] 96.44/24.93 = [c_10(gcd^#(y, 0()))] 96.44/24.93 96.44/24.93 [monus^#(a, b)] = [3] a + [0] 96.44/24.93 >= [3] a + [0] 96.44/24.93 = [c_11(m1^#(a, b, False(), False()))] 96.44/24.93 96.44/24.93 [l8^#(x, y, res, False(), mtmp, t)] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_12(l10^#(x, y, res, False(), mtmp, t))] 96.44/24.93 96.44/24.93 [l10^#(x, y, res, tmp, mtmp, t)] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_13(l11^#(x, y, res, tmp, mtmp, <(x, y)))] 96.44/24.93 96.44/24.93 [m4^#(S(x'), S(x), res, t)] = [3] x' + [9] 96.44/24.93 > [3] x' + [1] 96.44/24.93 = [c_14(monus^#(x', x))] 96.44/24.93 96.44/24.93 [l12^#(x, y, res, tmp, mtmp, t)] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_15(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y))] 96.44/24.93 96.44/24.93 [l11^#(x, y, res, tmp, mtmp, True())] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_16(l12^#(x, y, res, tmp, mtmp, True()))] 96.44/24.93 96.44/24.93 [l11^#(x, y, res, tmp, mtmp, False())] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_17(l14^#(x, y, res, tmp, mtmp, False()))] 96.44/24.93 96.44/24.93 [l3^#(x, y, res, tmp, mtmp, t)] = [3] x + [3] y + [0] 96.44/24.93 >= [3] x + [3] y + [0] 96.44/24.93 = [c_18(l4^#(x, y, 0(), tmp, mtmp, t))] 96.44/24.93 96.44/24.93 [l4^#(x', x, res, tmp, mtmp, t)] = [3] x + [3] x' + [0] 96.44/24.93 >= [3] x + [3] x' + [0] 96.44/24.93 = [c_19(l5^#(x', x, res, tmp, mtmp, False()))] 96.44/24.93 96.44/24.93 [m2^#(a, b, res, False())] = [3] a + [0] 96.44/24.93 >= [3] a + [0] 96.44/24.93 = [c_20(m4^#(a, b, res, False()))] 96.44/24.93 96.44/24.93 [m1^#(a, x, res, t)] = [3] a + [0] 96.44/24.93 >= [3] a + [0] 96.44/24.93 = [c_21(m2^#(a, x, res, False()))] 96.44/24.93 96.44/24.93 96.44/24.93 The strictly oriented rules are moved into the weak component. 96.44/24.93 96.44/24.93 We are left with following problem, upon which TcT provides the 96.44/24.93 certificate YES(O(1),O(n^1)). 96.44/24.93 96.44/24.93 Strict DPs: 96.44/24.93 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.93 c_1(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.93 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.93 c_2(l8^#(x, y, res, equal0(x, y), mtmp, t)) 96.44/24.93 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.93 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.93 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.93 c_4(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.93 , l13^#(x, y, res, tmp, False(), t) -> c_6(gcd^#(0(), y)) 96.44/24.93 , gcd^#(x, y) -> c_7(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.93 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.93 c_8(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.93 , l15^#(x, y, res, tmp, False(), t) -> c_10(gcd^#(y, 0())) 96.44/24.93 , monus^#(a, b) -> c_11(m1^#(a, b, False(), False())) 96.44/24.93 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.93 c_12(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.93 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.93 c_13(l11^#(x, y, res, tmp, mtmp, <(x, y))) 96.44/24.93 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.93 c_15(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.93 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.93 c_16(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.93 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.93 c_17(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.93 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.93 c_18(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.93 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.93 c_19(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.93 , m2^#(a, b, res, False()) -> c_20(m4^#(a, b, res, False())) 96.44/24.93 , m1^#(a, x, res, t) -> c_21(m2^#(a, x, res, False())) } 96.44/24.93 Weak DPs: 96.44/24.93 { l13^#(x, y, res, tmp, True(), t) -> c_5(gcd^#(S(0()), y)) 96.44/24.93 , l15^#(x, y, res, tmp, True(), t) -> c_9(gcd^#(y, S(0()))) 96.44/24.93 , m4^#(S(x'), S(x), res, t) -> c_14(monus^#(x', x)) } 96.44/24.93 Weak Trs: 96.44/24.93 { e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.93 , e2(a, b, res, False()) -> False() 96.44/24.93 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.93 , m5(a, b, res, t) -> res 96.44/24.93 , <(x, 0()) -> False() 96.44/24.93 , <(S(x), S(y)) -> <(x, y) 96.44/24.93 , <(0(), S(y)) -> True() 96.44/24.93 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.93 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.93 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.93 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.93 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.93 , m2(S(0()), b, res, True()) -> False() 96.44/24.93 , m2(0(), b, res, True()) -> False() 96.44/24.93 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.93 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.93 , e4(a, b, res, True()) -> True() 96.44/24.93 , e4(a, b, res, False()) -> False() } 96.44/24.93 Obligation: 96.44/24.93 innermost runtime complexity 96.44/24.93 Answer: 96.44/24.93 YES(O(1),O(n^1)) 96.44/24.93 96.44/24.93 We use the processor 'matrix interpretation of dimension 2' to 96.44/24.93 orient following rules strictly. 96.44/24.93 96.44/24.93 DPs: 96.44/24.93 { 1: l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.93 c_1(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.93 , 5: l13^#(x, y, res, tmp, False(), t) -> c_6(gcd^#(0(), y)) 96.44/24.93 , 8: l15^#(x, y, res, tmp, False(), t) -> c_10(gcd^#(y, 0())) 96.44/24.93 , 9: monus^#(a, b) -> c_11(m1^#(a, b, False(), False())) 96.44/24.93 , 21: m4^#(S(x'), S(x), res, t) -> c_14(monus^#(x', x)) } 96.44/24.93 Trs: { m2(S(S(x)), b, res, True()) -> True() } 96.44/24.93 96.44/24.93 Sub-proof: 96.44/24.93 ---------- 96.44/24.93 The following argument positions are usable: 96.44/24.93 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 96.44/24.93 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 96.44/24.93 Uargs(c_7) = {1}, Uargs(c_8) = {1, 2}, Uargs(c_9) = {1}, 96.44/24.93 Uargs(c_10) = {1}, Uargs(c_11) = {1}, Uargs(c_12) = {1}, 96.44/24.93 Uargs(c_13) = {1}, Uargs(c_14) = {1}, Uargs(c_15) = {1, 2}, 96.44/24.93 Uargs(c_16) = {1}, Uargs(c_17) = {1}, Uargs(c_18) = {1}, 96.44/24.93 Uargs(c_19) = {1}, Uargs(c_20) = {1}, Uargs(c_21) = {1} 96.44/24.93 96.44/24.93 TcT has computed the following constructor-based matrix 96.44/24.93 interpretation satisfying not(EDA) and not(IDA(1)). 96.44/24.93 96.44/24.93 [True] = [0] 96.44/24.93 [2] 96.44/24.93 96.44/24.93 [e2](x1, x2, x3, x4) = [7 4] x3 + [0] 96.44/24.93 [4 7] [0] 96.44/24.93 96.44/24.93 [e3](x1, x2, x3, x4) = [7 0] x1 + [7 0] x2 + [7 96.44/24.93 4] x3 + [7 0] x4 + [0] 96.44/24.93 [7 7] [7 7] [4 96.44/24.93 7] [7 0] [0] 96.44/24.93 96.44/24.93 [m5](x1, x2, x3, x4) = [4 0] x3 + [0 4] x4 + [0] 96.44/24.93 [0 2] [0 7] [0] 96.44/24.93 96.44/24.93 [<](x1, x2) = [0] 96.44/24.93 [0] 96.44/24.93 96.44/24.93 [e1](x1, x2, x3, x4) = [6 0] x1 + [6 0] x2 + [0 96.44/24.93 4] x3 + [0 4] x4 + [0] 96.44/24.93 [6 6] [6 6] [0 96.44/24.93 7] [0 5] [0] 96.44/24.93 96.44/24.93 [m4](x1, x2, x3, x4) = [0 4] x3 + [0 4] x4 + [0] 96.44/24.93 [0 5] [0 7] [0] 96.44/24.93 96.44/24.93 [equal0](x1, x2) = [0] 96.44/24.93 [0] 96.44/24.93 96.44/24.93 [False] = [2] 96.44/24.93 [0] 96.44/24.93 96.44/24.93 [m2](x1, x2, x3, x4) = [0 4] x3 + [0 1] x4 + [0] 96.44/24.93 [0 5] [0 4] [0] 96.44/24.93 96.44/24.93 [monus](x1, x2) = [0] 96.44/24.93 [0] 96.44/24.93 96.44/24.93 [S](x1) = [1 2] x1 + [3] 96.44/24.93 [0 0] [5] 96.44/24.93 96.44/24.93 [0] = [0] 96.44/24.93 [0] 96.44/24.93 96.44/24.93 [m1](x1, x2, x3, x4) = [0 4] x3 + [0 4] x4 + [0] 96.44/24.93 [0 5] [0 7] [0] 96.44/24.93 96.44/24.93 [e4](x1, x2, x3, x4) = [7 1] x1 + [7 1] x2 + [7 96.44/24.93 4] x3 + [0] 96.44/24.93 [7 7] [7 7] [4 96.44/24.93 7] [0] 96.44/24.93 96.44/24.93 [l5^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x3 + [0 0] x4 + [0 0] x5 + [0 96.44/24.93 0] x6 + [4] 96.44/24.93 [4 0] [4 0] [4 96.44/24.93 0] [4 4] [4 4] [4 96.44/24.93 0] [0] 96.44/24.93 96.44/24.93 [l7^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x3 + [0 0] x5 + [0 0] x6 + [3] 96.44/24.93 [0 4] [4 0] [0 96.44/24.93 4] [4 4] [4 0] [0] 96.44/24.93 96.44/24.93 [l1^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x3 + [0 0] x4 + [0 4] x5 + [4] 96.44/24.93 [4 0] [4 0] [4 96.44/24.93 0] [4 4] [4 4] [0] 96.44/24.93 96.44/24.93 [l2^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x3 + [0 4] x5 + [1 0] x6 + [2] 96.44/24.93 [4 4] [0 0] [4 96.44/24.93 4] [4 0] [0 0] [0] 96.44/24.93 96.44/24.93 [l13^#](x1, x2, x3, x4, x5, x6) = [2 1] x2 + [4 6] x5 + [0] 96.44/24.93 [4 4] [0 0] [0] 96.44/24.93 96.44/24.93 [gcd^#](x1, x2) = [1 1] x1 + [2 1] x2 + [4] 96.44/24.93 [4 4] [0 4] [0] 96.44/24.93 96.44/24.93 [l14^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [1 1] x2 + [0 96.44/24.93 0] x6 + [3] 96.44/24.93 [4 4] [4 4] [0 96.44/24.93 4] [0] 96.44/24.93 96.44/24.93 [l15^#](x1, x2, x3, x4, x5, x6) = [1 1] x2 + [4 7] x5 + [1] 96.44/24.93 [4 0] [4 4] [0] 96.44/24.93 96.44/24.93 [monus^#](x1, x2) = [1 1] x1 + [2] 96.44/24.93 [0 0] [1] 96.44/24.93 96.44/24.93 [l8^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x5 + [0 0] x6 + [3] 96.44/24.93 [4 4] [0 4] [4 96.44/24.93 0] [4 4] [0] 96.44/24.93 96.44/24.93 [l10^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x3 + [0 0] x4 + [3] 96.44/24.93 [0 4] [4 0] [0 96.44/24.93 4] [4 0] [0] 96.44/24.93 96.44/24.93 [m4^#](x1, x2, x3, x4) = [1 1] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [l12^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x3 + [0 0] x6 + [2] 96.44/24.93 [0 0] [4 0] [4 96.44/24.93 4] [4 0] [0] 96.44/24.93 96.44/24.93 [l11^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x3 + [0 0] x4 + [0 0] x5 + [3] 96.44/24.93 [4 4] [4 0] [4 96.44/24.93 4] [0 4] [4 4] [4] 96.44/24.93 96.44/24.93 [l3^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x4 + [0 4] x5 + [4] 96.44/24.93 [4 0] [4 0] [0 96.44/24.93 4] [0 0] [0] 96.44/24.93 96.44/24.93 [l4^#](x1, x2, x3, x4, x5, x6) = [1 1] x1 + [2 1] x2 + [0 96.44/24.93 0] x3 + [0 0] x4 + [0 4] x5 + [4] 96.44/24.93 [4 0] [0 0] [4 96.44/24.93 4] [4 0] [0 0] [0] 96.44/24.93 96.44/24.93 [m2^#](x1, x2, x3, x4) = [1 1] x1 + [0 0] x2 + [0 96.44/24.93 0] x3 + [0] 96.44/24.93 [0 0] [0 4] [4 96.44/24.93 4] [0] 96.44/24.93 96.44/24.93 [m1^#](x1, x2, x3, x4) = [1 1] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_1](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [7] 96.44/24.93 96.44/24.93 [c_2](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_3](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_4](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_5](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_6](x1) = [1 0] x1 + [3] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_7](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_8](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 96.44/24.93 [0 0] [0 0] [0] 96.44/24.93 96.44/24.93 [c_9](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [3] 96.44/24.93 96.44/24.93 [c_10](x1) = [1 0] x1 + [3] 96.44/24.93 [0 0] [3] 96.44/24.93 96.44/24.93 [c_11](x1) = [1 0] x1 + [1] 96.44/24.93 [0 0] [1] 96.44/24.93 96.44/24.93 [c_12](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_13](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_14](x1) = [1 2] x1 + [3] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_15](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 96.44/24.93 [0 0] [0 0] [0] 96.44/24.93 96.44/24.93 [c_16](x1) = [1 0] x1 + [1] 96.44/24.93 [0 0] [3] 96.44/24.93 96.44/24.93 [c_17](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [3] 96.44/24.93 96.44/24.93 [c_18](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_19](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_20](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 [c_21](x1) = [1 0] x1 + [0] 96.44/24.93 [0 0] [0] 96.44/24.93 96.44/24.93 The order satisfies the following ordering constraints: 96.44/24.93 96.44/24.93 [e2(a, b, res, True())] = [7 4] res + [0] 96.44/24.93 [4 7] [0] 96.44/24.93 ? [7 0] b + [7 4] res + [7 0] a + [0] 96.44/24.93 [7 7] [4 7] [7 7] [0] 96.44/24.93 = [e3(a, b, res, True())] 96.44/24.93 96.44/24.93 [e2(a, b, res, False())] = [7 4] res + [0] 96.44/24.93 [4 7] [0] 96.44/24.93 ? [2] 96.44/24.93 [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [e3(a, b, res, t)] = [7 0] b + [7 4] res + [7 0] t + [7 0] a + [0] 96.44/24.93 [7 7] [4 7] [7 0] [7 7] [0] 96.44/24.93 ? [7 1] b + [7 4] res + [7 1] a + [0] 96.44/24.93 [7 7] [4 7] [7 7] [0] 96.44/24.93 = [e4(a, b, res, <(b, a))] 96.44/24.93 96.44/24.93 [m5(a, b, res, t)] = [4 0] res + [0 4] t + [0] 96.44/24.93 [0 2] [0 7] [0] 96.44/24.93 >= [1 0] res + [0] 96.44/24.93 [0 1] [0] 96.44/24.93 = [res] 96.44/24.93 96.44/24.93 [<(x, 0())] = [0] 96.44/24.93 [0] 96.44/24.93 ? [2] 96.44/24.93 [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [<(S(x), S(y))] = [0] 96.44/24.93 [0] 96.44/24.93 >= [0] 96.44/24.93 [0] 96.44/24.93 = [<(x, y)] 96.44/24.93 96.44/24.93 [<(0(), S(y))] = [0] 96.44/24.93 [0] 96.44/24.93 ? [0] 96.44/24.93 [2] 96.44/24.93 = [True()] 96.44/24.93 96.44/24.93 [e1(a, b, res, t)] = [6 0] b + [0 4] res + [0 4] t + [6 0] a + [0] 96.44/24.93 [6 6] [0 7] [0 5] [6 6] [0] 96.44/24.93 ? [7 4] res + [0] 96.44/24.93 [4 7] [0] 96.44/24.93 = [e2(a, b, res, <(a, b))] 96.44/24.93 96.44/24.93 [m4(S(x'), S(x), res, t)] = [0 4] res + [0 4] t + [0] 96.44/24.93 [0 5] [0 7] [0] 96.44/24.93 >= [0 4] t + [0] 96.44/24.93 [0 7] [0] 96.44/24.93 = [m5(S(x'), S(x), monus(x', x), t)] 96.44/24.93 96.44/24.93 [equal0(a, b)] = [0] 96.44/24.93 [0] 96.44/24.93 ? [6 0] b + [6 0] a + [0] 96.44/24.93 [6 6] [6 6] [0] 96.44/24.93 = [e1(a, b, False(), False())] 96.44/24.93 96.44/24.93 [m2(a, b, res, False())] = [0 4] res + [0] 96.44/24.93 [0 5] [0] 96.44/24.93 >= [0 4] res + [0] 96.44/24.93 [0 5] [0] 96.44/24.93 = [m4(a, b, res, False())] 96.44/24.93 96.44/24.93 [m2(S(S(x)), b, res, True())] = [0 4] res + [2] 96.44/24.93 [0 5] [8] 96.44/24.93 > [0] 96.44/24.93 [2] 96.44/24.93 = [True()] 96.44/24.93 96.44/24.93 [m2(S(0()), b, res, True())] = [0 4] res + [2] 96.44/24.93 [0 5] [8] 96.44/24.93 >= [2] 96.44/24.93 [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [m2(0(), b, res, True())] = [0 4] res + [2] 96.44/24.93 [0 5] [8] 96.44/24.93 >= [2] 96.44/24.93 [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [monus(a, b)] = [0] 96.44/24.93 [0] 96.44/24.93 >= [0] 96.44/24.93 [0] 96.44/24.93 = [m1(a, b, False(), False())] 96.44/24.93 96.44/24.93 [m1(a, x, res, t)] = [0 4] res + [0 4] t + [0] 96.44/24.93 [0 5] [0 7] [0] 96.44/24.93 >= [0 4] res + [0] 96.44/24.93 [0 5] [0] 96.44/24.93 = [m2(a, x, res, False())] 96.44/24.93 96.44/24.93 [e4(a, b, res, True())] = [7 1] b + [7 4] res + [7 1] a + [0] 96.44/24.93 [7 7] [4 7] [7 7] [0] 96.44/24.93 ? [0] 96.44/24.93 [2] 96.44/24.93 = [True()] 96.44/24.93 96.44/24.93 [e4(a, b, res, False())] = [7 1] b + [7 4] res + [7 1] a + [0] 96.44/24.93 [7 7] [4 7] [7 7] [0] 96.44/24.93 ? [2] 96.44/24.93 [0] 96.44/24.93 = [False()] 96.44/24.93 96.44/24.93 [l5^#(x, y, res, tmp, mtmp, False())] = [0 0] res + [1 1] x + [2 1] y + [0 0] mtmp + [0 0] tmp + [4] 96.44/24.93 [4 0] [4 0] [4 0] [4 4] [4 4] [8] 96.44/24.93 > [1 1] x + [2 1] y + [3] 96.44/24.93 [0 0] [0 0] [7] 96.44/24.93 = [c_1(l7^#(x, y, res, tmp, mtmp, False()))] 96.44/24.93 96.44/24.93 [l7^#(x, y, res, tmp, mtmp, t)] = [0 0] res + [1 1] x + [0 0] t + [2 1] y + [0 0] mtmp + [3] 96.44/24.93 [0 4] [0 4] [4 0] [4 0] [4 4] [0] 96.44/24.93 >= [1 1] x + [2 1] y + [3] 96.44/24.93 [0 0] [0 0] [0] 96.44/24.93 = [c_2(l8^#(x, y, res, equal0(x, y), mtmp, t))] 96.44/24.93 96.44/24.93 [l1^#(x, y, res, tmp, mtmp, t)] = [0 0] res + [1 1] x + [2 1] y + [0 4] mtmp + [0 0] tmp + [4] 96.44/24.93 [4 0] [4 0] [4 0] [4 4] [4 4] [0] 96.44/24.93 >= [1 1] x + [2 1] y + [0 4] mtmp + [4] 96.44/24.93 [0 0] [0 0] [0 0] [0] 96.44/24.93 = [c_3(l2^#(x, y, res, tmp, mtmp, False()))] 96.44/24.93 96.44/24.93 [l2^#(x, y, res, tmp, mtmp, False())] = [0 0] res + [1 1] x + [2 1] y + [0 4] mtmp + [4] 96.44/24.93 [4 4] [4 4] [0 0] [4 0] [0] 96.44/24.93 >= [1 1] x + [2 1] y + [0 4] mtmp + [4] 96.44/24.93 [0 0] [0 0] [0 0] [0] 96.44/24.93 = [c_4(l3^#(x, y, res, tmp, mtmp, False()))] 96.44/24.93 96.44/24.93 [l13^#(x, y, res, tmp, True(), t)] = [2 1] y + [12] 96.44/24.93 [4 4] [0] 96.44/24.93 >= [2 1] y + [12] 96.44/24.93 [0 0] [0] 96.44/24.93 = [c_5(gcd^#(S(0()), y))] 96.44/24.93 96.44/24.93 [l13^#(x, y, res, tmp, False(), t)] = [2 1] y + [8] 96.44/24.93 [4 4] [0] 96.44/24.93 > [2 1] y + [7] 96.44/24.93 [0 0] [0] 96.44/24.93 = [c_6(gcd^#(0(), y))] 96.44/24.93 96.44/24.93 [gcd^#(x, y)] = [1 1] x + [2 1] y + [4] 96.44/24.93 [4 4] [0 4] [0] 96.44/24.93 >= [1 1] x + [2 1] y + [4] 96.44/24.93 [0 0] [0 0] [0] 96.44/24.93 = [c_7(l1^#(x, y, 0(), False(), False(), False()))] 96.44/24.93 96.44/24.93 [l14^#(x, y, res, tmp, mtmp, t)] = [1 1] x + [0 0] t + [1 1] y + [3] 96.44/24.93 [4 4] [0 4] [4 4] [0] 96.44/24.93 >= [1 1] x + [1 1] y + [3] 96.44/24.93 [0 0] [0 0] [0] 96.44/24.93 = [c_8(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y))] 96.44/24.93 96.44/24.93 [l15^#(x, y, res, tmp, True(), t)] = [1 1] y + [15] 96.44/24.93 [4 0] [8] 96.44/24.93 >= [1 1] y + [15] 96.44/24.93 [0 0] [3] 96.44/24.93 = [c_9(gcd^#(y, S(0())))] 96.44/24.93 96.44/24.93 [l15^#(x, y, res, tmp, False(), t)] = [1 1] y + [9] 96.44/24.93 [4 0] [8] 96.44/24.93 > [1 1] y + [7] 96.44/24.93 [0 0] [3] 96.44/24.93 = [c_10(gcd^#(y, 0()))] 96.44/24.93 96.44/24.93 [monus^#(a, b)] = [1 1] a + [2] 96.44/24.93 [0 0] [1] 96.44/24.93 > [1 1] a + [1] 96.44/24.93 [0 0] [1] 96.44/24.93 = [c_11(m1^#(a, b, False(), False()))] 96.44/24.93 96.44/24.93 [l8^#(x, y, res, False(), mtmp, t)] = [1 1] x + [0 0] t + [2 1] y + [0 0] mtmp + [3] 96.44/24.93 [4 4] [4 4] [0 4] [4 0] [0] 96.44/24.93 >= [1 1] x + [2 1] y + [3] 96.44/24.93 [0 0] [0 0] [0] 96.44/24.94 = [c_12(l10^#(x, y, res, False(), mtmp, t))] 96.44/24.94 96.44/24.94 [l10^#(x, y, res, tmp, mtmp, t)] = [0 0] res + [1 1] x + [2 1] y + [0 0] tmp + [3] 96.44/24.94 [0 4] [0 4] [4 0] [4 0] [0] 96.44/24.94 >= [1 1] x + [2 1] y + [3] 96.44/24.94 [0 0] [0 0] [0] 96.44/24.94 = [c_13(l11^#(x, y, res, tmp, mtmp, <(x, y)))] 96.44/24.94 96.44/24.94 [m4^#(S(x'), S(x), res, t)] = [1 2] x' + [8] 96.44/24.94 [0 0] [0] 96.44/24.94 > [1 1] x' + [7] 96.44/24.94 [0 0] [0] 96.44/24.94 = [c_14(monus^#(x', x))] 96.44/24.94 96.44/24.94 [l12^#(x, y, res, tmp, mtmp, t)] = [0 0] res + [1 1] x + [0 0] t + [2 1] y + [2] 96.44/24.94 [4 4] [0 0] [4 0] [4 0] [0] 96.44/24.94 >= [1 1] x + [2 1] y + [2] 96.44/24.94 [0 0] [0 0] [0] 96.44/24.94 = [c_15(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y))] 96.44/24.94 96.44/24.94 [l11^#(x, y, res, tmp, mtmp, True())] = [0 0] res + [1 1] x + [2 1] y + [0 0] mtmp + [0 0] tmp + [3] 96.44/24.94 [4 4] [4 4] [4 0] [4 4] [0 4] [4] 96.44/24.94 >= [1 1] x + [2 1] y + [3] 96.44/24.94 [0 0] [0 0] [3] 96.44/24.94 = [c_16(l12^#(x, y, res, tmp, mtmp, True()))] 96.44/24.94 96.44/24.94 [l11^#(x, y, res, tmp, mtmp, False())] = [0 0] res + [1 1] x + [2 1] y + [0 0] mtmp + [0 0] tmp + [3] 96.44/24.94 [4 4] [4 4] [4 0] [4 4] [0 4] [4] 96.44/24.94 >= [1 1] x + [1 1] y + [3] 96.44/24.94 [0 0] [0 0] [3] 96.44/24.94 = [c_17(l14^#(x, y, res, tmp, mtmp, False()))] 96.44/24.94 96.44/24.94 [l3^#(x, y, res, tmp, mtmp, t)] = [1 1] x + [2 1] y + [0 4] mtmp + [0 0] tmp + [4] 96.44/24.94 [4 0] [4 0] [0 0] [0 4] [0] 96.44/24.94 >= [1 1] x + [2 1] y + [0 4] mtmp + [4] 96.44/24.94 [0 0] [0 0] [0 0] [0] 96.44/24.94 = [c_18(l4^#(x, y, 0(), tmp, mtmp, t))] 96.44/24.94 96.44/24.94 [l4^#(x', x, res, tmp, mtmp, t)] = [0 0] res + [2 1] x + [0 4] mtmp + [0 0] tmp + [1 1] x' + [4] 96.44/24.94 [4 4] [0 0] [0 0] [4 0] [4 0] [0] 96.44/24.94 >= [2 1] x + [1 1] x' + [4] 96.44/24.94 [0 0] [0 0] [0] 96.44/24.94 = [c_19(l5^#(x', x, res, tmp, mtmp, False()))] 96.44/24.94 96.44/24.94 [m2^#(a, b, res, False())] = [0 0] b + [0 0] res + [1 1] a + [0] 96.44/24.94 [0 4] [4 4] [0 0] [0] 96.44/24.94 >= [1 1] a + [0] 96.44/24.94 [0 0] [0] 96.44/24.94 = [c_20(m4^#(a, b, res, False()))] 96.44/24.94 96.44/24.94 [m1^#(a, x, res, t)] = [1 1] a + [0] 96.44/24.94 [0 0] [0] 96.44/24.94 >= [1 1] a + [0] 96.44/24.94 [0 0] [0] 96.44/24.94 = [c_21(m2^#(a, x, res, False()))] 96.44/24.94 96.44/24.94 96.44/24.94 We return to the main proof. Consider the set of all dependency 96.44/24.94 pairs 96.44/24.94 96.44/24.94 : 96.44/24.94 { 1: l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_1(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , 2: l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_2(l8^#(x, y, res, equal0(x, y), mtmp, t)) 96.44/24.94 , 3: l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , 4: l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_4(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , 5: l13^#(x, y, res, tmp, False(), t) -> c_6(gcd^#(0(), y)) 96.44/24.94 , 6: gcd^#(x, y) -> c_7(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.94 , 7: l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_8(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.94 , 8: l15^#(x, y, res, tmp, False(), t) -> c_10(gcd^#(y, 0())) 96.44/24.94 , 9: monus^#(a, b) -> c_11(m1^#(a, b, False(), False())) 96.44/24.94 , 10: l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.94 c_12(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.94 , 11: l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_13(l11^#(x, y, res, tmp, mtmp, <(x, y))) 96.44/24.94 , 12: l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_15(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.94 , 13: l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.94 c_16(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.94 , 14: l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_17(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , 15: l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_18(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.94 , 16: l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.94 c_19(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.94 , 17: m2^#(a, b, res, False()) -> c_20(m4^#(a, b, res, False())) 96.44/24.94 , 18: m1^#(a, x, res, t) -> c_21(m2^#(a, x, res, False())) 96.44/24.94 , 19: l13^#(x, y, res, tmp, True(), t) -> c_5(gcd^#(S(0()), y)) 96.44/24.94 , 20: l15^#(x, y, res, tmp, True(), t) -> c_9(gcd^#(y, S(0()))) 96.44/24.94 , 21: m4^#(S(x'), S(x), res, t) -> c_14(monus^#(x', x)) } 96.44/24.94 96.44/24.94 Processor 'matrix interpretation of dimension 2' induces the 96.44/24.94 complexity certificate YES(?,O(n^1)) on application of dependency 96.44/24.94 pairs {1,5,8,9,21}. These cover all (indirect) predecessors of 96.44/24.94 dependency pairs 96.44/24.94 {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21}, their 96.44/24.94 number of application is equally bounded. The dependency pairs are 96.44/24.94 shifted into the weak component. 96.44/24.94 96.44/24.94 We are left with following problem, upon which TcT provides the 96.44/24.94 certificate YES(O(1),O(1)). 96.44/24.94 96.44/24.94 Weak DPs: 96.44/24.94 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_1(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_2(l8^#(x, y, res, equal0(x, y), mtmp, t)) 96.44/24.94 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_4(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , l13^#(x, y, res, tmp, True(), t) -> c_5(gcd^#(S(0()), y)) 96.44/24.94 , l13^#(x, y, res, tmp, False(), t) -> c_6(gcd^#(0(), y)) 96.44/24.94 , gcd^#(x, y) -> c_7(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.94 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_8(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.94 , l15^#(x, y, res, tmp, True(), t) -> c_9(gcd^#(y, S(0()))) 96.44/24.94 , l15^#(x, y, res, tmp, False(), t) -> c_10(gcd^#(y, 0())) 96.44/24.94 , monus^#(a, b) -> c_11(m1^#(a, b, False(), False())) 96.44/24.94 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.94 c_12(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.94 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_13(l11^#(x, y, res, tmp, mtmp, <(x, y))) 96.44/24.94 , m4^#(S(x'), S(x), res, t) -> c_14(monus^#(x', x)) 96.44/24.94 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_15(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.94 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.94 c_16(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.94 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_17(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_18(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.94 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.94 c_19(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.94 , m2^#(a, b, res, False()) -> c_20(m4^#(a, b, res, False())) 96.44/24.94 , m1^#(a, x, res, t) -> c_21(m2^#(a, x, res, False())) } 96.44/24.94 Weak Trs: 96.44/24.94 { e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.94 , e2(a, b, res, False()) -> False() 96.44/24.94 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.94 , m5(a, b, res, t) -> res 96.44/24.94 , <(x, 0()) -> False() 96.44/24.94 , <(S(x), S(y)) -> <(x, y) 96.44/24.94 , <(0(), S(y)) -> True() 96.44/24.94 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.94 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.94 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.94 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.94 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.94 , m2(S(0()), b, res, True()) -> False() 96.44/24.94 , m2(0(), b, res, True()) -> False() 96.44/24.94 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.94 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.94 , e4(a, b, res, True()) -> True() 96.44/24.94 , e4(a, b, res, False()) -> False() } 96.44/24.94 Obligation: 96.44/24.94 innermost runtime complexity 96.44/24.94 Answer: 96.44/24.94 YES(O(1),O(1)) 96.44/24.94 96.44/24.94 The following weak DPs constitute a sub-graph of the DG that is 96.44/24.94 closed under successors. The DPs are removed. 96.44/24.94 96.44/24.94 { l5^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_1(l7^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , l7^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_2(l8^#(x, y, res, equal0(x, y), mtmp, t)) 96.44/24.94 , l1^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_3(l2^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , l2^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_4(l3^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , l13^#(x, y, res, tmp, True(), t) -> c_5(gcd^#(S(0()), y)) 96.44/24.94 , l13^#(x, y, res, tmp, False(), t) -> c_6(gcd^#(0(), y)) 96.44/24.94 , gcd^#(x, y) -> c_7(l1^#(x, y, 0(), False(), False(), False())) 96.44/24.94 , l14^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_8(l15^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.94 , l15^#(x, y, res, tmp, True(), t) -> c_9(gcd^#(y, S(0()))) 96.44/24.94 , l15^#(x, y, res, tmp, False(), t) -> c_10(gcd^#(y, 0())) 96.44/24.94 , monus^#(a, b) -> c_11(m1^#(a, b, False(), False())) 96.44/24.94 , l8^#(x, y, res, False(), mtmp, t) -> 96.44/24.94 c_12(l10^#(x, y, res, False(), mtmp, t)) 96.44/24.94 , l10^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_13(l11^#(x, y, res, tmp, mtmp, <(x, y))) 96.44/24.94 , m4^#(S(x'), S(x), res, t) -> c_14(monus^#(x', x)) 96.44/24.94 , l12^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_15(l13^#(x, y, res, tmp, monus(x, y), t), monus^#(x, y)) 96.44/24.94 , l11^#(x, y, res, tmp, mtmp, True()) -> 96.44/24.94 c_16(l12^#(x, y, res, tmp, mtmp, True())) 96.44/24.94 , l11^#(x, y, res, tmp, mtmp, False()) -> 96.44/24.94 c_17(l14^#(x, y, res, tmp, mtmp, False())) 96.44/24.94 , l3^#(x, y, res, tmp, mtmp, t) -> 96.44/24.94 c_18(l4^#(x, y, 0(), tmp, mtmp, t)) 96.44/24.94 , l4^#(x', x, res, tmp, mtmp, t) -> 96.44/24.94 c_19(l5^#(x', x, res, tmp, mtmp, False())) 96.44/24.94 , m2^#(a, b, res, False()) -> c_20(m4^#(a, b, res, False())) 96.44/24.94 , m1^#(a, x, res, t) -> c_21(m2^#(a, x, res, False())) } 96.44/24.94 96.44/24.94 We are left with following problem, upon which TcT provides the 96.44/24.94 certificate YES(O(1),O(1)). 96.44/24.94 96.44/24.94 Weak Trs: 96.44/24.94 { e2(a, b, res, True()) -> e3(a, b, res, True()) 96.44/24.94 , e2(a, b, res, False()) -> False() 96.44/24.94 , e3(a, b, res, t) -> e4(a, b, res, <(b, a)) 96.44/24.94 , m5(a, b, res, t) -> res 96.44/24.94 , <(x, 0()) -> False() 96.44/24.94 , <(S(x), S(y)) -> <(x, y) 96.44/24.94 , <(0(), S(y)) -> True() 96.44/24.94 , e1(a, b, res, t) -> e2(a, b, res, <(a, b)) 96.44/24.94 , m4(S(x'), S(x), res, t) -> m5(S(x'), S(x), monus(x', x), t) 96.44/24.94 , equal0(a, b) -> e1(a, b, False(), False()) 96.44/24.94 , m2(a, b, res, False()) -> m4(a, b, res, False()) 96.44/24.94 , m2(S(S(x)), b, res, True()) -> True() 96.44/24.94 , m2(S(0()), b, res, True()) -> False() 96.44/24.94 , m2(0(), b, res, True()) -> False() 96.44/24.94 , monus(a, b) -> m1(a, b, False(), False()) 96.44/24.94 , m1(a, x, res, t) -> m2(a, x, res, False()) 96.44/24.94 , e4(a, b, res, True()) -> True() 96.44/24.94 , e4(a, b, res, False()) -> False() } 96.44/24.94 Obligation: 96.44/24.94 innermost runtime complexity 96.44/24.94 Answer: 96.44/24.94 YES(O(1),O(1)) 96.44/24.94 96.44/24.94 No rule is usable, rules are removed from the input problem. 96.44/24.94 96.44/24.94 We are left with following problem, upon which TcT provides the 96.44/24.94 certificate YES(O(1),O(1)). 96.44/24.94 96.44/24.94 Rules: Empty 96.44/24.94 Obligation: 96.44/24.94 innermost runtime complexity 96.44/24.94 Answer: 96.44/24.94 YES(O(1),O(1)) 96.44/24.94 96.44/24.94 Empty rules are trivially bounded 96.44/24.94 96.44/24.94 Hurray, we answered YES(O(1),O(n^1)) 96.60/25.03 EOF