YES(?,O(n^1))
0.16/0.33	YES(?,O(n^1))
0.16/0.33	
0.16/0.33	Problem:
0.16/0.33	 f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'()))
0.16/0.33	 f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'()))
0.16/0.33	
0.16/0.33	Proof:
0.16/0.33	 Bounds Processor:
0.16/0.33	  bound: 1
0.16/0.33	  enrichment: match
0.16/0.33	  automaton:
0.16/0.33	   final states: {1,2}
0.16/0.33	   transitions:
0.16/0.33	    if1(13,31,25) -> 1*
0.16/0.33	    if1(13,12,9) -> 1*
0.16/0.33	    e1() -> 13*
0.16/0.33	    f1(8,5) -> 9*
0.16/0.33	    f1(30,26) -> 31*
0.16/0.33	    f1(11,5) -> 12*
0.16/0.33	    f1(6,5) -> 25*
0.16/0.33	    .1(10,29) -> 30*
0.16/0.33	    .1(10,6) -> 11*
0.16/0.33	    .1(7,6) -> 8*
0.16/0.33	    b1() -> 10*
0.16/0.33	    g1(28,6) -> 29*
0.16/0.33	    h1(27,10) -> 28*
0.16/0.33	    a1() -> 27*
0.16/0.33	    c1() -> 6*
0.16/0.33	    d1() -> 26*
0.16/0.33	    d'1() -> 5*
0.16/0.33	    b'1() -> 7*
0.16/0.33	    f0(1,2) -> 1*
0.16/0.33	    f0(2,1) -> 1*
0.16/0.33	    f0(1,1) -> 1*
0.16/0.33	    f0(2,2) -> 1*
0.16/0.33	    g0(1,2) -> 1*
0.16/0.33	    g0(2,1) -> 1*
0.16/0.33	    g0(1,1) -> 1*
0.16/0.33	    g0(2,2) -> 1*
0.16/0.33	    i0(1,1,1) -> 2*
0.16/0.33	    i0(2,2,1) -> 2*
0.16/0.33	    i0(1,1,2) -> 2*
0.16/0.33	    i0(2,2,2) -> 2*
0.16/0.33	    i0(1,2,1) -> 2*
0.16/0.33	    i0(2,1,1) -> 2*
0.16/0.33	    i0(1,2,2) -> 2*
0.16/0.33	    i0(2,1,2) -> 2*
0.16/0.33	    a0() -> 1*
0.16/0.33	    b0() -> 1*
0.16/0.33	    b'0() -> 1*
0.16/0.33	    c0() -> 1*
0.16/0.33	    d0() -> 1*
0.16/0.33	    if0(1,1,1) -> 1*
0.16/0.33	    if0(2,2,1) -> 1*
0.16/0.33	    if0(1,1,2) -> 1*
0.16/0.33	    if0(2,2,2) -> 1*
0.16/0.33	    if0(1,2,1) -> 1*
0.16/0.33	    if0(2,1,1) -> 1*
0.16/0.33	    if0(1,2,2) -> 1*
0.16/0.33	    if0(2,1,2) -> 1*
0.16/0.33	    e0() -> 1*
0.16/0.33	    .0(1,2) -> 1*
0.16/0.33	    .0(2,1) -> 1*
0.16/0.33	    .0(1,1) -> 1*
0.16/0.33	    .0(2,2) -> 1*
0.16/0.33	    d'0() -> 1*
0.16/0.33	    h0(1,2) -> 1*
0.16/0.33	    h0(2,1) -> 1*
0.16/0.33	    h0(1,1) -> 1*
0.16/0.33	    h0(2,2) -> 1*
0.16/0.33	  problem:
0.16/0.33	   
0.16/0.33	  Qed
0.16/0.34	EOF