login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit

# Edit detail for SandBoxSum revision 11 of 14

 1 2 3 4 5 6 7 8 9 10 11 12 13 14 Editor: Bill Page Time: 2008/08/29 11:42:34 GMT-7 Note: DirectSum

The Sum domain constructor is intended to be the
Categorical Dual
of the Product
domain constructor
)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
--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

\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.
)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
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

\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.3.0-2009-01-05; 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
Segmentation fault
GCL (GNU Common Lisp)  2.6.7 CLtL1    Oct 29 2006 20:31:33
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter
Use (help) to get some basic information on how to use GCL.
Temporary directory for compiler files set to /tmp/
OpenAxiom: The Open Scientific Computation Platform
Version: OpenAxiom 1.3.0-2009-01-05
Built on Wednesday January 7, 2009 at 17:48:30
-----------------------------------------------------------------------------
Issue )summary for a summary of useful system commands.
-----------------------------------------------------------------------------
(1) -> (1) -> (1) -> (1) -> (1) -> <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
--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</spad>
Compiling OpenAxiom source code from file
SUM abbreviates domain Sum


Some or all expressions may not have rendered properly, because Latex returned the following error:
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6)
\write18 enabled.
%&-line parsing enabled.
entering extended mode
(./7709895480293645513-16.0px.tex
LaTeX2e <2005/12/01>
Babel <v3.8h> and hyphenation patterns for english, usenglishmax, dumylang, noh
yphenation, arabic, farsi, croatian, ukrainian, russian, bulgarian, czech, slov
ak, danish, dutch, finnish, basque, french, german, ngerman, ibycus, greek, mon
ogreek, ancientgreek, hungarian, italian, latin, mongolian, norsk, icelandic, i
nterlingua, turkish, coptic, romanian, welsh, serbian, slovenian, estonian, esp
eranto, uppersorbian, indonesian, polish, portuguese, spanish, catalan, galicia
(/usr/share/texmf-texlive/tex/latex/base/article.cls
Document Class: article 2005/09/16 v1.4f Standard LaTeX document class
(/usr/share/texmf-texlive/tex/latex/base/size12.clo))
(/usr/share/texmf-texlive/tex/latex/geometry/geometry.sty
(/usr/share/texmf-texlive/tex/latex/graphics/keyval.sty)
(/usr/share/texmf-texlive/tex/xelatex/xetexconfig/geometry.cfg)

Package geometry Warning: lmargin' and rmargin' result in NEGATIVE (-108.405p
t).
width' should be shortened in length.
) (/usr/share/texmf-texlive/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the ? option.
(/usr/share/texmf-texlive/tex/latex/amsmath/amstext.sty
(/usr/share/texmf-texlive/tex/latex/amsmath/amsgen.sty))
(/usr/share/texmf-texlive/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texmf-texlive/tex/latex/amsmath/amsopn.sty))
(/usr/share/texmf-texlive/tex/latex/amsfonts/amsfonts.sty)
(/usr/share/texmf-texlive/tex/latex/amsfonts/amssymb.sty)
(/usr/share/texmf-texlive/tex/latex/amscls/amsthm.sty)
(/usr/share/texmf-texlive/tex/latex/setspace/setspace.sty
Package: setspace 6.7 <2000/12/01>
) (/usr/share/texmf-texlive/tex/generic/xypic/xy.sty
(/usr/share/texmf-texlive/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes,
docmode, (/usr/share/texmf-texlive/tex/generic/xypic/xyrecat.tex)
(/usr/share/texmf-texlive/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.

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

(/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd)
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsb.fd)
(/usr/share/texmf-texlive/tex/latex/base/ulasy.fd)
Missing $inserted. <inserted text>$
l.125  Missing $inserted. <inserted text>$
l.140

Overfull \hbox (64.99706pt too wide) in paragraph at lines 126--140
[]\OT1/cmr/m/n/12 if A has Fi-nite and B has Fi-nite then size == size$\OML/cmm /m/it/12 A \OT1/cmr/m/n/12 + \OML/cmm/m/it/12 size$\OT1/cmr/m/n/12 B in-dex(n)
== n > size$\OML/cmm/m/it/12 B \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 ((\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/12 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 (\OML/cmm/m/it/ 12 n\OT1/cmr/m/n/12 )$B]
Overfull \hbox (56.09259pt too wide) in paragraph at lines 126--140
\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 ) == \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 caseacomp \OT1 /cmr/m/n/12 =\OML/cmm/m/it/12 > \OT1/cmr/m/n/12 (\OML/cmm/m/it/12 lookup\OT1/cm r/m/n/12 (\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/1 2 )\OML/cmm/m/it/12 :acomp\OT1/cmr/m/n/12 )$A::NonNegativeInteger
Overfull \hbox (49.75084pt too wide) in paragraph at lines 126--140
\OT1/cmr/m/n/12 + size$\OML/cmm/m/it/12 B\OT1/cmr/m/n/12 ) :: \OML/cmm/m/it/12 PositiveIntegerlookup\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 :bcomp\OT1/cmr/m/n/12 )$B hash(
x) == rep(x) case acomp => hash(rep(x).acomp)$\OML/cmm/m/it/12 A \OT1/cmr/m/n/1 2 + \OML/cmm/m/it/12 size$\OT1/cmr/m/n/12 B::SingleInteger hash(rep(x).bcomp)$\ OML/cmm/m/it/12 B$
Missing $inserted. <inserted text>$
l.159  Missing $inserted. <inserted text>$
l.171

[1]
LaTeX Warning: Characters dropped after \end{axiom}' on input line 195.
Missing $inserted. <inserted text>$
l.241
Missing $inserted. <inserted text>$
l.254
Overfull \hbox (17.33601pt too wide) in paragraph at lines 245--254
[]\OT1/cmr/m/n/12 if S has Abelian-Monoid then -- rep-re-sent zero of Sum(A,B)
as 0$\OML/cmm/m/it/12 S\OT1/cmr/m/n/12 0 == \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 x \OT1/cmr/m/n/12 + \O ML/cmm/m/it/12 y \OT1/cmr/m/n/12 == \OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/c mm/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 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 y\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :ind \OT1/cmr/m/n/12 =\OML/cmm/m/it/12 > per\OT1/cmr/m/n/12 [\OML/cmm/m/it/12 r ep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :ind; re p\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 + [2] LaTeX Warning: Characters dropped after \end{axiom}' on input line 279. Missing$ inserted.
<inserted text>
$l.332 Missing$ inserted.
<inserted text>
$l.345 Overfull \hbox (86.00618pt too wide) in paragraph at lines 336--345 []\OT1/cmr/m/n/12 if S has Abelian-Monoid then -- rep-re-sent zero of Sum(A,B) as 0$\OML/cmm/m/it/12 S\OT1/cmr/m/n/12 0 == \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]\OM
L/cmm/m/it/12 x \OT1/cmr/m/n/12 + \OML/cmm/m/it/12 y \OT1/cmr/m/n/12 == \OML/cm
m/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 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12
y\OT1/cmr/m/n/12 )\OML/cmm/m/it/12 :ind \OT1/cmr/m/n/12 =\OML/cmm/m/it/12 > pe
r\OT1/cmr/m/n/12 [\OML/cmm/m/it/12 rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/c
mr/m/n/12 )\OML/cmm/m/it/12 :ind; rep\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 x\OT1/cm
r/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 +
[3]
LaTeX Warning: Characters dropped after \end{axiom}' on input line 383.
[4] [5] [6]
Misplaced alignment tab character &.
l.387 $$B =& gt; per [index((n::Integer - size$$\newpage
[7]
Misplaced alignment tab character &.
l.388 $$Boolean =& gt; per [random()$$\newpage
[8] [9] [10] [11] (./7709895480293645513-16.0px.aux) )
(see the transcript file for additional information)
Output written on 7709895480293645513-16.0px.dvi (11 pages, 13948 bytes).
Transcript written on 7709895480293645513-16.0px.log.