Loading theory "Linear_Recurrences.Eulerian_Polynomials" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Inhomogenous_Recurrences")
Loading theory "Linear_Recurrences.Linear_Recurrences_Common" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences")
### theory "Linear_Recurrences.Linear_Recurrences_Common"
### 0.115s elapsed time, 0.320s cpu time, 0.000s GC time
Loading theory "Linear_Recurrences.Linear_Recurrences_Misc" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences" via "Linear_Recurrences.Rational_FPS_Solver" via "Linear_Recurrences.Partial_Fraction_Decomposition")
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
consts
  eulerian_poly :: "nat \<Rightarrow> 'a poly"
consts
  fps_monom_poly_aux :: "'a \<Rightarrow> nat \<Rightarrow> 'a poly"
### theory "Linear_Recurrences.Eulerian_Polynomials"
### 0.498s elapsed time, 1.132s cpu time, 0.000s GC time
Loading theory "Linear_Recurrences.RatFPS" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences")
### theory "Linear_Recurrences.Linear_Recurrences_Misc"
### 0.458s elapsed time, 0.964s cpu time, 0.000s GC time
Loading theory "Linear_Recurrences.Factorizations" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences" via "Linear_Recurrences.Rational_FPS_Solver")
### Generation of a parametrized correspondence relation failed.
### Reason:  No relator for the type "Polynomial.poly" found.
instantiation
  ratfps :: ({factorial_ring_gcd,field}) idom
  uminus_ratfps == uminus :: 'a ratfps \<Rightarrow> 'a ratfps
  one_ratfps == one_class.one :: 'a ratfps
  times_ratfps == times ::
    'a ratfps \<Rightarrow> 'a ratfps \<Rightarrow> 'a ratfps
  zero_ratfps == zero_class.zero :: 'a ratfps
  minus_ratfps == minus ::
    'a ratfps \<Rightarrow> 'a ratfps \<Rightarrow> 'a ratfps
  plus_ratfps == plus ::
    'a ratfps \<Rightarrow> 'a ratfps \<Rightarrow> 'a ratfps
### theory "Linear_Recurrences.Factorizations"
### 0.249s elapsed time, 0.500s cpu time, 0.000s GC time
Loading theory "Linear_Recurrences.Factorial_Ring" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences" via "Linear_Recurrences.Rational_FPS_Solver" via "Linear_Recurrences.Pochhammer_Polynomials" via "Linear_Recurrences.Polynomial")
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
instantiation
  ratfps :: ({factorial_ring_gcd,field}) inverse
  inverse_ratfps == inverse :: 'a ratfps \<Rightarrow> 'a ratfps
  divide_ratfps == divide ::
    'a ratfps \<Rightarrow> 'a ratfps \<Rightarrow> 'a ratfps
instantiation
  ratfps :: (equal) equal
  equal_ratfps == equal_class.equal ::
    'a ratfps \<Rightarrow> 'a ratfps \<Rightarrow> bool
instantiation
  fps :: (equal) equal
  equal_fps == equal_class.equal ::
    'a fps \<Rightarrow> 'a fps \<Rightarrow> bool
### theory "Linear_Recurrences.RatFPS"
### 1.545s elapsed time, 3.036s cpu time, 0.304s GC time
Loading theory "Linear_Recurrences.Partial_Fraction_Decomposition" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences" via "Linear_Recurrences.Rational_FPS_Solver")
class normalization_semidom = algebraic_semidom +
  semidom_divide_unit_factor +
  fixes normalize :: "'a \<Rightarrow> 'a" 
  assumes
    "unit_factor_mult_normalize": "\<And>a. unit_factor a * normalize a = a"
    and "normalize_0": "normalize (0::'a) = (0::'a)"
class semiring_gcd = gcd + normalization_semidom +
  assumes "gcd_dvd1": "\<And>a b. gcd a b dvd a"
    and "gcd_dvd2": "\<And>a b. gcd a b dvd b"
    and
    "gcd_greatest":
      "\<And>c a b.
          \<lbrakk>c dvd a; c dvd b\<rbrakk>
          \<Longrightarrow> c dvd gcd a b"
    and "normalize_gcd": "\<And>a b. normalize (gcd a b) = gcd a b"
    and "lcm_gcd": "\<And>a b. lcm a b = normalize (a * b) div gcd a b"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
consts
  decompose_aux :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
### theory "Linear_Recurrences.Partial_Fraction_Decomposition"
### 1.460s elapsed time, 2.920s cpu time, 0.000s GC time
Loading theory "Linear_Recurrences.Stirling" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences" via "Linear_Recurrences.Rational_FPS_Solver" via "Linear_Recurrences.Pochhammer_Polynomials")
Found termination order:
  "(\<lambda>p. size (snd p)) <*mlex*>
   (\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (snd p)) <*mlex*>
   (\<lambda>p. size (fst p)) <*mlex*> {}"
consts
  stirling_row_aux ::
    "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
### theory "Linear_Recurrences.Stirling"
### 0.461s elapsed time, 0.908s cpu time, 0.000s GC time
### Ignoring duplicate rewrite rule:
### fps_of_poly 0 \<equiv> 0
### Ignoring duplicate rewrite rule:
### fps_of_poly 1 \<equiv> 1
### Ignoring duplicate rewrite rule:
### fps_of_poly (numeral ?n1) \<equiv> numeral ?n1
### Ignoring duplicate rewrite rule:
### fps_of_poly [:0::?'a1, 1::?'a1:] \<equiv> fps_X
class factorial_semiring = normalization_semidom +
  assumes
    "prime_factorization_exists":
      "\<And>x.
          x \<noteq> (0::'a) \<Longrightarrow>
          \<exists>A.
             (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and>
             prod_mset A = normalize x"
### Ignoring duplicate rewrite rule:
### fps_of_poly 0 \<equiv> 0
### Ignoring duplicate rewrite rule:
### fps_of_poly 1 \<equiv> 1
### Ignoring duplicate rewrite rule:
### fps_of_poly (numeral ?n1) \<equiv> numeral ?n1
### Ignoring duplicate rewrite rule:
### fps_of_poly [:0::?'a1, 1::?'a1:] \<equiv> fps_X
### Ignoring duplicate rewrite rule:
### fps_of_poly (pCons ?c1 ?p1) \<equiv> fps_const ?c1 + fps_of_poly ?p1 * fps_X
class factorial_semiring = normalization_semidom +
  assumes
    "prime_factorization_exists":
      "\<And>x.
          x \<noteq> (0::'a) \<Longrightarrow>
          \<exists>A.
             (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and>
             prod_mset A = normalize x"
*** Failed to apply initial proof method (line 214 of "~~/afp/thys/Linear_Recurrences/Linear_Recurrences_Misc.thy"):
*** goal (1 subgoal):
***  1. gcd [:1::'a, c:] [:1::'a, c':] =
***     gcd ([:1::'a, c:] mod [:1::'a, c':]) [:1::'a, c':]
*** At command "by" (line 214 of "~~/afp/thys/Linear_Recurrences/Linear_Recurrences_Misc.thy")
class factorial_semiring_gcd = factorial_semiring + Gcd +
  assumes "gcd_eq_gcd_factorial": "\<And>a b. gcd a b = gcd_factorial a b"
    and "lcm_eq_lcm_factorial": "\<And>a b. lcm a b = lcm_factorial a b"
    and "Gcd_eq_Gcd_factorial": "\<And>A. Gcd A = Gcd_factorial A"
    and "Lcm_eq_Lcm_factorial": "\<And>A. Lcm A = Lcm_factorial A"
### theory "Linear_Recurrences.Factorial_Ring"
### 10.047s elapsed time, 19.848s cpu time, 1.268s GC time
Loading theory "Linear_Recurrences.Polynomial" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences" via "Linear_Recurrences.Rational_FPS_Solver" via "Linear_Recurrences.Pochhammer_Polynomials")
instantiation
  poly :: (zero) zero
  zero_poly == zero_class.zero :: 'a poly
consts
  Poly :: "'a list \<Rightarrow> 'a poly"
instantiation
  poly :: ({zero,equal}) equal
  equal_poly == equal_class.equal ::
    'a poly \<Rightarrow> 'a poly \<Rightarrow> bool
instantiation
  poly :: (comm_monoid_add) comm_monoid_add
  plus_poly == plus :: 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly
instantiation
  poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
  minus_poly == minus :: 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly
instantiation
  poly :: (ab_group_add) ab_group_add
  uminus_poly == uminus :: 'a poly \<Rightarrow> 'a poly
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
instantiation
  poly :: (comm_semiring_0) comm_semiring_0
  times_poly == times :: 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly
instantiation
  poly :: (comm_semiring_1) comm_semiring_1
  one_poly == one_class.one :: 'a poly
instantiation
  poly :: (linordered_idom) linordered_idom
  sgn_poly == sgn :: 'a poly \<Rightarrow> 'a poly
  abs_poly == abs :: 'a poly \<Rightarrow> 'a poly
  less_eq_poly == less_eq ::
    'a poly \<Rightarrow> 'a poly \<Rightarrow> bool
  less_poly == less :: 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
instantiation
  poly :: (idom_divide) idom_divide
  divide_poly == divide ::
    'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly
Found termination order:
  "(\<lambda>p. size (snd (snd (snd (snd (snd p)))))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (snd (snd (snd (snd (snd p)))))) <*mlex*> {}"
instantiation
  poly :: ({idom_divide,semidom_divide_unit_factor}) normalization_semidom
  normalize_poly == normalize :: 'a poly \<Rightarrow> 'a poly
  unit_factor_poly == unit_factor :: 'a poly \<Rightarrow> 'a poly
class field_unit_factor = field + unit_factor +
  assumes "unit_factor_field": "unit_factor = id"
Proofs for inductive predicate(s) "eucl_rel_poly"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
instantiation
  poly :: (field) semidom_modulo
  modulo_poly == modulo ::
    'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (snd (snd (snd (snd p))))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (snd (snd (snd p)))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (snd (snd (snd p)))) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size (snd (snd (snd (snd p))))) <*mlex*> {}"
### theory "Linear_Recurrences.Polynomial"
### 8.337s elapsed time, 16.560s cpu time, 1.056s GC time
Loading theory "Linear_Recurrences.Pochhammer_Polynomials" (required by "Linear_Recurrences.Linear_Recurrences_Solver" via "Linear_Recurrences.Linear_Homogenous_Recurrences" via "Linear_Recurrences.Rational_FPS_Solver")
### theory "Linear_Recurrences.Pochhammer_Polynomials"
### 0.902s elapsed time, 1.748s cpu time, 0.380s GC time
isabelle document -o 'pdf' -n 'document' -t '' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Linear_Recurrences/document 2>&1
isabelle document -o 'pdf' -n 'outline' -t '/proof,/ML' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Linear_Recurrences/outline 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/amsfonts/amsfonts.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (./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/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) [1{/var/lib/texmf/fo
nts/map/pdftex/updmap/pdftex.map}] (./session.tex (./RatFPS.tex)
(./Stirling.tex [2] [3]) (./Factorial_Ring.tex [4] [5] [6] [7] [8] [9] [10]
[11]
Overfull \hbox (11.16814pt too wide) in paragraph at lines 2329--2329
[]\OT1/cmr/bx/n/12 Factorial semir-ings: al-ge-braic struc-tures with unique pr
ime
[12] [13] [14] [15] [16] [17] [18] [19]
Overfull \hbox (6.21616pt too wide) in paragraph at lines 4855--4856
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 a div b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 prime[]factorization
[20] [21] [22]
Overfull \hbox (14.46059pt too wide) in paragraph at lines 6031--6032
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 gcd a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[23]
Overfull \hbox (15.99394pt too wide) in paragraph at lines 6051--6052
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 lcm a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[24]) (./Polynomial.tex [25]

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


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


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


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


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


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

[26] [27] [28] [29] [30]
Overfull \hbox (5.01166pt too wide) in paragraph at lines 1745--1747
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 poly[]of[]list[]impl $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 code ab-stract$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 co-
effs $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 poly[]of[]list as$\OT1/cmr/m/n/10 )$ $
=$ \OT1/cmr/m/it/10 strip[]while $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 HOL$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 eq
[31] [32] [33] [34] [35] [36] [37] [38]
Overfull \hbox (32.25041pt too wide) in paragraph at lines 3854--3856
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]0$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$ 
\OT1/cmr/m/it/10 semiring[]no[]zero[]divisors[] 
[39]
Overfull \hbox (49.62807pt too wide) in paragraph at lines 4247--4263
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]1$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]1[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 
)$ \OT1/cmr/m/it/10 semiring[]1[]no[]zero[]divisors
[40] [41] [42] [43] [44] [45] [46]
Overfull \hbox (9.43272pt too wide) in paragraph at lines 6157--6158
[][]  \OT1/cmr/m/it/10 synthetic[]divmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pC
ons a p$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 c $\OT1/cmr/m/n/10 =$ $($$\OML/cmm/
m/it/10 ^^U$$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 q$\OML/cmm/m/it/10 ;$ \OT1/cmr/
m/it/10 r$\OT1/cmr/m/n/10 )$$\OML/cmm/m/it/10 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/
it/10 pCons r q$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1
/cmr/m/it/10 c $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 r$\OT1/cmr/m/n/10 )$$)$ 
$($\OT1/cmr/m/it/10 synthetic[]divmod
[47] [48] [49] [50] [51] [52] [53] [54] [55] [56]
Overfull \hbox (43.11435pt too wide) in paragraph at lines 9486--9488
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 DERIV[]add[]const$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 DE-RIV f x $\OT1/cmr/m/n/10 :$$\OML/cmm/m/it/10 >$ \OT1/cmr/
m/it/10 D $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 DE-RIV $\OT1
/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 x$\OML/cmm/m/it/10 :$ \OT1
/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 f x $\OT1/cmr/m/n/10 :$$:$ 
$ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]fi
eld$\OT1/cmr/m/n/10 )$
[57] [58] [59] [60] [61] [62] [63]
Overfull \hbox (29.60196pt too wide) in paragraph at lines 11712--11714
[][]\OT1/cmr/bx/n/10 instantiation \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$
 $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 semidom[]divide[]unit[]factor$\OML/cmm
/m/it/10 ;$\OT1/cmr/m/it/10 idom[]divide$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$
 \OT1/cmr/m/it/10 normalization[]semidom[] 
[64] [65] [66] [67] [68] [69] [70]
Overfull \hbox (8.8534pt too wide) in paragraph at lines 13637--13639
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]mod[]impl$\OT1/cmr/m/n/10 [
$\OT1/cmr/m/it/10 code$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 pseudo[]mod f g $
\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 poly[]of[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 pseudo[]mod[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 coeffs
[71]
Overfull \hbox (37.10872pt too wide) in paragraph at lines 13863--13865
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list[]1$\OT1/
cmr/m/n/10 :$ \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list 1 $\OT1/cmr/m/n/10 =$
 \OT1/cmr/m/it/10 divmod[]poly[]one[]main[]list[] 
[72]
Overfull \hbox (93.00832pt too wide) in paragraph at lines 13945--13947
[][]\OT1/cmr/bx/n/10 lemmas \OT1/cmr/m/it/10 pdivmod[]via[]divmod[]list $\OT1/c
mr/m/n/10 =$ \OT1/cmr/m/it/10 pdivmod[]via[]pseudo[]divmod[]list$\OT1/cmr/m/n/1
0 [$\OT1/cmr/m/it/10 unfolded pseudo[]divmod[]main[]list[]1$\OT1/cmr/m/n/10 ]$[
] 

Overfull \hbox (63.45209pt too wide) in paragraph at lines 13948--13950
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 mod[]poly[]one[]main[]list$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 snd $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 divmod[]pol
y[]one[]main[]list q r d n$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 mod[]poly[]o
ne[]main[]list
[73] [74] [75] [76]) (./Pochhammer_Polynomials.tex
Overfull \hbox (39.72092pt too wide) in paragraph at lines 105--107
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pochhammer[]poly[]Suc$\OT1/cmr/m/n/
10 :$ \OT1/cmr/m/it/10 pochhammer[]poly $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Suc
 n$\OT1/cmr/m/n/10 )$ $=$ $[$$:$\OT1/cmr/m/it/10 of[]nat n$\OML/cmm/m/it/10 ;$\
OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10
 pochhammer[]poly
) (./Linear_Recurrences_Misc.tex) (./Partial_Fraction_Decomposition.tex)
(./Factorizations.tex [77] [78] [79]) (./Linear_Recurrences_Common.tex
Overfull \hbox (2.17294pt too wide) in paragraph at lines 6--6
[]\OT1/cmr/bx/n/14.4 Material com-mon to ho-moge-nous and in-ho-moge-
) (./Eulerian_Polynomials.tex [80]
Overfull \hbox (6.71323pt too wide) in paragraph at lines 177--178
[][]  \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 fps[]monom[]poly c k $\OT1/cmr/m/
n/10 =$ $($\OT1/cmr/m/it/10 if k $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 then 1 
else pcom-pose $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pCons 0 $\OT1/cmr/m/n/10 ($\
OT1/cmr/m/it/10 eulerian[]poly
[81]))
No file root.bbl.
[82] (./root.aux)

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

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr
10.pfb></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/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/amsfonts/cm/cmti12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/symbols/msam10.pfb>
Output written on root.pdf (82 pages, 328256 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/amsfonts/amsfonts.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (./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/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (./root.toc [1{/var/
lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (2.68887pt too wide) in paragraph at lines 48--48
 [][] [][][]\OT1/cmr/m/n/10.95 Improved Code-Equations for Poly-no-mial (Pseudo
) Di- 
[2]) [3] (./session.tex (./RatFPS.tex) (./Stirling.tex [4] [5])
(./Factorial_Ring.tex [6] [7] [8] [9] [10] [11] [12] [13]
Overfull \hbox (11.16814pt too wide) in paragraph at lines 2329--2329
[]\OT1/cmr/bx/n/12 Factorial semir-ings: al-ge-braic struc-tures with unique pr
ime
[14] [15] [16] [17] [18] [19] [20] [21]
Overfull \hbox (6.21616pt too wide) in paragraph at lines 4855--4856
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 a div b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 prime[]factorization
[22] [23] [24]
Overfull \hbox (14.46059pt too wide) in paragraph at lines 6031--6032
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 gcd a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[25]
Overfull \hbox (15.99394pt too wide) in paragraph at lines 6051--6052
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 lcm a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[26]) (./Polynomial.tex [27]

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


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


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


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


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


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

[28] [29] [30] [31] [32]
Overfull \hbox (5.01166pt too wide) in paragraph at lines 1745--1747
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 poly[]of[]list[]impl $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 code ab-stract$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 co-
effs $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 poly[]of[]list as$\OT1/cmr/m/n/10 )$ $
=$ \OT1/cmr/m/it/10 strip[]while $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 HOL$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 eq
[33] [34] [35] [36] [37] [38] [39] [40]
Overfull \hbox (32.25041pt too wide) in paragraph at lines 3854--3856
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]0$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$ 
\OT1/cmr/m/it/10 semiring[]no[]zero[]divisors[] 
[41]
Overfull \hbox (49.62807pt too wide) in paragraph at lines 4247--4263
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]1$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]1[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 
)$ \OT1/cmr/m/it/10 semiring[]1[]no[]zero[]divisors
[42] [43] [44] [45] [46] [47] [48]
Overfull \hbox (9.43272pt too wide) in paragraph at lines 6157--6158
[][]  \OT1/cmr/m/it/10 synthetic[]divmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pC
ons a p$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 c $\OT1/cmr/m/n/10 =$ $($$\OML/cmm/
m/it/10 ^^U$$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 q$\OML/cmm/m/it/10 ;$ \OT1/cmr/
m/it/10 r$\OT1/cmr/m/n/10 )$$\OML/cmm/m/it/10 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/
it/10 pCons r q$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1
/cmr/m/it/10 c $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 r$\OT1/cmr/m/n/10 )$$)$ 
$($\OT1/cmr/m/it/10 synthetic[]divmod
[49] [50] [51] [52] [53] [54] [55] [56] [57] [58]
Overfull \hbox (43.11435pt too wide) in paragraph at lines 9486--9488
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 DERIV[]add[]const$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 DE-RIV f x $\OT1/cmr/m/n/10 :$$\OML/cmm/m/it/10 >$ \OT1/cmr/
m/it/10 D $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 DE-RIV $\OT1
/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 x$\OML/cmm/m/it/10 :$ \OT1
/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 f x $\OT1/cmr/m/n/10 :$$:$ 
$ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]fi
eld$\OT1/cmr/m/n/10 )$
[59] [60] [61] [62] [63] [64] [65]
Overfull \hbox (29.60196pt too wide) in paragraph at lines 11712--11714
[][]\OT1/cmr/bx/n/10 instantiation \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$
 $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 semidom[]divide[]unit[]factor$\OML/cmm
/m/it/10 ;$\OT1/cmr/m/it/10 idom[]divide$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$
 \OT1/cmr/m/it/10 normalization[]semidom[] 
[66] [67] [68] [69] [70] [71] [72]
Overfull \hbox (8.8534pt too wide) in paragraph at lines 13637--13639
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]mod[]impl$\OT1/cmr/m/n/10 [
$\OT1/cmr/m/it/10 code$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 pseudo[]mod f g $
\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 poly[]of[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 pseudo[]mod[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 coeffs
[73]
Overfull \hbox (37.10872pt too wide) in paragraph at lines 13863--13865
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list[]1$\OT1/
cmr/m/n/10 :$ \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list 1 $\OT1/cmr/m/n/10 =$
 \OT1/cmr/m/it/10 divmod[]poly[]one[]main[]list[] 
[74]
Overfull \hbox (93.00832pt too wide) in paragraph at lines 13945--13947
[][]\OT1/cmr/bx/n/10 lemmas \OT1/cmr/m/it/10 pdivmod[]via[]divmod[]list $\OT1/c
mr/m/n/10 =$ \OT1/cmr/m/it/10 pdivmod[]via[]pseudo[]divmod[]list$\OT1/cmr/m/n/1
0 [$\OT1/cmr/m/it/10 unfolded pseudo[]divmod[]main[]list[]1$\OT1/cmr/m/n/10 ]$[
] 

Overfull \hbox (63.45209pt too wide) in paragraph at lines 13948--13950
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 mod[]poly[]one[]main[]list$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 snd $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 divmod[]pol
y[]one[]main[]list q r d n$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 mod[]poly[]o
ne[]main[]list
[75] [76] [77] [78]) (./Pochhammer_Polynomials.tex
Overfull \hbox (39.72092pt too wide) in paragraph at lines 105--107
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pochhammer[]poly[]Suc$\OT1/cmr/m/n/
10 :$ \OT1/cmr/m/it/10 pochhammer[]poly $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Suc
 n$\OT1/cmr/m/n/10 )$ $=$ $[$$:$\OT1/cmr/m/it/10 of[]nat n$\OML/cmm/m/it/10 ;$\
OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10
 pochhammer[]poly
) (./Linear_Recurrences_Misc.tex) (./Partial_Fraction_Decomposition.tex)
(./Factorizations.tex [79] [80] [81]) (./Linear_Recurrences_Common.tex
Overfull \hbox (2.17294pt too wide) in paragraph at lines 6--6
[]\OT1/cmr/bx/n/14.4 Material com-mon to ho-moge-nous and in-ho-moge-
) (./Eulerian_Polynomials.tex [82]
Overfull \hbox (6.71323pt too wide) in paragraph at lines 177--178
[][]  \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 fps[]monom[]poly c k $\OT1/cmr/m/
n/10 =$ $($\OT1/cmr/m/it/10 if k $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 then 1 
else pcom-pose $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pCons 0 $\OT1/cmr/m/n/10 ($\
OT1/cmr/m/it/10 eulerian[]poly
[83]))
No file root.bbl.
[84] (./root.aux) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr
10.pfb></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/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/amsfonts/cm/cmti12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/symbols/msam10.pfb>
Output written on root.pdf (84 pages, 337527 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/amsfonts/amsfonts.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (./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/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (./root.toc [1{/var/
lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (2.68887pt too wide) in paragraph at lines 48--48
 [][] [][][]\OT1/cmr/m/n/10.95 Improved Code-Equations for Poly-no-mial (Pseudo
) Di- 
[2]) [3] (./session.tex (./RatFPS.tex) (./Stirling.tex [4] [5])
(./Factorial_Ring.tex [6] [7] [8] [9] [10] [11] [12] [13]
Overfull \hbox (11.16814pt too wide) in paragraph at lines 2329--2329
[]\OT1/cmr/bx/n/12 Factorial semir-ings: al-ge-braic struc-tures with unique pr
ime
[14] [15] [16] [17] [18] [19] [20] [21]
Overfull \hbox (6.21616pt too wide) in paragraph at lines 4855--4856
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 a div b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 prime[]factorization
[22] [23] [24]
Overfull \hbox (14.46059pt too wide) in paragraph at lines 6031--6032
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 gcd a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[25]
Overfull \hbox (15.99394pt too wide) in paragraph at lines 6051--6052
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 lcm a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[26]) (./Polynomial.tex [27]

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


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


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


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


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


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

[28] [29] [30] [31] [32]
Overfull \hbox (5.01166pt too wide) in paragraph at lines 1745--1747
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 poly[]of[]list[]impl $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 code ab-stract$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 co-
effs $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 poly[]of[]list as$\OT1/cmr/m/n/10 )$ $
=$ \OT1/cmr/m/it/10 strip[]while $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 HOL$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 eq
[33] [34] [35] [36] [37] [38] [39] [40]
Overfull \hbox (32.25041pt too wide) in paragraph at lines 3854--3856
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]0$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$ 
\OT1/cmr/m/it/10 semiring[]no[]zero[]divisors[] 
[41]
Overfull \hbox (49.62807pt too wide) in paragraph at lines 4247--4263
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]1$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]1[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 
)$ \OT1/cmr/m/it/10 semiring[]1[]no[]zero[]divisors
[42] [43] [44] [45] [46] [47] [48]
Overfull \hbox (9.43272pt too wide) in paragraph at lines 6157--6158
[][]  \OT1/cmr/m/it/10 synthetic[]divmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pC
ons a p$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 c $\OT1/cmr/m/n/10 =$ $($$\OML/cmm/
m/it/10 ^^U$$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 q$\OML/cmm/m/it/10 ;$ \OT1/cmr/
m/it/10 r$\OT1/cmr/m/n/10 )$$\OML/cmm/m/it/10 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/
it/10 pCons r q$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1
/cmr/m/it/10 c $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 r$\OT1/cmr/m/n/10 )$$)$ 
$($\OT1/cmr/m/it/10 synthetic[]divmod
[49] [50] [51] [52] [53] [54] [55] [56] [57] [58]
Overfull \hbox (43.11435pt too wide) in paragraph at lines 9486--9488
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 DERIV[]add[]const$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 DE-RIV f x $\OT1/cmr/m/n/10 :$$\OML/cmm/m/it/10 >$ \OT1/cmr/
m/it/10 D $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 DE-RIV $\OT1
/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 x$\OML/cmm/m/it/10 :$ \OT1
/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 f x $\OT1/cmr/m/n/10 :$$:$ 
$ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]fi
eld$\OT1/cmr/m/n/10 )$
[59] [60] [61] [62] [63] [64] [65]
Overfull \hbox (29.60196pt too wide) in paragraph at lines 11712--11714
[][]\OT1/cmr/bx/n/10 instantiation \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$
 $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 semidom[]divide[]unit[]factor$\OML/cmm
/m/it/10 ;$\OT1/cmr/m/it/10 idom[]divide$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$
 \OT1/cmr/m/it/10 normalization[]semidom[] 
[66] [67] [68] [69] [70] [71] [72]
Overfull \hbox (8.8534pt too wide) in paragraph at lines 13637--13639
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]mod[]impl$\OT1/cmr/m/n/10 [
$\OT1/cmr/m/it/10 code$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 pseudo[]mod f g $
\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 poly[]of[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 pseudo[]mod[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 coeffs
[73]
Overfull \hbox (37.10872pt too wide) in paragraph at lines 13863--13865
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list[]1$\OT1/
cmr/m/n/10 :$ \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list 1 $\OT1/cmr/m/n/10 =$
 \OT1/cmr/m/it/10 divmod[]poly[]one[]main[]list[] 
[74]
Overfull \hbox (93.00832pt too wide) in paragraph at lines 13945--13947
[][]\OT1/cmr/bx/n/10 lemmas \OT1/cmr/m/it/10 pdivmod[]via[]divmod[]list $\OT1/c
mr/m/n/10 =$ \OT1/cmr/m/it/10 pdivmod[]via[]pseudo[]divmod[]list$\OT1/cmr/m/n/1
0 [$\OT1/cmr/m/it/10 unfolded pseudo[]divmod[]main[]list[]1$\OT1/cmr/m/n/10 ]$[
] 

Overfull \hbox (63.45209pt too wide) in paragraph at lines 13948--13950
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 mod[]poly[]one[]main[]list$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 snd $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 divmod[]pol
y[]one[]main[]list q r d n$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 mod[]poly[]o
ne[]main[]list
[75] [76] [77] [78]) (./Pochhammer_Polynomials.tex
Overfull \hbox (39.72092pt too wide) in paragraph at lines 105--107
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pochhammer[]poly[]Suc$\OT1/cmr/m/n/
10 :$ \OT1/cmr/m/it/10 pochhammer[]poly $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Suc
 n$\OT1/cmr/m/n/10 )$ $=$ $[$$:$\OT1/cmr/m/it/10 of[]nat n$\OML/cmm/m/it/10 ;$\
OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10
 pochhammer[]poly
) (./Linear_Recurrences_Misc.tex) (./Partial_Fraction_Decomposition.tex)
(./Factorizations.tex [79] [80] [81]) (./Linear_Recurrences_Common.tex
Overfull \hbox (2.17294pt too wide) in paragraph at lines 6--6
[]\OT1/cmr/bx/n/14.4 Material com-mon to ho-moge-nous and in-ho-moge-
) (./Eulerian_Polynomials.tex [82]
Overfull \hbox (6.71323pt too wide) in paragraph at lines 177--178
[][]  \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 fps[]monom[]poly c k $\OT1/cmr/m/
n/10 =$ $($\OT1/cmr/m/it/10 if k $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 then 1 
else pcom-pose $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pCons 0 $\OT1/cmr/m/n/10 ($\
OT1/cmr/m/it/10 eulerian[]poly
[83]))
No file root.bbl.
[84] (./root.aux) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr
10.pfb></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/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/amsfonts/cm/cmti12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/symbols/msam10.pfb>
Output written on root.pdf (84 pages, 337738 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/amsfonts/amsfonts.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (./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/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) [1{/var/lib/texmf/fo
nts/map/pdftex/updmap/pdftex.map}] (./session.tex (./RatFPS.tex)
(./Stirling.tex [2] [3] [4] [5] [6] [7]) (./Factorial_Ring.tex [8] [9] [10]
Overfull \hbox (9.44902pt too wide) in paragraph at lines 455--469
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 unit[]imp[]no[]irreducible[]divi
sors$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF assms$\OT1/cmr/m/n/10 ($\OT1/cmr/m/i
t/10 1$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 prime[]elem[]imp[]irreducible$\OT1/c
mr/m/n/10 [$\OT1/cmr/m/it/10 OF
[11] [12]
Overfull \hbox (26.81523pt too wide) in paragraph at lines 836--841
[][]  \OT1/cmr/bx/n/10 more-over from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 h
ave $\OMS/cmsy/m/n/10 :$\OT1/cmr/m/it/10 is[]unit p \OT1/cmr/bx/n/10 by $\OT1/c
mr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime
[]elem[]def is[]unit[]power[]iff$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (10.79758pt too wide) in paragraph at lines 908--921
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cm
r/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]def mult$\OML/cmm/m/it/10 :$\OT1/cmr/
m/it/10 commute$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of a$\OT1/cmr/m/n/10 ]$ \OT1
/cmr/m/it/10 is[]unit[]mult[]iff mult[]unit[]dvd[]iff$\OT1/cmr/m/n/10 )$[] 
[13]
Overfull \hbox (12.0489pt too wide) in paragraph at lines 976--978
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis dvd[]mu
lt[]right dvd[]times[]left[]cancel[]iff mult$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/1
0 left[]commute mult[]zero[]left$\OT1/cmr/m/n/10 )$[] 
[14]
Overfull \hbox (5.12607pt too wide) in paragraph at lines 1132--1146
[][]  \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 n$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 a
uto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]not[]unit prime[]elem
[]dvd[]multD$\OT1/cmr/m/n/10 )$[] 
[15] [16] [17]
Overfull \hbox (11.69632pt too wide) in paragraph at lines 1788--1792
[][]  \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 ir-re-ducible q \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 prime[]elem[]imp[]irreducible 
prime[]def$\OT1/cmr/m/n/10 )$[] 
[18]
Overfull \hbox (30.63289pt too wide) in paragraph at lines 1943--1957
[][]  \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 in-tro$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 p
rod[]mset[]subset[]imp[]dvd prod[]mset[]primes[]dvd[]imp[]subset$\OT1/cmr/m/n/1
0 )$[] 
[19]
Overfull \hbox (11.4095pt too wide) in paragraph at lines 2017--2019
[][]    \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 A1[]def A2[]def Mul-ti-set$\OML/cmm/m/it/10 :$\O
T1/cmr/m/it/10 subset[]eq[]diff[]conv Mul-ti-set$\OML/cmm/m/it/10 :$\OT1/cmr/m/
it/10 union[]commute$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (1.77489pt too wide) in paragraph at lines 2032--2034
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst $\OT1/cmr
/m/n/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 1 2$\OT1/
cmr/m/n/10 )$ \OT1/cmr/m/it/10 is[]unit[]prod[]mset[]primes[]iff$\OT1/cmr/m/n/1
0 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 Mul-ti-s
et$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 in[]diffD$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (1.20242pt too wide) in paragraph at lines 2076--2080
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 x \OT1/cmr/bx/n/10 have \OT1/cmr
/m/it/10 x ^ n dvd prod[]mset A ^ n \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1
/cmr/m/it/10 intro dvd[]power[]same dvd[]prod[]mset$\OT1/cmr/m/n/10 )$[] 
[20] [21]
Overfull \hbox (11.16814pt too wide) in paragraph at lines 2329--2329
[]\OT1/cmr/bx/n/12 Factorial semir-ings: al-ge-braic struc-tures with unique pr
ime

Overfull \hbox (6.13147pt too wide) in paragraph at lines 2376--2380
[][]      \OT1/cmr/bx/n/10 with []$\OMS/cmsy/m/n/10 :$\OT1/cmr/m/it/10 is[]unit
 a[] less$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 prems \OT1/cmr/bx/n/10 have \OT1/
cmr/m/it/10 ir-re-ducible a \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/i
t/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 irreducible[]altdef$\OT1/cmr
/m/n/10 )$[] 
[22]
Overfull \hbox (5.4238pt too wide) in paragraph at lines 2490--2494
[][]      \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 A B \OT1/cmr/bx/n/10 show \OT1
/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 i
ntro exI$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] A $\OT1/cmr/m/n/10 +$ \OT1/cm
r/m/it/10 B$\OT1/cmr/m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10
 :$ \OT1/cmr/m/it/10 c normalize[]mult$\OT1/cmr/m/n/10 )$[] 
[23]
Overfull \hbox (7.38255pt too wide) in paragraph at lines 2623--2625
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 dvd prod[]mset[]primes[]irreduci
ble[]imp[]prime$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of A B C$\OML/cmm/m/it/10 ;$
 \OT1/cmr/m/it/10 OF this ABC$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OML/cmm/m/i
t/10 ;$\OT1/cmr/m/it/10 3$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 5$\OT1/cmr/m/n/10
 )$$]$
[24]
Overfull \hbox (6.55193pt too wide) in paragraph at lines 2724--2729
[][]    \OT1/cmr/bx/n/10 fi-nally show \OT1/cmr/m/it/10 p $\OMS/cmsy/m/n/10 2$$
\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 A \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 
p A \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst $\OT1/cmr/m/n
/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 prime[]dvd[]prod
[]mset[]primes[]iff$\OT1/cmr/m/n/10 )$[] 
[25] [26]
Overfull \hbox (35.03365pt too wide) in paragraph at lines 3242--3256
[][]  \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 subst prime[]elem[]multiplicity[]eq[]zero[]iff$\O
T1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it
/10 primes[]dvd[]imp[]eq$\OT1/cmr/m/n/10 )$[] 
[27]
Overfull \hbox (31.33105pt too wide) in paragraph at lines 3368--3373
[][]    \OT1/cmr/bx/n/10 more-over from \OT1/cmr/m/it/10 assms$\OT1/cmr/m/n/10 
($\OT1/cmr/m/it/10 2$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 xp \OT1/cmr/bx/n/10 ha
ve \OT1/cmr/m/it/10 mul-ti-plic-ity p x $\OML/cmm/m/it/10 <$ \OT1/cmr/m/it/10 S
uc n \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro multiplicity
[]lessI$\OT1/cmr/m/n/10 )$[] 
[28] [29]
Overfull \hbox (42.299pt too wide) in paragraph at lines 3630--3632
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst mult$\OML
/cmm/m/it/10 :$\OT1/cmr/m/it/10 commute$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 
simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 mult[]unit[]dvd[]iff power[]mult[]
distrib is[]unit[]power[]iff$\OT1/cmr/m/n/10 )$[] 
[30]
Overfull \hbox (2.52225pt too wide) in paragraph at lines 3909--3911
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro multiplic
ity[]geI $\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 :$
 \OT1/cmr/m/it/10 dvd[]trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF multiplicity
[]dvd$ [] $ assms$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$$]$$)$
[] 
[31] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (4.71416pt too wide) in paragraph at lines 4108--4113
[][]      \OT1/cmr/bx/n/10 also from \OT1/cmr/m/it/10 x p \OT1/cmr/bx/n/10 have
 $[] $ $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 $\OMS/cmsy/m/n/10  []!$ $:$\OT1/c
mr/m/it/10 p dvd x \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 multiplicity[]eq[]zero[]iff$\OT1/cmr/m
/n/10 )$[] 
[32]
Overfull \hbox (0.98625pt too wide) in paragraph at lines 4243--4245
[][]  \OT1/cmr/bx/n/10 thus \OT1/cmr/m/it/10 count $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 p $\OMS/cmsy/m
/n/10 ^^C$ \OT1/cmr/m/it/10 x$\OT1/cmr/m/n/10 )$$)$ \OT1/cmr/m/it/10 q $\OT1/cm
r/m/n/10 =$ \OT1/cmr/m/it/10 count $\OT1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 f$$\OT1
/cmr/m/n/10 #$\OT1/cmr/m/it/10 p$\OT1/cmr/m/n/10 #$$\OMS/cmsy/m/n/10 g$ $\OT1/c
mr/m/n/10 +$ \OT1/cmr/m/it/10 prime[]factorization
[33] [34]
Overfull \hbox (15.81303pt too wide) in paragraph at lines 4481--4483
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\
OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 mult[]ac prime[]factorization[]times[]prime 
Mul-ti-set$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 union[]commute$\OT1/cmr/m/n/10 )
$[] 

Overfull \hbox (40.95099pt too wide) in paragraph at lines 4532--4536
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 show \OT1/c
mr/m/it/10 nor-mal-ize x $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 nor-mal-ize y \OT
1/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 prod[]mset[]prime[]factorization$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (44.55727pt too wide) in paragraph at lines 4567--4569
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule prime[]fac
torization[]prod[]mset[]primes$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all
 add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]prime[]factors[]imp[]prime$\OT1/cm
r/m/n/10 )$[] 

Overfull \hbox (20.85785pt too wide) in paragraph at lines 4569--4572
[][]  \OT1/cmr/bx/n/10 also have \OT1/cmr/m/it/10 prime[]factorization $\OT1/cm
r/m/n/10 ($\OT1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prim
e[]factorization x $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 prime[]factorization

Overfull \hbox (33.42188pt too wide) in paragraph at lines 4573--4575
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule prime[]fac
torization[]prod[]mset[]primes$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp
$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]prime[]factors[]imp[]prime$\OT1/cmr/m/
n/10 )$[] 
[35]
Overfull \hbox (25.28094pt too wide) in paragraph at lines 4719--4720
[][]                   $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]multiplicity[]prod[]mset[]distrib su
m[]unfold[]sum[]mset[] 
[36]
Overfull \hbox (16.5629pt too wide) in paragraph at lines 4744--4757
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst prime[]elem
[]multiplicity[]power[]distrib$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp
$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]multiplicity[]other$\OT1/cmr/m/n/10
 )$[] 

Overfull \hbox (50.5364pt too wide) in paragraph at lines 4771--4777
[][]     $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \
OT1/cmr/m/it/10 prime[]factorization[]mult prime[]factorization[]prime Mul-ti-s
et$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 union[]commute$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (22.83113pt too wide) in paragraph at lines 4810--4812
[][]  \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 x dvd y $\OMS/cmsy/m/n/10  []!$ \O
T1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorizat
ion x$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 dvd prod[]mset $\OT1/cmr/m/n/10 ($\OT
1/cmr/m/it/10 prime[]factorization

Overfull \hbox (6.21616pt too wide) in paragraph at lines 4855--4856
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 a div b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 prime[]factorization
[37]
Overfull \hbox (12.16023pt too wide) in paragraph at lines 4951--4952
[][]      $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ 
\OT1/cmr/m/it/10 assms count[]prime[]factorization[]prime in[]prime[]factors[]i
mp[]prime$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (24.46587pt too wide) in paragraph at lines 4993--4996
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 A[]def \OT1/cmr/bx/n/10 b
y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst mul-ti-set$\OML/cmm/m/it/10 :$\OT1/
cmr/m/it/10 Abs[]multiset[]inverse$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[
]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 multiset[]def$\OT1/cmr/m/n/10 )$[]
 

Overfull \hbox (1.20328pt too wide) in paragraph at lines 5005--5009
[][]  \OT1/cmr/bx/n/10 also have $[] $ $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 pro
d[]mset A \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 prod[]mset[]multiplicity S[]eq set[]mset[]A

Overfull \hbox (29.18195pt too wide) in paragraph at lines 5026--5029
[][]  \OT1/cmr/bx/n/10 also have \OT1/cmr/m/it/10 prime[]factorization $\OT1/cm
r/m/n/10 ($\OT1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prim
e[]factorization n$\OT1/cmr/m/n/10 )$$)$ $=$ \OT1/cmr/m/it/10 prime[]factorizat
ion
[38]
Overfull \hbox (56.44945pt too wide) in paragraph at lines 5063--5065
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro image[]
mset[]cong$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ 
\OT1/cmr/m/it/10 set[]mset[]A multiplicity[]self prime[]multiplicity[]other$\OT
1/cmr/m/n/10 )$[] 

Overfull \hbox (5.04556pt too wide) in paragraph at lines 5143--5147
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms False \OT1/cmr/bx/n/10 show 
\OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/
10 subst $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/
it/10 prime[]factorization[]subset[]iff[]dvd$\OT1/cmr/m/n/10 )$[] 
[39] [40]
Overfull \hbox (1.69742pt too wide) in paragraph at lines 5361--5362
[][]          \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a 
$\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization

Overfull \hbox (1.69742pt too wide) in paragraph at lines 5397--5398
[][]          \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a 
$\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization
[41]
Overfull \hbox (4.25296pt too wide) in paragraph at lines 5631--5632
[][]           \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cm
r/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a
 $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization
[42]
Overfull \hbox (3.08865pt too wide) in paragraph at lines 5772--5775
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Gcd[]factor
ial A$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 Inf $\OT1/cmr/m/n/10 ($\OT1/cmr/m
/it/10 prime[]factorization
[43] [44]
Overfull \hbox (14.46059pt too wide) in paragraph at lines 6031--6032
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 gcd a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization

Overfull \hbox (15.99394pt too wide) in paragraph at lines 6051--6052
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 lcm a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[45]
Overfull \hbox (43.35431pt too wide) in paragraph at lines 6080--6087
[][]  \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 prime[]factorization[]Gcd[]factorial Gcd[]eq[]Gcd[]
factorial Gcd[]factorial[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (49.76532pt too wide) in paragraph at lines 6102--6109
[][]  \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 prime[]factorization[]Lcm[]factorial Lcm[]eq[]Lcm[]
factorial Lcm[]factorial[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 
[46]
Overfull \hbox (55.76273pt too wide) in paragraph at lines 6263--6265
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 count[]prime[]factorization[]prime $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 prime[]fact
orization[]gcd[]factorial$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (57.29608pt too wide) in paragraph at lines 6276--6278
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 count[]prime[]factorization[]prime $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 prime[]fact
orization[]lcm[]factorial$\OT1/cmr/m/n/10 )$[] 
[47]) (./Polynomial.tex [48]

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


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


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


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


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


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

[49] [50] [51] [52] [53] [54] [55] [56]
Overfull \hbox (5.01166pt too wide) in paragraph at lines 1745--1747
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 poly[]of[]list[]impl $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 code ab-stract$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 co-
effs $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 poly[]of[]list as$\OT1/cmr/m/n/10 )$ $
=$ \OT1/cmr/m/it/10 strip[]while $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 HOL$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 eq
[57] [58] [59] [60] [61]
Overfull \hbox (7.42665pt too wide) in paragraph at lines 2755--2768
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis coeff[]add 
coeff[]eq[]0 monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 add$\OML/cm
m/m/it/10 :$\OT1/cmr/m/it/10 left[]neutral degree[]add[]eq[]right$\OT1/cmr/m/n/
10 )$[] 
[62] [63]
Overfull \hbox (38.39879pt too wide) in paragraph at lines 3009--3011
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule coeffs[]eq
I$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 nth[]default[]map[]eq nth[]default[]coeffs[]eq no[]trailing[]map
[64] [65]
Overfull \hbox (45.5543pt too wide) in paragraph at lines 3596--3598
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule coeffs[]eq
I$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp add$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 no[]trailing[]map nth[]default[]map[]eq nth[]default[]coeffs[]eq
[66] [67]
Overfull \hbox (32.25041pt too wide) in paragraph at lines 3854--3856
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]0$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$ 
\OT1/cmr/m/it/10 semiring[]no[]zero[]divisors[] 
[68] [69]
Overfull \hbox (49.62807pt too wide) in paragraph at lines 4247--4263
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]1$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]1[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 
)$ \OT1/cmr/m/it/10 semiring[]1[]no[]zero[]divisors
[70] [71]
Overfull \hbox (23.10243pt too wide) in paragraph at lines 4776--4778
[][]        \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 assms length[]coeffs nth[]default[]coeffs[]e
q $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/i
t/10 nth[]default[]def$\OT1/cmr/m/n/10 )$[] 
[72]
Overfull \hbox (5.96727pt too wide) in paragraph at lines 4824--4837
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro poly[]eqI$\
OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr
/m/it/10 assms coeff[]map[]poly coeff[]pCons split$\OT1/cmr/m/n/10 :$ \OT1/cmr/
m/it/10 nat$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 splits$\OT1/cmr/m/n/10 )$[] 
[73] [74] [75]
Overfull \hbox (22.59839pt too wide) in paragraph at lines 5527--5540
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule order[]antis
ym $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le le[]degree$\OT1/cmr/
m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 c
oeff[]mult[]degree[]sum$\OT1/cmr/m/n/10 )$[] 
[76] [77] [78] [79]
Overfull \hbox (9.43272pt too wide) in paragraph at lines 6157--6158
[][]  \OT1/cmr/m/it/10 synthetic[]divmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pC
ons a p$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 c $\OT1/cmr/m/n/10 =$ $($$\OML/cmm/
m/it/10 ^^U$$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 q$\OML/cmm/m/it/10 ;$ \OT1/cmr/
m/it/10 r$\OT1/cmr/m/n/10 )$$\OML/cmm/m/it/10 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/
it/10 pCons r q$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1
/cmr/m/it/10 c $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 r$\OT1/cmr/m/n/10 )$$)$ 
$($\OT1/cmr/m/it/10 synthetic[]divmod
[80] [81] [82] [83]
Overfull \hbox (12.44328pt too wide) in paragraph at lines 6791--6793
[][]   \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis order[
]2 not[]gr0 poly[]eq[]0[]iff[]dvd power[]0 power[]Suc[]0 power[]one[]right$\OT1
/cmr/m/n/10 )$[] 
[84] [85]
Overfull \hbox (57.51828pt too wide) in paragraph at lines 7009--7011
[][]    \OT1/cmr/bx/n/10 by $\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 hide[
]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 One[]nat[]def add[]Suc[]right monoid[
]add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr
/m/it/10 right[]neutral[] 

Overfull \hbox (4.7849pt too wide) in paragraph at lines 7011--7012
[][]      \OT1/cmr/m/it/10 one[]neq[]zero order[]mult pCons[]eq[]0[]iff power[]
add power[]eq[]0[]iff power[]one[]right$\OT1/cmr/m/n/10 )$[] 
[86] [87] [88]
Overfull \hbox (23.32683pt too wide) in paragraph at lines 7630--7643
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct p ar-bi-tr
ary$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 q$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/1
0 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]add pcompose[]smu
lt pcompose[]pCons
[89]
Overfull \hbox (24.07547pt too wide) in paragraph at lines 7649--7662
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct p ar-bi-tr
ary$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 q$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/1
0 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]pCons pcompose[]a
dd pcompose[]mult$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (3.83954pt too wide) in paragraph at lines 7704--7717
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct A rule$\OT
1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 infinite[]finite[]induct$\OT1/cmr/m/n/10 )$ $(
$\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]1
 pcompose[]mult$\OT1/cmr/m/n/10 )$[] 
[90] [91] [92] [93] [94]
Overfull \hbox (26.78821pt too wide) in paragraph at lines 8578--8591
[][]  \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 degree[]eq[]length[]coeffs coeffs[]reflect[]poly le
ngth[]dropWhile[]le diff[]le[]mono$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (7.1392pt too wide) in paragraph at lines 8614--8627
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases p rule$\OT1
/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pCons[]cases$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/i
t/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 reflect[]poly[]pCons degree[]
eq[]length[]coeffs$\OT1/cmr/m/n/10 )$[] 
[95] [96] [97] [98] [99] [100]
Overfull \hbox (43.11435pt too wide) in paragraph at lines 9486--9488
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 DERIV[]add[]const$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 DE-RIV f x $\OT1/cmr/m/n/10 :$$\OML/cmm/m/it/10 >$ \OT1/cmr/
m/it/10 D $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 DE-RIV $\OT1
/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 x$\OML/cmm/m/it/10 :$ \OT1
/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 f x $\OT1/cmr/m/n/10 :$$:$ 
$ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]fi
eld$\OT1/cmr/m/n/10 )$
[101] [102] [103]
Overfull \hbox (5.12115pt too wide) in paragraph at lines 9897--9899
[][]      \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\O
MS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 nd dvd[]mult[]cancel[]right power[]not[]ze
ro pCons[]eq[]0[]iff power[]Suc
[104] [105] [106] [107] [108]
Overfull \hbox (43.09401pt too wide) in paragraph at lines 10585--10588
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dr b[]def \OT1/cmr/bx/n/1
0 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule or-der$\OML/cmm/m/it/10 :$\OT1/cm
r/m/it/10 trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le$\OT1/cmr
/m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 degree[]monom[]le$\OT1/cmr/m/n/10 )$[] 
[109] [110] [111] [112] [113]
Overfull \hbox (18.54pt too wide) in paragraph at lines 11313--11316
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dr \OT1/cmr/bx/n/10 by $\
OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule or-der$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/
10 trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le$\OT1/cmr/m/n/10
 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 degree
[]monom[]le$\OT1/cmr/m/n/10 )$[] 
[114] [115] [116] [117]
Overfull \hbox (29.60196pt too wide) in paragraph at lines 11712--11714
[][]\OT1/cmr/bx/n/10 instantiation \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$
 $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 semidom[]divide[]unit[]factor$\OML/cmm
/m/it/10 ;$\OT1/cmr/m/it/10 idom[]divide$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$
 \OT1/cmr/m/it/10 normalization[]semidom[] 
[118] [119] [120] [121] [122] [123] [124] [125] [126] [127] [128] [129]
Overfull \hbox (5.7678pt too wide) in paragraph at lines 13500--13502
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 Suc$\OML/cmm/m/it/10 :$\O
T1/cmr/m/it/10 hyps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$$[$\
OT1/cmr/m/it/10 OF v n[]ok$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 sym-met-ric$\OT
1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 pseudo[]divmod[]main$\OML/cmm/m/it/10 :$\OT1/c
mr/m/it/10 simps Let[]def[] 
[130]
Overfull \hbox (8.8534pt too wide) in paragraph at lines 13637--13639
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]mod[]impl$\OT1/cmr/m/n/10 [
$\OT1/cmr/m/it/10 code$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 pseudo[]mod f g $
\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 poly[]of[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 pseudo[]mod[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 coeffs
[131] [132] [133]
Overfull \hbox (37.10872pt too wide) in paragraph at lines 13863--13865
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list[]1$\OT1/
cmr/m/n/10 :$ \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list 1 $\OT1/cmr/m/n/10 =$
 \OT1/cmr/m/it/10 divmod[]poly[]one[]main[]list[] 

Overfull \hbox (93.00832pt too wide) in paragraph at lines 13945--13947
[][]\OT1/cmr/bx/n/10 lemmas \OT1/cmr/m/it/10 pdivmod[]via[]divmod[]list $\OT1/c
mr/m/n/10 =$ \OT1/cmr/m/it/10 pdivmod[]via[]pseudo[]divmod[]list$\OT1/cmr/m/n/1
0 [$\OT1/cmr/m/it/10 unfolded pseudo[]divmod[]main[]list[]1$\OT1/cmr/m/n/10 ]$[
] 
[134]
Overfull \hbox (63.45209pt too wide) in paragraph at lines 13948--13950
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 mod[]poly[]one[]main[]list$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 snd $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 divmod[]pol
y[]one[]main[]list q r d n$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 mod[]poly[]o
ne[]main[]list
[135] [136] [137]
Overfull \hbox (2.32649pt too wide) in paragraph at lines 14301--14305
[][]    \OT1/cmr/bx/n/10 then ob-tain \OT1/cmr/m/it/10 a$ [] $ b$ [] $ \OT1/cmr
/bx/n/10 where \OT1/cmr/m/it/10 ab$ [] $$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 a 
$\OT1/cmr/m/n/10 =$ $[$$:$\OT1/cmr/m/it/10 a$ [] $$\OT1/cmr/m/n/10 :$$]$ \OT1/c
mr/m/it/10 b $\OT1/cmr/m/n/10 =$ $[$$:$\OT1/cmr/m/it/10 b$ [] $$\OT1/cmr/m/n/10
 :$$]$ \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/c
mr/m/n/10 !$$:$ \OT1/cmr/m/it/10 degree[]eq[]zeroE$\OT1/cmr/m/n/10 )$[] 
[138] [139]
Overfull \hbox (14.12436pt too wide) in paragraph at lines 14546--14550
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 A \OT1/cmr/bx/n/10 and \OT1/cmr/
m/it/10 this \OT1/cmr/bx/n/10 have $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/it/10 c$\OT
1/cmr/m/n/10 :$$]$ \OT1/cmr/m/it/10 dvd $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/it/10 
a$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 _$ $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/i
t/10 c$\OT1/cmr/m/n/10 :$$]$ \OT1/cmr/m/it/10 dvd $\OT1/cmr/m/n/10 [$$:$\OT1/cm
r/m/it/10 b$\OT1/cmr/m/n/10 :$$]$ \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/c
mr/m/it/10 rule prime[]elem[]dvd[]multD$\OT1/cmr/m/n/10 )$[] 
[140] [141] [142] [143] [144]) (./Pochhammer_Polynomials.tex [145]
Overfull \hbox (39.72092pt too wide) in paragraph at lines 105--107
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pochhammer[]poly[]Suc$\OT1/cmr/m/n/
10 :$ \OT1/cmr/m/it/10 pochhammer[]poly $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Suc
 n$\OT1/cmr/m/n/10 )$ $=$ $[$$:$\OT1/cmr/m/it/10 of[]nat n$\OML/cmm/m/it/10 ;$\
OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10
 pochhammer[]poly

Overfull \hbox (40.14108pt too wide) in paragraph at lines 143--151
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases n$\OT1/cmr/
m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 pochhammer[]poly[]altdef poly[]prod add[]ac lessThan[]Suc[]atMost
) (./Linear_Recurrences_Misc.tex) (./Partial_Fraction_Decomposition.tex)
(./Factorizations.tex [146]
Overfull \hbox (5.12407pt too wide) in paragraph at lines 72--74
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 interp[]factorization[]def interp[]alt[]factoriza
tion[]def case[]prod[]unfold[] 

Overfull \hbox (5.12407pt too wide) in paragraph at lines 116--118
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 interp[]factorization[]def interp[]alt[]factoriza
tion[]def case[]prod[]unfold[] 
[147]
Overfull \hbox (16.71938pt too wide) in paragraph at lines 244--248
[][]  \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 p $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 interp[]factorization fc-trs 
\OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/1
0 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (16.22148pt too wide) in paragraph at lines 263--267
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 interp[]factorization fc-trs $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 
\OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/1
0 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def$\OT1/cmr/m/n/10 )$[] 
[148] [149]
Overfull \hbox (15.7888pt too wide) in paragraph at lines 465--468
[][]    \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 dis-tinct assms \OT1/cmr/bx/n/
10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro sum[]list[]cong$\OT1/cmr/m/n/10
 )$ $($\OT1/cmr/m/it/10 force simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 distinct
[]map inj[]on[]def$\OT1/cmr/m/n/10 )$$+$[] 

Overfull \hbox (15.70007pt too wide) in paragraph at lines 510--512
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro exI$\OT1/
cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 0$\OML/
cmm/m/it/10 ;$ $\OT1/cmr/m/n/10 [$$]$$)$$]$$)$ $($\OT1/cmr/m/it/10 auto simp$\O
T1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def interp[]factorizat
ion[]def$\OT1/cmr/m/n/10 )$[] 
[150]) (./Linear_Recurrences_Common.tex
Overfull \hbox (2.17294pt too wide) in paragraph at lines 6--6
[]\OT1/cmr/bx/n/14.4 Material com-mon to ho-moge-nous and in-ho-moge-
[151]) (./Eulerian_Polynomials.tex [152]
Overfull \hbox (5.86856pt too wide) in paragraph at lines 78--80
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 p fps[]deriv[]power algebra[]simps fps[]const[]ne
g $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/i
t/10 fps[]of[]nat
[153]
Overfull \hbox (6.71323pt too wide) in paragraph at lines 177--178
[][]  \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 fps[]monom[]poly c k $\OT1/cmr/m/
n/10 =$ $($\OT1/cmr/m/it/10 if k $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 then 1 
else pcom-pose $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pCons 0 $\OT1/cmr/m/n/10 ($\
OT1/cmr/m/it/10 eulerian[]poly
[154]
Overfull \hbox (21.73657pt too wide) in paragraph at lines 301--303
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 fps[]compose[]power $\OT1/cmr/m/n/10 [$\OT1/cmr/m
/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 fps[]compose[]sub[]distrib
 del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 power[]Suc$\OT1/cmr/m/n/10 )$[] 
))
No file root.bbl.
[155] (./root.aux)

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

 )
(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/cmr8.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmsy5.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmti12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbol
s/msam10.pfb>
Output written on root.pdf (155 pages, 535158 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/amsfonts/amsfonts.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (./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/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (./root.toc [1{/var/
lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (2.68887pt too wide) in paragraph at lines 48--48
 [][] [][][]\OT1/cmr/m/n/10.95 Improved Code-Equations for Poly-no-mial (Pseudo
) Di- 
[2]) [3] (./session.tex (./RatFPS.tex) (./Stirling.tex [4] [5] [6] [7] [8]
[9]) (./Factorial_Ring.tex [10] [11] [12]
Overfull \hbox (9.44902pt too wide) in paragraph at lines 455--469
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 unit[]imp[]no[]irreducible[]divi
sors$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF assms$\OT1/cmr/m/n/10 ($\OT1/cmr/m/i
t/10 1$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 prime[]elem[]imp[]irreducible$\OT1/c
mr/m/n/10 [$\OT1/cmr/m/it/10 OF
[13] [14]
Overfull \hbox (26.81523pt too wide) in paragraph at lines 836--841
[][]  \OT1/cmr/bx/n/10 more-over from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 h
ave $\OMS/cmsy/m/n/10 :$\OT1/cmr/m/it/10 is[]unit p \OT1/cmr/bx/n/10 by $\OT1/c
mr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime
[]elem[]def is[]unit[]power[]iff$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (10.79758pt too wide) in paragraph at lines 908--921
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cm
r/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]def mult$\OML/cmm/m/it/10 :$\OT1/cmr/
m/it/10 commute$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of a$\OT1/cmr/m/n/10 ]$ \OT1
/cmr/m/it/10 is[]unit[]mult[]iff mult[]unit[]dvd[]iff$\OT1/cmr/m/n/10 )$[] 
[15]
Overfull \hbox (12.0489pt too wide) in paragraph at lines 976--978
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis dvd[]mu
lt[]right dvd[]times[]left[]cancel[]iff mult$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/1
0 left[]commute mult[]zero[]left$\OT1/cmr/m/n/10 )$[] 
[16]
Overfull \hbox (5.12607pt too wide) in paragraph at lines 1132--1146
[][]  \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 n$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 a
uto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]not[]unit prime[]elem
[]dvd[]multD$\OT1/cmr/m/n/10 )$[] 
[17] [18] [19]
Overfull \hbox (11.69632pt too wide) in paragraph at lines 1788--1792
[][]  \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 ir-re-ducible q \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 prime[]elem[]imp[]irreducible 
prime[]def$\OT1/cmr/m/n/10 )$[] 
[20]
Overfull \hbox (30.63289pt too wide) in paragraph at lines 1943--1957
[][]  \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 in-tro$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 p
rod[]mset[]subset[]imp[]dvd prod[]mset[]primes[]dvd[]imp[]subset$\OT1/cmr/m/n/1
0 )$[] 
[21]
Overfull \hbox (11.4095pt too wide) in paragraph at lines 2017--2019
[][]    \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 A1[]def A2[]def Mul-ti-set$\OML/cmm/m/it/10 :$\O
T1/cmr/m/it/10 subset[]eq[]diff[]conv Mul-ti-set$\OML/cmm/m/it/10 :$\OT1/cmr/m/
it/10 union[]commute$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (1.77489pt too wide) in paragraph at lines 2032--2034
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst $\OT1/cmr
/m/n/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 1 2$\OT1/
cmr/m/n/10 )$ \OT1/cmr/m/it/10 is[]unit[]prod[]mset[]primes[]iff$\OT1/cmr/m/n/1
0 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 Mul-ti-s
et$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 in[]diffD$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (1.20242pt too wide) in paragraph at lines 2076--2080
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 x \OT1/cmr/bx/n/10 have \OT1/cmr
/m/it/10 x ^ n dvd prod[]mset A ^ n \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1
/cmr/m/it/10 intro dvd[]power[]same dvd[]prod[]mset$\OT1/cmr/m/n/10 )$[] 
[22] [23]
Overfull \hbox (11.16814pt too wide) in paragraph at lines 2329--2329
[]\OT1/cmr/bx/n/12 Factorial semir-ings: al-ge-braic struc-tures with unique pr
ime

Overfull \hbox (6.13147pt too wide) in paragraph at lines 2376--2380
[][]      \OT1/cmr/bx/n/10 with []$\OMS/cmsy/m/n/10 :$\OT1/cmr/m/it/10 is[]unit
 a[] less$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 prems \OT1/cmr/bx/n/10 have \OT1/
cmr/m/it/10 ir-re-ducible a \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/i
t/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 irreducible[]altdef$\OT1/cmr
/m/n/10 )$[] 
[24]
Overfull \hbox (5.4238pt too wide) in paragraph at lines 2490--2494
[][]      \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 A B \OT1/cmr/bx/n/10 show \OT1
/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 i
ntro exI$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] A $\OT1/cmr/m/n/10 +$ \OT1/cm
r/m/it/10 B$\OT1/cmr/m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10
 :$ \OT1/cmr/m/it/10 c normalize[]mult$\OT1/cmr/m/n/10 )$[] 
[25]
Overfull \hbox (7.38255pt too wide) in paragraph at lines 2623--2625
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 dvd prod[]mset[]primes[]irreduci
ble[]imp[]prime$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of A B C$\OML/cmm/m/it/10 ;$
 \OT1/cmr/m/it/10 OF this ABC$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OML/cmm/m/i
t/10 ;$\OT1/cmr/m/it/10 3$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 5$\OT1/cmr/m/n/10
 )$$]$
[26]
Overfull \hbox (6.55193pt too wide) in paragraph at lines 2724--2729
[][]    \OT1/cmr/bx/n/10 fi-nally show \OT1/cmr/m/it/10 p $\OMS/cmsy/m/n/10 2$$
\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 A \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 
p A \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst $\OT1/cmr/m/n
/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 prime[]dvd[]prod
[]mset[]primes[]iff$\OT1/cmr/m/n/10 )$[] 
[27] [28]
Overfull \hbox (35.03365pt too wide) in paragraph at lines 3242--3256
[][]  \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 subst prime[]elem[]multiplicity[]eq[]zero[]iff$\O
T1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it
/10 primes[]dvd[]imp[]eq$\OT1/cmr/m/n/10 )$[] 
[29]
Overfull \hbox (31.33105pt too wide) in paragraph at lines 3368--3373
[][]    \OT1/cmr/bx/n/10 more-over from \OT1/cmr/m/it/10 assms$\OT1/cmr/m/n/10 
($\OT1/cmr/m/it/10 2$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 xp \OT1/cmr/bx/n/10 ha
ve \OT1/cmr/m/it/10 mul-ti-plic-ity p x $\OML/cmm/m/it/10 <$ \OT1/cmr/m/it/10 S
uc n \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro multiplicity
[]lessI$\OT1/cmr/m/n/10 )$[] 
[30] [31]
Overfull \hbox (42.299pt too wide) in paragraph at lines 3630--3632
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst mult$\OML
/cmm/m/it/10 :$\OT1/cmr/m/it/10 commute$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 
simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 mult[]unit[]dvd[]iff power[]mult[]
distrib is[]unit[]power[]iff$\OT1/cmr/m/n/10 )$[] 
[32]
Overfull \hbox (2.52225pt too wide) in paragraph at lines 3909--3911
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro multiplic
ity[]geI $\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 :$
 \OT1/cmr/m/it/10 dvd[]trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF multiplicity
[]dvd$ [] $ assms$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$$]$$)$
[] 
[33] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (4.71416pt too wide) in paragraph at lines 4108--4113
[][]      \OT1/cmr/bx/n/10 also from \OT1/cmr/m/it/10 x p \OT1/cmr/bx/n/10 have
 $[] $ $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 $\OMS/cmsy/m/n/10  []!$ $:$\OT1/c
mr/m/it/10 p dvd x \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 multiplicity[]eq[]zero[]iff$\OT1/cmr/m
/n/10 )$[] 
[34]
Overfull \hbox (0.98625pt too wide) in paragraph at lines 4243--4245
[][]  \OT1/cmr/bx/n/10 thus \OT1/cmr/m/it/10 count $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 p $\OMS/cmsy/m
/n/10 ^^C$ \OT1/cmr/m/it/10 x$\OT1/cmr/m/n/10 )$$)$ \OT1/cmr/m/it/10 q $\OT1/cm
r/m/n/10 =$ \OT1/cmr/m/it/10 count $\OT1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 f$$\OT1
/cmr/m/n/10 #$\OT1/cmr/m/it/10 p$\OT1/cmr/m/n/10 #$$\OMS/cmsy/m/n/10 g$ $\OT1/c
mr/m/n/10 +$ \OT1/cmr/m/it/10 prime[]factorization
[35] [36]
Overfull \hbox (15.81303pt too wide) in paragraph at lines 4481--4483
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\
OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 mult[]ac prime[]factorization[]times[]prime 
Mul-ti-set$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 union[]commute$\OT1/cmr/m/n/10 )
$[] 

Overfull \hbox (40.95099pt too wide) in paragraph at lines 4532--4536
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 show \OT1/c
mr/m/it/10 nor-mal-ize x $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 nor-mal-ize y \OT
1/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 prod[]mset[]prime[]factorization$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (44.55727pt too wide) in paragraph at lines 4567--4569
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule prime[]fac
torization[]prod[]mset[]primes$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all
 add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]prime[]factors[]imp[]prime$\OT1/cm
r/m/n/10 )$[] 

Overfull \hbox (20.85785pt too wide) in paragraph at lines 4569--4572
[][]  \OT1/cmr/bx/n/10 also have \OT1/cmr/m/it/10 prime[]factorization $\OT1/cm
r/m/n/10 ($\OT1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prim
e[]factorization x $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 prime[]factorization

Overfull \hbox (33.42188pt too wide) in paragraph at lines 4573--4575
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule prime[]fac
torization[]prod[]mset[]primes$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp
$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]prime[]factors[]imp[]prime$\OT1/cmr/m/
n/10 )$[] 
[37]
Overfull \hbox (25.28094pt too wide) in paragraph at lines 4719--4720
[][]                   $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]multiplicity[]prod[]mset[]distrib su
m[]unfold[]sum[]mset[] 
[38]
Overfull \hbox (16.5629pt too wide) in paragraph at lines 4744--4757
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst prime[]elem
[]multiplicity[]power[]distrib$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp
$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]multiplicity[]other$\OT1/cmr/m/n/10
 )$[] 

Overfull \hbox (50.5364pt too wide) in paragraph at lines 4771--4777
[][]     $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \
OT1/cmr/m/it/10 prime[]factorization[]mult prime[]factorization[]prime Mul-ti-s
et$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 union[]commute$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (22.83113pt too wide) in paragraph at lines 4810--4812
[][]  \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 x dvd y $\OMS/cmsy/m/n/10  []!$ \O
T1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorizat
ion x$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 dvd prod[]mset $\OT1/cmr/m/n/10 ($\OT
1/cmr/m/it/10 prime[]factorization

Overfull \hbox (6.21616pt too wide) in paragraph at lines 4855--4856
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 a div b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 prime[]factorization
[39]
Overfull \hbox (12.16023pt too wide) in paragraph at lines 4951--4952
[][]      $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ 
\OT1/cmr/m/it/10 assms count[]prime[]factorization[]prime in[]prime[]factors[]i
mp[]prime$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (24.46587pt too wide) in paragraph at lines 4993--4996
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 A[]def \OT1/cmr/bx/n/10 b
y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst mul-ti-set$\OML/cmm/m/it/10 :$\OT1/
cmr/m/it/10 Abs[]multiset[]inverse$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[
]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 multiset[]def$\OT1/cmr/m/n/10 )$[]
 

Overfull \hbox (1.20328pt too wide) in paragraph at lines 5005--5009
[][]  \OT1/cmr/bx/n/10 also have $[] $ $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 pro
d[]mset A \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 prod[]mset[]multiplicity S[]eq set[]mset[]A

Overfull \hbox (29.18195pt too wide) in paragraph at lines 5026--5029
[][]  \OT1/cmr/bx/n/10 also have \OT1/cmr/m/it/10 prime[]factorization $\OT1/cm
r/m/n/10 ($\OT1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prim
e[]factorization n$\OT1/cmr/m/n/10 )$$)$ $=$ \OT1/cmr/m/it/10 prime[]factorizat
ion
[40]
Overfull \hbox (56.44945pt too wide) in paragraph at lines 5063--5065
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro image[]
mset[]cong$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ 
\OT1/cmr/m/it/10 set[]mset[]A multiplicity[]self prime[]multiplicity[]other$\OT
1/cmr/m/n/10 )$[] 

Overfull \hbox (5.04556pt too wide) in paragraph at lines 5143--5147
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms False \OT1/cmr/bx/n/10 show 
\OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/
10 subst $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/
it/10 prime[]factorization[]subset[]iff[]dvd$\OT1/cmr/m/n/10 )$[] 
[41] [42]
Overfull \hbox (1.69742pt too wide) in paragraph at lines 5361--5362
[][]          \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a 
$\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization

Overfull \hbox (1.69742pt too wide) in paragraph at lines 5397--5398
[][]          \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a 
$\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization
[43]
Overfull \hbox (4.25296pt too wide) in paragraph at lines 5631--5632
[][]           \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cm
r/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a
 $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization
[44]
Overfull \hbox (3.08865pt too wide) in paragraph at lines 5772--5775
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Gcd[]factor
ial A$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 Inf $\OT1/cmr/m/n/10 ($\OT1/cmr/m
/it/10 prime[]factorization
[45] [46]
Overfull \hbox (14.46059pt too wide) in paragraph at lines 6031--6032
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 gcd a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization

Overfull \hbox (15.99394pt too wide) in paragraph at lines 6051--6052
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 lcm a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[47]
Overfull \hbox (43.35431pt too wide) in paragraph at lines 6080--6087
[][]  \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 prime[]factorization[]Gcd[]factorial Gcd[]eq[]Gcd[]
factorial Gcd[]factorial[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (49.76532pt too wide) in paragraph at lines 6102--6109
[][]  \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 prime[]factorization[]Lcm[]factorial Lcm[]eq[]Lcm[]
factorial Lcm[]factorial[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 
[48]
Overfull \hbox (55.76273pt too wide) in paragraph at lines 6263--6265
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 count[]prime[]factorization[]prime $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 prime[]fact
orization[]gcd[]factorial$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (57.29608pt too wide) in paragraph at lines 6276--6278
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 count[]prime[]factorization[]prime $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 prime[]fact
orization[]lcm[]factorial$\OT1/cmr/m/n/10 )$[] 
[49]) (./Polynomial.tex [50]

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


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


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


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


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


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

[51] [52] [53] [54] [55] [56] [57] [58]
Overfull \hbox (5.01166pt too wide) in paragraph at lines 1745--1747
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 poly[]of[]list[]impl $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 code ab-stract$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 co-
effs $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 poly[]of[]list as$\OT1/cmr/m/n/10 )$ $
=$ \OT1/cmr/m/it/10 strip[]while $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 HOL$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 eq
[59] [60] [61] [62] [63]
Overfull \hbox (7.42665pt too wide) in paragraph at lines 2755--2768
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis coeff[]add 
coeff[]eq[]0 monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 add$\OML/cm
m/m/it/10 :$\OT1/cmr/m/it/10 left[]neutral degree[]add[]eq[]right$\OT1/cmr/m/n/
10 )$[] 
[64] [65]
Overfull \hbox (38.39879pt too wide) in paragraph at lines 3009--3011
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule coeffs[]eq
I$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 nth[]default[]map[]eq nth[]default[]coeffs[]eq no[]trailing[]map
[66] [67]
Overfull \hbox (45.5543pt too wide) in paragraph at lines 3596--3598
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule coeffs[]eq
I$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp add$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 no[]trailing[]map nth[]default[]map[]eq nth[]default[]coeffs[]eq
[68] [69]
Overfull \hbox (32.25041pt too wide) in paragraph at lines 3854--3856
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]0$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$ 
\OT1/cmr/m/it/10 semiring[]no[]zero[]divisors[] 
[70] [71]
Overfull \hbox (49.62807pt too wide) in paragraph at lines 4247--4263
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]1$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]1[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 
)$ \OT1/cmr/m/it/10 semiring[]1[]no[]zero[]divisors
[72] [73]
Overfull \hbox (23.10243pt too wide) in paragraph at lines 4776--4778
[][]        \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 assms length[]coeffs nth[]default[]coeffs[]e
q $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/i
t/10 nth[]default[]def$\OT1/cmr/m/n/10 )$[] 
[74]
Overfull \hbox (5.96727pt too wide) in paragraph at lines 4824--4837
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro poly[]eqI$\
OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr
/m/it/10 assms coeff[]map[]poly coeff[]pCons split$\OT1/cmr/m/n/10 :$ \OT1/cmr/
m/it/10 nat$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 splits$\OT1/cmr/m/n/10 )$[] 
[75] [76] [77]
Overfull \hbox (22.59839pt too wide) in paragraph at lines 5527--5540
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule order[]antis
ym $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le le[]degree$\OT1/cmr/
m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 c
oeff[]mult[]degree[]sum$\OT1/cmr/m/n/10 )$[] 
[78] [79] [80] [81]
Overfull \hbox (9.43272pt too wide) in paragraph at lines 6157--6158
[][]  \OT1/cmr/m/it/10 synthetic[]divmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pC
ons a p$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 c $\OT1/cmr/m/n/10 =$ $($$\OML/cmm/
m/it/10 ^^U$$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 q$\OML/cmm/m/it/10 ;$ \OT1/cmr/
m/it/10 r$\OT1/cmr/m/n/10 )$$\OML/cmm/m/it/10 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/
it/10 pCons r q$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1
/cmr/m/it/10 c $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 r$\OT1/cmr/m/n/10 )$$)$ 
$($\OT1/cmr/m/it/10 synthetic[]divmod
[82] [83] [84] [85]
Overfull \hbox (12.44328pt too wide) in paragraph at lines 6791--6793
[][]   \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis order[
]2 not[]gr0 poly[]eq[]0[]iff[]dvd power[]0 power[]Suc[]0 power[]one[]right$\OT1
/cmr/m/n/10 )$[] 
[86] [87]
Overfull \hbox (57.51828pt too wide) in paragraph at lines 7009--7011
[][]    \OT1/cmr/bx/n/10 by $\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 hide[
]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 One[]nat[]def add[]Suc[]right monoid[
]add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr
/m/it/10 right[]neutral[] 

Overfull \hbox (4.7849pt too wide) in paragraph at lines 7011--7012
[][]      \OT1/cmr/m/it/10 one[]neq[]zero order[]mult pCons[]eq[]0[]iff power[]
add power[]eq[]0[]iff power[]one[]right$\OT1/cmr/m/n/10 )$[] 
[88] [89] [90]
Overfull \hbox (23.32683pt too wide) in paragraph at lines 7630--7643
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct p ar-bi-tr
ary$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 q$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/1
0 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]add pcompose[]smu
lt pcompose[]pCons
[91]
Overfull \hbox (24.07547pt too wide) in paragraph at lines 7649--7662
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct p ar-bi-tr
ary$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 q$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/1
0 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]pCons pcompose[]a
dd pcompose[]mult$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (3.83954pt too wide) in paragraph at lines 7704--7717
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct A rule$\OT
1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 infinite[]finite[]induct$\OT1/cmr/m/n/10 )$ $(
$\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]1
 pcompose[]mult$\OT1/cmr/m/n/10 )$[] 
[92] [93] [94] [95] [96]
Overfull \hbox (26.78821pt too wide) in paragraph at lines 8578--8591
[][]  \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 degree[]eq[]length[]coeffs coeffs[]reflect[]poly le
ngth[]dropWhile[]le diff[]le[]mono$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (7.1392pt too wide) in paragraph at lines 8614--8627
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases p rule$\OT1
/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pCons[]cases$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/i
t/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 reflect[]poly[]pCons degree[]
eq[]length[]coeffs$\OT1/cmr/m/n/10 )$[] 
[97] [98] [99] [100] [101] [102]
Overfull \hbox (43.11435pt too wide) in paragraph at lines 9486--9488
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 DERIV[]add[]const$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 DE-RIV f x $\OT1/cmr/m/n/10 :$$\OML/cmm/m/it/10 >$ \OT1/cmr/
m/it/10 D $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 DE-RIV $\OT1
/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 x$\OML/cmm/m/it/10 :$ \OT1
/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 f x $\OT1/cmr/m/n/10 :$$:$ 
$ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]fi
eld$\OT1/cmr/m/n/10 )$
[103] [104] [105]
Overfull \hbox (5.12115pt too wide) in paragraph at lines 9897--9899
[][]      \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\O
MS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 nd dvd[]mult[]cancel[]right power[]not[]ze
ro pCons[]eq[]0[]iff power[]Suc
[106] [107] [108] [109] [110]
Overfull \hbox (43.09401pt too wide) in paragraph at lines 10585--10588
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dr b[]def \OT1/cmr/bx/n/1
0 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule or-der$\OML/cmm/m/it/10 :$\OT1/cm
r/m/it/10 trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le$\OT1/cmr
/m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 degree[]monom[]le$\OT1/cmr/m/n/10 )$[] 
[111] [112] [113] [114] [115]
Overfull \hbox (18.54pt too wide) in paragraph at lines 11313--11316
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dr \OT1/cmr/bx/n/10 by $\
OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule or-der$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/
10 trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le$\OT1/cmr/m/n/10
 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 degree
[]monom[]le$\OT1/cmr/m/n/10 )$[] 
[116] [117] [118] [119]
Overfull \hbox (29.60196pt too wide) in paragraph at lines 11712--11714
[][]\OT1/cmr/bx/n/10 instantiation \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$
 $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 semidom[]divide[]unit[]factor$\OML/cmm
/m/it/10 ;$\OT1/cmr/m/it/10 idom[]divide$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$
 \OT1/cmr/m/it/10 normalization[]semidom[] 
[120] [121] [122] [123] [124] [125] [126] [127] [128] [129] [130] [131]
Overfull \hbox (5.7678pt too wide) in paragraph at lines 13500--13502
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 Suc$\OML/cmm/m/it/10 :$\O
T1/cmr/m/it/10 hyps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$$[$\
OT1/cmr/m/it/10 OF v n[]ok$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 sym-met-ric$\OT
1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 pseudo[]divmod[]main$\OML/cmm/m/it/10 :$\OT1/c
mr/m/it/10 simps Let[]def[] 
[132]
Overfull \hbox (8.8534pt too wide) in paragraph at lines 13637--13639
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]mod[]impl$\OT1/cmr/m/n/10 [
$\OT1/cmr/m/it/10 code$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 pseudo[]mod f g $
\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 poly[]of[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 pseudo[]mod[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 coeffs
[133] [134] [135]
Overfull \hbox (37.10872pt too wide) in paragraph at lines 13863--13865
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list[]1$\OT1/
cmr/m/n/10 :$ \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list 1 $\OT1/cmr/m/n/10 =$
 \OT1/cmr/m/it/10 divmod[]poly[]one[]main[]list[] 

Overfull \hbox (93.00832pt too wide) in paragraph at lines 13945--13947
[][]\OT1/cmr/bx/n/10 lemmas \OT1/cmr/m/it/10 pdivmod[]via[]divmod[]list $\OT1/c
mr/m/n/10 =$ \OT1/cmr/m/it/10 pdivmod[]via[]pseudo[]divmod[]list$\OT1/cmr/m/n/1
0 [$\OT1/cmr/m/it/10 unfolded pseudo[]divmod[]main[]list[]1$\OT1/cmr/m/n/10 ]$[
] 
[136]
Overfull \hbox (63.45209pt too wide) in paragraph at lines 13948--13950
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 mod[]poly[]one[]main[]list$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 snd $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 divmod[]pol
y[]one[]main[]list q r d n$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 mod[]poly[]o
ne[]main[]list
[137] [138] [139]
Overfull \hbox (2.32649pt too wide) in paragraph at lines 14301--14305
[][]    \OT1/cmr/bx/n/10 then ob-tain \OT1/cmr/m/it/10 a$ [] $ b$ [] $ \OT1/cmr
/bx/n/10 where \OT1/cmr/m/it/10 ab$ [] $$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 a 
$\OT1/cmr/m/n/10 =$ $[$$:$\OT1/cmr/m/it/10 a$ [] $$\OT1/cmr/m/n/10 :$$]$ \OT1/c
mr/m/it/10 b $\OT1/cmr/m/n/10 =$ $[$$:$\OT1/cmr/m/it/10 b$ [] $$\OT1/cmr/m/n/10
 :$$]$ \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/c
mr/m/n/10 !$$:$ \OT1/cmr/m/it/10 degree[]eq[]zeroE$\OT1/cmr/m/n/10 )$[] 
[140] [141]
Overfull \hbox (14.12436pt too wide) in paragraph at lines 14546--14550
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 A \OT1/cmr/bx/n/10 and \OT1/cmr/
m/it/10 this \OT1/cmr/bx/n/10 have $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/it/10 c$\OT
1/cmr/m/n/10 :$$]$ \OT1/cmr/m/it/10 dvd $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/it/10 
a$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 _$ $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/i
t/10 c$\OT1/cmr/m/n/10 :$$]$ \OT1/cmr/m/it/10 dvd $\OT1/cmr/m/n/10 [$$:$\OT1/cm
r/m/it/10 b$\OT1/cmr/m/n/10 :$$]$ \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/c
mr/m/it/10 rule prime[]elem[]dvd[]multD$\OT1/cmr/m/n/10 )$[] 
[142] [143] [144] [145] [146]) (./Pochhammer_Polynomials.tex [147]
Overfull \hbox (39.72092pt too wide) in paragraph at lines 105--107
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pochhammer[]poly[]Suc$\OT1/cmr/m/n/
10 :$ \OT1/cmr/m/it/10 pochhammer[]poly $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Suc
 n$\OT1/cmr/m/n/10 )$ $=$ $[$$:$\OT1/cmr/m/it/10 of[]nat n$\OML/cmm/m/it/10 ;$\
OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10
 pochhammer[]poly

Overfull \hbox (40.14108pt too wide) in paragraph at lines 143--151
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases n$\OT1/cmr/
m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 pochhammer[]poly[]altdef poly[]prod add[]ac lessThan[]Suc[]atMost
) (./Linear_Recurrences_Misc.tex) (./Partial_Fraction_Decomposition.tex)
(./Factorizations.tex [148]
Overfull \hbox (5.12407pt too wide) in paragraph at lines 72--74
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 interp[]factorization[]def interp[]alt[]factoriza
tion[]def case[]prod[]unfold[] 

Overfull \hbox (5.12407pt too wide) in paragraph at lines 116--118
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 interp[]factorization[]def interp[]alt[]factoriza
tion[]def case[]prod[]unfold[] 
[149]
Overfull \hbox (16.71938pt too wide) in paragraph at lines 244--248
[][]  \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 p $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 interp[]factorization fc-trs 
\OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/1
0 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (16.22148pt too wide) in paragraph at lines 263--267
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 interp[]factorization fc-trs $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 
\OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/1
0 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def$\OT1/cmr/m/n/10 )$[] 
[150] [151]
Overfull \hbox (15.7888pt too wide) in paragraph at lines 465--468
[][]    \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 dis-tinct assms \OT1/cmr/bx/n/
10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro sum[]list[]cong$\OT1/cmr/m/n/10
 )$ $($\OT1/cmr/m/it/10 force simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 distinct
[]map inj[]on[]def$\OT1/cmr/m/n/10 )$$+$[] 

Overfull \hbox (15.70007pt too wide) in paragraph at lines 510--512
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro exI$\OT1/
cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 0$\OML/
cmm/m/it/10 ;$ $\OT1/cmr/m/n/10 [$$]$$)$$]$$)$ $($\OT1/cmr/m/it/10 auto simp$\O
T1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def interp[]factorizat
ion[]def$\OT1/cmr/m/n/10 )$[] 
[152]) (./Linear_Recurrences_Common.tex
Overfull \hbox (2.17294pt too wide) in paragraph at lines 6--6
[]\OT1/cmr/bx/n/14.4 Material com-mon to ho-moge-nous and in-ho-moge-
[153]) (./Eulerian_Polynomials.tex [154]
Overfull \hbox (5.86856pt too wide) in paragraph at lines 78--80
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 p fps[]deriv[]power algebra[]simps fps[]const[]ne
g $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/i
t/10 fps[]of[]nat
[155]
Overfull \hbox (6.71323pt too wide) in paragraph at lines 177--178
[][]  \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 fps[]monom[]poly c k $\OT1/cmr/m/
n/10 =$ $($\OT1/cmr/m/it/10 if k $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 then 1 
else pcom-pose $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pCons 0 $\OT1/cmr/m/n/10 ($\
OT1/cmr/m/it/10 eulerian[]poly
[156]
Overfull \hbox (21.73657pt too wide) in paragraph at lines 301--303
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 fps[]compose[]power $\OT1/cmr/m/n/10 [$\OT1/cmr/m
/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 fps[]compose[]sub[]distrib
 del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 power[]Suc$\OT1/cmr/m/n/10 )$[] 
))
No file root.bbl.
[157] (./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/cmr8.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmsy5.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmti12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbol
s/msam10.pfb>
Output written on root.pdf (157 pages, 544247 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/amsfonts/amsfonts.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (./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/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (./root.toc [1{/var/
lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
Overfull \hbox (2.68887pt too wide) in paragraph at lines 48--48
 [][] [][][]\OT1/cmr/m/n/10.95 Improved Code-Equations for Poly-no-mial (Pseudo
) Di- 
[2]) [3] (./session.tex (./RatFPS.tex) (./Stirling.tex [4] [5] [6] [7] [8]
[9]) (./Factorial_Ring.tex [10] [11] [12]
Overfull \hbox (9.44902pt too wide) in paragraph at lines 455--469
[][]  \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 unit[]imp[]no[]irreducible[]divi
sors$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF assms$\OT1/cmr/m/n/10 ($\OT1/cmr/m/i
t/10 1$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 prime[]elem[]imp[]irreducible$\OT1/c
mr/m/n/10 [$\OT1/cmr/m/it/10 OF
[13] [14]
Overfull \hbox (26.81523pt too wide) in paragraph at lines 836--841
[][]  \OT1/cmr/bx/n/10 more-over from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 h
ave $\OMS/cmsy/m/n/10 :$\OT1/cmr/m/it/10 is[]unit p \OT1/cmr/bx/n/10 by $\OT1/c
mr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime
[]elem[]def is[]unit[]power[]iff$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (10.79758pt too wide) in paragraph at lines 908--921
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp$\OT1/cm
r/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]def mult$\OML/cmm/m/it/10 :$\OT1/cmr/
m/it/10 commute$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of a$\OT1/cmr/m/n/10 ]$ \OT1
/cmr/m/it/10 is[]unit[]mult[]iff mult[]unit[]dvd[]iff$\OT1/cmr/m/n/10 )$[] 
[15]
Overfull \hbox (12.0489pt too wide) in paragraph at lines 976--978
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis dvd[]mu
lt[]right dvd[]times[]left[]cancel[]iff mult$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/1
0 left[]commute mult[]zero[]left$\OT1/cmr/m/n/10 )$[] 
[16]
Overfull \hbox (5.12607pt too wide) in paragraph at lines 1132--1146
[][]  \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 n$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 a
uto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]not[]unit prime[]elem
[]dvd[]multD$\OT1/cmr/m/n/10 )$[] 
[17] [18] [19]
Overfull \hbox (11.69632pt too wide) in paragraph at lines 1788--1792
[][]  \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 ir-re-ducible q \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 prime[]elem[]imp[]irreducible 
prime[]def$\OT1/cmr/m/n/10 )$[] 
[20]
Overfull \hbox (30.63289pt too wide) in paragraph at lines 1943--1957
[][]  \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 in-tro$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 p
rod[]mset[]subset[]imp[]dvd prod[]mset[]primes[]dvd[]imp[]subset$\OT1/cmr/m/n/1
0 )$[] 
[21]
Overfull \hbox (11.4095pt too wide) in paragraph at lines 2017--2019
[][]    \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 A1[]def A2[]def Mul-ti-set$\OML/cmm/m/it/10 :$\O
T1/cmr/m/it/10 subset[]eq[]diff[]conv Mul-ti-set$\OML/cmm/m/it/10 :$\OT1/cmr/m/
it/10 union[]commute$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (1.77489pt too wide) in paragraph at lines 2032--2034
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst $\OT1/cmr
/m/n/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 1 2$\OT1/
cmr/m/n/10 )$ \OT1/cmr/m/it/10 is[]unit[]prod[]mset[]primes[]iff$\OT1/cmr/m/n/1
0 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 Mul-ti-s
et$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 in[]diffD$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (1.20242pt too wide) in paragraph at lines 2076--2080
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 x \OT1/cmr/bx/n/10 have \OT1/cmr
/m/it/10 x ^ n dvd prod[]mset A ^ n \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1
/cmr/m/it/10 intro dvd[]power[]same dvd[]prod[]mset$\OT1/cmr/m/n/10 )$[] 
[22] [23]
Overfull \hbox (11.16814pt too wide) in paragraph at lines 2329--2329
[]\OT1/cmr/bx/n/12 Factorial semir-ings: al-ge-braic struc-tures with unique pr
ime

Overfull \hbox (6.13147pt too wide) in paragraph at lines 2376--2380
[][]      \OT1/cmr/bx/n/10 with []$\OMS/cmsy/m/n/10 :$\OT1/cmr/m/it/10 is[]unit
 a[] less$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 prems \OT1/cmr/bx/n/10 have \OT1/
cmr/m/it/10 ir-re-ducible a \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/i
t/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 irreducible[]altdef$\OT1/cmr
/m/n/10 )$[] 
[24]
Overfull \hbox (5.4238pt too wide) in paragraph at lines 2490--2494
[][]      \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 A B \OT1/cmr/bx/n/10 show \OT1
/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 i
ntro exI$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] A $\OT1/cmr/m/n/10 +$ \OT1/cm
r/m/it/10 B$\OT1/cmr/m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10
 :$ \OT1/cmr/m/it/10 c normalize[]mult$\OT1/cmr/m/n/10 )$[] 
[25]
Overfull \hbox (7.38255pt too wide) in paragraph at lines 2623--2625
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 dvd prod[]mset[]primes[]irreduci
ble[]imp[]prime$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 of A B C$\OML/cmm/m/it/10 ;$
 \OT1/cmr/m/it/10 OF this ABC$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OML/cmm/m/i
t/10 ;$\OT1/cmr/m/it/10 3$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 5$\OT1/cmr/m/n/10
 )$$]$
[26]
Overfull \hbox (6.55193pt too wide) in paragraph at lines 2724--2729
[][]    \OT1/cmr/bx/n/10 fi-nally show \OT1/cmr/m/it/10 p $\OMS/cmsy/m/n/10 2$$
\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 A \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 
p A \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst $\OT1/cmr/m/n
/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 prime[]dvd[]prod
[]mset[]primes[]iff$\OT1/cmr/m/n/10 )$[] 
[27] [28]
Overfull \hbox (35.03365pt too wide) in paragraph at lines 3242--3256
[][]  \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 subst prime[]elem[]multiplicity[]eq[]zero[]iff$\O
T1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto dest$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it
/10 primes[]dvd[]imp[]eq$\OT1/cmr/m/n/10 )$[] 
[29]
Overfull \hbox (31.33105pt too wide) in paragraph at lines 3368--3373
[][]    \OT1/cmr/bx/n/10 more-over from \OT1/cmr/m/it/10 assms$\OT1/cmr/m/n/10 
($\OT1/cmr/m/it/10 2$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 xp \OT1/cmr/bx/n/10 ha
ve \OT1/cmr/m/it/10 mul-ti-plic-ity p x $\OML/cmm/m/it/10 <$ \OT1/cmr/m/it/10 S
uc n \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro multiplicity
[]lessI$\OT1/cmr/m/n/10 )$[] 
[30] [31]
Overfull \hbox (42.299pt too wide) in paragraph at lines 3630--3632
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst mult$\OML
/cmm/m/it/10 :$\OT1/cmr/m/it/10 commute$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 
simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 mult[]unit[]dvd[]iff power[]mult[]
distrib is[]unit[]power[]iff$\OT1/cmr/m/n/10 )$[] 
[32]
Overfull \hbox (2.52225pt too wide) in paragraph at lines 3909--3911
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro multiplic
ity[]geI $\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto in-tro$\OT1/cmr/m/n/10 :$
 \OT1/cmr/m/it/10 dvd[]trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF multiplicity
[]dvd$ [] $ assms$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$$]$$)$
[] 
[33] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (4.71416pt too wide) in paragraph at lines 4108--4113
[][]      \OT1/cmr/bx/n/10 also from \OT1/cmr/m/it/10 x p \OT1/cmr/bx/n/10 have
 $[] $ $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 $\OMS/cmsy/m/n/10  []!$ $:$\OT1/c
mr/m/it/10 p dvd x \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 multiplicity[]eq[]zero[]iff$\OT1/cmr/m
/n/10 )$[] 
[34]
Overfull \hbox (0.98625pt too wide) in paragraph at lines 4243--4245
[][]  \OT1/cmr/bx/n/10 thus \OT1/cmr/m/it/10 count $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 p $\OMS/cmsy/m
/n/10 ^^C$ \OT1/cmr/m/it/10 x$\OT1/cmr/m/n/10 )$$)$ \OT1/cmr/m/it/10 q $\OT1/cm
r/m/n/10 =$ \OT1/cmr/m/it/10 count $\OT1/cmr/m/n/10 ($$\OMS/cmsy/m/n/10 f$$\OT1
/cmr/m/n/10 #$\OT1/cmr/m/it/10 p$\OT1/cmr/m/n/10 #$$\OMS/cmsy/m/n/10 g$ $\OT1/c
mr/m/n/10 +$ \OT1/cmr/m/it/10 prime[]factorization
[35] [36]
Overfull \hbox (15.81303pt too wide) in paragraph at lines 4481--4483
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\
OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 mult[]ac prime[]factorization[]times[]prime 
Mul-ti-set$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 union[]commute$\OT1/cmr/m/n/10 )
$[] 

Overfull \hbox (40.95099pt too wide) in paragraph at lines 4532--4536
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 show \OT1/c
mr/m/it/10 nor-mal-ize x $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 nor-mal-ize y \OT
1/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 prod[]mset[]prime[]factorization$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (44.55727pt too wide) in paragraph at lines 4567--4569
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule prime[]fac
torization[]prod[]mset[]primes$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all
 add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]prime[]factors[]imp[]prime$\OT1/cm
r/m/n/10 )$[] 

Overfull \hbox (20.85785pt too wide) in paragraph at lines 4569--4572
[][]  \OT1/cmr/bx/n/10 also have \OT1/cmr/m/it/10 prime[]factorization $\OT1/cm
r/m/n/10 ($\OT1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prim
e[]factorization x $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 prime[]factorization

Overfull \hbox (33.42188pt too wide) in paragraph at lines 4573--4575
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule prime[]fac
torization[]prod[]mset[]primes$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp
$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 in[]prime[]factors[]imp[]prime$\OT1/cmr/m/
n/10 )$[] 
[37]
Overfull \hbox (25.28094pt too wide) in paragraph at lines 4719--4720
[][]                   $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]elem[]multiplicity[]prod[]mset[]distrib su
m[]unfold[]sum[]mset[] 
[38]
Overfull \hbox (16.5629pt too wide) in paragraph at lines 4744--4757
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst prime[]elem
[]multiplicity[]power[]distrib$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp
$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 prime[]multiplicity[]other$\OT1/cmr/m/n/10
 )$[] 

Overfull \hbox (50.5364pt too wide) in paragraph at lines 4771--4777
[][]     $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \
OT1/cmr/m/it/10 prime[]factorization[]mult prime[]factorization[]prime Mul-ti-s
et$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 union[]commute$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (22.83113pt too wide) in paragraph at lines 4810--4812
[][]  \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 x dvd y $\OMS/cmsy/m/n/10  []!$ \O
T1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorizat
ion x$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 dvd prod[]mset $\OT1/cmr/m/n/10 ($\OT
1/cmr/m/it/10 prime[]factorization

Overfull \hbox (6.21616pt too wide) in paragraph at lines 4855--4856
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 a div b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 prime[]factorization
[39]
Overfull \hbox (12.16023pt too wide) in paragraph at lines 4951--4952
[][]      $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ 
\OT1/cmr/m/it/10 assms count[]prime[]factorization[]prime in[]prime[]factors[]i
mp[]prime$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (24.46587pt too wide) in paragraph at lines 4993--4996
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 A[]def \OT1/cmr/bx/n/10 b
y $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 subst mul-ti-set$\OML/cmm/m/it/10 :$\OT1/
cmr/m/it/10 Abs[]multiset[]inverse$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[
]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 multiset[]def$\OT1/cmr/m/n/10 )$[]
 

Overfull \hbox (1.20328pt too wide) in paragraph at lines 5005--5009
[][]  \OT1/cmr/bx/n/10 also have $[] $ $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 pro
d[]mset A \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 prod[]mset[]multiplicity S[]eq set[]mset[]A

Overfull \hbox (29.18195pt too wide) in paragraph at lines 5026--5029
[][]  \OT1/cmr/bx/n/10 also have \OT1/cmr/m/it/10 prime[]factorization $\OT1/cm
r/m/n/10 ($\OT1/cmr/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prim
e[]factorization n$\OT1/cmr/m/n/10 )$$)$ $=$ \OT1/cmr/m/it/10 prime[]factorizat
ion
[40]
Overfull \hbox (56.44945pt too wide) in paragraph at lines 5063--5065
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro image[]
mset[]cong$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ 
\OT1/cmr/m/it/10 set[]mset[]A multiplicity[]self prime[]multiplicity[]other$\OT
1/cmr/m/n/10 )$[] 

Overfull \hbox (5.04556pt too wide) in paragraph at lines 5143--5147
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms False \OT1/cmr/bx/n/10 show 
\OT1/cmr/m/it/10 ?the-sis \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/
10 subst $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 asm$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/
it/10 prime[]factorization[]subset[]iff[]dvd$\OT1/cmr/m/n/10 )$[] 
[41] [42]
Overfull \hbox (1.69742pt too wide) in paragraph at lines 5361--5362
[][]          \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a 
$\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization

Overfull \hbox (1.69742pt too wide) in paragraph at lines 5397--5398
[][]          \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr
/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a 
$\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization
[43]
Overfull \hbox (4.25296pt too wide) in paragraph at lines 5631--5632
[][]           \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cm
r/m/it/10 prod[]mset $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 prime[]factorization a
 $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prime[]factorization
[44]
Overfull \hbox (3.08865pt too wide) in paragraph at lines 5772--5775
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 prime[]factorization $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Gcd[]factor
ial A$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 Inf $\OT1/cmr/m/n/10 ($\OT1/cmr/m
/it/10 prime[]factorization
[45] [46]
Overfull \hbox (14.46059pt too wide) in paragraph at lines 6031--6032
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 gcd a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 \$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization

Overfull \hbox (15.99394pt too wide) in paragraph at lines 6051--6052
[][]  \OT1/cmr/bx/n/10 shows   \OT1/cmr/m/it/10 prime[]factorization $\OT1/cmr/
m/n/10 ($\OT1/cmr/m/it/10 lcm a b$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 prime
[]factorization a $\OMS/cmsy/m/n/10 [$$\OT1/cmr/m/n/10 #$ \OT1/cmr/m/it/10 prim
e[]factorization
[47]
Overfull \hbox (43.35431pt too wide) in paragraph at lines 6080--6087
[][]  \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 prime[]factorization[]Gcd[]factorial Gcd[]eq[]Gcd[]
factorial Gcd[]factorial[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (49.76532pt too wide) in paragraph at lines 6102--6109
[][]  \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 prime[]factorization[]Lcm[]factorial Lcm[]eq[]Lcm[]
factorial Lcm[]factorial[]eq[]0[]iff$\OT1/cmr/m/n/10 )$[] 
[48]
Overfull \hbox (55.76273pt too wide) in paragraph at lines 6263--6265
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 count[]prime[]factorization[]prime $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 prime[]fact
orization[]gcd[]factorial$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (57.29608pt too wide) in paragraph at lines 6276--6278
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 count[]prime[]factorization[]prime $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 prime[]fact
orization[]lcm[]factorial$\OT1/cmr/m/n/10 )$[] 
[49]) (./Polynomial.tex [50]

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


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


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


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


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


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

[51] [52] [53] [54] [55] [56] [57] [58]
Overfull \hbox (5.01166pt too wide) in paragraph at lines 1745--1747
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 poly[]of[]list[]impl $\OT1/cmr/m/n/
10 [$\OT1/cmr/m/it/10 code ab-stract$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 co-
effs $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 poly[]of[]list as$\OT1/cmr/m/n/10 )$ $
=$ \OT1/cmr/m/it/10 strip[]while $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 HOL$\OML/c
mm/m/it/10 :$\OT1/cmr/m/it/10 eq
[59] [60] [61] [62] [63]
Overfull \hbox (7.42665pt too wide) in paragraph at lines 2755--2768
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis coeff[]add 
coeff[]eq[]0 monoid[]add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 add$\OML/cm
m/m/it/10 :$\OT1/cmr/m/it/10 left[]neutral degree[]add[]eq[]right$\OT1/cmr/m/n/
10 )$[] 
[64] [65]
Overfull \hbox (38.39879pt too wide) in paragraph at lines 3009--3011
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule coeffs[]eq
I$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 nth[]default[]map[]eq nth[]default[]coeffs[]eq no[]trailing[]map
[66] [67]
Overfull \hbox (45.5543pt too wide) in paragraph at lines 3596--3598
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule coeffs[]eq
I$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp add$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 no[]trailing[]map nth[]default[]map[]eq nth[]default[]coeffs[]eq
[68] [69]
Overfull \hbox (32.25041pt too wide) in paragraph at lines 3854--3856
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]0$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$ 
\OT1/cmr/m/it/10 semiring[]no[]zero[]divisors[] 
[70] [71]
Overfull \hbox (49.62807pt too wide) in paragraph at lines 4247--4263
[][]\OT1/cmr/bx/n/10 instance \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$ $($$
\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 comm[]semiring[]1$\OML/cmm/m/it/10 ;$\OT1/c
mr/m/it/10 semiring[]1[]no[]zero[]divisors$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 
)$ \OT1/cmr/m/it/10 semiring[]1[]no[]zero[]divisors
[72] [73]
Overfull \hbox (23.10243pt too wide) in paragraph at lines 4776--4778
[][]        \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 assms length[]coeffs nth[]default[]coeffs[]e
q $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/i
t/10 nth[]default[]def$\OT1/cmr/m/n/10 )$[] 
[74]
Overfull \hbox (5.96727pt too wide) in paragraph at lines 4824--4837
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro poly[]eqI$\
OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr
/m/it/10 assms coeff[]map[]poly coeff[]pCons split$\OT1/cmr/m/n/10 :$ \OT1/cmr/
m/it/10 nat$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 splits$\OT1/cmr/m/n/10 )$[] 
[75] [76] [77]
Overfull \hbox (22.59839pt too wide) in paragraph at lines 5527--5540
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule order[]antis
ym $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le le[]degree$\OT1/cmr/
m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 c
oeff[]mult[]degree[]sum$\OT1/cmr/m/n/10 )$[] 
[78] [79] [80] [81]
Overfull \hbox (9.43272pt too wide) in paragraph at lines 6157--6158
[][]  \OT1/cmr/m/it/10 synthetic[]divmod $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pC
ons a p$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 c $\OT1/cmr/m/n/10 =$ $($$\OML/cmm/
m/it/10 ^^U$$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 q$\OML/cmm/m/it/10 ;$ \OT1/cmr/
m/it/10 r$\OT1/cmr/m/n/10 )$$\OML/cmm/m/it/10 :$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/
it/10 pCons r q$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1
/cmr/m/it/10 c $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 r$\OT1/cmr/m/n/10 )$$)$ 
$($\OT1/cmr/m/it/10 synthetic[]divmod
[82] [83] [84] [85]
Overfull \hbox (12.44328pt too wide) in paragraph at lines 6791--6793
[][]   \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis order[
]2 not[]gr0 poly[]eq[]0[]iff[]dvd power[]0 power[]Suc[]0 power[]one[]right$\OT1
/cmr/m/n/10 )$[] 
[86] [87]
Overfull \hbox (57.51828pt too wide) in paragraph at lines 7009--7011
[][]    \OT1/cmr/bx/n/10 by $\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 hide[
]lams$\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 One[]nat[]def add[]Suc[]right monoid[
]add[]class$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 add$\OML/cmm/m/it/10 :$\OT1/cmr
/m/it/10 right[]neutral[] 

Overfull \hbox (4.7849pt too wide) in paragraph at lines 7011--7012
[][]      \OT1/cmr/m/it/10 one[]neq[]zero order[]mult pCons[]eq[]0[]iff power[]
add power[]eq[]0[]iff power[]one[]right$\OT1/cmr/m/n/10 )$[] 
[88] [89] [90]
Overfull \hbox (23.32683pt too wide) in paragraph at lines 7630--7643
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct p ar-bi-tr
ary$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 q$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/1
0 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]add pcompose[]smu
lt pcompose[]pCons
[91]
Overfull \hbox (24.07547pt too wide) in paragraph at lines 7649--7662
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct p ar-bi-tr
ary$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 q$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/it/1
0 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]pCons pcompose[]a
dd pcompose[]mult$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (3.83954pt too wide) in paragraph at lines 7704--7717
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 induct A rule$\OT
1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 infinite[]finite[]induct$\OT1/cmr/m/n/10 )$ $(
$\OT1/cmr/m/it/10 simp[]all add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pcompose[]1
 pcompose[]mult$\OT1/cmr/m/n/10 )$[] 
[92] [93] [94] [95] [96]
Overfull \hbox (26.78821pt too wide) in paragraph at lines 8578--8591
[][]  \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 degree[]eq[]length[]coeffs coeffs[]reflect[]poly le
ngth[]dropWhile[]le diff[]le[]mono$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (7.1392pt too wide) in paragraph at lines 8614--8627
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases p rule$\OT1
/cmr/m/n/10 :$ \OT1/cmr/m/it/10 pCons[]cases$\OT1/cmr/m/n/10 )$ $($\OT1/cmr/m/i
t/10 simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 reflect[]poly[]pCons degree[]
eq[]length[]coeffs$\OT1/cmr/m/n/10 )$[] 
[97] [98] [99] [100] [101] [102]
Overfull \hbox (43.11435pt too wide) in paragraph at lines 9486--9488
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 DERIV[]add[]const$\OT1/cmr/m/n/10 :
$ \OT1/cmr/m/it/10 DE-RIV f x $\OT1/cmr/m/n/10 :$$\OML/cmm/m/it/10 >$ \OT1/cmr/
m/it/10 D $\OT1/cmr/m/n/10 =[]\OMS/cmsy/m/n/10 )$ \OT1/cmr/m/it/10 DE-RIV $\OT1
/cmr/m/n/10 ($$\OML/cmm/m/it/10 ^^U$\OT1/cmr/m/it/10 x$\OML/cmm/m/it/10 :$ \OT1
/cmr/m/it/10 a $\OT1/cmr/m/n/10 +$ \OT1/cmr/m/it/10 f x $\OT1/cmr/m/n/10 :$$:$ 
$ [] $\OT1/cmr/m/it/10 a$\OT1/cmr/m/n/10 :$$:$\OT1/cmr/m/it/10 real[]normed[]fi
eld$\OT1/cmr/m/n/10 )$
[103] [104] [105]
Overfull \hbox (5.12115pt too wide) in paragraph at lines 9897--9899
[][]      \OT1/cmr/bx/n/10 ap-ply $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 metis $\O
MS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10 nd dvd[]mult[]cancel[]right power[]not[]ze
ro pCons[]eq[]0[]iff power[]Suc
[106] [107] [108] [109] [110]
Overfull \hbox (43.09401pt too wide) in paragraph at lines 10585--10588
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dr b[]def \OT1/cmr/bx/n/1
0 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule or-der$\OML/cmm/m/it/10 :$\OT1/cm
r/m/it/10 trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le$\OT1/cmr
/m/n/10 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 degree[]monom[]le$\OT1/cmr/m/n/10 )$[] 
[111] [112] [113] [114] [115]
Overfull \hbox (18.54pt too wide) in paragraph at lines 11313--11316
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 dr \OT1/cmr/bx/n/10 by $\
OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 rule or-der$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/
10 trans$\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 OF degree[]mult[]le$\OT1/cmr/m/n/10
 ]$$)$ $($\OT1/cmr/m/it/10 auto simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 degree
[]monom[]le$\OT1/cmr/m/n/10 )$[] 
[116] [117] [118] [119]
Overfull \hbox (29.60196pt too wide) in paragraph at lines 11712--11714
[][]\OT1/cmr/bx/n/10 instantiation \OT1/cmr/m/it/10 poly $\OT1/cmr/m/n/10 :$$:$
 $($$\OMS/cmsy/m/n/10 f$\OT1/cmr/m/it/10 semidom[]divide[]unit[]factor$\OML/cmm
/m/it/10 ;$\OT1/cmr/m/it/10 idom[]divide$\OMS/cmsy/m/n/10 g$$\OT1/cmr/m/n/10 )$
 \OT1/cmr/m/it/10 normalization[]semidom[] 
[120] [121] [122] [123] [124] [125] [126] [127] [128] [129] [130] [131]
Overfull \hbox (5.7678pt too wide) in paragraph at lines 13500--13502
[][]    \OT1/cmr/bx/n/10 un-fold-ing \OT1/cmr/m/it/10 Suc$\OML/cmm/m/it/10 :$\O
T1/cmr/m/it/10 hyps$\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 )$$[$\
OT1/cmr/m/it/10 OF v n[]ok$\OML/cmm/m/it/10 ;$ \OT1/cmr/m/it/10 sym-met-ric$\OT
1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 pseudo[]divmod[]main$\OML/cmm/m/it/10 :$\OT1/c
mr/m/it/10 simps Let[]def[] 
[132]
Overfull \hbox (8.8534pt too wide) in paragraph at lines 13637--13639
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]mod[]impl$\OT1/cmr/m/n/10 [
$\OT1/cmr/m/it/10 code$\OT1/cmr/m/n/10 ]$$:$ \OT1/cmr/m/it/10 pseudo[]mod f g $
\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 poly[]of[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/
m/it/10 pseudo[]mod[]list $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 coeffs
[133] [134] [135]
Overfull \hbox (37.10872pt too wide) in paragraph at lines 13863--13865
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list[]1$\OT1/
cmr/m/n/10 :$ \OT1/cmr/m/it/10 pseudo[]divmod[]main[]list 1 $\OT1/cmr/m/n/10 =$
 \OT1/cmr/m/it/10 divmod[]poly[]one[]main[]list[] 

Overfull \hbox (93.00832pt too wide) in paragraph at lines 13945--13947
[][]\OT1/cmr/bx/n/10 lemmas \OT1/cmr/m/it/10 pdivmod[]via[]divmod[]list $\OT1/c
mr/m/n/10 =$ \OT1/cmr/m/it/10 pdivmod[]via[]pseudo[]divmod[]list$\OT1/cmr/m/n/1
0 [$\OT1/cmr/m/it/10 unfolded pseudo[]divmod[]main[]list[]1$\OT1/cmr/m/n/10 ]$[
] 
[136]
Overfull \hbox (63.45209pt too wide) in paragraph at lines 13948--13950
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 mod[]poly[]one[]main[]list$\OT1/cmr
/m/n/10 :$ \OT1/cmr/m/it/10 snd $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 divmod[]pol
y[]one[]main[]list q r d n$\OT1/cmr/m/n/10 )$ $=$ \OT1/cmr/m/it/10 mod[]poly[]o
ne[]main[]list
[137] [138] [139]
Overfull \hbox (2.32649pt too wide) in paragraph at lines 14301--14305
[][]    \OT1/cmr/bx/n/10 then ob-tain \OT1/cmr/m/it/10 a$ [] $ b$ [] $ \OT1/cmr
/bx/n/10 where \OT1/cmr/m/it/10 ab$ [] $$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 a 
$\OT1/cmr/m/n/10 =$ $[$$:$\OT1/cmr/m/it/10 a$ [] $$\OT1/cmr/m/n/10 :$$]$ \OT1/c
mr/m/it/10 b $\OT1/cmr/m/n/10 =$ $[$$:$\OT1/cmr/m/it/10 b$ [] $$\OT1/cmr/m/n/10
 :$$]$ \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto elim$\OT1/c
mr/m/n/10 !$$:$ \OT1/cmr/m/it/10 degree[]eq[]zeroE$\OT1/cmr/m/n/10 )$[] 
[140] [141]
Overfull \hbox (14.12436pt too wide) in paragraph at lines 14546--14550
[][]    \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 A \OT1/cmr/bx/n/10 and \OT1/cmr/
m/it/10 this \OT1/cmr/bx/n/10 have $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/it/10 c$\OT
1/cmr/m/n/10 :$$]$ \OT1/cmr/m/it/10 dvd $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/it/10 
a$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 _$ $\OT1/cmr/m/n/10 [$$:$\OT1/cmr/m/i
t/10 c$\OT1/cmr/m/n/10 :$$]$ \OT1/cmr/m/it/10 dvd $\OT1/cmr/m/n/10 [$$:$\OT1/cm
r/m/it/10 b$\OT1/cmr/m/n/10 :$$]$ \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/c
mr/m/it/10 rule prime[]elem[]dvd[]multD$\OT1/cmr/m/n/10 )$[] 
[142] [143] [144] [145] [146]) (./Pochhammer_Polynomials.tex [147]
Overfull \hbox (39.72092pt too wide) in paragraph at lines 105--107
[][]\OT1/cmr/bx/n/10 lemma \OT1/cmr/m/it/10 pochhammer[]poly[]Suc$\OT1/cmr/m/n/
10 :$ \OT1/cmr/m/it/10 pochhammer[]poly $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 Suc
 n$\OT1/cmr/m/n/10 )$ $=$ $[$$:$\OT1/cmr/m/it/10 of[]nat n$\OML/cmm/m/it/10 ;$\
OT1/cmr/m/it/10 1$\OT1/cmr/m/n/10 :$$]$ $\OMS/cmsy/m/n/10 ^^C$ \OT1/cmr/m/it/10
 pochhammer[]poly

Overfull \hbox (40.14108pt too wide) in paragraph at lines 143--151
[][]  \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 cases n$\OT1/cmr/
m/n/10 )$ $($\OT1/cmr/m/it/10 auto simp add$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10
 pochhammer[]poly[]altdef poly[]prod add[]ac lessThan[]Suc[]atMost
) (./Linear_Recurrences_Misc.tex) (./Partial_Fraction_Decomposition.tex)
(./Factorizations.tex [148]
Overfull \hbox (5.12407pt too wide) in paragraph at lines 72--74
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 interp[]factorization[]def interp[]alt[]factoriza
tion[]def case[]prod[]unfold[] 

Overfull \hbox (5.12407pt too wide) in paragraph at lines 116--118
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 interp[]factorization[]def interp[]alt[]factoriza
tion[]def case[]prod[]unfold[] 
[149]
Overfull \hbox (16.71938pt too wide) in paragraph at lines 244--248
[][]  \OT1/cmr/bx/n/10 from \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 p $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 interp[]factorization fc-trs 
\OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/1
0 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def$\OT1/cmr/m/n/10 )$[] 

Overfull \hbox (16.22148pt too wide) in paragraph at lines 263--267
[][]  \OT1/cmr/bx/n/10 with \OT1/cmr/m/it/10 assms \OT1/cmr/bx/n/10 have \OT1/c
mr/m/it/10 interp[]factorization fc-trs $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 
\OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/cmr/m/n/1
0 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def$\OT1/cmr/m/n/10 )$[] 
[150] [151]
Overfull \hbox (15.7888pt too wide) in paragraph at lines 465--468
[][]    \OT1/cmr/bx/n/10 us-ing \OT1/cmr/m/it/10 dis-tinct assms \OT1/cmr/bx/n/
10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro sum[]list[]cong$\OT1/cmr/m/n/10
 )$ $($\OT1/cmr/m/it/10 force simp$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 distinct
[]map inj[]on[]def$\OT1/cmr/m/n/10 )$$+$[] 

Overfull \hbox (15.70007pt too wide) in paragraph at lines 510--512
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 intro exI$\OT1/
cmr/m/n/10 [$\OT1/cmr/m/it/10 of [] $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 0$\OML/
cmm/m/it/10 ;$ $\OT1/cmr/m/n/10 [$$]$$)$$]$$)$ $($\OT1/cmr/m/it/10 auto simp$\O
T1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 is[]factorization[]of[]def interp[]factorizat
ion[]def$\OT1/cmr/m/n/10 )$[] 
[152]) (./Linear_Recurrences_Common.tex
Overfull \hbox (2.17294pt too wide) in paragraph at lines 6--6
[]\OT1/cmr/bx/n/14.4 Material com-mon to ho-moge-nous and in-ho-moge-
[153]) (./Eulerian_Polynomials.tex [154]
Overfull \hbox (5.86856pt too wide) in paragraph at lines 78--80
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 p fps[]deriv[]power algebra[]simps fps[]const[]ne
g $\OT1/cmr/m/n/10 [$\OT1/cmr/m/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/i
t/10 fps[]of[]nat
[155]
Overfull \hbox (6.71323pt too wide) in paragraph at lines 177--178
[][]  \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 fps[]monom[]poly c k $\OT1/cmr/m/
n/10 =$ $($\OT1/cmr/m/it/10 if k $\OT1/cmr/m/n/10 =$ \OT1/cmr/m/it/10 0 then 1 
else pcom-pose $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 pCons 0 $\OT1/cmr/m/n/10 ($\
OT1/cmr/m/it/10 eulerian[]poly
[156]
Overfull \hbox (21.73657pt too wide) in paragraph at lines 301--303
[][]    \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1/c
mr/m/n/10 :$ \OT1/cmr/m/it/10 fps[]compose[]power $\OT1/cmr/m/n/10 [$\OT1/cmr/m
/it/10 symmetric$\OT1/cmr/m/n/10 ]$ \OT1/cmr/m/it/10 fps[]compose[]sub[]distrib
 del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 power[]Suc$\OT1/cmr/m/n/10 )$[] 
))
No file root.bbl.
[157] (./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/cmr8.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmsy5.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmti12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbol
s/msam10.pfb>
Output written on root.pdf (157 pages, 544251 bytes).
Transcript written on root.log.

*** Undeclared class: "??.semiring_div" (line 110 of "~~/afp/thys/Linear_Recurrences/Partial_Fraction_Decomposition.thy")
*** Failed to parse type
*** At command "definition" (line 109 of "~~/afp/thys/Linear_Recurrences/Partial_Fraction_Decomposition.thy")
*** Failed to load theory "Linear_Recurrences.Rational_FPS_Solver" (unresolved "Linear_Recurrences.Partial_Fraction_Decomposition")
*** Failed to load theory "Linear_Recurrences.Linear_Homogenous_Recurrences" (unresolved "Linear_Recurrences.RatFPS", "Linear_Recurrences.Rational_FPS_Solver")
*** Failed to load theory "Linear_Recurrences.Linear_Inhomogenous_Recurrences" (unresolved "Linear_Recurrences.Linear_Homogenous_Recurrences", "Linear_Recurrences.RatFPS")
*** Failed to load theory "Linear_Recurrences.Linear_Recurrences_Solver" (unresolved "Linear_Recurrences.Linear_Homogenous_Recurrences", "Linear_Recurrences.Linear_Inhomogenous_Recurrences")
*** Failed to apply initial proof method (line 214 of "~~/afp/thys/Linear_Recurrences/Linear_Recurrences_Misc.thy"):
*** goal (1 subgoal):
***  1. gcd [:1::'a, c:] [:1::'a, c':] =
***     gcd ([:1::'a, c:] mod [:1::'a, c':]) [:1::'a, c':]
*** At command "by" (line 214 of "~~/afp/thys/Linear_Recurrences/Linear_Recurrences_Misc.thy")
*** Undeclared class: "??.ring_div" (line 554 of "~~/afp/thys/Linear_Recurrences/RatFPS.thy")
*** Failed to parse sort
*** At command "instantiation" (line 554 of "~~/afp/thys/Linear_Recurrences/RatFPS.thy")