YES Problem: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Proof: DP Processor: DPs: minus#(X,s(Y)) -> minus#(X,Y) minus#(X,s(Y)) -> pred#(minus(X,Y)) le#(s(X),s(Y)) -> le#(X,Y) gcd#(s(X),s(Y)) -> le#(Y,X) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) if#(true(),s(X),s(Y)) -> minus#(X,Y) if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) if#(false(),s(X),s(Y)) -> minus#(Y,X) if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Usable Rule Processor: DPs: minus#(X,s(Y)) -> minus#(X,Y) minus#(X,s(Y)) -> pred#(minus(X,Y)) le#(s(X),s(Y)) -> le#(X,Y) gcd#(s(X),s(Y)) -> le#(Y,X) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) if#(true(),s(X),s(Y)) -> minus#(X,Y) if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) if#(false(),s(X),s(Y)) -> minus#(Y,X) if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) TRS: f14(x,y) -> x f14(x,y) -> y minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() CDG Processor: DPs: minus#(X,s(Y)) -> minus#(X,Y) minus#(X,s(Y)) -> pred#(minus(X,Y)) le#(s(X),s(Y)) -> le#(X,Y) gcd#(s(X),s(Y)) -> le#(Y,X) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) if#(true(),s(X),s(Y)) -> minus#(X,Y) if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) if#(false(),s(X),s(Y)) -> minus#(Y,X) if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) TRS: f14(x,y) -> x f14(x,y) -> y minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() graph: if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) -> gcd#(s(X),s(Y)) -> le#(Y,X) if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) -> gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) if#(true(),s(X),s(Y)) -> minus#(X,Y) -> minus#(X,s(Y)) -> minus#(X,Y) if#(true(),s(X),s(Y)) -> minus#(X,Y) -> minus#(X,s(Y)) -> pred#(minus(X,Y)) if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) -> gcd#(s(X),s(Y)) -> le#(Y,X) if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) -> gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) if#(false(),s(X),s(Y)) -> minus#(Y,X) -> minus#(X,s(Y)) -> minus#(X,Y) if#(false(),s(X),s(Y)) -> minus#(Y,X) -> minus#(X,s(Y)) -> pred#(minus(X,Y)) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) -> if#(true(),s(X),s(Y)) -> minus#(X,Y) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) -> if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) -> if#(false(),s(X),s(Y)) -> minus#(Y,X) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) -> if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) gcd#(s(X),s(Y)) -> le#(Y,X) -> le#(s(X),s(Y)) -> le#(X,Y) le#(s(X),s(Y)) -> le#(X,Y) -> le#(s(X),s(Y)) -> le#(X,Y) minus#(X,s(Y)) -> minus#(X,Y) -> minus#(X,s(Y)) -> minus#(X,Y) minus#(X,s(Y)) -> minus#(X,Y) -> minus#(X,s(Y)) -> pred#(minus(X,Y)) Restore Modifier: DPs: minus#(X,s(Y)) -> minus#(X,Y) minus#(X,s(Y)) -> pred#(minus(X,Y)) le#(s(X),s(Y)) -> le#(X,Y) gcd#(s(X),s(Y)) -> le#(Y,X) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) if#(true(),s(X),s(Y)) -> minus#(X,Y) if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) if#(false(),s(X),s(Y)) -> minus#(Y,X) if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) SCC Processor: #sccs: 3 #rules: 5 #arcs: 16/81 DPs: if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) gcd#(s(X),s(Y)) -> if#(le(Y,X),s(X),s(Y)) if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [if#](x0, x1, x2) = x1 + x2, [gcd#](x0, x1) = x0 + x1 + 1, [if](x0, x1, x2) = x1 + x2 + 1, [gcd](x0, x1) = x0 + x1 + 1, [true] = 0, [false] = 0, [le](x0, x1) = 0, [0] = 1, [pred](x0) = x0, [minus](x0, x1) = x0, [s](x0) = x0 + 1 orientation: if#(true(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd#(minus(X,Y),s(Y)) gcd#(s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = if#(le(Y,X),s(X),s(Y)) if#(false(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd#(minus(Y,X),s(X)) minus(X,s(Y)) = X >= X = pred(minus(X,Y)) minus(X,0()) = X >= X = X pred(s(X)) = X + 1 >= X = X le(s(X),s(Y)) = 0 >= 0 = le(X,Y) le(s(X),0()) = 0 >= 0 = false() le(0(),Y) = 0 >= 0 = true() gcd(0(),Y) = Y + 2 >= 1 = 0() gcd(s(X),0()) = X + 3 >= X + 1 = s(X) gcd(s(X),s(Y)) = X + Y + 3 >= X + Y + 3 = if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = gcd(minus(Y,X),s(X)) problem: DPs: if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) if#(false(),s(X),s(Y)) -> gcd#(minus(Y,X),s(X)) TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [if#](x0, x1, x2) = x0, [gcd#](x0, x1) = 0, [if](x0, x1, x2) = x1 + x2, [gcd](x0, x1) = x0 + x1, [true] = 0, [false] = 1, [le](x0, x1) = 1, [0] = 0, [pred](x0) = x0, [minus](x0, x1) = x0 + 1, [s](x0) = x0 + 1 orientation: if#(true(),s(X),s(Y)) = 0 >= 0 = gcd#(minus(X,Y),s(Y)) if#(false(),s(X),s(Y)) = 1 >= 0 = gcd#(minus(Y,X),s(X)) minus(X,s(Y)) = X + 1 >= X + 1 = pred(minus(X,Y)) minus(X,0()) = X + 1 >= X = X pred(s(X)) = X + 1 >= X = X le(s(X),s(Y)) = 1 >= 1 = le(X,Y) le(s(X),0()) = 1 >= 1 = false() le(0(),Y) = 1 >= 0 = true() gcd(0(),Y) = Y >= 0 = 0() gcd(s(X),0()) = X + 1 >= X + 1 = s(X) gcd(s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(Y,X),s(X)) problem: DPs: if#(true(),s(X),s(Y)) -> gcd#(minus(X,Y),s(Y)) TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [if#](x0, x1, x2) = x2, [gcd#](x0, x1) = 0, [if](x0, x1, x2) = x1 + x2 + 1, [gcd](x0, x1) = x0 + x1 + 1, [true] = 1, [false] = 1, [le](x0, x1) = 1, [0] = 0, [pred](x0) = x0, [minus](x0, x1) = x0, [s](x0) = x0 + 1 orientation: if#(true(),s(X),s(Y)) = Y + 1 >= 0 = gcd#(minus(X,Y),s(Y)) minus(X,s(Y)) = X >= X = pred(minus(X,Y)) minus(X,0()) = X >= X = X pred(s(X)) = X + 1 >= X = X le(s(X),s(Y)) = 1 >= 1 = le(X,Y) le(s(X),0()) = 1 >= 1 = false() le(0(),Y) = 1 >= 1 = true() gcd(0(),Y) = Y + 1 >= 0 = 0() gcd(s(X),0()) = X + 2 >= X + 1 = s(X) gcd(s(X),s(Y)) = X + Y + 3 >= X + Y + 3 = if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) = X + Y + 3 >= X + Y + 2 = gcd(minus(Y,X),s(X)) problem: DPs: TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Qed DPs: minus#(X,s(Y)) -> minus#(X,Y) TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [minus#](x0, x1) = x1 + 1, [if](x0, x1, x2) = x1 + x2, [gcd](x0, x1) = x0 + x1, [true] = 0, [false] = 0, [le](x0, x1) = 0, [0] = 0, [pred](x0) = x0, [minus](x0, x1) = x0 + 1, [s](x0) = x0 + 1 orientation: minus#(X,s(Y)) = Y + 2 >= Y + 1 = minus#(X,Y) minus(X,s(Y)) = X + 1 >= X + 1 = pred(minus(X,Y)) minus(X,0()) = X + 1 >= X = X pred(s(X)) = X + 1 >= X = X le(s(X),s(Y)) = 0 >= 0 = le(X,Y) le(s(X),0()) = 0 >= 0 = false() le(0(),Y) = 0 >= 0 = true() gcd(0(),Y) = Y >= 0 = 0() gcd(s(X),0()) = X + 1 >= X + 1 = s(X) gcd(s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(Y,X),s(X)) problem: DPs: TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Qed DPs: le#(s(X),s(Y)) -> le#(X,Y) TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Matrix Interpretation Processor: dimension: 1 interpretation: [le#](x0, x1) = x1 + 1, [if](x0, x1, x2) = x1 + x2, [gcd](x0, x1) = x0 + x1, [true] = 0, [false] = 0, [le](x0, x1) = 0, [0] = 0, [pred](x0) = x0, [minus](x0, x1) = x0 + 1, [s](x0) = x0 + 1 orientation: le#(s(X),s(Y)) = Y + 2 >= Y + 1 = le#(X,Y) minus(X,s(Y)) = X + 1 >= X + 1 = pred(minus(X,Y)) minus(X,0()) = X + 1 >= X = X pred(s(X)) = X + 1 >= X = X le(s(X),s(Y)) = 0 >= 0 = le(X,Y) le(s(X),0()) = 0 >= 0 = false() le(0(),Y) = 0 >= 0 = true() gcd(0(),Y) = Y >= 0 = 0() gcd(s(X),0()) = X + 1 >= X + 1 = s(X) gcd(s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = gcd(minus(Y,X),s(X)) problem: DPs: TRS: minus(X,s(Y)) -> pred(minus(X,Y)) minus(X,0()) -> X pred(s(X)) -> X le(s(X),s(Y)) -> le(X,Y) le(s(X),0()) -> false() le(0(),Y) -> true() gcd(0(),Y) -> 0() gcd(s(X),0()) -> s(X) gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y)) if(true(),s(X),s(Y)) -> gcd(minus(X,Y),s(Y)) if(false(),s(X),s(Y)) -> gcd(minus(Y,X),s(X)) Qed