YES(?,O(n^1))

Problem:
 a12(a12(x1)) -> x1
 a13(a13(x1)) -> x1
 a14(a14(x1)) -> x1
 a15(a15(x1)) -> x1
 a16(a16(x1)) -> x1
 a23(a23(x1)) -> x1
 a24(a24(x1)) -> x1
 a25(a25(x1)) -> x1
 a26(a26(x1)) -> x1
 a34(a34(x1)) -> x1
 a35(a35(x1)) -> x1
 a36(a36(x1)) -> x1
 a45(a45(x1)) -> x1
 a46(a46(x1)) -> x1
 a56(a56(x1)) -> x1
 a13(x1) -> a12(a23(a12(x1)))
 a14(x1) -> a12(a23(a34(a23(a12(x1)))))
 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
 a24(x1) -> a23(a34(a23(x1)))
 a25(x1) -> a23(a34(a45(a34(a23(x1)))))
 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
 a35(x1) -> a34(a45(a34(x1)))
 a36(x1) -> a34(a45(a56(a45(a34(x1)))))
 a46(x1) -> a45(a56(a45(x1)))
 a12(a23(a12(a23(a12(a23(x1)))))) -> x1
 a23(a34(a23(a34(a23(a34(x1)))))) -> x1
 a34(a45(a34(a45(a34(a45(x1)))))) -> x1
 a45(a56(a45(a56(a45(a56(x1)))))) -> x1
 a12(a34(x1)) -> a34(a12(x1))
 a12(a45(x1)) -> a45(a12(x1))
 a12(a56(x1)) -> a56(a12(x1))
 a23(a45(x1)) -> a45(a23(x1))
 a23(a56(x1)) -> a56(a23(x1))
 a34(a56(x1)) -> a56(a34(x1))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {16,15,14,13,12,11,10,9,8,7,6,5,4,3,2}
   transitions:
    a451(97) -> 98*
    a451(82) -> 83*
    a451(77) -> 78*
    a451(99) -> 100*
    a451(94) -> 95*
    a451(44) -> 45*
    a451(63) -> 64*
    a451(38) -> 39*
    a561(76) -> 77*
    a561(98) -> 99*
    a561(93) -> 94*
    a561(43) -> 44*
    a341(95) -> 96*
    a341(60) -> 61*
    a341(45) -> 46*
    a341(25) -> 26*
    a341(64) -> 65*
    a341(39) -> 40*
    a341(81) -> 82*
    a341(83) -> 84*
    a341(78) -> 79*
    a231(65) -> 66*
    a231(40) -> 41*
    a231(22) -> 23*
    a231(79) -> 80*
    a231(59) -> 60*
    a231(61) -> 62*
    a231(46) -> 47*
    a231(26) -> 27*
    a121(47) -> 48*
    a121(27) -> 28*
    a121(41) -> 42*
    a121(21) -> 22*
    a121(23) -> 24*
    a120(1) -> 2*
    a130(1) -> 3*
    a140(1) -> 4*
    a150(1) -> 5*
    a160(1) -> 6*
    a230(1) -> 7*
    a240(1) -> 8*
    a250(1) -> 9*
    a260(1) -> 10*
    a340(1) -> 11*
    a350(1) -> 12*
    a360(1) -> 13*
    a450(1) -> 14*
    a460(1) -> 15*
    a560(1) -> 16*
    f300() -> 1*
    1 -> 97,81,59,21
    23 -> 25*
    24 -> 3*
    26 -> 38*
    28 -> 4*
    39 -> 43*
    42 -> 5*
    48 -> 6*
    61 -> 63*
    62 -> 8*
    64 -> 76*
    66 -> 9*
    80 -> 10*
    83 -> 93*
    84 -> 12*
    96 -> 13*
    100 -> 15*
  problem:
   
  Qed