WORST_CASE(Omega(n^1),?)
proof of input_S67DXxOgpj.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, INF).

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


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

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


The TRS R consists of the following rules:

   -(x, 0) -> x
   -(0, s(y)) -> 0
   -(s(x), s(y)) -> -(x, y)
   f(0) -> 0
   f(s(x)) -> -(s(x), g(f(x)))
   g(0) -> s(0)
   g(s(x)) -> -(s(x), f(g(x)))

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

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   -(z0, 0) -> z0
   -(0, s(z0)) -> 0
   -(s(z0), s(z1)) -> -(z0, z1)
   f(0) -> 0
   f(s(z0)) -> -(s(z0), g(f(z0)))
   g(0) -> s(0)
   g(s(z0)) -> -(s(z0), f(g(z0)))
Tuples:
   -'(z0, 0) -> c
   -'(0, s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   F(0) -> c3
   F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
   G(0) -> c5
   G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
S tuples:
   -'(z0, 0) -> c
   -'(0, s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   F(0) -> c3
   F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
   G(0) -> c5
   G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
K tuples:none
Defined Rule Symbols:   -_2, f_1, g_1

Defined Pair Symbols:   -'_2, F_1, G_1

Compound Symbols:   c, c1, c2_1, c3, c4_3, c5, c6_3


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

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

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


The TRS R consists of the following rules:

   -'(z0, 0) -> c
   -'(0, s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   F(0) -> c3
   F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
   G(0) -> c5
   G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))

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

   -(z0, 0) -> z0
   -(0, s(z0)) -> 0
   -(s(z0), s(z1)) -> -(z0, z1)
   f(0) -> 0
   f(s(z0)) -> -(s(z0), g(f(z0)))
   g(0) -> s(0)
   g(s(z0)) -> -(s(z0), f(g(z0)))

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

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

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


The TRS R consists of the following rules:

   -'(z0, 0') -> c
   -'(0', s(z0)) -> c1
   -'(s(z0), s(z1)) -> c2(-'(z0, z1))
   F(0') -> c3
   F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
   G(0') -> c5
   G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))

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

   -(z0, 0') -> z0
   -(0', s(z0)) -> 0'
   -(s(z0), s(z1)) -> -(z0, z1)
   f(0') -> 0'
   f(s(z0)) -> -(s(z0), g(f(z0)))
   g(0') -> s(0')
   g(s(z0)) -> -(s(z0), f(g(z0)))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(0', s(z0)) -> c1
-'(s(z0), s(z1)) -> c2(-'(z0, z1))
F(0') -> c3
F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c5
G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
-(z0, 0') -> z0
-(0', s(z0)) -> 0'
-(s(z0), s(z1)) -> -(z0, z1)
f(0') -> 0'
f(s(z0)) -> -(s(z0), g(f(z0)))
g(0') -> s(0')
g(s(z0)) -> -(s(z0), f(g(z0)))

Types:
-' :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
F :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c:c1:c2 -> c5:c6 -> c3:c4 -> c3:c4
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c:c1:c2 -> c3:c4 -> c5:c6 -> c5:c6
- :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_7 :: c:c1:c2
hole_0':s2_7 :: 0':s
hole_c3:c43_7 :: c3:c4
hole_c5:c64_7 :: c5:c6
gen_c:c1:c25_7 :: Nat -> c:c1:c2
gen_0':s6_7 :: Nat -> 0':s
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
-', F, g, f, G, -

They will be analysed ascendingly in the following order:
-' < F
-' < G
g < F
f < F
F = G
g = f
g < G
- < g
f < G
- < f

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

(10)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(0', s(z0)) -> c1
-'(s(z0), s(z1)) -> c2(-'(z0, z1))
F(0') -> c3
F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c5
G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
-(z0, 0') -> z0
-(0', s(z0)) -> 0'
-(s(z0), s(z1)) -> -(z0, z1)
f(0') -> 0'
f(s(z0)) -> -(s(z0), g(f(z0)))
g(0') -> s(0')
g(s(z0)) -> -(s(z0), f(g(z0)))

Types:
-' :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
F :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c:c1:c2 -> c5:c6 -> c3:c4 -> c3:c4
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c:c1:c2 -> c3:c4 -> c5:c6 -> c5:c6
- :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_7 :: c:c1:c2
hole_0':s2_7 :: 0':s
hole_c3:c43_7 :: c3:c4
hole_c5:c64_7 :: c5:c6
gen_c:c1:c25_7 :: Nat -> c:c1:c2
gen_0':s6_7 :: Nat -> 0':s
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Generator Equations:
gen_c:c1:c25_7(0) <=> c
gen_c:c1:c25_7(+(x, 1)) <=> c2(gen_c:c1:c25_7(x))
gen_0':s6_7(0) <=> 0'
gen_0':s6_7(+(x, 1)) <=> s(gen_0':s6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(c, c5, gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c3, gen_c5:c68_7(x))


The following defined symbols remain to be analysed:
-', F, g, f, G, -

They will be analysed ascendingly in the following order:
-' < F
-' < G
g < F
f < F
F = G
g = f
g < G
- < g
f < G
- < f

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-'(gen_0':s6_7(n10_7), gen_0':s6_7(n10_7)) -> gen_c:c1:c25_7(n10_7), rt in Omega(1 + n10_7)

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

Induction Step:
-'(gen_0':s6_7(+(n10_7, 1)), gen_0':s6_7(+(n10_7, 1))) ->_R^Omega(1)
c2(-'(gen_0':s6_7(n10_7), gen_0':s6_7(n10_7))) ->_IH
c2(gen_c:c1:c25_7(c11_7))

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

(12)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(0', s(z0)) -> c1
-'(s(z0), s(z1)) -> c2(-'(z0, z1))
F(0') -> c3
F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c5
G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
-(z0, 0') -> z0
-(0', s(z0)) -> 0'
-(s(z0), s(z1)) -> -(z0, z1)
f(0') -> 0'
f(s(z0)) -> -(s(z0), g(f(z0)))
g(0') -> s(0')
g(s(z0)) -> -(s(z0), f(g(z0)))

Types:
-' :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
F :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c:c1:c2 -> c5:c6 -> c3:c4 -> c3:c4
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c:c1:c2 -> c3:c4 -> c5:c6 -> c5:c6
- :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_7 :: c:c1:c2
hole_0':s2_7 :: 0':s
hole_c3:c43_7 :: c3:c4
hole_c5:c64_7 :: c5:c6
gen_c:c1:c25_7 :: Nat -> c:c1:c2
gen_0':s6_7 :: Nat -> 0':s
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Generator Equations:
gen_c:c1:c25_7(0) <=> c
gen_c:c1:c25_7(+(x, 1)) <=> c2(gen_c:c1:c25_7(x))
gen_0':s6_7(0) <=> 0'
gen_0':s6_7(+(x, 1)) <=> s(gen_0':s6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(c, c5, gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c3, gen_c5:c68_7(x))


The following defined symbols remain to be analysed:
-', F, g, f, G, -

They will be analysed ascendingly in the following order:
-' < F
-' < G
g < F
f < F
F = G
g = f
g < G
- < g
f < G
- < f

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(0', s(z0)) -> c1
-'(s(z0), s(z1)) -> c2(-'(z0, z1))
F(0') -> c3
F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c5
G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
-(z0, 0') -> z0
-(0', s(z0)) -> 0'
-(s(z0), s(z1)) -> -(z0, z1)
f(0') -> 0'
f(s(z0)) -> -(s(z0), g(f(z0)))
g(0') -> s(0')
g(s(z0)) -> -(s(z0), f(g(z0)))

Types:
-' :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
F :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c:c1:c2 -> c5:c6 -> c3:c4 -> c3:c4
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c:c1:c2 -> c3:c4 -> c5:c6 -> c5:c6
- :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_7 :: c:c1:c2
hole_0':s2_7 :: 0':s
hole_c3:c43_7 :: c3:c4
hole_c5:c64_7 :: c5:c6
gen_c:c1:c25_7 :: Nat -> c:c1:c2
gen_0':s6_7 :: Nat -> 0':s
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Lemmas:
-'(gen_0':s6_7(n10_7), gen_0':s6_7(n10_7)) -> gen_c:c1:c25_7(n10_7), rt in Omega(1 + n10_7)


Generator Equations:
gen_c:c1:c25_7(0) <=> c
gen_c:c1:c25_7(+(x, 1)) <=> c2(gen_c:c1:c25_7(x))
gen_0':s6_7(0) <=> 0'
gen_0':s6_7(+(x, 1)) <=> s(gen_0':s6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(c, c5, gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c3, gen_c5:c68_7(x))


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

They will be analysed ascendingly in the following order:
g < F
f < F
F = G
g = f
g < G
- < g
f < G
- < f

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-(gen_0':s6_7(n555_7), gen_0':s6_7(n555_7)) -> gen_0':s6_7(0), rt in Omega(0)

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

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

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:
-'(z0, 0') -> c
-'(0', s(z0)) -> c1
-'(s(z0), s(z1)) -> c2(-'(z0, z1))
F(0') -> c3
F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c5
G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
-(z0, 0') -> z0
-(0', s(z0)) -> 0'
-(s(z0), s(z1)) -> -(z0, z1)
f(0') -> 0'
f(s(z0)) -> -(s(z0), g(f(z0)))
g(0') -> s(0')
g(s(z0)) -> -(s(z0), f(g(z0)))

Types:
-' :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
F :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c:c1:c2 -> c5:c6 -> c3:c4 -> c3:c4
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c:c1:c2 -> c3:c4 -> c5:c6 -> c5:c6
- :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_7 :: c:c1:c2
hole_0':s2_7 :: 0':s
hole_c3:c43_7 :: c3:c4
hole_c5:c64_7 :: c5:c6
gen_c:c1:c25_7 :: Nat -> c:c1:c2
gen_0':s6_7 :: Nat -> 0':s
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Lemmas:
-'(gen_0':s6_7(n10_7), gen_0':s6_7(n10_7)) -> gen_c:c1:c25_7(n10_7), rt in Omega(1 + n10_7)
-(gen_0':s6_7(n555_7), gen_0':s6_7(n555_7)) -> gen_0':s6_7(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c25_7(0) <=> c
gen_c:c1:c25_7(+(x, 1)) <=> c2(gen_c:c1:c25_7(x))
gen_0':s6_7(0) <=> 0'
gen_0':s6_7(+(x, 1)) <=> s(gen_0':s6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(c, c5, gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c3, gen_c5:c68_7(x))


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

They will be analysed ascendingly in the following order:
g < F
f < F
F = G
g = f
g < G
f < G

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
f(gen_0':s6_7(+(1, n1282_7))) -> *9_7, rt in Omega(0)

Induction Base:
f(gen_0':s6_7(+(1, 0)))

Induction Step:
f(gen_0':s6_7(+(1, +(n1282_7, 1)))) ->_R^Omega(0)
-(s(gen_0':s6_7(+(1, n1282_7))), g(f(gen_0':s6_7(+(1, n1282_7))))) ->_IH
-(s(gen_0':s6_7(+(1, n1282_7))), g(*9_7))

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

(20)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(0', s(z0)) -> c1
-'(s(z0), s(z1)) -> c2(-'(z0, z1))
F(0') -> c3
F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c5
G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
-(z0, 0') -> z0
-(0', s(z0)) -> 0'
-(s(z0), s(z1)) -> -(z0, z1)
f(0') -> 0'
f(s(z0)) -> -(s(z0), g(f(z0)))
g(0') -> s(0')
g(s(z0)) -> -(s(z0), f(g(z0)))

Types:
-' :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
F :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c:c1:c2 -> c5:c6 -> c3:c4 -> c3:c4
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c:c1:c2 -> c3:c4 -> c5:c6 -> c5:c6
- :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_7 :: c:c1:c2
hole_0':s2_7 :: 0':s
hole_c3:c43_7 :: c3:c4
hole_c5:c64_7 :: c5:c6
gen_c:c1:c25_7 :: Nat -> c:c1:c2
gen_0':s6_7 :: Nat -> 0':s
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Lemmas:
-'(gen_0':s6_7(n10_7), gen_0':s6_7(n10_7)) -> gen_c:c1:c25_7(n10_7), rt in Omega(1 + n10_7)
-(gen_0':s6_7(n555_7), gen_0':s6_7(n555_7)) -> gen_0':s6_7(0), rt in Omega(0)
f(gen_0':s6_7(+(1, n1282_7))) -> *9_7, rt in Omega(0)


Generator Equations:
gen_c:c1:c25_7(0) <=> c
gen_c:c1:c25_7(+(x, 1)) <=> c2(gen_c:c1:c25_7(x))
gen_0':s6_7(0) <=> 0'
gen_0':s6_7(+(x, 1)) <=> s(gen_0':s6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(c, c5, gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c3, gen_c5:c68_7(x))


The following defined symbols remain to be analysed:
g, F, G

They will be analysed ascendingly in the following order:
g < F
f < F
F = G
g = f
g < G
f < G

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
g(gen_0':s6_7(+(1, n5401_7))) -> *9_7, rt in Omega(0)

Induction Base:
g(gen_0':s6_7(+(1, 0)))

Induction Step:
g(gen_0':s6_7(+(1, +(n5401_7, 1)))) ->_R^Omega(0)
-(s(gen_0':s6_7(+(1, n5401_7))), f(g(gen_0':s6_7(+(1, n5401_7))))) ->_IH
-(s(gen_0':s6_7(+(1, n5401_7))), f(*9_7))

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:
-'(z0, 0') -> c
-'(0', s(z0)) -> c1
-'(s(z0), s(z1)) -> c2(-'(z0, z1))
F(0') -> c3
F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c5
G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
-(z0, 0') -> z0
-(0', s(z0)) -> 0'
-(s(z0), s(z1)) -> -(z0, z1)
f(0') -> 0'
f(s(z0)) -> -(s(z0), g(f(z0)))
g(0') -> s(0')
g(s(z0)) -> -(s(z0), f(g(z0)))

Types:
-' :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
F :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c:c1:c2 -> c5:c6 -> c3:c4 -> c3:c4
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c:c1:c2 -> c3:c4 -> c5:c6 -> c5:c6
- :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_7 :: c:c1:c2
hole_0':s2_7 :: 0':s
hole_c3:c43_7 :: c3:c4
hole_c5:c64_7 :: c5:c6
gen_c:c1:c25_7 :: Nat -> c:c1:c2
gen_0':s6_7 :: Nat -> 0':s
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Lemmas:
-'(gen_0':s6_7(n10_7), gen_0':s6_7(n10_7)) -> gen_c:c1:c25_7(n10_7), rt in Omega(1 + n10_7)
-(gen_0':s6_7(n555_7), gen_0':s6_7(n555_7)) -> gen_0':s6_7(0), rt in Omega(0)
f(gen_0':s6_7(+(1, n1282_7))) -> *9_7, rt in Omega(0)
g(gen_0':s6_7(+(1, n5401_7))) -> *9_7, rt in Omega(0)


Generator Equations:
gen_c:c1:c25_7(0) <=> c
gen_c:c1:c25_7(+(x, 1)) <=> c2(gen_c:c1:c25_7(x))
gen_0':s6_7(0) <=> 0'
gen_0':s6_7(+(x, 1)) <=> s(gen_0':s6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(c, c5, gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c3, gen_c5:c68_7(x))


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

They will be analysed ascendingly in the following order:
g < F
f < F
F = G
g = f
g < G
f < G

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
f(gen_0':s6_7(+(1, n65737_7))) -> *9_7, rt in Omega(0)

Induction Base:
f(gen_0':s6_7(+(1, 0)))

Induction Step:
f(gen_0':s6_7(+(1, +(n65737_7, 1)))) ->_R^Omega(0)
-(s(gen_0':s6_7(+(1, n65737_7))), g(f(gen_0':s6_7(+(1, n65737_7))))) ->_IH
-(s(gen_0':s6_7(+(1, n65737_7))), g(*9_7))

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:
-'(z0, 0') -> c
-'(0', s(z0)) -> c1
-'(s(z0), s(z1)) -> c2(-'(z0, z1))
F(0') -> c3
F(s(z0)) -> c4(-'(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c5
G(s(z0)) -> c6(-'(s(z0), f(g(z0))), F(g(z0)), G(z0))
-(z0, 0') -> z0
-(0', s(z0)) -> 0'
-(s(z0), s(z1)) -> -(z0, z1)
f(0') -> 0'
f(s(z0)) -> -(s(z0), g(f(z0)))
g(0') -> s(0')
g(s(z0)) -> -(s(z0), f(g(z0)))

Types:
-' :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
F :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c:c1:c2 -> c5:c6 -> c3:c4 -> c3:c4
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c5:c6
c5 :: c5:c6
c6 :: c:c1:c2 -> c3:c4 -> c5:c6 -> c5:c6
- :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_7 :: c:c1:c2
hole_0':s2_7 :: 0':s
hole_c3:c43_7 :: c3:c4
hole_c5:c64_7 :: c5:c6
gen_c:c1:c25_7 :: Nat -> c:c1:c2
gen_0':s6_7 :: Nat -> 0':s
gen_c3:c47_7 :: Nat -> c3:c4
gen_c5:c68_7 :: Nat -> c5:c6


Lemmas:
-'(gen_0':s6_7(n10_7), gen_0':s6_7(n10_7)) -> gen_c:c1:c25_7(n10_7), rt in Omega(1 + n10_7)
-(gen_0':s6_7(n555_7), gen_0':s6_7(n555_7)) -> gen_0':s6_7(0), rt in Omega(0)
f(gen_0':s6_7(+(1, n65737_7))) -> *9_7, rt in Omega(0)
g(gen_0':s6_7(+(1, n5401_7))) -> *9_7, rt in Omega(0)


Generator Equations:
gen_c:c1:c25_7(0) <=> c
gen_c:c1:c25_7(+(x, 1)) <=> c2(gen_c:c1:c25_7(x))
gen_0':s6_7(0) <=> 0'
gen_0':s6_7(+(x, 1)) <=> s(gen_0':s6_7(x))
gen_c3:c47_7(0) <=> c3
gen_c3:c47_7(+(x, 1)) <=> c4(c, c5, gen_c3:c47_7(x))
gen_c5:c68_7(0) <=> c5
gen_c5:c68_7(+(x, 1)) <=> c6(c, c3, gen_c5:c68_7(x))


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

They will be analysed ascendingly in the following order:
F = G