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

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


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