WORST_CASE(?,O(n^1))
proof of input_R5yPD43Ef8.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CdtProblem
(9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 83 ms]
(10) CdtProblem
(11) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CdtProblem
(13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CdtProblem
(15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 8 ms]
(16) CdtProblem
(17) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
(18) BOUNDS(1, 1)


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

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


The TRS R consists of the following rules:

   p(0) -> 0
   p(s(x)) -> x
   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   minus(x, 0) -> x
   minus(x, s(y)) -> if(le(x, s(y)), 0, p(minus(x, p(s(y)))))
   if(true, x, y) -> x
   if(false, x, y) -> y

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

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   p(0) -> 0
   p(s(z0)) -> z0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(z0, 0) -> z0
   minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1)))))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
Tuples:
   P(0) -> c
   P(s(z0)) -> c1
   LE(0, z0) -> c2
   LE(s(z0), 0) -> c3
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, 0) -> c5
   MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1)))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9
S tuples:
   P(0) -> c
   P(s(z0)) -> c1
   LE(0, z0) -> c2
   LE(s(z0), 0) -> c3
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, 0) -> c5
   MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1)))
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9
K tuples:none
Defined Rule Symbols:   p_1, le_2, minus_2, if_3

Defined Pair Symbols:   P_1, LE_2, MINUS_2, IF_3

Compound Symbols:   c, c1, c2, c3, c4_1, c5, c6_2, c7_4, c8, c9


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 7 trailing nodes:
   IF(true, z0, z1) -> c8
   IF(false, z0, z1) -> c9
   P(0) -> c
   MINUS(z0, 0) -> c5
   LE(s(z0), 0) -> c3
   P(s(z0)) -> c1
   LE(0, z0) -> c2

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   p(0) -> 0
   p(s(z0)) -> z0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(z0, 0) -> z0
   minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1)))))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1)))
S tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(IF(le(z0, s(z1)), 0, p(minus(z0, p(s(z1))))), P(minus(z0, p(s(z1)))), MINUS(z0, p(s(z1))), P(s(z1)))
K tuples:none
Defined Rule Symbols:   p_1, le_2, minus_2, if_3

Defined Pair Symbols:   LE_2, MINUS_2

Compound Symbols:   c4_1, c6_2, c7_4


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

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 4 trailing tuple parts
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   p(0) -> 0
   p(s(z0)) -> z0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(z0, 0) -> z0
   minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1)))))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(MINUS(z0, p(s(z1))))
S tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(MINUS(z0, p(s(z1))))
K tuples:none
Defined Rule Symbols:   p_1, le_2, minus_2, if_3

Defined Pair Symbols:   LE_2, MINUS_2

Compound Symbols:   c4_1, c6_1, c7_1


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   p(0) -> 0
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(z0, 0) -> z0
   minus(z0, s(z1)) -> if(le(z0, s(z1)), 0, p(minus(z0, p(s(z1)))))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   p(s(z0)) -> z0
Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(MINUS(z0, p(s(z1))))
S tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(MINUS(z0, p(s(z1))))
K tuples:none
Defined Rule Symbols:   p_1

Defined Pair Symbols:   LE_2, MINUS_2

Compound Symbols:   c4_1, c6_1, c7_1


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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
We considered the (Usable) Rules:
   p(s(z0)) -> z0
And the Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(MINUS(z0, p(s(z1))))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(LE(x_1, x_2)) = x_2
   POL(MINUS(x_1, x_2)) = [1] + x_2
   POL(c4(x_1)) = x_1
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(p(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   p(s(z0)) -> z0
Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(z0, s(z1)) -> c7(MINUS(z0, p(s(z1))))
S tuples:
   MINUS(z0, s(z1)) -> c7(MINUS(z0, p(s(z1))))
K tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
Defined Rule Symbols:   p_1

Defined Pair Symbols:   LE_2, MINUS_2

Compound Symbols:   c4_1, c6_1, c7_1


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

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace MINUS(z0, s(z1)) -> c7(MINUS(z0, p(s(z1)))) by 
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   p(s(z0)) -> z0
Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))
S tuples:
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))
K tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
Defined Rule Symbols:   p_1

Defined Pair Symbols:   LE_2, MINUS_2

Compound Symbols:   c4_1, c6_1, c7_1


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

(13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   p(s(z0)) -> z0

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))
S tuples:
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))
K tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
Defined Rule Symbols:none

Defined Pair Symbols:   LE_2, MINUS_2

Compound Symbols:   c4_1, c6_1, c7_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.
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))
We considered the (Usable) Rules:none
And the Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(LE(x_1, x_2)) = [1] + x_1 + x_2
   POL(MINUS(x_1, x_2)) = [1] + x_1 + x_2
   POL(c4(x_1)) = x_1
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))
S tuples:none
K tuples:
   LE(s(z0), s(z1)) -> c4(LE(z0, z1))
   MINUS(z0, s(z1)) -> c6(LE(z0, s(z1)))
   MINUS(x0, s(z0)) -> c7(MINUS(x0, z0))
Defined Rule Symbols:none

Defined Pair Symbols:   LE_2, MINUS_2

Compound Symbols:   c4_1, c6_1, c7_1


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

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

(18)
BOUNDS(1, 1)