WORST_CASE(Omega(n^1),?)
proof of input_MviL8TbvVO.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), 3 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 309 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), 56 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 1572 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 2299 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 2692 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:

   minus(x, 0) -> x
   minus(s(x), s(y)) -> minus(x, y)
   f(0) -> s(0)
   f(s(x)) -> minus(s(x), g(f(x)))
   g(0) -> 0
   g(s(x)) -> minus(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:
   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   f(0) -> s(0)
   f(s(z0)) -> minus(s(z0), g(f(z0)))
   g(0) -> 0
   g(s(z0)) -> minus(s(z0), f(g(z0)))
Tuples:
   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   F(0) -> c2
   F(s(z0)) -> c3(MINUS(s(z0), g(f(z0))), G(f(z0)), F(z0))
   G(0) -> c4
   G(s(z0)) -> c5(MINUS(s(z0), f(g(z0))), F(g(z0)), G(z0))
S tuples:
   MINUS(z0, 0) -> c
   MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
   F(0) -> c2
   F(s(z0)) -> c3(MINUS(s(z0), g(f(z0))), G(f(z0)), F(z0))
   G(0) -> c4
   G(s(z0)) -> c5(MINUS(s(z0), f(g(z0))), F(g(z0)), G(z0))
K tuples:none
Defined Rule Symbols:   minus_2, f_1, g_1

Defined Pair Symbols:   MINUS_2, F_1, G_1

Compound Symbols:   c, c1_1, c2, c3_3, c4, c5_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:

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

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

   minus(z0, 0) -> z0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   f(0) -> s(0)
   f(s(z0)) -> minus(s(z0), g(f(z0)))
   g(0) -> 0
   g(s(z0)) -> minus(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:

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

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

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

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

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

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

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
F :: 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c4:c5 -> c2:c3 -> c2:c3
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5 -> c4:c5
minus :: 0':s -> 0':s -> 0':s
hole_c:c11_6 :: c:c1
hole_0':s2_6 :: 0':s
hole_c2:c33_6 :: c2:c3
hole_c4:c54_6 :: c4:c5
gen_c:c15_6 :: Nat -> c:c1
gen_0':s6_6 :: Nat -> 0':s
gen_c2:c37_6 :: Nat -> c2:c3
gen_c4:c58_6 :: Nat -> c4:c5

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

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

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

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

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

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
F :: 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c4:c5 -> c2:c3 -> c2:c3
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5 -> c4:c5
minus :: 0':s -> 0':s -> 0':s
hole_c:c11_6 :: c:c1
hole_0':s2_6 :: 0':s
hole_c2:c33_6 :: c2:c3
hole_c4:c54_6 :: c4:c5
gen_c:c15_6 :: Nat -> c:c1
gen_0':s6_6 :: Nat -> 0':s
gen_c2:c37_6 :: Nat -> c2:c3
gen_c4:c58_6 :: Nat -> c4:c5


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_0':s6_6(0) <=> 0'
gen_0':s6_6(+(x, 1)) <=> s(gen_0':s6_6(x))
gen_c2:c37_6(0) <=> c2
gen_c2:c37_6(+(x, 1)) <=> c3(c, c4, gen_c2:c37_6(x))
gen_c4:c58_6(0) <=> c4
gen_c4:c58_6(+(x, 1)) <=> c5(c, c2, gen_c4:c58_6(x))


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

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

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINUS(gen_0':s6_6(n10_6), gen_0':s6_6(n10_6)) -> gen_c:c15_6(n10_6), rt in Omega(1 + n10_6)

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

Induction Step:
MINUS(gen_0':s6_6(+(n10_6, 1)), gen_0':s6_6(+(n10_6, 1))) ->_R^Omega(1)
c1(MINUS(gen_0':s6_6(n10_6), gen_0':s6_6(n10_6))) ->_IH
c1(gen_c:c15_6(c11_6))

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

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
F :: 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c4:c5 -> c2:c3 -> c2:c3
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5 -> c4:c5
minus :: 0':s -> 0':s -> 0':s
hole_c:c11_6 :: c:c1
hole_0':s2_6 :: 0':s
hole_c2:c33_6 :: c2:c3
hole_c4:c54_6 :: c4:c5
gen_c:c15_6 :: Nat -> c:c1
gen_0':s6_6 :: Nat -> 0':s
gen_c2:c37_6 :: Nat -> c2:c3
gen_c4:c58_6 :: Nat -> c4:c5


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_0':s6_6(0) <=> 0'
gen_0':s6_6(+(x, 1)) <=> s(gen_0':s6_6(x))
gen_c2:c37_6(0) <=> c2
gen_c2:c37_6(+(x, 1)) <=> c3(c, c4, gen_c2:c37_6(x))
gen_c4:c58_6(0) <=> c4
gen_c4:c58_6(+(x, 1)) <=> c5(c, c2, gen_c4:c58_6(x))


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

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

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

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

(15)
BOUNDS(n^1, INF)

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

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

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
F :: 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c4:c5 -> c2:c3 -> c2:c3
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5 -> c4:c5
minus :: 0':s -> 0':s -> 0':s
hole_c:c11_6 :: c:c1
hole_0':s2_6 :: 0':s
hole_c2:c33_6 :: c2:c3
hole_c4:c54_6 :: c4:c5
gen_c:c15_6 :: Nat -> c:c1
gen_0':s6_6 :: Nat -> 0':s
gen_c2:c37_6 :: Nat -> c2:c3
gen_c4:c58_6 :: Nat -> c4:c5


Lemmas:
MINUS(gen_0':s6_6(n10_6), gen_0':s6_6(n10_6)) -> gen_c:c15_6(n10_6), rt in Omega(1 + n10_6)


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_0':s6_6(0) <=> 0'
gen_0':s6_6(+(x, 1)) <=> s(gen_0':s6_6(x))
gen_c2:c37_6(0) <=> c2
gen_c2:c37_6(+(x, 1)) <=> c3(c, c4, gen_c2:c37_6(x))
gen_c4:c58_6(0) <=> c4
gen_c4:c58_6(+(x, 1)) <=> c5(c, c2, gen_c4:c58_6(x))


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

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

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

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

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

Induction Step:
minus(gen_0':s6_6(+(n351_6, 1)), gen_0':s6_6(+(n351_6, 1))) ->_R^Omega(0)
minus(gen_0':s6_6(n351_6), gen_0':s6_6(n351_6)) ->_IH
gen_0':s6_6(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:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
F(0') -> c2
F(s(z0)) -> c3(MINUS(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c4
G(s(z0)) -> c5(MINUS(s(z0), f(g(z0))), F(g(z0)), G(z0))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
f(0') -> s(0')
f(s(z0)) -> minus(s(z0), g(f(z0)))
g(0') -> 0'
g(s(z0)) -> minus(s(z0), f(g(z0)))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
F :: 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c4:c5 -> c2:c3 -> c2:c3
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5 -> c4:c5
minus :: 0':s -> 0':s -> 0':s
hole_c:c11_6 :: c:c1
hole_0':s2_6 :: 0':s
hole_c2:c33_6 :: c2:c3
hole_c4:c54_6 :: c4:c5
gen_c:c15_6 :: Nat -> c:c1
gen_0':s6_6 :: Nat -> 0':s
gen_c2:c37_6 :: Nat -> c2:c3
gen_c4:c58_6 :: Nat -> c4:c5


Lemmas:
MINUS(gen_0':s6_6(n10_6), gen_0':s6_6(n10_6)) -> gen_c:c15_6(n10_6), rt in Omega(1 + n10_6)
minus(gen_0':s6_6(n351_6), gen_0':s6_6(n351_6)) -> gen_0':s6_6(0), rt in Omega(0)


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_0':s6_6(0) <=> 0'
gen_0':s6_6(+(x, 1)) <=> s(gen_0':s6_6(x))
gen_c2:c37_6(0) <=> c2
gen_c2:c37_6(+(x, 1)) <=> c3(c, c4, gen_c2:c37_6(x))
gen_c4:c58_6(0) <=> c4
gen_c4:c58_6(+(x, 1)) <=> c5(c, c2, gen_c4:c58_6(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_6(+(1, n895_6))) -> *9_6, rt in Omega(0)

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

Induction Step:
f(gen_0':s6_6(+(1, +(n895_6, 1)))) ->_R^Omega(0)
minus(s(gen_0':s6_6(+(1, n895_6))), g(f(gen_0':s6_6(+(1, n895_6))))) ->_IH
minus(s(gen_0':s6_6(+(1, n895_6))), g(*9_6))

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

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
F :: 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c4:c5 -> c2:c3 -> c2:c3
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5 -> c4:c5
minus :: 0':s -> 0':s -> 0':s
hole_c:c11_6 :: c:c1
hole_0':s2_6 :: 0':s
hole_c2:c33_6 :: c2:c3
hole_c4:c54_6 :: c4:c5
gen_c:c15_6 :: Nat -> c:c1
gen_0':s6_6 :: Nat -> 0':s
gen_c2:c37_6 :: Nat -> c2:c3
gen_c4:c58_6 :: Nat -> c4:c5


Lemmas:
MINUS(gen_0':s6_6(n10_6), gen_0':s6_6(n10_6)) -> gen_c:c15_6(n10_6), rt in Omega(1 + n10_6)
minus(gen_0':s6_6(n351_6), gen_0':s6_6(n351_6)) -> gen_0':s6_6(0), rt in Omega(0)
f(gen_0':s6_6(+(1, n895_6))) -> *9_6, rt in Omega(0)


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_0':s6_6(0) <=> 0'
gen_0':s6_6(+(x, 1)) <=> s(gen_0':s6_6(x))
gen_c2:c37_6(0) <=> c2
gen_c2:c37_6(+(x, 1)) <=> c3(c, c4, gen_c2:c37_6(x))
gen_c4:c58_6(0) <=> c4
gen_c4:c58_6(+(x, 1)) <=> c5(c, c2, gen_c4:c58_6(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_6(+(1, n4671_6))) -> *9_6, rt in Omega(0)

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

Induction Step:
g(gen_0':s6_6(+(1, +(n4671_6, 1)))) ->_R^Omega(0)
minus(s(gen_0':s6_6(+(1, n4671_6))), f(g(gen_0':s6_6(+(1, n4671_6))))) ->_IH
minus(s(gen_0':s6_6(+(1, n4671_6))), f(*9_6))

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

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
F :: 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c4:c5 -> c2:c3 -> c2:c3
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5 -> c4:c5
minus :: 0':s -> 0':s -> 0':s
hole_c:c11_6 :: c:c1
hole_0':s2_6 :: 0':s
hole_c2:c33_6 :: c2:c3
hole_c4:c54_6 :: c4:c5
gen_c:c15_6 :: Nat -> c:c1
gen_0':s6_6 :: Nat -> 0':s
gen_c2:c37_6 :: Nat -> c2:c3
gen_c4:c58_6 :: Nat -> c4:c5


Lemmas:
MINUS(gen_0':s6_6(n10_6), gen_0':s6_6(n10_6)) -> gen_c:c15_6(n10_6), rt in Omega(1 + n10_6)
minus(gen_0':s6_6(n351_6), gen_0':s6_6(n351_6)) -> gen_0':s6_6(0), rt in Omega(0)
f(gen_0':s6_6(+(1, n895_6))) -> *9_6, rt in Omega(0)
g(gen_0':s6_6(+(1, n4671_6))) -> *9_6, rt in Omega(0)


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_0':s6_6(0) <=> 0'
gen_0':s6_6(+(x, 1)) <=> s(gen_0':s6_6(x))
gen_c2:c37_6(0) <=> c2
gen_c2:c37_6(+(x, 1)) <=> c3(c, c4, gen_c2:c37_6(x))
gen_c4:c58_6(0) <=> c4
gen_c4:c58_6(+(x, 1)) <=> c5(c, c2, gen_c4:c58_6(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_6(+(1, n63269_6))) -> *9_6, rt in Omega(0)

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

Induction Step:
f(gen_0':s6_6(+(1, +(n63269_6, 1)))) ->_R^Omega(0)
minus(s(gen_0':s6_6(+(1, n63269_6))), g(f(gen_0':s6_6(+(1, n63269_6))))) ->_IH
minus(s(gen_0':s6_6(+(1, n63269_6))), g(*9_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:
MINUS(z0, 0') -> c
MINUS(s(z0), s(z1)) -> c1(MINUS(z0, z1))
F(0') -> c2
F(s(z0)) -> c3(MINUS(s(z0), g(f(z0))), G(f(z0)), F(z0))
G(0') -> c4
G(s(z0)) -> c5(MINUS(s(z0), f(g(z0))), F(g(z0)), G(z0))
minus(z0, 0') -> z0
minus(s(z0), s(z1)) -> minus(z0, z1)
f(0') -> s(0')
f(s(z0)) -> minus(s(z0), g(f(z0)))
g(0') -> 0'
g(s(z0)) -> minus(s(z0), f(g(z0)))

Types:
MINUS :: 0':s -> 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
F :: 0':s -> c2:c3
c2 :: c2:c3
c3 :: c:c1 -> c4:c5 -> c2:c3 -> c2:c3
g :: 0':s -> 0':s
f :: 0':s -> 0':s
G :: 0':s -> c4:c5
c4 :: c4:c5
c5 :: c:c1 -> c2:c3 -> c4:c5 -> c4:c5
minus :: 0':s -> 0':s -> 0':s
hole_c:c11_6 :: c:c1
hole_0':s2_6 :: 0':s
hole_c2:c33_6 :: c2:c3
hole_c4:c54_6 :: c4:c5
gen_c:c15_6 :: Nat -> c:c1
gen_0':s6_6 :: Nat -> 0':s
gen_c2:c37_6 :: Nat -> c2:c3
gen_c4:c58_6 :: Nat -> c4:c5


Lemmas:
MINUS(gen_0':s6_6(n10_6), gen_0':s6_6(n10_6)) -> gen_c:c15_6(n10_6), rt in Omega(1 + n10_6)
minus(gen_0':s6_6(n351_6), gen_0':s6_6(n351_6)) -> gen_0':s6_6(0), rt in Omega(0)
f(gen_0':s6_6(+(1, n63269_6))) -> *9_6, rt in Omega(0)
g(gen_0':s6_6(+(1, n4671_6))) -> *9_6, rt in Omega(0)


Generator Equations:
gen_c:c15_6(0) <=> c
gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x))
gen_0':s6_6(0) <=> 0'
gen_0':s6_6(+(x, 1)) <=> s(gen_0':s6_6(x))
gen_c2:c37_6(0) <=> c2
gen_c2:c37_6(+(x, 1)) <=> c3(c, c4, gen_c2:c37_6(x))
gen_c4:c58_6(0) <=> c4
gen_c4:c58_6(+(x, 1)) <=> c5(c, c2, gen_c4:c58_6(x))


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

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