YES Problem: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Proof: DP Processor: DPs: minus_active#(s(x),s(y)) -> minus_active#(x,y) mark#(s(x)) -> mark#(x) mark#(minus(x,y)) -> minus_active#(x,y) mark#(ge(x,y)) -> ge_active#(x,y) ge_active#(s(x),s(y)) -> ge_active#(x,y) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) mark#(if(x,y,z)) -> mark#(x) mark#(if(x,y,z)) -> if_active#(mark(x),y,z) div_active#(s(x),s(y)) -> ge_active#(x,y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) if_active#(false(),x,y) -> mark#(y) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) TDG Processor: DPs: minus_active#(s(x),s(y)) -> minus_active#(x,y) mark#(s(x)) -> mark#(x) mark#(minus(x,y)) -> minus_active#(x,y) mark#(ge(x,y)) -> ge_active#(x,y) ge_active#(s(x),s(y)) -> ge_active#(x,y) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) mark#(if(x,y,z)) -> mark#(x) mark#(if(x,y,z)) -> if_active#(mark(x),y,z) div_active#(s(x),s(y)) -> ge_active#(x,y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) if_active#(false(),x,y) -> mark#(y) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) graph: if_active#(false(),x,y) -> mark#(y) -> mark#(if(x,y,z)) -> if_active#(mark(x),y,z) if_active#(false(),x,y) -> mark#(y) -> mark#(if(x,y,z)) -> mark#(x) if_active#(false(),x,y) -> mark#(y) -> mark#(div(x,y)) -> div_active#(mark(x),y) if_active#(false(),x,y) -> mark#(y) -> mark#(div(x,y)) -> mark#(x) if_active#(false(),x,y) -> mark#(y) -> mark#(ge(x,y)) -> ge_active#(x,y) if_active#(false(),x,y) -> mark#(y) -> mark#(minus(x,y)) -> minus_active#(x,y) if_active#(false(),x,y) -> mark#(y) -> mark#(s(x)) -> mark#(x) if_active#(true(),x,y) -> mark#(x) -> mark#(if(x,y,z)) -> if_active#(mark(x),y,z) if_active#(true(),x,y) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x) if_active#(true(),x,y) -> mark#(x) -> mark#(div(x,y)) -> div_active#(mark(x),y) if_active#(true(),x,y) -> mark#(x) -> mark#(div(x,y)) -> mark#(x) if_active#(true(),x,y) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y) if_active#(true(),x,y) -> mark#(x) -> mark#(minus(x,y)) -> minus_active#(x,y) if_active#(true(),x,y) -> mark#(x) -> mark#(s(x)) -> mark#(x) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) -> if_active#(false(),x,y) -> mark#(y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) -> if_active#(true(),x,y) -> mark#(x) div_active#(s(x),s(y)) -> ge_active#(x,y) -> ge_active#(s(x),s(y)) -> ge_active#(x,y) ge_active#(s(x),s(y)) -> ge_active#(x,y) -> ge_active#(s(x),s(y)) -> ge_active#(x,y) mark#(if(x,y,z)) -> if_active#(mark(x),y,z) -> if_active#(false(),x,y) -> mark#(y) mark#(if(x,y,z)) -> if_active#(mark(x),y,z) -> if_active#(true(),x,y) -> mark#(x) mark#(if(x,y,z)) -> mark#(x) -> mark#(if(x,y,z)) -> if_active#(mark(x),y,z) mark#(if(x,y,z)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x) mark#(if(x,y,z)) -> mark#(x) -> mark#(div(x,y)) -> div_active#(mark(x),y) mark#(if(x,y,z)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x) mark#(if(x,y,z)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y) mark#(if(x,y,z)) -> mark#(x) -> mark#(minus(x,y)) -> minus_active#(x,y) mark#(if(x,y,z)) -> mark#(x) -> mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) -> div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) mark#(div(x,y)) -> div_active#(mark(x),y) -> div_active#(s(x),s(y)) -> ge_active#(x,y) mark#(div(x,y)) -> mark#(x) -> mark#(if(x,y,z)) -> if_active#(mark(x),y,z) mark#(div(x,y)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x) mark#(div(x,y)) -> mark#(x) -> mark#(div(x,y)) -> div_active#(mark(x),y) mark#(div(x,y)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y) mark#(div(x,y)) -> mark#(x) -> mark#(minus(x,y)) -> minus_active#(x,y) mark#(div(x,y)) -> mark#(x) -> mark#(s(x)) -> mark#(x) mark#(ge(x,y)) -> ge_active#(x,y) -> ge_active#(s(x),s(y)) -> ge_active#(x,y) mark#(minus(x,y)) -> minus_active#(x,y) -> minus_active#(s(x),s(y)) -> minus_active#(x,y) mark#(s(x)) -> mark#(x) -> mark#(if(x,y,z)) -> if_active#(mark(x),y,z) mark#(s(x)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x) mark#(s(x)) -> mark#(x) -> mark#(div(x,y)) -> div_active#(mark(x),y) mark#(s(x)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x) mark#(s(x)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y) mark#(s(x)) -> mark#(x) -> mark#(minus(x,y)) -> minus_active#(x,y) mark#(s(x)) -> mark#(x) -> mark#(s(x)) -> mark#(x) minus_active#(s(x),s(y)) -> minus_active#(x,y) -> minus_active#(s(x),s(y)) -> minus_active#(x,y) SCC Processor: #sccs: 3 #rules: 10 #arcs: 46/169 DPs: if_active#(false(),x,y) -> mark#(y) mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) mark#(if(x,y,z)) -> mark#(x) mark#(if(x,y,z)) -> if_active#(mark(x),y,z) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [if_active#](x0, x1, x2) = x1 + x2 + 0, [div_active#](x0, x1) = 3x1 + 0, [mark#](x0) = x0 + 0, [if_active](x0, x1, x2) = x0 + 2x1 + 2x2 + 0, [if](x0, x1, x2) = 2x0 + x1 + 1x2 + 2, [div_active](x0, x1) = x0 + x1 + 0, [div](x0, x1) = x0 + 3x1 + 0, [ge](x0, x1) = 1x0 + -8x1 + -4, [false] = 7, [minus](x0, x1) = x1 + 0, [true] = 1, [ge_active](x0, x1) = 5x0 + 0, [s](x0) = x0, [mark](x0) = x0, [minus_active](x0, x1) = x0 + -2x1 + 0, [0] = 0 orientation: if_active#(false(),x,y) = x + y + 0 >= y + 0 = mark#(y) mark#(s(x)) = x + 0 >= x + 0 = mark#(x) mark#(div(x,y)) = x + 3y + 0 >= x + 0 = mark#(x) mark#(div(x,y)) = x + 3y + 0 >= 3y + 0 = div_active#(mark(x),y) div_active#(s(x),s(y)) = 3y + 0 >= 3y + 0 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = x + y + 0 >= x + 0 = mark#(x) mark#(if(x,y,z)) = 2x + y + 1z + 2 >= x + 0 = mark#(x) mark#(if(x,y,z)) = 2x + y + 1z + 2 >= y + z + 0 = if_active#(mark(x),y,z) minus_active(0(),y) = -2y + 0 >= 0 = 0() mark(0()) = 0 >= 0 = 0() minus_active(s(x),s(y)) = x + -2y + 0 >= x + -2y + 0 = minus_active(x,y) mark(s(x)) = x >= x = s(mark(x)) ge_active(x,0()) = 5x + 0 >= 1 = true() mark(minus(x,y)) = y + 0 >= x + -2y + 0 = minus_active(x,y) ge_active(0(),s(y)) = 5 >= 7 = false() mark(ge(x,y)) = 1x + -8y + -4 >= 5x + 0 = ge_active(x,y) ge_active(s(x),s(y)) = 5x + 0 >= 5x + 0 = ge_active(x,y) mark(div(x,y)) = x + 3y + 0 >= x + y + 0 = div_active(mark(x),y) div_active(0(),s(y)) = y + 0 >= 0 = 0() mark(if(x,y,z)) = 2x + y + 1z + 2 >= x + 2y + 2z + 0 = if_active(mark(x),y,z) div_active(s(x),s(y)) = x + y + 0 >= 5x + 5y + 2 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = 2x + 2y + 1 >= x = mark(x) minus_active(x,y) = x + -2y + 0 >= y + 0 = minus(x,y) if_active(false(),x,y) = 2x + 2y + 7 >= y = mark(y) ge_active(x,y) = 5x + 0 >= 1x + -8y + -4 = ge(x,y) if_active(x,y,z) = x + 2y + 2z + 0 >= 2x + y + 1z + 2 = if(x,y,z) div_active(x,y) = x + y + 0 >= x + 3y + 0 = div(x,y) problem: DPs: if_active#(false(),x,y) -> mark#(y) mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) mark#(if(x,y,z)) -> if_active#(mark(x),y,z) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Restore Modifier: DPs: if_active#(false(),x,y) -> mark#(y) mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) mark#(if(x,y,z)) -> if_active#(mark(x),y,z) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [if_active#](x0, x1, x2) = x1 + x2 + 0, [div_active#](x0, x1) = x1 + -16, [mark#](x0) = x0 + 0, [if_active](x0, x1, x2) = -8x0 + 2x2, [if](x0, x1, x2) = x0 + 1x1 + 2x2 + 1, [div_active](x0, x1) = x1 + 4, [div](x0, x1) = x0 + x1, [ge](x0, x1) = -8x0 + x1 + 0, [false] = 9, [minus](x0, x1) = 0, [true] = 6, [ge_active](x0, x1) = x0 + x1, [s](x0) = x0 + 0, [mark](x0) = x0 + 0, [minus_active](x0, x1) = x0 + 2x1 + 8, [0] = 0 orientation: if_active#(false(),x,y) = x + y + 0 >= y + 0 = mark#(y) mark#(s(x)) = x + 0 >= x + 0 = mark#(x) mark#(div(x,y)) = x + y + 0 >= x + 0 = mark#(x) mark#(div(x,y)) = x + y + 0 >= y + -16 = div_active#(mark(x),y) div_active#(s(x),s(y)) = y + 0 >= y + 0 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = x + y + 0 >= x + 0 = mark#(x) mark#(if(x,y,z)) = x + 1y + 2z + 1 >= y + z + 0 = if_active#(mark(x),y,z) minus_active(0(),y) = 2y + 8 >= 0 = 0() mark(0()) = 0 >= 0 = 0() minus_active(s(x),s(y)) = x + 2y + 8 >= x + 2y + 8 = minus_active(x,y) mark(s(x)) = x + 0 >= x + 0 = s(mark(x)) ge_active(x,0()) = x + 0 >= 6 = true() mark(minus(x,y)) = 0 >= x + 2y + 8 = minus_active(x,y) ge_active(0(),s(y)) = y + 0 >= 9 = false() mark(ge(x,y)) = -8x + y + 0 >= x + y = ge_active(x,y) ge_active(s(x),s(y)) = x + y + 0 >= x + y = ge_active(x,y) mark(div(x,y)) = x + y + 0 >= y + 4 = div_active(mark(x),y) div_active(0(),s(y)) = y + 4 >= 0 = 0() mark(if(x,y,z)) = x + 1y + 2z + 1 >= -8x + 2z + -8 = if_active(mark(x),y,z) div_active(s(x),s(y)) = y + 4 >= -8x + -8y + 2 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = 2y + -2 >= x + 0 = mark(x) minus_active(x,y) = x + 2y + 8 >= 0 = minus(x,y) if_active(false(),x,y) = 2y + 1 >= y + 0 = mark(y) ge_active(x,y) = x + y >= -8x + y + 0 = ge(x,y) if_active(x,y,z) = -8x + 2z >= x + 1y + 2z + 1 = if(x,y,z) div_active(x,y) = y + 4 >= x + y = div(x,y) problem: DPs: if_active#(false(),x,y) -> mark#(y) mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Restore Modifier: DPs: if_active#(false(),x,y) -> mark#(y) mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) ge_active(x,y) -> ge(x,y) interpretation: [if_active#](x0, x1, x2) = -7x0 + x1 + 2x2 + -16, [div_active#](x0, x1) = 3x1, [mark#](x0) = x0 + -16, [if_active](x0, x1, x2) = 4x1 + 7x2 + 0, [if](x0, x1, x2) = 4x0 + 1x1 + 4x2 + 4, [div_active](x0, x1) = x0 + 4x1 + 0, [div](x0, x1) = x0 + 3x1 + -7, [ge](x0, x1) = x1, [false] = 7, [minus](x0, x1) = -8x1 + 0, [true] = 0, [ge_active](x0, x1) = 7x1, [s](x0) = x0 + 0, [mark](x0) = x0 + 6, [minus_active](x0, x1) = x0 + 1x1 + 2, [0] = 0 orientation: if_active#(false(),x,y) = x + 2y + 0 >= y + -16 = mark#(y) mark#(s(x)) = x + 0 >= x + -16 = mark#(x) mark#(div(x,y)) = x + 3y + -7 >= x + -16 = mark#(x) mark#(div(x,y)) = x + 3y + -7 >= 3y = div_active#(mark(x),y) div_active#(s(x),s(y)) = 3y + 3 >= 3y + 3 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = x + 2y + -7 >= x + -16 = mark#(x) minus_active(0(),y) = 1y + 2 >= 0 = 0() mark(0()) = 6 >= 0 = 0() minus_active(s(x),s(y)) = x + 1y + 2 >= x + 1y + 2 = minus_active(x,y) mark(s(x)) = x + 6 >= x + 6 = s(mark(x)) ge_active(x,0()) = 7 >= 0 = true() mark(minus(x,y)) = -8y + 6 >= x + 1y + 2 = minus_active(x,y) ge_active(0(),s(y)) = 7y + 7 >= 7 = false() mark(ge(x,y)) = y + 6 >= 7y = ge_active(x,y) ge_active(s(x),s(y)) = 7y + 7 >= 7y = ge_active(x,y) mark(div(x,y)) = x + 3y + 6 >= x + 4y + 6 = div_active(mark(x),y) div_active(0(),s(y)) = 4y + 4 >= 0 = 0() mark(if(x,y,z)) = 4x + 1y + 4z + 6 >= 4y + 7z + 0 = if_active(mark(x),y,z) div_active(s(x),s(y)) = x + 4y + 4 >= 7y + 7 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = 4x + 7y + 0 >= x + 6 = mark(x) minus_active(x,y) = x + 1y + 2 >= -8y + 0 = minus(x,y) if_active(false(),x,y) = 4x + 7y + 0 >= y + 6 = mark(y) ge_active(x,y) = 7y >= y = ge(x,y) if_active(x,y,z) = 4y + 7z + 0 >= 4x + 1y + 4z + 4 = if(x,y,z) div_active(x,y) = x + 4y + 0 >= x + 3y + -7 = div(x,y) problem: DPs: mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Restore Modifier: DPs: mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [if_active#](x0, x1, x2) = 1x1 + x2 + 2, [div_active#](x0, x1) = 4x1 + 0, [mark#](x0) = 1x0 + -16, [if_active](x0, x1, x2) = x0 + 2x1 + -16, [if](x0, x1, x2) = 1x0 + 6x1 + x2 + 0, [div_active](x0, x1) = 2x0 + x1 + 0, [div](x0, x1) = 1x0 + 3x1 + 0, [ge](x0, x1) = 4x0 + 8x1 + 6, [false] = 6, [minus](x0, x1) = 2x1 + 0, [true] = 2, [ge_active](x0, x1) = 2x0 + x1 + 0, [s](x0) = x0 + -2, [mark](x0) = 0, [minus_active](x0, x1) = x0 + 4x1 + -16, [0] = 2 orientation: mark#(s(x)) = 1x + -1 >= 1x + -16 = mark#(x) mark#(div(x,y)) = 2x + 4y + 1 >= 1x + -16 = mark#(x) mark#(div(x,y)) = 2x + 4y + 1 >= 4y + 0 = div_active#(mark(x),y) div_active#(s(x),s(y)) = 4y + 2 >= 4y + 2 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = 1x + y + 2 >= 1x + -16 = mark#(x) minus_active(0(),y) = 4y + 2 >= 2 = 0() mark(0()) = 0 >= 2 = 0() minus_active(s(x),s(y)) = x + 4y + 2 >= x + 4y + -16 = minus_active(x,y) mark(s(x)) = 0 >= 0 = s(mark(x)) ge_active(x,0()) = 2x + 2 >= 2 = true() mark(minus(x,y)) = 0 >= x + 4y + -16 = minus_active(x,y) ge_active(0(),s(y)) = y + 4 >= 6 = false() mark(ge(x,y)) = 0 >= 2x + y + 0 = ge_active(x,y) ge_active(s(x),s(y)) = 2x + y + 0 >= 2x + y + 0 = ge_active(x,y) mark(div(x,y)) = 0 >= y + 2 = div_active(mark(x),y) div_active(0(),s(y)) = y + 4 >= 2 = 0() mark(if(x,y,z)) = 0 >= 2y + 0 = if_active(mark(x),y,z) div_active(s(x),s(y)) = 2x + y + 0 >= 2x + 5y + 3 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = 2x + 2 >= 0 = mark(x) minus_active(x,y) = x + 4y + -16 >= 2y + 0 = minus(x,y) if_active(false(),x,y) = 2x + 6 >= 0 = mark(y) ge_active(x,y) = 2x + y + 0 >= 4x + 8y + 6 = ge(x,y) if_active(x,y,z) = x + 2y + -16 >= 1x + 6y + z + 0 = if(x,y,z) div_active(x,y) = 2x + y + 0 >= 1x + 3y + 0 = div(x,y) problem: DPs: mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Restore Modifier: DPs: mark#(s(x)) -> mark#(x) mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) interpretation: [if_active#](x0, x1, x2) = x1 + 5x2, [div_active#](x0, x1) = x0 + 0, [mark#](x0) = x0, [if_active](x0, x1, x2) = x0 + 1x1 + 4x2 + 0, [if](x0, x1, x2) = x0 + 1x1 + 4x2, [div_active](x0, x1) = 1x0 + 0, [div](x0, x1) = 1x0 + 0, [ge](x0, x1) = x0, [false] = 0, [minus](x0, x1) = 3, [true] = 0, [ge_active](x0, x1) = x0 + 0, [s](x0) = 2x0 + 6, [mark](x0) = 1x0 + 0, [minus_active](x0, x1) = 4, [0] = 1 orientation: mark#(s(x)) = 2x + 6 >= x = mark#(x) mark#(div(x,y)) = 1x + 0 >= 1x + 0 = div_active#(mark(x),y) div_active#(s(x),s(y)) = 2x + 6 >= 6 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = x + 5y >= x = mark#(x) minus_active(0(),y) = 4 >= 1 = 0() mark(0()) = 2 >= 1 = 0() minus_active(s(x),s(y)) = 4 >= 4 = minus_active(x,y) mark(s(x)) = 3x + 7 >= 3x + 6 = s(mark(x)) ge_active(x,0()) = x + 0 >= 0 = true() mark(minus(x,y)) = 4 >= 4 = minus_active(x,y) ge_active(0(),s(y)) = 1 >= 0 = false() mark(ge(x,y)) = 1x + 0 >= x + 0 = ge_active(x,y) ge_active(s(x),s(y)) = 2x + 6 >= x + 0 = ge_active(x,y) mark(div(x,y)) = 2x + 1 >= 2x + 1 = div_active(mark(x),y) div_active(0(),s(y)) = 2 >= 1 = 0() mark(if(x,y,z)) = 1x + 2y + 5z + 0 >= 1x + 1y + 4z + 0 = if_active(mark(x),y,z) div_active(s(x),s(y)) = 3x + 7 >= x + 7 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = 1x + 4y + 0 >= 1x + 0 = mark(x) minus_active(x,y) = 4 >= 3 = minus(x,y) if_active(false(),x,y) = 1x + 4y + 0 >= 1y + 0 = mark(y) ge_active(x,y) = x + 0 >= x = ge(x,y) if_active(x,y,z) = x + 1y + 4z + 0 >= x + 1y + 4z = if(x,y,z) div_active(x,y) = 1x + 0 >= 1x + 0 = div(x,y) problem: DPs: mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Restore Modifier: DPs: mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) -> mark#(x) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) interpretation: [if_active#](x0, x1, x2) = 4x0 + 1x1 + 5, [div_active#](x0, x1) = x0 + 6x1 + 0, [mark#](x0) = x0, [if_active](x0, x1, x2) = x1 + 4x2 + 1, [if](x0, x1, x2) = x1 + 4x2 + 1, [div_active](x0, x1) = x0 + 6x1 + 0, [div](x0, x1) = x0 + 6x1 + 0, [ge](x0, x1) = 2, [false] = 2, [minus](x0, x1) = 0, [true] = 0, [ge_active](x0, x1) = 2, [s](x0) = 0, [mark](x0) = x0, [minus_active](x0, x1) = 0, [0] = 0 orientation: mark#(div(x,y)) = x + 6y + 0 >= x + 6y + 0 = div_active#(mark(x),y) div_active#(s(x),s(y)) = 6 >= 6 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = 1x + 5 >= x = mark#(x) minus_active(0(),y) = 0 >= 0 = 0() mark(0()) = 0 >= 0 = 0() minus_active(s(x),s(y)) = 0 >= 0 = minus_active(x,y) mark(s(x)) = 0 >= 0 = s(mark(x)) ge_active(x,0()) = 2 >= 0 = true() mark(minus(x,y)) = 0 >= 0 = minus_active(x,y) ge_active(0(),s(y)) = 2 >= 2 = false() mark(ge(x,y)) = 2 >= 2 = ge_active(x,y) ge_active(s(x),s(y)) = 2 >= 2 = ge_active(x,y) mark(div(x,y)) = x + 6y + 0 >= x + 6y + 0 = div_active(mark(x),y) div_active(0(),s(y)) = 6 >= 0 = 0() mark(if(x,y,z)) = y + 4z + 1 >= y + 4z + 1 = if_active(mark(x),y,z) div_active(s(x),s(y)) = 6 >= 4 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = x + 4y + 1 >= x = mark(x) minus_active(x,y) = 0 >= 0 = minus(x,y) if_active(false(),x,y) = x + 4y + 1 >= y = mark(y) ge_active(x,y) = 2 >= 2 = ge(x,y) if_active(x,y,z) = y + 4z + 1 >= y + 4z + 1 = if(x,y,z) div_active(x,y) = x + 6y + 0 >= x + 6y + 0 = div(x,y) problem: DPs: mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Restore Modifier: DPs: mark#(div(x,y)) -> div_active#(mark(x),y) div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) SCC Processor: #sccs: 0 #rules: 0 #arcs: 30/4 DPs: ge_active#(s(x),s(y)) -> ge_active#(x,y) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Subterm Criterion Processor: simple projection: pi(ge_active#) = 0 problem: DPs: TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Qed DPs: minus_active#(s(x),s(y)) -> minus_active#(x,y) TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Subterm Criterion Processor: simple projection: pi(minus_active#) = 0 problem: DPs: TRS: minus_active(0(),y) -> 0() mark(0()) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) ge_active(x,0()) -> true() mark(minus(x,y)) -> minus_active(x,y) ge_active(0(),s(y)) -> false() mark(ge(x,y)) -> ge_active(x,y) ge_active(s(x),s(y)) -> ge_active(x,y) mark(div(x,y)) -> div_active(mark(x),y) div_active(0(),s(y)) -> 0() mark(if(x,y,z)) -> if_active(mark(x),y,z) div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) -> mark(x) minus_active(x,y) -> minus(x,y) if_active(false(),x,y) -> mark(y) ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) div_active(x,y) -> div(x,y) Qed