We consider the system Applicative_first_order_05__#3.55.

  Alphabet:

    0 : [] --> b 
    add : [b * c] --> c 
    app : [c * c] --> c 
    false : [] --> a 
    filter : [b -> a * c] --> c 
    filter2 : [a * b -> a * b * c] --> c 
    high : [b * c] --> c 
    if!fac6220high : [a * b * c] --> c 
    if!fac6220low : [a * b * c] --> c 
    le : [b * b] --> a 
    low : [b * c] --> c 
    map : [b -> b * c] --> c 
    minus : [b * b] --> b 
    nil : [] --> c 
    quicksort : [c] --> c 
    quot : [b * b] --> b 
    s : [b] --> b 
    true : [] --> a 

  Rules:

    minus(x, 0) => x 
    minus(s(x), s(y)) => minus(x, y) 
    quot(0, s(x)) => 0 
    quot(s(x), s(y)) => s(quot(minus(x, y), s(y))) 
    le(0, x) => true 
    le(s(x), 0) => false 
    le(s(x), s(y)) => le(x, y) 
    app(nil, x) => x 
    app(add(x, y), z) => add(x, app(y, z)) 
    low(x, nil) => nil 
    low(x, add(y, z)) => if!fac6220low(le(y, x), x, add(y, z)) 
    if!fac6220low(true, x, add(y, z)) => add(y, low(x, z)) 
    if!fac6220low(false, x, add(y, z)) => low(x, z) 
    high(x, nil) => nil 
    high(x, add(y, z)) => if!fac6220high(le(y, x), x, add(y, z)) 
    if!fac6220high(true, x, add(y, z)) => high(x, z) 
    if!fac6220high(false, x, add(y, z)) => add(y, high(x, z)) 
    quicksort(nil) => nil 
    quicksort(add(x, y)) => app(quicksort(low(x, y)), add(x, quicksort(high(x, y)))) 
    map(f, nil) => nil 
    map(f, add(x, y)) => add(f x, map(f, y)) 
    filter(f, nil) => nil 
    filter(f, add(x, y)) => filter2(f x, f, x, y) 
    filter2(true, f, x, y) => add(x, filter(f, y)) 
    filter2(false, f, x, y) => filter(f, y) 

This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0).

We observe that the rules contain a first-order subset:

  minus(X, 0) => X 
  minus(s(X), s(Y)) => minus(X, Y) 
  quot(0, s(X)) => 0 
  quot(s(X), s(Y)) => s(quot(minus(X, Y), s(Y))) 
  le(0, X) => true 
  le(s(X), 0) => false 
  le(s(X), s(Y)) => le(X, Y) 
  app(nil, X) => X 
  app(add(X, Y), Z) => add(X, app(Y, Z)) 
  low(X, nil) => nil 
  low(X, add(Y, Z)) => if!fac6220low(le(Y, X), X, add(Y, Z)) 
  if!fac6220low(true, X, add(Y, Z)) => add(Y, low(X, Z)) 
  if!fac6220low(false, X, add(Y, Z)) => low(X, Z) 
  high(X, nil) => nil 
  high(X, add(Y, Z)) => if!fac6220high(le(Y, X), X, add(Y, Z)) 
  if!fac6220high(true, X, add(Y, Z)) => high(X, Z) 
  if!fac6220high(false, X, add(Y, Z)) => add(Y, high(X, Z)) 
  quicksort(nil) => nil 
  quicksort(add(X, Y)) => app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) 

Moreover, the system is orthogonal.  Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is terminating when seen as a many-sorted first-order TRS.

According to the external first-order termination prover, this system is indeed terminating:

 || proof of resources/system.trs
 || # AProVE Commit ID: d84c10301d352dfd14de2104819581f4682260f5 fuhs 20130616
 || 
 || 
 || Termination w.r.t. Q of the given QTRS could be proven:
 || 
 || (0) QTRS
 || (1) Overlay + Local Confluence [EQUIVALENT]
 || (2) QTRS
 || (3) DependencyPairsProof [EQUIVALENT]
 || (4) QDP
 || (5) DependencyGraphProof [EQUIVALENT]
 || (6) AND
 ||     (7) QDP
 ||         (8) UsableRulesProof [EQUIVALENT]
 ||         (9) QDP
 ||         (10) QReductionProof [EQUIVALENT]
 ||         (11) QDP
 ||         (12) QDPSizeChangeProof [EQUIVALENT]
 ||         (13) YES
 ||     (14) QDP
 ||         (15) UsableRulesProof [EQUIVALENT]
 ||         (16) QDP
 ||         (17) QReductionProof [EQUIVALENT]
 ||         (18) QDP
 ||         (19) QDPSizeChangeProof [EQUIVALENT]
 ||         (20) YES
 ||     (21) QDP
 ||         (22) UsableRulesProof [EQUIVALENT]
 ||         (23) QDP
 ||         (24) QReductionProof [EQUIVALENT]
 ||         (25) QDP
 ||         (26) QDPSizeChangeProof [EQUIVALENT]
 ||         (27) YES
 ||     (28) QDP
 ||         (29) UsableRulesProof [EQUIVALENT]
 ||         (30) QDP
 ||         (31) QReductionProof [EQUIVALENT]
 ||         (32) QDP
 ||         (33) QDPSizeChangeProof [EQUIVALENT]
 ||         (34) YES
 ||     (35) QDP
 ||         (36) UsableRulesProof [EQUIVALENT]
 ||         (37) QDP
 ||         (38) QReductionProof [EQUIVALENT]
 ||         (39) QDP
 ||         (40) QDPOrderProof [EQUIVALENT]
 ||         (41) QDP
 ||         (42) PisEmptyProof [EQUIVALENT]
 ||         (43) YES
 ||     (44) QDP
 ||         (45) UsableRulesProof [EQUIVALENT]
 ||         (46) QDP
 ||         (47) QReductionProof [EQUIVALENT]
 ||         (48) QDP
 ||         (49) QDPSizeChangeProof [EQUIVALENT]
 ||         (50) YES
 ||     (51) QDP
 ||         (52) UsableRulesProof [EQUIVALENT]
 ||         (53) QDP
 ||         (54) QReductionProof [EQUIVALENT]
 ||         (55) QDP
 ||         (56) QDPOrderProof [EQUIVALENT]
 ||         (57) QDP
 ||         (58) PisEmptyProof [EQUIVALENT]
 ||         (59) YES
 || 
 || 
 || ----------------------------------------
 || 
 || (0)
 || Obligation:
 || Q restricted rewrite system:
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || 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:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 
 || ----------------------------------------
 || 
 || (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:
 || 
 ||    MINUS(s(%X), s(%Y)) -> MINUS(%X, %Y)
 ||    QUOT(s(%X), s(%Y)) -> QUOT(minus(%X, %Y), s(%Y))
 ||    QUOT(s(%X), s(%Y)) -> MINUS(%X, %Y)
 ||    LE(s(%X), s(%Y)) -> LE(%X, %Y)
 ||    APP(add(%X, %Y), %Z) -> APP(%Y, %Z)
 ||    LOW(%X, add(%Y, %Z)) -> IF!FAC6220LOW(le(%Y, %X), %X, add(%Y, %Z))
 ||    LOW(%X, add(%Y, %Z)) -> LE(%Y, %X)
 ||    IF!FAC6220LOW(true, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 ||    IF!FAC6220LOW(false, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 ||    HIGH(%X, add(%Y, %Z)) -> IF!FAC6220HIGH(le(%Y, %X), %X, add(%Y, %Z))
 ||    HIGH(%X, add(%Y, %Z)) -> LE(%Y, %X)
 ||    IF!FAC6220HIGH(true, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 ||    IF!FAC6220HIGH(false, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 ||    QUICKSORT(add(%X, %Y)) -> APP(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(low(%X, %Y))
 ||    QUICKSORT(add(%X, %Y)) -> LOW(%X, %Y)
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(high(%X, %Y))
 ||    QUICKSORT(add(%X, %Y)) -> HIGH(%X, %Y)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (5) DependencyGraphProof (EQUIVALENT)
 || The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 7 SCCs with 6 less nodes.
 || ----------------------------------------
 || 
 || (6)
 || Complex Obligation (AND)
 || 
 || ----------------------------------------
 || 
 || (7)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    APP(add(%X, %Y), %Z) -> APP(%Y, %Z)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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:
 || 
 ||    APP(add(%X, %Y), %Z) -> APP(%Y, %Z)
 || 
 || R is empty.
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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].
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 
 || ----------------------------------------
 || 
 || (11)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    APP(add(%X, %Y), %Z) -> APP(%Y, %Z)
 || 
 || 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:
 || *APP(add(%X, %Y), %Z) -> APP(%Y, %Z)
 || 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:
 || 
 ||    LE(s(%X), s(%Y)) -> LE(%X, %Y)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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:
 || 
 ||    LE(s(%X), s(%Y)) -> LE(%X, %Y)
 || 
 || R is empty.
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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].
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 
 || ----------------------------------------
 || 
 || (18)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    LE(s(%X), s(%Y)) -> LE(%X, %Y)
 || 
 || 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:
 || *LE(s(%X), s(%Y)) -> LE(%X, %Y)
 || The graph contains the following edges 1 > 1, 2 > 2
 || 
 || 
 || ----------------------------------------
 || 
 || (20)
 || YES
 || 
 || ----------------------------------------
 || 
 || (21)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    HIGH(%X, add(%Y, %Z)) -> IF!FAC6220HIGH(le(%Y, %X), %X, add(%Y, %Z))
 ||    IF!FAC6220HIGH(true, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 ||    IF!FAC6220HIGH(false, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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:
 || 
 ||    HIGH(%X, add(%Y, %Z)) -> IF!FAC6220HIGH(le(%Y, %X), %X, add(%Y, %Z))
 ||    IF!FAC6220HIGH(true, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 ||    IF!FAC6220HIGH(false, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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].
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 
 || ----------------------------------------
 || 
 || (25)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    HIGH(%X, add(%Y, %Z)) -> IF!FAC6220HIGH(le(%Y, %X), %X, add(%Y, %Z))
 ||    IF!FAC6220HIGH(true, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 ||    IF!FAC6220HIGH(false, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 || 
 || The set Q consists of the following terms:
 || 
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 || 
 || 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:
 || *HIGH(%X, add(%Y, %Z)) -> IF!FAC6220HIGH(le(%Y, %X), %X, add(%Y, %Z))
 || The graph contains the following edges 1 >= 2, 2 >= 3
 || 
 || 
 || *IF!FAC6220HIGH(true, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 || The graph contains the following edges 2 >= 1, 3 > 2
 || 
 || 
 || *IF!FAC6220HIGH(false, %X, add(%Y, %Z)) -> HIGH(%X, %Z)
 || The graph contains the following edges 2 >= 1, 3 > 2
 || 
 || 
 || ----------------------------------------
 || 
 || (27)
 || YES
 || 
 || ----------------------------------------
 || 
 || (28)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    LOW(%X, add(%Y, %Z)) -> IF!FAC6220LOW(le(%Y, %X), %X, add(%Y, %Z))
 ||    IF!FAC6220LOW(true, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 ||    IF!FAC6220LOW(false, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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:
 || 
 ||    LOW(%X, add(%Y, %Z)) -> IF!FAC6220LOW(le(%Y, %X), %X, add(%Y, %Z))
 ||    IF!FAC6220LOW(true, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 ||    IF!FAC6220LOW(false, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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].
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 
 || ----------------------------------------
 || 
 || (32)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    LOW(%X, add(%Y, %Z)) -> IF!FAC6220LOW(le(%Y, %X), %X, add(%Y, %Z))
 ||    IF!FAC6220LOW(true, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 ||    IF!FAC6220LOW(false, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 || 
 || The set Q consists of the following terms:
 || 
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 || 
 || 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:
 || *LOW(%X, add(%Y, %Z)) -> IF!FAC6220LOW(le(%Y, %X), %X, add(%Y, %Z))
 || The graph contains the following edges 1 >= 2, 2 >= 3
 || 
 || 
 || *IF!FAC6220LOW(true, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 || The graph contains the following edges 2 >= 1, 3 > 2
 || 
 || 
 || *IF!FAC6220LOW(false, %X, add(%Y, %Z)) -> LOW(%X, %Z)
 || The graph contains the following edges 2 >= 1, 3 > 2
 || 
 || 
 || ----------------------------------------
 || 
 || (34)
 || YES
 || 
 || ----------------------------------------
 || 
 || (35)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(high(%X, %Y))
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(low(%X, %Y))
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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:
 || 
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(high(%X, %Y))
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(low(%X, %Y))
 || 
 || The TRS R consists of the following rules:
 || 
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 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].
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 
 || ----------------------------------------
 || 
 || (39)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(high(%X, %Y))
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(low(%X, %Y))
 || 
 || The TRS R consists of the following rules:
 || 
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 || 
 || The set Q consists of the following terms:
 || 
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (40) QDPOrderProof (EQUIVALENT)
 || We use the reduction pair processor [LPAR04,JAR06].
 || 
 || 
 || The following pairs can be oriented strictly and are deleted.
 || 
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(high(%X, %Y))
 ||    QUICKSORT(add(%X, %Y)) -> QUICKSORT(low(%X, %Y))
 || The remaining pairs can at least be oriented weakly.
 || Used ordering:  Polynomial Order [NEGPOLO,POLO] with Interpretation:
 || 
 || POL( QUICKSORT_1(x_1) ) = max{0, 2x_1 - 2}
 || POL( high_2(x_1, x_2) ) = 2x_2
 || POL( nil ) = 0
 || POL( add_2(x_1, x_2) ) = 2x_2 + 2
 || POL( if!fac6220high_3(x_1, ..., x_3) ) = max{0, 2x_3 - 2}
 || POL( le_2(x_1, x_2) ) = 2x_2
 || POL( true ) = 2
 || POL( low_2(x_1, x_2) ) = 2x_2
 || POL( if!fac6220low_3(x_1, ..., x_3) ) = max{0, 2x_3 - 2}
 || POL( false ) = 2
 || POL( 0 ) = 0
 || POL( s_1(x_1) ) = 1
 || 
 || The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
 || 
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 || 
 || 
 || ----------------------------------------
 || 
 || (41)
 || Obligation:
 || Q DP problem:
 || P is empty.
 || The TRS R consists of the following rules:
 || 
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 || 
 || The set Q consists of the following terms:
 || 
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (42) PisEmptyProof (EQUIVALENT)
 || The TRS P is empty. Hence, there is no (P,Q,R) chain.
 || ----------------------------------------
 || 
 || (43)
 || YES
 || 
 || ----------------------------------------
 || 
 || (44)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    MINUS(s(%X), s(%Y)) -> MINUS(%X, %Y)
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (45) 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.
 || ----------------------------------------
 || 
 || (46)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    MINUS(s(%X), s(%Y)) -> MINUS(%X, %Y)
 || 
 || R is empty.
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (47) 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].
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 
 || ----------------------------------------
 || 
 || (48)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    MINUS(s(%X), s(%Y)) -> MINUS(%X, %Y)
 || 
 || R is empty.
 || Q is empty.
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (49) 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:
 || *MINUS(s(%X), s(%Y)) -> MINUS(%X, %Y)
 || The graph contains the following edges 1 > 1, 2 > 2
 || 
 || 
 || ----------------------------------------
 || 
 || (50)
 || YES
 || 
 || ----------------------------------------
 || 
 || (51)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    QUOT(s(%X), s(%Y)) -> QUOT(minus(%X, %Y), s(%Y))
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 ||    quot(0, s(%X)) -> 0
 ||    quot(s(%X), s(%Y)) -> s(quot(minus(%X, %Y), s(%Y)))
 ||    le(0, %X) -> true
 ||    le(s(%X), 0) -> false
 ||    le(s(%X), s(%Y)) -> le(%X, %Y)
 ||    app(nil, %X) -> %X
 ||    app(add(%X, %Y), %Z) -> add(%X, app(%Y, %Z))
 ||    low(%X, nil) -> nil
 ||    low(%X, add(%Y, %Z)) -> if!fac6220low(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220low(true, %X, add(%Y, %Z)) -> add(%Y, low(%X, %Z))
 ||    if!fac6220low(false, %X, add(%Y, %Z)) -> low(%X, %Z)
 ||    high(%X, nil) -> nil
 ||    high(%X, add(%Y, %Z)) -> if!fac6220high(le(%Y, %X), %X, add(%Y, %Z))
 ||    if!fac6220high(true, %X, add(%Y, %Z)) -> high(%X, %Z)
 ||    if!fac6220high(false, %X, add(%Y, %Z)) -> add(%Y, high(%X, %Z))
 ||    quicksort(nil) -> nil
 ||    quicksort(add(%X, %Y)) -> app(quicksort(low(%X, %Y)), add(%X, quicksort(high(%X, %Y))))
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (52) 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.
 || ----------------------------------------
 || 
 || (53)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    QUOT(s(%X), s(%Y)) -> QUOT(minus(%X, %Y), s(%Y))
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (54) 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].
 || 
 ||    quot(0, s(x0))
 ||    quot(s(x0), s(x1))
 ||    le(0, x0)
 ||    le(s(x0), 0)
 ||    le(s(x0), s(x1))
 ||    app(nil, x0)
 ||    app(add(x0, x1), x2)
 ||    low(x0, nil)
 ||    low(x0, add(x1, x2))
 ||    if!fac6220low(true, x0, add(x1, x2))
 ||    if!fac6220low(false, x0, add(x1, x2))
 ||    high(x0, nil)
 ||    high(x0, add(x1, x2))
 ||    if!fac6220high(true, x0, add(x1, x2))
 ||    if!fac6220high(false, x0, add(x1, x2))
 ||    quicksort(nil)
 ||    quicksort(add(x0, x1))
 || 
 || 
 || ----------------------------------------
 || 
 || (55)
 || Obligation:
 || Q DP problem:
 || The TRS P consists of the following rules:
 || 
 ||    QUOT(s(%X), s(%Y)) -> QUOT(minus(%X, %Y), s(%Y))
 || 
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (56) QDPOrderProof (EQUIVALENT)
 || We use the reduction pair processor [LPAR04,JAR06].
 || 
 || 
 || The following pairs can be oriented strictly and are deleted.
 || 
 ||    QUOT(s(%X), s(%Y)) -> QUOT(minus(%X, %Y), s(%Y))
 || The remaining pairs can at least be oriented weakly.
 || Used ordering:  Polynomial Order [NEGPOLO,POLO] with Interpretation:
 || 
 || POL( QUOT_2(x_1, x_2) ) = 2x_1 + x_2
 || POL( minus_2(x_1, x_2) ) = x_1 + 1
 || POL( 0 ) = 2
 || POL( s_1(x_1) ) = 2x_1 + 2
 || 
 || The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 || 
 || 
 || ----------------------------------------
 || 
 || (57)
 || Obligation:
 || Q DP problem:
 || P is empty.
 || The TRS R consists of the following rules:
 || 
 ||    minus(%X, 0) -> %X
 ||    minus(s(%X), s(%Y)) -> minus(%X, %Y)
 || 
 || The set Q consists of the following terms:
 || 
 ||    minus(x0, 0)
 ||    minus(s(x0), s(x1))
 || 
 || We have to consider all minimal (P,Q,R)-chains.
 || ----------------------------------------
 || 
 || (58) PisEmptyProof (EQUIVALENT)
 || The TRS P is empty. Hence, there is no (P,Q,R) chain.
 || ----------------------------------------
 || 
 || (59)
 || YES
 || 
We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, formative):

  Dependency Pairs P_0:

    0] map#(F, add(X, Y)) =#> F(X)   
    1] map#(F, add(X, Y)) =#> map#(F, Y)   
    2] filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y)   
    3] filter#(F, add(X, Y)) =#> F(X)   
    4] filter2#(true, F, X, Y) =#> filter#(F, Y)   
    5] filter2#(false, F, X, Y) =#> filter#(F, Y)   

  Rules R_0:

    minus(X, 0) => X 
    minus(s(X), s(Y)) => minus(X, Y) 
    quot(0, s(X)) => 0 
    quot(s(X), s(Y)) => s(quot(minus(X, Y), s(Y))) 
    le(0, X) => true 
    le(s(X), 0) => false 
    le(s(X), s(Y)) => le(X, Y) 
    app(nil, X) => X 
    app(add(X, Y), Z) => add(X, app(Y, Z)) 
    low(X, nil) => nil 
    low(X, add(Y, Z)) => if!fac6220low(le(Y, X), X, add(Y, Z)) 
    if!fac6220low(true, X, add(Y, Z)) => add(Y, low(X, Z)) 
    if!fac6220low(false, X, add(Y, Z)) => low(X, Z) 
    high(X, nil) => nil 
    high(X, add(Y, Z)) => if!fac6220high(le(Y, X), X, add(Y, Z)) 
    if!fac6220high(true, X, add(Y, Z)) => high(X, Z) 
    if!fac6220high(false, X, add(Y, Z)) => add(Y, high(X, Z)) 
    quicksort(nil) => nil 
    quicksort(add(X, Y)) => app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) 
    map(F, nil) => nil 
    map(F, add(X, Y)) => add(F X, map(F, Y)) 
    filter(F, nil) => nil 
    filter(F, add(X, Y)) => filter2(F X, F, X, Y) 
    filter2(true, F, X, Y) => add(X, filter(F, Y)) 
    filter2(false, F, X, Y) => filter(F, Y) 

Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  map#(F, add(X, Y)) >? F(X) 
  map#(F, add(X, Y)) >? map#(F, Y) 
  filter#(F, add(X, Y)) >? filter2#(F X, F, X, Y) 
  filter#(F, add(X, Y)) >? F(X) 
  filter2#(true, F, X, Y) >? filter#(F, Y) 
  filter2#(false, F, X, Y) >? filter#(F, Y) 
  minus(X, 0) >= X 
  minus(s(X), s(Y)) >= minus(X, Y) 
  quot(0, s(X)) >= 0 
  quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) 
  le(0, X) >= true 
  le(s(X), 0) >= false 
  le(s(X), s(Y)) >= le(X, Y) 
  app(nil, X) >= X 
  app(add(X, Y), Z) >= add(X, app(Y, Z)) 
  low(X, nil) >= nil 
  low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) 
  if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) 
  if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) 
  high(X, nil) >= nil 
  high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) 
  if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) 
  if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) 
  quicksort(nil) >= nil 
  quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) 
  map(F, nil) >= nil 
  map(F, add(X, Y)) >= add(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, add(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= add(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 
  [[false]] = _|_ 
  [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_3, x_1) 
  [[filter2#(x_1, x_2, x_3, x_4)]] = filter2#(x_2, x_4) 
  [[high(x_1, x_2)]] = high(x_2) 
  [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) 
  [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) 
  [[low(x_1, x_2)]] = low(x_2) 
  [[minus(x_1, x_2)]] = x_1 
  [[nil]] = _|_ 
  [[s(x_1)]] = x_1 
  [[true]] = _|_ 

We choose Lex = {filter, filter2} and Mul = {@_{o -> o}, add, app, filter2#, filter#, high, if!fac6220high, if!fac6220low, le, low, map, map#, quicksort, quot}, and the following precedence: filter = filter2 > le > map > quicksort > app > quot > add = high = if!fac6220high = if!fac6220low = low > filter2# = filter# > map# > @_{o -> o}

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  map#(F, add(X, Y)) >= @_{o -> o}(F, X) 
  map#(F, add(X, Y)) >= map#(F, Y) 
  filter#(F, add(X, Y)) >= filter2#(F, Y) 
  filter#(F, add(X, Y)) > @_{o -> o}(F, X) 
  filter2#(F, X) >= filter#(F, X) 
  filter2#(F, X) >= filter#(F, X) 
  X >= X 
  X >= X 
  quot(_|_, X) >= _|_ 
  quot(X, Y) >= quot(X, Y) 
  le(_|_, X) >= _|_ 
  le(X, _|_) >= _|_ 
  le(X, Y) >= le(X, Y) 
  app(_|_, X) >= X 
  app(add(X, Y), Z) >= add(X, app(Y, Z)) 
  low(_|_) >= _|_ 
  low(add(X, Y)) >= if!fac6220low(add(X, Y)) 
  if!fac6220low(add(X, Y)) >= add(X, low(Y)) 
  if!fac6220low(add(X, Y)) >= low(Y) 
  high(_|_) >= _|_ 
  high(add(X, Y)) >= if!fac6220high(add(X, Y)) 
  if!fac6220high(add(X, Y)) >= high(Y) 
  if!fac6220high(add(X, Y)) >= add(X, high(Y)) 
  quicksort(_|_) >= _|_ 
  quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) 
  map(F, _|_) >= _|_ 
  map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) 
  filter(F, _|_) >= _|_ 
  filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) 
  filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) 
  filter2(_|_, F, X, Y) >= filter(F, Y) 

With these choices, we have:

  1] map#(F, add(X, Y)) >= @_{o -> o}(F, X)  because [2], by (Star) 
  2] map#*(F, add(X, Y)) >= @_{o -> o}(F, X)  because map# > @_{o -> o}, [3] and [5], by (Copy) 
  3] map#*(F, add(X, Y)) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] map#*(F, add(X, Y)) >= X  because [6], by (Select) 
  6] add(X, Y) >= X  because [7], by (Star) 
  7] add*(X, Y) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 

  9] map#(F, add(X, Y)) >= map#(F, Y)  because map# in Mul, [10] and [11], by (Fun) 
  10] F >= F  by (Meta) 
  11] add(X, Y) >= Y  because [12], by (Star) 
  12] add*(X, Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 

  14] filter#(F, add(X, Y)) >= filter2#(F, Y)  because filter# = filter2#, filter# in Mul, [15] and [16], by (Fun) 
  15] F >= F  by (Meta) 
  16] add(X, Y) >= Y  because [17], by (Star) 
  17] add*(X, Y) >= Y  because [18], by (Select) 
  18] Y >= Y  by (Meta) 

  19] filter#(F, add(X, Y)) > @_{o -> o}(F, X)  because [20], by definition 
  20] filter#*(F, add(X, Y)) >= @_{o -> o}(F, X)  because filter# > @_{o -> o}, [21] and [22], by (Copy) 
  21] filter#*(F, add(X, Y)) >= F  because [15], by (Select) 
  22] filter#*(F, add(X, Y)) >= X  because [23], by (Select) 
  23] add(X, Y) >= X  because [24], by (Star) 
  24] add*(X, Y) >= X  because [25], by (Select) 
  25] X >= X  by (Meta) 

  26] filter2#(F, X) >= filter#(F, X)  because filter2# = filter#, filter2# in Mul, [27] and [28], by (Fun) 
  27] F >= F  by (Meta) 
  28] X >= X  by (Meta) 

  29] filter2#(F, X) >= filter#(F, X)  because filter2# = filter#, filter2# in Mul, [30] and [31], by (Fun) 
  30] F >= F  by (Meta) 
  31] X >= X  by (Meta) 

  32] X >= X  by (Meta) 

  33] X >= X  by (Meta) 

  34] quot(_|_, X) >= _|_  by (Bot) 

  35] quot(X, Y) >= quot(X, Y)  because quot in Mul, [36] and [37], by (Fun) 
  36] X >= X  by (Meta) 
  37] Y >= Y  by (Meta) 

  38] le(_|_, X) >= _|_  by (Bot) 

  39] le(X, _|_) >= _|_  by (Bot) 

  40] le(X, Y) >= le(X, Y)  because le in Mul, [41] and [42], by (Fun) 
  41] X >= X  by (Meta) 
  42] Y >= Y  by (Meta) 

  43] app(_|_, X) >= X  because [44], by (Star) 
  44] app*(_|_, X) >= X  because [45], by (Select) 
  45] X >= X  by (Meta) 

  46] app(add(X, Y), Z) >= add(X, app(Y, Z))  because [47], by (Star) 
  47] app*(add(X, Y), Z) >= add(X, app(Y, Z))  because app > add, [48] and [52], by (Copy) 
  48] app*(add(X, Y), Z) >= X  because [49], by (Select) 
  49] add(X, Y) >= X  because [50], by (Star) 
  50] add*(X, Y) >= X  because [51], by (Select) 
  51] X >= X  by (Meta) 
  52] app*(add(X, Y), Z) >= app(Y, Z)  because app in Mul, [53] and [56], by (Stat) 
  53] add(X, Y) > Y  because [54], by definition 
  54] add*(X, Y) >= Y  because [55], by (Select) 
  55] Y >= Y  by (Meta) 
  56] Z >= Z  by (Meta) 

  57] low(_|_) >= _|_  by (Bot) 

  58] low(add(X, Y)) >= if!fac6220low(add(X, Y))  because low = if!fac6220low, low in Mul and [59], by (Fun) 
  59] add(X, Y) >= add(X, Y)  because add in Mul, [60] and [61], by (Fun) 
  60] X >= X  by (Meta) 
  61] Y >= Y  by (Meta) 

  62] if!fac6220low(add(X, Y)) >= add(X, low(Y))  because [63], by (Star) 
  63] if!fac6220low*(add(X, Y)) >= add(X, low(Y))  because if!fac6220low = add, if!fac6220low in Mul, [64] and [67], by (Stat) 
  64] add(X, Y) > X  because [65], by definition 
  65] add*(X, Y) >= X  because [66], by (Select) 
  66] X >= X  by (Meta) 
  67] add(X, Y) > low(Y)  because [68], by definition 
  68] add*(X, Y) >= low(Y)  because add = low, add in Mul and [69], by (Stat) 
  69] Y >= Y  by (Meta) 

  70] if!fac6220low(add(X, Y)) >= low(Y)  because if!fac6220low = low, if!fac6220low in Mul and [71], by (Fun) 
  71] add(X, Y) >= Y  because [72], by (Star) 
  72] add*(X, Y) >= Y  because [73], by (Select) 
  73] Y >= Y  by (Meta) 

  74] high(_|_) >= _|_  by (Bot) 

  75] high(add(X, Y)) >= if!fac6220high(add(X, Y))  because high = if!fac6220high, high in Mul and [76], by (Fun) 
  76] add(X, Y) >= add(X, Y)  because add in Mul, [77] and [78], by (Fun) 
  77] X >= X  by (Meta) 
  78] Y >= Y  by (Meta) 

  79] if!fac6220high(add(X, Y)) >= high(Y)  because if!fac6220high = high, if!fac6220high in Mul and [80], by (Fun) 
  80] add(X, Y) >= Y  because [81], by (Star) 
  81] add*(X, Y) >= Y  because [82], by (Select) 
  82] Y >= Y  by (Meta) 

  83] if!fac6220high(add(X, Y)) >= add(X, high(Y))  because [84], by (Star) 
  84] if!fac6220high*(add(X, Y)) >= add(X, high(Y))  because if!fac6220high = add, if!fac6220high in Mul, [85] and [88], by (Stat) 
  85] add(X, Y) > X  because [86], by definition 
  86] add*(X, Y) >= X  because [87], by (Select) 
  87] X >= X  by (Meta) 
  88] add(X, Y) > high(Y)  because [89], by definition 
  89] add*(X, Y) >= high(Y)  because add = high, add in Mul and [90], by (Stat) 
  90] Y >= Y  by (Meta) 

  91] quicksort(_|_) >= _|_  by (Bot) 

  92] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y))))  because [93], by (Star) 
  93] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y))))  because quicksort > app, [94] and [98], by (Copy) 
  94] quicksort*(add(X, Y)) >= quicksort(low(Y))  because quicksort in Mul and [95], by (Stat) 
  95] add(X, Y) > low(Y)  because [96], by definition 
  96] add*(X, Y) >= low(Y)  because add = low, add in Mul and [97], by (Stat) 
  97] Y >= Y  by (Meta) 
  98] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y)))  because quicksort > add, [99] and [103], by (Copy) 
  99] quicksort*(add(X, Y)) >= X  because [100], by (Select) 
  100] add(X, Y) >= X  because [101], by (Star) 
  101] add*(X, Y) >= X  because [102], by (Select) 
  102] X >= X  by (Meta) 
  103] quicksort*(add(X, Y)) >= quicksort(high(Y))  because quicksort in Mul and [104], by (Stat) 
  104] add(X, Y) > high(Y)  because [105], by definition 
  105] add*(X, Y) >= high(Y)  because add = high, add in Mul and [97], by (Stat) 

  106] map(F, _|_) >= _|_  by (Bot) 

  107] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y))  because [108], by (Star) 
  108] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y))  because map > add, [109] and [112], by (Copy) 
  109] map*(F, add(X, Y)) >= @_{o -> o}(F, X)  because map > @_{o -> o}, [110] and [111], by (Copy) 
  110] map*(F, add(X, Y)) >= F  because [10], by (Select) 
  111] map*(F, add(X, Y)) >= X  because [6], by (Select) 
  112] map*(F, add(X, Y)) >= map(F, Y)  because map in Mul, [10] and [113], by (Stat) 
  113] add(X, Y) > Y  because [114], by definition 
  114] add*(X, Y) >= Y  because [13], by (Select) 

  115] filter(F, _|_) >= _|_  by (Bot) 

  116] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y)  because [117], by (Star) 
  117] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y)  because filter = filter2, [15], [118], [120], [121], [122] and [123], by (Stat) 
  118] add(X, Y) > Y  because [119], by definition 
  119] add*(X, Y) >= Y  because [18], by (Select) 
  120] filter*(F, add(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [121] and [122], by (Copy) 
  121] filter*(F, add(X, Y)) >= F  because [15], by (Select) 
  122] filter*(F, add(X, Y)) >= X  because [23], by (Select) 
  123] filter*(F, add(X, Y)) >= Y  because [16], by (Select) 

  124] filter2(_|_, F, X, Y) >= add(X, filter(F, Y))  because [125], by (Star) 
  125] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y))  because filter2 > add, [126] and [128], by (Copy) 
  126] filter2*(_|_, F, X, Y) >= X  because [127], by (Select) 
  127] X >= X  by (Meta) 
  128] filter2*(_|_, F, X, Y) >= filter(F, Y)  because filter2 = filter, [27], [28], [129] and [130], by (Stat) 
  129] filter2*(_|_, F, X, Y) >= F  because [27], by (Select) 
  130] filter2*(_|_, F, X, Y) >= Y  because [28], by (Select) 

  131] filter2(_|_, F, X, Y) >= filter(F, Y)  because [132], by (Star) 
  132] filter2*(_|_, F, X, Y) >= filter(F, Y)  because filter2 = filter, [30], [31], [133] and [134], by (Stat) 
  133] filter2*(_|_, F, X, Y) >= F  because [30], by (Select) 
  134] filter2*(_|_, F, X, Y) >= Y  because [31], by (Select) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, minimal, formative) by (P_1, R_0, minimal, formative), where P_1 consists of:

  map#(F, add(X, Y)) =#> F(X)   
  map#(F, add(X, Y)) =#> map#(F, Y)   
  filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y)   
  filter2#(true, F, X, Y) =#> filter#(F, Y)   
  filter2#(false, F, X, Y) =#> filter#(F, Y)   

Thus, the original system is terminating if (P_1, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_1, R_0, minimal, formative).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 : 0, 1, 2, 3, 4 
    * 1 : 0, 1 
    * 2 : 3, 4 
    * 3 : 2 
    * 4 : 2 

This graph has the following strongly connected components:

  P_2:

    map#(F, add(X, Y)) =#> F(X)   
    map#(F, add(X, Y)) =#> map#(F, Y)   

  P_3:

    filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y)   
    filter2#(true, F, X, Y) =#> filter#(F, Y)   
    filter2#(false, F, X, Y) =#> filter#(F, Y)   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_1, R_0, m, f) by (P_2, R_0, m, f) and (P_3, R_0, m, f).

Thus, the original system is terminating if each of (P_2, R_0, minimal, formative) and (P_3, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_3, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(filter2#) = 4 
  nu(filter#) = 2 

Thus, we can orient the dependency pairs as follows:

  nu(filter#(F, add(X, Y))) = add(X, Y) |> Y = nu(filter2#(F X, F, X, Y)) 
  nu(filter2#(true, F, X, Y)) = Y = Y = nu(filter#(F, Y)) 
  nu(filter2#(false, F, X, Y)) = Y = Y = nu(filter#(F, Y)) 

By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_3, R_0, minimal, f) by (P_4, R_0, minimal, f), where P_4 contains:

  filter2#(true, F, X, Y) =#> filter#(F, Y)   
  filter2#(false, F, X, Y) =#> filter#(F, Y)   

Thus, the original system is terminating if each of (P_2, R_0, minimal, formative) and (P_4, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_4, R_0, minimal, formative).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 :  
    * 1 :  

This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

Thus, the original system is terminating if (P_2, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_2, R_0, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  map#(F, add(X, Y)) >? F(X) 
  map#(F, add(X, Y)) >? map#(F, Y) 
  minus(X, 0) >= X 
  minus(s(X), s(Y)) >= minus(X, Y) 
  quot(0, s(X)) >= 0 
  quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) 
  le(0, X) >= true 
  le(s(X), 0) >= false 
  le(s(X), s(Y)) >= le(X, Y) 
  app(nil, X) >= X 
  app(add(X, Y), Z) >= add(X, app(Y, Z)) 
  low(X, nil) >= nil 
  low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) 
  if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) 
  if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) 
  high(X, nil) >= nil 
  high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) 
  if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) 
  if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) 
  quicksort(nil) >= nil 
  quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) 
  map(F, nil) >= nil 
  map(F, add(X, Y)) >= add(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, add(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= add(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 
  [[filter(x_1, x_2)]] = x_2 
  [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_3, x_4) 
  [[high(x_1, x_2)]] = x_2 
  [[if!fac6220high(x_1, x_2, x_3)]] = x_3 
  [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) 
  [[low(x_1, x_2)]] = low(x_2) 
  [[minus(x_1, x_2)]] = x_1 
  [[nil]] = _|_ 
  [[s(x_1)]] = x_1 

We choose Lex = {} and Mul = {@_{o -> o}, add, app, false, filter2, if!fac6220low, le, low, map, map#, quicksort, quot, true}, and the following precedence: map > quicksort > le > app > add = filter2 = if!fac6220low = low > true > false > @_{o -> o} = map# > quot

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  map#(F, add(X, Y)) > @_{o -> o}(F, X) 
  map#(F, add(X, Y)) >= map#(F, Y) 
  X >= X 
  X >= X 
  quot(_|_, X) >= _|_ 
  quot(X, Y) >= quot(X, Y) 
  le(_|_, X) >= true 
  le(X, _|_) >= false 
  le(X, Y) >= le(X, Y) 
  app(_|_, X) >= X 
  app(add(X, Y), Z) >= add(X, app(Y, Z)) 
  low(_|_) >= _|_ 
  low(add(X, Y)) >= if!fac6220low(add(X, Y)) 
  if!fac6220low(add(X, Y)) >= add(X, low(Y)) 
  if!fac6220low(add(X, Y)) >= low(Y) 
  _|_ >= _|_ 
  add(X, Y) >= add(X, Y) 
  add(X, Y) >= Y 
  add(X, Y) >= add(X, Y) 
  quicksort(_|_) >= _|_ 
  quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y))) 
  map(F, _|_) >= _|_ 
  map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) 
  _|_ >= _|_ 
  add(X, Y) >= filter2(X, Y) 
  filter2(X, Y) >= add(X, Y) 
  filter2(X, Y) >= Y 

With these choices, we have:

  1] map#(F, add(X, Y)) > @_{o -> o}(F, X)  because [2], by definition 
  2] map#*(F, add(X, Y)) >= @_{o -> o}(F, X)  because map# = @_{o -> o}, map# in Mul, [3] and [4], by (Stat) 
  3] F >= F  by (Meta) 
  4] add(X, Y) > X  because [5], by definition 
  5] add*(X, Y) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] map#(F, add(X, Y)) >= map#(F, Y)  because map# in Mul, [3] and [8], by (Fun) 
  8] add(X, Y) >= Y  because [9], by (Star) 
  9] add*(X, Y) >= Y  because [10], by (Select) 
  10] Y >= Y  by (Meta) 

  11] X >= X  by (Meta) 

  12] X >= X  by (Meta) 

  13] quot(_|_, X) >= _|_  by (Bot) 

  14] quot(X, Y) >= quot(X, Y)  because quot in Mul, [15] and [16], by (Fun) 
  15] X >= X  by (Meta) 
  16] Y >= Y  by (Meta) 

  17] le(_|_, X) >= true  because [18], by (Star) 
  18] le*(_|_, X) >= true  because le > true, by (Copy) 

  19] le(X, _|_) >= false  because [20], by (Star) 
  20] le*(X, _|_) >= false  because le > false, by (Copy) 

  21] le(X, Y) >= le(X, Y)  because le in Mul, [22] and [23], by (Fun) 
  22] X >= X  by (Meta) 
  23] Y >= Y  by (Meta) 

  24] app(_|_, X) >= X  because [25], by (Star) 
  25] app*(_|_, X) >= X  because [26], by (Select) 
  26] X >= X  by (Meta) 

  27] app(add(X, Y), Z) >= add(X, app(Y, Z))  because [28], by (Star) 
  28] app*(add(X, Y), Z) >= add(X, app(Y, Z))  because app > add, [29] and [33], by (Copy) 
  29] app*(add(X, Y), Z) >= X  because [30], by (Select) 
  30] add(X, Y) >= X  because [31], by (Star) 
  31] add*(X, Y) >= X  because [32], by (Select) 
  32] X >= X  by (Meta) 
  33] app*(add(X, Y), Z) >= app(Y, Z)  because app in Mul, [34] and [37], by (Stat) 
  34] add(X, Y) > Y  because [35], by definition 
  35] add*(X, Y) >= Y  because [36], by (Select) 
  36] Y >= Y  by (Meta) 
  37] Z >= Z  by (Meta) 

  38] low(_|_) >= _|_  by (Bot) 

  39] low(add(X, Y)) >= if!fac6220low(add(X, Y))  because low = if!fac6220low, low in Mul and [40], by (Fun) 
  40] add(X, Y) >= add(X, Y)  because add in Mul, [41] and [42], by (Fun) 
  41] X >= X  by (Meta) 
  42] Y >= Y  by (Meta) 

  43] if!fac6220low(add(X, Y)) >= add(X, low(Y))  because [44], by (Star) 
  44] if!fac6220low*(add(X, Y)) >= add(X, low(Y))  because if!fac6220low = add, if!fac6220low in Mul, [45] and [48], by (Stat) 
  45] add(X, Y) > X  because [46], by definition 
  46] add*(X, Y) >= X  because [47], by (Select) 
  47] X >= X  by (Meta) 
  48] add(X, Y) > low(Y)  because [49], by definition 
  49] add*(X, Y) >= low(Y)  because add = low, add in Mul and [50], by (Stat) 
  50] Y >= Y  by (Meta) 

  51] if!fac6220low(add(X, Y)) >= low(Y)  because [52], by (Star) 
  52] if!fac6220low*(add(X, Y)) >= low(Y)  because if!fac6220low = low, if!fac6220low in Mul and [53], by (Stat) 
  53] add(X, Y) > Y  because [54], by definition 
  54] add*(X, Y) >= Y  because [55], by (Select) 
  55] Y >= Y  by (Meta) 

  56] _|_ >= _|_  by (Bot) 

  57] add(X, Y) >= add(X, Y)  because add in Mul, [58] and [59], by (Fun) 
  58] X >= X  by (Meta) 
  59] Y >= Y  by (Meta) 

  60] add(X, Y) >= Y  because [61], by (Star) 
  61] add*(X, Y) >= Y  because [62], by (Select) 
  62] Y >= Y  by (Meta) 

  63] add(X, Y) >= add(X, Y)  because add in Mul, [64] and [65], by (Fun) 
  64] X >= X  by (Meta) 
  65] Y >= Y  by (Meta) 

  66] quicksort(_|_) >= _|_  by (Bot) 

  67] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y)))  because [68], by (Star) 
  68] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y)))  because quicksort > app, [69] and [73], by (Copy) 
  69] quicksort*(add(X, Y)) >= quicksort(low(Y))  because quicksort in Mul and [70], by (Stat) 
  70] add(X, Y) > low(Y)  because [71], by definition 
  71] add*(X, Y) >= low(Y)  because add = low, add in Mul and [72], by (Stat) 
  72] Y >= Y  by (Meta) 
  73] quicksort*(add(X, Y)) >= add(X, quicksort(Y))  because quicksort > add, [74] and [78], by (Copy) 
  74] quicksort*(add(X, Y)) >= X  because [75], by (Select) 
  75] add(X, Y) >= X  because [76], by (Star) 
  76] add*(X, Y) >= X  because [77], by (Select) 
  77] X >= X  by (Meta) 
  78] quicksort*(add(X, Y)) >= quicksort(Y)  because quicksort in Mul and [79], by (Stat) 
  79] add(X, Y) > Y  because [80], by definition 
  80] add*(X, Y) >= Y  because [72], by (Select) 

  81] map(F, _|_) >= _|_  by (Bot) 

  82] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y))  because [83], by (Star) 
  83] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y))  because map > add, [84] and [88], by (Copy) 
  84] map*(F, add(X, Y)) >= @_{o -> o}(F, X)  because map > @_{o -> o}, [85] and [86], by (Copy) 
  85] map*(F, add(X, Y)) >= F  because [3], by (Select) 
  86] map*(F, add(X, Y)) >= X  because [87], by (Select) 
  87] add(X, Y) >= X  because [5], by (Star) 
  88] map*(F, add(X, Y)) >= map(F, Y)  because map in Mul, [3] and [89], by (Stat) 
  89] add(X, Y) > Y  because [90], by definition 
  90] add*(X, Y) >= Y  because [10], by (Select) 

  91] _|_ >= _|_  by (Bot) 

  92] add(X, Y) >= filter2(X, Y)  because add = filter2, add in Mul, [93] and [94], by (Fun) 
  93] X >= X  by (Meta) 
  94] Y >= Y  by (Meta) 

  95] filter2(X, Y) >= add(X, Y)  because filter2 = add, filter2 in Mul, [96] and [97], by (Fun) 
  96] X >= X  by (Meta) 
  97] Y >= Y  by (Meta) 

  98] filter2(X, Y) >= Y  because [99], by (Star) 
  99] filter2*(X, Y) >= Y  because [100], by (Select) 
  100] Y >= Y  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_0, minimal, formative) by (P_5, R_0, minimal, formative), where P_5 consists of:

  map#(F, add(X, Y)) =#> map#(F, Y)   

Thus, the original system is terminating if (P_5, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_5, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(map#) = 2 

Thus, we can orient the dependency pairs as follows:

  nu(map#(F, add(X, Y))) = add(X, Y) |> Y = nu(map#(F, Y)) 

By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_5, R_0, minimal, f) by ({}, R_0, minimal, f).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

[FuhKop19]  C. Fuhs, and C. Kop.  A static higher-order dependency pair framework.  In Proceedings of ESOP 2019, 2019.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.