YES(?,O(n^1)) Problem: f(nil()) -> nil() f(.(nil(),y)) -> .(nil(),f(y)) f(.(.(x,y),z)) -> f(.(x,.(y,z))) g(nil()) -> nil() g(.(x,nil())) -> .(g(x),nil()) g(.(x,.(y,z))) -> g(.(.(x,y),z)) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {4,3} transitions: g1(12) -> 14* g1(7) -> 14* g1(2) -> 14* g1(16) -> 14,4 g1(1) -> 14* .1(2,12) -> 8* .1(3,5) -> 5,3 .1(16,2) -> 16* .1(1,2) -> 7* .1(1,8) -> 8* .1(1,12) -> 8* .1(12,1) -> 16* .1(7,1) -> 16* .1(2,1) -> 7* .1(2,7) -> 8* .1(14,3) -> 14,4 .1(16,1) -> 16* .1(1,1) -> 12* .1(1,7) -> 8* .1(12,2) -> 16* .1(7,2) -> 16* .1(2,2) -> 7* .1(2,8) -> 8* nil1() -> 14,5,4,3 f1(12) -> 5* f1(7) -> 5* f1(2) -> 5* f1(1) -> 5* f1(8) -> 5,3 f0(2) -> 3* f0(1) -> 3* nil0() -> 1* .0(1,2) -> 2* .0(2,1) -> 2* .0(1,1) -> 2* .0(2,2) -> 2* g0(2) -> 4* g0(1) -> 4* problem: Qed