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(66) -> 67*
    s3(65) -> 66*
    s3(132) -> 133*
    s3(84) -> 85*
    s3(64) -> 65*
    s3(76) -> 77*
    s3(108) -> 109*
    f4(82) -> 83*
    f4(124) -> 125*
    f4(98) -> 99*
    f4(150) -> 151*
    03() -> 76*
    s4(104) -> 105*
    f0(5) -> 5*
    04() -> 104*
    00() -> 5*
    s5(130) -> 131*
    s0(5) -> 5*
    05() -> 130*
    g0(5) -> 5*
    f1(20) -> 21*
    f1(92) -> 93*
    f1(74) -> 75*
    f1(138) -> 139*
    f1(118) -> 119*
    f1(38) -> 39*
    s1(10) -> 11*
    s1(11) -> 12*
    s1(8) -> 9*
    01() -> 8*
    g1(12) -> 13*
    g1(26) -> 27*
    f2(40) -> 41*
    f2(72) -> 73*
    f2(114) -> 115*
    f2(94) -> 95*
    f2(54) -> 55*
    f2(136) -> 137*
    g2(30) -> 31*
    s2(112) -> 113*
    s2(134) -> 135*
    s2(29) -> 30*
    s2(68) -> 69*
    s2(48) -> 49*
    s2(28) -> 29*
    s2(90) -> 91*
    f3(80) -> 81*
    f3(122) -> 123*
    f3(52) -> 53*
    f3(96) -> 97*
    f3(148) -> 149*
    02() -> 48*
    5 -> 20,10
    8 -> 54,38,28
    9 -> 27,41,13,21,5
    10 -> 40*
    11 -> 26*
    13 -> 41,21,5
    21 -> 27,5
    27 -> 5*
    28 -> 52*
    31 -> 41,13,21,5
    39 -> 5*
    41 -> 13,5
    48 -> 80,74,72,64
    49 -> 139,119,93,75,68,53,55,31,39
    53 -> 31,21
    55 -> 27,5
    64 -> 82*
    67 -> 13*
    69 -> 30*
    73 -> 27*
    75 -> 5,20,10,40
    76 -> 98,94,92,90
    77 -> 137,115,95,84,83,81,31,67,73,27
    81 -> 31*
    83 -> 67,41
    85 -> 66*
    90 -> 96*
    91 -> 29*
    93 -> 5*
    95 -> 27,5
    97 -> 31*
    99 -> 67,41
    104 -> 118,114,112,108
    105 -> 149,123,97,99
    108 -> 124*
    109 -> 65*
    112 -> 122*
    113 -> 29*
    115 -> 27*
    119 -> 5,20,10,40
    123 -> 31*
    125 -> 67,41
    130 -> 138,136,134,132
    131 -> 151,125
    132 -> 150*
    133 -> 65*
    134 -> 148*
    135 -> 29*
    137 -> 27*
    139 -> 5,20,10,40
    149 -> 31*
    151 -> 67,41
  problem:
   
  Qed