| Example | State | Remark |
|---|---|---|
| Binary search | DONE | |
| Factorial | DONE | |
| Find | DONE | |
| Find first | DONE | |
| Find quatuor | DONE | |
| Maximum elimination | DONE | |
| Sum | DONE | Require option -wp-rte |
| Voting | WP | A relational property remains unproven (waiting for a RPP feature) |
| Inserion sort | DONE | |
| Insertion sort swap | DONE | |
| Selection sort | DONE | |
| Bubblesort | DONE | |
| Quicksort | TODO | |
| Heapsort | TODO |