YES(?,O(n^1))
0.16/0.30	YES(?,O(n^1))
0.16/0.31	
0.16/0.31	Problem:
0.16/0.31	 a__g(X) -> a__h(X)
0.16/0.31	 a__c() -> d()
0.16/0.31	 a__h(d()) -> a__g(c())
0.16/0.31	 mark(g(X)) -> a__g(X)
0.16/0.31	 mark(h(X)) -> a__h(X)
0.16/0.31	 mark(c()) -> a__c()
0.16/0.31	 mark(d()) -> d()
0.16/0.31	 a__g(X) -> g(X)
0.16/0.31	 a__h(X) -> h(X)
0.16/0.31	 a__c() -> c()
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}
0.16/0.31	   transitions:
0.16/0.31	    c1() -> 29*
0.16/0.31	    h1(65) -> 66*
0.16/0.31	    h1(79) -> 80*
0.16/0.31	    h1(71) -> 72*
0.16/0.31	    h1(73) -> 74*
0.16/0.31	    g1(55) -> 56*
0.16/0.31	    g1(57) -> 58*
0.16/0.31	    g1(49) -> 50*
0.16/0.31	    g1(63) -> 64*
0.16/0.31	    d1() -> 25*
0.16/0.31	    a__c1() -> 47*
0.16/0.31	    a__h1(15) -> 16*
0.16/0.31	    a__h1(17) -> 18*
0.16/0.31	    a__h1(9) -> 10*
0.16/0.31	    a__h1(23) -> 24*
0.16/0.31	    a__g1(45) -> 46*
0.16/0.31	    a__g1(37) -> 38*
0.16/0.31	    a__g1(39) -> 40*
0.16/0.31	    a__g1(29) -> 30*
0.16/0.31	    a__g1(31) -> 32*
0.16/0.31	    c2() -> 139*
0.16/0.31	    h2(137) -> 138*
0.16/0.31	    h2(129) -> 130*
0.16/0.31	    h2(131) -> 132*
0.16/0.31	    h2(123) -> 124*
0.16/0.31	    a__g0(2) -> 5*
0.16/0.31	    a__g0(4) -> 5*
0.16/0.31	    a__g0(1) -> 5*
0.16/0.31	    a__g0(3) -> 5*
0.16/0.31	    g2(107) -> 108*
0.16/0.31	    g2(121) -> 122*
0.16/0.31	    g2(113) -> 114*
0.16/0.31	    g2(115) -> 116*
0.16/0.31	    g2(105) -> 106*
0.16/0.31	    a__h0(2) -> 7*
0.16/0.31	    a__h0(4) -> 7*
0.16/0.31	    a__h0(1) -> 7*
0.16/0.31	    a__h0(3) -> 7*
0.16/0.31	    d2() -> 101*
0.16/0.31	    a__c0() -> 6*
0.16/0.31	    a__h2(85) -> 86*
0.16/0.31	    a__h2(99) -> 100*
0.16/0.31	    a__h2(91) -> 92*
0.16/0.31	    a__h2(93) -> 94*
0.16/0.31	    a__h2(83) -> 84*
0.16/0.31	    d0() -> 1*
0.16/0.31	    h3(147) -> 148*
0.16/0.31	    h3(159) -> 160*
0.16/0.31	    h3(141) -> 142*
0.16/0.31	    h3(153) -> 154*
0.16/0.31	    h3(155) -> 156*
0.16/0.31	    c0() -> 2*
0.16/0.31	    mark0(2) -> 8*
0.16/0.31	    mark0(4) -> 8*
0.16/0.31	    mark0(1) -> 8*
0.16/0.31	    mark0(3) -> 8*
0.16/0.31	    g0(2) -> 3*
0.16/0.31	    g0(4) -> 3*
0.16/0.31	    g0(1) -> 3*
0.16/0.31	    g0(3) -> 3*
0.16/0.31	    h0(2) -> 4*
0.16/0.31	    h0(4) -> 4*
0.16/0.31	    h0(1) -> 4*
0.16/0.31	    h0(3) -> 4*
0.16/0.31	    1 -> 71,55,39,15
0.16/0.31	    2 -> 79,63,31,23
0.16/0.31	    3 -> 65,49,45,9
0.16/0.31	    4 -> 73,57,37,17
0.16/0.31	    9 -> 131*
0.16/0.31	    10 -> 8,5
0.16/0.31	    15 -> 137*
0.16/0.31	    16 -> 8,5
0.16/0.31	    17 -> 123*
0.16/0.31	    18 -> 8,5
0.16/0.31	    23 -> 129*
0.16/0.31	    24 -> 8,5
0.16/0.31	    25 -> 8,6
0.16/0.31	    29 -> 107,85,6
0.16/0.31	    30 -> 94,40,16,5,8,7
0.16/0.31	    31 -> 113,91
0.16/0.31	    32 -> 8*
0.16/0.31	    37 -> 105,83
0.16/0.31	    38 -> 8*
0.16/0.31	    39 -> 115,93
0.16/0.31	    40 -> 8*
0.16/0.31	    45 -> 121,99
0.16/0.31	    46 -> 8*
0.16/0.31	    47 -> 8*
0.16/0.31	    50 -> 5*
0.16/0.31	    56 -> 5*
0.16/0.31	    58 -> 5*
0.16/0.31	    64 -> 5*
0.16/0.31	    66 -> 7*
0.16/0.31	    72 -> 7*
0.16/0.31	    74 -> 7*
0.16/0.31	    80 -> 7*
0.16/0.31	    83 -> 159*
0.16/0.31	    84 -> 38*
0.16/0.31	    85 -> 141*
0.16/0.31	    86 -> 30*
0.16/0.31	    91 -> 153*
0.16/0.31	    92 -> 32*
0.16/0.31	    93 -> 155*
0.16/0.31	    94 -> 40,8
0.16/0.31	    99 -> 147*
0.16/0.31	    100 -> 46,8
0.16/0.31	    101 -> 47,8
0.16/0.31	    106 -> 38*
0.16/0.31	    108 -> 30*
0.16/0.31	    114 -> 32*
0.16/0.31	    116 -> 40,8
0.16/0.31	    122 -> 46,8
0.16/0.31	    124 -> 18*
0.16/0.31	    130 -> 24*
0.16/0.31	    132 -> 10,8,5
0.16/0.31	    138 -> 16,8,5
0.16/0.31	    139 -> 47,8
0.16/0.31	    142 -> 86,30,16
0.16/0.31	    148 -> 100,46
0.16/0.31	    154 -> 92,32
0.16/0.31	    156 -> 94,40
0.16/0.31	    160 -> 84,38
0.16/0.31	  problem:
0.16/0.31	   
0.16/0.31	  Qed
0.16/0.31	EOF