YES(?,O(n^1)) 0.15/0.20 YES(?,O(n^1)) 0.15/0.21 0.15/0.21 Problem: 0.15/0.21 first(0(),X) -> nil() 0.15/0.21 first(s(X),cons(Y)) -> cons(Y) 0.15/0.21 from(X) -> cons(X) 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: {6,5} 0.15/0.21 transitions: 0.15/0.21 cons1(2) -> 6,5 0.15/0.21 cons1(4) -> 6,5 0.15/0.21 cons1(1) -> 6,5 0.15/0.21 cons1(3) -> 6,5 0.15/0.21 nil1() -> 5* 0.15/0.21 first0(3,1) -> 5* 0.15/0.21 first0(3,3) -> 5* 0.15/0.21 first0(4,2) -> 5* 0.15/0.21 first0(4,4) -> 5* 0.15/0.21 first0(1,2) -> 5* 0.15/0.21 first0(1,4) -> 5* 0.15/0.21 first0(2,1) -> 5* 0.15/0.21 first0(2,3) -> 5* 0.15/0.21 first0(3,2) -> 5* 0.15/0.21 first0(3,4) -> 5* 0.15/0.21 first0(4,1) -> 5* 0.15/0.21 first0(4,3) -> 5* 0.15/0.21 first0(1,1) -> 5* 0.15/0.21 first0(1,3) -> 5* 0.15/0.21 first0(2,2) -> 5* 0.15/0.21 first0(2,4) -> 5* 0.15/0.21 00() -> 1* 0.15/0.21 nil0() -> 2* 0.15/0.21 s0(2) -> 3* 0.15/0.21 s0(4) -> 3* 0.15/0.21 s0(1) -> 3* 0.15/0.21 s0(3) -> 3* 0.15/0.21 cons0(2) -> 4* 0.15/0.21 cons0(4) -> 4* 0.15/0.21 cons0(1) -> 4* 0.15/0.21 cons0(3) -> 4* 0.15/0.21 from0(2) -> 6* 0.15/0.21 from0(4) -> 6* 0.15/0.21 from0(1) -> 6* 0.15/0.21 from0(3) -> 6* 0.15/0.21 problem: 0.15/0.21 0.15/0.21 Qed 0.15/0.21 EOF