diff --git a/Paper/biblio.bib b/Paper/biblio.bib
deleted file mode 100644
index 5b28438c41852551dbf209908202afa110341e53..0000000000000000000000000000000000000000
--- a/Paper/biblio.bib
+++ /dev/null
@@ -1,553 +0,0 @@
-@string{lnai = "Lecture Notes in Artificial Intelligence"}
-@string{lncs = "Lecture Notes in Computer Science"}
-@string{sldct ="Synthesis Lectures on Distributed Computing Theory"}
-@string{lipics = "Leibniz International Proceedings in Informatics (LIPIcs)"}
-
-@string{ahn  = "Ad-Hoc Networks"}
-@string{cacm  = "Communications of the ACM"}
-@string{dc    = "Distributed Computing"}
-@string{entcs  = "Electronic Notes in Theoretical Computer Science"}
-@string{fac    = "Formal Aspects of Computing"}
-@string{ieeetpds = "IEEE Transactions on Parallel and Distributed Systems"}
-@string{ijfcs  = "International Journal of Foundations of Computer Science"}
-@string{ijpp   = "International Journal of Parallel Programming"}
-@string{infsoc = "International Journal of Informatics Society"}
-@string{ipl    = "Information Processing Letters"}
-@string{jar    = "Journal of Automated Reasoning"}
-@string{jfp    = "Journal of Functional Programming"}
-@string{jlp    = "Journal of Logic Programming"}
-@string{jsc    = "Journal of Symbolic Computation"}
-@string{jlap   = "Journal of Logic and Algebraic Programming"}
-@string{lmcs   = "Logical Methods in Computer Science"}
-@string{mna    = "Mobile Networks and Applications"}
-@string{ppl    = "Parallel Processing Letters"}
-@string{scp = "Science of Computer Programming"}  		  
-@string{siu = "Studia Informatica Universalis"}  		  
-@string{siamjc = "SIAM Journal of Computing"}
-@string{tcs    = "Theoretical Computer Science"}
-@string{tocs = "Theory of Computing Systems"}
-@string{toplas = "ACM Transactions on Programming Languages and Systems"}
-@string{un = "L'Usine Nouvelle"}
-
-@string{ACM = "ACM Press"}
-@string{AP = "Academic Press"}
-@string{CUP = "Cambridge University Press"}
-@string{Dagstuhl = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik"}
-@string{Elsevier = "Elsevier"}
-@string{IEEECS = "IEEE Computer Society"}
-@string{MC = "Morgan {\&} Claypool Publishers"}
-@string{SV = "Springer-Verlag"}
-@string{SN = "Springer Nature"}
-
-@string{CEDRIC = "Cédric"}
-
-@article{balabonskiArxiv21,
-  author    = {Thibaut Balabonski and
-               Pierre Courtieu and
-               Robin Pelle and
-               Lionel Rieg and
-               S{\'{e}}bastien Tixeuil and
-               Xavier Urbain},
-  title     = {Computer Aided Formal Design of Swarm Robotics Algorithms},
-  journal   = {CoRR},
-  volume    = {abs/2101.06966},
-  year      = {2021},
-  url       = {https://arxiv.org/abs/2101.06966},
-  eprinttype = {arXiv},
-  eprint    = {2101.06966},
-  timestamp = {Fri, 22 Jan 2021 15:16:00 +0100},
-  biburl    = {https://dblp.org/rec/journals/corr/abs-2101-06966.bib},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@proceedings{DBLP:conf/sofl/2016,
-	Bibsource = {dblp computer science bibliography, http://dblp.org},
-	Biburl = {http://dblp.uni-trier.de/rec/bib/conf/sofl/2016},
-	Doi = {10.1007/978-3-319-57708-1},
-	Isbn = {978-3-319-57707-4},
-	Series = lncs,
-	Timestamp = {Fri, 21 Apr 2017 14:45:47 +0200},
-	Title = {Structured Object-Oriented Formal Language and Method - 6th International Workshop, {SOFL+MSVL}, Revised Selected Papers},
-	Url = {http://dx.doi.org/10.1007/978-3-319-57708-1},
-	Volume = {10189},
-	Year = {2017},
-	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-319-57708-1}}
-
-
-@inproceedings{doan16sofl,
-	Author = {Ha Thi Thu Doan and Fran{\c{c}}ois Bonnet and Kazuhiro Ogata},
-	Bibsource = {dblp computer science bibliography, http://dblp.org},
-	Biburl = {http://dblp.uni-trier.de/rec/bib/conf/sofl/DoanBO16},
-        Crossref = {sofl2016},
-	Doi = {10.1007/978-3-319-57708-1\_12},
-	Pages = {201--219},
-	Timestamp = {Fri, 21 Apr 2017 14:46:40 +0200},
-	Title = {Model Checking of a Mobile Robots Perpetual Exploration Algorithm},
-	Year = {2016},
-	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-319-57708-1\_12}}
-
-
-@inproceedings{altisen16forte,
-  author    = {Karine Altisen and
-               Pierre Corbineau and
-               St{\'{e}}phane Devismes},
-  editor    = {Elvira Albert and
-               Ivan Lanese},
-  title     = {A Framework for Certified Self-Stabilization},
-  booktitle = {Formal Techniques for Distributed Objects, Components, and Systems
-               - 36th {IFIP} {WG} 6.1 International Conference, {FORTE} 2016, Held
-               as Part of the 11th International Federated Conference on Distributed
-               Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June
-               6-9, 2016, Proceedings},
-  series    = lncs,
-  volume    = {9688},
-  pages     = {36--51},
-  publisher = SV,
-  year      = {2016},
-  doi       = {10.1007/978-3-319-39570-8\_3},
-  timestamp = {Mon, 23 May 2016 14:44:36 +0200},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/forte/AltisenCD16},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-
-@InProceedings{auger13sss,
-  author = 	 {C\'edric Auger and Zohir Bouzid and Pierre Courtieu and S\'ebastien Tixeuil and Xavier Urbain},
-  title = 	 {{Certified Impossibility Results for Byzantine-Tolerant Mobile Robots}},
-  crossref =  {sss13},
-  pages = 	 {178--186},
-  year = 	 {2013},
-  doi = {10.1007/978-3-319-03089-0\_13},
-  ee = {http://dx.doi.org/10.1007/978-3-319-03089-0\_13}
-}
-
-@inproceedings{balabonski18icdcn,
-  author    = {Thibaut Balabonski and
-               Robin Pelle and
-               Lionel Rieg and
-               S{\'{e}}bastien Tixeuil},
-  editor    = {Paolo Bellavista and
-               Vijay K. Garg},
-  title     = {A Foundational Framework for Certified Impossibility Results with
-               Mobile Robots on Graphs},
-  booktitle = {Proceedings of the 19th International Conference on Distributed Computing
-               and Networking, {ICDCN} 2018, Varanasi, India, January 4-7, 2018},
-  pages     = {5:1--5:10},
-  publisher = {{ACM}},
-  year      = {2018},
-  doi       = {10.1145/3154273.3154321},
-  timestamp = {Tue, 06 Nov 2018 11:07:44 +0100},
-  biburl    = {https://dblp.org/rec/bib/conf/icdcn/BalabonskiPRT18},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@Article{balabonski19tocs,
-  author = 	 {Thibaut Balabonski and Amélie Delga and Lionel Rieg and Sébastien Tixeuil and Xavier Urbain},
-  title = 	 {Synchronous Gathering without Multiplicity Detection: A Certified Algorithm},
-  journal = 	 tocs,
-  year = 	 {2019},
-  doi =          {10.1007/s00224-017-9828-z},
-}
-
-@inproceedings{balabonski2019netys,
-author    = {Thibaut Balabonski and
-               Pierre Courtieu and
-               Robin Pelle and
-               Lionel Rieg and
-               S{\'{e}}bastien Tixeuil and
-               Xavier Urbain},
-  editor    = {Mohamed Faouzi Atig and
-               Alexander A. Schwarzmann},
-  title     = {Continuous vs. Discrete Asynchronous Moves: {A} Certified Approach
-               for Mobile Robots},
-  booktitle = {Networked Systems - 7th International Conference, {NETYS} 2019, Marrakech,
-               Morocco, June 19-21, 2019, Revised Selected Papers},
-  series    = lncs,
-  volume    = {11704},
-  pages     = {93--109},
-  publisher = SV,
-  year      = {2019},
-  doi       = {10.1007/978-3-030-31277-0\_7},
-  timestamp = {Mon, 16 Sep 2019 19:30:06 +0200},
-  biburl    = {https://dblp.org/rec/conf/netys/BalabonskiCPRTU19.bib},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@article{berard16dc,
-author = {B\'{e}atrice B\'{e}rard and Pascal Lafourcade and Laure Millet and Maria Potop-Butucaru and Yann Thierry-Mieg and S\'{e}bastien Tixeuil},
-title = {Formal Verification of Mobile Robot Protocols},
-journal = dc,
-year = 2016,
-volume = 29,
-number = 6,
-pages = {459--487},
-doi = {10.1007/s00446-016-0271-1},
-}
-
-@article{bezem97fac,
-  author = 	 {Marc Bezem and Roland Bol and Jan Frisco Groote},
-  title = 	 {{Formalizing Process Algebraic Verifications in the Calculus of Constructions}},
-  journal = 	 fac,
-  year = 	 {1997},
-  volume = 	 {9},
-  pages = 	 {1-48},
-  ee    = {http://dx.doi.org/10.1007/BF01212523},
-  publisher = SV
-}
-
-@inproceedings{bonnet14wssr,
-  author    = {Fran{\c{c}}ois Bonnet and
-               Xavier D{\'{e}}fago and
-               Franck Petit and
-               Maria Potop{-}Butucaru and
-               S{\'{e}}bastien Tixeuil},
-  title     = {Discovering and Assessing Fine-Grained Metrics in Robot Networks Protocols},
-  booktitle = {33rd {IEEE} International Symposium on Reliable Distributed Systems
-               Workshops, {SRDS} Workshops 2014, Nara, Japan, October 6-9, 2014},
-  pages     = {50--59},
-  publisher = {{IEEE}},
-  year      = {2014},
-  doi       = {10.1109/SRDSW.2014.34},
-  timestamp = {Fri, 16 Jan 2015 12:43:20 +0100},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/srds/BonnetDPPT14},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@article{courtieu15ipl,
-  author    = {Pierre Courtieu and
-               Lionel Rieg and
-               Sébastien Tixeuil and Xavier Urbain},
-  title     = {{Impossibility of Gathering, a Certification}},
-  journal   = ipl,
-  year      = 2015,
-  volume    = {115},
-  pages     = {447-452},
-  doi       = {10.1016/j.ipl.2014.11.001},
-}
-
-@InProceedings{courtieu16disc,
-  author   =  {Pierre Courtieu and Lionel Rieg and Sébastien Tixeuil and
-                  Xavier Urbain},
-  title    =  {Certified Universal Gathering Algorithm in {$\mathbb{R}^2$} for Oblivious Mobile Robots},
-  crossref =  {disc2016},
-}
-
-@inproceedings{cousineau12fm,
-  author    = {Denis Cousineau and
-               Damien Doligez and
-               Leslie Lamport and
-               Stephan Merz and
-               Daniel Ricketts and
-               Hern{\'a}n Vanzetto},
-  title     = {{TLA} + {P}roofs},
-  pages     = {147-154},
-  ee        = {http://dx.doi.org/10.1007/978-3-642-32759-9\_14},
-  crossref  = {fm2012},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@inproceedings{deng09tase,
-	Abstract = {Population protocols are an elegant model recently introduced for distributed algorithms running in large and unreliable networks of tiny mobile agents. Correctness proofs of such protocols involve subtle arguments on infinite sequences of events. We propose a general formalization of self-stabilizing population protocols with the Coq proof assistant. It is used in reasoning about a concrete protocol for leader election in complete graphs. The protocol is formally proved to be correct for networks of arbitrarily large size. To this end we develop an appropriate theory of infinite sequences, including results for reasoning on abstractions. In addition, we provide a constructive correctness proof for a leader election protocol in directed rings. An advantage of using a constructive setting is that we get more informative proofs on the scenarios that converge to the desired configurations.},
-	Author = {Yuxin Deng and Jean-Fran\c{c}ois Monin},
-	Bibsource = {DBLP, http://dblp.uni-trier.de},
-	Crossref = {tase09},
-	Ee = {http://dx.doi.org/10.1109/TASE.2009.9},
-	Pages = {201-208},
-	Title = {{Verifying Self-stabilizing Population Protocols with Coq}},
-	Year = {2009}}
-
-
-@inproceedings{devismes12sss,
-	Abstract = {We propose optimal (w.r.t. the number of robots) solutions for the deterministic terminating exploration (exploration for short) of a grid-shaped network by a team of asynchronous oblivious robots in the asynchronous non-atomic model, so-called CORDA.
-In more details, we first consider the ATOM model. We show that it is impossible to explore a grid of at least three nodes with less than three robots. Next, we show that it is impossible to explore a (2,2)-Grid with less than 4 robots, and a (3,3)-Grid with less than 5 robots, respectively. The two first results hold for both deterministic and probabilistic settings, while the latter holds only in the deterministic case. ATOM being strictly stronger than CORDA, all these impossibility results also hold in CORDA.
-Then, we propose deterministic algorithms in CORDA to exhibit the optimal number of robots allowing to explore of a given grid. Our results show that except in two particular cases, 3 robots are necessary and sufficient to deterministically explore a grid of at least three nodes. The optimal number of robots for the two remaining cases is: 4 for the (2,2)-Grid and 5 for the (3,3)-Grid, respectively.},
-	Author = {St\'{e}phane Devismes and Anissa Lamani and Franck Petit and Pascal Raymond and S\'{e}bastien Tixeuil},
-	Title = {{Optimal Grid Exploration by Asynchronous Oblivious Robots}},
-pages = {64-76},
-crossref = {sss12}
-}
-
-@inproceedings{defago20srds,
-  author    = {Xavier D{\'{e}}fago and
-               Adam Heriban and
-               S{\'{e}}bastien Tixeuil and
-               Koichi Wada},
-  title     = {Using Model Checking to Formally Verify Rendezvous Algorithms for
-               Robots with Lights in Euclidean Space},
-  booktitle = {International Symposium on Reliable Distributed Systems, {SRDS} 2020,
-               Shanghai, China, September 21-24, 2020},
-  pages     = {113--122},
-  publisher = {{IEEE}},
-  year      = {2020},
-  doi       = {10.1109/SRDS51746.2020.00019},
-  timestamp = {Thu, 19 Nov 2020 11:03:40 +0100},
-  biburl    = {https://dblp.org/rec/conf/srds/DefagoHTW20.bib},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@article{sangnier20fmsd,
-  author    = {Arnaud Sangnier and
-               Nathalie Sznajder and
-               Maria Potop{-}Butucaru and
-               S{\'{e}}bastien Tixeuil},
-  title     = {Parameterized verification of algorithms for oblivious robots on a
-               ring},
-  journal   = {Formal Methods Syst. Des.},
-  volume    = {56},
-  number    = {1},
-  pages     = {55--89},
-  year      = {2020},
-  doi       = {10.1007/s10703-019-00335-y},
-  timestamp = {Wed, 02 Dec 2020 13:38:57 +0100},
-  biburl    = {https://dblp.org/rec/journals/fmsd/SangnierSPT20.bib},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@inproceedings{doan17opodis,
-  author    = {Ha Thi Thu Doan and
-               Fran{\c{c}}ois Bonnet and
-               Kazuhiro Ogata},
-  editor    = {James Aspnes and
-               Alysson Bessani and
-               Pascal Felber and
-               Jo{\~{a}}o Leit{\~{a}}o},
-  title     = {Model Checking of Robot Gathering},
-  booktitle = {21st International Conference on Principles of Distributed Systems,
-               {OPODIS} 2017, Lisbon, Portugal, December 18-20, 2017},
-  series    = {LIPIcs},
-  volume    = {95},
-  pages     = {12:1--12:16},
-  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
-  year      = {2017},
-  doi       = {10.4230/LIPIcs.OPODIS.2017.12},
-  timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
-  biburl    = {https://dblp.org/rec/conf/opodis/Doan0017.bib},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@book{fokkink07,
-  author = 	 {Wan Fokkink},
-  title = 	 {{Modelling Distributed Systems}},
-  series = {EATCS Texts in Theoretical Computer Science},
-  isbn = {978-3-540-73938-8},
-  publisher = 	 SV,
-  year = 	 {2007}
-}
-
-@inproceedings{gaspar14ijpp,
-   author = {Nuno Gaspar and
-                          Ludovic Henrio and
-                          Eric Madelaine},
-   title    = {Bringing Coq into the World of GCM Distributed Applications.},
-   journal   = ijpp,
-   year     = {2014},
-   pages  = {643-662},
-   ee     = {http://dx.doi.org/10.1007/s10766-013-0264-7},
-}
-
-@inproceedings{kuefner12ifiptcs,
-  author    = {Philipp K{\"u}fner and
-               Uwe Nestmann and
-               Christina Rickmann},
-  title     = {{Formal Verification of Distributed Algorithms - From Pseudo
-               Code to Checked Proofs}},
-  pages     = {209-224},
-  ee        = {http://dx.doi.org/10.1007/978-3-642-33475-7\_15},
-  crossref  = {ifiptcs2012},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@article{suzuki99siam,
-  author    = {Ichiro Suzuki and
-               Masafumi Yamashita},
-  title     = {{Distributed Anonymous Mobile Robots: Formation of Geometric
-               Patterns}},
-  journal   = siamjc,
-  volume    = {28},
-  number    = {4},
-  year      = {1999},
-  pages     = {1347-1363},
-  ee        = {http://dx.doi.org/10.1137/S009753979628292X},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@inproceedings{MPST14c,
-  author    = {Laure Millet and
-               Maria Potop{-}Butucaru and
-               Nathalie Sznajder and
-               S{\'{e}}bastien Tixeuil},
-  title     = {On the Synthesis of Mobile Robots Algorithms: The Case of Ring Gathering},
-  year      = {2014},
-  pages     = {237--251},
-  crossref  = {sss14},
-  doi       = {10.1007/978-3-319-11764-5\_17},
-  timestamp = {Thu, 02 Oct 2014 16:57:09 +0200},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sss/MilletPST14},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@proceedings{disc2016,
-  editor    = {Cyril Gavoille and David Ilcinkas},
-  title     = {Distributed Computing - 30th International Symposium, (DISC 2016)},
-  address   = {Paris, France},
-  month     = sep,
-  booktitle = {Distributed Computing - 30th International Symposium, (DISC 2016)},
-  series    = lncs,
-  year      = {2016},
-  volume    = {9888},
-  publisher = SV,
-  isbn      = {978-3-662-53426-7},
-}
-
-@proceedings{fm2012,
-  editor    = {Dimitra Giannakopoulou and
-               Dominique M{\'e}ry},
-  title     = {Formal Methods - 18th International Symposium (FM 2012)},
-  booktitle = {FM},
-  publisher = SV,
-  series    = lncs,
-  volume    = {7436},
-  year      = {2012},
-  month     = aug,
-  address   = {Paris, France},
-  isbn      = {978-3-642-32758-2},
-  ee        = {http://dx.doi.org/10.1007/978-3-642-32759-9},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@proceedings{ifipTCS2012,
-  editor    = {Jos C. M. Baeten and
-               Thomas Ball and
-               Frank S. de Boer},
-  title     = {Theoretical Computer Science - 7th IFIP TC 1/WG 2.2 International
-               Conference (TCS 2012)},
-  booktitle = {IFIP TCS},
-  publisher = SV,
-  series    = lncs,
-  volume    = {7604},
-  year      = {2012},
-  month     = sep,
-  address   = {Amsterdam, The Netherlands},
-  isbn      = {978-3-642-33474-0},
-  ee        = {http://dx.doi.org/10.1007/978-3-642-33475-7},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
-}
-
-@proceedings{sofl2016,
-  editor    = {Shaoying Liu and
-               Zhenhua Duan and
-               Cong Tian and
-               Fumiko Nagoya},
-  booktitle     = {Structured Object-Oriented Formal Language and Method - 6th International
-               Workshop, {SOFL+MSVL} 2016, Tokyo, Japan, November 15, 2016, Revised
-               Selected Papers},
-  series    = lncs,
-  volume    = {10189},
-  year      = {2017},
-  doi       = {10.1007/978-3-319-57708-1},
-  isbn      = {978-3-319-57707-4},
-  timestamp = {Wed, 17 May 2017 14:24:52 +0200},
-  biburl    = {http://dblp2.uni-trier.de/rec/bib/conf/sofl/2016},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@proceedings{sss12,
-  editor    = {Andr{\'e}a W. Richa and
-               Christian Scheideler},
-  title     = {Stabilization, Safety, and Security of Distributed Systems
-               - 14th International Symposium (SSS 2012)},
-  booktitle = {Stabilization, Safety, and Security of Distributed Systems
-               - 14th International Symposium (SSS 2012)},
-  publisher = SV,
-  series    = lncs,
-  volume    = {7596},
-  year      = {2012},
-  month = oct,
-  address = {Toronto, Canada},
-  isbn      = {978-3-642-33535-8},
-  ee        = {http://dx.doi.org/10.1007/978-3-642-33536-5}
-}
-
-@proceedings{sss13,
-  editor    = {Teruo Higashino and Yoshiaki Katayama and
-               Toshimitsu Masuzawa and Maria Potop-Butucaru and
-               Masafumi Yamashita},
-  title     = {Stabilization, Safety, and Security of Distributed Systems
-               - 15th International Symposium (SSS 2013)},
-  booktitle = {Stabilization, Safety, and Security of Distributed Systems
-               - 15th International Symposium (SSS 2013)},
-  publisher = SV,
-  series    = lncs,
-  volume    = {8255},
-  year      = {2013},
-  month     = nov,
-  address   = {Osaka, Japan},
-  isbn      = {978-3-319-03088-3},
-  ee        = {http://dx.doi.org/10.1007/978-3-319-03089-0}
-}
-
-@proceedings{sss14,
-  editor    = {Pascal Felber and
-               Vijay K. Garg},
-  title     = {Stabilization, Safety, and Security of Distributed Systems - 16th
-               International Symposium, (SSS 2014)},
-  booktitle = {Stabilization, Safety, and Security of Distributed Systems - 16th
-               International Symposium, (SSS 2014)},
-  series    = lncs,
-  year      = {2014},
-  volume    = {8756},
-  publisher = SV,
-  month     = sep,
-  ee       = {http://dx.doi.org/10.1007/978-3-319-11764-5},
-  isbn      = {978-3-319-11763-8},
-  timestamp = {Thu, 02 Oct 2014 16:57:09 +0200},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sss/2014},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@proceedings{tase09,
-	Bibsource = {DBLP, http://dblp.uni-trier.de},
-	Editor = {Wei-Ngan Chin and Shengchao Qin},
-	Isbn = {978-0-7695-3757-3},
-	Publisher = {IEEE Computer Society},
-	booktitle = {Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009)},
-
-	Title = {Third IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009)},
-        Address = {Tianjin, China},
-        month   = jul,
-	Year = 2009}
-
-@article{flocchini05tcs,
-  author    = {Paola Flocchini and
-               Giuseppe Prencipe and
-               Nicola Santoro and
-               Peter Widmayer},
-  title     = {Gathering of asynchronous robots with limited visibility},
-  journal   = {Theor. Comput. Sci.},
-  volume    = {337},
-  number    = {1-3},
-  pages     = {147--168},
-  year      = {2005},
-  doi       = {10.1016/j.tcs.2005.01.001},
-  timestamp = {Sun, 28 May 2017 13:20:06 +0200},
-  biburl    = {https://dblp.org/rec/journals/tcs/FlocchiniPSW05.bib},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@article{lamport1994ACM,
-author = {Lamport, Leslie},
-title = {The Temporal Logic of Actions},
-year = {1994},
-issue_date = {May 1994},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {16},
-number = {3},
-issn = {0164-0925},
-doi = {10.1145/177492.177726},
-journal = {ACM Trans. Program. Lang. Syst.},
-month = may,
-pages = {872–923},
-numpages = {52},
-keywords = {safety properties, liveness properties, concurrent programming}
-}
diff --git a/Paper/img/contraction_lemma.drawio.png b/Paper/img/contraction_lemma.drawio.png
deleted file mode 100644
index 2658cac9f6d24ad1890b3e7b3694e922012469a1..0000000000000000000000000000000000000000
Binary files a/Paper/img/contraction_lemma.drawio.png and /dev/null differ
diff --git a/Paper/img/measure_decrease_not_on_A.drawio.png b/Paper/img/measure_decrease_not_on_A.drawio.png
deleted file mode 100644
index 551315ebd291102fa46897e0eaee3c51ff85903b..0000000000000000000000000000000000000000
Binary files a/Paper/img/measure_decrease_not_on_A.drawio.png and /dev/null differ
diff --git a/Paper/img/measure_decrease_not_on_B.drawio.png b/Paper/img/measure_decrease_not_on_B.drawio.png
deleted file mode 100644
index 609ad64a5332905220d72bfc9ae58890606ba01e..0000000000000000000000000000000000000000
Binary files a/Paper/img/measure_decrease_not_on_B.drawio.png and /dev/null differ
diff --git a/Paper/img/measure_decrease_on_A.drawio.png b/Paper/img/measure_decrease_on_A.drawio.png
deleted file mode 100644
index 5f166b4b1fdccd15f0316b7b07030cec5709a973..0000000000000000000000000000000000000000
Binary files a/Paper/img/measure_decrease_on_A.drawio.png and /dev/null differ
diff --git a/Paper/img/measure_decrease_on_B.drawio.png b/Paper/img/measure_decrease_on_B.drawio.png
deleted file mode 100644
index 798adfbbc126164452f5babb7f393c515a99e71a..0000000000000000000000000000000000000000
Binary files a/Paper/img/measure_decrease_on_B.drawio.png and /dev/null differ
diff --git a/Paper/img/phase_transition_diagram.drawio.png b/Paper/img/phase_transition_diagram.drawio.png
deleted file mode 100644
index 48df159d0f96e30bcc467ad01545c2681b32541a..0000000000000000000000000000000000000000
Binary files a/Paper/img/phase_transition_diagram.drawio.png and /dev/null differ
diff --git a/Paper/img/weber_examples_A.drawio.png b/Paper/img/weber_examples_A.drawio.png
deleted file mode 100644
index 6ef2a05d373ee58a7abed21da71c85150ce465ae..0000000000000000000000000000000000000000
Binary files a/Paper/img/weber_examples_A.drawio.png and /dev/null differ
diff --git a/Paper/img/weber_examples_B.drawio.png b/Paper/img/weber_examples_B.drawio.png
deleted file mode 100644
index b65d1789d8106deb2c5618e8f5c883e5f1b3d622..0000000000000000000000000000000000000000
Binary files a/Paper/img/weber_examples_B.drawio.png and /dev/null differ
diff --git a/Paper/img/weber_examples_C.drawio.png b/Paper/img/weber_examples_C.drawio.png
deleted file mode 100644
index 5d7e86acd3820ce9ce39063c0edf533d32e9a29e..0000000000000000000000000000000000000000
Binary files a/Paper/img/weber_examples_C.drawio.png and /dev/null differ
diff --git a/Paper/llncs.cls b/Paper/llncs.cls
deleted file mode 100644
index 886bf7264d8dd0e22e13e9bcf419c1fa6b1448cc..0000000000000000000000000000000000000000
--- a/Paper/llncs.cls
+++ /dev/null
@@ -1,1218 +0,0 @@
-% LLNCS DOCUMENT CLASS -- version 2.20 (10-Mar-2018)
-% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
-%
-%%
-%% \CharacterTable
-%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
-%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
-%%   Digits        \0\1\2\3\4\5\6\7\8\9
-%%   Exclamation   \!     Double quote  \"     Hash (number) \#
-%%   Dollar        \$     Percent       \%     Ampersand     \&
-%%   Acute accent  \'     Left paren    \(     Right paren   \)
-%%   Asterisk      \*     Plus          \+     Comma         \,
-%%   Minus         \-     Point         \.     Solidus       \/
-%%   Colon         \:     Semicolon     \;     Less than     \<
-%%   Equals        \=     Greater than  \>     Question mark \?
-%%   Commercial at \@     Left bracket  \[     Backslash     \\
-%%   Right bracket \]     Circumflex    \^     Underscore    \_
-%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
-%%   Right brace   \}     Tilde         \~}
-%%
-\NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesClass{llncs}[2018/03/10 v2.20
-^^J LaTeX document class for Lecture Notes in Computer Science]
-% Options
-\let\if@envcntreset\iffalse
-\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
-\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
-\DeclareOption{oribibl}{\let\oribibl=Y}
-\let\if@custvec\iftrue
-\DeclareOption{orivec}{\let\if@custvec\iffalse}
-\let\if@envcntsame\iffalse
-\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
-\let\if@envcntsect\iffalse
-\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
-\let\if@runhead\iffalse
-\DeclareOption{runningheads}{\let\if@runhead\iftrue}
-
-\let\if@openright\iftrue
-\let\if@openbib\iffalse
-\DeclareOption{openbib}{\let\if@openbib\iftrue}
-
-% languages
-\let\switcht@@therlang\relax
-\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
-\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
-
-\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
-
-\ProcessOptions
-
-\LoadClass[twoside]{article}
-\RequirePackage{multicol} % needed for the list of participants, index
-\RequirePackage{aliascnt}
-
-\setlength{\textwidth}{12.2cm}
-\setlength{\textheight}{19.3cm}
-\renewcommand\@pnumwidth{2em}
-\renewcommand\@tocrmarg{3.5em}
-%
-\def\@dottedtocline#1#2#3#4#5{%
-  \ifnum #1>\c@tocdepth \else
-    \vskip \z@ \@plus.2\p@
-    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
-               \parfillskip -\rightskip \pretolerance=10000
-     \parindent #2\relax\@afterindenttrue
-     \interlinepenalty\@M
-     \leavevmode
-     \@tempdima #3\relax
-     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
-     {#4}\nobreak
-     \leaders\hbox{$\m@th
-        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
-        mu$}\hfill
-     \nobreak
-     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
-     \par}%
-  \fi}
-%
-\def\switcht@albion{%
-\def\abstractname{Abstract.}
-\def\ackname{Acknowledgement.}
-\def\andname{and}
-\def\lastandname{\unskip, and}
-\def\appendixname{Appendix}
-\def\chaptername{Chapter}
-\def\claimname{Claim}
-\def\conjecturename{Conjecture}
-\def\contentsname{Table of Contents}
-\def\corollaryname{Corollary}
-\def\definitionname{Definition}
-\def\examplename{Example}
-\def\exercisename{Exercise}
-\def\figurename{Fig.}
-\def\keywordname{{\bf Keywords:}}
-\def\indexname{Index}
-\def\lemmaname{Lemma}
-\def\contriblistname{List of Contributors}
-\def\listfigurename{List of Figures}
-\def\listtablename{List of Tables}
-\def\mailname{{\it Correspondence to\/}:}
-\def\noteaddname{Note added in proof}
-\def\notename{Note}
-\def\partname{Part}
-\def\problemname{Problem}
-\def\proofname{Proof}
-\def\propertyname{Property}
-\def\propositionname{Proposition}
-\def\questionname{Question}
-\def\remarkname{Remark}
-\def\seename{see}
-\def\solutionname{Solution}
-\def\subclassname{{\it Subject Classifications\/}:}
-\def\tablename{Table}
-\def\theoremname{Theorem}}
-\switcht@albion
-% Names of theorem like environments are already defined
-% but must be translated if another language is chosen
-%
-% French section
-\def\switcht@francais{%\typeout{On parle francais.}%
- \def\abstractname{R\'esum\'e.}%
- \def\ackname{Remerciements.}%
- \def\andname{et}%
- \def\lastandname{ et}%
- \def\appendixname{Appendice}
- \def\chaptername{Chapitre}%
- \def\claimname{Pr\'etention}%
- \def\conjecturename{Hypoth\`ese}%
- \def\contentsname{Table des mati\`eres}%
- \def\corollaryname{Corollaire}%
- \def\definitionname{D\'efinition}%
- \def\examplename{Exemple}%
- \def\exercisename{Exercice}%
- \def\figurename{Fig.}%
- \def\keywordname{{\bf Mots-cl\'e:}}
- \def\indexname{Index}
- \def\lemmaname{Lemme}%
- \def\contriblistname{Liste des contributeurs}
- \def\listfigurename{Liste des figures}%
- \def\listtablename{Liste des tables}%
- \def\mailname{{\it Correspondence to\/}:}
- \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
- \def\notename{Remarque}%
- \def\partname{Partie}%
- \def\problemname{Probl\`eme}%
- \def\proofname{Preuve}%
- \def\propertyname{Caract\'eristique}%
-%\def\propositionname{Proposition}%
- \def\questionname{Question}%
- \def\remarkname{Remarque}%
- \def\seename{voir}
- \def\solutionname{Solution}%
- \def\subclassname{{\it Subject Classifications\/}:}
- \def\tablename{Tableau}%
- \def\theoremname{Th\'eor\`eme}%
-}
-%
-% German section
-\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
- \def\abstractname{Zusammenfassung.}%
- \def\ackname{Danksagung.}%
- \def\andname{und}%
- \def\lastandname{ und}%
- \def\appendixname{Anhang}%
- \def\chaptername{Kapitel}%
- \def\claimname{Behauptung}%
- \def\conjecturename{Hypothese}%
- \def\contentsname{Inhaltsverzeichnis}%
- \def\corollaryname{Korollar}%
-%\def\definitionname{Definition}%
- \def\examplename{Beispiel}%
- \def\exercisename{\"Ubung}%
- \def\figurename{Abb.}%
- \def\keywordname{{\bf Schl\"usselw\"orter:}}
- \def\indexname{Index}
-%\def\lemmaname{Lemma}%
- \def\contriblistname{Mitarbeiter}
- \def\listfigurename{Abbildungsverzeichnis}%
- \def\listtablename{Tabellenverzeichnis}%
- \def\mailname{{\it Correspondence to\/}:}
- \def\noteaddname{Nachtrag}%
- \def\notename{Anmerkung}%
- \def\partname{Teil}%
-%\def\problemname{Problem}%
- \def\proofname{Beweis}%
- \def\propertyname{Eigenschaft}%
-%\def\propositionname{Proposition}%
- \def\questionname{Frage}%
- \def\remarkname{Anmerkung}%
- \def\seename{siehe}
- \def\solutionname{L\"osung}%
- \def\subclassname{{\it Subject Classifications\/}:}
- \def\tablename{Tabelle}%
-%\def\theoremname{Theorem}%
-}
-
-% Ragged bottom for the actual page
-\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
-\global\let\@textbottom\relax}}
-
-\renewcommand\small{%
-   \@setfontsize\small\@ixpt{11}%
-   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
-   \abovedisplayshortskip \z@ \@plus2\p@
-   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
-   \def\@listi{\leftmargin\leftmargini
-               \parsep 0\p@ \@plus1\p@ \@minus\p@
-               \topsep 8\p@ \@plus2\p@ \@minus4\p@
-               \itemsep0\p@}%
-   \belowdisplayskip \abovedisplayskip
-}
-
-\frenchspacing
-\widowpenalty=10000
-\clubpenalty=10000
-
-\setlength\oddsidemargin   {63\p@}
-\setlength\evensidemargin  {63\p@}
-\setlength\marginparwidth  {90\p@}
-
-\setlength\headsep   {16\p@}
-
-\setlength\footnotesep{7.7\p@}
-\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
-\setlength\intextsep   {8mm\@plus 2\p@ \@minus 2\p@}
-
-\setcounter{secnumdepth}{2}
-
-\newcounter {chapter}
-\renewcommand\thechapter      {\@arabic\c@chapter}
-
-\newif\if@mainmatter \@mainmattertrue
-\newcommand\frontmatter{\cleardoublepage
-            \@mainmatterfalse\pagenumbering{Roman}}
-\newcommand\mainmatter{\cleardoublepage
-       \@mainmattertrue\pagenumbering{arabic}}
-\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
-      \@mainmatterfalse}
-
-\renewcommand\part{\cleardoublepage
-                 \thispagestyle{empty}%
-                 \if@twocolumn
-                     \onecolumn
-                     \@tempswatrue
-                   \else
-                     \@tempswafalse
-                 \fi
-                 \null\vfil
-                 \secdef\@part\@spart}
-
-\def\@part[#1]#2{%
-    \ifnum \c@secnumdepth >-2\relax
-      \refstepcounter{part}%
-      \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
-    \else
-      \addcontentsline{toc}{part}{#1}%
-    \fi
-    \markboth{}{}%
-    {\centering
-     \interlinepenalty \@M
-     \normalfont
-     \ifnum \c@secnumdepth >-2\relax
-       \huge\bfseries \partname~\thepart
-       \par
-       \vskip 20\p@
-     \fi
-     \Huge \bfseries #2\par}%
-    \@endpart}
-\def\@spart#1{%
-    {\centering
-     \interlinepenalty \@M
-     \normalfont
-     \Huge \bfseries #1\par}%
-    \@endpart}
-\def\@endpart{\vfil\newpage
-              \if@twoside
-                \null
-                \thispagestyle{empty}%
-                \newpage
-              \fi
-              \if@tempswa
-                \twocolumn
-              \fi}
-
-\newcommand\chapter{\clearpage
-                    \thispagestyle{empty}%
-                    \global\@topnum\z@
-                    \@afterindentfalse
-                    \secdef\@chapter\@schapter}
-\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
-                       \if@mainmatter
-                         \refstepcounter{chapter}%
-                         \typeout{\@chapapp\space\thechapter.}%
-                         \addcontentsline{toc}{chapter}%
-                                  {\protect\numberline{\thechapter}#1}%
-                       \else
-                         \addcontentsline{toc}{chapter}{#1}%
-                       \fi
-                    \else
-                      \addcontentsline{toc}{chapter}{#1}%
-                    \fi
-                    \chaptermark{#1}%
-                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
-                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
-                    \if@twocolumn
-                      \@topnewpage[\@makechapterhead{#2}]%
-                    \else
-                      \@makechapterhead{#2}%
-                      \@afterheading
-                    \fi}
-\def\@makechapterhead#1{%
-% \vspace*{50\p@}%
-  {\centering
-    \ifnum \c@secnumdepth >\m@ne
-      \if@mainmatter
-        \large\bfseries \@chapapp{} \thechapter
-        \par\nobreak
-        \vskip 20\p@
-      \fi
-    \fi
-    \interlinepenalty\@M
-    \Large \bfseries #1\par\nobreak
-    \vskip 40\p@
-  }}
-\def\@schapter#1{\if@twocolumn
-                   \@topnewpage[\@makeschapterhead{#1}]%
-                 \else
-                   \@makeschapterhead{#1}%
-                   \@afterheading
-                 \fi}
-\def\@makeschapterhead#1{%
-% \vspace*{50\p@}%
-  {\centering
-    \normalfont
-    \interlinepenalty\@M
-    \Large \bfseries  #1\par\nobreak
-    \vskip 40\p@
-  }}
-
-\renewcommand\section{\@startsection{section}{1}{\z@}%
-                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
-                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
-                       {\normalfont\large\bfseries\boldmath
-                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
-\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
-                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
-                       {8\p@ \@plus 4\p@ \@minus 4\p@}%
-                       {\normalfont\normalsize\bfseries\boldmath
-                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
-\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
-                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
-                       {-0.5em \@plus -0.22em \@minus -0.1em}%
-                       {\normalfont\normalsize\bfseries\boldmath}}
-\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
-                       {-12\p@ \@plus -4\p@ \@minus -4\p@}%
-                       {-0.5em \@plus -0.22em \@minus -0.1em}%
-                       {\normalfont\normalsize\itshape}}
-\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
-                  \string\subparagraph\space with this class}\vskip0.5cm
-You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
-
-\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
-\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
-\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
-\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
-\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
-\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
-\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
-\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
-\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
-\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
-\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
-
-\let\footnotesize\small
-
-\if@custvec
-\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
-{\mbox{\boldmath$\textstyle#1$}}
-{\mbox{\boldmath$\scriptstyle#1$}}
-{\mbox{\boldmath$\scriptscriptstyle#1$}}}
-\fi
-
-\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
-\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
-\penalty50\hskip1em\null\nobreak\hfil\squareforqed
-\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
-
-\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
-\halign{\hfil
-$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
-\cr\to\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
-\cr\to\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
-\gets\cr\to\cr}}}}}
-\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
-$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
-\noalign{\vskip1.2pt}=\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
-\noalign{\vskip1pt}=\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
-<\cr
-\noalign{\vskip0.9pt}=\cr}}}}}
-\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
-$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
-\noalign{\vskip1.2pt}=\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
-\noalign{\vskip1pt}=\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
->\cr
-\noalign{\vskip0.9pt}=\cr}}}}}
-\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
-\halign{\hfil
-$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
->\cr\noalign{\vskip-1pt}<\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
->\cr\noalign{\vskip-0.8pt}<\cr}}}
-{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
->\cr\noalign{\vskip-0.3pt}<\cr}}}}}
-\def\bbbr{{\rm I\!R}} %reelle Zahlen
-\def\bbbm{{\rm I\!M}}
-\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
-\def\bbbf{{\rm I\!F}}
-\def\bbbh{{\rm I\!H}}
-\def\bbbk{{\rm I\!K}}
-\def\bbbp{{\rm I\!P}}
-\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
-{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
-\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
-to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
-{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
-to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
-{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
-to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
-{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
-to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
-\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
-Q$}\hbox{\raise
-0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
-{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
-0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
-{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
-0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
-{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
-0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
-\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
-T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
-{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
-to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
-{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
-to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
-{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
-to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
-\def\bbbs{{\mathchoice
-{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
-to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
-to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
-{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
-to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
-to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
-{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
-to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
-to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
-{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
-to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
-to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
-\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
-{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
-{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
-{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
-
-\let\ts\,
-
-\setlength\leftmargini  {17\p@}
-\setlength\leftmargin    {\leftmargini}
-\setlength\leftmarginii  {\leftmargini}
-\setlength\leftmarginiii {\leftmargini}
-\setlength\leftmarginiv  {\leftmargini}
-\setlength  \labelsep  {.5em}
-\setlength  \labelwidth{\leftmargini}
-\addtolength\labelwidth{-\labelsep}
-
-\def\@listI{\leftmargin\leftmargini
-            \parsep 0\p@ \@plus1\p@ \@minus\p@
-            \topsep 8\p@ \@plus2\p@ \@minus4\p@
-            \itemsep0\p@}
-\let\@listi\@listI
-\@listi
-\def\@listii {\leftmargin\leftmarginii
-              \labelwidth\leftmarginii
-              \advance\labelwidth-\labelsep
-              \topsep    0\p@ \@plus2\p@ \@minus\p@}
-\def\@listiii{\leftmargin\leftmarginiii
-              \labelwidth\leftmarginiii
-              \advance\labelwidth-\labelsep
-              \topsep    0\p@ \@plus\p@\@minus\p@
-              \parsep    \z@
-              \partopsep \p@ \@plus\z@ \@minus\p@}
-
-\renewcommand\labelitemi{\normalfont\bfseries --}
-\renewcommand\labelitemii{$\m@th\bullet$}
-
-\setlength\arraycolsep{1.4\p@}
-\setlength\tabcolsep{1.4\p@}
-
-\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
-                                                    {{\contentsname}}}
- \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
- \def\lastand{\ifnum\value{auco}=2\relax
-                 \unskip{} \andname\
-              \else
-                 \unskip \lastandname\
-              \fi}%
- \def\and{\stepcounter{@auth}\relax
-          \ifnum\value{@auth}=\value{auco}%
-             \lastand
-          \else
-             \unskip,
-          \fi}%
- \@starttoc{toc}\if@restonecol\twocolumn\fi}
-
-\def\l@part#1#2{\addpenalty{\@secpenalty}%
-   \addvspace{2em plus\p@}%  % space above part line
-   \begingroup
-     \parindent \z@
-     \rightskip \z@ plus 5em
-     \hrule\vskip5pt
-     \large               % same size as for a contribution heading
-     \bfseries\boldmath   % set line in boldface
-     \leavevmode          % TeX command to enter horizontal mode.
-     #1\par
-     \vskip5pt
-     \hrule
-     \vskip1pt
-     \nobreak             % Never break after part entry
-   \endgroup}
-
-\def\@dotsep{2}
-
-\let\phantomsection=\relax
-
-\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
-{}\fi}
-
-\def\addnumcontentsmark#1#2#3{%
-\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
-                     {\thechapter}#3}{\thepage}\hyperhrefextend}}%
-\def\addcontentsmark#1#2#3{%
-\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}%
-\def\addcontentsmarkwop#1#2#3{%
-\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}%
-
-\def\@adcmk[#1]{\ifcase #1 \or
-\def\@gtempa{\addnumcontentsmark}%
-  \or    \def\@gtempa{\addcontentsmark}%
-  \or    \def\@gtempa{\addcontentsmarkwop}%
-  \fi\@gtempa{toc}{chapter}%
-}
-\def\addtocmark{%
-\phantomsection
-\@ifnextchar[{\@adcmk}{\@adcmk[3]}%
-}
-
-\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
- \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
- \parindent \z@ \rightskip \@tocrmarg
- \advance\rightskip by 0pt plus 2cm
- \parfillskip -\rightskip \pretolerance=10000
- \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
- {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
- \else
-      \nobreak
-      \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
-      \@dotsep mu$}\hfill
-      \nobreak\hbox to\@pnumwidth{\hss #2}%
- \fi\par
- \penalty\@highpenalty \endgroup}
-
-\def\l@title#1#2{\addpenalty{-\@highpenalty}
- \addvspace{8pt plus 1pt}
- \@tempdima \z@
- \begingroup
- \parindent \z@ \rightskip \@tocrmarg
- \advance\rightskip by 0pt plus 2cm
- \parfillskip -\rightskip \pretolerance=10000
- \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
- #1\nobreak
- \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
- \@dotsep mu$}\hfill
- \nobreak\hbox to\@pnumwidth{\hss #2}\par
- \penalty\@highpenalty \endgroup}
-
-\def\l@author#1#2{\addpenalty{\@highpenalty}
- \@tempdima=15\p@ %\z@
- \begingroup
- \parindent \z@ \rightskip \@tocrmarg
- \advance\rightskip by 0pt plus 2cm
- \pretolerance=10000
- \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
- \textit{#1}\par
- \penalty\@highpenalty \endgroup}
-
-\setcounter{tocdepth}{0}
-\newdimen\tocchpnum
-\newdimen\tocsecnum
-\newdimen\tocsectotal
-\newdimen\tocsubsecnum
-\newdimen\tocsubsectotal
-\newdimen\tocsubsubsecnum
-\newdimen\tocsubsubsectotal
-\newdimen\tocparanum
-\newdimen\tocparatotal
-\newdimen\tocsubparanum
-\tocchpnum=\z@            % no chapter numbers
-\tocsecnum=15\p@          % section 88. plus 2.222pt
-\tocsubsecnum=23\p@       % subsection 88.8 plus 2.222pt
-\tocsubsubsecnum=27\p@    % subsubsection 88.8.8 plus 1.444pt
-\tocparanum=35\p@         % paragraph 88.8.8.8 plus 1.666pt
-\tocsubparanum=43\p@      % subparagraph 88.8.8.8.8 plus 1.888pt
-\def\calctocindent{%
-\tocsectotal=\tocchpnum
-\advance\tocsectotal by\tocsecnum
-\tocsubsectotal=\tocsectotal
-\advance\tocsubsectotal by\tocsubsecnum
-\tocsubsubsectotal=\tocsubsectotal
-\advance\tocsubsubsectotal by\tocsubsubsecnum
-\tocparatotal=\tocsubsubsectotal
-\advance\tocparatotal by\tocparanum}
-\calctocindent
-
-\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
-\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
-\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
-\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
-\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
-
-\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
- \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
- \@starttoc{lof}\if@restonecol\twocolumn\fi}
-\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
-
-\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
- \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
- \@starttoc{lot}\if@restonecol\twocolumn\fi}
-\let\l@table\l@figure
-
-\renewcommand\listoffigures{%
-    \section*{\listfigurename
-      \@mkboth{\listfigurename}{\listfigurename}}%
-    \@starttoc{lof}%
-    }
-
-\renewcommand\listoftables{%
-    \section*{\listtablename
-      \@mkboth{\listtablename}{\listtablename}}%
-    \@starttoc{lot}%
-    }
-
-\ifx\oribibl\undefined
-\ifx\citeauthoryear\undefined
-\renewenvironment{thebibliography}[1]
-     {\section*{\refname}
-      \def\@biblabel##1{##1.}
-      \small
-      \list{\@biblabel{\@arabic\c@enumiv}}%
-           {\settowidth\labelwidth{\@biblabel{#1}}%
-            \leftmargin\labelwidth
-            \advance\leftmargin\labelsep
-            \if@openbib
-              \advance\leftmargin\bibindent
-              \itemindent -\bibindent
-              \listparindent \itemindent
-              \parsep \z@
-            \fi
-            \usecounter{enumiv}%
-            \let\p@enumiv\@empty
-            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
-      \if@openbib
-        \renewcommand\newblock{\par}%
-      \else
-        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
-      \fi
-      \sloppy\clubpenalty4000\widowpenalty4000%
-      \sfcode`\.=\@m}
-     {\def\@noitemerr
-       {\@latex@warning{Empty `thebibliography' environment}}%
-      \endlist}
-\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
-     {\let\protect\noexpand\immediate
-     \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
-\newcount\@tempcntc
-\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
-  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
-    {\@ifundefined
-       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
-        ?}\@warning
-       {Citation `\@citeb' on page \thepage \space undefined}}%
-    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
-     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
-       \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
-     \else
-      \advance\@tempcntb\@ne
-      \ifnum\@tempcntb=\@tempcntc
-      \else\advance\@tempcntb\m@ne\@citeo
-      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
-\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
-               \@citea\def\@citea{,\,\hskip\z@skip}%
-               \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
-               {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
-                \def\@citea{--}\fi
-      \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
-\else
-\renewenvironment{thebibliography}[1]
-     {\section*{\refname}
-      \small
-      \list{}%
-           {\settowidth\labelwidth{}%
-            \leftmargin\parindent
-            \itemindent=-\parindent
-            \labelsep=\z@
-            \if@openbib
-              \advance\leftmargin\bibindent
-              \itemindent -\bibindent
-              \listparindent \itemindent
-              \parsep \z@
-            \fi
-            \usecounter{enumiv}%
-            \let\p@enumiv\@empty
-            \renewcommand\theenumiv{}}%
-      \if@openbib
-        \renewcommand\newblock{\par}%
-      \else
-        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
-      \fi
-      \sloppy\clubpenalty4000\widowpenalty4000%
-      \sfcode`\.=\@m}
-     {\def\@noitemerr
-       {\@latex@warning{Empty `thebibliography' environment}}%
-      \endlist}
-      \def\@cite#1{#1}%
-      \def\@lbibitem[#1]#2{\item[]\if@filesw
-        {\def\protect##1{\string ##1\space}\immediate
-      \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
-   \fi
-\else
-\@cons\@openbib@code{\noexpand\small}
-\fi
-
-\def\idxquad{\hskip 10\p@}% space that divides entry from number
-
-\def\@idxitem{\par\hangindent 10\p@}
-
-\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
-                \noindent\hangindent\wd0\box0}% index entry
-
-\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
-                \noindent\hangindent\wd0\box0}% order index entry
-
-\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
-
-\renewenvironment{theindex}
-               {\@mkboth{\indexname}{\indexname}%
-                \thispagestyle{empty}\parindent\z@
-                \parskip\z@ \@plus .3\p@\relax
-                \let\item\par
-                \def\,{\relax\ifmmode\mskip\thinmuskip
-                             \else\hskip0.2em\ignorespaces\fi}%
-                \normalfont\small
-                \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
-                }
-                {\end{multicols}}
-
-\renewcommand\footnoterule{%
-  \kern-3\p@
-  \hrule\@width 2truecm
-  \kern2.6\p@}
-  \newdimen\fnindent
-  \fnindent1em
-\long\def\@makefntext#1{%
-    \parindent \fnindent%
-    \leftskip \fnindent%
-    \noindent
-    \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
-
-\long\def\@makecaption#1#2{%
-  \small
-  \vskip\abovecaptionskip
-  \sbox\@tempboxa{{\bfseries #1.} #2}%
-  \ifdim \wd\@tempboxa >\hsize
-    {\bfseries #1.} #2\par
-  \else
-    \global \@minipagefalse
-    \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
-  \fi
-  \vskip\belowcaptionskip}
-
-\def\fps@figure{htbp}
-\def\fnum@figure{\figurename\thinspace\thefigure}
-\def \@floatboxreset {%
-        \reset@font
-        \small
-        \@setnobreak
-        \@setminipage
-}
-\def\fps@table{htbp}
-\def\fnum@table{\tablename~\thetable}
-\renewenvironment{table}
-               {\setlength\abovecaptionskip{0\p@}%
-                \setlength\belowcaptionskip{10\p@}%
-                \@float{table}}
-               {\end@float}
-\renewenvironment{table*}
-               {\setlength\abovecaptionskip{0\p@}%
-                \setlength\belowcaptionskip{10\p@}%
-                \@dblfloat{table}}
-               {\end@dblfloat}
-
-\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
-  ext@#1\endcsname}{#1}{\protect\numberline{\csname
-  the#1\endcsname}{\ignorespaces #2}}\begingroup
-    \@parboxrestore
-    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
-  \endgroup}
-
-% LaTeX does not provide a command to enter the authors institute
-% addresses. The \institute command is defined here.
-
-\newcounter{@inst}
-\newcounter{@auth}
-\newcounter{auco}
-\newdimen\instindent
-\newbox\authrun
-\newtoks\authorrunning
-\newtoks\tocauthor
-\newbox\titrun
-\newtoks\titlerunning
-\newtoks\toctitle
-
-\def\clearheadinfo{\gdef\@author{No Author Given}%
-                   \gdef\@title{No Title Given}%
-                   \gdef\@subtitle{}%
-                   \gdef\@institute{No Institute Given}%
-                   \gdef\@thanks{}%
-                   \global\titlerunning={}\global\authorrunning={}%
-                   \global\toctitle={}\global\tocauthor={}}
-
-\def\institute#1{\gdef\@institute{#1}}
-
-\def\institutename{\par
- \begingroup
- \parskip=\z@
- \parindent=\z@
- \setcounter{@inst}{1}%
- \def\and{\par\stepcounter{@inst}%
- \noindent$^{\the@inst}$\enspace\ignorespaces}%
- \setbox0=\vbox{\def\thanks##1{}\@institute}%
- \ifnum\c@@inst=1\relax
-   \gdef\fnnstart{0}%
- \else
-   \xdef\fnnstart{\c@@inst}%
-   \setcounter{@inst}{1}%
-   \noindent$^{\the@inst}$\enspace
- \fi
- \ignorespaces
- \@institute\par
- \endgroup}
-
-\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
-   {\star\star\star}\or \dagger\or \ddagger\or
-   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
-   \or \ddagger\ddagger \else\@ctrerr\fi}}
-
-\def\inst#1{\unskip$^{#1}$}
-\def\orcidID#1{\unskip$^{[#1]}$} % added MR 2018-03-10
-\def\fnmsep{\unskip$^,$}
-\def\email#1{{\tt#1}}
-
-\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
-\@ifpackageloaded{babel}{%
-\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
-\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
-\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
-\@ifundefined{extrasngerman}{}{\addto\extrasngerman{\switcht@deutsch}}%
-}{\switcht@@therlang}%
-\providecommand{\keywords}[1]{\def\and{{\textperiodcentered} }%
-\par\addvspace\baselineskip
-\noindent\keywordname\enspace\ignorespaces#1}%
-\@ifpackageloaded{hyperref}{%
-\def\doi#1{\href{https://doi.org/#1}{https://doi.org/#1}}}{
-\def\doi#1{https://doi.org/#1}}
-}
-\def\homedir{\~{ }}
-
-\def\subtitle#1{\gdef\@subtitle{#1}}
-\clearheadinfo
-%
-%%% to avoid hyperref warnings
-\providecommand*{\toclevel@author}{999}
-%%% to make title-entry parent of section-entries
-\providecommand*{\toclevel@title}{0}
-%
-\renewcommand\maketitle{\newpage
-\phantomsection
-  \refstepcounter{chapter}%
-  \stepcounter{section}%
-  \setcounter{section}{0}%
-  \setcounter{subsection}{0}%
-  \setcounter{figure}{0}
-  \setcounter{table}{0}
-  \setcounter{equation}{0}
-  \setcounter{footnote}{0}%
-  \begingroup
-    \parindent=\z@
-    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
-    \if@twocolumn
-      \ifnum \col@number=\@ne
-        \@maketitle
-      \else
-        \twocolumn[\@maketitle]%
-      \fi
-    \else
-      \newpage
-      \global\@topnum\z@   % Prevents figures from going at top of page.
-      \@maketitle
-    \fi
-    \thispagestyle{empty}\@thanks
-%
-    \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
-    \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
-    \instindent=\hsize
-    \advance\instindent by-\headlineindent
-    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
-       \addcontentsline{toc}{title}{\the\toctitle}\fi
-    \if@runhead
-       \if!\the\titlerunning!\else
-         \edef\@title{\the\titlerunning}%
-       \fi
-       \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
-       \ifdim\wd\titrun>\instindent
-          \typeout{Title too long for running head. Please supply}%
-          \typeout{a shorter form with \string\titlerunning\space prior to
-                   \string\maketitle}%
-          \global\setbox\titrun=\hbox{\small\rm
-          Title Suppressed Due to Excessive Length}%
-       \fi
-       \xdef\@title{\copy\titrun}%
-    \fi
-%
-    \if!\the\tocauthor!\relax
-      {\def\and{\noexpand\protect\noexpand\and}%
-       \def\inst##1{}%    added MR 2017-09-20 to remove inst numbers from the TOC
-       \def\orcidID##1{}% added MR 2017-09-20 to remove ORCID ids from the TOC
-      \protected@xdef\toc@uthor{\@author}}%
-    \else
-      \def\\{\noexpand\protect\noexpand\newline}%
-      \protected@xdef\scratch{\the\tocauthor}%
-      \protected@xdef\toc@uthor{\scratch}%
-    \fi
-    \addtocontents{toc}{\noexpand\protect\noexpand\authcount{\the\c@auco}}%
-    \addcontentsline{toc}{author}{\toc@uthor}%
-    \if@runhead
-       \if!\the\authorrunning!
-         \value{@inst}=\value{@auth}%
-         \setcounter{@auth}{1}%
-       \else
-         \edef\@author{\the\authorrunning}%
-       \fi
-       \global\setbox\authrun=\hbox{\def\inst##1{}%    added MR 2017-09-20 to remove inst numbers from the runninghead
-                                    \def\orcidID##1{}% added MR 2017-09-20 to remove ORCID ids from the runninghead
-                                    \small\unboldmath\@author\unskip}%
-       \ifdim\wd\authrun>\instindent
-          \typeout{Names of authors too long for running head. Please supply}%
-          \typeout{a shorter form with \string\authorrunning\space prior to
-                   \string\maketitle}%
-          \global\setbox\authrun=\hbox{\small\rm
-          Authors Suppressed Due to Excessive Length}%
-       \fi
-       \xdef\@author{\copy\authrun}%
-       \markboth{\@author}{\@title}%
-     \fi
-  \endgroup
-  \setcounter{footnote}{\fnnstart}%
-  \clearheadinfo}
-%
-\def\@maketitle{\newpage
- \markboth{}{}%
- \def\lastand{\ifnum\value{@inst}=2\relax
-                 \unskip{} \andname\
-              \else
-                 \unskip \lastandname\
-              \fi}%
- \def\and{\stepcounter{@auth}\relax
-          \ifnum\value{@auth}=\value{@inst}%
-             \lastand
-          \else
-             \unskip,
-          \fi}%
- \begin{center}%
- \let\newline\\
- {\Large \bfseries\boldmath
-  \pretolerance=10000
-  \@title \par}\vskip .8cm
-\if!\@subtitle!\else {\large \bfseries\boldmath
-  \vskip -.65cm
-  \pretolerance=10000
-  \@subtitle \par}\vskip .8cm\fi
- \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
- \def\thanks##1{}\@author}%
- \global\value{@inst}=\value{@auth}%
- \global\value{auco}=\value{@auth}%
- \setcounter{@auth}{1}%
-{\lineskip .5em
-\noindent\ignorespaces
-\@author\vskip.35cm}
- {\small\institutename}
- \end{center}%
- }
-
-% definition of the "\spnewtheorem" command.
-%
-% Usage:
-%
-%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
-% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
-% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
-%
-% New is "cap_font" and "body_font". It stands for
-% fontdefinition of the caption and the text itself.
-%
-% "\spnewtheorem*" gives a theorem without number.
-%
-% A defined spnewthoerem environment is used as described
-% by Lamport.
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\def\@thmcountersep{}
-\def\@thmcounterend{.}
-
-\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
-
-% definition of \spnewtheorem with number
-
-\def\@spnthm#1#2{%
-  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
-\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
-
-\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
-   {\@definecounter{#1}\@addtoreset{#1}{#3}%
-   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
-     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
-   \expandafter\xdef\csname #1name\endcsname{#2}%
-   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
-                              \global\@namedef{end#1}{\@endtheorem}}}
-
-\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
-   {\@definecounter{#1}%
-   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
-   \expandafter\xdef\csname #1name\endcsname{#2}%
-   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
-                               \global\@namedef{end#1}{\@endtheorem}}}
-
-\def\@spothm#1[#2]#3#4#5{%
-  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
-  {\expandafter\@ifdefinable\csname #1\endcsname
-  {\newaliascnt{#1}{#2}%
-  \expandafter\xdef\csname #1name\endcsname{#3}%
-  \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
-  \global\@namedef{end#1}{\@endtheorem}}}}
-
-\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
-\refstepcounter{#1}%
-\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
-
-\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
-                    \ignorespaces}
-
-\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
-       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
-
-\def\@spbegintheorem#1#2#3#4{\trivlist
-                 \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
-
-\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
-      \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
-
-% definition of \spnewtheorem* without number
-
-\def\@sthm#1#2{\@Ynthm{#1}{#2}}
-
-\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
-   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
-    \expandafter\xdef\csname #1name\endcsname{#2}%
-    \global\@namedef{end#1}{\@endtheorem}}}
-
-\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
-\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
-
-\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
-
-\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
-       {#4}{#2}{#3}\ignorespaces}
-
-\def\@Begintheorem#1#2#3{#3\trivlist
-                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
-
-\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
-      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
-
-\if@envcntsect
-   \def\@thmcountersep{.}
-   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
-\else
-   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
-   \if@envcntreset
-      \@addtoreset{theorem}{section}
-   \else
-      \@addtoreset{theorem}{chapter}
-   \fi
-\fi
-
-%definition of divers theorem environments
-\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
-\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
-\if@envcntsame % alle Umgebungen wie Theorem.
-   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
-\else % alle Umgebungen mit eigenem Zaehler
-   \if@envcntsect % mit section numeriert
-      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
-   \else % nicht mit section numeriert
-      \if@envcntreset
-         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
-                                   \@addtoreset{#1}{section}}
-      \else
-         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
-                                   \@addtoreset{#1}{chapter}}%
-      \fi
-   \fi
-\fi
-\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
-\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
-\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
-\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
-\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
-\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
-\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
-\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
-\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
-\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
-\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
-\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
-\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
-\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
-
-\def\@takefromreset#1#2{%
-    \def\@tempa{#1}%
-    \let\@tempd\@elt
-    \def\@elt##1{%
-        \def\@tempb{##1}%
-        \ifx\@tempa\@tempb\else
-            \@addtoreset{##1}{#2}%
-        \fi}%
-    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
-    \expandafter\def\csname cl@#2\endcsname{}%
-    \@tempc
-    \let\@elt\@tempd}
-
-\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
-      \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
-                  \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
-      \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
-      }
-
-\renewenvironment{abstract}{%
-      \list{}{\advance\topsep by0.35cm\relax\small
-      \leftmargin=1cm
-      \labelwidth=\z@
-      \listparindent=\z@
-      \itemindent\listparindent
-      \rightmargin\leftmargin}\item[\hskip\labelsep
-                                    \bfseries\abstractname]}
-    {\endlist}
-
-\newdimen\headlineindent             % dimension for space between
-\headlineindent=1.166cm              % number and text of headings.
-
-\def\ps@headings{\let\@mkboth\@gobbletwo
-   \let\@oddfoot\@empty\let\@evenfoot\@empty
-   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
-                  \leftmark\hfil}
-   \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
-                 \llap{\thepage}}
-   \def\chaptermark##1{}%
-   \def\sectionmark##1{}%
-   \def\subsectionmark##1{}}
-
-\def\ps@titlepage{\let\@mkboth\@gobbletwo
-   \let\@oddfoot\@empty\let\@evenfoot\@empty
-   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
-                  \hfil}
-   \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
-                 \llap{\thepage}}
-   \def\chaptermark##1{}%
-   \def\sectionmark##1{}%
-   \def\subsectionmark##1{}}
-
-\if@runhead\ps@headings\else
-\ps@empty\fi
-
-\setlength\arraycolsep{1.4\p@}
-\setlength\tabcolsep{1.4\p@}
-
-\endinput
-%end of file llncs.cls
diff --git a/Paper/lstcoq.sty b/Paper/lstcoq.sty
deleted file mode 100644
index 45f03ff8d62272c1bce5762f8715bfeb72018aa9..0000000000000000000000000000000000000000
--- a/Paper/lstcoq.sty
+++ /dev/null
@@ -1,93 +0,0 @@
-%%
-%% Coq definition (c) 2001 Guillaume Dufay 
-%%                           <Guillaume.Dufay@sophia.inria.fr>
-%%
-\lstdefinelanguage{Coq}%
-  {morekeywords={let,in,signature,polyinterpkind,termination,%
-      coq_certify_proof,termcrit,Goal,Notation,Class%
-      Variable,Inductive,CoInductive,Fixpoint,CoFixpoint,Function,%
-      Definition,Lemma,Theorem,Axiom,Local,Save,Grammar,Syntax,intro,%
-      trivial,Qed,intros,symmetry,simpl,rewrite,apply,elim,assumption,%
-      left,cut,match,auto,unfold,exact,right,Hypothesis,pattern,destruct,%
-      constructor,Defined,Fix,Record,Proof,induction,Hints,exists,%% exists_,%
-%      myexb,myforb,myex_,%
-      Parameter,Parameters,split,red,reflexivity,transitivity,if,then,else,%
-      Opaque,Transparent,inversion,absurd,generalize,Mutual,of,end,with,%
-      Class,Module,Type,Prop,Declare,Section,End,Import,fun,Rewall,match,fail,%
-      eauto,repeat,replace,progress,forall,forallb,autorewrite,Functional,%
-      Scheme,params,refine,using,discriminate,try,solve,functional,%
-      Instance,Corollary,%
-%      nat_ind,le_ind,%
-    },%
-   sensitive,%
-   morecomment=[n]{(*}{*)},%
-   commentstyle={\ttfamily\color{red!75!black}},
-   escapeinside={(*@}{@*)},%
-   morestring=[d]",%
-   literate={=>}{{$\Rightarrow$}}2{>->}{{$\rightarrowtail$}}2%
-{->}{{$\mathop{\to{}}$}}1{~}{{$\ $}}1{\\not}{{$\neg$}}1%
-{<->}{{$\Leftrightarrow$}}1
-% Necessite amssymb %%%%%%%%%%%%%%
-{\\Parrow}{{$\Rrightarrow$}}1%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-{==}{{$\equiv$}}1%
-{<>}{{$\neq$}}1%
-{<=}{{$\leq$}}1%
-{/\\}{{$\land$}}2{\\/}{{$\lor$}}2%
-{forall}{{$\forall$}}1{exists}{{$\exists$}}1%
-{forallb}{{forallb}}7%
-{myforb}{{forallb}}7%
-{myexb}{{existsb}}7%
-{myex_}{{exists_}}6%
-{exists_}{{exists}}6%
-{\\G}{{$\mathrm{\Gamma}$}}1{|-}{{$\vdash$}}2%
-{\\D}{{$\mathrm{\Delta}$}}1{-o}{{$\multimap$}}3%
-{\\E}{{$\mathrm{\Delta\!}$\textquotesingle}}2%
-{**}{{$\otimes$}}1{++}{{$\oplus$}}1%
-{\\emptyset}{{$\emptyset$}}1{\\in}{{$\in$}}2%
-{\\Top}{{$\top$}}1{\\U}{{$\cup$}}3%
-{epsilon}{{$\varepsilon$}}1%
-{\\!}{{$\!$}}1{\\phi}{{$\phi$}}1%
-{Qc}{{$\mathbb{Q}$}}1%
-{Rset}{{$\mathbb{R}$}}1%
-{Zset}{{$\mathbb{Z}$}}1%
-{\%R}{{$_\mathbb{R}$}}1%
-{\%R2}{{$_{\mathbb{R}^2}$}}1%
-{\%nat}{{$_\mathbb{N}$}}1%
-{\%Z}{{$_\mathbb{Z}$}}1%
-{\%V}{{$_V$}}1%
-{\]\]}{$\texttt{]\!]}$}1% $\texttt{$[\![#1]\!]$
-{\[\[}{$\texttt{[\![}$}1% $\texttt{$[\![#1]\!]$
-%{\{}{$\texttt{\{}$}1%
-{\{}{{\normalsize\bf\ttfamily\{}}1%
-{\}}{{\normalsize\bf\ttfamily\}}}1%
-{;}{{\normalsize\bf\ttfamily;}}1%
-{sigma}{$\sigma$}1%
-{delta}{$\delta$}1%
-{uplus}{$\uplus$}1%
-{lceil}{$\lceil$}1%
-{rceil}{$\rceil$}1%
-{singl}{$\texttt{\{\!\,\cdot\,\!\}}$}2%
-{\\o}{$\circ$}1%
-{^-1}{{${}^{\texttt -1}${}}}1%
-{__}{{\_}}1%
-% {_0}{{${}_{\tt 0}${}}}1%
- {_1}{{${}_{\tt 1}${}}}1%
- {_2}{{${}_{\tt 2}${}}}1%
- {_3}{{${}_{\tt 3}${}}}1%
-% {_4}{{${}_{\tt 4}${}}}1%
-% {_n}{{${}_{\tt n}${}}}1%
-% {_k}{{${}_{\tt k}${}}}1%
-{~}{$\neg$}1%
-}[keywords,comments,strings]%
-\endinput
-
-
-%%% Local Variables: ***
-%%% mode: latex ***
-%%% TeX-PDF-mode: t ***
-%%% ispell-dictionary: "british" ***
-%%% ispell-local-dictionary: "british" ***
-%%% mode: flyspell ***
-%%% TeX-master: "main" ***
-%%% End: ***
diff --git a/Paper/splncs04.bst b/Paper/splncs04.bst
deleted file mode 100644
index 3be8de3ac7c33fd679d5fd4f6709a6fcc4d21bc2..0000000000000000000000000000000000000000
--- a/Paper/splncs04.bst
+++ /dev/null
@@ -1,1548 +0,0 @@
-%% BibTeX bibliography style `splncs03'
-%%
-%% BibTeX bibliography style for use with numbered references in
-%% Springer Verlag's "Lecture Notes in Computer Science" series.
-%% (See Springer's documentation for llncs.cls for
-%% more details of the suggested reference format.)  Note that this
-%% file will not work for author-year style citations.
-%%
-%% Use \documentclass{llncs} and \bibliographystyle{splncs03}, and cite
-%% a reference with (e.g.) \cite{smith77} to get a "[1]" in the text.
-%%
-%% This file comes to you courtesy of Maurizio "Titto" Patrignani of
-%% Dipartimento di Informatica e Automazione Universita' Roma Tre
-%%
-%% ================================================================================================
-%% This was file `titto-lncs-02.bst' produced on Wed Apr 1, 2009
-%% Edited by hand by titto based on `titto-lncs-01.bst' (see below)
-%%
-%% CHANGES (with respect to titto-lncs-01.bst):
-%% - Removed the call to \urlprefix (thus no "URL" string is added to the output)
-%% ================================================================================================
-%% This was file `titto-lncs-01.bst' produced on Fri Aug 22, 2008
-%% Edited by hand by titto based on `titto.bst' (see below)
-%%
-%% CHANGES (with respect to titto.bst):
-%% - Removed the "capitalize" command for editors string "(eds.)" and "(ed.)"
-%% - Introduced the functions titto.bbl.pages and titto.bbl.page for journal pages (without "pp.")
-%% - Added a new.sentence command to separate with a dot booktitle and series in the inproceedings
-%% - Commented all new.block commands before urls and notes (to separate them with a comma)
-%% - Introduced the functions titto.bbl.volume for handling journal volumes (without "vol." label)
-%% - Used for editors the same name conventions used for authors (see function format.in.ed.booktitle)
-%% - Removed a \newblock to avoid long spaces between title and "In: ..."
-%% - Added function titto.space.prefix to add a space instead of "~" after the (removed) "vol." label
-%% - Added doi
-%% ================================================================================================
-%% This was file `titto.bst',
-%% generated with the docstrip utility.
-%%
-%% The original source files were:
-%%
-%% merlin.mbs  (with options: `vonx,nm-rvvc,yr-par,jttl-rm,volp-com,jwdpg,jwdvol,numser,ser-vol,jnm-x,btit-rm,bt-rm,edparxc,bkedcap,au-col,in-col,fin-bare,pp,ed,abr,mth-bare,xedn,jabr,and-com,and-com-ed,xand,url,url-blk,em-x,nfss,')
-%% ----------------------------------------
-%% *** Tentative .bst file for Springer LNCS ***
-%%
-%% Copyright 1994-2007 Patrick W Daly
- % ===============================================================
- % IMPORTANT NOTICE:
- % This bibliographic style (bst) file has been generated from one or
- % more master bibliographic style (mbs) files, listed above.
- %
- % This generated file can be redistributed and/or modified under the terms
- % of the LaTeX Project Public License Distributed from CTAN
- % archives in directory macros/latex/base/lppl.txt; either
- % version 1 of the License, or any later version.
- % ===============================================================
- % Name and version information of the main mbs file:
- % \ProvidesFile{merlin.mbs}[2007/04/24 4.20 (PWD, AO, DPC)]
- %   For use with BibTeX version 0.99a or later
- %-------------------------------------------------------------------
- % This bibliography style file is intended for texts in ENGLISH
- % This is a numerical citation style, and as such is standard LaTeX.
- % It requires no extra package to interface to the main text.
- % The form of the \bibitem entries is
- %   \bibitem{key}...
- % Usage of \cite is as follows:
- %   \cite{key} ==>>          [#]
- %   \cite[chap. 2]{key} ==>> [#, chap. 2]
- % where # is a number determined by the ordering in the reference list.
- % The order in the reference list is alphabetical by authors.
- %---------------------------------------------------------------------
-
-ENTRY
-  { address
-    author
-    booktitle
-    chapter
-    doi
-    edition
-    editor
-    eid
-    howpublished
-    institution
-    journal
-    key
-    month
-    note
-    number
-    organization
-    pages
-    publisher
-    school
-    series
-    title
-    type
-    url
-    volume
-    year
-  }
-  {}
-  { label }
-INTEGERS { output.state before.all mid.sentence after.sentence after.block }
-FUNCTION {init.state.consts}
-{ #0 'before.all :=
-  #1 'mid.sentence :=
-  #2 'after.sentence :=
-  #3 'after.block :=
-}
-STRINGS { s t}
-FUNCTION {output.nonnull}
-{ 's :=
-  output.state mid.sentence =
-    { ", " * write$ }
-    { output.state after.block =
-        { add.period$ write$
-%          newline$
-%          "\newblock " write$  % removed for titto-lncs-01
-          " " write$            % to avoid long spaces between title and "In: ..."
-        }
-        { output.state before.all =
-            'write$
-            { add.period$ " " * write$ }
-          if$
-        }
-      if$
-      mid.sentence 'output.state :=
-    }
-  if$
-  s
-}
-FUNCTION {output}
-{ duplicate$ empty$
-    'pop$
-    'output.nonnull
-  if$
-}
-FUNCTION {output.check}
-{ 't :=
-  duplicate$ empty$
-    { pop$ "empty " t * " in " * cite$ * warning$ }
-    'output.nonnull
-  if$
-}
-FUNCTION {fin.entry}
-{ duplicate$ empty$
-    'pop$
-    'write$
-  if$
-  newline$
-}
-
-FUNCTION {new.block}
-{ output.state before.all =
-    'skip$
-    { after.block 'output.state := }
-  if$
-}
-FUNCTION {new.sentence}
-{ output.state after.block =
-    'skip$
-    { output.state before.all =
-        'skip$
-        { after.sentence 'output.state := }
-      if$
-    }
-  if$
-}
-FUNCTION {add.blank}
-{  " " * before.all 'output.state :=
-}
-
-
-FUNCTION {add.colon}
-{ duplicate$ empty$
-    'skip$
-    { ":" * add.blank }
-  if$
-}
-
-FUNCTION {date.block}
-{
-  new.block
-}
-
-FUNCTION {not}
-{   { #0 }
-    { #1 }
-  if$
-}
-FUNCTION {and}
-{   'skip$
-    { pop$ #0 }
-  if$
-}
-FUNCTION {or}
-{   { pop$ #1 }
-    'skip$
-  if$
-}
-STRINGS {z}
-FUNCTION {remove.dots}
-{ 'z :=
-  ""
-  { z empty$ not }
-  { z #1 #1 substring$
-    z #2 global.max$ substring$ 'z :=
-    duplicate$ "." = 'pop$
-      { * }
-    if$
-  }
-  while$
-}
-FUNCTION {new.block.checka}
-{ empty$
-    'skip$
-    'new.block
-  if$
-}
-FUNCTION {new.block.checkb}
-{ empty$
-  swap$ empty$
-  and
-    'skip$
-    'new.block
-  if$
-}
-FUNCTION {new.sentence.checka}
-{ empty$
-    'skip$
-    'new.sentence
-  if$
-}
-FUNCTION {new.sentence.checkb}
-{ empty$
-  swap$ empty$
-  and
-    'skip$
-    'new.sentence
-  if$
-}
-FUNCTION {field.or.null}
-{ duplicate$ empty$
-    { pop$ "" }
-    'skip$
-  if$
-}
-FUNCTION {emphasize}
-{ skip$ }
-
-FUNCTION {embolden}
-{ duplicate$ empty$
-{ pop$ "" }
-{ "\textbf{" swap$ * "}" * }
-if$
-}
-FUNCTION {tie.or.space.prefix}
-{ duplicate$ text.length$ #5 <
-    { "~" }
-    { " " }
-  if$
-  swap$
-}
-FUNCTION {titto.space.prefix} %  always introduce a space
-{ duplicate$ text.length$ #3 <
-    { " " }
-    { " " }
-  if$
-  swap$
-}
-
-
-FUNCTION {capitalize}
-{ "u" change.case$ "t" change.case$ }
-
-FUNCTION {space.word}
-{ " " swap$ * " " * }
- % Here are the language-specific definitions for explicit words.
- % Each function has a name bbl.xxx where xxx is the English word.
- % The language selected here is ENGLISH
-FUNCTION {bbl.and}
-{ "and"}
-
-FUNCTION {bbl.etal}
-{ "et~al." }
-
-FUNCTION {bbl.editors}
-{ "eds." }
-
-FUNCTION {bbl.editor}
-{ "ed." }
-
-FUNCTION {bbl.edby}
-{ "edited by" }
-
-FUNCTION {bbl.edition}
-{ "edn." }
-
-FUNCTION {bbl.volume}
-{ "vol." }
-
-FUNCTION {titto.bbl.volume} % for handling journals
-{ "" }
-
-FUNCTION {bbl.of}
-{ "of" }
-
-FUNCTION {bbl.number}
-{ "no." }
-
-FUNCTION {bbl.nr}
-{ "no." }
-
-FUNCTION {bbl.in}
-{ "in" }
-
-FUNCTION {bbl.pages}
-{ "pp." }
-
-FUNCTION {bbl.page}
-{ "p." }
-
-FUNCTION {titto.bbl.pages} % for journals
-{ "" }
-
-FUNCTION {titto.bbl.page}  % for journals
-{ "" }
-
-FUNCTION {bbl.chapter}
-{ "chap." }
-
-FUNCTION {bbl.techrep}
-{ "Tech. Rep." }
-
-FUNCTION {bbl.mthesis}
-{ "Master's thesis" }
-
-FUNCTION {bbl.phdthesis}
-{ "Ph.D. thesis" }
-
-MACRO {jan} {"Jan."}
-
-MACRO {feb} {"Feb."}
-
-MACRO {mar} {"Mar."}
-
-MACRO {apr} {"Apr."}
-
-MACRO {may} {"May"}
-
-MACRO {jun} {"Jun."}
-
-MACRO {jul} {"Jul."}
-
-MACRO {aug} {"Aug."}
-
-MACRO {sep} {"Sep."}
-
-MACRO {oct} {"Oct."}
-
-MACRO {nov} {"Nov."}
-
-MACRO {dec} {"Dec."}
-
-MACRO {acmcs} {"ACM Comput. Surv."}
-
-MACRO {acta} {"Acta Inf."}
-
-MACRO {cacm} {"Commun. ACM"}
-
-MACRO {ibmjrd} {"IBM J. Res. Dev."}
-
-MACRO {ibmsj} {"IBM Syst.~J."}
-
-MACRO {ieeese} {"IEEE Trans. Software Eng."}
-
-MACRO {ieeetc} {"IEEE Trans. Comput."}
-
-MACRO {ieeetcad}
- {"IEEE Trans. Comput. Aid. Des."}
-
-MACRO {ipl} {"Inf. Process. Lett."}
-
-MACRO {jacm} {"J.~ACM"}
-
-MACRO {jcss} {"J.~Comput. Syst. Sci."}
-
-MACRO {scp} {"Sci. Comput. Program."}
-
-MACRO {sicomp} {"SIAM J. Comput."}
-
-MACRO {tocs} {"ACM Trans. Comput. Syst."}
-
-MACRO {tods} {"ACM Trans. Database Syst."}
-
-MACRO {tog} {"ACM Trans. Graphic."}
-
-MACRO {toms} {"ACM Trans. Math. Software"}
-
-MACRO {toois} {"ACM Trans. Office Inf. Syst."}
-
-MACRO {toplas} {"ACM Trans. Progr. Lang. Syst."}
-
-MACRO {tcs} {"Theor. Comput. Sci."}
-
-FUNCTION {bibinfo.check}
-{ swap$
-  duplicate$ missing$
-    {
-      pop$ pop$
-      ""
-    }
-    { duplicate$ empty$
-        {
-          swap$ pop$
-        }
-        { swap$
-          pop$
-        }
-      if$
-    }
-  if$
-}
-FUNCTION {bibinfo.warn}
-{ swap$
-  duplicate$ missing$
-    {
-      swap$ "missing " swap$ * " in " * cite$ * warning$ pop$
-      ""
-    }
-    { duplicate$ empty$
-        {
-          swap$ "empty " swap$ * " in " * cite$ * warning$
-        }
-        { swap$
-          pop$
-        }
-      if$
-    }
-  if$
-}
-FUNCTION {format.url}
-{ url empty$
-    { "" }
-%    { "\urlprefix\url{" url * "}" * }
-    { "\url{" url * "}" * }  % changed in titto-lncs-02.bst
-  if$
-}
-
-FUNCTION {format.doi} % added in splncs04.bst
-{ doi empty$
-     { "" }
-     { after.block 'output.state :=
-       "\doi{" doi * "}" * }
-  if$
-}
-
-INTEGERS { nameptr namesleft numnames }
-
-
-STRINGS  { bibinfo}
-
-FUNCTION {format.names}
-{ 'bibinfo :=
-  duplicate$ empty$ 'skip$ {
-  's :=
-  "" 't :=
-  #1 'nameptr :=
-  s num.names$ 'numnames :=
-  numnames 'namesleft :=
-    { namesleft #0 > }
-    { s nameptr
-      "{vv~}{ll}{, jj}{, f{.}.}"
-      format.name$
-      bibinfo bibinfo.check
-      't :=
-      nameptr #1 >
-        {
-          namesleft #1 >
-            { ", " * t * }
-            {
-              s nameptr "{ll}" format.name$ duplicate$ "others" =
-                { 't := }
-                { pop$ }
-              if$
-              "," *
-              t "others" =
-                {
-                  " " * bbl.etal *
-                }
-                { " " * t * }
-              if$
-            }
-          if$
-        }
-        't
-      if$
-      nameptr #1 + 'nameptr :=
-      namesleft #1 - 'namesleft :=
-    }
-  while$
-  } if$
-}
-FUNCTION {format.names.ed}
-{
-  'bibinfo :=
-  duplicate$ empty$ 'skip$ {
-  's :=
-  "" 't :=
-  #1 'nameptr :=
-  s num.names$ 'numnames :=
-  numnames 'namesleft :=
-    { namesleft #0 > }
-    { s nameptr
-      "{f{.}.~}{vv~}{ll}{ jj}"
-      format.name$
-      bibinfo bibinfo.check
-      't :=
-      nameptr #1 >
-        {
-          namesleft #1 >
-            { ", " * t * }
-            {
-              s nameptr "{ll}" format.name$ duplicate$ "others" =
-                { 't := }
-                { pop$ }
-              if$
-              "," *
-              t "others" =
-                {
-
-                  " " * bbl.etal *
-                }
-                { " " * t * }
-              if$
-            }
-          if$
-        }
-        't
-      if$
-      nameptr #1 + 'nameptr :=
-      namesleft #1 - 'namesleft :=
-    }
-  while$
-  } if$
-}
-FUNCTION {format.authors}
-{ author "author" format.names
-}
-FUNCTION {get.bbl.editor}
-{ editor num.names$ #1 > 'bbl.editors 'bbl.editor if$ }
-
-FUNCTION {format.editors}
-{ editor "editor" format.names duplicate$ empty$ 'skip$
-    {
-      " " *
-      get.bbl.editor
-%      capitalize
-   "(" swap$ * ")" *
-      *
-    }
-  if$
-}
-FUNCTION {format.note}
-{
- note empty$
-    { "" }
-    { note #1 #1 substring$
-      duplicate$ "{" =
-        'skip$
-        { output.state mid.sentence =
-          { "l" }
-          { "u" }
-        if$
-        change.case$
-        }
-      if$
-      note #2 global.max$ substring$ * "note" bibinfo.check
-    }
-  if$
-}
-
-FUNCTION {format.title}
-{ title
-  duplicate$ empty$ 'skip$
-    { "t" change.case$ }
-  if$
-  "title" bibinfo.check
-}
-FUNCTION {output.bibitem}
-{ newline$
-  "\bibitem{" write$
-  cite$ write$
-  "}" write$
-  newline$
-  ""
-  before.all 'output.state :=
-}
-
-FUNCTION {n.dashify}
-{
-  't :=
-  ""
-    { t empty$ not }
-    { t #1 #1 substring$ "-" =
-        { t #1 #2 substring$ "--" = not
-            { "--" *
-              t #2 global.max$ substring$ 't :=
-            }
-            {   { t #1 #1 substring$ "-" = }
-                { "-" *
-                  t #2 global.max$ substring$ 't :=
-                }
-              while$
-            }
-          if$
-        }
-        { t #1 #1 substring$ *
-          t #2 global.max$ substring$ 't :=
-        }
-      if$
-    }
-  while$
-}
-
-FUNCTION {word.in}
-{ bbl.in capitalize
-  ":" *
-  " " * }
-
-FUNCTION {format.date}
-{
-  month "month" bibinfo.check
-  duplicate$ empty$
-  year  "year"  bibinfo.check duplicate$ empty$
-    { swap$ 'skip$
-        { "there's a month but no year in " cite$ * warning$ }
-      if$
-      *
-    }
-    { swap$ 'skip$
-        {
-          swap$
-          " " * swap$
-        }
-      if$
-      *
-      remove.dots
-    }
-  if$
-  duplicate$ empty$
-    'skip$
-    {
-      before.all 'output.state :=
-    " (" swap$ * ")" *
-    }
-  if$
-}
-FUNCTION {format.btitle}
-{ title "title" bibinfo.check
-  duplicate$ empty$ 'skip$
-    {
-    }
-  if$
-}
-FUNCTION {either.or.check}
-{ empty$
-    'pop$
-    { "can't use both " swap$ * " fields in " * cite$ * warning$ }
-  if$
-}
-FUNCTION {format.bvolume}
-{ volume empty$
-    { "" }
-    { bbl.volume volume tie.or.space.prefix
-      "volume" bibinfo.check * *
-      series "series" bibinfo.check
-      duplicate$ empty$ 'pop$
-        { emphasize ", " * swap$ * }
-      if$
-      "volume and number" number either.or.check
-    }
-  if$
-}
-FUNCTION {format.number.series}
-{ volume empty$
-    { number empty$
-        { series field.or.null }
-        { output.state mid.sentence =
-            { bbl.number }
-            { bbl.number capitalize }
-          if$
-          number tie.or.space.prefix "number" bibinfo.check * *
-          series empty$
-            { "there's a number but no series in " cite$ * warning$ }
-            { bbl.in space.word *
-              series "series" bibinfo.check *
-            }
-          if$
-        }
-      if$
-    }
-    { "" }
-  if$
-}
-
-FUNCTION {format.edition}
-{ edition duplicate$ empty$ 'skip$
-    {
-      output.state mid.sentence =
-        { "l" }
-        { "t" }
-      if$ change.case$
-      "edition" bibinfo.check
-      " " * bbl.edition *
-    }
-  if$
-}
-INTEGERS { multiresult }
-FUNCTION {multi.page.check}
-{ 't :=
-  #0 'multiresult :=
-    { multiresult not
-      t empty$ not
-      and
-    }
-    { t #1 #1 substring$
-      duplicate$ "-" =
-      swap$ duplicate$ "," =
-      swap$ "+" =
-      or or
-        { #1 'multiresult := }
-        { t #2 global.max$ substring$ 't := }
-      if$
-    }
-  while$
-  multiresult
-}
-FUNCTION {format.pages}
-{ pages duplicate$ empty$ 'skip$
-    { duplicate$ multi.page.check
-        {
-          bbl.pages swap$
-          n.dashify
-        }
-        {
-          bbl.page swap$
-        }
-      if$
-      tie.or.space.prefix
-      "pages" bibinfo.check
-      * *
-    }
-  if$
-}
-FUNCTION {format.journal.pages}
-{ pages duplicate$ empty$ 'pop$
-    { swap$ duplicate$ empty$
-        { pop$ pop$ format.pages }
-        {
-          ", " *
-          swap$
-          n.dashify
-          pages multi.page.check
-            'titto.bbl.pages
-            'titto.bbl.page
-          if$
-          swap$ tie.or.space.prefix
-          "pages" bibinfo.check
-          * *
-          *
-        }
-      if$
-    }
-  if$
-}
-FUNCTION {format.journal.eid}
-{ eid "eid" bibinfo.check
-  duplicate$ empty$ 'pop$
-    { swap$ duplicate$ empty$ 'skip$
-      {
-          ", " *
-      }
-      if$
-      swap$ *
-    }
-  if$
-}
-FUNCTION {format.vol.num.pages} % this function is used only for journal entries
-{ volume field.or.null embolden
-  duplicate$ empty$ 'skip$
-    {
-%    bbl.volume swap$ tie.or.space.prefix
-     titto.bbl.volume swap$ titto.space.prefix
-%            rationale for the change above: for journals you don't want "vol." label
-%            hence it does not make sense to attach the journal number to the label when
-%            it is short
-      "volume" bibinfo.check
-      * *
-      }
-  if$
-  number "number" bibinfo.check duplicate$ empty$ 'skip$
-    {
-      swap$ duplicate$ empty$
-        { "there's a number but no volume in " cite$ * warning$ }
-        'skip$
-      if$
-      swap$
-      "(" swap$ * ")" *
-    }
-  if$ *
-  eid empty$
-    { format.journal.pages }
-    { format.journal.eid }
-  if$
-}
-
-FUNCTION {format.chapter.pages}
-{ chapter empty$
-    'format.pages
-    { type empty$
-        { bbl.chapter }
-        { type "l" change.case$
-          "type" bibinfo.check
-        }
-      if$
-      chapter tie.or.space.prefix
-      "chapter" bibinfo.check
-      * *
-      pages empty$
-        'skip$
-        { ", " * format.pages * }
-      if$
-    }
-  if$
-}
-
-FUNCTION {format.booktitle}
-{
-  booktitle "booktitle" bibinfo.check
-}
-FUNCTION {format.in.ed.booktitle}
-{ format.booktitle duplicate$ empty$ 'skip$
-    {
-%     editor "editor" format.names.ed duplicate$ empty$ 'pop$ % changed by titto
-      editor "editor" format.names duplicate$ empty$ 'pop$
-        {
-          " " *
-          get.bbl.editor
-%          capitalize
-          "(" swap$ * ") " *
-          * swap$
-          * }
-      if$
-      word.in swap$ *
-    }
-  if$
-}
-FUNCTION {empty.misc.check}
-{ author empty$ title empty$ howpublished empty$
-  month empty$ year empty$ note empty$
-  and and and and and
-  key empty$ not and
-    { "all relevant fields are empty in " cite$ * warning$ }
-    'skip$
-  if$
-}
-FUNCTION {format.thesis.type}
-{ type duplicate$ empty$
-    'pop$
-    { swap$ pop$
-      "t" change.case$ "type" bibinfo.check
-    }
-  if$
-}
-FUNCTION {format.tr.number}
-{ number "number" bibinfo.check
-  type duplicate$ empty$
-    { pop$ bbl.techrep }
-    'skip$
-  if$
-  "type" bibinfo.check
-  swap$ duplicate$ empty$
-    { pop$ "t" change.case$ }
-    { tie.or.space.prefix * * }
-  if$
-}
-FUNCTION {format.article.crossref}
-{
-  key duplicate$ empty$
-    { pop$
-      journal duplicate$ empty$
-        { "need key or journal for " cite$ * " to crossref " * crossref * warning$ }
-        { "journal" bibinfo.check emphasize word.in swap$ * }
-      if$
-    }
-    { word.in swap$ * " " *}
-  if$
-  " \cite{" * crossref * "}" *
-}
-FUNCTION {format.crossref.editor}
-{ editor #1 "{vv~}{ll}" format.name$
-  "editor" bibinfo.check
-  editor num.names$ duplicate$
-  #2 >
-    { pop$
-      "editor" bibinfo.check
-      " " * bbl.etal
-      *
-    }
-    { #2 <
-        'skip$
-        { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =
-            {
-              "editor" bibinfo.check
-              " " * bbl.etal
-              *
-            }
-            {
-             bbl.and space.word
-              * editor #2 "{vv~}{ll}" format.name$
-              "editor" bibinfo.check
-              *
-            }
-          if$
-        }
-      if$
-    }
-  if$
-}
-FUNCTION {format.book.crossref}
-{ volume duplicate$ empty$
-    { "empty volume in " cite$ * "'s crossref of " * crossref * warning$
-      pop$ word.in
-    }
-    { bbl.volume
-      capitalize
-      swap$ tie.or.space.prefix "volume" bibinfo.check * * bbl.of space.word *
-    }
-  if$
-  editor empty$
-  editor field.or.null author field.or.null =
-  or
-    { key empty$
-        { series empty$
-            { "need editor, key, or series for " cite$ * " to crossref " *
-              crossref * warning$
-              "" *
-            }
-            { series emphasize * }
-          if$
-        }
-        { key * }
-      if$
-    }
-    { format.crossref.editor * }
-  if$
-  " \cite{" * crossref * "}" *
-}
-FUNCTION {format.incoll.inproc.crossref}
-{
-  editor empty$
-  editor field.or.null author field.or.null =
-  or
-    { key empty$
-        { format.booktitle duplicate$ empty$
-            { "need editor, key, or booktitle for " cite$ * " to crossref " *
-              crossref * warning$
-            }
-            { word.in swap$ * }
-          if$
-        }
-        { word.in key * " " *}
-      if$
-    }
-    { word.in format.crossref.editor * " " *}
-  if$
-  " \cite{" * crossref * "}" *
-}
-FUNCTION {format.org.or.pub}
-{ 't :=
-  ""
-  address empty$ t empty$ and
-    'skip$
-    {
-      t empty$
-        { address "address" bibinfo.check *
-        }
-        { t *
-          address empty$
-            'skip$
-            { ", " * address "address" bibinfo.check * }
-          if$
-        }
-      if$
-    }
-  if$
-}
-FUNCTION {format.publisher.address}
-{ publisher "publisher" bibinfo.warn format.org.or.pub
-}
-
-FUNCTION {format.organization.address}
-{ organization "organization" bibinfo.check format.org.or.pub
-}
-
-FUNCTION {article}
-{ output.bibitem
-  format.authors "author" output.check
-  add.colon
-  new.block
-  format.title "title" output.check
-  new.block
-  crossref missing$
-    {
-      journal
-      "journal" bibinfo.check
-      "journal" output.check
-      add.blank
-      format.vol.num.pages output
-      format.date "year" output.check
-    }
-    { format.article.crossref output.nonnull
-      format.pages output
-    }
-  if$
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-FUNCTION {book}
-{ output.bibitem
-  author empty$
-    { format.editors "author and editor" output.check
-      add.colon
-    }
-    { format.authors output.nonnull
-      add.colon
-      crossref missing$
-        { "author and editor" editor either.or.check }
-        'skip$
-      if$
-    }
-  if$
-  new.block
-  format.btitle "title" output.check
-  crossref missing$
-    { format.bvolume output
-      new.block
-      new.sentence
-      format.number.series output
-      format.publisher.address output
-    }
-    {
-      new.block
-      format.book.crossref output.nonnull
-    }
-  if$
-  format.edition output
-  format.date "year" output.check
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-FUNCTION {booklet}
-{ output.bibitem
-  format.authors output
-  add.colon
-  new.block
-  format.title "title" output.check
-  new.block
-  howpublished "howpublished" bibinfo.check output
-  address "address" bibinfo.check output
-  format.date output
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-
-FUNCTION {inbook}
-{ output.bibitem
-  author empty$
-    { format.editors "author and editor" output.check
-      add.colon
-    }
-    { format.authors output.nonnull
-      add.colon
-      crossref missing$
-        { "author and editor" editor either.or.check }
-        'skip$
-      if$
-    }
-  if$
-  new.block
-  format.btitle "title" output.check
-  crossref missing$
-    {
-      format.bvolume output
-      format.chapter.pages "chapter and pages" output.check
-      new.block
-      new.sentence
-      format.number.series output
-      format.publisher.address output
-    }
-    {
-      format.chapter.pages "chapter and pages" output.check
-      new.block
-      format.book.crossref output.nonnull
-    }
-  if$
-  format.edition output
-  format.date "year" output.check
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-
-FUNCTION {incollection}
-{ output.bibitem
-  format.authors "author" output.check
-  add.colon
-  new.block
-  format.title "title" output.check
-  new.block
-  crossref missing$
-    { format.in.ed.booktitle "booktitle" output.check
-      format.bvolume output
-      format.chapter.pages output
-      new.sentence
-      format.number.series output
-      format.publisher.address output
-      format.edition output
-      format.date "year" output.check
-    }
-    { format.incoll.inproc.crossref output.nonnull
-      format.chapter.pages output
-    }
-  if$
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-FUNCTION {inproceedings}
-{ output.bibitem
-  format.authors "author" output.check
-  add.colon
-  new.block
-  format.title "title" output.check
-  new.block
-  crossref missing$
-    { format.in.ed.booktitle "booktitle" output.check
-      new.sentence % added by titto
-      format.bvolume output
-      format.pages output
-      new.sentence
-      format.number.series output
-      publisher empty$
-        { format.organization.address output }
-        { organization "organization" bibinfo.check output
-          format.publisher.address output
-        }
-      if$
-      format.date "year" output.check
-    }
-    { format.incoll.inproc.crossref output.nonnull
-      format.pages output
-    }
-  if$
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-FUNCTION {conference} { inproceedings }
-FUNCTION {manual}
-{ output.bibitem
-  author empty$
-    { organization "organization" bibinfo.check
-      duplicate$ empty$ 'pop$
-        { output
-          address "address" bibinfo.check output
-        }
-      if$
-    }
-    { format.authors output.nonnull }
-  if$
-  add.colon
-  new.block
-  format.btitle "title" output.check
-  author empty$
-    { organization empty$
-        {
-          address new.block.checka
-          address "address" bibinfo.check output
-        }
-        'skip$
-      if$
-    }
-    {
-      organization address new.block.checkb
-      organization "organization" bibinfo.check output
-      address "address" bibinfo.check output
-    }
-  if$
-  format.edition output
-  format.date output
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-
-FUNCTION {mastersthesis}
-{ output.bibitem
-  format.authors "author" output.check
-  add.colon
-  new.block
-  format.btitle
-  "title" output.check
-  new.block
-  bbl.mthesis format.thesis.type output.nonnull
-  school "school" bibinfo.warn output
-  address "address" bibinfo.check output
-  format.date "year" output.check
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-
-FUNCTION {misc}
-{ output.bibitem
-  format.authors output
-  add.colon
-  title howpublished new.block.checkb
-  format.title output
-  howpublished new.block.checka
-  howpublished "howpublished" bibinfo.check output
-  format.date output
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-  empty.misc.check
-}
-FUNCTION {phdthesis}
-{ output.bibitem
-  format.authors "author" output.check
-  add.colon
-  new.block
-  format.btitle
-  "title" output.check
-  new.block
-  bbl.phdthesis format.thesis.type output.nonnull
-  school "school" bibinfo.warn output
-  address "address" bibinfo.check output
-  format.date "year" output.check
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-
-FUNCTION {proceedings}
-{ output.bibitem
-  editor empty$
-    { organization "organization" bibinfo.check output
-    }
-    { format.editors output.nonnull }
-  if$
-  add.colon
-  new.block
-  format.btitle "title" output.check
-  format.bvolume output
-  editor empty$
-    { publisher empty$
-        {  format.number.series output }
-        {
-          new.sentence
-          format.number.series output
-          format.publisher.address output
-        }
-      if$
-    }
-    { publisher empty$
-        {
-          new.sentence
-          format.number.series output
-          format.organization.address output }
-        {
-          new.sentence
-          format.number.series output
-          organization "organization" bibinfo.check output
-          format.publisher.address output
-        }
-      if$
-     }
-  if$
-      format.date "year" output.check
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-
-FUNCTION {techreport}
-{ output.bibitem
-  format.authors "author" output.check
-  add.colon
-  new.block
-  format.title
-  "title" output.check
-  new.block
-  format.tr.number output.nonnull
-  institution "institution" bibinfo.warn output
-  address "address" bibinfo.check output
-  format.date "year" output.check
-%  new.block
-  format.doi output
-  format.url output
-%  new.block
-  format.note output
-  fin.entry
-}
-
-FUNCTION {unpublished}
-{ output.bibitem
-  format.authors "author" output.check
-  add.colon
-  new.block
-  format.title "title" output.check
-  format.date output
-%  new.block
-  format.url output
-%  new.block
-  format.note "note" output.check
-  fin.entry
-}
-
-FUNCTION {default.type} { misc }
-READ
-FUNCTION {sortify}
-{ purify$
-  "l" change.case$
-}
-INTEGERS { len }
-FUNCTION {chop.word}
-{ 's :=
-  'len :=
-  s #1 len substring$ =
-    { s len #1 + global.max$ substring$ }
-    's
-  if$
-}
-FUNCTION {sort.format.names}
-{ 's :=
-  #1 'nameptr :=
-  ""
-  s num.names$ 'numnames :=
-  numnames 'namesleft :=
-    { namesleft #0 > }
-    { s nameptr
-      "{ll{ }}{  ff{ }}{  jj{ }}"
-      format.name$ 't :=
-      nameptr #1 >
-        {
-          "   "  *
-          namesleft #1 = t "others" = and
-            { "zzzzz" * }
-            { t sortify * }
-          if$
-        }
-        { t sortify * }
-      if$
-      nameptr #1 + 'nameptr :=
-      namesleft #1 - 'namesleft :=
-    }
-  while$
-}
-
-FUNCTION {sort.format.title}
-{ 't :=
-  "A " #2
-    "An " #3
-      "The " #4 t chop.word
-    chop.word
-  chop.word
-  sortify
-  #1 global.max$ substring$
-}
-FUNCTION {author.sort}
-{ author empty$
-    { key empty$
-        { "to sort, need author or key in " cite$ * warning$
-          ""
-        }
-        { key sortify }
-      if$
-    }
-    { author sort.format.names }
-  if$
-}
-FUNCTION {author.editor.sort}
-{ author empty$
-    { editor empty$
-        { key empty$
-            { "to sort, need author, editor, or key in " cite$ * warning$
-              ""
-            }
-            { key sortify }
-          if$
-        }
-        { editor sort.format.names }
-      if$
-    }
-    { author sort.format.names }
-  if$
-}
-FUNCTION {author.organization.sort}
-{ author empty$
-    { organization empty$
-        { key empty$
-            { "to sort, need author, organization, or key in " cite$ * warning$
-              ""
-            }
-            { key sortify }
-          if$
-        }
-        { "The " #4 organization chop.word sortify }
-      if$
-    }
-    { author sort.format.names }
-  if$
-}
-FUNCTION {editor.organization.sort}
-{ editor empty$
-    { organization empty$
-        { key empty$
-            { "to sort, need editor, organization, or key in " cite$ * warning$
-              ""
-            }
-            { key sortify }
-          if$
-        }
-        { "The " #4 organization chop.word sortify }
-      if$
-    }
-    { editor sort.format.names }
-  if$
-}
-FUNCTION {presort}
-{ type$ "book" =
-  type$ "inbook" =
-  or
-    'author.editor.sort
-    { type$ "proceedings" =
-        'editor.organization.sort
-        { type$ "manual" =
-            'author.organization.sort
-            'author.sort
-          if$
-        }
-      if$
-    }
-  if$
-  "    "
-  *
-  year field.or.null sortify
-  *
-  "    "
-  *
-  title field.or.null
-  sort.format.title
-  *
-  #1 entry.max$ substring$
-  'sort.key$ :=
-}
-ITERATE {presort}
-SORT
-STRINGS { longest.label }
-INTEGERS { number.label longest.label.width }
-FUNCTION {initialize.longest.label}
-{ "" 'longest.label :=
-  #1 'number.label :=
-  #0 'longest.label.width :=
-}
-FUNCTION {longest.label.pass}
-{ number.label int.to.str$ 'label :=
-  number.label #1 + 'number.label :=
-  label width$ longest.label.width >
-    { label 'longest.label :=
-      label width$ 'longest.label.width :=
-    }
-    'skip$
-  if$
-}
-EXECUTE {initialize.longest.label}
-ITERATE {longest.label.pass}
-FUNCTION {begin.bib}
-{ preamble$ empty$
-    'skip$
-    { preamble$ write$ newline$ }
-  if$
-  "\begin{thebibliography}{"  longest.label  * "}" *
-  write$ newline$
-  "\providecommand{\url}[1]{\texttt{#1}}"
-  write$ newline$
-  "\providecommand{\urlprefix}{URL }"
-  write$ newline$
-  "\providecommand{\doi}[1]{https://doi.org/#1}"
-  write$ newline$
-}
-EXECUTE {begin.bib}
-EXECUTE {init.state.consts}
-ITERATE {call.type$}
-FUNCTION {end.bib}
-{ newline$
-  "\end{thebibliography}" write$ newline$
-}
-EXECUTE {end.bib}
-%% End of customized bst file
-%%
-%% End of file `titto.bst'.
diff --git a/Paper/weber_main.pdf b/Paper/weber_main.pdf
deleted file mode 100644
index 60749ff76c3ade1d8c63f0d438e8dd18dd4805ef..0000000000000000000000000000000000000000
Binary files a/Paper/weber_main.pdf and /dev/null differ
diff --git a/Paper/weber_main.synctex.gz b/Paper/weber_main.synctex.gz
deleted file mode 100644
index 59acb7ac8b3097c4ca2a8cff4ff11041a8062440..0000000000000000000000000000000000000000
Binary files a/Paper/weber_main.synctex.gz and /dev/null differ
diff --git a/Paper/weber_main.tex b/Paper/weber_main.tex
deleted file mode 100644
index 50f6503fdbbd4fbaae35e72824dd343e2da600e3..0000000000000000000000000000000000000000
--- a/Paper/weber_main.tex
+++ /dev/null
@@ -1,890 +0,0 @@
-\documentclass[]{llncs}%\documentclass[10pt,letter,conference,compsoc,twocolumn]{IEEEtran}
-%\usepackage[T1]{fontenc}
-%\usepackage[utf8]{inputenc}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%ù
-%\IEEEoverridecommandlockouts  %pour avoir un \thanks
-
-\usepackage[nocompress]{cite}
-\usepackage[british]{babel}
-\usepackage{amssymb,amsmath}
-\usepackage{xspace}
-\usepackage[inline]{enumitem}
-%\usepackage{pifont}
-\usepackage{url}
-\usepackage{relsize}
-\usepackage{caption}
-
-\usepackage{subcaption}
-%\usepackage[caption=false,font=normalsize,labelfont=sf,textfont=sf]{subfig}
-
-
-\usepackage[final]{listings}
-\usepackage{lstcoq}
-\lstset{%
-  escapeinside={(*@}{@*)},%
-  morecomment=*[n][\it\sffamily]{(*}{*)},% reconnaît mots-clés, commentaires...
-  moredelim=[s][\it\ttfamily]{/*}{*/},% éviter keyword style in comment
-  flexiblecolumns=false,%
-  mathescape=true,%
-  basicstyle=\tt\small,%
-  keywordstyle=\bf\ttfamily,%
-  commentstyle=\it\ttfamily,%
-  %frame=tb,% top + bottom
-  morekeywords={String},%
-  % backgroundcolor=\color{grey2},%
-}
-\lstset{language=Coq}
-
-
-%\usepackage{colonequals}
-\usepackage[final]{listings}
-\renewcommand{\ttdefault}{pcr}
-\newcommand*{\origrightarrow}{}
-\let\oldarrow\textrightarrow
-%\renewcommand{\textrightarrow}{\fontfamily{cmr}\selectfont\origrightarrow
-\newcommand{\mytilde}{\raise.17ex\hbox{$\scriptstyle\sim$}}
-
-%
-%\usepackage[textwidth=5em]{todonotes}
-\usepackage{todonotes}%[disable]
-% Everyone has its own color for todo-notes
-\newcommand\todoRP[1]{\todo[color=green!40, size=\tiny]{ #1}\xspace}
-\newcommand\todoXU[1]{\todo[color=blue!40, size=\tiny]{ #1}\xspace}
-\newcommand\todoXUi[1]{\todo[inline, color=blue!40, size=\tiny]{ #1}\xspace}
-\newcommand\todoPC[1]{\todo[color=orange!40, size=\tiny]{ #1}\xspace}
-\newcommand\todoST[1]{\todo[color=violet!40, size=\tiny]{ #1}\xspace}
-\newcommand\todoTB[1]{\todo[color=purple!40, size=\tiny]{ #1}\xspace}
-\newcommand\todoTBi[1]{\todo[inline, color=purple!40, size=\tiny]{ #1}\xspace}
-\newcommand\robin[1]{\textcolor{green}{#1}\xspace} % utiliser todoRP
-\newcommand\todoLR[2][]{\todo[color=gray!40, size=\tiny, #1]{{ #2}}\xspace}
-
-\newcommand{\coq}{\textsc{Coq}\xspace}
-\newcommand{\pactole}{\textsc{Pactole}\xspace}
-%\newcommand{\dmax}{\ensuremath{D_{\!{\textsl{max}}}}\xspace}
-\newcommand{\LCM}{LCM\xspace}
-\newcommand{\setR}{\ensuremath{\mathbb{R}}\xspace}
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%\usepackage[colorlinks=true]{hyperref}
-
-
-\definecolor{coqbg}{rgb}{.9,.9,.9}
-
-\lstnewenvironment{coqcode}[1][]
-  {\lstset{backgroundcolor = \color{coqbg},aboveskip=2pt,belowskip=2pt,basicstyle=\tt\small\relsize{-0.9}, #1}}
-  {}
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%\usepackage[pdftex]{hyperref}      % Utilisation de HyperTeX
-%\hypersetup{%
-%  bookmarks         = true,%       % Signets
-%  bookmarksnumbered = true,%       % Signets num\'erot\'es
-%  bookmarksopen     = true,%       % Affichage des signets.
-%  pdfpagemode       = UseNone,%    % Signets/vignettes ferm\'e \`a l'ouverture
-%  pdfborder         = {0 0 0},%    % Style de bordure : ici, pas de bordure
-%  pdfstartview      = FitH,%       % La page prend toute la largeur
-%  pdfpagelayout     = SinglePage,% % Vue par page
-%  colorlinks        = true,%       % Liens en couleur
-%  urlcolor          = blue,%       % Couleur des liens externes
-%  linkcolor         = blue,%       % Couleur des liens externes
-%  pagecolor         = blue,%       % Couleur des liens externes
-%  anchorcolor       = blue,%       % Couleur des liens externes
-%  citecolor         = blue,%
-%  filecolor         = blue,%
-%  linktocpage       = true,%
-%  breaklinks        = true,%       % retour ligne des liens trop longs
-%  backref           = true,%       % permet d'ajouter des liens dans...
-%  pagebackref       = true,%.      % ..les bibliographies
-%  hyperindex        = true,%       % ajoute des liens dans les index.
-%  %%% TODO documenter !
-%  % TODO: si on change le titre, il faut le changer aussi dans le \title{} plus bas
-%  pdftitle    = {Certified gathering protocol for non synchronized robots with non rigid moves in $R^2$},%
-%  pdfsubject  = {protocols and formal mechanized proof framework for swarms of robots},%
-%  pdfauthor   = {double blind},%
-%  pdfkeywords = {Formal Proof, Proof Assistant, Coq, Mobile Autonomous
-%  Robots, Distributed Algorithms, Automated Deduction, Program
-%  Verification}
-%}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% tikz commands 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\usetikzlibrary{patterns}
-\pgfdeclarelayer{bg}    % declare background layer
-\pgfsetlayers{bg,main}  % set the order of the layers (main is the standard layer)
-
-\tikzstyle{petitrond}=[circle=0pt,inner sep=1.5pt,outer sep=1.5pt,draw=black]
-\newcommand{\robot}[3]{\node (r) at (#1,#2) [draw,color=#3,fill,petitrond] {};}
-\newcommand{\robotn}[4]{\node (#4) at (#1,#2) [draw,color=#3,fill,petitrond] {};}
-
-%\pagenumbering{arabic}
-\begin{document}
-
-% Si on change le titre il faut le changer aussi dans le pdftitle plus haut.
-\title{Certified Weber-based ASYNC Gathering in $\setR^2$}
-%   \thanks{This work was partially supported by Project SAPPORO of the
-%     French National Research Agency (ANR) under the reference ANR-19-CE25-0005.}
-% }
-
-
-\author{}
-\institute{}
-% \author{%
-%   Thibaut Balabonski\inst{1},
-%   Pierre Courtieu\inst{2},
-%   Robin Pelle\inst{1},
-%   Lionel Rieg\inst{3},
-%   S\'{e}bastien Tixeuil\inst{4} and
-%   Xavier Urbain\inst{5}%
-% }%end author  
-% \institute{Université Paris-Saclay, CNRS, LMF
-%   \and C\'edric, Conservatoire des Arts et Métiers, Paris
-%   \and VERIMAG, UMR 5160, Grenoble INP, Univ. Grenoble Alpes
-%   \and Sorbonne University, CNRS, LIP6
-%   \and Université Claude Bernard Lyon 1, LIRIS \textsc{umr5205}
-% }
-
-
-% remerciements
-
-\maketitle
-
-\pagestyle{plain}
-\begin{abstract}
-  \todoPC{À retravailler à la fin}\todoXU{Ah ! Qu'en termes galants\dots}
-  Previous works on gathering oblivious robots in different flavors of
-  asynchronous scheduling has been studied. We provide a new insight
-  on the problem by proving that a simple algorithm based on the Weber
-  point solves the gathering for a large category of initial
-  configurations, even if the robots movements are not rigid (i.e. a
-  robot may be reactivated before reaching its previous target
-  position). Moreover the asynchronous model, the algorithm and its
-  proofs (including geometrical properties of the Weber point) have
-  been completely done in the Coq proof assistant using the dedicated
-  \pactole library.
-\end{abstract}
-
-%extra (negative) spacing
-% pour les bidouilles de gain de place au dernier moment. Mais pas avant.
-%\newcommand\beforesubsubsec{\vspace{-.5cm}}
-%\newcommand\beforesubsec{\vspace{-.45cm}}
-%\newcommand\aftersubsec{\vspace{-.15cm}}
-%\newcommand\aftersec{}
-
-
-\section{Introduction}\label{sec:intro}
-%\todoXUi{Ici on parle d'essaims et de MF.}
-
-%\beforesubsec
-%\subsection{Context}
-%\aftersubsec
-
-
-\noindent\textbf{Context.}
-
-\todoXUi{S\& Y}
-%% les essaims de robots c'est bien
-
-%% Mais c'est compliqué et on a besoin de modèles mathématiques et
-%% d'étudier leurs expressivités comparées.
-
-%Swarm robotics envisions groups of mobile robots self-organizing and cooperating toward the resolution of common objectives, such as patrolling, exploring and mapping disaster areas, constructing ad hoc mobile \mbox{communication} infrastructures to enable communication with rescue teams, etc. As several of those applications are life-critical, the correctness of the deployed protocols becomes of paramount importance. In turn, correctness reasoning about autonom\-ous moving and computing entities that collaborate to achieve a global objective in a setting where unpredictable hazards may occur is complex and error prone. A first step into more formal reasoning is to use a sound \mbox{\emph{mathematical model}.}  
- 
-
-%% Suzuki&Yamashita prpose un modèle générique qui s'est révélé fructueux.
-%% Mais c'est dur de pas se tromper => méthodes formelles.
-
-%Suzuki \& Yamashita~\cite{suzuki99siam} introduced such a mathematical model describing the behaviour of robots in this context. The model is targeted at swarms of very weak robots evolving in harsh environments. At its core, the model simply commands individual robots to repetitively \emph{observe} their environment before \emph{computing} a path of actions to pursue and acting on it, usually by \emph{moving} to a specific location.
-
-%%Three different levels of synchronization have been commonly considered. The fully-synchronous (FSYNC) case~\cite{suzuki99siam} ensures each phase of each cycle is performed simultaneously by all robots. The semi-synchronous (SSYNC) case~\cite{suzuki99siam} allows that only a proper subset of robots execute a cycle at each round. Finally, the asynchronous (ASYNC) case~\cite{flocchini05tcs} allows each robot to execute its cycle at its own pace. %arbitrary delays among the Look, Compute and Move phases, and the movement itself may take an arbitrary amount of time. 
-
-%% The Look-Compute-Move (\LCM) model received a considerable amount of attention from the Distributed Computing community,\footnote{Yamashita received the ``Prize for Innovation in Distributed Computing'' for his seminal work on this model.} yielding a large variety of submodels used to assess the solvability of a certain task assuming certain system hypotheses. As such, the Distributed Computing literature about mobile robots so far can be seen as \emph{computability-oriented}.
-
-%Alas, the various submodels make it extremely tedious to check whether a particular property of a robot protocol holds in a particular setting.  Furthermore, these variants do not behave well regarding proof reusability: checking that a property holding in a given setting also holds in another setting that is not strictly contained in the former often amounts to developing a completely new proof, regardless of the proof arguments similarity. 
-%%This constitutes a major issue when one investigates the correctness of new solutions or implementations of existing protocols to be used in more realistic execution models. 
-%This problem is specially acute because of the great diversity of subtly different models: one may be tempted to simply hand-wave their way around the issue by declaring that the proof in this model is ``obviously'' also valid in this very close model, even more so as even a careful examination may not always find the most subtle errors. %\todoLR{Il faut des citations là, pour justifier le bashing}
-%Last but not least, protocols are typically written in an informal high-level language: assessing whether they conform to a particular model setting is particularly cumbersome, and may lead to hard to find mismatches.
-%As a result, sustained research effort was made in the last decade to use \emph{formal methods} in the context of mobile robotic swarms.
-
-\todoXUi{le pw (point qui minimise la somme des distances à lui, aussi
-  connu sous le nom de point de Torricelli, etc.) est un instrument
-  intéressant dès qu'il s'agit de résoudre le problème du
-  rassemblement, c'est-à-dire dès qu'on veut amener les robots d'un
-  essaim en un même point et les y faire rester. Même s'il n'a pas de
-  forme close (ref), ses propriétés le font considérer dans de
-  nombreuses approches (ref). Nous étudions ce point et ses
-  caractéristiques dans la bibliothèque de preuve formelle Pactole dédiée à la
-  vérification formelle pour essaims de robots. \textbf{Nos contributions} sont
-  - bien sûr tout un tas de théorèmes passionnants mais aussi - un
-  protocole réalisant le gathering dans le cas async. À notre
-  connaissance il s'agit du premier protocole connu dans ce contexte ;
-  il est en outre certifié formellement à l'aide de l'assistant à la
-  preuve Coq et de Pactole.}
-
-\todoXUi{on vend 3 choses : 1) un dév. pour Weber en Pactole, 2) un
-  protocole original et 3) une première preuve formelle *de correction* en ASYNC pour
-  les essaims de robots.}
-\todoXUi{Dans le contexte SSS : on s'adresse à des gens qui
-  connaissent, dans un contexte plus général (IPL ?) on introduirait
-  davantage le modèle.}
-\todoXUi{On ordonne ces contribs suivant le CHOIX qu'on fait pour la
-  contrib. vedette (et éventuellement on modifie le titre)}
-
-This work presents a formal study of the properties of a very simple
-protocol for gathering, yet surprisingly powerful. We stress that the
-formal methods used during the proofs allowed us to understand what
-was the actual minimal hypothesis under which this algorithm solves
-the gathering. Those hypothesis is very simple: if the initial
-configuration is such that the Weber point is uniquely defined, then
-the protocols solves the gathering for the asynchronous scheduler and
-even if movements are not rigid.\todoXU{Shakespeare in Pain}
-
-
-%\beforesubsec
-%\subsection{Related work}
-%\aftersubsec
-
-\noindent\textbf{Related Work.}
-\todoXUi{Quelle est la première contribution ? Si gathering weber alors
-  on \emph{commence} par l'état de l'art là-dessus et on termine par « aucune
-  de ces approches n'est formellement prouvée » ce qui fait toujours
-  une belle transition. \emph{Ensuite} on
-  peut aborder la vérif formelle mais c'est vraiment un second temps.}
-\todoXUi{Si la contribution vedette est la formalisation c'est
-  différent. On commence par aborder la difficulté de travailler
-  formellement en distrib., donc effectivement "quelques outils
-  formels". Ok on a un truc marrant pour faire du gathering : le pw
-  (qq citations) mais voilà, comme parmi les outils précités il n'y a guère que la
-  preuve qui permet de parler explicitement du pw (une propriété
-  extérieure au système) on se concentre là dessus.}
-
-\todoPC{Parler des autres outils formels}
-~
-\todoPC{parler des papiers sur le gathering async, rigid et/ou flexible. Comparer avec nous.}
-\todoXU{bof}
-~
-%Formal methods encompass a long-lasting path of research that is meant to overcome errors of human origin.
-%Perhaps the most well known instance in the Distributed Computing community is the~\emph{Temporal Logic of Actions} and its companion tools TLA/TLA+\cite{lamport1994ACM,cousineau12fm}. Though very expressive, TLA is designed for the shared
-%memory and message passing contexts, thus not well suited to studying mobile robotic swarms.
-%\emph{Model-checking} and its powerful automation proved useful to find bugs in existing literature~\cite{berard16dc,doan16sofl,doan17opodis}, and to assess formally published algorithms~\cite{devismes12sss,berard16dc,defago20srds}. Automatic program synthesis (for the problem of perpetual exclusive exploration in a ring-shaped discrete space) is due to Bonnet \emph{et al.}\!~\cite{bonnet14wssr}, and can be used to obtain automatically algorithms that are ``correct-by-design''. The approach was refined by Millet \emph{et al.}\!~\cite{MPST14c} for the problem of gathering in a discrete ring network. 
-%However, these are limited to instances with few robots. Generalizing them to an arbitrary number of robots with similar models is doubtful as Sangnier \emph{et al.}\!~\cite{sangnier20fmsd} proved that safety and reachability problems are undecidable in the parameterized case.
-%Another limitation of the above approaches is that they \emph{only} consider cases where mobile robots \emph{evolve in a discrete space} (\emph{i.e.}, graph). This limitation is due to the model used, that closely matches the original execution model by Suzuki and Yamashita~\cite{suzuki99siam}. As a computer can only model a finite set of locations, a continuous 2D Euclidean space cannot be expressed in this model.
-%Défago \emph{et al.}~\cite{defago20srds} used a more abstract model to model-check rendez-vous algorithms in a continuous 2D Euclidean space, however, their model is highly specific to rendez-vous and thus is not as versatile as one hopes, suggesting a \mbox{more general and systematic technique.}
- 
-
-The approach\todoPC{modifier à la marge cette partie}\todoXU{oui on
-  résume, ce sont des morceaux à prendre} on which we focus in this work is \emph{formal proof}, that is proof development mechanically certified by a proof assistant. 
-Mechanical proof assistants are proof management systems where a user can
-express data, programs, theorems and proofs. In sharp contrast with automated
-provers (like model-checkers), they are mostly interactive, and thus require some kind of expertise from their users. Sceptical proof assistants provide an additional guarantee by checking mechanically the soundness of a proof after it has been interactively developed.
-Formal proofs allow for more generality % \todoLR{Le reviewer 3 n'aimait pas genericity}
-as this approach is not limited to \emph{particular instances} of algorithms. 
-During the last twenty years, the use of tool-assisted verification has extended
-to the validation of distributed processes, in contexts such as process algebras~\cite{fokkink07,bezem97fac}, symmetric interconnection networks~\cite{gaspar14ijpp}, message passing settings~\cite{kuefner12ifiptcs}, self-stabilization~\cite{deng09tase,altisen16forte}, etc.
-The main approach for mechanized proof dedicated to swarms of mobile
-entities is the \pactole\footnote{\tt \url{https://pactole.liris.cnrs.fr}} framework, based on the \coq proof assistant.
-%Initiated in 2010, The \pactole framework enabled the use of
-%high-order logic to certify impossibility results, as well as
-%soundness of protocol, for swarms of autonomous mobile robots.
-%To certify results and to guarantee the soundness of theorems, the proof
-%assistant it uses is \coq.
-Briefly, \coq is a Curry-Howard-based interactive proof assistant that
-enjoys a trustworthy kernel. %Its base language is a very expressive
-%$\lambda$-calculus, the \emph{Calculus of Inductive Constructions}
-%\cite{coquand90colog}, where datatypes, objects, algorithms,
-%theorems and proofs can be expressed in a unified way, as terms.
-% The syntax is close to that of an ML-like programming language, and
-Then, a proof development consists in building, interactively and using
-tactics, a $\lambda$-term, the type of which corresponds to the theorem
-to be proven. % (Curry-Howard style).
-% The small kernel of \coq simply
-% type-checks $\lambda$-terms to ensure soundness.
-Most importantly:
-\emph{a theorem or a lemma can only be saved/defined in the system if
-  it comes with its type-checked proof}.
-Designed for mobile entities, and making the most of \coq's assets,
-\pactole allows for working on a given protocol to establish and
-certify its correctness \cite{courtieu16disc,balabonski19tocs}, as
-well as for quantifying over all protocol so as to prove
-\emph{impossibility} results
-\cite{auger13sss,courtieu15ipl,balabonski18icdcn}, with an unspecified
-number of robots, possibly including a proportion of Byzantine faults, in
-continuous or discrete spaces.
-FSYNC/SSYNC and ASYNC modes are all supported, and the framework is
-expressive enough to state and certify formally results as theoretical
-as comparisons between demons or models \cite{balabonski19netys}.
-
-%\beforesubsec
-%\subsection{Our Contribution}
-%\label{sec:contribution}
-%\aftersubsec
-
-\noindent\textbf{Contributions.}
-
-\todoXUi{Cfr ce qu'on a décidé plus haut.}
-We provide and certify a protocol to solve the gathering problem (with
-no light) for a large set of initial configuration in the most relaxed
-synchronicity model the ASYNC non-rigid\todoPC{avons nous déjà défini
-  ça plus haut?} one, with multiplicity detection. Gathering is well
-known to be impossible to solve if the initial configuration is
-bivalent \cite{suzuki99siam,courtieu15ipl} ,i.e. exactly two occupied
-positions with exactly the same number of robots on each, in this
-setting.
-
-
-The developments  described in this work, for \coq v8.13, based on the current version of \pactole, are available
-at {...\todoPC{faire une archive, en aveugle si nécessaire (procédure
-    assez pénible...)}}.\todoXU{J'en profite pour ajouer que si c'est
-  de la soumission anonyme on ne met les références du projet
-  qu'après, hein ?}
-
-\subsection{A brief description of the solution}
-
-\todoPC{pour que le lecteur pressé puisse voir l'algo, et l'argument
-  principal, informellement. Ensuite on décrit pactole, on décrit le
-  modèle async (important d'être pédagogique à ce moment), puis les
-  lemmes clés et le théorème final.}.
-
-%\subsection{Criticity of the solution}\label{sec:important}
-
-\section{A Brief Overview of %the
-  \pactole} % Framework}
-\label{sec:pactole}
-%\aftersec
-
-\todoPC{Il faut peut-être réorienter un peu cette section vers l'async
-  et le flexible. Pour que la section d'après soit plus facile à lire.
-}
-\todoXUi{Encore ? très très ``brief'' alors. On a écrit whatmille
-  papiers dessus qu'on peut citer.}
-
-
-
-%\todoXUi{euh les notions de base de pactole : configuration, round, observation ?}
-One of the aims of \pactole is to stay as simple and as close as possible to the definitions of the robotic swarm community: %
-\begin{coqcode}[gobble=2]
-  Definition configuration := ident -> state.
-  Definition execution := Stream.t configuration.
-  Definition demon := Stream.t demonic_action.
-  Definition robogram := observation -> action.
-\end{coqcode}
-A state of the overall system, a \emph{configuration}, is defined
-as the collection of all robots'  states, conveniently combined into a map from robot names to robot states.
-A robot \emph{state} can be anything (to accurately describe reality) but must at least contains its \emph{location}, accessible through a function \lstinline{get_location:} \lstinline{state -> location}, where type \lstinline{location} denotes the space where robots are.
-
-An \emph{execution} is an infinite sequence of configurations.
-Executions are usually built by executing a protocol (called a
-\emph{robogram}) against an environment, represented as a
-\emph{demon}, \emph{i.e.} an infinite sequence of decisions called \emph{demonic actions}.
-The robogram represents the Compute part of the \LCM cycle,
-taking a robot's observation as an input and returning the action that
-the robot should perform.
-
-This \emph{observation} denotes a degraded\todoXU{coarse-grained plutôt} version of the configuration centred on the observing robot, depending on its sensors.
-It is a parameter of the model and its computation from a (local) configuration is performed by an \lstinline{obs_from_config} function, which hides the information unavailable to robots and takes as input the configuration and the state of the observing robot.
-This function is specified by a logical formula \lstinline{obs_is_ok} relating any configuration to its possible observation from any robot state.
-\begin{coqcode}[gobble=2]
-  Parameters (observation: Type)
-   (obs_from_config: configuration -> state -> observation)
-   (obs_is_ok: observation ->  configuration -> state -> Prop)
-   (obs_from_config_spec:
-   (*@\hfill@*)forall cfg st, obs_is_ok (obs_from_config cfg st) cfg st).
-\end{coqcode}
-
-To represent the fact that robots observe from a local point of view, they have their own \emph{frame of reference} that need not be consistent in time or with other robots (other orientation, other scale, other origin, etc.).
-This frame of reference allows for a \emph{local configuration}
-(by opposition to the point of view of the demon denoted as \emph{global}) from which the observation is computed, it depends on the underlying space and it is picked by the demon.
-
-In such an execution, the robogram corresponds to one \LCM
-cycle\todoXU{Comprends pas cette phrase}
-% \todoLR{pas vrai pour ASYNC mais bon}
-and the demonic action to the reaction of the environment.
-Their interaction is described by a function \lstinline{round} so that
-the resulting execution is simply repeatedly calling this function
-with the robogram, the demon and the starting configuration. % :
-%\todoLR{Le code est trop compliqué et pas très utile, non ?}\todoXU{commenté}
-% \begin{coqcode}[gobble=2]
-%   Definition execute (r : robogram)
-%     : demon -> configuration -> execution :=
-%     cofix execute d config :=
-%     Stream.cons config
-%       (execute (Stream.tl d) (round r (Stream.hd d) config)).
-% \end{coqcode}
-\lstinline{round} is the heart of the model. It implements the \LCM cycle by computing the configuration obtained after one round.
-Note that it is the same for all variants, FSYNC/SSYNC/ASYNC synchronization, all spaces, all sensors, etc.
-%For simplicity, we only consider the case of SSYNC (of which FSYNC is a particular case), the case of ASYNC already being presented elsewhere~\cite{balabonski2019netys}.
-It proceeds by the following consecutive steps for each robot name \lstinline{id}:
-\begin{enumerate}
-  \item If \lstinline{id} is not activated, its state may undergo some change by the \lstinline{inactive} function to represent an ongoing action or the effect of the environment.
-  \item If \lstinline{id} is Byzantine it is relocated by demonic action \lstinline{da}.
-  \item Use local frame of reference provided by \lstinline{da} to compute local configuration.
-  \item Transform this local configuration into an observation.
-  \item Apply the robogram on this observation.
-  \item If moves are flexible compute new position of \lstinline{id} using \lstinline{da} decision.
-  \item Convert the new position back to the global frame.
-\end{enumerate}
-
-\section{The ASYNC non-rigid setting }
-\label{sec:setting}
-
-\todoPC{$R^2$, ASYNC, flexible, multiplicity, comment on paramètre
-  tout ça en coq. On peut essayer de décrire ça sans montrer la
-  fonction \lstinline!round! pour une fois, mais c'est pas gagné.}
-\todoXU{tu viens de décrire round (sans préciser ASYNC), on va pas mettre le code}
-\section{Key steps of the proof}
-\label{sec:keysteps}
-
-\todoPC{propriétés du point Weber, on voit combien de place on a pour décrire les preuves, ou pas}
-
-\todoPC{le lemme de Zohir} \todoXU{c'est quoi ça ?}
-
-\todoPC{la mesure async, inutile de raconter les mesures pour les cas
-  plus simple à mon avis.}
-\todoXU{yep}
-
-\section{Conclusion}
-
-\todoPC{Cet algo peut peut-être se combiner avec un autre pour
-  résoudre le gathering dans tous les cas non bivalents. Voir ave
-  Quentin si sa solution marche.}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% WIP Mathis
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\section{Weber Points}
-
-\noindent\textbf{Definition and description in \coq.}
-
-Given a finite collection $X$ of points in $\mathbb{R}^2$, we define the \emph{sum of distances to $X$} as follows.
-$$ D_X(p) = \sum_{x \in X} \lVert p - x \rVert$$
-A point $p$ is then a Weber point of $X$ if and only if it minimizes $D_X$. 
-Examples of Weber points are given in Figure \ref{fig:weberExamples}.
-In \coq, the $D_X$ function and Weber point definition are written as :
-
-\begin{coqcode}[gobble=2]
-  Definition dist_sum (points : list R2) (x : R2) := 
-    list_sum (List.map (dist x) points).
-  Definition argmin {A : Type} (f : A -> R) : A -> Prop := 
-    fun a => forall b, (f a <= f b)%R.   
-  Definition Weber (points : list R2) : R2 -> Prop := 
-    argmin (dist_sum points).
-\end{coqcode}
-
-
-\begin{figure}[htp]
-	\centering
-	\begin{subfigure}{.3\textwidth}
-		\centering 	
-		\includegraphics[width=\linewidth]{img/weber_examples_A.drawio.png}
-		\caption{The points in $X$ are $A$, $B$, $C$ and $D$. 
-      The point $D$ is the unique Weber point.}
-	\end{subfigure}% 
-  \hfill%
-	\begin{subfigure}{.3\textwidth}
-		\centering 	
-		\includegraphics[width=\linewidth]{img/weber_examples_B.drawio.png}
-		\caption{There are infinitely many Weber points forming a segment, with endpoints $A$ and $B$ included.}
-	\end{subfigure}
-	\hfill% 
-	\begin{subfigure}{.3\textwidth}
-		\centering 	
-		\includegraphics[width=\linewidth]{img/weber_examples_C.drawio.png}
-		\caption{The point $A$ is in $X$ and is the unique Weber point.}
-	\end{subfigure}
-	  
-	\caption{A set $X$ of points is represented in blue, each point with multiplicity $1$. 
-    The Weber points of $X$ are represented in red.
-    In general the set of Weber points is always a segment (possibly reduced to a single point).}
-  \label{fig:weberExamples}
-\end{figure}
-
-
-\noindent\textbf{Weber point of non-aligned points.}
-
-As shown in Figure \ref{fig:weberExamples}, the Weber point is not always unique. 
-This has some consequences for algorithms that wish to rely on the Weber point, 
-and we will be forced to use a different strategy depending on whether the Weber point is unique or not.
-The good news however is that for most configurations the Weber point is unique : 
-indeed it is the case as soon as the points in $X$ are not aligned (i.e. $X$ contains three non-colinear points).
-
-\noindent\textbf{Weber point of aligned points.}
-
-When the points in $X$ are aligned, there might be several distinct Weber points. 
-However in this case the minimizers of $D_X$ are simple to characterize. 
-Let $p$ be a point, and $\textrm{left}(p)$ (resp. $\textrm{on}(p)$ and $\textrm{right}(p)$) the subset of points of $X$ 
-that are strictly to the \emph{left} (resp. \emph{on} and strictly to the \emph{right}) of $p$. 
-Then $p$ is a Weber points if and only if : 
-$$\lvert \textrm{card}(\textrm{left}(p)) - \textrm{card}(\textrm{right}(p)) \rvert \leq \textrm{card}(\textrm{on}(p))$$
-
-This characterization allows us to state several useful properties, in the aligned case :
-\begin{enumerate}
-  \item The set of Weber points is a segment with endpoints in $X$.
-  \item Whenever $\textrm{card}(X)$ is odd, every Weber point is included in $X$ and thus there is a unique Weber point.
-  \item If a point has multiplicity at least $\frac{\textrm{card}(X) + 1}{2}$, then it is a Weber point.
-\end{enumerate}
-
-\noindent\textbf{The contraction lemma.}
-
-The property of the Weber point that makes it so convenient for solving the 
-Gathering problem is the \emph{contraction lemma}. 
-Informally, if we move all robots in a straight line towards their unique Weber point, then it remains unique and at the same place.
-We give more details concerning this lemma.\\
-
-We say that $X = (x_i)_{i \in I}$ \emph{contracts} to $Y = (y_i)_{i \in I}$ around $p$ if :
-$$\forall i \in I, y_i \textrm{ is in the segment } [ x_i, p ]$$
-The \emph{contraction lemma} (see Figure \ref{fig:contractionLemma}) states :
-If there exists a Weber point $p_0$ of $X$ such that $X$ contracts to $Y$ around $p_0$, then : 
-$$\forall p, p \textrm{ is a Weber point of } Y \iff (p \textrm{ is a Weber point of } X \textrm{ and } X \textrm{ contracts to } Y \textrm{ around  } p) $$
-
-Note that in the case where $p_0$ is the unique Weber point of $X$, and in particular when the points in $X$ are not aligned,
-this means that $p_0$ is also the unique Weber point of $Y$.
-
-\begin{figure}[htp]
-	\centering 
-	\includegraphics[width=0.7\linewidth]{img/contraction_lemma.drawio.png}  
-	\caption{A set $X$ of points (in blue) contracts to a set $Y$ (in red) around the unique Weber point $W$ of $X$. 
-    By the contraction lemma, $W$ is also the unique Weber point of $Y$.}
-  \label{fig:contractionLemma}
-\end{figure}
-
-\section{The ASYNC flexible setting}
-
-The core of \pactole (for instance the round function) is written with a high level of generality with respect to the setting (FSYNC, SSYNC, rigid, flexible, etc.).
-The mechanism that allows this is the use of \coq typeclasses : to define a specific setting, 
-it suffices to instantiate a few typeclasses. 
-This mainly requires specifying a type for the state of robots, 
-and writing the definition of the update function and inactive function
-that determine how to update the state of active and inactive robots every round.
-\\
-We chose to represent robots using a triplet composed of : 
-\begin{enumerate}
-  \item The \emph{start} position of the robot : the last position it was activated at.
-  \item The \emph{destination} position of the robot : the last position it computed using the robogram.
-  \item The robot's \emph{ratio} : a real number between $0$ and $1$ that indicates where the robot is on the segment 
-    between its start and destination points.
-\end{enumerate}
-Both positions are to be interpreted in the global frame of reference, as opposed to the robot's local frame.
-The current position of the robot is computed as $\textrm{start} + \textrm{ratio} * (\textrm{destination} - \textrm{start})$.
-\\
-Note that when a robot performs a Look, we only give it the set of current positions of the other robots, \emph{not} the start and destination of every robot.
-\\
-\noindent\textbf{Inactive function.}
-
-The inactive function is then very straightforward : it simply increases the ratio of the robot, 
-using another ratio chosen by the demon. The demon can choose a ratio of $0$ : in this case the robot does not move.
-\begin{coqcode}[gobble=2]
-  start[i+1] <- start[i]
-  destination[i+1] <- destination[i]
-  ratio[i+1] <- min(1, ratio[i] + demon_ratio[i])
-\end{coqcode} 
-
-\noindent\textbf{Update function.}
-
-The update function is where the robot performs its Look and Compute. 
-The start position of the robot is reset to its current position, 
-and its destination is computed using the robogram. 
-\begin{coqcode}[gobble=2]
-  start[i+1] <- current_position[i]
-  destination[i+1] <- robogram_output[i]
-  ratio[i+1] <- 0
-\end{coqcode}
-
-\noindent\textbf{Rigid and flexible settings.}
-
-A subtlety with this model of ASYNC is that the demon could in theory choose to never move inactive robots.
-In this case the robots would never move and always be activated in the same configuration.
-To prevent this we have to specify an additional property, depending on whether we choose a rigid or flexible setting.
-In a rigid setting, robots can only be activated once they have reached their destination : 
-
-\begin{coqcode}[gobble=2]
-  Definition rigid_da_prop (da:demonic_action) := 
-    forall (id:identifier) (config : configuration), 
-      activate da id = true -> 
-      get_location (config id) == get_destination (config id).
-\end{coqcode}
-
-In a flexible setting, robots can be activated once they have either 
-reached their destination or moved at least a distance $\delta > 0$ since their last activation.
-
-\begin{coqcode}[gobble=2]
-  Definition flex_da_prop (da:demonic_action) := 
-    forall (id:identifier) (config : configuration), 
-      activate da id = true -> 
-      get_location (config id) == get_destination (config id) \/ 
-      delta <= dist (get_start (config id)) (get_location (config id)).
-\end{coqcode}
-
-\noindent\textbf{Initial configuration.}
-
-We say that a robot is \emph{looping} if its start and destination are equal.
-From now on we will assume a weak self-stable initial configuration : initially every robot is looping. 
-
-
-\section{Description of the solution}
-
-We assume given a function that calculates a single Weber point of a finite collection of points in $\mathbb{R}^2$.
-\begin{coqcode}[gobble=2]
-  Axiom weber_calc : list R2 -> R2.
-  Axiom weber_calc_correct : 
-    forall (points:list R2), Weber points (weber_calc points).
-\end{coqcode}
-
-It is easy to extend this function to compute the endpoints of the Weber segment.
-\begin{coqcode}[gobble=2]
-  Definition weber_calc_seg : list R2 -> R2 * R2 := ...
-  Lemma weber_calc_seg_correct : 
-    forall (points:list R2) (w:R2),
-    let (w1, w2) := weber_calc_seg points in 
-    Weber points w <-> segment w1 w2 w.
-\end{coqcode}
-Where \textbf{segment a b x} means that \textbf{x} lies in the segment \textbf{[a, b]}, endpoints included.
-
-\subsection{A First Attempt}
-
-Leveraging the contraction lemma, a reasonable strategy is to move every robot in a straight line towards the weber point.
-This simple robogram works in most cases : in fact, it works provided that the Weber point is unique in the initial configuration.
-The \coq robogram is very concise :
-
-\begin{coqcode}[gobble=2]
-  Definition gather_pgm (obs:observation) : location := 
-    if aligned_dec obs 
-    then 0%VS 
-    else weber_calc obs.
-\end{coqcode}
-
-Remember that both the observation and the robogram output are to be interpreted in the robot's local frame of reference.
-This means that \textbf{0\%VS} refers to the robot's current position.
-\\
-We assume that the initial configuration has a unique Weber point $w$ : this means in particular that it is not bivalent.
-We then claim that $w$ will remain the unique Weber point throughout the whole execution. 
-Additionally the destination of every non-looping robot will always be equal to $w$, and the robots will eventually gather at $w$.
-
-\subsection{The full robogram}
-
-We now extend the simple robogram to also handle the cases where the Weber point is not unique.
-The basic idea is to divide the execution into \emph{phases}, depending on whether the Weber point is unique or not.
-Note that the ASYNC setting complicates reasoning about about phases : when we change phase, 
-some robots may still have some pending moves from the previous phase, and thus act differently from what we would intuitively expect.
-\\
-The solution is divided into four distinct phases. 
-Let $w_1$ and $w_2$ be the endpoints of the Weber segment. 
-When the robots are aligned, let $r_1$ and $r_2$ be the endpoints of the segment they form, and $m$ be the middle of the segment $[ r_1, r_2 ]$.
-\begin{enumerate}
-  \item Phase 1 : $w_1 = w_2$. 
-    In this case all robots move towards $w_1$.
-  \item Phase 2 : $w_1 \neq w_2$, and there is a robot $t$ of multiplicity $\frac{n}{2}$. 
-    In this case all robots move towards $t$.
-  \item Phase 3 : $w_1 \neq w_2$, all robots have multiplicity less than $\frac{n}{2}$, and $m$ is in the segment $[ w_1, w_2 ]$. 
-    In this case robots on $w_1$ or $w_2$ move towards $m$.
-  \item Phase 4 : $w_1 \neq w_2$, all robots have multiplicity less than $\frac{n}{2}$, and $m$ is \emph{not} in the segment $[ w_1, w_2 ]$. 
-    Assumes without loss of generality that $m < w_1 < w_2$. 
-    In this case all robots on $w_2$ move towards $w_1$.  
-\end{enumerate}
-Note that in phases $2$, $3$ and $4$, the number $n$ of robots is even, the robots are aligned and every point has multiplicity at most $\frac{n}{2}$.
-
-The \coq robogram for the complete solution is :
-
-\begin{coqcode}[gobble=2]
-  (* [n] is the number of robots *)
-  Definition gather_pgm (obs:observation) : location := 
-    let (w1, w2) := weber_calc_seg obs in
-    let (r1, r2) := ... in 
-    let m := middle r1 r2 in
-    (* phase 1 : move to the unique weber point *)   
-    if w1 ==b w2 then w1 else 
-    match robot_with_mult (Nat.div2 (n+1)) obs with
-    | Some t =>
-      (* phase 2 : move to [t] unless
-       * there is a robot between [0%VS] and [t]. *)
-      if existsb (strict_segment_decb 0%VS t) obs 
-      then 0%VS else t
-    | None =>
-      if segment_decb w1 w2 m then 
-        (* phase 3 : robots on [w1] or [w2] move to the middle *)
-        if (w1 ==b 0%VS) || (w2 ==b 0%VS) then m else 0%VS
-      else if segment_decb m w1 w2 then 
-        (* phase 4 : robots on [w1] move to [w2] *)
-        if w1 ==b 0%VS then w2 else 0%VS 
-      else if segment_decb m w2 w1 then
-        (* also phase 4 : robots on [w2] move to [w1] *)
-        if w2 ==b 0%VS then w1 else 0%VS
-      else 
-        (* this should not happen *) 
-        0%VS                    
-    end.
-\end{coqcode}
-
-Where \textbf{segment\_decb a b x} and \textbf{strict\_segment\_decb a b x} test whether \textbf{x} 
-is respectively in the closed and open interval with endpoints \textbf{a} and \textbf{b}.
-
-\section{Key steps of the proof}
-
-\noindent\textbf{Different phases of the algorithm.}
-We characterize each phase by an invariant.
-As an example we show the \coq code for the simple invariant of phase $1$ : 
-
-\begin{coqcode}[gobble=2]
-  Definition inv1 config w : Prop := 
-    (* All robots are moving towards [w]. *)
-    config_stg config w /\ 
-    (* [w] is the unique weber point. *)
-    OnlyWeber (pos_list config) w.
-\end{coqcode}
-Where \textbf{config\_stg config w} means that all robots are either staying where they are or going towards \textbf{w}.
-\\ 
-Using these invariants, we prove a transition diagram between the different phases : see Figure \ref{fig:phaseTransitionDiagram}.
-We also show that if the initial configuration is weak self-stable and not bivalent, then it verifies one of the four phase invariants.
-
-\begin{figure}[htp]
-  \centering   
-  \includegraphics[width=0.6\linewidth]{img/phase_transition_diagram.drawio.png}
-  \caption{Phase transition diagram.}
-  \label{fig:phaseTransitionDiagram}
-\end{figure}
-
-This translates into a series of \coq lemmas of the following form : 
-
-\begin{coqcode}[gobble=2]
-  (* This describes the transitions we can make from phase 2. *)
-  Lemma phase2_transitions config (da:demonic_action) (L:line) :
-    similarity_da_prop da -> 
-    inv2 config L -> 
-    (exists w, inv1 (round gatherW da config) w) \/ 
-    inv2 (round gatherW da config) L.
-\end{coqcode}
-
-What is remarkable (and allows the algorithm to work) is that 
-the destination of the robots always stays at the same place and is the same for every robot, 
-even when we change phase.
-
-\noindent\textbf{Decreasing measure.}
-
-We define a measure of the configuration in each phase. 
-This measure is constructed not only from the positions of the robots, but also from their destination and start points.
-Let $D$ be the common destination point of all the (moving) robots.
-In all phases, the measure is equal to the sum of :
-\begin{enumerate}
-  \item The number of robots that are \emph{not} looping on $D$.
-  \item The total distance between $D$ and the start of every robot.
-\end{enumerate}
-The measure is real-valued, nonnegative, and always decreases or stays equal between rounds. 
-Additionally, within a single phase, the measure regularly decreases by a constant amount.
-More precisely, it decreases at every round that has a \emph{progress} robot.
-We say that a robot is a \emph{progress} robot if it is activated and it is not looping.
-Indeed, whenever there is a progress robot in a round, there are two possible cases : 
-\begin{enumerate}
-  \item The robot is not on $D$  : see Figure \ref{fig:measureDecreaseNotOn}. 
-  \item The robot is on $D$ : see Figure \ref{fig:measureDecreaseOn}.
-\end{enumerate}
-The measure thus decreases by at least $\textrm{min}(\delta, 1)$.
-
-\begin{figure}[htp]
-  \centering 
-  \begin{subfigure}{.45\textwidth}
-		\centering 	
-		\includegraphics[width=\linewidth]{img/measure_decrease_not_on_A.drawio.png}
-    \caption{Round $i$.}
-	\end{subfigure}% 
-  \hfill%
-	\begin{subfigure}{.45\textwidth}
-		\centering 	
-		\includegraphics[width=\linewidth]{img/measure_decrease_not_on_B.drawio.png}
-    \caption{Round $i+1$.}
-	\end{subfigure}
-	
-  \caption{In round $i$, the robot $r$ is a progress robot and is \emph{not} on $D$. 
-    The start and destination of $r$ are represented by the base and the tip of the arrow.
-    Since we are in a flexible setting, in round $i+1$ the start of $r$ is now closer by at least $\delta$ to $d$, 
-    and the second part of the measure decreases by at least $\delta$.}
-  \label{fig:measureDecreaseNotOn}
-\end{figure}
-
-\begin{figure}[htp]
-  \centering 
-  \begin{subfigure}{.45\textwidth}
-		\centering 	
-		\includegraphics[width=\linewidth]{img/measure_decrease_on_A.drawio.png}
-    \caption{Round $i$.}
-	\end{subfigure}% 
-  \hfill%
-	\begin{subfigure}{.45\textwidth}
-		\centering 	 
-		\includegraphics[width=.4\linewidth]{img/measure_decrease_on_B.drawio.png}
-    \caption{Round $i+1$.}
-	\end{subfigure}
-	
-  \caption{In round $i$, the robot $r$ is a progress robot and is on $D$. 
-    The start and destination of $r$ are represented by the base and the tip of the arrow.
-    In round $i+1$, $r$ is now looping on $D$ so the first part of the measure decreases by $1$.}
-  \label{fig:measureDecreaseOn}
-\end{figure}
-
-The \coq code for the relevant lemmas is as follows.
-
-\begin{coqcode}[gobble=2]  
-  (* In phase 1, the common destination point of the robots 
-   * is [w] the unique Weber point *)
-  Lemma phase1_decrease config (da:demonic_action) w : 
-    similarity_da_prop da ->
-    flex_da_prop da ->
-    inv1 config w -> 
-    inv1 (round gatherW da config) w ->
-    (exists id, activate da id = true /\
-                get_dest (config id) =/= get_start (config id)) ->
-    measure w (round gatherW da config) <= measure w config - Rmin 1%R delta.
-\end{coqcode}
-
-The last step is to prove that there will always eventually be a progress robot : 
-this is a consequence of the \emph{fairness} assumption, that states that a robot is always eventually activated.
-
-\noindent\textbf{Correctness theorem.}
-
-In an ASYNC and flexible setting, assuming that initially the configuration is not bivalent and that every robot is looping,
-the robots will eventually gather at a point. Written in \coq, the correctess theorem is as follows. 
-We can clearly see all the hypotheses needed to prove this result.
-
-\begin{coqcode}[gobble=2]
-  Theorem gather_correct config demon : 
-    (* The demon is fair. *)
-    Fair demon -> 
-    (* The frame changes (chosen by the demon) 
-     * are similarities centered on the observing robot. *)
-    (Stream.forever (Stream.instant similarity_da_prop)) demon -> 
-    (* We are in a flexible setting *)
-    (Stream.forever (Stream.instant flex_da_prop)) demon -> 
-    (* Initially, the configuration is valid (i.e. not bivalent). *)
-    ~invalid config ->
-    (* Initially, all robots are looping. *)
-    config_stay config -> 
-    (* The robots will eventually gather 
-     * and stay gathered at the same point forever. *)
-    WillGather (execute robogram demon config).
-\end{coqcode}
-
-\bibliographystyle{splncs04}
-%\bibliographystyle{abbrv}
-\bibliography{../../biblio}
-
-%\newpage
-\appendix
-%\beforesubsec
-%\section{Bla}
-
-\end{document}
-
-
-%%% Local Variables: ***
-%%% mode: latex ***
-%%% TeX-PDF-mode: t ***
-%%% ispell-dictionary: "british-ize-w_accents" ***
-%%% ispell-local-dictionary: "british-ize-w_accents" ***
-%%% mode: flyspell ***
-%%% TeX-master: t ***
-%%% End: ***
-
-% LocalWords:  provers  Défago Yamashita
-