MAYBE
Problem:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app(app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
Proof:
DP Processor:
DPs:
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(eq(),n)
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m)
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(le(),n)
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m)
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(le(),n)
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m)
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(if_min(),app(app(le(),n),m))
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(cons(),n),x)
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x))
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x))
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(eq(),n)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(app(eq(),n),k)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(if_replace(),app(app(eq(),n),k))
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(if_replace(),app(app(eq(),n),k)),n)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(if_replace(),app(app(eq(),n),k)),n),m)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(cons(),m)
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(app(cons(),m),x)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(replace(),n)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(app(replace(),n),m)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(cons(),k),app(app(app(replace(),n),m),x))
app#(sort(),app(app(cons(),n),x)) -> app#(replace(),app(min(),app(app(cons(),n),x)))
app#(sort(),app(app(cons(),n),x)) -> app#(app(replace(),app(min(),app(app(cons(),n),x))),n)
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x))
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x))
app#(sort(),app(app(cons(),n),x)) -> app#(cons(),app(min(),app(app(cons(),n),x)))
app#(sort(),app(app(cons(),n),x)) ->
app#(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(filter(),f)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(cons(),x)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(cons(),x),app(app(filter(),f),xs))
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(filter(),f)
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs)
TRS:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(app
(replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
EDG Processor:
DPs:
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(eq(),n)
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m)
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(le(),n)
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m)
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(le(),n)
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m)
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(if_min(),app(app(le(),n),m))
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(cons(),n),x)
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x))
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x))
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(eq(),n)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(app(eq(),n),k)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(if_replace(),app(app(eq(),n),k))
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(if_replace(),app(app(eq(),n),k)),n)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(if_replace(),app(app(eq(),n),k)),n),m)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(cons(),m)
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(app(cons(),m),x)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(replace(),n)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(app(replace(),n),m)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(cons(),k),app(app(app(replace(),n),m),x))
app#(sort(),app(app(cons(),n),x)) -> app#(replace(),app(min(),app(app(cons(),n),x)))
app#(sort(),app(app(cons(),n),x)) -> app#(app(replace(),app(min(),app(app(cons(),n),x))),n)
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x))
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x))
app#(sort(),app(app(cons(),n),x)) -> app#(cons(),app(min(),app(app(cons(),n),x)))
app#(sort(),app(app(cons(),n),x)) ->
app#(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(filter(),f)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(cons(),x)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(cons(),x),app(app(filter(),f),xs))
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(filter(),f)
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs)
TRS:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
graph:
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)) ->
app#(sort(),app(app(cons(),n),x)) -> app#(replace(),app(min(),app(app(cons(),n),x)))
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)) ->
app#(sort(),app(app(cons(),n),x)) -> app#(app(replace(),app(min(),app(app(cons(),n),x))),n)
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x))
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)) ->
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x))
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)) ->
app#(sort(),app(app(cons(),n),x)) -> app#(cons(),app(min(),app(app(cons(),n),x)))
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(le(),n)
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m)
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(if_min(),app(app(le(),n),m))
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(eq(),n)
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(app(eq(),n),k)
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(if_replace(),app(app(eq(),n),k))
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(if_replace(),app(app(eq(),n),k)),n)
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(if_replace(),app(app(eq(),n),k)),n),m)
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(cons(),n),x)
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x))
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x))
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m) ->
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(le(),n)
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m) ->
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(filter(),f)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(cons(),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(cons(),x),app(app(filter(),f),xs))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
->
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(filter(),f)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
->
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(eq(),n)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(le(),n)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(le(),n)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(if_min(),app(app(le(),n),m))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(cons(),n),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(eq(),n)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(app(eq(),n),k)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(if_replace(),app(app(eq(),n),k))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(if_replace(),app(app(eq(),n),k)),n)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(if_replace(),app(app(eq(),n),k)),n),m)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(cons(),m)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(app(cons(),m),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(replace(),n)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(app(replace(),n),m)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(cons(),k),app(app(app(replace(),n),m),x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) -> app#(replace(),app(min(),app(app(cons(),n),x)))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) -> app#(app(replace(),app(min(),app(app(cons(),n),x))),n)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) -> app#(cons(),app(min(),app(app(cons(),n),x)))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(filter(),f)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(cons(),x)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(cons(),x),app(app(filter(),f),xs))
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(filter(),f)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(eq(),n)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(le(),n)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(le(),n)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(if_min(),app(app(le(),n),m))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(cons(),n),x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(eq(),n)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(app(eq(),n),k)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(if_replace(),app(app(eq(),n),k))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(if_replace(),app(app(eq(),n),k)),n)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(if_replace(),app(app(eq(),n),k)),n),m)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(cons(),m)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(app(cons(),m),x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(replace(),n)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(app(replace(),n),m)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(cons(),k),app(app(app(replace(),n),m),x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) -> app#(replace(),app(min(),app(app(cons(),n),x)))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) -> app#(app(replace(),app(min(),app(app(cons(),n),x))),n)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) -> app#(min(),app(app(cons(),n),x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) -> app#(cons(),app(min(),app(app(cons(),n),x)))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(sort(),app(app(cons(),n),x)) ->
app#(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(filter(),f)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(cons(),x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(cons(),x),app(app(filter(),f),xs))
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(filter(),f)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) ->
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(le(),n)
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m)
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(if_min(),app(app(le(),n),m))
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(le(),n)
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(app(le(),n),m)
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) -> app#(if_min(),app(app(le(),n),m))
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x)) ->
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m) ->
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(le(),n)
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m) ->
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(cons(),m)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app#(app(cons(),m),x)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(replace(),n)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) -> app#(app(replace(),n),m)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(cons(),k),app(app(app(replace(),n),m),x))
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(app(eq(),n),k) ->
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(eq(),n)
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(app(eq(),n),k) ->
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m)
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x))
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f)
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x)
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x))
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) ->
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(eq(),n)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(app(eq(),n),k)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) -> app#(if_replace(),app(app(eq(),n),k))
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(if_replace(),app(app(eq(),n),k)),n)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(if_replace(),app(app(eq(),n),k)),n),m)
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x) ->
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m) ->
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(eq(),n)
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m) ->
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m)
SCC Processor:
#sccs: 6
#rules: 14
#arcs: 158/2025
DPs:
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs)
app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x)
app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs)
TRS:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
Open
DPs:
app#(sort(),app(app(cons(),n),x)) ->
app#(sort(),app(app(app(replace(),app(min(),app(app(cons(),n),x))),n),x))
TRS:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
Open
DPs:
app#(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app#(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app#(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app#(app(app(replace(),n),m),x)
TRS:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
Open
DPs:
app#(app(eq(),app(s(),n)),app(s(),m)) -> app#(app(eq(),n),m)
TRS:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
Open
DPs:
app#(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app#(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),m),x))
app#(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app#(min(),app(app(cons(),n),x))
TRS:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
Open
DPs:
app#(app(le(),app(s(),n)),app(s(),m)) -> app#(app(le(),n),m)
TRS:
app(app(eq(),0()),0()) -> true()
app(app(eq(),0()),app(s(),m)) -> false()
app(app(eq(),app(s(),n)),0()) -> false()
app(app(eq(),app(s(),n)),app(s(),m)) -> app(app(eq(),n),m)
app(app(le(),0()),m) -> true()
app(app(le(),app(s(),n)),0()) -> false()
app(app(le(),app(s(),n)),app(s(),m)) -> app(app(le(),n),m)
app(min(),app(app(cons(),0()),nil())) -> 0()
app(min(),app(app(cons(),app(s(),n)),nil())) -> app(s(),n)
app(min(),app(app(cons(),n),app(app(cons(),m),x))) ->
app(app(if_min(),app(app(le(),n),m)),app(app(cons(),n),app(app(cons(),m),x)))
app(app(if_min(),true()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),n),x))
app(app(if_min(),false()),app(app(cons(),n),app(app(cons(),m),x))) ->
app(min(),app(app(cons(),m),x))
app(app(app(replace(),n),m),nil()) -> nil()
app(app(app(replace(),n),m),app(app(cons(),k),x)) ->
app(app(app(app(if_replace(),app(app(eq(),n),k)),n),m),app(app(cons(),k),x))
app(app(app(app(if_replace(),true()),n),m),app(app(cons(),k),x)) -> app(app(cons(),m),x)
app(app(app(app(if_replace(),false()),n),m),app(app(cons(),k),x)) ->
app(app(cons(),k),app(app(app(replace(),n),m),x))
app(sort(),nil()) -> nil()
app(sort(),app(app(cons(),n),x)) ->
app(app(cons(),app(min(),app(app(cons(),n),x))),app(sort(),app(app
(
app
(
replace(),
app
(min(),app(app(cons(),n),x))),
n),
x)))
app(app(map(),f),nil()) -> nil()
app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
app(app(filter(),f),nil()) -> nil()
app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)
Open