YES(?,O(n^1))
0.15/0.37	YES(?,O(n^1))
0.15/0.37	
0.15/0.37	Problem:
0.15/0.37	 f(X) -> if(X,c(),n__f(n__true()))
0.15/0.37	 if(true(),X,Y) -> X
0.15/0.37	 if(false(),X,Y) -> activate(Y)
0.15/0.37	 f(X) -> n__f(X)
0.15/0.37	 true() -> n__true()
0.15/0.37	 activate(n__f(X)) -> f(activate(X))
0.15/0.37	 activate(n__true()) -> true()
0.15/0.37	 activate(X) -> X
0.15/0.37	
0.15/0.37	Proof:
0.15/0.37	 Bounds Processor:
0.15/0.37	  bound: 4
0.15/0.37	  enrichment: match
0.15/0.37	  automaton:
0.15/0.37	   final states: {8,7,6,5}
0.15/0.37	   transitions:
0.15/0.37	    c3() -> 25*
0.15/0.37	    true1() -> 6,8
0.15/0.37	    n__true3() -> 21,23
0.15/0.37	    f1(6) -> 6,8
0.15/0.37	    true3() -> 29*
0.15/0.37	    activate1(10) -> 5*
0.15/0.37	    activate1(2) -> 6*
0.15/0.37	    activate1(19) -> 6,8
0.15/0.37	    activate1(4) -> 6*
0.15/0.37	    activate1(1) -> 6*
0.15/0.37	    activate1(3) -> 6*
0.15/0.37	    n__true4() -> 29*
0.15/0.37	    n__true1() -> 7,9
0.15/0.37	    n__f1(2) -> 5*
0.15/0.37	    n__f1(9) -> 10*
0.15/0.37	    n__f1(4) -> 5*
0.15/0.37	    n__f1(1) -> 5*
0.15/0.37	    n__f1(3) -> 5*
0.15/0.37	    if1(1,11,10) -> 5*
0.15/0.37	    if1(3,11,10) -> 5*
0.15/0.37	    if1(2,11,10) -> 5*
0.15/0.37	    if1(4,11,10) -> 5*
0.15/0.37	    c1() -> 11*
0.15/0.37	    n__true2() -> 6,8,18
0.15/0.37	    n__f2(6) -> 6,8
0.15/0.37	    n__f2(18) -> 19*
0.15/0.37	    f0(2) -> 5*
0.15/0.37	    f0(4) -> 5*
0.15/0.37	    f0(1) -> 5*
0.15/0.37	    f0(3) -> 5*
0.15/0.37	    if2(6,20,19) -> 6,8
0.15/0.37	    if0(3,4,2) -> 6*
0.15/0.37	    if0(1,1,4) -> 6*
0.15/0.37	    if0(1,3,4) -> 6*
0.15/0.37	    if0(4,1,2) -> 6*
0.15/0.37	    if0(1,1,1) -> 6*
0.15/0.37	    if0(4,3,2) -> 6*
0.15/0.37	    if0(1,3,1) -> 6*
0.15/0.37	    if0(2,2,4) -> 6*
0.15/0.37	    if0(2,4,4) -> 6*
0.15/0.37	    if0(1,2,3) -> 6*
0.15/0.37	    if0(1,4,3) -> 6*
0.15/0.37	    if0(2,2,1) -> 6*
0.15/0.37	    if0(2,4,1) -> 6*
0.15/0.37	    if0(3,1,4) -> 6*
0.15/0.37	    if0(3,3,4) -> 6*
0.15/0.37	    if0(2,1,3) -> 6*
0.15/0.37	    if0(2,3,3) -> 6*
0.15/0.37	    if0(3,1,1) -> 6*
0.15/0.37	    if0(1,1,2) -> 6*
0.15/0.37	    if0(3,3,1) -> 6*
0.15/0.37	    if0(1,3,2) -> 6*
0.15/0.37	    if0(4,2,4) -> 6*
0.15/0.37	    if0(4,4,4) -> 6*
0.15/0.37	    if0(3,2,3) -> 6*
0.15/0.37	    if0(3,4,3) -> 6*
0.15/0.37	    if0(4,2,1) -> 6*
0.15/0.37	    if0(2,2,2) -> 6*
0.15/0.37	    if0(4,4,1) -> 6*
0.15/0.37	    if0(2,4,2) -> 6*
0.15/0.37	    if0(4,1,3) -> 6*
0.15/0.37	    if0(4,3,3) -> 6*
0.15/0.37	    if0(3,1,2) -> 6*
0.15/0.37	    if0(3,3,2) -> 6*
0.15/0.37	    if0(1,2,4) -> 6*
0.15/0.37	    if0(1,4,4) -> 6*
0.15/0.37	    if0(4,2,2) -> 6*
0.15/0.37	    if0(1,2,1) -> 6*
0.15/0.37	    if0(4,4,2) -> 6*
0.15/0.37	    if0(1,4,1) -> 6*
0.15/0.37	    if0(2,1,4) -> 6*
0.15/0.37	    if0(2,3,4) -> 6*
0.15/0.37	    if0(1,1,3) -> 6*
0.15/0.37	    if0(1,3,3) -> 6*
0.15/0.37	    if0(2,1,1) -> 6*
0.15/0.37	    if0(2,3,1) -> 6*
0.15/0.37	    if0(3,2,4) -> 6*
0.15/0.37	    if0(3,4,4) -> 6*
0.15/0.37	    if0(2,2,3) -> 6*
0.15/0.37	    if0(2,4,3) -> 6*
0.15/0.37	    if0(3,2,1) -> 6*
0.15/0.37	    if0(1,2,2) -> 6*
0.15/0.37	    if0(3,4,1) -> 6*
0.15/0.37	    if0(1,4,2) -> 6*
0.15/0.37	    if0(4,1,4) -> 6*
0.15/0.37	    if0(4,3,4) -> 6*
0.15/0.37	    if0(3,1,3) -> 6*
0.15/0.37	    if0(3,3,3) -> 6*
0.15/0.37	    if0(4,1,1) -> 6*
0.15/0.37	    if0(2,1,2) -> 6*
0.15/0.37	    if0(4,3,1) -> 6*
0.15/0.37	    if0(2,3,2) -> 6*
0.15/0.37	    if0(4,2,3) -> 6*
0.15/0.37	    if0(4,4,3) -> 6*
0.15/0.37	    if0(3,2,2) -> 6*
0.15/0.37	    c2() -> 20*
0.15/0.37	    c0() -> 1*
0.15/0.37	    f2(29) -> 6,8
0.15/0.37	    f2(21) -> 5*
0.15/0.37	    n__f0(2) -> 2*
0.15/0.37	    n__f0(4) -> 2*
0.15/0.37	    n__f0(1) -> 2*
0.15/0.37	    n__f0(3) -> 2*
0.15/0.37	    activate2(9) -> 21*
0.15/0.37	    activate2(18) -> 29*
0.15/0.37	    n__true0() -> 3*
0.15/0.37	    true2() -> 21*
0.15/0.37	    true0() -> 7*
0.15/0.37	    n__f3(29) -> 6,8
0.15/0.37	    n__f3(21) -> 5*
0.15/0.37	    n__f3(23) -> 24*
0.15/0.37	    false0() -> 4*
0.15/0.37	    if3(29,25,5) -> 6*
0.15/0.37	    if3(29,25,24) -> 8*
0.15/0.37	    if3(21,25,24) -> 5*
0.15/0.37	    activate0(2) -> 8*
0.15/0.37	    activate0(4) -> 8*
0.15/0.37	    activate0(1) -> 8*
0.15/0.37	    activate0(3) -> 8*
0.15/0.37	    1 -> 6,8
0.15/0.37	    2 -> 6,8
0.15/0.37	    3 -> 6,8
0.15/0.37	    4 -> 6,8
0.15/0.37	    9 -> 21*
0.15/0.37	    10 -> 5*
0.15/0.37	    18 -> 29*
0.15/0.37	    19 -> 6,8
0.15/0.37	    20 -> 6,8
0.15/0.37	    25 -> 6,8,5
0.15/0.37	  problem:
0.15/0.37	   
0.15/0.37	  Qed
0.15/0.38	EOF