YES(?,O(n^1)) 0.16/0.27 YES(?,O(n^1)) 0.16/0.28 0.16/0.28 Problem: 0.16/0.28 b(a(b(b(a(b(a(x1))))))) -> a(b(a(a(b(b(a(b(b(a(x1)))))))))) 0.16/0.28 0.16/0.28 Proof: 0.16/0.28 Bounds Processor: 0.16/0.28 bound: 2 0.16/0.28 enrichment: match 0.16/0.28 automaton: 0.16/0.28 final states: {2,1} 0.16/0.28 transitions: 0.16/0.28 a1(35) -> 36* 0.16/0.28 a1(10) -> 11* 0.16/0.28 a1(7) -> 8* 0.16/0.28 a1(4) -> 5* 0.16/0.28 a1(11) -> 12* 0.16/0.28 a1(13) -> 14* 0.16/0.28 b1(5) -> 6* 0.16/0.28 b1(12) -> 13* 0.16/0.28 b1(39) -> 40* 0.16/0.28 b1(9) -> 10* 0.16/0.28 b1(41) -> 42* 0.16/0.28 b1(6) -> 7* 0.16/0.28 b1(8) -> 9* 0.16/0.28 a2(50) -> 51* 0.16/0.28 a2(52) -> 53* 0.16/0.28 a2(49) -> 50* 0.16/0.28 a2(46) -> 47* 0.16/0.28 a2(43) -> 44* 0.16/0.28 b0(2) -> 1* 0.16/0.28 b0(1) -> 1* 0.16/0.28 b2(45) -> 46* 0.16/0.28 b2(47) -> 48* 0.16/0.28 b2(54) -> 55* 0.16/0.28 b2(44) -> 45* 0.16/0.28 b2(51) -> 52* 0.16/0.28 b2(48) -> 49* 0.16/0.28 a0(2) -> 2* 0.16/0.28 a0(1) -> 2* 0.16/0.28 1 -> 35* 0.16/0.28 2 -> 4* 0.16/0.28 10 -> 39* 0.16/0.28 11 -> 43* 0.16/0.28 13 -> 41* 0.16/0.28 14 -> 6,9,1 0.16/0.28 36 -> 5* 0.16/0.28 40 -> 7* 0.16/0.28 42 -> 7* 0.16/0.28 52 -> 54* 0.16/0.28 53 -> 9* 0.16/0.28 55 -> 46* 0.16/0.28 problem: 0.16/0.28 0.16/0.28 Qed 0.16/0.28 EOF