WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 596 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 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), 296 ms]
(10) BEST
    (11) proven lower bound
        (12) LowerBoundPropagationProof [FINISHED, 0 ms]
        (13) BOUNDS(n^1, INF)
    (14) typed CpxTrs
        (15) RewriteLemmaProof [LOWER BOUND(ID), 61 ms]
        (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 77 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 57 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 38 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 59 ms]
        (24) typed CpxTrs


----------------------------------------

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


The TRS R consists of the following rules:

   MIN(z0, 0) -> c
   MIN(0, z0) -> c1
   MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
   MAX(z0, 0) -> c3
   MAX(0, z0) -> c4
   MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
   -'(z0, 0) -> c6
   -'(s(z0), s(z1)) -> c7(-'(z0, z1))
   GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
   GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
   GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
   GCD(s(z0), 0) -> c11
   GCD(0, s(z0)) -> c12

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

   min(z0, 0) -> 0
   min(0, z0) -> 0
   min(s(z0), s(z1)) -> s(min(z0, z1))
   max(z0, 0) -> z0
   max(0, z0) -> z0
   max(s(z0), s(z1)) -> s(max(z0, z1))
   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
   gcd(s(z0), 0) -> s(z0)
   gcd(0, s(z0)) -> s(z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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


The TRS R consists of the following rules:

   MIN(z0, 0) -> c
   MIN(0, z0) -> c1
   MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
   MAX(z0, 0) -> c3
   MAX(0, z0) -> c4
   MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
   -'(z0, 0) -> c6
   -'(s(z0), s(z1)) -> c7(-'(z0, z1))
   GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
   GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
   GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
   GCD(s(z0), 0) -> c11
   GCD(0, s(z0)) -> c12

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

   min(z0, 0) -> 0
   min(0, z0) -> 0
   min(s(z0), s(z1)) -> s(min(z0, z1))
   max(z0, 0) -> z0
   max(0, z0) -> z0
   max(s(z0), s(z1)) -> s(max(z0, z1))
   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
   gcd(s(z0), 0) -> s(z0)
   gcd(0, s(z0)) -> s(z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(3) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   MIN(z0, 0') -> c
   MIN(0', z0) -> c1
   MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
   MAX(z0, 0') -> c3
   MAX(0', z0) -> c4
   MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
   -'(z0, 0') -> c6
   -'(s(z0), s(z1)) -> c7(-'(z0, z1))
   GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
   GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
   GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
   GCD(s(z0), 0') -> c11
   GCD(0', s(z0)) -> c12

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

   min(z0, 0') -> 0'
   min(0', z0) -> 0'
   min(s(z0), s(z1)) -> s(min(z0, z1))
   max(z0, 0') -> z0
   max(0', z0) -> z0
   max(s(z0), s(z1)) -> s(max(z0, z1))
   -(z0, 0') -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
   gcd(s(z0), 0') -> s(z0)
   gcd(0', s(z0)) -> s(z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(6)
Obligation:
Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12

----------------------------------------

(7) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MIN, MAX, -', GCD, -, max, min, gcd

They will be analysed ascendingly in the following order:
MIN < GCD
MAX < GCD
-' < GCD
- < GCD
max < GCD
min < GCD
- < gcd
max < gcd
min < gcd

----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(gen_c:c1:c26_13(x))
gen_0':s7_13(0) <=> 0'
gen_0':s7_13(+(x, 1)) <=> s(gen_0':s7_13(x))
gen_c3:c4:c58_13(0) <=> c3
gen_c3:c4:c58_13(+(x, 1)) <=> c5(gen_c3:c4:c58_13(x))
gen_c6:c79_13(0) <=> c6
gen_c6:c79_13(+(x, 1)) <=> c7(gen_c6:c79_13(x))
gen_c8:c9:c10:c11:c1210_13(0) <=> c11
gen_c8:c9:c10:c11:c1210_13(+(x, 1)) <=> c8(gen_c8:c9:c10:c11:c1210_13(x), c6, c3)


The following defined symbols remain to be analysed:
MIN, MAX, -', GCD, -, max, min, gcd

They will be analysed ascendingly in the following order:
MIN < GCD
MAX < GCD
-' < GCD
- < GCD
max < GCD
min < GCD
- < gcd
max < gcd
min < gcd

----------------------------------------

(9) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MIN(gen_0':s7_13(n12_13), gen_0':s7_13(n12_13)) -> gen_c:c1:c26_13(n12_13), rt in Omega(1 + n12_13)

Induction Base:
MIN(gen_0':s7_13(0), gen_0':s7_13(0)) ->_R^Omega(1)
c

Induction Step:
MIN(gen_0':s7_13(+(n12_13, 1)), gen_0':s7_13(+(n12_13, 1))) ->_R^Omega(1)
c2(MIN(gen_0':s7_13(n12_13), gen_0':s7_13(n12_13))) ->_IH
c2(gen_c:c1:c26_13(c13_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(10)
Complex Obligation (BEST)

----------------------------------------

(11)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(gen_c:c1:c26_13(x))
gen_0':s7_13(0) <=> 0'
gen_0':s7_13(+(x, 1)) <=> s(gen_0':s7_13(x))
gen_c3:c4:c58_13(0) <=> c3
gen_c3:c4:c58_13(+(x, 1)) <=> c5(gen_c3:c4:c58_13(x))
gen_c6:c79_13(0) <=> c6
gen_c6:c79_13(+(x, 1)) <=> c7(gen_c6:c79_13(x))
gen_c8:c9:c10:c11:c1210_13(0) <=> c11
gen_c8:c9:c10:c11:c1210_13(+(x, 1)) <=> c8(gen_c8:c9:c10:c11:c1210_13(x), c6, c3)


The following defined symbols remain to be analysed:
MIN, MAX, -', GCD, -, max, min, gcd

They will be analysed ascendingly in the following order:
MIN < GCD
MAX < GCD
-' < GCD
- < GCD
max < GCD
min < GCD
- < gcd
max < gcd
min < gcd

----------------------------------------

(12) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(13)
BOUNDS(n^1, INF)

----------------------------------------

(14)
Obligation:
Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12


Lemmas:
MIN(gen_0':s7_13(n12_13), gen_0':s7_13(n12_13)) -> gen_c:c1:c26_13(n12_13), rt in Omega(1 + n12_13)


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(gen_c:c1:c26_13(x))
gen_0':s7_13(0) <=> 0'
gen_0':s7_13(+(x, 1)) <=> s(gen_0':s7_13(x))
gen_c3:c4:c58_13(0) <=> c3
gen_c3:c4:c58_13(+(x, 1)) <=> c5(gen_c3:c4:c58_13(x))
gen_c6:c79_13(0) <=> c6
gen_c6:c79_13(+(x, 1)) <=> c7(gen_c6:c79_13(x))
gen_c8:c9:c10:c11:c1210_13(0) <=> c11
gen_c8:c9:c10:c11:c1210_13(+(x, 1)) <=> c8(gen_c8:c9:c10:c11:c1210_13(x), c6, c3)


The following defined symbols remain to be analysed:
MAX, -', GCD, -, max, min, gcd

They will be analysed ascendingly in the following order:
MAX < GCD
-' < GCD
- < GCD
max < GCD
min < GCD
- < gcd
max < gcd
min < gcd

----------------------------------------

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MAX(gen_0':s7_13(n508_13), gen_0':s7_13(n508_13)) -> gen_c3:c4:c58_13(n508_13), rt in Omega(1 + n508_13)

Induction Base:
MAX(gen_0':s7_13(0), gen_0':s7_13(0)) ->_R^Omega(1)
c3

Induction Step:
MAX(gen_0':s7_13(+(n508_13, 1)), gen_0':s7_13(+(n508_13, 1))) ->_R^Omega(1)
c5(MAX(gen_0':s7_13(n508_13), gen_0':s7_13(n508_13))) ->_IH
c5(gen_c3:c4:c58_13(c509_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12


Lemmas:
MIN(gen_0':s7_13(n12_13), gen_0':s7_13(n12_13)) -> gen_c:c1:c26_13(n12_13), rt in Omega(1 + n12_13)
MAX(gen_0':s7_13(n508_13), gen_0':s7_13(n508_13)) -> gen_c3:c4:c58_13(n508_13), rt in Omega(1 + n508_13)


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(gen_c:c1:c26_13(x))
gen_0':s7_13(0) <=> 0'
gen_0':s7_13(+(x, 1)) <=> s(gen_0':s7_13(x))
gen_c3:c4:c58_13(0) <=> c3
gen_c3:c4:c58_13(+(x, 1)) <=> c5(gen_c3:c4:c58_13(x))
gen_c6:c79_13(0) <=> c6
gen_c6:c79_13(+(x, 1)) <=> c7(gen_c6:c79_13(x))
gen_c8:c9:c10:c11:c1210_13(0) <=> c11
gen_c8:c9:c10:c11:c1210_13(+(x, 1)) <=> c8(gen_c8:c9:c10:c11:c1210_13(x), c6, c3)


The following defined symbols remain to be analysed:
-', GCD, -, max, min, gcd

They will be analysed ascendingly in the following order:
-' < GCD
- < GCD
max < GCD
min < GCD
- < gcd
max < gcd
min < gcd

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-'(gen_0':s7_13(n1079_13), gen_0':s7_13(n1079_13)) -> gen_c6:c79_13(n1079_13), rt in Omega(1 + n1079_13)

Induction Base:
-'(gen_0':s7_13(0), gen_0':s7_13(0)) ->_R^Omega(1)
c6

Induction Step:
-'(gen_0':s7_13(+(n1079_13, 1)), gen_0':s7_13(+(n1079_13, 1))) ->_R^Omega(1)
c7(-'(gen_0':s7_13(n1079_13), gen_0':s7_13(n1079_13))) ->_IH
c7(gen_c6:c79_13(c1080_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12


Lemmas:
MIN(gen_0':s7_13(n12_13), gen_0':s7_13(n12_13)) -> gen_c:c1:c26_13(n12_13), rt in Omega(1 + n12_13)
MAX(gen_0':s7_13(n508_13), gen_0':s7_13(n508_13)) -> gen_c3:c4:c58_13(n508_13), rt in Omega(1 + n508_13)
-'(gen_0':s7_13(n1079_13), gen_0':s7_13(n1079_13)) -> gen_c6:c79_13(n1079_13), rt in Omega(1 + n1079_13)


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(gen_c:c1:c26_13(x))
gen_0':s7_13(0) <=> 0'
gen_0':s7_13(+(x, 1)) <=> s(gen_0':s7_13(x))
gen_c3:c4:c58_13(0) <=> c3
gen_c3:c4:c58_13(+(x, 1)) <=> c5(gen_c3:c4:c58_13(x))
gen_c6:c79_13(0) <=> c6
gen_c6:c79_13(+(x, 1)) <=> c7(gen_c6:c79_13(x))
gen_c8:c9:c10:c11:c1210_13(0) <=> c11
gen_c8:c9:c10:c11:c1210_13(+(x, 1)) <=> c8(gen_c8:c9:c10:c11:c1210_13(x), c6, c3)


The following defined symbols remain to be analysed:
-, GCD, max, min, gcd

They will be analysed ascendingly in the following order:
- < GCD
max < GCD
min < GCD
- < gcd
max < gcd
min < gcd

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-(gen_0':s7_13(n1660_13), gen_0':s7_13(n1660_13)) -> gen_0':s7_13(0), rt in Omega(0)

Induction Base:
-(gen_0':s7_13(0), gen_0':s7_13(0)) ->_R^Omega(0)
gen_0':s7_13(0)

Induction Step:
-(gen_0':s7_13(+(n1660_13, 1)), gen_0':s7_13(+(n1660_13, 1))) ->_R^Omega(0)
-(gen_0':s7_13(n1660_13), gen_0':s7_13(n1660_13)) ->_IH
gen_0':s7_13(0)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12


Lemmas:
MIN(gen_0':s7_13(n12_13), gen_0':s7_13(n12_13)) -> gen_c:c1:c26_13(n12_13), rt in Omega(1 + n12_13)
MAX(gen_0':s7_13(n508_13), gen_0':s7_13(n508_13)) -> gen_c3:c4:c58_13(n508_13), rt in Omega(1 + n508_13)
-'(gen_0':s7_13(n1079_13), gen_0':s7_13(n1079_13)) -> gen_c6:c79_13(n1079_13), rt in Omega(1 + n1079_13)
-(gen_0':s7_13(n1660_13), gen_0':s7_13(n1660_13)) -> gen_0':s7_13(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(gen_c:c1:c26_13(x))
gen_0':s7_13(0) <=> 0'
gen_0':s7_13(+(x, 1)) <=> s(gen_0':s7_13(x))
gen_c3:c4:c58_13(0) <=> c3
gen_c3:c4:c58_13(+(x, 1)) <=> c5(gen_c3:c4:c58_13(x))
gen_c6:c79_13(0) <=> c6
gen_c6:c79_13(+(x, 1)) <=> c7(gen_c6:c79_13(x))
gen_c8:c9:c10:c11:c1210_13(0) <=> c11
gen_c8:c9:c10:c11:c1210_13(+(x, 1)) <=> c8(gen_c8:c9:c10:c11:c1210_13(x), c6, c3)


The following defined symbols remain to be analysed:
max, GCD, min, gcd

They will be analysed ascendingly in the following order:
max < GCD
min < GCD
max < gcd
min < gcd

----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
max(gen_0':s7_13(n2432_13), gen_0':s7_13(n2432_13)) -> gen_0':s7_13(n2432_13), rt in Omega(0)

Induction Base:
max(gen_0':s7_13(0), gen_0':s7_13(0)) ->_R^Omega(0)
gen_0':s7_13(0)

Induction Step:
max(gen_0':s7_13(+(n2432_13, 1)), gen_0':s7_13(+(n2432_13, 1))) ->_R^Omega(0)
s(max(gen_0':s7_13(n2432_13), gen_0':s7_13(n2432_13))) ->_IH
s(gen_0':s7_13(c2433_13))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12


Lemmas:
MIN(gen_0':s7_13(n12_13), gen_0':s7_13(n12_13)) -> gen_c:c1:c26_13(n12_13), rt in Omega(1 + n12_13)
MAX(gen_0':s7_13(n508_13), gen_0':s7_13(n508_13)) -> gen_c3:c4:c58_13(n508_13), rt in Omega(1 + n508_13)
-'(gen_0':s7_13(n1079_13), gen_0':s7_13(n1079_13)) -> gen_c6:c79_13(n1079_13), rt in Omega(1 + n1079_13)
-(gen_0':s7_13(n1660_13), gen_0':s7_13(n1660_13)) -> gen_0':s7_13(0), rt in Omega(0)
max(gen_0':s7_13(n2432_13), gen_0':s7_13(n2432_13)) -> gen_0':s7_13(n2432_13), rt in Omega(0)


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(gen_c:c1:c26_13(x))
gen_0':s7_13(0) <=> 0'
gen_0':s7_13(+(x, 1)) <=> s(gen_0':s7_13(x))
gen_c3:c4:c58_13(0) <=> c3
gen_c3:c4:c58_13(+(x, 1)) <=> c5(gen_c3:c4:c58_13(x))
gen_c6:c79_13(0) <=> c6
gen_c6:c79_13(+(x, 1)) <=> c7(gen_c6:c79_13(x))
gen_c8:c9:c10:c11:c1210_13(0) <=> c11
gen_c8:c9:c10:c11:c1210_13(+(x, 1)) <=> c8(gen_c8:c9:c10:c11:c1210_13(x), c6, c3)


The following defined symbols remain to be analysed:
min, GCD, gcd

They will be analysed ascendingly in the following order:
min < GCD
min < gcd

----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
min(gen_0':s7_13(n3285_13), gen_0':s7_13(n3285_13)) -> gen_0':s7_13(n3285_13), rt in Omega(0)

Induction Base:
min(gen_0':s7_13(0), gen_0':s7_13(0)) ->_R^Omega(0)
0'

Induction Step:
min(gen_0':s7_13(+(n3285_13, 1)), gen_0':s7_13(+(n3285_13, 1))) ->_R^Omega(0)
s(min(gen_0':s7_13(n3285_13), gen_0':s7_13(n3285_13))) ->_IH
s(gen_0':s7_13(c3286_13))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
MIN(z0, 0') -> c
MIN(0', z0) -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(z0, 0') -> c3
MAX(0', z0) -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
-'(z0, 0') -> c6
-'(s(z0), s(z1)) -> c7(-'(z0, z1))
GCD(s(z0), s(z1)) -> c8(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MAX(z0, z1))
GCD(s(z0), s(z1)) -> c9(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), -'(s(max(z0, z1)), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), s(z1)) -> c10(GCD(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1))), MIN(z0, z1))
GCD(s(z0), 0') -> c11
GCD(0', s(z0)) -> c12
min(z0, 0') -> 0'
min(0', z0) -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(z0, 0') -> z0
max(0', z0) -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
gcd(s(z0), s(z1)) -> gcd(-(s(max(z0, z1)), s(min(z0, z1))), s(min(z0, z1)))
gcd(s(z0), 0') -> s(z0)
gcd(0', s(z0)) -> s(z0)

Types:
MIN :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
c1 :: c:c1:c2
s :: 0':s -> 0':s
c2 :: c:c1:c2 -> c:c1:c2
MAX :: 0':s -> 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
-' :: 0':s -> 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
GCD :: 0':s -> 0':s -> c8:c9:c10:c11:c12
c8 :: c8:c9:c10:c11:c12 -> c6:c7 -> c3:c4:c5 -> c8:c9:c10:c11:c12
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
c9 :: c8:c9:c10:c11:c12 -> c6:c7 -> c:c1:c2 -> c8:c9:c10:c11:c12
c10 :: c8:c9:c10:c11:c12 -> c:c1:c2 -> c8:c9:c10:c11:c12
c11 :: c8:c9:c10:c11:c12
c12 :: c8:c9:c10:c11:c12
gcd :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c8:c9:c10:c11:c125_13 :: c8:c9:c10:c11:c12
gen_c:c1:c26_13 :: Nat -> c:c1:c2
gen_0':s7_13 :: Nat -> 0':s
gen_c3:c4:c58_13 :: Nat -> c3:c4:c5
gen_c6:c79_13 :: Nat -> c6:c7
gen_c8:c9:c10:c11:c1210_13 :: Nat -> c8:c9:c10:c11:c12


Lemmas:
MIN(gen_0':s7_13(n12_13), gen_0':s7_13(n12_13)) -> gen_c:c1:c26_13(n12_13), rt in Omega(1 + n12_13)
MAX(gen_0':s7_13(n508_13), gen_0':s7_13(n508_13)) -> gen_c3:c4:c58_13(n508_13), rt in Omega(1 + n508_13)
-'(gen_0':s7_13(n1079_13), gen_0':s7_13(n1079_13)) -> gen_c6:c79_13(n1079_13), rt in Omega(1 + n1079_13)
-(gen_0':s7_13(n1660_13), gen_0':s7_13(n1660_13)) -> gen_0':s7_13(0), rt in Omega(0)
max(gen_0':s7_13(n2432_13), gen_0':s7_13(n2432_13)) -> gen_0':s7_13(n2432_13), rt in Omega(0)
min(gen_0':s7_13(n3285_13), gen_0':s7_13(n3285_13)) -> gen_0':s7_13(n3285_13), rt in Omega(0)


Generator Equations:
gen_c:c1:c26_13(0) <=> c
gen_c:c1:c26_13(+(x, 1)) <=> c2(gen_c:c1:c26_13(x))
gen_0':s7_13(0) <=> 0'
gen_0':s7_13(+(x, 1)) <=> s(gen_0':s7_13(x))
gen_c3:c4:c58_13(0) <=> c3
gen_c3:c4:c58_13(+(x, 1)) <=> c5(gen_c3:c4:c58_13(x))
gen_c6:c79_13(0) <=> c6
gen_c6:c79_13(+(x, 1)) <=> c7(gen_c6:c79_13(x))
gen_c8:c9:c10:c11:c1210_13(0) <=> c11
gen_c8:c9:c10:c11:c1210_13(+(x, 1)) <=> c8(gen_c8:c9:c10:c11:c1210_13(x), c6, c3)


The following defined symbols remain to be analysed:
GCD, gcd