YES(?,O(n^1)) 0.16/0.31 YES(?,O(n^1)) 0.16/0.31 0.16/0.31 Problem: 0.16/0.31 f(f(X)) -> c(n__f(g(n__f(X)))) 0.16/0.31 c(X) -> d(activate(X)) 0.16/0.31 h(X) -> c(n__d(X)) 0.16/0.31 f(X) -> n__f(X) 0.16/0.31 d(X) -> n__d(X) 0.16/0.31 activate(n__f(X)) -> f(X) 0.16/0.31 activate(n__d(X)) -> d(X) 0.16/0.31 activate(X) -> X 0.16/0.31 0.16/0.31 Proof: 0.16/0.31 Bounds Processor: 0.16/0.31 bound: 3 0.16/0.31 enrichment: match 0.16/0.31 automaton: 0.16/0.31 final states: {8,7,6,5,4} 0.16/0.31 transitions: 0.16/0.31 d1(65) -> 66* 0.16/0.31 d1(10) -> 11* 0.16/0.31 d1(71) -> 72* 0.16/0.31 d1(63) -> 64* 0.16/0.31 f1(55) -> 56* 0.16/0.31 f1(57) -> 58* 0.16/0.31 f1(49) -> 50* 0.16/0.31 n__d1(35) -> 36* 0.16/0.31 n__d1(29) -> 30* 0.16/0.31 n__d1(26) -> 27* 0.16/0.31 n__f1(45) -> 46* 0.16/0.31 n__f1(37) -> 38* 0.16/0.31 n__f1(43) -> 44* 0.16/0.31 c1(27) -> 28* 0.16/0.31 activate1(17) -> 18* 0.16/0.31 activate1(19) -> 20* 0.16/0.31 activate1(9) -> 10* 0.16/0.31 n__d2(97) -> 98* 0.16/0.31 n__d2(99) -> 100* 0.16/0.31 n__d2(91) -> 92* 0.16/0.31 n__d2(105) -> 106* 0.16/0.31 n__f2(89) -> 90* 0.16/0.31 n__f2(81) -> 82* 0.16/0.31 n__f2(83) -> 84* 0.16/0.31 d2(77) -> 78* 0.16/0.31 d2(119) -> 120* 0.16/0.31 d2(111) -> 112* 0.16/0.31 d2(113) -> 114* 0.16/0.31 f0(2) -> 4* 0.16/0.31 f0(1) -> 4* 0.16/0.31 f0(3) -> 4* 0.16/0.31 activate2(76) -> 77* 0.16/0.31 c0(2) -> 5* 0.16/0.31 c0(1) -> 5* 0.16/0.31 c0(3) -> 5* 0.16/0.31 n__d3(107) -> 108* 0.16/0.31 n__d3(131) -> 132* 0.16/0.31 n__d3(123) -> 124* 0.16/0.31 n__d3(125) -> 126* 0.16/0.31 n__f0(2) -> 1* 0.16/0.31 n__f0(1) -> 1* 0.16/0.31 n__f0(3) -> 1* 0.16/0.31 g0(2) -> 2* 0.16/0.31 g0(1) -> 2* 0.16/0.31 g0(3) -> 2* 0.16/0.31 d0(2) -> 7* 0.16/0.31 d0(1) -> 7* 0.16/0.31 d0(3) -> 7* 0.16/0.31 activate0(2) -> 8* 0.16/0.31 activate0(1) -> 8* 0.16/0.31 activate0(3) -> 8* 0.16/0.31 h0(2) -> 6* 0.16/0.31 h0(1) -> 6* 0.16/0.31 h0(3) -> 6* 0.16/0.31 n__d0(2) -> 3* 0.16/0.31 n__d0(1) -> 3* 0.16/0.31 n__d0(3) -> 3* 0.16/0.31 1 -> 8,65,55,43,29,17 0.16/0.31 2 -> 8,63,49,45,35,19 0.16/0.31 3 -> 8,71,57,37,26,9 0.16/0.31 9 -> 10* 0.16/0.31 10 -> 91* 0.16/0.31 11 -> 5* 0.16/0.31 17 -> 18,10 0.16/0.31 18 -> 10* 0.16/0.31 19 -> 20* 0.16/0.31 20 -> 10* 0.16/0.31 26 -> 119* 0.16/0.31 27 -> 76,7 0.16/0.31 28 -> 6* 0.16/0.31 29 -> 113* 0.16/0.31 30 -> 27* 0.16/0.31 35 -> 111* 0.16/0.31 36 -> 27* 0.16/0.31 38 -> 4* 0.16/0.31 44 -> 4* 0.16/0.31 46 -> 4* 0.16/0.31 49 -> 83* 0.16/0.31 50 -> 18,10,8 0.16/0.31 55 -> 89* 0.16/0.31 56 -> 18,10,8 0.16/0.31 57 -> 81* 0.16/0.31 58 -> 18,10,8 0.16/0.31 63 -> 99* 0.16/0.31 64 -> 10,8 0.16/0.31 65 -> 105* 0.16/0.31 66 -> 10,8 0.16/0.31 71 -> 97* 0.16/0.31 72 -> 10,8 0.16/0.31 76 -> 77* 0.16/0.31 77 -> 107* 0.16/0.31 78 -> 28,6 0.16/0.31 82 -> 58* 0.16/0.31 84 -> 50,8 0.16/0.31 90 -> 56,8 0.16/0.31 92 -> 11* 0.16/0.31 98 -> 72* 0.16/0.31 100 -> 64,8 0.16/0.31 106 -> 66,8 0.16/0.31 108 -> 78,28 0.16/0.31 111 -> 123* 0.16/0.31 112 -> 77* 0.16/0.31 113 -> 125* 0.16/0.31 114 -> 77* 0.16/0.31 119 -> 131* 0.16/0.31 120 -> 77* 0.16/0.31 124 -> 112* 0.16/0.31 126 -> 114,77,107 0.16/0.31 132 -> 120,77,107 0.16/0.31 problem: 0.16/0.31 0.16/0.31 Qed 0.16/0.32 EOF