YES(?,O(n^1))
0.15/0.23	YES(?,O(n^1))
0.15/0.23	
0.15/0.23	Problem:
0.15/0.23	 g(x,a(),b()) -> g(b(),b(),a())
0.15/0.23	
0.15/0.23	Proof:
0.15/0.23	 Bounds Processor:
0.15/0.23	  bound: 1
0.15/0.23	  enrichment: match
0.15/0.23	  automaton:
0.15/0.23	   final states: {3,2,1}
0.15/0.23	   transitions:
0.15/0.23	    g1(6,6,5) -> 1*
0.15/0.23	    b1() -> 6*
0.15/0.23	    a1() -> 5*
0.15/0.23	    g0(1,1,1) -> 1*
0.15/0.23	    g0(1,3,1) -> 1*
0.15/0.23	    g0(1,2,3) -> 1*
0.15/0.23	    g0(2,2,1) -> 1*
0.15/0.23	    g0(2,1,3) -> 1*
0.15/0.23	    g0(2,3,3) -> 1*
0.15/0.23	    g0(3,1,1) -> 1*
0.15/0.23	    g0(1,1,2) -> 1*
0.15/0.23	    g0(3,3,1) -> 1*
0.15/0.23	    g0(1,3,2) -> 1*
0.15/0.23	    g0(3,2,3) -> 1*
0.15/0.23	    g0(2,2,2) -> 1*
0.15/0.23	    g0(3,1,2) -> 1*
0.15/0.23	    g0(3,3,2) -> 1*
0.15/0.23	    g0(1,2,1) -> 1*
0.15/0.23	    g0(1,1,3) -> 1*
0.15/0.23	    g0(1,3,3) -> 1*
0.15/0.23	    g0(2,1,1) -> 1*
0.15/0.23	    g0(2,3,1) -> 1*
0.15/0.23	    g0(2,2,3) -> 1*
0.15/0.23	    g0(3,2,1) -> 1*
0.15/0.23	    g0(1,2,2) -> 1*
0.15/0.23	    g0(3,1,3) -> 1*
0.15/0.23	    g0(3,3,3) -> 1*
0.15/0.23	    g0(2,1,2) -> 1*
0.15/0.23	    g0(2,3,2) -> 1*
0.15/0.23	    g0(3,2,2) -> 1*
0.15/0.23	    a0() -> 2*
0.15/0.23	    b0() -> 3*
0.15/0.23	  problem:
0.15/0.23	   
0.15/0.23	  Qed
0.15/0.23	EOF