YES(?,O(n^3)) 103.97/35.04 YES(?,O(n^3)) 103.97/35.05 103.97/35.05 Problem: 103.97/35.05 a__nats() -> a__adx(a__zeros()) 103.97/35.05 a__zeros() -> cons(0(),zeros()) 103.97/35.05 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.05 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.05 a__hd(cons(X,Y)) -> mark(X) 103.97/35.05 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.05 mark(nats()) -> a__nats() 103.97/35.05 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.05 mark(zeros()) -> a__zeros() 103.97/35.05 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.05 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.05 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.05 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.05 mark(0()) -> 0() 103.97/35.05 mark(s(X)) -> s(X) 103.97/35.05 a__nats() -> nats() 103.97/35.05 a__adx(X) -> adx(X) 103.97/35.05 a__zeros() -> zeros() 103.97/35.05 a__incr(X) -> incr(X) 103.97/35.05 a__hd(X) -> hd(X) 103.97/35.05 a__tl(X) -> tl(X) 103.97/35.05 103.97/35.05 Proof: 103.97/35.05 Complexity Transformation Processor: 103.97/35.05 strict: 103.97/35.05 a__nats() -> a__adx(a__zeros()) 103.97/35.05 a__zeros() -> cons(0(),zeros()) 103.97/35.05 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.05 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.05 a__hd(cons(X,Y)) -> mark(X) 103.97/35.05 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.05 mark(nats()) -> a__nats() 103.97/35.05 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.05 mark(zeros()) -> a__zeros() 103.97/35.05 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.05 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.05 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.05 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.05 mark(0()) -> 0() 103.97/35.05 mark(s(X)) -> s(X) 103.97/35.05 a__nats() -> nats() 103.97/35.05 a__adx(X) -> adx(X) 103.97/35.05 a__zeros() -> zeros() 103.97/35.05 a__incr(X) -> incr(X) 103.97/35.05 a__hd(X) -> hd(X) 103.97/35.05 a__tl(X) -> tl(X) 103.97/35.05 weak: 103.97/35.05 103.97/35.05 Matrix Interpretation Processor: dim=1 103.97/35.05 103.97/35.05 max_matrix: 103.97/35.05 1 103.97/35.05 interpretation: 103.97/35.05 [tl](x0) = x0 + 130, 103.97/35.05 103.97/35.05 [hd](x0) = x0 + 46, 103.97/35.05 103.97/35.05 [nats] = 14, 103.97/35.05 103.97/35.05 [a__tl](x0) = x0 + 231, 103.97/35.05 103.97/35.05 [mark](x0) = x0 + 20, 103.97/35.05 103.97/35.05 [a__hd](x0) = x0 + 63, 103.97/35.05 103.97/35.05 [adx](x0) = x0, 103.97/35.05 103.97/35.05 [incr](x0) = x0 + 255, 103.97/35.05 103.97/35.05 [s](x0) = x0, 103.97/35.05 103.97/35.05 [a__incr](x0) = x0 + 113, 103.97/35.05 103.97/35.05 [cons](x0, x1) = x0 + x1 + 1, 103.97/35.05 103.97/35.05 [zeros] = 15, 103.97/35.05 103.97/35.05 [0] = 194, 103.97/35.05 103.97/35.05 [a__adx](x0) = x0 + 239, 103.97/35.05 103.97/35.05 [a__zeros] = 34, 103.97/35.05 103.97/35.05 [a__nats] = 0 103.97/35.05 orientation: 103.97/35.05 a__nats() = 0 >= 273 = a__adx(a__zeros()) 103.97/35.05 103.97/35.05 a__zeros() = 34 >= 210 = cons(0(),zeros()) 103.97/35.05 103.97/35.05 a__incr(cons(X,Y)) = X + Y + 114 >= X + Y + 256 = cons(s(X),incr(Y)) 103.97/35.05 103.97/35.05 a__adx(cons(X,Y)) = X + Y + 240 >= X + Y + 114 = a__incr(cons(X,adx(Y))) 103.97/35.05 103.97/35.05 a__hd(cons(X,Y)) = X + Y + 64 >= X + 20 = mark(X) 103.97/35.05 103.97/35.05 a__tl(cons(X,Y)) = X + Y + 232 >= Y + 20 = mark(Y) 103.97/35.05 103.97/35.05 mark(nats()) = 34 >= 0 = a__nats() 103.97/35.05 103.97/35.05 mark(adx(X)) = X + 20 >= X + 259 = a__adx(mark(X)) 103.97/35.05 103.97/35.05 mark(zeros()) = 35 >= 34 = a__zeros() 103.97/35.05 103.97/35.05 mark(incr(X)) = X + 275 >= X + 133 = a__incr(mark(X)) 103.97/35.05 103.97/35.05 mark(hd(X)) = X + 66 >= X + 83 = a__hd(mark(X)) 103.97/35.05 103.97/35.05 mark(tl(X)) = X + 150 >= X + 251 = a__tl(mark(X)) 103.97/35.05 103.97/35.05 mark(cons(X1,X2)) = X1 + X2 + 21 >= X1 + X2 + 1 = cons(X1,X2) 103.97/35.05 103.97/35.05 mark(0()) = 214 >= 194 = 0() 103.97/35.05 103.97/35.05 mark(s(X)) = X + 20 >= X = s(X) 103.97/35.05 103.97/35.05 a__nats() = 0 >= 14 = nats() 103.97/35.05 103.97/35.05 a__adx(X) = X + 239 >= X = adx(X) 103.97/35.05 103.97/35.05 a__zeros() = 34 >= 15 = zeros() 103.97/35.05 103.97/35.05 a__incr(X) = X + 113 >= X + 255 = incr(X) 103.97/35.05 103.97/35.05 a__hd(X) = X + 63 >= X + 46 = hd(X) 103.97/35.05 103.97/35.05 a__tl(X) = X + 231 >= X + 130 = tl(X) 103.97/35.05 problem: 103.97/35.05 strict: 103.97/35.05 a__nats() -> a__adx(a__zeros()) 103.97/35.05 a__zeros() -> cons(0(),zeros()) 103.97/35.05 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.05 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.05 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.05 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.05 a__nats() -> nats() 103.97/35.05 a__incr(X) -> incr(X) 103.97/35.05 weak: 103.97/35.05 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.05 a__hd(cons(X,Y)) -> mark(X) 103.97/35.05 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.05 mark(nats()) -> a__nats() 103.97/35.05 mark(zeros()) -> a__zeros() 103.97/35.05 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.05 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.05 mark(0()) -> 0() 103.97/35.05 mark(s(X)) -> s(X) 103.97/35.05 a__adx(X) -> adx(X) 103.97/35.05 a__zeros() -> zeros() 103.97/35.05 a__hd(X) -> hd(X) 103.97/35.05 a__tl(X) -> tl(X) 103.97/35.05 Matrix Interpretation Processor: dim=1 103.97/35.05 103.97/35.05 max_matrix: 103.97/35.05 1 103.97/35.05 interpretation: 103.97/35.05 [tl](x0) = x0, 103.97/35.05 103.97/35.05 [hd](x0) = x0, 103.97/35.05 103.97/35.05 [nats] = 5, 103.97/35.05 103.97/35.05 [a__tl](x0) = x0, 103.97/35.05 103.97/35.05 [mark](x0) = x0, 103.97/35.05 103.97/35.05 [a__hd](x0) = x0, 103.97/35.05 103.97/35.05 [adx](x0) = x0 + 2, 103.97/35.05 103.97/35.05 [incr](x0) = x0, 103.97/35.05 103.97/35.05 [s](x0) = x0 + 3, 103.97/35.05 103.97/35.05 [a__incr](x0) = x0, 103.97/35.05 103.97/35.05 [cons](x0, x1) = x0 + x1, 103.97/35.05 103.97/35.05 [zeros] = 0, 103.97/35.05 103.97/35.05 [0] = 0, 103.97/35.05 103.97/35.05 [a__adx](x0) = x0 + 2, 103.97/35.05 103.97/35.05 [a__zeros] = 0, 103.97/35.05 103.97/35.05 [a__nats] = 5 103.97/35.05 orientation: 103.97/35.05 a__nats() = 5 >= 2 = a__adx(a__zeros()) 103.97/35.05 103.97/35.05 a__zeros() = 0 >= 0 = cons(0(),zeros()) 103.97/35.05 103.97/35.05 a__incr(cons(X,Y)) = X + Y >= X + Y + 3 = cons(s(X),incr(Y)) 103.97/35.05 103.97/35.05 mark(adx(X)) = X + 2 >= X + 2 = a__adx(mark(X)) 103.97/35.05 103.97/35.05 mark(hd(X)) = X >= X = a__hd(mark(X)) 103.97/35.05 103.97/35.05 mark(tl(X)) = X >= X = a__tl(mark(X)) 103.97/35.05 103.97/35.05 a__nats() = 5 >= 5 = nats() 103.97/35.05 103.97/35.05 a__incr(X) = X >= X = incr(X) 103.97/35.05 103.97/35.05 a__adx(cons(X,Y)) = X + Y + 2 >= X + Y + 2 = a__incr(cons(X,adx(Y))) 103.97/35.05 103.97/35.05 a__hd(cons(X,Y)) = X + Y >= X = mark(X) 103.97/35.05 103.97/35.05 a__tl(cons(X,Y)) = X + Y >= Y = mark(Y) 103.97/35.05 103.97/35.05 mark(nats()) = 5 >= 5 = a__nats() 103.97/35.05 103.97/35.05 mark(zeros()) = 0 >= 0 = a__zeros() 103.97/35.05 103.97/35.05 mark(incr(X)) = X >= X = a__incr(mark(X)) 103.97/35.05 103.97/35.05 mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2) 103.97/35.05 103.97/35.05 mark(0()) = 0 >= 0 = 0() 103.97/35.05 103.97/35.05 mark(s(X)) = X + 3 >= X + 3 = s(X) 103.97/35.05 103.97/35.05 a__adx(X) = X + 2 >= X + 2 = adx(X) 103.97/35.05 103.97/35.05 a__zeros() = 0 >= 0 = zeros() 103.97/35.05 103.97/35.05 a__hd(X) = X >= X = hd(X) 103.97/35.05 103.97/35.05 a__tl(X) = X >= X = tl(X) 103.97/35.05 problem: 103.97/35.05 strict: 103.97/35.05 a__zeros() -> cons(0(),zeros()) 103.97/35.05 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.05 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.05 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.05 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.05 a__nats() -> nats() 103.97/35.05 a__incr(X) -> incr(X) 103.97/35.05 weak: 103.97/35.05 a__nats() -> a__adx(a__zeros()) 103.97/35.05 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.05 a__hd(cons(X,Y)) -> mark(X) 103.97/35.05 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.05 mark(nats()) -> a__nats() 103.97/35.05 mark(zeros()) -> a__zeros() 103.97/35.05 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.05 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.05 mark(0()) -> 0() 103.97/35.05 mark(s(X)) -> s(X) 103.97/35.05 a__adx(X) -> adx(X) 103.97/35.05 a__zeros() -> zeros() 103.97/35.05 a__hd(X) -> hd(X) 103.97/35.05 a__tl(X) -> tl(X) 103.97/35.05 Matrix Interpretation Processor: dim=1 103.97/35.05 103.97/35.05 max_matrix: 103.97/35.05 1 103.97/35.05 interpretation: 103.97/35.05 [tl](x0) = x0 + 2, 103.97/35.05 103.97/35.05 [hd](x0) = x0 + 4, 103.97/35.05 103.97/35.05 [nats] = 0, 103.97/35.05 103.97/35.05 [a__tl](x0) = x0 + 8, 103.97/35.05 103.97/35.05 [mark](x0) = x0 + 8, 103.97/35.05 103.97/35.05 [a__hd](x0) = x0 + 8, 103.97/35.05 103.97/35.05 [adx](x0) = x0, 103.97/35.05 103.97/35.05 [incr](x0) = x0, 103.97/35.05 103.97/35.05 [s](x0) = x0 + 2, 103.97/35.05 103.97/35.05 [a__incr](x0) = x0, 103.97/35.05 103.97/35.05 [cons](x0, x1) = x0 + x1, 103.97/35.05 103.97/35.05 [zeros] = 0, 103.97/35.05 103.97/35.05 [0] = 10, 103.97/35.05 103.97/35.05 [a__adx](x0) = x0, 103.97/35.05 103.97/35.05 [a__zeros] = 8, 103.97/35.05 103.97/35.05 [a__nats] = 8 103.97/35.05 orientation: 103.97/35.05 a__zeros() = 8 >= 10 = cons(0(),zeros()) 103.97/35.05 103.97/35.05 a__incr(cons(X,Y)) = X + Y >= X + Y + 2 = cons(s(X),incr(Y)) 103.97/35.05 103.97/35.05 mark(adx(X)) = X + 8 >= X + 8 = a__adx(mark(X)) 103.97/35.05 103.97/35.05 mark(hd(X)) = X + 12 >= X + 16 = a__hd(mark(X)) 103.97/35.05 103.97/35.05 mark(tl(X)) = X + 10 >= X + 16 = a__tl(mark(X)) 103.97/35.05 103.97/35.05 a__nats() = 8 >= 0 = nats() 103.97/35.05 103.97/35.05 a__incr(X) = X >= X = incr(X) 103.97/35.05 103.97/35.05 a__nats() = 8 >= 8 = a__adx(a__zeros()) 103.97/35.05 103.97/35.05 a__adx(cons(X,Y)) = X + Y >= X + Y = a__incr(cons(X,adx(Y))) 103.97/35.05 103.97/35.05 a__hd(cons(X,Y)) = X + Y + 8 >= X + 8 = mark(X) 103.97/35.05 103.97/35.05 a__tl(cons(X,Y)) = X + Y + 8 >= Y + 8 = mark(Y) 103.97/35.05 103.97/35.05 mark(nats()) = 8 >= 8 = a__nats() 103.97/35.05 103.97/35.05 mark(zeros()) = 8 >= 8 = a__zeros() 103.97/35.05 103.97/35.05 mark(incr(X)) = X + 8 >= X + 8 = a__incr(mark(X)) 103.97/35.05 103.97/35.05 mark(cons(X1,X2)) = X1 + X2 + 8 >= X1 + X2 = cons(X1,X2) 103.97/35.05 103.97/35.05 mark(0()) = 18 >= 10 = 0() 103.97/35.05 103.97/35.05 mark(s(X)) = X + 10 >= X + 2 = s(X) 103.97/35.05 103.97/35.05 a__adx(X) = X >= X = adx(X) 103.97/35.05 103.97/35.05 a__zeros() = 8 >= 0 = zeros() 103.97/35.05 103.97/35.05 a__hd(X) = X + 8 >= X + 4 = hd(X) 103.97/35.05 103.97/35.05 a__tl(X) = X + 8 >= X + 2 = tl(X) 103.97/35.05 problem: 103.97/35.05 strict: 103.97/35.05 a__zeros() -> cons(0(),zeros()) 103.97/35.05 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.05 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.05 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.05 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.05 a__incr(X) -> incr(X) 103.97/35.05 weak: 103.97/35.05 a__nats() -> nats() 103.97/35.05 a__nats() -> a__adx(a__zeros()) 103.97/35.05 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.05 a__hd(cons(X,Y)) -> mark(X) 103.97/35.05 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.06 mark(nats()) -> a__nats() 103.97/35.06 mark(zeros()) -> a__zeros() 103.97/35.06 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.06 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.06 mark(0()) -> 0() 103.97/35.06 mark(s(X)) -> s(X) 103.97/35.06 a__adx(X) -> adx(X) 103.97/35.06 a__zeros() -> zeros() 103.97/35.06 a__hd(X) -> hd(X) 103.97/35.06 a__tl(X) -> tl(X) 103.97/35.06 Matrix Interpretation Processor: dim=1 103.97/35.06 103.97/35.06 max_matrix: 103.97/35.06 1 103.97/35.06 interpretation: 103.97/35.06 [tl](x0) = x0 + 8, 103.97/35.06 103.97/35.06 [hd](x0) = x0 + 1, 103.97/35.06 103.97/35.06 [nats] = 6, 103.97/35.06 103.97/35.06 [a__tl](x0) = x0 + 8, 103.97/35.06 103.97/35.06 [mark](x0) = x0 + 1, 103.97/35.06 103.97/35.06 [a__hd](x0) = x0 + 1, 103.97/35.06 103.97/35.06 [adx](x0) = x0, 103.97/35.06 103.97/35.06 [incr](x0) = x0 + 3, 103.97/35.06 103.97/35.06 [s](x0) = x0 + 4, 103.97/35.06 103.97/35.06 [a__incr](x0) = x0 + 3, 103.97/35.06 103.97/35.06 [cons](x0, x1) = x0 + x1, 103.97/35.06 103.97/35.06 [zeros] = 3, 103.97/35.06 103.97/35.06 [0] = 0, 103.97/35.06 103.97/35.06 [a__adx](x0) = x0 + 3, 103.97/35.06 103.97/35.06 [a__zeros] = 4, 103.97/35.06 103.97/35.06 [a__nats] = 7 103.97/35.06 orientation: 103.97/35.06 a__zeros() = 4 >= 3 = cons(0(),zeros()) 103.97/35.06 103.97/35.06 a__incr(cons(X,Y)) = X + Y + 3 >= X + Y + 7 = cons(s(X),incr(Y)) 103.97/35.06 103.97/35.06 mark(adx(X)) = X + 1 >= X + 4 = a__adx(mark(X)) 103.97/35.06 103.97/35.06 mark(hd(X)) = X + 2 >= X + 2 = a__hd(mark(X)) 103.97/35.06 103.97/35.06 mark(tl(X)) = X + 9 >= X + 9 = a__tl(mark(X)) 103.97/35.06 103.97/35.06 a__incr(X) = X + 3 >= X + 3 = incr(X) 103.97/35.06 103.97/35.06 a__nats() = 7 >= 6 = nats() 103.97/35.06 103.97/35.06 a__nats() = 7 >= 7 = a__adx(a__zeros()) 103.97/35.06 103.97/35.06 a__adx(cons(X,Y)) = X + Y + 3 >= X + Y + 3 = a__incr(cons(X,adx(Y))) 103.97/35.06 103.97/35.06 a__hd(cons(X,Y)) = X + Y + 1 >= X + 1 = mark(X) 103.97/35.06 103.97/35.06 a__tl(cons(X,Y)) = X + Y + 8 >= Y + 1 = mark(Y) 103.97/35.06 103.97/35.06 mark(nats()) = 7 >= 7 = a__nats() 103.97/35.06 103.97/35.06 mark(zeros()) = 4 >= 4 = a__zeros() 103.97/35.06 103.97/35.06 mark(incr(X)) = X + 4 >= X + 4 = a__incr(mark(X)) 103.97/35.06 103.97/35.06 mark(cons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 = cons(X1,X2) 103.97/35.06 103.97/35.06 mark(0()) = 1 >= 0 = 0() 103.97/35.06 103.97/35.06 mark(s(X)) = X + 5 >= X + 4 = s(X) 103.97/35.06 103.97/35.06 a__adx(X) = X + 3 >= X = adx(X) 103.97/35.06 103.97/35.06 a__zeros() = 4 >= 3 = zeros() 103.97/35.06 103.97/35.06 a__hd(X) = X + 1 >= X + 1 = hd(X) 103.97/35.06 103.97/35.06 a__tl(X) = X + 8 >= X + 8 = tl(X) 103.97/35.06 problem: 103.97/35.06 strict: 103.97/35.06 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.06 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.06 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.06 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.06 a__incr(X) -> incr(X) 103.97/35.06 weak: 103.97/35.06 a__zeros() -> cons(0(),zeros()) 103.97/35.06 a__nats() -> nats() 103.97/35.06 a__nats() -> a__adx(a__zeros()) 103.97/35.06 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.06 a__hd(cons(X,Y)) -> mark(X) 103.97/35.06 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.06 mark(nats()) -> a__nats() 103.97/35.06 mark(zeros()) -> a__zeros() 103.97/35.06 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.06 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.06 mark(0()) -> 0() 103.97/35.06 mark(s(X)) -> s(X) 103.97/35.06 a__adx(X) -> adx(X) 103.97/35.06 a__zeros() -> zeros() 103.97/35.06 a__hd(X) -> hd(X) 103.97/35.06 a__tl(X) -> tl(X) 103.97/35.06 Splitting Processor: 103.97/35.06 strict: 103.97/35.06 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.06 weak: 103.97/35.06 a__zeros() -> cons(0(),zeros()) 103.97/35.06 a__nats() -> nats() 103.97/35.06 a__nats() -> a__adx(a__zeros()) 103.97/35.06 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.06 a__hd(cons(X,Y)) -> mark(X) 103.97/35.06 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.06 mark(nats()) -> a__nats() 103.97/35.06 mark(zeros()) -> a__zeros() 103.97/35.06 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.06 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.06 mark(0()) -> 0() 103.97/35.06 mark(s(X)) -> s(X) 103.97/35.06 a__adx(X) -> adx(X) 103.97/35.06 a__zeros() -> zeros() 103.97/35.06 a__hd(X) -> hd(X) 103.97/35.06 a__tl(X) -> tl(X) 103.97/35.06 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.06 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.06 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.06 a__incr(X) -> incr(X) 103.97/35.06 Matrix Interpretation Processor: dim=3 103.97/35.06 103.97/35.06 max_matrix: 103.97/35.06 [1 0 1] 103.97/35.06 [0 0 0] 103.97/35.06 [0 0 1] 103.97/35.06 interpretation: 103.97/35.06 [1 0 1] [1] 103.97/35.06 [tl](x0) = [0 0 0]x0 + [0] 103.97/35.06 [0 0 1] [1], 103.97/35.06 103.97/35.06 [1 0 1] [0] 103.97/35.06 [hd](x0) = [0 0 0]x0 + [0] 103.97/35.06 [0 0 1] [1], 103.97/35.06 103.97/35.06 [1] 103.97/35.06 [nats] = [0] 103.97/35.06 [0], 103.97/35.06 103.97/35.06 [1 0 1] [1] 103.97/35.06 [a__tl](x0) = [0 0 0]x0 + [0] 103.97/35.06 [0 0 1] [1], 103.97/35.06 103.97/35.06 [1 0 1] 103.97/35.06 [mark](x0) = [0 0 0]x0 103.97/35.06 [0 0 1] , 103.97/35.06 103.97/35.06 [1 0 1] [0] 103.97/35.06 [a__hd](x0) = [0 0 0]x0 + [0] 103.97/35.06 [0 0 1] [1], 103.97/35.06 103.97/35.06 [1 0 1] 103.97/35.06 [adx](x0) = [0 0 0]x0 103.97/35.06 [0 0 1] , 103.97/35.06 103.97/35.06 [1 0 0] 103.97/35.06 [incr](x0) = [0 0 0]x0 103.97/35.06 [0 0 1] , 103.97/35.06 103.97/35.06 [1 0 0] 103.97/35.06 [s](x0) = [0 0 0]x0 103.97/35.06 [0 0 0] , 103.97/35.06 103.97/35.06 [1 0 0] 103.97/35.06 [a__incr](x0) = [0 0 0]x0 103.97/35.06 [0 0 1] , 103.97/35.06 103.97/35.06 [1 0 1] [1 0 0] 103.97/35.06 [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 103.97/35.06 [0 0 1] [0 0 1] , 103.97/35.06 103.97/35.06 [1] 103.97/35.06 [zeros] = [0] 103.97/35.06 [0], 103.97/35.06 103.97/35.06 [0] 103.97/35.06 [0] = [0] 103.97/35.06 [0], 103.97/35.06 103.97/35.06 [1 0 1] 103.97/35.06 [a__adx](x0) = [0 0 0]x0 103.97/35.06 [0 0 1] , 103.97/35.06 103.97/35.06 [1] 103.97/35.06 [a__zeros] = [0] 103.97/35.06 [0], 103.97/35.06 103.97/35.06 [1] 103.97/35.06 [a__nats] = [0] 103.97/35.06 [0] 103.97/35.06 orientation: 103.97/35.06 [1 0 2] [2] [1 0 2] [1] 103.97/35.06 mark(tl(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__tl(mark(X)) 103.97/35.06 [0 0 1] [1] [0 0 1] [1] 103.97/35.06 103.97/35.06 [1] [1] 103.97/35.06 a__zeros() = [0] >= [0] = cons(0(),zeros()) 103.97/35.06 [0] [0] 103.97/35.06 103.97/35.06 [1] [1] 103.97/35.06 a__nats() = [0] >= [0] = nats() 103.97/35.06 [0] [0] 103.97/35.06 103.97/35.06 [1] [1] 103.97/35.06 a__nats() = [0] >= [0] = a__adx(a__zeros()) 103.97/35.06 [0] [0] 103.97/35.06 103.97/35.06 [1 0 2] [1 0 1] [1 0 1] [1 0 1] 103.97/35.06 a__adx(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = a__incr(cons(X,adx(Y))) 103.97/35.06 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 103.97/35.06 103.97/35.06 [1 0 2] [1 0 1] [0] [1 0 1] 103.97/35.06 a__hd(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [0] >= [0 0 0]X = mark(X) 103.97/35.06 [0 0 1] [0 0 1] [1] [0 0 1] 103.97/35.06 103.97/35.06 [1 0 2] [1 0 1] [1] [1 0 1] 103.97/35.06 a__tl(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [0] >= [0 0 0]Y = mark(Y) 103.97/35.06 [0 0 1] [0 0 1] [1] [0 0 1] 103.97/35.06 103.97/35.06 [1] [1] 103.97/35.06 mark(nats()) = [0] >= [0] = a__nats() 103.97/35.06 [0] [0] 103.97/35.06 103.97/35.06 [1] [1] 103.97/35.06 mark(zeros()) = [0] >= [0] = a__zeros() 103.97/35.06 [0] [0] 103.97/35.06 103.97/35.06 [1 0 1] [1 0 1] 103.97/35.06 mark(incr(X)) = [0 0 0]X >= [0 0 0]X = a__incr(mark(X)) 103.97/35.06 [0 0 1] [0 0 1] 103.97/35.06 103.97/35.06 [1 0 2] [1 0 1] [1 0 1] [1 0 0] 103.97/35.06 mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 103.97/35.06 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 103.97/35.06 103.97/35.06 [0] [0] 103.97/35.06 mark(0()) = [0] >= [0] = 0() 103.97/35.06 [0] [0] 103.97/35.06 103.97/35.06 [1 0 0] [1 0 0] 103.97/35.06 mark(s(X)) = [0 0 0]X >= [0 0 0]X = s(X) 103.97/35.06 [0 0 0] [0 0 0] 103.97/35.06 103.97/35.06 [1 0 1] [1 0 1] 103.97/35.06 a__adx(X) = [0 0 0]X >= [0 0 0]X = adx(X) 103.97/35.06 [0 0 1] [0 0 1] 103.97/35.06 103.97/35.06 [1] [1] 103.97/35.06 a__zeros() = [0] >= [0] = zeros() 103.97/35.06 [0] [0] 103.97/35.06 103.97/35.06 [1 0 1] [0] [1 0 1] [0] 103.97/35.06 a__hd(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = hd(X) 103.97/35.06 [0 0 1] [1] [0 0 1] [1] 103.97/35.06 103.97/35.06 [1 0 1] [1] [1 0 1] [1] 103.97/35.06 a__tl(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = tl(X) 103.97/35.06 [0 0 1] [1] [0 0 1] [1] 103.97/35.06 103.97/35.06 [1 0 1] [1 0 0] [1 0 0] [1 0 0] 103.97/35.06 a__incr(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = cons(s(X),incr(Y)) 103.97/35.06 [0 0 1] [0 0 1] [0 0 0] [0 0 1] 103.97/35.06 103.97/35.06 [1 0 2] [1 0 2] 103.97/35.06 mark(adx(X)) = [0 0 0]X >= [0 0 0]X = a__adx(mark(X)) 103.97/35.06 [0 0 1] [0 0 1] 103.97/35.06 103.97/35.06 [1 0 2] [1] [1 0 2] [0] 103.97/35.06 mark(hd(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__hd(mark(X)) 103.97/35.06 [0 0 1] [1] [0 0 1] [1] 103.97/35.06 103.97/35.06 [1 0 0] [1 0 0] 103.97/35.06 a__incr(X) = [0 0 0]X >= [0 0 0]X = incr(X) 103.97/35.06 [0 0 1] [0 0 1] 103.97/35.06 problem: 103.97/35.06 strict: 103.97/35.06 103.97/35.06 weak: 103.97/35.06 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.06 a__zeros() -> cons(0(),zeros()) 103.97/35.06 a__nats() -> nats() 103.97/35.06 a__nats() -> a__adx(a__zeros()) 103.97/35.06 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.06 a__hd(cons(X,Y)) -> mark(X) 103.97/35.06 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.06 mark(nats()) -> a__nats() 103.97/35.06 mark(zeros()) -> a__zeros() 103.97/35.06 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.06 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.06 mark(0()) -> 0() 103.97/35.06 mark(s(X)) -> s(X) 103.97/35.06 a__adx(X) -> adx(X) 103.97/35.06 a__zeros() -> zeros() 103.97/35.06 a__hd(X) -> hd(X) 103.97/35.06 a__tl(X) -> tl(X) 103.97/35.06 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.06 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.06 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.06 a__incr(X) -> incr(X) 103.97/35.06 Qed 103.97/35.06 103.97/35.06 strict: 103.97/35.06 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.06 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.06 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.06 a__incr(X) -> incr(X) 103.97/35.06 weak: 103.97/35.06 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.06 a__zeros() -> cons(0(),zeros()) 103.97/35.06 a__nats() -> nats() 103.97/35.06 a__nats() -> a__adx(a__zeros()) 103.97/35.06 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.06 a__hd(cons(X,Y)) -> mark(X) 103.97/35.06 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.06 mark(nats()) -> a__nats() 103.97/35.06 mark(zeros()) -> a__zeros() 103.97/35.06 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.06 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.06 mark(0()) -> 0() 103.97/35.06 mark(s(X)) -> s(X) 103.97/35.06 a__adx(X) -> adx(X) 103.97/35.06 a__zeros() -> zeros() 103.97/35.06 a__hd(X) -> hd(X) 103.97/35.06 a__tl(X) -> tl(X) 103.97/35.06 Splitting Processor: 103.97/35.06 strict: 103.97/35.06 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.06 weak: 103.97/35.06 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.06 a__zeros() -> cons(0(),zeros()) 103.97/35.06 a__nats() -> nats() 103.97/35.06 a__nats() -> a__adx(a__zeros()) 103.97/35.06 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.06 a__hd(cons(X,Y)) -> mark(X) 103.97/35.06 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.06 mark(nats()) -> a__nats() 103.97/35.06 mark(zeros()) -> a__zeros() 103.97/35.06 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.06 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.06 mark(0()) -> 0() 103.97/35.06 mark(s(X)) -> s(X) 103.97/35.06 a__adx(X) -> adx(X) 103.97/35.06 a__zeros() -> zeros() 103.97/35.06 a__hd(X) -> hd(X) 103.97/35.06 a__tl(X) -> tl(X) 103.97/35.06 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.06 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.06 a__incr(X) -> incr(X) 103.97/35.06 Splitting Processor: 103.97/35.06 strict: 103.97/35.06 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.06 weak: 103.97/35.06 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.07 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.07 a__zeros() -> cons(0(),zeros()) 103.97/35.07 a__nats() -> nats() 103.97/35.07 a__nats() -> a__adx(a__zeros()) 103.97/35.07 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.07 a__hd(cons(X,Y)) -> mark(X) 103.97/35.07 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.07 mark(nats()) -> a__nats() 103.97/35.07 mark(zeros()) -> a__zeros() 103.97/35.07 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.07 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.07 mark(0()) -> 0() 103.97/35.07 mark(s(X)) -> s(X) 103.97/35.07 a__adx(X) -> adx(X) 103.97/35.07 a__zeros() -> zeros() 103.97/35.07 a__hd(X) -> hd(X) 103.97/35.07 a__tl(X) -> tl(X) 103.97/35.07 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.07 a__incr(X) -> incr(X) 103.97/35.07 Matrix Interpretation Processor: dim=3 103.97/35.07 103.97/35.07 max_matrix: 103.97/35.07 [1 1 1] 103.97/35.07 [0 1 1] 103.97/35.07 [0 0 0] 103.97/35.07 interpretation: 103.97/35.07 [1 1 1] 103.97/35.07 [tl](x0) = [0 1 1]x0 103.97/35.07 [0 0 0] , 103.97/35.07 103.97/35.07 [1 0 1] 103.97/35.07 [hd](x0) = [0 1 1]x0 103.97/35.07 [0 0 0] , 103.97/35.07 103.97/35.07 [0] 103.97/35.07 [nats] = [1] 103.97/35.07 [0], 103.97/35.07 103.97/35.07 [1 1 1] 103.97/35.07 [a__tl](x0) = [0 1 1]x0 103.97/35.07 [0 0 0] , 103.97/35.07 103.97/35.07 [1 1 0] 103.97/35.07 [mark](x0) = [0 1 0]x0 103.97/35.07 [0 0 0] , 103.97/35.07 103.97/35.07 [1 0 1] 103.97/35.07 [a__hd](x0) = [0 1 1]x0 103.97/35.07 [0 0 0] , 103.97/35.07 103.97/35.07 [1 0 0] [1] 103.97/35.07 [adx](x0) = [0 1 0]x0 + [1] 103.97/35.07 [0 0 0] [0], 103.97/35.07 103.97/35.07 [1 0 1] 103.97/35.07 [incr](x0) = [0 1 1]x0 103.97/35.07 [0 0 0] , 103.97/35.07 103.97/35.07 [1 0 0] 103.97/35.07 [s](x0) = [0 1 0]x0 103.97/35.07 [0 0 0] , 103.97/35.07 103.97/35.07 [1 0 1] 103.97/35.07 [a__incr](x0) = [0 1 1]x0 103.97/35.07 [0 0 0] , 103.97/35.07 103.97/35.07 [1 1 1] [1 0 1] 103.97/35.07 [cons](x0, x1) = [0 1 0]x0 + [0 1 1]x1 103.97/35.07 [0 0 0] [0 0 0] , 103.97/35.07 103.97/35.07 [0] 103.97/35.07 [zeros] = [0] 103.97/35.07 [0], 103.97/35.07 103.97/35.07 [0] 103.97/35.07 [0] = [0] 103.97/35.07 [0], 103.97/35.07 103.97/35.07 [1 0 0] [1] 103.97/35.07 [a__adx](x0) = [0 1 1]x0 + [1] 103.97/35.07 [0 0 0] [0], 103.97/35.07 103.97/35.07 [0] 103.97/35.07 [a__zeros] = [0] 103.97/35.07 [0], 103.97/35.07 103.97/35.07 [1] 103.97/35.07 [a__nats] = [1] 103.97/35.07 [0] 103.97/35.07 orientation: 103.97/35.07 [1 1 0] [2] [1 1 0] [1] 103.97/35.07 mark(adx(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = a__adx(mark(X)) 103.97/35.07 [0 0 0] [0] [0 0 0] [0] 103.97/35.07 103.97/35.07 [1 1 2] [1 1 0] 103.97/35.07 mark(hd(X)) = [0 1 1]X >= [0 1 0]X = a__hd(mark(X)) 103.97/35.07 [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [1 2 2] [1 2 0] 103.97/35.07 mark(tl(X)) = [0 1 1]X >= [0 1 0]X = a__tl(mark(X)) 103.97/35.07 [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [0] [0] 103.97/35.07 a__zeros() = [0] >= [0] = cons(0(),zeros()) 103.97/35.07 [0] [0] 103.97/35.07 103.97/35.07 [1] [0] 103.97/35.07 a__nats() = [1] >= [1] = nats() 103.97/35.07 [0] [0] 103.97/35.07 103.97/35.07 [1] [1] 103.97/35.07 a__nats() = [1] >= [1] = a__adx(a__zeros()) 103.97/35.07 [0] [0] 103.97/35.07 103.97/35.07 [1 1 1] [1 0 1] [1] [1 1 1] [1 0 0] [1] 103.97/35.07 a__adx(cons(X,Y)) = [0 1 0]X + [0 1 1]Y + [1] >= [0 1 0]X + [0 1 0]Y + [1] = a__incr(cons(X,adx(Y))) 103.97/35.07 [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] 103.97/35.07 103.97/35.07 [1 1 1] [1 0 1] [1 1 0] 103.97/35.07 a__hd(cons(X,Y)) = [0 1 0]X + [0 1 1]Y >= [0 1 0]X = mark(X) 103.97/35.07 [0 0 0] [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [1 2 1] [1 1 2] [1 1 0] 103.97/35.07 a__tl(cons(X,Y)) = [0 1 0]X + [0 1 1]Y >= [0 1 0]Y = mark(Y) 103.97/35.07 [0 0 0] [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [1] [1] 103.97/35.07 mark(nats()) = [1] >= [1] = a__nats() 103.97/35.07 [0] [0] 103.97/35.07 103.97/35.07 [0] [0] 103.97/35.07 mark(zeros()) = [0] >= [0] = a__zeros() 103.97/35.07 [0] [0] 103.97/35.07 103.97/35.07 [1 1 2] [1 1 0] 103.97/35.07 mark(incr(X)) = [0 1 1]X >= [0 1 0]X = a__incr(mark(X)) 103.97/35.07 [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [1 2 1] [1 1 2] [1 1 1] [1 0 1] 103.97/35.07 mark(cons(X1,X2)) = [0 1 0]X1 + [0 1 1]X2 >= [0 1 0]X1 + [0 1 1]X2 = cons(X1,X2) 103.97/35.07 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [0] [0] 103.97/35.07 mark(0()) = [0] >= [0] = 0() 103.97/35.07 [0] [0] 103.97/35.07 103.97/35.07 [1 1 0] [1 0 0] 103.97/35.07 mark(s(X)) = [0 1 0]X >= [0 1 0]X = s(X) 103.97/35.07 [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [1 0 0] [1] [1 0 0] [1] 103.97/35.07 a__adx(X) = [0 1 1]X + [1] >= [0 1 0]X + [1] = adx(X) 103.97/35.07 [0 0 0] [0] [0 0 0] [0] 103.97/35.07 103.97/35.07 [0] [0] 103.97/35.07 a__zeros() = [0] >= [0] = zeros() 103.97/35.07 [0] [0] 103.97/35.07 103.97/35.07 [1 0 1] [1 0 1] 103.97/35.07 a__hd(X) = [0 1 1]X >= [0 1 1]X = hd(X) 103.97/35.07 [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [1 1 1] [1 1 1] 103.97/35.07 a__tl(X) = [0 1 1]X >= [0 1 1]X = tl(X) 103.97/35.07 [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [1 1 1] [1 0 1] [1 1 0] [1 0 1] 103.97/35.07 a__incr(cons(X,Y)) = [0 1 0]X + [0 1 1]Y >= [0 1 0]X + [0 1 1]Y = cons(s(X),incr(Y)) 103.97/35.07 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 103.97/35.07 103.97/35.07 [1 0 1] [1 0 1] 103.97/35.07 a__incr(X) = [0 1 1]X >= [0 1 1]X = incr(X) 103.97/35.07 [0 0 0] [0 0 0] 103.97/35.07 problem: 103.97/35.07 strict: 103.97/35.07 103.97/35.07 weak: 103.97/35.07 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.07 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.07 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.07 a__zeros() -> cons(0(),zeros()) 103.97/35.07 a__nats() -> nats() 103.97/35.07 a__nats() -> a__adx(a__zeros()) 103.97/35.07 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.07 a__hd(cons(X,Y)) -> mark(X) 103.97/35.07 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.07 mark(nats()) -> a__nats() 103.97/35.07 mark(zeros()) -> a__zeros() 103.97/35.07 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.07 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.07 mark(0()) -> 0() 103.97/35.07 mark(s(X)) -> s(X) 103.97/35.07 a__adx(X) -> adx(X) 103.97/35.07 a__zeros() -> zeros() 103.97/35.07 a__hd(X) -> hd(X) 103.97/35.07 a__tl(X) -> tl(X) 103.97/35.07 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.07 a__incr(X) -> incr(X) 103.97/35.07 Qed 103.97/35.07 103.97/35.07 strict: 103.97/35.07 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.07 a__incr(X) -> incr(X) 103.97/35.07 weak: 103.97/35.07 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.07 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.07 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.07 a__zeros() -> cons(0(),zeros()) 103.97/35.07 a__nats() -> nats() 103.97/35.07 a__nats() -> a__adx(a__zeros()) 103.97/35.07 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.08 a__hd(cons(X,Y)) -> mark(X) 103.97/35.08 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.08 mark(nats()) -> a__nats() 103.97/35.08 mark(zeros()) -> a__zeros() 103.97/35.08 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.08 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.08 mark(0()) -> 0() 103.97/35.08 mark(s(X)) -> s(X) 103.97/35.08 a__adx(X) -> adx(X) 103.97/35.08 a__zeros() -> zeros() 103.97/35.08 a__hd(X) -> hd(X) 103.97/35.08 a__tl(X) -> tl(X) 103.97/35.08 Matrix Interpretation Processor: dim=4 103.97/35.08 103.97/35.08 max_matrix: 103.97/35.08 [1 1 1 1] 103.97/35.08 [0 0 0 0] 103.97/35.08 [0 0 1 1] 103.97/35.08 [0 0 0 1] 103.97/35.08 interpretation: 103.97/35.08 [1 0 1 1] [1] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [tl](x0) = [0 0 1 1]x0 + [0] 103.97/35.08 [0 0 0 1] [0], 103.97/35.08 103.97/35.08 [1 0 1 0] [1] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [hd](x0) = [0 0 1 1]x0 + [0] 103.97/35.08 [0 0 0 1] [0], 103.97/35.08 103.97/35.08 [0] 103.97/35.08 [0] 103.97/35.08 [nats] = [0] 103.97/35.08 [1], 103.97/35.08 103.97/35.08 [1 1 1 1] [1] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [a__tl](x0) = [0 0 1 1]x0 + [0] 103.97/35.08 [0 0 0 1] [0], 103.97/35.08 103.97/35.08 [1 0 1 1] 103.97/35.08 [0 0 0 0] 103.97/35.08 [mark](x0) = [0 0 1 1]x0 103.97/35.08 [0 0 0 1] , 103.97/35.08 103.97/35.08 [1 0 1 0] [1] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [a__hd](x0) = [0 0 1 1]x0 + [0] 103.97/35.08 [0 0 0 1] [0], 103.97/35.08 103.97/35.08 [1 0 0 0] [0] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [adx](x0) = [0 0 1 0]x0 + [0] 103.97/35.08 [0 0 0 1] [1], 103.97/35.08 103.97/35.08 [1 0 0 0] [0] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [incr](x0) = [0 0 1 0]x0 + [1] 103.97/35.08 [0 0 0 1] [0], 103.97/35.08 103.97/35.08 [1 0 0 0] [1] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [s](x0) = [0 0 1 0]x0 + [0] 103.97/35.08 [0 0 0 0] [0], 103.97/35.08 103.97/35.08 [1 0 0 0] [1] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [a__incr](x0) = [0 0 1 0]x0 + [1] 103.97/35.08 [0 0 0 1] [0], 103.97/35.08 103.97/35.08 [1 0 0 1] [1 0 0 0] 103.97/35.08 [0 0 0 0] [0 0 0 0] 103.97/35.08 [cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 103.97/35.08 [0 0 0 1] [0 0 0 1] , 103.97/35.08 103.97/35.08 [0] 103.97/35.08 [0] 103.97/35.08 [zeros] = [0] 103.97/35.08 [0], 103.97/35.08 103.97/35.08 [0] 103.97/35.08 [0] 103.97/35.08 [0] = [0] 103.97/35.08 [0], 103.97/35.08 103.97/35.08 [1 0 0 0] [1] 103.97/35.08 [0 0 0 0] [0] 103.97/35.08 [a__adx](x0) = [0 0 1 0]x0 + [1] 103.97/35.08 [0 0 0 1] [1], 103.97/35.08 103.97/35.08 [0] 103.97/35.08 [0] 103.97/35.08 [a__zeros] = [0] 103.97/35.08 [0], 103.97/35.08 103.97/35.08 [1] 103.97/35.08 [0] 103.97/35.08 [a__nats] = [1] 103.97/35.08 [1] 103.97/35.08 orientation: 103.97/35.08 [1 0 0 1] [1 0 0 0] [1] [1 0 0 0] [1 0 0 0] [1] 103.97/35.08 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 103.97/35.08 a__incr(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y + [1] >= [0 0 1 0]X + [0 0 1 0]Y + [1] = cons(s(X),incr(Y)) 103.97/35.08 [0 0 0 1] [0 0 0 1] [0] [0 0 0 0] [0 0 0 1] [0] 103.97/35.08 103.97/35.08 [1 0 0 0] [1] [1 0 0 0] [0] 103.97/35.08 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.08 a__incr(X) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = incr(X) 103.97/35.08 [0 0 0 1] [0] [0 0 0 1] [0] 103.97/35.08 103.97/35.08 [1 0 1 1] [1] [1 0 1 1] [1] 103.97/35.08 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.08 mark(adx(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = a__adx(mark(X)) 103.97/35.08 [0 0 0 1] [1] [0 0 0 1] [1] 103.97/35.08 103.97/35.08 [1 0 2 2] [1] [1 0 2 2] [1] 103.97/35.08 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.08 mark(hd(X)) = [0 0 1 2]X + [0] >= [0 0 1 2]X + [0] = a__hd(mark(X)) 103.97/35.08 [0 0 0 1] [0] [0 0 0 1] [0] 103.97/35.08 103.97/35.08 [1 0 2 3] [1] [1 0 2 3] [1] 103.97/35.08 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.08 mark(tl(X)) = [0 0 1 2]X + [0] >= [0 0 1 2]X + [0] = a__tl(mark(X)) 103.97/35.08 [0 0 0 1] [0] [0 0 0 1] [0] 103.97/35.08 103.97/35.08 [0] [0] 103.97/35.08 [0] [0] 103.97/35.08 a__zeros() = [0] >= [0] = cons(0(),zeros()) 103.97/35.08 [0] [0] 103.97/35.08 103.97/35.08 [1] [0] 103.97/35.08 [0] [0] 103.97/35.08 a__nats() = [1] >= [0] = nats() 103.97/35.08 [1] [1] 103.97/35.08 103.97/35.08 [1] [1] 103.97/35.08 [0] [0] 103.97/35.08 a__nats() = [1] >= [1] = a__adx(a__zeros()) 103.97/35.08 [1] [1] 103.97/35.08 103.97/35.08 [1 0 0 1] [1 0 0 0] [1] [1 0 0 1] [1 0 0 0] [1] 103.97/35.08 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 103.97/35.08 a__adx(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y + [1] >= [0 0 1 0]X + [0 0 1 0]Y + [1] = a__incr(cons(X,adx(Y))) 103.97/35.08 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 103.97/35.08 103.97/35.08 [1 0 1 1] [1 0 1 0] [1] [1 0 1 1] 103.97/35.08 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 103.97/35.08 a__hd(cons(X,Y)) = [0 0 1 1]X + [0 0 1 1]Y + [0] >= [0 0 1 1]X = mark(X) 103.97/35.08 [0 0 0 1] [0 0 0 1] [0] [0 0 0 1] 103.97/35.08 103.97/35.08 [1 0 1 2] [1 0 1 1] [1] [1 0 1 1] 103.97/35.08 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 103.97/35.08 a__tl(cons(X,Y)) = [0 0 1 1]X + [0 0 1 1]Y + [0] >= [0 0 1 1]Y = mark(Y) 103.97/35.08 [0 0 0 1] [0 0 0 1] [0] [0 0 0 1] 103.97/35.08 103.97/35.08 [1] [1] 103.97/35.08 [0] [0] 103.97/35.08 mark(nats()) = [1] >= [1] = a__nats() 103.97/35.08 [1] [1] 103.97/35.08 103.97/35.08 [0] [0] 103.97/35.08 [0] [0] 103.97/35.08 mark(zeros()) = [0] >= [0] = a__zeros() 103.97/35.08 [0] [0] 103.97/35.08 103.97/35.08 [1 0 1 1] [1] [1 0 1 1] [1] 103.97/35.08 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.08 mark(incr(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = a__incr(mark(X)) 103.97/35.08 [0 0 0 1] [0] [0 0 0 1] [0] 103.97/35.08 103.97/35.08 [1 0 1 2] [1 0 1 1] [1 0 0 1] [1 0 0 0] 103.97/35.08 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 103.97/35.08 mark(cons(X1,X2)) = [0 0 1 1]X1 + [0 0 1 1]X2 >= [0 0 1 0]X1 + [0 0 1 0]X2 = cons(X1,X2) 103.97/35.08 [0 0 0 1] [0 0 0 1] [0 0 0 1] [0 0 0 1] 103.97/35.08 103.97/35.08 [0] [0] 103.97/35.08 [0] [0] 103.97/35.08 mark(0()) = [0] >= [0] = 0() 103.97/35.08 [0] [0] 103.97/35.08 103.97/35.09 [1 0 1 0] [1] [1 0 0 0] [1] 103.97/35.09 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.09 mark(s(X)) = [0 0 1 0]X + [0] >= [0 0 1 0]X + [0] = s(X) 103.97/35.09 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.09 103.97/35.09 [1 0 0 0] [1] [1 0 0 0] [0] 103.97/35.09 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.09 a__adx(X) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [0] = adx(X) 103.97/35.09 [0 0 0 1] [1] [0 0 0 1] [1] 103.97/35.09 103.97/35.09 [0] [0] 103.97/35.09 [0] [0] 103.97/35.09 a__zeros() = [0] >= [0] = zeros() 103.97/35.09 [0] [0] 103.97/35.09 103.97/35.09 [1 0 1 0] [1] [1 0 1 0] [1] 103.97/35.09 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.09 a__hd(X) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = hd(X) 103.97/35.09 [0 0 0 1] [0] [0 0 0 1] [0] 103.97/35.09 103.97/35.09 [1 1 1 1] [1] [1 0 1 1] [1] 103.97/35.09 [0 0 0 0] [0] [0 0 0 0] [0] 103.97/35.09 a__tl(X) = [0 0 1 1]X + [0] >= [0 0 1 1]X + [0] = tl(X) 103.97/35.09 [0 0 0 1] [0] [0 0 0 1] [0] 103.97/35.09 problem: 103.97/35.09 strict: 103.97/35.09 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.09 weak: 103.97/35.09 a__incr(X) -> incr(X) 103.97/35.09 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.09 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.09 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.09 a__zeros() -> cons(0(),zeros()) 103.97/35.09 a__nats() -> nats() 103.97/35.09 a__nats() -> a__adx(a__zeros()) 103.97/35.09 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.09 a__hd(cons(X,Y)) -> mark(X) 103.97/35.09 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.09 mark(nats()) -> a__nats() 103.97/35.09 mark(zeros()) -> a__zeros() 103.97/35.09 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.09 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.09 mark(0()) -> 0() 103.97/35.09 mark(s(X)) -> s(X) 103.97/35.09 a__adx(X) -> adx(X) 103.97/35.09 a__zeros() -> zeros() 103.97/35.09 a__hd(X) -> hd(X) 103.97/35.09 a__tl(X) -> tl(X) 103.97/35.09 Matrix Interpretation Processor: dim=4 103.97/35.09 103.97/35.09 max_matrix: 103.97/35.09 [1 1 1 1] 103.97/35.09 [0 1 1 1] 103.97/35.09 [0 0 0 0] 103.97/35.09 [0 0 0 1] 103.97/35.09 interpretation: 103.97/35.09 [1 1 1 1] [0] 103.97/35.09 [0 1 1 1] [0] 103.97/35.09 [tl](x0) = [0 0 0 0]x0 + [0] 103.97/35.09 [0 0 0 1] [1], 103.97/35.09 103.97/35.09 [1 0 0 0] [0] 103.97/35.09 [0 1 1 0] [0] 103.97/35.09 [hd](x0) = [0 0 0 0]x0 + [0] 103.97/35.09 [0 0 0 1] [1], 103.97/35.09 103.97/35.09 [0] 103.97/35.09 [0] 103.97/35.09 [nats] = [0] 103.97/35.09 [1], 103.97/35.09 103.97/35.09 [1 1 1 1] [0] 103.97/35.09 [0 1 1 1] [0] 103.97/35.09 [a__tl](x0) = [0 0 0 0]x0 + [1] 103.97/35.09 [0 0 0 1] [1], 103.97/35.09 103.97/35.09 [1 1 1 1] [1] 103.97/35.09 [0 1 1 1] [0] 103.97/35.09 [mark](x0) = [0 0 0 0]x0 + [1] 103.97/35.09 [0 0 0 1] [0], 103.97/35.09 103.97/35.09 [1 0 0 0] [1] 103.97/35.09 [0 1 1 0] [0] 103.97/35.09 [a__hd](x0) = [0 0 0 0]x0 + [1] 103.97/35.09 [0 0 0 1] [1], 103.97/35.09 103.97/35.09 [1 0 0 0] [0] 103.97/35.09 [0 1 1 0] [0] 103.97/35.09 [adx](x0) = [0 0 0 0]x0 + [0] 103.97/35.09 [0 0 0 1] [1], 103.97/35.09 103.97/35.09 [1 0 0 0] [0] 103.97/35.09 [0 1 1 0] [0] 103.97/35.09 [incr](x0) = [0 0 0 0]x0 + [1] 103.97/35.09 [0 0 0 1] [0], 103.97/35.09 103.97/35.09 [1 0 0 0] 103.97/35.09 [0 0 1 0] 103.97/35.09 [s](x0) = [0 0 0 0]x0 103.97/35.09 [0 0 0 1] , 103.97/35.09 103.97/35.09 [1 0 1 0] [0] 103.97/35.09 [0 1 1 0] [0] 103.97/35.09 [a__incr](x0) = [0 0 0 0]x0 + [1] 103.97/35.09 [0 0 0 1] [0], 103.97/35.09 103.97/35.09 [1 1 1 1] [1 0 0 0] [0] 103.97/35.09 [0 1 1 1] [0 1 1 0] [0] 103.97/35.09 [cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [1] 103.97/35.09 [0 0 0 1] [0 0 0 1] [0], 103.97/35.09 103.97/35.09 [0] 103.97/35.09 [0] 103.97/35.09 [zeros] = [0] 103.97/35.09 [0], 103.97/35.09 103.97/35.09 [0] 103.97/35.09 [0] 103.97/35.09 [0] = [0] 103.97/35.09 [0], 103.97/35.09 103.97/35.09 [1 0 0 0] [1] 103.97/35.09 [0 1 1 0] [0] 103.97/35.09 [a__adx](x0) = [0 0 0 0]x0 + [1] 103.97/35.09 [0 0 0 1] [1], 103.97/35.09 103.97/35.09 [0] 103.97/35.09 [0] 103.97/35.09 [a__zeros] = [1] 103.97/35.09 [0], 103.97/35.09 103.97/35.09 [1] 103.97/35.09 [1] 103.97/35.09 [a__nats] = [1] 103.97/35.09 [1] 103.97/35.09 orientation: 103.97/35.09 [1 1 1 1] [1 0 0 0] [1] [1 0 1 1] [1 0 0 0] [0] 103.97/35.09 [0 1 1 1] [0 1 1 0] [1] [0 0 1 1] [0 1 1 0] [1] 103.97/35.09 a__incr(cons(X,Y)) = [0 0 0 0]X + [0 0 0 0]Y + [1] >= [0 0 0 0]X + [0 0 0 0]Y + [1] = cons(s(X),incr(Y)) 103.97/35.09 [0 0 0 1] [0 0 0 1] [0] [0 0 0 1] [0 0 0 1] [0] 103.97/35.09 103.97/35.09 [1 0 1 0] [0] [1 0 0 0] [0] 103.97/35.09 [0 1 1 0] [0] [0 1 1 0] [0] 103.97/35.09 a__incr(X) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = incr(X) 103.97/35.09 [0 0 0 1] [0] [0 0 0 1] [0] 103.97/35.09 103.97/35.09 [1 1 1 1] [2] [1 1 1 1] [2] 103.97/35.09 [0 1 1 1] [1] [0 1 1 1] [1] 103.97/35.09 mark(adx(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = a__adx(mark(X)) 103.97/35.09 [0 0 0 1] [1] [0 0 0 1] [1] 103.97/35.09 103.97/35.09 [1 1 1 1] [2] [1 1 1 1] [2] 103.97/35.09 [0 1 1 1] [1] [0 1 1 1] [1] 103.97/35.09 mark(hd(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = a__hd(mark(X)) 103.97/35.09 [0 0 0 1] [1] [0 0 0 1] [1] 103.97/35.09 103.97/35.09 [1 2 2 3] [2] [1 2 2 3] [2] 103.97/35.09 [0 1 1 2] [1] [0 1 1 2] [1] 103.97/35.09 mark(tl(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = a__tl(mark(X)) 103.97/35.09 [0 0 0 1] [1] [0 0 0 1] [1] 103.97/35.09 103.97/35.09 [0] [0] 103.97/35.09 [0] [0] 103.97/35.09 a__zeros() = [1] >= [1] = cons(0(),zeros()) 103.97/35.09 [0] [0] 103.97/35.09 103.97/35.09 [1] [0] 103.97/35.09 [1] [0] 103.97/35.09 a__nats() = [1] >= [0] = nats() 103.97/35.09 [1] [1] 103.97/35.09 103.97/35.09 [1] [1] 103.97/35.09 [1] [1] 103.97/35.09 a__nats() = [1] >= [1] = a__adx(a__zeros()) 103.97/35.09 [1] [1] 103.97/35.09 103.97/35.09 [1 1 1 1] [1 0 0 0] [1] [1 1 1 1] [1 0 0 0] [1] 103.97/35.09 [0 1 1 1] [0 1 1 0] [1] [0 1 1 1] [0 1 1 0] [1] 103.97/35.09 a__adx(cons(X,Y)) = [0 0 0 0]X + [0 0 0 0]Y + [1] >= [0 0 0 0]X + [0 0 0 0]Y + [1] = a__incr(cons(X,adx(Y))) 103.97/35.09 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 103.97/35.09 103.97/35.09 [1 1 1 1] [1 0 0 0] [1] [1 1 1 1] [1] 103.97/35.09 [0 1 1 1] [0 1 1 0] [1] [0 1 1 1] [0] 103.97/35.10 a__hd(cons(X,Y)) = [0 0 0 0]X + [0 0 0 0]Y + [1] >= [0 0 0 0]X + [1] = mark(X) 103.97/35.10 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0] 103.97/35.10 103.97/35.10 [1 2 2 3] [1 1 1 1] [1] [1 1 1 1] [1] 103.97/35.10 [0 1 1 2] [0 1 1 1] [1] [0 1 1 1] [0] 103.97/35.10 a__tl(cons(X,Y)) = [0 0 0 0]X + [0 0 0 0]Y + [1] >= [0 0 0 0]Y + [1] = mark(Y) 103.97/35.10 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0] 103.97/35.10 103.97/35.10 [2] [1] 103.97/35.10 [1] [1] 103.97/35.10 mark(nats()) = [1] >= [1] = a__nats() 103.97/35.10 [1] [1] 103.97/35.10 103.97/35.10 [1] [0] 103.97/35.10 [0] [0] 103.97/35.10 mark(zeros()) = [1] >= [1] = a__zeros() 103.97/35.10 [0] [0] 103.97/35.10 103.97/35.10 [1 1 1 1] [2] [1 1 1 1] [2] 103.97/35.10 [0 1 1 1] [1] [0 1 1 1] [1] 103.97/35.10 mark(incr(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [1] = a__incr(mark(X)) 103.97/35.10 [0 0 0 1] [0] [0 0 0 1] [0] 103.97/35.10 103.97/35.10 [1 2 2 3] [1 1 1 1] [2] [1 1 1 1] [1 0 0 0] [0] 103.97/35.10 [0 1 1 2] [0 1 1 1] [1] [0 1 1 1] [0 1 1 0] [0] 103.97/35.10 mark(cons(X1,X2)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [1] >= [0 0 0 0]X1 + [0 0 0 0]X2 + [1] = cons(X1,X2) 103.97/35.10 [0 0 0 1] [0 0 0 1] [0] [0 0 0 1] [0 0 0 1] [0] 103.97/35.10 103.97/35.10 [1] [0] 103.97/35.10 [0] [0] 103.97/35.10 mark(0()) = [1] >= [0] = 0() 103.97/35.10 [0] [0] 103.97/35.10 103.97/35.10 [1 0 1 1] [1] [1 0 0 0] 103.97/35.10 [0 0 1 1] [0] [0 0 1 0] 103.97/35.10 mark(s(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X = s(X) 103.97/35.10 [0 0 0 1] [0] [0 0 0 1] 103.97/35.10 103.97/35.10 [1 0 0 0] [1] [1 0 0 0] [0] 103.97/35.10 [0 1 1 0] [0] [0 1 1 0] [0] 103.97/35.10 a__adx(X) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [0] = adx(X) 103.97/35.10 [0 0 0 1] [1] [0 0 0 1] [1] 103.97/35.10 103.97/35.10 [0] [0] 103.97/35.10 [0] [0] 103.97/35.10 a__zeros() = [1] >= [0] = zeros() 103.97/35.10 [0] [0] 103.97/35.10 103.97/35.10 [1 0 0 0] [1] [1 0 0 0] [0] 103.97/35.10 [0 1 1 0] [0] [0 1 1 0] [0] 103.97/35.10 a__hd(X) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [0] = hd(X) 103.97/35.10 [0 0 0 1] [1] [0 0 0 1] [1] 103.97/35.10 103.97/35.10 [1 1 1 1] [0] [1 1 1 1] [0] 103.97/35.10 [0 1 1 1] [0] [0 1 1 1] [0] 103.97/35.10 a__tl(X) = [0 0 0 0]X + [1] >= [0 0 0 0]X + [0] = tl(X) 103.97/35.10 [0 0 0 1] [1] [0 0 0 1] [1] 103.97/35.10 problem: 103.97/35.10 strict: 103.97/35.10 103.97/35.10 weak: 103.97/35.10 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 103.97/35.10 a__incr(X) -> incr(X) 103.97/35.10 mark(adx(X)) -> a__adx(mark(X)) 103.97/35.10 mark(hd(X)) -> a__hd(mark(X)) 103.97/35.10 mark(tl(X)) -> a__tl(mark(X)) 103.97/35.10 a__zeros() -> cons(0(),zeros()) 103.97/35.10 a__nats() -> nats() 103.97/35.10 a__nats() -> a__adx(a__zeros()) 103.97/35.10 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 103.97/35.10 a__hd(cons(X,Y)) -> mark(X) 103.97/35.10 a__tl(cons(X,Y)) -> mark(Y) 103.97/35.10 mark(nats()) -> a__nats() 103.97/35.10 mark(zeros()) -> a__zeros() 103.97/35.10 mark(incr(X)) -> a__incr(mark(X)) 103.97/35.10 mark(cons(X1,X2)) -> cons(X1,X2) 103.97/35.10 mark(0()) -> 0() 103.97/35.10 mark(s(X)) -> s(X) 104.07/35.10 a__adx(X) -> adx(X) 104.07/35.10 a__zeros() -> zeros() 104.07/35.10 a__hd(X) -> hd(X) 104.07/35.10 a__tl(X) -> tl(X) 104.07/35.10 Qed 104.07/35.10 104.07/35.10 strict: 104.07/35.10 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 104.07/35.10 mark(adx(X)) -> a__adx(mark(X)) 104.07/35.10 a__incr(X) -> incr(X) 104.07/35.10 weak: 104.07/35.10 mark(hd(X)) -> a__hd(mark(X)) 104.07/35.10 mark(tl(X)) -> a__tl(mark(X)) 104.07/35.10 a__zeros() -> cons(0(),zeros()) 104.07/35.10 a__nats() -> nats() 104.07/35.10 a__nats() -> a__adx(a__zeros()) 104.07/35.10 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 104.07/35.10 a__hd(cons(X,Y)) -> mark(X) 104.07/35.10 a__tl(cons(X,Y)) -> mark(Y) 104.07/35.10 mark(nats()) -> a__nats() 104.07/35.10 mark(zeros()) -> a__zeros() 104.07/35.10 mark(incr(X)) -> a__incr(mark(X)) 104.07/35.10 mark(cons(X1,X2)) -> cons(X1,X2) 104.07/35.10 mark(0()) -> 0() 104.07/35.10 mark(s(X)) -> s(X) 104.07/35.10 a__adx(X) -> adx(X) 104.07/35.10 a__zeros() -> zeros() 104.07/35.10 a__hd(X) -> hd(X) 104.07/35.10 a__tl(X) -> tl(X) 104.07/35.10 Matrix Interpretation Processor: dim=4 104.07/35.10 104.07/35.10 max_matrix: 104.07/35.10 [1 1 1 1] 104.07/35.10 [0 0 0 1] 104.07/35.10 [0 0 1 1] 104.07/35.10 [0 0 0 0] 104.07/35.10 interpretation: 104.07/35.10 [1 0 1 0] 104.07/35.10 [0 0 0 0] 104.07/35.10 [tl](x0) = [0 0 1 0]x0 104.07/35.10 [0 0 0 0] , 104.07/35.10 104.07/35.10 [1 0 0 1] [1] 104.07/35.10 [0 0 0 0] [0] 104.07/35.10 [hd](x0) = [0 0 1 1]x0 + [1] 104.07/35.10 [0 0 0 0] [0], 104.07/35.10 104.07/35.10 [0] 104.07/35.10 [0] 104.07/35.10 [nats] = [1] 104.07/35.10 [0], 104.07/35.10 104.07/35.10 [1 0 1 0] 104.07/35.10 [0 0 0 0] 104.07/35.10 [a__tl](x0) = [0 0 1 0]x0 104.07/35.10 [0 0 0 0] , 104.07/35.10 104.07/35.10 [1 0 1 0] 104.07/35.10 [0 0 0 0] 104.07/35.10 [mark](x0) = [0 0 1 0]x0 104.07/35.10 [0 0 0 0] , 104.07/35.10 104.07/35.10 [1 0 0 1] [1] 104.07/35.10 [0 0 0 0] [0] 104.07/35.10 [a__hd](x0) = [0 0 1 1]x0 + [1] 104.07/35.10 [0 0 0 0] [0], 104.07/35.10 104.07/35.10 [1 0 0 1] 104.07/35.10 [0 0 0 0] 104.07/35.10 [adx](x0) = [0 0 1 0]x0 104.07/35.10 [0 0 0 0] , 104.07/35.10 104.07/35.10 [1 0 0 0] 104.07/35.10 [0 0 0 1] 104.07/35.10 [incr](x0) = [0 0 1 0]x0 104.07/35.10 [0 0 0 0] , 104.07/35.10 104.07/35.10 [1 0 0 0] 104.07/35.10 [0 0 0 0] 104.07/35.10 [s](x0) = [0 0 0 0]x0 104.07/35.10 [0 0 0 0] , 104.07/35.10 104.07/35.10 [1 0 0 1] 104.07/35.10 [0 0 0 1] 104.07/35.10 [a__incr](x0) = [0 0 1 1]x0 104.07/35.10 [0 0 0 0] , 104.07/35.10 104.07/35.10 [1 0 1 0] [1 1 0 1] 104.07/35.10 [0 0 0 0] [0 0 0 0] 104.07/35.10 [cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 104.07/35.10 [0 0 0 0] [0 0 0 0] , 104.07/35.10 104.07/35.10 [0] 104.07/35.10 [0] 104.07/35.10 [zeros] = [1] 104.07/35.10 [0], 104.07/35.10 104.07/35.10 [0] 104.07/35.10 [0] 104.07/35.10 [0] = [0] 104.07/35.10 [0], 104.07/35.10 104.07/35.10 [1 0 0 1] 104.07/35.10 [0 0 0 0] 104.07/35.10 [a__adx](x0) = [0 0 1 0]x0 104.07/35.10 [0 0 0 0] , 104.07/35.10 104.07/35.10 [0] 104.07/35.10 [0] 104.07/35.10 [a__zeros] = [1] 104.07/35.10 [0], 104.07/35.10 104.07/35.10 [0] 104.07/35.10 [0] 104.07/35.10 [a__nats] = [1] 104.07/35.10 [0] 104.07/35.10 orientation: 104.07/35.10 [1 0 1 2] [2] [1 0 1 0] [1] 104.07/35.10 [0 0 0 0] [0] [0 0 0 0] [0] 104.07/35.10 mark(hd(X)) = [0 0 1 1]X + [1] >= [0 0 1 0]X + [1] = a__hd(mark(X)) 104.07/35.10 [0 0 0 0] [0] [0 0 0 0] [0] 104.07/35.10 104.07/35.10 [1 0 2 0] [1 0 2 0] 104.07/35.10 [0 0 0 0] [0 0 0 0] 104.07/35.10 mark(tl(X)) = [0 0 1 0]X >= [0 0 1 0]X = a__tl(mark(X)) 104.07/35.10 [0 0 0 0] [0 0 0 0] 104.07/35.10 104.07/35.10 [0] [0] 104.07/35.11 [0] [0] 104.07/35.11 a__zeros() = [1] >= [1] = cons(0(),zeros()) 104.07/35.11 [0] [0] 104.07/35.11 104.07/35.11 [0] [0] 104.07/35.11 [0] [0] 104.07/35.11 a__nats() = [1] >= [1] = nats() 104.07/35.11 [0] [0] 104.07/35.11 104.07/35.11 [0] [0] 104.07/35.11 [0] [0] 104.07/35.11 a__nats() = [1] >= [1] = a__adx(a__zeros()) 104.07/35.11 [0] [0] 104.07/35.11 104.07/35.11 [1 0 1 0] [1 1 0 1] [1 0 1 0] [1 0 0 1] 104.07/35.11 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 104.07/35.11 a__adx(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y >= [0 0 1 0]X + [0 0 1 0]Y = a__incr(cons(X,adx(Y))) 104.07/35.11 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [1 0 1 0] [1 1 0 1] [1] [1 0 1 0] 104.07/35.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 104.07/35.11 a__hd(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y + [1] >= [0 0 1 0]X = mark(X) 104.07/35.11 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 104.07/35.11 104.07/35.11 [1 0 2 0] [1 1 1 1] [1 0 1 0] 104.07/35.11 [0 0 0 0] [0 0 0 0] [0 0 0 0] 104.07/35.11 a__tl(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y >= [0 0 1 0]Y = mark(Y) 104.07/35.11 [0 0 0 0] [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [1] [0] 104.07/35.11 [0] [0] 104.07/35.11 mark(nats()) = [1] >= [1] = a__nats() 104.07/35.11 [0] [0] 104.07/35.11 104.07/35.11 [1] [0] 104.07/35.11 [0] [0] 104.07/35.11 mark(zeros()) = [1] >= [1] = a__zeros() 104.07/35.11 [0] [0] 104.07/35.11 104.07/35.11 [1 0 1 0] [1 0 1 0] 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 mark(incr(X)) = [0 0 1 0]X >= [0 0 1 0]X = a__incr(mark(X)) 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [1 0 2 0] [1 1 1 1] [1 0 1 0] [1 1 0 1] 104.07/35.11 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 104.07/35.11 mark(cons(X1,X2)) = [0 0 1 0]X1 + [0 0 1 0]X2 >= [0 0 1 0]X1 + [0 0 1 0]X2 = cons(X1,X2) 104.07/35.11 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [0] [0] 104.07/35.11 [0] [0] 104.07/35.11 mark(0()) = [0] >= [0] = 0() 104.07/35.11 [0] [0] 104.07/35.11 104.07/35.11 [1 0 0 0] [1 0 0 0] 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 mark(s(X)) = [0 0 0 0]X >= [0 0 0 0]X = s(X) 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [1 0 0 1] [1 0 0 1] 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 a__adx(X) = [0 0 1 0]X >= [0 0 1 0]X = adx(X) 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [0] [0] 104.07/35.11 [0] [0] 104.07/35.11 a__zeros() = [1] >= [1] = zeros() 104.07/35.11 [0] [0] 104.07/35.11 104.07/35.11 [1 0 0 1] [1] [1 0 0 1] [1] 104.07/35.11 [0 0 0 0] [0] [0 0 0 0] [0] 104.07/35.11 a__hd(X) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = hd(X) 104.07/35.11 [0 0 0 0] [0] [0 0 0 0] [0] 104.07/35.11 104.07/35.11 [1 0 1 0] [1 0 1 0] 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 a__tl(X) = [0 0 1 0]X >= [0 0 1 0]X = tl(X) 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [1 0 1 0] [1 1 0 1] [1 0 0 0] [1 0 0 1] 104.07/35.11 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 104.07/35.11 a__incr(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y >= [0 0 0 0]X + [0 0 1 0]Y = cons(s(X),incr(Y)) 104.07/35.11 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [1 0 1 1] [1 0 1 0] 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 mark(adx(X)) = [0 0 1 0]X >= [0 0 1 0]X = a__adx(mark(X)) 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 104.07/35.11 [1 0 0 1] [1 0 0 0] 104.07/35.11 [0 0 0 1] [0 0 0 1] 104.07/35.11 a__incr(X) = [0 0 1 1]X >= [0 0 1 0]X = incr(X) 104.07/35.11 [0 0 0 0] [0 0 0 0] 104.07/35.11 problem: 104.07/35.11 strict: 104.07/35.11 104.07/35.11 weak: 104.07/35.11 mark(hd(X)) -> a__hd(mark(X)) 104.07/35.11 mark(tl(X)) -> a__tl(mark(X)) 104.07/35.11 a__zeros() -> cons(0(),zeros()) 104.07/35.11 a__nats() -> nats() 104.07/35.11 a__nats() -> a__adx(a__zeros()) 104.07/35.11 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 104.07/35.11 a__hd(cons(X,Y)) -> mark(X) 104.07/35.11 a__tl(cons(X,Y)) -> mark(Y) 104.07/35.11 mark(nats()) -> a__nats() 104.07/35.11 mark(zeros()) -> a__zeros() 104.07/35.11 mark(incr(X)) -> a__incr(mark(X)) 104.07/35.11 mark(cons(X1,X2)) -> cons(X1,X2) 104.07/35.11 mark(0()) -> 0() 104.07/35.11 mark(s(X)) -> s(X) 104.07/35.11 a__adx(X) -> adx(X) 104.07/35.11 a__zeros() -> zeros() 104.07/35.11 a__hd(X) -> hd(X) 104.07/35.11 a__tl(X) -> tl(X) 104.07/35.11 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 104.07/35.11 mark(adx(X)) -> a__adx(mark(X)) 104.07/35.11 a__incr(X) -> incr(X) 104.07/35.11 Qed 104.07/35.12 EOF