***
***	Maude interpreter standard prelude.
***	Version alpha 75a.
***	Copyright 1998-2002 SRI International.
***
***	Some of the overall structure is taken from the OBJ3
***	interpreter standard prelude.
***

set include BOOL off .

fmod TRUTH-VALUE is
  sort Bool .
  op true : -> Bool [ctor special (id-hook SystemTrue)] .
  op false : -> Bool [ctor special (id-hook SystemFalse)] .
endfm

fmod TRUTH is
  protecting TRUTH-VALUE .
  op if_then_else_fi : Bool Universal Universal -> Universal 
	[special (id-hook BranchSymbol
		  term-hook trueTerm (true)
		  term-hook falseTerm (false))] .

  op _==_ : Universal Universal -> Bool 
	[prec 51
         special (id-hook EqualitySymbol
		  term-hook equalTerm (true)
		  term-hook notEqualTerm (false))] .

  op _=/=_ : Universal Universal -> Bool 
	[prec 51
         special (id-hook EqualitySymbol
		  term-hook equalTerm (false)
		  term-hook notEqualTerm (true))] .
endfm

fmod BOOL is
  protecting TRUTH .
  op _and_ : Bool Bool -> Bool [assoc comm prec 55] .
  op _or_ : Bool Bool -> Bool [assoc comm prec 59] .
  op _xor_ : Bool Bool -> Bool [assoc comm prec 57] .
  op not_ : Bool -> Bool [prec 53] .
  op _implies_ : Bool Bool -> Bool [gather (e E) prec 61] .
  vars A B C : Bool .
  eq true and A = A .
  eq false and A = false .
  eq A and A = A .
  eq false xor A = A .
  eq A xor A = false .
  eq A and (B xor C) = A and B xor A and C .
  eq not A = A xor true .
  eq A or B = A and B xor A xor B .
  eq A implies B = not(A xor A and B) .
endfm

set include BOOL on .

fmod IDENTICAL is
  op _===_ : Universal Universal -> Bool 
	[prec 51 strat (0) 
         special (id-hook EqualitySymbol
		  term-hook equalTerm (true)
		  term-hook notEqualTerm (false))] .

  op _=/==_ : Universal Universal -> Bool 
        [prec 51 strat (0) 
	 special (id-hook EqualitySymbol
		  term-hook equalTerm (false)
		  term-hook notEqualTerm (true))] .
endfm

fmod NAT is
  sorts Zero NzNat Nat .
  subsort Zero NzNat < Nat .
  op 0 : -> Zero [ctor] .

  op s_ : Nat -> NzNat
	[ctor iter
	 special (id-hook SuccSymbol
		  term-hook zeroTerm (0))] .

  op _+_ : NzNat Nat -> NzNat
	[assoc comm prec 33
	 special (id-hook ACU_NumberOpSymbol (+)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
  op _+_ : Nat Nat -> Nat [ditto] .

  op sd : Nat Nat -> Nat
        [comm
	 special (id-hook CUI_NumberOpSymbol (sd)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op _*_ : NzNat NzNat -> NzNat
	[assoc comm prec 31
	 special (id-hook ACU_NumberOpSymbol (*)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
  op _*_ : Nat Nat -> Nat [ditto] .

  op _quo_ : Nat NzNat -> Nat
	[prec 31 gather (E e)
	 special (id-hook NumberOpSymbol (quo)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op _rem_ : Nat NzNat -> Nat
	[prec 31 gather (E e)
	 special (id-hook NumberOpSymbol (rem)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op _^_ : Nat Nat -> Nat
	[prec 29  gather (E e)
	 special (id-hook NumberOpSymbol (^)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
 
  op modExp : Nat Nat NzNat ~> Nat
	[special (id-hook NumberOpSymbol (modExp)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
 
  op gcd : NzNat NzNat -> NzNat
	[assoc comm
	 special (id-hook ACU_NumberOpSymbol (gcd)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
  op gcd : Nat Nat -> Nat [ditto] .

  op lcm : NzNat NzNat -> NzNat
	[assoc comm
	 special (id-hook ACU_NumberOpSymbol (lcm)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
  op lcm : Nat Nat -> Nat [ditto] .

  op _xor_ : Nat Nat -> Nat
	[assoc comm prec 55
	 special (id-hook ACU_NumberOpSymbol (xor)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op _&_ : Nat Nat -> Nat
	[assoc comm prec 53
	 special (id-hook ACU_NumberOpSymbol (&)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op _|_ : NzNat Nat -> NzNat
	[assoc comm prec 57
	 special (id-hook ACU_NumberOpSymbol (|)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .
  op _|_ : Nat Nat -> Nat [ditto] .

  op _>>_ : Nat Nat -> Nat
	[prec 35 gather (E e)
	 special (id-hook NumberOpSymbol (>>)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op _<<_ : Nat Nat -> Nat
	[prec 35 gather (E e)
	 special (id-hook NumberOpSymbol (<<)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op _<_ : Nat Nat -> Bool 
	[prec 37
	 special (id-hook NumberOpSymbol (<)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _<=_ : Nat Nat -> Bool 
	[prec 37
	 special (id-hook NumberOpSymbol (<=)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>_ : Nat Nat -> Bool 
	[prec 37
	 special (id-hook NumberOpSymbol (>)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>=_ : Nat Nat -> Bool 
	[prec 37
	 special (id-hook NumberOpSymbol (>=)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _divides_ : NzNat Nat -> Bool
	[prec 51
	 special (id-hook NumberOpSymbol (divides)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .
endfm

fmod INT is
  protecting NAT .
  sorts NzInt Int .
  subsorts NzNat < NzInt Nat < Int .

  op -_ : NzNat -> NzInt
	[ctor
	 special (id-hook MinusSymbol
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op -_ : NzInt -> NzInt [ditto] .
  op -_ : Int -> Int [ditto] .

  op _+_ : Int Int -> Int
	[assoc comm prec 33
	 special (id-hook ACU_NumberOpSymbol (+)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _-_ : Int Int -> Int
	[prec 33 gather (E e)
	 special (id-hook NumberOpSymbol (-)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _*_ : NzInt NzInt -> NzInt
	[assoc comm prec 31
	 special (id-hook ACU_NumberOpSymbol (*)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op _*_ : Int Int -> Int [ditto] .

  op _quo_ : Int NzInt -> Int
	[prec 31 gather (E e)
	 special (id-hook NumberOpSymbol (quo)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _rem_ : Int NzInt -> Int
	[prec 31 gather (E e)
	 special (id-hook NumberOpSymbol (rem)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _^_ : Int Nat -> Int
	[prec 29  gather (E e)
	 special (id-hook NumberOpSymbol (^)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op abs : NzInt -> NzNat
	[special (id-hook NumberOpSymbol (abs)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op abs : Int -> Nat [ditto] .

  op gcd : NzInt NzInt -> NzNat
	[assoc comm
	 special (id-hook ACU_NumberOpSymbol (gcd)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op gcd : Int Int -> Nat [ditto] .

  op lcm : NzInt NzInt -> NzNat
	[assoc comm
	 special (id-hook ACU_NumberOpSymbol (lcm)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op lcm : Int Int -> Nat [ditto] .

  op ~_ : Int -> Int
	[special (id-hook NumberOpSymbol (~)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _xor_ : Int Int -> Int
	[assoc comm prec 55
	 special (id-hook ACU_NumberOpSymbol (xor)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _&_ : Int Int -> Int
	[assoc comm prec 53
	 special (id-hook ACU_NumberOpSymbol (&)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _|_ : NzInt Int -> NzInt
	[assoc comm prec 57
	 special (id-hook ACU_NumberOpSymbol (|)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op _|_ : Int Int -> Int [ditto] .

  op _>>_ : Int Nat -> Int
	[prec 35 gather (E e)
	 special (id-hook NumberOpSymbol (>>)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _<<_ : Int Nat -> Int
	[prec 35 gather (E e)
	 special (id-hook NumberOpSymbol (<<)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  op _<_ : Int Int -> Bool 
	[prec 37
	 special (id-hook NumberOpSymbol (<)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _<=_ : Int Int -> Bool 
	[prec 37
	 special (id-hook NumberOpSymbol (<=)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>_ : Int Int -> Bool 
	[prec 37
	 special (id-hook NumberOpSymbol (>)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>=_ : Int Int -> Bool 
	[prec 37
	 special (id-hook NumberOpSymbol (>=)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _divides_ : NzInt Int -> Bool
	[prec 51
	 special (id-hook NumberOpSymbol (divides)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .
endfm

fmod RAT is
  protecting INT .
  sorts NzRat Rat .
  subsorts NzInt < NzRat Int < Rat .

  op _/_ : NzInt NzNat -> NzRat
	[ctor prec 31 gather (E e)
	 special (id-hook DivisionSymbol
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int))] .

  var I J : NzInt .
  var N M : NzNat .
  var K : Int .
  var Z : Nat .

  op _/_ : NzRat NzRat -> NzRat [ditto] .
  op _/_ : Rat NzRat -> Rat [ditto] .
  eq 0 / N = 0 .
  eq I / - N = - I / N .
  eq (I / N) / (J / M) = (I * M) / (J * N) .
  eq (I / N) / J = I / (J * N) .
  eq I / (J / M) = (I * M) / J .

  op -_ : NzRat -> NzRat [ditto] .
  op -_ : Rat -> Rat [ditto] .
  eq - (I / N) = - I / N .

  op _+_ : Rat Rat -> Rat [ditto] .
  eq I / N + J / M = (I * M + J * N) / (N * M) .
  eq I / N + J = (I + J * N) / N .

  op _-_ : Rat Rat -> Rat [ditto] .
  eq I / N - J / M = (I * M - J * N) / (N * M) .
  eq I / N - J = (I - J * N) / N .
  eq I - J / M = (I * M - J ) / M .

  op _*_ : NzRat NzRat -> NzRat [ditto] .
  op _*_ : Rat Rat -> Rat [ditto] .
  eq (I / N) * (J / M) = (I * J) / (N * M).
  eq (I / N) * J = (I * J) / N .

  op _^_ : Rat Nat -> Rat [ditto] .
  eq (I / N) ^ Z = (I ^ Z) / (N ^ Z) .

  op abs : Int -> Nat [ditto] .
  eq abs(I / N) = abs(I) / N .

  op _<_ : Rat Rat -> Bool [ditto] .
  eq (I / N) < (J / M) = (I * M) < (J * N) .
  eq (I / N) < J = I < (J * N) .
  eq I < (J / M) = (I * M) < J .

  op _<=_ : Rat Rat -> Bool [ditto] .
  eq (I / N) <= (J / M) = (I * M) <= (J * N) .
  eq (I / N) <= J = I <= (J * N) .
  eq I <= (J / M) = (I * M) <= J .

  op _>_ : Rat Rat -> Bool [ditto] .
  eq (I / N) > (J / M) = (I * M) > (J * N) .
  eq (I / N) > J = I > (J * N) .
  eq I > (J / M) = (I * M) > J .

  op _>=_ : Rat Rat -> Bool [ditto] .
  eq (I / N) >= (J / M) = (I * M) >= (J * N) .
  eq (I / N) >= J = I >= (J * N) .
  eq I >= (J / M) = (I * M) >= J .

  op trunc : Rat -> Int .
  eq trunc(K) = K .
  eq trunc(I / N) = I quo N .
  
  op frac : Rat -> Rat .
  eq frac(K) = 0 .
  eq frac(I / N) = (I rem N) / N .

  op floor : Rat -> Int .
  op ceiling : Rat -> Int .
  eq floor(K) = K .
  eq ceiling(K) = K .
  eq floor(N / M) = N quo M .
  eq ceiling(N / M) = ((N + M) - 1) quo M .
  eq floor(- N / M) = - ceiling(N / M) .
  eq ceiling(- N / M) = - floor(N / M) .
endfm

fmod FLOAT is
  sorts FiniteFloat Float .
  subsort FiniteFloat < Float .
  op <Floats> : -> FiniteFloat [special (id-hook FloatSymbol)] .
  op <Floats> : -> Float [ditto] .

  op -_ : Float -> Float
	[prec 15
	 special (id-hook FloatOpSymbol (-)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op -_ : FiniteFloat -> FiniteFloat [ditto] .

  op _+_ : Float Float -> Float
	[prec 33 gather (E e)
	 special (id-hook FloatOpSymbol (+)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op _-_ : Float Float -> Float
	[prec 33 gather (E e)
	 special (id-hook FloatOpSymbol (-)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op _*_ : Float Float -> Float
	[prec 31 gather (E e)
	 special (id-hook FloatOpSymbol (*)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op _/_ : Float Float ~> Float
	[prec 31 gather (E e)
	 special (id-hook FloatOpSymbol (/)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op _rem_ : Float Float ~> Float
	[prec 31 gather (E e)
	 special (id-hook FloatOpSymbol (rem)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op _^_ : Float Float ~> Float
	[prec 29  gather (E e)
	 special (id-hook FloatOpSymbol (^)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op abs : Float -> Float
	[special (id-hook FloatOpSymbol (abs)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op abs : FiniteFloat -> FiniteFloat [ditto] .

  op floor : Float -> Float
	[special (id-hook FloatOpSymbol (floor)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op ceiling : Float -> Float
	[special (id-hook FloatOpSymbol (ceiling)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op sqrt : Float ~> Float
	[special (id-hook FloatOpSymbol (sqrt)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op exp : Float -> Float
 	[special (id-hook FloatOpSymbol (exp)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op log : Float ~> Float
	[special (id-hook FloatOpSymbol (log)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op sin : Float -> Float
 	[special (id-hook FloatOpSymbol (sin)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op cos : Float -> Float
 	[special (id-hook FloatOpSymbol (cos)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op tan : Float -> Float
 	[special (id-hook FloatOpSymbol (tan)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op asin : Float ~> Float
 	[special (id-hook FloatOpSymbol (asin)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op acos : Float ~> Float
 	[special (id-hook FloatOpSymbol (acos)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op atan : Float -> Float
 	[special (id-hook FloatOpSymbol (atan)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op atan : Float Float -> Float
 	[special (id-hook FloatOpSymbol (atan)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op _<_ : Float Float -> Bool
	[prec 51
	 special (id-hook FloatOpSymbol (<)
		  op-hook floatSymbol (<Floats> : ~> Float)
 		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _<=_ : Float Float -> Bool
	[prec 51
	 special (id-hook FloatOpSymbol (<=)
		  op-hook floatSymbol (<Floats> : ~> Float)
  		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>_ : Float Float -> Bool
	[prec 51
	 special (id-hook FloatOpSymbol (>)
		  op-hook floatSymbol (<Floats> : ~> Float)
  		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>=_ : Float Float -> Bool
	[prec 51
	 special (id-hook FloatOpSymbol (>=)
		  op-hook floatSymbol (<Floats> : ~> Float)
  		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op pi : -> FiniteFloat .
  eq pi = 3.1415926535897931 .

  op _=[_]_ : Float FiniteFloat Float -> Bool [prec 51] .
  var X Y : Float .
  var Z : FiniteFloat .
  eq X =[Z] Y = abs(X - Y) < Z .
endfm

fmod STRING is
  protecting NAT .
  sorts String Char FindResult .
  subsort Char < String .
  subsort Nat < FindResult .
  op <Strings> : -> Char [special (id-hook StringSymbol)] .
  op <Strings> : -> String [ditto] .
  op notFound : -> FindResult .

  op ascii : Char -> Nat
	[special (id-hook StringOpSymbol (ascii)
		  op-hook stringSymbol (<Strings> : ~> Char)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op char : Nat ~> Char
	[special (id-hook StringOpSymbol (char)
		  op-hook stringSymbol (<Strings> : ~> Char)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op _+_ : String String -> String
	[prec 33 gather (E e)
	 special (id-hook StringOpSymbol (+)
		  op-hook stringSymbol (<Strings> : ~> String))] .

  op length : String -> Nat
	[special (id-hook StringOpSymbol (length)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op substr : String Nat Nat -> String
	[special (id-hook StringOpSymbol (substr)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook succSymbol (s_ : Nat ~> NzNat))] .

  op find : String String Nat -> FindResult
	[special (id-hook StringOpSymbol (find)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  term-hook notFoundTerm (notFound))] .

  op rfind : String String Nat -> FindResult
	[special (id-hook StringOpSymbol (rfind)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  term-hook notFoundTerm (notFound))] .

  op _<_ : String String -> Bool 
	[prec 37
	 special (id-hook StringOpSymbol (<)
		  op-hook stringSymbol (<Strings> : ~> String)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _<=_ : String String -> Bool 
	[prec 37
	 special (id-hook StringOpSymbol (<=)
		  op-hook stringSymbol (<Strings> : ~> String)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>_ : String String -> Bool 
	[prec 37
	 special (id-hook StringOpSymbol (>)
		  op-hook stringSymbol (<Strings> : ~> String)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>=_ : String String -> Bool 
	[prec 37
	 special (id-hook StringOpSymbol (>=)
		  op-hook stringSymbol (<Strings> : ~> String)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .
endfm

fmod NUMBER-CONVERSION is
  protecting RAT .
  protecting FLOAT .
  protecting STRING .
  sort DecFloat .
  op <_,_,_> : Int String Int -> DecFloat [ctor] .

  op float : Rat -> Float
	[special (id-hook FloatOpSymbol (float)
		  op-hook floatSymbol (<Floats> : ~> Float)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  op-hook divisionSymbol (_/_ : NzInt NzNat ~> NzRat))] .

  op rat : FiniteFloat -> Rat
	[special (id-hook FloatOpSymbol (rat)
		  op-hook floatSymbol (<Floats> : ~> Float)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  op-hook divisionSymbol (_/_ : NzInt NzNat ~> NzRat))] .

  op string : Rat NzNat ~> String
	[special (id-hook StringOpSymbol (string)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  op-hook divisionSymbol (_/_ : NzInt NzNat ~> NzRat))] .

  op rat : String NzNat ~> Rat
	[special (id-hook StringOpSymbol (rat)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  op-hook divisionSymbol (_/_ : NzInt NzNat ~> NzRat))] .

  op string : Float -> String
	[special (id-hook StringOpSymbol (string)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op float : String ~> Float
	[special (id-hook StringOpSymbol (float)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook floatSymbol (<Floats> : ~> Float))] .

  op decFloat : Float Nat -> DecFloat
	[special (id-hook StringOpSymbol (decFloat)
		  op-hook stringSymbol (<Strings> : ~> String)
		  op-hook floatSymbol (<Floats> : ~> Float)
		  op-hook succSymbol (s_ : Nat ~> NzNat)
		  op-hook minusSymbol (-_ : NzNat ~> Int)
		  op-hook decFloatSymbol 
                          (<_,_,_> : Int String Int ~> DecFloat))] .
endfm

fmod QID is
  protecting STRING .
  sort Qid .
  op <Qids> : -> Qid [special (id-hook QuotedIdentifierSymbol)] .

  op string : Qid -> String 
	[special (id-hook QuotedIdentifierOpSymbol (string)
		  op-hook quotedIdentifierSymbol (<Qids> : ~> Qid)
		  op-hook stringSymbol (<Strings> : ~> String))] .

  op qid : String ~> Qid 
	[special (id-hook QuotedIdentifierOpSymbol (qid)
		  op-hook quotedIdentifierSymbol (<Qids> : ~> Qid)
		  op-hook stringSymbol (<Strings> : ~> String))] .
endfm

fmod QID-LIST is
  protecting QID .
  sort QidList .
  subsort Qid < QidList .
  op nil : -> QidList [ctor] .
  op __ : QidList QidList -> QidList [ctor assoc id: nil] .
endfm

fmod META-TERM is
  protecting QID .

*** types
  sorts Sort Kind Type .
  subsorts Sort Kind < Type < Qid .
  op <Qids> : -> Sort [special (id-hook QuotedIdentifierSymbol (sortQid))] .
  op <Qids> : -> Kind [special (id-hook QuotedIdentifierSymbol (kindQid))] .

*** terms
  sorts Constant Variable GroundTerm Term GroundTermList TermList .
  subsorts Constant Variable < Qid Term .
  subsorts Constant < GroundTerm < Term GroundTermList < TermList .
  op <Qids> : -> Constant [special (id-hook QuotedIdentifierSymbol (constantQid))] .
  op <Qids> : -> Variable [special (id-hook QuotedIdentifierSymbol (variableQid))] .
  op _,_ : GroundTermList GroundTermList -> GroundTermList [ctor assoc gather (e E) prec 120] .
  op _,_ : TermList TermList -> TermList [ctor assoc gather (e E) prec 120] .
  op _[_] : Qid GroundTermList -> GroundTerm [ctor] .
  op _[_] : Qid TermList -> Term [ctor] .

*** extraction of names and types
  op getName : Constant -> Qid .
  op getType : Constant -> Type .
  var C : Constant .
  eq getName(C) = qid(substr(string(C),
			     0,
			     rfind(string(C), ".", length(string(C))))) .
  eq getType(C) = qid(substr(string(C),
			     rfind(string(C), ".", length(string(C))) + 1,
			     length(string(C)))) .

  op getName : Variable -> Qid .
  op getType : Variable -> Type .
  var V : Variable .
  eq getName(V) = qid(substr(string(V),
			     0,
			     rfind(string(V), ":", length(string(V))))) .
  eq getType(V) = qid(substr(string(V),
			     rfind(string(V), ":", length(string(V))) + 1,
			     length(string(V)))) .

*** substitutions
  sorts Assignment Substitution .
  subsort Assignment < Substitution .
  op _<-_ : Variable Term -> Assignment [ctor prec 63 format (nt d d d)] .
  op none : -> Substitution [ctor] .
  op _;_ : Substitution Substitution -> Substitution
    [ctor assoc comm id: none prec 65] .
  eq A:Assignment ; A:Assignment = A:Assignment .

*** contexts (terms with a single hole)
  sorts Context CTermList GTermList .
  subsort Context < CTermList .
  subsorts TermList CTermList < GTermList .

  op [] : -> Context [ctor] .
  op _,_ : TermList CTermList -> CTermList [ctor assoc gather (e E) prec 120] .
  op _,_ : CTermList TermList -> CTermList [ctor assoc gather (e E) prec 120] .
  op _[_] : Qid CTermList -> Context [ctor] .
endfm

fmod META-MODULE is
  protecting META-TERM .
  protecting QID-LIST .

*** importations
  sorts ModuleExpression Import ImportList .
  subsort Qid < ModuleExpression .
  subsort Import < ImportList .
  op protecting_. : ModuleExpression -> Import [ctor] .
  op including_. : ModuleExpression -> Import [ctor] .
  op nil : -> ImportList [ctor] .
  op __ : ImportList ImportList -> ImportList
    [ctor assoc id: nil format (d ni d)] .

*** sort sets
  sort SortSet .
  subsort Sort < SortSet .
  op none : -> SortSet [ctor] .
  op _;_ : SortSet SortSet -> SortSet [ctor assoc comm id: none] .
  eq S:Sort ; S:Sort = S:Sort .

*** subsort declarations
  sorts SubsortDecl SubsortDeclSet .
  subsort SubsortDecl < SubsortDeclSet .
  op subsort_<_. : Sort Sort -> SubsortDecl [ctor] .
  op none : -> SubsortDeclSet [ctor] .
  op __ : SubsortDeclSet SubsortDeclSet -> SubsortDeclSet
    [ctor assoc comm id: none format (d ni d)] .
  eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl .

*** type lists
  sort TypeList .
  subsort Type < TypeList < QidList .
  op nil : -> TypeList [ctor] .
  op __ : TypeList TypeList -> TypeList [ditto] .

*** Nat lists
  sort NatList .
  subsort Nat < NatList .
  op __ : NatList NatList -> NatList [ctor assoc] .

*** hooks
  sorts Hook HookList .
  subsort Hook < HookList .
  op id-hook : Qid QidList -> Hook [ctor] .
  op op-hook : Qid Qid QidList Qid -> Hook [ctor] .
  op term-hook : Qid Term -> Hook [ctor] .
  op __ : HookList HookList -> HookList [ctor assoc] .

*** attribute sets
  sorts Attr AttrSet .
  subsort Attr < AttrSet .
  op none : -> AttrSet [ctor] .
  op __ : AttrSet AttrSet -> AttrSet [ctor assoc comm id: none] .
  eq A:Attr A:Attr = A:Attr .

*** operator attributes
  op assoc : -> Attr [ctor] .
  op comm : -> Attr [ctor] .
  op idem : -> Attr [ctor] .
  op iter : -> Attr [ctor] .
  op id : Term -> Attr [ctor] .
  op left-id : Term -> Attr [ctor] .
  op right-id : Term -> Attr [ctor] .
  op strat : NatList -> Attr [ctor] .
  op memo : -> Attr [ctor] .
  op prec : Nat -> Attr [ctor] .
  op gather : QidList -> Attr [ctor] .
  op format : QidList -> Attr [ctor] .
  op ctor : -> Attr [ctor] .
  op frozen : -> Attr [ctor] .
  op special : HookList -> Attr [ctor] .

*** statement attributes
  op label : Qid -> Attr [ctor] .
  op metadata : String -> Attr [ctor] .

*** operator declarations
  sorts OpDecl OpDeclSet .
  subsort OpDecl < OpDeclSet .
  op (op_:_->_[_].) : Qid TypeList Type AttrSet -> OpDecl
    [ctor format (d d d d d d s d d s d)] .
  op none : -> OpDeclSet [ctor] .
  op __ : OpDeclSet OpDeclSet -> OpDeclSet
    [ctor assoc comm id: none format (d ni d)] .
  eq O:OpDecl O:OpDecl = O:OpDecl .

*** conditions
  sorts EqCondition Condition .
  subsort EqCondition < Condition .
  op nil : -> EqCondition .
  op _=_ : Term Term -> EqCondition [ctor prec 71] .
  op _:_ : Term Sort -> EqCondition [ctor prec 71] .
  op _:=_ : Term Term -> EqCondition [ctor prec 71] .
  op _=>_ : Term Term -> Condition [ctor prec 71] .
  op _/\_ : EqCondition EqCondition -> EqCondition [ctor assoc id: nil prec 73] .
  op _/\_ : Condition Condition -> Condition [ctor assoc id: nil prec 73] .

*** membership axioms
  sorts MembAx MembAxSet .
  subsort MembAx < MembAxSet .
  op mb_:_[_]. : Term Sort AttrSet -> MembAx [ctor] .
  op cmb_:_if_[_]. : Term Sort EqCondition AttrSet -> MembAx [ctor] .
  op none : -> MembAxSet [ctor] .
  op __ : MembAxSet MembAxSet -> MembAxSet
    [ctor assoc comm id: none format (d ni d)] .
  eq M:MembAx M:MembAx = M:MembAx .

*** equations
  sorts Equation EquationSet .
  subsort Equation < EquationSet .
  op eq_=_[_]. : Term Term AttrSet -> Equation [ctor] .
  op ceq_=_if_[_]. : Term Term EqCondition AttrSet -> Equation [ctor] .
  op none : -> EquationSet [ctor] .
  op __ : EquationSet EquationSet -> EquationSet
    [ctor assoc comm id: none format (d ni d)] .
  eq E:Equation E:Equation = E:Equation .

*** rules
  sorts Rule RuleSet .
  subsort Rule < RuleSet .
  op rl_=>_[_]. : Term Term AttrSet -> Rule [ctor] .
  op crl_=>_if_[_]. : Term Term Condition AttrSet -> Rule [ctor] .
  op none : -> RuleSet [ctor] .
  op __ : RuleSet RuleSet -> RuleSet
    [ctor assoc comm id: none format (d ni d)] .
  eq R:Rule R:Rule = R:Rule .

*** modules
  sorts FModule Module .
  subsort FModule < Module .
  op fmod_is_sorts_.____endfm : Qid ImportList SortSet SubsortDeclSet
    OpDeclSet MembAxSet EquationSet -> FModule [ctor gather (& & & & & & &)
     format (d d d n++i ni d d ni ni ni ni n--i d)] .
  op mod_is_sorts_._____endm : Qid ImportList SortSet SubsortDeclSet
    OpDeclSet MembAxSet EquationSet RuleSet -> Module
    [ctor gather (& & & & & & & &)
     format (d d d n++i ni d d ni ni ni ni ni n--i d)] .
  op [_] : Qid -> Module .
  eq [Q:Qid] = (mod Q:Qid is protecting Q:Qid .
                sorts none . none none none none none endm) .

*** projection functions
  var Q : Qid .
  var IL : ImportList .
  var SS : SortSet .
  var SSDS : SubsortDeclSet .
  var OPDS : OpDeclSet .
  var MAS : MembAxSet .
  var EQS : EquationSet .
  var RLS : RuleSet .

  op getName : Module -> Qid .
  eq getName(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q .
  eq getName(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q .

  op getImports : Module -> ImportList .
  eq getImports(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = IL .
  eq getImports(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = IL .

  op getSorts : Module -> SortSet .
  eq getSorts(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = SS .
  eq getSorts(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = SS .

  op getSubsorts : Module -> SubsortDeclSet .
  eq getSubsorts(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = SSDS .
  eq getSubsorts(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = SSDS .

  op getOps : Module -> OpDeclSet .
  eq getOps(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = OPDS .
  eq getOps(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = OPDS .

  op getMbs : Module -> MembAxSet .
  eq getMbs(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = MAS .
  eq getMbs(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = MAS .

  op getEqs : Module -> EquationSet .
  eq getEqs(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = EQS .
  eq getEqs(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = EQS .

  op getRls : Module -> RuleSet .
  eq getRls(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = none .
  eq getRls(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = RLS .
endfm

fmod META-LEVEL is
  protecting META-MODULE .

*** bounds
  sort Bound .
  subsort Nat < Bound .
  op unbounded : -> Bound .

*** kind sets
  sort KindSet .
  subsort Kind < KindSet .
  op empty : -> KindSet [ctor] .
  op _&_ : KindSet KindSet -> KindSet [ctor assoc comm id: empty] .
  eq K:Kind & K:Kind = K:Kind .

*** argument values
  sort Type? .
  subsort Type < Type? .
  op anyType : -> Type? [ctor] .

*** success results
  sorts ResultPair ResultTriple Result4Tuple MatchPair .
  op {_,_} : Term Type -> ResultPair [ctor] .
  op {_,_,_} : Term Type Substitution -> ResultTriple [ctor] .
  op {_,_,_,_} : Term Type Substitution Context -> Result4Tuple [ctor] .
  op {_,_} : Substitution Context -> MatchPair [ctor] .

*** failure results
  sorts ResultPair? ResultTriple? Result4Tuple? MatchPair? Substitution? .
  subsort ResultPair < ResultPair? .
  subsort ResultTriple < ResultTriple? .
  subsort Result4Tuple < Result4Tuple? .
  subsort MatchPair < MatchPair? .
  subsort Substitution < Substitution? .
  op noParse : Nat -> ResultPair? [ctor] .
  op ambiguity : ResultPair ResultPair -> ResultPair? [ctor] .

  op failure : -> ResultTriple? [ctor] .
  op failure : -> Result4Tuple? [ctor] .
  op noMatch : -> Substitution? [ctor] .
  op noMatch : -> MatchPair? [ctor] .

*** projection functions
  op getTerm : ResultPair -> Term .
  eq getTerm({T:Term, T:Type}) = T:Term .
  op getType : ResultPair -> Type .
  eq getType({T:Term, T:Type}) = T:Type .

  op getTerm : ResultTriple -> Term .
  eq getTerm({T:Term, T:Type, S:Substitution}) = T:Term .
  op getType : ResultTriple -> Type .
  eq getType({T:Term, T:Type, S:Substitution}) = T:Type .
  op getSubstitution : ResultTriple -> Substitution .
  eq getSubstitution({T:Term, T:Type, S:Substitution}) = S:Substitution .

  op getTerm : Result4Tuple -> Term .
  eq getTerm({T:Term, T:Type, S:Substitution, C:Context}) = T:Term .
  op getType : Result4Tuple -> Type .
  eq getType({T:Term, T:Type, S:Substitution, C:Context}) = T:Type .
  op getSubstitution : Result4Tuple -> Substitution .
  eq getSubstitution({T:Term, T:Type, S:Substitution, C:Context}) = S:Substitution .
  op getContext : Result4Tuple -> Context .
  eq getContext({T:Term, T:Type, S:Substitution, C:Context}) = C:Context .

  op getSubstitution : MatchPair -> Substitution .
  eq getSubstitution({S:Substitution, C:Context}) = S:Substitution .
  op getContext : MatchPair -> Context .
  eq getContext({S:Substitution, C:Context}) = C:Context .

*** descent functions
  op metaReduce : Module Term ~> ResultPair
     [special (
	id-hook MetaLevelOpSymbol	(metaReduce)

	op-hook qidSymbol		(<Qids> : ~> Qid)
	op-hook metaTermSymbol		(_[_] : Qid TermList ~> Term)
	op-hook metaArgSymbol		(_,_ : TermList TermList ~> TermList)

	op-hook assignmentSymbol	(_<-_ : Qid Term ~> Assignment)
	op-hook substitutionSymbol	
		(_;_ : Substitution Substitution ~> Substitution)
	op-hook emptySubstitutionSymbol	(none : ~> Substitution)
	op-hook holeSymbol		([] : ~> Context)

	op-hook protectingSymbol	(protecting_. : ModuleExpression ~> Import)
	op-hook includingSymbol		(including_. : ModuleExpression ~> Import)
	op-hook nilImportListSymbol	(nil : ~> ImportList)
	op-hook importListSymbol	(__ : ImportList ImportList ~> ImportList)

	op-hook emptySortSetSymbol	(none : ~> SortSet)
	op-hook sortSetSymbol		(_;_ : SortSet SortSet ~> SortSet)

	op-hook subsortSymbol		(subsort_<_. : Sort Sort ~> SubsortDecl)
	op-hook emptySubsortDeclSetSymbol	(none : ~> SubsortDeclSet)
	op-hook subsortDeclSetSymbol
		(__ : SubsortDeclSet SubsortDeclSet ~> SubsortDeclSet)

	op-hook nilQidListSymbol	(nil : ~> QidList)
	op-hook qidListSymbol		(__ : QidList QidList ~> QidList)

	op-hook succSymbol		(s_ : Nat ~> NzNat)
	op-hook natListSymbol		(__ : NatList NatList ~> NatList)
	op-hook unboundedSymbol		(unbounded : ~> Bound)

	op-hook stringSymbol		(<Strings> : ~> String)
	op-hook idHookSymbol		(id-hook : Qid QidList ~> Hook)
	op-hook opHookSymbol		(op-hook : Qid Qid QidList Qid ~> Hook)
	op-hook termHookSymbol		(term-hook : Qid Term ~> Hook)
	op-hook hookListSymbol		(__ : HookList HookList ~> HookList)

	op-hook assocSymbol		(assoc : ~> Attr)
	op-hook commSymbol		(comm : ~> Attr)
	op-hook idemSymbol		(idem : ~> Attr)
	op-hook iterSymbol		(iter : ~> Attr)
	op-hook idSymbol		(id : Term ~> Attr)
	op-hook leftIdSymbol		(left-id : Term ~> Attr)
	op-hook rightIdSymbol		(right-id : Term ~> Attr)
	op-hook stratSymbol		(strat : NatList ~> Attr)
	op-hook memoSymbol		(memo : ~> Attr)
	op-hook precSymbol		(prec : Nat ~> Attr)
	op-hook gatherSymbol		(gather : QidList ~> Attr)
	op-hook formatSymbol		(format : QidList ~> Attr)
	op-hook ctorSymbol		(ctor : ~> Attr)
	op-hook frozenSymbol		(frozen : ~> Attr)
	op-hook specialSymbol		(special : HookList ~> Attr)
	op-hook labelSymbol		(label : Qid ~> Attr)
	op-hook metadataSymbol		(metadata : String ~> Attr)
	op-hook emptyAttrSetSymbol	(none : ~> AttrSet)
	op-hook attrSetSymbol		(__ : AttrSet AttrSet ~> AttrSet)

	op-hook opDeclSymbol
		(op_:_->_[_]. : Qid TypeList Type AttrSet ~> OpDecl)
	op-hook emptyOpDeclSetSymbol	(none : ~> OpDeclSet)
	op-hook opDeclSetSymbol		(__ : OpDeclSet OpDeclSet ~> OpDeclSet)

	op-hook noConditionSymbol	(nil : ~> EqCondition)
	op-hook equalityConditionSymbol	(_=_ : Term Term ~> EqCondition)
	op-hook sortTestConditionSymbol	(_:_ : Term Sort ~> EqCondition)
	op-hook matchConditionSymbol	(_:=_ : Term Term ~> EqCondition)
	op-hook rewriteConditionSymbol	(_=>_ : Term Term ~> Condition)
	op-hook conjunctionSymbol	(_/\_ : Condition Condition ~> Condition)

	op-hook mbSymbol		(mb_:_[_]. : Term Sort AttrSet ~> MembAx)
	op-hook cmbSymbol
		(cmb_:_if_[_]. : Term Sort EqCondition AttrSet ~> MembAx)
	op-hook emptyMembAxSetSymbol	(none : ~> MembAxSet)
	op-hook membAxSetSymbol		(__ : MembAxSet MembAxSet ~> MembAxSet)

	op-hook eqSymbol		(eq_=_[_]. : Term Term AttrSet ~> Equation)
	op-hook ceqSymbol
		(ceq_=_if_[_]. : Term Term EqCondition AttrSet ~> Equation)
	op-hook emptyEquationSetSymbol	(none : ~> EquationSet)
	op-hook equationSetSymbol	
		(__ : EquationSet EquationSet ~> EquationSet)

	op-hook rlSymbol		(rl_=>_[_]. : Term Term AttrSet ~> Rule)
	op-hook crlSymbol
		(crl_=>_if_[_]. : Term Term Condition AttrSet ~> Rule)
	op-hook emptyRuleSetSymbol	(none : ~> RuleSet)
	op-hook ruleSetSymbol		(__ : RuleSet RuleSet ~> RuleSet)

	op-hook fmodSymbol
		(fmod_is_sorts_.____endfm :
			Qid ImportList SortSet SubsortDeclSet OpDeclSet 
			MembAxSet EquationSet ~> FModule)
	op-hook modSymbol
		(mod_is_sorts_._____endm :
			Qid ImportList SortSet SubsortDeclSet OpDeclSet 
			MembAxSet EquationSet RuleSet ~> Module)

	op-hook kindSetSymbol		(_&_ : KindSet KindSet ~> KindSet)
	op-hook emptyKindSetSymbol	(empty : ~> KindSet)

	op-hook anyTypeSymbol		(anyType : ~> Type?)

	op-hook resultPairSymbol	({_,_} : Term Type ~> ResultPair)
	op-hook resultTripleSymbol
		({_,_,_} : Term Type Substitution ~> ResultTriple)
	op-hook result4TupleSymbol
		({_,_,_,_} : Term Type Substitution Context ~> Result4Tuple)
	op-hook matchPairSymbol		({_,_} : Substitution Context ~> MatchPair)

	op-hook noParseSymbol		(noParse : Nat ~> ResultPair?)
	op-hook ambiguitySymbol		(ambiguity : ResultPair ResultPair ~> ResultPair?)
	op-hook failure3Symbol		(failure : ~> ResultTriple?)
	op-hook failure4Symbol		(failure : ~> Result4Tuple?)
	op-hook noMatchSubstSymbol	(noMatch : ~> Substitution?)
	op-hook noMatchPairSymbol	(noMatch : ~> MatchPair?)

	term-hook trueTerm		(true)
	term-hook falseTerm		(false))] .

  op metaRewrite : Module Term Bound ~> ResultPair
	[special (
	   id-hook MetaLevelOpSymbol	(metaRewrite)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaFrewrite : Module Term Bound Nat ~> ResultPair
	[special (
	   id-hook MetaLevelOpSymbol	(metaFrewrite)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaApply : Module Term Qid Substitution Nat ~> ResultTriple?
	[special (
	   id-hook MetaLevelOpSymbol	(metaApply)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaXapply : Module Term Qid Substitution Nat Bound Nat ~> Result4Tuple?
	[special (
	   id-hook MetaLevelOpSymbol	(metaXapply)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaMatch : Module Term Term Condition Nat ~> Substitution?
	[special (
	   id-hook MetaLevelOpSymbol	(metaMatch)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaXmatch : Module Term Term Condition Nat Bound Nat ~> MatchPair?
	[special (
	   id-hook MetaLevelOpSymbol	(metaXmatch)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaSearch : Module Term Term Condition Qid Bound Nat ~> ResultTriple?
	[special (
	   id-hook MetaLevelOpSymbol	(metaSearch)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op sortLeq : Module Sort Sort ~> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaSortLeq)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op sameKind : Module Type Type ~> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaSameKind)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op lesserSorts : Module Type ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaLesserSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op glbSorts : Module Sort Sort ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaGlbSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op leastSort : Module Term ~> Type
	[special (
	   id-hook MetaLevelOpSymbol	(metaLeastSort)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op completeName : Module Type ~> Type
	[special (
	   id-hook MetaLevelOpSymbol	(metaCompleteName)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaParse : Module QidList Type? ~> ResultPair?
	[special (
	   id-hook MetaLevelOpSymbol	(metaParse)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaPrettyPrint : Module Term ~> QidList
	[special (
	   id-hook MetaLevelOpSymbol	(metaPrettyPrint)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op wellFormed : Module -> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaWellFormedModule)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op wellFormed : Module Term ~> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaWellFormedTerm)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op wellFormed : Module Substitution ~> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaWellFormedSubstitution)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op getKind : Module Type ~> Kind
	[special (
	   id-hook MetaLevelOpSymbol	(metaGetKind)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op getKinds : Module ~> KindSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaGetKinds)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op maximalSorts : Module Kind ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaMaximalSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op minimalSorts : Module Kind ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaMinimalSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upMbs : Qid Bool ~> MembAxSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpMbs)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upEqs : Qid Bool ~> EquationSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpEqs)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upRls : Qid Bool ~> RuleSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpRls)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .
endfm

mod LOOP-MODE is
  protecting QID-LIST .
  sorts State System .
  op [_,_,_] : QidList State QidList -> System 
	[ctor special (
	   id-hook LoopSymbol
	   op-hook qidSymbol		(<Qids> : ~> Qid)
  	   op-hook nilQidListSymbol	(nil : ~> QidList)
	   op-hook qidListSymbol	(__ : QidList QidList ~> QidList))] .
endm

mod CONFIGURATION is
  sorts Attribute AttributeSet .
  subsort Attribute < AttributeSet .
  op none : -> AttributeSet .
  op _,_ : AttributeSet AttributeSet -> AttributeSet [ctor assoc comm id: none] .

  sorts Oid Cid Object Msg Configuration .
  subsort Object Msg < Configuration .
  op <_:_|_> : Oid Cid AttributeSet -> Object [ctor object].
  op none : -> Configuration .
  op __ : Configuration Configuration -> Configuration [ctor config assoc comm id: none] .
endm

set omod include CONFIGURATION on .

select NUMBER-CONVERSION .