MAYBE Problem: app(app(append(),nil()),l) -> l app(app(append(),app(app(cons(),h),t)),l) -> app(app(cons(),h),app(app(append(),t),l)) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),h),t)) -> app(app(cons(),app(f,h)),app(app(map(),f),t)) app(app(append(),app(app(append(),l1),l2)),l3) -> app(app(append(),l1),app(app(append(),l2),l3)) app(app(map(),f),app(app(append(),l1),l2)) -> app(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) Proof: DP Processor: DPs: app#(app(append(),app(app(cons(),h),t)),l) -> app#(append(),t) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(cons(),h),app(app(append(),t),l)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) app#(app(map(),f),app(app(cons(),h),t)) -> app#(cons(),app(f,h)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(cons(),app(f,h)),app(app(map(),f),t)) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(append(),l2) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(append(),app(app(map(),f),l1)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) TRS: app(app(append(),nil()),l) -> l app(app(append(),app(app(cons(),h),t)),l) -> app(app(cons(),h),app(app(append(),t),l)) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),h),t)) -> app(app(cons(),app(f,h)),app(app(map(),f),t)) app(app(append(),app(app(append(),l1),l2)),l3) -> app(app(append(),l1),app(app(append(),l2),l3)) app(app(map(),f),app(app(append(),l1),l2)) -> app(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) EDG Processor: DPs: app#(app(append(),app(app(cons(),h),t)),l) -> app#(append(),t) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(cons(),h),app(app(append(),t),l)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) app#(app(map(),f),app(app(cons(),h),t)) -> app#(cons(),app(f,h)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(cons(),app(f,h)),app(app(map(),f),t)) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(append(),l2) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(append(),app(app(map(),f),l1)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) TRS: app(app(append(),nil()),l) -> l app(app(append(),app(app(cons(),h),t)),l) -> app(app(cons(),h),app(app(append(),t),l)) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),h),t)) -> app(app(cons(),app(f,h)),app(app(map(),f),t)) app(app(append(),app(app(append(),l1),l2)),l3) -> app(app(append(),l1),app(app(append(),l2),l3)) app(app(map(),f),app(app(append(),l1),l2)) -> app(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) graph: app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(cons(),app(f,h)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(cons(),app(f,h)),app(app(map(),f),t)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(append(),app(app(map(),f),l1)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(append(),t) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(cons(),h),app(app(append(),t),l)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(cons(),app(f,h)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(cons(),app(f,h)),app(app(map(),f),t)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(append(),l2) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(append(),app(app(map(),f),l1)) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(cons(),app(f,h)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(cons(),app(f,h)),app(app(map(),f),t)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(append(),app(app(map(),f),l1)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(cons(),app(f,h)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) -> app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(cons(),app(f,h)),app(app(map(),f),t)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(append(),app(app(map(),f),l1)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) -> app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(append(),t) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(cons(),h),app(app(append(),t),l)) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(append(),l2) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(append(),t) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(cons(),h),app(app(append(),t),l)) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(append(),l2) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(append(),t) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(cons(),h),app(app(append(),t),l)) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(append(),l2) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(append(),t) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) -> app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(cons(),h),app(app(append(),t),l)) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(append(),l2) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) -> app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) SCC Processor: #sccs: 2 #rules: 7 #arcs: 62/196 DPs: app#(app(map(),f),app(app(cons(),h),t)) -> app#(app(map(),f),t) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l1) app#(app(map(),f),app(app(append(),l1),l2)) -> app#(app(map(),f),l2) app#(app(map(),f),app(app(cons(),h),t)) -> app#(f,h) TRS: app(app(append(),nil()),l) -> l app(app(append(),app(app(cons(),h),t)),l) -> app(app(cons(),h),app(app(append(),t),l)) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),h),t)) -> app(app(cons(),app(f,h)),app(app(map(),f),t)) app(app(append(),app(app(append(),l1),l2)),l3) -> app(app(append(),l1),app(app(append(),l2),l3)) app(app(map(),f),app(app(append(),l1),l2)) -> app(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) Open DPs: app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l1),app(app(append(),l2),l3)) app#(app(append(),app(app(append(),l1),l2)),l3) -> app#(app(append(),l2),l3) app#(app(append(),app(app(cons(),h),t)),l) -> app#(app(append(),t),l) TRS: app(app(append(),nil()),l) -> l app(app(append(),app(app(cons(),h),t)),l) -> app(app(cons(),h),app(app(append(),t),l)) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),h),t)) -> app(app(cons(),app(f,h)),app(app(map(),f),t)) app(app(append(),app(app(append(),l1),l2)),l3) -> app(app(append(),l1),app(app(append(),l2),l3)) app(app(map(),f),app(app(append(),l1),l2)) -> app(app(append(),app(app(map(),f),l1)),app(app(map(),f),l2)) Open