MAYBE Problem: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Proof: DP Processor: DPs: a__f#(X) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) TDG Processor: DPs: a__f#(X) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) graph: a__if#(false(),X,Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(false(),X,Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__if#(false(),X,Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X2) a__if#(false(),X,Y) -> mark#(Y) -> mark#(f(X)) -> a__f#(mark(X)) a__if#(false(),X,Y) -> mark#(Y) -> mark#(f(X)) -> mark#(X) a__if#(true(),X,Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__if#(true(),X,Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) a__if#(true(),X,Y) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) a__if#(true(),X,Y) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) -> a__if#(false(),X,Y) -> mark#(Y) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) -> a__if#(true(),X,Y) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) -> a__f#(X) -> a__if#(mark(X),c(),f(true())) mark#(f(X)) -> a__f#(mark(X)) -> a__f#(X) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) -> a__if#(false(),X,Y) -> mark#(Y) a__f#(X) -> a__if#(mark(X),c(),f(true())) -> a__if#(true(),X,Y) -> mark#(X) a__f#(X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__f#(X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__f#(X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) a__f#(X) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) a__f#(X) -> mark#(X) -> mark#(f(X)) -> mark#(X) SCC Processor: #sccs: 1 #rules: 9 #arcs: 36/81 DPs: a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) a__f#(X) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Matrix Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = x1 + x2, [mark#](x0) = x0, [a__f#](x0) = x0 + 1, [if](x0, x1, x2) = x0 + x1 + x2, [false] = 0, [a__if](x0, x1, x2) = x0 + x1 + x2, [f](x0) = x0 + 1, [true] = 0, [c] = 0, [mark](x0) = x0, [a__f](x0) = x0 + 1 orientation: a__if#(false(),X,Y) = X + Y >= Y = mark#(Y) mark#(f(X)) = X + 1 >= X = mark#(X) mark#(f(X)) = X + 1 >= X + 1 = a__f#(mark(X)) a__f#(X) = X + 1 >= X = mark#(X) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X2 = mark#(X2) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 = mark#(X1) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X2 + X3 = a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) = X + Y >= X = mark#(X) a__f#(X) = X + 1 >= 1 = a__if#(mark(X),c(),f(true())) a__f(X) = X + 1 >= X + 1 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = X + Y >= X = mark(X) a__if(false(),X,Y) = X + Y >= Y = mark(Y) mark(f(X)) = X + 1 >= X + 1 = a__f(mark(X)) mark(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = a__if(mark(X1),mark(X2),X3) mark(c()) = 0 >= 0 = c() mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__f(X) = X + 1 >= X + 1 = f(X) a__if(X1,X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3) problem: DPs: a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Matrix Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = x0 + x1 + x2, [mark#](x0) = x0, [a__f#](x0) = x0, [if](x0, x1, x2) = x0 + x1 + x2, [false] = 1, [a__if](x0, x1, x2) = x0 + x1 + x2, [f](x0) = x0, [true] = 0, [c] = 0, [mark](x0) = x0, [a__f](x0) = x0 orientation: a__if#(false(),X,Y) = X + Y + 1 >= Y = mark#(Y) mark#(f(X)) = X >= X = a__f#(mark(X)) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X2 = mark#(X2) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 = mark#(X1) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) = X + Y >= X = mark#(X) a__f#(X) = X >= X = a__if#(mark(X),c(),f(true())) a__f(X) = X >= X = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = X + Y >= X = mark(X) a__if(false(),X,Y) = X + Y + 1 >= Y = mark(Y) mark(f(X)) = X >= X = a__f(mark(X)) mark(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = a__if(mark(X1),mark(X2),X3) mark(c()) = 0 >= 0 = c() mark(true()) = 0 >= 0 = true() mark(false()) = 1 >= 1 = false() a__f(X) = X >= X = f(X) a__if(X1,X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3) problem: DPs: mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Matrix Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = x1, [mark#](x0) = x0, [a__f#](x0) = 1, [if](x0, x1, x2) = x0 + x1 + x2, [false] = 1, [a__if](x0, x1, x2) = x0 + x1 + x2, [f](x0) = x0 + 1, [true] = 0, [c] = 0, [mark](x0) = x0, [a__f](x0) = x0 + 1 orientation: mark#(f(X)) = X + 1 >= 1 = a__f#(mark(X)) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X2 = mark#(X2) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 = mark#(X1) mark#(if(X1,X2,X3)) = X1 + X2 + X3 >= X2 = a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) = X >= X = mark#(X) a__f#(X) = 1 >= 0 = a__if#(mark(X),c(),f(true())) a__f(X) = X + 1 >= X + 1 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = X + Y >= X = mark(X) a__if(false(),X,Y) = X + Y + 1 >= Y = mark(Y) mark(f(X)) = X + 1 >= X + 1 = a__f(mark(X)) mark(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = a__if(mark(X1),mark(X2),X3) mark(c()) = 0 >= 0 = c() mark(true()) = 0 >= 0 = true() mark(false()) = 1 >= 1 = false() a__f(X) = X + 1 >= X + 1 = f(X) a__if(X1,X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = if(X1,X2,X3) problem: DPs: mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) -> mark#(X) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Matrix Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = 1, [mark#](x0) = 1, [a__f#](x0) = 0, [if](x0, x1, x2) = 0, [false] = 0, [a__if](x0, x1, x2) = 0, [f](x0) = 0, [true] = 0, [c] = 0, [mark](x0) = 0, [a__f](x0) = 0 orientation: mark#(f(X)) = 1 >= 0 = a__f#(mark(X)) mark#(if(X1,X2,X3)) = 1 >= 1 = mark#(X2) mark#(if(X1,X2,X3)) = 1 >= 1 = mark#(X1) mark#(if(X1,X2,X3)) = 1 >= 1 = a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) = 1 >= 1 = mark#(X) a__f(X) = 0 >= 0 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = 0 >= 0 = mark(X) a__if(false(),X,Y) = 0 >= 0 = mark(Y) mark(f(X)) = 0 >= 0 = a__f(mark(X)) mark(if(X1,X2,X3)) = 0 >= 0 = a__if(mark(X1),mark(X2),X3) mark(c()) = 0 >= 0 = c() mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__f(X) = 0 >= 0 = f(X) a__if(X1,X2,X3) = 0 >= 0 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) -> mark#(X) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Open