YES(?,O(n^1)) 0.15/0.25 YES(?,O(n^1)) 0.15/0.25 0.15/0.25 Problem: 0.15/0.25 f(c(X,s(Y))) -> f(c(s(X),Y)) 0.15/0.25 g(c(s(X),Y)) -> f(c(X,s(Y))) 0.15/0.25 0.15/0.25 Proof: 0.15/0.25 Bounds Processor: 0.15/0.25 bound: 2 0.15/0.25 enrichment: match 0.15/0.25 automaton: 0.15/0.25 final states: {4,3} 0.15/0.25 transitions: 0.15/0.25 f1(9) -> 4* 0.15/0.25 f1(8) -> 3* 0.15/0.25 c1(16,2) -> 9* 0.15/0.25 c1(7,1) -> 8* 0.15/0.25 c1(2,7) -> 9* 0.15/0.25 c1(16,1) -> 9* 0.15/0.25 c1(1,7) -> 9* 0.15/0.25 c1(7,2) -> 8* 0.15/0.25 s1(7) -> 7* 0.15/0.25 s1(2) -> 7* 0.15/0.25 s1(16) -> 16* 0.15/0.25 s1(1) -> 7* 0.15/0.25 s1(13) -> 16* 0.15/0.25 f2(14) -> 4* 0.15/0.25 c2(13,1) -> 14* 0.15/0.25 c2(13,7) -> 14* 0.15/0.25 c2(13,2) -> 14* 0.15/0.25 f0(2) -> 3* 0.15/0.25 f0(1) -> 3* 0.15/0.25 s2(2) -> 13* 0.15/0.25 s2(1) -> 13* 0.15/0.25 s2(13) -> 13* 0.15/0.25 c0(1,2) -> 1* 0.15/0.25 c0(2,1) -> 1* 0.15/0.25 c0(1,1) -> 1* 0.15/0.25 c0(2,2) -> 1* 0.15/0.25 s0(2) -> 2* 0.15/0.25 s0(1) -> 2* 0.15/0.25 g0(2) -> 4* 0.15/0.25 g0(1) -> 4* 0.15/0.25 problem: 0.15/0.25 0.15/0.25 Qed 0.15/0.25 EOF