KILLED
proof of input_Z6F88CH24a.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CpxTRS
(3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(4) CpxTRS
(5) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) typed CpxTrs
    (13) OrderProof [LOWER BOUND(ID), 19 ms]
    (14) typed CpxTrs
    (15) RewriteLemmaProof [LOWER BOUND(ID), 386 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) typed CpxTrs
            (21) RewriteLemmaProof [LOWER BOUND(ID), 90 ms]
            (22) typed CpxTrs
            (23) RewriteLemmaProof [LOWER BOUND(ID), 51 ms]
            (24) typed CpxTrs
            (25) RewriteLemmaProof [LOWER BOUND(ID), 117 ms]
            (26) typed CpxTrs
            (27) RewriteLemmaProof [LOWER BOUND(ID), 353 ms]
            (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 222.9 s]
            (30) BOUNDS(1, INF)
(31) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(32) CdtProblem
    (33) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (34) CdtProblem
    (35) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (36) CdtProblem
    (37) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (38) CpxRelTRS
        (39) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
        (40) CpxTRS
        (41) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
        (42) CpxWeightedTrs
            (43) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
            (44) CpxTypedWeightedTrs
            (45) CompletionProof [UPPER BOUND(ID), 0 ms]
            (46) CpxTypedWeightedCompleteTrs
                (47) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
                (48) CpxTypedWeightedCompleteTrs
                (49) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
                (50) CpxRNTS
                (51) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
                (52) CpxRNTS
                (53) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
                (54) CpxRNTS
                (55) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (56) CpxRNTS
                (57) IntTrsBoundProof [UPPER BOUND(ID), 159 ms]
                (58) CpxRNTS
                (59) IntTrsBoundProof [UPPER BOUND(ID), 5 ms]
                (60) CpxRNTS
                (61) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (62) CpxRNTS
                (63) IntTrsBoundProof [UPPER BOUND(ID), 107 ms]
                (64) CpxRNTS
                (65) IntTrsBoundProof [UPPER BOUND(ID), 84 ms]
                (66) CpxRNTS
                (67) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
                (68) CpxRNTS
                (69) IntTrsBoundProof [UPPER BOUND(ID), 408 ms]
                (70) CpxRNTS
                (71) IntTrsBoundProof [UPPER BOUND(ID), 193 ms]
                (72) CpxRNTS
            (73) CompletionProof [UPPER BOUND(ID), 0 ms]
            (74) CpxTypedWeightedCompleteTrs
                (75) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
                (76) CpxRNTS
    (77) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 104 ms]
    (78) CdtProblem
        (79) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 39 ms]
        (80) CdtProblem
        (81) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 11 ms]
        (82) CdtProblem
        (83) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (84) CdtProblem
        (85) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
        (86) CdtProblem
        (87) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (88) CdtProblem
        (89) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
        (90) CdtProblem
        (91) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (92) CdtProblem
        (93) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (94) CdtProblem
        (95) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (96) CdtProblem
        (97) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (98) CdtProblem
        (99) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
        (100) CdtProblem
        (101) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (102) CdtProblem
        (103) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (104) CdtProblem
        (105) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (106) CdtProblem
        (107) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (108) CdtProblem
        (109) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (110) CdtProblem
        (111) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (112) CdtProblem
        (113) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (114) CdtProblem
        (115) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (116) CdtProblem
        (117) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (118) CdtProblem
        (119) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (120) CdtProblem
        (121) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (122) CdtProblem
        (123) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (124) CdtProblem
(125) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(126) CpxWeightedTrs
    (127) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (128) CpxTypedWeightedTrs
    (129) CompletionProof [UPPER BOUND(ID), 0 ms]
    (130) CpxTypedWeightedCompleteTrs
        (131) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (132) CpxTypedWeightedCompleteTrs
        (133) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (134) CpxRNTS
        (135) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (136) CpxRNTS
        (137) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
        (138) CpxRNTS
        (139) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (140) CpxRNTS
        (141) IntTrsBoundProof [UPPER BOUND(ID), 339 ms]
        (142) CpxRNTS
        (143) IntTrsBoundProof [UPPER BOUND(ID), 96 ms]
        (144) CpxRNTS
        (145) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
        (146) CpxRNTS
        (147) IntTrsBoundProof [UPPER BOUND(ID), 901 ms]
        (148) CpxRNTS
        (149) IntTrsBoundProof [UPPER BOUND(ID), 184 ms]
        (150) CpxRNTS
    (151) CompletionProof [UPPER BOUND(ID), 0 ms]
    (152) CpxTypedWeightedCompleteTrs
        (153) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (154) CpxRNTS


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

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


The TRS R consists of the following rules:

   from(X) -> cons(X, from(s(X)))
   sel(0, cons(X, XS)) -> X
   sel(s(N), cons(X, XS)) -> sel(N, XS)
   minus(X, 0) -> 0
   minus(s(X), s(Y)) -> minus(X, Y)
   quot(0, s(Y)) -> 0
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
   zWquot(XS, nil) -> nil
   zWquot(nil, XS) -> nil
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS))

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

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

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


The TRS R consists of the following rules:

   from(X) -> cons(X, from(s(X)))
   sel(0', cons(X, XS)) -> X
   sel(s(N), cons(X, XS)) -> sel(N, XS)
   minus(X, 0') -> 0'
   minus(s(X), s(Y)) -> minus(X, Y)
   quot(0', s(Y)) -> 0'
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
   zWquot(XS, nil) -> nil
   zWquot(nil, XS) -> nil
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS))

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

(3) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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


The TRS R consists of the following rules:

   from(X) -> cons(X, from(s(X)))
   sel(0, cons(X, XS)) -> X
   sel(s(N), cons(X, XS)) -> sel(N, XS)
   minus(X, 0) -> 0
   minus(s(X), s(Y)) -> minus(X, Y)
   quot(0, s(Y)) -> 0
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
   zWquot(XS, nil) -> nil
   zWquot(nil, XS) -> nil
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS))

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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   from(z0) -> cons(z0, from(s(z0)))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(0, cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0) -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(0, cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0) -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
K tuples:none
Defined Rule Symbols:   from_1, sel_2, minus_2, quot_2, zWquot_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2

Compound Symbols:   c_1, c1, c2_1, c3, c4_1, c5, c6_2, c7, c8, c9_1, c10_1


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

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


The TRS R consists of the following rules:

   FROM(z0) -> c(FROM(s(z0)))
   SEL(0, cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0) -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))

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

   from(z0) -> cons(z0, from(s(z0)))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

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

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

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

   FROM(z0) -> c(FROM(s(z0)))
   SEL(0', cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0') -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0', s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))

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

   from(z0) -> cons(z0, from(s(z0)))
   sel(0', cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   minus(z0, 0') -> 0'
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0', s(z0)) -> 0'
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

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

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

(12)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10

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

(13) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
FROM, SEL, MINUS, QUOT, minus, ZWQUOT, from, sel, quot, zWquot

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

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

(14)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
FROM, SEL, MINUS, QUOT, minus, ZWQUOT, from, sel, quot, zWquot

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

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)

Induction Base:
SEL(gen_s:0'9_11(0), gen_cons:nil11_11(+(1, 0))) ->_R^Omega(1)
c1

Induction Step:
SEL(gen_s:0'9_11(+(n165_11, 1)), gen_cons:nil11_11(+(1, +(n165_11, 1)))) ->_R^Omega(1)
c2(SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11)))) ->_IH
c2(gen_c1:c210_11(c166_11))

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

(16)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
SEL, MINUS, QUOT, minus, ZWQUOT, from, sel, quot, zWquot

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

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
MINUS, QUOT, minus, ZWQUOT, from, sel, quot, zWquot

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

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)

Induction Base:
MINUS(gen_s:0'9_11(0), gen_s:0'9_11(0)) ->_R^Omega(1)
c3

Induction Step:
MINUS(gen_s:0'9_11(+(n693_11, 1)), gen_s:0'9_11(+(n693_11, 1))) ->_R^Omega(1)
c4(MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11))) ->_IH
c4(gen_c3:c412_11(c694_11))

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

(22)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
minus, QUOT, ZWQUOT, from, sel, quot, zWquot

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

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) -> gen_s:0'9_11(0), rt in Omega(0)

Induction Base:
minus(gen_s:0'9_11(0), gen_s:0'9_11(0)) ->_R^Omega(0)
0'

Induction Step:
minus(gen_s:0'9_11(+(n1270_11, 1)), gen_s:0'9_11(+(n1270_11, 1))) ->_R^Omega(0)
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) ->_IH
gen_s:0'9_11(0)

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

(24)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) -> gen_s:0'9_11(0), rt in Omega(0)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
QUOT, ZWQUOT, from, sel, quot, zWquot

They will be analysed ascendingly in the following order:
QUOT < ZWQUOT
quot < zWquot

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ZWQUOT(gen_cons:nil11_11(n2873_11), gen_cons:nil11_11(n2873_11)) -> gen_c7:c8:c9:c1014_11(n2873_11), rt in Omega(1 + n2873_11)

Induction Base:
ZWQUOT(gen_cons:nil11_11(0), gen_cons:nil11_11(0)) ->_R^Omega(1)
c7

Induction Step:
ZWQUOT(gen_cons:nil11_11(+(n2873_11, 1)), gen_cons:nil11_11(+(n2873_11, 1))) ->_R^Omega(1)
c10(ZWQUOT(gen_cons:nil11_11(n2873_11), gen_cons:nil11_11(n2873_11))) ->_IH
c10(gen_c7:c8:c9:c1014_11(c2874_11))

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

(26)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) -> gen_s:0'9_11(0), rt in Omega(0)
ZWQUOT(gen_cons:nil11_11(n2873_11), gen_cons:nil11_11(n2873_11)) -> gen_c7:c8:c9:c1014_11(n2873_11), rt in Omega(1 + n2873_11)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
from, sel, quot, zWquot

They will be analysed ascendingly in the following order:
quot < zWquot

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sel(gen_s:0'9_11(n4111_11), gen_cons:nil11_11(+(1, n4111_11))) -> gen_s:0'9_11(0), rt in Omega(0)

Induction Base:
sel(gen_s:0'9_11(0), gen_cons:nil11_11(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
sel(gen_s:0'9_11(+(n4111_11, 1)), gen_cons:nil11_11(+(1, +(n4111_11, 1)))) ->_R^Omega(0)
sel(gen_s:0'9_11(n4111_11), gen_cons:nil11_11(+(1, n4111_11))) ->_IH
gen_s:0'9_11(0)

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

(28)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) -> gen_s:0'9_11(0), rt in Omega(0)
ZWQUOT(gen_cons:nil11_11(n2873_11), gen_cons:nil11_11(n2873_11)) -> gen_c7:c8:c9:c1014_11(n2873_11), rt in Omega(1 + n2873_11)
sel(gen_s:0'9_11(n4111_11), gen_cons:nil11_11(+(1, n4111_11))) -> gen_s:0'9_11(0), rt in Omega(0)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
quot, zWquot

They will be analysed ascendingly in the following order:
quot < zWquot

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
zWquot(gen_cons:nil11_11(+(1, n5050_11)), gen_cons:nil11_11(+(1, n5050_11))) -> *15_11, rt in Omega(0)

Induction Base:
zWquot(gen_cons:nil11_11(+(1, 0)), gen_cons:nil11_11(+(1, 0)))

Induction Step:
zWquot(gen_cons:nil11_11(+(1, +(n5050_11, 1))), gen_cons:nil11_11(+(1, +(n5050_11, 1)))) ->_R^Omega(0)
cons(quot(0', 0'), zWquot(gen_cons:nil11_11(+(1, n5050_11)), gen_cons:nil11_11(+(1, n5050_11)))) ->_IH
cons(quot(0', 0'), *15_11)

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

(30)
BOUNDS(1, INF)

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

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

(32)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   from(z0) -> cons(z0, from(s(z0)))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(0, cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0) -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(0, cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0) -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
K tuples:none
Defined Rule Symbols:   from_1, sel_2, minus_2, quot_2, zWquot_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2

Compound Symbols:   c_1, c1, c2_1, c3, c4_1, c5, c6_2, c7, c8, c9_1, c10_1


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

(33) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 5 trailing nodes:
   ZWQUOT(nil, z0) -> c8
   QUOT(0, s(z0)) -> c5
   SEL(0, cons(z0, z1)) -> c1
   MINUS(z0, 0) -> c3
   ZWQUOT(z0, nil) -> c7

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

(34)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   from(z0) -> cons(z0, from(s(z0)))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
K tuples:none
Defined Rule Symbols:   from_1, sel_2, minus_2, quot_2, zWquot_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c6_2, c9_1, c10_1


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

(35) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   from(z0) -> cons(z0, from(s(z0)))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

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

(36)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
K tuples:none
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c6_2, c9_1, c10_1


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

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

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


The TRS R consists of the following rules:

   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))

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

   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)

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

(39) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(40)
Obligation:
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)

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

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

(42)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   FROM(z0) -> c(FROM(s(z0))) [1]
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) [1]
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) [1]
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) [1]
   minus(z0, 0) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]

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

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

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

   FROM(z0) -> c(FROM(s(z0))) [1]
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) [1]
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) [1]
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) [1]
   minus(z0, 0) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]

The TRS has the following type information:
FROM :: s:0 -> c
c :: c -> c
s :: s:0 -> s:0
SEL :: s:0 -> cons -> c2
cons :: s:0 -> cons -> cons
c2 :: c2 -> c2
MINUS :: s:0 -> s:0 -> c4
c4 :: c4 -> c4
QUOT :: s:0 -> s:0 -> c6
c6 :: c6 -> c4 -> c6
minus :: s:0 -> s:0 -> s:0
ZWQUOT :: cons -> cons -> c9:c10
c9 :: c6 -> c9:c10
c10 :: c9:c10 -> c9:c10
0 :: s:0

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

(45) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

   FROM_1
   SEL_2
   MINUS_2
   QUOT_2
   ZWQUOT_2

(c) The following functions are completely defined:

   minus_2

Due to the following rules being added:

   minus(v0, v1) -> 0 [0]

And the following fresh constants:    const, const1, const2, const3, const4, const5

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

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

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

   FROM(z0) -> c(FROM(s(z0))) [1]
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) [1]
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) [1]
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) [1]
   minus(z0, 0) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   minus(v0, v1) -> 0 [0]

The TRS has the following type information:
FROM :: s:0 -> c
c :: c -> c
s :: s:0 -> s:0
SEL :: s:0 -> cons -> c2
cons :: s:0 -> cons -> cons
c2 :: c2 -> c2
MINUS :: s:0 -> s:0 -> c4
c4 :: c4 -> c4
QUOT :: s:0 -> s:0 -> c6
c6 :: c6 -> c4 -> c6
minus :: s:0 -> s:0 -> s:0
ZWQUOT :: cons -> cons -> c9:c10
c9 :: c6 -> c9:c10
c10 :: c9:c10 -> c9:c10
0 :: s:0
const :: c
const1 :: c2
const2 :: cons
const3 :: c4
const4 :: c6
const5 :: c9:c10

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

(47) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

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

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

   FROM(z0) -> c(FROM(s(z0))) [1]
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) [1]
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) [1]
   QUOT(s(z0), s(0)) -> c6(QUOT(0, s(0)), MINUS(z0, 0)) [1]
   QUOT(s(s(z0')), s(s(z1'))) -> c6(QUOT(minus(z0', z1'), s(s(z1'))), MINUS(s(z0'), s(z1'))) [1]
   QUOT(s(z0), s(z1)) -> c6(QUOT(0, s(z1)), MINUS(z0, z1)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) [1]
   minus(z0, 0) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   minus(v0, v1) -> 0 [0]

The TRS has the following type information:
FROM :: s:0 -> c
c :: c -> c
s :: s:0 -> s:0
SEL :: s:0 -> cons -> c2
cons :: s:0 -> cons -> cons
c2 :: c2 -> c2
MINUS :: s:0 -> s:0 -> c4
c4 :: c4 -> c4
QUOT :: s:0 -> s:0 -> c6
c6 :: c6 -> c4 -> c6
minus :: s:0 -> s:0 -> s:0
ZWQUOT :: cons -> cons -> c9:c10
c9 :: c6 -> c9:c10
c10 :: c9:c10 -> c9:c10
0 :: s:0
const :: c
const1 :: c2
const2 :: cons
const3 :: c4
const4 :: c6
const5 :: c9:c10

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

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

   0 => 0
   const => 0
   const1 => 0
   const2 => 0
   const3 => 0
   const4 => 0
   const5 => 0

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z0) :|: z = z0, z0 >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   QUOT(z, z') -{ 1 }-> 1 + QUOT(minus(z0', z1'), 1 + (1 + z1')) + MINUS(1 + z0', 1 + z1') :|: z' = 1 + (1 + z1'), z = 1 + (1 + z0'), z0' >= 0, z1' >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + z1) + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z0, 0) :|: z = 1 + z0, z' = 1 + 0, z0 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z0, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1


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

(51) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0


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

(53) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { minus }
   { SEL }
   { FROM }
   { MINUS }
   { QUOT }
   { ZWQUOT }

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {minus}, {SEL}, {FROM}, {MINUS}, {QUOT}, {ZWQUOT}

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

(55) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {minus}, {SEL}, {FROM}, {MINUS}, {QUOT}, {ZWQUOT}

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

(57) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: minus
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {minus}, {SEL}, {FROM}, {MINUS}, {QUOT}, {ZWQUOT}
Previous analysis results are:
  minus: runtime: ?, size: O(1) [0]

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

(59) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: minus
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {SEL}, {FROM}, {MINUS}, {QUOT}, {ZWQUOT}
Previous analysis results are:
  minus: runtime: O(1) [0], size: O(1) [0]

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

(61) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(s, 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: s >= 0, s <= 0, z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 0, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {SEL}, {FROM}, {MINUS}, {QUOT}, {ZWQUOT}
Previous analysis results are:
  minus: runtime: O(1) [0], size: O(1) [0]

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

(63) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: SEL
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(s, 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: s >= 0, s <= 0, z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 0, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {SEL}, {FROM}, {MINUS}, {QUOT}, {ZWQUOT}
Previous analysis results are:
  minus: runtime: O(1) [0], size: O(1) [0]
  SEL: runtime: ?, size: O(1) [0]

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

(65) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: SEL
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z'

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(s, 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: s >= 0, s <= 0, z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 }-> 1 + SEL(z - 1, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 0, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {FROM}, {MINUS}, {QUOT}, {ZWQUOT}
Previous analysis results are:
  minus: runtime: O(1) [0], size: O(1) [0]
  SEL: runtime: O(n^1) [z'], size: O(1) [0]

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

(67) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(s, 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: s >= 0, s <= 0, z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 + z2 }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 0, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {FROM}, {MINUS}, {QUOT}, {ZWQUOT}
Previous analysis results are:
  minus: runtime: O(1) [0], size: O(1) [0]
  SEL: runtime: O(n^1) [z'], size: O(1) [0]

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

(69) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: FROM
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(s, 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: s >= 0, s <= 0, z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 + z2 }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 0, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {FROM}, {MINUS}, {QUOT}, {ZWQUOT}
Previous analysis results are:
  minus: runtime: O(1) [0], size: O(1) [0]
  SEL: runtime: O(n^1) [z'], size: O(1) [0]
  FROM: runtime: ?, size: O(1) [0]

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

(71) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: FROM
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z) :|: z >= 0
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(s, 1 + (1 + (z' - 2))) + MINUS(1 + (z - 2), 1 + (z' - 2)) :|: s >= 0, s <= 0, z - 2 >= 0, z' - 2 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + 0) + MINUS(z - 1, 0) :|: z' = 1 + 0, z - 1 >= 0
   QUOT(z, z') -{ 1 }-> 1 + QUOT(0, 1 + (z' - 1)) + MINUS(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   SEL(z, z') -{ 1 + z2 }-> 1 + s'' :|: s'' >= 0, s'' <= 0, z1 >= 0, z' = 1 + z1 + z2, z - 1 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> s' :|: s' >= 0, s' <= 0, z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0

Function symbols to be analyzed: {FROM}, {MINUS}, {QUOT}, {ZWQUOT}
Previous analysis results are:
  minus: runtime: O(1) [0], size: O(1) [0]
  SEL: runtime: O(n^1) [z'], size: O(1) [0]
  FROM: runtime: INF, size: O(1) [0]

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

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

   minus(v0, v1) -> null_minus [0]
   SEL(v0, v1) -> null_SEL [0]
   MINUS(v0, v1) -> null_MINUS [0]
   QUOT(v0, v1) -> null_QUOT [0]
   ZWQUOT(v0, v1) -> null_ZWQUOT [0]

And the following fresh constants:    null_minus, null_SEL, null_MINUS, null_QUOT, null_ZWQUOT, const, const1

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

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

   FROM(z0) -> c(FROM(s(z0))) [1]
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) [1]
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) [1]
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) [1]
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) [1]
   minus(z0, 0) -> 0 [0]
   minus(s(z0), s(z1)) -> minus(z0, z1) [0]
   minus(v0, v1) -> null_minus [0]
   SEL(v0, v1) -> null_SEL [0]
   MINUS(v0, v1) -> null_MINUS [0]
   QUOT(v0, v1) -> null_QUOT [0]
   ZWQUOT(v0, v1) -> null_ZWQUOT [0]

The TRS has the following type information:
FROM :: s:0:null_minus -> c
c :: c -> c
s :: s:0:null_minus -> s:0:null_minus
SEL :: s:0:null_minus -> cons -> c2:null_SEL
cons :: s:0:null_minus -> cons -> cons
c2 :: c2:null_SEL -> c2:null_SEL
MINUS :: s:0:null_minus -> s:0:null_minus -> c4:null_MINUS
c4 :: c4:null_MINUS -> c4:null_MINUS
QUOT :: s:0:null_minus -> s:0:null_minus -> c6:null_QUOT
c6 :: c6:null_QUOT -> c4:null_MINUS -> c6:null_QUOT
minus :: s:0:null_minus -> s:0:null_minus -> s:0:null_minus
ZWQUOT :: cons -> cons -> c9:c10:null_ZWQUOT
c9 :: c6:null_QUOT -> c9:c10:null_ZWQUOT
c10 :: c9:c10:null_ZWQUOT -> c9:c10:null_ZWQUOT
0 :: s:0:null_minus
null_minus :: s:0:null_minus
null_SEL :: c2:null_SEL
null_MINUS :: c4:null_MINUS
null_QUOT :: c6:null_QUOT
null_ZWQUOT :: c9:c10:null_ZWQUOT
const :: c
const1 :: cons

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

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

   0 => 0
   null_minus => 0
   null_SEL => 0
   null_MINUS => 0
   null_QUOT => 0
   null_ZWQUOT => 0
   const => 0
   const1 => 0

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

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

   FROM(z) -{ 1 }-> 1 + FROM(1 + z0) :|: z = z0, z0 >= 0
   MINUS(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   MINUS(z, z') -{ 1 }-> 1 + MINUS(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   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
   SEL(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   SEL(z, z') -{ 1 }-> 1 + SEL(z0, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   ZWQUOT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   ZWQUOT(z, z') -{ 1 }-> 1 + ZWQUOT(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   ZWQUOT(z, z') -{ 1 }-> 1 + QUOT(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   minus(z, z') -{ 0 }-> minus(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   minus(z, z') -{ 0 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

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

(77) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
We considered the (Usable) Rules:none
And the Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(FROM(x_1)) = [2]x_1 + [2]x_1^2
   POL(MINUS(x_1, x_2)) = 0
   POL(QUOT(x_1, x_2)) = 0
   POL(SEL(x_1, x_2)) = [2]x_2^2
   POL(ZWQUOT(x_1, x_2)) = 0
   POL(c(x_1)) = x_1
   POL(c10(x_1)) = x_1
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c9(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_2
   POL(minus(x_1, x_2)) = 0
   POL(s(x_1)) = 0

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

(78)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
K tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c6_2, c9_1, c10_1


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

(79) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
We considered the (Usable) Rules:
   minus(s(z0), s(z1)) -> minus(z0, z1)
   minus(z0, 0) -> 0
And the Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(FROM(x_1)) = 0
   POL(MINUS(x_1, x_2)) = 0
   POL(QUOT(x_1, x_2)) = x_1^2
   POL(SEL(x_1, x_2)) = x_2 + [2]x_2^2
   POL(ZWQUOT(x_1, x_2)) = [2]x_1^2
   POL(c(x_1)) = x_1
   POL(c10(x_1)) = x_1
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c9(x_1)) = x_1
   POL(cons(x_1, x_2)) = x_1 + x_2
   POL(minus(x_1, x_2)) = 0
   POL(s(x_1)) = [2]

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

(80)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
K tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c6_2, c9_1, c10_1


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

(81) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
We considered the (Usable) Rules:
   minus(s(z0), s(z1)) -> minus(z0, z1)
   minus(z0, 0) -> 0
And the Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [1]
   POL(FROM(x_1)) = 0
   POL(MINUS(x_1, x_2)) = x_1
   POL(QUOT(x_1, x_2)) = [1] + x_1 + x_2
   POL(SEL(x_1, x_2)) = x_1 + x_2
   POL(ZWQUOT(x_1, x_2)) = [1] + x_1 + x_2
   POL(c(x_1)) = x_1
   POL(c10(x_1)) = x_1
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c9(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_1 + x_2
   POL(minus(x_1, x_2)) = [1]
   POL(s(x_1)) = [1] + x_1

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

(82)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
K tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c6_2, c9_1, c10_1


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

(83) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1)) by 
   QUOT(s(z0), s(0)) -> c6(QUOT(0, s(0)), MINUS(z0, 0))
   QUOT(s(s(z0)), s(s(z1))) -> c6(QUOT(minus(z0, z1), s(s(z1))), MINUS(s(z0), s(z1)))

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

(84)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(z0), s(0)) -> c6(QUOT(0, s(0)), MINUS(z0, 0))
   QUOT(s(s(z0)), s(s(z1))) -> c6(QUOT(minus(z0, z1), s(s(z1))), MINUS(s(z0), s(z1)))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
K tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, ZWQUOT_2, QUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c9_1, c10_1, c6_2


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

(85) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   QUOT(s(z0), s(0)) -> c6(QUOT(0, s(0)), MINUS(z0, 0))

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

(86)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(z0)), s(s(z1))) -> c6(QUOT(minus(z0, z1), s(s(z1))), MINUS(s(z0), s(z1)))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
K tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, ZWQUOT_2, QUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c9_1, c10_1, c6_2


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

(87) CdtNarrowingProof (BOTH BOUNDS(ID, ID))
Use narrowing to replace QUOT(s(s(z0)), s(s(z1))) -> c6(QUOT(minus(z0, z1), s(s(z1))), MINUS(s(z0), s(z1))) by 
   QUOT(s(s(z0)), s(s(0))) -> c6(QUOT(0, s(s(0))), MINUS(s(z0), s(0)))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))

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

(88)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(z0)), s(s(0))) -> c6(QUOT(0, s(s(0))), MINUS(s(z0), s(0)))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
K tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, ZWQUOT_2, QUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c9_1, c10_1, c6_2, c6_1


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

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

(90)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
   QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0)))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
K tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, ZWQUOT_2, QUOT_2

Compound Symbols:   c_1, c2_1, c4_1, c9_1, c10_1, c6_2, c6_1


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

(91) CdtInstantiationProof (BOTH BOUNDS(ID, ID))
Use instantiation to replace FROM(z0) -> c(FROM(s(z0))) by 
   FROM(s(x0)) -> c(FROM(s(s(x0))))

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

(92)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
   QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0)))
   FROM(s(x0)) -> c(FROM(s(s(x0))))
S tuples:
   FROM(s(x0)) -> c(FROM(s(s(x0))))
K tuples:
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   SEL_2, MINUS_2, ZWQUOT_2, QUOT_2, FROM_1

Compound Symbols:   c2_1, c4_1, c9_1, c10_1, c6_2, c6_1, c_1


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

(93) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2)) by 
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))

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

(94)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
   QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0)))
   FROM(s(x0)) -> c(FROM(s(s(x0))))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
S tuples:
   FROM(s(x0)) -> c(FROM(s(s(x0))))
K tuples:
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   MINUS_2, ZWQUOT_2, QUOT_2, FROM_1, SEL_2

Compound Symbols:   c4_1, c9_1, c10_1, c6_2, c6_1, c_1, c2_1


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

(95) CdtInstantiationProof (BOTH BOUNDS(ID, ID))
Use instantiation to replace FROM(s(x0)) -> c(FROM(s(s(x0)))) by 
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))

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

(96)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
   QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0)))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   MINUS_2, ZWQUOT_2, QUOT_2, SEL_2, FROM_1

Compound Symbols:   c4_1, c9_1, c10_1, c6_2, c6_1, c2_1, c_1


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

(97) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1)) by 
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))

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

(98)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
   QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0)))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   ZWQUOT_2, QUOT_2, SEL_2, FROM_1, MINUS_2

Compound Symbols:   c9_1, c10_1, c6_2, c6_1, c2_1, c_1, c4_1


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

(99) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing nodes:
   QUOT(s(s(z0)), s(s(0))) -> c6(MINUS(s(z0), s(0)))

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

(100)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   ZWQUOT_2, QUOT_2, SEL_2, FROM_1, MINUS_2

Compound Symbols:   c9_1, c10_1, c6_2, c6_1, c2_1, c_1, c4_1


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

(101) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2)) by 
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))

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

(102)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   ZWQUOT_2, QUOT_2, SEL_2, FROM_1, MINUS_2

Compound Symbols:   c10_1, c6_2, c6_1, c2_1, c_1, c4_1, c9_1


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

(103) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3)) by 
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))

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

(104)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1)))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   QUOT_2, SEL_2, FROM_1, MINUS_2, ZWQUOT_2

Compound Symbols:   c6_2, c6_1, c2_1, c_1, c4_1, c9_1, c10_1


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

(105) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace QUOT(s(s(x0)), s(s(x1))) -> c6(MINUS(s(x0), s(x1))) by 
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))

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

(106)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2)))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   QUOT_2, SEL_2, FROM_1, MINUS_2, ZWQUOT_2

Compound Symbols:   c6_2, c2_1, c_1, c4_1, c9_1, c10_1, c6_1


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

(107) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace SEL(s(s(y0)), cons(z1, cons(y1, y2))) -> c2(SEL(s(y0), cons(y1, y2))) by 
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))

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

(108)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1)))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   QUOT_2, FROM_1, MINUS_2, ZWQUOT_2, SEL_2

Compound Symbols:   c6_2, c_1, c4_1, c9_1, c10_1, c6_1, c2_1


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

(109) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace MINUS(s(s(y0)), s(s(y1))) -> c4(MINUS(s(y0), s(y1))) by 
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))

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

(110)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))))
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   QUOT_2, FROM_1, ZWQUOT_2, SEL_2, MINUS_2

Compound Symbols:   c6_2, c_1, c9_1, c10_1, c6_1, c2_1, c4_1


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

(111) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace QUOT(s(s(s(z0))), s(s(s(z1)))) -> c6(QUOT(minus(z0, z1), s(s(s(z1)))), MINUS(s(s(z0)), s(s(z1)))) by 
   QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(QUOT(minus(s(y0), s(y1)), s(s(s(s(y1))))), MINUS(s(s(s(y0))), s(s(s(y1)))))

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

(112)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(QUOT(minus(s(y0), s(y1)), s(s(s(s(y1))))), MINUS(s(s(s(y0))), s(s(s(y1)))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2

Compound Symbols:   c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2


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

(113) CdtRewritingProof (BOTH BOUNDS(ID, ID))
Used rewriting to replace QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(QUOT(minus(s(y0), s(y1)), s(s(s(s(y1))))), MINUS(s(s(s(y0))), s(s(s(y1))))) by QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1)))))
----------------------------------------

(114)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1)))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2

Compound Symbols:   c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2


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

(115) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ZWQUOT(cons(s(s(y0)), z1), cons(s(s(y1)), z3)) -> c9(QUOT(s(s(y0)), s(s(y1)))) by 
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))

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

(116)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1)))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3)))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2

Compound Symbols:   c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2


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

(117) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ZWQUOT(cons(z0, cons(y0, y1)), cons(z2, cons(y2, y3))) -> c10(ZWQUOT(cons(y0, y1), cons(y2, y3))) by 
   ZWQUOT(cons(z0, cons(s(s(s(y0))), z2)), cons(z3, cons(s(s(s(y2))), z5))) -> c10(ZWQUOT(cons(s(s(s(y0))), z2), cons(s(s(s(y2))), z5)))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))

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

(118)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1)))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2

Compound Symbols:   c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2


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

(119) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ZWQUOT(cons(z0, cons(s(s(y0)), y1)), cons(z2, cons(s(s(y2)), y3))) -> c10(ZWQUOT(cons(s(s(y0)), y1), cons(s(s(y2)), y3))) by 
   ZWQUOT(cons(z0, cons(s(s(s(y0))), z2)), cons(z3, cons(s(s(s(y2))), z5))) -> c10(ZWQUOT(cons(s(s(s(y0))), z2), cons(s(s(s(y2))), z5)))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5))))

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

(120)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1))))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1)))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, ZWQUOT_2, QUOT_2, SEL_2, MINUS_2

Compound Symbols:   c_1, c9_1, c10_1, c6_1, c2_1, c4_1, c6_2


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

(121) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace QUOT(s(s(s(y0))), s(s(s(y1)))) -> c6(MINUS(s(s(y0)), s(s(y1)))) by 
   QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(MINUS(s(s(s(y0))), s(s(s(y1)))))

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

(122)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1)))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5))))
   QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(MINUS(s(s(s(y0))), s(s(s(y1)))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, ZWQUOT_2, SEL_2, MINUS_2, QUOT_2

Compound Symbols:   c_1, c9_1, c10_1, c2_1, c4_1, c6_2, c6_1


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

(123) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1))))) by 
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))

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

(124)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
Tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
   ZWQUOT(cons(s(s(s(y0))), z1), cons(s(s(s(y1))), z3)) -> c9(QUOT(s(s(s(y0))), s(s(s(y1)))))
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   QUOT(s(s(s(s(z0)))), s(s(s(s(z1))))) -> c6(QUOT(minus(z0, z1), s(s(s(s(z1))))), MINUS(s(s(s(z0))), s(s(s(z1)))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5))))
   QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))) -> c6(MINUS(s(s(s(y0))), s(s(s(y1)))))
S tuples:
   FROM(s(s(x0))) -> c(FROM(s(s(s(x0)))))
K tuples:
   ZWQUOT(cons(z0, cons(s(s(s(y0))), y1)), cons(z2, cons(s(s(s(y2))), y3))) -> c10(ZWQUOT(cons(s(s(s(y0))), y1), cons(s(s(s(y2))), y3)))
   SEL(s(s(s(y0))), cons(z1, cons(z2, cons(y2, y3)))) -> c2(SEL(s(s(y0)), cons(z2, cons(y2, y3))))
   MINUS(s(s(s(y0))), s(s(s(y1)))) -> c4(MINUS(s(s(y0)), s(s(y1))))
   ZWQUOT(cons(s(s(s(s(y0)))), z1), cons(s(s(s(s(y1)))), z3)) -> c9(QUOT(s(s(s(s(y0)))), s(s(s(s(y1))))))
   ZWQUOT(cons(z0, cons(z1, cons(y1, y2))), cons(z3, cons(z4, cons(y4, y5)))) -> c10(ZWQUOT(cons(z1, cons(y1, y2)), cons(z4, cons(y4, y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(s(y1))), y2))), cons(z3, cons(z4, cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(s(y1))), y2)), cons(z4, cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(z1, cons(s(s(y1)), y2))), cons(z3, cons(z4, cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(z1, cons(s(s(y1)), y2)), cons(z4, cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(s(s(y0)))), z2)), cons(z3, cons(s(s(s(s(y2)))), z5))) -> c10(ZWQUOT(cons(s(s(s(s(y0)))), z2), cons(s(s(s(s(y2)))), z5)))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(y1))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(y4))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(y1))), y2)), cons(s(s(z4)), cons(s(s(s(y4))), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(y1)), y2))), cons(z3, cons(s(s(z4)), cons(s(s(y4)), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(y1)), y2)), cons(s(s(z4)), cons(s(s(y4)), y5))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(y2, y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(y6, y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(y2, y3))), cons(s(s(z4)), cons(y5, cons(y6, y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(s(y2))), y3))), cons(s(s(z4)), cons(y5, cons(s(s(s(y6))), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3)))), cons(z3, cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7))))) -> c10(ZWQUOT(cons(s(s(z1)), cons(y1, cons(s(s(y2)), y3))), cons(s(s(z4)), cons(y5, cons(s(s(y6)), y7)))))
   ZWQUOT(cons(z0, cons(s(s(z1)), cons(s(s(s(s(y1)))), y2))), cons(z3, cons(s(s(z4)), cons(s(s(s(s(y4)))), y5)))) -> c10(ZWQUOT(cons(s(s(z1)), cons(s(s(s(s(y1)))), y2)), cons(s(s(z4)), cons(s(s(s(s(y4)))), y5))))
Defined Rule Symbols:   minus_2

Defined Pair Symbols:   FROM_1, ZWQUOT_2, SEL_2, MINUS_2, QUOT_2

Compound Symbols:   c_1, c9_1, c10_1, c2_1, c4_1, c6_2, c6_1


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

(125) RelTrsToWeightedTrsProof (UPPER BOUND(ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(126)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   from(X) -> cons(X, from(s(X))) [1]
   sel(0, cons(X, XS)) -> X [1]
   sel(s(N), cons(X, XS)) -> sel(N, XS) [1]
   minus(X, 0) -> 0 [1]
   minus(s(X), s(Y)) -> minus(X, Y) [1]
   quot(0, s(Y)) -> 0 [1]
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) [1]
   zWquot(XS, nil) -> nil [1]
   zWquot(nil, XS) -> nil [1]
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1]

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

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

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

   from(X) -> cons(X, from(s(X))) [1]
   sel(0, cons(X, XS)) -> X [1]
   sel(s(N), cons(X, XS)) -> sel(N, XS) [1]
   minus(X, 0) -> 0 [1]
   minus(s(X), s(Y)) -> minus(X, Y) [1]
   quot(0, s(Y)) -> 0 [1]
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) [1]
   zWquot(XS, nil) -> nil [1]
   zWquot(nil, XS) -> nil [1]
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1]

The TRS has the following type information:
from :: s:0 -> cons:nil
cons :: s:0 -> cons:nil -> cons:nil
s :: s:0 -> s:0
sel :: s:0 -> cons:nil -> s:0
0 :: s:0
minus :: s:0 -> s:0 -> s:0
quot :: s:0 -> s:0 -> s:0
zWquot :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil

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

(129) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

   from_1
   sel_2
   quot_2
   zWquot_2

(c) The following functions are completely defined:

   minus_2

Due to the following rules being added:

   minus(v0, v1) -> 0 [0]

And the following fresh constants: none

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

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

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

   from(X) -> cons(X, from(s(X))) [1]
   sel(0, cons(X, XS)) -> X [1]
   sel(s(N), cons(X, XS)) -> sel(N, XS) [1]
   minus(X, 0) -> 0 [1]
   minus(s(X), s(Y)) -> minus(X, Y) [1]
   quot(0, s(Y)) -> 0 [1]
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) [1]
   zWquot(XS, nil) -> nil [1]
   zWquot(nil, XS) -> nil [1]
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1]
   minus(v0, v1) -> 0 [0]

The TRS has the following type information:
from :: s:0 -> cons:nil
cons :: s:0 -> cons:nil -> cons:nil
s :: s:0 -> s:0
sel :: s:0 -> cons:nil -> s:0
0 :: s:0
minus :: s:0 -> s:0 -> s:0
quot :: s:0 -> s:0 -> s:0
zWquot :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil

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

(131) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

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

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

   from(X) -> cons(X, from(s(X))) [1]
   sel(0, cons(X, XS)) -> X [1]
   sel(s(N), cons(X, XS)) -> sel(N, XS) [1]
   minus(X, 0) -> 0 [1]
   minus(s(X), s(Y)) -> minus(X, Y) [1]
   quot(0, s(Y)) -> 0 [1]
   quot(s(X), s(0)) -> s(quot(0, s(0))) [2]
   quot(s(s(X')), s(s(Y'))) -> s(quot(minus(X', Y'), s(s(Y')))) [2]
   quot(s(X), s(Y)) -> s(quot(0, s(Y))) [1]
   zWquot(XS, nil) -> nil [1]
   zWquot(nil, XS) -> nil [1]
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1]
   minus(v0, v1) -> 0 [0]

The TRS has the following type information:
from :: s:0 -> cons:nil
cons :: s:0 -> cons:nil -> cons:nil
s :: s:0 -> s:0
sel :: s:0 -> cons:nil -> s:0
0 :: s:0
minus :: s:0 -> s:0 -> s:0
quot :: s:0 -> s:0 -> s:0
zWquot :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil

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

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

   0 => 0
   nil => 0

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

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

   from(z) -{ 1 }-> 1 + X + from(1 + X) :|: X >= 0, z = X
   minus(z, z') -{ 1 }-> minus(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
   minus(z, z') -{ 1 }-> 0 :|: X >= 0, z = X, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   quot(z, z') -{ 1 }-> 0 :|: Y >= 0, z' = 1 + Y, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(X', Y'), 1 + (1 + Y')) :|: z' = 1 + (1 + Y'), Y' >= 0, X' >= 0, z = 1 + (1 + X')
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z = 1 + X, X >= 0, z' = 1 + 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 }-> sel(N, XS) :|: z = 1 + N, z' = 1 + X + XS, X >= 0, XS >= 0, N >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = XS, XS >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z' = XS, z = 0, XS >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0


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

(135) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

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

   from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0
   minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0


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

(137) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { sel }
   { from }
   { minus }
   { quot }
   { zWquot }

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

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

   from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0
   minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0

Function symbols to be analyzed: {sel}, {from}, {minus}, {quot}, {zWquot}

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

(139) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0
   minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0

Function symbols to be analyzed: {sel}, {from}, {minus}, {quot}, {zWquot}

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

(141) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: sel
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z'

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

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

   from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0
   minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0

Function symbols to be analyzed: {sel}, {from}, {minus}, {quot}, {zWquot}
Previous analysis results are:
  sel: runtime: ?, size: O(n^1) [z']

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

(143) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: sel
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z

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

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

   from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0
   minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 }-> sel(z - 1, XS) :|: z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0

Function symbols to be analyzed: {from}, {minus}, {quot}, {zWquot}
Previous analysis results are:
  sel: runtime: O(n^1) [1 + z], size: O(n^1) [z']

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

(145) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

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

   from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0
   minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 + z }-> s :|: s >= 0, s <= XS, z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0

Function symbols to be analyzed: {from}, {minus}, {quot}, {zWquot}
Previous analysis results are:
  sel: runtime: O(n^1) [1 + z], size: O(n^1) [z']

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

(147) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: from
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

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

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

   from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0
   minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 + z }-> s :|: s >= 0, s <= XS, z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0

Function symbols to be analyzed: {from}, {minus}, {quot}, {zWquot}
Previous analysis results are:
  sel: runtime: O(n^1) [1 + z], size: O(n^1) [z']
  from: runtime: ?, size: O(1) [0]

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

(149) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: from
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

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

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

   from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0
   minus(z, z') -{ 1 }-> minus(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   minus(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   quot(z, z') -{ 1 }-> 0 :|: z' - 1 >= 0, z = 0
   quot(z, z') -{ 2 }-> 1 + quot(minus(z - 2, z' - 2), 1 + (1 + (z' - 2))) :|: z' - 2 >= 0, z - 2 >= 0
   quot(z, z') -{ 2 }-> 1 + quot(0, 1 + 0) :|: z - 1 >= 0, z' = 1 + 0
   quot(z, z') -{ 1 }-> 1 + quot(0, 1 + (z' - 1)) :|: z' - 1 >= 0, z - 1 >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 + z }-> s :|: s >= 0, s <= XS, z' = 1 + X + XS, X >= 0, XS >= 0, z - 1 >= 0
   zWquot(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z = 0, z' >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0

Function symbols to be analyzed: {from}, {minus}, {quot}, {zWquot}
Previous analysis results are:
  sel: runtime: O(n^1) [1 + z], size: O(n^1) [z']
  from: runtime: INF, size: O(1) [0]

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

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

   sel(v0, v1) -> null_sel [0]
   minus(v0, v1) -> null_minus [0]
   quot(v0, v1) -> null_quot [0]

And the following fresh constants:    null_sel, null_minus, null_quot

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

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

   from(X) -> cons(X, from(s(X))) [1]
   sel(0, cons(X, XS)) -> X [1]
   sel(s(N), cons(X, XS)) -> sel(N, XS) [1]
   minus(X, 0) -> 0 [1]
   minus(s(X), s(Y)) -> minus(X, Y) [1]
   quot(0, s(Y)) -> 0 [1]
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))) [1]
   zWquot(XS, nil) -> nil [1]
   zWquot(nil, XS) -> nil [1]
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS)) [1]
   sel(v0, v1) -> null_sel [0]
   minus(v0, v1) -> null_minus [0]
   quot(v0, v1) -> null_quot [0]

The TRS has the following type information:
from :: s:0:null_sel:null_minus:null_quot -> cons:nil
cons :: s:0:null_sel:null_minus:null_quot -> cons:nil -> cons:nil
s :: s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot
sel :: s:0:null_sel:null_minus:null_quot -> cons:nil -> s:0:null_sel:null_minus:null_quot
0 :: s:0:null_sel:null_minus:null_quot
minus :: s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot
quot :: s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot -> s:0:null_sel:null_minus:null_quot
zWquot :: cons:nil -> cons:nil -> cons:nil
nil :: cons:nil
null_sel :: s:0:null_sel:null_minus:null_quot
null_minus :: s:0:null_sel:null_minus:null_quot
null_quot :: s:0:null_sel:null_minus:null_quot

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

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

   0 => 0
   nil => 0
   null_sel => 0
   null_minus => 0
   null_quot => 0

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

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

   from(z) -{ 1 }-> 1 + X + from(1 + X) :|: X >= 0, z = X
   minus(z, z') -{ 1 }-> minus(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
   minus(z, z') -{ 1 }-> 0 :|: X >= 0, z = X, z' = 0
   minus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   quot(z, z') -{ 1 }-> 0 :|: Y >= 0, z' = 1 + Y, z = 0
   quot(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   quot(z, z') -{ 1 }-> 1 + quot(minus(X, Y), 1 + Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
   sel(z, z') -{ 1 }-> X :|: z' = 1 + X + XS, X >= 0, z = 0, XS >= 0
   sel(z, z') -{ 1 }-> sel(N, XS) :|: z = 1 + N, z' = 1 + X + XS, X >= 0, XS >= 0, N >= 0
   sel(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   zWquot(z, z') -{ 1 }-> 0 :|: z = XS, XS >= 0, z' = 0
   zWquot(z, z') -{ 1 }-> 0 :|: z' = XS, z = 0, XS >= 0
   zWquot(z, z') -{ 1 }-> 1 + quot(X, Y) + zWquot(XS, YS) :|: z = 1 + X + XS, Y >= 0, X >= 0, YS >= 0, z' = 1 + Y + YS, XS >= 0

Only complete derivations are relevant for the runtime complexity.