WORST_CASE(Omega(n^1),O(n^3))
proof of input_Zzb0nT4TFx.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, n^3).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxWeightedTrs
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxTypedWeightedTrs
    (13) CompletionProof [UPPER BOUND(ID), 0 ms]
    (14) CpxTypedWeightedCompleteTrs
    (15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (16) CpxRNTS
    (17) CompleteCoflocoProof [FINISHED, 900 ms]
    (18) BOUNDS(1, n^3)
(19) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CdtProblem
    (21) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) CpxRelTRS
    (23) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) typed CpxTrs
    (27) OrderProof [LOWER BOUND(ID), 10 ms]
    (28) typed CpxTrs
    (29) RewriteLemmaProof [LOWER BOUND(ID), 411 ms]
    (30) BEST
        (31) proven lower bound
            (32) LowerBoundPropagationProof [FINISHED, 0 ms]
            (33) BOUNDS(n^1, INF)
        (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 77 ms]
            (36) typed CpxTrs


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

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


The TRS R consists of the following rules:

   le(0, Y) -> true
   le(s(X), 0) -> false
   le(s(X), s(Y)) -> le(X, Y)
   minus(0, Y) -> 0
   minus(s(X), Y) -> ifMinus(le(s(X), Y), s(X), Y)
   ifMinus(true, s(X), Y) -> 0
   ifMinus(false, s(X), Y) -> s(minus(X, Y))
   quot(0, s(Y)) -> 0
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(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:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(0, z0) -> 0
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
   ifMinus(true, s(z0), z1) -> 0
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
Tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(0, z0) -> c3
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(true, s(z0), z1) -> c5
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c7
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
S tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(0, z0) -> c3
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(true, s(z0), z1) -> c5
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c7
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
K tuples:none
Defined Rule Symbols:   le_2, minus_2, ifMinus_3, quot_2

Defined Pair Symbols:   LE_2, MINUS_2, IFMINUS_3, QUOT_2

Compound Symbols:   c, c1, c2_1, c3, c4_2, c5, c6_1, c7, c8_2


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 5 trailing nodes:
   MINUS(0, z0) -> c3
   LE(0, z0) -> c
   QUOT(0, s(z0)) -> c7
   LE(s(z0), 0) -> c1
   IFMINUS(true, s(z0), z1) -> c5

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(0, z0) -> 0
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
   ifMinus(true, s(z0), z1) -> 0
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
Tuples:
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
S tuples:
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
K tuples:none
Defined Rule Symbols:   le_2, minus_2, ifMinus_3, quot_2

Defined Pair Symbols:   LE_2, MINUS_2, IFMINUS_3, QUOT_2

Compound Symbols:   c2_1, c4_2, c6_1, c8_2


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   le(0, z0) -> true
   minus(0, z0) -> 0
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
   ifMinus(true, s(z0), z1) -> 0
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
Tuples:
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
S tuples:
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
K tuples:none
Defined Rule Symbols:   le_2, minus_2, ifMinus_3

Defined Pair Symbols:   LE_2, MINUS_2, IFMINUS_3, QUOT_2

Compound Symbols:   c2_1, c4_2, c6_1, c8_2


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

(7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))

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

   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   le(0, z0) -> true
   minus(0, z0) -> 0
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
   ifMinus(true, s(z0), z1) -> 0
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1))

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

(9) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   LE(s(z0), s(z1)) -> c2(LE(z0, z1)) [1]
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1)) [1]
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1)) [1]
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   le(0, z0) -> true [0]
   minus(0, z0) -> 0 [0]
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1) [0]
   ifMinus(true, s(z0), z1) -> 0 [0]
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1)) [0]

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

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

(12)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   LE(s(z0), s(z1)) -> c2(LE(z0, z1)) [1]
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1)) [1]
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1)) [1]
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   le(0, z0) -> true [0]
   minus(0, z0) -> 0 [0]
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1) [0]
   ifMinus(true, s(z0), z1) -> 0 [0]
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1)) [0]

The TRS has the following type information:
LE :: s:0 -> s:0 -> c2
s :: s:0 -> s:0
c2 :: c2 -> c2
MINUS :: s:0 -> s:0 -> c4
c4 :: c6 -> c2 -> c4
IFMINUS :: false:true -> s:0 -> s:0 -> c6
le :: s:0 -> s:0 -> false:true
false :: false:true
c6 :: c4 -> c6
QUOT :: s:0 -> s:0 -> c8
c8 :: c8 -> c4 -> c8
minus :: s:0 -> s:0 -> s:0
0 :: s:0
true :: false:true
ifMinus :: false:true -> s:0 -> s:0 -> s:0

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

(13) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   le(v0, v1) -> null_le [0]
   minus(v0, v1) -> null_minus [0]
   ifMinus(v0, v1, v2) -> null_ifMinus [0]
   LE(v0, v1) -> null_LE [0]
   MINUS(v0, v1) -> null_MINUS [0]
   IFMINUS(v0, v1, v2) -> null_IFMINUS [0]
   QUOT(v0, v1) -> null_QUOT [0]

And the following fresh constants:    null_le, null_minus, null_ifMinus, null_LE, null_MINUS, null_IFMINUS, null_QUOT

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

(14)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   LE(s(z0), s(z1)) -> c2(LE(z0, z1)) [1]
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1)) [1]
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1)) [1]
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   le(s(z0), 0) -> false [0]
   le(s(z0), s(z1)) -> le(z0, z1) [0]
   le(0, z0) -> true [0]
   minus(0, z0) -> 0 [0]
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1) [0]
   ifMinus(true, s(z0), z1) -> 0 [0]
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1)) [0]
   le(v0, v1) -> null_le [0]
   minus(v0, v1) -> null_minus [0]
   ifMinus(v0, v1, v2) -> null_ifMinus [0]
   LE(v0, v1) -> null_LE [0]
   MINUS(v0, v1) -> null_MINUS [0]
   IFMINUS(v0, v1, v2) -> null_IFMINUS [0]
   QUOT(v0, v1) -> null_QUOT [0]

The TRS has the following type information:
LE :: s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus -> c2:null_LE
s :: s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus
c2 :: c2:null_LE -> c2:null_LE
MINUS :: s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus -> c4:null_MINUS
c4 :: c6:null_IFMINUS -> c2:null_LE -> c4:null_MINUS
IFMINUS :: false:true:null_le -> s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus -> c6:null_IFMINUS
le :: s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus -> false:true:null_le
false :: false:true:null_le
c6 :: c4:null_MINUS -> c6:null_IFMINUS
QUOT :: s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus -> c8:null_QUOT
c8 :: c8:null_QUOT -> c4:null_MINUS -> c8:null_QUOT
minus :: s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus
0 :: s:0:null_minus:null_ifMinus
true :: false:true:null_le
ifMinus :: false:true:null_le -> s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus -> s:0:null_minus:null_ifMinus
null_le :: false:true:null_le
null_minus :: s:0:null_minus:null_ifMinus
null_ifMinus :: s:0:null_minus:null_ifMinus
null_LE :: c2:null_LE
null_MINUS :: c4:null_MINUS
null_IFMINUS :: c6:null_IFMINUS
null_QUOT :: c8:null_QUOT

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

(15) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   false => 1
   0 => 0
   true => 2
   null_le => 0
   null_minus => 0
   null_ifMinus => 0
   null_LE => 0
   null_MINUS => 0
   null_IFMINUS => 0
   null_QUOT => 0

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

(16)
Obligation:
Complexity RNTS consisting of the following rules:

   IFMINUS(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IFMINUS(z, z', z'') -{ 1 }-> 1 + MINUS(z0, z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = 1 + z0, z'' = z1
   LE(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LE(z, z') -{ 1 }-> 1 + LE(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   MINUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MINUS(z, z') -{ 1 }-> 1 + IFMINUS(le(1 + z0, z1), 1 + z0, z1) + LE(1 + z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   QUOT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   QUOT(z, z') -{ 1 }-> 1 + QUOT(minus(z0, z1), 1 + z1) + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   ifMinus(z, z', z'') -{ 0 }-> 0 :|: z = 2, z1 >= 0, z0 >= 0, z' = 1 + z0, z'' = z1
   ifMinus(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   ifMinus(z, z', z'') -{ 0 }-> 1 + minus(z0, z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = 1 + z0, z'' = z1
   le(z, z') -{ 0 }-> le(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   le(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   le(z, z') -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   le(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   minus(z, z') -{ 0 }-> ifMinus(le(1 + z0, z1), 1 + z0, z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

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

(17) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V1, V, V6),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[fun2(V1, V, V6, Out)],[V1 >= 0,V >= 0,V6 >= 0]).
eq(start(V1, V, V6),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[le(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[minus(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[ifMinus(V1, V, V6, Out)],[V1 >= 0,V >= 0,V6 >= 0]).
eq(fun(V1, V, Out),1,[fun(V3, V2, Ret1)],[Out = 1 + Ret1,V2 >= 0,V1 = 1 + V3,V3 >= 0,V = 1 + V2]).
eq(fun1(V1, V, Out),1,[le(1 + V5, V4, Ret010),fun2(Ret010, 1 + V5, V4, Ret01),fun(1 + V5, V4, Ret11)],[Out = 1 + Ret01 + Ret11,V4 >= 0,V1 = 1 + V5,V = V4,V5 >= 0]).
eq(fun2(V1, V, V6, Out),1,[fun1(V8, V7, Ret12)],[Out = 1 + Ret12,V7 >= 0,V1 = 1,V8 >= 0,V = 1 + V8,V6 = V7]).
eq(fun3(V1, V, Out),1,[minus(V9, V10, Ret0101),fun3(Ret0101, 1 + V10, Ret011),fun1(V9, V10, Ret13)],[Out = 1 + Ret011 + Ret13,V10 >= 0,V1 = 1 + V9,V9 >= 0,V = 1 + V10]).
eq(le(V1, V, Out),0,[],[Out = 1,V1 = 1 + V11,V11 >= 0,V = 0]).
eq(le(V1, V, Out),0,[le(V13, V12, Ret)],[Out = Ret,V12 >= 0,V1 = 1 + V13,V13 >= 0,V = 1 + V12]).
eq(le(V1, V, Out),0,[],[Out = 2,V14 >= 0,V1 = 0,V = V14]).
eq(minus(V1, V, Out),0,[],[Out = 0,V15 >= 0,V1 = 0,V = V15]).
eq(minus(V1, V, Out),0,[le(1 + V17, V16, Ret0),ifMinus(Ret0, 1 + V17, V16, Ret2)],[Out = Ret2,V16 >= 0,V1 = 1 + V17,V = V16,V17 >= 0]).
eq(ifMinus(V1, V, V6, Out),0,[],[Out = 0,V1 = 2,V19 >= 0,V18 >= 0,V = 1 + V18,V6 = V19]).
eq(ifMinus(V1, V, V6, Out),0,[minus(V21, V20, Ret14)],[Out = 1 + Ret14,V20 >= 0,V1 = 1,V21 >= 0,V = 1 + V21,V6 = V20]).
eq(le(V1, V, Out),0,[],[Out = 0,V23 >= 0,V22 >= 0,V1 = V23,V = V22]).
eq(minus(V1, V, Out),0,[],[Out = 0,V25 >= 0,V24 >= 0,V1 = V25,V = V24]).
eq(ifMinus(V1, V, V6, Out),0,[],[Out = 0,V27 >= 0,V6 = V28,V26 >= 0,V1 = V27,V = V26,V28 >= 0]).
eq(fun(V1, V, Out),0,[],[Out = 0,V29 >= 0,V30 >= 0,V1 = V29,V = V30]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V32 >= 0,V31 >= 0,V1 = V32,V = V31]).
eq(fun2(V1, V, V6, Out),0,[],[Out = 0,V34 >= 0,V6 = V35,V33 >= 0,V1 = V34,V = V33,V35 >= 0]).
eq(fun3(V1, V, Out),0,[],[Out = 0,V37 >= 0,V36 >= 0,V1 = V37,V = V36]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,V,V6,Out),[V1,V,V6],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(le(V1,V,Out),[V1,V],[Out]).
input_output_vars(minus(V1,V,Out),[V1,V],[Out]).
input_output_vars(ifMinus(V1,V,V6,Out),[V1,V,V6],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [fun/3]
1. recursive  : [le/3]
2. recursive [non_tail] : [fun1/3,fun2/4]
3. recursive  : [ifMinus/4,minus/3]
4. recursive [non_tail] : [fun3/3]
5. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/3
1. SCC is partially evaluated into le/3
2. SCC is partially evaluated into fun1/3
3. SCC is partially evaluated into minus/3
4. SCC is partially evaluated into fun3/3
5. SCC is partially evaluated into start/3

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations fun/3 
* CE 16 is refined into CE [23] 
* CE 15 is refined into CE [24] 


### Cost equations --> "Loop" of fun/3 
* CEs [24] --> Loop 15 
* CEs [23] --> Loop 16 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [15]: [V,V1]

#### Partial ranking functions of CR fun(V1,V,Out) 
* Partial RF of phase [15]:
  - RF of loop [15:1]:
    V
    V1


### Specialization of cost equations le/3 
* CE 22 is refined into CE [25] 
* CE 19 is refined into CE [26] 
* CE 21 is refined into CE [27] 
* CE 20 is refined into CE [28] 


### Cost equations --> "Loop" of le/3 
* CEs [28] --> Loop 17 
* CEs [25] --> Loop 18 
* CEs [26] --> Loop 19 
* CEs [27] --> Loop 20 

### Ranking functions of CR le(V1,V,Out) 
* RF of phase [17]: [V,V1]

#### Partial ranking functions of CR le(V1,V,Out) 
* Partial RF of phase [17]:
  - RF of loop [17:1]:
    V
    V1


### Specialization of cost equations fun1/3 
* CE 12 is refined into CE [29,30,31,32,33,34,35] 
* CE 14 is refined into CE [36] 
* CE 13 is refined into CE [37,38,39] 


### Cost equations --> "Loop" of fun1/3 
* CEs [39] --> Loop 21 
* CEs [38] --> Loop 22 
* CEs [37] --> Loop 23 
* CEs [33] --> Loop 24 
* CEs [31,35] --> Loop 25 
* CEs [36] --> Loop 26 
* CEs [29,30,32,34] --> Loop 27 

### Ranking functions of CR fun1(V1,V,Out) 
* RF of phase [21,22]: [V1-1,V1-V]
* RF of phase [23]: [V1]

#### Partial ranking functions of CR fun1(V1,V,Out) 
* Partial RF of phase [21,22]:
  - RF of loop [21:1,22:1]:
    V1-1
    V1-V
* Partial RF of phase [23]:
  - RF of loop [23:1]:
    V1


### Specialization of cost equations minus/3 
* CE 9 is refined into CE [40,41,42,43] 
* CE 11 is refined into CE [44] 
* CE 10 is refined into CE [45,46] 


### Cost equations --> "Loop" of minus/3 
* CEs [46] --> Loop 28 
* CEs [45] --> Loop 29 
* CEs [40,41,42,43,44] --> Loop 30 

### Ranking functions of CR minus(V1,V,Out) 
* RF of phase [28]: [V1-1,V1-V]
* RF of phase [29]: [V1]

#### Partial ranking functions of CR minus(V1,V,Out) 
* Partial RF of phase [28]:
  - RF of loop [28:1]:
    V1-1
    V1-V
* Partial RF of phase [29]:
  - RF of loop [29:1]:
    V1


### Specialization of cost equations fun3/3 
* CE 18 is refined into CE [47] 
* CE 17 is refined into CE [48,49,50,51,52,53,54,55,56,57,58,59] 


### Cost equations --> "Loop" of fun3/3 
* CEs [58,59] --> Loop 31 
* CEs [57] --> Loop 32 
* CEs [56] --> Loop 33 
* CEs [55] --> Loop 34 
* CEs [53] --> Loop 35 
* CEs [52] --> Loop 36 
* CEs [54] --> Loop 37 
* CEs [48] --> Loop 38 
* CEs [50] --> Loop 39 
* CEs [49] --> Loop 40 
* CEs [51] --> Loop 41 
* CEs [47] --> Loop 42 

### Ranking functions of CR fun3(V1,V,Out) 
* RF of phase [31,32,33]: [V1/2-1,V1/2-V/2]
* RF of phase [38,39,40]: [V1-1]

#### Partial ranking functions of CR fun3(V1,V,Out) 
* Partial RF of phase [31,32,33]:
  - RF of loop [31:1,32:1,33:1]:
    V1/2-1
    V1/2-V/2
* Partial RF of phase [38,39,40]:
  - RF of loop [38:1,39:1,40:1]:
    V1-1


### Specialization of cost equations start/3 
* CE 1 is refined into CE [60] 
* CE 2 is refined into CE [61,62,63] 
* CE 3 is refined into CE [64,65,66,67,68] 
* CE 4 is refined into CE [69,70] 
* CE 5 is refined into CE [71,72,73,74,75] 
* CE 6 is refined into CE [76,77,78,79,80,81] 
* CE 7 is refined into CE [82,83,84,85,86] 
* CE 8 is refined into CE [87,88,89] 


### Cost equations --> "Loop" of start/3 
* CEs [76] --> Loop 43 
* CEs [71,83,87] --> Loop 44 
* CEs [61,62,63,64,65,66,67,68] --> Loop 45 
* CEs [60,69,70,72,73,74,75,77,78,79,80,81,82,84,85,86,88,89] --> Loop 46 

### Ranking functions of CR start(V1,V,V6) 

#### Partial ranking functions of CR start(V1,V,V6) 


Computing Bounds
=====================================

#### Cost of chains of fun(V1,V,Out):
* Chain [[15],16]: 1*it(15)+0
  Such that:it(15) =< Out

  with precondition: [Out>=1,V1>=Out,V>=Out] 

* Chain [16]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of le(V1,V,Out):
* Chain [[17],20]: 0
  with precondition: [Out=2,V1>=1,V>=V1] 

* Chain [[17],19]: 0
  with precondition: [Out=1,V>=1,V1>=V+1] 

* Chain [[17],18]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [20]: 0
  with precondition: [V1=0,Out=2,V>=0] 

* Chain [19]: 0
  with precondition: [V=0,Out=1,V1>=1] 

* Chain [18]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun1(V1,V,Out):
* Chain [[23],27]: 2*it(23)+1
  Such that:it(23) =< Out/2

  with precondition: [V=0,Out>=3,2*V1>=Out+1] 

* Chain [[23],26]: 2*it(23)+0
  Such that:it(23) =< Out/2

  with precondition: [V=0,Out>=2,2*V1>=Out] 

* Chain [[21,22],27]: 4*it(21)+1*s(3)+1
  Such that:aux(2) =< V1
aux(1) =< V
aux(6) =< V1-V
it(21) =< aux(2)
it(21) =< aux(6)
s(3) =< it(21)*aux(1)

  with precondition: [V>=1,Out>=3,V1>=V+1] 

* Chain [[21,22],26]: 4*it(21)+1*s(3)+0
  Such that:aux(2) =< V1
aux(1) =< V
aux(7) =< V1-V
it(21) =< aux(2)
it(21) =< aux(7)
s(3) =< it(21)*aux(1)

  with precondition: [V>=1,Out>=2,V1>=V+1] 

* Chain [[21,22],25]: 4*it(21)+1*s(3)+1*s(4)+1*s(5)+1
  Such that:aux(3) =< V1-V
aux(8) =< V1
aux(9) =< V
s(5) =< aux(8)
s(4) =< aux(9)
it(21) =< aux(8)
it(21) =< aux(3)
s(3) =< it(21)*aux(9)

  with precondition: [V>=1,Out>=4,V1>=V+1] 

* Chain [[21,22],24]: 4*it(21)+1*s(3)+1*s(6)+1
  Such that:aux(2) =< V1
aux(10) =< V1-V
aux(11) =< V
s(6) =< aux(11)
it(21) =< aux(2)
it(21) =< aux(10)
s(3) =< it(21)*aux(11)

  with precondition: [V>=1,Out>=4,V1>=V+2] 

* Chain [27]: 1
  with precondition: [Out=1,V1>=1,V>=0] 

* Chain [26]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [25]: 1*s(4)+1*s(5)+1
  Such that:s(5) =< V1
s(4) =< V

  with precondition: [Out>=2,V1+1>=Out,V+1>=Out] 

* Chain [24]: 1*s(6)+1
  Such that:s(6) =< V

  with precondition: [Out>=2,V1>=V+1,V+1>=Out] 


#### Cost of chains of minus(V1,V,Out):
* Chain [[29],30]: 0
  with precondition: [V=0,Out>=1,V1>=Out] 

* Chain [[28],30]: 0
  with precondition: [V>=1,Out>=1,V1>=Out+V] 

* Chain [30]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun3(V1,V,Out):
* Chain [[38,39,40],42]: 5*it(38)+4*s(37)+0
  Such that:aux(19) =< V1
it(38) =< aux(19)
s(38) =< it(38)*aux(19)
s(37) =< s(38)

  with precondition: [V=1,V1>=2,Out>=1] 

* Chain [[38,39,40],41,42]: 9*it(38)+4*s(37)+2
  Such that:aux(20) =< V1
it(38) =< aux(20)
s(38) =< it(38)*aux(20)
s(37) =< s(38)

  with precondition: [V=1,V1>=3,Out>=4] 

* Chain [[38,39,40],36,42]: 5*it(38)+4*s(37)+1
  Such that:aux(21) =< V1
it(38) =< aux(21)
s(38) =< it(38)*aux(21)
s(37) =< s(38)

  with precondition: [V=1,V1>=2,Out>=2] 

* Chain [[38,39,40],35,42]: 5*it(38)+4*s(37)+2
  Such that:aux(22) =< V1
it(38) =< aux(22)
s(38) =< it(38)*aux(22)
s(37) =< s(38)

  with precondition: [V=1,V1>=3,Out>=3] 

* Chain [[31,32,33],42]: 2*it(31)+3*it(32)+4*s(57)+16*s(58)+4*s(59)+2*s(60)+0
  Such that:aux(26) =< V1-V
aux(30) =< V1/2-V/2
s(52) =< V
aux(33) =< V1
aux(34) =< V1/2
it(32) =< aux(33)
it(31) =< aux(34)
it(32) =< aux(34)
it(31) =< aux(30)
it(32) =< aux(30)
s(61) =< it(31)*aux(26)
s(62) =< it(31)*aux(33)
s(60) =< s(62)
s(57) =< aux(33)
s(58) =< s(62)
s(58) =< s(61)
s(59) =< s(58)*s(52)

  with precondition: [V>=2,Out>=1,V1>=V+1] 

* Chain [[31,32,33],37,42]: 2*it(31)+3*it(32)+4*s(57)+16*s(58)+4*s(59)+2*s(60)+3*s(67)+16*s(68)+4*s(69)+1*s(70)+2
  Such that:aux(29) =< V1/2
aux(30) =< V1/2-V/2
aux(35) =< V1
aux(36) =< V1-V
aux(37) =< V
s(67) =< aux(37)
s(68) =< aux(35)
s(68) =< aux(36)
s(69) =< s(68)*aux(37)
s(70) =< aux(35)
it(32) =< aux(35)
s(63) =< aux(35)
it(32) =< aux(36)
s(63) =< aux(36)
it(31) =< aux(29)
it(32) =< aux(29)
it(31) =< aux(30)
it(32) =< aux(30)
it(31) =< aux(36)
s(61) =< it(31)*aux(36)
s(62) =< it(31)*aux(35)
s(60) =< s(62)
s(57) =< s(63)
s(58) =< s(62)
s(58) =< s(61)
s(59) =< s(58)*aux(37)

  with precondition: [V>=2,Out>=4,V1>=2*V+1] 

* Chain [[31,32,33],36,42]: 2*it(31)+3*it(32)+4*s(57)+16*s(58)+4*s(59)+2*s(60)+1
  Such that:aux(26) =< V1-V
aux(30) =< V1/2-V/2
s(52) =< V
aux(38) =< V1
aux(39) =< V1/2
it(32) =< aux(38)
it(31) =< aux(39)
it(32) =< aux(39)
it(31) =< aux(30)
it(32) =< aux(30)
s(61) =< it(31)*aux(26)
s(62) =< it(31)*aux(38)
s(60) =< s(62)
s(57) =< aux(38)
s(58) =< s(62)
s(58) =< s(61)
s(59) =< s(58)*s(52)

  with precondition: [V>=2,Out>=2,V1>=V+1] 

* Chain [[31,32,33],35,42]: 2*it(31)+3*it(32)+4*s(57)+16*s(58)+4*s(59)+2*s(60)+2
  Such that:aux(26) =< V1-V
aux(30) =< V1/2-V/2
s(52) =< V
aux(40) =< V1
aux(41) =< V1/2
it(32) =< aux(40)
it(31) =< aux(41)
it(32) =< aux(41)
it(31) =< aux(30)
it(32) =< aux(30)
s(61) =< it(31)*aux(26)
s(62) =< it(31)*aux(40)
s(60) =< s(62)
s(57) =< aux(40)
s(58) =< s(62)
s(58) =< s(61)
s(59) =< s(58)*s(52)

  with precondition: [V>=2,Out>=3,V1>=V+2] 

* Chain [[31,32,33],34,42]: 5*it(31)+5*s(57)+16*s(58)+4*s(59)+2*s(60)+1*s(72)+2
  Such that:aux(26) =< V1-V
aux(29) =< V1/2
aux(30) =< V1/2-V/2
aux(42) =< V1
aux(43) =< V
s(57) =< aux(42)
s(72) =< aux(43)
it(31) =< aux(42)
it(31) =< aux(29)
it(31) =< aux(30)
s(61) =< it(31)*aux(26)
s(62) =< it(31)*aux(42)
s(60) =< s(62)
s(58) =< s(62)
s(58) =< s(61)
s(59) =< s(58)*aux(43)

  with precondition: [V>=2,Out>=4,V1>=V+2] 

* Chain [42]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [41,42]: 4*s(40)+2
  Such that:s(39) =< V1
s(40) =< s(39)

  with precondition: [V=1,Out>=3,2*V1>=Out+1] 

* Chain [37,42]: 3*s(67)+16*s(68)+4*s(69)+1*s(70)+2
  Such that:s(64) =< V1
s(65) =< V1-V
s(66) =< V
s(67) =< s(66)
s(68) =< s(64)
s(68) =< s(65)
s(69) =< s(68)*s(66)
s(70) =< s(64)

  with precondition: [V>=2,Out>=3,V1>=V+1] 

* Chain [36,42]: 1
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [35,42]: 2
  with precondition: [Out=2,V1>=2,V>=1] 

* Chain [34,42]: 1*s(71)+1*s(72)+2
  Such that:s(71) =< V1
s(72) =< V

  with precondition: [Out>=3,V1+1>=Out,V+1>=Out] 


#### Cost of chains of start(V1,V,V6):
* Chain [46]: 13*s(168)+48*s(173)+12*s(174)+22*s(175)+14*s(187)+2*s(190)+16*s(191)+4*s(192)+6*s(193)+6*s(196)+48*s(197)+12*s(198)+3*s(199)+2*s(201)+2*s(204)+4*s(205)+16*s(206)+4*s(207)+2
  Such that:s(180) =< V1/2
s(181) =< V1/2-V/2
aux(50) =< V1
aux(51) =< V1-V
aux(52) =< V
s(175) =< aux(50)
s(168) =< aux(52)
s(173) =< aux(50)
s(173) =< aux(51)
s(174) =< s(173)*aux(52)
s(187) =< aux(50)
s(187) =< s(180)
s(187) =< s(181)
s(188) =< s(187)*aux(51)
s(189) =< s(187)*aux(50)
s(190) =< s(189)
s(191) =< s(189)
s(191) =< s(188)
s(192) =< s(191)*aux(52)
s(193) =< s(180)
s(193) =< s(181)
s(194) =< s(193)*aux(51)
s(195) =< s(193)*aux(50)
s(196) =< s(195)
s(197) =< s(195)
s(197) =< s(194)
s(198) =< s(197)*aux(52)
s(199) =< aux(50)
s(200) =< aux(50)
s(199) =< aux(51)
s(200) =< aux(51)
s(201) =< s(180)
s(199) =< s(180)
s(201) =< s(181)
s(199) =< s(181)
s(201) =< aux(51)
s(202) =< s(201)*aux(51)
s(203) =< s(201)*aux(50)
s(204) =< s(203)
s(205) =< s(200)
s(206) =< s(203)
s(206) =< s(202)
s(207) =< s(206)*aux(52)

  with precondition: [V1>=0,V>=0] 

* Chain [45]: 6*s(211)+4*s(215)+16*s(216)+4*s(217)+2
  Such that:s(213) =< V-V6
aux(53) =< V
aux(54) =< V6
s(211) =< aux(53)
s(215) =< aux(54)
s(216) =< aux(53)
s(216) =< s(213)
s(217) =< s(216)*aux(54)

  with precondition: [V1=1,V>=1,V6>=0] 

* Chain [44]: 4*s(222)+1
  Such that:s(221) =< V1
s(222) =< s(221)

  with precondition: [V=0,V1>=1] 

* Chain [43]: 28*s(224)+16*s(226)+2
  Such that:s(223) =< V1
s(224) =< s(223)
s(225) =< s(224)*s(223)
s(226) =< s(225)

  with precondition: [V=1,V1>=2] 


Closed-form bounds of start(V1,V,V6): 
-------------------------------------
* Chain [46] with precondition: [V1>=0,V>=0] 
    - Upper bound: 91*V1+2+18*V1*V1+4*V1*V1*V+12*V1*V+V1/2*(16*V1*V)+V1/2*(72*V1)+13*V+4*V1 
    - Complexity: n^3 
* Chain [45] with precondition: [V1=1,V>=1,V6>=0] 
    - Upper bound: 22*V+2+4*V*V6+4*V6 
    - Complexity: n^2 
* Chain [44] with precondition: [V=0,V1>=1] 
    - Upper bound: 4*V1+1 
    - Complexity: n 
* Chain [43] with precondition: [V=1,V1>=2] 
    - Upper bound: 28*V1+2+16*V1*V1 
    - Complexity: n^2 

### Maximum cost of start(V1,V,V6): max([22*V+1+4*V*nat(V6)+nat(V6)*4,2*V1*V1+63*V1+4*V1*V1*V+12*V1*V+V1/2*(16*V1*V)+V1/2*(72*V1)+13*V+4*V1+(24*V1+1+16*V1*V1)+4*V1])+1 
Asymptotic class: n^3 
* Total analysis performed in 803 ms.


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

(18)
BOUNDS(1, n^3)

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

(19) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(0, z0) -> 0
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
   ifMinus(true, s(z0), z1) -> 0
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
Tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(0, z0) -> c3
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(true, s(z0), z1) -> c5
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c7
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
S tuples:
   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(0, z0) -> c3
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(true, s(z0), z1) -> c5
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c7
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
K tuples:none
Defined Rule Symbols:   le_2, minus_2, ifMinus_3, quot_2

Defined Pair Symbols:   LE_2, MINUS_2, IFMINUS_3, QUOT_2

Compound Symbols:   c, c1, c2_1, c3, c4_2, c5, c6_1, c7, c8_2


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

(21) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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

   LE(0, z0) -> c
   LE(s(z0), 0) -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(0, z0) -> c3
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(true, s(z0), z1) -> c5
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c7
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))

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

   le(0, z0) -> true
   le(s(z0), 0) -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(0, z0) -> 0
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
   ifMinus(true, s(z0), z1) -> 0
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))

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

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

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

   LE(0', z0) -> c
   LE(s(z0), 0') -> c1
   LE(s(z0), s(z1)) -> c2(LE(z0, z1))
   MINUS(0', z0) -> c3
   MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
   IFMINUS(true, s(z0), z1) -> c5
   IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
   QUOT(0', s(z0)) -> c7
   QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))

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

   le(0', z0) -> true
   le(s(z0), 0') -> false
   le(s(z0), s(z1)) -> le(z0, z1)
   minus(0', z0) -> 0'
   minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
   ifMinus(true, s(z0), z1) -> 0'
   ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
   quot(0', s(z0)) -> 0'
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))

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

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

(26)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
MINUS(0', z0) -> c3
MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
IFMINUS(true, s(z0), z1) -> c5
IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
QUOT(0', s(z0)) -> c7
QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
minus(0', z0) -> 0'
minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
ifMinus(true, s(z0), z1) -> 0'
ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s -> 0':s -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c:c1:c2 -> c3:c4
IFMINUS :: true:false -> 0':s -> 0':s -> c5:c6
le :: 0':s -> 0':s -> true:false
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
QUOT :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c3:c4 -> c7:c8
minus :: 0':s -> 0':s -> 0':s
ifMinus :: true:false -> 0':s -> 0':s -> 0':s
quot :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_9 :: c:c1:c2
hole_0':s2_9 :: 0':s
hole_c3:c43_9 :: c3:c4
hole_c5:c64_9 :: c5:c6
hole_true:false5_9 :: true:false
hole_c7:c86_9 :: c7:c8
gen_c:c1:c27_9 :: Nat -> c:c1:c2
gen_0':s8_9 :: Nat -> 0':s
gen_c7:c89_9 :: Nat -> c7:c8

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

(27) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LE, MINUS, le, QUOT, minus, quot

They will be analysed ascendingly in the following order:
LE < MINUS
le < MINUS
MINUS < QUOT
le < minus
minus < QUOT
minus < quot

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

(28)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
MINUS(0', z0) -> c3
MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
IFMINUS(true, s(z0), z1) -> c5
IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
QUOT(0', s(z0)) -> c7
QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
minus(0', z0) -> 0'
minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
ifMinus(true, s(z0), z1) -> 0'
ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s -> 0':s -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c:c1:c2 -> c3:c4
IFMINUS :: true:false -> 0':s -> 0':s -> c5:c6
le :: 0':s -> 0':s -> true:false
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
QUOT :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c3:c4 -> c7:c8
minus :: 0':s -> 0':s -> 0':s
ifMinus :: true:false -> 0':s -> 0':s -> 0':s
quot :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_9 :: c:c1:c2
hole_0':s2_9 :: 0':s
hole_c3:c43_9 :: c3:c4
hole_c5:c64_9 :: c5:c6
hole_true:false5_9 :: true:false
hole_c7:c86_9 :: c7:c8
gen_c:c1:c27_9 :: Nat -> c:c1:c2
gen_0':s8_9 :: Nat -> 0':s
gen_c7:c89_9 :: Nat -> c7:c8


Generator Equations:
gen_c:c1:c27_9(0) <=> c
gen_c:c1:c27_9(+(x, 1)) <=> c2(gen_c:c1:c27_9(x))
gen_0':s8_9(0) <=> 0'
gen_0':s8_9(+(x, 1)) <=> s(gen_0':s8_9(x))
gen_c7:c89_9(0) <=> c7
gen_c7:c89_9(+(x, 1)) <=> c8(gen_c7:c89_9(x), c3)


The following defined symbols remain to be analysed:
LE, MINUS, le, QUOT, minus, quot

They will be analysed ascendingly in the following order:
LE < MINUS
le < MINUS
MINUS < QUOT
le < minus
minus < QUOT
minus < quot

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LE(gen_0':s8_9(n11_9), gen_0':s8_9(n11_9)) -> gen_c:c1:c27_9(n11_9), rt in Omega(1 + n11_9)

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

Induction Step:
LE(gen_0':s8_9(+(n11_9, 1)), gen_0':s8_9(+(n11_9, 1))) ->_R^Omega(1)
c2(LE(gen_0':s8_9(n11_9), gen_0':s8_9(n11_9))) ->_IH
c2(gen_c:c1:c27_9(c12_9))

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

(30)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
MINUS(0', z0) -> c3
MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
IFMINUS(true, s(z0), z1) -> c5
IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
QUOT(0', s(z0)) -> c7
QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
minus(0', z0) -> 0'
minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
ifMinus(true, s(z0), z1) -> 0'
ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s -> 0':s -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c:c1:c2 -> c3:c4
IFMINUS :: true:false -> 0':s -> 0':s -> c5:c6
le :: 0':s -> 0':s -> true:false
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
QUOT :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c3:c4 -> c7:c8
minus :: 0':s -> 0':s -> 0':s
ifMinus :: true:false -> 0':s -> 0':s -> 0':s
quot :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_9 :: c:c1:c2
hole_0':s2_9 :: 0':s
hole_c3:c43_9 :: c3:c4
hole_c5:c64_9 :: c5:c6
hole_true:false5_9 :: true:false
hole_c7:c86_9 :: c7:c8
gen_c:c1:c27_9 :: Nat -> c:c1:c2
gen_0':s8_9 :: Nat -> 0':s
gen_c7:c89_9 :: Nat -> c7:c8


Generator Equations:
gen_c:c1:c27_9(0) <=> c
gen_c:c1:c27_9(+(x, 1)) <=> c2(gen_c:c1:c27_9(x))
gen_0':s8_9(0) <=> 0'
gen_0':s8_9(+(x, 1)) <=> s(gen_0':s8_9(x))
gen_c7:c89_9(0) <=> c7
gen_c7:c89_9(+(x, 1)) <=> c8(gen_c7:c89_9(x), c3)


The following defined symbols remain to be analysed:
LE, MINUS, le, QUOT, minus, quot

They will be analysed ascendingly in the following order:
LE < MINUS
le < MINUS
MINUS < QUOT
le < minus
minus < QUOT
minus < quot

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

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

(33)
BOUNDS(n^1, INF)

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

(34)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
MINUS(0', z0) -> c3
MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
IFMINUS(true, s(z0), z1) -> c5
IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
QUOT(0', s(z0)) -> c7
QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
minus(0', z0) -> 0'
minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
ifMinus(true, s(z0), z1) -> 0'
ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s -> 0':s -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c:c1:c2 -> c3:c4
IFMINUS :: true:false -> 0':s -> 0':s -> c5:c6
le :: 0':s -> 0':s -> true:false
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
QUOT :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c3:c4 -> c7:c8
minus :: 0':s -> 0':s -> 0':s
ifMinus :: true:false -> 0':s -> 0':s -> 0':s
quot :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_9 :: c:c1:c2
hole_0':s2_9 :: 0':s
hole_c3:c43_9 :: c3:c4
hole_c5:c64_9 :: c5:c6
hole_true:false5_9 :: true:false
hole_c7:c86_9 :: c7:c8
gen_c:c1:c27_9 :: Nat -> c:c1:c2
gen_0':s8_9 :: Nat -> 0':s
gen_c7:c89_9 :: Nat -> c7:c8


Lemmas:
LE(gen_0':s8_9(n11_9), gen_0':s8_9(n11_9)) -> gen_c:c1:c27_9(n11_9), rt in Omega(1 + n11_9)


Generator Equations:
gen_c:c1:c27_9(0) <=> c
gen_c:c1:c27_9(+(x, 1)) <=> c2(gen_c:c1:c27_9(x))
gen_0':s8_9(0) <=> 0'
gen_0':s8_9(+(x, 1)) <=> s(gen_0':s8_9(x))
gen_c7:c89_9(0) <=> c7
gen_c7:c89_9(+(x, 1)) <=> c8(gen_c7:c89_9(x), c3)


The following defined symbols remain to be analysed:
le, MINUS, QUOT, minus, quot

They will be analysed ascendingly in the following order:
le < MINUS
MINUS < QUOT
le < minus
minus < QUOT
minus < quot

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
le(gen_0':s8_9(n569_9), gen_0':s8_9(n569_9)) -> true, rt in Omega(0)

Induction Base:
le(gen_0':s8_9(0), gen_0':s8_9(0)) ->_R^Omega(0)
true

Induction Step:
le(gen_0':s8_9(+(n569_9, 1)), gen_0':s8_9(+(n569_9, 1))) ->_R^Omega(0)
le(gen_0':s8_9(n569_9), gen_0':s8_9(n569_9)) ->_IH
true

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

(36)
Obligation:
Innermost TRS:
Rules:
LE(0', z0) -> c
LE(s(z0), 0') -> c1
LE(s(z0), s(z1)) -> c2(LE(z0, z1))
MINUS(0', z0) -> c3
MINUS(s(z0), z1) -> c4(IFMINUS(le(s(z0), z1), s(z0), z1), LE(s(z0), z1))
IFMINUS(true, s(z0), z1) -> c5
IFMINUS(false, s(z0), z1) -> c6(MINUS(z0, z1))
QUOT(0', s(z0)) -> c7
QUOT(s(z0), s(z1)) -> c8(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
le(0', z0) -> true
le(s(z0), 0') -> false
le(s(z0), s(z1)) -> le(z0, z1)
minus(0', z0) -> 0'
minus(s(z0), z1) -> ifMinus(le(s(z0), z1), s(z0), z1)
ifMinus(true, s(z0), z1) -> 0'
ifMinus(false, s(z0), z1) -> s(minus(z0, z1))
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))

Types:
LE :: 0':s -> 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
MINUS :: 0':s -> 0':s -> c3:c4
c3 :: c3:c4
c4 :: c5:c6 -> c:c1:c2 -> c3:c4
IFMINUS :: true:false -> 0':s -> 0':s -> c5:c6
le :: 0':s -> 0':s -> true:false
true :: true:false
c5 :: c5:c6
false :: true:false
c6 :: c3:c4 -> c5:c6
QUOT :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c3:c4 -> c7:c8
minus :: 0':s -> 0':s -> 0':s
ifMinus :: true:false -> 0':s -> 0':s -> 0':s
quot :: 0':s -> 0':s -> 0':s
hole_c:c1:c21_9 :: c:c1:c2
hole_0':s2_9 :: 0':s
hole_c3:c43_9 :: c3:c4
hole_c5:c64_9 :: c5:c6
hole_true:false5_9 :: true:false
hole_c7:c86_9 :: c7:c8
gen_c:c1:c27_9 :: Nat -> c:c1:c2
gen_0':s8_9 :: Nat -> 0':s
gen_c7:c89_9 :: Nat -> c7:c8


Lemmas:
LE(gen_0':s8_9(n11_9), gen_0':s8_9(n11_9)) -> gen_c:c1:c27_9(n11_9), rt in Omega(1 + n11_9)
le(gen_0':s8_9(n569_9), gen_0':s8_9(n569_9)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c27_9(0) <=> c
gen_c:c1:c27_9(+(x, 1)) <=> c2(gen_c:c1:c27_9(x))
gen_0':s8_9(0) <=> 0'
gen_0':s8_9(+(x, 1)) <=> s(gen_0':s8_9(x))
gen_c7:c89_9(0) <=> c7
gen_c7:c89_9(+(x, 1)) <=> c8(gen_c7:c89_9(x), c3)


The following defined symbols remain to be analysed:
MINUS, QUOT, minus, quot

They will be analysed ascendingly in the following order:
MINUS < QUOT
minus < QUOT
minus < quot