help links subscribe changes refresh edit

	SandBox	Cartesian Product
SandBoxSqrt ←	↑		→ SandBoxSurfaceComplex

SandBoxSum

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

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

spad

   Compiling OpenAxiom source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8219446594478290117-25px001.spad
      using Spad compiler.
   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.

   Adding Boolean modemaps
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: Monoid
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: Monoid
   compiling exported One : () -> %
Time: 0 SEC.

   compiling exported * : (%,%) -> %
   Adding OutputForm modemaps
Time: 0.02 SEC.

   compiling exported ** : (%,NonNegativeInteger) -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: Finite
   Adding B modemaps
 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.

   Adding SingleInteger modemaps
   compiling exported hash : % -> SingleInteger
Time: 0 SEC.

   Adding Boolean modemaps
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: Group
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: Group
   compiling exported inv : % -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: AbelianMonoid
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: AbelianMonoid
   compiling exported Zero : () -> %
Time: 0.01 SEC.

   compiling exported + : (%,%) -> %
   Adding OutputForm modemaps
Time: 0.01 SEC.

   compiling exported * : (PositiveInteger,%) -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: AbelianGroup
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: AbelianGroup
   compiling exported - : % -> %
Time: 0.01 SEC.

   compiling exported - : (%,%) -> %
   Adding OutputForm modemaps
Time: 0.02 SEC.

   compiling exported * : (Integer,%) -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: OrderedAbelianMonoidSup
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: OrderedAbelianMonoidSup
   compiling exported sup : (%,%) -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: OrderedSet
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: OrderedSet
   compiling exported < : (%,%) -> Boolean
Time: 0.02 SEC.

   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: AbelianGroup
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: AbelianGroup
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: Finite
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: Finite
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: Group
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: Group
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: OrderedAbelianMonoidSup
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: OrderedAbelianMonoidSup
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: AbelianGroup
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: AbelianGroup
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: AbelianGroup
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: AbelianGroup
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: AbelianGroup
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: AbelianGroup
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: Group
   Adding B modemaps
 Note: Domain B already in scope
   augmenting B: Group
   Adding A modemaps
 Note: Domain A already in scope
   augmenting A: OrderedAbelianMonoidSup
   Adding B modemaps
 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
"makesecond(\\spad{b}) \\undocumented"
     -- 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)

$\label{eq1}20$

(1)

Type: NonNegativeInteger?

axiom

size()$Sum(PF 7,Product(PF 3,PF 13))

$\label{eq2}46$

(2)

Type: NonNegativeInteger?

axiom

in1(10)$Sum(Integer,Integer)

$\label{eq3}{10}_{1}$

(3)

Type: Sum(Integer,Integer)

axiom

in1(10)$Sum(Integer,Integer) < in2(10)$Sum(Integer,Integer)

$\label{eq4} \mbox{\rm true}$

(4)

Type: Boolean

axiom

sup(in1(99)$Sum(NNI,NNI), in2(10)$Sum(NNI,NNI))

$\label{eq5}{10}_{2}$

(5)

Type: Sum(NonNegativeInteger?,NonNegativeInteger?)

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

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

spad

   Compiling OpenAxiom source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2899346089849641949-25px003.spad
      using Spad compiler.
   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.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: SetCategory
   compiling exported = : (%,%) -> Boolean
Time: 0.01 SEC.

   Adding OutputForm modemaps
   compiling exported coerce : % -> OutputForm
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: Monoid
   compiling exported One : () -> %
Time: 0 SEC.

   compiling exported * : (%,%) -> %
   Adding OutputForm modemaps
Time: 0.01 SEC.

   compiling exported ** : (%,NonNegativeInteger) -> %
Time: 0 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: Group
   compiling exported inv : % -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianMonoid
   compiling exported Zero : () -> %
Time: 0.01 SEC.

   compiling exported + : (%,%) -> %
   Adding OutputForm modemaps
Time: 0.01 SEC.

   compiling exported * : (PositiveInteger,%) -> %
Time: 0 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianGroup
   compiling exported - : % -> %
Time: 0 SEC.

   compiling exported - : (%,%) -> %
   Adding OutputForm modemaps
Time: 0.01 SEC.

   compiling exported * : (Integer,%) -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: OrderedAbelianMonoidSup
   compiling exported sup : (%,%) -> %
Time: 0 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: OrderedSet
   compiling exported < : (%,%) -> Boolean
Time: 0.01 SEC.

   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianMonoid
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianGroup
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianMonoid
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: CancellationAbelianMonoid
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: Group
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: Monoid
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: OrderedAbelianMonoidSup
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: OrderedSet
   Adding S modemaps
 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
"inject(\\spad{x},{}\\spad{n}) returns \\spad{x} as an element of the \\spad{n}-th component of the CoTuple. CoTuples are 0-based"
     -- ind : % -> NonNegativeInteger
--->-->CoTuple((ind ((NonNegativeInteger) %))): Improper first word in comments: index
"index(\\spad{x}) returns the component number of \\spad{x} in the CoTuple"
     -- 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)

$\label{eq6}{10}_{1}$

(6)

Type: CoTuple? PositiveInteger?

axiom

inj(1,10) < inj(2,10)

$\label{eq7} \mbox{\rm true}$

(7)

Type: Boolean

axiom

sup(inj(1,99), inj(2,10))$CoTuple(NNI)

$\label{eq8}{10}_{2}$

(8)

Type: CoTuple? NonNegativeInteger?

The DirectSum? domain constructor implements an associative (flat) DirectSum? domain that is the dual to DirectProduct?.

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

spad

   Compiling OpenAxiom source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4753740315816852461-25px005.spad
      using Spad compiler.
   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,%) -> %
   Adding Boolean modemaps
   Adding OutputForm modemaps
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.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: SetCategory
   compiling exported = : (%,%) -> Boolean
Time: 0.01 SEC.

   Adding OutputForm modemaps
   compiling exported coerce : % -> OutputForm
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: Monoid
   compiling exported One : () -> %
Time: 0.01 SEC.

   compiling exported * : (%,%) -> %
   Adding OutputForm modemaps
Time: 0.01 SEC.

   compiling exported ** : (%,NonNegativeInteger) -> %
Time: 0 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: Group
   compiling exported inv : % -> %
Time: 0 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianMonoid
   compiling exported Zero : () -> %
Time: 0.01 SEC.

   compiling exported + : (%,%) -> %
   Adding OutputForm modemaps
Time: 0 SEC.

   compiling exported * : (PositiveInteger,%) -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianGroup
   compiling exported - : % -> %
Time: 0 SEC.

   compiling exported - : (%,%) -> %
   Adding OutputForm modemaps
Time: 0.02 SEC.

   compiling exported * : (Integer,%) -> %
Time: 0 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: OrderedAbelianMonoidSup
   compiling exported sup : (%,%) -> %
Time: 0.01 SEC.

   Adding Boolean modemaps
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: OrderedSet
   compiling exported < : (%,%) -> Boolean
Time: 0.01 SEC.

   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianMonoid
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianGroup
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: AbelianMonoid
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: CancellationAbelianMonoid
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: Group
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: Monoid
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: OrderedAbelianMonoidSup
   Adding S modemaps
 Note: Domain S already in scope
   augmenting S: OrderedSet
   Adding S modemaps
 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
"inject(\\spad{i},{}\\spad{n},{}\\spad{x}) injects the \\spad{m}-CoTuple element \\spad{x} as the (\\spad{m} + \\spad{i})\\spad{-}th component of the (\\spad{n+m})-CoTuple."
     -- ind : % -> NonNegativeInteger
--->-->DirectSum((ind ((NonNegativeInteger) %))): Improper first word in comments: index
"index(\\spad{x}) returns the component number of \\spad{x} in the CoTuple"
     -- 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)

$\label{eq9}{10}_{0}$

(9)

Type: DirectSum? Integer

axiom

inj(0,2,10) < inj(1,2,10)

$\label{eq10} \mbox{\rm true}$

(10)

Type: Boolean

axiom

sup(inj(0,2,99), inj(1,2,10))$DirectSum(NNI)

$\label{eq11}{10}_{1}$

(11)

Type: DirectSum? NonNegativeInteger?

axiom

a0:=inj(0,2,'a)

$\label{eq12}a_{0}$

(12)

Type: DirectSum? Polynomial Integer

axiom

len(a0)

$\label{eq13}2$

(13)

Type: PositiveInteger?

axiom

b1:=inj(1,2,'b)

$\label{eq14}b_{1}$

(14)

Type: DirectSum? Polynomial Integer

axiom

len(b1)

$\label{eq15}2$

(15)

Type: PositiveInteger?

axiom

a2:=inj(0,2,inj(0,2,'aa))

$\label{eq16}aa_{2}$

(16)

Type: DirectSum? Polynomial Integer

axiom

len(a2)

$\label{eq17}4$

(17)

Type: PositiveInteger?

axiom

a3:=inj(1,2,inj(0,2,'ba))

$\label{eq18}ba_{3}$

(18)

Type: DirectSum? Polynomial Integer

axiom

len(a3)

$\label{eq19}4$

(19)

Type: PositiveInteger?

axiom

b2:=inj(0,2,inj(1,2,'ab))

$\label{eq20}ab_{2}$

(20)

Type: DirectSum? Polynomial Integer

axiom

len(b2)

$\label{eq21}4$

(21)

Type: PositiveInteger?

axiom

b3:=inj(1,2,inj(1,2,'bb))

$\label{eq22}bb_{3}$

(22)

Type: DirectSum? Polynomial Integer

axiom

len(b3)

$\label{eq23}4$

(23)

Type: PositiveInteger?

axiom

inj(2,3,b3)

$\label{eq24}bb_{6}$

(24)

Type: DirectSum? Polynomial Integer