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 + 4, [div_active#](x0, x1) = x1 + 4, [mark#](x0) = x0 + 4, [if_active](x0, x1, x2) = x0 + 2x1 + x2 + 0, [if](x0, x1, x2) = 7x0 + 1x1 + x2 + 7, [div_active](x0, x1) = x0 + x1 + 0, [div](x0, x1) = x0 + x1 + 4, [ge](x0, x1) = x0 + x1 + 3, [false] = 0, [minus](x0, x1) = x1 + 4, [true] = 0, [ge_active](x0, x1) = x0 + x1 + 0, [s](x0) = x0, [mark](x0) = x0 + 0, [minus_active](x0, x1) = x0 + x1 + 0, [0] = 0 orientation: if_active#(false(),x,y) = x + y + 4 >= y + 4 = mark#(y) mark#(s(x)) = x + 4 >= x + 4 = mark#(x) mark#(div(x,y)) = x + y + 4 >= x + 4 = mark#(x) mark#(div(x,y)) = x + y + 4 >= y + 4 = div_active#(mark(x),y) div_active#(s(x),s(y)) = y + 4 >= y + 4 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = x + y + 4 >= x + 4 = mark#(x) mark#(if(x,y,z)) = 7x + 1y + z + 7 >= x + 4 = mark#(x) mark#(if(x,y,z)) = 7x + 1y + z + 7 >= y + z + 4 = if_active#(mark(x),y,z) minus_active(0(),y) = y + 0 >= 0 = 0() mark(0()) = 0 >= 0 = 0() minus_active(s(x),s(y)) = x + y + 0 >= x + y + 0 = minus_active(x,y) mark(s(x)) = x + 0 >= x + 0 = s(mark(x)) ge_active(x,0()) = x + 0 >= 0 = true() mark(minus(x,y)) = y + 4 >= x + y + 0 = minus_active(x,y) ge_active(0(),s(y)) = y + 0 >= 0 = false() mark(ge(x,y)) = x + y + 3 >= x + y + 0 = ge_active(x,y) ge_active(s(x),s(y)) = x + y + 0 >= x + y + 0 = ge_active(x,y) mark(div(x,y)) = x + y + 4 >= x + y + 0 = div_active(mark(x),y) div_active(0(),s(y)) = y + 0 >= 0 = 0() mark(if(x,y,z)) = 7x + 1y + z + 7 >= x + 2y + z + 0 = if_active(mark(x),y,z) div_active(s(x),s(y)) = x + y + 0 >= x + 2y + 6 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = 2x + y + 0 >= x + 0 = mark(x) minus_active(x,y) = x + y + 0 >= y + 4 = minus(x,y) if_active(false(),x,y) = 2x + y + 0 >= y + 0 = mark(y) ge_active(x,y) = x + y + 0 >= x + y + 3 = ge(x,y) if_active(x,y,z) = x + 2y + z + 0 >= 7x + 1y + z + 7 = if(x,y,z) div_active(x,y) = x + y + 0 >= x + y + 4 = 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, [mark#](x0) = x0, [if_active](x0, x1, x2) = x0 + x1 + x2 + 0, [if](x0, x1, x2) = x0 + 1x1 + 6x2 + 1, [div_active](x0, x1) = x0 + x1 + 0, [div](x0, x1) = x0 + x1, [ge](x0, x1) = 4x0 + x1 + 2, [false] = 0, [minus](x0, x1) = x1, [true] = 4, [ge_active](x0, x1) = 4x0 + 0, [s](x0) = x0 + 1, [mark](x0) = x0 + 0, [minus_active](x0, x1) = 3x0 + 2x1 + 0, [0] = 0 orientation: if_active#(false(),x,y) = x + y + 0 >= y = mark#(y) mark#(s(x)) = x + 1 >= x = mark#(x) mark#(div(x,y)) = x + y >= x = mark#(x) mark#(div(x,y)) = x + y >= y = div_active#(mark(x),y) div_active#(s(x),s(y)) = y + 1 >= y + 1 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = x + y + 0 >= x = mark#(x) mark#(if(x,y,z)) = x + 1y + 6z + 1 >= y + z + 0 = if_active#(mark(x),y,z) minus_active(0(),y) = 2y + 3 >= 0 = 0() mark(0()) = 0 >= 0 = 0() minus_active(s(x),s(y)) = 3x + 2y + 4 >= 3x + 2y + 0 = minus_active(x,y) mark(s(x)) = x + 1 >= x + 1 = s(mark(x)) ge_active(x,0()) = 4x + 0 >= 4 = true() mark(minus(x,y)) = y + 0 >= 3x + 2y + 0 = minus_active(x,y) ge_active(0(),s(y)) = 4 >= 0 = false() mark(ge(x,y)) = 4x + y + 2 >= 4x + 0 = ge_active(x,y) ge_active(s(x),s(y)) = 4x + 5 >= 4x + 0 = ge_active(x,y) mark(div(x,y)) = x + y + 0 >= x + y + 0 = div_active(mark(x),y) div_active(0(),s(y)) = y + 1 >= 0 = 0() mark(if(x,y,z)) = x + 1y + 6z + 1 >= x + y + z + 0 = if_active(mark(x),y,z) div_active(s(x),s(y)) = x + y + 1 >= 4x + y + 1 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = x + y + 4 >= x + 0 = mark(x) minus_active(x,y) = 3x + 2y + 0 >= y = minus(x,y) if_active(false(),x,y) = x + y + 0 >= y + 0 = mark(y) ge_active(x,y) = 4x + 0 >= 4x + y + 2 = ge(x,y) if_active(x,y,z) = x + y + z + 0 >= x + 1y + 6z + 1 = if(x,y,z) div_active(x,y) = x + y + 0 >= 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: 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 + x2, [div_active#](x0, x1) = 6x0 + x1, [mark#](x0) = x0, [if_active](x0, x1, x2) = x1 + 6x2 + -7, [if](x0, x1, x2) = x1 + 6x2 + -7, [div_active](x0, x1) = 6x0 + x1 + 0, [div](x0, x1) = 6x0 + x1 + 0, [ge](x0, x1) = x0 + x1 + 0, [false] = 0, [minus](x0, x1) = x0 + -6x1 + -2, [true] = 0, [ge_active](x0, x1) = x0 + x1 + 0, [s](x0) = x0 + 0, [mark](x0) = x0, [minus_active](x0, x1) = x0 + -6x1 + -2, [0] = 0 orientation: if_active#(false(),x,y) = x + y >= y = mark#(y) mark#(s(x)) = x + 0 >= x = mark#(x) mark#(div(x,y)) = 6x + y + 0 >= x = mark#(x) mark#(div(x,y)) = 6x + y + 0 >= 6x + y = div_active#(mark(x),y) div_active#(s(x),s(y)) = 6x + y + 6 >= 6x + y + 4 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = x + y >= x = mark#(x) minus_active(0(),y) = -6y + 0 >= 0 = 0() mark(0()) = 0 >= 0 = 0() minus_active(s(x),s(y)) = x + -6y + 0 >= x + -6y + -2 = minus_active(x,y) mark(s(x)) = x + 0 >= x + 0 = s(mark(x)) ge_active(x,0()) = x + 0 >= 0 = true() mark(minus(x,y)) = x + -6y + -2 >= x + -6y + -2 = minus_active(x,y) ge_active(0(),s(y)) = y + 0 >= 0 = false() mark(ge(x,y)) = x + y + 0 >= x + y + 0 = ge_active(x,y) ge_active(s(x),s(y)) = x + y + 0 >= x + y + 0 = ge_active(x,y) mark(div(x,y)) = 6x + y + 0 >= 6x + y + 0 = div_active(mark(x),y) div_active(0(),s(y)) = y + 6 >= 0 = 0() mark(if(x,y,z)) = y + 6z + -7 >= y + 6z + -7 = if_active(mark(x),y,z) div_active(s(x),s(y)) = 6x + y + 6 >= 6x + y + 6 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = x + 6y + -7 >= x = mark(x) minus_active(x,y) = x + -6y + -2 >= x + -6y + -2 = minus(x,y) if_active(false(),x,y) = x + 6y + -7 >= y = mark(y) ge_active(x,y) = x + y + 0 >= x + y + 0 = ge(x,y) if_active(x,y,z) = y + 6z + -7 >= y + 6z + -7 = if(x,y,z) div_active(x,y) = 6x + y + 0 >= 6x + y + 0 = div(x,y) problem: DPs: if_active#(false(),x,y) -> mark#(y) 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: if_active#(false(),x,y) -> mark#(y) 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) = x0 + x1 + 1x2 + 0, [div_active#](x0, x1) = x0 + 1x1 + 0, [mark#](x0) = x0, [if_active](x0, x1, x2) = x1 + 1x2 + 0, [if](x0, x1, x2) = x1 + 1x2, [div_active](x0, x1) = x0 + 1x1 + 0, [div](x0, x1) = x0 + 1x1 + 0, [ge](x0, x1) = 1x1, [false] = 0, [minus](x0, x1) = x0 + x1, [true] = 0, [ge_active](x0, x1) = 1x1 + 0, [s](x0) = x0 + 0, [mark](x0) = x0 + 0, [minus_active](x0, x1) = x0 + x1, [0] = 0 orientation: if_active#(false(),x,y) = x + 1y + 0 >= y = mark#(y) mark#(s(x)) = x + 0 >= x = mark#(x) mark#(div(x,y)) = x + 1y + 0 >= x + 1y + 0 = div_active#(mark(x),y) div_active#(s(x),s(y)) = x + 1y + 1 >= x + 1y + 1 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = x + 1y + 0 >= x = mark#(x) minus_active(0(),y) = y + 0 >= 0 = 0() mark(0()) = 0 >= 0 = 0() minus_active(s(x),s(y)) = x + y + 0 >= x + y = minus_active(x,y) mark(s(x)) = x + 0 >= x + 0 = s(mark(x)) ge_active(x,0()) = 1 >= 0 = true() mark(minus(x,y)) = x + y + 0 >= x + y = minus_active(x,y) ge_active(0(),s(y)) = 1y + 1 >= 0 = false() mark(ge(x,y)) = 1y + 0 >= 1y + 0 = ge_active(x,y) ge_active(s(x),s(y)) = 1y + 1 >= 1y + 0 = ge_active(x,y) mark(div(x,y)) = x + 1y + 0 >= x + 1y + 0 = div_active(mark(x),y) div_active(0(),s(y)) = 1y + 1 >= 0 = 0() mark(if(x,y,z)) = y + 1z + 0 >= y + 1z + 0 = if_active(mark(x),y,z) div_active(s(x),s(y)) = x + 1y + 1 >= x + 1y + 1 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = x + 1y + 0 >= x + 0 = mark(x) minus_active(x,y) = x + y >= x + y = minus(x,y) if_active(false(),x,y) = x + 1y + 0 >= y + 0 = mark(y) ge_active(x,y) = 1y + 0 >= 1y = ge(x,y) if_active(x,y,z) = y + 1z + 0 >= y + 1z = if(x,y,z) div_active(x,y) = x + 1y + 0 >= x + 1y + 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) Matrix Interpretation Processor: dim=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) = 3x1 + 2, [div_active#](x0, x1) = 5x0 + 1, [mark#](x0) = 3x0 + 2, [if_active](x0, x1, x2) = 4x0 + 3x1 + 5x2 + 4, [if](x0, x1, x2) = 4x0 + 2x1 + 4x2 + 4, [div_active](x0, x1) = 6x0, [div](x0, x1) = 6x0, [ge](x0, x1) = 3x0, [false] = 0, [minus](x0, x1) = 0, [true] = 0, [ge_active](x0, x1) = 4x0, [s](x0) = 4x0 + 2, [mark](x0) = 3x0, [minus_active](x0, x1) = 0, [0] = 0 orientation: mark#(s(x)) = 12x + 8 >= 3x + 2 = mark#(x) mark#(div(x,y)) = 18x + 2 >= 15x + 1 = div_active#(mark(x),y) div_active#(s(x),s(y)) = 20x + 11 >= 8 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active#(true(),x,y) = 3x + 2 >= 3x + 2 = 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)) = 12x + 6 >= 12x + 2 = s(mark(x)) ge_active(x,0()) = 4x >= 0 = true() mark(minus(x,y)) = 0 >= 0 = minus_active(x,y) ge_active(0(),s(y)) = 0 >= 0 = false() mark(ge(x,y)) = 9x >= 4x = ge_active(x,y) ge_active(s(x),s(y)) = 16x + 8 >= 4x = ge_active(x,y) mark(div(x,y)) = 18x >= 18x = div_active(mark(x),y) div_active(0(),s(y)) = 0 >= 0 = 0() mark(if(x,y,z)) = 12x + 6y + 12z + 12 >= 12x + 3y + 5z + 4 = if_active(mark(x),y,z) div_active(s(x),s(y)) = 24x + 12 >= 16x + 10 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) if_active(true(),x,y) = 3x + 5y + 4 >= 3x = mark(x) minus_active(x,y) = 0 >= 0 = minus(x,y) if_active(false(),x,y) = 3x + 5y + 4 >= 3y = mark(y) ge_active(x,y) = 4x >= 3x = ge(x,y) if_active(x,y,z) = 4x + 3y + 5z + 4 >= 4x + 2y + 4z + 4 = if(x,y,z) div_active(x,y) = 6x >= 6x = div(x,y) problem: DPs: 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#(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) SCC Processor: #sccs: 0 #rules: 0 #arcs: 30/1 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#) = 1 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#) = 1 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