MAYBE Problem: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() Proof: DP Processor: DPs: *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) i#(*(x,y)) -> i#(x) i#(*(x,y)) -> i#(y) i#(*(x,y)) -> *#(i(y),i(x)) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() TDG Processor: DPs: *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) i#(*(x,y)) -> i#(x) i#(*(x,y)) -> i#(y) i#(*(x,y)) -> *#(i(y),i(x)) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() graph: i#(*(x,y)) -> i#(y) -> i#(*(x,y)) -> *#(i(y),i(x)) i#(*(x,y)) -> i#(y) -> i#(*(x,y)) -> i#(y) i#(*(x,y)) -> i#(y) -> i#(*(x,y)) -> i#(x) i#(*(x,y)) -> i#(x) -> i#(*(x,y)) -> *#(i(y),i(x)) i#(*(x,y)) -> i#(x) -> i#(*(x,y)) -> i#(y) i#(*(x,y)) -> i#(x) -> i#(*(x,y)) -> i#(x) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(x,*(y,z)) -> *#(*(x,y),z) i#(*(x,y)) -> *#(i(y),i(x)) -> *#(x,*(y,z)) -> *#(x,y) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) -> *#(x,*(y,z)) -> *#(x,y) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) -> *#(x,*(y,z)) -> *#(x,y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) -> *#(x,*(y,z)) -> *#(x,y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) -> *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x)) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(x,*(y,z)) -> *#(x,y) -> *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(x,*(y,z)) -> *#(x,y) -> *#(x,*(y,z)) -> *#(*(x,y),z) *#(x,*(y,z)) -> *#(x,y) -> *#(x,*(y,z)) -> *#(x,y) SCC Processor: #sccs: 2 #rules: 8 #arcs: 55/100 DPs: i#(*(x,y)) -> i#(y) i#(*(x,y)) -> i#(x) TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() Matrix Interpretation Processor: dim=1 interpretation: [i#](x0) = 2x0 + 4, [k](x0, x1) = 7, [i](x0) = 2x0 + 3, [*](x0, x1) = x0 + x1 + 4, [1] = 7 orientation: i#(*(x,y)) = 2x + 2y + 12 >= 2y + 4 = i#(y) i#(*(x,y)) = 2x + 2y + 12 >= 2x + 4 = i#(x) *(x,1()) = x + 11 >= x = x *(1(),y) = y + 11 >= y = y *(i(x),x) = 3x + 7 >= 7 = 1() *(x,i(x)) = 3x + 7 >= 7 = 1() *(x,*(y,z)) = x + y + z + 8 >= x + y + z + 8 = *(*(x,y),z) i(1()) = 17 >= 7 = 1() *(*(x,y),i(y)) = x + 3y + 11 >= x = x *(*(x,i(y)),y) = x + 3y + 11 >= x = x i(i(x)) = 4x + 9 >= x = x i(*(x,y)) = 2x + 2y + 11 >= 2x + 2y + 10 = *(i(y),i(x)) k(x,1()) = 7 >= 7 = 1() k(x,x) = 7 >= 7 = 1() *(k(x,y),k(y,x)) = 18 >= 7 = 1() *(*(i(x),k(y,z)),x) = 3x + 18 >= 7 = k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) = 7 >= 7 = 1() problem: DPs: TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() Qed DPs: *#(x,*(y,z)) -> *#(x,y) *#(x,*(y,z)) -> *#(*(x,y),z) *#(*(i(x),k(y,z)),x) -> *#(i(x),z) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),z),x) *#(*(i(x),k(y,z)),x) -> *#(i(x),y) *#(*(i(x),k(y,z)),x) -> *#(*(i(x),y),x) TRS: *(x,1()) -> x *(1(),y) -> y *(i(x),x) -> 1() *(x,i(x)) -> 1() *(x,*(y,z)) -> *(*(x,y),z) i(1()) -> 1() *(*(x,y),i(y)) -> x *(*(x,i(y)),y) -> x i(i(x)) -> x i(*(x,y)) -> *(i(y),i(x)) k(x,1()) -> 1() k(x,x) -> 1() *(k(x,y),k(y,x)) -> 1() *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x)) k(*(x,i(y)),*(y,i(x))) -> 1() Open