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), 413 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 9 ms]
(6) typed CpxTrs
(7) OrderProof [LOWER BOUND(ID), 0 ms]
(8) typed CpxTrs
(9) RewriteLemmaProof [LOWER BOUND(ID), 632 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 859 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 410 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 28 ms]
(16) typed CpxTrs
(17) RewriteLemmaProof [LOWER BOUND(ID), 521 ms]
(18) typed CpxTrs
(19) RewriteLemmaProof [LOWER BOUND(ID), 537 ms]
(20) BEST
    (21) proven lower bound
        (22) LowerBoundPropagationProof [FINISHED, 0 ms]
        (23) BOUNDS(n^1, INF)
    (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 2213 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 510 ms]
        (28) BOUNDS(1, INF)


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

(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:

   A__AND(tt, z0) -> c(MARK(z0))
   A__AND(z0, z1) -> c1
   A__PLUS(z0, 0) -> c2(MARK(z0))
   A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
   A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
   A__PLUS(z0, z1) -> c5
   A__X(z0, 0) -> c6
   A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
   A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
   A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
   A__X(z0, z1) -> c10
   MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
   MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
   MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
   MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
   MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
   MARK(tt) -> c16
   MARK(0) -> c17
   MARK(s(z0)) -> c18(MARK(z0))

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

   a__and(tt, z0) -> mark(z0)
   a__and(z0, z1) -> and(z0, z1)
   a__plus(z0, 0) -> mark(z0)
   a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
   a__plus(z0, z1) -> plus(z0, z1)
   a__x(z0, 0) -> 0
   a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
   a__x(z0, z1) -> x(z0, z1)
   mark(and(z0, z1)) -> a__and(mark(z0), z1)
   mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
   mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
   mark(tt) -> tt
   mark(0) -> 0
   mark(s(z0)) -> s(mark(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:

   A__AND(tt, z0) -> c(MARK(z0))
   A__AND(z0, z1) -> c1
   A__PLUS(z0, 0) -> c2(MARK(z0))
   A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
   A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
   A__PLUS(z0, z1) -> c5
   A__X(z0, 0) -> c6
   A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
   A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
   A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
   A__X(z0, z1) -> c10
   MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
   MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
   MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
   MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
   MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
   MARK(tt) -> c16
   MARK(0) -> c17
   MARK(s(z0)) -> c18(MARK(z0))

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

   a__and(tt, z0) -> mark(z0)
   a__and(z0, z1) -> and(z0, z1)
   a__plus(z0, 0) -> mark(z0)
   a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
   a__plus(z0, z1) -> plus(z0, z1)
   a__x(z0, 0) -> 0
   a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
   a__x(z0, z1) -> x(z0, z1)
   mark(and(z0, z1)) -> a__and(mark(z0), z1)
   mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
   mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
   mark(tt) -> tt
   mark(0) -> 0
   mark(s(z0)) -> s(mark(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:

   A__AND(tt, z0) -> c(MARK(z0))
   A__AND(z0, z1) -> c1
   A__PLUS(z0, 0') -> c2(MARK(z0))
   A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
   A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
   A__PLUS(z0, z1) -> c5
   A__X(z0, 0') -> c6
   A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
   A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
   A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
   A__X(z0, z1) -> c10
   MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
   MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
   MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
   MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
   MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
   MARK(tt) -> c16
   MARK(0') -> c17
   MARK(s(z0)) -> c18(MARK(z0))

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

   a__and(tt, z0) -> mark(z0)
   a__and(z0, z1) -> and(z0, z1)
   a__plus(z0, 0') -> mark(z0)
   a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
   a__plus(z0, z1) -> plus(z0, z1)
   a__x(z0, 0') -> 0'
   a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
   a__x(z0, z1) -> x(z0, z1)
   mark(and(z0, z1)) -> a__and(mark(z0), z1)
   mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
   mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
   mark(tt) -> tt
   mark(0') -> 0'
   mark(s(z0)) -> s(mark(z0))

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

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

(6)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10

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

(7) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MARK, A__PLUS, mark, A__X, a__x, a__plus

They will be analysed ascendingly in the following order:
MARK = A__PLUS
mark < MARK
MARK = A__X
mark < A__PLUS
A__PLUS = A__X
mark < A__X
mark = a__x
mark = a__plus
a__x < A__X
a__x = a__plus

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

(8)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
a__plus, MARK, A__PLUS, mark, A__X, a__x

They will be analysed ascendingly in the following order:
MARK = A__PLUS
mark < MARK
MARK = A__X
mark < A__PLUS
A__PLUS = A__X
mark < A__X
mark = a__x
mark = a__plus
a__x < A__X
a__x = a__plus

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

(9) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
mark(gen_tt:0':s:and:plus:x6_19(n12198_19)) -> gen_tt:0':s:and:plus:x6_19(n12198_19), rt in Omega(0)

Induction Base:
mark(gen_tt:0':s:and:plus:x6_19(0)) ->_R^Omega(0)
tt

Induction Step:
mark(gen_tt:0':s:and:plus:x6_19(+(n12198_19, 1))) ->_R^Omega(0)
s(mark(gen_tt:0':s:and:plus:x6_19(n12198_19))) ->_IH
s(gen_tt:0':s:and:plus:x6_19(c12199_19))

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

(10)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Lemmas:
mark(gen_tt:0':s:and:plus:x6_19(n12198_19)) -> gen_tt:0':s:and:plus:x6_19(n12198_19), rt in Omega(0)


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
a__x, MARK, A__PLUS, A__X, a__plus

They will be analysed ascendingly in the following order:
MARK = A__PLUS
mark < MARK
MARK = A__X
mark < A__PLUS
A__PLUS = A__X
mark < A__X
mark = a__x
mark = a__plus
a__x < A__X
a__x = a__plus

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n13459_19))) -> *10_19, rt in Omega(0)

Induction Base:
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, 0)))

Induction Step:
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, +(n13459_19, 1)))) ->_R^Omega(0)
a__plus(a__x(mark(gen_tt:0':s:and:plus:x6_19(a)), mark(gen_tt:0':s:and:plus:x6_19(+(1, n13459_19)))), mark(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
a__plus(a__x(gen_tt:0':s:and:plus:x6_19(a), mark(gen_tt:0':s:and:plus:x6_19(+(1, n13459_19)))), mark(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
a__plus(a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n13459_19))), mark(gen_tt:0':s:and:plus:x6_19(a))) ->_IH
a__plus(*10_19, mark(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
a__plus(*10_19, gen_tt:0':s:and:plus:x6_19(a))

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

(12)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Lemmas:
mark(gen_tt:0':s:and:plus:x6_19(n12198_19)) -> gen_tt:0':s:and:plus:x6_19(n12198_19), rt in Omega(0)
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n13459_19))) -> *10_19, rt in Omega(0)


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
a__plus, MARK, A__PLUS, mark, A__X

They will be analysed ascendingly in the following order:
MARK = A__PLUS
mark < MARK
MARK = A__X
mark < A__PLUS
A__PLUS = A__X
mark < A__X
mark = a__x
mark = a__plus
a__x < A__X
a__x = a__plus

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))) -> *10_19, rt in Omega(0)

Induction Base:
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, 0)))

Induction Step:
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, +(n21738_19, 1)))) ->_R^Omega(0)
s(a__plus(mark(gen_tt:0':s:and:plus:x6_19(a)), mark(gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))))) ->_L^Omega(0)
s(a__plus(gen_tt:0':s:and:plus:x6_19(a), mark(gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))))) ->_L^Omega(0)
s(a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n21738_19)))) ->_IH
s(*10_19)

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

(14)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Lemmas:
mark(gen_tt:0':s:and:plus:x6_19(n12198_19)) -> gen_tt:0':s:and:plus:x6_19(n12198_19), rt in Omega(0)
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n13459_19))) -> *10_19, rt in Omega(0)
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))) -> *10_19, rt in Omega(0)


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
mark, MARK, A__PLUS, A__X, a__x

They will be analysed ascendingly in the following order:
MARK = A__PLUS
mark < MARK
MARK = A__X
mark < A__PLUS
A__PLUS = A__X
mark < A__X
mark = a__x
mark = a__plus
a__x < A__X
a__x = a__plus

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
mark(gen_tt:0':s:and:plus:x6_19(n25340_19)) -> gen_tt:0':s:and:plus:x6_19(n25340_19), rt in Omega(0)

Induction Base:
mark(gen_tt:0':s:and:plus:x6_19(0)) ->_R^Omega(0)
tt

Induction Step:
mark(gen_tt:0':s:and:plus:x6_19(+(n25340_19, 1))) ->_R^Omega(0)
s(mark(gen_tt:0':s:and:plus:x6_19(n25340_19))) ->_IH
s(gen_tt:0':s:and:plus:x6_19(c25341_19))

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

(16)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Lemmas:
mark(gen_tt:0':s:and:plus:x6_19(n25340_19)) -> gen_tt:0':s:and:plus:x6_19(n25340_19), rt in Omega(0)
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n13459_19))) -> *10_19, rt in Omega(0)
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))) -> *10_19, rt in Omega(0)


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
a__x, MARK, A__PLUS, A__X

They will be analysed ascendingly in the following order:
MARK = A__PLUS
mark < MARK
MARK = A__X
mark < A__PLUS
A__PLUS = A__X
mark < A__X
mark = a__x
mark = a__plus
a__x < A__X
a__x = a__plus

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n26807_19))) -> *10_19, rt in Omega(0)

Induction Base:
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, 0)))

Induction Step:
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, +(n26807_19, 1)))) ->_R^Omega(0)
a__plus(a__x(mark(gen_tt:0':s:and:plus:x6_19(a)), mark(gen_tt:0':s:and:plus:x6_19(+(1, n26807_19)))), mark(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
a__plus(a__x(gen_tt:0':s:and:plus:x6_19(a), mark(gen_tt:0':s:and:plus:x6_19(+(1, n26807_19)))), mark(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
a__plus(a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n26807_19))), mark(gen_tt:0':s:and:plus:x6_19(a))) ->_IH
a__plus(*10_19, mark(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
a__plus(*10_19, gen_tt:0':s:and:plus:x6_19(a))

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

(18)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Lemmas:
mark(gen_tt:0':s:and:plus:x6_19(n25340_19)) -> gen_tt:0':s:and:plus:x6_19(n25340_19), rt in Omega(0)
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n26807_19))) -> *10_19, rt in Omega(0)
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))) -> *10_19, rt in Omega(0)


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
A__PLUS, MARK, A__X

They will be analysed ascendingly in the following order:
MARK = A__PLUS
MARK = A__X
A__PLUS = A__X

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n35904_19))) -> *10_19, rt in Omega(n35904_19)

Induction Base:
A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, 0)))

Induction Step:
A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, +(n35904_19, 1)))) ->_R^Omega(1)
c3(A__PLUS(mark(gen_tt:0':s:and:plus:x6_19(a)), mark(gen_tt:0':s:and:plus:x6_19(+(1, n35904_19)))), MARK(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
c3(A__PLUS(gen_tt:0':s:and:plus:x6_19(a), mark(gen_tt:0':s:and:plus:x6_19(+(1, n35904_19)))), MARK(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
c3(A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n35904_19))), MARK(gen_tt:0':s:and:plus:x6_19(a))) ->_IH
c3(*10_19, MARK(gen_tt:0':s:and:plus:x6_19(a)))

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

(20)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Lemmas:
mark(gen_tt:0':s:and:plus:x6_19(n25340_19)) -> gen_tt:0':s:and:plus:x6_19(n25340_19), rt in Omega(0)
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n26807_19))) -> *10_19, rt in Omega(0)
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))) -> *10_19, rt in Omega(0)


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
A__PLUS, MARK, A__X

They will be analysed ascendingly in the following order:
MARK = A__PLUS
MARK = A__X
A__PLUS = A__X

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

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

(23)
BOUNDS(n^1, INF)

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

(24)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Lemmas:
mark(gen_tt:0':s:and:plus:x6_19(n25340_19)) -> gen_tt:0':s:and:plus:x6_19(n25340_19), rt in Omega(0)
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n26807_19))) -> *10_19, rt in Omega(0)
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))) -> *10_19, rt in Omega(0)
A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n35904_19))) -> *10_19, rt in Omega(n35904_19)


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
MARK, A__X

They will be analysed ascendingly in the following order:
MARK = A__PLUS
MARK = A__X
A__PLUS = A__X

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MARK(gen_tt:0':s:and:plus:x6_19(+(1, n45034_19))) -> *10_19, rt in Omega(n45034_19)

Induction Base:
MARK(gen_tt:0':s:and:plus:x6_19(+(1, 0)))

Induction Step:
MARK(gen_tt:0':s:and:plus:x6_19(+(1, +(n45034_19, 1)))) ->_R^Omega(1)
c18(MARK(gen_tt:0':s:and:plus:x6_19(+(1, n45034_19)))) ->_IH
c18(*10_19)

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

(26)
Obligation:
Innermost TRS:
Rules:
A__AND(tt, z0) -> c(MARK(z0))
A__AND(z0, z1) -> c1
A__PLUS(z0, 0') -> c2(MARK(z0))
A__PLUS(z0, s(z1)) -> c3(A__PLUS(mark(z0), mark(z1)), MARK(z0))
A__PLUS(z0, s(z1)) -> c4(A__PLUS(mark(z0), mark(z1)), MARK(z1))
A__PLUS(z0, z1) -> c5
A__X(z0, 0') -> c6
A__X(z0, s(z1)) -> c7(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z0))
A__X(z0, s(z1)) -> c8(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), A__X(mark(z0), mark(z1)), MARK(z1))
A__X(z0, s(z1)) -> c9(A__PLUS(a__x(mark(z0), mark(z1)), mark(z0)), MARK(z0))
A__X(z0, z1) -> c10
MARK(and(z0, z1)) -> c11(A__AND(mark(z0), z1), MARK(z0))
MARK(plus(z0, z1)) -> c12(A__PLUS(mark(z0), mark(z1)), MARK(z0))
MARK(plus(z0, z1)) -> c13(A__PLUS(mark(z0), mark(z1)), MARK(z1))
MARK(x(z0, z1)) -> c14(A__X(mark(z0), mark(z1)), MARK(z0))
MARK(x(z0, z1)) -> c15(A__X(mark(z0), mark(z1)), MARK(z1))
MARK(tt) -> c16
MARK(0') -> c17
MARK(s(z0)) -> c18(MARK(z0))
a__and(tt, z0) -> mark(z0)
a__and(z0, z1) -> and(z0, z1)
a__plus(z0, 0') -> mark(z0)
a__plus(z0, s(z1)) -> s(a__plus(mark(z0), mark(z1)))
a__plus(z0, z1) -> plus(z0, z1)
a__x(z0, 0') -> 0'
a__x(z0, s(z1)) -> a__plus(a__x(mark(z0), mark(z1)), mark(z0))
a__x(z0, z1) -> x(z0, z1)
mark(and(z0, z1)) -> a__and(mark(z0), z1)
mark(plus(z0, z1)) -> a__plus(mark(z0), mark(z1))
mark(x(z0, z1)) -> a__x(mark(z0), mark(z1))
mark(tt) -> tt
mark(0') -> 0'
mark(s(z0)) -> s(mark(z0))

Types:
A__AND :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c:c1
tt :: tt:0':s:and:plus:x
c :: c11:c12:c13:c14:c15:c16:c17:c18 -> c:c1
MARK :: tt:0':s:and:plus:x -> c11:c12:c13:c14:c15:c16:c17:c18
c1 :: c:c1
A__PLUS :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c2:c3:c4:c5
0' :: tt:0':s:and:plus:x
c2 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
s :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c3 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
mark :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c4 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c2:c3:c4:c5
c5 :: c2:c3:c4:c5
A__X :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> c6:c7:c8:c9:c10
c6 :: c6:c7:c8:c9:c10
c7 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
a__x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c8 :: c2:c3:c4:c5 -> c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c9 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c6:c7:c8:c9:c10
c10 :: c6:c7:c8:c9:c10
and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c11 :: c:c1 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c12 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c13 :: c2:c3:c4:c5 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
x :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
c14 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c15 :: c6:c7:c8:c9:c10 -> c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
c16 :: c11:c12:c13:c14:c15:c16:c17:c18
c17 :: c11:c12:c13:c14:c15:c16:c17:c18
c18 :: c11:c12:c13:c14:c15:c16:c17:c18 -> c11:c12:c13:c14:c15:c16:c17:c18
a__and :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
a__plus :: tt:0':s:and:plus:x -> tt:0':s:and:plus:x -> tt:0':s:and:plus:x
hole_c:c11_19 :: c:c1
hole_tt:0':s:and:plus:x2_19 :: tt:0':s:and:plus:x
hole_c11:c12:c13:c14:c15:c16:c17:c183_19 :: c11:c12:c13:c14:c15:c16:c17:c18
hole_c2:c3:c4:c54_19 :: c2:c3:c4:c5
hole_c6:c7:c8:c9:c105_19 :: c6:c7:c8:c9:c10
gen_tt:0':s:and:plus:x6_19 :: Nat -> tt:0':s:and:plus:x
gen_c11:c12:c13:c14:c15:c16:c17:c187_19 :: Nat -> c11:c12:c13:c14:c15:c16:c17:c18
gen_c2:c3:c4:c58_19 :: Nat -> c2:c3:c4:c5
gen_c6:c7:c8:c9:c109_19 :: Nat -> c6:c7:c8:c9:c10


Lemmas:
mark(gen_tt:0':s:and:plus:x6_19(n25340_19)) -> gen_tt:0':s:and:plus:x6_19(n25340_19), rt in Omega(0)
a__x(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n26807_19))) -> *10_19, rt in Omega(0)
a__plus(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n21738_19))) -> *10_19, rt in Omega(0)
A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n35904_19))) -> *10_19, rt in Omega(n35904_19)
MARK(gen_tt:0':s:and:plus:x6_19(+(1, n45034_19))) -> *10_19, rt in Omega(n45034_19)


Generator Equations:
gen_tt:0':s:and:plus:x6_19(0) <=> tt
gen_tt:0':s:and:plus:x6_19(+(x, 1)) <=> s(gen_tt:0':s:and:plus:x6_19(x))
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(0) <=> c16
gen_c11:c12:c13:c14:c15:c16:c17:c187_19(+(x, 1)) <=> c11(c(c16), gen_c11:c12:c13:c14:c15:c16:c17:c187_19(x))
gen_c2:c3:c4:c58_19(0) <=> c2(c16)
gen_c2:c3:c4:c58_19(+(x, 1)) <=> c3(gen_c2:c3:c4:c58_19(x), c16)
gen_c6:c7:c8:c9:c109_19(0) <=> c6
gen_c6:c7:c8:c9:c109_19(+(x, 1)) <=> c7(c2(c16), gen_c6:c7:c8:c9:c109_19(x), c16)


The following defined symbols remain to be analysed:
A__X, A__PLUS

They will be analysed ascendingly in the following order:
MARK = A__PLUS
MARK = A__X
A__PLUS = A__X

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n70317_19))) -> *10_19, rt in Omega(n70317_19)

Induction Base:
A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, 0)))

Induction Step:
A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, +(n70317_19, 1)))) ->_R^Omega(1)
c3(A__PLUS(mark(gen_tt:0':s:and:plus:x6_19(a)), mark(gen_tt:0':s:and:plus:x6_19(+(1, n70317_19)))), MARK(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
c3(A__PLUS(gen_tt:0':s:and:plus:x6_19(a), mark(gen_tt:0':s:and:plus:x6_19(+(1, n70317_19)))), MARK(gen_tt:0':s:and:plus:x6_19(a))) ->_L^Omega(0)
c3(A__PLUS(gen_tt:0':s:and:plus:x6_19(a), gen_tt:0':s:and:plus:x6_19(+(1, n70317_19))), MARK(gen_tt:0':s:and:plus:x6_19(a))) ->_IH
c3(*10_19, MARK(gen_tt:0':s:and:plus:x6_19(a)))

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

(28)
BOUNDS(1, INF)