Edit detail for Cartesian Product revision 2 of 4

axiom
)show Product
 Product(A: SetCategory,B: SetCategory)  is a domain constructor
 Abbreviation for Product is PRODUCT 
 This constructor is not exposed in this frame.
 Issue )edit /usr/local/lib/axiom/target/x86_64-unknown-linux/../../src/algebra/PRODUCT.spad to see algebra source code for PRODUCT 
------------------------------- Operations --------------------------------
 ?=? : (%,%) -> Boolean                coerce : % -> OutputForm
 hash : % -> SingleInteger             latex : % -> String
 makeprod : (A,B) -> %                 selectfirst : % -> A
 selectsecond : % -> B                 ?~=? : (%,%) -> Boolean
 ?*? : (%,%) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
 ?*? : (PositiveInteger,%) -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
 ?*? : (NonNegativeInteger,%) -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
 ?*? : (Integer,%) -> % if A has ABELGRP and B has ABELGRP
 ?**? : (%,PositiveInteger) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
 ?**? : (%,NonNegativeInteger) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
 ?**? : (%,Integer) -> % if A has GROUP and B has GROUP
 ?+? : (%,%) -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
 -? : % -> % if A has ABELGRP and B has ABELGRP
 ?-? : (%,%) -> % if A has ABELGRP and B has ABELGRP
 ?/? : (%,%) -> % if A has GROUP and B has GROUP
 ?<? : (%,%) -> Boolean if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
 ?<=? : (%,%) -> Boolean if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
 ?>? : (%,%) -> Boolean if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
 ?>=? : (%,%) -> Boolean if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
 1 : () -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
 0 : () -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
 ?^? : (%,PositiveInteger) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
 ?^? : (%,NonNegativeInteger) -> % if A has GROUP and B has GROUP or A has MONOID and B has MONOID
 ?^? : (%,Integer) -> % if A has GROUP and B has GROUP
 commutator : (%,%) -> % if A has GROUP and B has GROUP
 conjugate : (%,%) -> % if A has GROUP and B has GROUP
 enumerate : () -> List % if A has FINITE and B has FINITE
 index : PositiveInteger -> % if A has FINITE and B has FINITE
 inv : % -> % if A has GROUP and B has GROUP
 lookup : % -> PositiveInteger if A has FINITE and B has FINITE
 max : (%,%) -> % if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
 min : (%,%) -> % if A has OAMONS and B has OAMONS or A has ORDSET and B has ORDSET
 one? : % -> Boolean if A has GROUP and B has GROUP or A has MONOID and B has MONOID
 random : () -> % if A has FINITE and B has FINITE
 recip : % -> Union(%,"failed") if A has GROUP and B has GROUP or A has MONOID and B has MONOID
 sample : () -> % if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has GROUP and B has GROUP or A has MONOID and B has MONOID or A has OAMONS and B has OAMONS
 size : () -> NonNegativeInteger if A has FINITE and B has FINITE
 subtractIfCan : (%,%) -> Union(%,"failed") if A has ABELGRP and B has ABELGRP or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS
 sup : (%,%) -> % if A has OAMONS and B has OAMONS
 zero? : % -> Boolean if A has ABELGRP and B has ABELGRP or A has ABELMON and B has ABELMON or A has CABMON and B has CABMON or A has OAMONS and B has OAMONS

spad
)abbrev domain PRODUCT Product
Product (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
       makeprod     : (A,B) -> %
        ++ makeprod(a,b) \undocumented
       selectfirst  :   %   -> A
        ++ selectfirst(x) \undocumented
       selectsecond :   %   -> B
        ++ selectsecond(x) \undocumented
  T == add
    --representations
       Rep := Record(acomp:A,bcomp:B)
    --declarations
       x,y: %
       i: NonNegativeInteger
       p: NonNegativeInteger
       a: A
       b: B
       d: Integer
    --define
       coerce(x):OutputForm == paren [(x.acomp)::OutputForm,
                                      (x.bcomp)::OutputForm]
       x=y ==
           x.acomp = y.acomp => x.bcomp = y.bcomp
           false
       makeprod(a:A,b:B) :%   == [a,b]
       selectfirst(x:%) : A   == x.acomp
       selectsecond (x:%) : B == x.bcomp
       if A has Monoid and B has Monoid then
          1 == [1$A,1$B]
          x * y == [x.acomp * y.acomp,x.bcomp * y.bcomp]
          x ** p == [x.acomp ** p ,x.bcomp ** p]
       if A has Finite and B has Finite then
          size == size$A * size$B
          index(n) == [index((((n::Integer-1) quo size$B )+1)::PositiveInteger)$A,
                       index((((n::Integer-1) rem size$B )+1)::PositiveInteger)$B]
          random() == [random()$A,random()$B]
          lookup(x) == ((lookup(x.acomp)$A::Integer-1) * size$B::Integer +
                        lookup(x.bcomp)$B::Integer)::PositiveInteger
          hash(x) == hash(x.acomp)$A * size$B::SingleInteger + hash(x.bcomp)$B
       if A has Group and B has Group then
          inv(x) == [inv(x.acomp),inv(x.bcomp)]
       if A has AbelianMonoid and B has AbelianMonoid then
          0 == [0$A,0$B]
          x + y == [x.acomp + y.acomp,x.bcomp + y.bcomp]
          c:NonNegativeInteger * x == [c * x.acomp,c*x.bcomp]
       if A has CancellationAbelianMonoid and
          B has CancellationAbelianMonoid then
            subtractIfCan(x, y) : Union(%,"failed") ==
              (na:= subtractIfCan(x.acomp, y.acomp)) case "failed" => "failed"
              (nb:= subtractIfCan(x.bcomp, y.bcomp)) case "failed" => "failed"
              [na::A,nb::B]
       if A has AbelianGroup and B has AbelianGroup then
          - x == [- x.acomp,-x.bcomp]
          (x - y):% == [x.acomp - y.acomp,x.bcomp - y.bcomp]
          d * x == [d * x.acomp,d * x.bcomp]
       if A has OrderedAbelianMonoidSup and B has OrderedAbelianMonoidSup then
          sup(x,y) == [sup(x.acomp,y.acomp),sup(x.bcomp,y.bcomp)]
       if A has OrderedSet and B has OrderedSet then
          x < y ==
               xa:= x.acomp ; ya:= y.acomp
               xa < ya => true
               xb:= x.bcomp ; yb:= y.bcomp
               xa = ya => (xb < yb)
               false
--     coerce(x:%):Symbol ==
--      PrintableForm()
--      formList([x.acomp::Expression,x.bcomp::Expression])$PrintableForm

axiom
X:=Product(IntegerMod 3,Set PF 3)

axiom
size()$X

axiom
[index(i)$X for i in 1..size()$X::PositiveInteger]

Compiling function G1544 with type NonNegativeInteger -> Boolean

axiom
reduce(_and,[(lookup(index(i)$X)=i)::Boolean for i in 1..size()$X::PositiveInteger])

axiom
lookup(makeprod(2,[2])$X)

axiom
[random()$X for i in 1..5]