Maude-help mailing list

[Mandy Martin <tesleft AT hotmail.com>]

Hi,

Maude> rew in MYPOLY : X + X . Warning: <standard input>, line 60: bad token X. Warning: <standard input>, line 60: no parse for term.

fth TRIV is 
 sort Elt .
endfth

fth RING is  
    sort Ring .  
    ops z e : -> Ring .  
    op _+_ : Ring Ring -> Ring [assoc comm id: z] .  
    op _*_ : Ring Ring -> Ring [assoc comm id: e] .  
    op -_ : Ring -> Ring .  
    vars A B C : Ring .  
    eq A + (- A) = z [nonexec] .  
    eq A * (B + C) = (A * B) + (A * C) [nonexec] .  
endfth

fmod MONOMIAL{X :: TRIV} is  
    protecting NAT .  
    sorts Pow{X} Mon{X} .  
    subsorts Pow{X} < Mon{X} .  
    *** multiplication  
    op __ : Mon{X} Mon{X} -> Mon{X} [assoc comm] .  
    op _^_ : X$Elt NzNat -> Pow{X} .  
    var  X : X$Elt .  
    vars N M : NzNat .  
    eq (X ^ N) (X ^ M) = X ^ (N + M) .  
endfm

fmod POLYNOMIAL{R :: RING, X :: TRIV} is  
    protecting MONOMIAL{X} .  
    sorts Poly{R, X} .  
    subsorts R$Ring < Poly{R, X} .  
    *** multiplication  
    op __ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .  
    *** addition  
    op _++_ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .  
    op --_ : Poly{R, X} -> Poly{R, X} .  
    op __ : R$Ring Mon{X} -> Poly{R, X} .  

    vars A B : R$Ring .  
    vars U V : Mon{X} .  
    vars P Q R : Poly{R, X} .  
    eq P ++ z = P .  
    eq P ++ (-- P) = z .  
    eq P e = P .  
    eq -- (P ++ Q) = (-- P) ++ (-- Q) .  
    eq -- (A U) = (- A) U .  
    eq P (Q ++ R) = (P Q) ++ (P R) .  
    eq z U = z .  
    eq z P = z .  
    eq A (B U) = (A B) U .  
    eq (A U) ++ (B U) = (A ++ B) U .  
    eq (A U) (B V) = (A B) (U V) .  
    eq A B = A * B .  
    eq A ++ B = A + B .  
endfm

fmod MYPOLY is 
 inc POLYNOMIAL{RING, TRIV2PACKET} .
endfm

rew in MYPOLY : X + X

Regards,

Martin Lee