YES(?,O(n^1))

Problem:
 f(a(),b()) -> f(a(),c())
 f(c(),d()) -> f(b(),d())

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6}
   transitions:
    f1(10,9) -> 6*
    b1() -> 10*
    d1() -> 9*
    a1() -> 10*
    c1() -> 9*
    f0(6,6) -> 6*
    a0() -> 6*
    b0() -> 6*
    c0() -> 6*
    d0() -> 6*
  problem:
   
  Qed