YES(?,O(n^2)) 47.85/19.28 YES(?,O(n^2)) 47.85/19.28 47.85/19.28 Problem: 47.85/19.28 top(sent(x)) -> top(check(rest(x))) 47.85/19.28 rest(nil()) -> sent(nil()) 47.85/19.28 rest(cons(x,y)) -> sent(y) 47.85/19.28 check(sent(x)) -> sent(check(x)) 47.85/19.28 check(rest(x)) -> rest(check(x)) 47.85/19.28 check(cons(x,y)) -> cons(check(x),y) 47.85/19.28 check(cons(x,y)) -> cons(x,check(y)) 47.85/19.28 check(cons(x,y)) -> cons(x,y) 47.85/19.28 47.85/19.28 Proof: 47.85/19.28 Complexity Transformation Processor: 47.85/19.28 strict: 47.85/19.28 top(sent(x)) -> top(check(rest(x))) 47.85/19.28 rest(nil()) -> sent(nil()) 47.85/19.28 rest(cons(x,y)) -> sent(y) 47.85/19.28 check(sent(x)) -> sent(check(x)) 47.85/19.28 check(rest(x)) -> rest(check(x)) 47.85/19.28 check(cons(x,y)) -> cons(check(x),y) 47.85/19.28 check(cons(x,y)) -> cons(x,check(y)) 47.85/19.28 check(cons(x,y)) -> cons(x,y) 47.85/19.28 weak: 47.85/19.28 47.85/19.28 Matrix Interpretation Processor: dim=1 47.85/19.28 47.85/19.28 max_matrix: 47.85/19.28 1 47.85/19.28 interpretation: 47.85/19.28 [cons](x0, x1) = x0 + x1 + 248, 47.85/19.28 47.85/19.28 [nil] = 196, 47.85/19.28 47.85/19.28 [check](x0) = x0 + 5, 47.85/19.28 47.85/19.28 [rest](x0) = x0 + 137, 47.85/19.28 47.85/19.28 [top](x0) = x0 + 102, 47.85/19.28 47.85/19.28 [sent](x0) = x0 + 82 47.85/19.28 orientation: 47.85/19.28 top(sent(x)) = x + 184 >= x + 244 = top(check(rest(x))) 47.85/19.28 47.85/19.28 rest(nil()) = 333 >= 278 = sent(nil()) 47.85/19.28 47.85/19.28 rest(cons(x,y)) = x + y + 385 >= y + 82 = sent(y) 47.85/19.28 47.85/19.28 check(sent(x)) = x + 87 >= x + 87 = sent(check(x)) 47.85/19.28 47.85/19.28 check(rest(x)) = x + 142 >= x + 142 = rest(check(x)) 47.85/19.28 47.85/19.28 check(cons(x,y)) = x + y + 253 >= x + y + 253 = cons(check(x),y) 47.85/19.28 47.85/19.28 check(cons(x,y)) = x + y + 253 >= x + y + 253 = cons(x,check(y)) 47.85/19.28 47.85/19.28 check(cons(x,y)) = x + y + 253 >= x + y + 248 = cons(x,y) 47.85/19.28 problem: 47.85/19.28 strict: 47.85/19.28 top(sent(x)) -> top(check(rest(x))) 47.85/19.28 check(sent(x)) -> sent(check(x)) 47.85/19.28 check(rest(x)) -> rest(check(x)) 47.85/19.28 check(cons(x,y)) -> cons(check(x),y) 47.85/19.28 check(cons(x,y)) -> cons(x,check(y)) 47.85/19.28 weak: 47.85/19.28 rest(nil()) -> sent(nil()) 47.85/19.28 rest(cons(x,y)) -> sent(y) 47.85/19.28 check(cons(x,y)) -> cons(x,y) 47.85/19.28 Matrix Interpretation Processor: dim=4 47.85/19.28 47.85/19.28 max_matrix: 47.85/19.28 [1 0 0 1] 47.85/19.28 [0 0 0 0] 47.85/19.28 [0 0 0 0] 47.85/19.28 [0 0 0 1] 47.85/19.28 interpretation: 47.85/19.28 [1 0 0 0] [1 0 0 1] [0] 47.85/19.28 [0 0 0 0] [0 0 0 0] [0] 47.85/19.28 [cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0] 47.85/19.28 [0 0 0 1] [0 0 0 1] [1], 47.85/19.28 47.85/19.28 [0] 47.85/19.28 [0] 47.85/19.28 [nil] = [0] 47.85/19.28 [0], 47.85/19.28 47.85/19.28 [1 0 0 1] 47.85/19.28 [0 0 0 0] 47.85/19.28 [check](x0) = [0 0 0 0]x0 47.85/19.28 [0 0 0 1] , 47.85/19.28 47.85/19.28 [1 0 0 0] 47.85/19.28 [0 0 0 0] 47.85/19.28 [rest](x0) = [0 0 0 0]x0 47.85/19.28 [0 0 0 1] , 47.85/19.28 47.85/19.28 [1 0 0 0] [1] 47.85/19.28 [0 0 0 0] [0] 47.85/19.28 [top](x0) = [0 0 0 0]x0 + [1] 47.85/19.28 [0 0 0 0] [0], 47.85/19.28 47.85/19.28 [1 0 0 1] 47.85/19.28 [0 0 0 0] 47.85/19.28 [sent](x0) = [0 0 0 0]x0 47.85/19.28 [0 0 0 1] 47.85/19.28 orientation: 47.85/19.28 [1 0 0 1] [1] [1 0 0 1] [1] 47.85/19.28 [0 0 0 0] [0] [0 0 0 0] [0] 47.85/19.28 top(sent(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [1] = top(check(rest(x))) 47.85/19.28 [0 0 0 0] [0] [0 0 0 0] [0] 47.85/19.28 47.85/19.28 [1 0 0 2] [1 0 0 2] 47.85/19.28 [0 0 0 0] [0 0 0 0] 47.85/19.28 check(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = sent(check(x)) 47.85/19.28 [0 0 0 1] [0 0 0 1] 47.85/19.28 47.85/19.28 [1 0 0 1] [1 0 0 1] 47.85/19.28 [0 0 0 0] [0 0 0 0] 47.85/19.28 check(rest(x)) = [0 0 0 0]x >= [0 0 0 0]x = rest(check(x)) 47.85/19.28 [0 0 0 1] [0 0 0 1] 47.85/19.28 47.85/19.28 [1 0 0 1] [1 0 0 2] [1] [1 0 0 1] [1 0 0 1] [0] 47.85/19.28 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 47.85/19.28 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) 47.85/19.28 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 47.85/19.28 47.85/19.28 [1 0 0 1] [1 0 0 2] [1] [1 0 0 0] [1 0 0 2] [0] 47.85/19.29 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 47.85/19.29 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)) 47.85/19.29 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 47.85/19.29 47.85/19.29 [0] [0] 47.85/19.29 [0] [0] 47.85/19.29 rest(nil()) = [0] >= [0] = sent(nil()) 47.85/19.29 [0] [0] 47.85/19.29 47.85/19.29 [1 0 0 0] [1 0 0 1] [0] [1 0 0 1] 47.85/19.29 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 47.85/19.29 rest(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]y = sent(y) 47.85/19.29 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] 47.85/19.29 47.85/19.29 [1 0 0 1] [1 0 0 2] [1] [1 0 0 0] [1 0 0 1] [0] 47.85/19.29 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 47.85/19.29 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) 47.85/19.29 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 47.85/19.29 problem: 47.85/19.29 strict: 47.85/19.29 top(sent(x)) -> top(check(rest(x))) 47.85/19.29 check(sent(x)) -> sent(check(x)) 47.85/19.29 check(rest(x)) -> rest(check(x)) 47.85/19.29 weak: 47.85/19.29 check(cons(x,y)) -> cons(check(x),y) 47.85/19.29 check(cons(x,y)) -> cons(x,check(y)) 47.85/19.29 rest(nil()) -> sent(nil()) 47.85/19.29 rest(cons(x,y)) -> sent(y) 47.85/19.29 check(cons(x,y)) -> cons(x,y) 47.85/19.29 Splitting Processor: 47.85/19.29 strict: 47.85/19.29 top(sent(x)) -> top(check(rest(x))) 47.85/19.29 weak: 47.85/19.29 check(cons(x,y)) -> cons(check(x),y) 47.85/19.29 check(cons(x,y)) -> cons(x,check(y)) 47.85/19.29 rest(nil()) -> sent(nil()) 47.85/19.29 rest(cons(x,y)) -> sent(y) 47.85/19.29 check(cons(x,y)) -> cons(x,y) 47.85/19.29 check(sent(x)) -> sent(check(x)) 47.85/19.29 check(rest(x)) -> rest(check(x)) 47.85/19.29 Matrix Interpretation Processor: dim=5 47.85/19.29 47.85/19.29 max_matrix: 47.85/19.29 [1 1 1 1 1] 47.85/19.29 [0 0 1 1 1] 47.85/19.29 [0 0 1 1 1] 47.85/19.29 [0 0 0 0 0] 47.85/19.29 [0 0 0 0 0] 47.85/19.29 interpretation: 47.85/19.29 [1 0 0 0 0] [1 0 0 0 1] [1] 47.85/19.29 [0 0 0 0 0] [0 0 1 1 1] [0] 47.85/19.29 [cons](x0, x1) = [0 0 1 1 0]x0 + [0 0 1 1 1]x1 + [0] 47.85/19.29 [0 0 0 0 0] [0 0 0 0 0] [0] 47.85/19.29 [0 0 0 0 0] [0 0 0 0 0] [0], 47.85/19.29 47.85/19.29 [0] 47.85/19.29 [0] 47.85/19.29 [nil] = [0] 47.85/19.29 [1] 47.85/19.29 [1], 47.85/19.29 47.85/19.29 [1 0 0 0 0] 47.85/19.29 [0 0 1 0 0] 47.85/19.29 [check](x0) = [0 0 1 0 0]x0 47.85/19.29 [0 0 0 0 0] 47.85/19.29 [0 0 0 0 0] , 47.85/19.29 47.85/19.29 [1 0 1 1 1] 47.85/19.29 [0 0 1 1 1] 47.85/19.29 [rest](x0) = [0 0 1 0 0]x0 47.85/19.29 [0 0 0 0 0] 47.85/19.29 [0 0 0 0 0] , 47.85/19.29 47.85/19.29 [1 1 0 0 0] 47.85/19.29 [0 0 0 0 0] 47.85/19.29 [top](x0) = [0 0 0 1 0]x0 47.85/19.29 [0 0 0 0 0] 47.85/19.29 [0 0 0 0 0] , 47.85/19.29 47.85/19.29 [1 0 1 0 0] [1] 47.85/19.29 [0 0 1 1 1] [0] 47.85/19.29 [sent](x0) = [0 0 1 0 0]x0 + [0] 47.85/19.29 [0 0 0 0 0] [0] 47.85/19.29 [0 0 0 0 0] [0] 47.85/19.29 orientation: 47.85/19.29 [1 0 2 1 1] [1] [1 0 2 1 1] 47.85/19.29 [0 0 0 0 0] [0] [0 0 0 0 0] 47.85/19.29 top(sent(x)) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x = top(check(rest(x))) 47.85/19.29 [0 0 0 0 0] [0] [0 0 0 0 0] 47.85/19.29 [0 0 0 0 0] [0] [0 0 0 0 0] 47.85/19.29 47.85/19.29 [1 0 0 0 0] [1 0 0 0 1] [1] [1 0 0 0 0] [1 0 0 0 1] [1] 47.85/19.29 [0 0 1 1 0] [0 0 1 1 1] [0] [0 0 0 0 0] [0 0 1 1 1] [0] 47.85/19.29 check(cons(x,y)) = [0 0 1 1 0]x + [0 0 1 1 1]y + [0] >= [0 0 1 0 0]x + [0 0 1 1 1]y + [0] = cons(check(x),y) 47.85/19.29 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 47.95/19.30 47.95/19.30 [1 0 0 0 0] [1 0 0 0 1] [1] [1 0 0 0 0] [1 0 0 0 0] [1] 47.95/19.30 [0 0 1 1 0] [0 0 1 1 1] [0] [0 0 0 0 0] [0 0 1 0 0] [0] 47.95/19.30 check(cons(x,y)) = [0 0 1 1 0]x + [0 0 1 1 1]y + [0] >= [0 0 1 1 0]x + [0 0 1 0 0]y + [0] = cons(x,check(y)) 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 47.95/19.30 47.95/19.30 [2] [1] 47.95/19.30 [2] [2] 47.95/19.30 rest(nil()) = [0] >= [0] = sent(nil()) 47.95/19.30 [0] [0] 47.95/19.30 [0] [0] 47.95/19.30 47.95/19.30 [1 0 1 1 0] [1 0 1 1 2] [1] [1 0 1 0 0] [1] 47.95/19.30 [0 0 1 1 0] [0 0 1 1 1] [0] [0 0 1 1 1] [0] 47.95/19.30 rest(cons(x,y)) = [0 0 1 1 0]x + [0 0 1 1 1]y + [0] >= [0 0 1 0 0]y + [0] = sent(y) 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0] 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0] 47.95/19.30 47.95/19.30 [1 0 0 0 0] [1 0 0 0 1] [1] [1 0 0 0 0] [1 0 0 0 1] [1] 47.95/19.30 [0 0 1 1 0] [0 0 1 1 1] [0] [0 0 0 0 0] [0 0 1 1 1] [0] 47.95/19.30 check(cons(x,y)) = [0 0 1 1 0]x + [0 0 1 1 1]y + [0] >= [0 0 1 1 0]x + [0 0 1 1 1]y + [0] = cons(x,y) 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 47.95/19.30 47.95/19.30 [1 0 1 0 0] [1] [1 0 1 0 0] [1] 47.95/19.30 [0 0 1 0 0] [0] [0 0 1 0 0] [0] 47.95/19.30 check(sent(x)) = [0 0 1 0 0]x + [0] >= [0 0 1 0 0]x + [0] = sent(check(x)) 47.95/19.30 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 47.95/19.30 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 47.95/19.30 47.95/19.30 [1 0 1 1 1] [1 0 1 0 0] 47.95/19.30 [0 0 1 0 0] [0 0 1 0 0] 47.95/19.30 check(rest(x)) = [0 0 1 0 0]x >= [0 0 1 0 0]x = rest(check(x)) 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] 47.95/19.30 [0 0 0 0 0] [0 0 0 0 0] 47.95/19.30 problem: 47.95/19.30 strict: 47.95/19.30 47.95/19.30 weak: 47.95/19.30 top(sent(x)) -> top(check(rest(x))) 47.95/19.30 check(cons(x,y)) -> cons(check(x),y) 47.95/19.30 check(cons(x,y)) -> cons(x,check(y)) 47.95/19.30 rest(nil()) -> sent(nil()) 47.95/19.30 rest(cons(x,y)) -> sent(y) 47.95/19.30 check(cons(x,y)) -> cons(x,y) 47.95/19.30 check(sent(x)) -> sent(check(x)) 47.95/19.30 check(rest(x)) -> rest(check(x)) 47.95/19.30 Qed 47.95/19.30 47.95/19.30 strict: 47.95/19.30 check(sent(x)) -> sent(check(x)) 47.95/19.30 check(rest(x)) -> rest(check(x)) 47.95/19.30 weak: 47.95/19.30 top(sent(x)) -> top(check(rest(x))) 47.95/19.30 check(cons(x,y)) -> cons(check(x),y) 47.95/19.30 check(cons(x,y)) -> cons(x,check(y)) 47.95/19.30 rest(nil()) -> sent(nil()) 47.95/19.30 rest(cons(x,y)) -> sent(y) 47.95/19.30 check(cons(x,y)) -> cons(x,y) 47.95/19.30 Matrix Interpretation Processor: dim=4 47.95/19.30 47.95/19.30 max_matrix: 47.95/19.30 [1 1 1 1] 47.95/19.30 [0 0 1 1] 47.95/19.30 [0 0 1 1] 47.95/19.30 [0 0 0 0] 47.95/19.30 interpretation: 47.95/19.30 [1 0 1 0] [1 0 1 0] [1] 47.95/19.30 [0 0 1 0] [0 0 0 0] [0] 47.95/19.30 [cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 1]x1 + [0] 47.95/19.30 [0 0 0 0] [0 0 0 0] [0], 47.95/19.30 47.95/19.30 [0] 47.95/19.30 [0] 47.95/19.30 [nil] = [0] 47.95/19.30 [1], 47.95/19.30 47.95/19.30 [1 0 1 0] 47.95/19.30 [0 0 1 0] 47.95/19.30 [check](x0) = [0 0 1 0]x0 47.95/19.31 [0 0 0 0] , 47.95/19.31 47.95/19.31 [1 0 0 1] [0] 47.95/19.31 [0 0 1 1] [1] 47.95/19.31 [rest](x0) = [0 0 1 0]x0 + [1] 47.95/19.31 [0 0 0 0] [0], 47.95/19.31 47.95/19.31 [1 1 0 0] 47.95/19.31 [0 0 1 1] 47.95/19.31 [top](x0) = [0 0 0 0]x0 47.95/19.31 [0 0 0 0] , 47.95/19.31 47.95/19.31 [1 0 1 0] [1] 47.95/19.31 [0 0 1 1] [1] 47.95/19.31 [sent](x0) = [0 0 1 0]x0 + [1] 47.95/19.31 [0 0 0 0] [0] 47.95/19.31 orientation: 47.95/19.31 [1 0 2 0] [2] [1 0 2 0] [1] 47.95/19.31 [0 0 1 0] [1] [0 0 1 0] [1] 47.95/19.31 check(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = sent(check(x)) 47.95/19.31 [0 0 0 0] [0] [0 0 0 0] [0] 47.95/19.31 47.95/19.31 [1 0 1 1] [1] [1 0 1 0] [0] 47.95/19.31 [0 0 1 0] [1] [0 0 1 0] [1] 47.95/19.31 check(rest(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = rest(check(x)) 47.95/19.31 [0 0 0 0] [0] [0 0 0 0] [0] 47.95/19.31 47.95/19.31 [1 0 2 1] [2] [1 0 2 1] [2] 47.95/19.31 [0 0 1 0] [1] [0 0 1 0] [1] 47.95/19.31 top(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = top(check(rest(x))) 47.95/19.31 [0 0 0 0] [0] [0 0 0 0] [0] 47.95/19.31 47.95/19.31 [1 0 2 0] [1 0 2 1] [1] [1 0 2 0] [1 0 1 0] [1] 47.95/19.31 [0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 0] [0] 47.95/19.31 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) 47.95/19.31 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 47.95/19.31 47.95/19.31 [1 0 2 0] [1 0 2 1] [1] [1 0 1 0] [1 0 2 0] [1] 47.95/19.31 [0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 0] [0] 47.95/19.31 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)) 47.95/19.31 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 47.95/19.31 47.95/19.31 [1] [1] 47.95/19.31 [2] [2] 47.95/19.31 rest(nil()) = [1] >= [1] = sent(nil()) 47.95/19.31 [0] [0] 47.95/19.31 47.95/19.31 [1 0 1 0] [1 0 1 0] [1] [1 0 1 0] [1] 47.95/19.31 [0 0 1 0] [0 0 1 1] [1] [0 0 1 1] [1] 47.95/19.31 rest(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [1] >= [0 0 1 0]y + [1] = sent(y) 47.95/19.31 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 47.95/19.31 47.95/19.31 [1 0 2 0] [1 0 2 1] [1] [1 0 1 0] [1 0 1 0] [1] 47.95/19.31 [0 0 1 0] [0 0 1 1] [0] [0 0 1 0] [0 0 0 0] [0] 47.95/19.31 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) 47.95/19.31 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 47.95/19.31 problem: 47.95/19.31 strict: 47.95/19.31 47.95/19.31 weak: 47.95/19.31 check(sent(x)) -> sent(check(x)) 47.95/19.31 check(rest(x)) -> rest(check(x)) 47.95/19.31 top(sent(x)) -> top(check(rest(x))) 47.95/19.31 check(cons(x,y)) -> cons(check(x),y) 47.95/19.31 check(cons(x,y)) -> cons(x,check(y)) 47.95/19.31 rest(nil()) -> sent(nil()) 47.95/19.31 rest(cons(x,y)) -> sent(y) 47.95/19.31 check(cons(x,y)) -> cons(x,y) 47.95/19.31 Qed 47.95/19.31 EOF