Edit detail for SandBoxProp revision 1 of 1

\begin{spad}
)abbrev domain INEQTY InEquality
++ Author: kfp
++ Date Created: Sun Oct 26 02:21:23 CEST 2014
++ License: BSD (same as Axiom)
++ Date Last Updated:
++ Basic Operations: 
++ Related Domains: 
++ Also See:
++ AMS Classifications:
++ Keywords: 
++ Examples:
++ References:
++
++ Description:
++ 
++
InEquality(S:Comparable) : Exports == Implementation where
  OF ==> OutputForm  
  Exports == Join(Comparable , CoercibleTo OutputForm) with
    "<"  : (S,S) -> %
      ++ < means lesser than
    "<=" : (S,S) -> %
      ++ <= means lesser than or equal
    ">"  : (S,S) -> %
      ++ > means greater than
    ">=" : (S,S) -> %
      ++ >= means greater than or equal
    eql  : (S,S) -> %
      ++ = means equal
    neq  : (S,S) -> %
      ++ neq means not equal.
    lhs  : % -> S
      ++ lhs returns the left hand side of the inequality
    rhs  : % -> S
      ++ rhs returns the right hand side of the inequality
    rel  : % -> Symbol
      ++ rel returns the inequality (relation) symbol 
    converse : % -> %
      ++ converse inequality 
    coerce : % -> OF
      ++ coerce to output form
  Implementation ==  add 
    Rep := Record(rel:Symbol , lhs : S, rhs : S)
    s:List(Symbol):=['<,'<=,'>,'>=,'=,'~=]
    l:S <  r:S == [s.1, l, r]$Rep
    l:S <= r:S == [s.2, l, r]$Rep
    l:S >  r:S == [s.3, l, r]$Rep
    l:S >= r:S == [s.4, l, r]$Rep
    eql(l:S,r:S) == [s.5, l, r]$Rep
    neq(l:S,r:S) == [s.6, l, r]$Rep
    lhs x == x.lhs
    rhs x == x.rhs
    rel x == x.rel
    converse x == 
      x.rel = s.1 => [s.3, x.rhs, x.lhs]$Rep
      x.rel = s.2 => [s.4, x.rhs, x.lhs]$Rep
      x.rel = s.3 => [s.1, x.rhs, x.lhs]$Rep
      x.rel = s.4 => [s.2, x.rhs, x.lhs]$Rep
      x.rel = s.5 => [s.5, x.rhs, x.lhs]$Rep
      x.rel = s.6 => [s.6, x.rhs, x.lhs]$Rep
    coerce(x:%):OF == 
      hconcat [x.lhs::OF," ", x.rel::OF, " ", x.rhs::OF] 

)abbrev domain PROP Prop
++ Prop is the domain of Propositions over a type T
Prop(T:Comparable) : Exports == Implementation where
  S   ==> Symbol
  PI  ==> PositiveInteger
  EQT ==> InEquality(T)
  TT  ==> Union(S,T,PI,EQT)
  Exports == with
        assert : InEquality(T) -> %
          ++ assert an equation of type InEquality(T)
        assert : Equation(T) -> %
          ++ assert an equation of type Equation(T) (convenience)       
        And : (%,%) -> %
          ++ And means the logical connective and
        Or  : (%,%) -> %
          ++ Or means the logical connective or
        Imp : (%,%) -> %
          ++ Imp means the logical connective implies
        Eqv : (%,%) -> %
          ++ Eqv means the logical connective equivalent
        Not : % -> %
          ++ Not means negation not
        All : (Symbol,%) -> %
          ++ All means the universal quantifier forall
        Ex  : (Symbol,%) -> %
          ++ Ex means the existential quantifier exists
        coerce : % -> OutputForm
          ++ coerce to output form
        qvars : % -> List(TT)
          ++ qvars lists all quantifier variables
        nnf : % -> %
          ++ nnf means negation normal form nnf

  Implementation == add
BinaryTree(TT) add 
    Rep := BinaryTree(TT)
    -- map x in TT to Rep
    iD(x:TT):%   == binaryTree(x)$Rep
    rs:List(Symbol):=['<,'<=,'>,'>=,'=,'~=]

    -----------------------
Op id's
    -- 1  ..... and
    -- 2  ..... or
    -- 3  ..... implies
    -- 4  ..... equivalent
    -- 5  ..... not
    -- 6  ..... forall
    -- 7  ..... exists
    -- 8,9 .... reserved
    -- 10 ..... equality
    -- 11 ..... neq
    -- 12 ..... lt
    -- 13 ..... leq
    -- 14 ..... gt
    -- 15 ..... geq
    -----------------------

    -- assert an element of type Equation(T)
    assert(s:Equation(T)):% == binaryTree(iD lhs s,10,iD rhs s)$Rep
    assert(s:EQT):% == 
      rel s = rs.1 => binaryTree(iD lhs s,12,iD rhs s)$Rep
      rel s = rs.2 => binaryTree(iD lhs s,13,iD rhs s)$Rep
      rel s = rs.3 => binaryTree(iD lhs s,14,iD rhs s)$Rep
      rel s = rs.4 => binaryTree(iD lhs s,15,iD rhs s)$Rep
      rel s = rs.5 => binaryTree(iD lhs s,10,iD rhs s)$Rep
      rel s = rs.6 => binaryTree(iD lhs s,11,iD rhs s)$Rep
    -- variable, the only nodes without left/right
    var(x:S):%     == binaryTree(x)$Rep
    And(p:%,q:%):% == binaryTree(p,1,q)$Rep
    Or (p:%,q:%):% == binaryTree(p,2,q)$Rep
    Imp(p:%,q:%):% == binaryTree(p,3,q)$Rep
    Eqv(p:%,q:%):% == binaryTree(p,4,q)$Rep
    Not(p:%):%     == binaryTree(p,5,empty())$Rep
    All(x:S,p:%):% == binaryTree(var x,6,p)$Rep
    Ex (x:S,p:%):% == binaryTree(var x,7,p)$Rep
    coerce(p) == 
      OF ==> OutputForm
      lp:OF:="("
      rp:OF:=")"
      lb:OF:="{"
      rb:OF:="}"
      lk:OF:="["
      rk:OF:="]"
      of:OF:=""
      s0:OF:="."
      s1:OF:=" & "
      s2:OF:=" | "
      s3:OF:=" => "
      s4:OF:=" <=> "
      s5:OF:="~"
      s6:OF:="\"
      s7:OF:="?"
      s10:OF:=" = "
      s11:OF:=" ~= "
      s12:OF:=" < "
      s13:OF:=" <= "
      s14:OF:=" > "
      s15:OF:=" >= "
      empty? p => of
      val:= value p
      val=1 => of:=hconcat [of,lp,coerce(left p),s1,coerce(right p),rp]
      val=2 => of:=hconcat [of,lp,coerce(left p),s2,coerce(right p),rp]
      val=3 => of:=hconcat [of,lp,coerce(left p),s3,coerce(right p),rp]
      val=4 => of:=hconcat [of,lp,coerce(left p),s4,coerce(right p),rp]
      val=5 => of:=hconcat [of,s5,lp,coerce(left p),rp]
      val=6 => of:=hconcat [of,s6,coerce(left p),s0,lk,coerce(right p),rk]
      val=7 => of:=hconcat [of,s7,coerce(left p),s0,lk,coerce(right p),rk]
      val=10=> of:=hconcat [of,lb,coerce(left p),s10,coerce(right p),rb] 
      val=11=> of:=hconcat [of,lb,coerce(left p),s11,coerce(right p),rb] 
      val=12=> of:=hconcat [of,lb,coerce(left p),s12,coerce(right p),rb] 
      val=13=> of:=hconcat [of,lb,coerce(left p),s13,coerce(right p),rb] 
      val=14=> of:=hconcat [of,lb,coerce(left p),s14,coerce(right p),rb] 
      val=15=> of:=hconcat [of,lb,coerce(left p),s15,coerce(right p),rb] 
      of:=hconcat[of,val::OF]
      of
    --local  
    mvNot(p:%):% ==
      val := value p
      val=1 => Or(Not(left p),Not(right p))::Rep
      val=2 => And(Not(left p),Not(right p))::Rep
      val=3 => And(left p, Not(right p))::Rep
      val=4 => Not(Or(And(left p,right p),And(Not(left p),Not(right p))))
      val=5 => (left p)::Rep
      val=6 => Ex(value(left p)::S, Not(right p))::Rep
      val=7 => All(value(left p)::S, Not(right p))::Rep
      val=10 => binaryTree(left p,11,right p)$Rep
      val=11 => binaryTree(left p,10,right p)$Rep
      val=12 => binaryTree(left p,15,right p)$Rep
      val=13 => binaryTree(left p,14,right p)$Rep
      val=14 => binaryTree(left p,13,right p)$Rep
      val=15 => binaryTree(left p,12,right p)$Rep
      p::Rep
    nnf(p:%):% ==
      empty? p => p::Rep
      val := value p
      val=1 => And(nnf(left p),nnf(right p))
      val=2 => Or(nnf(left p),nnf(right p))
      val=3 => nnf(Or(Not(left p),right p))
      val=4 => nnf(And(Or(left p,Not(right p)),Or(Not(left p),right p)))
      val=5 => nnf(mvNot(left p))
      val=6 => All(value(left p)::S, nnf(right p))
      val=7 => Ex(value(left p)::S, nnf(right p))
      p::Rep
    qvars(p:%):List(TT) == 
      L:List(TT):=[]
      empty? p => []::List(TT)
      val := value p
      if (val case S) then
        L:=append(L,[val])
      else
        L:=append(L,qvars(left p))
        L:=append(L,qvars(right p))
      L



)abbrev domain SUBSET SubsetOf
++ Author: kfp
++ Date Created: Mon Nov 03 20:41:24 CET 2014
++ License: BSD (same as Axiom)
++ Date Last Updated:
++ Basic Operations: 
++ Related Domains: 
++ Also See:
++ AMS Classifications:
++ Keywords: 
++ Examples:
++ References:
++
++ Description:
++ 
++
SubsetOf(T:Comparable) : Exports == Implementation where
  OF ==> OutputForm
  Exports == Join(Comparable , CoercibleTo OutputForm) with
    setOfAll : (List Symbol, Prop T ) -> %
    member? : (List T,%) -> Boolean
    coerce : % -> OutputForm
  Implementation == Prop(T) add 
    Rep := Record(s:List Symbol, p:Prop T)
    setOfAll(ls,P) == [ls,P]::Rep
    member?(t,ss) == false
    coerce(ss:%):OF ==
      r:=ss::Rep
      sym:OF:=(r.s)::OF
      prop:OF:=(r.p)::OF
      hconcat [Set of all , sym, such that , prop]

\end{spad}
InEq
\begin{axiom}
)set output tex off
)set output algebra on
x>0
x^2+y^2<1
a+b<=2
sin(x)+y>=1+y
eql(x,y)
neq(x,y)
P1:=sin(x)+y>=1+y
lhs P1
rhs P1
rel P1
converse P1
\end{axiom}
Propositions
\begin{axiom}
assert(P1)
R ==> EXPR INT
A:=assert(x::R + y + z >=1)
B:=assert(z::R<1/2)
C:=assert(x+y=4::R)
And(A,B)
Or(A,B)
Imp(A,C)
Eqv(B,C)
Not(A)
Not(C)
All(x,A)
All(y,Ex(z,A))
All(x,All(y,Imp(assert(x=y),assert(y=x))))
\end{axiom}
NNF
\begin{axiom}
m1:=assert(m>1::R)
m2:=assert(m
SUBSETS
\begin{axiom}
setOfAll([x,y,z],assert(x^2+y^2+z^2<=1))
setOfAll([x,y],And(assert(x^2c)))
\end{axiom}
-- continue with NatDed/Solve/RSPACE/Cell/Interval/Surface(k) , requires: CAD


    Some or all expressions may not have rendered properly,
    because Axiom returned the following error:
Error: export FRICAS=/usr/local/lib/fricas/target/x86_64-unknown-linux; export ALDORROOT=/usr/local/aldor/linux/1.1.0; export PATH=$ALDORROOT/bin:$PATH; export HOME=/var/zope2/var/LatexWiki; ulimit -t 600; export LD_LIBRARY_PATH=/usr/local/lib/fricas/target/x86_64-unknown-linux/lib; LANG=en_US.UTF-8 $FRICAS/bin/FRICASsys < /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8659343403449756850-25px.axm
/bin/sh: /usr/local/lib/fricas/target/x86_64-unknown-linux/bin/FRICASsys: not found

This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6)
 \write18 enabled.
 %&-line parsing enabled.
entering extended mode
(./2008420880488702843-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
n, swedish, ukenglish, pinyin, loaded.
(/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/ucs/ucs.sty
(/usr/share/texmf-texlive/tex/latex/ucs/data/uni-global.def))
(/usr/share/texmf-texlive/tex/latex/base/inputenc.sty
(/usr/share/texmf-texlive/tex/latex/ucs/utf8x.def))
(/usr/share/texmf-texlive/tex/latex/bbm/bbm.sty)
(/usr/share/texmf-texlive/tex/latex/jknapltx/mathrsfs.sty)
(/usr/share/texmf-texlive/tex/latex/base/fontenc.sty
(/usr/share/texmf-texlive/tex/latex/base/t1enc.def))
(/usr/share/texmf-texlive/tex/latex/pstricks/pstricks.sty
(/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.tex
`PSTricks' v1.15  <2006/12/22> (tvz)
(/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.con))
(/usr/share/texmf/tex/latex/xcolor/xcolor.sty
(/etc/texmf/tex/latex/config/color.cfg)
(/usr/share/texmf-texlive/tex/latex/graphics/dvips.def)
(/usr/share/texmf-texlive/tex/latex/graphics/dvipsnam.def)))
(/usr/share/texmf-texlive/tex/latex/graphics/epsfig.sty
(/usr/share/texmf-texlive/tex/latex/graphics/graphicx.sty
(/usr/share/texmf-texlive/tex/latex/graphics/keyval.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/pst-grad/pst-grad.sty
(/usr/share/texmf-texlive/tex/generic/pst-grad/pst-grad.tex
(/usr/share/texmf-texlive/tex/latex/xkeyval/pst-xkey.tex
(/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.sty
(/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.tex)))
`pst-plot' v1.05, 2006/11/04 (tvz,dg,hv)))
(/usr/share/texmf-texlive/tex/latex/pstricks/pst-plot.sty
(/usr/share/texmf-texlive/tex/generic/pstricks/pst-plot.tex
 v97 patch 2, 1999/12/12
(/usr/share/texmf-texlive/tex/generic/multido/multido.tex
 v1.41, 2004/05/18 <tvz>)))
(/usr/share/texmf-texlive/tex/latex/geometry/geometry.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.

Loading kernel: messages; fonts; allocations: state, direction,
utility macros; pictures: \xy, positions, objects, decorations;
kernel objects: directionals, circles, text; options; algorithms: directions,
edges, connections;  Xy-pic loaded))
(/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
 Xy-pic option: More Tips extension v.3.3 loaded) loaded)
(/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
 Xy-pic option: Graph feature v.3.7 loaded) loaded)
(/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 2008420880488702843-16.0px.sage
) (/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))
(./2008420880488702843-16.0px.aux)
(/usr/share/texmf-texlive/tex/latex/ucs/ucsencs.def)
(/usr/share/texmf-texlive/tex/latex/jknapltx/ursfs.fd)
(/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) [1]
 Misplaced alignment tab character &.
l.308       s1:OF:=" &
                       "
Overfull \hbox (38.1871pt too wide) in paragraph at lines 298--338
\T1/cmr/m/n/12 [of,s6,coerce(left p),s0,lk,coerce(right p),rk] val=7 => of:=hco
ncat [of,s7,coerce(left p),s0,lk,coerce(right p),rk] val=10=> of:=hconcat [of,l
b,coerce(left
Overfull \hbox (39.7535pt too wide) in paragraph at lines 298--338
\T1/cmr/m/n/12 p),s10,coerce(right p),rb] val=11=> of:=hconcat [of,lb,coerce(le
ft p),s11,coerce(right p),rb] val=12=> of:=hconcat [of,lb,coerce(left p),s12,co
erce(right
[2] [3] (/usr/share/texmf-texlive/tex/latex/base/t1cmtt.fd)
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 439.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 455.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 465.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 469.
[4] [5] (./2008420880488702843-16.0px.aux) )
(see the transcript file for additional information)
Output written on 2008420880488702843-16.0px.dvi (5 pages, 10784 bytes).
Transcript written on 2008420880488702843-16.0px.log.