YES(?,O(n^1))
0.17/0.28	YES(?,O(n^1))
0.17/0.29	
0.17/0.29	Problem:
0.17/0.29	 rec(rec(x)) -> sent(rec(x))
0.17/0.29	 rec(sent(x)) -> sent(rec(x))
0.17/0.29	 rec(no(x)) -> sent(rec(x))
0.17/0.29	 rec(bot()) -> up(sent(bot()))
0.17/0.29	 rec(up(x)) -> up(rec(x))
0.17/0.29	 sent(up(x)) -> up(sent(x))
0.17/0.29	 no(up(x)) -> up(no(x))
0.17/0.29	 top(rec(up(x))) -> top(check(rec(x)))
0.17/0.29	 top(sent(up(x))) -> top(check(rec(x)))
0.17/0.29	 top(no(up(x))) -> top(check(rec(x)))
0.17/0.29	 check(up(x)) -> up(check(x))
0.17/0.29	 check(sent(x)) -> sent(check(x))
0.17/0.29	 check(rec(x)) -> rec(check(x))
0.17/0.29	 check(no(x)) -> no(check(x))
0.17/0.29	 check(no(x)) -> no(x)
0.17/0.29	
0.17/0.29	Proof:
0.17/0.29	 Bounds Processor:
0.17/0.29	  bound: 1
0.17/0.29	  enrichment: match
0.17/0.29	  automaton:
0.17/0.29	   final states: {7,6,5,4,3}
0.17/0.29	   transitions:
0.17/0.29	    up1(9) -> 10*
0.17/0.29	    up1(46) -> 47*
0.17/0.29	    up1(36) -> 37*
0.17/0.29	    up1(26) -> 27*
0.17/0.29	    check1(45) -> 46*
0.17/0.29	    check1(48) -> 49*
0.17/0.29	    no1(35) -> 36*
0.17/0.29	    no1(38) -> 39*
0.17/0.29	    sent1(25) -> 26*
0.17/0.29	    sent1(28) -> 29*
0.17/0.29	    sent1(8) -> 9*
0.17/0.29	    rec1(16) -> 17*
0.17/0.29	    rec1(18) -> 19*
0.17/0.29	    bot1() -> 8*
0.17/0.29	    rec0(2) -> 3*
0.17/0.29	    rec0(1) -> 3*
0.17/0.29	    sent0(2) -> 4*
0.17/0.29	    sent0(1) -> 4*
0.17/0.29	    no0(2) -> 5*
0.17/0.29	    no0(1) -> 5*
0.17/0.29	    bot0() -> 1*
0.17/0.29	    up0(2) -> 2*
0.17/0.29	    up0(1) -> 2*
0.17/0.29	    top0(2) -> 6*
0.17/0.29	    top0(1) -> 6*
0.17/0.29	    check0(2) -> 7*
0.17/0.29	    check0(1) -> 7*
0.17/0.29	    1 -> 48,38,28,18
0.17/0.29	    2 -> 45,35,25,16
0.17/0.29	    10 -> 17,19,9,3
0.17/0.29	    17 -> 9*
0.17/0.29	    19 -> 9*
0.17/0.29	    27 -> 26,4
0.17/0.29	    29 -> 26*
0.17/0.29	    37 -> 36,5
0.17/0.29	    39 -> 36*
0.17/0.29	    47 -> 46,7
0.17/0.29	    49 -> 46*
0.17/0.29	  problem:
0.17/0.29	   
0.17/0.29	  Qed
0.17/0.29	EOF