WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox2/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, n^1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 252 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 6 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CdtProblem
    (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 33 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 15 ms]
    (16) CdtProblem
    (17) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) BOUNDS(1, 1)
(19) RenamingProof [BOTH BOUNDS(ID, ID), 4 ms]
(20) CpxRelTRS
    (21) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) typed CpxTrs
    (23) OrderProof [LOWER BOUND(ID), 12 ms]
    (24) typed CpxTrs
    (25) RewriteLemmaProof [LOWER BOUND(ID), 267 ms]
    (26) BEST
        (27) proven lower bound
            (28) LowerBoundPropagationProof [FINISHED, 0 ms]
            (29) BOUNDS(n^1, INF)
        (30) typed CpxTrs
            (31) RewriteLemmaProof [LOWER BOUND(ID), 29 ms]
            (32) typed CpxTrs


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

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


The TRS R consists of the following rules:

   F(0) -> c1
   F(1) -> c2
   F(s(z0)) -> c3(F(z0))
   IF(true, s(z0), s(z1)) -> c4
   IF(false, s(z0), s(z1)) -> c5
   G(z0, c(z1)) -> c6(G(z0, z1))
   G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
   G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))

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

   f(0) -> true
   f(1) -> false
   f(s(z0)) -> f(z0)
   if(true, s(z0), s(z1)) -> s(z0)
   if(false, s(z0), s(z1)) -> s(z1)
   g(z0, c(z1)) -> c(g(z0, z1))
   g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))

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, n^1).


The TRS R consists of the following rules:

   F(0) -> c1
   F(1) -> c2
   F(s(z0)) -> c3(F(z0))
   IF(true, s(z0), s(z1)) -> c4
   IF(false, s(z0), s(z1)) -> c5
   G(z0, c(z1)) -> c6(G(z0, z1))
   G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
   G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))

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

   f(0) -> true
   f(1) -> false
   f(s(z0)) -> f(z0)
   if(true, s(z0), s(z1)) -> s(z0)
   if(false, s(z0), s(z1)) -> s(z1)
   g(z0, c(z1)) -> c(g(z0, z1))
   g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))

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

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(0) -> true
   f(1) -> false
   f(s(z0)) -> f(z0)
   if(true, s(z0), s(z1)) -> s(z0)
   if(false, s(z0), s(z1)) -> s(z1)
   g(z0, c(z1)) -> c(g(z0, z1))
   g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))
   F(0) -> c1
   F(1) -> c2
   F(s(z0)) -> c3(F(z0))
   IF(true, s(z0), s(z1)) -> c4
   IF(false, s(z0), s(z1)) -> c5
   G(z0, c(z1)) -> c6(G(z0, z1))
   G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
   G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
Tuples:
   F'(0) -> c9
   F'(1) -> c10
   F'(s(z0)) -> c11(F'(z0))
   IF'(true, s(z0), s(z1)) -> c12
   IF'(false, s(z0), s(z1)) -> c13
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   G'(z0, c(z1)) -> c15(G'(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1))
   F''(0) -> c16
   F''(1) -> c17
   F''(s(z0)) -> c18(F''(z0))
   IF''(true, s(z0), s(z1)) -> c19
   IF''(false, s(z0), s(z1)) -> c20
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c22(G''(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), IF''(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), F''(z0))
   G''(z0, c(z1)) -> c23(G''(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), IF''(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
S tuples:
   F''(0) -> c16
   F''(1) -> c17
   F''(s(z0)) -> c18(F''(z0))
   IF''(true, s(z0), s(z1)) -> c19
   IF''(false, s(z0), s(z1)) -> c20
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c22(G''(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), IF''(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), F''(z0))
   G''(z0, c(z1)) -> c23(G''(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), IF''(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
K tuples:none
Defined Rule Symbols:   F_1, IF_3, G_2, f_1, if_3, g_2

Defined Pair Symbols:   F'_1, IF'_3, G'_2, F''_1, IF''_3, G''_2

Compound Symbols:   c9, c10, c11_1, c12, c13, c14_1, c15_4, c16, c17, c18_1, c19, c20, c21_1, c22_8, c23_8


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 8 trailing nodes:
   F''(0) -> c16
   IF'(true, s(z0), s(z1)) -> c12
   IF''(true, s(z0), s(z1)) -> c19
   IF'(false, s(z0), s(z1)) -> c13
   F'(1) -> c10
   IF''(false, s(z0), s(z1)) -> c20
   F''(1) -> c17
   F'(0) -> c9

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(0) -> true
   f(1) -> false
   f(s(z0)) -> f(z0)
   if(true, s(z0), s(z1)) -> s(z0)
   if(false, s(z0), s(z1)) -> s(z1)
   g(z0, c(z1)) -> c(g(z0, z1))
   g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))
   F(0) -> c1
   F(1) -> c2
   F(s(z0)) -> c3(F(z0))
   IF(true, s(z0), s(z1)) -> c4
   IF(false, s(z0), s(z1)) -> c5
   G(z0, c(z1)) -> c6(G(z0, z1))
   G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
   G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
Tuples:
   F'(s(z0)) -> c11(F'(z0))
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   G'(z0, c(z1)) -> c15(G'(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1))
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c22(G''(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), IF''(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), F''(z0))
   G''(z0, c(z1)) -> c23(G''(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), IF''(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
S tuples:
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c22(G''(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), IF''(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), F''(z0))
   G''(z0, c(z1)) -> c23(G''(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF'(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), IF''(f(z0), c(g(s(z0), z1)), c(z1)), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
K tuples:none
Defined Rule Symbols:   F_1, IF_3, G_2, f_1, if_3, g_2

Defined Pair Symbols:   F'_1, G'_2, F''_1, G''_2

Compound Symbols:   c11_1, c14_1, c15_4, c18_1, c21_1, c22_8, c23_8


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

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 8 trailing tuple parts
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(0) -> true
   f(1) -> false
   f(s(z0)) -> f(z0)
   if(true, s(z0), s(z1)) -> s(z0)
   if(false, s(z0), s(z1)) -> s(z1)
   g(z0, c(z1)) -> c(g(z0, z1))
   g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))
   F(0) -> c1
   F(1) -> c2
   F(s(z0)) -> c3(F(z0))
   IF(true, s(z0), s(z1)) -> c4
   IF(false, s(z0), s(z1)) -> c5
   G(z0, c(z1)) -> c6(G(z0, z1))
   G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
   G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
Tuples:
   F'(s(z0)) -> c11(F'(z0))
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G'(z0, c(z1)) -> c15(F'(z0), G'(s(z0), z1))
   G''(z0, c(z1)) -> c22(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), F''(z0))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
S tuples:
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c22(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), F''(z0))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
K tuples:none
Defined Rule Symbols:   F_1, IF_3, G_2, f_1, if_3, g_2

Defined Pair Symbols:   F'_1, G'_2, F''_1, G''_2

Compound Symbols:   c11_1, c14_1, c18_1, c21_1, c15_2, c22_5, c23_5


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

(9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(0) -> true
   f(1) -> false
   f(s(z0)) -> f(z0)
   if(true, s(z0), s(z1)) -> s(z0)
   if(false, s(z0), s(z1)) -> s(z1)
   g(z0, c(z1)) -> c(g(z0, z1))
   g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))
   F(0) -> c1
   F(1) -> c2
   F(s(z0)) -> c3(F(z0))
   IF(true, s(z0), s(z1)) -> c4
   IF(false, s(z0), s(z1)) -> c5
   G(z0, c(z1)) -> c6(G(z0, z1))
   G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
   G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
Tuples:
   F'(s(z0)) -> c11(F'(z0))
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G'(z0, c(z1)) -> c15(F'(z0), G'(s(z0), z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
S tuples:
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
K tuples:none
Defined Rule Symbols:   F_1, IF_3, G_2, f_1, if_3, g_2

Defined Pair Symbols:   F'_1, G'_2, F''_1, G''_2

Compound Symbols:   c11_1, c14_1, c18_1, c21_1, c15_2, c23_5, c9_1


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

(11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   f(0) -> true
   f(1) -> false
   f(s(z0)) -> f(z0)
   if(true, s(z0), s(z1)) -> s(z0)
   if(false, s(z0), s(z1)) -> s(z1)
   g(z0, c(z1)) -> c(g(z0, z1))
   g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))
   F(0) -> c1
   F(1) -> c2
   F(s(z0)) -> c3(F(z0))
   IF(true, s(z0), s(z1)) -> c4
   IF(false, s(z0), s(z1)) -> c5
   G(z0, c(z1)) -> c6(G(z0, z1))
   G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
   G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F'(s(z0)) -> c11(F'(z0))
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G'(z0, c(z1)) -> c15(F'(z0), G'(s(z0), z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
S tuples:
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   F'_1, G'_2, F''_1, G''_2

Compound Symbols:   c11_1, c14_1, c18_1, c21_1, c15_2, c23_5, c9_1


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

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
We considered the (Usable) Rules:none
And the Tuples:
   F'(s(z0)) -> c11(F'(z0))
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G'(z0, c(z1)) -> c15(F'(z0), G'(s(z0), z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(F'(x_1)) = 0
   POL(F''(x_1)) = [3] + [2]x_1
   POL(G'(x_1, x_2)) = 0
   POL(G''(x_1, x_2)) = [2] + [3]x_1 + [3]x_2
   POL(c(x_1)) = [2] + x_1
   POL(c11(x_1)) = x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1)) = x_1
   POL(c21(x_1)) = x_1
   POL(c23(x_1, x_2, x_3, x_4, x_5)) = x_1 + x_2 + x_3 + x_4 + x_5
   POL(c9(x_1)) = x_1
   POL(s(x_1)) = x_1

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F'(s(z0)) -> c11(F'(z0))
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G'(z0, c(z1)) -> c15(F'(z0), G'(s(z0), z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
S tuples:
   F''(s(z0)) -> c18(F''(z0))
K tuples:
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
Defined Rule Symbols:none

Defined Pair Symbols:   F'_1, G'_2, F''_1, G''_2

Compound Symbols:   c11_1, c14_1, c18_1, c21_1, c15_2, c23_5, c9_1


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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   F''(s(z0)) -> c18(F''(z0))
We considered the (Usable) Rules:none
And the Tuples:
   F'(s(z0)) -> c11(F'(z0))
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G'(z0, c(z1)) -> c15(F'(z0), G'(s(z0), z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(F'(x_1)) = 0
   POL(F''(x_1)) = [1] + x_1
   POL(G'(x_1, x_2)) = 0
   POL(G''(x_1, x_2)) = x_1 + x_2
   POL(c(x_1)) = [1] + x_1
   POL(c11(x_1)) = x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1, x_2)) = x_1 + x_2
   POL(c18(x_1)) = x_1
   POL(c21(x_1)) = x_1
   POL(c23(x_1, x_2, x_3, x_4, x_5)) = x_1 + x_2 + x_3 + x_4 + x_5
   POL(c9(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F'(s(z0)) -> c11(F'(z0))
   G'(z0, c(z1)) -> c14(G'(z0, z1))
   F''(s(z0)) -> c18(F''(z0))
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G'(z0, c(z1)) -> c15(F'(z0), G'(s(z0), z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
S tuples:none
K tuples:
   G''(z0, c(z1)) -> c21(G''(z0, z1))
   G''(z0, c(z1)) -> c23(F'(z0), G'(s(z0), z1), F'(z0), G'(s(z0), z1), G''(s(z0), z1))
   G''(z0, c(z1)) -> c9(F'(z0))
   G''(z0, c(z1)) -> c9(G'(s(z0), z1))
   G''(z0, c(z1)) -> c9(F''(z0))
   F''(s(z0)) -> c18(F''(z0))
Defined Rule Symbols:none

Defined Pair Symbols:   F'_1, G'_2, F''_1, G''_2

Compound Symbols:   c11_1, c14_1, c18_1, c21_1, c15_2, c23_5, c9_1


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

(17) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(18)
BOUNDS(1, 1)

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

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

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

   F(0') -> c1
   F(1') -> c2
   F(s(z0)) -> c3(F(z0))
   IF(true, s(z0), s(z1)) -> c4
   IF(false, s(z0), s(z1)) -> c5
   G(z0, c(z1)) -> c6(G(z0, z1))
   G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
   G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))

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

   f(0') -> true
   f(1') -> false
   f(s(z0)) -> f(z0)
   if(true, s(z0), s(z1)) -> s(z0)
   if(false, s(z0), s(z1)) -> s(z1)
   g(z0, c(z1)) -> c(g(z0, z1))
   g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))

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

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

(22)
Obligation:
Innermost TRS:
Rules:
F(0') -> c1
F(1') -> c2
F(s(z0)) -> c3(F(z0))
IF(true, s(z0), s(z1)) -> c4
IF(false, s(z0), s(z1)) -> c5
G(z0, c(z1)) -> c6(G(z0, z1))
G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
f(0') -> true
f(1') -> false
f(s(z0)) -> f(z0)
if(true, s(z0), s(z1)) -> s(z0)
if(false, s(z0), s(z1)) -> s(z1)
g(z0, c(z1)) -> c(g(z0, z1))
g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))

Types:
F :: 0':1':s:c -> c1:c2:c3
0' :: 0':1':s:c
c1 :: c1:c2:c3
1' :: 0':1':s:c
c2 :: c1:c2:c3
s :: 0':1':s:c -> 0':1':s:c
c3 :: c1:c2:c3 -> c1:c2:c3
IF :: true:false -> 0':1':s:c -> 0':1':s:c -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
G :: 0':1':s:c -> 0':1':s:c -> c6:c7:c8
c :: 0':1':s:c -> 0':1':s:c
c6 :: c6:c7:c8 -> c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c1:c2:c3 -> c6:c7:c8
if :: true:false -> 0':1':s:c -> 0':1':s:c -> 0':1':s:c
f :: 0':1':s:c -> true:false
g :: 0':1':s:c -> 0':1':s:c -> 0':1':s:c
c8 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8 -> c6:c7:c8
hole_c1:c2:c31_9 :: c1:c2:c3
hole_0':1':s:c2_9 :: 0':1':s:c
hole_c4:c53_9 :: c4:c5
hole_true:false4_9 :: true:false
hole_c6:c7:c85_9 :: c6:c7:c8
gen_c1:c2:c36_9 :: Nat -> c1:c2:c3
gen_0':1':s:c7_9 :: Nat -> 0':1':s:c
gen_c6:c7:c88_9 :: Nat -> c6:c7:c8

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

(23) 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
f < G
g < G
f < g

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

(24)
Obligation:
Innermost TRS:
Rules:
F(0') -> c1
F(1') -> c2
F(s(z0)) -> c3(F(z0))
IF(true, s(z0), s(z1)) -> c4
IF(false, s(z0), s(z1)) -> c5
G(z0, c(z1)) -> c6(G(z0, z1))
G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
f(0') -> true
f(1') -> false
f(s(z0)) -> f(z0)
if(true, s(z0), s(z1)) -> s(z0)
if(false, s(z0), s(z1)) -> s(z1)
g(z0, c(z1)) -> c(g(z0, z1))
g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))

Types:
F :: 0':1':s:c -> c1:c2:c3
0' :: 0':1':s:c
c1 :: c1:c2:c3
1' :: 0':1':s:c
c2 :: c1:c2:c3
s :: 0':1':s:c -> 0':1':s:c
c3 :: c1:c2:c3 -> c1:c2:c3
IF :: true:false -> 0':1':s:c -> 0':1':s:c -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
G :: 0':1':s:c -> 0':1':s:c -> c6:c7:c8
c :: 0':1':s:c -> 0':1':s:c
c6 :: c6:c7:c8 -> c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c1:c2:c3 -> c6:c7:c8
if :: true:false -> 0':1':s:c -> 0':1':s:c -> 0':1':s:c
f :: 0':1':s:c -> true:false
g :: 0':1':s:c -> 0':1':s:c -> 0':1':s:c
c8 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8 -> c6:c7:c8
hole_c1:c2:c31_9 :: c1:c2:c3
hole_0':1':s:c2_9 :: 0':1':s:c
hole_c4:c53_9 :: c4:c5
hole_true:false4_9 :: true:false
hole_c6:c7:c85_9 :: c6:c7:c8
gen_c1:c2:c36_9 :: Nat -> c1:c2:c3
gen_0':1':s:c7_9 :: Nat -> 0':1':s:c
gen_c6:c7:c88_9 :: Nat -> c6:c7:c8


Generator Equations:
gen_c1:c2:c36_9(0) <=> c1
gen_c1:c2:c36_9(+(x, 1)) <=> c3(gen_c1:c2:c36_9(x))
gen_0':1':s:c7_9(0) <=> 0'
gen_0':1':s:c7_9(+(x, 1)) <=> s(gen_0':1':s:c7_9(x))
gen_c6:c7:c88_9(0) <=> hole_c6:c7:c85_9
gen_c6:c7:c88_9(+(x, 1)) <=> c6(gen_c6:c7:c88_9(x))


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

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

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
F(gen_0':1':s:c7_9(n10_9)) -> gen_c1:c2:c36_9(n10_9), rt in Omega(1 + n10_9)

Induction Base:
F(gen_0':1':s:c7_9(0)) ->_R^Omega(1)
c1

Induction Step:
F(gen_0':1':s:c7_9(+(n10_9, 1))) ->_R^Omega(1)
c3(F(gen_0':1':s:c7_9(n10_9))) ->_IH
c3(gen_c1:c2:c36_9(c11_9))

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

(26)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
F(0') -> c1
F(1') -> c2
F(s(z0)) -> c3(F(z0))
IF(true, s(z0), s(z1)) -> c4
IF(false, s(z0), s(z1)) -> c5
G(z0, c(z1)) -> c6(G(z0, z1))
G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
f(0') -> true
f(1') -> false
f(s(z0)) -> f(z0)
if(true, s(z0), s(z1)) -> s(z0)
if(false, s(z0), s(z1)) -> s(z1)
g(z0, c(z1)) -> c(g(z0, z1))
g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))

Types:
F :: 0':1':s:c -> c1:c2:c3
0' :: 0':1':s:c
c1 :: c1:c2:c3
1' :: 0':1':s:c
c2 :: c1:c2:c3
s :: 0':1':s:c -> 0':1':s:c
c3 :: c1:c2:c3 -> c1:c2:c3
IF :: true:false -> 0':1':s:c -> 0':1':s:c -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
G :: 0':1':s:c -> 0':1':s:c -> c6:c7:c8
c :: 0':1':s:c -> 0':1':s:c
c6 :: c6:c7:c8 -> c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c1:c2:c3 -> c6:c7:c8
if :: true:false -> 0':1':s:c -> 0':1':s:c -> 0':1':s:c
f :: 0':1':s:c -> true:false
g :: 0':1':s:c -> 0':1':s:c -> 0':1':s:c
c8 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8 -> c6:c7:c8
hole_c1:c2:c31_9 :: c1:c2:c3
hole_0':1':s:c2_9 :: 0':1':s:c
hole_c4:c53_9 :: c4:c5
hole_true:false4_9 :: true:false
hole_c6:c7:c85_9 :: c6:c7:c8
gen_c1:c2:c36_9 :: Nat -> c1:c2:c3
gen_0':1':s:c7_9 :: Nat -> 0':1':s:c
gen_c6:c7:c88_9 :: Nat -> c6:c7:c8


Generator Equations:
gen_c1:c2:c36_9(0) <=> c1
gen_c1:c2:c36_9(+(x, 1)) <=> c3(gen_c1:c2:c36_9(x))
gen_0':1':s:c7_9(0) <=> 0'
gen_0':1':s:c7_9(+(x, 1)) <=> s(gen_0':1':s:c7_9(x))
gen_c6:c7:c88_9(0) <=> hole_c6:c7:c85_9
gen_c6:c7:c88_9(+(x, 1)) <=> c6(gen_c6:c7:c88_9(x))


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

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

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

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

(29)
BOUNDS(n^1, INF)

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

(30)
Obligation:
Innermost TRS:
Rules:
F(0') -> c1
F(1') -> c2
F(s(z0)) -> c3(F(z0))
IF(true, s(z0), s(z1)) -> c4
IF(false, s(z0), s(z1)) -> c5
G(z0, c(z1)) -> c6(G(z0, z1))
G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
f(0') -> true
f(1') -> false
f(s(z0)) -> f(z0)
if(true, s(z0), s(z1)) -> s(z0)
if(false, s(z0), s(z1)) -> s(z1)
g(z0, c(z1)) -> c(g(z0, z1))
g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))

Types:
F :: 0':1':s:c -> c1:c2:c3
0' :: 0':1':s:c
c1 :: c1:c2:c3
1' :: 0':1':s:c
c2 :: c1:c2:c3
s :: 0':1':s:c -> 0':1':s:c
c3 :: c1:c2:c3 -> c1:c2:c3
IF :: true:false -> 0':1':s:c -> 0':1':s:c -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
G :: 0':1':s:c -> 0':1':s:c -> c6:c7:c8
c :: 0':1':s:c -> 0':1':s:c
c6 :: c6:c7:c8 -> c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c1:c2:c3 -> c6:c7:c8
if :: true:false -> 0':1':s:c -> 0':1':s:c -> 0':1':s:c
f :: 0':1':s:c -> true:false
g :: 0':1':s:c -> 0':1':s:c -> 0':1':s:c
c8 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8 -> c6:c7:c8
hole_c1:c2:c31_9 :: c1:c2:c3
hole_0':1':s:c2_9 :: 0':1':s:c
hole_c4:c53_9 :: c4:c5
hole_true:false4_9 :: true:false
hole_c6:c7:c85_9 :: c6:c7:c8
gen_c1:c2:c36_9 :: Nat -> c1:c2:c3
gen_0':1':s:c7_9 :: Nat -> 0':1':s:c
gen_c6:c7:c88_9 :: Nat -> c6:c7:c8


Lemmas:
F(gen_0':1':s:c7_9(n10_9)) -> gen_c1:c2:c36_9(n10_9), rt in Omega(1 + n10_9)


Generator Equations:
gen_c1:c2:c36_9(0) <=> c1
gen_c1:c2:c36_9(+(x, 1)) <=> c3(gen_c1:c2:c36_9(x))
gen_0':1':s:c7_9(0) <=> 0'
gen_0':1':s:c7_9(+(x, 1)) <=> s(gen_0':1':s:c7_9(x))
gen_c6:c7:c88_9(0) <=> hole_c6:c7:c85_9
gen_c6:c7:c88_9(+(x, 1)) <=> c6(gen_c6:c7:c88_9(x))


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

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

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
f(gen_0':1':s:c7_9(n286_9)) -> true, rt in Omega(0)

Induction Base:
f(gen_0':1':s:c7_9(0)) ->_R^Omega(0)
true

Induction Step:
f(gen_0':1':s:c7_9(+(n286_9, 1))) ->_R^Omega(0)
f(gen_0':1':s:c7_9(n286_9)) ->_IH
true

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

(32)
Obligation:
Innermost TRS:
Rules:
F(0') -> c1
F(1') -> c2
F(s(z0)) -> c3(F(z0))
IF(true, s(z0), s(z1)) -> c4
IF(false, s(z0), s(z1)) -> c5
G(z0, c(z1)) -> c6(G(z0, z1))
G(z0, c(z1)) -> c7(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), F(z0))
G(z0, c(z1)) -> c8(G(z0, if(f(z0), c(g(s(z0), z1)), c(z1))), IF(f(z0), c(g(s(z0), z1)), c(z1)), G(s(z0), z1))
f(0') -> true
f(1') -> false
f(s(z0)) -> f(z0)
if(true, s(z0), s(z1)) -> s(z0)
if(false, s(z0), s(z1)) -> s(z1)
g(z0, c(z1)) -> c(g(z0, z1))
g(z0, c(z1)) -> g(z0, if(f(z0), c(g(s(z0), z1)), c(z1)))

Types:
F :: 0':1':s:c -> c1:c2:c3
0' :: 0':1':s:c
c1 :: c1:c2:c3
1' :: 0':1':s:c
c2 :: c1:c2:c3
s :: 0':1':s:c -> 0':1':s:c
c3 :: c1:c2:c3 -> c1:c2:c3
IF :: true:false -> 0':1':s:c -> 0':1':s:c -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
G :: 0':1':s:c -> 0':1':s:c -> c6:c7:c8
c :: 0':1':s:c -> 0':1':s:c
c6 :: c6:c7:c8 -> c6:c7:c8
c7 :: c6:c7:c8 -> c4:c5 -> c1:c2:c3 -> c6:c7:c8
if :: true:false -> 0':1':s:c -> 0':1':s:c -> 0':1':s:c
f :: 0':1':s:c -> true:false
g :: 0':1':s:c -> 0':1':s:c -> 0':1':s:c
c8 :: c6:c7:c8 -> c4:c5 -> c6:c7:c8 -> c6:c7:c8
hole_c1:c2:c31_9 :: c1:c2:c3
hole_0':1':s:c2_9 :: 0':1':s:c
hole_c4:c53_9 :: c4:c5
hole_true:false4_9 :: true:false
hole_c6:c7:c85_9 :: c6:c7:c8
gen_c1:c2:c36_9 :: Nat -> c1:c2:c3
gen_0':1':s:c7_9 :: Nat -> 0':1':s:c
gen_c6:c7:c88_9 :: Nat -> c6:c7:c8


Lemmas:
F(gen_0':1':s:c7_9(n10_9)) -> gen_c1:c2:c36_9(n10_9), rt in Omega(1 + n10_9)
f(gen_0':1':s:c7_9(n286_9)) -> true, rt in Omega(0)


Generator Equations:
gen_c1:c2:c36_9(0) <=> c1
gen_c1:c2:c36_9(+(x, 1)) <=> c3(gen_c1:c2:c36_9(x))
gen_0':1':s:c7_9(0) <=> 0'
gen_0':1':s:c7_9(+(x, 1)) <=> s(gen_0':1':s:c7_9(x))
gen_c6:c7:c88_9(0) <=> hole_c6:c7:c85_9
gen_c6:c7:c88_9(+(x, 1)) <=> c6(gen_c6:c7:c88_9(x))


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

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