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

# Edit detail for SandBoxInequation revision 5 of 11

 1 2 3 4 5 6 7 8 9 10 11 Editor: Bill Page Time: 2008/06/11 04:48:51 GMT-7 Note: inequality

```changed:
-    not neq  == equation(neq.lhs,neq.rhs)
_not neq  == equation(neq.lhs,neq.rhs)

changed:
---   "x > y" to "inequality(y,x)", "x <= y" to "not lessThan(y,x)"
---   and "x >= y" to "not lessThan(x,y)".
--   "x > y" to "inequality(y,x)", "x <= y" to "not inequality(y,x)"
--   and "x >= y" to "not inequality(x,y)".

changed:
-    _not: \$ -> Union(\$, Equation S)
-    _not: Union(\$, Equation S) -> \$
_not: \$ -> \$

changed:
-    if S has SetCategory then
if S has OrderedSet then

coerce:Union(\$,Equation S)->OutputForm

changed:
-            ++ inequality leqn.
++ inequality leq.

changed:
-    Rep := Record(lhs: S, rhs: S)
-    leq1,leq2,leg: \$
Rep := Record(lhs: S, cmp:String ,rhs: S)
leq1,leq2,leq: \$

changed:
-    l:S < r:S      == [l, r]
-    inequality(l, r) == [l, r]    -- hack!  See comment above.
-    not(leq:\$):Union(\$,Equation S) == (leq.rhs < leq.lhs) pretend Union(\$,Equation S)
-    not(gre:Union(\$,Equation S)):\$ ==
-      leq := gre pretend \$
-      leq.rhs < leq.lhs
-
l:S < r:S      == [l, "<", r]
inequality(l, r) == [l, "<",  r]    -- hack!  See comment above.
_not(leq:\$):\$ ==
leq.cmp="<" => [leq.rhs, ">=", leq.lhs]
[leq.rhs, "<", leq.lhs]

changed:
-    if S has SetCategory then
if S has OrderedSet then

changed:
-        coerce(leq:\$):OutputForm == blankSeparate([eqn.lhs::OutputForm, "<", eqn.rhs::OutputForm])\$OutputForm
-        coerce(leq:Union(\$,Equation S):OutputForm == blankSeparate([eqn.lhs::OutputForm, "<=", eqn.rhs::OutputForm])\$OutputForm
coerce(leq:\$):OutputForm ==
leq.cmp="<" => blankSeparate([leq.lhs::OutputForm, "<", leq.rhs::OutputForm])\$OutputForm
blankSeparate([leq.lhs::OutputForm, ">=", leq.rhs::OutputForm])\$OutputForm

changed:
-            [subst(lhs leq1,eq2),subst(rhs leq1,eq2)]
[subst(lhs leq1,eq2),leq1.cmp,subst(rhs leq1,eq2)]

changed:
-lessThan(a,b)
-t1:=lessThan(2,3)
-t1::Boolean
-t2:=equation(2,3)
-t2::Boolean
w1:=inequality(a,b)
w2:=inequality(2,3)
w2::Boolean
not w1
w3:=not w2
w3::Boolean
```

```spad)abbrev domain NE Inequation
++ Author: Bill Page
++ Based on: Equation by Stephen M. Watt, enhancements by Johannes Grabmeier
++ Date Created: June 2008
++ Basic Operations: ~=
++ Related Domains: Equation
++ Also See:
++ AMS Classifications:
++ Keywords: inequation
++ Examples:
++ References:
++ Description:
++   Inequations as mathematical objects.  All properties of the basis domain,
++   e.g. being an abelian group are carried over the equation domain, by
++   performing the structural operations on the left and on the
++   right hand side.
--   The interpreter translates "~=" to "inequation".  Otherwise, it will
--   find a modemap for "~=" in the domain of the arguments.
Inequation(S: Type): public == private where
public ==> Type with
"~=": (S, S) -> \$
++ a~=b creates an inequation.
inequation: (S, S) -> \$
++ inequation(a,b) creates an inequation.
_not: \$ -> Equation(S)
swap: \$ -> \$
++ swap(neq) interchanges left and right hand side of inequation neq.
lhs: \$ -> S
++ lhs(neq) returns the left hand side of inequation neq.
rhs: \$ -> S
++ rhs(neq) returns the right hand side of inequation neq.
map: (S -> S, \$) -> \$
++ map(f,neq) constructs a new inequation by applying f to both
++ sides of neq. (f must be an injection)
if S has InnerEvalable(Symbol,S) then
InnerEvalable(Symbol,S)
if S has SetCategory then
SetCategory
CoercibleTo Boolean
if S has Evalable(S) then
eval: (\$, Equation S) -> \$
++ eval(neq, x=f) replaces x by f in inequation neq.
eval: (\$, List Equation S) -> \$
++ eval(neq, [x1=v1, ... xn=vn]) replaces xi by vi in inequation neq.
if S has AbelianSemiGroup then
"+": (S, \$) -> \$
++ x+neq produces a new inequation by adding x to both sides of
++ inequation neq.
"+": (\$, S) -> \$
++ neq+x produces a new inequation by adding x to both sides of
++ inequation neq.
if S has AbelianGroup then
"-": \$ -> \$
leftZero : \$ -> \$
++ leftZero(neq) subtracts the left hand side.
rightZero : \$ -> \$
++ rightZero(neq) subtracts the right hand side.
"-": (S, \$) -> \$
++ x-neq produces a new equation by subtracting both sides of
++ equation neq from x.
"-": (\$, S) -> \$
++ neq-x produces a new equation by subtracting x from  both sides of
++ equation neq.
if S has Monoid then
recip: \$ -> Union(\$,"failed")
leftOne : \$ -> Union(\$,"failed")
++ leftOne(neq) divides by the left hand side, if possible.
rightOne : \$ -> Union(\$,"failed")
++ rightOne(neq) divides by the right hand side, if possible.
if S has Group then
leftOne : \$ -> Union(\$,"failed")
++ leftOne(neq) divides by the left hand side.
rightOne : \$ -> Union(\$,"failed")
++ rightOne(neq) divides by the right hand side.
if S has IntegralDomain then
factorAndSplit : \$ -> List \$
++ factorAndSplit(neq) make the right hand side 0 and
++ factors the new left hand side. Each factor is equated
++ to 0 and put into the resulting list without repetitions.
if S has ExpressionSpace then
subst: (\$, Equation S) -> \$
++ subst(neq1,eq2) substitutes eq2 into both sides of neq1
++ the lhs of eq2 should be a kernel
Rep := Record(lhs: S, rhs: S)
neq1,neq2, neq: \$
eq2: Equation S
s : S
if S has IntegralDomain then
factorAndSplit neq ==
(S has factor : S -> Factored S) =>
neq0 := rightZero neq
[inequation(rcf.factor,0) for rcf in factors factor lhs neq0]
[neq]
l:S ~= r:S      == [l, r]
inequation(l, r) == [l, r]    -- hack!  See comment above.
_not neq  == equation(neq.lhs,neq.rhs)
lhs neq  == neq.lhs
rhs neq  == neq.rhs
swap neq == [rhs neq, lhs neq]
map(fn, neq)   == inequation(fn(neq.lhs), fn(neq.rhs))
if S has InnerEvalable(Symbol,S) then
s:Symbol
ls:List Symbol
x:S
lx:List S
eval(neq,s,x) == eval(neq.lhs,s,x) ~= eval(neq.rhs,s,x)
eval(neq,ls,lx) == eval(neq.lhs,ls,lx) ~= eval(neq.rhs,ls,lx)
if S has Evalable(S) then
eval(neq1:\$, eqn2:Equation S):\$ ==
eval(neq1.lhs, eqn2) ~= eval(neq1.rhs, eqn2)
eval(neq1:\$, leqn2:List Equation S):\$ ==
eval(neq1.lhs, leqn2) ~= eval(neq1.rhs, leqn2)
if S has SetCategory then
neq1 = neq2 == (neq1.lhs = neq2.lhs)@Boolean and
(neq1.rhs = neq2.rhs)@Boolean
coerce(neq:\$):OutputForm == blankSeparate([neq.lhs::OutputForm, "~=", neq.rhs::OutputForm])\$OutputForm
coerce(neq:\$):Boolean == neq.lhs ~= neq.rhs
if S has AbelianSemiGroup then
s + neq2 == s+neq2.lhs ~= s+neq2.rhs
neq1 + s == neq1.lhs+s ~= neq1.rhs+s
if S has AbelianGroup then
- neq == -neq.lhs ~= -neq.rhs
s - neq2 == s-neq2.lhs ~= s-neq2.rhs
neq1 - s == neq1.lhs-s ~= neq1.rhs-s
leftZero neq == 0 ~= rhs neq - lhs neq
rightZero neq == lhs neq - rhs neq ~= 0
if S has Monoid then
recip neq ==
(lh := recip lhs neq) case "failed" => "failed"
(rh := recip rhs neq) case "failed" => "failed"
[lh :: S, rh :: S]
leftOne neq ==
(re := recip lhs neq) case "failed" => "failed"
1 ~= rhs neq * re
rightOne neq ==
(re := recip rhs neq) case "failed" => "failed"
lhs neq * re ~= 1
if S has Group then
leftOne neq == 1 ~= rhs neq * inv rhs neq
rightOne neq == lhs neq * inv rhs neq ~= 1
if S has IntegralDomain then
factorAndSplit neq ==
(S has factor : S -> Factored S) =>
neq0 := rightZero neq
[inequation(rcf.factor,0) for rcf in factors factor lhs neq0]
(S has Polynomial Integer) =>
neq0 := rightZero neq
MF ==> MultivariateFactorize(Symbol, IndexedExponents Symbol, _
Integer, Polynomial Integer)
p : Polynomial Integer := (lhs neq0) pretend Polynomial Integer
[inequation((rcf.factor) pretend S,0) for rcf in factors factor(p)\$MF]
[neq]
if S has ExpressionSpace then
subst(neq1,eq2) ==
[subst(lhs neq1,eq2),subst(rhs neq1,eq2)]```
```   Compiling FriCAS source code from file
old system compiler.
NE abbreviates domain Inequation
processing macro definition public ==> -- the constructor category
processing macro definition private ==> -- the constructor capsule
------------------------------------------------------------------------
initializing NRLIB NE for Inequation
compiling into NRLIB NE
****** Domain: S already in scope
augmenting S: (IntegralDomain)
augmenting \$: (SIGNATURE \$ factorAndSplit ((List \$) \$))
compiling exported factorAndSplit : \$ -> List \$
augmenting S: (SIGNATURE S factor ((Factored S) S))
Time: 0.04 SEC.
compiling exported ~= : (S,S) -> \$
NE;~=;2S\$;2 is replaced by CONS
Time: 0 SEC.
compiling exported inequation : (S,S) -> \$
NE;inequation;2S\$;3 is replaced by CONS
Time: 0 SEC.
compiling exported not : \$ -> Equation S
Time: 0 SEC.
compiling exported lhs : \$ -> S
NE;lhs;\$S;5 is replaced by QCAR
Time: 0 SEC.
compiling exported rhs : \$ -> S
NE;rhs;\$S;6 is replaced by QCDR
Time: 0 SEC.
compiling exported swap : \$ -> \$
Time: 0 SEC.
compiling exported map : (S -> S,\$) -> \$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (InnerEvalable (Symbol) S)
compiling exported eval : (\$,Symbol,S) -> \$
Time: 0.02 SEC.
compiling exported eval : (\$,List Symbol,List S) -> \$
Time: 0.06 SEC.
****** Domain: S already in scope
augmenting S: (Evalable S)
compiling exported eval : (\$,Equation S) -> \$
Time: 0 SEC.
compiling exported eval : (\$,List Equation S) -> \$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (SetCategory)
compiling exported = : (\$,\$) -> Boolean
Time: 0.01 SEC.
compiling exported coerce : \$ -> OutputForm
Time: 0.01 SEC.
compiling exported coerce : \$ -> Boolean
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (AbelianSemiGroup)
augmenting \$: (SIGNATURE \$ + (\$ S \$))
augmenting \$: (SIGNATURE \$ + (\$ \$ S))
compiling exported + : (S,\$) -> \$
Time: 0 SEC.
compiling exported + : (\$,S) -> \$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (AbelianGroup)
augmenting \$: (SIGNATURE \$ - (\$ \$))
augmenting \$: (SIGNATURE \$ leftZero (\$ \$))
augmenting \$: (SIGNATURE \$ rightZero (\$ \$))
augmenting \$: (SIGNATURE \$ - (\$ S \$))
augmenting \$: (SIGNATURE \$ - (\$ \$ S))
compiling exported - : \$ -> \$
Time: 0 SEC.
compiling exported - : (S,\$) -> \$
Time: 0 SEC.
compiling exported - : (\$,S) -> \$
Time: 0 SEC.
compiling exported leftZero : \$ -> \$
Time: 0.01 SEC.
compiling exported rightZero : \$ -> \$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (Monoid)
augmenting \$: (SIGNATURE \$ recip ((Union \$ failed) \$))
augmenting \$: (SIGNATURE \$ leftOne ((Union \$ failed) \$))
augmenting \$: (SIGNATURE \$ rightOne ((Union \$ failed) \$))
compiling exported recip : \$ -> Union(\$,failed)
Time: 0 SEC.
compiling exported leftOne : \$ -> Union(\$,failed)
Time: 0 SEC.
compiling exported rightOne : \$ -> Union(\$,failed)
Time: 0.01 SEC.
****** Domain: S already in scope
augmenting S: (Group)
augmenting \$: (SIGNATURE \$ leftOne ((Union \$ failed) \$))
augmenting \$: (SIGNATURE \$ rightOne ((Union \$ failed) \$))
compiling exported leftOne : \$ -> Union(\$,failed)
Time: 0 SEC.
compiling exported rightOne : \$ -> Union(\$,failed)
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (IntegralDomain)
augmenting \$: (SIGNATURE \$ factorAndSplit ((List \$) \$))
compiling exported factorAndSplit : \$ -> List \$
augmenting S: (SIGNATURE S factor ((Factored S) S))
extension of ##1 to (Polynomial (Integer)) ignored
processing macro definition MF ==> MultivariateFactorize(Symbol,IndexedExponents Symbol,Integer,Polynomial Integer)
Time: 0.21 SEC.
****** Domain: S already in scope
augmenting S: (ExpressionSpace)
augmenting \$: (SIGNATURE \$ subst (\$ \$ (Equation S)))
compiling exported subst : (\$,Equation S) -> \$
Time: 0.07 SEC.
****** Domain: S already in scope
augmenting S: (Evalable S)
****** Domain: S already in scope
augmenting S: (SetCategory)
augmenting \$: (SIGNATURE \$ eval (\$ \$ (Equation S)))
augmenting \$: (SIGNATURE \$ eval (\$ \$ (List (Equation S))))
****** Domain: S already in scope
augmenting S: (AbelianGroup)
augmenting \$: (SIGNATURE \$ - (\$ \$))
augmenting \$: (SIGNATURE \$ leftZero (\$ \$))
augmenting \$: (SIGNATURE \$ rightZero (\$ \$))
augmenting \$: (SIGNATURE \$ - (\$ S \$))
augmenting \$: (SIGNATURE \$ - (\$ \$ S))
****** Domain: S already in scope
augmenting S: (AbelianSemiGroup)
augmenting \$: (SIGNATURE \$ + (\$ S \$))
augmenting \$: (SIGNATURE \$ + (\$ \$ S))
****** Domain: S already in scope
augmenting S: (ExpressionSpace)
augmenting \$: (SIGNATURE \$ subst (\$ \$ (Equation S)))
****** Domain: S already in scope
augmenting S: (InnerEvalable (Symbol) S)
****** Domain: S already in scope
augmenting S: (IntegralDomain)
augmenting \$: (SIGNATURE \$ factorAndSplit ((List \$) \$))
****** Domain: S already in scope
augmenting S: (Monoid)
augmenting \$: (SIGNATURE \$ recip ((Union \$ failed) \$))
augmenting \$: (SIGNATURE \$ leftOne ((Union \$ failed) \$))
augmenting \$: (SIGNATURE \$ rightOne ((Union \$ failed) \$))
****** Domain: S already in scope
augmenting S: (SetCategory)
(time taken in buildFunctor:  0)
;;;     ***       |Inequation| REDEFINED
;;;     ***       |Inequation| REDEFINED
Time: 0.02 SEC.
Semantic Errors:
 factorAndSplit:  rcf has two modes:
Warnings:
 factorAndSplit: not known that (IntegralDomain) is of mode (CATEGORY domain (SIGNATURE factorAndSplit ((List \$) \$)))
 factorAndSplit: not known that (IntegralDomain) is of mode (CATEGORY S (SIGNATURE factor ((Factored S) S)))
Cumulative Statistics for Constructor Inequation
Time: 0.46 seconds
finalizing NRLIB NE
Processing Inequation for Browser database:
--------(~= (\$ S S))---------
--------(inequation (\$ S S))---------
--->-->Inequation((not ((Equation S) \$))): Not documented!!!!
--------(swap (\$ \$))---------
--------(lhs (S \$))---------
--------(rhs (S \$))---------
--------(map (\$ (Mapping S S) \$))---------
--------(eval (\$ \$ (Equation S)))---------
--------(eval (\$ \$ (List (Equation S))))---------
--------(+ (\$ S \$))---------
--------(+ (\$ \$ S))---------
--->-->Inequation((- (\$ \$))): Not documented!!!!
--------(leftZero (\$ \$))---------
--------(rightZero (\$ \$))---------
--------(- (\$ S \$))---------
--------(- (\$ \$ S))---------
--->-->Inequation((recip ((Union \$ failed) \$))): Not documented!!!!
--------(leftOne ((Union \$ failed) \$))---------
--------(rightOne ((Union \$ failed) \$))---------
--------(leftOne ((Union \$ failed) \$))---------
--------(rightOne ((Union \$ failed) \$))---------
--------(factorAndSplit ((List \$) \$))---------
--------(subst (\$ \$ (Equation S)))---------
--------constructor---------
------------------------------------------------------------------------
Inequation is now explicitly exposed in frame initial
Inequation will be automatically loaded when needed from
/var/zope2/var/LatexWiki/NE.NRLIB/code```

It works but the LaTeX? output does not display ```axiom)set output tex on
)set output algebra on
inequation(a,b)
(1)  a ~= b``` (1)
Type: Inequation Symbol
```axiomt1:=inequation(2,3)
(2)  2 ~= 3``` (2)
Type: Inequation PositiveInteger?
```axiomt1::Boolean
(3)  true``` (3)
Type: Boolean
```axiomt2:=equation(2,3)
(4)  2= 3``` (4)
Type: Equation PositiveInteger?
```axiomt2::Boolean
(5)  false``` (5)
Type: Boolean
```axioms1:= not t1
(6)  2= 3``` (6)
Type: Equation PositiveInteger?
```axioms1::Boolean
(7)  false``` (7)
Type: Boolean
```axiomt1*4
There are 34 exposed and 23 unexposed library operations named *
having 2 argument(s) but none was determined to be applicable.
Use HyperDoc Browse, or issue
)display op *
package-calling the operation or using coercions on the arguments
will allow you to apply the operation.
Cannot find a definition or applicable library operation named *
with argument type(s)
Inequation PositiveInteger
PositiveInteger
Perhaps you should use "@" to indicate the required return type,
or "\$" to specify which version of the function you need.
t1+t2
There are 13 exposed and 5 unexposed library operations named +
having 2 argument(s) but none was determined to be applicable.
Use HyperDoc Browse, or issue
)display op +
package-calling the operation or using coercions on the arguments
will allow you to apply the operation.
Cannot find a definition or applicable library operation named +
with argument type(s)
Inequation PositiveInteger
Equation PositiveInteger
Perhaps you should use "@" to indicate the required return type,
or "\$" to specify which version of the function you need.
t1*t2
There are 34 exposed and 23 unexposed library operations named *
having 2 argument(s) but none was determined to be applicable.
Use HyperDoc Browse, or issue
)display op *
package-calling the operation or using coercions on the arguments
will allow you to apply the operation.
Cannot find a definition or applicable library operation named *
with argument type(s)
Inequation PositiveInteger
Equation PositiveInteger
Perhaps you should use "@" to indicate the required return type,
or "\$" to specify which version of the function you need.```

```spad)abbrev domain LT Inequality
++ Author: Bill Page
++ Based on: Equation by Stephen M. Watt, enhancements by Johannes Grabmeier
++ Date Created: June 2008
++ Basic Operations: <
++ Related Domains: Equation Inequation
++ Also See:
++ AMS Classifications:
++ Keywords: inequality
++ Examples:
++ References:
++ Description:
++   Inequalities as mathematical objects.  All properties of the basis domain,
++   e.g. being an abelian group are carried over the equation domain, by
++   performing the structural operations on the left and on the
++   right hand side.
--   The interpreter translates "x < y" to "inequality(x,y)",
--   "x > y" to "inequality(y,x)", "x <= y" to "not inequality(y,x)"
--   and "x >= y" to "not inequality(x,y)".
Inequality(S: Type): public == private where
public ==> Type with
"<": (S, S) -> \$
++ a~=b creates an inequality.
inequality: (S, S) -> \$
++ equality(a,b) creates an inequality.
_not: \$ -> \$
lhs: \$ -> S
++ lhs(leq) returns the left hand side of inequality leq.
rhs: \$ -> S
++ rhs(leq) returns the right hand side of inequality leq.
if S has InnerEvalable(Symbol,S) then
InnerEvalable(Symbol,S)
if S has OrderedSet then
SetCategory
CoercibleTo Boolean
if S has Evalable(S) then
eval: (\$, Equation S) -> \$
++ eval(leq, x=f) replaces x by f in inequality leq.
eval: (\$, List Equation S) -> \$
++ eval(leq, [x1=v1, ... xn=vn]) replaces xi by vi in inequality leq.
coerce:Union(\$,Equation S)->OutputForm
if S has AbelianSemiGroup then
"+": (S, \$) -> \$
++ x+leq produces a new inequality by adding x to both sides of
++ inequality leq.
"+": (\$, S) -> \$
++ leq+x produces a new inequality by adding x to both sides of
++ inequality leq.
if S has AbelianGroup then
"-": \$ -> \$
leftZero : \$ -> \$
++ leftZero(leq) subtracts the left hand side.
rightZero : \$ -> \$
++ rightZero(leq) subtracts the right hand side.
"-": (S, \$) -> \$
++ x-leq produces a new inquality by subtracting both sides of
++ inequality leq from x.
"-": (\$, S) -> \$
++ leq-x produces a new inequality by subtracting x from both sides of
++ inequality leq.
if S has ExpressionSpace then
subst: (\$, Equation S) -> \$
++ subst(leq,eq2) substitutes eq2 into both sides of leq
++ the lhs of eq2 should be a kernel
Rep := Record(lhs: S, cmp:String ,rhs: S)
leq1,leq2,leq: \$
eq2: Equation S
s : S
l:S < r:S      == [l, "<", r]
inequality(l, r) == [l, "<",  r]    -- hack!  See comment above.
_not(leq:\$):\$ ==
leq.cmp="<" => [leq.rhs, ">=", leq.lhs]
[leq.rhs, "<", leq.lhs]
lhs leq        == leq.lhs
rhs leq        == leq.rhs
if S has InnerEvalable(Symbol,S) then
s:Symbol
ls:List Symbol
x:S
lx:List S
eval(leq,s,x) == eval(leq.lhs,s,x) < eval(leq.rhs,s,x)
eval(leq,ls,lx) == eval(leq.lhs,ls,lx) < eval(leq.rhs,ls,lx)
if S has Evalable(S) then
eval(leq:\$, eqn2:Equation S):\$ ==
eval(leq.lhs, eqn2) < eval(leq.rhs, eqn2)
eval(leq:\$, eqn2:List Equation S):\$ ==
eval(leq.lhs, eqn2) < eval(leq.rhs, eqn2)
if S has OrderedSet then
leq1 = leq2 == (leq1.lhs = leq2.lhs)@Boolean and
(leq1.rhs = leq2.rhs)@Boolean
coerce(leq:\$):OutputForm ==
leq.cmp="<" => blankSeparate([leq.lhs::OutputForm, "<", leq.rhs::OutputForm])\$OutputForm
blankSeparate([leq.lhs::OutputForm, ">=", leq.rhs::OutputForm])\$OutputForm
coerce(leq:\$):Boolean == leq.lhs < leq.rhs
if S has AbelianSemiGroup then
s + leq2 == s+leq2.lhs < s+leq2.rhs
leq1 + s == leq1.lhs+s < leq1.rhs+s
if S has AbelianGroup then
- leq ==  (-rhs leq) < (- lhs leq)
leftZero leq == 0 < rhs leq - lhs leq
rightZero leq == lhs leq - rhs leq < 0
s - leq2 ==  s-leq2.rhs < s-leq2.lhs
leq1 - s == leq1.lhs-s < leq1.rhs-s
if S has ExpressionSpace then
subst(leq1,eq2) ==
[subst(lhs leq1,eq2),leq1.cmp,subst(rhs leq1,eq2)]```
```   Compiling FriCAS source code from file
old system compiler.
LT abbreviates domain Inequality
processing macro definition public ==> -- the constructor category
processing macro definition private ==> -- the constructor capsule
------------------------------------------------------------------------
initializing NRLIB LT for Inequality
compiling into NRLIB LT
compiling exported < : (S,S) -> \$
LT;<;2S\$;1 is replaced by VECTORl<r
Time: 0.01 SEC.
compiling exported inequality : (S,S) -> \$
LT;inequality;2S\$;2 is replaced by VECTORl<r
Time: 0.07 SEC.
compiling exported not : \$ -> \$
Time: 0 SEC.
compiling exported lhs : \$ -> S
LT;lhs;\$S;4 is replaced by QVELTleq0
Time: 0 SEC.
compiling exported rhs : \$ -> S
LT;rhs;\$S;5 is replaced by QVELTleq2
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (InnerEvalable (Symbol) S)
compiling exported eval : (\$,Symbol,S) -> \$
Time: 0.01 SEC.
compiling exported eval : (\$,List Symbol,List S) -> \$
Time: 0.01 SEC.
****** Domain: S already in scope
augmenting S: (Evalable S)
compiling exported eval : (\$,Equation S) -> \$
Time: 0 SEC.
compiling exported eval : (\$,List Equation S) -> \$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (OrderedSet)
augmenting \$: (SIGNATURE \$ coerce ((OutputForm) (Union \$ (Equation S))))
compiling exported = : (\$,\$) -> Boolean
Time: 0 SEC.
compiling exported coerce : \$ -> OutputForm
Time: 0.03 SEC.
compiling exported coerce : \$ -> Boolean
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (AbelianSemiGroup)
augmenting \$: (SIGNATURE \$ + (\$ S \$))
augmenting \$: (SIGNATURE \$ + (\$ \$ S))
compiling exported + : (S,\$) -> \$
Time: 0 SEC.
compiling exported + : (\$,S) -> \$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (AbelianGroup)
augmenting \$: (SIGNATURE \$ - (\$ \$))
augmenting \$: (SIGNATURE \$ leftZero (\$ \$))
augmenting \$: (SIGNATURE \$ rightZero (\$ \$))
augmenting \$: (SIGNATURE \$ - (\$ S \$))
augmenting \$: (SIGNATURE \$ - (\$ \$ S))
compiling exported - : \$ -> \$
Time: 0.01 SEC.
compiling exported leftZero : \$ -> \$
Time: 0 SEC.
compiling exported rightZero : \$ -> \$
Time: 0 SEC.
compiling exported - : (S,\$) -> \$
Time: 0 SEC.
compiling exported - : (\$,S) -> \$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (ExpressionSpace)
augmenting \$: (SIGNATURE \$ subst (\$ \$ (Equation S)))
compiling exported subst : (\$,Equation S) -> \$
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (Evalable S)
****** Domain: S already in scope
augmenting S: (OrderedSet)
augmenting \$: (SIGNATURE \$ eval (\$ \$ (Equation S)))
augmenting \$: (SIGNATURE \$ eval (\$ \$ (List (Equation S))))
augmenting \$: (SIGNATURE \$ coerce ((OutputForm) (Union \$ (Equation S))))
****** Domain: S already in scope
augmenting S: (AbelianGroup)
augmenting \$: (SIGNATURE \$ - (\$ \$))
augmenting \$: (SIGNATURE \$ leftZero (\$ \$))
augmenting \$: (SIGNATURE \$ rightZero (\$ \$))
augmenting \$: (SIGNATURE \$ - (\$ S \$))
augmenting \$: (SIGNATURE \$ - (\$ \$ S))
****** Domain: S already in scope
augmenting S: (AbelianSemiGroup)
augmenting \$: (SIGNATURE \$ + (\$ S \$))
augmenting \$: (SIGNATURE \$ + (\$ \$ S))
****** Domain: S already in scope
augmenting S: (ExpressionSpace)
augmenting \$: (SIGNATURE \$ subst (\$ \$ (Equation S)))
****** Domain: S already in scope
augmenting S: (InnerEvalable (Symbol) S)
****** Domain: S already in scope
augmenting S: (OrderedSet)
augmenting \$: (SIGNATURE \$ coerce ((OutputForm) (Union \$ (Equation S))))
(time taken in buildFunctor:  0)
;;;     ***       |Inequality| REDEFINED
;;;     ***       |Inequality| REDEFINED
Time: 0.01 SEC.
Cumulative Statistics for Constructor Inequality
Time: 0.15 seconds
finalizing NRLIB LT
Processing Inequality for Browser database:
--------(< (\$ S S))---------
--->-->Inequality((< (\$ S S))): Improper initial operator in comments: ~=
"a~=b creates an inequality."
--------(inequality (\$ S S))---------
--->-->Inequality((inequality (\$ S S))): Improper first word in comments: equality
"equality(a,{}\\spad{b}) creates an inequality."
--->-->Inequality((not (\$ \$))): Not documented!!!!
--------(lhs (S \$))---------
--------(rhs (S \$))---------
--------(eval (\$ \$ (Equation S)))---------
--------(eval (\$ \$ (List (Equation S))))---------
--->-->Inequality((coerce ((OutputForm) (Union \$ (Equation S))))): Not documented!!!!
--------(+ (\$ S \$))---------
--------(+ (\$ \$ S))---------
--->-->Inequality((- (\$ \$))): Not documented!!!!
--------(leftZero (\$ \$))---------
--------(rightZero (\$ \$))---------
--------(- (\$ S \$))---------
--------(- (\$ \$ S))---------
--------(subst (\$ \$ (Equation S)))---------
--------constructor---------
------------------------------------------------------------------------
Inequality is now explicitly exposed in frame initial
Inequality will be automatically loaded when needed from
/var/zope2/var/LatexWiki/LT.NRLIB/code```

It works but the LaTeX? output does not display ```axiom)set output tex on
)set output algebra on
w1:=inequality(a,b)
(8)  a < b``` (8)
Type: Inequality Symbol
```axiomw2:=inequality(2,3)
(9)  2 < 3``` (9)
Type: Inequality PositiveInteger?
```axiomw2::Boolean
(10)  true``` (10)
Type: Boolean
```axiomnot w1
(11)  b >= a``` (11)
Type: Inequality Symbol
```axiomw3:=not w2
(12)  3 >= 2``` (12)
Type: Inequality PositiveInteger?
```axiomw3::Boolean
(13)  false``` (13)
Type: Boolean