MAYBE Problem: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Proof: DP Processor: DPs: +#(s(x),y) -> +#(x,y) ++#(:(x,xs),ys) -> ++#(xs,ys) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) length#(:(x,xs)) -> length#(xs) avg#(xs) -> length#(xs) avg#(xs) -> sum#(xs) avg#(xs) -> hd#(sum(xs)) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Usable Rule Processor: DPs: +#(s(x),y) -> +#(x,y) ++#(:(x,xs),ys) -> ++#(xs,ys) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) length#(:(x,xs)) -> length#(xs) avg#(xs) -> length#(xs) avg#(xs) -> sum#(xs) avg#(xs) -> hd#(sum(xs)) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) TRS: f20(x,y) -> x f20(x,y) -> y +(0(),y) -> y +(s(x),y) -> s(+(x,y)) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x TDG Processor: DPs: +#(s(x),y) -> +#(x,y) ++#(:(x,xs),ys) -> ++#(xs,ys) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) length#(:(x,xs)) -> length#(xs) avg#(xs) -> length#(xs) avg#(xs) -> sum#(xs) avg#(xs) -> hd#(sum(xs)) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) TRS: f20(x,y) -> x f20(x,y) -> y +(0(),y) -> y +(s(x),y) -> s(+(x,y)) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x graph: avg#(xs) -> length#(xs) -> length#(:(x,xs)) -> length#(xs) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -> quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -> quot#(s(x),s(y)) -> -#(x,y) avg#(xs) -> sum#(xs) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) avg#(xs) -> sum#(xs) -> sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) avg#(xs) -> sum#(xs) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) avg#(xs) -> sum#(xs) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) avg#(xs) -> sum#(xs) -> sum#(:(x,:(y,xs))) -> +#(x,y) length#(:(x,xs)) -> length#(xs) -> length#(:(x,xs)) -> length#(xs) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) -> quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) -> quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y) -#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -> sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -> sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> +#(x,y) -> +#(s(x),y) -> +#(x,y) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -> sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -> sum#(:(x,:(y,xs))) -> +#(x,y) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(:(x,:(y,xs))) -> +#(x,y) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) -> ++#(:(x,xs),ys) -> ++#(xs,ys) ++#(:(x,xs),ys) -> ++#(xs,ys) -> ++#(:(x,xs),ys) -> ++#(xs,ys) +#(s(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y) EDG Processor: DPs: +#(s(x),y) -> +#(x,y) ++#(:(x,xs),ys) -> ++#(xs,ys) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) length#(:(x,xs)) -> length#(xs) avg#(xs) -> length#(xs) avg#(xs) -> sum#(xs) avg#(xs) -> hd#(sum(xs)) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) TRS: f20(x,y) -> x f20(x,y) -> y +(0(),y) -> y +(s(x),y) -> s(+(x,y)) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(:(x,nil())) -> :(x,nil()) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x graph: avg#(xs) -> length#(xs) -> length#(:(x,xs)) -> length#(xs) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -> quot#(s(x),s(y)) -> -#(x,y) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) -> quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) avg#(xs) -> sum#(xs) -> sum#(:(x,:(y,xs))) -> +#(x,y) avg#(xs) -> sum#(xs) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) avg#(xs) -> sum#(xs) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) avg#(xs) -> sum#(xs) -> sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) avg#(xs) -> sum#(xs) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) length#(:(x,xs)) -> length#(xs) -> length#(:(x,xs)) -> length#(xs) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) -> quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) -> quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) quot#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y) -#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -> sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(:(x,:(y,xs))) -> +#(x,y) -> +#(s(x),y) -> +#(x,y) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -> sum#(:(x,:(y,xs))) -> +#(x,y) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(:(x,:(y,xs))) -> +#(x,y) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -> sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) -> ++#(:(x,xs),ys) -> ++#(xs,ys) ++#(:(x,xs),ys) -> ++#(xs,ys) -> ++#(:(x,xs),ys) -> ++#(xs,ys) +#(s(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y) Restore Modifier: DPs: +#(s(x),y) -> +#(x,y) ++#(:(x,xs),ys) -> ++#(xs,ys) sum#(:(x,:(y,xs))) -> +#(x,y) sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) sum#(++(xs,:(x,:(y,ys)))) -> sum#(:(x,:(y,ys))) sum#(++(xs,:(x,:(y,ys)))) -> ++#(xs,sum(:(x,:(y,ys)))) sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) -#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> -#(x,y) quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) length#(:(x,xs)) -> length#(xs) avg#(xs) -> length#(xs) avg#(xs) -> sum#(xs) avg#(xs) -> hd#(sum(xs)) avg#(xs) -> quot#(hd(sum(xs)),length(xs)) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) SCC Processor: #sccs: 7 #rules: 7 #arcs: 26/225 DPs: sum#(++(xs,:(x,:(y,ys)))) -> sum#(++(xs,sum(:(x,:(y,ys))))) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Open DPs: sum#(:(x,:(y,xs))) -> sum#(:(+(x,y),xs)) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [sum#](x0) = x0, [avg](x0) = 0, [hd](x0) = x0 + 1, [length](x0) = 0, [quot](x0, x1) = 0, [-](x0, x1) = x0, [sum](x0) = x0, [:](x0, x1) = x0 + x1 + 1, [++](x0, x1) = x0 + x1, [nil] = 0, [s](x0) = x0, [+](x0, x1) = x0 + x1, [0] = 0 orientation: sum#(:(x,:(y,xs))) = x + xs + y + 2 >= x + xs + y + 1 = sum#(:(+(x,y),xs)) +(0(),y) = y >= y = y +(s(x),y) = x + y >= x + y = s(+(x,y)) ++(nil(),ys) = ys >= ys = ys ++(:(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = :(x,++(xs,ys)) sum(:(x,nil())) = x + 1 >= x + 1 = :(x,nil()) sum(:(x,:(y,xs))) = x + xs + y + 2 >= x + xs + y + 1 = sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) = x + xs + y + ys + 2 >= x + xs + y + ys + 2 = sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) = x >= x = x -(0(),s(y)) = 0 >= 0 = 0() -(s(x),s(y)) = x >= x = -(x,y) quot(0(),s(y)) = 0 >= 0 = 0() quot(s(x),s(y)) = 0 >= 0 = s(quot(-(x,y),s(y))) length(nil()) = 0 >= 0 = 0() length(:(x,xs)) = 0 >= 0 = s(length(xs)) hd(:(x,xs)) = x + xs + 2 >= x = x avg(xs) = 0 >= 0 = quot(hd(sum(xs)),length(xs)) problem: DPs: TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Qed DPs: +#(s(x),y) -> +#(x,y) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [+#](x0, x1) = x0 + 1, [avg](x0) = x0 + 1, [hd](x0) = x0, [length](x0) = x0, [quot](x0, x1) = x0 + 1, [-](x0, x1) = x0, [sum](x0) = x0, [:](x0, x1) = x0 + x1 + 1, [++](x0, x1) = x0 + x1, [nil] = 1, [s](x0) = x0 + 1, [+](x0, x1) = x0 + x1, [0] = 1 orientation: +#(s(x),y) = x + 2 >= x + 1 = +#(x,y) +(0(),y) = y + 1 >= y = y +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y)) ++(nil(),ys) = ys + 1 >= ys = ys ++(:(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = :(x,++(xs,ys)) sum(:(x,nil())) = x + 2 >= x + 2 = :(x,nil()) sum(:(x,:(y,xs))) = x + xs + y + 2 >= x + xs + y + 1 = sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) = x + xs + y + ys + 2 >= x + xs + y + ys + 2 = sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) = x >= x = x -(0(),s(y)) = 1 >= 1 = 0() -(s(x),s(y)) = x + 1 >= x = -(x,y) quot(0(),s(y)) = 2 >= 1 = 0() quot(s(x),s(y)) = x + 2 >= x + 2 = s(quot(-(x,y),s(y))) length(nil()) = 1 >= 1 = 0() length(:(x,xs)) = x + xs + 1 >= xs + 1 = s(length(xs)) hd(:(x,xs)) = x + xs + 1 >= x = x avg(xs) = xs + 1 >= xs + 1 = quot(hd(sum(xs)),length(xs)) problem: DPs: TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Qed DPs: ++#(:(x,xs),ys) -> ++#(xs,ys) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [++#](x0, x1) = x0 + 1, [avg](x0) = 0, [hd](x0) = x0, [length](x0) = 0, [quot](x0, x1) = 0, [-](x0, x1) = x0, [sum](x0) = x0, [:](x0, x1) = x0 + x1 + 1, [++](x0, x1) = x0 + x1, [nil] = 1, [s](x0) = x0, [+](x0, x1) = x1 + 1, [0] = 0 orientation: ++#(:(x,xs),ys) = x + xs + 2 >= xs + 1 = ++#(xs,ys) +(0(),y) = y + 1 >= y = y +(s(x),y) = y + 1 >= y + 1 = s(+(x,y)) ++(nil(),ys) = ys + 1 >= ys = ys ++(:(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = :(x,++(xs,ys)) sum(:(x,nil())) = x + 2 >= x + 2 = :(x,nil()) sum(:(x,:(y,xs))) = x + xs + y + 2 >= xs + y + 2 = sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) = x + xs + y + ys + 2 >= x + xs + y + ys + 2 = sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) = x >= x = x -(0(),s(y)) = 0 >= 0 = 0() -(s(x),s(y)) = x >= x = -(x,y) quot(0(),s(y)) = 0 >= 0 = 0() quot(s(x),s(y)) = 0 >= 0 = s(quot(-(x,y),s(y))) length(nil()) = 0 >= 0 = 0() length(:(x,xs)) = 0 >= 0 = s(length(xs)) hd(:(x,xs)) = x + xs + 1 >= x = x avg(xs) = 0 >= 0 = quot(hd(sum(xs)),length(xs)) problem: DPs: TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Qed DPs: quot#(s(x),s(y)) -> quot#(-(x,y),s(y)) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [quot#](x0, x1) = x0, [avg](x0) = x0 + 1, [hd](x0) = x0, [length](x0) = x0, [quot](x0, x1) = x0, [-](x0, x1) = x0, [sum](x0) = x0, [:](x0, x1) = x0 + x1 + 1, [++](x0, x1) = x0 + x1 + 1, [nil] = 0, [s](x0) = x0 + 1, [+](x0, x1) = x0 + x1 + 1, [0] = 0 orientation: quot#(s(x),s(y)) = x + 1 >= x = quot#(-(x,y),s(y)) +(0(),y) = y + 1 >= y = y +(s(x),y) = x + y + 2 >= x + y + 2 = s(+(x,y)) ++(nil(),ys) = ys + 1 >= ys = ys ++(:(x,xs),ys) = x + xs + ys + 2 >= x + xs + ys + 2 = :(x,++(xs,ys)) sum(:(x,nil())) = x + 1 >= x + 1 = :(x,nil()) sum(:(x,:(y,xs))) = x + xs + y + 2 >= x + xs + y + 2 = sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) = x + xs + y + ys + 3 >= x + xs + y + ys + 3 = sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) = x >= x = x -(0(),s(y)) = 0 >= 0 = 0() -(s(x),s(y)) = x + 1 >= x = -(x,y) quot(0(),s(y)) = 0 >= 0 = 0() quot(s(x),s(y)) = x + 1 >= x + 1 = s(quot(-(x,y),s(y))) length(nil()) = 0 >= 0 = 0() length(:(x,xs)) = x + xs + 1 >= xs + 1 = s(length(xs)) hd(:(x,xs)) = x + xs + 1 >= x = x avg(xs) = xs + 1 >= xs = quot(hd(sum(xs)),length(xs)) problem: DPs: TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Qed DPs: -#(s(x),s(y)) -> -#(x,y) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [-#](x0, x1) = x0, [avg](x0) = x0 + 1, [hd](x0) = x0, [length](x0) = x0, [quot](x0, x1) = x0, [-](x0, x1) = x0, [sum](x0) = x0, [:](x0, x1) = x0 + x1 + 1, [++](x0, x1) = x0 + x1 + 1, [nil] = 0, [s](x0) = x0 + 1, [+](x0, x1) = x0 + x1, [0] = 0 orientation: -#(s(x),s(y)) = x + 1 >= x = -#(x,y) +(0(),y) = y >= y = y +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y)) ++(nil(),ys) = ys + 1 >= ys = ys ++(:(x,xs),ys) = x + xs + ys + 2 >= x + xs + ys + 2 = :(x,++(xs,ys)) sum(:(x,nil())) = x + 1 >= x + 1 = :(x,nil()) sum(:(x,:(y,xs))) = x + xs + y + 2 >= x + xs + y + 1 = sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) = x + xs + y + ys + 3 >= x + xs + y + ys + 3 = sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) = x >= x = x -(0(),s(y)) = 0 >= 0 = 0() -(s(x),s(y)) = x + 1 >= x = -(x,y) quot(0(),s(y)) = 0 >= 0 = 0() quot(s(x),s(y)) = x + 1 >= x + 1 = s(quot(-(x,y),s(y))) length(nil()) = 0 >= 0 = 0() length(:(x,xs)) = x + xs + 1 >= xs + 1 = s(length(xs)) hd(:(x,xs)) = x + xs + 1 >= x = x avg(xs) = xs + 1 >= xs = quot(hd(sum(xs)),length(xs)) problem: DPs: TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Qed DPs: length#(:(x,xs)) -> length#(xs) TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Matrix Interpretation Processor: dimension: 1 interpretation: [length#](x0) = x0 + 1, [avg](x0) = 0, [hd](x0) = x0, [length](x0) = 0, [quot](x0, x1) = 0, [-](x0, x1) = x0, [sum](x0) = x0, [:](x0, x1) = x0 + x1 + 1, [++](x0, x1) = x0 + x1, [nil] = 1, [s](x0) = x0, [+](x0, x1) = x1 + 1, [0] = 0 orientation: length#(:(x,xs)) = x + xs + 2 >= xs + 1 = length#(xs) +(0(),y) = y + 1 >= y = y +(s(x),y) = y + 1 >= y + 1 = s(+(x,y)) ++(nil(),ys) = ys + 1 >= ys = ys ++(:(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = :(x,++(xs,ys)) sum(:(x,nil())) = x + 2 >= x + 2 = :(x,nil()) sum(:(x,:(y,xs))) = x + xs + y + 2 >= xs + y + 2 = sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) = x + xs + y + ys + 2 >= x + xs + y + ys + 2 = sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) = x >= x = x -(0(),s(y)) = 0 >= 0 = 0() -(s(x),s(y)) = x >= x = -(x,y) quot(0(),s(y)) = 0 >= 0 = 0() quot(s(x),s(y)) = 0 >= 0 = s(quot(-(x,y),s(y))) length(nil()) = 0 >= 0 = 0() length(:(x,xs)) = 0 >= 0 = s(length(xs)) hd(:(x,xs)) = x + xs + 1 >= x = x avg(xs) = 0 >= 0 = quot(hd(sum(xs)),length(xs)) problem: DPs: TRS: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) ++(nil(),ys) -> ys ++(:(x,xs),ys) -> :(x,++(xs,ys)) sum(:(x,nil())) -> :(x,nil()) sum(:(x,:(y,xs))) -> sum(:(+(x,y),xs)) sum(++(xs,:(x,:(y,ys)))) -> sum(++(xs,sum(:(x,:(y,ys))))) -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(-(x,y),s(y))) length(nil()) -> 0() length(:(x,xs)) -> s(length(xs)) hd(:(x,xs)) -> x avg(xs) -> quot(hd(sum(xs)),length(xs)) Qed