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