Edit detail for SandBoxSum revision 10 of 14

The Sum domain constructor is intended to be the
Categorical Dual
of the Product
domain constructor
\begin{spad}
)abbrev domain SUM Sum
++ Description:
++ This domain implements direct union
Sum (A:SetCategory,B:SetCategory) : C == T
 where
  C == SetCategory  with
       if A has Finite and B has Finite then Finite
       if A has Monoid and B has Monoid then Monoid
       if A has AbelianMonoid and B has AbelianMonoid then AbelianMonoid
       if A has CancellationAbelianMonoid and
          B has CancellationAbelianMonoid then CancellationAbelianMonoid
       if A has Group  and B has Group  then  Group
       if A has AbelianGroup and B has AbelianGroup then  AbelianGroup
       if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup
                                             then OrderedAbelianMonoidSup
       if A has OrderedSet and B has OrderedSet then  OrderedSet
       selectsum     : % -> Union(acomp:A,bcomp:B)
        ++ selectsum(x) \undocumented
       in1  :   A -> %
        ++ makefirst(a) \undocumented
       in2 :   B -> %
        ++ makesecond(b) \undocumented
  T == add
    --representations
       Rep == Union(acomp:A,bcomp:B)
       import Rep
    --declarations
       x,y: %
       i: NonNegativeInteger
       p: NonNegativeInteger
       a: A
       b: B
       c: PositiveInteger
       d: Integer
    --define
       coerce(x:%):OutputForm ==
         rep(x) case acomp => sub(coerce(rep(x).acomp),"1")
         sub(coerce(rep(x).bcomp),"2")
       x=y == rep(x)=rep(y)
       selectsum(x) == rep(x)
       in1(a) == per [a]
       in2(b) == per [b]

       if A has Monoid and B has Monoid then
represent unit of Sum(A,B) as 1$A (We could use either 1$A or 1$B)
          1 == per [1$A]
          x * y ==
                   rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp * rep(y).acomp]
                   rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp  rep(y).bcomp]
                   -- unit of Sum(A,B)=1$A is unit for B
                   x=1 => y
                   y=1 => x
                   error "not same type"
          x * p ==
                   rep(x) case acomp => per [rep(x).acomp ** p]
                   per [rep(x).bcomp ** p]

       if A has Finite and B has Finite then
          size == size$A + size$B
          index(n) ==
                      n > size$B => per [index((n::Integer - size$B)::PositiveInteger)$A]
                      per [index(n)$B]
          random() ==
                      random()$Boolean => per [random()$A]
                      per [random()$B]
          lookup(x) ==
                      rep(x) case acomp => (lookup(rep(x).acomp)$A::NonNegativeInteger + size$B)::PositiveInteger
                      lookup(rep(x).bcomp)$B
          hash(x) ==
                      rep(x) case acomp => hash(rep(x).acomp)$A + size$B::SingleInteger
                      hash(rep(x).bcomp)$B
       if A has Group and B has Group then
          inv(x) ==
                    rep(x) case acomp => per [inv(rep(x).acomp)]
                    per [inv(rep(x).bcomp)]

       if A has AbelianMonoid and B has AbelianMonoid then
represent zero of Sum(A,B) as 0$A (We could use either 0$A or 0$B)
          0 == per [0$A]
          x + y ==
                   rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp + rep(y).acomp]
                   rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp + rep(y).bcomp]
                   -- zero of Sum(A,B)=0$A is zero for B
                   x=0 => y
                   y=0 => x
                   error "not same type"
          c * x ==
                   rep(x) case acomp => per [c * rep(x).acomp]
                   per [c* rep(x).bcomp]

       if A has AbelianGroup and B has AbelianGroup then
          -x ==
                 rep(x) case acomp => per [- rep(x).acomp]
                 per [- rep(x).bcomp]
          (x - y):% ==
                   rep(x) case acomp and rep(y) case acomp => per [rep(x).acomp - rep(y).acomp]
                   rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp - rep(y).bcomp]
                   -- zero of Sum(A,B)=0$A is zero for B
                   x=0 => -y
                   y=0 => x
                   error "not same type"
          d * x ==
                   rep(x) case acomp => per [d * rep(x).acomp]
                   per [d* rep(x).bcomp]

       if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then
          sup(x,y) ==
                   rep(x) case acomp and rep(y) case acomp => per [sup(rep(x).acomp,rep(y).acomp)]
                   rep(x) case bcomp and rep(y) case bcomp => per [sup(rep(x).bcomp,rep(y).bcomp)]
                   rep(x) case acomp and rep(y) case bcomp => y
                   x
       if A has OrderedSet and B has OrderedSet then
          x < y ==
                   rep(x) case acomp and rep(y) case acomp => rep(x).acomp < rep(y).acomp
                   rep(x) case bcomp and rep(y) case bcomp => rep(x).bcomp < rep(y).bcomp
                   rep(x) case acomp and rep(y) case bcomp
\end{spad}


\begin{axiom}
size()$Sum(PF 7,PF 13)
size()$Sum(PF 7,Product(PF 3,PF 13))
in1(10)$Sum(Integer,Integer)
in1(10)$Sum(Integer,Integer) < in2(10)$Sum(Integer,Integer)
sup(in1(99)$Sum(NNI,NNI), in2(10)$Sum(NNI,NNI))
\end{axiom}
The CoTuple domain constructor is intended to be the
Categorical Dual
of the Tuple
domain constructor
\begin{spad}
)abbrev domain COT CoTuple
++ This domain is intended to be the categorical dual of a
++ Tuple (comma-delimited homogeneous sequence of values).
++ As such it implements an n-ary disjoint union.
CoTuple(S:Type): CoercibleTo(S) with
    inj: (NonNegativeInteger,S) -> %
      ++ inject(x,n) returns x as an element of the n-th
      ++ component of the CoTuple. CoTuples are 0-based
    ind: % -> NonNegativeInteger
      ++ index(x) returns the component number of x in the CoTuple
    if S has Monoid then Monoid
    if S has AbelianMonoid then AbelianMonoid
    if S has CancellationAbelianMonoid then CancellationAbelianMonoid
    if S has Group then Group
    if S has AbelianGroup then  AbelianGroup
    if S has OrderedAbelianMonoidSup then OrderedAbelianMonoidSup
    if S has SetCategory then SetCategory
    if S has OrderedSet then OrderedSet
  == add
    Rep == Record(ind : NonNegativeInteger, elt : S)
    --declarations
    x,y: %
    s: S
    i: NonNegativeInteger
    p: NonNegativeInteger
    c: PositiveInteger
    d: Integer
    coerce(x:%):S == rep(x).elt
    inj(i,s) == per [i,s]
    ind(x) == rep(x).ind
    if S has SetCategory then
      x = y == (rep(x).ind = rep(y).ind) and (rep(x).elt = rep(y).elt)
      coerce(x : %): OutputForm == sub(coerce(rep(x).elt),coerce(rep(x).ind))
    if S has Monoid then
      -- represent unit of CoTuple(S) as 1$S of component 0
      1 == per [0,1]
      x * y ==
        rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).elt  rep(y).elt]
        x = 1 => y
        y = 1 => x
        error "not same type"
      x * p == per [rep(x).ind, rep(x).elt ** p]
    if S has Group then
       inv(x) == per [rep(x).ind, inv(rep(x).elt)]

    if S has AbelianMonoid then
represent zero of Sum(A,B) as 0$S
       0 == per [0,0]
       x + y ==
         rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).elt + rep(y).elt]
         x = 0 => y
         y = 0 => x
         error "not same type"
       c * x == per [rep(x).ind, c * rep(x).elt]

    if S has AbelianGroup then
      - x == per [rep(x).ind, -rep(x).elt]
      (x - y):% ==
        rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).elt - rep(y).elt]
        x = 0 => -y
        y = 0 => x
        error "not same type"
      d * x == per [rep(x).ind, d* rep(x).elt]

    if S has OrderedAbelianMonoidSup then
      sup(x,y) ==
        rep(x).ind = rep(y).ind => per [rep(x).ind, sup(rep(x).elt,rep(y).elt)]
        rep(x).ind < rep(y).ind => y
        x
    if S has OrderedSet then
      x < y ==
        rep(x).ind = rep(y).ind => rep(x).elt < rep(y).elt
        rep(x).ind < rep(y).ind
\end{spad}

\begin{axiom}
inj(1,10)
inj(1,10) < inj(2,10)
sup(inj(1,99), inj(2,10))$CoTuple(NNI)
\end{axiom}
The DirectSum domain constructor implements an associative
(flat) DirectSum domain that is the dual to DirectProduct.
\begin{spad}
)abbrev domain DIRSUM DirectSum
++ This domain is intended to be the categorical dual of
++ DirectProduct (comma-delimited homogeneous sequence of
++ values). As such it implements an n-ary disjoint union.
DirectSum(S:Type): Type with
    coerce: S -> %
      ++ any type is a 1-ary union
    inj: (NonNegativeInteger,NonNegativeInteger,%) -> %
      ++ inject(i,n,x) injects the m-CoTuple element x as the
      ++ (m + i)-th component of the (n+m)-CoTuple.
    ind: % -> NonNegativeInteger
      ++ index(x) returns the component number of x in the CoTuple
    len: % -> NonNegativeInteger
      ++ len(x) returns the number of components
    if S has Monoid then Monoid
    if S has AbelianMonoid then AbelianMonoid
    if S has CancellationAbelianMonoid then CancellationAbelianMonoid
    if S has Group then Group
    if S has AbelianGroup then  AbelianGroup
    if S has OrderedAbelianMonoidSup then OrderedAbelianMonoidSup
    if S has SetCategory then SetCategory
    if S has OrderedSet then OrderedSet
  == add
    Rep == Record(ind:NonNegativeInteger, len:NonNegativeInteger, elt:S)
    --declarations
    x,y: %
    s: S
    i: NonNegativeInteger
    p: NonNegativeInteger
    c: PositiveInteger
    d: Integer
    coerce(s:S):% == per [0,0,s]
    inj(i,n,x) ==
      i < n => per [rep(x).len+i,rep(x).len+n,rep(x).elt]
      error "index out of bounds"
    ind(x) == rep(x).ind
    len(x) == rep(x).len
    if S has SetCategory then
      x = y == (rep(x).ind = rep(y).ind) and (rep(x).elt = rep(y).elt)
      coerce(x : %): OutputForm == sub(coerce(rep(x).elt),coerce(rep(x).ind))
    if S has Monoid then
      -- represent unit of CoTuple(S) as 1$S of component 0
      1 == per [0,0,1]
      x * y ==
        rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).len, rep(x).elt  rep(y).elt]
        x = 1 => y
        y = 1 => x
        error "not same type"
      x * p == per [rep(x).ind, rep(x).len, rep(x).elt ** p]
    if S has Group then
       inv(x) == per [rep(x).ind, rep(x).len, inv(rep(x).elt)]

    if S has AbelianMonoid then
represent zero of Sum(A,B) as 0$S
       0 == per [0,0,0]
       x + y ==
         rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).len, rep(x).elt + rep(y).elt]
         x = 0 => y
         y = 0 => x
         error "not same type"
       c * x == per [rep(x).ind, rep(x).len, c * rep(x).elt]

    if S has AbelianGroup then
      - x == per [rep(x).ind, rep(x).len, -rep(x).elt]
      (x - y):% ==
        rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).len, rep(x).elt - rep(y).elt]
        x = 0 => -y
        y = 0 => x
        error "not same type"
      d * x == per [rep(x).ind, rep(x).len, d* rep(x).elt]

    if S has OrderedAbelianMonoidSup then
      sup(x,y) ==
        rep(x).ind = rep(y).ind => per [rep(x).ind, rep(x).len, sup(rep(x).elt,rep(y).elt)]
        rep(x).ind < rep(y).ind => y
        x
    if S has OrderedSet then
      x < y ==
        rep(x).ind = rep(y).ind => rep(x).elt < rep(y).elt
        rep(x).ind < rep(y).ind
\end{spad}

\begin{axiom}
inj(0,2,10)
inj(0,2,10) < inj(1,2,10)
sup(inj(0,2,99), inj(1,2,10))$DirectSum(NNI)
a0:=inj(0,2,'a)
len(a0)
b1:=inj(1,2,'b)
len(b1)
a2:=inj(0,2,inj(0,2,'aa))
len(a2)
a3:=inj(1,2,inj(0,2,'ba))
len(a3)
b2:=inj(0,2,inj(1,2,'ab))
len(b2)
b3:=inj(1,2,inj(1,2,'bb))
len(b3)
inj(2,3,b3)
\end{axiom}


    Some or all expressions may not have rendered properly,
    because Axiom returned the following error:
Error: export AXIOM=/usr/local/lib/open-axiom/x86_64-unknown-linux/1.2.0-2008-05-07; export ALDORROOT=/usr/local/aldor/linux/1.1.0; export PATH=$ALDORROOT/bin:$PATH; export HOME=/var/zope2/var/LatexWiki; ulimit -t 240; $AXIOM/bin/AXIOMsys < /var/zope2/var/LatexWiki/6339553375145284602-25px.axm

This is pdfeTeX, Version 3.141592-1.21a-2.2 (Web2C 7.5.4)
 \write18 enabled.
entering extended mode
(./5484179902931425861-18.0px.tex
LaTeX2e <2003/12/01>
Babel <v3.8d> and hyphenation patterns for american, french, german, ngerman, b
ahasa, basque, bulgarian, catalan, croatian, czech, danish, dutch, esperanto, e
stonian, finnish, greek, icelandic, irish, italian, latin, magyar, norsk, polis
h, portuges, romanian, russian, serbian, slovak, slovene, spanish, swedish, tur
kish, ukrainian, nohyphenation, loaded.
(/usr/share/texmf-tetex/tex/latex/base/article.cls
Document Class: article 2004/02/16 v1.4f Standard LaTeX document class
(/usr/share/texmf-tetex/tex/latex/base/size12.clo))
(/usr/share/texmf/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texmf/tex/latex/amsmath/amstext.sty
(/usr/share/texmf/tex/latex/amsmath/amsgen.sty))
(/usr/share/texmf/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texmf/tex/latex/amsmath/amsopn.sty))
(/usr/share/texmf/tex/latex/amsfonts/amsfonts.sty)
(/usr/share/texmf/tex/latex/amsfonts/amssymb.sty)
(/usr/share/texmf/tex/latex/amscls/amsthm.sty)
(/usr/share/texmf/tex/generic/xypic/xy.sty
(/usr/share/texmf/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes, docmode,
(/usr/share/texmf/tex/generic/xypic/xyrecat.tex)
(/usr/share/texmf/tex/generic/xypic/xyidioms.tex)
 Xy-pic version 3.7 <1999/02/16>
 Copyright (c) 1991-1998 by Kristoffer H. Rose <krisrose@ens-lyon.fr>
 Xy-pic is free software: see the User's Guide for details.

Loading kernel: messages; fonts; allocations: state, direction,
utility macros; pictures: \xy, positions, objects, decorations;
kernel objects: directionals, circles, text; options; algorithms: directions,
edges, connections;  Xy-pic loaded)
(/usr/share/texmf/tex/generic/xypic/xyall.tex
 Xy-pic option: All features v.3.3
(/usr/share/texmf/tex/generic/xypic/xycurve.tex
 Xy-pic option: Curve and Spline extension v.3.7 curve, circles, loaded)
(/usr/share/texmf/tex/generic/xypic/xyframe.tex
 Xy-pic option: Frame and Bracket extension v.3.7 loaded)
(/usr/share/texmf/tex/generic/xypic/xycmtip.tex
 Xy-pic option: Computer Modern tip extension v.3.3
(/usr/share/texmf/tex/generic/xypic/xytips.tex
 Xy-pic option: More Tips extension v.3.3 loaded) loaded)
(/usr/share/texmf/tex/generic/xypic/xyline.tex
 Xy-pic option: Line styles extension v.3.6 loaded)
(/usr/share/texmf/tex/generic/xypic/xyrotate.tex
 Xy-pic option: Rotate and Scale extension v.3.3 loaded)
(/usr/share/texmf/tex/generic/xypic/xycolor.tex
 Xy-pic option: Colour extension v.3.3 loaded)
(/usr/share/texmf/tex/generic/xypic/xymatrix.tex
 Xy-pic option: Matrix feature v.3.4 loaded)
(/usr/share/texmf/tex/generic/xypic/xyarrow.tex
 Xy-pic option: Arrow and Path feature v.3.5 path, \ar, loaded)
(/usr/share/texmf/tex/generic/xypic/xygraph.tex
 Xy-pic option: Graph feature v.3.7 loaded) loaded))
(/usr/share/texmf-tetex/tex/latex/graphics/graphicx.sty
(/usr/share/texmf-tetex/tex/latex/graphics/keyval.sty)
(/usr/share/texmf-tetex/tex/latex/graphics/graphics.sty
(/usr/share/texmf-tetex/tex/latex/graphics/trig.sty)
(/usr/share/texmf-tetex/tex/latex/graphics/graphics.cfg)
(/usr/share/texmf-tetex/tex/latex/graphics/dvips.def)))
(/usr/share/texmf-tetex/tex/latex/graphics/color.sty
(/usr/share/texmf-tetex/tex/latex/graphics/color.cfg)
(/usr/share/texmf-tetex/tex/latex/graphics/dvipsnam.def))
(/usr/share/texmf-tetex/tex/latex/tools/verbatim.sty)
(/usr/share/texmf/tex/latex/graphviz/graphviz.sty
(/usr/share/texmf/tex/latex/psfrag/psfrag.sty))
(/usr/share/texmf/tex/latex/sagetex.sty
Writing sage input file 5484179902931425861-18.0px.sage
(./5484179902931425861-18.0px.sout))
(/usr/share/texmf/tex/latex/gnuplottex/gnuplottex.sty
(/usr/share/texmf-tetex/tex/latex/base/latexsym.sty)
(/usr/share/texmf/tex/latex/moreverb/moreverb.sty)
(/usr/share/texmf-tetex/tex/latex/base/ifthen.sty))
(./5484179902931425861-18.0px.aux)
 Undefined control sequence.
l.80         ++ selectsum(x) \undocumented
 Undefined control sequence.
l.82         ++ makefirst(a) \undocumented
 Undefined control sequence.
l.84         ++ makesecond(b) \undocumented

Overfull \hbox (139.9195pt too wide) in paragraph at lines 101--109
[]\OT1/cmr/m/n/12 --define co-erce(x:rep(x) case acomp => sub(coerce(rep(x).aco
mp),"1") sub(coerce(rep(x).bcomp),"2")
(/usr/share/texmf/tex/latex/amsfonts/umsa.fd)
(/usr/share/texmf/tex/latex/amsfonts/umsb.fd)
(/usr/share/texmf-tetex/tex/latex/base/ulasy.fd)
 Missing $ inserted.
<inserted text> 
                $
l.123 
 Missing $ inserted.
<inserted text> 
                $
l.138 

Overfull \hbox (9.6173pt too wide) in paragraph at lines 124--138
\OT1/cmr/m/n/12 > size$\OML/cmm/m/it/12 B \OT1/cmr/m/n/12 =\OML/cmm/m/it/12 > p
er\OT1/cmr/m/n/12 [\OML/cmm/m/it/12 index\OT1/cmr/m/n/12 ((\OML/cmm/m/it/12 n \
OT1/cmr/m/n/12 :: \OML/cmm/m/it/12 Integer \OMS/cmsy/m/n/12 ^^@ \OML/cmm/m/it/1
2 size$\OT1/cmr/m/n/12 B)::PositiveInteger)$\OML/cmm/m/it/12 A\OT1/cmr/m/n/12 ]
\OML/cmm/m/it/12 per\OT1/cmr/m/n/12 [\OML/cmm/m/it/12 index\OT1/cmr/m/n/12 (\OM
L/cmm/m/it/12 n\OT1/cmr/m/n/12 )$B]
Overfull \hbox (38.36574pt too wide) in paragraph at lines 124--138
\OT1/cmr/m/n/12 ran-dom() == random()$\OML/cmm/m/it/12 Boolean \OT1/cmr/m/n/12 
=\OML/cmm/m/it/12 > per\OT1/cmr/m/n/12 [\OML/cmm/m/it/12 random\OT1/cmr/m/n/12 
()$A] per [random()$\OML/cmm/m/it/12 B\OT1/cmr/m/n/12 ]\OML/cmm/m/it/12 lookup\
OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 ) ==
Overfull \hbox (13.75964pt too wide) in paragraph at lines 124--138
\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )\OML/cm
m/m/it/12 caseacomp \OT1/cmr/m/n/12 =\OML/cmm/m/it/12 > \OT1/cmr/m/n/12 (\OML/c
mm/m/it/12 lookup\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm
/m/it/12 x\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :acomp\OT1/cmr/m/n/12 )$A::NonNegat
iveInteger + size$\OML/cmm/m/it/12 B\OT1/cmr/m/n/12 ) ::
 Missing $ inserted.
<inserted text> 
                $
l.157 
Overfull \hbox (16.80688pt too wide) in paragraph at lines 144--157
\OT1/cmr/m/n/12 rep(x) case bcomp and rep(y) case bcomp => per [rep(x).bcomp + 
rep(y).bcomp]
Overfull \hbox (26.15411pt too wide) in paragraph at lines 144--157
\OT1/cmr/m/n/12 -- zero of Sum(A,B)=0$\OML/cmm/m/it/12 AiszeroforBx \OT1/cmr/m/
n/12 = 0 =\OML/cmm/m/it/12 > yy \OT1/cmr/m/n/12 = 0 =\OML/cmm/m/it/12 > xerror\
OT1/cmr/m/n/12 "\OML/cmm/m/it/12 notsametype\OT1/cmr/m/n/12 "\OML/cmm/m/it/12 c
 \OMS/cmsy/m/n/12 ^^C
[1]
 Missing $ inserted.
<inserted text> 
                $
l.169 
Overfull \hbox (10.2139pt too wide) in paragraph at lines 170--173
[]\OT1/cmr/m/n/12 d * x == rep(x) case acomp => per [d * rep(x).acomp] per [d* 
rep(x).bcomp] 
[2] [3]
 Missing $ inserted.
<inserted text> 
                $
l.241 
 Missing $ inserted.
<inserted text> 
                $
l.254 

Overfull \hbox (19.35013pt too wide) in paragraph at lines 245--254
\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 y\OT1/cmr/m/n/12 )\OML/cm
m/m/it/12 :elt\OT1/cmr/m/n/12 ]\OML/cmm/m/it/12 x \OT1/cmr/m/n/12 = 0 =\OML/cmm
/m/it/12 > yy \OT1/cmr/m/n/12 = 0 =\OML/cmm/m/it/12 > xerror\OT1/cmr/m/n/12 "\O
ML/cmm/m/it/12 notsametype\OT1/cmr/m/n/12 "\OML/cmm/m/it/12 c \OMS/cmsy/m/n/12 
^^C \OML/cmm/m/it/12 x \OT1/cmr/m/n/12 == \OML/cmm/m/it/12 per\OT1/cmr/m/n/12 [
\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )\OML/cm
m/m/it/12 :ind; c \OMS/cmsy/m/n/12 ^^C
Overfull \hbox (16.79726pt too wide) in paragraph at lines 265--275
[]\OT1/cmr/m/n/12 if S has Or-dered-Abelian-Monoid-Sup then sup(x,y) == rep(x).
ind = rep(y).ind
[4] [5]
Overfull \hbox (1.0751pt too wide) in paragraph at lines 315--321
[]\OT1/cmr/m/n/12 coerce(s:S):inj(i,n,x) == i < n => per [rep(x).len+i,rep(x).l
en+n,rep(x).elt]
 Missing $ inserted.
<inserted text> 
                $
l.334 
Overfull \hbox (22.61702pt too wide) in paragraph at lines 322--334
\OML/cmm/m/it/12 yy \OT1/cmr/m/n/12 = 1 =\OML/cmm/m/it/12 > xerror\OT1/cmr/m/n/
12 "\OML/cmm/m/it/12 notsametype\OT1/cmr/m/n/12 "\OML/cmm/m/it/12 x \OMS/cmsy/m
/n/12 ^^C ^^C\OML/cmm/m/it/12 p \OT1/cmr/m/n/12 == \OML/cmm/m/it/12 per\OT1/cmr
/m/n/12 [\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12
 )\OML/cmm/m/it/12 :ind; rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 
)\OML/cmm/m/it/12 :len; rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )
\OML/cmm/m/it/12 :elt \OMS/cmsy/m/n/12 ^^C
 Missing $ inserted.
<inserted text> 
                $
l.347 
Overfull \hbox (49.97095pt too wide) in paragraph at lines 338--347
\OML/cmm/m/it/12 per\OT1/cmr/m/n/12 [0\OML/cmm/m/it/12 ; \OT1/cmr/m/n/12 0\OML/
cmm/m/it/12 ; \OT1/cmr/m/n/12 0]\OML/cmm/m/it/12 x \OT1/cmr/m/n/12 + \OML/cmm/m
/it/12 y \OT1/cmr/m/n/12 == \OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/
12 x\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :ind \OT1/cmr/m/n/12 = \OML/cmm/m/it/12 r
ep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 y\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :ind \OT
1/cmr/m/n/12 =\OML/cmm/m/it/12 > per\OT1/cmr/m/n/12 [\OML/cmm/m/it/12 rep\OT1/c
mr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :ind; rep\OT1/cm
r/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :len; rep\OT1/cmr
/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :elt \OT1/cmr/m/n/
12 +
Overfull \hbox (76.88153pt too wide) in paragraph at lines 338--347
\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 y\OT1/cmr/m/n/12 )\OML/cm
m/m/it/12 :elt\OT1/cmr/m/n/12 ]\OML/cmm/m/it/12 x \OT1/cmr/m/n/12 = 0 =\OML/cmm
/m/it/12 > yy \OT1/cmr/m/n/12 = 0 =\OML/cmm/m/it/12 > xerror\OT1/cmr/m/n/12 "\O
ML/cmm/m/it/12 notsametype\OT1/cmr/m/n/12 "\OML/cmm/m/it/12 c \OMS/cmsy/m/n/12 
^^C \OML/cmm/m/it/12 x \OT1/cmr/m/n/12 == \OML/cmm/m/it/12 per\OT1/cmr/m/n/12 [
\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )\OML/cm
m/m/it/12 :ind; rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )\OML/cmm
/m/it/12 :len; c \OMS/cmsy/m/n/12 ^^C
Overfull \hbox (16.79726pt too wide) in paragraph at lines 358--368
[]\OT1/cmr/m/n/12 if S has Or-dered-Abelian-Monoid-Sup then sup(x,y) == rep(x).
ind = rep(y).ind
Overfull \hbox (6.16672pt too wide) in paragraph at lines 358--368
\OT1/cmr/m/n/12 => per [rep(x).ind, rep(x).len, sup(rep(x).elt,rep(y).elt)] rep
(x).ind < rep(y).ind
[6] [7] [8] (./5484179902931425861-18.0px.aux) )
(see the transcript file for additional information)
Output written on 5484179902931425861-18.0px.dvi (8 pages, 13660 bytes).
Transcript written on 5484179902931425861-18.0px.log.