YES(?,O(n^1))

Problem:
 f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'()))
 f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'()))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {1,2}
   transitions:
    if1(13,31,25) -> 1*
    if1(13,12,9) -> 1*
    e1() -> 13*
    f1(8,5) -> 9*
    f1(30,26) -> 31*
    f1(11,5) -> 12*
    f1(6,5) -> 25*
    .1(10,29) -> 30*
    .1(10,6) -> 11*
    .1(7,6) -> 8*
    b1() -> 10*
    g1(28,6) -> 29*
    h1(27,10) -> 28*
    a1() -> 27*
    c1() -> 6*
    d1() -> 26*
    d'1() -> 5*
    b'1() -> 7*
    f0(1,2) -> 1*
    f0(2,1) -> 1*
    f0(1,1) -> 1*
    f0(2,2) -> 1*
    g0(1,2) -> 1*
    g0(2,1) -> 1*
    g0(1,1) -> 1*
    g0(2,2) -> 1*
    i0(1,1,1) -> 2*
    i0(2,2,1) -> 2*
    i0(1,1,2) -> 2*
    i0(2,2,2) -> 2*
    i0(1,2,1) -> 2*
    i0(2,1,1) -> 2*
    i0(1,2,2) -> 2*
    i0(2,1,2) -> 2*
    a0() -> 1*
    b0() -> 1*
    b'0() -> 1*
    c0() -> 1*
    d0() -> 1*
    if0(1,1,1) -> 1*
    if0(2,2,1) -> 1*
    if0(1,1,2) -> 1*
    if0(2,2,2) -> 1*
    if0(1,2,1) -> 1*
    if0(2,1,1) -> 1*
    if0(1,2,2) -> 1*
    if0(2,1,2) -> 1*
    e0() -> 1*
    .0(1,2) -> 1*
    .0(2,1) -> 1*
    .0(1,1) -> 1*
    .0(2,2) -> 1*
    d'0() -> 1*
    h0(1,2) -> 1*
    h0(2,1) -> 1*
    h0(1,1) -> 1*
    h0(2,2) -> 1*
  problem:
   
  Qed