YES(?,O(n^1)) 0.15/0.21 YES(?,O(n^1)) 0.15/0.21 0.15/0.21 Problem: 0.15/0.21 app(app(app(uncurry(),f),x),y) -> app(app(f,x),y) 0.15/0.21 0.15/0.21 Proof: 0.15/0.21 Bounds Processor: 0.15/0.21 bound: 1 0.15/0.21 enrichment: match 0.15/0.21 automaton: 0.15/0.21 final states: {2,1} 0.15/0.21 transitions: 0.15/0.21 app1(5,1) -> 5,1 0.15/0.21 app1(1,2) -> 5* 0.15/0.21 app1(2,1) -> 5* 0.15/0.21 app1(5,2) -> 5,1 0.15/0.21 app1(1,1) -> 5* 0.15/0.21 app1(2,2) -> 5* 0.15/0.21 app0(1,2) -> 1* 0.15/0.21 app0(2,1) -> 1* 0.15/0.21 app0(1,1) -> 1* 0.15/0.21 app0(2,2) -> 1* 0.15/0.21 uncurry0() -> 2* 0.15/0.21 problem: 0.15/0.21 0.15/0.21 Qed 0.15/0.22 EOF