Adding Decision Procedures to SMT Solvers Using Axioms with Triggers

Satisfiability modulo theories (SMT) solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns, also known as triggers. Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a feature-rich axiomatization of doubly-linked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doubly-linked lists and sets.

1. These three hypothesis are not needed to apply T -Backjump. Still, to implement conflict analysis, we want to make j as small as possible.

2. http://bware.lri.fr/index.php/BWare_project.

We would like to thank the anonymous reviewers for their careful reading of our article, as well as their helpful comments which greatly contributed to the quality of this paper. This work is partially supported by the BWare Project (ANR-12-INSE-0010, http://bware.lri.fr/) and the Joint Laboratory ProofInUse (ANR-13-LAB3-0007, http://www.spark-2014.org/proofinuse) of the French national research organization.

Authors and Affiliations

1. LRI, CNRS, Université Paris-Sud 11, 91405, Orsay, France

   Claire Dross, Sylvain Conchon & Andrei Paskevich

2. Toccata, INRIA Saclay-Île de France, 91893, Orsay, France

   Claire Dross, Sylvain Conchon & Andrei Paskevich

3. AdaCore, 75009, Paris, France

   Claire Dross & Johannes Kanig

Corresponding author

Correspondence to Claire Dross.

Appendix: Axiomatization of Imperative Doubly-Linked Lists

• length_gte_zero:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list. [length(l)] length(l)\ge 0\end{array} \end{aligned}$$

• is_empty:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list. [is\_empty(l)] is\_empty(l)\approx {\mathtt {t}}\leftrightarrow length(l)\approx 0\end{array} \end{aligned}$$

• empty_is_empty:

  $$\begin{aligned} \begin{array}{l} is\_empty(empty)\end{array} \end{aligned}$$

• equal_elements_refl:

  $$\begin{aligned} \forall e{:}\,element\_type. [equal\_elements(e,e)]equal\_elements(e,e)\approx {\mathtt {t}} \end{aligned}$$

• equal_elements_sym:

  $$\begin{aligned} \begin{array}{l}\forall e_1 e_2{:}\,element\_type. [equal\_elements(e_1,e_2)]\\ equal\_elements(e_1,e_2)\approx equal\_elements(e_2,e_1)\end{array} \end{aligned}$$

• equal_elements_trans:

  $$\begin{aligned} \begin{array}{l}\forall e_1 e_2 e_3{:}\,element\_type. [equal\_elements(e_1,e_2), equal\_elements(e_2,e_3)]\\ equal\_elements(e_1,e_2)\approx {\mathtt {t}}\rightarrow equal\_elements(e_2, e_3)\approx {\mathtt {t}}\rightarrow {}\\ equal\_elements(e_1,e_3)\approx {\mathtt {t}}\\ \forall e_1 e_2 e_3{:}\,element\_type. [equal\_elements(e_1,e_2), equal\_elements(e_1,e_3)]\\ equal\_elements(e_1,e_2)\approx {\mathtt {t}}\rightarrow equal\_elements(e_2, e_3)\approx {\mathtt {t}}\rightarrow {}\\ equal\_elements(e_1,e_3)\approx {\mathtt {t}}\end{array} \end{aligned}$$

• position_gte_zero:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list, c{:}\,cursor. [position(l, c)]\\ length(l)\ge position(l,c)\wedge position(l,c)\ge 0\end{array} \end{aligned}$$

• positionno_element:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list. [position(l,no\_element)]position(l,no\_element)\approx 0\end{array} \end{aligned}$$

• position_eq:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list, c_1 c_2{:}\,cursor. [position(l,c_1),position(l,c_2)]\\ position(l,c_1)> 0\rightarrow position(l,c_1)\approx position(l,c_2)\rightarrow c_1\approx c_2\end{array} \end{aligned}$$

• previous_in:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list, c{:}\,cursor. [previous(l,c)]\\ (position(l,c)> 1\vee position(l,previous(l,c))> 0)\rightarrow {}\\ position(l,previous(l,c))\approx position(l,c)-1 \end{array} \end{aligned}$$

• previous_ext:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list, c{:}\,cursor. [previous(l,c)]\\ (position(l,c)\approx 1\vee c\approx no\_element)\rightarrow previous(l,c)\approx no\_element \end{array} \end{aligned}$$

• next_in:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list, c{:}\,cursor. [next(l,c)]\\ (length(l)>position(l,c)>0\vee position(l,next(l,c))> 0)\rightarrow {}\\ position(l,next(l,c))\approx position(l,c)+1 \end{array} \end{aligned}$$

• next_ext:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list, c{:}\,cursor. [next(l,c)]\\ (position(l,c)\approx length(l)\vee c\approx no\_element)\rightarrow next(l,c)\approx no\_element \end{array} \end{aligned}$$

• last_empty:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list. [last(l)]length(l)\approx 0\leftrightarrow last(l)\approx no\_element \end{array} \end{aligned}$$

• last_gen:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list. [last(l)]length(l)\approx position(l,last(l)) \end{array} \end{aligned}$$

• first_empty:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list. [first(l)]length(l)\approx 0\leftrightarrow first(l)\approx no\_element \end{array} \end{aligned}$$

• first_gen:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list. [first(l)]length(l)>0\rightarrow position(l,first(l))\approx 1 \end{array} \end{aligned}$$

• has_element_def:

  $$\begin{aligned} \begin{array}{l} \forall l{:}\,list, c{:}\,cursor. [has\_element(l,c)]position(l,c)>0\leftrightarrow has\_element(l,c)\approx {\mathtt {t}} \end{array} \end{aligned}$$

• left_no_element:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list. [left(l,no\_element)]left(l,no\_element)\approx l \end{array} \end{aligned}$$

• left_length:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, c{:}\,cursor. [left(l,c)]\\ position(l,c)>0\rightarrow length(left(l,c))\approx position(l,c) - 1\end{array} \end{aligned}$$

• left_position_in:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, c_1 c_2{:}\,cursor.[position(left(l,c_1),c_2)]\\ (position(left(l,c_1),c_2)>0\vee position(l,c_2)<position(l,c_1))\rightarrow {}\\ position(left(l,c_1),c_2)\approx position(l,c_2)\\ \forall l{:}\,list, c_1 c_2{:}\,cursor.[left(l,c_1),position(l,c_2)]\\ (position(left(l,c_1),c_2)>0\vee position(l,c_2)<position(l,c_1))\rightarrow {}\\ position(left(l,c_1),c_2)\approx position(l,c_2)\end{array} \end{aligned}$$

• left_position_ext:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, c_1 c_2{:}\,cursor.[position(left(l,c_1),c_2)]\\ position(l,c_2)\ge position(l,c_1))>0\rightarrow {}\\ position(left(l,c_1),c_2)\approx 0\end{array} \end{aligned}$$

• left_element:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, c_1 c_2{:}\,cursor.[element(left(l,c_1),c_2)]\\ (position(left(l,c_1),c_2)>0\vee 0<position(l,c_2)<position(l,c_1))\rightarrow {}\\ element(left(l,c_1),c_2)\approx element(l,c_2)\\ \forall l{:}\,list, c_1 c_2{:}\,cursor.[left(l,c_1),element(l,c_2)]\\ (position(left(l,c_1),c_2)>0\vee 0<position(l,c_2)<position(l,c_1))\rightarrow {}\\ element(left(l,c_1),c_2)\approx element(l,c_2)\end{array} \end{aligned}$$

• right_no_element:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list. [right(l,no\_element)]right(l,no\_element)\approx empty\end{array} \end{aligned}$$

• right_length:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, c{:}\,cursor. [right(l,c)]\\ position(l,c)>0\rightarrow length(right(l,c))\approx length(l) - position(l,c) + 1\end{array} \end{aligned}$$

• right_position_in:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, c_1 c_2{:}\,cursor.[position(right(l,c_1),c_2)]\\ (position(right(l,c_1),c_2)>0\vee 0<position(l,c_1)\le position(l,c_2))\rightarrow {}\\ position(right(l,c_1),c_2)\approx position(l,c_2) - position(l,c_1) + 1\\ \forall l{:}\,list, c_1 c_2{:}\,cursor.[right(l,c_1),position(l,c_2)]\\ (position(right(l,c_1),c_2)>0\vee 0<position(l,c_1)\le position(l,c_2))\rightarrow {}\\ position(right(l,c_1),c_2)\approx position(l,c_2) - position(l,c_1) + 1\end{array} \end{aligned}$$

• right_position_ext:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, c_1 c_2{:}\,cursor.[position(right(l,c_1),c_2)]\\ position(l,c_2)< position(l,c_1))\rightarrow {}\\ position(right(l,c_1),c_2)\approx 0\end{array} \end{aligned}$$

• right_element:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, c_1 c_2{:}\,cursor.[element(right(l,c_1),c_2)]\\ (position(right(l,c_1),c_2)>0\vee 0<position(l,c_1)\le position(l,c_2))\rightarrow {}\\ element(right(l,c_1),c_2)\approx element(l,c_2)\\ \forall l{:}\,list, c_1 c_2{:}\,cursor.[right(l,c_1),element(l,c_2)]\\ (position(right(l,c_1),c_2)>0\vee 0<position(l,c_1)\le position(l,c_2))\rightarrow {}\\ element(right(l,c_1),c_2)\approx element(l,c_2)\end{array} \end{aligned}$$

• find_first_range:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, e{:}\,element\_type. [find\_first(l,e)]\\ find\_first(l,e)\approx no\_element\vee position(l,find\_first(l,e))>0\end{array} \end{aligned}$$

• find_first_not:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, e{:}\,element\_type, c : cursor.[find\_first(l,e),element(l,c)]\\ find\_first(l,e)\approx no\_element\rightarrow position(l,c)>0\rightarrow {}\\ equal\_elements(element(l,c),e)\not \approx {\mathtt {t}}\end{array} \end{aligned}$$

• find_first_first:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, e{:}\,element\_type, c : cursor.[find\_first(l,e),element(l,c)]\\ 0<position(l,c)<position(l,find\_first(l,e))\rightarrow {}\\ equal\_elements(element(l,c),e)\not \approx {\mathtt {t}}\end{array} \end{aligned}$$

• find_first_element:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, e{:}\,element\_type.[find\_first(l,e)]0<position(l,find\_first(l,e))\rightarrow {}\\ equal\_elements(element(l,find\_first(l,e)),e)\approx {\mathtt {t}}\end{array} \end{aligned}$$

• contains_def:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, e{:}\,element\_type.[contains(l,e)]\\ contains(l,e)\leftrightarrow 0<position(l,find\_first(l,e))\end{array} \end{aligned}$$

• find_first:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, e{:}\,element\_type.[find(l,e,no\_element)]\\ find(l,e,no\_element)\approx find\_first(l,e)\end{array} \end{aligned}$$

• find_others:

  $$\begin{aligned} \begin{array}{l}\forall l{:}\,list, e{:}\,element\_type, c{:}\,cursor.[find(l,e,c)]\\ position(l,c)>0\rightarrow find(l,e,c)\approx find\_first(right(l,c),e)\end{array} \end{aligned}$$

• replace_element_range:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[replace\_element(l_1,c,e,l_2)]\\ replace\_element(l_1,c,e,l_2)\approx {\mathtt {t}}\rightarrow position(l_1,c)>0\end{array} \end{aligned}$$

• replace_element_length:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[replace\_element(l_1,c,e,l_2)]\\ replace\_element(l_1,c,e,l_2)\approx {\mathtt {t}}\rightarrow length(l_1)\approx length(l_2)\end{array} \end{aligned}$$

• replace_element_position:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[replace\_element(l_1,c_1,e,l_2),\\ position(l_1,c_2]\\ replace\_element(l_1,c_1,e,l_2)\approx {\mathtt {t}}\rightarrow position(l_1,c_2)\approx position(l_2,c_2)\\ \forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[replace\_element(l_1,c_1,e,l_2),\\ position(l_2,c_2]\\ replace\_element(l_1,c_1,e,l_2)\approx {\mathtt {t}}\rightarrow position(l_1,c_2)\approx position(l_2,c_2)\end{array} \end{aligned}$$

• replace_element_element_in:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[replace\_element(l_1,c,e,l_2)]\\ replace\_element(l_1,c,e,l_2)\approx {\mathtt {t}}\rightarrow element(l_2,c)\approx e\end{array} \end{aligned}$$

• replace_element_element_ext:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[replace\_element(l_1,c_1,e,l_2),\\ element(l_1,c_2)]\\ (replace\_element(l_1,c_1,e,l_2)\approx {\mathtt {t}}\wedge position(l_1,c_2)>0\wedge c_1\not \approx c_2)\rightarrow {}\\ element(l_1,c_2)\approx element(l_2,c_2)\\ \forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[replace\_element(l_1,c_1,e,l_2),\\ element(l_2,c_2)]\\ (replace\_element(l_1,c_1,e,l_2)\approx {\mathtt {t}}\wedge position(l_1,c_2)>0\wedge c_1\not \approx c_2)\rightarrow {}\\ element(l_1,c_2)\approx element(l_2,c_2)\end{array} \end{aligned}$$

• insert_range:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[insert(l_1,c,e,l_2)]\\ insert(l_1,c,e,l_2)\approx {\mathtt {t}}\rightarrow c\approx no\_element\vee position(l_1,c)>0\end{array} \end{aligned}$$

• insert_length:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[insert(l_1,c,e,l_2)]\\ insert(l_1,c,e,l_2)\approx {\mathtt {t}}\rightarrow length(l_2)\approx length(l_1)+1\end{array} \end{aligned}$$

• insert_new:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[insert(l_1,c,e,l_2)]\\ (insert(l_1,c,e,l_2)\approx {\mathtt {t}}\wedge position(l_1,c)>0)\rightarrow {}\\ position(l_1,previous(l_2,c))\approx 0\wedge element(l_2,previous(l_2,c))\approx e\end{array} \end{aligned}$$

• insert_new_no_element:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[insert(l_1,no\_element,e,l_2)]\\ insert(l_1,no\_element,e,l_2)\approx {\mathtt {t}}\rightarrow {}\\ position(l_1,last(l_2))\approx 0\wedge element(l_2,last(l_2))\approx e\end{array} \end{aligned}$$

• insert_position_before:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[insert(l_1,c_1,e,l_2),position(l_1,c_2)]\\ (insert(l_1,c_1,e,l_2)\approx {\mathtt {t}}\wedge 0<position(l_1,c_2)<position(l_1,c_1))\rightarrow {}\\ position(l_1,c_2)\approx position(l_2,c_2)\\ \forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[insert(l_1,c_1,e,l_2),position(l_2,c_2)]\\ (insert(l_1,c_1,e,l_2)\approx {\mathtt {t}}\wedge position(l_2,c_2)<position(l_1,c_1))\rightarrow {}\\ position(l_1,c_2)\approx position(l_2,c_2)\end{array} \end{aligned}$$

• insert_position_after:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[insert(l_1,c_1,e,l_2),position(l_1,c_2)]\\ (insert(l_1,c_1,e,l_2)\approx {\mathtt {t}}\wedge position(l_1,c_2)\ge position(l_1,c_1)>0)\rightarrow {}\\ position(l_1,c_2)+1\approx position(l_2,c_2)\\ \forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[insert(l_1,c_1,e,l_2),position(l_2,c_2)]\\ (insert(l_1,c_1,e,l_2)\approx {\mathtt {t}}\wedge position(l_2,c_2)>position(l_1,c_1)>0)\rightarrow {}\\ position(l_1,c_2)+1\approx position(l_2,c_2)\end{array} \end{aligned}$$

• insert_position_no_element:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[insert(l_1,no\_element,e,l_2),position(l_1,c)]\\ (insert(l_1,no\_element,e,l_2)\approx {\mathtt {t}}\wedge position(l_1,c)>0)\rightarrow {}\\ position(l_1,c)\approx position(l_2,c)\\ \forall l_1 l_2{:}\,list, c{:}\,cursor, e{:}\,element\_type .[insert(l_1,no\_element,e,l_2),position(l_2,c)]\\ (insert(l_1,no\_element,e,l_2)\approx {\mathtt {t}}\wedge position(l_2,c_2)<length(l_2))\rightarrow {}\\ position(l_1,c)\approx position(l_2,c)\end{array} \end{aligned}$$

• insert_element:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[insert(l_1,c_1,e,l_2),element(l_1,c_2)]\\ (insert(l_1,c_1,e,l_2)\approx {\mathtt {t}}\wedge position(l_1,c_2)>0)\rightarrow {}\\ element(l_1,c_2)\approx element(l_2,c_2)\\ \forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor, e{:}\,element\_type .[insert(l_1,c_1,e,l_2),element(l_2,c_2)]\\ (insert(l_1,c_1,e,l_2)\approx {\mathtt {t}}\wedge position(l_1,c_2)>0)\rightarrow {}\\ element(l_1,c_2)\approx element(l_2,c_2)\end{array} \end{aligned}$$

• delete_range:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor .[delete(l_1,c,l_2)]\\ delete(l_1,c,l_2)\approx {\mathtt {t}}\rightarrow position(l_1,c)>0\end{array} \end{aligned}$$

• delete_length:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor .[delete(l_1,c,l_2)]\\ delete(l_1,c,l_2)\approx {\mathtt {t}}\rightarrow length(l_2)+1\approx length(l_1)\end{array} \end{aligned}$$

• delete_position_before:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor .[delete(l_1,c_1,l_2),position(l_1,c_2)]\\ (delete(l_1,c_1,l_2)\approx {\mathtt {t}}\wedge position(l_1,c_2)<position(l_1,c_1))\rightarrow {}\\ position(l_1,c_2)\approx position(l_2,c_2)\\ \forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor .[delete(l_1,c_1,l_2),position(l_2,c_2)]\\ (delete(l_1,c_1,l_2)\approx {\mathtt {t}}\wedge 0<position(l_2,c_2)<position(l_1,c_1))\rightarrow {}\\ position(l_1,c_2)\approx position(l_2,c_2)\end{array} \end{aligned}$$

• delete_position_after:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor .[delete(l_1,c_1,l_2),position(l_1,c_2)]\\ (delete(l_1,c_1,l_2)\approx {\mathtt {t}}\wedge position(l_1,c_2)>position(l_1,c_1))\rightarrow {}\\ position(l_1,c_2)\approx position(l_2,c_2)+1\\ \forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor .[delete(l_1,c_1,l_2),position(l_2,c_2)]\\ (delete(l_1,c_1,l_2)\approx {\mathtt {t}}\wedge position(l_2,c_2)\ge position(l_1,c_1))\rightarrow {}\\ position(l_1,c_2)\approx position(l_2,c_2)+1\end{array} \end{aligned}$$

• delete_position_next:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c{:}\,cursor .[delete(l_1,c,l_2)]delete(l_1,c,l_2)\approx {\mathtt {t}}\rightarrow \langle next(l_1, c)\rangle {\mathtt {t}}\end{array} \end{aligned}$$

• delete_element:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list, c_1 c_2{:}\,cursor .[delete(l_1,c_1,l_2),element(l_1,c_2)]\\ (delete(l_1,c,l_2)\approx {\mathtt {t}}\wedge position(l_2,c_2)>0)\rightarrow {}\\ element(l_1,c_2)=element(l_2,c_2)\end{array} \end{aligned}$$

• equal_lists_position:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list .[equal\_lists(l_1,l_2)]equal\_lists(l_1,l_2)\approx {\mathtt {t}}\rightarrow {}\\ (\forall c{:}\,cursor. [position(l_1, c)] position(l_1, c)\approx position(l_2, c))\wedge {}\\ (\forall c{:}\,cursor. [position(l_2, c)] position(l_1, c)\approx position(l_2, c))\end{array} \end{aligned}$$

• equal_lists_element:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list .[equal\_lists(l_1,l_2)]equal\_lists(l_1,l_2)\approx {\mathtt {t}}\rightarrow {}\\ (\forall c{:}\,cursor. [element(l_1, c)] position(l_1, c)>0\rightarrow \\ element(l_1,c)\approx element(l_2, c))\wedge {}\\ (\forall c{:}\,cursor. [element(l_2, c)] position(l_1, c)>0\rightarrow \\ element(l_1,c)\approx element(l_2, c))\end{array} \end{aligned}$$

• equal_lists_inv:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list .[equal\_lists(l_1,l_2)]equal\_lists(l_1,l_2)\not \approx {\mathtt {t}}\rightarrow {}\\ (\exists c{:}\,cursor. position(l_1,c)>0\wedge {}\\ (position(l_1,c)\approx position (l_2,c)\rightarrow element(l_1,c)\not \approx element(l_2, c)))\end{array} \end{aligned}$$

• equal_lists_length:

  $$\begin{aligned} \begin{array}{l}\forall l_1 l_2{:}\,list .[equal\_lists(l_1,l_2)]equal\_lists(l_1,l_2)\approx {\mathtt {t}}\rightarrow length(l_1)\approx length(l_2)\end{array} \end{aligned}$$

Reprints and permissions