1285   code with a few apply-scripts interspersed. The formal model of PIP

  1285   code with a few apply-scripts interspersed. The formal model of PIP

  1286   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary

  1286   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary

  1287   definitions and proofs span over 770 lines of code. The properties relevant

  1287   definitions and proofs span over 770 lines of code. The properties relevant

  1288   for an implementation require 2000 lines. The code of our formalisation 

  1288   for an implementation require 2000 lines. The code of our formalisation 

  1289   can be downloaded from

  1289   can be downloaded from

  1291 

  1296 

  1292   \bibliographystyle{plain}

  1297   \bibliographystyle{plain}

  1293   \bibliography{root}

  1298   \bibliography{root}

  1294 *}

  1299 *}

  1295 

  1300