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

# Edit detail for SandBoxProp revision 1 of 1

 1 Editor: Kurt Pagani Time: 2014/11/07 05:10:59 GMT+0 Note:

changed:
-
)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

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'

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

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 "::OF, sym," such that "::OF, prop]

**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<n::R)
p:=Imp(And(m1,m2),Not(Ex(k,assert(k*m=n::R))))
Prime(n) == All(m,p)
Prime(n)
nnf Prime(n)
nnf Not Imp(And(A,B),Not Or(Not C,B))
nnf Not(And(A,B))
\end{axiom}

**SUBSETS**

\begin{axiom}
setOfAll([x,y,z],assert(x^2+y^2+z^2<=1))
setOfAll([x,y],And(assert(x^2<y^2+1),assert(x+y>c)))
\end{axiom}

-- continue with NatDed/Solve/RSPACE/Cell/Interval/Surface(k) , requires: CAD


\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
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

-- 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
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]

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


Some or all expressions may not have rendered properly, because Latex returned the following error:
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
(/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/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.

utility macros; pictures: \xy, positions, objects, decorations;
kernel objects: directionals, circles, text; options; algorithms: directions,
(/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
(/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
(/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.
`