WORST_CASE(Omega(n^1),O(n^1))
proof of input_CDm36dFWLw.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(2) CpxTRS
    (3) CpxTrsMatchBoundsTAProof [FINISHED, 24 ms]
    (4) BOUNDS(1, n^1)
(5) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) typed CpxTrs
    (13) OrderProof [LOWER BOUND(ID), 9 ms]
    (14) typed CpxTrs
    (15) RewriteLemmaProof [LOWER BOUND(ID), 257 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) typed CpxTrs
            (21) RewriteLemmaProof [LOWER BOUND(ID), 72 ms]
            (22) typed CpxTrs
            (23) RewriteLemmaProof [LOWER BOUND(ID), 35 ms]
            (24) typed CpxTrs
            (25) RewriteLemmaProof [LOWER BOUND(ID), 68 ms]
            (26) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1))
   compS_f#1(id, x3) -> S(x3)
   iter#3(0) -> id
   iter#3(S(x6)) -> compS_f(iter#3(x6))
   main(0) -> 0
   main(S(x9)) -> compS_f#1(iter#3(x9), 0)

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

(1) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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


The TRS R consists of the following rules:

   compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1))
   compS_f#1(id, x3) -> S(x3)
   iter#3(0) -> id
   iter#3(S(x6)) -> compS_f(iter#3(x6))
   main(0) -> 0
   main(S(x9)) -> compS_f#1(iter#3(x9), 0)

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

(3) CpxTrsMatchBoundsTAProof (FINISHED)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2. 

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: 
final states : [1, 2, 3]
transitions: 
compS_f0(0) -> 0
S0(0) -> 0
id0() -> 0
00() -> 0
compS_f#10(0, 0) -> 1
iter#30(0) -> 2
main0(0) -> 3
S1(0) -> 4
compS_f#11(0, 4) -> 1
S1(0) -> 1
id1() -> 2
iter#31(0) -> 5
compS_f1(5) -> 2
01() -> 3
iter#31(0) -> 6
01() -> 7
compS_f#11(6, 7) -> 3
S1(4) -> 4
S1(4) -> 1
id1() -> 5
id1() -> 6
compS_f1(5) -> 5
compS_f1(5) -> 6
S2(7) -> 8
compS_f#12(5, 8) -> 3
S2(7) -> 3
S2(8) -> 8
S2(8) -> 3

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

(4)
BOUNDS(1, n^1)

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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
   compS_f#1(id, z0) -> S(z0)
   iter#3(0) -> id
   iter#3(S(z0)) -> compS_f(iter#3(z0))
   main(0) -> 0
   main(S(z0)) -> compS_f#1(iter#3(z0), 0)
Tuples:
   COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
   COMPS_F#1(id, z0) -> c1
   ITER#3(0) -> c2
   ITER#3(S(z0)) -> c3(ITER#3(z0))
   MAIN(0) -> c4
   MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0), ITER#3(z0))
S tuples:
   COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
   COMPS_F#1(id, z0) -> c1
   ITER#3(0) -> c2
   ITER#3(S(z0)) -> c3(ITER#3(z0))
   MAIN(0) -> c4
   MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0), ITER#3(z0))
K tuples:none
Defined Rule Symbols:   compS_f#1_2, iter#3_1, main_1

Defined Pair Symbols:   COMPS_F#1_2, ITER#3_1, MAIN_1

Compound Symbols:   c_1, c1, c2, c3_1, c4, c5_2


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

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

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

   COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
   COMPS_F#1(id, z0) -> c1
   ITER#3(0) -> c2
   ITER#3(S(z0)) -> c3(ITER#3(z0))
   MAIN(0) -> c4
   MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0), ITER#3(z0))

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

   compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
   compS_f#1(id, z0) -> S(z0)
   iter#3(0) -> id
   iter#3(S(z0)) -> compS_f(iter#3(z0))
   main(0) -> 0
   main(S(z0)) -> compS_f#1(iter#3(z0), 0)

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

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

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

   COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
   COMPS_F#1(id, z0) -> c1
   ITER#3(0') -> c2
   ITER#3(S(z0)) -> c3(ITER#3(z0))
   MAIN(0') -> c4
   MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0'), ITER#3(z0))

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

   compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
   compS_f#1(id, z0) -> S(z0)
   iter#3(0') -> id
   iter#3(S(z0)) -> compS_f(iter#3(z0))
   main(0') -> 0'
   main(S(z0)) -> compS_f#1(iter#3(z0), 0')

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

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

(12)
Obligation:
Innermost TRS:
Rules:
COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
COMPS_F#1(id, z0) -> c1
ITER#3(0') -> c2
ITER#3(S(z0)) -> c3(ITER#3(z0))
MAIN(0') -> c4
MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0'), ITER#3(z0))
compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
compS_f#1(id, z0) -> S(z0)
iter#3(0') -> id
iter#3(S(z0)) -> compS_f(iter#3(z0))
main(0') -> 0'
main(S(z0)) -> compS_f#1(iter#3(z0), 0')

Types:
COMPS_F#1 :: compS_f:id -> S:0' -> c:c1
compS_f :: compS_f:id -> compS_f:id
c :: c:c1 -> c:c1
S :: S:0' -> S:0'
id :: compS_f:id
c1 :: c:c1
ITER#3 :: S:0' -> c2:c3
0' :: S:0'
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
MAIN :: S:0' -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5
iter#3 :: S:0' -> compS_f:id
compS_f#1 :: compS_f:id -> S:0' -> S:0'
main :: S:0' -> S:0'
hole_c:c11_6 :: c:c1
hole_compS_f:id2_6 :: compS_f:id
hole_S:0'3_6 :: S:0'
hole_c2:c34_6 :: c2:c3
hole_c4:c55_6 :: c4:c5
gen_c:c16_6 :: Nat -> c:c1
gen_compS_f:id7_6 :: Nat -> compS_f:id
gen_S:0'8_6 :: Nat -> S:0'
gen_c2:c39_6 :: Nat -> c2:c3

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

(13) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
COMPS_F#1, ITER#3, iter#3, compS_f#1
----------------------------------------

(14)
Obligation:
Innermost TRS:
Rules:
COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
COMPS_F#1(id, z0) -> c1
ITER#3(0') -> c2
ITER#3(S(z0)) -> c3(ITER#3(z0))
MAIN(0') -> c4
MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0'), ITER#3(z0))
compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
compS_f#1(id, z0) -> S(z0)
iter#3(0') -> id
iter#3(S(z0)) -> compS_f(iter#3(z0))
main(0') -> 0'
main(S(z0)) -> compS_f#1(iter#3(z0), 0')

Types:
COMPS_F#1 :: compS_f:id -> S:0' -> c:c1
compS_f :: compS_f:id -> compS_f:id
c :: c:c1 -> c:c1
S :: S:0' -> S:0'
id :: compS_f:id
c1 :: c:c1
ITER#3 :: S:0' -> c2:c3
0' :: S:0'
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
MAIN :: S:0' -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5
iter#3 :: S:0' -> compS_f:id
compS_f#1 :: compS_f:id -> S:0' -> S:0'
main :: S:0' -> S:0'
hole_c:c11_6 :: c:c1
hole_compS_f:id2_6 :: compS_f:id
hole_S:0'3_6 :: S:0'
hole_c2:c34_6 :: c2:c3
hole_c4:c55_6 :: c4:c5
gen_c:c16_6 :: Nat -> c:c1
gen_compS_f:id7_6 :: Nat -> compS_f:id
gen_S:0'8_6 :: Nat -> S:0'
gen_c2:c39_6 :: Nat -> c2:c3


Generator Equations:
gen_c:c16_6(0) <=> c1
gen_c:c16_6(+(x, 1)) <=> c(gen_c:c16_6(x))
gen_compS_f:id7_6(0) <=> id
gen_compS_f:id7_6(+(x, 1)) <=> compS_f(gen_compS_f:id7_6(x))
gen_S:0'8_6(0) <=> 0'
gen_S:0'8_6(+(x, 1)) <=> S(gen_S:0'8_6(x))
gen_c2:c39_6(0) <=> c2
gen_c2:c39_6(+(x, 1)) <=> c3(gen_c2:c39_6(x))


The following defined symbols remain to be analysed:
COMPS_F#1, ITER#3, iter#3, compS_f#1
----------------------------------------

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
COMPS_F#1(gen_compS_f:id7_6(n11_6), gen_S:0'8_6(b)) -> gen_c:c16_6(n11_6), rt in Omega(1 + n11_6)

Induction Base:
COMPS_F#1(gen_compS_f:id7_6(0), gen_S:0'8_6(b)) ->_R^Omega(1)
c1

Induction Step:
COMPS_F#1(gen_compS_f:id7_6(+(n11_6, 1)), gen_S:0'8_6(b)) ->_R^Omega(1)
c(COMPS_F#1(gen_compS_f:id7_6(n11_6), S(gen_S:0'8_6(b)))) ->_IH
c(gen_c:c16_6(c12_6))

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

(16)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
COMPS_F#1(id, z0) -> c1
ITER#3(0') -> c2
ITER#3(S(z0)) -> c3(ITER#3(z0))
MAIN(0') -> c4
MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0'), ITER#3(z0))
compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
compS_f#1(id, z0) -> S(z0)
iter#3(0') -> id
iter#3(S(z0)) -> compS_f(iter#3(z0))
main(0') -> 0'
main(S(z0)) -> compS_f#1(iter#3(z0), 0')

Types:
COMPS_F#1 :: compS_f:id -> S:0' -> c:c1
compS_f :: compS_f:id -> compS_f:id
c :: c:c1 -> c:c1
S :: S:0' -> S:0'
id :: compS_f:id
c1 :: c:c1
ITER#3 :: S:0' -> c2:c3
0' :: S:0'
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
MAIN :: S:0' -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5
iter#3 :: S:0' -> compS_f:id
compS_f#1 :: compS_f:id -> S:0' -> S:0'
main :: S:0' -> S:0'
hole_c:c11_6 :: c:c1
hole_compS_f:id2_6 :: compS_f:id
hole_S:0'3_6 :: S:0'
hole_c2:c34_6 :: c2:c3
hole_c4:c55_6 :: c4:c5
gen_c:c16_6 :: Nat -> c:c1
gen_compS_f:id7_6 :: Nat -> compS_f:id
gen_S:0'8_6 :: Nat -> S:0'
gen_c2:c39_6 :: Nat -> c2:c3


Generator Equations:
gen_c:c16_6(0) <=> c1
gen_c:c16_6(+(x, 1)) <=> c(gen_c:c16_6(x))
gen_compS_f:id7_6(0) <=> id
gen_compS_f:id7_6(+(x, 1)) <=> compS_f(gen_compS_f:id7_6(x))
gen_S:0'8_6(0) <=> 0'
gen_S:0'8_6(+(x, 1)) <=> S(gen_S:0'8_6(x))
gen_c2:c39_6(0) <=> c2
gen_c2:c39_6(+(x, 1)) <=> c3(gen_c2:c39_6(x))


The following defined symbols remain to be analysed:
COMPS_F#1, ITER#3, iter#3, compS_f#1
----------------------------------------

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
COMPS_F#1(id, z0) -> c1
ITER#3(0') -> c2
ITER#3(S(z0)) -> c3(ITER#3(z0))
MAIN(0') -> c4
MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0'), ITER#3(z0))
compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
compS_f#1(id, z0) -> S(z0)
iter#3(0') -> id
iter#3(S(z0)) -> compS_f(iter#3(z0))
main(0') -> 0'
main(S(z0)) -> compS_f#1(iter#3(z0), 0')

Types:
COMPS_F#1 :: compS_f:id -> S:0' -> c:c1
compS_f :: compS_f:id -> compS_f:id
c :: c:c1 -> c:c1
S :: S:0' -> S:0'
id :: compS_f:id
c1 :: c:c1
ITER#3 :: S:0' -> c2:c3
0' :: S:0'
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
MAIN :: S:0' -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5
iter#3 :: S:0' -> compS_f:id
compS_f#1 :: compS_f:id -> S:0' -> S:0'
main :: S:0' -> S:0'
hole_c:c11_6 :: c:c1
hole_compS_f:id2_6 :: compS_f:id
hole_S:0'3_6 :: S:0'
hole_c2:c34_6 :: c2:c3
hole_c4:c55_6 :: c4:c5
gen_c:c16_6 :: Nat -> c:c1
gen_compS_f:id7_6 :: Nat -> compS_f:id
gen_S:0'8_6 :: Nat -> S:0'
gen_c2:c39_6 :: Nat -> c2:c3


Lemmas:
COMPS_F#1(gen_compS_f:id7_6(n11_6), gen_S:0'8_6(b)) -> gen_c:c16_6(n11_6), rt in Omega(1 + n11_6)


Generator Equations:
gen_c:c16_6(0) <=> c1
gen_c:c16_6(+(x, 1)) <=> c(gen_c:c16_6(x))
gen_compS_f:id7_6(0) <=> id
gen_compS_f:id7_6(+(x, 1)) <=> compS_f(gen_compS_f:id7_6(x))
gen_S:0'8_6(0) <=> 0'
gen_S:0'8_6(+(x, 1)) <=> S(gen_S:0'8_6(x))
gen_c2:c39_6(0) <=> c2
gen_c2:c39_6(+(x, 1)) <=> c3(gen_c2:c39_6(x))


The following defined symbols remain to be analysed:
ITER#3, iter#3, compS_f#1
----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ITER#3(gen_S:0'8_6(n427_6)) -> gen_c2:c39_6(n427_6), rt in Omega(1 + n427_6)

Induction Base:
ITER#3(gen_S:0'8_6(0)) ->_R^Omega(1)
c2

Induction Step:
ITER#3(gen_S:0'8_6(+(n427_6, 1))) ->_R^Omega(1)
c3(ITER#3(gen_S:0'8_6(n427_6))) ->_IH
c3(gen_c2:c39_6(c428_6))

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:
COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
COMPS_F#1(id, z0) -> c1
ITER#3(0') -> c2
ITER#3(S(z0)) -> c3(ITER#3(z0))
MAIN(0') -> c4
MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0'), ITER#3(z0))
compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
compS_f#1(id, z0) -> S(z0)
iter#3(0') -> id
iter#3(S(z0)) -> compS_f(iter#3(z0))
main(0') -> 0'
main(S(z0)) -> compS_f#1(iter#3(z0), 0')

Types:
COMPS_F#1 :: compS_f:id -> S:0' -> c:c1
compS_f :: compS_f:id -> compS_f:id
c :: c:c1 -> c:c1
S :: S:0' -> S:0'
id :: compS_f:id
c1 :: c:c1
ITER#3 :: S:0' -> c2:c3
0' :: S:0'
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
MAIN :: S:0' -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5
iter#3 :: S:0' -> compS_f:id
compS_f#1 :: compS_f:id -> S:0' -> S:0'
main :: S:0' -> S:0'
hole_c:c11_6 :: c:c1
hole_compS_f:id2_6 :: compS_f:id
hole_S:0'3_6 :: S:0'
hole_c2:c34_6 :: c2:c3
hole_c4:c55_6 :: c4:c5
gen_c:c16_6 :: Nat -> c:c1
gen_compS_f:id7_6 :: Nat -> compS_f:id
gen_S:0'8_6 :: Nat -> S:0'
gen_c2:c39_6 :: Nat -> c2:c3


Lemmas:
COMPS_F#1(gen_compS_f:id7_6(n11_6), gen_S:0'8_6(b)) -> gen_c:c16_6(n11_6), rt in Omega(1 + n11_6)
ITER#3(gen_S:0'8_6(n427_6)) -> gen_c2:c39_6(n427_6), rt in Omega(1 + n427_6)


Generator Equations:
gen_c:c16_6(0) <=> c1
gen_c:c16_6(+(x, 1)) <=> c(gen_c:c16_6(x))
gen_compS_f:id7_6(0) <=> id
gen_compS_f:id7_6(+(x, 1)) <=> compS_f(gen_compS_f:id7_6(x))
gen_S:0'8_6(0) <=> 0'
gen_S:0'8_6(+(x, 1)) <=> S(gen_S:0'8_6(x))
gen_c2:c39_6(0) <=> c2
gen_c2:c39_6(+(x, 1)) <=> c3(gen_c2:c39_6(x))


The following defined symbols remain to be analysed:
iter#3, compS_f#1
----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
iter#3(gen_S:0'8_6(n765_6)) -> gen_compS_f:id7_6(n765_6), rt in Omega(0)

Induction Base:
iter#3(gen_S:0'8_6(0)) ->_R^Omega(0)
id

Induction Step:
iter#3(gen_S:0'8_6(+(n765_6, 1))) ->_R^Omega(0)
compS_f(iter#3(gen_S:0'8_6(n765_6))) ->_IH
compS_f(gen_compS_f:id7_6(c766_6))

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:
COMPS_F#1(compS_f(z0), z1) -> c(COMPS_F#1(z0, S(z1)))
COMPS_F#1(id, z0) -> c1
ITER#3(0') -> c2
ITER#3(S(z0)) -> c3(ITER#3(z0))
MAIN(0') -> c4
MAIN(S(z0)) -> c5(COMPS_F#1(iter#3(z0), 0'), ITER#3(z0))
compS_f#1(compS_f(z0), z1) -> compS_f#1(z0, S(z1))
compS_f#1(id, z0) -> S(z0)
iter#3(0') -> id
iter#3(S(z0)) -> compS_f(iter#3(z0))
main(0') -> 0'
main(S(z0)) -> compS_f#1(iter#3(z0), 0')

Types:
COMPS_F#1 :: compS_f:id -> S:0' -> c:c1
compS_f :: compS_f:id -> compS_f:id
c :: c:c1 -> c:c1
S :: S:0' -> S:0'
id :: compS_f:id
c1 :: c:c1
ITER#3 :: S:0' -> c2:c3
0' :: S:0'
c2 :: c2:c3
c3 :: c2:c3 -> c2:c3
MAIN :: S:0' -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5
iter#3 :: S:0' -> compS_f:id
compS_f#1 :: compS_f:id -> S:0' -> S:0'
main :: S:0' -> S:0'
hole_c:c11_6 :: c:c1
hole_compS_f:id2_6 :: compS_f:id
hole_S:0'3_6 :: S:0'
hole_c2:c34_6 :: c2:c3
hole_c4:c55_6 :: c4:c5
gen_c:c16_6 :: Nat -> c:c1
gen_compS_f:id7_6 :: Nat -> compS_f:id
gen_S:0'8_6 :: Nat -> S:0'
gen_c2:c39_6 :: Nat -> c2:c3


Lemmas:
COMPS_F#1(gen_compS_f:id7_6(n11_6), gen_S:0'8_6(b)) -> gen_c:c16_6(n11_6), rt in Omega(1 + n11_6)
ITER#3(gen_S:0'8_6(n427_6)) -> gen_c2:c39_6(n427_6), rt in Omega(1 + n427_6)
iter#3(gen_S:0'8_6(n765_6)) -> gen_compS_f:id7_6(n765_6), rt in Omega(0)


Generator Equations:
gen_c:c16_6(0) <=> c1
gen_c:c16_6(+(x, 1)) <=> c(gen_c:c16_6(x))
gen_compS_f:id7_6(0) <=> id
gen_compS_f:id7_6(+(x, 1)) <=> compS_f(gen_compS_f:id7_6(x))
gen_S:0'8_6(0) <=> 0'
gen_S:0'8_6(+(x, 1)) <=> S(gen_S:0'8_6(x))
gen_c2:c39_6(0) <=> c2
gen_c2:c39_6(+(x, 1)) <=> c3(gen_c2:c39_6(x))


The following defined symbols remain to be analysed:
compS_f#1
----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
compS_f#1(gen_compS_f:id7_6(n1039_6), gen_S:0'8_6(b)) -> gen_S:0'8_6(+(+(1, n1039_6), b)), rt in Omega(0)

Induction Base:
compS_f#1(gen_compS_f:id7_6(0), gen_S:0'8_6(b)) ->_R^Omega(0)
S(gen_S:0'8_6(b))

Induction Step:
compS_f#1(gen_compS_f:id7_6(+(n1039_6, 1)), gen_S:0'8_6(b)) ->_R^Omega(0)
compS_f#1(gen_compS_f:id7_6(n1039_6), S(gen_S:0'8_6(b))) ->_IH
gen_S:0'8_6(+(+(1, +(b, 1)), c1040_6))

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

(26)
BOUNDS(1, INF)