YES(?,O(n^1)) 0.15/0.20 YES(?,O(n^1)) 0.15/0.20 0.15/0.20 Problem: 0.15/0.20 rev(ls) -> r1(ls,empty()) 0.15/0.20 r1(empty(),a) -> a 0.15/0.20 r1(cons(x,k),a) -> r1(k,cons(x,a)) 0.15/0.20 0.15/0.20 Proof: 0.15/0.20 Bounds Processor: 0.15/0.20 bound: 1 0.15/0.20 enrichment: match 0.15/0.20 automaton: 0.15/0.20 final states: {4,3} 0.15/0.20 transitions: 0.15/0.20 r11(1,10) -> 4* 0.15/0.20 r11(2,5) -> 3* 0.15/0.20 r11(2,7) -> 4* 0.15/0.20 r11(1,5) -> 3* 0.15/0.20 r11(1,7) -> 4* 0.15/0.20 r11(2,10) -> 4* 0.15/0.20 cons1(1,2) -> 7* 0.15/0.20 cons1(1,10) -> 7* 0.15/0.20 cons1(2,1) -> 7* 0.15/0.20 cons1(2,5) -> 5* 0.15/0.20 cons1(2,7) -> 7* 0.15/0.20 cons1(1,1) -> 7* 0.15/0.20 cons1(1,5) -> 5* 0.15/0.20 cons1(1,7) -> 7* 0.15/0.20 cons1(2,2) -> 10* 0.15/0.20 cons1(2,10) -> 7* 0.15/0.20 empty1() -> 5* 0.15/0.20 rev0(2) -> 3* 0.15/0.20 rev0(1) -> 3* 0.15/0.20 r10(1,2) -> 4* 0.15/0.20 r10(2,1) -> 4* 0.15/0.20 r10(1,1) -> 4* 0.15/0.20 r10(2,2) -> 4* 0.15/0.20 empty0() -> 1* 0.15/0.20 cons0(1,2) -> 2* 0.15/0.20 cons0(2,1) -> 2* 0.15/0.20 cons0(1,1) -> 2* 0.15/0.20 cons0(2,2) -> 2* 0.15/0.20 1 -> 4* 0.15/0.20 2 -> 4* 0.15/0.20 5 -> 3* 0.15/0.20 7 -> 4* 0.15/0.20 10 -> 4* 0.15/0.20 problem: 0.15/0.20 0.15/0.20 Qed 0.15/0.21 EOF