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), 286 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 28 ms]
    (12) CdtProblem
    (13) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) BOUNDS(1, 1)
(15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(16) TRS for Loop Detection
    (17) DecreasingLoopProof [LOWER BOUND(ID), 38 ms]
    (18) BEST
        (19) proven lower bound
            (20) LowerBoundPropagationProof [FINISHED, 0 ms]
            (21) BOUNDS(n^1, INF)
        (22) TRS for Loop Detection


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

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

   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))

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

   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))

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:

   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))

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

   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))
Tuples:
   PERFECTP'(0) -> c7
   PERFECTP'(s(z0)) -> c8(F'(z0, s(0), s(z0), s(z0)))
   F'(0, z0, 0, z1) -> c9
   F'(0, z0, s(z1), z2) -> c10
   F'(s(z0), 0, z1, z2) -> c11(F'(z0, z2, minus(z1, s(z0)), z2))
   F'(s(z0), s(z1), z2, z3) -> c12(F'(s(z0), minus(z1, z0), z2, z3), F'(z0, z3, z2, z3))
   PERFECTP''(0) -> c13
   PERFECTP''(s(z0)) -> c14(F''(z0, s(0), s(z0), s(z0)))
   F''(0, z0, 0, z1) -> c15
   F''(0, z0, s(z1), z2) -> c16
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c18(F''(s(z0), minus(z1, z0), z2, z3))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
S tuples:
   PERFECTP''(0) -> c13
   PERFECTP''(s(z0)) -> c14(F''(z0, s(0), s(z0), s(z0)))
   F''(0, z0, 0, z1) -> c15
   F''(0, z0, s(z1), z2) -> c16
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c18(F''(s(z0), minus(z1, z0), z2, z3))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
K tuples:none
Defined Rule Symbols:   PERFECTP_1, F_4, perfectp_1, f_4

Defined Pair Symbols:   PERFECTP'_1, F'_4, PERFECTP''_1, F''_4

Compound Symbols:   c7, c8_1, c9, c10, c11_1, c12_2, c13, c14_1, c15, c16, c17_1, c18_1, c19_1


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

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 2 leading nodes:
   PERFECTP'(s(z0)) -> c8(F'(z0, s(0), s(z0), s(z0)))
   PERFECTP''(s(z0)) -> c14(F''(z0, s(0), s(z0), s(z0)))
Removed 7 trailing nodes:
   PERFECTP'(0) -> c7
   PERFECTP''(0) -> c13
   F''(0, z0, s(z1), z2) -> c16
   F''(0, z0, 0, z1) -> c15
   F'(0, z0, s(z1), z2) -> c10
   F''(s(z0), s(z1), z2, z3) -> c18(F''(s(z0), minus(z1, z0), z2, z3))
   F'(0, z0, 0, z1) -> c9

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))
Tuples:
   F'(s(z0), 0, z1, z2) -> c11(F'(z0, z2, minus(z1, s(z0)), z2))
   F'(s(z0), s(z1), z2, z3) -> c12(F'(s(z0), minus(z1, z0), z2, z3), F'(z0, z3, z2, z3))
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
S tuples:
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
K tuples:none
Defined Rule Symbols:   PERFECTP_1, F_4, perfectp_1, f_4

Defined Pair Symbols:   F'_4, F''_4

Compound Symbols:   c11_1, c12_2, c17_1, c19_1


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

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))
Tuples:
   F'(s(z0), 0, z1, z2) -> c11(F'(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
   F'(s(z0), s(z1), z2, z3) -> c12(F'(z0, z3, z2, z3))
S tuples:
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
K tuples:none
Defined Rule Symbols:   PERFECTP_1, F_4, perfectp_1, f_4

Defined Pair Symbols:   F'_4, F''_4

Compound Symbols:   c11_1, c17_1, c19_1, c12_1


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

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))
   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F'(s(z0), 0, z1, z2) -> c11(F'(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
   F'(s(z0), s(z1), z2, z3) -> c12(F'(z0, z3, z2, z3))
S tuples:
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   F'_4, F''_4

Compound Symbols:   c11_1, c17_1, c19_1, c12_1


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

(11) 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), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
We considered the (Usable) Rules:none
And the Tuples:
   F'(s(z0), 0, z1, z2) -> c11(F'(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
   F'(s(z0), s(z1), z2, z3) -> c12(F'(z0, z3, z2, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(F'(x_1, x_2, x_3, x_4)) = x_1
   POL(F''(x_1, x_2, x_3, x_4)) = [2]x_1
   POL(c11(x_1)) = x_1
   POL(c12(x_1)) = x_1
   POL(c17(x_1)) = x_1
   POL(c19(x_1)) = x_1
   POL(minus(x_1, x_2)) = x_1
   POL(s(x_1)) = [2] + x_1

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   F'(s(z0), 0, z1, z2) -> c11(F'(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
   F'(s(z0), s(z1), z2, z3) -> c12(F'(z0, z3, z2, z3))
S tuples:none
K tuples:
   F''(s(z0), 0, z1, z2) -> c17(F''(z0, z2, minus(z1, s(z0)), z2))
   F''(s(z0), s(z1), z2, z3) -> c19(F''(z0, z3, z2, z3))
Defined Rule Symbols:none

Defined Pair Symbols:   F'_4, F''_4

Compound Symbols:   c11_1, c17_1, c19_1, c12_1


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

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

(14)
BOUNDS(1, 1)

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

(15) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(16)
Obligation:
Analyzing the following TRS for decreasing loops:

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:

   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))

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

   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))

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

(17) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

F(s(s(z01_1)), s(z1), z2, s(z12_1)) ->^+ c6(c6(F(z01_1, s(z12_1), z2, s(z12_1))))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0].

The pumping substitution is [z01_1 / s(s(z01_1))].

The result substitution is [z1 / z12_1].




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

(18)
Complex Obligation (BEST)

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

(19)
Obligation:
Proved the lower bound n^1 for the following 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:

   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))

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

   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))

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

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

(21)
BOUNDS(n^1, INF)

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

(22)
Obligation:
Analyzing the following TRS for decreasing loops:

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:

   PERFECTP(0) -> c
   PERFECTP(s(z0)) -> c1(F(z0, s(0), s(z0), s(z0)))
   F(0, z0, 0, z1) -> c2
   F(0, z0, s(z1), z2) -> c3
   F(s(z0), 0, z1, z2) -> c4(F(z0, z2, minus(z1, s(z0)), z2))
   F(s(z0), s(z1), z2, z3) -> c5(F(s(z0), minus(z1, z0), z2, z3))
   F(s(z0), s(z1), z2, z3) -> c6(F(z0, z3, z2, z3))

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

   perfectp(0) -> false
   perfectp(s(z0)) -> f(z0, s(0), s(z0), s(z0))
   f(0, z0, 0, z1) -> true
   f(0, z0, s(z1), z2) -> false
   f(s(z0), 0, z1, z2) -> f(z0, z2, minus(z1, s(z0)), z2)
   f(s(z0), s(z1), z2, z3) -> if(le(z0, z1), f(s(z0), minus(z1, z0), z2, z3), f(z0, z3, z2, z3))

Rewrite Strategy: INNERMOST