YES(?,O(n^1)) 0.16/0.22 YES(?,O(n^1)) 0.16/0.22 0.16/0.22 Problem: 0.16/0.22 +(+(x,y),z) -> +(x,+(y,z)) 0.16/0.22 +(f(x),f(y)) -> f(+(x,y)) 0.16/0.22 +(f(x),+(f(y),z)) -> +(f(+(x,y)),z) 0.16/0.22 0.16/0.22 Proof: 0.16/0.22 Bounds Processor: 0.16/0.22 bound: 1 0.16/0.22 enrichment: match 0.16/0.22 automaton: 0.16/0.22 final states: {2} 0.16/0.22 transitions: 0.16/0.22 f1(4) -> 4,2 0.16/0.22 +1(1,1) -> 4* 0.16/0.22 +0(1,1) -> 2* 0.16/0.22 f0(1) -> 1* 0.16/0.22 problem: 0.16/0.22 0.16/0.22 Qed 0.16/0.22 EOF