YES(?,O(n^2)) 64.87/27.92 YES(?,O(n^2)) 64.87/27.93 64.87/27.93 Problem: 64.87/27.93 a__f(X,X) -> a__f(a(),b()) 64.87/27.93 a__b() -> a() 64.87/27.93 mark(f(X1,X2)) -> a__f(mark(X1),X2) 64.87/27.93 mark(b()) -> a__b() 64.87/27.93 mark(a()) -> a() 64.87/27.93 a__f(X1,X2) -> f(X1,X2) 64.87/27.93 a__b() -> b() 64.87/27.93 64.87/27.93 Proof: 64.87/27.93 Complexity Transformation Processor: 64.87/27.93 strict: 64.87/27.93 a__f(X,X) -> a__f(a(),b()) 64.87/27.93 a__b() -> a() 64.87/27.93 mark(f(X1,X2)) -> a__f(mark(X1),X2) 64.87/27.93 mark(b()) -> a__b() 64.87/27.93 mark(a()) -> a() 64.87/27.93 a__f(X1,X2) -> f(X1,X2) 64.87/27.93 a__b() -> b() 64.87/27.93 weak: 64.87/27.93 64.87/27.93 Matrix Interpretation Processor: dim=1 64.87/27.93 64.87/27.93 max_matrix: 64.87/27.93 1 64.87/27.93 interpretation: 64.87/27.93 [mark](x0) = x0 + 4, 64.87/27.93 64.87/27.93 [f](x0, x1) = x0 + x1 + 130, 64.87/27.93 64.87/27.93 [a__b] = 1, 64.87/27.93 64.87/27.93 [b] = 0, 64.87/27.93 64.87/27.93 [a] = 0, 64.87/27.93 64.87/27.93 [a__f](x0, x1) = x0 + x1 + 254 64.87/27.93 orientation: 64.87/27.93 a__f(X,X) = 2X + 254 >= 254 = a__f(a(),b()) 64.87/27.93 64.87/27.93 a__b() = 1 >= 0 = a() 64.87/27.93 64.87/27.93 mark(f(X1,X2)) = X1 + X2 + 134 >= X1 + X2 + 258 = a__f(mark(X1),X2) 64.87/27.93 64.87/27.93 mark(b()) = 4 >= 1 = a__b() 64.87/27.93 64.87/27.93 mark(a()) = 4 >= 0 = a() 64.87/27.93 64.87/27.93 a__f(X1,X2) = X1 + X2 + 254 >= X1 + X2 + 130 = f(X1,X2) 64.87/27.93 64.87/27.93 a__b() = 1 >= 0 = b() 64.87/27.93 problem: 64.87/27.93 strict: 64.87/27.93 a__f(X,X) -> a__f(a(),b()) 64.87/27.93 mark(f(X1,X2)) -> a__f(mark(X1),X2) 64.87/27.93 weak: 64.87/27.93 a__b() -> a() 64.87/27.93 mark(b()) -> a__b() 64.87/27.93 mark(a()) -> a() 64.87/27.93 a__f(X1,X2) -> f(X1,X2) 64.87/27.93 a__b() -> b() 64.87/27.93 Splitting Processor: 64.87/27.93 strict: 64.87/27.93 mark(f(X1,X2)) -> a__f(mark(X1),X2) 64.87/27.93 weak: 64.87/27.93 a__b() -> a() 64.87/27.93 mark(b()) -> a__b() 64.87/27.93 mark(a()) -> a() 64.87/27.93 a__f(X1,X2) -> f(X1,X2) 64.87/27.93 a__b() -> b() 64.87/27.93 a__f(X,X) -> a__f(a(),b()) 64.87/27.93 Bounds Processor: 64.87/27.93 bound: 1 64.87/27.93 enrichment: match 64.87/27.93 automaton: 64.87/27.93 final states: {28,24,23,22,17,16,14,13,6,5,4} 64.87/27.93 transitions: 64.87/27.93 a__f0(22,16) -> 4* 64.87/27.93 a__f0(17,16) -> 5* 64.87/27.93 a__f0(28,1) -> 17*,4,5 64.87/27.93 a__f0(2,16) -> 4* 64.87/27.93 a__f0(23,1) -> 4* 64.87/27.93 a__f0(28,3) -> 17*,4,5 64.87/27.93 a__f0(22,22) -> 4* 64.87/27.93 a__f0(23,3) -> 4* 64.87/27.93 a__f0(13,1) -> 4* 64.87/27.93 a__f0(17,22) -> 5* 64.87/27.93 a__f0(22,24) -> 4* 64.87/27.93 a__f0(13,3) -> 4* 64.87/27.93 a__f0(3,1) -> 4* 64.87/27.93 a__f0(17,24) -> 5* 64.87/27.93 a__f0(2,22) -> 4* 64.87/27.93 a__f0(3,3) -> 4* 64.87/27.93 a__f0(2,24) -> 4* 64.87/27.93 a__f0(22,28) -> 4* 64.87/27.93 a__f0(17,28) -> 5* 64.87/27.93 a__f0(28,13) -> 17*,4,5 64.87/27.93 a__f0(2,28) -> 4* 64.87/27.93 a__f0(23,13) -> 4* 64.87/27.93 a__f0(13,13) -> 4* 64.87/27.93 a__f0(3,13) -> 4* 64.87/27.93 a__f0(24,2) -> 17*,4,5 64.87/27.93 a__f0(28,23) -> 17*,5,4 64.87/27.93 a__f0(23,23) -> 4* 64.87/27.93 a__f0(14,2) -> 5* 64.87/27.93 a__f0(13,23) -> 4* 64.87/27.93 a__f0(3,23) -> 4* 64.87/27.93 a__f0(24,16) -> 17*,4,5 64.87/27.93 a__f0(14,16) -> 5* 64.87/27.93 a__f0(24,22) -> 17*,4,5 64.87/27.93 a__f0(14,22) -> 5* 64.87/27.93 a__f0(24,24) -> 17*,4,5 64.87/27.93 a__f0(5,1) -> 5* 64.87/27.93 a__f0(14,24) -> 5* 64.87/27.93 a__f0(5,3) -> 5* 64.87/27.93 a__f0(24,28) -> 4,17*,5 64.87/27.93 a__f0(14,28) -> 5* 64.87/27.93 a__f0(5,13) -> 5* 64.87/27.93 a__f0(16,2) -> 17*,4,5 64.87/27.93 a__f0(1,2) -> 4* 64.87/27.93 a__f0(5,23) -> 5* 64.87/27.93 a__f0(16,16) -> 17*,5,4 64.87/27.93 a__f0(1,16) -> 4* 64.87/27.93 a__f0(22,1) -> 4* 64.87/27.93 a__f0(17,1) -> 5* 64.87/27.93 a__f0(22,3) -> 4* 64.87/27.93 a__f0(16,22) -> 5,17*,4 64.87/27.93 a__f0(17,3) -> 5* 64.87/27.93 a__f0(2,1) -> 4* 64.87/27.93 a__f0(16,24) -> 17*,5,4 64.87/27.93 a__f0(1,22) -> 4* 64.87/27.93 a__f0(2,3) -> 4* 64.87/27.93 a__f0(1,24) -> 4* 64.87/27.93 a__f0(16,28) -> 5,17*,4 64.87/27.93 a__f0(1,28) -> 4* 64.87/27.93 a__f0(22,13) -> 4* 64.87/27.93 a__f0(17,13) -> 5* 64.87/27.93 a__f0(2,13) -> 4* 64.87/27.93 a__f0(28,2) -> 17*,5,4 64.87/27.93 a__f0(23,2) -> 4* 64.87/27.93 a__f0(22,23) -> 4* 64.87/27.93 a__f0(13,2) -> 4* 64.87/27.93 a__f0(17,23) -> 5* 64.87/27.93 a__f0(3,2) -> 4* 64.87/27.93 a__f0(2,23) -> 4* 64.87/27.93 a__f0(28,16) -> 17*,4,5 64.87/27.93 a__f0(23,16) -> 4* 64.87/27.93 a__f0(13,16) -> 4* 64.87/27.93 a__f0(3,16) -> 4* 64.87/27.93 a__f0(24,1) -> 17*,4,5 64.87/27.93 a__f0(28,22) -> 17*,4,5 64.87/27.93 a__f0(23,22) -> 4* 64.87/27.93 a__f0(14,1) -> 5* 64.87/27.93 a__f0(24,3) -> 17*,4,5 64.87/27.93 a__f0(28,24) -> 17*,4,5 64.87/27.93 a__f0(13,22) -> 4* 64.87/27.93 a__f0(23,24) -> 4* 64.87/27.93 a__f0(14,3) -> 5* 64.87/27.93 a__f0(3,22) -> 4* 64.87/27.93 a__f0(13,24) -> 4* 64.87/27.93 a__f0(28,28) -> 17*,5,4 64.87/27.93 a__f0(3,24) -> 4* 64.87/27.93 a__f0(23,28) -> 4* 64.87/27.93 a__f0(13,28) -> 4* 64.87/27.93 a__f0(3,28) -> 4* 64.87/27.93 a__f0(24,13) -> 17*,4,5 64.87/27.93 a__f0(14,13) -> 5* 64.87/27.93 a__f0(24,23) -> 17*,4,5 64.87/27.93 a__f0(14,23) -> 5* 64.87/27.93 a__f0(5,2) -> 5* 64.87/27.93 a__f0(5,16) -> 5* 64.87/27.93 a__f0(16,1) -> 17*,5,4 64.87/27.93 a__f0(16,3) -> 17*,5,4 64.87/27.93 a__f0(1,1) -> 4* 64.87/27.93 a__f0(5,22) -> 5* 64.87/27.93 a__f0(1,3) -> 4* 64.87/27.93 a__f0(5,24) -> 5* 64.87/27.93 a__f0(5,28) -> 5* 64.87/27.93 a__f0(16,13) -> 17*,5,4 64.87/27.93 a__f0(1,13) -> 4* 64.87/27.93 a__f0(22,2) -> 4* 64.87/27.93 a__f0(17,2) -> 5* 64.87/27.93 a__f0(16,23) -> 17*,4,5 64.87/27.93 a__f0(2,2) -> 4* 64.87/27.93 a__f0(1,23) -> 4* 64.87/27.93 a0() -> 13,14,16*,5,6,1 64.87/27.93 b0() -> 23,14,28*,6,2 64.87/27.93 mark0(22) -> 5* 64.87/27.93 mark0(2) -> 5* 64.87/27.93 mark0(24) -> 5* 64.87/27.93 mark0(16) -> 5* 64.87/27.93 mark0(1) -> 5* 64.87/27.93 mark0(28) -> 5* 64.87/27.93 mark0(23) -> 5* 64.87/27.93 mark0(13) -> 5* 64.87/27.93 mark0(3) -> 5* 64.87/27.93 f0(22,16) -> 4,22*,3 64.87/27.93 f0(17,16) -> 5* 64.87/27.93 f0(28,1) -> 17,24*,5 64.87/27.93 f0(2,16) -> 4,22*,3 64.87/27.93 f0(23,1) -> 4,22* 64.87/27.93 f0(28,3) -> 17,24*,5 64.87/27.93 f0(22,22) -> 4,22*,3 64.87/27.93 f0(23,3) -> 4,22* 64.87/27.93 f0(13,1) -> 4,22*,3 64.87/27.93 f0(17,22) -> 5* 64.87/27.93 f0(22,24) -> 4,22* 64.87/27.93 f0(13,3) -> 4,22*,3 64.87/27.93 f0(3,1) -> 22*,4,3 64.87/27.93 f0(17,24) -> 5* 64.87/27.93 f0(2,22) -> 4,22*,3 64.87/27.93 f0(3,3) -> 22*,4,3 64.87/27.93 f0(2,24) -> 4,22* 64.87/27.93 f0(22,28) -> 4,22* 64.87/27.93 f0(17,28) -> 5* 64.87/27.93 f0(28,13) -> 17,24*,5 64.87/27.93 f0(2,28) -> 4,22* 64.87/27.93 f0(23,13) -> 4,22* 64.87/27.93 f0(13,13) -> 4,22*,3 64.87/27.93 f0(3,13) -> 4,22*,3 64.87/27.93 f0(24,2) -> 22,17,24*,5 64.87/27.93 f0(28,23) -> 17,24*,5 64.87/27.93 f0(23,23) -> 4,22* 64.87/27.93 f0(14,2) -> 5* 64.87/27.93 f0(13,23) -> 4,22* 64.87/27.93 f0(3,23) -> 4,22* 64.87/27.93 f0(24,16) -> 22,17,24*,5 64.87/27.93 f0(14,16) -> 5* 64.87/27.93 f0(24,22) -> 22,17,24*,5 64.87/27.93 f0(24,24) -> 22,17,5,24* 64.87/27.93 f0(14,22) -> 5* 64.87/27.93 f0(5,1) -> 5* 64.87/27.93 f0(14,24) -> 5* 64.87/27.93 f0(5,3) -> 5* 64.87/27.93 f0(24,28) -> 17,24*,5 64.87/27.93 f0(14,28) -> 5* 64.87/27.93 f0(5,13) -> 5* 64.87/27.93 f0(16,2) -> 17,22,5,24*,3 64.87/27.93 f0(1,2) -> 22*,4,3 64.87/27.93 f0(5,23) -> 5* 64.87/27.93 f0(16,16) -> 17,22,5,24*,3 64.87/27.93 f0(1,16) -> 4,22*,3 64.87/27.93 f0(22,1) -> 4,22*,3 64.87/27.93 f0(17,1) -> 5* 64.87/27.93 f0(22,3) -> 4,22*,3 64.87/27.93 f0(16,22) -> 17,22,5,24*,3 64.87/27.93 f0(17,3) -> 5* 64.87/27.93 f0(2,1) -> 22*,4,3 64.87/27.93 f0(16,24) -> 22,17,5,24* 64.87/27.93 f0(1,22) -> 4,22*,3 64.87/27.93 f0(2,3) -> 22*,4,3 64.87/27.93 f0(1,24) -> 4,22* 64.87/27.93 f0(16,28) -> 17,5,24* 64.87/27.93 f0(1,28) -> 4,22* 64.87/27.93 f0(22,13) -> 4,22*,3 64.87/27.93 f0(17,13) -> 5* 64.87/27.93 f0(2,13) -> 4,22*,3 64.87/27.93 f0(28,2) -> 17,24*,5 64.87/27.93 f0(23,2) -> 4,22* 64.87/27.93 f0(22,23) -> 4,22* 64.87/27.93 f0(13,2) -> 4,22*,3 64.87/27.93 f0(17,23) -> 5* 64.87/27.93 f0(3,2) -> 22*,4,3 64.87/27.93 f0(2,23) -> 4,22* 64.87/27.93 f0(28,16) -> 17,24*,5 64.87/27.93 f0(23,16) -> 4,22* 64.87/27.93 f0(13,16) -> 4,22*,3 64.87/27.93 f0(3,16) -> 4,22*,3 64.87/27.93 f0(24,1) -> 22,17,24*,5 64.87/27.93 f0(28,22) -> 17,24*,5 64.87/27.93 f0(23,22) -> 4,22* 64.87/27.93 f0(14,1) -> 5* 64.87/27.93 f0(24,3) -> 22,17,24*,5 64.87/27.93 f0(28,24) -> 17,24*,5 64.87/27.93 f0(13,22) -> 4,22*,3 64.87/27.93 f0(23,24) -> 4,22* 64.87/27.93 f0(14,3) -> 5* 64.87/27.93 f0(3,22) -> 4,22*,3 64.87/27.93 f0(13,24) -> 4,22* 64.87/27.93 f0(28,28) -> 17,24*,5 64.87/27.93 f0(3,24) -> 4,22* 64.87/27.93 f0(23,28) -> 4,22* 64.87/27.93 f0(13,28) -> 4,22* 64.87/27.93 f0(3,28) -> 4,22* 64.87/27.93 f0(24,13) -> 22,17,24*,5 64.87/27.93 f0(14,13) -> 5* 64.87/27.93 f0(24,23) -> 22,17,24*,5 64.87/27.93 f0(14,23) -> 5* 64.87/27.93 f0(5,2) -> 5* 64.87/27.93 f0(5,16) -> 5* 64.87/27.93 f0(16,1) -> 17,22,5,24*,3 64.87/27.93 f0(16,3) -> 17,22,5,24*,3 64.87/27.93 f0(1,1) -> 22*,4,3 64.87/27.93 f0(5,22) -> 5* 64.87/27.93 f0(1,3) -> 22*,4,3 64.87/27.93 f0(5,24) -> 5* 64.87/27.93 f0(5,28) -> 5* 64.87/27.93 f0(16,13) -> 17,22,5,24*,3 64.87/27.93 f0(1,13) -> 4,22*,3 64.87/27.93 f0(22,2) -> 4,22*,3 64.87/27.93 f0(17,2) -> 5* 64.87/27.93 f0(16,23) -> 17,22,5,24* 64.87/27.93 f0(2,2) -> 22*,4,3 64.87/27.93 f0(1,23) -> 4,22* 64.87/27.93 a__b0() -> 14*,5,6 64.87/27.93 a__f1(13,23) -> 4* 64.87/27.93 a__f1(16,2) -> 5,17*,4 64.87/27.93 a__f1(1,2) -> 4* 64.87/27.93 a__f1(16,28) -> 5,17*,4 64.87/27.93 a__f1(1,28) -> 4* 64.87/27.93 a__f1(13,2) -> 4* 64.87/27.93 a__f1(13,28) -> 4* 64.87/27.93 a__f1(16,23) -> 5,17*,4 64.87/27.93 a__f1(1,23) -> 4* 64.87/27.93 a1() -> 13,14,16*,5,6,1 64.87/27.93 b1() -> 23,14,28*,6,2 64.87/27.93 f1(13,23) -> 4,22* 64.87/27.93 f1(16,2) -> 17,22,5,24*,3 64.87/27.93 f1(1,2) -> 22*,3,4 64.87/27.93 f1(16,28) -> 17,5,24* 64.87/27.93 f1(1,28) -> 4,22* 64.87/27.93 f1(13,2) -> 4,3,22* 64.87/27.93 f1(13,28) -> 4,22* 64.87/27.93 f1(16,23) -> 17,22,5,24* 64.87/27.93 f1(1,23) -> 4,22* 64.87/27.93 a__b1() -> 6,14*,5 64.87/27.93 mark1(16) -> 5,16* 64.87/27.94 mark1(1) -> 5,16* 64.87/27.94 mark1(13) -> 5,16* 64.87/27.94 problem: 64.87/27.94 strict: 64.87/27.94 64.87/27.94 weak: 64.87/27.94 a__f(X,X) -> a__f(a(),b()) 64.87/27.94 mark(f(X1,X2)) -> a__f(mark(X1),X2) 64.87/27.94 a__b() -> a() 64.87/27.94 mark(b()) -> a__b() 64.87/27.94 mark(a()) -> a() 64.87/27.94 a__f(X1,X2) -> f(X1,X2) 64.87/27.94 a__b() -> b() 64.87/27.94 Qed 64.87/27.94 64.87/27.94 strict: 64.87/27.94 a__f(X,X) -> a__f(a(),b()) 64.87/27.94 weak: 64.87/27.94 mark(f(X1,X2)) -> a__f(mark(X1),X2) 64.87/27.94 a__b() -> a() 64.87/27.94 mark(b()) -> a__b() 64.87/27.94 mark(a()) -> a() 64.87/27.94 a__f(X1,X2) -> f(X1,X2) 64.87/27.94 a__b() -> b() 64.87/27.94 Matrix Interpretation Processor: dim=5 64.87/27.94 64.87/27.94 max_matrix: 64.87/27.94 [1 1 0 0 1] 64.87/27.94 [0 0 1 1 1] 64.87/27.94 [0 0 0 0 0] 64.87/27.94 [0 0 0 1 1] 64.87/27.94 [0 0 0 0 0] 64.87/27.94 interpretation: 64.87/27.94 [1 1 0 0 0] 64.87/27.94 [0 0 0 1 0] 64.87/27.94 [mark](x0) = [0 0 0 0 0]x0 64.87/27.94 [0 0 0 1 0] 64.87/27.94 [0 0 0 0 0] , 64.87/27.94 64.87/27.94 [1 1 0 0 0] [1 0 0 0 0] [0] 64.87/27.94 [0 0 0 1 1] [0 0 0 0 0] [1] 64.87/27.94 [f](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [0] 64.87/27.94 [0 0 0 1 0] [0 0 0 1 0] [1] 64.87/27.94 [0 0 0 0 0] [0 0 0 0 0] [0], 64.87/27.94 64.87/27.94 [0] 64.87/27.94 [0] 64.87/27.94 [a__b] = [0] 64.87/27.94 [0] 64.87/27.94 [0], 64.87/27.94 64.87/27.94 [0] 64.87/27.94 [0] 64.87/27.94 [b] = [0] 64.87/27.94 [0] 64.87/27.94 [0], 64.87/27.94 64.87/27.94 [0] 64.87/27.94 [0] 64.87/27.94 [a] = [0] 64.87/27.94 [0] 64.87/27.94 [0], 64.87/27.94 64.87/27.94 [1 1 0 0 1] [1 0 0 0 0] [0] 64.87/27.94 [0 0 1 1 1] [0 0 0 1 0] [1] 64.87/27.94 [a__f](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 0 0]x1 + [0] 64.87/27.94 [0 0 0 1 1] [0 0 0 1 0] [1] 64.87/27.94 [0 0 0 0 0] [0 0 0 0 0] [0] 64.87/27.94 orientation: 64.87/27.94 [1 1 0 1 1] [1 0 0 0 0] [1] [1 1 0 1 0] [1 0 0 0 0] [0] 64.87/27.94 [0 0 0 1 0] [0 0 0 1 0] [1] [0 0 0 1 0] [0 0 0 1 0] [1] 64.87/27.94 mark(f(X1,X2)) = [0 0 0 0 0]X1 + [0 0 0 0 0]X2 + [0] >= [0 0 0 0 0]X1 + [0 0 0 0 0]X2 + [0] = a__f(mark(X1),X2) 64.87/27.94 [0 0 0 1 0] [0 0 0 1 0] [1] [0 0 0 1 0] [0 0 0 1 0] [1] 64.87/27.94 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 64.87/27.94 64.87/27.94 [0] [0] 64.87/27.94 [0] [0] 64.87/27.94 a__b() = [0] >= [0] = a() 64.87/27.94 [0] [0] 64.87/27.94 [0] [0] 64.87/27.94 64.87/27.94 [0] [0] 64.87/27.94 [0] [0] 64.87/27.94 mark(b()) = [0] >= [0] = a__b() 64.87/27.94 [0] [0] 64.87/27.94 [0] [0] 64.87/27.94 64.87/27.94 [0] [0] 64.87/27.94 [0] [0] 64.87/27.94 mark(a()) = [0] >= [0] = a() 64.87/27.94 [0] [0] 64.87/27.94 [0] [0] 64.87/27.94 64.87/27.94 [1 1 0 0 1] [1 0 0 0 0] [0] [1 1 0 0 0] [1 0 0 0 0] [0] 64.87/27.94 [0 0 1 1 1] [0 0 0 1 0] [1] [0 0 0 1 1] [0 0 0 0 0] [1] 64.87/27.94 a__f(X1,X2) = [0 0 0 0 0]X1 + [0 0 0 0 0]X2 + [0] >= [0 0 0 0 0]X1 + [0 0 0 0 0]X2 + [0] = f(X1,X2) 64.87/27.94 [0 0 0 1 1] [0 0 0 1 0] [1] [0 0 0 1 0] [0 0 0 1 0] [1] 64.87/27.94 [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] 64.87/27.94 64.87/27.94 [0] [0] 64.87/27.94 [0] [0] 64.87/27.94 a__b() = [0] >= [0] = b() 64.87/27.94 [0] [0] 64.87/27.94 [0] [0] 64.87/27.94 64.87/27.94 [2 1 0 0 1] [0] [0] 64.87/27.94 [0 0 1 2 1] [1] [1] 64.87/27.94 a__f(X,X) = [0 0 0 0 0]X + [0] >= [0] = a__f(a(),b()) 64.87/27.94 [0 0 0 2 1] [1] [1] 64.87/27.94 [0 0 0 0 0] [0] [0] 64.87/27.94 problem: 64.87/27.94 strict: 64.87/27.94 64.87/27.94 weak: 64.87/27.94 mark(f(X1,X2)) -> a__f(mark(X1),X2) 64.87/27.94 a__b() -> a() 64.87/27.94 mark(b()) -> a__b() 64.87/27.94 mark(a()) -> a() 64.87/27.94 a__f(X1,X2) -> f(X1,X2) 64.87/27.94 a__b() -> b() 64.87/27.94 a__f(X,X) -> a__f(a(),b()) 64.87/27.94 Qed 64.87/27.94 EOF