WORST_CASE(Omega(n^1),?)
proof of input_vByDbdPMPh.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 8 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 357 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 55 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 59 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 51 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 28 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 64 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 34 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 56 ms]
        (30) typed CpxTrs


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

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


The TRS R consists of the following rules:

   min(0, y) -> 0
   min(x, 0) -> 0
   min(s(x), s(y)) -> s(min(x, y))
   max(0, y) -> y
   max(x, 0) -> x
   max(s(x), s(y)) -> s(max(x, y))
   twice(0) -> 0
   twice(s(x)) -> s(s(twice(x)))
   -(x, 0) -> x
   -(s(x), s(y)) -> -(x, y)
   p(s(x)) -> x
   f(s(x), s(y)) -> f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   min(0, z0) -> 0
   min(z0, 0) -> 0
   min(s(z0), s(z1)) -> s(min(z0, z1))
   max(0, z0) -> z0
   max(z0, 0) -> z0
   max(s(z0), s(z1)) -> s(max(z0, z1))
   twice(0) -> 0
   twice(s(z0)) -> s(s(twice(z0)))
   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   p(s(z0)) -> z0
   f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))
Tuples:
   MIN(0, z0) -> c
   MIN(z0, 0) -> c1
   MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
   MAX(0, z0) -> c3
   MAX(z0, 0) -> c4
   MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
   TWICE(0) -> c6
   TWICE(s(z0)) -> c7(TWICE(z0))
   -'(z0, 0) -> c8
   -'(s(z0), s(z1)) -> c9(-'(z0, z1))
   P(s(z0)) -> c10
   F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
S tuples:
   MIN(0, z0) -> c
   MIN(z0, 0) -> c1
   MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
   MAX(0, z0) -> c3
   MAX(z0, 0) -> c4
   MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
   TWICE(0) -> c6
   TWICE(s(z0)) -> c7(TWICE(z0))
   -'(z0, 0) -> c8
   -'(s(z0), s(z1)) -> c9(-'(z0, z1))
   P(s(z0)) -> c10
   F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
K tuples:none
Defined Rule Symbols:   min_2, max_2, twice_1, -_2, p_1, f_2

Defined Pair Symbols:   MIN_2, MAX_2, TWICE_1, -'_2, P_1, F_2

Compound Symbols:   c, c1, c2_1, c3, c4, c5_1, c6, c7_1, c8, c9_1, c10, c11_3, c12_3, c13_4


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

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(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(0, z0) -> c
   MIN(z0, 0) -> c1
   MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
   MAX(0, z0) -> c3
   MAX(z0, 0) -> c4
   MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
   TWICE(0) -> c6
   TWICE(s(z0)) -> c7(TWICE(z0))
   -'(z0, 0) -> c8
   -'(s(z0), s(z1)) -> c9(-'(z0, z1))
   P(s(z0)) -> c10
   F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))

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

   min(0, z0) -> 0
   min(z0, 0) -> 0
   min(s(z0), s(z1)) -> s(min(z0, z1))
   max(0, z0) -> z0
   max(z0, 0) -> z0
   max(s(z0), s(z1)) -> s(max(z0, z1))
   twice(0) -> 0
   twice(s(z0)) -> s(s(twice(z0)))
   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   p(s(z0)) -> z0
   f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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

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

(6)
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(0', z0) -> c
   MIN(z0, 0') -> c1
   MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
   MAX(0', z0) -> c3
   MAX(z0, 0') -> c4
   MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
   TWICE(0') -> c6
   TWICE(s(z0)) -> c7(TWICE(z0))
   -'(z0, 0') -> c8
   -'(s(z0), s(z1)) -> c9(-'(z0, z1))
   P(s(z0)) -> c10
   F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
   F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))

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

   min(0', z0) -> 0'
   min(z0, 0') -> 0'
   min(s(z0), s(z1)) -> s(min(z0, z1))
   max(0', z0) -> z0
   max(z0, 0') -> z0
   max(s(z0), s(z1)) -> s(max(z0, z1))
   twice(0') -> 0'
   twice(s(z0)) -> s(s(twice(z0)))
   -(z0, 0') -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   p(s(z0)) -> z0
   f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MIN, MAX, TWICE, -', F, -, max, min, twice, f

They will be analysed ascendingly in the following order:
MIN < F
MAX < F
TWICE < F
-' < F
- < F
max < F
min < F
twice < F
- < f
max < f
min < f
twice < f

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

(10)
Obligation:
Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
MIN, MAX, TWICE, -', F, -, max, min, twice, f

They will be analysed ascendingly in the following order:
MIN < F
MAX < F
TWICE < F
-' < F
- < F
max < F
min < F
twice < F
- < f
max < f
min < f
twice < f

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)

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

Induction Step:
MIN(gen_0':s10_14(+(n16_14, 1)), gen_0':s10_14(+(n16_14, 1))) ->_R^Omega(1)
c2(MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14))) ->_IH
c2(gen_c:c1:c29_14(c17_14))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
MIN, MAX, TWICE, -', F, -, max, min, twice, f

They will be analysed ascendingly in the following order:
MIN < F
MAX < F
TWICE < F
-' < F
- < F
max < F
min < F
twice < F
- < f
max < f
min < f
twice < f

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Lemmas:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
MAX, TWICE, -', F, -, max, min, twice, f

They will be analysed ascendingly in the following order:
MAX < F
TWICE < F
-' < F
- < F
max < F
min < F
twice < F
- < f
max < f
min < f
twice < f

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14)) -> gen_c3:c4:c511_14(n536_14), rt in Omega(1 + n536_14)

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

Induction Step:
MAX(gen_0':s10_14(+(n536_14, 1)), gen_0':s10_14(+(n536_14, 1))) ->_R^Omega(1)
c5(MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14))) ->_IH
c5(gen_c3:c4:c511_14(c537_14))

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(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Lemmas:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)
MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14)) -> gen_c3:c4:c511_14(n536_14), rt in Omega(1 + n536_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
TWICE, -', F, -, max, min, twice, f

They will be analysed ascendingly in the following order:
TWICE < F
-' < F
- < F
max < F
min < F
twice < F
- < f
max < f
min < f
twice < f

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TWICE(gen_0':s10_14(n1131_14)) -> gen_c6:c712_14(n1131_14), rt in Omega(1 + n1131_14)

Induction Base:
TWICE(gen_0':s10_14(0)) ->_R^Omega(1)
c6

Induction Step:
TWICE(gen_0':s10_14(+(n1131_14, 1))) ->_R^Omega(1)
c7(TWICE(gen_0':s10_14(n1131_14))) ->_IH
c7(gen_c6:c712_14(c1132_14))

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

(20)
Obligation:
Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Lemmas:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)
MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14)) -> gen_c3:c4:c511_14(n536_14), rt in Omega(1 + n536_14)
TWICE(gen_0':s10_14(n1131_14)) -> gen_c6:c712_14(n1131_14), rt in Omega(1 + n1131_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
-', F, -, max, min, twice, f

They will be analysed ascendingly in the following order:
-' < F
- < F
max < F
min < F
twice < F
- < f
max < f
min < f
twice < f

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-'(gen_0':s10_14(n1566_14), gen_0':s10_14(n1566_14)) -> gen_c8:c913_14(n1566_14), rt in Omega(1 + n1566_14)

Induction Base:
-'(gen_0':s10_14(0), gen_0':s10_14(0)) ->_R^Omega(1)
c8

Induction Step:
-'(gen_0':s10_14(+(n1566_14, 1)), gen_0':s10_14(+(n1566_14, 1))) ->_R^Omega(1)
c9(-'(gen_0':s10_14(n1566_14), gen_0':s10_14(n1566_14))) ->_IH
c9(gen_c8:c913_14(c1567_14))

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

(22)
Obligation:
Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Lemmas:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)
MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14)) -> gen_c3:c4:c511_14(n536_14), rt in Omega(1 + n536_14)
TWICE(gen_0':s10_14(n1131_14)) -> gen_c6:c712_14(n1131_14), rt in Omega(1 + n1131_14)
-'(gen_0':s10_14(n1566_14), gen_0':s10_14(n1566_14)) -> gen_c8:c913_14(n1566_14), rt in Omega(1 + n1566_14)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
-, F, max, min, twice, f

They will be analysed ascendingly in the following order:
- < F
max < F
min < F
twice < F
- < f
max < f
min < f
twice < f

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

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

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

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

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(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Lemmas:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)
MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14)) -> gen_c3:c4:c511_14(n536_14), rt in Omega(1 + n536_14)
TWICE(gen_0':s10_14(n1131_14)) -> gen_c6:c712_14(n1131_14), rt in Omega(1 + n1131_14)
-'(gen_0':s10_14(n1566_14), gen_0':s10_14(n1566_14)) -> gen_c8:c913_14(n1566_14), rt in Omega(1 + n1566_14)
-(gen_0':s10_14(n2212_14), gen_0':s10_14(n2212_14)) -> gen_0':s10_14(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
max, F, min, twice, f

They will be analysed ascendingly in the following order:
max < F
min < F
twice < F
max < f
min < f
twice < f

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
max(gen_0':s10_14(n3084_14), gen_0':s10_14(n3084_14)) -> gen_0':s10_14(n3084_14), rt in Omega(0)

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

Induction Step:
max(gen_0':s10_14(+(n3084_14, 1)), gen_0':s10_14(+(n3084_14, 1))) ->_R^Omega(0)
s(max(gen_0':s10_14(n3084_14), gen_0':s10_14(n3084_14))) ->_IH
s(gen_0':s10_14(c3085_14))

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

(26)
Obligation:
Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Lemmas:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)
MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14)) -> gen_c3:c4:c511_14(n536_14), rt in Omega(1 + n536_14)
TWICE(gen_0':s10_14(n1131_14)) -> gen_c6:c712_14(n1131_14), rt in Omega(1 + n1131_14)
-'(gen_0':s10_14(n1566_14), gen_0':s10_14(n1566_14)) -> gen_c8:c913_14(n1566_14), rt in Omega(1 + n1566_14)
-(gen_0':s10_14(n2212_14), gen_0':s10_14(n2212_14)) -> gen_0':s10_14(0), rt in Omega(0)
max(gen_0':s10_14(n3084_14), gen_0':s10_14(n3084_14)) -> gen_0':s10_14(n3084_14), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
min, F, twice, f

They will be analysed ascendingly in the following order:
min < F
twice < F
min < f
twice < f

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
min(gen_0':s10_14(n4006_14), gen_0':s10_14(n4006_14)) -> gen_0':s10_14(n4006_14), rt in Omega(0)

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

Induction Step:
min(gen_0':s10_14(+(n4006_14, 1)), gen_0':s10_14(+(n4006_14, 1))) ->_R^Omega(0)
s(min(gen_0':s10_14(n4006_14), gen_0':s10_14(n4006_14))) ->_IH
s(gen_0':s10_14(c4007_14))

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

(28)
Obligation:
Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Lemmas:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)
MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14)) -> gen_c3:c4:c511_14(n536_14), rt in Omega(1 + n536_14)
TWICE(gen_0':s10_14(n1131_14)) -> gen_c6:c712_14(n1131_14), rt in Omega(1 + n1131_14)
-'(gen_0':s10_14(n1566_14), gen_0':s10_14(n1566_14)) -> gen_c8:c913_14(n1566_14), rt in Omega(1 + n1566_14)
-(gen_0':s10_14(n2212_14), gen_0':s10_14(n2212_14)) -> gen_0':s10_14(0), rt in Omega(0)
max(gen_0':s10_14(n3084_14), gen_0':s10_14(n3084_14)) -> gen_0':s10_14(n3084_14), rt in Omega(0)
min(gen_0':s10_14(n4006_14), gen_0':s10_14(n4006_14)) -> gen_0':s10_14(n4006_14), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
twice, F, f

They will be analysed ascendingly in the following order:
twice < F
twice < f

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
twice(gen_0':s10_14(n4610_14)) -> gen_0':s10_14(*(2, n4610_14)), rt in Omega(0)

Induction Base:
twice(gen_0':s10_14(0)) ->_R^Omega(0)
0'

Induction Step:
twice(gen_0':s10_14(+(n4610_14, 1))) ->_R^Omega(0)
s(s(twice(gen_0':s10_14(n4610_14)))) ->_IH
s(s(gen_0':s10_14(*(2, c4611_14))))

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

(30)
Obligation:
Innermost TRS:
Rules:
MIN(0', z0) -> c
MIN(z0, 0') -> c1
MIN(s(z0), s(z1)) -> c2(MIN(z0, z1))
MAX(0', z0) -> c3
MAX(z0, 0') -> c4
MAX(s(z0), s(z1)) -> c5(MAX(z0, z1))
TWICE(0') -> c6
TWICE(s(z0)) -> c7(TWICE(z0))
-'(z0, 0') -> c8
-'(s(z0), s(z1)) -> c9(-'(z0, z1))
P(s(z0)) -> c10
F(s(z0), s(z1)) -> c11(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MAX(s(z0), s(z1)))
F(s(z0), s(z1)) -> c12(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), -'(max(s(z0), s(z1)), min(s(z0), s(z1))), MIN(s(z0), s(z1)))
F(s(z0), s(z1)) -> c13(F(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1)))), P(twice(min(z0, z1))), TWICE(min(z0, z1)), MIN(z0, z1))
min(0', z0) -> 0'
min(z0, 0') -> 0'
min(s(z0), s(z1)) -> s(min(z0, z1))
max(0', z0) -> z0
max(z0, 0') -> z0
max(s(z0), s(z1)) -> s(max(z0, z1))
twice(0') -> 0'
twice(s(z0)) -> s(s(twice(z0)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
p(s(z0)) -> z0
f(s(z0), s(z1)) -> f(-(max(s(z0), s(z1)), min(s(z0), s(z1))), p(twice(min(z0, z1))))

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
TWICE :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
-' :: 0':s -> 0':s -> c8:c9
c8 :: c8:c9
c9 :: c8:c9 -> c8:c9
P :: 0':s -> c10
c10 :: c10
F :: 0':s -> 0':s -> c11:c12:c13
c11 :: c11:c12:c13 -> c8:c9 -> c3:c4:c5 -> c11:c12:c13
- :: 0':s -> 0':s -> 0':s
max :: 0':s -> 0':s -> 0':s
min :: 0':s -> 0':s -> 0':s
p :: 0':s -> 0':s
twice :: 0':s -> 0':s
c12 :: c11:c12:c13 -> c8:c9 -> c:c1:c2 -> c11:c12:c13
c13 :: c11:c12:c13 -> c10 -> c6:c7 -> c:c1:c2 -> c11:c12:c13
f :: 0':s -> 0':s -> f
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s2_14 :: 0':s
hole_c3:c4:c53_14 :: c3:c4:c5
hole_c6:c74_14 :: c6:c7
hole_c8:c95_14 :: c8:c9
hole_c106_14 :: c10
hole_c11:c12:c137_14 :: c11:c12:c13
hole_f8_14 :: f
gen_c:c1:c29_14 :: Nat -> c:c1:c2
gen_0':s10_14 :: Nat -> 0':s
gen_c3:c4:c511_14 :: Nat -> c3:c4:c5
gen_c6:c712_14 :: Nat -> c6:c7
gen_c8:c913_14 :: Nat -> c8:c9
gen_c11:c12:c1314_14 :: Nat -> c11:c12:c13


Lemmas:
MIN(gen_0':s10_14(n16_14), gen_0':s10_14(n16_14)) -> gen_c:c1:c29_14(n16_14), rt in Omega(1 + n16_14)
MAX(gen_0':s10_14(n536_14), gen_0':s10_14(n536_14)) -> gen_c3:c4:c511_14(n536_14), rt in Omega(1 + n536_14)
TWICE(gen_0':s10_14(n1131_14)) -> gen_c6:c712_14(n1131_14), rt in Omega(1 + n1131_14)
-'(gen_0':s10_14(n1566_14), gen_0':s10_14(n1566_14)) -> gen_c8:c913_14(n1566_14), rt in Omega(1 + n1566_14)
-(gen_0':s10_14(n2212_14), gen_0':s10_14(n2212_14)) -> gen_0':s10_14(0), rt in Omega(0)
max(gen_0':s10_14(n3084_14), gen_0':s10_14(n3084_14)) -> gen_0':s10_14(n3084_14), rt in Omega(0)
min(gen_0':s10_14(n4006_14), gen_0':s10_14(n4006_14)) -> gen_0':s10_14(n4006_14), rt in Omega(0)
twice(gen_0':s10_14(n4610_14)) -> gen_0':s10_14(*(2, n4610_14)), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_14(0) <=> c
gen_c:c1:c29_14(+(x, 1)) <=> c2(gen_c:c1:c29_14(x))
gen_0':s10_14(0) <=> 0'
gen_0':s10_14(+(x, 1)) <=> s(gen_0':s10_14(x))
gen_c3:c4:c511_14(0) <=> c3
gen_c3:c4:c511_14(+(x, 1)) <=> c5(gen_c3:c4:c511_14(x))
gen_c6:c712_14(0) <=> c6
gen_c6:c712_14(+(x, 1)) <=> c7(gen_c6:c712_14(x))
gen_c8:c913_14(0) <=> c8
gen_c8:c913_14(+(x, 1)) <=> c9(gen_c8:c913_14(x))
gen_c11:c12:c1314_14(0) <=> hole_c11:c12:c137_14
gen_c11:c12:c1314_14(+(x, 1)) <=> c11(gen_c11:c12:c1314_14(x), c8, c3)


The following defined symbols remain to be analysed:
F, f