The file testcases.tar.gz contains source code files w.r.t. 64 test cases carried out for this thesis. It also contains log files that contain output of these test cases. The latter are also contained in the file Appendix.pdf, which serves as an on-line appendix for the thesis. Other sources which are of importance for the thesis can be found in https://doi.org/10.5281/zenodo.3517081. Three proof files have been re-established for the purpose of describing these proofs in the thesis. Thus: they deviate from the ones that can be found in https://doi.org/10.5281/zenodo.3517081. These three can be found in the file "Three renewed proof files.zip". It concerns proof files for lastIndexOf(Object), linkFirst(Object), and addFirst(Object). https://doi.org/10.5281/zenodo.3517081 is a link that has been created to store artefacts w.r.t. a paper for the TACAS conference in April 2020 in Dublin, Ireland. The paper carries the same title as this thesis.