Loading theory "Diophantine_Eqns_Lin_Hom.List_Vector"
Loading theory "Diophantine_Eqns_Lin_Hom.Sorted_Wrt"
Proofs for inductive predicate(s) "sorted_wrt"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Diophantine_Eqns_Lin_Hom.Sorted_Wrt"
### 0.232s elapsed time, 0.532s cpu time, 0.000s GC time
Loading theory "Diophantine_Eqns_Lin_Hom.Minimize_Wrt"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "Diophantine_Eqns_Lin_Hom.Minimize_Wrt"
### 0.222s elapsed time, 0.448s cpu time, 0.000s GC time
Found termination order:
  "(\<lambda>p. length (snd (snd (snd p)))) <*mlex*> {}"
### theory "Diophantine_Eqns_Lin_Hom.List_Vector"
### 0.886s elapsed time, 1.812s cpu time, 0.000s GC time
Loading theory "Diophantine_Eqns_Lin_Hom.Linear_Diophantine_Equations"
locale
 
hlde_ops


fixes a :: "nat list" 
  and b :: "nat list" 
locale
 
hlde


fixes a :: "nat list" 
  and b :: "nat list" 


assumes "hlde a b"
### theory "Diophantine_Eqns_Lin_Hom.Linear_Diophantine_Equations"
### 0.878s elapsed time, 1.740s cpu time, 0.256s GC time
Loading theory "Diophantine_Eqns_Lin_Hom.Algorithm"
Found termination order: "{}"
### The following clauses are redundant (covered by preceding clauses):
### x \<Rightarrow> []
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
locale
 
bounded_lexs


fixes C :: "nat list \<Rightarrow> nat \<Rightarrow> bool" 
  and B :: "nat" 


assumes "bounded_lexs C B"
Found termination order: "size_list size <*mlex*> {}"
locale
 
bounded_lexs2


fixes C\<^sub>2 :: "nat list \<Rightarrow> nat \<Rightarrow> bool" 
  and B\<^sub>2 :: "nat" 
  and
  C\<^sub>1 ::
    "nat list
     \<Rightarrow> nat list
                   \<Rightarrow> nat list
                                 \<Rightarrow> nat \<Rightarrow> bool"
    
  and B\<^sub>1 :: "nat list \<Rightarrow> nat" 


assumes "bounded_lexs2 C\<^sub>2 B\<^sub>2 C\<^sub>1 B\<^sub>1"
Found termination order: "{}"
Found termination order: "{}"
locale
 
bounded_incs


fixes cond :: "nat list \<Rightarrow> nat \<Rightarrow> bool" 
  and B :: "nat" 


assumes "bounded_incs cond B"
Found termination order:
  "(\<lambda>p. size_list size (snd (snd p))) <*mlex*> {}"
### theory "Diophantine_Eqns_Lin_Hom.Algorithm"
### 2.536s elapsed time, 5.056s cpu time, 0.264s GC time
"[(([0, 0], 0), [0], 0), (([1, 0], 1), [0], 0), (([2, 0], 2), [0], 0),
  (([0, 1], 1), [0], 0), (([1, 1], 2), [0], 0), (([2, 1], 3), [0], 0),
  (([0, 2], 2), [0], 0), (([1, 2], 3), [0], 0), (([2, 2], 4), [0], 0),
  (([0, 0], 0), [1], 2), (([1, 0], 1), [1], 2), (([2, 0], 2), [1], 2),
  (([0, 1], 1), [1], 2), (([1, 1], 2), [1], 2), (([2, 1], 3), [1], 2),
  (([0, 2], 2), [1], 2), (([1, 2], 3), [1], 2), (([2, 2], 4), [1], 2)]"
  :: "((nat list \<times> nat) \<times> nat list \<times> nat) list"
Loading theory "Diophantine_Eqns_Lin_Hom.Solver_Code"
### theory "Diophantine_Eqns_Lin_Hom.Solver_Code"
### 0.871s elapsed time, 0.644s cpu time, 0.000s GC time
isabelle document -o 'pdf' -n 'outline' -t '/proof,/ML' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Diophantine_Eqns_Lin_Hom/outline 2>&1
isabelle document -o 'pdf' -n 'document' -t '' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Diophantine_Eqns_Lin_Hom/document 2>&1
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty
Including comment 'isadelimproof' Excluding comment 'isatagproof'
Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty
) (/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu))) (./pdfsetup.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
No file root.aux.
(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)

LaTeX Warning: Citation `Huet1978' on page 1 undefined on input line 25.

(./session.tex (./List_Vector.tex [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdf
tex.map}] [2] [3] [4] [5] [6] [7] [8] [9] [10])
(./Linear_Diophantine_Equations.tex [11] [12] [13] [14] [15]

LaTeX Warning: Citation `Huet1978' on page 16 undefined on input line 1004.

[16] [17] [18] [19]
Overfull \hbox (4.55975pt too wide) in paragraph at lines 2669--2669
[]\OT1/cmr/bx/n/12 New con-di-tions: fa-cil-i-tat-ing gen-er-a-tion of can-di-d
ates from
[20] [21]) (./Sorted_Wrt.tex
Overfull \hbox (2.4711pt too wide) in paragraph at lines 47--49
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 sorted[]wrt[]Cons$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 sorted[]wrt P $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x $\OT1/cm
r/m/n/10 #$ \OT1/cmr/m/it/10 xs$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10  []!$ $\OT
1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 8 $\OT1/cmr/m/it/10 y$\OMS/cmsy/m/n/10 2$\OT1/
cmr/m/it/10 set xs$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 P x y$\OT1/cmr/m/n/10 )
$ $\OMS/cmsy/m/n/10 ^$ \OT1/cmr/m/it/10 sorted[]wrt
[22] [23]) (./Minimize_Wrt.tex [24]) (./Algorithm.tex [25] [26] [27] [28]
[29] [30] [31] [32]

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.

[33] [34] [35] [36] [37]) (./Solver_Code.tex))
No file root.bbl.
[38] (./root.aux)

Package rerunfilecheck Warning: File `root.out' has changed.
(rerunfilecheck)                Rerun to get outlines right
(rerunfilecheck)                or use package `bookmark'.


LaTeX Warning: There were undefined references.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts
/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmti10.pfb>
Output written on root.pdf (38 pages, 251511 bytes).
Transcript written on root.log.
This is BibTeX, Version 0.99d (TeX Live 2015/Debian)
The top-level auxiliary file: root.aux
The style file: abbrv.bst
Database file #1: root.bib
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty
Including comment 'isadelimproof' Excluding comment 'isatagproof'
Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty
) (/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu))) (./pdfsetup.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(./root.aux) (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)

LaTeX Warning: Citation `Huet1978' on page 1 undefined on input line 25.

(./root.toc [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}])
(./session.tex (./List_Vector.tex [2] [3] [4] [5] [6] [7] [8] [9] [10] [11])
(./Linear_Diophantine_Equations.tex [12] [13] [14] [15] [16]

LaTeX Warning: Citation `Huet1978' on page 17 undefined on input line 1004.

[17] [18] [19] [20]
Overfull \hbox (4.55975pt too wide) in paragraph at lines 2669--2669
[]\OT1/cmr/bx/n/12 New con-di-tions: fa-cil-i-tat-ing gen-er-a-tion of can-di-d
ates from
[21]) (./Sorted_Wrt.tex
Overfull \hbox (2.4711pt too wide) in paragraph at lines 47--49
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 sorted[]wrt[]Cons$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 sorted[]wrt P $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x $\OT1/cm
r/m/n/10 #$ \OT1/cmr/m/it/10 xs$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10  []!$ $\OT
1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 8 $\OT1/cmr/m/it/10 y$\OMS/cmsy/m/n/10 2$\OT1/
cmr/m/it/10 set xs$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 P x y$\OT1/cmr/m/n/10 )
$ $\OMS/cmsy/m/n/10 ^$ \OT1/cmr/m/it/10 sorted[]wrt
[22] [23]) (./Minimize_Wrt.tex [24] [25]) (./Algorithm.tex [26] [27] [28]
[29] [30] [31] [32]

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.

[33] [34] [35] [36] [37] [38]) (./Solver_Code.tex)) (./root.bbl) [39]
(./root.aux)

LaTeX Warning: There were undefined references.


LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts
/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmti10.pfb>
Output written on root.pdf (39 pages, 259478 bytes).
Transcript written on root.log.
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty
Including comment 'isadelimproof' Excluding comment 'isatagproof'
Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty
) (/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu))) (./pdfsetup.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(./root.aux) (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) (./root.toc [1{/var/li
b/texmf/fonts/map/pdftex/updmap/pdftex.map}]) (./session.tex (./List_Vector.tex
[2] [3] [4] [5] [6] [7] [8] [9] [10] [11]) (./Linear_Diophantine_Equations.tex
[12] [13] [14] [15] [16] [17] [18] [19] [20]
Overfull \hbox (4.55975pt too wide) in paragraph at lines 2669--2669
[]\OT1/cmr/bx/n/12 New con-di-tions: fa-cil-i-tat-ing gen-er-a-tion of can-di-d
ates from
[21]) (./Sorted_Wrt.tex
Overfull \hbox (2.4711pt too wide) in paragraph at lines 47--49
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 sorted[]wrt[]Cons$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 sorted[]wrt P $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x $\OT1/cm
r/m/n/10 #$ \OT1/cmr/m/it/10 xs$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10  []!$ $\OT
1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 8 $\OT1/cmr/m/it/10 y$\OMS/cmsy/m/n/10 2$\OT1/
cmr/m/it/10 set xs$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 P x y$\OT1/cmr/m/n/10 )
$ $\OMS/cmsy/m/n/10 ^$ \OT1/cmr/m/it/10 sorted[]wrt
[22] [23]) (./Minimize_Wrt.tex [24] [25]) (./Algorithm.tex [26] [27] [28]
[29] [30] [31] [32]

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.

[33] [34] [35] [36] [37] [38]) (./Solver_Code.tex)) (./root.bbl) [39]
(./root.aux) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts
/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmti10.pfb>
Output written on root.pdf (39 pages, 259789 bytes).
Transcript written on root.log.

This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu))) (./pdfsetup.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
No file root.aux.
(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)

LaTeX Warning: Citation `Huet1978' on page 1 undefined on input line 25.

(./session.tex (./List_Vector.tex [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdf
tex.map}] [2]
Overfull \hbox (24.5045pt too wide) in paragraph at lines 319--333
[][]  \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dotprod[]def \OT1/cmr/bx/n/
10 and \OT1/cmr/m/it/10 length[]Cons \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 min[
]Suc[]Suc \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 sum[]lessThan[]Suc[]shift
[3]
Overfull \hbox (18.0128pt too wide) in paragraph at lines 494--501
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis add[]right[
]cancel leI length[]append length[]drop not[]add[]less1 dotprod[]append$\OT1/cm
r/m/n/10 )$[] 
[4] [5]
Overfull \hbox (6.59976pt too wide) in paragraph at lines 945--958
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n
/10 )$ $($\OT1/cmr/m/it/10 metis $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$
\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lift-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/
10 assms le[]append order[]vec$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 order$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 strict[]iff[]order$\OT1/cmr/m/n/10 )$[] 
[6] [7]
Overfull \hbox (7.74632pt too wide) in paragraph at lines 1164--1166
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases b$\OT1/
cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 less[]Cons add[]mono[]thms[]linordered[]field dotprod[]le[]left$\OT1/cmr/m/n/1
0 )$[] 
[8] [9] [10] [11]
Overfull \hbox (6.9256pt too wide) in paragraph at lines 1757--1770
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 vdiff[]def upt[]Cons[]conv $\OT1/cmr/m/n/10 [$\OT1/
cmr/m/it/10 OF zero[]less[]Suc$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 map[]upt[]Su
c del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 upt[]Suc$\OT1/cmr/m/n/10 )$[] 
[12] [13] [14]) (./Linear_Diophantine_Equations.tex [15]
Overfull \hbox (24.2947pt too wide) in paragraph at lines 30--43
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis div[]by[]0 
div[]le[]dividend div[]le[]mono div[]mult[]self[]is[]m lcm[]nat[]def neq0[]conv
$\OT1/cmr/m/n/10 )$[] 
[16] [17] [18] [19] [20] [21] [22]
Overfull \hbox (54.43536pt too wide) in paragraph at lines 948--952
[][]  \OT1/cmr/bx/n/10 have $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 simp$\OT1/cmr/m
/n/10 ]$$:$ \OT1/cmr/m/it/10 length v $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 n \O
T1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/
10 ($\OT1/cmr/m/it/10 force dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 less[]appe
ndD Minimal[]Solutions[]length$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (17.49998pt too wide) in paragraph at lines 962--967
[][]  \OT1/cmr/bx/n/10 ul-ti-mately show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/1
0 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 hlde[]ops$\OML/cmm/m/it/
10 :$\OT1/cmr/m/it/10 Minimal[]Solutions[]def$\OT1/cmr/m/n/10 )$[] 

LaTeX Warning: Citation `Huet1978' on page 23 undefined on input line 1004.

[23] [24]
Overfull \hbox (28.40901pt too wide) in paragraph at lines 1262--1276
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/
cmr/m/n/10 ($\OT1/cmr/m/it/10 induct i$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 a
uto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]set[]conv[]nth sum[]list[]inc[
]gt0$ [] $ sum[]list[]inc[]gt0$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (3.48936pt too wide) in paragraph at lines 1375--1381
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis  inc$\OML/cmm/m/it/10 :$\OT1/
cmr/m/it/10 simps Suc[]eq[]plus1 Suc[]leI antisym[]conv2 leD sum[]list[]list[]u
pdate[]Suc$\OT1/cmr/m/n/10 )$[] 
[25]
Overfull \hbox (36.19467pt too wide) in paragraph at lines 1408--1415
[][]\OT1/cmr/bx/n/10 qed $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis Suc[]eq[]plu
s1 Suc[]leI antisym[]conv gr[]implies[]not0 sum[]list[]us[]gt0 sum[]list[]us[]l
e$\OT1/cmr/m/n/10 )$[] 
[26]
Overfull \hbox (0.45879pt too wide) in paragraph at lines 1593--1595
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro zero[]les
s$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis gr[]implies[]not0 nonzero[]iff s
l[]ys[]g[]ak sum[]list[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 
[27] [28] [29] [30] [31] [32] [33] [34] [35]
Overfull \hbox (24.2614pt too wide) in paragraph at lines 2590--2592
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis List[]Vec
tor$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 le0 Minimal[]Solutions[]length le[]appe
nd le[]list[]update less[]append

Overfull \hbox (4.55975pt too wide) in paragraph at lines 2669--2669
[]\OT1/cmr/bx/n/12 New con-di-tions: fa-cil-i-tat-ing gen-er-a-tion of can-di-d
ates from
[36]
Overfull \hbox (9.11513pt too wide) in paragraph at lines 2768--2771
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by$
\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/1
0 Special[]Solutions[]def$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis append[]
eq[]append[]conv[] 
[37] [38]
Overfull \hbox (9.11513pt too wide) in paragraph at lines 2929--2932
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by$
\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/1
0 Special[]Solutions[]def$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis append[]
eq[]append[]conv[] 
[39]
Overfull \hbox (19.99059pt too wide) in paragraph at lines 3065--3069
[][]  \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 sol$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/
it/10 a $[]$ x $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 b $[]$ y \OT1/cmr/bx/n/10 u
s-ing \OT1/cmr/m/it/10 min \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it
/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 Solutions[]def Minimal[]Solut
ions[]def$\OT1/cmr/m/n/10 )$[] 
[40] [41]) (./Sorted_Wrt.tex
Overfull \hbox (2.4711pt too wide) in paragraph at lines 47--49
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 sorted[]wrt[]Cons$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 sorted[]wrt P $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x $\OT1/cm
r/m/n/10 #$ \OT1/cmr/m/it/10 xs$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10  []!$ $\OT
1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 8 $\OT1/cmr/m/it/10 y$\OMS/cmsy/m/n/10 2$\OT1/
cmr/m/it/10 set xs$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 P x y$\OT1/cmr/m/n/10 )
$ $\OMS/cmsy/m/n/10 ^$ \OT1/cmr/m/it/10 sorted[]wrt
[42] [43]) (./Minimize_Wrt.tex
Overfull \hbox (18.87743pt too wide) in paragraph at lines 78--84
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sorted[]wrt[]Cons sorted[]wrt[]filter dest$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subse
t$\OT1/cmr/m/n/10 ]$$)$[] 
[44]
Overfull \hbox (8.81795pt too wide) in paragraph at lines 102--109
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct xs$\OT1/cm
r/m/n/10 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 s
ub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subset$\OT1/cmr/m
/n/10 ]$ \OT1/cmr/m/it/10 simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 sorted[]wrt[
]Cons$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (26.50385pt too wide) in paragraph at lines 138--152
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/
cmr/m/n/10 ($\OT1/cmr/m/it/10 induct xs$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 
auto$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 metis contra[]subsetD filter[]cong mi
nimize[]wrt[]subset$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (18.87743pt too wide) in paragraph at lines 165--171
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sorted[]wrt[]Cons sorted[]wrt[]filter dest$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subse
t$\OT1/cmr/m/n/10 ]$$)$[] 
) (./Algorithm.tex [45] [46]
Overfull \hbox (5.02478pt too wide) in paragraph at lines 227--228
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto$\OML/cmm/m/it/10 ;$ \OT1/cmr/m
/it/10 metis $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ 
\OT1/cmr/m/it/10 lift-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 append[]is[]Nil[]
conv case[]prod[]conv list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 set[]intros$\OT1
/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$[] 
[47] [48] [49] [50] [51] [52] [53] [54] [55]

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Overfull \hbox (13.07939pt too wide) in paragraph at lines 1499--1502
[][]  \OT1/cmr/bx/n/10 then con-sider $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x$\OM
L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 y$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 2$ \OT
1/cmr/m/it/10 set $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 special[]solutions a b$\O
T1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 j$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x$\OM
L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 y$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 2$ \OT
1/cmr/m/it/10 set $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 non[]special[]solutions
[56]
Overfull \hbox (45.58296pt too wide) in paragraph at lines 1543--1546
[][]      \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 ass \OT1/cmr/bx/n/10 by $\OT
1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 s
olve[]def Special[]Solutions[]in[]Solutions in[]non[]special[]solutions$\OT1/cm
r/m/n/10 )$[] 

Overfull \hbox (33.62244pt too wide) in paragraph at lines 1554--1556
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis 2 eq[]0
[]iff len nonzero[]Solutions[]iff nonzero[]iff zeroes[]ni[]non[]special[]soluti
ons$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (35.52946pt too wide) in paragraph at lines 1584--1587
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 sol \OT1/cmr/bx/n/10 by $\
OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 Minimal[]Solutions[]def Solutions[]def elim$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/i
t/10 less[]append[]cases$\OT1/cmr/m/n/10 )$[] 
[57]
Overfull \hbox (13.97485pt too wide) in paragraph at lines 1632--1634
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 sol$ [] $ set[]generate $\
OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of ?b ?a a b$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it
/10 uv $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 THEN Minimal[]Solutions[]imp[]Soluti
ons$\OT1/cmr/m/n/10 ]$

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.

[58]
Overfull \hbox (4.27965pt too wide) in paragraph at lines 1754--1772
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 solve[]subset[]Minimal[]Solution
s \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 Minimal[]Solutions[]subset[]solve \OT1/
cmr/bx/n/10 by \OT1/cmr/m/it/10 blast 
[59] [60] [61] [62] [63] [64] [65] [66]
Overfull \hbox (20.0726pt too wide) in paragraph at lines 2738--2740
[][]     \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tr
o$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 suffs[]cond1I suffs[]cond2I simp$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 pdprodl[]impl[]def suffs[]cond2[]conv$\OT1/cmr/m/n/
10 )$[] 
[67] [68]) (./Solver_Code.tex))
No file root.bbl.
[69] (./root.aux)

Package rerunfilecheck Warning: File `root.out' has changed.
(rerunfilecheck)                Rerun to get outlines right
(rerunfilecheck)                or use package `bookmark'.


LaTeX Warning: There were undefined references.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts
/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmsy5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mti10.pfb>
Output written on root.pdf (69 pages, 349210 bytes).
Transcript written on root.log.
This is BibTeX, Version 0.99d (TeX Live 2015/Debian)
The top-level auxiliary file: root.aux
The style file: abbrv.bst
Database file #1: root.bib
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu))) (./pdfsetup.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(./root.aux) (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)

LaTeX Warning: Citation `Huet1978' on page 1 undefined on input line 25.

(./root.toc [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}])
(./session.tex (./List_Vector.tex [2]
Overfull \hbox (24.5045pt too wide) in paragraph at lines 319--333
[][]  \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dotprod[]def \OT1/cmr/bx/n/
10 and \OT1/cmr/m/it/10 length[]Cons \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 min[
]Suc[]Suc \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 sum[]lessThan[]Suc[]shift
[3]
Overfull \hbox (18.0128pt too wide) in paragraph at lines 494--501
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis add[]right[
]cancel leI length[]append length[]drop not[]add[]less1 dotprod[]append$\OT1/cm
r/m/n/10 )$[] 
[4] [5] [6]
Overfull \hbox (6.59976pt too wide) in paragraph at lines 945--958
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n
/10 )$ $($\OT1/cmr/m/it/10 metis $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$
\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lift-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/
10 assms le[]append order[]vec$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 order$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 strict[]iff[]order$\OT1/cmr/m/n/10 )$[] 
[7]
Overfull \hbox (7.74632pt too wide) in paragraph at lines 1164--1166
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases b$\OT1/
cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 less[]Cons add[]mono[]thms[]linordered[]field dotprod[]le[]left$\OT1/cmr/m/n/1
0 )$[] 
[8] [9] [10] [11]
Overfull \hbox (6.9256pt too wide) in paragraph at lines 1757--1770
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 vdiff[]def upt[]Cons[]conv $\OT1/cmr/m/n/10 [$\OT1/
cmr/m/it/10 OF zero[]less[]Suc$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 map[]upt[]Su
c del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 upt[]Suc$\OT1/cmr/m/n/10 )$[] 
[12] [13] [14] [15]) (./Linear_Diophantine_Equations.tex
Overfull \hbox (24.2947pt too wide) in paragraph at lines 30--43
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis div[]by[]0 
div[]le[]dividend div[]le[]mono div[]mult[]self[]is[]m lcm[]nat[]def neq0[]conv
$\OT1/cmr/m/n/10 )$[] 
[16] [17] [18] [19] [20] [21] [22]
Overfull \hbox (54.43536pt too wide) in paragraph at lines 948--952
[][]  \OT1/cmr/bx/n/10 have $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 simp$\OT1/cmr/m
/n/10 ]$$:$ \OT1/cmr/m/it/10 length v $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 n \O
T1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/
10 ($\OT1/cmr/m/it/10 force dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 less[]appe
ndD Minimal[]Solutions[]length$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (17.49998pt too wide) in paragraph at lines 962--967
[][]  \OT1/cmr/bx/n/10 ul-ti-mately show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/1
0 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 hlde[]ops$\OML/cmm/m/it/
10 :$\OT1/cmr/m/it/10 Minimal[]Solutions[]def$\OT1/cmr/m/n/10 )$[] 

LaTeX Warning: Citation `Huet1978' on page 23 undefined on input line 1004.

[23] [24]
Overfull \hbox (28.40901pt too wide) in paragraph at lines 1262--1276
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/
cmr/m/n/10 ($\OT1/cmr/m/it/10 induct i$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 a
uto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]set[]conv[]nth sum[]list[]inc[
]gt0$ [] $ sum[]list[]inc[]gt0$\OT1/cmr/m/n/10 )$[] 
[25]
Overfull \hbox (3.48936pt too wide) in paragraph at lines 1375--1381
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis  inc$\OML/cmm/m/it/10 :$\OT1/
cmr/m/it/10 simps Suc[]eq[]plus1 Suc[]leI antisym[]conv2 leD sum[]list[]list[]u
pdate[]Suc$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (36.19467pt too wide) in paragraph at lines 1408--1415
[][]\OT1/cmr/bx/n/10 qed $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis Suc[]eq[]plu
s1 Suc[]leI antisym[]conv gr[]implies[]not0 sum[]list[]us[]gt0 sum[]list[]us[]l
e$\OT1/cmr/m/n/10 )$[] 
[26] [27]
Overfull \hbox (0.45879pt too wide) in paragraph at lines 1593--1595
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro zero[]les
s$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis gr[]implies[]not0 nonzero[]iff s
l[]ys[]g[]ak sum[]list[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 
[28] [29] [30] [31] [32] [33] [34] [35]
Overfull \hbox (24.2614pt too wide) in paragraph at lines 2590--2592
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis List[]Vec
tor$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 le0 Minimal[]Solutions[]length le[]appe
nd le[]list[]update less[]append
[36]
Overfull \hbox (4.55975pt too wide) in paragraph at lines 2669--2669
[]\OT1/cmr/bx/n/12 New con-di-tions: fa-cil-i-tat-ing gen-er-a-tion of can-di-d
ates from
[37]
Overfull \hbox (9.11513pt too wide) in paragraph at lines 2768--2771
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by$
\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/1
0 Special[]Solutions[]def$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis append[]
eq[]append[]conv[] 
[38]
Overfull \hbox (9.11513pt too wide) in paragraph at lines 2929--2932
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by$
\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/1
0 Special[]Solutions[]def$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis append[]
eq[]append[]conv[] 
[39]
Overfull \hbox (19.99059pt too wide) in paragraph at lines 3065--3069
[][]  \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 sol$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/
it/10 a $[]$ x $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 b $[]$ y \OT1/cmr/bx/n/10 u
s-ing \OT1/cmr/m/it/10 min \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it
/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 Solutions[]def Minimal[]Solut
ions[]def$\OT1/cmr/m/n/10 )$[] 
[40] [41]) (./Sorted_Wrt.tex [42]
Overfull \hbox (2.4711pt too wide) in paragraph at lines 47--49
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 sorted[]wrt[]Cons$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 sorted[]wrt P $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x $\OT1/cm
r/m/n/10 #$ \OT1/cmr/m/it/10 xs$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10  []!$ $\OT
1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 8 $\OT1/cmr/m/it/10 y$\OMS/cmsy/m/n/10 2$\OT1/
cmr/m/it/10 set xs$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 P x y$\OT1/cmr/m/n/10 )
$ $\OMS/cmsy/m/n/10 ^$ \OT1/cmr/m/it/10 sorted[]wrt
[43] [44]) (./Minimize_Wrt.tex
Overfull \hbox (18.87743pt too wide) in paragraph at lines 78--84
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sorted[]wrt[]Cons sorted[]wrt[]filter dest$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subse
t$\OT1/cmr/m/n/10 ]$$)$[] 

Overfull \hbox (8.81795pt too wide) in paragraph at lines 102--109
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct xs$\OT1/cm
r/m/n/10 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 s
ub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subset$\OT1/cmr/m
/n/10 ]$ \OT1/cmr/m/it/10 simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 sorted[]wrt[
]Cons$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (26.50385pt too wide) in paragraph at lines 138--152
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/
cmr/m/n/10 ($\OT1/cmr/m/it/10 induct xs$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 
auto$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 metis contra[]subsetD filter[]cong mi
nimize[]wrt[]subset$\OT1/cmr/m/n/10 )$[] 
[45]
Overfull \hbox (18.87743pt too wide) in paragraph at lines 165--171
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sorted[]wrt[]Cons sorted[]wrt[]filter dest$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subse
t$\OT1/cmr/m/n/10 ]$$)$[] 
) (./Algorithm.tex [46] [47]
Overfull \hbox (5.02478pt too wide) in paragraph at lines 227--228
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto$\OML/cmm/m/it/10 ;$ \OT1/cmr/m
/it/10 metis $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ 
\OT1/cmr/m/it/10 lift-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 append[]is[]Nil[]
conv case[]prod[]conv list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 set[]intros$\OT1
/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$[] 
[48] [49] [50] [51] [52] [53] [54] [55] [56]

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Overfull \hbox (13.07939pt too wide) in paragraph at lines 1499--1502
[][]  \OT1/cmr/bx/n/10 then con-sider $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x$\OM
L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 y$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 2$ \OT
1/cmr/m/it/10 set $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 special[]solutions a b$\O
T1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 j$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x$\OM
L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 y$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 2$ \OT
1/cmr/m/it/10 set $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 non[]special[]solutions

Overfull \hbox (45.58296pt too wide) in paragraph at lines 1543--1546
[][]      \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 ass \OT1/cmr/bx/n/10 by $\OT
1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 s
olve[]def Special[]Solutions[]in[]Solutions in[]non[]special[]solutions$\OT1/cm
r/m/n/10 )$[] 

Overfull \hbox (33.62244pt too wide) in paragraph at lines 1554--1556
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis 2 eq[]0
[]iff len nonzero[]Solutions[]iff nonzero[]iff zeroes[]ni[]non[]special[]soluti
ons$\OT1/cmr/m/n/10 )$[] 
[57]
Overfull \hbox (35.52946pt too wide) in paragraph at lines 1584--1587
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 sol \OT1/cmr/bx/n/10 by $\
OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 Minimal[]Solutions[]def Solutions[]def elim$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/i
t/10 less[]append[]cases$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (13.97485pt too wide) in paragraph at lines 1632--1634
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 sol$ [] $ set[]generate $\
OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of ?b ?a a b$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it
/10 uv $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 THEN Minimal[]Solutions[]imp[]Soluti
ons$\OT1/cmr/m/n/10 ]$

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.

[58]
Overfull \hbox (4.27965pt too wide) in paragraph at lines 1754--1772
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 solve[]subset[]Minimal[]Solution
s \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 Minimal[]Solutions[]subset[]solve \OT1/
cmr/bx/n/10 by \OT1/cmr/m/it/10 blast 
[59] [60] [61] [62] [63] [64] [65] [66]
Overfull \hbox (20.0726pt too wide) in paragraph at lines 2738--2740
[][]     \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tr
o$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 suffs[]cond1I suffs[]cond2I simp$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 pdprodl[]impl[]def suffs[]cond2[]conv$\OT1/cmr/m/n/
10 )$[] 
[67] [68]) (./Solver_Code.tex)) (./root.bbl) [69] (./root.aux)

LaTeX Warning: There were undefined references.


LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts
/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmsy5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mti10.pfb>
Output written on root.pdf (69 pages, 356655 bytes).
Transcript written on root.log.
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu))) (./pdfsetup.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(./root.aux) (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) (./root.toc [1{/var/li
b/texmf/fonts/map/pdftex/updmap/pdftex.map}]) (./session.tex (./List_Vector.tex
[2]
Overfull \hbox (24.5045pt too wide) in paragraph at lines 319--333
[][]  \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dotprod[]def \OT1/cmr/bx/n/
10 and \OT1/cmr/m/it/10 length[]Cons \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 min[
]Suc[]Suc \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 sum[]lessThan[]Suc[]shift
[3]
Overfull \hbox (18.0128pt too wide) in paragraph at lines 494--501
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis add[]right[
]cancel leI length[]append length[]drop not[]add[]less1 dotprod[]append$\OT1/cm
r/m/n/10 )$[] 
[4] [5] [6]
Overfull \hbox (6.59976pt too wide) in paragraph at lines 945--958
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto$\OT1/cmr/m/n
/10 )$ $($\OT1/cmr/m/it/10 metis $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$
\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 lift-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/
10 assms le[]append order[]vec$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 order$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 strict[]iff[]order$\OT1/cmr/m/n/10 )$[] 
[7]
Overfull \hbox (7.74632pt too wide) in paragraph at lines 1164--1166
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases b$\OT1/
cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 less[]Cons add[]mono[]thms[]linordered[]field dotprod[]le[]left$\OT1/cmr/m/n/1
0 )$[] 
[8] [9] [10] [11]
Overfull \hbox (6.9256pt too wide) in paragraph at lines 1757--1770
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 vdiff[]def upt[]Cons[]conv $\OT1/cmr/m/n/10 [$\OT1/
cmr/m/it/10 OF zero[]less[]Suc$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 map[]upt[]Su
c del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 upt[]Suc$\OT1/cmr/m/n/10 )$[] 
[12] [13] [14] [15]) (./Linear_Diophantine_Equations.tex
Overfull \hbox (24.2947pt too wide) in paragraph at lines 30--43
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis div[]by[]0 
div[]le[]dividend div[]le[]mono div[]mult[]self[]is[]m lcm[]nat[]def neq0[]conv
$\OT1/cmr/m/n/10 )$[] 
[16] [17] [18] [19] [20] [21] [22]
Overfull \hbox (54.43536pt too wide) in paragraph at lines 948--952
[][]  \OT1/cmr/bx/n/10 have $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 simp$\OT1/cmr/m
/n/10 ]$$:$ \OT1/cmr/m/it/10 length v $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 n \O
T1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/
10 ($\OT1/cmr/m/it/10 force dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 less[]appe
ndD Minimal[]Solutions[]length$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (17.49998pt too wide) in paragraph at lines 962--967
[][]  \OT1/cmr/bx/n/10 ul-ti-mately show \OT1/cmr/m/it/10 False \OT1/cmr/bx/n/1
0 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 hlde[]ops$\OML/cmm/m/it/
10 :$\OT1/cmr/m/it/10 Minimal[]Solutions[]def$\OT1/cmr/m/n/10 )$[] 
[23] [24]
Overfull \hbox (28.40901pt too wide) in paragraph at lines 1262--1276
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/
cmr/m/n/10 ($\OT1/cmr/m/it/10 induct i$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 a
uto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]set[]conv[]nth sum[]list[]inc[
]gt0$ [] $ sum[]list[]inc[]gt0$\OT1/cmr/m/n/10 )$[] 
[25]
Overfull \hbox (3.48936pt too wide) in paragraph at lines 1375--1381
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis  inc$\OML/cmm/m/it/10 :$\OT1/
cmr/m/it/10 simps Suc[]eq[]plus1 Suc[]leI antisym[]conv2 leD sum[]list[]list[]u
pdate[]Suc$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (36.19467pt too wide) in paragraph at lines 1408--1415
[][]\OT1/cmr/bx/n/10 qed $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis Suc[]eq[]plu
s1 Suc[]leI antisym[]conv gr[]implies[]not0 sum[]list[]us[]gt0 sum[]list[]us[]l
e$\OT1/cmr/m/n/10 )$[] 
[26] [27]
Overfull \hbox (0.45879pt too wide) in paragraph at lines 1593--1595
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro zero[]les
s$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis gr[]implies[]not0 nonzero[]iff s
l[]ys[]g[]ak sum[]list[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 
[28] [29] [30] [31] [32] [33] [34] [35]
Overfull \hbox (24.2614pt too wide) in paragraph at lines 2590--2592
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis List[]Vec
tor$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 le0 Minimal[]Solutions[]length le[]appe
nd le[]list[]update less[]append
[36]
Overfull \hbox (4.55975pt too wide) in paragraph at lines 2669--2669
[]\OT1/cmr/bx/n/12 New con-di-tions: fa-cil-i-tat-ing gen-er-a-tion of can-di-d
ates from
[37]
Overfull \hbox (9.11513pt too wide) in paragraph at lines 2768--2771
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by$
\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/1
0 Special[]Solutions[]def$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis append[]
eq[]append[]conv[] 
[38]
Overfull \hbox (9.11513pt too wide) in paragraph at lines 2929--2932
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by$
\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/1
0 Special[]Solutions[]def$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 metis append[]
eq[]append[]conv[] 
[39]
Overfull \hbox (19.99059pt too wide) in paragraph at lines 3065--3069
[][]  \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 sol$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/
it/10 a $[]$ x $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 b $[]$ y \OT1/cmr/bx/n/10 u
s-ing \OT1/cmr/m/it/10 min \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it
/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 Solutions[]def Minimal[]Solut
ions[]def$\OT1/cmr/m/n/10 )$[] 
[40] [41]) (./Sorted_Wrt.tex [42]
Overfull \hbox (2.4711pt too wide) in paragraph at lines 47--49
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 sorted[]wrt[]Cons$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 sorted[]wrt P $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x $\OT1/cm
r/m/n/10 #$ \OT1/cmr/m/it/10 xs$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10  []!$ $\OT
1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 8 $\OT1/cmr/m/it/10 y$\OMS/cmsy/m/n/10 2$\OT1/
cmr/m/it/10 set xs$\OML/cmm/m/it/10 :$ \OT1/cmr/m/it/10 P x y$\OT1/cmr/m/n/10 )
$ $\OMS/cmsy/m/n/10 ^$ \OT1/cmr/m/it/10 sorted[]wrt
[43] [44]) (./Minimize_Wrt.tex
Overfull \hbox (18.87743pt too wide) in paragraph at lines 78--84
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sorted[]wrt[]Cons sorted[]wrt[]filter dest$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subse
t$\OT1/cmr/m/n/10 ]$$)$[] 

Overfull \hbox (8.81795pt too wide) in paragraph at lines 102--109
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct xs$\OT1/cm
r/m/n/10 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 s
ub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subset$\OT1/cmr/m
/n/10 ]$ \OT1/cmr/m/it/10 simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 sorted[]wrt[
]Cons$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (26.50385pt too wide) in paragraph at lines 138--152
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 by $\OT1/
cmr/m/n/10 ($\OT1/cmr/m/it/10 induct xs$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 
auto$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 metis contra[]subsetD filter[]cong mi
nimize[]wrt[]subset$\OT1/cmr/m/n/10 )$[] 
[45]
Overfull \hbox (18.87743pt too wide) in paragraph at lines 165--171
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sorted[]wrt[]Cons sorted[]wrt[]filter dest$\OT1/cmr/m/n/10 :$ \OT1/c
mr/m/it/10 sub-setD $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF minimize[]wrt[]subse
t$\OT1/cmr/m/n/10 ]$$)$[] 
) (./Algorithm.tex [46] [47]
Overfull \hbox (5.02478pt too wide) in paragraph at lines 227--228
[][]    $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto$\OML/cmm/m/it/10 ;$ \OT1/cmr/m
/it/10 metis $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 no[]types$\OML/cmm/m/it/10 ;$ 
\OT1/cmr/m/it/10 lift-ing$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 append[]is[]Nil[]
conv case[]prod[]conv list$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 set[]intros$\OT1
/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$[] 
[48] [49] [50] [51] [52] [53] [54] [55] [56]

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1481.


Overfull \hbox (13.07939pt too wide) in paragraph at lines 1499--1502
[][]  \OT1/cmr/bx/n/10 then con-sider $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x$\OM
L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 y$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 2$ \OT
1/cmr/m/it/10 set $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 special[]solutions a b$\O
T1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 j$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 x$\OM
L/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 y$\OT1/cmr/m/n/10 )$ $\OMS/cmsy/m/n/10 2$ \OT
1/cmr/m/it/10 set $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 non[]special[]solutions

Overfull \hbox (45.58296pt too wide) in paragraph at lines 1543--1546
[][]      \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 ass \OT1/cmr/bx/n/10 by $\OT
1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 s
olve[]def Special[]Solutions[]in[]Solutions in[]non[]special[]solutions$\OT1/cm
r/m/n/10 )$[] 

Overfull \hbox (33.62244pt too wide) in paragraph at lines 1554--1556
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis 2 eq[]0
[]iff len nonzero[]Solutions[]iff nonzero[]iff zeroes[]ni[]non[]special[]soluti
ons$\OT1/cmr/m/n/10 )$[] 
[57]
Overfull \hbox (35.52946pt too wide) in paragraph at lines 1584--1587
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 sol \OT1/cmr/bx/n/10 by $\
OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 Minimal[]Solutions[]def Solutions[]def elim$\OT1/cmr/m/n/10 !$$:$ \OT1/cmr/m/i
t/10 less[]append[]cases$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (13.97485pt too wide) in paragraph at lines 1632--1634
[][]        \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 sol$ [] $ set[]generate $\
OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of ?b ?a a b$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it
/10 uv $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 THEN Minimal[]Solutions[]imp[]Soluti
ons$\OT1/cmr/m/n/10 ]$

Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.


Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
(hyperref)                removing `\sfcode' on input line 1661.

[58]
Overfull \hbox (4.27965pt too wide) in paragraph at lines 1754--1772
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 solve[]subset[]Minimal[]Solution
s \OT1/cmr/bx/n/10 and \OT1/cmr/m/it/10 Minimal[]Solutions[]subset[]solve \OT1/
cmr/bx/n/10 by \OT1/cmr/m/it/10 blast 
[59] [60] [61] [62] [63] [64] [65] [66]
Overfull \hbox (20.0726pt too wide) in paragraph at lines 2738--2740
[][]     \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto in-tr
o$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 suffs[]cond1I suffs[]cond2I simp$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 pdprodl[]impl[]def suffs[]cond2[]conv$\OT1/cmr/m/n/
10 )$[] 
[67] [68]) (./Solver_Code.tex)) (./root.bbl) [69] (./root.aux) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts
/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmsy5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mti10.pfb>
Output written on root.pdf (69 pages, 356614 bytes).
Transcript written on root.log.

*** No such directory: "/media/data/jenkins/workspace/afp-repo-afp/afp/thys/Diophantine_Eqns_Lin_Hom/generated"
*** At command "export_code" (line 17 of "~~/afp/thys/Diophantine_Eqns_Lin_Hom/Solver_Code.thy")