YES Problem: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) Proof: DP Processor: DPs: le#(s(x),s(y)) -> le#(x,y) minus#(x,s(y)) -> minus#(x,y) minus#(x,s(y)) -> pred#(minus(x,y)) gcd#(s(x),s(y)) -> le#(y,x) gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) if_gcd#(true(),s(x),s(y)) -> minus#(x,y) if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) if_gcd#(false(),s(x),s(y)) -> minus#(y,x) if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) TDG Processor: DPs: le#(s(x),s(y)) -> le#(x,y) minus#(x,s(y)) -> minus#(x,y) minus#(x,s(y)) -> pred#(minus(x,y)) gcd#(s(x),s(y)) -> le#(y,x) gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) if_gcd#(true(),s(x),s(y)) -> minus#(x,y) if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) if_gcd#(false(),s(x),s(y)) -> minus#(y,x) if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) graph: if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) -> gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) -> gcd#(s(x),s(y)) -> le#(y,x) if_gcd#(false(),s(x),s(y)) -> minus#(y,x) -> minus#(x,s(y)) -> pred#(minus(x,y)) if_gcd#(false(),s(x),s(y)) -> minus#(y,x) -> minus#(x,s(y)) -> minus#(x,y) if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) -> gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) -> gcd#(s(x),s(y)) -> le#(y,x) if_gcd#(true(),s(x),s(y)) -> minus#(x,y) -> minus#(x,s(y)) -> pred#(minus(x,y)) if_gcd#(true(),s(x),s(y)) -> minus#(x,y) -> minus#(x,s(y)) -> minus#(x,y) gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) -> if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) -> if_gcd#(false(),s(x),s(y)) -> minus#(y,x) gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) -> if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) -> if_gcd#(true(),s(x),s(y)) -> minus#(x,y) gcd#(s(x),s(y)) -> le#(y,x) -> le#(s(x),s(y)) -> le#(x,y) minus#(x,s(y)) -> minus#(x,y) -> minus#(x,s(y)) -> pred#(minus(x,y)) minus#(x,s(y)) -> minus#(x,y) -> minus#(x,s(y)) -> minus#(x,y) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) SCC Processor: #sccs: 3 #rules: 5 #arcs: 16/81 DPs: if_gcd#(false(),s(x),s(y)) -> gcd#(minus(y,x),s(x)) gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) Arctic Interpretation Processor: dimension: 1 interpretation: [if_gcd#](x0, x1, x2) = 3x0 + 1x1 + x2 + 0, [gcd#](x0, x1) = 3x0 + x1 + 0, [if_gcd](x0, x1, x2) = x0 + 3x1 + x2 + 0, [gcd](x0, x1) = 3x0 + x1 + 2, [minus](x0, x1) = x0 + 0, [pred](x0) = x0 + 0, [false] = 1, [s](x0) = 4x0 + 4, [true] = 2, [le](x0, x1) = 3x1 + 2, [0] = 0 orientation: if_gcd#(false(),s(x),s(y)) = 5x + 4y + 5 >= 4x + 3y + 4 = gcd#(minus(y,x),s(x)) gcd#(s(x),s(y)) = 7x + 4y + 7 >= 6x + 4y + 5 = if_gcd#(le(y,x),s(x),s(y)) if_gcd#(true(),s(x),s(y)) = 5x + 4y + 5 >= 3x + 4y + 4 = gcd#(minus(x,y),s(y)) le(0(),y) = 3y + 2 >= 2 = true() le(s(x),0()) = 3 >= 1 = false() le(s(x),s(y)) = 7y + 7 >= 3y + 2 = le(x,y) pred(s(x)) = 4x + 4 >= x = x minus(x,0()) = x + 0 >= x = x minus(x,s(y)) = x + 0 >= x + 0 = pred(minus(x,y)) gcd(0(),y) = y + 3 >= y = y gcd(s(x),0()) = 7x + 7 >= 4x + 4 = s(x) gcd(s(x),s(y)) = 7x + 4y + 7 >= 7x + 4y + 7 = if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) = 7x + 4y + 7 >= 3x + 4y + 4 = gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) = 7x + 4y + 7 >= 4x + 3y + 4 = gcd(minus(y,x),s(x)) problem: DPs: gcd#(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y)) if_gcd#(true(),s(x),s(y)) -> gcd#(minus(x,y),s(y)) TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) Arctic Interpretation Processor: dimension: 1 interpretation: [if_gcd#](x0, x1, x2) = x1, [gcd#](x0, x1) = 1x0, [if_gcd](x0, x1, x2) = x1 + x2, [gcd](x0, x1) = x0 + x1, [minus](x0, x1) = x0, [pred](x0) = x0, [false] = 0, [s](x0) = 3x0, [true] = 0, [le](x0, x1) = x0 + 0, [0] = 0 orientation: gcd#(s(x),s(y)) = 4x >= 3x = if_gcd#(le(y,x),s(x),s(y)) if_gcd#(true(),s(x),s(y)) = 3x >= 1x = gcd#(minus(x,y),s(y)) le(0(),y) = 0 >= 0 = true() le(s(x),0()) = 3x + 0 >= 0 = false() le(s(x),s(y)) = 3x + 0 >= x + 0 = le(x,y) pred(s(x)) = 3x >= x = x minus(x,0()) = x >= x = x minus(x,s(y)) = x >= x = pred(minus(x,y)) gcd(0(),y) = y + 0 >= y = y gcd(s(x),0()) = 3x + 0 >= 3x = s(x) gcd(s(x),s(y)) = 3x + 3y >= 3x + 3y = if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) = 3x + 3y >= x + 3y = gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) = 3x + 3y >= 3x + y = gcd(minus(y,x),s(x)) problem: DPs: TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) Qed DPs: minus#(x,s(y)) -> minus#(x,y) TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) Subterm Criterion Processor: simple projection: pi(minus#) = 1 problem: DPs: TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) Qed DPs: le#(s(x),s(y)) -> le#(x,y) TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) Subterm Criterion Processor: simple projection: pi(le#) = 1 problem: DPs: TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(minus(x,y)) gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) Qed