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

# Edit detail for SandBoxSum revision 13 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
   Compiling OpenAxiom source code from file
SUM abbreviates domain Sum
------------------------------------------------------------------------
initializing NRLIB SUM for Sum
compiling into NRLIB SUM
Adding $modemaps Adding A modemaps Adding B modemaps importing Rep Adding Integer modemaps Adding NonNegativeInteger modemaps Adding PositiveInteger modemaps Adding OutputForm modemaps compiling exported coerce : % -> OutputForm Adding Boolean modemaps Time: 0.04 SEC. Adding Boolean modemaps compiling exported = : (%,%) -> Boolean Time: 0.01 SEC. compiling exported selectsum : % -> Union(acomp: A,bcomp: B) SUM;selectsum;$U;3 is replaced by x
Time: 0 SEC.
compiling exported in1 : A -> %
SUM;in1;A$;4 is replaced by CONS0a Time: 0 SEC. compiling exported in2 : B -> % SUM;in2;B$;5 is replaced by CONS1b
Time: 0 SEC.
Note: Domain A already in scope
augmenting A: Monoid
Note: Domain B already in scope
augmenting B: Monoid
compiling exported One : () -> %
Time: 0 SEC.
compiling exported * : (%,%) -> %
Time: 0.02 SEC.
compiling exported ** : (%,NonNegativeInteger) -> %
Time: 0.01 SEC.
Note: Domain A already in scope
augmenting A: Finite
Note: Domain B already in scope
augmenting B: Finite
compiling exported size : () -> NonNegativeInteger
Time: 0.01 SEC.
compiling exported index : PositiveInteger -> %
Time: 0 SEC.
compiling exported random : () -> %
Time: 0 SEC.
compiling exported lookup : % -> PositiveInteger
Time: 0.01 SEC.
compiling exported hash : % -> SingleInteger
Time: 0 SEC.
Note: Domain A already in scope
augmenting A: Group
Note: Domain B already in scope
augmenting B: Group
compiling exported inv : % -> %
Time: 0.01 SEC.
Note: Domain A already in scope
augmenting A: AbelianMonoid
Note: Domain B already in scope
augmenting B: AbelianMonoid
compiling exported Zero : () -> %
Time: 0.01 SEC.
compiling exported + : (%,%) -> %
Time: 0.01 SEC.
compiling exported * : (PositiveInteger,%) -> %
Time: 0.01 SEC.
Note: Domain A already in scope
augmenting A: AbelianGroup
Note: Domain B already in scope
augmenting B: AbelianGroup
compiling exported - : % -> %
Time: 0.01 SEC.
compiling exported - : (%,%) -> %
Time: 0.02 SEC.
compiling exported * : (Integer,%) -> %
Time: 0.01 SEC.
Note: Domain A already in scope
augmenting A: OrderedAbelianMonoidSup
Note: Domain B already in scope
augmenting B: OrderedAbelianMonoidSup
compiling exported sup : (%,%) -> %
Time: 0.01 SEC.
Note: Domain A already in scope
augmenting A: OrderedSet
Note: Domain B already in scope
augmenting B: OrderedSet
compiling exported < : (%,%) -> Boolean
Time: 0.02 SEC.
Note: Domain A already in scope
augmenting A: AbelianGroup
Note: Domain B already in scope
augmenting B: AbelianGroup
Note: Domain A already in scope
augmenting A: Finite
Note: Domain B already in scope
augmenting B: Finite
Note: Domain A already in scope
augmenting A: Group
Note: Domain B already in scope
augmenting B: Group
Note: Domain A already in scope
augmenting A: OrderedAbelianMonoidSup
Note: Domain B already in scope
augmenting B: OrderedAbelianMonoidSup
Note: Domain A already in scope
augmenting A: AbelianGroup
Note: Domain B already in scope
augmenting B: AbelianGroup
Note: Domain A already in scope
augmenting A: AbelianGroup
Note: Domain B already in scope
augmenting B: AbelianGroup
Note: Domain A already in scope
augmenting A: AbelianGroup
Note: Domain B already in scope
augmenting B: AbelianGroup
Note: Domain A already in scope
augmenting A: Group
Note: Domain B already in scope
augmenting B: Group
Note: Domain A already in scope
augmenting A: OrderedAbelianMonoidSup
Note: Domain B already in scope
augmenting B: OrderedAbelianMonoidSup
(time taken in buildFunctor:  20)
;;;     ***       |Sum| REDEFINED
;;;     ***       |Sum| REDEFINED
Time: 0.05 SEC.
Warnings:
[1] coerce:  acomp has no value
[2] coerce:  bcomp has no value
[3] *:  acomp has no value
[4] **:  acomp has no value
[5] inv:  acomp has no value
[6] +:  acomp has no value
[7] -:  acomp has no value
[8] sup:  acomp has no value
[9] <:  acomp has no value
[10] <:  bcomp has no value
Cumulative Statistics for Constructor Sum
Time: 0.26 seconds
finalizing NRLIB SUM
Processing Sum for Browser database:
-- selectsum : % -> Union(acomp: A,bcomp: B)
-- in1 : A -> %
--->-->Sum((in1 (% A))): Improper first word in comments: makefirst
"makefirst(a) \\undocumented"
-- in2 : B -> %
--->-->Sum((in2 (% B))): Improper first word in comments: makesecond
-- constructor
; compiling file "/var/aw/var/LatexWiki/SUM.NRLIB/code.lsp" (written 25 MAR 2013 07:34:26 AM):
; compiling (/VERSIONCHECK 2)
; compiling (DEFUN |SUM;coerce;$Of;1| ...) ; compiling (DEFUN |SUM;=;2$B;2| ...)
; compiling (PUT (QUOTE |SUM;selectsum;$U;3|) ...) ; compiling (DEFUN |SUM;selectsum;$U;3| ...)
; compiling (PUT (QUOTE |SUM;in1;A$;4|) ...) ; compiling (DEFUN |SUM;in1;A$;4| ...)
; compiling (PUT (QUOTE |SUM;in2;B$;5|) ...) ; compiling (DEFUN |SUM;in2;B$;5| ...)
; compiling (DEFUN |SUM;One;$;6| ...) ; compiling (DEFUN |SUM;*;3$;7| ...)
; compiling (DEFUN |SUM;**;$Nni$;8| ...)
; compiling (DEFUN |SUM;size;Nni;9| ...)
; compiling (DEFUN |SUM;index;Pi$;10| ...) ; compiling (DEFUN |SUM;random;$;11| ...)
; compiling (DEFUN |SUM;lookup;$Pi;12| ...) ; compiling (DEFUN |SUM;hash;$Si;13| ...)
; compiling (DEFUN |SUM;inv;2$;14| ...) ; compiling (DEFUN |SUM;Zero;$;15| ...)
; compiling (DEFUN |SUM;+;3$;16| ...) ; compiling (DEFUN |SUM;*;Pi2$;17| ...)
; compiling (DEFUN |SUM;-;2$;18| ...) ; compiling (DEFUN |SUM;-;3$;19| ...)
; compiling (DEFUN |SUM;*;I2$;20| ...) ; compiling (DEFUN |SUM;sup;3$;21| ...)
; compiling (DEFUN |SUM;<;2$B;22| ...) ; compiling (DEFUN |Sum| ...) ; compiling (DEFUN |Sum;| ...) ; compiling (MAKEPROP (QUOTE |Sum|) ...) ; /var/aw/var/LatexWiki/SUM.NRLIB/code.fasl written ; compilation finished in 0:00:00.092 ------------------------------------------------------------------------ Sum is now explicitly exposed in frame initial Sum will be automatically loaded when needed from /var/aw/var/LatexWiki/SUM.NRLIB/code.fasl axiom size()$Sum(PF 7,PF 13)
 (1)
Type: NonNegativeInteger?
axiom
size()$Sum(PF 7,Product(PF 3,PF 13))  (2) Type: NonNegativeInteger? axiom in1(10)$Sum(Integer,Integer)
 (3)
Type: Sum(Integer,Integer)
axiom
in1(10)$Sum(Integer,Integer) < in2(10)$Sum(Integer,Integer)
 (4)
Type: Boolean
axiom
sup(in1(99)$Sum(NNI,NNI), in2(10)$Sum(NNI,NNI))
 (5)
Type: Sum(NonNegativeInteger?,NonNegativeInteger?)

The CoTuple? domain constructor is intended to be the Categorical Dual of the Tuple domain constructor

)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
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
   Compiling OpenAxiom source code from file
COT abbreviates domain CoTuple
------------------------------------------------------------------------
initializing NRLIB COT for CoTuple
compiling into NRLIB COT
Adding $modemaps Adding S modemaps Adding Integer modemaps Adding NonNegativeInteger modemaps Adding PositiveInteger modemaps compiling exported coerce : % -> S COT;coerce;$S;1 is replaced by QCDR
Time: 0.02 SEC.
compiling exported inj : (NonNegativeInteger,S) -> %
COT;inj;NniS$;2 is replaced by CONS Time: 0 SEC. compiling exported ind : % -> NonNegativeInteger COT;ind;$Nni;3 is replaced by QCAR
Time: 0 SEC.
Note: Domain S already in scope
augmenting S: SetCategory
compiling exported = : (%,%) -> Boolean
Time: 0.01 SEC.
compiling exported coerce : % -> OutputForm
Time: 0.01 SEC.
Note: Domain S already in scope
augmenting S: Monoid
compiling exported One : () -> %
Time: 0 SEC.
compiling exported * : (%,%) -> %
Time: 0.01 SEC.
compiling exported ** : (%,NonNegativeInteger) -> %
Time: 0 SEC.
Note: Domain S already in scope
augmenting S: Group
compiling exported inv : % -> %
Time: 0.01 SEC.
Note: Domain S already in scope
augmenting S: AbelianMonoid
compiling exported Zero : () -> %
Time: 0.01 SEC.
compiling exported + : (%,%) -> %
Time: 0.01 SEC.
compiling exported * : (PositiveInteger,%) -> %
Time: 0 SEC.
Note: Domain S already in scope
augmenting S: AbelianGroup
compiling exported - : % -> %
Time: 0 SEC.
compiling exported - : (%,%) -> %
Time: 0.01 SEC.
compiling exported * : (Integer,%) -> %
Time: 0.01 SEC.
Note: Domain S already in scope
augmenting S: OrderedAbelianMonoidSup
compiling exported sup : (%,%) -> %
Time: 0 SEC.
Note: Domain S already in scope
augmenting S: OrderedSet
compiling exported < : (%,%) -> Boolean
Time: 0.01 SEC.
Note: Domain S already in scope
augmenting S: AbelianMonoid
Note: Domain S already in scope
augmenting S: AbelianGroup
Note: Domain S already in scope
augmenting S: AbelianMonoid
Note: Domain S already in scope
augmenting S: CancellationAbelianMonoid
Note: Domain S already in scope
augmenting S: Group
Note: Domain S already in scope
augmenting S: Monoid
Note: Domain S already in scope
augmenting S: OrderedAbelianMonoidSup
Note: Domain S already in scope
augmenting S: OrderedSet
Note: Domain S already in scope
augmenting S: SetCategory
(time taken in buildFunctor:  20)
;;;     ***       |CoTuple| REDEFINED
;;;     ***       |CoTuple| REDEFINED
Time: 0.04 SEC.
Warnings:
[1] Type NonNegativeInteger is not in scope. Import it
Cumulative Statistics for Constructor CoTuple
Time: 0.15 seconds
finalizing NRLIB COT
Processing CoTuple for Browser database:
-- inj : (NonNegativeInteger,S) -> %
--->-->CoTuple((inj (% (NonNegativeInteger) S))): Improper first word in comments: inject
-- ind : % -> NonNegativeInteger
--->-->CoTuple((ind ((NonNegativeInteger) %))): Improper first word in comments: index
-- constructor
; compiling file "/var/aw/var/LatexWiki/COT.NRLIB/code.lsp" (written 25 MAR 2013 07:34:27 AM):
; compiling (/VERSIONCHECK 2)
; compiling (PUT (QUOTE |COT;coerce;$S;1|) ...) ; compiling (DEFUN |COT;coerce;$S;1| ...)
; compiling (PUT (QUOTE |COT;inj;NniS$;2|) ...) ; compiling (DEFUN |COT;inj;NniS$;2| ...)
; compiling (PUT (QUOTE |COT;ind;$Nni;3|) ...) ; compiling (DEFUN |COT;ind;$Nni;3| ...)
; compiling (DEFUN |COT;=;2$B;4| ...) ; compiling (DEFUN |COT;coerce;$Of;5| ...)
; compiling (DEFUN |COT;One;$;6| ...) ; compiling (DEFUN |COT;*;3$;7| ...)
; compiling (DEFUN |COT;**;$Nni$;8| ...)
; compiling (DEFUN |COT;inv;2$;9| ...) ; compiling (DEFUN |COT;Zero;$;10| ...)
; compiling (DEFUN |COT;+;3$;11| ...) ; compiling (DEFUN |COT;*;Pi2$;12| ...)
; compiling (DEFUN |COT;-;2$;13| ...) ; compiling (DEFUN |COT;-;3$;14| ...)
; compiling (DEFUN |COT;*;I2$;15| ...) ; compiling (DEFUN |COT;sup;3$;16| ...)
; compiling (DEFUN |COT;<;2$B;17| ...) ; compiling (DEFUN |CoTuple| ...) ; compiling (DEFUN |CoTuple;| ...) ; compiling (MAKEPROP (QUOTE |CoTuple|) ...) ; /var/aw/var/LatexWiki/COT.NRLIB/code.fasl written ; compilation finished in 0:00:00.043 ------------------------------------------------------------------------ CoTuple is now explicitly exposed in frame initial CoTuple will be automatically loaded when needed from /var/aw/var/LatexWiki/COT.NRLIB/code.fasl axiom inj(1,10)  (6) Type: CoTuple? PositiveInteger? axiom inj(1,10) < inj(2,10)  (7) Type: Boolean axiom sup(inj(1,99), inj(2,10))$CoTuple(NNI)
 (8)
Type: CoTuple? NonNegativeInteger?

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
   Compiling OpenAxiom source code from file
DIRSUM abbreviates domain DirectSum
------------------------------------------------------------------------
initializing NRLIB DIRSUM for DirectSum
compiling into NRLIB DIRSUM
Adding $modemaps Adding S modemaps Adding Integer modemaps Adding NonNegativeInteger modemaps Adding PositiveInteger modemaps compiling exported coerce : S -> % DIRSUM;coerce;S$;1 is replaced by VECTOR00s
Time: 0.02 SEC.
compiling exported inj : (NonNegativeInteger,NonNegativeInteger,%) -> %
Time: 0.01 SEC.
compiling exported ind : % -> NonNegativeInteger
DIRSUM;ind;$Nni;3 is replaced by QVELTx0 Time: 0 SEC. compiling exported len : % -> NonNegativeInteger DIRSUM;len;$Nni;4 is replaced by QVELTx1
Time: 0 SEC.
Note: Domain S already in scope
augmenting S: SetCategory
compiling exported = : (%,%) -> Boolean
Time: 0.01 SEC.
compiling exported coerce : % -> OutputForm
Time: 0.01 SEC.
Note: Domain S already in scope
augmenting S: Monoid
compiling exported One : () -> %
Time: 0.01 SEC.
compiling exported * : (%,%) -> %
Time: 0.01 SEC.
compiling exported ** : (%,NonNegativeInteger) -> %
Time: 0 SEC.
Note: Domain S already in scope
augmenting S: Group
compiling exported inv : % -> %
Time: 0 SEC.
Note: Domain S already in scope
augmenting S: AbelianMonoid
compiling exported Zero : () -> %
Time: 0.01 SEC.
compiling exported + : (%,%) -> %
Time: 0 SEC.
compiling exported * : (PositiveInteger,%) -> %
Time: 0.01 SEC.
Note: Domain S already in scope
augmenting S: AbelianGroup
compiling exported - : % -> %
Time: 0 SEC.
compiling exported - : (%,%) -> %
Time: 0.02 SEC.
compiling exported * : (Integer,%) -> %
Time: 0 SEC.
Note: Domain S already in scope
augmenting S: OrderedAbelianMonoidSup
compiling exported sup : (%,%) -> %
Time: 0.01 SEC.
Note: Domain S already in scope
augmenting S: OrderedSet
compiling exported < : (%,%) -> Boolean
Time: 0.01 SEC.
Note: Domain S already in scope
augmenting S: AbelianMonoid
Note: Domain S already in scope
augmenting S: AbelianGroup
Note: Domain S already in scope
augmenting S: AbelianMonoid
Note: Domain S already in scope
augmenting S: CancellationAbelianMonoid
Note: Domain S already in scope
augmenting S: Group
Note: Domain S already in scope
augmenting S: Monoid
Note: Domain S already in scope
augmenting S: OrderedAbelianMonoidSup
Note: Domain S already in scope
augmenting S: OrderedSet
Note: Domain S already in scope
augmenting S: SetCategory
(time taken in buildFunctor:  10)
;;;     ***       |DirectSum| REDEFINED
;;;     ***       |DirectSum| REDEFINED
Time: 0.02 SEC.
Warnings:
[1] Type NonNegativeInteger is not in scope. Import it
Cumulative Statistics for Constructor DirectSum
Time: 0.15 seconds
finalizing NRLIB DIRSUM
Processing DirectSum for Browser database:
-- coerce : S -> %
--->-->DirectSum((coerce (% S))): Improper first word in comments: any
"any type is a 1-ary union"
-- inj : (NonNegativeInteger,NonNegativeInteger,%) -> %
--->-->DirectSum((inj (% (NonNegativeInteger) (NonNegativeInteger) %))): Improper first word in comments: inject
-- ind : % -> NonNegativeInteger
--->-->DirectSum((ind ((NonNegativeInteger) %))): Improper first word in comments: index
-- len : % -> NonNegativeInteger
-- constructor
; compiling file "/var/aw/var/LatexWiki/DIRSUM.NRLIB/code.lsp" (written 25 MAR 2013 07:34:27 AM):
; compiling (/VERSIONCHECK 2)
; compiling (PUT (QUOTE |DIRSUM;coerce;S$;1|) ...) ; compiling (DEFUN |DIRSUM;coerce;S$;1| ...)
; compiling (DEFUN |DIRSUM;inj;2Nni2$;2| ...) ; compiling (PUT (QUOTE |DIRSUM;ind;$Nni;3|) ...)
; compiling (DEFUN |DIRSUM;ind;$Nni;3| ...) ; compiling (PUT (QUOTE |DIRSUM;len;$Nni;4|) ...)
; compiling (DEFUN |DIRSUM;len;$Nni;4| ...) ; compiling (DEFUN |DIRSUM;=;2$B;5| ...)
; compiling (DEFUN |DIRSUM;coerce;$Of;6| ...) ; compiling (DEFUN |DIRSUM;One;$;7| ...)
; compiling (DEFUN |DIRSUM;*;3$;8| ...) ; compiling (DEFUN |DIRSUM;**;$Nni$;9| ...) ; compiling (DEFUN |DIRSUM;inv;2$;10| ...)
; compiling (DEFUN |DIRSUM;Zero;$;11| ...) ; compiling (DEFUN |DIRSUM;+;3$;12| ...)
; compiling (DEFUN |DIRSUM;*;Pi2$;13| ...) ; compiling (DEFUN |DIRSUM;-;2$;14| ...)
; compiling (DEFUN |DIRSUM;-;3$;15| ...) ; compiling (DEFUN |DIRSUM;*;I2$;16| ...)
; compiling (DEFUN |DIRSUM;sup;3$;17| ...) ; compiling (DEFUN |DIRSUM;<;2$B;18| ...)
; compiling (DEFUN |DirectSum| ...)
; compiling (DEFUN |DirectSum;| ...)
; compiling (MAKEPROP (QUOTE |DirectSum|) ...)
; /var/aw/var/LatexWiki/DIRSUM.NRLIB/code.fasl written
; compilation finished in 0:00:00.062
------------------------------------------------------------------------
DirectSum is now explicitly exposed in frame initial
DirectSum will be automatically loaded when needed from
/var/aw/var/LatexWiki/DIRSUM.NRLIB/code.fasl

axiom
inj(0,2,10)
 (9)
Type: DirectSum? Integer
axiom
inj(0,2,10) < inj(1,2,10)
 (10)
Type: Boolean
axiom
sup(inj(0,2,99), inj(1,2,10))\$DirectSum(NNI)
 (11)
Type: DirectSum? NonNegativeInteger?
axiom
a0:=inj(0,2,'a)
 (12)
Type: DirectSum? Polynomial Integer
axiom
len(a0)
 (13)
Type: PositiveInteger?
axiom
b1:=inj(1,2,'b)
 (14)
Type: DirectSum? Polynomial Integer
axiom
len(b1)
 (15)
Type: PositiveInteger?
axiom
a2:=inj(0,2,inj(0,2,'aa))
 (16)
Type: DirectSum? Polynomial Integer
axiom
len(a2)
 (17)
Type: PositiveInteger?
axiom
a3:=inj(1,2,inj(0,2,'ba))
 (18)
Type: DirectSum? Polynomial Integer
axiom
len(a3)
 (19)
Type: PositiveInteger?
axiom
b2:=inj(0,2,inj(1,2,'ab))
 (20)
Type: DirectSum? Polynomial Integer
axiom
len(b2)
 (21)
Type: PositiveInteger?
axiom
b3:=inj(1,2,inj(1,2,'bb))
 (22)
Type: DirectSum? Polynomial Integer
axiom
len(b3)
 (23)
Type: PositiveInteger?
axiom
inj(2,3,b3)
 (24)
Type: DirectSum? Polynomial Integer