YES(?,O(n^1))

Problem:
 f(0()) -> s(0())
 f(s(x)) -> g(s(s(x)))
 g(0()) -> s(0())
 g(s(0())) -> s(0())
 g(s(s(x))) -> f(x)

Proof:
 Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {5}
   transitions:
    g3(62) -> 63*
    s3(60) -> 61*
    s3(84) -> 85*
    s3(74) -> 75*
    s3(66) -> 67*
    s3(61) -> 62*
    s3(100) -> 101*
    f4(70) -> 71*
    f4(108) -> 109*
    f4(78) -> 79*
    f4(90) -> 91*
    03() -> 66*
    s4(80) -> 81*
    f0(5) -> 5*
    04() -> 80*
    00() -> 5*
    s5(96) -> 97*
    s0(5) -> 5*
    05() -> 96*
    g0(5) -> 5*
    f1(20) -> 21*
    f1(102) -> 103*
    f1(86) -> 87*
    f1(38) -> 39*
    s1(10) -> 11*
    s1(11) -> 12*
    s1(8) -> 9*
    01() -> 8*
    g1(12) -> 13*
    g1(26) -> 27*
    f2(40) -> 41*
    f2(104) -> 105*
    f2(64) -> 65*
    f2(76) -> 77*
    f2(88) -> 89*
    g2(30) -> 31*
    s2(29) -> 30*
    s2(48) -> 49*
    s2(28) -> 29*
    f3(50) -> 51*
    02() -> 48*
    5 -> 20,10
    8 -> 38,28
    9 -> 27,41,13,21,5
    10 -> 40*
    11 -> 26*
    13 -> 41,21,5
    21 -> 27,5
    27 -> 5*
    28 -> 50*
    31 -> 41,13,21,5
    39 -> 5*
    41 -> 13,5
    48 -> 64,60
    49 -> 103,87,51,31,39
    51 -> 31,27,21
    60 -> 70*
    63 -> 13*
    65 -> 27*
    66 -> 78,76
    67 -> 105,89,77,74,71,63,65,27,5,20,10,40
    71 -> 63,13
    75 -> 62*
    77 -> 27*
    79 -> 63,13
    80 -> 90,88,86
    81 -> 84,79
    85 -> 62*
    87 -> 5*
    89 -> 27,5
    91 -> 63,13
    96 -> 108,104,102
    97 -> 109,100,91,63
    101 -> 62*
    103 -> 5*
    105 -> 27,5
    109 -> 63,13
  problem:
   
  Qed