WORST_CASE(?,O(1))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, 1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 300 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
(5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) BOUNDS(1, 1)


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

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


The TRS R consists of the following rules:

   F(z0, z1, z2) -> c(G(<=(z0, z1), z0, z1, z2))
   G(true, z0, z1, z2) -> c1
   G(false, z0, z1, z2) -> c2(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z0), z1, z2), P(z0))
   G(false, z0, z1, z2) -> c3(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z1), z2, z0), P(z1))
   G(false, z0, z1, z2) -> c4(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z2), z0, z1), P(z2))
   P(0) -> c5
   P(s(z0)) -> c6

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

   f(z0, z1, z2) -> g(<=(z0, z1), z0, z1, z2)
   g(true, z0, z1, z2) -> z2
   g(false, z0, z1, z2) -> f(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))
   p(0) -> 0
   p(s(z0)) -> z0

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


The TRS R consists of the following rules:

   F(z0, z1, z2) -> c(G(<=(z0, z1), z0, z1, z2))
   G(true, z0, z1, z2) -> c1
   G(false, z0, z1, z2) -> c2(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z0), z1, z2), P(z0))
   G(false, z0, z1, z2) -> c3(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z1), z2, z0), P(z1))
   G(false, z0, z1, z2) -> c4(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z2), z0, z1), P(z2))
   P(0) -> c5
   P(s(z0)) -> c6

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

   f(z0, z1, z2) -> g(<=(z0, z1), z0, z1, z2)
   g(true, z0, z1, z2) -> z2
   g(false, z0, z1, z2) -> f(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))
   p(0) -> 0
   p(s(z0)) -> z0

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(z0, z1, z2) -> g(<=(z0, z1), z0, z1, z2)
   g(true, z0, z1, z2) -> z2
   g(false, z0, z1, z2) -> f(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))
   p(0) -> 0
   p(s(z0)) -> z0
   F(z0, z1, z2) -> c(G(<=(z0, z1), z0, z1, z2))
   G(true, z0, z1, z2) -> c1
   G(false, z0, z1, z2) -> c2(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z0), z1, z2), P(z0))
   G(false, z0, z1, z2) -> c3(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z1), z2, z0), P(z1))
   G(false, z0, z1, z2) -> c4(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z2), z0, z1), P(z2))
   P(0) -> c5
   P(s(z0)) -> c6
Tuples:
   F'(z0, z1, z2) -> c7(G'(<=(z0, z1), z0, z1, z2))
   G'(true, z0, z1, z2) -> c8
   G'(false, z0, z1, z2) -> c9(F'(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2))
   P'(0) -> c10
   P'(s(z0)) -> c11
   F''(z0, z1, z2) -> c12(G''(<=(z0, z1), z0, z1, z2))
   G''(true, z0, z1, z2) -> c13
   G''(false, z0, z1, z2) -> c14(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z0), z1, z2), P'(z0), P''(z0))
   G''(false, z0, z1, z2) -> c15(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z1), z2, z0), P'(z1), P''(z1))
   G''(false, z0, z1, z2) -> c16(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z2), z0, z1), P'(z2), P''(z2))
   P''(0) -> c17
   P''(s(z0)) -> c18
S tuples:
   F''(z0, z1, z2) -> c12(G''(<=(z0, z1), z0, z1, z2))
   G''(true, z0, z1, z2) -> c13
   G''(false, z0, z1, z2) -> c14(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z0), z1, z2), P'(z0), P''(z0))
   G''(false, z0, z1, z2) -> c15(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z1), z2, z0), P'(z1), P''(z1))
   G''(false, z0, z1, z2) -> c16(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z2), z0, z1), P'(z2), P''(z2))
   P''(0) -> c17
   P''(s(z0)) -> c18
K tuples:none
Defined Rule Symbols:   F_3, G_4, P_1, f_3, g_4, p_1

Defined Pair Symbols:   F'_3, G'_4, P'_1, F''_3, G''_4, P''_1

Compound Symbols:   c7_1, c8, c9_7, c10, c11, c12_1, c13, c14_10, c15_10, c16_10, c17, c18


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 12 trailing nodes:
   G''(false, z0, z1, z2) -> c15(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z1), z2, z0), P'(z1), P''(z1))
   P''(0) -> c17
   F''(z0, z1, z2) -> c12(G''(<=(z0, z1), z0, z1, z2))
   F'(z0, z1, z2) -> c7(G'(<=(z0, z1), z0, z1, z2))
   G'(true, z0, z1, z2) -> c8
   P'(s(z0)) -> c11
   G''(false, z0, z1, z2) -> c14(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z0), z1, z2), P'(z0), P''(z0))
   G''(true, z0, z1, z2) -> c13
   G'(false, z0, z1, z2) -> c9(F'(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2))
   G''(false, z0, z1, z2) -> c16(F''(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F'(p(z0), z1, z2), P'(z0), F'(p(z1), z2, z0), P'(z1), F'(p(z2), z0, z1), P'(z2), F''(p(z2), z0, z1), P'(z2), P''(z2))
   P''(s(z0)) -> c18
   P'(0) -> c10

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(z0, z1, z2) -> g(<=(z0, z1), z0, z1, z2)
   g(true, z0, z1, z2) -> z2
   g(false, z0, z1, z2) -> f(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))
   p(0) -> 0
   p(s(z0)) -> z0
   F(z0, z1, z2) -> c(G(<=(z0, z1), z0, z1, z2))
   G(true, z0, z1, z2) -> c1
   G(false, z0, z1, z2) -> c2(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z0), z1, z2), P(z0))
   G(false, z0, z1, z2) -> c3(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z1), z2, z0), P(z1))
   G(false, z0, z1, z2) -> c4(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z2), z0, z1), P(z2))
   P(0) -> c5
   P(s(z0)) -> c6
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:   F_3, G_4, P_1, f_3, g_4, p_1

Defined Pair Symbols:none

Compound Symbols:none


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

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

(8)
BOUNDS(1, 1)