MAYBE Problem: app'(app'(eq(),0()),0()) -> true() app'(app'(eq(),0()),app'(s(),x)) -> false() app'(app'(eq(),app'(s(),x)),0()) -> false() app'(app'(eq(),app'(s(),x)),app'(s(),y)) -> app'(app'(eq(),x),y) app'(app'(le(),0()),y) -> true() app'(app'(le(),app'(s(),x)),0()) -> false() app'(app'(le(),app'(s(),x)),app'(s(),y)) -> app'(app'(le(),x),y) app'(app'(app(),nil()),y) -> y app'(app'(app(),app'(app'(add(),n),x)),y) -> app'(app'(add(),n),app'(app'(app(),x),y)) app'(min(),app'(app'(add(),n),nil())) -> n app'(min(),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(app'(if_min(),app'(app'(le(),n),m)),app'(app'(add(),n),app'(app'(add(),m),x))) app'(app'(if_min(),true()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(min(),app'(app'(add(),n),x)) app'(app'(if_min(),false()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(min(),app'(app'(add(),m),x)) app'(app'(rm(),n),nil()) -> nil() app'(app'(rm(),n),app'(app'(add(),m),x)) -> app'(app'(app'(if_rm(),app'(app'(eq(),n),m)),n),app'(app'(add(),m),x)) app'(app'(app'(if_rm(),true()),n),app'(app'(add(),m),x)) -> app'(app'(rm(),n),x) app'(app'(app'(if_rm(),false()),n),app'(app'(add(),m),x)) -> app'(app'(add(),m),app'(app'(rm(),n),x)) app'(app'(minsort(),nil()),nil()) -> nil() app'(app'(minsort(),app'(app'(add(),n),x)),y) -> app'(app'(app'(if_minsort(),app'(app'(eq(),n),app'(min(),app'(app'(add(),n),x)))), app'(app'(add(),n),x)),y) app'(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'(app'(add(),n),app'(app'(minsort(),app'(app'(app(),app'(app'(rm(),n),x)),y)),nil())) app'(app'(app'(if_minsort(),false()),app'(app'(add(),n),x)),y) -> app'(app'(minsort(),x),app'(app'(add(),n),y)) app'(app'(map(),f),nil()) -> nil() app'(app'(map(),f),app'(app'(add(),x),xs)) -> app'(app'(add(),app'(f,x)),app'(app'(map(),f),xs)) app'(app'(filter(),f),nil()) -> nil() app'(app'(filter(),f),app'(app'(add(),x),xs)) -> app'(app'(app'(app'(filter2(),app'(f,x)),f),x),xs) app'(app'(app'(app'(filter2(),true()),f),x),xs) -> app'(app'(add(),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(),x)),app'(s(),y)) -> app'#(eq(),x) app'#(app'(eq(),app'(s(),x)),app'(s(),y)) -> app'#(app'(eq(),x),y) app'#(app'(le(),app'(s(),x)),app'(s(),y)) -> app'#(le(),x) app'#(app'(le(),app'(s(),x)),app'(s(),y)) -> app'#(app'(le(),x),y) app'#(app'(app(),app'(app'(add(),n),x)),y) -> app'#(app(),x) app'#(app'(app(),app'(app'(add(),n),x)),y) -> app'#(app'(app(),x),y) app'#(app'(app(),app'(app'(add(),n),x)),y) -> app'#(app'(add(),n),app'(app'(app(),x),y)) app'#(min(),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'#(le(),n) app'#(min(),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'#(app'(le(),n),m) app'#(min(),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'#(if_min(),app'(app'(le(),n),m)) app'#(min(),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'#(app'(if_min(),app'(app'(le(),n),m)),app'(app'(add(),n),app'(app'(add(),m),x))) app'#(app'(if_min(),true()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'#(app'(add(),n),x) app'#(app'(if_min(),true()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'#(min(),app'(app'(add(),n),x)) app'#(app'(if_min(),false()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'#(min(),app'(app'(add(),m),x)) app'#(app'(rm(),n),app'(app'(add(),m),x)) -> app'#(eq(),n) app'#(app'(rm(),n),app'(app'(add(),m),x)) -> app'#(app'(eq(),n),m) app'#(app'(rm(),n),app'(app'(add(),m),x)) -> app'#(if_rm(),app'(app'(eq(),n),m)) app'#(app'(rm(),n),app'(app'(add(),m),x)) -> app'#(app'(if_rm(),app'(app'(eq(),n),m)),n) app'#(app'(rm(),n),app'(app'(add(),m),x)) -> app'#(app'(app'(if_rm(),app'(app'(eq(),n),m)),n),app'(app'(add(),m),x)) app'#(app'(app'(if_rm(),true()),n),app'(app'(add(),m),x)) -> app'#(rm(),n) app'#(app'(app'(if_rm(),true()),n),app'(app'(add(),m),x)) -> app'#(app'(rm(),n),x) app'#(app'(app'(if_rm(),false()),n),app'(app'(add(),m),x)) -> app'#(rm(),n) app'#(app'(app'(if_rm(),false()),n),app'(app'(add(),m),x)) -> app'#(app'(rm(),n),x) app'#(app'(app'(if_rm(),false()),n),app'(app'(add(),m),x)) -> app'#(app'(add(),m),app'(app'(rm(),n),x)) app'#(app'(minsort(),app'(app'(add(),n),x)),y) -> app'#(min(),app'(app'(add(),n),x)) app'#(app'(minsort(),app'(app'(add(),n),x)),y) -> app'#(eq(),n) app'#(app'(minsort(),app'(app'(add(),n),x)),y) -> app'#(app'(eq(),n),app'(min(),app'(app'(add(),n),x))) app'#(app'(minsort(),app'(app'(add(),n),x)),y) -> app'#(if_minsort(),app'(app'(eq(),n),app'(min(),app'(app'(add(),n),x)))) app'#(app'(minsort(),app'(app'(add(),n),x)),y) -> app'#(app'(if_minsort(),app'(app'(eq(),n),app'(min(),app'(app'(add(),n),x)))), app'(app'(add(),n),x)) app'#(app'(minsort(),app'(app'(add(),n),x)),y) -> app'#(app'(app'(if_minsort(),app'(app'(eq(),n),app'(min(),app'(app'(add(),n),x)))), app'(app'(add(),n),x)),y) app'#(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'#(rm(),n) app'#(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'#(app'(rm(),n),x) app'#(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'#(app(),app'(app'(rm(),n),x)) app'#(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'#(app'(app(),app'(app'(rm(),n),x)),y) app'#(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'#(minsort(),app'(app'(app(),app'(app'(rm(),n),x)),y)) app'#(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'#(app'(minsort(),app'(app'(app(),app'(app'(rm(),n),x)),y)),nil()) app'#(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'#(app'(add(),n),app'(app'(minsort(),app'(app'(app(),app'(app'(rm(),n),x)),y)),nil())) app'#(app'(app'(if_minsort(),false()),app'(app'(add(),n),x)),y) -> app'#(app'(add(),n),y) app'#(app'(app'(if_minsort(),false()),app'(app'(add(),n),x)),y) -> app'#(minsort(),x) app'#(app'(app'(if_minsort(),false()),app'(app'(add(),n),x)),y) -> app'#(app'(minsort(),x),app'(app'(add(),n),y)) app'#(app'(map(),f),app'(app'(add(),x),xs)) -> app'#(app'(map(),f),xs) app'#(app'(map(),f),app'(app'(add(),x),xs)) -> app'#(f,x) app'#(app'(map(),f),app'(app'(add(),x),xs)) -> app'#(add(),app'(f,x)) app'#(app'(map(),f),app'(app'(add(),x),xs)) -> app'#(app'(add(),app'(f,x)),app'(app'(map(),f),xs)) app'#(app'(filter(),f),app'(app'(add(),x),xs)) -> app'#(f,x) app'#(app'(filter(),f),app'(app'(add(),x),xs)) -> app'#(filter2(),app'(f,x)) app'#(app'(filter(),f),app'(app'(add(),x),xs)) -> app'#(app'(filter2(),app'(f,x)),f) app'#(app'(filter(),f),app'(app'(add(),x),xs)) -> app'#(app'(app'(filter2(),app'(f,x)),f),x) app'#(app'(filter(),f),app'(app'(add(),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'#(add(),x) app'#(app'(app'(app'(filter2(),true()),f),x),xs) -> app'#(app'(add(),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(),x)) -> false() app'(app'(eq(),app'(s(),x)),0()) -> false() app'(app'(eq(),app'(s(),x)),app'(s(),y)) -> app'(app'(eq(),x),y) app'(app'(le(),0()),y) -> true() app'(app'(le(),app'(s(),x)),0()) -> false() app'(app'(le(),app'(s(),x)),app'(s(),y)) -> app'(app'(le(),x),y) app'(app'(app(),nil()),y) -> y app'(app'(app(),app'(app'(add(),n),x)),y) -> app'(app'(add(),n),app'(app'(app(),x),y)) app'(min(),app'(app'(add(),n),nil())) -> n app'(min(),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(app'(if_min(),app'(app'(le(),n),m)),app'(app'(add(),n),app'(app'(add(),m),x))) app'(app'(if_min(),true()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(min(),app'(app'(add(),n),x)) app'(app'(if_min(),false()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(min(),app'(app'(add(),m),x)) app'(app'(rm(),n),nil()) -> nil() app'(app'(rm(),n),app'(app'(add(),m),x)) -> app'(app'(app'(if_rm(),app'(app'(eq(),n),m)),n),app'(app'(add(),m),x)) app'(app'(app'(if_rm(),true()),n),app'(app'(add(),m),x)) -> app'(app'(rm(),n),x) app'(app'(app'(if_rm(),false()),n),app'(app'(add(),m),x)) -> app'(app'(add(),m),app'(app'(rm(),n),x)) app'(app'(minsort(),nil()),nil()) -> nil() app'(app'(minsort(),app'(app'(add(),n),x)),y) -> app'(app'(app'(if_minsort(),app'(app'(eq(),n),app'(min(),app'(app'(add(),n),x)))), app'(app'(add(),n),x)),y) app'(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'(app'(add(),n),app'(app'(minsort(),app'(app'(app(),app'(app'(rm(),n),x)),y)),nil())) app'(app'(app'(if_minsort(),false()),app'(app'(add(),n),x)),y) -> app'(app'(minsort(),x),app'(app'(add(),n),y)) app'(app'(map(),f),nil()) -> nil() app'(app'(map(),f),app'(app'(add(),x),xs)) -> app'(app'(add(),app'(f,x)),app'(app'(map(),f),xs)) app'(app'(filter(),f),nil()) -> nil() app'(app'(filter(),f),app'(app'(add(),x),xs)) -> app'(app'(app'(app'(filter2(),app'(f,x)),f),x),xs) app'(app'(app'(app'(filter2(),true()),f),x),xs) -> app'(app'(add(),x),app'(app'(filter(),f),xs)) app'(app'(app'(app'(filter2(),false()),f),x),xs) -> app'(app'(filter(),f),xs) Open