YES(?,O(n^2)) 43.72/18.09 YES(?,O(n^2)) 43.82/18.10 43.82/18.10 Problem: 43.82/18.10 top(sent(x)) -> top(check(rest(x))) 43.82/18.10 rest(nil()) -> sent(nil()) 43.82/18.10 rest(cons(x,y)) -> sent(y) 43.82/18.10 check(sent(x)) -> sent(check(x)) 43.82/18.10 check(rest(x)) -> rest(check(x)) 43.82/18.10 check(cons(x,y)) -> cons(check(x),y) 43.82/18.10 check(cons(x,y)) -> cons(x,check(y)) 43.82/18.10 check(cons(x,y)) -> cons(x,y) 43.82/18.10 43.82/18.10 Proof: 43.82/18.10 Complexity Transformation Processor: 43.82/18.10 strict: 43.82/18.10 top(sent(x)) -> top(check(rest(x))) 43.82/18.10 rest(nil()) -> sent(nil()) 43.82/18.10 rest(cons(x,y)) -> sent(y) 43.82/18.10 check(sent(x)) -> sent(check(x)) 43.82/18.10 check(rest(x)) -> rest(check(x)) 43.82/18.10 check(cons(x,y)) -> cons(check(x),y) 43.82/18.10 check(cons(x,y)) -> cons(x,check(y)) 43.82/18.10 check(cons(x,y)) -> cons(x,y) 43.82/18.10 weak: 43.82/18.10 43.82/18.10 Matrix Interpretation Processor: dim=1 43.82/18.10 43.82/18.10 max_matrix: 43.82/18.10 1 43.82/18.10 interpretation: 43.82/18.10 [cons](x0, x1) = x0 + x1 + 248, 43.82/18.10 43.82/18.10 [nil] = 196, 43.82/18.10 43.82/18.10 [check](x0) = x0 + 5, 43.82/18.10 43.82/18.10 [rest](x0) = x0 + 137, 43.82/18.10 43.82/18.10 [top](x0) = x0 + 102, 43.82/18.10 43.82/18.10 [sent](x0) = x0 + 82 43.82/18.10 orientation: 43.82/18.10 top(sent(x)) = x + 184 >= x + 244 = top(check(rest(x))) 43.82/18.10 43.82/18.10 rest(nil()) = 333 >= 278 = sent(nil()) 43.82/18.10 43.82/18.10 rest(cons(x,y)) = x + y + 385 >= y + 82 = sent(y) 43.82/18.10 43.82/18.10 check(sent(x)) = x + 87 >= x + 87 = sent(check(x)) 43.82/18.10 43.82/18.10 check(rest(x)) = x + 142 >= x + 142 = rest(check(x)) 43.82/18.10 43.82/18.10 check(cons(x,y)) = x + y + 253 >= x + y + 253 = cons(check(x),y) 43.82/18.10 43.82/18.10 check(cons(x,y)) = x + y + 253 >= x + y + 253 = cons(x,check(y)) 43.82/18.10 43.82/18.10 check(cons(x,y)) = x + y + 253 >= x + y + 248 = cons(x,y) 43.82/18.10 problem: 43.82/18.10 strict: 43.82/18.10 top(sent(x)) -> top(check(rest(x))) 43.82/18.10 check(sent(x)) -> sent(check(x)) 43.82/18.10 check(rest(x)) -> rest(check(x)) 43.82/18.10 check(cons(x,y)) -> cons(check(x),y) 43.82/18.10 check(cons(x,y)) -> cons(x,check(y)) 43.82/18.10 weak: 43.82/18.10 rest(nil()) -> sent(nil()) 43.82/18.10 rest(cons(x,y)) -> sent(y) 43.82/18.10 check(cons(x,y)) -> cons(x,y) 43.82/18.10 Matrix Interpretation Processor: dim=4 43.82/18.10 43.82/18.10 max_matrix: 43.82/18.10 [1 0 0 1] 43.82/18.10 [0 0 0 0] 43.82/18.10 [0 0 0 0] 43.82/18.10 [0 0 0 1] 43.82/18.10 interpretation: 43.82/18.10 [1 0 0 0] [1 0 0 1] [0] 43.82/18.10 [0 0 0 0] [0 0 0 0] [0] 43.82/18.10 [cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0] 43.82/18.10 [0 0 0 1] [0 0 0 1] [1], 43.82/18.10 43.82/18.10 [0] 43.82/18.10 [0] 43.82/18.10 [nil] = [0] 43.82/18.10 [0], 43.82/18.10 43.82/18.10 [1 0 0 1] 43.82/18.10 [0 0 0 0] 43.82/18.10 [check](x0) = [0 0 0 0]x0 43.82/18.10 [0 0 0 1] , 43.82/18.10 43.82/18.10 [1 0 0 0] 43.82/18.10 [0 0 0 0] 43.82/18.10 [rest](x0) = [0 0 0 0]x0 43.82/18.10 [0 0 0 1] , 43.82/18.10 43.82/18.10 [1 0 0 0] [1] 43.82/18.10 [0 0 0 0] [0] 43.82/18.10 [top](x0) = [0 0 0 0]x0 + [1] 43.82/18.10 [0 0 0 0] [0], 43.82/18.10 43.82/18.10 [1 0 0 1] 43.82/18.10 [0 0 0 0] 43.82/18.10 [sent](x0) = [0 0 0 0]x0 43.82/18.10 [0 0 0 1] 43.82/18.10 orientation: 43.82/18.10 [1 0 0 1] [1] [1 0 0 1] [1] 43.82/18.10 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.10 top(sent(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [1] = top(check(rest(x))) 43.82/18.10 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.10 43.82/18.10 [1 0 0 2] [1 0 0 2] 43.82/18.10 [0 0 0 0] [0 0 0 0] 43.82/18.10 check(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = sent(check(x)) 43.82/18.10 [0 0 0 1] [0 0 0 1] 43.82/18.10 43.82/18.10 [1 0 0 1] [1 0 0 1] 43.82/18.10 [0 0 0 0] [0 0 0 0] 43.82/18.10 check(rest(x)) = [0 0 0 0]x >= [0 0 0 0]x = rest(check(x)) 43.82/18.10 [0 0 0 1] [0 0 0 1] 43.82/18.10 43.82/18.10 [1 0 0 1] [1 0 0 2] [1] [1 0 0 1] [1 0 0 1] [0] 43.82/18.10 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.10 check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(check(x),y) 43.82/18.10 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 43.82/18.10 43.82/18.10 [1 0 0 1] [1 0 0 2] [1] [1 0 0 0] [1 0 0 2] [0] 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,check(y)) 43.82/18.11 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 43.82/18.11 43.82/18.11 [0] [0] 43.82/18.11 [0] [0] 43.82/18.11 rest(nil()) = [0] >= [0] = sent(nil()) 43.82/18.11 [0] [0] 43.82/18.11 43.82/18.11 [1 0 0 0] [1 0 0 1] [0] [1 0 0 1] 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 43.82/18.11 rest(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]y = sent(y) 43.82/18.11 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] 43.82/18.11 43.82/18.11 [1 0 0 1] [1 0 0 2] [1] [1 0 0 0] [1 0 0 1] [0] 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,y) 43.82/18.11 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 43.82/18.11 problem: 43.82/18.11 strict: 43.82/18.11 top(sent(x)) -> top(check(rest(x))) 43.82/18.11 check(sent(x)) -> sent(check(x)) 43.82/18.11 check(rest(x)) -> rest(check(x)) 43.82/18.11 weak: 43.82/18.11 check(cons(x,y)) -> cons(check(x),y) 43.82/18.11 check(cons(x,y)) -> cons(x,check(y)) 43.82/18.11 rest(nil()) -> sent(nil()) 43.82/18.11 rest(cons(x,y)) -> sent(y) 43.82/18.11 check(cons(x,y)) -> cons(x,y) 43.82/18.11 Matrix Interpretation Processor: dim=4 43.82/18.11 43.82/18.11 max_matrix: 43.82/18.11 [1 1 1 1] 43.82/18.11 [0 0 1 1] 43.82/18.11 [0 0 1 1] 43.82/18.11 [0 0 0 0] 43.82/18.11 interpretation: 43.82/18.11 [1 0 1 0] [1 0 1 0] [1] 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 [cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 1]x1 + [0] 43.82/18.11 [0 0 0 0] [0 0 0 0] [0], 43.82/18.11 43.82/18.11 [0] 43.82/18.11 [0] 43.82/18.11 [nil] = [0] 43.82/18.11 [1], 43.82/18.11 43.82/18.11 [1 0 0 0] 43.82/18.11 [0 0 1 0] 43.82/18.11 [check](x0) = [0 0 1 0]x0 43.82/18.11 [0 0 0 0] , 43.82/18.11 43.82/18.11 [1 0 0 1] 43.82/18.11 [0 0 1 1] 43.82/18.11 [rest](x0) = [0 0 1 0]x0 43.82/18.11 [0 0 0 0] , 43.82/18.11 43.82/18.11 [1 1 0 0] [0] 43.82/18.11 [0 0 0 1] [0] 43.82/18.11 [top](x0) = [0 0 0 1]x0 + [1] 43.82/18.11 [0 0 0 0] [0], 43.82/18.11 43.82/18.11 [1 0 1 0] [1] 43.82/18.11 [0 0 0 1] [0] 43.82/18.11 [sent](x0) = [0 0 0 0]x0 + [0] 43.82/18.11 [0 0 0 0] [0] 43.82/18.11 orientation: 43.82/18.11 [1 0 1 1] [1] [1 0 1 1] [0] 43.82/18.11 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.11 top(sent(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [1] = top(check(rest(x))) 43.82/18.11 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1 0 1 0] [1] [1 0 1 0] [1] 43.82/18.11 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.11 check(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = sent(check(x)) 43.82/18.11 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1 0 0 1] [1 0 0 0] 43.82/18.11 [0 0 1 0] [0 0 1 0] 43.82/18.11 check(rest(x)) = [0 0 1 0]x >= [0 0 1 0]x = rest(check(x)) 43.82/18.11 [0 0 0 0] [0 0 0 0] 43.82/18.11 43.82/18.11 [1 0 1 0] [1 0 1 0] [1] [1 0 1 0] [1 0 1 0] [1] 43.82/18.11 [0 0 0 0] [0 0 0 1] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 check(cons(x,y)) = [0 0 0 0]x + [0 0 0 1]y + [0] >= [0 0 0 0]x + [0 0 0 1]y + [0] = cons(check(x),y) 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1 0 1 0] [1 0 1 0] [1] [1 0 1 0] [1 0 1 0] [1] 43.82/18.11 [0 0 0 0] [0 0 0 1] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 check(cons(x,y)) = [0 0 0 0]x + [0 0 0 1]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,check(y)) 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1] [1] 43.82/18.11 [1] [1] 43.82/18.11 rest(nil()) = [0] >= [0] = sent(nil()) 43.82/18.11 [0] [0] 43.82/18.11 43.82/18.11 [1 0 1 0] [1 0 1 0] [1] [1 0 1 0] [1] 43.82/18.11 [0 0 0 0] [0 0 0 1] [0] [0 0 0 1] [0] 43.82/18.11 rest(cons(x,y)) = [0 0 0 0]x + [0 0 0 1]y + [0] >= [0 0 0 0]y + [0] = sent(y) 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1 0 1 0] [1 0 1 0] [1] [1 0 1 0] [1 0 1 0] [1] 43.82/18.11 [0 0 0 0] [0 0 0 1] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 check(cons(x,y)) = [0 0 0 0]x + [0 0 0 1]y + [0] >= [0 0 0 0]x + [0 0 0 1]y + [0] = cons(x,y) 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 problem: 43.82/18.11 strict: 43.82/18.11 check(sent(x)) -> sent(check(x)) 43.82/18.11 check(rest(x)) -> rest(check(x)) 43.82/18.11 weak: 43.82/18.11 top(sent(x)) -> top(check(rest(x))) 43.82/18.11 check(cons(x,y)) -> cons(check(x),y) 43.82/18.11 check(cons(x,y)) -> cons(x,check(y)) 43.82/18.11 rest(nil()) -> sent(nil()) 43.82/18.11 rest(cons(x,y)) -> sent(y) 43.82/18.11 check(cons(x,y)) -> cons(x,y) 43.82/18.11 Matrix Interpretation Processor: dim=4 43.82/18.11 43.82/18.11 max_matrix: 43.82/18.11 [1 1 1 1] 43.82/18.11 [0 0 1 1] 43.82/18.11 [0 0 1 1] 43.82/18.11 [0 0 0 0] 43.82/18.11 interpretation: 43.82/18.11 [1 0 1 0] [1 0 1 0] [1] 43.82/18.11 [0 0 1 0] [0 0 0 0] [0] 43.82/18.11 [cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 1]x1 + [0] 43.82/18.11 [0 0 0 0] [0 0 0 0] [0], 43.82/18.11 43.82/18.11 [0] 43.82/18.11 [0] 43.82/18.11 [nil] = [0] 43.82/18.11 [1], 43.82/18.11 43.82/18.11 [1 0 1 0] 43.82/18.11 [0 0 1 0] 43.82/18.11 [check](x0) = [0 0 1 0]x0 43.82/18.11 [0 0 0 0] , 43.82/18.11 43.82/18.11 [1 0 0 1] [0] 43.82/18.11 [0 0 1 1] [1] 43.82/18.11 [rest](x0) = [0 0 1 0]x0 + [1] 43.82/18.11 [0 0 0 0] [0], 43.82/18.11 43.82/18.11 [1 1 0 0] 43.82/18.11 [0 0 1 1] 43.82/18.11 [top](x0) = [0 0 0 0]x0 43.82/18.11 [0 0 0 0] , 43.82/18.11 43.82/18.11 [1 0 1 0] [1] 43.82/18.11 [0 0 1 1] [1] 43.82/18.11 [sent](x0) = [0 0 1 0]x0 + [1] 43.82/18.11 [0 0 0 0] [0] 43.82/18.11 orientation: 43.82/18.11 [1 0 2 0] [2] [1 0 2 0] [1] 43.82/18.11 [0 0 1 0] [1] [0 0 1 0] [1] 43.82/18.11 check(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = sent(check(x)) 43.82/18.11 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1 0 1 1] [1] [1 0 1 0] [0] 43.82/18.11 [0 0 1 0] [1] [0 0 1 0] [1] 43.82/18.11 check(rest(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = rest(check(x)) 43.82/18.11 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1 0 2 1] [2] [1 0 2 1] [2] 43.82/18.11 [0 0 1 0] [1] [0 0 1 0] [1] 43.82/18.11 top(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = top(check(rest(x))) 43.82/18.11 [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1 0 2 0] [1 0 2 1] [1] [1 0 2 0] [1 0 1 0] [1] 43.82/18.11 [0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 0] [0] 43.82/18.11 check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(check(x),y) 43.82/18.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.11 43.82/18.11 [1 0 2 0] [1 0 2 1] [1] [1 0 1 0] [1 0 2 0] [1] 43.82/18.12 [0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 0] [0] 43.82/18.12 check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0] = cons(x,check(y)) 43.82/18.12 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.12 43.82/18.12 [1] [1] 43.82/18.12 [2] [2] 43.82/18.12 rest(nil()) = [1] >= [1] = sent(nil()) 43.82/18.12 [0] [0] 43.82/18.12 43.82/18.12 [1 0 1 0] [1 0 1 0] [1] [1 0 1 0] [1] 43.82/18.12 [0 0 1 0] [0 0 1 1] [1] [0 0 1 1] [1] 43.82/18.12 rest(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [1] >= [0 0 1 0]y + [1] = sent(y) 43.82/18.12 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 43.82/18.12 43.82/18.12 [1 0 2 0] [1 0 2 1] [1] [1 0 1 0] [1 0 1 0] [1] 43.82/18.12 [0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 0] [0] 43.82/18.12 check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(x,y) 43.82/18.12 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 43.82/18.12 problem: 43.82/18.12 strict: 43.82/18.12 43.82/18.12 weak: 43.82/18.12 check(sent(x)) -> sent(check(x)) 43.82/18.12 check(rest(x)) -> rest(check(x)) 43.82/18.12 top(sent(x)) -> top(check(rest(x))) 43.82/18.12 check(cons(x,y)) -> cons(check(x),y) 43.82/18.12 check(cons(x,y)) -> cons(x,check(y)) 43.82/18.12 rest(nil()) -> sent(nil()) 43.82/18.12 rest(cons(x,y)) -> sent(y) 43.82/18.12 check(cons(x,y)) -> cons(x,y) 43.82/18.12 Qed 43.82/18.12 EOF