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