Runtime Complexity (innermost) proof of /tmp/tmp8guMW3/gexgcd.xml

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

0 CpxRelTRS

↳1 RenamingProof (⇔, 0 ms)

↳2 CpxRelTRS

↳3 SlicingProof (LOWER BOUND(ID), 28 ms)

↳4 CpxRelTRS

↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 typed CpxTrs

↳7 OrderProof (LOWER BOUND(ID), 0 ms)

↳8 typed CpxTrs

↳9 RewriteLemmaProof (LOWER BOUND(ID), 433 ms)

↳10 BEST

    ↳11 typed CpxTrs

        ↳12 RewriteLemmaProof (LOWER BOUND(ID), 193 ms)

        ↳13 BEST

            ↳14 typed CpxTrs

                ↳15 RewriteLemmaProof (LOWER BOUND(ID), 131 ms)

                ↳16 BEST

                    ↳17 typed CpxTrs

                        ↳18 RewriteLemmaProof (LOWER BOUND(ID), 126 ms)

                        ↳19 BEST

                            ↳20 typed CpxTrs

                                ↳21 RewriteLemmaProof (LOWER BOUND(ID), 118 ms)

                                ↳22 BEST

                                    ↳23 typed CpxTrs

                                        ↳24 RewriteLemmaProof (LOWER BOUND(ID), 109 ms)

                                        ↳25 BEST

                                            ↳26 typed CpxTrs

                                                ↳27 NoRewriteLemmaProof (LOWER BOUND(ID), 847 ms)

                                                ↳28 typed CpxTrs

                                                ↳29 NoRewriteLemmaProof (LOWER BOUND(ID), 235 ms)

                                                ↳30 typed CpxTrs

                                                ↳31 NoRewriteLemmaProof (LOWER BOUND(ID), 201 ms)

                                                ↳32 typed CpxTrs

                                                ↳33 NoRewriteLemmaProof (LOWER BOUND(ID), 190 ms)

                                                ↳34 typed CpxTrs

                                                ↳35 NoRewriteLemmaProof (LOWER BOUND(ID), 189 ms)

                                                ↳36 typed CpxTrs

                                                ↳37 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)

                                                ↳38 typed CpxTrs

                                                ↳39 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)

                                                ↳40 typed CpxTrs

                                                ↳41 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)

                                                ↳42 typed CpxTrs

                                                ↳43 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)

                                                ↳44 typed CpxTrs

                                                ↳45 LowerBoundsProof (⇔, 0 ms)

                                                ↳46 BOUNDS(n^1, INF)

                                            ↳47 typed CpxTrs

                                                ↳48 LowerBoundsProof (⇔, 0 ms)

                                                ↳49 BOUNDS(n^1, INF)

                                    ↳50 typed CpxTrs

                                        ↳51 LowerBoundsProof (⇔, 0 ms)

                                        ↳52 BOUNDS(n^1, INF)

                            ↳53 typed CpxTrs

                                ↳54 LowerBoundsProof (⇔, 0 ms)

                                ↳55 BOUNDS(n^1, INF)

                    ↳56 typed CpxTrs

                        ↳57 LowerBoundsProof (⇔, 0 ms)

                        ↳58 BOUNDS(n^1, INF)

            ↳59 typed CpxTrs

                ↳60 LowerBoundsProof (⇔, 0 ms)

                ↳61 BOUNDS(n^1, INF)

    ↳62 typed CpxTrs

        ↳63 LowerBoundsProof (⇔, 0 ms)

        ↳64 BOUNDS(1, INF)

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

m2(S(0), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0, b, res, True) → False
m3(S(0), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0, b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0
help1(S(0)) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0)), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0, y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0) → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0, tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0, False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
l15(x, y, res, tmp, False, t) → l16(x, y, gcd(y, 0'), tmp, False, t)
l15(x, y, res, tmp, True, t) → l16(x, y, gcd(y, S(0')), tmp, True, t)
l13(x, y, res, tmp, False, t) → l16(x, y, gcd(0', y), tmp, False, t)
l13(x, y, res, tmp, True, t) → l16(x, y, gcd(S(0'), y), tmp, True, t)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
l11(x, y, res, tmp, mtmp, False) → l14(x, y, res, tmp, mtmp, False)
l11(x, y, res, tmp, mtmp, True) → l12(x, y, res, tmp, mtmp, True)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Rewrite Strategy: INNERMOST

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
m2/2
m3/1
m3/2
m3/3
l8/2
l8/4
l8/5
l5/2
l5/3
l5/4
e4/0
e4/1
e4/2
e2/2
l15/0
l15/2
l15/3
l15/5
l16/0
l16/1
l16/3
l16/4
l16/5
l13/0
l13/2
l13/3
l13/5
m4/2
m4/3
m5/0
m5/1
m5/3
l10/2
l10/3
l10/4
l10/5
l7/2
l7/3
l7/4
l7/5
l2/3
l2/4
l3/2
l3/3
l3/4
l3/5
l11/2
l11/3
l11/4
l14/2
l14/3
l14/4
l14/5
l12/2
l12/3
l12/4
l12/5
e3/2
e3/3
m1/2
m1/3
l9/1
l9/2
l9/3
l9/4
l9/5
l6/0
l6/1
l6/2
l6/3
l6/4
l6/5
l4/2
l4/3
l4/4
l4/5
l1/3
l1/4
l1/5
e7/0
e7/1
e7/2
e7/3
e6/0
e6/1
e6/2
e6/3
e5/0
e5/1
e5/2
e5/3
e1/2
e1/3
e8/0
e8/1
e8/3

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

m2(S(0'), b, True) → False
m2(S(S(x)), b, True) → True
m2(0', b, True) → False
m3(S(0')) → False
m3(S(S(x))) → True
m3(0') → False
l8(res, y, True) → res
l5(x, y, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(False) → False
e4(True) → True
e2(a, b, False) → False
l15(y, False) → l16(gcd(y, 0'))
l15(y, True) → l16(gcd(y, S(0')))
l13(y, False) → l16(gcd(0', y))
l13(y, True) → l16(gcd(S(0'), y))
m4(S(x'), S(x)) → m5(monus(x', x))
m2(a, b, False) → m4(a, b)
l8(x, y, False) → l10(x, y)
l5(x, y, False) → l7(x, y)
l2(x, y, res, False) → l3(x, y)
l2(x, y, res, True) → res
l11(x, y, False) → l14(x, y)
l11(x, y, True) → l12(x, y)
help1(0') → False
e2(a, b, True) → e3(a, b)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x) → m2(a, x, False)
l9(res) → res
l6 → 0'
l4(x', x) → l5(x', x, False)
l1(x, y, res) → l2(x, y, res, False)
e7 → False
e6 → False
e5 → True
monus(a, b) → m1(a, b)
m5(res) → res
l7(x, y) → l8(x, y, equal0(x, y))
l3(x, y) → l4(x, y)
l16(res) → res
l14(x, y) → l15(y, monus(x, y))
l12(x, y) → l13(y, monus(x, y))
l10(x, y) → l11(x, y, <(x, y))
gcd(x, y) → l1(x, y, 0')
equal0(a, b) → e1(a, b)
e8(res) → res
e3(a, b) → e4(<(b, a))
e1(a, b) → e2(a, b, <(a, b))

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
m2(S(0'), b, True) → False
m2(S(S(x)), b, True) → True
m2(0', b, True) → False
m3(S(0')) → False
m3(S(S(x))) → True
m3(0') → False
l8(res, y, True) → res
l5(x, y, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(False) → False
e4(True) → True
e2(a, b, False) → False
l15(y, False) → l16(gcd(y, 0'))
l15(y, True) → l16(gcd(y, S(0')))
l13(y, False) → l16(gcd(0', y))
l13(y, True) → l16(gcd(S(0'), y))
m4(S(x'), S(x)) → m5(monus(x', x))
m2(a, b, False) → m4(a, b)
l8(x, y, False) → l10(x, y)
l5(x, y, False) → l7(x, y)
l2(x, y, res, False) → l3(x, y)
l2(x, y, res, True) → res
l11(x, y, False) → l14(x, y)
l11(x, y, True) → l12(x, y)
help1(0') → False
e2(a, b, True) → e3(a, b)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x) → m2(a, x, False)
l9(res) → res
l6 → 0'
l4(x', x) → l5(x', x, False)
l1(x, y, res) → l2(x, y, res, False)
e7 → False
e6 → False
e5 → True
monus(a, b) → m1(a, b)
m5(res) → res
l7(x, y) → l8(x, y, equal0(x, y))
l3(x, y) → l4(x, y)
l16(res) → res
l14(x, y) → l15(y, monus(x, y))
l12(x, y) → l13(y, monus(x, y))
l10(x, y) → l11(x, y, <(x, y))
gcd(x, y) → l1(x, y, 0')
equal0(a, b) → e1(a, b)
e8(res) → res
e3(a, b) → e4(<(b, a))
e1(a, b) → e2(a, b, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False

Types:
m2 :: 0':S → 0':S → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → True:False
l8 :: 0':S → 0':S → True:False → 0':S
l5 :: 0':S → 0':S → True:False → 0':S
help1 :: 0':S → True:False
e4 :: True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False
l15 :: 0':S → True:False → 0':S
l16 :: 0':S → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → True:False → 0':S
m4 :: 0':S → 0':S → True:False
m5 :: True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S
l7 :: 0':S → 0':S → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → 0':S
l3 :: 0':S → 0':S → 0':S
l11 :: 0':S → 0':S → True:False → 0':S
l14 :: 0':S → 0':S → 0':S
l12 :: 0':S → 0':S → 0':S
e3 :: 0':S → 0':S → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False
l9 :: l9 → l9
l6 :: 0':S
l4 :: 0':S → 0':S → 0':S
l1 :: 0':S → 0':S → 0':S → 0':S
e7 :: True:False
e6 :: True:False
e5 :: True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False
e8 :: e8 → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_l93_17 :: l9
hole_e84_17 :: e8
gen_0':S5_17 :: Nat → 0':S

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
l15, gcd, l13, m4, monus, l10, l7, l3, l14, l12, m1, l4, <

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m1
monus < l14
monus < l12
monus = m1
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
< < l10
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(8) Obligation:

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
<, l15, gcd, l13, m4, monus, l10, l7, l3, l14, l12, m1, l4

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)

Induction Base:
<(gen_0':S5_17(0), gen_0':S5_17(+(1, 0))) →_R^Ω(0)
True

Induction Step:
<(gen_0':S5_17(+(n7_17, 1)), gen_0':S5_17(+(1, +(n7_17, 1)))) →_R^Ω(0)
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) →_IH
True

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n⁰).

(10) Complex Obligation (BEST)

(11) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
monus, l15, gcd, l13, m4, l10, l7, l3, l14, l12, m1, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m1
monus < l14
monus < l12
monus = m1
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
monus(gen_0':S5_17(n644_17), gen_0':S5_17(n644_17)) → *6_17, rt ∈ Ω(n644₁₇)

Induction Base:
monus(gen_0':S5_17(0), gen_0':S5_17(0))

Induction Step:
monus(gen_0':S5_17(+(n644_17, 1)), gen_0':S5_17(+(n644_17, 1))) →_R^Ω(1)
m1(gen_0':S5_17(+(n644_17, 1)), gen_0':S5_17(+(n644_17, 1))) →_R^Ω(1)
m2(gen_0':S5_17(+(1, n644_17)), gen_0':S5_17(+(1, n644_17)), False) →_R^Ω(1)
m4(gen_0':S5_17(+(1, n644_17)), gen_0':S5_17(+(1, n644_17))) →_R^Ω(1)
m5(monus(gen_0':S5_17(n644_17), gen_0':S5_17(n644_17))) →_IH
m5(*6_17)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(13) Complex Obligation (BEST)

(14) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n644_17), gen_0':S5_17(n644_17)) → *6_17, rt ∈ Ω(n644₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
m1, l15, gcd, l13, m4, l10, l7, l3, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m1
monus < l14
monus < l12
monus = m1
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
m1(gen_0':S5_17(n2564_17), gen_0':S5_17(n2564_17)) → *6_17, rt ∈ Ω(n2564₁₇)

Induction Base:
m1(gen_0':S5_17(0), gen_0':S5_17(0))

Induction Step:
m1(gen_0':S5_17(+(n2564_17, 1)), gen_0':S5_17(+(n2564_17, 1))) →_R^Ω(1)
m2(gen_0':S5_17(+(n2564_17, 1)), gen_0':S5_17(+(n2564_17, 1)), False) →_R^Ω(1)
m4(gen_0':S5_17(+(1, n2564_17)), gen_0':S5_17(+(1, n2564_17))) →_R^Ω(1)
m5(monus(gen_0':S5_17(n2564_17), gen_0':S5_17(n2564_17))) →_R^Ω(1)
m5(m1(gen_0':S5_17(n2564_17), gen_0':S5_17(n2564_17))) →_IH
m5(*6_17)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(16) Complex Obligation (BEST)

(17) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n644_17), gen_0':S5_17(n644_17)) → *6_17, rt ∈ Ω(n644₁₇)
m1(gen_0':S5_17(n2564_17), gen_0':S5_17(n2564_17)) → *6_17, rt ∈ Ω(n2564₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
m4, l15, gcd, l13, monus, l10, l7, l3, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m1
monus < l14
monus < l12
monus = m1
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Induction Base:
m4(gen_0':S5_17(+(1, 0)), gen_0':S5_17(+(1, 0)))

Induction Step:
m4(gen_0':S5_17(+(1, +(n4548_17, 1))), gen_0':S5_17(+(1, +(n4548_17, 1)))) →_R^Ω(1)
m5(monus(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17)))) →_R^Ω(1)
m5(m1(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17)))) →_R^Ω(1)
m5(m2(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17)), False)) →_R^Ω(1)
m5(m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17)))) →_IH
m5(*6_17)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(19) Complex Obligation (BEST)

(20) Obligation:

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
monus, l15, gcd, l13, l10, l7, l3, l14, l12, m1, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m1
monus < l14
monus < l12
monus = m1
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(21) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)

Induction Base:
monus(gen_0':S5_17(0), gen_0':S5_17(0))

Induction Step:
monus(gen_0':S5_17(+(n7092_17, 1)), gen_0':S5_17(+(n7092_17, 1))) →_R^Ω(1)
m1(gen_0':S5_17(+(n7092_17, 1)), gen_0':S5_17(+(n7092_17, 1))) →_R^Ω(1)
m2(gen_0':S5_17(+(1, n7092_17)), gen_0':S5_17(+(1, n7092_17)), False) →_R^Ω(1)
m4(gen_0':S5_17(+(1, n7092_17)), gen_0':S5_17(+(1, n7092_17))) →_R^Ω(1)
m5(monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17))) →_IH
m5(*6_17)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(22) Complex Obligation (BEST)

(23) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n2564_17), gen_0':S5_17(n2564_17)) → *6_17, rt ∈ Ω(n2564₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
m1, l15, gcd, l13, l10, l7, l3, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m1
monus < l14
monus < l12
monus = m1
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(24) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)

Induction Base:
m1(gen_0':S5_17(0), gen_0':S5_17(0))

Induction Step:
m1(gen_0':S5_17(+(n9684_17, 1)), gen_0':S5_17(+(n9684_17, 1))) →_R^Ω(1)
m2(gen_0':S5_17(+(n9684_17, 1)), gen_0':S5_17(+(n9684_17, 1)), False) →_R^Ω(1)
m4(gen_0':S5_17(+(1, n9684_17)), gen_0':S5_17(+(1, n9684_17))) →_R^Ω(1)
m5(monus(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17))) →_R^Ω(1)
m5(m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17))) →_IH
m5(*6_17)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(25) Complex Obligation (BEST)

(26) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
gcd, l15, l13, l10, l7, l3, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol gcd.

(28) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
l3, l15, l13, l10, l7, l14, l12, l4

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(29) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l3.

(30) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
l4, l15, l13, l10, l7, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(31) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l4.

(32) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
l7, l15, l13, l10, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(33) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l7.

(34) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
l10, l15, l13, l14, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(35) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l10.

(36) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
l14, l15, l13, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(37) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l14.

(38) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
l15, l13, l12

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(39) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l15.

(40) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
l12, l13

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(41) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l12.

(42) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

The following defined symbols remain to be analysed:
l13

They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l10
l15 = l7
l15 = l3
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l10
gcd = l7
gcd = l3
gcd = l14
gcd = l12
gcd = l4
l13 = l10
l13 = l7
l13 = l3
l13 = l14
l13 = l12
l13 = l4
l10 = l7
l10 = l3
l10 = l14
l10 = l12
l10 = l4
l7 = l3
l7 = l14
l7 = l12
l7 = l4
l3 = l14
l3 = l12
l3 = l4
l14 = l12
l14 = l4
l12 = l4

(43) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol l13.

(44) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

No more defined symbols left to analyse.

(45) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)

(46) BOUNDS(n^1, INF)

(47) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)
m1(gen_0':S5_17(n9684_17), gen_0':S5_17(n9684_17)) → *6_17, rt ∈ Ω(n9684₁₇)
m4(gen_0':S5_17(+(1, n4548_17)), gen_0':S5_17(+(1, n4548_17))) → *6_17, rt ∈ Ω(n4548₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

No more defined symbols left to analyse.

(48) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)

(49) BOUNDS(n^1, INF)

(50) Obligation:

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

No more defined symbols left to analyse.

(51) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
monus(gen_0':S5_17(n7092_17), gen_0':S5_17(n7092_17)) → *6_17, rt ∈ Ω(n7092₁₇)

(52) BOUNDS(n^1, INF)

(53) Obligation:

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

No more defined symbols left to analyse.

(54) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
monus(gen_0':S5_17(n644_17), gen_0':S5_17(n644_17)) → *6_17, rt ∈ Ω(n644₁₇)

(55) BOUNDS(n^1, INF)

(56) Obligation:

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

No more defined symbols left to analyse.

(57) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
monus(gen_0':S5_17(n644_17), gen_0':S5_17(n644_17)) → *6_17, rt ∈ Ω(n644₁₇)

(58) BOUNDS(n^1, INF)

(59) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)
monus(gen_0':S5_17(n644_17), gen_0':S5_17(n644_17)) → *6_17, rt ∈ Ω(n644₁₇)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

No more defined symbols left to analyse.

(60) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
monus(gen_0':S5_17(n644_17), gen_0':S5_17(n644_17)) → *6_17, rt ∈ Ω(n644₁₇)

(61) BOUNDS(n^1, INF)

(62) Obligation:

Lemmas:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)

Generator Equations:
gen_0':S5_17(0) ⇔ 0'
gen_0':S5_17(+(x, 1)) ⇔ S(gen_0':S5_17(x))

No more defined symbols left to analyse.

(63) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
<(gen_0':S5_17(n7_17), gen_0':S5_17(+(1, n7_17))) → True, rt ∈ Ω(0)

(0) Obligation:

(1) RenamingProof (EQUIVALENT transformation)

(2) Obligation:

(3) SlicingProof (LOWER BOUND(ID) transformation)

(4) Obligation:

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) OrderProof (LOWER BOUND(ID) transformation)

(8) Obligation:

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(10) Complex Obligation (BEST)

(11) Obligation:

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(13) Complex Obligation (BEST)

(14) Obligation:

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(16) Complex Obligation (BEST)

(17) Obligation:

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(19) Complex Obligation (BEST)

(20) Obligation:

(21) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(22) Complex Obligation (BEST)

(23) Obligation:

(24) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(25) Complex Obligation (BEST)

(26) Obligation:

(27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(28) Obligation:

(29) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(30) Obligation:

(31) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(32) Obligation:

(33) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(34) Obligation:

(35) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(36) Obligation:

(37) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(38) Obligation:

(39) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(40) Obligation:

(41) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(42) Obligation:

(43) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(44) Obligation:

(45) LowerBoundsProof (EQUIVALENT transformation)

(46) BOUNDS(n^1, INF)

(47) Obligation:

(48) LowerBoundsProof (EQUIVALENT transformation)

(49) BOUNDS(n^1, INF)

(50) Obligation:

(51) LowerBoundsProof (EQUIVALENT transformation)

(52) BOUNDS(n^1, INF)

(53) Obligation:

(54) LowerBoundsProof (EQUIVALENT transformation)

(55) BOUNDS(n^1, INF)

(56) Obligation:

(57) LowerBoundsProof (EQUIVALENT transformation)

(58) BOUNDS(n^1, INF)

(59) Obligation:

(60) LowerBoundsProof (EQUIVALENT transformation)

(61) BOUNDS(n^1, INF)

(62) Obligation:

(63) LowerBoundsProof (EQUIVALENT transformation)

(64) BOUNDS(1, INF)