MAYBE Problem: plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) -> y ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) sum(xs) -> sumIter(xs,0()) sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) -> x ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) isempty(nil()) -> true() isempty(cons(x,xs)) -> false() head(nil()) -> error() head(cons(x,xs)) -> x tail(nil()) -> nil() tail(cons(x,xs)) -> xs a() -> b() a() -> c() Proof: DP Processor: DPs: plus#(x,y) -> plusIter#(x,y,0()) plusIter#(x,y,z) -> le#(x,z) plusIter#(x,y,z) -> ifPlus#(le(x,z),x,y,z) ifPlus#(false(),x,y,z) -> plusIter#(x,s(y),s(z)) le#(s(x),s(y)) -> le#(x,y) sum#(xs) -> sumIter#(xs,0()) sumIter#(xs,x) -> head#(xs) sumIter#(xs,x) -> plus#(x,head(xs)) sumIter#(xs,x) -> isempty#(xs) sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs))) ifSum#(false(),xs,x,y) -> tail#(xs) ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y) TRS: plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) -> y ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) sum(xs) -> sumIter(xs,0()) sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) -> x ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) isempty(nil()) -> true() isempty(cons(x,xs)) -> false() head(nil()) -> error() head(cons(x,xs)) -> x tail(nil()) -> nil() tail(cons(x,xs)) -> xs a() -> b() a() -> c() TDG Processor: DPs: plus#(x,y) -> plusIter#(x,y,0()) plusIter#(x,y,z) -> le#(x,z) plusIter#(x,y,z) -> ifPlus#(le(x,z),x,y,z) ifPlus#(false(),x,y,z) -> plusIter#(x,s(y),s(z)) le#(s(x),s(y)) -> le#(x,y) sum#(xs) -> sumIter#(xs,0()) sumIter#(xs,x) -> head#(xs) sumIter#(xs,x) -> plus#(x,head(xs)) sumIter#(xs,x) -> isempty#(xs) sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs))) ifSum#(false(),xs,x,y) -> tail#(xs) ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y) TRS: plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) -> y ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) sum(xs) -> sumIter(xs,0()) sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) -> x ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) isempty(nil()) -> true() isempty(cons(x,xs)) -> false() head(nil()) -> error() head(cons(x,xs)) -> x tail(nil()) -> nil() tail(cons(x,xs)) -> xs a() -> b() a() -> c() graph: ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y) -> sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs))) ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y) -> sumIter#(xs,x) -> isempty#(xs) ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y) -> sumIter#(xs,x) -> plus#(x,head(xs)) ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y) -> sumIter#(xs,x) -> head#(xs) sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs))) -> ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y) sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs))) -> ifSum#(false(),xs,x,y) -> tail#(xs) sumIter#(xs,x) -> plus#(x,head(xs)) -> plus#(x,y) -> plusIter#(x,y,0()) sum#(xs) -> sumIter#(xs,0()) -> sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs))) sum#(xs) -> sumIter#(xs,0()) -> sumIter#(xs,x) -> isempty#(xs) sum#(xs) -> sumIter#(xs,0()) -> sumIter#(xs,x) -> plus#(x,head(xs)) sum#(xs) -> sumIter#(xs,0()) -> sumIter#(xs,x) -> head#(xs) ifPlus#(false(),x,y,z) -> plusIter#(x,s(y),s(z)) -> plusIter#(x,y,z) -> ifPlus#(le(x,z),x,y,z) ifPlus#(false(),x,y,z) -> plusIter#(x,s(y),s(z)) -> plusIter#(x,y,z) -> le#(x,z) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) plusIter#(x,y,z) -> ifPlus#(le(x,z),x,y,z) -> ifPlus#(false(),x,y,z) -> plusIter#(x,s(y),s(z)) plusIter#(x,y,z) -> le#(x,z) -> le#(s(x),s(y)) -> le#(x,y) plus#(x,y) -> plusIter#(x,y,0()) -> plusIter#(x,y,z) -> ifPlus#(le(x,z),x,y,z) plus#(x,y) -> plusIter#(x,y,0()) -> plusIter#(x,y,z) -> le#(x,z) SCC Processor: #sccs: 3 #rules: 5 #arcs: 18/144 DPs: ifSum#(false(),xs,x,y) -> sumIter#(tail(xs),y) sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs))) TRS: plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) -> y ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) sum(xs) -> sumIter(xs,0()) sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) -> x ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) isempty(nil()) -> true() isempty(cons(x,xs)) -> false() head(nil()) -> error() head(cons(x,xs)) -> x tail(nil()) -> nil() tail(cons(x,xs)) -> xs a() -> b() a() -> c() Matrix Interpretation Processor: dim=1 interpretation: [ifSum#](x0, x1, x2, x3) = 1/2x0 + x1 + 2, [sumIter#](x0, x1) = 2x0 + 2, [c] = 0, [b] = 1, [a] = 1, [error] = 0, [cons](x0, x1) = 2x0 + 2x1 + 2, [nil] = 0, [tail](x0) = 1/2x0, [ifSum](x0, x1, x2, x3) = 1/2x1 + x2 + x3, [head](x0) = 1/2x0, [isempty](x0) = 2x0, [sumIter](x0, x1) = x0 + x1, [sum](x0) = 2x0, [s](x0) = 0, [false] = 1, [true] = 0, [ifPlus](x0, x1, x2, x3) = x2, [le](x0, x1) = 1, [plusIter](x0, x1, x2) = x1, [0] = 0, [plus](x0, x1) = x1 orientation: ifSum#(false(),xs,x,y) = xs + 5/2 >= xs + 2 = sumIter#(tail(xs),y) sumIter#(xs,x) = 2xs + 2 >= 2xs + 2 = ifSum#(isempty(xs),xs,x,plus(x,head(xs))) plus(x,y) = y >= y = plusIter(x,y,0()) plusIter(x,y,z) = y >= y = ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) = y >= y = y ifPlus(false(),x,y,z) = y >= 0 = plusIter(x,s(y),s(z)) le(s(x),0()) = 1 >= 1 = false() le(0(),y) = 1 >= 0 = true() le(s(x),s(y)) = 1 >= 1 = le(x,y) sum(xs) = 2xs >= xs = sumIter(xs,0()) sumIter(xs,x) = x + xs >= x + xs = ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) = x + 1/2xs + y >= x = x ifSum(false(),xs,x,y) = x + 1/2xs + y >= 1/2xs + y = sumIter(tail(xs),y) isempty(nil()) = 0 >= 0 = true() isempty(cons(x,xs)) = 4x + 4xs + 4 >= 1 = false() head(nil()) = 0 >= 0 = error() head(cons(x,xs)) = x + xs + 1 >= x = x tail(nil()) = 0 >= 0 = nil() tail(cons(x,xs)) = x + xs + 1 >= xs = xs a() = 1 >= 1 = b() a() = 1 >= 0 = c() problem: DPs: sumIter#(xs,x) -> ifSum#(isempty(xs),xs,x,plus(x,head(xs))) TRS: plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) -> y ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) sum(xs) -> sumIter(xs,0()) sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) -> x ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) isempty(nil()) -> true() isempty(cons(x,xs)) -> false() head(nil()) -> error() head(cons(x,xs)) -> x tail(nil()) -> nil() tail(cons(x,xs)) -> xs a() -> b() a() -> c() SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1 DPs: plusIter#(x,y,z) -> ifPlus#(le(x,z),x,y,z) ifPlus#(false(),x,y,z) -> plusIter#(x,s(y),s(z)) TRS: plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) -> y ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) sum(xs) -> sumIter(xs,0()) sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) -> x ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) isempty(nil()) -> true() isempty(cons(x,xs)) -> false() head(nil()) -> error() head(cons(x,xs)) -> x tail(nil()) -> nil() tail(cons(x,xs)) -> xs a() -> b() a() -> c() Open DPs: le#(s(x),s(y)) -> le#(x,y) TRS: plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) -> y ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) sum(xs) -> sumIter(xs,0()) sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) -> x ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) isempty(nil()) -> true() isempty(cons(x,xs)) -> false() head(nil()) -> error() head(cons(x,xs)) -> x tail(nil()) -> nil() tail(cons(x,xs)) -> xs a() -> b() a() -> c() Subterm Criterion Processor: simple projection: pi(le#) = 1 problem: DPs: TRS: plus(x,y) -> plusIter(x,y,0()) plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z) ifPlus(true(),x,y,z) -> y ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) sum(xs) -> sumIter(xs,0()) sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs))) ifSum(true(),xs,x,y) -> x ifSum(false(),xs,x,y) -> sumIter(tail(xs),y) isempty(nil()) -> true() isempty(cons(x,xs)) -> false() head(nil()) -> error() head(cons(x,xs)) -> x tail(nil()) -> nil() tail(cons(x,xs)) -> xs a() -> b() a() -> c() Qed