@MISC{GCD_1.MIZ,
  AUTHOR = {Schwarzweller, Christoph},
  TITLE = {The Correctness of the Generic Algorithms of {B}rown and {H}enrici
Concerning Addition and Multiplication in Fraction Fields},
  SECTION1 = {Basics},
  SECTION2 = {AmpleSets},
  SECTION3 = {GCD-Domains},
  SECTION4 = {The Theorems of Brown and Henrici},
  SECTION5 = {Correctness of the Algorithms},
  DAY = {16},
  MONTH = {June},
  YEAR = {1997},
  ADDRESS1 = {University of T{\"u}bingen
T{\"u}bingen},
  SUMMARY = {We prove the correctness of the generic algorithms of Brown and Henrici
concerning addition and multiplication in fraction fields of gcd-domains.
For that we first prove some basic facts about divisibility in integral
domains and introduce the concept of amplesets. After that we are able to
define gcd-domains and to prove the theorems of Brown and Henrici which are
crucial for the correctness of the algorithms. In the last section we
define Mizar functions mirroring their input/output behaviour and prove
properties of these functions that ensure the correctness of the algorithms.}}

