YES(?,O(n^3)) 85.26/31.54 YES(?,O(n^3)) 85.26/31.54 85.26/31.54 Problem: 85.26/31.54 a__nats() -> a__adx(a__zeros()) 85.26/31.54 a__zeros() -> cons(0(),zeros()) 85.26/31.54 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.54 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.54 a__hd(cons(X,Y)) -> mark(X) 85.26/31.54 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.54 mark(nats()) -> a__nats() 85.26/31.54 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.54 mark(zeros()) -> a__zeros() 85.26/31.54 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.54 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.54 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.54 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.54 mark(0()) -> 0() 85.26/31.54 mark(s(X)) -> s(X) 85.26/31.54 a__nats() -> nats() 85.26/31.54 a__adx(X) -> adx(X) 85.26/31.54 a__zeros() -> zeros() 85.26/31.54 a__incr(X) -> incr(X) 85.26/31.54 a__hd(X) -> hd(X) 85.26/31.54 a__tl(X) -> tl(X) 85.26/31.54 85.26/31.54 Proof: 85.26/31.54 Complexity Transformation Processor: 85.26/31.54 strict: 85.26/31.54 a__nats() -> a__adx(a__zeros()) 85.26/31.54 a__zeros() -> cons(0(),zeros()) 85.26/31.54 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.54 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.54 a__hd(cons(X,Y)) -> mark(X) 85.26/31.54 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.54 mark(nats()) -> a__nats() 85.26/31.54 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.54 mark(zeros()) -> a__zeros() 85.26/31.54 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.54 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.54 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.54 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.54 mark(0()) -> 0() 85.26/31.54 mark(s(X)) -> s(X) 85.26/31.54 a__nats() -> nats() 85.26/31.54 a__adx(X) -> adx(X) 85.26/31.54 a__zeros() -> zeros() 85.26/31.54 a__incr(X) -> incr(X) 85.26/31.54 a__hd(X) -> hd(X) 85.26/31.54 a__tl(X) -> tl(X) 85.26/31.54 weak: 85.26/31.54 85.26/31.54 Matrix Interpretation Processor: dim=1 85.26/31.54 85.26/31.54 max_matrix: 85.26/31.54 1 85.26/31.54 interpretation: 85.26/31.54 [tl](x0) = x0, 85.26/31.54 85.26/31.54 [hd](x0) = x0 + 10, 85.26/31.54 85.26/31.54 [nats] = 12, 85.26/31.54 85.26/31.54 [a__tl](x0) = x0 + 5, 85.26/31.54 85.26/31.54 [mark](x0) = x0 + 6, 85.26/31.54 85.26/31.54 [a__hd](x0) = x0 + 4, 85.26/31.54 85.26/31.54 [adx](x0) = x0, 85.26/31.54 85.26/31.54 [incr](x0) = x0, 85.26/31.54 85.26/31.54 [s](x0) = x0, 85.26/31.54 85.26/31.54 [a__incr](x0) = x0 + 4, 85.26/31.54 85.26/31.54 [cons](x0, x1) = x0 + x1 + 13, 85.26/31.54 85.26/31.54 [zeros] = 2, 85.26/31.54 85.26/31.54 [0] = 1, 85.26/31.54 85.26/31.54 [a__adx](x0) = x0 + 2, 85.26/31.54 85.26/31.54 [a__zeros] = 0, 85.26/31.54 85.26/31.54 [a__nats] = 0 85.26/31.54 orientation: 85.26/31.54 a__nats() = 0 >= 2 = a__adx(a__zeros()) 85.26/31.54 85.26/31.54 a__zeros() = 0 >= 16 = cons(0(),zeros()) 85.26/31.54 85.26/31.54 a__incr(cons(X,Y)) = X + Y + 17 >= X + Y + 13 = cons(s(X),incr(Y)) 85.26/31.54 85.26/31.54 a__adx(cons(X,Y)) = X + Y + 15 >= X + Y + 17 = a__incr(cons(X,adx(Y))) 85.26/31.54 85.26/31.54 a__hd(cons(X,Y)) = X + Y + 17 >= X + 6 = mark(X) 85.26/31.54 85.26/31.54 a__tl(cons(X,Y)) = X + Y + 18 >= Y + 6 = mark(Y) 85.26/31.54 85.26/31.54 mark(nats()) = 18 >= 0 = a__nats() 85.26/31.54 85.26/31.54 mark(adx(X)) = X + 6 >= X + 8 = a__adx(mark(X)) 85.26/31.54 85.26/31.54 mark(zeros()) = 8 >= 0 = a__zeros() 85.26/31.54 85.26/31.54 mark(incr(X)) = X + 6 >= X + 10 = a__incr(mark(X)) 85.26/31.54 85.26/31.54 mark(hd(X)) = X + 16 >= X + 10 = a__hd(mark(X)) 85.26/31.54 85.26/31.54 mark(tl(X)) = X + 6 >= X + 11 = a__tl(mark(X)) 85.26/31.54 85.26/31.54 mark(cons(X1,X2)) = X1 + X2 + 19 >= X1 + X2 + 13 = cons(X1,X2) 85.26/31.54 85.26/31.54 mark(0()) = 7 >= 1 = 0() 85.26/31.54 85.26/31.54 mark(s(X)) = X + 6 >= X = s(X) 85.26/31.54 85.26/31.54 a__nats() = 0 >= 12 = nats() 85.26/31.54 85.26/31.54 a__adx(X) = X + 2 >= X = adx(X) 85.26/31.54 85.26/31.54 a__zeros() = 0 >= 2 = zeros() 85.26/31.54 85.26/31.54 a__incr(X) = X + 4 >= X = incr(X) 85.26/31.54 85.26/31.54 a__hd(X) = X + 4 >= X + 10 = hd(X) 85.26/31.54 85.26/31.54 a__tl(X) = X + 5 >= X = tl(X) 85.26/31.54 problem: 85.26/31.54 strict: 85.26/31.54 a__nats() -> a__adx(a__zeros()) 85.26/31.54 a__zeros() -> cons(0(),zeros()) 85.26/31.54 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.54 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.54 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.54 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.54 a__nats() -> nats() 85.26/31.54 a__zeros() -> zeros() 85.26/31.54 a__hd(X) -> hd(X) 85.26/31.54 weak: 85.26/31.54 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.54 a__hd(cons(X,Y)) -> mark(X) 85.26/31.54 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.54 mark(nats()) -> a__nats() 85.26/31.54 mark(zeros()) -> a__zeros() 85.26/31.54 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.54 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.54 mark(0()) -> 0() 85.26/31.54 mark(s(X)) -> s(X) 85.26/31.54 a__adx(X) -> adx(X) 85.26/31.54 a__incr(X) -> incr(X) 85.26/31.54 a__tl(X) -> tl(X) 85.26/31.54 Matrix Interpretation Processor: dim=1 85.26/31.54 85.26/31.54 max_matrix: 85.26/31.54 1 85.26/31.54 interpretation: 85.26/31.54 [tl](x0) = x0, 85.26/31.54 85.26/31.54 [hd](x0) = x0, 85.26/31.54 85.26/31.54 [nats] = 6, 85.26/31.54 85.26/31.54 [a__tl](x0) = x0, 85.26/31.54 85.26/31.54 [mark](x0) = x0, 85.26/31.54 85.26/31.54 [a__hd](x0) = x0, 85.26/31.54 85.26/31.54 [adx](x0) = x0, 85.26/31.54 85.26/31.54 [incr](x0) = x0 + 4, 85.26/31.54 85.26/31.54 [s](x0) = x0, 85.26/31.54 85.26/31.54 [a__incr](x0) = x0 + 4, 85.26/31.54 85.26/31.54 [cons](x0, x1) = x0 + x1, 85.26/31.54 85.26/31.54 [zeros] = 8, 85.26/31.54 85.26/31.54 [0] = 0, 85.26/31.54 85.26/31.54 [a__adx](x0) = x0 + 8, 85.26/31.54 85.26/31.54 [a__zeros] = 8, 85.26/31.54 85.26/31.54 [a__nats] = 6 85.26/31.54 orientation: 85.26/31.54 a__nats() = 6 >= 16 = a__adx(a__zeros()) 85.26/31.54 85.26/31.54 a__zeros() = 8 >= 8 = cons(0(),zeros()) 85.26/31.54 85.26/31.54 a__adx(cons(X,Y)) = X + Y + 8 >= X + Y + 4 = a__incr(cons(X,adx(Y))) 85.26/31.54 85.26/31.54 mark(adx(X)) = X >= X + 8 = a__adx(mark(X)) 85.26/31.54 85.26/31.54 mark(incr(X)) = X + 4 >= X + 4 = a__incr(mark(X)) 85.26/31.54 85.26/31.54 mark(tl(X)) = X >= X = a__tl(mark(X)) 85.26/31.54 85.26/31.54 a__nats() = 6 >= 6 = nats() 85.26/31.54 85.26/31.54 a__zeros() = 8 >= 8 = zeros() 85.26/31.54 85.26/31.54 a__hd(X) = X >= X = hd(X) 85.26/31.54 85.26/31.54 a__incr(cons(X,Y)) = X + Y + 4 >= X + Y + 4 = cons(s(X),incr(Y)) 85.26/31.54 85.26/31.54 a__hd(cons(X,Y)) = X + Y >= X = mark(X) 85.26/31.54 85.26/31.54 a__tl(cons(X,Y)) = X + Y >= Y = mark(Y) 85.26/31.54 85.26/31.54 mark(nats()) = 6 >= 6 = a__nats() 85.26/31.54 85.26/31.54 mark(zeros()) = 8 >= 8 = a__zeros() 85.26/31.54 85.26/31.54 mark(hd(X)) = X >= X = a__hd(mark(X)) 85.26/31.54 85.26/31.54 mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2) 85.26/31.54 85.26/31.54 mark(0()) = 0 >= 0 = 0() 85.26/31.54 85.26/31.54 mark(s(X)) = X >= X = s(X) 85.26/31.54 85.26/31.54 a__adx(X) = X + 8 >= X = adx(X) 85.26/31.54 85.26/31.54 a__incr(X) = X + 4 >= X + 4 = incr(X) 85.26/31.54 85.26/31.54 a__tl(X) = X >= X = tl(X) 85.26/31.54 problem: 85.26/31.54 strict: 85.26/31.54 a__nats() -> a__adx(a__zeros()) 85.26/31.54 a__zeros() -> cons(0(),zeros()) 85.26/31.54 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.54 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.54 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.54 a__nats() -> nats() 85.26/31.54 a__zeros() -> zeros() 85.26/31.54 a__hd(X) -> hd(X) 85.26/31.54 weak: 85.26/31.54 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.54 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.54 a__hd(cons(X,Y)) -> mark(X) 85.26/31.54 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.54 mark(nats()) -> a__nats() 85.26/31.54 mark(zeros()) -> a__zeros() 85.26/31.54 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.54 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.54 mark(0()) -> 0() 85.26/31.54 mark(s(X)) -> s(X) 85.26/31.54 a__adx(X) -> adx(X) 85.26/31.54 a__incr(X) -> incr(X) 85.26/31.54 a__tl(X) -> tl(X) 85.26/31.54 Matrix Interpretation Processor: dim=1 85.26/31.54 85.26/31.54 max_matrix: 85.26/31.54 1 85.26/31.54 interpretation: 85.26/31.54 [tl](x0) = x0 + 26, 85.26/31.54 85.26/31.54 [hd](x0) = x0 + 26, 85.26/31.54 85.26/31.54 [nats] = 36, 85.26/31.54 85.26/31.54 [a__tl](x0) = x0 + 26, 85.26/31.54 85.26/31.54 [mark](x0) = x0 + 68, 85.26/31.54 85.26/31.54 [a__hd](x0) = x0 + 26, 85.26/31.54 85.26/31.54 [adx](x0) = x0 + 24, 85.26/31.54 85.26/31.54 [incr](x0) = x0 + 13, 85.26/31.54 85.26/31.54 [s](x0) = x0 + 37, 85.26/31.54 85.26/31.54 [a__incr](x0) = x0 + 50, 85.26/31.54 85.26/31.54 [cons](x0, x1) = x0 + x1 + 42, 85.26/31.54 85.26/31.54 [zeros] = 36, 85.26/31.54 85.26/31.54 [0] = 88, 85.26/31.54 85.26/31.54 [a__adx](x0) = x0 + 74, 85.26/31.54 85.26/31.54 [a__zeros] = 104, 85.26/31.54 85.26/31.54 [a__nats] = 104 85.26/31.54 orientation: 85.26/31.54 a__nats() = 104 >= 178 = a__adx(a__zeros()) 85.26/31.54 85.26/31.54 a__zeros() = 104 >= 166 = cons(0(),zeros()) 85.26/31.54 85.26/31.54 mark(adx(X)) = X + 92 >= X + 142 = a__adx(mark(X)) 85.26/31.54 85.26/31.54 mark(incr(X)) = X + 81 >= X + 118 = a__incr(mark(X)) 85.26/31.54 85.26/31.54 mark(tl(X)) = X + 94 >= X + 94 = a__tl(mark(X)) 85.26/31.54 85.26/31.54 a__nats() = 104 >= 36 = nats() 85.26/31.54 85.26/31.54 a__zeros() = 104 >= 36 = zeros() 85.26/31.54 85.26/31.54 a__hd(X) = X + 26 >= X + 26 = hd(X) 85.26/31.54 85.26/31.54 a__adx(cons(X,Y)) = X + Y + 116 >= X + Y + 116 = a__incr(cons(X,adx(Y))) 85.26/31.54 85.26/31.54 a__incr(cons(X,Y)) = X + Y + 92 >= X + Y + 92 = cons(s(X),incr(Y)) 85.26/31.54 85.26/31.54 a__hd(cons(X,Y)) = X + Y + 68 >= X + 68 = mark(X) 85.26/31.54 85.26/31.54 a__tl(cons(X,Y)) = X + Y + 68 >= Y + 68 = mark(Y) 85.26/31.54 85.26/31.54 mark(nats()) = 104 >= 104 = a__nats() 85.26/31.54 85.26/31.54 mark(zeros()) = 104 >= 104 = a__zeros() 85.26/31.54 85.26/31.54 mark(hd(X)) = X + 94 >= X + 94 = a__hd(mark(X)) 85.26/31.54 85.26/31.54 mark(cons(X1,X2)) = X1 + X2 + 110 >= X1 + X2 + 42 = cons(X1,X2) 85.26/31.54 85.26/31.54 mark(0()) = 156 >= 88 = 0() 85.26/31.54 85.26/31.54 mark(s(X)) = X + 105 >= X + 37 = s(X) 85.26/31.54 85.26/31.54 a__adx(X) = X + 74 >= X + 24 = adx(X) 85.26/31.54 85.26/31.54 a__incr(X) = X + 50 >= X + 13 = incr(X) 85.26/31.54 85.26/31.54 a__tl(X) = X + 26 >= X + 26 = tl(X) 85.26/31.54 problem: 85.26/31.54 strict: 85.26/31.54 a__nats() -> a__adx(a__zeros()) 85.26/31.54 a__zeros() -> cons(0(),zeros()) 85.26/31.54 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.54 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.54 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.54 a__hd(X) -> hd(X) 85.26/31.54 weak: 85.26/31.54 a__nats() -> nats() 85.26/31.54 a__zeros() -> zeros() 85.26/31.54 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.54 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.55 a__hd(cons(X,Y)) -> mark(X) 85.26/31.55 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.55 mark(nats()) -> a__nats() 85.26/31.55 mark(zeros()) -> a__zeros() 85.26/31.55 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.55 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.55 mark(0()) -> 0() 85.26/31.55 mark(s(X)) -> s(X) 85.26/31.55 a__adx(X) -> adx(X) 85.26/31.55 a__incr(X) -> incr(X) 85.26/31.55 a__tl(X) -> tl(X) 85.26/31.55 Matrix Interpretation Processor: dim=1 85.26/31.55 85.26/31.55 max_matrix: 85.26/31.55 1 85.26/31.55 interpretation: 85.26/31.55 [tl](x0) = x0, 85.26/31.55 85.26/31.55 [hd](x0) = x0, 85.26/31.55 85.26/31.55 [nats] = 10, 85.26/31.55 85.26/31.55 [a__tl](x0) = x0, 85.26/31.55 85.26/31.55 [mark](x0) = x0, 85.26/31.55 85.26/31.55 [a__hd](x0) = x0, 85.26/31.55 85.26/31.55 [adx](x0) = x0 + 4, 85.26/31.55 85.26/31.55 [incr](x0) = x0 + 1, 85.26/31.55 85.26/31.55 [s](x0) = x0, 85.26/31.55 85.26/31.55 [a__incr](x0) = x0 + 1, 85.26/31.55 85.26/31.55 [cons](x0, x1) = x0 + x1, 85.26/31.55 85.26/31.55 [zeros] = 0, 85.26/31.55 85.26/31.55 [0] = 8, 85.26/31.55 85.26/31.55 [a__adx](x0) = x0 + 5, 85.26/31.55 85.26/31.55 [a__zeros] = 0, 85.26/31.55 85.26/31.55 [a__nats] = 10 85.26/31.55 orientation: 85.26/31.55 a__nats() = 10 >= 5 = a__adx(a__zeros()) 85.26/31.55 85.26/31.55 a__zeros() = 0 >= 8 = cons(0(),zeros()) 85.26/31.55 85.26/31.55 mark(adx(X)) = X + 4 >= X + 5 = a__adx(mark(X)) 85.26/31.55 85.26/31.55 mark(incr(X)) = X + 1 >= X + 1 = a__incr(mark(X)) 85.26/31.55 85.26/31.55 mark(tl(X)) = X >= X = a__tl(mark(X)) 85.26/31.55 85.26/31.55 a__hd(X) = X >= X = hd(X) 85.26/31.55 85.26/31.55 a__nats() = 10 >= 10 = nats() 85.26/31.55 85.26/31.55 a__zeros() = 0 >= 0 = zeros() 85.26/31.55 85.26/31.55 a__adx(cons(X,Y)) = X + Y + 5 >= X + Y + 5 = a__incr(cons(X,adx(Y))) 85.26/31.55 85.26/31.55 a__incr(cons(X,Y)) = X + Y + 1 >= X + Y + 1 = cons(s(X),incr(Y)) 85.26/31.55 85.26/31.55 a__hd(cons(X,Y)) = X + Y >= X = mark(X) 85.26/31.55 85.26/31.55 a__tl(cons(X,Y)) = X + Y >= Y = mark(Y) 85.26/31.55 85.26/31.55 mark(nats()) = 10 >= 10 = a__nats() 85.26/31.55 85.26/31.55 mark(zeros()) = 0 >= 0 = a__zeros() 85.26/31.55 85.26/31.55 mark(hd(X)) = X >= X = a__hd(mark(X)) 85.26/31.55 85.26/31.55 mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2) 85.26/31.55 85.26/31.55 mark(0()) = 8 >= 8 = 0() 85.26/31.55 85.26/31.55 mark(s(X)) = X >= X = s(X) 85.26/31.55 85.26/31.55 a__adx(X) = X + 5 >= X + 4 = adx(X) 85.26/31.55 85.26/31.55 a__incr(X) = X + 1 >= X + 1 = incr(X) 85.26/31.55 85.26/31.55 a__tl(X) = X >= X = tl(X) 85.26/31.55 problem: 85.26/31.55 strict: 85.26/31.55 a__zeros() -> cons(0(),zeros()) 85.26/31.55 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.55 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.55 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.55 a__hd(X) -> hd(X) 85.26/31.55 weak: 85.26/31.55 a__nats() -> a__adx(a__zeros()) 85.26/31.55 a__nats() -> nats() 85.26/31.55 a__zeros() -> zeros() 85.26/31.55 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.55 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.55 a__hd(cons(X,Y)) -> mark(X) 85.26/31.55 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.55 mark(nats()) -> a__nats() 85.26/31.55 mark(zeros()) -> a__zeros() 85.26/31.55 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.55 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.55 mark(0()) -> 0() 85.26/31.55 mark(s(X)) -> s(X) 85.26/31.55 a__adx(X) -> adx(X) 85.26/31.55 a__incr(X) -> incr(X) 85.26/31.55 a__tl(X) -> tl(X) 85.26/31.55 Matrix Interpretation Processor: dim=1 85.26/31.55 85.26/31.55 max_matrix: 85.26/31.55 1 85.26/31.55 interpretation: 85.26/31.55 [tl](x0) = x0 + 1, 85.26/31.55 85.26/31.55 [hd](x0) = x0 + 1, 85.26/31.55 85.26/31.55 [nats] = 9, 85.26/31.55 85.26/31.55 [a__tl](x0) = x0 + 1, 85.26/31.55 85.26/31.55 [mark](x0) = x0 + 4, 85.26/31.55 85.26/31.55 [a__hd](x0) = x0 + 1, 85.26/31.55 85.26/31.55 [adx](x0) = x0, 85.26/31.55 85.26/31.55 [incr](x0) = x0, 85.26/31.55 85.26/31.55 [s](x0) = x0, 85.26/31.55 85.26/31.55 [a__incr](x0) = x0, 85.26/31.55 85.26/31.55 [cons](x0, x1) = x0 + x1 + 3, 85.26/31.55 85.26/31.55 [zeros] = 5, 85.26/31.55 85.26/31.55 [0] = 0, 85.26/31.55 85.26/31.55 [a__adx](x0) = x0, 85.26/31.55 85.26/31.55 [a__zeros] = 9, 85.26/31.55 85.26/31.55 [a__nats] = 9 85.26/31.55 orientation: 85.26/31.55 a__zeros() = 9 >= 8 = cons(0(),zeros()) 85.26/31.55 85.26/31.55 mark(adx(X)) = X + 4 >= X + 4 = a__adx(mark(X)) 85.26/31.55 85.26/31.55 mark(incr(X)) = X + 4 >= X + 4 = a__incr(mark(X)) 85.26/31.55 85.26/31.55 mark(tl(X)) = X + 5 >= X + 5 = a__tl(mark(X)) 85.26/31.55 85.26/31.55 a__hd(X) = X + 1 >= X + 1 = hd(X) 85.26/31.55 85.26/31.55 a__nats() = 9 >= 9 = a__adx(a__zeros()) 85.26/31.55 85.26/31.55 a__nats() = 9 >= 9 = nats() 85.26/31.55 85.26/31.55 a__zeros() = 9 >= 5 = zeros() 85.26/31.55 85.26/31.55 a__adx(cons(X,Y)) = X + Y + 3 >= X + Y + 3 = a__incr(cons(X,adx(Y))) 85.26/31.55 85.26/31.55 a__incr(cons(X,Y)) = X + Y + 3 >= X + Y + 3 = cons(s(X),incr(Y)) 85.26/31.55 85.26/31.55 a__hd(cons(X,Y)) = X + Y + 4 >= X + 4 = mark(X) 85.26/31.55 85.26/31.55 a__tl(cons(X,Y)) = X + Y + 4 >= Y + 4 = mark(Y) 85.26/31.55 85.26/31.55 mark(nats()) = 13 >= 9 = a__nats() 85.26/31.55 85.26/31.55 mark(zeros()) = 9 >= 9 = a__zeros() 85.26/31.55 85.26/31.55 mark(hd(X)) = X + 5 >= X + 5 = a__hd(mark(X)) 85.26/31.55 85.26/31.55 mark(cons(X1,X2)) = X1 + X2 + 7 >= X1 + X2 + 3 = cons(X1,X2) 85.26/31.55 85.26/31.55 mark(0()) = 4 >= 0 = 0() 85.26/31.55 85.26/31.55 mark(s(X)) = X + 4 >= X = s(X) 85.26/31.55 85.26/31.55 a__adx(X) = X >= X = adx(X) 85.26/31.55 85.26/31.55 a__incr(X) = X >= X = incr(X) 85.26/31.55 85.26/31.55 a__tl(X) = X + 1 >= X + 1 = tl(X) 85.26/31.55 problem: 85.26/31.55 strict: 85.26/31.55 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.55 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.55 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.55 a__hd(X) -> hd(X) 85.26/31.55 weak: 85.26/31.55 a__zeros() -> cons(0(),zeros()) 85.26/31.55 a__nats() -> a__adx(a__zeros()) 85.26/31.55 a__nats() -> nats() 85.26/31.55 a__zeros() -> zeros() 85.26/31.55 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.55 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.55 a__hd(cons(X,Y)) -> mark(X) 85.26/31.55 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.55 mark(nats()) -> a__nats() 85.26/31.55 mark(zeros()) -> a__zeros() 85.26/31.55 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.55 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.55 mark(0()) -> 0() 85.26/31.55 mark(s(X)) -> s(X) 85.26/31.55 a__adx(X) -> adx(X) 85.26/31.55 a__incr(X) -> incr(X) 85.26/31.55 a__tl(X) -> tl(X) 85.26/31.55 Splitting Processor: 85.26/31.55 strict: 85.26/31.55 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.55 weak: 85.26/31.55 a__zeros() -> cons(0(),zeros()) 85.26/31.55 a__nats() -> a__adx(a__zeros()) 85.26/31.55 a__nats() -> nats() 85.26/31.55 a__zeros() -> zeros() 85.26/31.55 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.55 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.55 a__hd(cons(X,Y)) -> mark(X) 85.26/31.55 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.55 mark(nats()) -> a__nats() 85.26/31.55 mark(zeros()) -> a__zeros() 85.26/31.55 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.55 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.55 mark(0()) -> 0() 85.26/31.55 mark(s(X)) -> s(X) 85.26/31.55 a__adx(X) -> adx(X) 85.26/31.55 a__incr(X) -> incr(X) 85.26/31.55 a__tl(X) -> tl(X) 85.26/31.55 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.55 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.55 a__hd(X) -> hd(X) 85.26/31.55 Splitting Processor: 85.26/31.55 strict: 85.26/31.55 a__hd(X) -> hd(X) 85.26/31.55 weak: 85.26/31.55 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.55 a__zeros() -> cons(0(),zeros()) 85.26/31.55 a__nats() -> a__adx(a__zeros()) 85.26/31.55 a__nats() -> nats() 85.26/31.55 a__zeros() -> zeros() 85.26/31.55 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.55 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.55 a__hd(cons(X,Y)) -> mark(X) 85.26/31.55 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.55 mark(nats()) -> a__nats() 85.26/31.55 mark(zeros()) -> a__zeros() 85.26/31.55 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.55 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.55 mark(0()) -> 0() 85.26/31.55 mark(s(X)) -> s(X) 85.26/31.55 a__adx(X) -> adx(X) 85.26/31.55 a__incr(X) -> incr(X) 85.26/31.55 a__tl(X) -> tl(X) 85.26/31.55 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.55 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.55 Matrix Interpretation Processor: dim=3 85.26/31.55 85.26/31.55 max_matrix: 85.26/31.55 [1 0 1] 85.26/31.55 [0 0 1] 85.26/31.55 [0 0 1] 85.26/31.55 interpretation: 85.26/31.55 [1 0 1] 85.26/31.55 [tl](x0) = [0 0 0]x0 85.26/31.55 [0 0 1] , 85.26/31.55 85.26/31.55 [1 0 1] [0] 85.26/31.55 [hd](x0) = [0 0 1]x0 + [0] 85.26/31.55 [0 0 1] [1], 85.26/31.55 85.26/31.55 [0] 85.26/31.55 [nats] = [0] 85.26/31.55 [1], 85.26/31.55 85.26/31.55 [1 0 1] 85.26/31.55 [a__tl](x0) = [0 0 1]x0 85.26/31.55 [0 0 1] , 85.26/31.55 85.26/31.55 [1 0 1] 85.26/31.55 [mark](x0) = [0 0 1]x0 85.26/31.55 [0 0 1] , 85.26/31.55 85.26/31.55 [1 0 1] [1] 85.26/31.55 [a__hd](x0) = [0 0 1]x0 + [0] 85.26/31.55 [0 0 1] [1], 85.26/31.55 85.26/31.55 [1 0 0] 85.26/31.56 [adx](x0) = [0 0 0]x0 85.26/31.56 [0 0 1] , 85.26/31.56 85.26/31.56 [1 0 0] 85.26/31.56 [incr](x0) = [0 0 0]x0 85.26/31.56 [0 0 1] , 85.26/31.56 85.26/31.56 [1 0 0] 85.26/31.56 [s](x0) = [0 0 1]x0 85.26/31.56 [0 0 1] , 85.26/31.56 85.26/31.56 [1 0 0] 85.26/31.56 [a__incr](x0) = [0 0 0]x0 85.26/31.56 [0 0 1] , 85.26/31.56 85.26/31.56 [1 0 0] [1 0 1] 85.26/31.56 [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 85.26/31.56 [0 0 1] [0 0 1] , 85.26/31.56 85.26/31.56 [0] 85.26/31.56 [zeros] = [0] 85.26/31.56 [0], 85.26/31.56 85.26/31.56 [0] 85.26/31.56 [0] = [0] 85.26/31.56 [0], 85.26/31.56 85.26/31.56 [1 0 0] 85.26/31.56 [a__adx](x0) = [0 0 0]x0 85.26/31.56 [0 0 1] , 85.26/31.56 85.26/31.56 [0] 85.26/31.56 [a__zeros] = [0] 85.26/31.56 [0], 85.26/31.56 85.26/31.56 [0] 85.26/31.56 [a__nats] = [0] 85.26/31.56 [1] 85.26/31.56 orientation: 85.26/31.56 [1 0 1] [1] [1 0 1] [0] 85.26/31.56 a__hd(X) = [0 0 1]X + [0] >= [0 0 1]X + [0] = hd(X) 85.26/31.56 [0 0 1] [1] [0 0 1] [1] 85.26/31.56 85.26/31.56 [1 0 2] [1 0 2] 85.26/31.56 mark(tl(X)) = [0 0 1]X >= [0 0 1]X = a__tl(mark(X)) 85.26/31.56 [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [0] [0] 85.26/31.56 a__zeros() = [0] >= [0] = cons(0(),zeros()) 85.26/31.56 [0] [0] 85.26/31.56 85.26/31.56 [0] [0] 85.26/31.56 a__nats() = [0] >= [0] = a__adx(a__zeros()) 85.26/31.56 [1] [0] 85.26/31.56 85.26/31.56 [0] [0] 85.26/31.56 a__nats() = [0] >= [0] = nats() 85.26/31.56 [1] [1] 85.26/31.56 85.26/31.56 [0] [0] 85.26/31.56 a__zeros() = [0] >= [0] = zeros() 85.26/31.56 [0] [0] 85.26/31.56 85.26/31.56 [1 0 0] [1 0 1] [1 0 0] [1 0 1] 85.26/31.56 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))) 85.26/31.56 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [1 0 0] [1 0 1] [1 0 0] [1 0 1] 85.26/31.56 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)) 85.26/31.56 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [1 0 1] [1 0 2] [1] [1 0 1] 85.26/31.56 a__hd(cons(X,Y)) = [0 0 1]X + [0 0 1]Y + [0] >= [0 0 1]X = mark(X) 85.26/31.56 [0 0 1] [0 0 1] [1] [0 0 1] 85.26/31.56 85.26/31.56 [1 0 1] [1 0 2] [1 0 1] 85.26/31.56 a__tl(cons(X,Y)) = [0 0 1]X + [0 0 1]Y >= [0 0 1]Y = mark(Y) 85.26/31.56 [0 0 1] [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [1] [0] 85.26/31.56 mark(nats()) = [1] >= [0] = a__nats() 85.26/31.56 [1] [1] 85.26/31.56 85.26/31.56 [0] [0] 85.26/31.56 mark(zeros()) = [0] >= [0] = a__zeros() 85.26/31.56 [0] [0] 85.26/31.56 85.26/31.56 [1 0 2] [1] [1 0 2] [1] 85.26/31.56 mark(hd(X)) = [0 0 1]X + [1] >= [0 0 1]X + [0] = a__hd(mark(X)) 85.26/31.56 [0 0 1] [1] [0 0 1] [1] 85.26/31.56 85.26/31.56 [1 0 1] [1 0 2] [1 0 0] [1 0 1] 85.26/31.56 mark(cons(X1,X2)) = [0 0 1]X1 + [0 0 1]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2) 85.26/31.56 [0 0 1] [0 0 1] [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [0] [0] 85.26/31.56 mark(0()) = [0] >= [0] = 0() 85.26/31.56 [0] [0] 85.26/31.56 85.26/31.56 [1 0 1] [1 0 0] 85.26/31.56 mark(s(X)) = [0 0 1]X >= [0 0 1]X = s(X) 85.26/31.56 [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [1 0 0] [1 0 0] 85.26/31.56 a__adx(X) = [0 0 0]X >= [0 0 0]X = adx(X) 85.26/31.56 [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [1 0 0] [1 0 0] 85.26/31.56 a__incr(X) = [0 0 0]X >= [0 0 0]X = incr(X) 85.26/31.56 [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [1 0 1] [1 0 1] 85.26/31.56 a__tl(X) = [0 0 1]X >= [0 0 0]X = tl(X) 85.26/31.56 [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [1 0 1] [1 0 1] 85.26/31.56 mark(adx(X)) = [0 0 1]X >= [0 0 0]X = a__adx(mark(X)) 85.26/31.56 [0 0 1] [0 0 1] 85.26/31.56 85.26/31.56 [1 0 1] [1 0 1] 85.26/31.56 mark(incr(X)) = [0 0 1]X >= [0 0 0]X = a__incr(mark(X)) 85.26/31.56 [0 0 1] [0 0 1] 85.26/31.56 problem: 85.26/31.56 strict: 85.26/31.56 85.26/31.56 weak: 85.26/31.56 a__hd(X) -> hd(X) 85.26/31.56 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.56 a__zeros() -> cons(0(),zeros()) 85.26/31.56 a__nats() -> a__adx(a__zeros()) 85.26/31.56 a__nats() -> nats() 85.26/31.56 a__zeros() -> zeros() 85.26/31.56 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.56 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.56 a__hd(cons(X,Y)) -> mark(X) 85.26/31.56 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.56 mark(nats()) -> a__nats() 85.26/31.56 mark(zeros()) -> a__zeros() 85.26/31.56 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.56 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.56 mark(0()) -> 0() 85.26/31.56 mark(s(X)) -> s(X) 85.26/31.56 a__adx(X) -> adx(X) 85.26/31.56 a__incr(X) -> incr(X) 85.26/31.56 a__tl(X) -> tl(X) 85.26/31.56 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.56 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.56 Qed 85.26/31.56 85.26/31.56 strict: 85.26/31.56 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.56 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.56 weak: 85.26/31.56 a__hd(X) -> hd(X) 85.26/31.56 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.56 a__zeros() -> cons(0(),zeros()) 85.26/31.56 a__nats() -> a__adx(a__zeros()) 85.26/31.56 a__nats() -> nats() 85.26/31.56 a__zeros() -> zeros() 85.26/31.56 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.56 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.56 a__hd(cons(X,Y)) -> mark(X) 85.26/31.56 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.56 mark(nats()) -> a__nats() 85.26/31.56 mark(zeros()) -> a__zeros() 85.26/31.56 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.56 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.56 mark(0()) -> 0() 85.26/31.56 mark(s(X)) -> s(X) 85.26/31.56 a__adx(X) -> adx(X) 85.26/31.56 a__incr(X) -> incr(X) 85.26/31.56 a__tl(X) -> tl(X) 85.26/31.56 Splitting Processor: 85.26/31.56 strict: 85.26/31.56 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.56 weak: 85.26/31.56 a__hd(X) -> hd(X) 85.26/31.56 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.56 a__zeros() -> cons(0(),zeros()) 85.26/31.56 a__nats() -> a__adx(a__zeros()) 85.26/31.56 a__nats() -> nats() 85.26/31.56 a__zeros() -> zeros() 85.26/31.56 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.56 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.56 a__hd(cons(X,Y)) -> mark(X) 85.26/31.56 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.56 mark(nats()) -> a__nats() 85.26/31.56 mark(zeros()) -> a__zeros() 85.26/31.56 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.56 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.56 mark(0()) -> 0() 85.26/31.56 mark(s(X)) -> s(X) 85.26/31.56 a__adx(X) -> adx(X) 85.26/31.56 a__incr(X) -> incr(X) 85.26/31.56 a__tl(X) -> tl(X) 85.26/31.56 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.56 Matrix Interpretation Processor: dim=4 85.26/31.56 85.26/31.56 max_matrix: 85.26/31.56 [1 1 1 1] 85.26/31.56 [0 0 0 0] 85.26/31.56 [0 0 1 1] 85.26/31.56 [0 0 0 1] 85.26/31.56 interpretation: 85.26/31.56 [1 0 1 0] [0] 85.26/31.56 [0 0 0 0] [0] 85.26/31.56 [tl](x0) = [0 0 1 1]x0 + [1] 85.26/31.56 [0 0 0 1] [0], 85.26/31.56 85.26/31.56 [1 0 1 1] [1] 85.26/31.56 [0 0 0 0] [0] 85.26/31.56 [hd](x0) = [0 0 1 1]x0 + [1] 85.26/31.56 [0 0 0 1] [0], 85.26/31.56 85.26/31.56 [0] 85.26/31.56 [0] 85.26/31.56 [nats] = [0] 85.26/31.56 [1], 85.26/31.56 85.26/31.56 [1 1 1 0] [0] 85.26/31.56 [0 0 0 0] [0] 85.26/31.56 [a__tl](x0) = [0 0 1 1]x0 + [1] 85.26/31.56 [0 0 0 1] [0], 85.26/31.56 85.26/31.56 [1 0 1 1] 85.26/31.56 [0 0 0 0] 85.26/31.56 [mark](x0) = [0 0 1 1]x0 85.26/31.56 [0 0 0 1] , 85.26/31.56 85.26/31.56 [1 0 1 1] [1] 85.26/31.56 [0 0 0 0] [0] 85.26/31.56 [a__hd](x0) = [0 0 1 1]x0 + [1] 85.26/31.56 [0 0 0 1] [0], 85.26/31.56 85.26/31.56 [1 0 0 0] [0] 85.26/31.56 [0 0 0 0] [0] 85.26/31.56 [adx](x0) = [0 0 1 0]x0 + [0] 85.26/31.56 [0 0 0 1] [1], 85.26/31.56 85.26/31.56 [1 0 0 0] [0] 85.26/31.56 [0 0 0 0] [0] 85.26/31.56 [incr](x0) = [0 0 1 0]x0 + [1] 85.26/31.56 [0 0 0 1] [0], 85.26/31.56 85.26/31.56 [1 0 0 0] 85.26/31.56 [0 0 0 0] 85.26/31.56 [s](x0) = [0 0 1 0]x0 85.26/31.56 [0 0 0 0] , 85.26/31.56 85.26/31.56 [1 0 0 0] [0] 85.26/31.56 [0 0 0 0] [0] 85.26/31.56 [a__incr](x0) = [0 0 1 0]x0 + [1] 85.26/31.56 [0 0 0 1] [0], 85.26/31.56 85.26/31.56 [1 0 0 0] [1 1 0 1] 85.26/31.56 [0 0 0 0] [0 0 0 0] 85.26/31.56 [cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 85.26/31.56 [0 0 0 1] [0 0 0 1] , 85.26/31.56 85.26/31.56 [0] 85.26/31.56 [0] 85.26/31.56 [zeros] = [0] 85.26/31.56 [0], 85.26/31.56 85.26/31.56 [0] 85.26/31.56 [0] 85.26/31.56 [0] = [0] 85.26/31.56 [0], 85.26/31.56 85.26/31.56 [1 0 0 0] [1] 85.26/31.56 [0 0 0 0] [0] 85.26/31.56 [a__adx](x0) = [0 0 1 0]x0 + [1] 85.26/31.56 [0 0 0 1] [1], 85.26/31.56 85.26/31.56 [0] 85.26/31.56 [0] 85.26/31.56 [a__zeros] = [0] 85.26/31.56 [0], 85.26/31.56 85.26/31.56 [1] 85.26/31.56 [0] 85.26/31.56 [a__nats] = [1] 85.26/31.56 [1] 85.26/31.56 orientation: 85.26/31.56 [1 0 1 1] [1] [1 0 1 1] [0] 85.26/31.56 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.56 mark(incr(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = a__incr(mark(X)) 85.26/31.56 [0 0 0 1] [0] [0 0 0 1] [0] 85.26/31.56 85.26/31.56 [1 0 1 1] [1] [1 0 1 1] [1] 85.26/31.56 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.56 mark(adx(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = a__adx(mark(X)) 85.26/31.56 [0 0 0 1] [1] [0 0 0 1] [1] 85.26/31.56 85.26/31.56 [1 0 1 1] [1] [1 0 1 1] [1] 85.26/31.56 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.56 a__hd(X) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = hd(X) 85.26/31.56 [0 0 0 1] [0] [0 0 0 1] [0] 85.26/31.56 85.26/31.56 [1 0 2 2] [1] [1 0 2 2] [0] 85.26/31.56 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.56 mark(tl(X)) = [0 0 1 2]X + [1] >= [0 0 1 2]X + [1] = a__tl(mark(X)) 85.26/31.56 [0 0 0 1] [0] [0 0 0 1] [0] 85.26/31.56 85.26/31.56 [0] [0] 85.26/31.56 [0] [0] 85.26/31.56 a__zeros() = [0] >= [0] = cons(0(),zeros()) 85.26/31.56 [0] [0] 85.26/31.56 85.26/31.56 [1] [1] 85.26/31.57 [0] [0] 85.26/31.57 a__nats() = [1] >= [1] = a__adx(a__zeros()) 85.26/31.57 [1] [1] 85.26/31.57 85.26/31.57 [1] [0] 85.26/31.57 [0] [0] 85.26/31.57 a__nats() = [1] >= [0] = nats() 85.26/31.57 [1] [1] 85.26/31.57 85.26/31.57 [0] [0] 85.26/31.57 [0] [0] 85.26/31.57 a__zeros() = [0] >= [0] = zeros() 85.26/31.57 [0] [0] 85.26/31.57 85.26/31.57 [1 0 0 0] [1 1 0 1] [1] [1 0 0 0] [1 0 0 1] [1] 85.26/31.57 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 85.26/31.57 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))) 85.26/31.57 [0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1] 85.26/31.57 85.26/31.57 [1 0 0 0] [1 1 0 1] [0] [1 0 0 0] [1 0 0 1] [0] 85.26/31.57 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 85.26/31.57 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)) 85.26/31.57 [0 0 0 1] [0 0 0 1] [0] [0 0 0 0] [0 0 0 1] [0] 85.26/31.57 85.26/31.57 [1 0 1 1] [1 1 1 2] [1] [1 0 1 1] 85.26/31.57 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 85.26/31.57 a__hd(cons(X,Y)) = [0 0 1 1]X + [0 0 1 1]Y + [1] >= [0 0 1 1]X = mark(X) 85.26/31.57 [0 0 0 1] [0 0 0 1] [0] [0 0 0 1] 85.26/31.57 85.26/31.57 [1 0 1 0] [1 1 1 1] [0] [1 0 1 1] 85.26/31.57 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] 85.26/31.57 a__tl(cons(X,Y)) = [0 0 1 1]X + [0 0 1 1]Y + [1] >= [0 0 1 1]Y = mark(Y) 85.26/31.57 [0 0 0 1] [0 0 0 1] [0] [0 0 0 1] 85.26/31.57 85.26/31.57 [1] [1] 85.26/31.57 [0] [0] 85.26/31.57 mark(nats()) = [1] >= [1] = a__nats() 85.26/31.57 [1] [1] 85.26/31.57 85.26/31.57 [0] [0] 85.26/31.57 [0] [0] 85.26/31.57 mark(zeros()) = [0] >= [0] = a__zeros() 85.26/31.57 [0] [0] 85.26/31.57 85.26/31.57 [1 0 2 3] [2] [1 0 2 3] [1] 85.26/31.57 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.57 mark(hd(X)) = [0 0 1 2]X + [1] >= [0 0 1 2]X + [1] = a__hd(mark(X)) 85.26/31.57 [0 0 0 1] [0] [0 0 0 1] [0] 85.26/31.57 85.26/31.57 [1 0 1 1] [1 1 1 2] [1 0 0 0] [1 1 0 1] 85.26/31.57 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 85.26/31.57 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) 85.26/31.57 [0 0 0 1] [0 0 0 1] [0 0 0 1] [0 0 0 1] 85.26/31.57 85.26/31.57 [0] [0] 85.26/31.57 [0] [0] 85.26/31.57 mark(0()) = [0] >= [0] = 0() 85.26/31.57 [0] [0] 85.26/31.57 85.26/31.57 [1 0 1 0] [1 0 0 0] 85.26/31.57 [0 0 0 0] [0 0 0 0] 85.26/31.57 mark(s(X)) = [0 0 1 0]X >= [0 0 1 0]X = s(X) 85.26/31.57 [0 0 0 0] [0 0 0 0] 85.26/31.57 85.26/31.57 [1 0 0 0] [1] [1 0 0 0] [0] 85.26/31.57 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.57 a__adx(X) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [0] = adx(X) 85.26/31.57 [0 0 0 1] [1] [0 0 0 1] [1] 85.26/31.57 85.26/31.57 [1 0 0 0] [0] [1 0 0 0] [0] 85.26/31.57 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.57 a__incr(X) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = incr(X) 85.26/31.57 [0 0 0 1] [0] [0 0 0 1] [0] 85.26/31.57 85.26/31.57 [1 1 1 0] [0] [1 0 1 0] [0] 85.26/31.57 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.57 a__tl(X) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = tl(X) 85.26/31.57 [0 0 0 1] [0] [0 0 0 1] [0] 85.26/31.57 problem: 85.26/31.57 strict: 85.26/31.57 85.26/31.57 weak: 85.26/31.57 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.57 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.57 a__hd(X) -> hd(X) 85.26/31.57 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.57 a__zeros() -> cons(0(),zeros()) 85.26/31.57 a__nats() -> a__adx(a__zeros()) 85.26/31.57 a__nats() -> nats() 85.26/31.57 a__zeros() -> zeros() 85.26/31.57 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.57 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.57 a__hd(cons(X,Y)) -> mark(X) 85.26/31.57 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.57 mark(nats()) -> a__nats() 85.26/31.57 mark(zeros()) -> a__zeros() 85.26/31.57 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.57 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.57 mark(0()) -> 0() 85.26/31.57 mark(s(X)) -> s(X) 85.26/31.57 a__adx(X) -> adx(X) 85.26/31.57 a__incr(X) -> incr(X) 85.26/31.57 a__tl(X) -> tl(X) 85.26/31.57 Qed 85.26/31.57 85.26/31.57 strict: 85.26/31.57 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.57 weak: 85.26/31.57 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.57 a__hd(X) -> hd(X) 85.26/31.57 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.57 a__zeros() -> cons(0(),zeros()) 85.26/31.57 a__nats() -> a__adx(a__zeros()) 85.26/31.57 a__nats() -> nats() 85.26/31.57 a__zeros() -> zeros() 85.26/31.57 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.57 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.57 a__hd(cons(X,Y)) -> mark(X) 85.26/31.57 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.57 mark(nats()) -> a__nats() 85.26/31.57 mark(zeros()) -> a__zeros() 85.26/31.57 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.57 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.57 mark(0()) -> 0() 85.26/31.57 mark(s(X)) -> s(X) 85.26/31.57 a__adx(X) -> adx(X) 85.26/31.57 a__incr(X) -> incr(X) 85.26/31.57 a__tl(X) -> tl(X) 85.26/31.57 Matrix Interpretation Processor: dim=4 85.26/31.57 85.26/31.57 max_matrix: 85.26/31.57 [1 1 1 1] 85.26/31.57 [0 0 0 1] 85.26/31.57 [0 0 1 1] 85.26/31.57 [0 0 0 0] 85.26/31.57 interpretation: 85.26/31.57 [1 0 1 0] [1] 85.26/31.57 [0 0 0 0] [0] 85.26/31.57 [tl](x0) = [0 0 1 0]x0 + [1] 85.26/31.57 [0 0 0 0] [0], 85.26/31.57 85.26/31.57 [1 0 0 0] [1] 85.26/31.57 [0 0 0 0] [0] 85.26/31.57 [hd](x0) = [0 0 1 1]x0 + [1] 85.26/31.57 [0 0 0 0] [0], 85.26/31.57 85.26/31.57 [0] 85.26/31.57 [0] 85.26/31.57 [nats] = [0] 85.26/31.57 [0], 85.26/31.57 85.26/31.57 [1 1 1 0] [1] 85.26/31.57 [0 0 0 1] [0] 85.26/31.57 [a__tl](x0) = [0 0 1 0]x0 + [1] 85.26/31.57 [0 0 0 0] [0], 85.26/31.57 85.26/31.57 [1 0 1 0] [1] 85.26/31.57 [0 0 0 0] [0] 85.26/31.57 [mark](x0) = [0 0 1 0]x0 + [1] 85.26/31.57 [0 0 0 0] [0], 85.26/31.57 85.26/31.57 [1 0 0 0] [1] 85.26/31.57 [0 0 0 0] [0] 85.26/31.57 [a__hd](x0) = [0 0 1 1]x0 + [1] 85.26/31.57 [0 0 0 0] [0], 85.26/31.57 85.26/31.57 [1 0 0 1] [0] 85.26/31.57 [0 0 0 0] [0] 85.26/31.57 [adx](x0) = [0 0 1 0]x0 + [1] 85.26/31.57 [0 0 0 0] [0], 85.26/31.57 85.26/31.57 [1 0 0 0] 85.26/31.57 [0 0 0 0] 85.26/31.57 [incr](x0) = [0 0 1 0]x0 85.26/31.57 [0 0 0 0] , 85.26/31.57 85.26/31.57 [1 1 0 0] 85.26/31.57 [0 0 0 0] 85.26/31.57 [s](x0) = [0 0 0 0]x0 85.26/31.58 [0 0 0 0] , 85.26/31.58 85.26/31.58 [1 0 0 0] 85.26/31.58 [0 0 0 1] 85.26/31.58 [a__incr](x0) = [0 0 1 0]x0 85.26/31.58 [0 0 0 0] , 85.26/31.58 85.26/31.58 [1 1 1 0] [1 0 0 1] 85.26/31.58 [0 0 0 0] [0 0 0 0] 85.26/31.58 [cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 85.26/31.58 [0 0 0 0] [0 0 0 0] , 85.26/31.58 85.26/31.58 [0] 85.26/31.58 [0] 85.26/31.58 [zeros] = [0] 85.26/31.58 [0], 85.26/31.58 85.26/31.58 [1] 85.26/31.58 [0] 85.26/31.58 [0] = [0] 85.26/31.58 [0], 85.26/31.58 85.26/31.58 [1 0 0 1] [0] 85.26/31.58 [0 0 0 0] [0] 85.26/31.58 [a__adx](x0) = [0 0 1 0]x0 + [1] 85.26/31.58 [0 0 0 0] [0], 85.26/31.58 85.26/31.58 [1] 85.26/31.58 [0] 85.26/31.58 [a__zeros] = [0] 85.26/31.58 [0], 85.26/31.58 85.26/31.58 [1] 85.26/31.58 [0] 85.26/31.58 [a__nats] = [1] 85.26/31.58 [0] 85.26/31.58 orientation: 85.26/31.58 [1 0 1 1] [2] [1 0 1 0] [1] 85.26/31.58 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.58 mark(adx(X)) = [0 0 1 0]X + [2] >= [0 0 1 0]X + [2] = a__adx(mark(X)) 85.26/31.58 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.58 85.26/31.58 [1 0 0 0] [1] [1 0 0 0] [1] 85.26/31.58 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.58 a__hd(X) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = hd(X) 85.26/31.58 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.58 85.26/31.58 [1 0 2 0] [3] [1 0 2 0] [3] 85.26/31.58 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.58 mark(tl(X)) = [0 0 1 0]X + [2] >= [0 0 1 0]X + [2] = a__tl(mark(X)) 85.26/31.58 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.58 85.26/31.58 [1] [1] 85.26/31.58 [0] [0] 85.26/31.58 a__zeros() = [0] >= [0] = cons(0(),zeros()) 85.26/31.58 [0] [0] 85.26/31.58 85.26/31.58 [1] [1] 85.26/31.58 [0] [0] 85.26/31.58 a__nats() = [1] >= [1] = a__adx(a__zeros()) 85.26/31.58 [0] [0] 85.26/31.58 85.26/31.58 [1] [0] 85.26/31.58 [0] [0] 85.26/31.58 a__nats() = [1] >= [0] = nats() 85.26/31.58 [0] [0] 85.26/31.58 85.26/31.58 [1] [0] 85.26/31.58 [0] [0] 85.26/31.58 a__zeros() = [0] >= [0] = zeros() 85.26/31.58 [0] [0] 85.26/31.58 85.26/31.58 [1 1 1 0] [1 0 0 1] [0] [1 1 1 0] [1 0 0 1] [0] 85.26/31.58 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 85.26/31.58 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))) 85.26/31.58 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] 85.26/31.58 85.26/31.58 [1 1 1 0] [1 0 0 1] [1 1 0 0] [1 0 0 0] 85.26/31.58 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 85.26/31.58 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)) 85.26/31.58 [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] 85.26/31.58 85.26/31.58 [1 1 1 0] [1 0 0 1] [1] [1 0 1 0] [1] 85.26/31.58 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.58 a__hd(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y + [1] >= [0 0 1 0]X + [1] = mark(X) 85.26/31.59 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 85.26/31.59 [1 1 2 0] [1 0 1 1] [1] [1 0 1 0] [1] 85.26/31.59 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 a__tl(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y + [1] >= [0 0 1 0]Y + [1] = mark(Y) 85.26/31.59 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 85.26/31.59 [1] [1] 85.26/31.59 [0] [0] 85.26/31.59 mark(nats()) = [1] >= [1] = a__nats() 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1] [1] 85.26/31.59 [0] [0] 85.26/31.59 mark(zeros()) = [1] >= [0] = a__zeros() 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1 0 1 1] [3] [1 0 1 0] [2] 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 mark(hd(X)) = [0 0 1 1]X + [2] >= [0 0 1 0]X + [2] = a__hd(mark(X)) 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 85.26/31.59 [1 1 2 0] [1 0 1 1] [1] [1 1 1 0] [1 0 0 1] 85.26/31.59 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] 85.26/31.59 mark(cons(X1,X2)) = [0 0 1 0]X1 + [0 0 1 0]X2 + [1] >= [0 0 1 0]X1 + [0 0 1 0]X2 = cons(X1,X2) 85.26/31.59 [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] 85.26/31.59 85.26/31.59 [2] [1] 85.26/31.59 [0] [0] 85.26/31.59 mark(0()) = [1] >= [0] = 0() 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1 1 0 0] [1] [1 1 0 0] 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] 85.26/31.59 mark(s(X)) = [0 0 0 0]X + [1] >= [0 0 0 0]X = s(X) 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] 85.26/31.59 85.26/31.59 [1 0 0 1] [0] [1 0 0 1] [0] 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 a__adx(X) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = adx(X) 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 85.26/31.59 [1 0 0 0] [1 0 0 0] 85.26/31.59 [0 0 0 1] [0 0 0 0] 85.26/31.59 a__incr(X) = [0 0 1 0]X >= [0 0 1 0]X = incr(X) 85.26/31.59 [0 0 0 0] [0 0 0 0] 85.26/31.59 85.26/31.59 [1 1 1 0] [1] [1 0 1 0] [1] 85.26/31.59 [0 0 0 1] [0] [0 0 0 0] [0] 85.26/31.59 a__tl(X) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = tl(X) 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 85.26/31.59 [1 0 1 0] [1] [1 0 1 0] [1] 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 mark(incr(X)) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = a__incr(mark(X)) 85.26/31.59 [0 0 0 0] [0] [0 0 0 0] [0] 85.26/31.59 problem: 85.26/31.59 strict: 85.26/31.59 85.26/31.59 weak: 85.26/31.59 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.59 a__hd(X) -> hd(X) 85.26/31.59 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.59 a__zeros() -> cons(0(),zeros()) 85.26/31.59 a__nats() -> a__adx(a__zeros()) 85.26/31.59 a__nats() -> nats() 85.26/31.59 a__zeros() -> zeros() 85.26/31.59 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.59 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.59 a__hd(cons(X,Y)) -> mark(X) 85.26/31.59 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.59 mark(nats()) -> a__nats() 85.26/31.59 mark(zeros()) -> a__zeros() 85.26/31.59 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.59 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.59 mark(0()) -> 0() 85.26/31.59 mark(s(X)) -> s(X) 85.26/31.59 a__adx(X) -> adx(X) 85.26/31.59 a__incr(X) -> incr(X) 85.26/31.59 a__tl(X) -> tl(X) 85.26/31.59 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.59 Qed 85.26/31.59 85.26/31.59 strict: 85.26/31.59 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.59 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.59 a__hd(X) -> hd(X) 85.26/31.59 weak: 85.26/31.59 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.59 a__zeros() -> cons(0(),zeros()) 85.26/31.59 a__nats() -> a__adx(a__zeros()) 85.26/31.59 a__nats() -> nats() 85.26/31.59 a__zeros() -> zeros() 85.26/31.59 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.59 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.59 a__hd(cons(X,Y)) -> mark(X) 85.26/31.59 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.59 mark(nats()) -> a__nats() 85.26/31.59 mark(zeros()) -> a__zeros() 85.26/31.59 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.59 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.59 mark(0()) -> 0() 85.26/31.59 mark(s(X)) -> s(X) 85.26/31.59 a__adx(X) -> adx(X) 85.26/31.59 a__incr(X) -> incr(X) 85.26/31.59 a__tl(X) -> tl(X) 85.26/31.59 Matrix Interpretation Processor: dim=3 85.26/31.59 85.26/31.59 max_matrix: 85.26/31.59 [1 1 1] 85.26/31.59 [0 1 1] 85.26/31.59 [0 0 0] 85.26/31.59 interpretation: 85.26/31.59 [1 0 0] [0] 85.26/31.59 [tl](x0) = [0 1 0]x0 + [1] 85.26/31.59 [0 0 0] [0], 85.26/31.59 85.26/31.59 [1 1 0] 85.26/31.59 [hd](x0) = [0 1 0]x0 85.26/31.59 [0 0 0] , 85.26/31.59 85.26/31.59 [0] 85.26/31.59 [nats] = [1] 85.26/31.59 [0], 85.26/31.59 85.26/31.59 [1 0 0] [0] 85.26/31.59 [a__tl](x0) = [0 1 0]x0 + [1] 85.26/31.59 [0 0 0] [0], 85.26/31.59 85.26/31.59 [1 1 0] 85.26/31.59 [mark](x0) = [0 1 0]x0 85.26/31.59 [0 0 0] , 85.26/31.59 85.26/31.59 [1 1 0] 85.26/31.59 [a__hd](x0) = [0 1 1]x0 85.26/31.59 [0 0 0] , 85.26/31.59 85.26/31.59 [1 0 1] 85.26/31.59 [adx](x0) = [0 1 0]x0 85.26/31.59 [0 0 0] , 85.26/31.59 85.26/31.59 [1 0 0] 85.26/31.59 [incr](x0) = [0 1 0]x0 85.26/31.59 [0 0 0] , 85.26/31.59 85.26/31.59 [1 1 0] 85.26/31.59 [s](x0) = [0 0 1]x0 85.26/31.59 [0 0 0] , 85.26/31.59 85.26/31.59 [1 0 0] 85.26/31.59 [a__incr](x0) = [0 1 0]x0 85.26/31.59 [0 0 0] , 85.26/31.59 85.26/31.59 [1 1 1] [1 1 1] 85.26/31.59 [cons](x0, x1) = [0 1 1]x0 + [0 1 0]x1 85.26/31.59 [0 0 0] [0 0 0] , 85.26/31.59 85.26/31.59 [0] 85.26/31.59 [zeros] = [1] 85.26/31.59 [0], 85.26/31.59 85.26/31.59 [0] 85.26/31.59 [0] = [0] 85.26/31.59 [0], 85.26/31.59 85.26/31.59 [1 0 1] 85.26/31.59 [a__adx](x0) = [0 1 0]x0 85.26/31.59 [0 0 0] , 85.26/31.59 85.26/31.59 [1] 85.26/31.59 [a__zeros] = [1] 85.26/31.59 [0], 85.26/31.59 85.26/31.59 [1] 85.26/31.59 [a__nats] = [1] 85.26/31.59 [0] 85.26/31.59 orientation: 85.26/31.59 [1 1 0] [1] [1 1 0] [0] 85.26/31.59 mark(tl(X)) = [0 1 0]X + [1] >= [0 1 0]X + [1] = a__tl(mark(X)) 85.26/31.59 [0 0 0] [0] [0 0 0] [0] 85.26/31.59 85.26/31.59 [1] [1] 85.26/31.59 a__zeros() = [1] >= [1] = cons(0(),zeros()) 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1] [1] 85.26/31.59 a__nats() = [1] >= [1] = a__adx(a__zeros()) 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1] [0] 85.26/31.59 a__nats() = [1] >= [1] = nats() 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1] [0] 85.26/31.59 a__zeros() = [1] >= [1] = zeros() 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1 1 1] [1 1 1] [1 1 1] [1 1 1] 85.26/31.59 a__adx(cons(X,Y)) = [0 1 1]X + [0 1 0]Y >= [0 1 1]X + [0 1 0]Y = a__incr(cons(X,adx(Y))) 85.26/31.59 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 1 1] [1 1 1] [1 1 1] [1 1 0] 85.26/31.59 a__incr(cons(X,Y)) = [0 1 1]X + [0 1 0]Y >= [0 0 1]X + [0 1 0]Y = cons(s(X),incr(Y)) 85.26/31.59 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 2 2] [1 2 1] [1 1 0] 85.26/31.59 a__hd(cons(X,Y)) = [0 1 1]X + [0 1 0]Y >= [0 1 0]X = mark(X) 85.26/31.59 [0 0 0] [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 1 1] [1 1 1] [0] [1 1 0] 85.26/31.59 a__tl(cons(X,Y)) = [0 1 1]X + [0 1 0]Y + [1] >= [0 1 0]Y = mark(Y) 85.26/31.59 [0 0 0] [0 0 0] [0] [0 0 0] 85.26/31.59 85.26/31.59 [1] [1] 85.26/31.59 mark(nats()) = [1] >= [1] = a__nats() 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1] [1] 85.26/31.59 mark(zeros()) = [1] >= [1] = a__zeros() 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1 2 0] [1 2 0] 85.26/31.59 mark(hd(X)) = [0 1 0]X >= [0 1 0]X = a__hd(mark(X)) 85.26/31.59 [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 2 2] [1 2 1] [1 1 1] [1 1 1] 85.26/31.59 mark(cons(X1,X2)) = [0 1 1]X1 + [0 1 0]X2 >= [0 1 1]X1 + [0 1 0]X2 = cons(X1,X2) 85.26/31.59 [0 0 0] [0 0 0] [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [0] [0] 85.26/31.59 mark(0()) = [0] >= [0] = 0() 85.26/31.59 [0] [0] 85.26/31.59 85.26/31.59 [1 1 1] [1 1 0] 85.26/31.59 mark(s(X)) = [0 0 1]X >= [0 0 1]X = s(X) 85.26/31.59 [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 0 1] [1 0 1] 85.26/31.59 a__adx(X) = [0 1 0]X >= [0 1 0]X = adx(X) 85.26/31.59 [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 0 0] [1 0 0] 85.26/31.59 a__incr(X) = [0 1 0]X >= [0 1 0]X = incr(X) 85.26/31.59 [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 0 0] [0] [1 0 0] [0] 85.26/31.59 a__tl(X) = [0 1 0]X + [1] >= [0 1 0]X + [1] = tl(X) 85.26/31.59 [0 0 0] [0] [0 0 0] [0] 85.26/31.59 85.26/31.59 [1 1 1] [1 1 0] 85.26/31.59 mark(adx(X)) = [0 1 0]X >= [0 1 0]X = a__adx(mark(X)) 85.26/31.59 [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 1 0] [1 1 0] 85.26/31.59 mark(incr(X)) = [0 1 0]X >= [0 1 0]X = a__incr(mark(X)) 85.26/31.59 [0 0 0] [0 0 0] 85.26/31.59 85.26/31.59 [1 1 0] [1 1 0] 85.26/31.59 a__hd(X) = [0 1 1]X >= [0 1 0]X = hd(X) 85.26/31.59 [0 0 0] [0 0 0] 85.26/31.59 problem: 85.26/31.59 strict: 85.26/31.59 85.26/31.59 weak: 85.26/31.59 mark(tl(X)) -> a__tl(mark(X)) 85.26/31.59 a__zeros() -> cons(0(),zeros()) 85.26/31.59 a__nats() -> a__adx(a__zeros()) 85.26/31.59 a__nats() -> nats() 85.26/31.59 a__zeros() -> zeros() 85.26/31.59 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y))) 85.26/31.59 a__incr(cons(X,Y)) -> cons(s(X),incr(Y)) 85.26/31.59 a__hd(cons(X,Y)) -> mark(X) 85.26/31.59 a__tl(cons(X,Y)) -> mark(Y) 85.26/31.59 mark(nats()) -> a__nats() 85.26/31.59 mark(zeros()) -> a__zeros() 85.26/31.59 mark(hd(X)) -> a__hd(mark(X)) 85.26/31.59 mark(cons(X1,X2)) -> cons(X1,X2) 85.26/31.59 mark(0()) -> 0() 85.26/31.59 mark(s(X)) -> s(X) 85.26/31.59 a__adx(X) -> adx(X) 85.26/31.59 a__incr(X) -> incr(X) 85.26/31.59 a__tl(X) -> tl(X) 85.26/31.59 mark(adx(X)) -> a__adx(mark(X)) 85.26/31.59 mark(incr(X)) -> a__incr(mark(X)) 85.26/31.59 a__hd(X) -> hd(X) 85.26/31.59 Qed 85.36/31.60 EOF