YES(?,O(n^1)) 0.16/0.27 YES(?,O(n^1)) 0.16/0.27 0.16/0.27 Problem: 0.16/0.27 b(a(c(b(b(x1))))) -> a(c(b(b(b(a(c(x1))))))) 0.16/0.27 0.16/0.27 Proof: 0.16/0.27 Bounds Processor: 0.16/0.27 bound: 2 0.16/0.27 enrichment: match 0.16/0.27 automaton: 0.16/0.27 final states: {4} 0.16/0.27 transitions: 0.16/0.27 a1(19) -> 20* 0.16/0.27 a1(14) -> 15* 0.16/0.27 c1(21) -> 22* 0.16/0.27 c1(18) -> 19* 0.16/0.27 c1(13) -> 14* 0.16/0.27 b1(15) -> 16* 0.16/0.27 b1(17) -> 18* 0.16/0.27 b1(16) -> 17* 0.16/0.27 a2(43) -> 44* 0.16/0.27 a2(38) -> 39* 0.16/0.27 a2(33) -> 34* 0.16/0.27 a2(28) -> 29* 0.16/0.27 b0(4) -> 4* 0.16/0.27 c2(42) -> 43* 0.16/0.27 c2(37) -> 38* 0.16/0.27 c2(32) -> 33* 0.16/0.27 c2(27) -> 28* 0.16/0.27 a0(4) -> 4* 0.16/0.27 b2(40) -> 41* 0.16/0.27 b2(30) -> 31* 0.16/0.27 b2(39) -> 40* 0.16/0.27 b2(29) -> 30* 0.16/0.27 b2(41) -> 42* 0.16/0.27 b2(31) -> 32* 0.16/0.27 c0(4) -> 4* 0.16/0.27 4 -> 13* 0.16/0.27 16 -> 27,21 0.16/0.27 20 -> 16,4 0.16/0.27 22 -> 14* 0.16/0.27 30 -> 37* 0.16/0.27 34 -> 17* 0.16/0.27 44 -> 18* 0.16/0.27 problem: 0.16/0.27 0.16/0.27 Qed 0.16/0.27 EOF