WORST_CASE(Omega(n^1),O(n^1))
proof of input_TzJ4w51C7g.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, 69 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), 7 ms]
    (14) typed CpxTrs
    (15) RewriteLemmaProof [LOWER BOUND(ID), 298 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), 31 ms]
            (22) typed CpxTrs


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

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

   revApp#2(Nil, x16) -> x16
   revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2))
   dfsAcc#3(Leaf(x8), x16) -> Cons(x8, x16)
   dfsAcc#3(Node(x6, x4), x2) -> dfsAcc#3(x4, dfsAcc#3(x6, x2))
   main(x1) -> revApp#2(dfsAcc#3(x1, Nil), Nil)

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:

   revApp#2(Nil, x16) -> x16
   revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2))
   dfsAcc#3(Leaf(x8), x16) -> Cons(x8, x16)
   dfsAcc#3(Node(x6, x4), x2) -> dfsAcc#3(x4, dfsAcc#3(x6, x2))
   main(x1) -> revApp#2(dfsAcc#3(x1, Nil), Nil)

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: 
Nil0() -> 0
Cons0(0, 0) -> 0
Leaf0(0) -> 0
Node0(0, 0) -> 0
revApp#20(0, 0) -> 1
dfsAcc#30(0, 0) -> 2
main0(0) -> 3
Cons1(0, 0) -> 4
revApp#21(0, 4) -> 1
Cons1(0, 0) -> 2
dfsAcc#31(0, 0) -> 5
dfsAcc#31(0, 5) -> 2
Nil1() -> 7
dfsAcc#31(0, 7) -> 6
Nil1() -> 8
revApp#21(6, 8) -> 3
Cons1(0, 4) -> 4
Cons1(0, 5) -> 2
Cons1(0, 0) -> 5
Cons1(0, 7) -> 6
dfsAcc#31(0, 5) -> 5
dfsAcc#31(0, 7) -> 5
dfsAcc#31(0, 5) -> 6
Cons2(0, 8) -> 9
revApp#22(7, 9) -> 3
Cons1(0, 5) -> 5
Cons1(0, 7) -> 5
Cons1(0, 5) -> 6
revApp#22(5, 9) -> 3
Cons2(0, 9) -> 9
revApp#22(0, 9) -> 3
Cons1(0, 9) -> 4
revApp#21(0, 4) -> 3
0 -> 1
4 -> 1
4 -> 3
9 -> 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:
   revApp#2(Nil, z0) -> z0
   revApp#2(Cons(z0, z1), z2) -> revApp#2(z1, Cons(z0, z2))
   dfsAcc#3(Leaf(z0), z1) -> Cons(z0, z1)
   dfsAcc#3(Node(z0, z1), z2) -> dfsAcc#3(z1, dfsAcc#3(z0, z2))
   main(z0) -> revApp#2(dfsAcc#3(z0, Nil), Nil)
Tuples:
   REVAPP#2(Nil, z0) -> c
   REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
   DFSACC#3(Leaf(z0), z1) -> c2
   DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
   MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))
S tuples:
   REVAPP#2(Nil, z0) -> c
   REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
   DFSACC#3(Leaf(z0), z1) -> c2
   DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
   MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))
K tuples:none
Defined Rule Symbols:   revApp#2_2, dfsAcc#3_2, main_1

Defined Pair Symbols:   REVAPP#2_2, DFSACC#3_2, MAIN_1

Compound Symbols:   c, c1_1, c2, c3_2, c4_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:

   REVAPP#2(Nil, z0) -> c
   REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
   DFSACC#3(Leaf(z0), z1) -> c2
   DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
   MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))

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

   revApp#2(Nil, z0) -> z0
   revApp#2(Cons(z0, z1), z2) -> revApp#2(z1, Cons(z0, z2))
   dfsAcc#3(Leaf(z0), z1) -> Cons(z0, z1)
   dfsAcc#3(Node(z0, z1), z2) -> dfsAcc#3(z1, dfsAcc#3(z0, z2))
   main(z0) -> revApp#2(dfsAcc#3(z0, Nil), Nil)

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:

   REVAPP#2(Nil, z0) -> c
   REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
   DFSACC#3(Leaf(z0), z1) -> c2
   DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
   MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))

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

   revApp#2(Nil, z0) -> z0
   revApp#2(Cons(z0, z1), z2) -> revApp#2(z1, Cons(z0, z2))
   dfsAcc#3(Leaf(z0), z1) -> Cons(z0, z1)
   dfsAcc#3(Node(z0, z1), z2) -> dfsAcc#3(z1, dfsAcc#3(z0, z2))
   main(z0) -> revApp#2(dfsAcc#3(z0, Nil), Nil)

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

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

(12)
Obligation:
Innermost TRS:
Rules:
REVAPP#2(Nil, z0) -> c
REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
DFSACC#3(Leaf(z0), z1) -> c2
DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))
revApp#2(Nil, z0) -> z0
revApp#2(Cons(z0, z1), z2) -> revApp#2(z1, Cons(z0, z2))
dfsAcc#3(Leaf(z0), z1) -> Cons(z0, z1)
dfsAcc#3(Node(z0, z1), z2) -> dfsAcc#3(z1, dfsAcc#3(z0, z2))
main(z0) -> revApp#2(dfsAcc#3(z0, Nil), Nil)

Types:
REVAPP#2 :: Nil:Cons -> Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: a -> Nil:Cons -> Nil:Cons
c1 :: c:c1 -> c:c1
DFSACC#3 :: Leaf:Node -> Nil:Cons -> c2:c3
Leaf :: a -> Leaf:Node
c2 :: c2:c3
Node :: Leaf:Node -> Leaf:Node -> Leaf:Node
c3 :: c2:c3 -> c2:c3 -> c2:c3
dfsAcc#3 :: Leaf:Node -> Nil:Cons -> Nil:Cons
MAIN :: Leaf:Node -> c4
c4 :: c:c1 -> c2:c3 -> c4
revApp#2 :: Nil:Cons -> Nil:Cons -> Nil:Cons
main :: Leaf:Node -> Nil:Cons
hole_c:c11_5 :: c:c1
hole_Nil:Cons2_5 :: Nil:Cons
hole_a3_5 :: a
hole_c2:c34_5 :: c2:c3
hole_Leaf:Node5_5 :: Leaf:Node
hole_c46_5 :: c4
gen_c:c17_5 :: Nat -> c:c1
gen_Nil:Cons8_5 :: Nat -> Nil:Cons
gen_c2:c39_5 :: Nat -> c2:c3
gen_Leaf:Node10_5 :: Nat -> Leaf:Node

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

(13) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
REVAPP#2, DFSACC#3, dfsAcc#3, revApp#2

They will be analysed ascendingly in the following order:
dfsAcc#3 < DFSACC#3

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

(14)
Obligation:
Innermost TRS:
Rules:
REVAPP#2(Nil, z0) -> c
REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
DFSACC#3(Leaf(z0), z1) -> c2
DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))
revApp#2(Nil, z0) -> z0
revApp#2(Cons(z0, z1), z2) -> revApp#2(z1, Cons(z0, z2))
dfsAcc#3(Leaf(z0), z1) -> Cons(z0, z1)
dfsAcc#3(Node(z0, z1), z2) -> dfsAcc#3(z1, dfsAcc#3(z0, z2))
main(z0) -> revApp#2(dfsAcc#3(z0, Nil), Nil)

Types:
REVAPP#2 :: Nil:Cons -> Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: a -> Nil:Cons -> Nil:Cons
c1 :: c:c1 -> c:c1
DFSACC#3 :: Leaf:Node -> Nil:Cons -> c2:c3
Leaf :: a -> Leaf:Node
c2 :: c2:c3
Node :: Leaf:Node -> Leaf:Node -> Leaf:Node
c3 :: c2:c3 -> c2:c3 -> c2:c3
dfsAcc#3 :: Leaf:Node -> Nil:Cons -> Nil:Cons
MAIN :: Leaf:Node -> c4
c4 :: c:c1 -> c2:c3 -> c4
revApp#2 :: Nil:Cons -> Nil:Cons -> Nil:Cons
main :: Leaf:Node -> Nil:Cons
hole_c:c11_5 :: c:c1
hole_Nil:Cons2_5 :: Nil:Cons
hole_a3_5 :: a
hole_c2:c34_5 :: c2:c3
hole_Leaf:Node5_5 :: Leaf:Node
hole_c46_5 :: c4
gen_c:c17_5 :: Nat -> c:c1
gen_Nil:Cons8_5 :: Nat -> Nil:Cons
gen_c2:c39_5 :: Nat -> c2:c3
gen_Leaf:Node10_5 :: Nat -> Leaf:Node


Generator Equations:
gen_c:c17_5(0) <=> c
gen_c:c17_5(+(x, 1)) <=> c1(gen_c:c17_5(x))
gen_Nil:Cons8_5(0) <=> Nil
gen_Nil:Cons8_5(+(x, 1)) <=> Cons(hole_a3_5, gen_Nil:Cons8_5(x))
gen_c2:c39_5(0) <=> c2
gen_c2:c39_5(+(x, 1)) <=> c3(c2, gen_c2:c39_5(x))
gen_Leaf:Node10_5(0) <=> Leaf(hole_a3_5)
gen_Leaf:Node10_5(+(x, 1)) <=> Node(Leaf(hole_a3_5), gen_Leaf:Node10_5(x))


The following defined symbols remain to be analysed:
REVAPP#2, DFSACC#3, dfsAcc#3, revApp#2

They will be analysed ascendingly in the following order:
dfsAcc#3 < DFSACC#3

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REVAPP#2(gen_Nil:Cons8_5(n12_5), gen_Nil:Cons8_5(b)) -> gen_c:c17_5(n12_5), rt in Omega(1 + n12_5)

Induction Base:
REVAPP#2(gen_Nil:Cons8_5(0), gen_Nil:Cons8_5(b)) ->_R^Omega(1)
c

Induction Step:
REVAPP#2(gen_Nil:Cons8_5(+(n12_5, 1)), gen_Nil:Cons8_5(b)) ->_R^Omega(1)
c1(REVAPP#2(gen_Nil:Cons8_5(n12_5), Cons(hole_a3_5, gen_Nil:Cons8_5(b)))) ->_IH
c1(gen_c:c17_5(c13_5))

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:
REVAPP#2(Nil, z0) -> c
REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
DFSACC#3(Leaf(z0), z1) -> c2
DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))
revApp#2(Nil, z0) -> z0
revApp#2(Cons(z0, z1), z2) -> revApp#2(z1, Cons(z0, z2))
dfsAcc#3(Leaf(z0), z1) -> Cons(z0, z1)
dfsAcc#3(Node(z0, z1), z2) -> dfsAcc#3(z1, dfsAcc#3(z0, z2))
main(z0) -> revApp#2(dfsAcc#3(z0, Nil), Nil)

Types:
REVAPP#2 :: Nil:Cons -> Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: a -> Nil:Cons -> Nil:Cons
c1 :: c:c1 -> c:c1
DFSACC#3 :: Leaf:Node -> Nil:Cons -> c2:c3
Leaf :: a -> Leaf:Node
c2 :: c2:c3
Node :: Leaf:Node -> Leaf:Node -> Leaf:Node
c3 :: c2:c3 -> c2:c3 -> c2:c3
dfsAcc#3 :: Leaf:Node -> Nil:Cons -> Nil:Cons
MAIN :: Leaf:Node -> c4
c4 :: c:c1 -> c2:c3 -> c4
revApp#2 :: Nil:Cons -> Nil:Cons -> Nil:Cons
main :: Leaf:Node -> Nil:Cons
hole_c:c11_5 :: c:c1
hole_Nil:Cons2_5 :: Nil:Cons
hole_a3_5 :: a
hole_c2:c34_5 :: c2:c3
hole_Leaf:Node5_5 :: Leaf:Node
hole_c46_5 :: c4
gen_c:c17_5 :: Nat -> c:c1
gen_Nil:Cons8_5 :: Nat -> Nil:Cons
gen_c2:c39_5 :: Nat -> c2:c3
gen_Leaf:Node10_5 :: Nat -> Leaf:Node


Generator Equations:
gen_c:c17_5(0) <=> c
gen_c:c17_5(+(x, 1)) <=> c1(gen_c:c17_5(x))
gen_Nil:Cons8_5(0) <=> Nil
gen_Nil:Cons8_5(+(x, 1)) <=> Cons(hole_a3_5, gen_Nil:Cons8_5(x))
gen_c2:c39_5(0) <=> c2
gen_c2:c39_5(+(x, 1)) <=> c3(c2, gen_c2:c39_5(x))
gen_Leaf:Node10_5(0) <=> Leaf(hole_a3_5)
gen_Leaf:Node10_5(+(x, 1)) <=> Node(Leaf(hole_a3_5), gen_Leaf:Node10_5(x))


The following defined symbols remain to be analysed:
REVAPP#2, DFSACC#3, dfsAcc#3, revApp#2

They will be analysed ascendingly in the following order:
dfsAcc#3 < DFSACC#3

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
REVAPP#2(Nil, z0) -> c
REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
DFSACC#3(Leaf(z0), z1) -> c2
DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))
revApp#2(Nil, z0) -> z0
revApp#2(Cons(z0, z1), z2) -> revApp#2(z1, Cons(z0, z2))
dfsAcc#3(Leaf(z0), z1) -> Cons(z0, z1)
dfsAcc#3(Node(z0, z1), z2) -> dfsAcc#3(z1, dfsAcc#3(z0, z2))
main(z0) -> revApp#2(dfsAcc#3(z0, Nil), Nil)

Types:
REVAPP#2 :: Nil:Cons -> Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: a -> Nil:Cons -> Nil:Cons
c1 :: c:c1 -> c:c1
DFSACC#3 :: Leaf:Node -> Nil:Cons -> c2:c3
Leaf :: a -> Leaf:Node
c2 :: c2:c3
Node :: Leaf:Node -> Leaf:Node -> Leaf:Node
c3 :: c2:c3 -> c2:c3 -> c2:c3
dfsAcc#3 :: Leaf:Node -> Nil:Cons -> Nil:Cons
MAIN :: Leaf:Node -> c4
c4 :: c:c1 -> c2:c3 -> c4
revApp#2 :: Nil:Cons -> Nil:Cons -> Nil:Cons
main :: Leaf:Node -> Nil:Cons
hole_c:c11_5 :: c:c1
hole_Nil:Cons2_5 :: Nil:Cons
hole_a3_5 :: a
hole_c2:c34_5 :: c2:c3
hole_Leaf:Node5_5 :: Leaf:Node
hole_c46_5 :: c4
gen_c:c17_5 :: Nat -> c:c1
gen_Nil:Cons8_5 :: Nat -> Nil:Cons
gen_c2:c39_5 :: Nat -> c2:c3
gen_Leaf:Node10_5 :: Nat -> Leaf:Node


Lemmas:
REVAPP#2(gen_Nil:Cons8_5(n12_5), gen_Nil:Cons8_5(b)) -> gen_c:c17_5(n12_5), rt in Omega(1 + n12_5)


Generator Equations:
gen_c:c17_5(0) <=> c
gen_c:c17_5(+(x, 1)) <=> c1(gen_c:c17_5(x))
gen_Nil:Cons8_5(0) <=> Nil
gen_Nil:Cons8_5(+(x, 1)) <=> Cons(hole_a3_5, gen_Nil:Cons8_5(x))
gen_c2:c39_5(0) <=> c2
gen_c2:c39_5(+(x, 1)) <=> c3(c2, gen_c2:c39_5(x))
gen_Leaf:Node10_5(0) <=> Leaf(hole_a3_5)
gen_Leaf:Node10_5(+(x, 1)) <=> Node(Leaf(hole_a3_5), gen_Leaf:Node10_5(x))


The following defined symbols remain to be analysed:
dfsAcc#3, DFSACC#3, revApp#2

They will be analysed ascendingly in the following order:
dfsAcc#3 < DFSACC#3

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
dfsAcc#3(gen_Leaf:Node10_5(n439_5), gen_Nil:Cons8_5(b)) -> gen_Nil:Cons8_5(+(+(1, n439_5), b)), rt in Omega(0)

Induction Base:
dfsAcc#3(gen_Leaf:Node10_5(0), gen_Nil:Cons8_5(b)) ->_R^Omega(0)
Cons(hole_a3_5, gen_Nil:Cons8_5(b))

Induction Step:
dfsAcc#3(gen_Leaf:Node10_5(+(n439_5, 1)), gen_Nil:Cons8_5(b)) ->_R^Omega(0)
dfsAcc#3(gen_Leaf:Node10_5(n439_5), dfsAcc#3(Leaf(hole_a3_5), gen_Nil:Cons8_5(b))) ->_R^Omega(0)
dfsAcc#3(gen_Leaf:Node10_5(n439_5), Cons(hole_a3_5, gen_Nil:Cons8_5(b))) ->_IH
gen_Nil:Cons8_5(+(+(1, +(b, 1)), c440_5))

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

(22)
Obligation:
Innermost TRS:
Rules:
REVAPP#2(Nil, z0) -> c
REVAPP#2(Cons(z0, z1), z2) -> c1(REVAPP#2(z1, Cons(z0, z2)))
DFSACC#3(Leaf(z0), z1) -> c2
DFSACC#3(Node(z0, z1), z2) -> c3(DFSACC#3(z1, dfsAcc#3(z0, z2)), DFSACC#3(z0, z2))
MAIN(z0) -> c4(REVAPP#2(dfsAcc#3(z0, Nil), Nil), DFSACC#3(z0, Nil))
revApp#2(Nil, z0) -> z0
revApp#2(Cons(z0, z1), z2) -> revApp#2(z1, Cons(z0, z2))
dfsAcc#3(Leaf(z0), z1) -> Cons(z0, z1)
dfsAcc#3(Node(z0, z1), z2) -> dfsAcc#3(z1, dfsAcc#3(z0, z2))
main(z0) -> revApp#2(dfsAcc#3(z0, Nil), Nil)

Types:
REVAPP#2 :: Nil:Cons -> Nil:Cons -> c:c1
Nil :: Nil:Cons
c :: c:c1
Cons :: a -> Nil:Cons -> Nil:Cons
c1 :: c:c1 -> c:c1
DFSACC#3 :: Leaf:Node -> Nil:Cons -> c2:c3
Leaf :: a -> Leaf:Node
c2 :: c2:c3
Node :: Leaf:Node -> Leaf:Node -> Leaf:Node
c3 :: c2:c3 -> c2:c3 -> c2:c3
dfsAcc#3 :: Leaf:Node -> Nil:Cons -> Nil:Cons
MAIN :: Leaf:Node -> c4
c4 :: c:c1 -> c2:c3 -> c4
revApp#2 :: Nil:Cons -> Nil:Cons -> Nil:Cons
main :: Leaf:Node -> Nil:Cons
hole_c:c11_5 :: c:c1
hole_Nil:Cons2_5 :: Nil:Cons
hole_a3_5 :: a
hole_c2:c34_5 :: c2:c3
hole_Leaf:Node5_5 :: Leaf:Node
hole_c46_5 :: c4
gen_c:c17_5 :: Nat -> c:c1
gen_Nil:Cons8_5 :: Nat -> Nil:Cons
gen_c2:c39_5 :: Nat -> c2:c3
gen_Leaf:Node10_5 :: Nat -> Leaf:Node


Lemmas:
REVAPP#2(gen_Nil:Cons8_5(n12_5), gen_Nil:Cons8_5(b)) -> gen_c:c17_5(n12_5), rt in Omega(1 + n12_5)
dfsAcc#3(gen_Leaf:Node10_5(n439_5), gen_Nil:Cons8_5(b)) -> gen_Nil:Cons8_5(+(+(1, n439_5), b)), rt in Omega(0)


Generator Equations:
gen_c:c17_5(0) <=> c
gen_c:c17_5(+(x, 1)) <=> c1(gen_c:c17_5(x))
gen_Nil:Cons8_5(0) <=> Nil
gen_Nil:Cons8_5(+(x, 1)) <=> Cons(hole_a3_5, gen_Nil:Cons8_5(x))
gen_c2:c39_5(0) <=> c2
gen_c2:c39_5(+(x, 1)) <=> c3(c2, gen_c2:c39_5(x))
gen_Leaf:Node10_5(0) <=> Leaf(hole_a3_5)
gen_Leaf:Node10_5(+(x, 1)) <=> Node(Leaf(hole_a3_5), gen_Leaf:Node10_5(x))


The following defined symbols remain to be analysed:
DFSACC#3, revApp#2