YES
proof of AProVE_09_Inductive_qsortmiddle.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


Termination w.r.t. Q of the given QTRS could be proven:

(0) QTRS
(1) Overlay + Local Confluence [EQUIVALENT, 0 ms]
(2) QTRS
(3) DependencyPairsProof [EQUIVALENT, 0 ms]
(4) QDP
(5) DependencyGraphProof [EQUIVALENT, 0 ms]
(6) AND
    (7) QDP
        (8) UsableRulesProof [EQUIVALENT, 0 ms]
        (9) QDP
        (10) QReductionProof [EQUIVALENT, 0 ms]
        (11) QDP
        (12) QDPSizeChangeProof [EQUIVALENT, 1 ms]
        (13) YES
    (14) QDP
        (15) UsableRulesProof [EQUIVALENT, 0 ms]
        (16) QDP
        (17) QReductionProof [EQUIVALENT, 0 ms]
        (18) QDP
        (19) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (20) YES
    (21) QDP
        (22) UsableRulesProof [EQUIVALENT, 0 ms]
        (23) QDP
        (24) QReductionProof [EQUIVALENT, 0 ms]
        (25) QDP
        (26) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (27) YES
    (28) QDP
        (29) UsableRulesProof [EQUIVALENT, 0 ms]
        (30) QDP
        (31) QReductionProof [EQUIVALENT, 0 ms]
        (32) QDP
        (33) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (34) YES
    (35) QDP
        (36) UsableRulesProof [EQUIVALENT, 0 ms]
        (37) QDP
        (38) QReductionProof [EQUIVALENT, 0 ms]
        (39) QDP
        (40) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (41) YES
    (42) QDP
        (43) UsableRulesProof [EQUIVALENT, 0 ms]
        (44) QDP
        (45) QReductionProof [EQUIVALENT, 0 ms]
        (46) QDP
        (47) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (48) YES
    (49) QDP
        (50) UsableRulesProof [EQUIVALENT, 0 ms]
        (51) QDP
        (52) QReductionProof [EQUIVALENT, 0 ms]
        (53) QDP
        (54) QDPSizeChangeProof [EQUIVALENT, 0 ms]
        (55) YES
    (56) QDP
        (57) UsableRulesProof [EQUIVALENT, 0 ms]
        (58) QDP
        (59) QReductionProof [EQUIVALENT, 2 ms]
        (60) QDP
        (61) TransformationProof [EQUIVALENT, 0 ms]
        (62) QDP
        (63) TransformationProof [EQUIVALENT, 0 ms]
        (64) QDP
        (65) TransformationProof [EQUIVALENT, 0 ms]
        (66) QDP
        (67) TransformationProof [EQUIVALENT, 0 ms]
        (68) QDP
        (69) TransformationProof [EQUIVALENT, 0 ms]
        (70) QDP
        (71) TransformationProof [EQUIVALENT, 0 ms]
        (72) QDP
        (73) TransformationProof [EQUIVALENT, 0 ms]
        (74) QDP
        (75) TransformationProof [EQUIVALENT, 0 ms]
        (76) QDP
        (77) TransformationProof [EQUIVALENT, 0 ms]
        (78) QDP
        (79) TransformationProof [EQUIVALENT, 0 ms]
        (80) QDP
        (81) TransformationProof [EQUIVALENT, 0 ms]
        (82) QDP
        (83) TransformationProof [EQUIVALENT, 0 ms]
        (84) QDP
        (85) TransformationProof [EQUIVALENT, 0 ms]
        (86) QDP
        (87) TransformationProof [EQUIVALENT, 0 ms]
        (88) QDP
        (89) TransformationProof [EQUIVALENT, 0 ms]
        (90) QDP
        (91) TransformationProof [EQUIVALENT, 0 ms]
        (92) QDP
        (93) TransformationProof [EQUIVALENT, 0 ms]
        (94) QDP
        (95) TransformationProof [EQUIVALENT, 0 ms]
        (96) QDP
        (97) TransformationProof [EQUIVALENT, 0 ms]
        (98) QDP
        (99) TransformationProof [EQUIVALENT, 0 ms]
        (100) QDP
        (101) TransformationProof [EQUIVALENT, 0 ms]
        (102) QDP
        (103) QDPQMonotonicMRRProof [EQUIVALENT, 53 ms]
        (104) QDP
        (105) QDPQMonotonicMRRProof [EQUIVALENT, 16 ms]
        (106) QDP
        (107) QDPQMonotonicMRRProof [EQUIVALENT, 31 ms]
        (108) QDP
        (109) QDPOrderProof [EQUIVALENT, 27 ms]
        (110) QDP
        (111) UsableRulesProof [EQUIVALENT, 0 ms]
        (112) QDP
        (113) QReductionProof [EQUIVALENT, 0 ms]
        (114) QDP
        (115) Induction-Processor [SOUND, 1 ms]
        (116) AND
            (117) QDP
                (118) Induction-Processor [SOUND, 3 ms]
                (119) AND
                    (120) QDP
                        (121) UsableRulesProof [EQUIVALENT, 0 ms]
                        (122) QDP
                        (123) QReductionProof [EQUIVALENT, 0 ms]
                        (124) QDP
                        (125) Induction-Processor [SOUND, 0 ms]
                        (126) AND
                            (127) QDP
                                (128) UsableRulesProof [EQUIVALENT, 0 ms]
                                (129) QDP
                                (130) QReductionProof [EQUIVALENT, 0 ms]
                                (131) QDP
                                (132) Induction-Processor [SOUND, 4 ms]
                                (133) AND
                                    (134) QDP
                                        (135) PisEmptyProof [EQUIVALENT, 0 ms]
                                        (136) YES
                                    (137) QTRS
                                        (138) QTRSRRRProof [EQUIVALENT, 56 ms]
                                        (139) QTRS
                                        (140) QTRSRRRProof [EQUIVALENT, 0 ms]
                                        (141) QTRS
                                        (142) RisEmptyProof [EQUIVALENT, 0 ms]
                                        (143) YES
                            (144) QTRS
                                (145) QTRSRRRProof [EQUIVALENT, 27 ms]
                                (146) QTRS
                                (147) QTRSRRRProof [EQUIVALENT, 0 ms]
                                (148) QTRS
                                (149) RisEmptyProof [EQUIVALENT, 0 ms]
                                (150) YES
                    (151) QTRS
                        (152) QTRSRRRProof [EQUIVALENT, 42 ms]
                        (153) QTRS
                        (154) QTRSRRRProof [EQUIVALENT, 0 ms]
                        (155) QTRS
                        (156) RisEmptyProof [EQUIVALENT, 0 ms]
                        (157) YES
            (158) QTRS
                (159) QTRSRRRProof [EQUIVALENT, 0 ms]
                (160) QTRS
                (161) QTRSRRRProof [EQUIVALENT, 0 ms]
                (162) QTRS
                (163) RisEmptyProof [EQUIVALENT, 0 ms]
                (164) YES


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

(0)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

Q is empty.

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

(1) Overlay + Local Confluence (EQUIVALENT)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
----------------------------------------

(2)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(3) DependencyPairsProof (EQUIVALENT)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
----------------------------------------

(4)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QSORT(xs) -> QS(half(length(xs)), xs)
   QSORT(xs) -> HALF(length(xs))
   QSORT(xs) -> LENGTH(xs)
   QS(n, cons(x, xs)) -> APPEND(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   QS(n, cons(x, xs)) -> QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
   QS(n, cons(x, xs)) -> HALF(n)
   QS(n, cons(x, xs)) -> FILTERLOW(get(n, cons(x, xs)), cons(x, xs))
   QS(n, cons(x, xs)) -> GET(n, cons(x, xs))
   QS(n, cons(x, xs)) -> QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
   QS(n, cons(x, xs)) -> FILTERHIGH(get(n, cons(x, xs)), cons(x, xs))
   FILTERLOW(n, cons(x, xs)) -> IF1(ge(n, x), n, x, xs)
   FILTERLOW(n, cons(x, xs)) -> GE(n, x)
   IF1(true, n, x, xs) -> FILTERLOW(n, xs)
   IF1(false, n, x, xs) -> FILTERLOW(n, xs)
   FILTERHIGH(n, cons(x, xs)) -> IF2(ge(x, n), n, x, xs)
   FILTERHIGH(n, cons(x, xs)) -> GE(x, n)
   IF2(true, n, x, xs) -> FILTERHIGH(n, xs)
   IF2(false, n, x, xs) -> FILTERHIGH(n, xs)
   GE(s(x), s(y)) -> GE(x, y)
   APPEND(cons(x, xs), ys) -> APPEND(xs, ys)
   LENGTH(cons(x, xs)) -> LENGTH(xs)
   HALF(s(s(x))) -> HALF(x)
   GET(s(n), cons(x, cons(y, xs))) -> GET(n, cons(y, xs))

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(5) DependencyGraphProof (EQUIVALENT)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 8 SCCs with 10 less nodes.
----------------------------------------

(6)
Complex Obligation (AND)

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

(7)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   GET(s(n), cons(x, cons(y, xs))) -> GET(n, cons(y, xs))

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(8) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(9)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   GET(s(n), cons(x, cons(y, xs))) -> GET(n, cons(y, xs))

R is empty.
The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(10) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(11)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   GET(s(n), cons(x, cons(y, xs))) -> GET(n, cons(y, xs))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(12) QDPSizeChangeProof (EQUIVALENT)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem. 

From the DPs we obtained the following set of size-change graphs:
*GET(s(n), cons(x, cons(y, xs))) -> GET(n, cons(y, xs))
The graph contains the following edges 1 > 1, 2 > 2


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

(13)
YES

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

(14)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   HALF(s(s(x))) -> HALF(x)

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(15) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(16)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   HALF(s(s(x))) -> HALF(x)

R is empty.
The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(17) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(18)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   HALF(s(s(x))) -> HALF(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(19) QDPSizeChangeProof (EQUIVALENT)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem. 

From the DPs we obtained the following set of size-change graphs:
*HALF(s(s(x))) -> HALF(x)
The graph contains the following edges 1 > 1


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

(20)
YES

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

(21)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   LENGTH(cons(x, xs)) -> LENGTH(xs)

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(22) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(23)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   LENGTH(cons(x, xs)) -> LENGTH(xs)

R is empty.
The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(24) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(25)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   LENGTH(cons(x, xs)) -> LENGTH(xs)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(26) QDPSizeChangeProof (EQUIVALENT)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem. 

From the DPs we obtained the following set of size-change graphs:
*LENGTH(cons(x, xs)) -> LENGTH(xs)
The graph contains the following edges 1 > 1


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

(27)
YES

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

(28)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   APPEND(cons(x, xs), ys) -> APPEND(xs, ys)

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(29) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(30)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   APPEND(cons(x, xs), ys) -> APPEND(xs, ys)

R is empty.
The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(31) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(32)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   APPEND(cons(x, xs), ys) -> APPEND(xs, ys)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(33) QDPSizeChangeProof (EQUIVALENT)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem. 

From the DPs we obtained the following set of size-change graphs:
*APPEND(cons(x, xs), ys) -> APPEND(xs, ys)
The graph contains the following edges 1 > 1, 2 >= 2


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

(34)
YES

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

(35)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   GE(s(x), s(y)) -> GE(x, y)

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(36) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(37)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   GE(s(x), s(y)) -> GE(x, y)

R is empty.
The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(38) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(39)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   GE(s(x), s(y)) -> GE(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(40) QDPSizeChangeProof (EQUIVALENT)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem. 

From the DPs we obtained the following set of size-change graphs:
*GE(s(x), s(y)) -> GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2


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

(41)
YES

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

(42)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   IF2(true, n, x, xs) -> FILTERHIGH(n, xs)
   FILTERHIGH(n, cons(x, xs)) -> IF2(ge(x, n), n, x, xs)
   IF2(false, n, x, xs) -> FILTERHIGH(n, xs)

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(43) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(44)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   IF2(true, n, x, xs) -> FILTERHIGH(n, xs)
   FILTERHIGH(n, cons(x, xs)) -> IF2(ge(x, n), n, x, xs)
   IF2(false, n, x, xs) -> FILTERHIGH(n, xs)

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(45) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(46)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   IF2(true, n, x, xs) -> FILTERHIGH(n, xs)
   FILTERHIGH(n, cons(x, xs)) -> IF2(ge(x, n), n, x, xs)
   IF2(false, n, x, xs) -> FILTERHIGH(n, xs)

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)

The set Q consists of the following terms:

   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(47) QDPSizeChangeProof (EQUIVALENT)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem. 

From the DPs we obtained the following set of size-change graphs:
*FILTERHIGH(n, cons(x, xs)) -> IF2(ge(x, n), n, x, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4


*IF2(true, n, x, xs) -> FILTERHIGH(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2


*IF2(false, n, x, xs) -> FILTERHIGH(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2


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

(48)
YES

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

(49)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   IF1(true, n, x, xs) -> FILTERLOW(n, xs)
   FILTERLOW(n, cons(x, xs)) -> IF1(ge(n, x), n, x, xs)
   IF1(false, n, x, xs) -> FILTERLOW(n, xs)

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(50) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(51)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   IF1(true, n, x, xs) -> FILTERLOW(n, xs)
   FILTERLOW(n, cons(x, xs)) -> IF1(ge(n, x), n, x, xs)
   IF1(false, n, x, xs) -> FILTERLOW(n, xs)

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(52) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(53)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   IF1(true, n, x, xs) -> FILTERLOW(n, xs)
   FILTERLOW(n, cons(x, xs)) -> IF1(ge(n, x), n, x, xs)
   IF1(false, n, x, xs) -> FILTERLOW(n, xs)

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)

The set Q consists of the following terms:

   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(54) QDPSizeChangeProof (EQUIVALENT)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem. 

From the DPs we obtained the following set of size-change graphs:
*FILTERLOW(n, cons(x, xs)) -> IF1(ge(n, x), n, x, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4


*IF1(true, n, x, xs) -> FILTERLOW(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2


*IF1(false, n, x, xs) -> FILTERLOW(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2


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

(55)
YES

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

(56)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
   QS(n, cons(x, xs)) -> QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

   qsort(xs) -> qs(half(length(xs)), xs)
   qs(n, nil) -> nil
   qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
   filterlow(n, nil) -> nil
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterhigh(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   append(nil, ys) -> ys
   append(cons(x, xs), ys) -> cons(x, append(xs, ys))
   length(nil) -> 0
   length(cons(x, xs)) -> s(length(xs))
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, nil) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(57) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(58)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
   QS(n, cons(x, xs)) -> QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(59) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   qsort(x0)
   qs(x0, nil)
   qs(x0, cons(x1, x2))
   append(nil, ys)
   append(cons(x0, x1), ys)
   length(nil)
   length(cons(x0, x1))


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

(60)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
   QS(n, cons(x, xs)) -> QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(61) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(n, cons(x, xs)) -> QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))) at position [1] we obtained the following new rules [LPAR04]:

   (QS(n, cons(x, xs)) -> QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs)),QS(n, cons(x, xs)) -> QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs)))


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

(62)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
   QS(n, cons(x, xs)) -> QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(63) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(n, cons(x, xs)) -> QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))) at position [1] we obtained the following new rules [LPAR04]:

   (QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs)),QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs)))


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

(64)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs))
   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(65) TransformationProof (EQUIVALENT)
By narrowing [LPAR04] the rule QS(n, cons(x, xs)) -> QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs)) at position [1] we obtained the following new rules [LPAR04]:

   (QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil)),QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil)))
   (QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))))
   (QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3))),QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3))))
   (QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil)),QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil)))
   (QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2))))
   (QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3))),QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3))))


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

(66)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(67) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil)) at position [1,1] we obtained the following new rules [LPAR04]:

   (QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil)),QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil)))


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

(68)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(69) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))) at position [0] we obtained the following new rules [LPAR04]:

   (QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))))


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

(70)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(71) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3))) at position [1,1] we obtained the following new rules [LPAR04]:

   (QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3))),QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3))))


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

(72)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(73) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil)) at position [1,0,1] we obtained the following new rules [LPAR04]:

   (QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil)),QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil)))


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

(74)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(75) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2))) at position [0] we obtained the following new rules [LPAR04]:

   (QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2))))


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

(76)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(77) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3))) at position [1,0,1] we obtained the following new rules [LPAR04]:

   (QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3))),QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3))))


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

(78)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(79) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))) at position [1,1] we obtained the following new rules [LPAR04]:

   (QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2))))


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

(80)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(81) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2))) at position [1,0,1] we obtained the following new rules [LPAR04]:

   (QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2))))


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

(82)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(83) TransformationProof (EQUIVALENT)
By narrowing [LPAR04] the rule QS(n, cons(x, xs)) -> QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs)) at position [1] we obtained the following new rules [LPAR04]:

   (QS(y0, cons(0, y2)) -> QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2)),QS(y0, cons(0, y2)) -> QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2)))
   (QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil)),QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil)))
   (QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))))
   (QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3))),QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3))))
   (QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil)),QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil)))
   (QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2))))
   (QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))),QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))))


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

(84)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(y0, cons(0, y2)) -> QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(85) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(y0, cons(0, y2)) -> QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2)) at position [1] we obtained the following new rules [LPAR04]:

   (QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2)),QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2)))


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

(86)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(87) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil)) at position [1,1] we obtained the following new rules [LPAR04]:

   (QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil)),QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil)))


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

(88)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(89) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))) at position [0] we obtained the following new rules [LPAR04]:

   (QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))))


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

(90)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(91) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3))) at position [1,1] we obtained the following new rules [LPAR04]:

   (QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))),QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))))


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

(92)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(93) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil)) at position [1,0,0] we obtained the following new rules [LPAR04]:

   (QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil)),QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil)))


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

(94)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(95) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(0, cons(x0, cons(x1, x2))) -> QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2))) at position [0] we obtained the following new rules [LPAR04]:

   (QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2))))


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

(96)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(97) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))) at position [1,0,0] we obtained the following new rules [LPAR04]:

   (QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))),QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))))


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

(98)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(99) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))) at position [1,1] we obtained the following new rules [LPAR04]:

   (QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2))))


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

(100)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(101) TransformationProof (EQUIVALENT)
By rewriting [LPAR04] the rule QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2))) at position [1,0,0] we obtained the following new rules [LPAR04]:

   (QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2))),QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2))))


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

(102)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(103) QDPQMonotonicMRRProof (EQUIVALENT)
By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.


Strictly oriented rules of the TRS R:

   half(s(0)) -> 0

Used ordering: Polynomial interpretation [POLO]:

   POL(0) = 2
   POL(QS(x_1, x_2)) = 2*x_1
   POL(cons(x_1, x_2)) = x_1 + 2*x_2
   POL(false) = 0
   POL(filterhigh(x_1, x_2)) = x_2
   POL(filterlow(x_1, x_2)) = x_2
   POL(ge(x_1, x_2)) = x_1 + x_2
   POL(get(x_1, x_2)) = x_2
   POL(half(x_1)) = x_1
   POL(if1(x_1, x_2, x_3, x_4)) = x_3 + 2*x_4
   POL(if2(x_1, x_2, x_3, x_4)) = x_3 + 2*x_4
   POL(nil) = 1
   POL(s(x_1)) = 2*x_1
   POL(true) = 0


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

(104)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   half(s(s(x))) -> s(half(x))
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(105) QDPQMonotonicMRRProof (EQUIVALENT)
By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.


Strictly oriented rules of the TRS R:

   half(s(s(x))) -> s(half(x))

Used ordering: Polynomial interpretation [POLO]:

   POL(0) = 1
   POL(QS(x_1, x_2)) = 2*x_1
   POL(cons(x_1, x_2)) = 1 + x_1 + 2*x_2
   POL(false) = 0
   POL(filterhigh(x_1, x_2)) = x_2
   POL(filterlow(x_1, x_2)) = x_2
   POL(ge(x_1, x_2)) = 0
   POL(get(x_1, x_2)) = x_2
   POL(half(x_1)) = x_1
   POL(if1(x_1, x_2, x_3, x_4)) = 1 + x_3 + 2*x_4
   POL(if2(x_1, x_2, x_3, x_4)) = 1 + 2*x_1 + x_3 + 2*x_4
   POL(nil) = 2
   POL(s(x_1)) = 1 + 2*x_1
   POL(true) = 0


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

(106)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(107) QDPQMonotonicMRRProof (EQUIVALENT)
By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented dependency pairs:

   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
   QS(s(x0), cons(x1, cons(x2, x3))) -> QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))


Used ordering: Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(QS(x_1, x_2)) = x_1
   POL(cons(x_1, x_2)) = x_1 + 2*x_2
   POL(false) = 0
   POL(filterhigh(x_1, x_2)) = x_2
   POL(filterlow(x_1, x_2)) = x_2
   POL(ge(x_1, x_2)) = 2
   POL(get(x_1, x_2)) = x_2
   POL(half(x_1)) = 0
   POL(if1(x_1, x_2, x_3, x_4)) = x_3 + 2*x_4
   POL(if2(x_1, x_2, x_3, x_4)) = x_3 + 2*x_4
   POL(nil) = 2
   POL(s(x_1)) = 1
   POL(true) = 0


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

(108)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(109) QDPOrderProof (EQUIVALENT)
We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.

   QS(y0, cons(0, y2)) -> QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
The remaining pairs can at least be oriented weakly.
Used ordering:  Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( QS_2(x_1, x_2) ) = 2x_1 + 2x_2 + 2
POL( half_1(x_1) ) = x_1
POL( 0 ) = 1
POL( if1_4(x_1, ..., x_4) ) = x_1 + x_3 + 2x_4 + 1
POL( if2_4(x_1, ..., x_4) ) = x_3 + 2x_4 + 1
POL( ge_2(x_1, x_2) ) = 0
POL( true ) = 0
POL( s_1(x_1) ) = 2
POL( filterhigh_2(x_1, x_2) ) = x_2
POL( cons_2(x_1, x_2) ) = x_1 + 2x_2 + 1
POL( false ) = 0
POL( filterlow_2(x_1, x_2) ) = x_2
POL( get_2(x_1, x_2) ) = max{0, -2}
POL( nil ) = 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

   half(0) -> 0
   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   if1(true, n, x, xs) -> filterlow(n, xs)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   filterlow(n, nil) -> nil
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   ge(0, s(x)) -> false
   filterhigh(n, nil) -> nil


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

(110)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   half(0) -> 0
   get(n, cons(x, nil)) -> x
   get(0, cons(x, cons(y, xs))) -> x
   get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   ge(x, 0) -> true
   ge(0, s(x)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(true, n, x, xs) -> filterhigh(n, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(111) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(112)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   if1(true, n, x, xs) -> filterlow(n, xs)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false
   half(0) -> 0
   if2(true, n, x, xs) -> filterhigh(n, xs)
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))
   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(113) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   get(x0, nil)
   get(x0, cons(x1, nil))
   get(0, cons(x0, cons(x1, x2)))
   get(s(x0), cons(x1, cons(x2, x3)))


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

(114)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   if1(true, n, x, xs) -> filterlow(n, xs)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false
   half(0) -> 0
   if2(true, n, x, xs) -> filterhigh(n, xs)
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(115) Induction-Processor (SOUND)

This DP could be deleted by the Induction-Processor:
QS(x0, cons(x1, nil)) -> QS(half(x0), if2(ge(x1, x1), x1, x1, nil))


This order was computed:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(QS(x_1, x_2)) = x_2
   POL(cons(x_1, x_2)) = 1 + x_2
   POL(false_renamed) = 1
   POL(filterhigh(x_1, x_2)) = x_2
   POL(filterlow(x_1, x_2)) = x_2
   POL(ge(x_1, x_2)) = 1
   POL(half(x_1)) = 1
   POL(if1(x_1, x_2, x_3, x_4)) = x_1 + x_4
   POL(if2(x_1, x_2, x_3, x_4)) = x_1 + x_4
   POL(nil) = 0
   POL(s(x_1)) = 1 + x_1
   POL(true_renamed) = 1

At least one of these decreasing rules is always used after the deleted DP:
if2(true_renamed, n2, x6, xs1) -> filterhigh(n2, xs1)


The following formula is valid:
x1:sort[a0].if2'(ge(x1, x1), x1, x1, nil)=true


The transformed set:
if2'(true_renamed, n2, x6, xs1) -> true
filterhigh'(n3, cons(x7, xs2)) -> if2'(ge(x7, n3), n3, x7, xs2)
if2'(false_renamed, n4, x8, xs3) -> filterhigh'(n4, xs3)
filterhigh'(n5, nil) -> false
ge(x, 0) -> true_renamed
ge(s(x'), s(y)) -> ge(x', y)
if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) -> nil
ge(0, s(x5)) -> false_renamed
half(0) -> 0
if2(true_renamed, n2, x6, xs1) -> filterhigh(n2, xs1)
filterhigh(n3, cons(x7, xs2)) -> if2(ge(x7, n3), n3, x7, xs2)
if2(false_renamed, n4, x8, xs3) -> cons(x8, filterhigh(n4, xs3))
filterhigh(n5, nil) -> nil
half(s(v14)) -> 0
equal_bool(true, false) -> false
equal_bool(false, true) -> false
equal_bool(true, true) -> true
equal_bool(false, false) -> true
and(true, x) -> x
and(false, x) -> false
or(true, x) -> true
or(false, x) -> x
not(false) -> true
not(true) -> false
isa_true(true) -> true
isa_true(false) -> false
isa_false(true) -> false
isa_false(false) -> true
equal_sort[a0](0, 0) -> true
equal_sort[a0](0, s(v23)) -> false
equal_sort[a0](s(v24), 0) -> false
equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
equal_sort[a5](cons(v26, v27), nil) -> false
equal_sort[a5](nil, cons(v30, v31)) -> false
equal_sort[a5](nil, nil) -> true
equal_sort[a36](true_renamed, true_renamed) -> true
equal_sort[a36](true_renamed, false_renamed) -> false
equal_sort[a36](false_renamed, true_renamed) -> false
equal_sort[a36](false_renamed, false_renamed) -> true
equal_sort[a66](witness_sort[a66], witness_sort[a66]) -> true


The proof given by the theorem prover:
The following output was given by the internal theorem prover:proof of internal
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


Partial correctness of the following Program

   [x, v23, v24, v25, v26, v27, v28, v29, v30, v31, n2, x6, xs1, n4, x8, x7, xs2, n5, n3, x', y, x5, n1, n', x3, xs', v14, n, x'', n'', x4]
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   true and x -> x
   false and x -> false
   true or x -> true
   false or x -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v23)) -> false
   equal_sort[a0](s(v24), 0) -> false
   equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
   equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> equal_sort[a0](v26, v28) and equal_sort[a5](v27, v29)
   equal_sort[a5](cons(v26, v27), nil) -> false
   equal_sort[a5](nil, cons(v30, v31)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a36](true_renamed, true_renamed) -> true
   equal_sort[a36](true_renamed, false_renamed) -> false
   equal_sort[a36](false_renamed, true_renamed) -> false
   equal_sort[a36](false_renamed, false_renamed) -> true
   equal_sort[a66](witness_sort[a66], witness_sort[a66]) -> true
   if2'(true_renamed, n2, x6, xs1) -> true
   if2'(false_renamed, n4, x8, cons(x7, xs2)) -> if2'(ge(x7, n4), n4, x7, xs2)
   if2'(false_renamed, n4, x8, nil) -> false
   filterhigh'(n5, nil) -> false
   equal_sort[a36](ge(x7, n3), true_renamed) -> true | filterhigh'(n3, cons(x7, xs2)) -> true
   equal_sort[a36](ge(x7, n3), true_renamed) -> false | filterhigh'(n3, cons(x7, xs2)) -> filterhigh'(n3, xs2)
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   ge(0, s(x5)) -> false_renamed
   filterlow(n1, nil) -> nil
   equal_sort[a36](ge(n', x3), true_renamed) -> true | filterlow(n', cons(x3, xs')) -> filterlow(n', xs')
   equal_sort[a36](ge(n', x3), true_renamed) -> false | filterlow(n', cons(x3, xs')) -> cons(x3, filterlow(n', xs'))
   half(0) -> 0
   half(s(v14)) -> 0
   filterhigh(n5, nil) -> nil
   equal_sort[a36](ge(x7, n3), true_renamed) -> true | filterhigh(n3, cons(x7, xs2)) -> filterhigh(n3, xs2)
   equal_sort[a36](ge(x7, n3), true_renamed) -> false | filterhigh(n3, cons(x7, xs2)) -> cons(x7, filterhigh(n3, xs2))
   if1(true_renamed, n, x'', cons(x3, xs')) -> if1(ge(n, x3), n, x3, xs')
   if1(true_renamed, n, x'', nil) -> nil
   if1(false_renamed, n'', x4, cons(x3, xs')) -> cons(x4, if1(ge(n'', x3), n'', x3, xs'))
   if1(false_renamed, n'', x4, nil) -> cons(x4, nil)
   if2(true_renamed, n2, x6, cons(x7, xs2)) -> if2(ge(x7, n2), n2, x7, xs2)
   if2(true_renamed, n2, x6, nil) -> nil
   if2(false_renamed, n4, x8, cons(x7, xs2)) -> cons(x8, if2(ge(x7, n4), n4, x7, xs2))
   if2(false_renamed, n4, x8, nil) -> cons(x8, nil)

using the following formula:
x1:sort[a0].if2'(ge(x1, x1), x1, x1, nil)=true

could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT, 0 ms]
(2) AND
    (3) Formula
        (4) Symbolic evaluation [EQUIVALENT, 0 ms]
        (5) YES
    (6) Formula
        (7) Symbolic evaluation [EQUIVALENT, 0 ms]
        (8) Formula
        (9) Hypothesis Lifting [EQUIVALENT, 0 ms]
        (10) Formula
        (11) Inverse Substitution [SOUND, 0 ms]
        (12) Formula
        (13) Inverse Substitution [SOUND, 0 ms]
        (14) Formula
        (15) Induction by data structure [EQUIVALENT, 0 ms]
        (16) AND
            (17) Formula
                (18) Symbolic evaluation [EQUIVALENT, 0 ms]
                (19) YES
            (20) Formula
                (21) Symbolic evaluation [EQUIVALENT, 0 ms]
                (22) YES


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

(0)
Obligation:
Formula:
x1:sort[a0].if2'(ge(x1, x1), x1, x1, nil)=true

There are no hypotheses.




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

(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
if2'(ge(0, 0), 0, 0, nil)=true

There are no hypotheses.





1. Step Case:
Formula:
n:sort[a0].if2'(ge(s(n), s(n)), s(n), s(n), nil)=true

Hypotheses:
n:sort[a0].if2'(ge(n, n), n, n, nil)=true






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

(2)
Complex Obligation (AND)

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

(3)
Obligation:
Formula:
if2'(ge(0, 0), 0, 0, nil)=true

There are no hypotheses.




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

(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(5)
YES

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

(6)
Obligation:
Formula:
n:sort[a0].if2'(ge(s(n), s(n)), s(n), s(n), nil)=true

Hypotheses:
n:sort[a0].if2'(ge(n, n), n, n, nil)=true




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

(7) Symbolic evaluation (EQUIVALENT)
Could be shown by simple symbolic evaluation.
----------------------------------------

(8)
Obligation:
Formula:
n:sort[a0].if2'(ge(n, n), s(n), s(n), nil)=true

Hypotheses:
n:sort[a0].if2'(ge(n, n), n, n, nil)=true




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

(9) Hypothesis Lifting (EQUIVALENT)
Formula could be generalised by hypothesis lifting to the following new obligation:
Formula:
n:sort[a0].(if2'(ge(n, n), n, n, nil)=true->if2'(ge(n, n), s(n), s(n), nil)=true)

There are no hypotheses.




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

(10)
Obligation:
Formula:
n:sort[a0].(if2'(ge(n, n), n, n, nil)=true->if2'(ge(n, n), s(n), s(n), nil)=true)

There are no hypotheses.




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

(11) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n':sort[a36],n:sort[a0].(if2'(n', n, n, nil)=true->if2'(n', s(n), s(n), nil)=true)

Inverse substitution used:
[ge(n, n)/n']


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

(12)
Obligation:
Formula:
n':sort[a36],n:sort[a0].(if2'(n', n, n, nil)=true->if2'(n', s(n), s(n), nil)=true)

There are no hypotheses.




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

(13) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n':sort[a36],n:sort[a0],n'':sort[a0].(if2'(n', n, n, nil)=true->if2'(n', n'', n'', nil)=true)

Inverse substitution used:
[s(n)/n'']


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

(14)
Obligation:
Formula:
n':sort[a36],n:sort[a0],n'':sort[a0].(if2'(n', n, n, nil)=true->if2'(n', n'', n'', nil)=true)

There are no hypotheses.




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

(15) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a36] generates the following cases:



1. Base Case:
Formula:
n:sort[a0],n'':sort[a0].(if2'(true_renamed, n, n, nil)=true->if2'(true_renamed, n'', n'', nil)=true)

There are no hypotheses.





1. Base Case:
Formula:
n:sort[a0],n'':sort[a0].(if2'(false_renamed, n, n, nil)=true->if2'(false_renamed, n'', n'', nil)=true)

There are no hypotheses.






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

(16)
Complex Obligation (AND)

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

(17)
Obligation:
Formula:
n:sort[a0],n'':sort[a0].(if2'(true_renamed, n, n, nil)=true->if2'(true_renamed, n'', n'', nil)=true)

There are no hypotheses.




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

(18) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(19)
YES

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

(20)
Obligation:
Formula:
n:sort[a0],n'':sort[a0].(if2'(false_renamed, n, n, nil)=true->if2'(false_renamed, n'', n'', nil)=true)

There are no hypotheses.




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

(21) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(22)
YES

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

(116)
Complex Obligation (AND)

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

(117)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   if1(true, n, x, xs) -> filterlow(n, xs)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false
   half(0) -> 0
   if2(true, n, x, xs) -> filterhigh(n, xs)
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(118) Induction-Processor (SOUND)

This DP could be deleted by the Induction-Processor:
QS(0, cons(x0, cons(x1, x2))) -> QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))


This order was computed:
Polynomial interpretation [POLO]:

   POL(0) = 1
   POL(QS(x_1, x_2)) = x_2
   POL(cons(x_1, x_2)) = 1 + x_2
   POL(false_renamed) = 1
   POL(filterhigh(x_1, x_2)) = x_2
   POL(filterlow(x_1, x_2)) = x_2
   POL(ge(x_1, x_2)) = 1
   POL(half(x_1)) = 1
   POL(if1(x_1, x_2, x_3, x_4)) = 1 + x_4
   POL(if2(x_1, x_2, x_3, x_4)) = x_1 + x_4
   POL(nil) = 0
   POL(s(x_1)) = 1 + x_1
   POL(true_renamed) = 1

At least one of these decreasing rules is always used after the deleted DP:
if2(true_renamed, n2, x6, xs1) -> filterhigh(n2, xs1)


The following formula is valid:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(x0, x0), x0, x0, cons(x1, x2))=true


The transformed set:
if2'(true_renamed, n2, x6, xs1) -> true
filterhigh'(n3, cons(x7, xs2)) -> if2'(ge(x7, n3), n3, x7, xs2)
if2'(false_renamed, n4, x8, xs3) -> filterhigh'(n4, xs3)
filterhigh'(n5, nil) -> false
ge(x, 0) -> true_renamed
ge(s(x'), s(y)) -> ge(x', y)
if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) -> nil
ge(0, s(x5)) -> false_renamed
half(0) -> 0
if2(true_renamed, n2, x6, xs1) -> filterhigh(n2, xs1)
filterhigh(n3, cons(x7, xs2)) -> if2(ge(x7, n3), n3, x7, xs2)
if2(false_renamed, n4, x8, xs3) -> cons(x8, filterhigh(n4, xs3))
filterhigh(n5, nil) -> nil
half(s(v14)) -> 0
equal_bool(true, false) -> false
equal_bool(false, true) -> false
equal_bool(true, true) -> true
equal_bool(false, false) -> true
and(true, x) -> x
and(false, x) -> false
or(true, x) -> true
or(false, x) -> x
not(false) -> true
not(true) -> false
isa_true(true) -> true
isa_true(false) -> false
isa_false(true) -> false
isa_false(false) -> true
equal_sort[a0](0, 0) -> true
equal_sort[a0](0, s(v23)) -> false
equal_sort[a0](s(v24), 0) -> false
equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
equal_sort[a5](cons(v26, v27), nil) -> false
equal_sort[a5](nil, cons(v30, v31)) -> false
equal_sort[a5](nil, nil) -> true
equal_sort[a34](true_renamed, true_renamed) -> true
equal_sort[a34](true_renamed, false_renamed) -> false
equal_sort[a34](false_renamed, true_renamed) -> false
equal_sort[a34](false_renamed, false_renamed) -> true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) -> true


The proof given by the theorem prover:
The following output was given by the internal theorem prover:proof of internal
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


Partial correctness of the following Program

   [x, v23, v24, v25, v26, v27, v28, v29, v30, v31, n2, x6, xs1, n4, x8, x7, xs2, n5, n3, x', y, x5, n1, n', x3, xs', v14, n, x'', n'', x4]
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   true and x -> x
   false and x -> false
   true or x -> true
   false or x -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v23)) -> false
   equal_sort[a0](s(v24), 0) -> false
   equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
   equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> equal_sort[a0](v26, v28) and equal_sort[a5](v27, v29)
   equal_sort[a5](cons(v26, v27), nil) -> false
   equal_sort[a5](nil, cons(v30, v31)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a34](true_renamed, true_renamed) -> true
   equal_sort[a34](true_renamed, false_renamed) -> false
   equal_sort[a34](false_renamed, true_renamed) -> false
   equal_sort[a34](false_renamed, false_renamed) -> true
   equal_sort[a64](witness_sort[a64], witness_sort[a64]) -> true
   if2'(true_renamed, n2, x6, xs1) -> true
   if2'(false_renamed, n4, x8, cons(x7, xs2)) -> if2'(ge(x7, n4), n4, x7, xs2)
   if2'(false_renamed, n4, x8, nil) -> false
   filterhigh'(n5, nil) -> false
   equal_sort[a34](ge(x7, n3), true_renamed) -> true | filterhigh'(n3, cons(x7, xs2)) -> true
   equal_sort[a34](ge(x7, n3), true_renamed) -> false | filterhigh'(n3, cons(x7, xs2)) -> filterhigh'(n3, xs2)
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   ge(0, s(x5)) -> false_renamed
   filterlow(n1, nil) -> nil
   equal_sort[a34](ge(n', x3), true_renamed) -> true | filterlow(n', cons(x3, xs')) -> filterlow(n', xs')
   equal_sort[a34](ge(n', x3), true_renamed) -> false | filterlow(n', cons(x3, xs')) -> cons(x3, filterlow(n', xs'))
   half(0) -> 0
   half(s(v14)) -> 0
   filterhigh(n5, nil) -> nil
   equal_sort[a34](ge(x7, n3), true_renamed) -> true | filterhigh(n3, cons(x7, xs2)) -> filterhigh(n3, xs2)
   equal_sort[a34](ge(x7, n3), true_renamed) -> false | filterhigh(n3, cons(x7, xs2)) -> cons(x7, filterhigh(n3, xs2))
   if1(true_renamed, n, x'', cons(x3, xs')) -> if1(ge(n, x3), n, x3, xs')
   if1(true_renamed, n, x'', nil) -> nil
   if1(false_renamed, n'', x4, cons(x3, xs')) -> cons(x4, if1(ge(n'', x3), n'', x3, xs'))
   if1(false_renamed, n'', x4, nil) -> cons(x4, nil)
   if2(true_renamed, n2, x6, cons(x7, xs2)) -> if2(ge(x7, n2), n2, x7, xs2)
   if2(true_renamed, n2, x6, nil) -> nil
   if2(false_renamed, n4, x8, cons(x7, xs2)) -> cons(x8, if2(ge(x7, n4), n4, x7, xs2))
   if2(false_renamed, n4, x8, nil) -> cons(x8, nil)

using the following formula:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(x0, x0), x0, x0, cons(x1, x2))=true

could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT, 0 ms]
(2) AND
    (3) Formula
        (4) Symbolic evaluation [EQUIVALENT, 0 ms]
        (5) YES
    (6) Formula
        (7) Symbolic evaluation [EQUIVALENT, 0 ms]
        (8) Formula
        (9) Case Analysis [EQUIVALENT, 0 ms]
        (10) AND
            (11) Formula
                (12) Case Analysis [EQUIVALENT, 0 ms]
                (13) AND
                    (14) Formula
                        (15) Inverse Substitution [SOUND, 0 ms]
                        (16) Formula
                        (17) Induction by data structure [SOUND, 0 ms]
                        (18) AND
                            (19) Formula
                                (20) Symbolic evaluation [EQUIVALENT, 0 ms]
                                (21) YES
                            (22) Formula
                                (23) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
                                (24) YES
                    (25) Formula
                        (26) Inverse Substitution [SOUND, 0 ms]
                        (27) Formula
                        (28) Induction by data structure [SOUND, 0 ms]
                        (29) AND
                            (30) Formula
                                (31) Symbolic evaluation [EQUIVALENT, 0 ms]
                                (32) YES
                            (33) Formula
                                (34) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
                                (35) YES
            (36) Formula
                (37) Case Analysis [EQUIVALENT, 0 ms]
                (38) AND
                    (39) Formula
                        (40) Inverse Substitution [SOUND, 0 ms]
                        (41) Formula
                        (42) Induction by data structure [SOUND, 0 ms]
                        (43) AND
                            (44) Formula
                                (45) Symbolic evaluation [EQUIVALENT, 0 ms]
                                (46) YES
                            (47) Formula
                                (48) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
                                (49) YES
                    (50) Formula
                        (51) Inverse Substitution [SOUND, 0 ms]
                        (52) Formula
                        (53) Induction by data structure [SOUND, 0 ms]
                        (54) AND
                            (55) Formula
                                (56) Symbolic evaluation [EQUIVALENT, 0 ms]
                                (57) YES
                            (58) Formula
                                (59) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
                                (60) YES


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

(0)
Obligation:
Formula:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(x0, x0), x0, x0, cons(x1, x2))=true

There are no hypotheses.




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

(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
x1:sort[a0],x2:sort[a5].if2'(ge(0, 0), 0, 0, cons(x1, x2))=true

There are no hypotheses.





1. Step Case:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(s(n), s(n)), s(n), s(n), cons(x1, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true






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

(2)
Complex Obligation (AND)

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

(3)
Obligation:
Formula:
x1:sort[a0],x2:sort[a5].if2'(ge(0, 0), 0, 0, cons(x1, x2))=true

There are no hypotheses.




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

(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(5)
YES

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

(6)
Obligation:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(s(n), s(n)), s(n), s(n), cons(x1, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(7) Symbolic evaluation (EQUIVALENT)
Could be shown by simple symbolic evaluation.
----------------------------------------

(8)
Obligation:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(x1, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(9) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:

Formula:
n:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(0, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true





Formula:
n:sort[a0],x_1:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(s(x_1), x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true






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

(10)
Complex Obligation (AND)

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

(11)
Obligation:
Formula:
n:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(0, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(12) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:

Formula:
n:sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(0, cons(x_1, x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true





Formula:
n:sort[a0].if2'(ge(n, n), s(n), s(n), cons(0, nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true






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

(13)
Complex Obligation (AND)

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

(14)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(0, cons(x_1, x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(15) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(n, n), n', n', cons(0, cons(x_1, x_2)))=true

Inverse substitution used:
[s(n)/n']


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

(16)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(n, n), n', n', cons(0, cons(x_1, x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(17) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(0, 0), n', n', cons(0, cons(x_1, x_2)))=true

There are no hypotheses.





1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(s(n''), s(n'')), n', n', cons(0, cons(x_1, x_2)))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true






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

(18)
Complex Obligation (AND)

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

(19)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(0, 0), n', n', cons(0, cons(x_1, x_2)))=true

There are no hypotheses.




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

(20) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(21)
YES

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

(22)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(s(n''), s(n'')), n', n', cons(0, cons(x_1, x_2)))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true




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

(23) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:

n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true

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

(24)
YES

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

(25)
Obligation:
Formula:
n:sort[a0].if2'(ge(n, n), s(n), s(n), cons(0, nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(26) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0].if2'(ge(n, n), n', n', cons(0, nil))=true

Inverse substitution used:
[s(n)/n']


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

(27)
Obligation:
Formula:
n:sort[a0],n':sort[a0].if2'(ge(n, n), n', n', cons(0, nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(28) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
n':sort[a0].if2'(ge(0, 0), n', n', cons(0, nil))=true

There are no hypotheses.





1. Step Case:
Formula:
n'':sort[a0],n':sort[a0].if2'(ge(s(n''), s(n'')), n', n', cons(0, nil))=true

Hypotheses:
n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', cons(0, nil))=true






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

(29)
Complex Obligation (AND)

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

(30)
Obligation:
Formula:
n':sort[a0].if2'(ge(0, 0), n', n', cons(0, nil))=true

There are no hypotheses.




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

(31) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(32)
YES

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

(33)
Obligation:
Formula:
n'':sort[a0],n':sort[a0].if2'(ge(s(n''), s(n'')), n', n', cons(0, nil))=true

Hypotheses:
n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', cons(0, nil))=true




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

(34) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:

n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', cons(0, nil))=true

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

(35)
YES

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

(36)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(s(x_1), x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(37) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:

Formula:
n:sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true





Formula:
n:sort[a0],x_1:sort[a0].if2'(ge(n, n), s(n), s(n), cons(s(x_1), nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true






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

(38)
Complex Obligation (AND)

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

(39)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(40) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(n, n), n', n', cons(s(x_1), cons(x_1', x_2)))=true

Inverse substitution used:
[s(n)/n']


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

(41)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(n, n), n', n', cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(42) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(0, 0), n', n', cons(s(x_1), cons(x_1', x_2)))=true

There are no hypotheses.





1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(s(n''), s(n'')), n', n', cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true






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

(43)
Complex Obligation (AND)

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

(44)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(0, 0), n', n', cons(s(x_1), cons(x_1', x_2)))=true

There are no hypotheses.




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

(45) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(46)
YES

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

(47)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(s(n''), s(n'')), n', n', cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true




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

(48) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:

n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true

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

(49)
YES

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

(50)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0].if2'(ge(n, n), s(n), s(n), cons(s(x_1), nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(51) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0].if2'(ge(n, n), n', n', cons(s(x_1), nil))=true

Inverse substitution used:
[s(n)/n']


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

(52)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0].if2'(ge(n, n), n', n', cons(s(x_1), nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true




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

(53) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0].if2'(ge(0, 0), n', n', cons(s(x_1), nil))=true

There are no hypotheses.





1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0].if2'(ge(s(n''), s(n'')), n', n', cons(s(x_1), nil))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if2'(ge(n'', n''), n', n', cons(s(x_1), nil))=true






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

(54)
Complex Obligation (AND)

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

(55)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0].if2'(ge(0, 0), n', n', cons(s(x_1), nil))=true

There are no hypotheses.




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

(56) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(57)
YES

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

(58)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0].if2'(ge(s(n''), s(n'')), n', n', cons(s(x_1), nil))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if2'(ge(n'', n''), n', n', cons(s(x_1), nil))=true




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

(59) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:

n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if2'(ge(n'', n''), n', n', cons(s(x_1), nil))=true

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

(60)
YES

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

(119)
Complex Obligation (AND)

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

(120)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   if1(true, n, x, xs) -> filterlow(n, xs)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false
   half(0) -> 0
   if2(true, n, x, xs) -> filterhigh(n, xs)
   filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
   if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
   filterhigh(n, nil) -> nil

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(121) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(122)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false
   half(0) -> 0

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(123) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   filterhigh(x0, nil)
   filterhigh(x0, cons(x1, x2))
   if2(true, x0, x1, x2)
   if2(false, x0, x1, x2)


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

(124)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false
   half(0) -> 0

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(125) Induction-Processor (SOUND)

This DP could be deleted by the Induction-Processor:
QS(x0, cons(x1, nil)) -> QS(half(x0), if1(ge(x1, x1), x1, x1, nil))


This order was computed:
Polynomial interpretation [POLO]:

   POL(0) = 1
   POL(QS(x_1, x_2)) = x_2
   POL(cons(x_1, x_2)) = 1 + x_2
   POL(false_renamed) = 1
   POL(filterlow(x_1, x_2)) = x_2
   POL(ge(x_1, x_2)) = 1
   POL(half(x_1)) = 1
   POL(if1(x_1, x_2, x_3, x_4)) = x_1 + x_4
   POL(nil) = 0
   POL(s(x_1)) = 1 + x_1
   POL(true_renamed) = 1

At least one of these decreasing rules is always used after the deleted DP:
if1(true_renamed, n, x'', xs) -> filterlow(n, xs)


The following formula is valid:
x1:sort[a0].if1'(ge(x1, x1), x1, x1, nil)=true


The transformed set:
if1'(true_renamed, n, x'', xs) -> true
if1'(false_renamed, n', x3, xs') -> filterlow'(n', xs')
filterlow'(n'', nil) -> false
filterlow'(n1, cons(x5, xs'')) -> if1'(ge(n1, x5), n1, x5, xs'')
ge(x, 0) -> true_renamed
ge(s(x'), s(y)) -> ge(x', y)
if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
if1(false_renamed, n', x3, xs') -> cons(x3, filterlow(n', xs'))
filterlow(n'', nil) -> nil
ge(0, s(x4)) -> false_renamed
half(0) -> 0
filterlow(n1, cons(x5, xs'')) -> if1(ge(n1, x5), n1, x5, xs'')
half(s(v14)) -> 0
equal_bool(true, false) -> false
equal_bool(false, true) -> false
equal_bool(true, true) -> true
equal_bool(false, false) -> true
and(true, x) -> x
and(false, x) -> false
or(true, x) -> true
or(false, x) -> x
not(false) -> true
not(true) -> false
isa_true(true) -> true
isa_true(false) -> false
isa_false(true) -> false
isa_false(false) -> true
equal_sort[a0](0, 0) -> true
equal_sort[a0](0, s(v15)) -> false
equal_sort[a0](s(v16), 0) -> false
equal_sort[a0](s(v16), s(v17)) -> equal_sort[a0](v16, v17)
equal_sort[a5](cons(v18, v19), cons(v20, v21)) -> and(equal_sort[a0](v18, v20), equal_sort[a5](v19, v21))
equal_sort[a5](cons(v18, v19), nil) -> false
equal_sort[a5](nil, cons(v22, v23)) -> false
equal_sort[a5](nil, nil) -> true
equal_sort[a21](true_renamed, true_renamed) -> true
equal_sort[a21](true_renamed, false_renamed) -> false
equal_sort[a21](false_renamed, true_renamed) -> false
equal_sort[a21](false_renamed, false_renamed) -> true
equal_sort[a43](witness_sort[a43], witness_sort[a43]) -> true


The proof given by the theorem prover:
The following output was given by the internal theorem prover:proof of internal
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


Partial correctness of the following Program

   [x, v15, v16, v17, v18, v19, v20, v21, v22, v23, n, x'', xs, n', x3, x5, xs'', n'', n1, x', y, x4, v14]
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   true and x -> x
   false and x -> false
   true or x -> true
   false or x -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v15)) -> false
   equal_sort[a0](s(v16), 0) -> false
   equal_sort[a0](s(v16), s(v17)) -> equal_sort[a0](v16, v17)
   equal_sort[a5](cons(v18, v19), cons(v20, v21)) -> equal_sort[a0](v18, v20) and equal_sort[a5](v19, v21)
   equal_sort[a5](cons(v18, v19), nil) -> false
   equal_sort[a5](nil, cons(v22, v23)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a21](true_renamed, true_renamed) -> true
   equal_sort[a21](true_renamed, false_renamed) -> false
   equal_sort[a21](false_renamed, true_renamed) -> false
   equal_sort[a21](false_renamed, false_renamed) -> true
   equal_sort[a43](witness_sort[a43], witness_sort[a43]) -> true
   if1'(true_renamed, n, x'', xs) -> true
   if1'(false_renamed, n', x3, nil) -> false
   if1'(false_renamed, n', x3, cons(x5, xs'')) -> if1'(ge(n', x5), n', x5, xs'')
   filterlow'(n'', nil) -> false
   equal_sort[a21](ge(n1, x5), true_renamed) -> true | filterlow'(n1, cons(x5, xs'')) -> true
   equal_sort[a21](ge(n1, x5), true_renamed) -> false | filterlow'(n1, cons(x5, xs'')) -> filterlow'(n1, xs'')
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   ge(0, s(x4)) -> false_renamed
   filterlow(n'', nil) -> nil
   equal_sort[a21](ge(n1, x5), true_renamed) -> true | filterlow(n1, cons(x5, xs'')) -> filterlow(n1, xs'')
   equal_sort[a21](ge(n1, x5), true_renamed) -> false | filterlow(n1, cons(x5, xs'')) -> cons(x5, filterlow(n1, xs''))
   half(0) -> 0
   half(s(v14)) -> 0
   if1(true_renamed, n, x'', nil) -> nil
   if1(true_renamed, n, x'', cons(x5, xs'')) -> if1(ge(n, x5), n, x5, xs'')
   if1(false_renamed, n', x3, nil) -> cons(x3, nil)
   if1(false_renamed, n', x3, cons(x5, xs'')) -> cons(x3, if1(ge(n', x5), n', x5, xs''))

using the following formula:
x1:sort[a0].if1'(ge(x1, x1), x1, x1, nil)=true

could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT, 0 ms]
(2) AND
    (3) Formula
        (4) Symbolic evaluation [EQUIVALENT, 0 ms]
        (5) YES
    (6) Formula
        (7) Symbolic evaluation [EQUIVALENT, 0 ms]
        (8) Formula
        (9) Hypothesis Lifting [EQUIVALENT, 0 ms]
        (10) Formula
        (11) Inverse Substitution [SOUND, 0 ms]
        (12) Formula
        (13) Inverse Substitution [SOUND, 0 ms]
        (14) Formula
        (15) Induction by data structure [EQUIVALENT, 0 ms]
        (16) AND
            (17) Formula
                (18) Symbolic evaluation [EQUIVALENT, 0 ms]
                (19) YES
            (20) Formula
                (21) Symbolic evaluation [EQUIVALENT, 0 ms]
                (22) YES


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

(0)
Obligation:
Formula:
x1:sort[a0].if1'(ge(x1, x1), x1, x1, nil)=true

There are no hypotheses.




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

(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
if1'(ge(0, 0), 0, 0, nil)=true

There are no hypotheses.





1. Step Case:
Formula:
n:sort[a0].if1'(ge(s(n), s(n)), s(n), s(n), nil)=true

Hypotheses:
n:sort[a0].if1'(ge(n, n), n, n, nil)=true






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

(2)
Complex Obligation (AND)

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

(3)
Obligation:
Formula:
if1'(ge(0, 0), 0, 0, nil)=true

There are no hypotheses.




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

(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(5)
YES

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

(6)
Obligation:
Formula:
n:sort[a0].if1'(ge(s(n), s(n)), s(n), s(n), nil)=true

Hypotheses:
n:sort[a0].if1'(ge(n, n), n, n, nil)=true




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

(7) Symbolic evaluation (EQUIVALENT)
Could be shown by simple symbolic evaluation.
----------------------------------------

(8)
Obligation:
Formula:
n:sort[a0].if1'(ge(n, n), s(n), s(n), nil)=true

Hypotheses:
n:sort[a0].if1'(ge(n, n), n, n, nil)=true




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

(9) Hypothesis Lifting (EQUIVALENT)
Formula could be generalised by hypothesis lifting to the following new obligation:
Formula:
n:sort[a0].(if1'(ge(n, n), n, n, nil)=true->if1'(ge(n, n), s(n), s(n), nil)=true)

There are no hypotheses.




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

(10)
Obligation:
Formula:
n:sort[a0].(if1'(ge(n, n), n, n, nil)=true->if1'(ge(n, n), s(n), s(n), nil)=true)

There are no hypotheses.




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

(11) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n':sort[a21],n:sort[a0].(if1'(n', n, n, nil)=true->if1'(n', s(n), s(n), nil)=true)

Inverse substitution used:
[ge(n, n)/n']


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

(12)
Obligation:
Formula:
n':sort[a21],n:sort[a0].(if1'(n', n, n, nil)=true->if1'(n', s(n), s(n), nil)=true)

There are no hypotheses.




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

(13) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n':sort[a21],n:sort[a0],n'':sort[a0].(if1'(n', n, n, nil)=true->if1'(n', n'', n'', nil)=true)

Inverse substitution used:
[s(n)/n'']


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

(14)
Obligation:
Formula:
n':sort[a21],n:sort[a0],n'':sort[a0].(if1'(n', n, n, nil)=true->if1'(n', n'', n'', nil)=true)

There are no hypotheses.




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

(15) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a21] generates the following cases:



1. Base Case:
Formula:
n:sort[a0],n'':sort[a0].(if1'(true_renamed, n, n, nil)=true->if1'(true_renamed, n'', n'', nil)=true)

There are no hypotheses.





1. Base Case:
Formula:
n:sort[a0],n'':sort[a0].(if1'(false_renamed, n, n, nil)=true->if1'(false_renamed, n'', n'', nil)=true)

There are no hypotheses.






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

(16)
Complex Obligation (AND)

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

(17)
Obligation:
Formula:
n:sort[a0],n'':sort[a0].(if1'(true_renamed, n, n, nil)=true->if1'(true_renamed, n'', n'', nil)=true)

There are no hypotheses.




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

(18) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(19)
YES

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

(20)
Obligation:
Formula:
n:sort[a0],n'':sort[a0].(if1'(false_renamed, n, n, nil)=true->if1'(false_renamed, n'', n'', nil)=true)

There are no hypotheses.




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

(21) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(22)
YES

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

(126)
Complex Obligation (AND)

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

(127)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(true, n, x, xs) -> filterlow(n, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false
   half(0) -> 0

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(128) UsableRulesProof (EQUIVALENT)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
----------------------------------------

(129)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   if1(true, n, x, xs) -> filterlow(n, xs)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))
   half(0)
   half(s(0))
   half(s(s(x0)))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(130) QReductionProof (EQUIVALENT)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

   half(0)
   half(s(0))
   half(s(s(x0)))


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

(131)
Obligation:
Q DP problem:
The TRS P consists of the following rules:

   QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))

The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   if1(true, n, x, xs) -> filterlow(n, xs)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(132) Induction-Processor (SOUND)

This DP could be deleted by the Induction-Processor:
QS(0, cons(x0, cons(x1, x2))) -> QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))


This order was computed:
Polynomial interpretation [POLO]:

   POL(0) = 1
   POL(QS(x_1, x_2)) = x_2
   POL(cons(x_1, x_2)) = 1 + x_2
   POL(false_renamed) = 1
   POL(filterlow(x_1, x_2)) = x_2
   POL(ge(x_1, x_2)) = 1
   POL(if1(x_1, x_2, x_3, x_4)) = x_1 + x_4
   POL(nil) = 0
   POL(s(x_1)) = x_1
   POL(true_renamed) = 1

At least one of these decreasing rules is always used after the deleted DP:
if1(true_renamed, n, x'', xs) -> filterlow(n, xs)


The following formula is valid:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(x0, x0), x0, x0, cons(x1, x2))=true


The transformed set:
if1'(true_renamed, n, x'', xs) -> true
filterlow'(n', cons(x3, xs')) -> if1'(ge(n', x3), n', x3, xs')
if1'(false_renamed, n'', x4, xs'') -> filterlow'(n'', xs'')
filterlow'(n1, nil) -> false
ge(x, 0) -> true_renamed
ge(s(x'), s(y)) -> ge(x', y)
if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) -> nil
ge(0, s(x5)) -> false_renamed
equal_bool(true, false) -> false
equal_bool(false, true) -> false
equal_bool(true, true) -> true
equal_bool(false, false) -> true
and(true, x) -> x
and(false, x) -> false
or(true, x) -> true
or(false, x) -> x
not(false) -> true
not(true) -> false
isa_true(true) -> true
isa_true(false) -> false
isa_false(true) -> false
isa_false(false) -> true
equal_sort[a0](0, 0) -> true
equal_sort[a0](0, s(v13)) -> false
equal_sort[a0](s(v14), 0) -> false
equal_sort[a0](s(v14), s(v15)) -> equal_sort[a0](v14, v15)
equal_sort[a5](cons(v16, v17), cons(v18, v19)) -> and(equal_sort[a0](v16, v18), equal_sort[a5](v17, v19))
equal_sort[a5](cons(v16, v17), nil) -> false
equal_sort[a5](nil, cons(v20, v21)) -> false
equal_sort[a5](nil, nil) -> true
equal_sort[a19](true_renamed, true_renamed) -> true
equal_sort[a19](true_renamed, false_renamed) -> false
equal_sort[a19](false_renamed, true_renamed) -> false
equal_sort[a19](false_renamed, false_renamed) -> true
equal_sort[a39](witness_sort[a39], witness_sort[a39]) -> true


The proof given by the theorem prover:
The following output was given by the internal theorem prover:proof of internal
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


Partial correctness of the following Program

   [x, v13, v14, v15, v16, v17, v18, v19, v20, v21, n, x'', xs, n'', x4, x3, xs', n1, n', x', y, x5]
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   true and x -> x
   false and x -> false
   true or x -> true
   false or x -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v13)) -> false
   equal_sort[a0](s(v14), 0) -> false
   equal_sort[a0](s(v14), s(v15)) -> equal_sort[a0](v14, v15)
   equal_sort[a5](cons(v16, v17), cons(v18, v19)) -> equal_sort[a0](v16, v18) and equal_sort[a5](v17, v19)
   equal_sort[a5](cons(v16, v17), nil) -> false
   equal_sort[a5](nil, cons(v20, v21)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a19](true_renamed, true_renamed) -> true
   equal_sort[a19](true_renamed, false_renamed) -> false
   equal_sort[a19](false_renamed, true_renamed) -> false
   equal_sort[a19](false_renamed, false_renamed) -> true
   equal_sort[a39](witness_sort[a39], witness_sort[a39]) -> true
   if1'(true_renamed, n, x'', xs) -> true
   if1'(false_renamed, n'', x4, cons(x3, xs')) -> if1'(ge(n'', x3), n'', x3, xs')
   if1'(false_renamed, n'', x4, nil) -> false
   filterlow'(n1, nil) -> false
   equal_sort[a19](ge(n', x3), true_renamed) -> true | filterlow'(n', cons(x3, xs')) -> true
   equal_sort[a19](ge(n', x3), true_renamed) -> false | filterlow'(n', cons(x3, xs')) -> filterlow'(n', xs')
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   ge(0, s(x5)) -> false_renamed
   filterlow(n1, nil) -> nil
   equal_sort[a19](ge(n', x3), true_renamed) -> true | filterlow(n', cons(x3, xs')) -> filterlow(n', xs')
   equal_sort[a19](ge(n', x3), true_renamed) -> false | filterlow(n', cons(x3, xs')) -> cons(x3, filterlow(n', xs'))
   if1(true_renamed, n, x'', cons(x3, xs')) -> if1(ge(n, x3), n, x3, xs')
   if1(true_renamed, n, x'', nil) -> nil
   if1(false_renamed, n'', x4, cons(x3, xs')) -> cons(x4, if1(ge(n'', x3), n'', x3, xs'))
   if1(false_renamed, n'', x4, nil) -> cons(x4, nil)

using the following formula:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(x0, x0), x0, x0, cons(x1, x2))=true

could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT, 0 ms]
(2) AND
    (3) Formula
        (4) Symbolic evaluation [EQUIVALENT, 0 ms]
        (5) YES
    (6) Formula
        (7) Symbolic evaluation [EQUIVALENT, 0 ms]
        (8) Formula
        (9) Case Analysis [EQUIVALENT, 0 ms]
        (10) AND
            (11) Formula
                (12) Case Analysis [EQUIVALENT, 0 ms]
                (13) AND
                    (14) Formula
                        (15) Inverse Substitution [SOUND, 0 ms]
                        (16) Formula
                        (17) Induction by data structure [SOUND, 0 ms]
                        (18) AND
                            (19) Formula
                                (20) Symbolic evaluation [EQUIVALENT, 0 ms]
                                (21) YES
                            (22) Formula
                                (23) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
                                (24) YES
                    (25) Formula
                        (26) Inverse Substitution [SOUND, 0 ms]
                        (27) Formula
                        (28) Induction by data structure [SOUND, 0 ms]
                        (29) AND
                            (30) Formula
                                (31) Symbolic evaluation [EQUIVALENT, 0 ms]
                                (32) YES
                            (33) Formula
                                (34) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
                                (35) YES
            (36) Formula
                (37) Case Analysis [EQUIVALENT, 0 ms]
                (38) AND
                    (39) Formula
                        (40) Inverse Substitution [SOUND, 0 ms]
                        (41) Formula
                        (42) Induction by data structure [SOUND, 0 ms]
                        (43) AND
                            (44) Formula
                                (45) Symbolic evaluation [EQUIVALENT, 0 ms]
                                (46) YES
                            (47) Formula
                                (48) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
                                (49) YES
                    (50) Formula
                        (51) Inverse Substitution [SOUND, 0 ms]
                        (52) Formula
                        (53) Induction by data structure [SOUND, 0 ms]
                        (54) AND
                            (55) Formula
                                (56) Symbolic evaluation [EQUIVALENT, 0 ms]
                                (57) YES
                            (58) Formula
                                (59) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
                                (60) YES


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

(0)
Obligation:
Formula:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(x0, x0), x0, x0, cons(x1, x2))=true

There are no hypotheses.




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

(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
x1:sort[a0],x2:sort[a5].if1'(ge(0, 0), 0, 0, cons(x1, x2))=true

There are no hypotheses.





1. Step Case:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(s(n), s(n)), s(n), s(n), cons(x1, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true






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

(2)
Complex Obligation (AND)

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

(3)
Obligation:
Formula:
x1:sort[a0],x2:sort[a5].if1'(ge(0, 0), 0, 0, cons(x1, x2))=true

There are no hypotheses.




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

(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(5)
YES

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

(6)
Obligation:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(s(n), s(n)), s(n), s(n), cons(x1, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(7) Symbolic evaluation (EQUIVALENT)
Could be shown by simple symbolic evaluation.
----------------------------------------

(8)
Obligation:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(x1, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(9) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:

Formula:
n:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(0, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true





Formula:
n:sort[a0],x_1:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(s(x_1), x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true






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

(10)
Complex Obligation (AND)

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

(11)
Obligation:
Formula:
n:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(0, x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(12) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:

Formula:
n:sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(0, cons(x_1, x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true





Formula:
n:sort[a0].if1'(ge(n, n), s(n), s(n), cons(0, nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true






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

(13)
Complex Obligation (AND)

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

(14)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(0, cons(x_1, x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(15) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(0, cons(x_1, x_2)))=true

Inverse substitution used:
[s(n)/n']


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

(16)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(0, cons(x_1, x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(17) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(0, cons(x_1, x_2)))=true

There are no hypotheses.





1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(0, cons(x_1, x_2)))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true






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

(18)
Complex Obligation (AND)

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

(19)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(0, cons(x_1, x_2)))=true

There are no hypotheses.




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

(20) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(21)
YES

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

(22)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(0, cons(x_1, x_2)))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true




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

(23) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:

n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true

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

(24)
YES

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

(25)
Obligation:
Formula:
n:sort[a0].if1'(ge(n, n), s(n), s(n), cons(0, nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(26) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0].if1'(ge(n, n), n', n', cons(0, nil))=true

Inverse substitution used:
[s(n)/n']


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

(27)
Obligation:
Formula:
n:sort[a0],n':sort[a0].if1'(ge(n, n), n', n', cons(0, nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(28) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
n':sort[a0].if1'(ge(0, 0), n', n', cons(0, nil))=true

There are no hypotheses.





1. Step Case:
Formula:
n'':sort[a0],n':sort[a0].if1'(ge(s(n''), s(n'')), n', n', cons(0, nil))=true

Hypotheses:
n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', cons(0, nil))=true






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

(29)
Complex Obligation (AND)

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

(30)
Obligation:
Formula:
n':sort[a0].if1'(ge(0, 0), n', n', cons(0, nil))=true

There are no hypotheses.




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

(31) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(32)
YES

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

(33)
Obligation:
Formula:
n'':sort[a0],n':sort[a0].if1'(ge(s(n''), s(n'')), n', n', cons(0, nil))=true

Hypotheses:
n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', cons(0, nil))=true




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

(34) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:

n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', cons(0, nil))=true

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

(35)
YES

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

(36)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(s(x_1), x2))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(37) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:

Formula:
n:sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true





Formula:
n:sort[a0],x_1:sort[a0].if1'(ge(n, n), s(n), s(n), cons(s(x_1), nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true






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

(38)
Complex Obligation (AND)

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

(39)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(40) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(s(x_1), cons(x_1', x_2)))=true

Inverse substitution used:
[s(n)/n']


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

(41)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(42) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(s(x_1), cons(x_1', x_2)))=true

There are no hypotheses.





1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true






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

(43)
Complex Obligation (AND)

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

(44)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(s(x_1), cons(x_1', x_2)))=true

There are no hypotheses.




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

(45) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(46)
YES

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

(47)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(s(x_1), cons(x_1', x_2)))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true




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

(48) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:

n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true

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

(49)
YES

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

(50)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0].if1'(ge(n, n), s(n), s(n), cons(s(x_1), nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(51) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0].if1'(ge(n, n), n', n', cons(s(x_1), nil))=true

Inverse substitution used:
[s(n)/n']


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

(52)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0].if1'(ge(n, n), n', n', cons(s(x_1), nil))=true

Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true




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

(53) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:



1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0].if1'(ge(0, 0), n', n', cons(s(x_1), nil))=true

There are no hypotheses.





1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0].if1'(ge(s(n''), s(n'')), n', n', cons(s(x_1), nil))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if1'(ge(n'', n''), n', n', cons(s(x_1), nil))=true






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

(54)
Complex Obligation (AND)

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

(55)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0].if1'(ge(0, 0), n', n', cons(s(x_1), nil))=true

There are no hypotheses.




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

(56) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------

(57)
YES

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

(58)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0].if1'(ge(s(n''), s(n'')), n', n', cons(s(x_1), nil))=true

Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if1'(ge(n'', n''), n', n', cons(s(x_1), nil))=true




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

(59) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:

n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if1'(ge(n'', n''), n', n', cons(s(x_1), nil))=true

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

(60)
YES

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

(133)
Complex Obligation (AND)

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

(134)
Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:

   ge(x, 0) -> true
   ge(s(x), s(y)) -> ge(x, y)
   if1(true, n, x, xs) -> filterlow(n, xs)
   filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
   if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
   filterlow(n, nil) -> nil
   ge(0, s(x)) -> false

The set Q consists of the following terms:

   filterlow(x0, nil)
   filterlow(x0, cons(x1, x2))
   if1(true, x0, x1, x2)
   if1(false, x0, x1, x2)
   ge(x0, 0)
   ge(0, s(x0))
   ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
----------------------------------------

(135) PisEmptyProof (EQUIVALENT)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
----------------------------------------

(136)
YES

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

(137)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   if1'(true_renamed, n, x'', xs) -> true
   filterlow'(n', cons(x3, xs')) -> if1'(ge(n', x3), n', x3, xs')
   if1'(false_renamed, n'', x4, xs'') -> filterlow'(n'', xs'')
   filterlow'(n1, nil) -> false
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
   filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
   if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
   filterlow(n1, nil) -> nil
   ge(0, s(x5)) -> false_renamed
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   and(true, x) -> x
   and(false, x) -> false
   or(true, x) -> true
   or(false, x) -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v13)) -> false
   equal_sort[a0](s(v14), 0) -> false
   equal_sort[a0](s(v14), s(v15)) -> equal_sort[a0](v14, v15)
   equal_sort[a5](cons(v16, v17), cons(v18, v19)) -> and(equal_sort[a0](v16, v18), equal_sort[a5](v17, v19))
   equal_sort[a5](cons(v16, v17), nil) -> false
   equal_sort[a5](nil, cons(v20, v21)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a19](true_renamed, true_renamed) -> true
   equal_sort[a19](true_renamed, false_renamed) -> false
   equal_sort[a19](false_renamed, true_renamed) -> false
   equal_sort[a19](false_renamed, false_renamed) -> true
   equal_sort[a39](witness_sort[a39], witness_sort[a39]) -> true

Q is empty.

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

(138) QTRSRRRProof (EQUIVALENT)
Used ordering:
if1'/4(YES,YES,YES,YES)
true_renamed/0)
true/0)
filterlow'/2(YES,YES)
cons/2(YES,YES)
ge/2(YES,YES)
false_renamed/0)
nil/0)
false/0)
0/0)
s/1(YES)
if1/4(YES,YES,YES,YES)
filterlow/2(YES,YES)
equal_bool/2(YES,YES)
and/2(YES,YES)
or/2(YES,YES)
not/1(YES)
isa_true/1)YES(
isa_false/1(YES)
equal_sort[a0]/2(YES,YES)
equal_sort[a5]/2(YES,YES)
equal_sort[a19]/2(YES,YES)
equal_sort[a39]/2(YES,YES)
witness_sort[a39]/0)

Quasi precedence:
[true_renamed, 0] > [nil, false, if1_4, filterlow_2, isa_false_1] > [if1'_4, true, filterlow'_2, equal_sort[a39]_2, witness_sort[a39]] > ge_2
[true_renamed, 0] > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > ge_2
[true_renamed, 0] > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > and_2
[true_renamed, 0] > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > equal_sort[a0]_2
s_1 > ge_2
s_1 > equal_sort[a0]_2
or_2 > [if1'_4, true, filterlow'_2, equal_sort[a39]_2, witness_sort[a39]] > ge_2
not_1 > [nil, false, if1_4, filterlow_2, isa_false_1] > [if1'_4, true, filterlow'_2, equal_sort[a39]_2, witness_sort[a39]] > ge_2
not_1 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > ge_2
not_1 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > and_2
not_1 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > equal_sort[a0]_2
equal_sort[a5]_2 > [nil, false, if1_4, filterlow_2, isa_false_1] > [if1'_4, true, filterlow'_2, equal_sort[a39]_2, witness_sort[a39]] > ge_2
equal_sort[a5]_2 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > ge_2
equal_sort[a5]_2 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > and_2
equal_sort[a5]_2 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > equal_sort[a0]_2
equal_sort[a19]_2 > [nil, false, if1_4, filterlow_2, isa_false_1] > [if1'_4, true, filterlow'_2, equal_sort[a39]_2, witness_sort[a39]] > ge_2
equal_sort[a19]_2 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > ge_2
equal_sort[a19]_2 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > and_2
equal_sort[a19]_2 > [nil, false, if1_4, filterlow_2, isa_false_1] > [cons_2, false_renamed] > equal_sort[a0]_2


Status:
if1'_4: [4,2,3,1]
true_renamed: multiset status
true: multiset status
filterlow'_2: [2,1]
cons_2: multiset status
ge_2: multiset status
false_renamed: multiset status
nil: multiset status
false: multiset status
0: multiset status
s_1: multiset status
if1_4: [2,4,3,1]
filterlow_2: [1,2]
equal_bool_2: [1,2]
and_2: multiset status
or_2: multiset status
not_1: [1]
isa_false_1: [1]
equal_sort[a0]_2: multiset status
equal_sort[a5]_2: multiset status
equal_sort[a19]_2: [1,2]
equal_sort[a39]_2: [1,2]
witness_sort[a39]: multiset status

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   if1'(true_renamed, n, x'', xs) -> true
   filterlow'(n', cons(x3, xs')) -> if1'(ge(n', x3), n', x3, xs')
   if1'(false_renamed, n'', x4, xs'') -> filterlow'(n'', xs'')
   filterlow'(n1, nil) -> false
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
   filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
   if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
   filterlow(n1, nil) -> nil
   ge(0, s(x5)) -> false_renamed
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   and(true, x) -> x
   and(false, x) -> false
   or(true, x) -> true
   or(false, x) -> x
   not(false) -> true
   not(true) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v13)) -> false
   equal_sort[a0](s(v14), 0) -> false
   equal_sort[a0](s(v14), s(v15)) -> equal_sort[a0](v14, v15)
   equal_sort[a5](cons(v16, v17), cons(v18, v19)) -> and(equal_sort[a0](v16, v18), equal_sort[a5](v17, v19))
   equal_sort[a5](cons(v16, v17), nil) -> false
   equal_sort[a5](nil, cons(v20, v21)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a19](true_renamed, true_renamed) -> true
   equal_sort[a19](true_renamed, false_renamed) -> false
   equal_sort[a19](false_renamed, true_renamed) -> false
   equal_sort[a19](false_renamed, false_renamed) -> true
   equal_sort[a39](witness_sort[a39], witness_sort[a39]) -> true




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

(139)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   isa_true(true) -> true
   isa_true(false) -> false

Q is empty.

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

(140) QTRSRRRProof (EQUIVALENT)
Used ordering:
Knuth-Bendix order [KBO] with precedence:isa_true_1 > false > true

and weight map:

   true=1
   false=1
   isa_true_1=0

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   isa_true(true) -> true
   isa_true(false) -> false




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

(141)
Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.

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

(142) RisEmptyProof (EQUIVALENT)
The TRS R is empty. Hence, termination is trivially proven.
----------------------------------------

(143)
YES

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

(144)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   if1'(true_renamed, n, x'', xs) -> true
   if1'(false_renamed, n', x3, xs') -> filterlow'(n', xs')
   filterlow'(n'', nil) -> false
   filterlow'(n1, cons(x5, xs'')) -> if1'(ge(n1, x5), n1, x5, xs'')
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
   if1(false_renamed, n', x3, xs') -> cons(x3, filterlow(n', xs'))
   filterlow(n'', nil) -> nil
   ge(0, s(x4)) -> false_renamed
   half(0) -> 0
   filterlow(n1, cons(x5, xs'')) -> if1(ge(n1, x5), n1, x5, xs'')
   half(s(v14)) -> 0
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   and(true, x) -> x
   and(false, x) -> false
   or(true, x) -> true
   or(false, x) -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v15)) -> false
   equal_sort[a0](s(v16), 0) -> false
   equal_sort[a0](s(v16), s(v17)) -> equal_sort[a0](v16, v17)
   equal_sort[a5](cons(v18, v19), cons(v20, v21)) -> and(equal_sort[a0](v18, v20), equal_sort[a5](v19, v21))
   equal_sort[a5](cons(v18, v19), nil) -> false
   equal_sort[a5](nil, cons(v22, v23)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a21](true_renamed, true_renamed) -> true
   equal_sort[a21](true_renamed, false_renamed) -> false
   equal_sort[a21](false_renamed, true_renamed) -> false
   equal_sort[a21](false_renamed, false_renamed) -> true
   equal_sort[a43](witness_sort[a43], witness_sort[a43]) -> true

Q is empty.

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

(145) QTRSRRRProof (EQUIVALENT)
Used ordering:
if1'/4(YES,YES,YES,YES)
true_renamed/0)
true/0)
false_renamed/0)
filterlow'/2(YES,YES)
nil/0)
false/0)
cons/2(YES,YES)
ge/2(YES,YES)
0/0)
s/1)YES(
if1/4(YES,YES,YES,YES)
filterlow/2(YES,YES)
half/1(YES)
equal_bool/2(YES,YES)
and/2(YES,YES)
or/2(YES,YES)
not/1(YES)
isa_true/1(YES)
isa_false/1(YES)
equal_sort[a0]/2(YES,YES)
equal_sort[a5]/2(YES,YES)
equal_sort[a21]/2(YES,YES)
equal_sort[a43]/2(YES,YES)
witness_sort[a43]/0)

Quasi precedence:
[if1_4, filterlow_2] > nil > [true, not_1, equal_sort[a5]_2] > and_2 > [false, isa_true_1]
[if1_4, filterlow_2] > nil > [true, not_1, equal_sort[a5]_2] > equal_sort[a0]_2 > [false, isa_true_1]
[if1_4, filterlow_2] > cons_2 > [if1'_4, filterlow'_2] > ge_2 > [false_renamed, 0] > true_renamed > [false, isa_true_1]
[if1_4, filterlow_2] > cons_2 > [if1'_4, filterlow'_2] > ge_2 > [false_renamed, 0] > [true, not_1, equal_sort[a5]_2] > and_2 > [false, isa_true_1]
[if1_4, filterlow_2] > cons_2 > [if1'_4, filterlow'_2] > ge_2 > [false_renamed, 0] > [true, not_1, equal_sort[a5]_2] > equal_sort[a0]_2 > [false, isa_true_1]
half_1 > [false_renamed, 0] > true_renamed > [false, isa_true_1]
half_1 > [false_renamed, 0] > [true, not_1, equal_sort[a5]_2] > and_2 > [false, isa_true_1]
half_1 > [false_renamed, 0] > [true, not_1, equal_sort[a5]_2] > equal_sort[a0]_2 > [false, isa_true_1]
equal_bool_2 > [true, not_1, equal_sort[a5]_2] > and_2 > [false, isa_true_1]
equal_bool_2 > [true, not_1, equal_sort[a5]_2] > equal_sort[a0]_2 > [false, isa_true_1]
or_2 > [true, not_1, equal_sort[a5]_2] > and_2 > [false, isa_true_1]
or_2 > [true, not_1, equal_sort[a5]_2] > equal_sort[a0]_2 > [false, isa_true_1]
isa_false_1 > [true, not_1, equal_sort[a5]_2] > and_2 > [false, isa_true_1]
isa_false_1 > [true, not_1, equal_sort[a5]_2] > equal_sort[a0]_2 > [false, isa_true_1]
equal_sort[a21]_2 > [true, not_1, equal_sort[a5]_2] > and_2 > [false, isa_true_1]
equal_sort[a21]_2 > [true, not_1, equal_sort[a5]_2] > equal_sort[a0]_2 > [false, isa_true_1]
equal_sort[a43]_2 > [false, isa_true_1]
witness_sort[a43] > [true, not_1, equal_sort[a5]_2] > and_2 > [false, isa_true_1]
witness_sort[a43] > [true, not_1, equal_sort[a5]_2] > equal_sort[a0]_2 > [false, isa_true_1]


Status:
if1'_4: [2,4,1,3]
true_renamed: multiset status
true: multiset status
false_renamed: multiset status
filterlow'_2: [1,2]
nil: multiset status
false: multiset status
cons_2: multiset status
ge_2: multiset status
0: multiset status
if1_4: [4,2,1,3]
filterlow_2: [2,1]
half_1: multiset status
equal_bool_2: [1,2]
and_2: multiset status
or_2: multiset status
not_1: multiset status
isa_true_1: [1]
isa_false_1: [1]
equal_sort[a0]_2: multiset status
equal_sort[a5]_2: [1,2]
equal_sort[a21]_2: [1,2]
equal_sort[a43]_2: [1,2]
witness_sort[a43]: multiset status

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   if1'(true_renamed, n, x'', xs) -> true
   if1'(false_renamed, n', x3, xs') -> filterlow'(n', xs')
   filterlow'(n'', nil) -> false
   filterlow'(n1, cons(x5, xs'')) -> if1'(ge(n1, x5), n1, x5, xs'')
   ge(x, 0) -> true_renamed
   if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
   if1(false_renamed, n', x3, xs') -> cons(x3, filterlow(n', xs'))
   filterlow(n'', nil) -> nil
   ge(0, s(x4)) -> false_renamed
   half(0) -> 0
   filterlow(n1, cons(x5, xs'')) -> if1(ge(n1, x5), n1, x5, xs'')
   half(s(v14)) -> 0
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   and(true, x) -> x
   and(false, x) -> false
   or(true, x) -> true
   or(false, x) -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v15)) -> false
   equal_sort[a0](s(v16), 0) -> false
   equal_sort[a5](cons(v18, v19), cons(v20, v21)) -> and(equal_sort[a0](v18, v20), equal_sort[a5](v19, v21))
   equal_sort[a5](cons(v18, v19), nil) -> false
   equal_sort[a5](nil, cons(v22, v23)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a21](true_renamed, true_renamed) -> true
   equal_sort[a21](true_renamed, false_renamed) -> false
   equal_sort[a21](false_renamed, true_renamed) -> false
   equal_sort[a21](false_renamed, false_renamed) -> true
   equal_sort[a43](witness_sort[a43], witness_sort[a43]) -> true




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

(146)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   ge(s(x'), s(y)) -> ge(x', y)
   equal_sort[a0](s(v16), s(v17)) -> equal_sort[a0](v16, v17)

Q is empty.

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

(147) QTRSRRRProof (EQUIVALENT)
Used ordering:
Knuth-Bendix order [KBO] with precedence:s_1 > equal_sort[a0]_2 > ge_2

and weight map:

   s_1=0
   ge_2=0
   equal_sort[a0]_2=0

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   ge(s(x'), s(y)) -> ge(x', y)
   equal_sort[a0](s(v16), s(v17)) -> equal_sort[a0](v16, v17)




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

(148)
Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.

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

(149) RisEmptyProof (EQUIVALENT)
The TRS R is empty. Hence, termination is trivially proven.
----------------------------------------

(150)
YES

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

(151)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   if2'(true_renamed, n2, x6, xs1) -> true
   filterhigh'(n3, cons(x7, xs2)) -> if2'(ge(x7, n3), n3, x7, xs2)
   if2'(false_renamed, n4, x8, xs3) -> filterhigh'(n4, xs3)
   filterhigh'(n5, nil) -> false
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
   filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
   if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
   filterlow(n1, nil) -> nil
   ge(0, s(x5)) -> false_renamed
   half(0) -> 0
   if2(true_renamed, n2, x6, xs1) -> filterhigh(n2, xs1)
   filterhigh(n3, cons(x7, xs2)) -> if2(ge(x7, n3), n3, x7, xs2)
   if2(false_renamed, n4, x8, xs3) -> cons(x8, filterhigh(n4, xs3))
   filterhigh(n5, nil) -> nil
   half(s(v14)) -> 0
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   and(true, x) -> x
   and(false, x) -> false
   or(true, x) -> true
   or(false, x) -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v23)) -> false
   equal_sort[a0](s(v24), 0) -> false
   equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
   equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
   equal_sort[a5](cons(v26, v27), nil) -> false
   equal_sort[a5](nil, cons(v30, v31)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a34](true_renamed, true_renamed) -> true
   equal_sort[a34](true_renamed, false_renamed) -> false
   equal_sort[a34](false_renamed, true_renamed) -> false
   equal_sort[a34](false_renamed, false_renamed) -> true
   equal_sort[a64](witness_sort[a64], witness_sort[a64]) -> true

Q is empty.

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

(152) QTRSRRRProof (EQUIVALENT)
Used ordering:
if2'/4(YES,YES,YES,YES)
true_renamed/0)
true/0)
filterhigh'/2(YES,YES)
cons/2(YES,YES)
ge/2(YES,YES)
false_renamed/0)
nil/0)
false/0)
0/0)
s/1)YES(
if1/4(YES,YES,YES,YES)
filterlow/2(YES,YES)
half/1(YES)
if2/4(YES,YES,YES,YES)
filterhigh/2(YES,YES)
equal_bool/2(YES,YES)
and/2(YES,YES)
or/2(YES,YES)
not/1(YES)
isa_true/1)YES(
isa_false/1(YES)
equal_sort[a0]/2(YES,YES)
equal_sort[a5]/2(YES,YES)
equal_sort[a34]/2(YES,YES)
equal_sort[a64]/2(YES,YES)
witness_sort[a64]/0)

Quasi precedence:
nil > [if2'_4, true, filterhigh'_2, equal_sort[a64]_2] > [true_renamed, false_renamed, false] > [if2_4, filterhigh_2] > ge_2 > cons_2
[if1_4, filterlow_2] > ge_2 > cons_2
half_1 > 0 > [true_renamed, false_renamed, false] > [if2_4, filterhigh_2] > ge_2 > cons_2
equal_bool_2 > [if2'_4, true, filterhigh'_2, equal_sort[a64]_2] > [true_renamed, false_renamed, false] > [if2_4, filterhigh_2] > ge_2 > cons_2
or_2 > cons_2
not_1 > [if2'_4, true, filterhigh'_2, equal_sort[a64]_2] > [true_renamed, false_renamed, false] > [if2_4, filterhigh_2] > ge_2 > cons_2
isa_false_1 > [if2'_4, true, filterhigh'_2, equal_sort[a64]_2] > [true_renamed, false_renamed, false] > [if2_4, filterhigh_2] > ge_2 > cons_2
equal_sort[a5]_2 > and_2 > [true_renamed, false_renamed, false] > [if2_4, filterhigh_2] > ge_2 > cons_2
equal_sort[a5]_2 > equal_sort[a0]_2 > [if2'_4, true, filterhigh'_2, equal_sort[a64]_2] > [true_renamed, false_renamed, false] > [if2_4, filterhigh_2] > ge_2 > cons_2
equal_sort[a34]_2 > [if2'_4, true, filterhigh'_2, equal_sort[a64]_2] > [true_renamed, false_renamed, false] > [if2_4, filterhigh_2] > ge_2 > cons_2
witness_sort[a64] > cons_2


Status:
if2'_4: [2,4,3,1]
true_renamed: multiset status
true: multiset status
filterhigh'_2: [1,2]
cons_2: [1,2]
ge_2: [1,2]
false_renamed: multiset status
nil: multiset status
false: multiset status
0: multiset status
if1_4: [4,2,3,1]
filterlow_2: [2,1]
half_1: multiset status
if2_4: [2,4,3,1]
filterhigh_2: [1,2]
equal_bool_2: multiset status
and_2: multiset status
or_2: multiset status
not_1: multiset status
isa_false_1: multiset status
equal_sort[a0]_2: [1,2]
equal_sort[a5]_2: multiset status
equal_sort[a34]_2: multiset status
equal_sort[a64]_2: [1,2]
witness_sort[a64]: multiset status

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   if2'(true_renamed, n2, x6, xs1) -> true
   filterhigh'(n3, cons(x7, xs2)) -> if2'(ge(x7, n3), n3, x7, xs2)
   if2'(false_renamed, n4, x8, xs3) -> filterhigh'(n4, xs3)
   filterhigh'(n5, nil) -> false
   ge(x, 0) -> true_renamed
   if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
   filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
   if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
   filterlow(n1, nil) -> nil
   ge(0, s(x5)) -> false_renamed
   half(0) -> 0
   if2(true_renamed, n2, x6, xs1) -> filterhigh(n2, xs1)
   filterhigh(n3, cons(x7, xs2)) -> if2(ge(x7, n3), n3, x7, xs2)
   if2(false_renamed, n4, x8, xs3) -> cons(x8, filterhigh(n4, xs3))
   filterhigh(n5, nil) -> nil
   half(s(v14)) -> 0
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   and(true, x) -> x
   and(false, x) -> false
   or(true, x) -> true
   or(false, x) -> x
   not(false) -> true
   not(true) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v23)) -> false
   equal_sort[a0](s(v24), 0) -> false
   equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
   equal_sort[a5](cons(v26, v27), nil) -> false
   equal_sort[a5](nil, cons(v30, v31)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a34](true_renamed, true_renamed) -> true
   equal_sort[a34](true_renamed, false_renamed) -> false
   equal_sort[a34](false_renamed, true_renamed) -> false
   equal_sort[a34](false_renamed, false_renamed) -> true
   equal_sort[a64](witness_sort[a64], witness_sort[a64]) -> true




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

(153)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   ge(s(x'), s(y)) -> ge(x', y)
   isa_true(true) -> true
   isa_true(false) -> false
   equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)

Q is empty.

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

(154) QTRSRRRProof (EQUIVALENT)
Used ordering:
Knuth-Bendix order [KBO] with precedence:s_1 > equal_sort[a0]_2 > false > true > isa_true_1 > ge_2

and weight map:

   true=1
   false=1
   s_1=0
   isa_true_1=1
   ge_2=0
   equal_sort[a0]_2=0

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   ge(s(x'), s(y)) -> ge(x', y)
   isa_true(true) -> true
   isa_true(false) -> false
   equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)




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

(155)
Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.

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

(156) RisEmptyProof (EQUIVALENT)
The TRS R is empty. Hence, termination is trivially proven.
----------------------------------------

(157)
YES

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

(158)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   if2'(true_renamed, n2, x6, xs1) -> true
   filterhigh'(n3, cons(x7, xs2)) -> if2'(ge(x7, n3), n3, x7, xs2)
   if2'(false_renamed, n4, x8, xs3) -> filterhigh'(n4, xs3)
   filterhigh'(n5, nil) -> false
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
   filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
   if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
   filterlow(n1, nil) -> nil
   ge(0, s(x5)) -> false_renamed
   half(0) -> 0
   if2(true_renamed, n2, x6, xs1) -> filterhigh(n2, xs1)
   filterhigh(n3, cons(x7, xs2)) -> if2(ge(x7, n3), n3, x7, xs2)
   if2(false_renamed, n4, x8, xs3) -> cons(x8, filterhigh(n4, xs3))
   filterhigh(n5, nil) -> nil
   half(s(v14)) -> 0
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   and(true, x) -> x
   and(false, x) -> false
   or(true, x) -> true
   or(false, x) -> x
   not(false) -> true
   not(true) -> false
   isa_true(true) -> true
   isa_true(false) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v23)) -> false
   equal_sort[a0](s(v24), 0) -> false
   equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
   equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
   equal_sort[a5](cons(v26, v27), nil) -> false
   equal_sort[a5](nil, cons(v30, v31)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a36](true_renamed, true_renamed) -> true
   equal_sort[a36](true_renamed, false_renamed) -> false
   equal_sort[a36](false_renamed, true_renamed) -> false
   equal_sort[a36](false_renamed, false_renamed) -> true
   equal_sort[a66](witness_sort[a66], witness_sort[a66]) -> true

Q is empty.

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

(159) QTRSRRRProof (EQUIVALENT)
Used ordering:
if2'/4(YES,YES,YES,YES)
true_renamed/0)
true/0)
filterhigh'/2(YES,YES)
cons/2(YES,YES)
ge/2(YES,YES)
false_renamed/0)
nil/0)
false/0)
0/0)
s/1(YES)
if1/4(YES,YES,YES,YES)
filterlow/2(YES,YES)
half/1)YES(
if2/4(YES,YES,YES,YES)
filterhigh/2(YES,YES)
equal_bool/2(YES,YES)
and/2(YES,YES)
or/2(YES,YES)
not/1(YES)
isa_true/1)YES(
isa_false/1(YES)
equal_sort[a0]/2(YES,YES)
equal_sort[a5]/2(YES,YES)
equal_sort[a36]/2(YES,YES)
equal_sort[a66]/2(YES,YES)
witness_sort[a66]/0)

Quasi precedence:
[if2'_4, filterhigh'_2] > [false, not_1] > true > [cons_2, ge_2, equal_sort[a0]_2]
s_1 > [false, not_1] > true > [cons_2, ge_2, equal_sort[a0]_2]
s_1 > 0 > true_renamed > [false_renamed, if1_4, filterlow_2] > [cons_2, ge_2, equal_sort[a0]_2]
s_1 > 0 > true > [cons_2, ge_2, equal_sort[a0]_2]
[if2_4, filterhigh_2] > nil > [cons_2, ge_2, equal_sort[a0]_2]
equal_bool_2 > true > [cons_2, ge_2, equal_sort[a0]_2]
or_2 > true > [cons_2, ge_2, equal_sort[a0]_2]
isa_false_1 > [false, not_1] > true > [cons_2, ge_2, equal_sort[a0]_2]
equal_sort[a5]_2 > [false, not_1] > true > [cons_2, ge_2, equal_sort[a0]_2]
equal_sort[a5]_2 > and_2 > [cons_2, ge_2, equal_sort[a0]_2]
equal_sort[a36]_2 > [false, not_1] > true > [cons_2, ge_2, equal_sort[a0]_2]
equal_sort[a66]_2 > true > [cons_2, ge_2, equal_sort[a0]_2]
witness_sort[a66] > [cons_2, ge_2, equal_sort[a0]_2]


Status:
if2'_4: [2,4,1,3]
true_renamed: multiset status
true: multiset status
filterhigh'_2: [1,2]
cons_2: multiset status
ge_2: multiset status
false_renamed: multiset status
nil: multiset status
false: multiset status
0: multiset status
s_1: multiset status
if1_4: [2,4,3,1]
filterlow_2: [1,2]
if2_4: [4,2,3,1]
filterhigh_2: [2,1]
equal_bool_2: multiset status
and_2: multiset status
or_2: multiset status
not_1: multiset status
isa_false_1: multiset status
equal_sort[a0]_2: multiset status
equal_sort[a5]_2: multiset status
equal_sort[a36]_2: [1,2]
equal_sort[a66]_2: multiset status
witness_sort[a66]: multiset status

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   if2'(true_renamed, n2, x6, xs1) -> true
   filterhigh'(n3, cons(x7, xs2)) -> if2'(ge(x7, n3), n3, x7, xs2)
   if2'(false_renamed, n4, x8, xs3) -> filterhigh'(n4, xs3)
   filterhigh'(n5, nil) -> false
   ge(x, 0) -> true_renamed
   ge(s(x'), s(y)) -> ge(x', y)
   if1(true_renamed, n, x'', xs) -> filterlow(n, xs)
   filterlow(n', cons(x3, xs')) -> if1(ge(n', x3), n', x3, xs')
   if1(false_renamed, n'', x4, xs'') -> cons(x4, filterlow(n'', xs''))
   filterlow(n1, nil) -> nil
   ge(0, s(x5)) -> false_renamed
   if2(true_renamed, n2, x6, xs1) -> filterhigh(n2, xs1)
   filterhigh(n3, cons(x7, xs2)) -> if2(ge(x7, n3), n3, x7, xs2)
   if2(false_renamed, n4, x8, xs3) -> cons(x8, filterhigh(n4, xs3))
   filterhigh(n5, nil) -> nil
   half(s(v14)) -> 0
   equal_bool(true, false) -> false
   equal_bool(false, true) -> false
   equal_bool(true, true) -> true
   equal_bool(false, false) -> true
   and(true, x) -> x
   and(false, x) -> false
   or(true, x) -> true
   or(false, x) -> x
   not(false) -> true
   not(true) -> false
   isa_false(true) -> false
   isa_false(false) -> true
   equal_sort[a0](0, 0) -> true
   equal_sort[a0](0, s(v23)) -> false
   equal_sort[a0](s(v24), 0) -> false
   equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
   equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
   equal_sort[a5](cons(v26, v27), nil) -> false
   equal_sort[a5](nil, cons(v30, v31)) -> false
   equal_sort[a5](nil, nil) -> true
   equal_sort[a36](true_renamed, true_renamed) -> true
   equal_sort[a36](true_renamed, false_renamed) -> false
   equal_sort[a36](false_renamed, true_renamed) -> false
   equal_sort[a36](false_renamed, false_renamed) -> true
   equal_sort[a66](witness_sort[a66], witness_sort[a66]) -> true




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

(160)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   half(0) -> 0
   isa_true(true) -> true
   isa_true(false) -> false

Q is empty.

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

(161) QTRSRRRProof (EQUIVALENT)
Used ordering:
Knuth-Bendix order [KBO] with precedence:isa_true_1 > false > true > 0 > half_1

and weight map:

   0=1
   true=1
   false=1
   half_1=1
   isa_true_1=0

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   half(0) -> 0
   isa_true(true) -> true
   isa_true(false) -> false




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

(162)
Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.

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

(163) RisEmptyProof (EQUIVALENT)
The TRS R is empty. Hence, termination is trivially proven.
----------------------------------------

(164)
YES