YES Problem: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Proof: DP Processor: DPs: min#(s(x),s(y)) -> min#(x,y) len#(cons(x,xs)) -> len#(xs) sum#(x,s(y)) -> sum#(x,y) le#(s(x),s(y)) -> le#(x,y) take#(s(x),cons(y,ys)) -> take#(x,ys) addList#(x,y) -> len#(y) addList#(x,y) -> len#(x) addList#(x,y) -> min#(len(x),len(y)) addList#(x,y) -> le#(0(),min(len(x),len(y))) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) if#(true(),c,xs,ys,z) -> take#(c,ys) if#(true(),c,xs,ys,z) -> take#(c,xs) if#(true(),c,xs,ys,z) -> sum#(take(c,xs),take(c,ys)) if#(true(),c,xs,ys,z) -> len#(ys) if#(true(),c,xs,ys,z) -> len#(xs) if#(true(),c,xs,ys,z) -> min#(len(xs),len(ys)) if#(true(),c,xs,ys,z) -> le#(s(c),min(len(xs),len(ys))) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) EDG Processor: DPs: min#(s(x),s(y)) -> min#(x,y) len#(cons(x,xs)) -> len#(xs) sum#(x,s(y)) -> sum#(x,y) le#(s(x),s(y)) -> le#(x,y) take#(s(x),cons(y,ys)) -> take#(x,ys) addList#(x,y) -> len#(y) addList#(x,y) -> len#(x) addList#(x,y) -> min#(len(x),len(y)) addList#(x,y) -> le#(0(),min(len(x),len(y))) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) if#(true(),c,xs,ys,z) -> take#(c,ys) if#(true(),c,xs,ys,z) -> take#(c,xs) if#(true(),c,xs,ys,z) -> sum#(take(c,xs),take(c,ys)) if#(true(),c,xs,ys,z) -> len#(ys) if#(true(),c,xs,ys,z) -> len#(xs) if#(true(),c,xs,ys,z) -> min#(len(xs),len(ys)) if#(true(),c,xs,ys,z) -> le#(s(c),min(len(xs),len(ys))) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) graph: if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) -> if#(true(),c,xs,ys,z) -> take#(c,ys) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) -> if#(true(),c,xs,ys,z) -> take#(c,xs) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) -> if#(true(),c,xs,ys,z) -> sum#(take(c,xs),take(c,ys)) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) -> if#(true(),c,xs,ys,z) -> len#(ys) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) -> if#(true(),c,xs,ys,z) -> len#(xs) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) -> if#(true(),c,xs,ys,z) -> min#(len(xs),len(ys)) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) -> if#(true(),c,xs,ys,z) -> le#(s(c),min(len(xs),len(ys))) if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) -> if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) if#(true(),c,xs,ys,z) -> take#(c,ys) -> take#(s(x),cons(y,ys)) -> take#(x,ys) if#(true(),c,xs,ys,z) -> take#(c,xs) -> take#(s(x),cons(y,ys)) -> take#(x,ys) if#(true(),c,xs,ys,z) -> le#(s(c),min(len(xs),len(ys))) -> le#(s(x),s(y)) -> le#(x,y) if#(true(),c,xs,ys,z) -> sum#(take(c,xs),take(c,ys)) -> sum#(x,s(y)) -> sum#(x,y) if#(true(),c,xs,ys,z) -> len#(ys) -> len#(cons(x,xs)) -> len#(xs) if#(true(),c,xs,ys,z) -> len#(xs) -> len#(cons(x,xs)) -> len#(xs) if#(true(),c,xs,ys,z) -> min#(len(xs),len(ys)) -> min#(s(x),s(y)) -> min#(x,y) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) -> if#(true(),c,xs,ys,z) -> take#(c,ys) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) -> if#(true(),c,xs,ys,z) -> take#(c,xs) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) -> if#(true(),c,xs,ys,z) -> sum#(take(c,xs),take(c,ys)) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) -> if#(true(),c,xs,ys,z) -> len#(ys) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) -> if#(true(),c,xs,ys,z) -> len#(xs) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) -> if#(true(),c,xs,ys,z) -> min#(len(xs),len(ys)) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) -> if#(true(),c,xs,ys,z) -> le#(s(c),min(len(xs),len(ys))) addList#(x,y) -> if#(le(0(),min(len(x),len(y))),0(),x,y,nil()) -> if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) addList#(x,y) -> len#(x) -> len#(cons(x,xs)) -> len#(xs) addList#(x,y) -> len#(y) -> len#(cons(x,xs)) -> len#(xs) addList#(x,y) -> min#(len(x),len(y)) -> min#(s(x),s(y)) -> min#(x,y) take#(s(x),cons(y,ys)) -> take#(x,ys) -> take#(s(x),cons(y,ys)) -> take#(x,ys) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) sum#(x,s(y)) -> sum#(x,y) -> sum#(x,s(y)) -> sum#(x,y) len#(cons(x,xs)) -> len#(xs) -> len#(cons(x,xs)) -> len#(xs) min#(s(x),s(y)) -> min#(x,y) -> min#(s(x),s(y)) -> min#(x,y) SCC Processor: #sccs: 6 #rules: 6 #arcs: 31/324 DPs: if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Usable Rule Processor: DPs: if#(true(),c,xs,ys,z) -> if#(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) TRS: f20(x,y) -> x f20(x,y) -> y take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) le(0(),x) -> true() Bounds Processor: bound: 0 enrichment: top-dp automaton: final states: {4} transitions: len0(25) -> 21* len0(20) -> 21* len0(15) -> 21* len0(22) -> 21* len0(24) -> 21* len0(26) -> 21* len0(21) -> 21* len0(16) -> 21* len0(23) -> 21* cons0(22,16) -> 16* cons0(22,20) -> 16* cons0(22,22) -> 16* cons0(22,24) -> 16* cons0(22,26) -> 16* cons0(23,15) -> 16* cons0(23,21) -> 16* cons0(23,23) -> 16* cons0(23,25) -> 16* cons0(24,16) -> 26* cons0(24,20) -> 26* cons0(24,22) -> 26* cons0(24,24) -> 26* cons0(24,26) -> 26* cons0(25,15) -> 16* cons0(20,15) -> 16* cons0(15,15) -> 16* cons0(25,21) -> 16* cons0(20,21) -> 16* cons0(25,23) -> 16* cons0(15,21) -> 16* cons0(20,23) -> 16* cons0(25,25) -> 16* cons0(15,23) -> 16* cons0(20,25) -> 16* cons0(15,25) -> 16* cons0(26,16) -> 16* cons0(21,16) -> 16* cons0(16,16) -> 16* cons0(26,20) -> 16* cons0(21,20) -> 16* cons0(26,22) -> 16* cons0(16,20) -> 16* cons0(21,22) -> 16* cons0(26,24) -> 16* cons0(16,22) -> 16* cons0(21,24) -> 16* cons0(26,26) -> 16* cons0(16,24) -> 16* cons0(21,26) -> 16* cons0(16,26) -> 16* cons0(22,15) -> 16* cons0(22,21) -> 16* cons0(22,23) -> 16* cons0(22,25) -> 16* cons0(23,16) -> 16* cons0(23,20) -> 16* cons0(23,22) -> 16* cons0(23,24) -> 16* cons0(23,26) -> 16* cons0(24,15) -> 26* cons0(24,21) -> 26* cons0(24,23) -> 26* cons0(24,25) -> 26* cons0(25,16) -> 16* cons0(20,16) -> 16* cons0(15,16) -> 16* cons0(25,20) -> 16* cons0(20,20) -> 16* cons0(25,22) -> 16* cons0(15,20) -> 16* cons0(20,22) -> 16* cons0(25,24) -> 16* cons0(15,22) -> 16* cons0(20,24) -> 16* cons0(25,26) -> 16* cons0(15,24) -> 16* cons0(20,26) -> 16* cons0(15,26) -> 16* cons0(26,15) -> 16* cons0(21,15) -> 16* cons0(16,15) -> 16* cons0(26,21) -> 16* cons0(21,21) -> 16* cons0(26,23) -> 16* cons0(16,21) -> 16* cons0(21,23) -> 16* cons0(26,25) -> 16* cons0(16,23) -> 16* cons0(21,25) -> 16* cons0(16,25) -> 16* sum0(22,16) -> 16* sum0(22,20) -> 16* sum0(22,22) -> 24* sum0(22,24) -> 16* sum0(22,26) -> 16* sum0(23,15) -> 16* sum0(23,21) -> 16* sum0(23,23) -> 16* sum0(23,25) -> 16* sum0(24,16) -> 16* sum0(24,20) -> 16* sum0(24,22) -> 16* sum0(24,24) -> 16* sum0(24,26) -> 16* sum0(25,15) -> 16* sum0(20,15) -> 16* sum0(15,15) -> 16* sum0(25,21) -> 16* sum0(20,21) -> 16* sum0(25,23) -> 16* sum0(15,21) -> 16* sum0(20,23) -> 16* sum0(25,25) -> 16* sum0(15,23) -> 16* sum0(20,25) -> 16* sum0(15,25) -> 16* sum0(26,16) -> 16* sum0(21,16) -> 16* sum0(16,16) -> 16* sum0(26,20) -> 16* sum0(21,20) -> 16* sum0(26,22) -> 16* sum0(16,20) -> 16* sum0(21,22) -> 16* sum0(26,24) -> 16* sum0(16,22) -> 16* sum0(21,24) -> 16* sum0(26,26) -> 16* sum0(16,24) -> 16* sum0(21,26) -> 16* sum0(16,26) -> 16* sum0(22,15) -> 16* sum0(22,21) -> 16* sum0(22,23) -> 16* sum0(22,25) -> 16* sum0(23,16) -> 16* sum0(23,20) -> 16* sum0(23,22) -> 16* sum0(23,24) -> 16* sum0(23,26) -> 16* sum0(24,15) -> 16* sum0(24,21) -> 16* sum0(24,23) -> 16* sum0(24,25) -> 16* sum0(25,16) -> 16* sum0(20,16) -> 16* sum0(15,16) -> 16* sum0(25,20) -> 16* sum0(20,20) -> 16* sum0(25,22) -> 16* sum0(15,20) -> 16* sum0(20,22) -> 16* sum0(25,24) -> 16* sum0(15,22) -> 16* sum0(20,24) -> 16* sum0(25,26) -> 16* sum0(15,24) -> 16* sum0(20,26) -> 16* sum0(15,26) -> 16* sum0(26,15) -> 16* sum0(21,15) -> 16* sum0(16,15) -> 16* sum0(26,21) -> 16* sum0(21,21) -> 16* sum0(26,23) -> 16* sum0(16,21) -> 16* sum0(21,23) -> 16* sum0(26,25) -> 16* sum0(16,23) -> 16* sum0(21,25) -> 16* sum0(16,25) -> 16* take0(22,16) -> 22* take0(22,20) -> 22* take0(22,22) -> 22* take0(22,24) -> 22* take0(22,26) -> 22* take0(23,15) -> 22* take0(23,21) -> 22* take0(23,23) -> 22* take0(23,25) -> 22* take0(24,16) -> 22* take0(24,20) -> 22* take0(24,22) -> 22* take0(24,24) -> 22* take0(24,26) -> 22* take0(25,15) -> 22* take0(20,15) -> 22* take0(15,15) -> 22* take0(25,21) -> 22* take0(20,21) -> 22* take0(25,23) -> 22* take0(15,21) -> 22* take0(20,23) -> 22* take0(25,25) -> 22* take0(15,23) -> 22* take0(20,25) -> 22* take0(15,25) -> 22* take0(26,16) -> 22* take0(21,16) -> 22* take0(16,16) -> 22* take0(26,20) -> 22* take0(21,20) -> 22* take0(26,22) -> 22* take0(16,20) -> 22* take0(21,22) -> 22* take0(26,24) -> 22* take0(16,22) -> 22* take0(21,24) -> 22* take0(26,26) -> 22* take0(16,24) -> 22* take0(21,26) -> 22* take0(16,26) -> 22* take0(22,15) -> 22* take0(22,21) -> 22* take0(22,23) -> 22* take0(22,25) -> 22* take0(23,16) -> 22* take0(23,20) -> 22* take0(23,22) -> 22* take0(23,24) -> 22* take0(23,26) -> 22* take0(24,15) -> 22* take0(24,21) -> 22* take0(24,23) -> 22* take0(24,25) -> 22* take0(25,16) -> 22* take0(20,16) -> 22* take0(15,16) -> 22* take0(25,20) -> 22* take0(20,20) -> 22* take0(25,22) -> 22* take0(15,20) -> 22* take0(20,22) -> 22* take0(25,24) -> 22* take0(15,22) -> 22* take0(20,24) -> 22* take0(25,26) -> 22* take0(15,24) -> 22* take0(20,26) -> 22* take0(15,26) -> 22* take0(26,15) -> 22* take0(21,15) -> 22* take0(16,15) -> 22* take0(26,21) -> 22* take0(21,21) -> 22* take0(26,23) -> 22* take0(16,21) -> 22* take0(21,23) -> 22* take0(26,25) -> 22* take0(16,23) -> 22* take0(21,25) -> 22* take0(16,25) -> 22* f200(22,16) -> 16* f200(22,20) -> 16* f200(22,22) -> 16* f200(22,24) -> 16* f200(22,26) -> 16* f200(23,15) -> 16* f200(23,21) -> 16* f200(23,23) -> 16* f200(23,25) -> 16* f200(24,16) -> 16* f200(24,20) -> 16* f200(24,22) -> 16* f200(24,24) -> 16* f200(24,26) -> 16* f200(25,15) -> 16* f200(20,15) -> 16* f200(15,15) -> 16* f200(25,21) -> 16* f200(20,21) -> 16* f200(25,23) -> 16* f200(15,21) -> 16* f200(20,23) -> 16* f200(25,25) -> 16* f200(15,23) -> 16* f200(20,25) -> 16* f200(15,25) -> 16* f200(26,16) -> 16* f200(21,16) -> 16* f200(16,16) -> 16* f200(26,20) -> 16* f200(21,20) -> 16* f200(26,22) -> 16* f200(16,20) -> 16* f200(21,22) -> 16* f200(26,24) -> 16* f200(16,22) -> 16* f200(21,24) -> 16* f200(26,26) -> 16* f200(16,24) -> 16* f200(21,26) -> 16* f200(16,26) -> 16* f200(22,15) -> 16* f200(22,21) -> 16* f200(22,23) -> 16* f200(22,25) -> 16* f200(23,16) -> 16* f200(23,20) -> 16* f200(23,22) -> 16* f200(23,24) -> 16* f200(23,26) -> 16* f200(24,15) -> 16* f200(24,21) -> 16* f200(24,23) -> 16* f200(24,25) -> 16* f200(25,16) -> 16* f200(20,16) -> 16* f200(15,16) -> 16* f200(25,20) -> 16* f200(20,20) -> 16* f200(25,22) -> 16* f200(15,20) -> 16* f200(20,22) -> 16* f200(25,24) -> 16* f200(15,22) -> 16* f200(20,24) -> 16* f200(25,26) -> 16* f200(15,24) -> 16* f200(20,26) -> 16* f200(15,26) -> 16* f200(26,15) -> 16* f200(21,15) -> 16* f200(16,15) -> 16* f200(26,21) -> 16* f200(21,21) -> 16* f200(26,23) -> 16* f200(16,21) -> 16* f200(21,23) -> 16* f200(26,25) -> 16* f200(16,23) -> 16* f200(21,25) -> 16* f200(16,25) -> 16* 00() -> 23,21,16 nil0() -> 16* false0() -> 25,16 if{#,0}(25,20,26,21,26) -> 4* if{#,0}(25,20,21,21,26) -> 4* if{#,0}(25,20,16,21,26) -> 4* if{#,0}(25,20,26,23,26) -> 4* if{#,0}(25,20,21,23,26) -> 4* if{#,0}(25,20,16,23,26) -> 4* if{#,0}(25,20,26,25,26) -> 4* if{#,0}(25,20,21,25,26) -> 4* if{#,0}(25,20,16,25,26) -> 4* if{#,0}(25,20,22,16,26) -> 4* if{#,0}(25,20,22,20,26) -> 4* if{#,0}(25,20,22,22,26) -> 4* if{#,0}(25,20,22,24,26) -> 4* if{#,0}(25,20,22,26,26) -> 4* if{#,0}(25,20,23,15,26) -> 4* if{#,0}(25,20,23,21,26) -> 4* if{#,0}(25,20,23,23,26) -> 4* if{#,0}(25,20,23,25,26) -> 4* if{#,0}(25,20,24,16,26) -> 4* if{#,0}(25,20,24,20,26) -> 4* if{#,0}(25,20,24,22,26) -> 4* if{#,0}(25,20,24,24,26) -> 4* if{#,0}(25,20,24,26,26) -> 4* if{#,0}(25,20,25,15,26) -> 4* if{#,0}(25,20,20,15,26) -> 4* if{#,0}(25,20,15,15,26) -> 4* if{#,0}(25,20,25,21,26) -> 4* if{#,0}(25,20,20,21,26) -> 4* if{#,0}(25,20,25,23,26) -> 4* if{#,0}(25,20,15,21,26) -> 4* if{#,0}(25,20,20,23,26) -> 4* if{#,0}(25,20,15,23,26) -> 4* if{#,0}(25,20,25,25,26) -> 4* if{#,0}(25,20,20,25,26) -> 4* if{#,0}(25,20,15,25,26) -> 4* if{#,0}(25,20,26,16,26) -> 4* if{#,0}(25,20,21,16,26) -> 4* if{#,0}(25,20,16,16,26) -> 4* if{#,0}(25,20,26,20,26) -> 4* if{#,0}(25,20,21,20,26) -> 4* if{#,0}(25,20,16,20,26) -> 4* if{#,0}(25,20,26,22,26) -> 4* if{#,0}(25,20,21,22,26) -> 4* if{#,0}(25,20,16,22,26) -> 4* if{#,0}(25,20,26,24,26) -> 4* if{#,0}(25,20,21,24,26) -> 4* if{#,0}(25,20,26,26,26) -> 4* if{#,0}(25,20,16,24,26) -> 4* if{#,0}(25,20,21,26,26) -> 4* if{#,0}(25,20,16,26,26) -> 4* if{#,0}(25,20,22,15,26) -> 4* if{#,0}(25,20,22,21,26) -> 4* if{#,0}(25,20,22,23,26) -> 4* if{#,0}(25,20,22,25,26) -> 4* if{#,0}(25,20,23,16,26) -> 4* if{#,0}(25,20,23,20,26) -> 4* if{#,0}(25,20,23,22,26) -> 4* if{#,0}(25,20,23,24,26) -> 4* if{#,0}(25,20,23,26,26) -> 4* if{#,0}(25,20,24,15,26) -> 4* if{#,0}(25,20,24,21,26) -> 4* if{#,0}(25,20,24,23,26) -> 4* if{#,0}(25,20,24,25,26) -> 4* if{#,0}(25,20,25,16,26) -> 4* if{#,0}(25,20,20,16,26) -> 4* if{#,0}(25,20,15,16,26) -> 4* if{#,0}(25,20,25,20,26) -> 4* if{#,0}(25,20,20,20,26) -> 4* if{#,0}(25,20,15,20,26) -> 4* if{#,0}(25,20,25,22,26) -> 4* if{#,0}(25,20,20,22,26) -> 4* if{#,0}(25,20,15,22,26) -> 4* if{#,0}(25,20,25,24,26) -> 4* if{#,0}(25,20,20,24,26) -> 4* if{#,0}(25,20,15,24,26) -> 4* if{#,0}(25,20,25,26,26) -> 4* if{#,0}(25,20,20,26,26) -> 4* if{#,0}(25,20,15,26,26) -> 4* if{#,0}(25,20,26,15,26) -> 4* if{#,0}(25,20,21,15,26) -> 4* if{#,0}(25,20,16,15,26) -> 4* true0() -> 15* le0(22,16) -> 16* le0(22,20) -> 16* le0(22,22) -> 16* le0(22,24) -> 16* le0(22,26) -> 16* le0(23,15) -> 16* le0(23,21) -> 16* le0(23,23) -> 16* le0(23,25) -> 16* le0(24,16) -> 16* le0(24,20) -> 16* le0(24,22) -> 16* le0(24,24) -> 16* le0(24,26) -> 16* le0(25,15) -> 16* le0(20,15) -> 16* le0(15,15) -> 16* le0(25,21) -> 16* le0(20,21) -> 16* le0(25,23) -> 16* le0(15,21) -> 16* le0(20,23) -> 25* le0(25,25) -> 16* le0(15,23) -> 16* le0(20,25) -> 16* le0(15,25) -> 16* le0(26,16) -> 16* le0(21,16) -> 16* le0(16,16) -> 16* le0(26,20) -> 16* le0(21,20) -> 16* le0(26,22) -> 16* le0(16,20) -> 16* le0(21,22) -> 16* le0(26,24) -> 16* le0(16,22) -> 16* le0(21,24) -> 16* le0(26,26) -> 16* le0(16,24) -> 16* le0(21,26) -> 16* le0(16,26) -> 16* le0(22,15) -> 16* le0(22,21) -> 16* le0(22,23) -> 16* le0(22,25) -> 16* le0(23,16) -> 16* le0(23,20) -> 16* le0(23,22) -> 16* le0(23,24) -> 16* le0(23,26) -> 16* le0(24,15) -> 16* le0(24,21) -> 16* le0(24,23) -> 16* le0(24,25) -> 16* le0(25,16) -> 16* le0(20,16) -> 16* le0(15,16) -> 16* le0(25,20) -> 16* le0(20,20) -> 16* le0(25,22) -> 16* le0(15,20) -> 16* le0(20,22) -> 16* le0(25,24) -> 16* le0(15,22) -> 16* le0(20,24) -> 16* le0(25,26) -> 16* le0(15,24) -> 16* le0(20,26) -> 16* le0(15,26) -> 16* le0(26,15) -> 16* le0(21,15) -> 16* le0(16,15) -> 16* le0(26,21) -> 16* le0(21,21) -> 16* le0(26,23) -> 16* le0(16,21) -> 16* le0(21,23) -> 16* le0(26,25) -> 16* le0(16,23) -> 16* le0(21,25) -> 16* le0(16,25) -> 16* s0(25) -> 20* s0(20) -> 20* s0(15) -> 20* s0(22) -> 20* s0(24) -> 20* s0(26) -> 20* s0(21) -> 21,20 s0(16) -> 20* s0(23) -> 20* min0(22,16) -> 16* min0(22,20) -> 16* min0(22,22) -> 16* min0(22,24) -> 16* min0(22,26) -> 16* min0(23,15) -> 16* min0(23,21) -> 16* min0(23,23) -> 16* min0(23,25) -> 16* min0(24,16) -> 16* min0(24,20) -> 16* min0(24,22) -> 16* min0(24,24) -> 16* min0(24,26) -> 16* min0(25,15) -> 16* min0(20,15) -> 16* min0(15,15) -> 16* min0(25,21) -> 16* min0(20,21) -> 16* min0(25,23) -> 16* min0(15,21) -> 16* min0(20,23) -> 16* min0(25,25) -> 16* min0(15,23) -> 16* min0(20,25) -> 16* min0(15,25) -> 16* min0(26,16) -> 16* min0(21,16) -> 16* min0(16,16) -> 16* min0(26,20) -> 16* min0(21,20) -> 16* min0(26,22) -> 16* min0(16,20) -> 16* min0(21,22) -> 16* min0(26,24) -> 16* min0(16,22) -> 16* min0(21,24) -> 16* min0(26,26) -> 16* min0(16,24) -> 16* min0(21,26) -> 16* min0(16,26) -> 16* min0(22,15) -> 16* min0(22,21) -> 16* min0(22,23) -> 16* min0(22,25) -> 16* min0(23,16) -> 16* min0(23,20) -> 16* min0(23,22) -> 16* min0(23,24) -> 16* min0(23,26) -> 16* min0(24,15) -> 16* min0(24,21) -> 16* min0(24,23) -> 16* min0(24,25) -> 16* min0(25,16) -> 16* min0(20,16) -> 16* min0(15,16) -> 16* min0(25,20) -> 16* min0(20,20) -> 16* min0(25,22) -> 16* min0(15,20) -> 16* min0(20,22) -> 16* min0(25,24) -> 16* min0(15,22) -> 16* min0(20,24) -> 16* min0(25,26) -> 16* min0(15,24) -> 16* min0(20,26) -> 16* min0(15,26) -> 16* min0(26,15) -> 16* min0(21,15) -> 16* min0(16,15) -> 16* min0(26,21) -> 16* min0(21,21) -> 23* min0(26,23) -> 16* min0(16,21) -> 16* min0(21,23) -> 16* min0(26,25) -> 16* min0(16,23) -> 16* min0(21,25) -> 16* min0(16,25) -> 16* 15 -> 16* 16 -> 22* 20 -> 16* 21 -> 16* 22 -> 24,16 23 -> 16* 24 -> 22,16 25 -> 16* 26 -> 16* problem: DPs: TRS: f20(x,y) -> x f20(x,y) -> y take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) le(0(),x) -> true() Qed DPs: take#(s(x),cons(y,ys)) -> take#(x,ys) TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Subterm Criterion Processor: simple projection: pi(take#) = 1 problem: DPs: TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Qed DPs: sum#(x,s(y)) -> sum#(x,y) TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Subterm Criterion Processor: simple projection: pi(sum#) = 1 problem: DPs: TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Qed DPs: len#(cons(x,xs)) -> len#(xs) TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Subterm Criterion Processor: simple projection: pi(len#) = 0 problem: DPs: TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Qed DPs: min#(s(x),s(y)) -> min#(x,y) TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Subterm Criterion Processor: simple projection: pi(min#) = 1 problem: DPs: TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Qed DPs: le#(s(x),s(y)) -> le#(x,y) TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Subterm Criterion Processor: simple projection: pi(le#) = 1 problem: DPs: TRS: min(0(),y) -> 0() min(s(x),0()) -> 0() min(s(x),s(y)) -> min(x,y) len(nil()) -> 0() len(cons(x,xs)) -> s(len(xs)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) take(0(),cons(y,ys)) -> y take(s(x),cons(y,ys)) -> take(x,ys) addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil()) if(false(),c,x,y,z) -> z if(true(),c,xs,ys,z) -> if(le(s(c),min(len(xs),len(ys))),s(c),xs,ys,cons(sum(take(c,xs),take(c,ys)),z)) Qed