YES(?,O(n^1)) 0.16/0.30 YES(?,O(n^1)) 0.16/0.30 0.16/0.30 Problem: 0.16/0.30 f(X) -> if(X,c(),n__f(true())) 0.16/0.30 if(true(),X,Y) -> X 0.16/0.30 if(false(),X,Y) -> activate(Y) 0.16/0.30 f(X) -> n__f(X) 0.16/0.30 activate(n__f(X)) -> f(X) 0.16/0.30 activate(X) -> X 0.16/0.30 0.16/0.30 Proof: 0.16/0.30 Bounds Processor: 0.16/0.30 bound: 3 0.16/0.30 enrichment: match 0.16/0.30 automaton: 0.16/0.30 final states: {8,9} 0.16/0.30 transitions: 0.16/0.30 true3() -> 19* 0.16/0.30 f1(9) -> 8* 0.16/0.30 f1(8) -> 8* 0.16/0.30 n__f1(13) -> 14* 0.16/0.30 n__f1(8) -> 8* 0.16/0.30 activate1(20) -> 8* 0.16/0.30 activate1(17) -> 8* 0.16/0.30 activate1(14) -> 8* 0.16/0.30 activate1(9) -> 8* 0.16/0.30 activate1(8) -> 8* 0.16/0.30 if1(9,15,14) -> 8* 0.16/0.30 if1(8,15,14) -> 8* 0.16/0.30 c1() -> 15* 0.16/0.30 true1() -> 13* 0.16/0.30 f2(19) -> 8* 0.16/0.30 f2(16) -> 8* 0.16/0.30 f2(13) -> 8* 0.16/0.30 f2(8) -> 8* 0.16/0.30 n__f2(16) -> 17* 0.16/0.30 n__f2(8) -> 8* 0.16/0.30 f0(9) -> 8* 0.16/0.30 f0(8) -> 8* 0.16/0.30 if2(8,18,17) -> 8* 0.16/0.30 if0(8,8,8) -> 8* 0.16/0.30 if0(9,9,8) -> 8* 0.16/0.30 if0(8,8,9) -> 8* 0.16/0.30 if0(9,9,9) -> 8* 0.16/0.30 if0(8,9,8) -> 8* 0.16/0.30 if0(9,8,8) -> 8* 0.16/0.30 if0(8,9,9) -> 8* 0.16/0.30 if0(9,8,9) -> 8* 0.16/0.30 c2() -> 18* 0.16/0.30 c0() -> 8* 0.16/0.30 true2() -> 16* 0.16/0.30 n__f0(9) -> 8* 0.16/0.30 n__f0(8) -> 8* 0.16/0.30 n__f3(19) -> 20* 0.16/0.30 n__f3(16) -> 8* 0.16/0.30 n__f3(13) -> 8* 0.16/0.30 n__f3(8) -> 8* 0.16/0.30 true0() -> 8* 0.16/0.30 if3(19,21,20) -> 8* 0.16/0.30 if3(16,21,20) -> 8* 0.16/0.30 if3(13,21,20) -> 8* 0.16/0.30 if3(8,21,20) -> 8* 0.16/0.30 false0() -> 9* 0.16/0.30 c3() -> 21* 0.16/0.30 activate0(9) -> 8* 0.16/0.30 activate0(8) -> 8* 0.16/0.30 9 -> 8* 0.16/0.30 14 -> 8* 0.16/0.30 15 -> 8* 0.16/0.30 17 -> 8* 0.16/0.30 18 -> 8* 0.16/0.30 20 -> 8* 0.16/0.30 21 -> 8* 0.16/0.30 problem: 0.16/0.30 0.16/0.30 Qed 0.16/0.31 EOF