MAYBE Problem: app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y) app(app(lt(),0()),app(s(),y)) -> true() app(app(lt(),y),0()) -> false() app(app(eq(),x),x) -> true() app(app(eq(),app(s(),x)),0()) -> false() app(app(eq(),0()),app(s(),x)) -> false() app(app(member(),w),null()) -> false() app(app(member(),w),app(app(app(fork(),x),y),z)) -> app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app (app(if(),app(app(eq(),w),y)), true ()), app(app(member(),w),z))) Proof: DP Processor: DPs: app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(lt(),x) app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(eq(),w) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(eq(),w),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(eq(),w),y)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(eq(),w),y)),true()) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(lt(),w) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(lt(),w),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(lt(),w),y)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app( app ( app(if(),app(app(eq(),w),y)), true ()), app(app(member(),w),z))) TRS: app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y) app(app(lt(),0()),app(s(),y)) -> true() app(app(lt(),y),0()) -> false() app(app(eq(),x),x) -> true() app(app(eq(),app(s(),x)),0()) -> false() app(app(eq(),0()),app(s(),x)) -> false() app(app(member(),w),null()) -> false() app(app(member(),w),app(app(app(fork(),x),y),z)) -> app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app ( app(if(),app(app(eq(),w),y)), true ()), app(app(member(),w),z))) Restore Modifier: DPs: app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(lt(),x) app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(eq(),w) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(eq(),w),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(eq(),w),y)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(eq(),w),y)),true()) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(lt(),w) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(lt(),w),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(lt(),w),y)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app (app (app(if(),app(app(eq(),w),y)), true ()), app(app(member(),w),z))) TRS: app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y) app(app(lt(),0()),app(s(),y)) -> true() app(app(lt(),y),0()) -> false() app(app(eq(),x),x) -> true() app(app(eq(),app(s(),x)),0()) -> false() app(app(eq(),0()),app(s(),x)) -> false() app(app(member(),w),null()) -> false() app(app(member(),w),app(app(app(fork(),x),y),z)) -> app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app( app ( app(if(),app(app(eq(),w),y)), true ()), app(app(member(),w),z))) SCC Processor: #sccs: 1 #rules: 14 #arcs: 196/196 DPs: app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(lt(),x) app#(app(lt(),app(s(),x)),app(s(),y)) -> app#(app(lt(),x),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),z) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(eq(),w) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(eq(),w),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(eq(),w),y)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(eq(),w),y)),true()) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(app(if(),app(app(eq(),w),y)),true()),app(app(member(),w),z)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(member(),w),x) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(lt(),w) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(lt(),w),y) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(if(),app(app(lt(),w),y)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)) app#(app(member(),w),app(app(app(fork(),x),y),z)) -> app#(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app (app ( app(if(),app(app(eq(),w),y)), true ()), app(app(member(),w),z))) TRS: app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y) app(app(lt(),0()),app(s(),y)) -> true() app(app(lt(),y),0()) -> false() app(app(eq(),x),x) -> true() app(app(eq(),app(s(),x)),0()) -> false() app(app(eq(),0()),app(s(),x)) -> false() app(app(member(),w),null()) -> false() app(app(member(),w),app(app(app(fork(),x),y),z)) -> app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app (app (app(if(),app(app(eq(),w),y)), true ()), app(app(member(),w),z))) Open