Warning: <standard input>, line 12 (mod FOO): variable Z is used before it is
    bound in rule:
crl f(X, Y, Y) => f(Z, X) if Z =/= Y = true .
mod FOO is
  including INT .
  sorts Foo .
  subsorts Int < Foo .
  op f : Int Int -> Int [assoc comm id: 1] .
  vars X Y Z : Int .
  eq f (f (X, Y), X) = f (Y, Y) .
  cq f (f (X, Y), Y) = f (Y, X) if X =/= Y .
  rl f (f (X, Y), X) => f (Y, Y) .
  crl f (f (X, Y), Y) => f (Z, X) if Z =/= Y .
  mb f (X, X) : NzInt .
  cmb f (X, Y) : NzInt if X =/= Y .
endm
Warning: membership axioms are not guaranteed to work correctly for iterated
    symbol s_ as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol _+_ as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol _*_ as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol gcd as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol lcm as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol min as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol max as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol _xor_ as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol _&_ as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol _|_ as it has declarations that are not at the kind level.
Warning: membership axioms are not guaranteed to work correctly for associative
    symbol f as it has declarations that are not at the kind level.
mod FOO is
  sorts Bool Zero NzNat Nat NzInt Int Foo .
  subsorts Zero NzNat NzNat < Nat .
  subsort NzNat < NzInt .
  subsorts NzInt Nat < Int .
  subsort Int < Foo .
  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
    0 gather (& & &) special (
    id-hook BranchSymbol
    term-hook 1 (true)
    term-hook 2 (false))] .
  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
    special (
    id-hook EqualitySymbol
    term-hook equalTerm (true)
    term-hook notEqualTerm (false))] .
  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
    special (
    id-hook EqualitySymbol
    term-hook equalTerm (false)
    term-hook notEqualTerm (true))] .
  op true : -> Bool [ctor special (
    id-hook SystemTrue)] .
  op false : -> Bool [ctor special (
    id-hook SystemFalse)] .
  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
  op not_ : Bool -> Bool [prec 53 gather (E)] .
  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
  op 0 : -> Zero [ctor] .
  op s_ : Nat -> NzNat [ctor iter prec 15 gather (E) special (
    id-hook SuccSymbol
    term-hook zeroTerm (0))] .
  op _+_ : NzNat Nat -> NzNat [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _+_ : Nat Nat -> Nat [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _+_ : Int Int -> Int [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : Nat Nat -> Nat [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : NzInt NzInt -> NzInt [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : Int Int -> Int [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _quo_ : Nat NzNat -> Nat [prec 31 gather (E e) special (
    id-hook NumberOpSymbol (quo)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 ~> NzInt))] .
  op _rem_ : Nat NzNat -> Nat [prec 31 gather (E e) special (
    id-hook NumberOpSymbol (rem)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 ~> NzInt))] .
  op _^_ : Nat Nat -> Nat [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : NzNat Nat -> NzNat [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : Int Nat -> Int [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : NzInt Nat -> NzInt [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op modExp : [Foo] [Foo] [Foo] -> [Foo] [special (
    id-hook NumberOpSymbol (modExp)
    op-hook succSymbol (s_ : Nat ~> NzNat))] .
  op gcd : NzNat Nat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : NzInt Int -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : Int Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : NzNat NzNat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : NzInt NzInt -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : Int Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : NzNat NzNat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : NzInt NzInt -> NzInt [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : Int Int -> Int [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzNat Nat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzInt NzInt -> NzInt [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Int Int -> Int [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzNat Int -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Nat Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _xor_ : Nat Nat -> Nat [assoc comm prec 55 gather (e E) special (
    id-hook ACU_NumberOpSymbol (xor)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _xor_ : Int Int -> Int [assoc comm prec 55 gather (e E) special (
    id-hook ACU_NumberOpSymbol (xor)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Nat Nat -> Nat [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Nat Int -> Nat [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Int Int -> Int [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : NzNat Nat -> NzNat [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : Nat Nat -> Nat [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : NzInt Int -> NzInt [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : Int Int -> Int [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _>>_ : Nat Nat -> Nat [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (>>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _>>_ : Int Nat -> Int [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (>>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<<_ : Nat Nat -> Nat [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (<<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<<_ : Int Nat -> Int [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (<<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<=_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<=_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>=_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>=_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _divides_ : NzNat Nat -> Bool [prec 51 gather (E E) special (
    id-hook NumberOpSymbol (divides)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _divides_ : NzInt Int -> Bool [prec 51 gather (E E) special (
    id-hook NumberOpSymbol (divides)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op -_ : NzNat -> NzInt [ctor prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op -_ : NzInt -> NzInt [prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op -_ : Int -> Int [prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _-_ : Int Int -> Int [prec 33 gather (E e) special (
    id-hook NumberOpSymbol (-)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op abs : NzInt -> NzNat [special (
    id-hook NumberOpSymbol (abs)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op abs : Int -> Nat [special (
    id-hook NumberOpSymbol (abs)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op ~_ : Int -> Int [prec 15 gather (E) special (
    id-hook NumberOpSymbol (~)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op f : Int Int -> Int [assoc comm id: 1] .
  var Z : Int .
  var X : Int .
  var Y : Int .
  mb f(X, X) : NzInt .
  cmb f(X, Y) : NzInt if X =/= Y = true .
  eq f(X, X, Y) = f(Y, Y) .
  ceq f(X, Y, Y) = f(X, Y) if X =/= Y = true .
  eq true and A:Bool = A:Bool .
  eq false and A:Bool = false .
  eq A:Bool and A:Bool = A:Bool .
  eq false xor A:Bool = A:Bool .
  eq A:Bool xor A:Bool = false .
  eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
  eq not A:Bool = true xor A:Bool .
  eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
  eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
  rl f(X, X, Y) => f(Y, Y) .
  crl f(X, Y, Y) => f(Z, X) if Z =/= Y = true [nonexec] .
endm
sort Bool .
sort Zero .	subsorts Zero < Nat Int Foo .
sort NzNat .	subsorts NzNat < Nat NzInt Int Foo .
sort Nat .	subsorts NzNat Zero < Nat < Int Foo .
sort NzInt .	subsorts NzNat < NzInt < Int Foo .
sort Int .	subsorts NzNat Zero Nat NzInt < Int < Foo .
sort Foo .	subsorts NzNat Zero Nat NzInt Int < Foo .
[Bool]:
	1	Bool

[Foo]:
	1	Foo
	2	Int
	3	NzInt
	4	Nat
	5	Zero
	6	NzNat
eq f(X, X, Y) = f(Y, Y) .
ceq f(X, Y, Y) = f(X, Y) if X =/= Y = true .
eq true and A:Bool = A:Bool .
eq false and A:Bool = false .
eq A:Bool and A:Bool = A:Bool .
eq false xor A:Bool = A:Bool .
eq A:Bool xor A:Bool = false .
eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
eq not A:Bool = true xor A:Bool .
eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
mb f(X, X) : NzInt .
cmb f(X, Y) : NzInt if X =/= Y = true .
rl f(X, X, Y) => f(Y, Y) .
crl f(X, Y, Y) => f(Z, X) if Z =/= Y = true [nonexec] .
var Z : Int .
var X : Int .
var Y : Int .
Grammar:
	nonterminals: 42
	terminals: 125
	productions: 193

Term rewriting system:
	kinds: 2
	sorts: 7
	user symbols: 35
	total symbols: 38
	polymorphic operators: 3
	membership axioms: 2
	equations: 11
	rules: 2
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 _^_ : NzInt Nat -> NzInt [ditto] .
  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 Int -> 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 min : NzInt NzInt -> NzInt [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op min : Int Int -> Int [ditto] .
  op max : NzInt NzInt -> NzInt [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op max : Int Int -> Int [ditto] .
  op max : NzNat Int -> NzNat [ditto] .
  op max : Nat 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 _&_ : Nat Int -> Nat [assoc comm prec 53 special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> Int))] .
  op _&_ : Int Int -> Int [ditto] .
  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
mod FOO is
  including INT .
  sorts Foo .
  subsorts Int < Foo .
  op f : Int Int -> Int [assoc comm id: 1] .
  vars X Y Z : Int .
  eq f (f (X, Y), X) = f (Y, Y) .
  cq f (f (X, Y), Y) = f (Y, X) if X =/= Y .
  rl f (f (X, Y), X) => f (Y, Y) .
  crl f (f (X, Y), Y) => f (Z, X) if Z =/= Y .
  mb f (X, X) : NzInt .
  cmb f (X, Y) : NzInt if X =/= Y .
endm
eq f(X, X, Y) = f(Y, Y) .
ceq f(X, Y, Y) = f(X, Y) if X =/= Y = true .
eq true and A:Bool = A:Bool .
eq false and A:Bool = false .
eq A:Bool and A:Bool = A:Bool .
eq false xor A:Bool = A:Bool .
eq A:Bool xor A:Bool = false .
eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
eq not A:Bool = true xor A:Bool .
eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
Int: f(0, 2)
mod FOO is
  sorts Bool Zero NzNat Nat NzInt Int Foo .
  subsorts Zero NzNat NzNat < Nat .
  subsort NzNat < NzInt .
  subsorts NzInt Nat < Int .
  subsort Int < Foo .
  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
    0 gather (& & &) special (
    id-hook BranchSymbol
    term-hook 1 (true)
    term-hook 2 (false))] .
  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
    special (
    id-hook EqualitySymbol
    term-hook equalTerm (true)
    term-hook notEqualTerm (false))] .
  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
    special (
    id-hook EqualitySymbol
    term-hook equalTerm (false)
    term-hook notEqualTerm (true))] .
  op true : -> Bool [ctor special (
    id-hook SystemTrue)] .
  op false : -> Bool [ctor special (
    id-hook SystemFalse)] .
  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
  op not_ : Bool -> Bool [prec 53 gather (E)] .
  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
  op 0 : -> Zero [ctor] .
  op s_ : Nat -> NzNat [ctor iter prec 15 gather (E) special (
    id-hook SuccSymbol
    term-hook zeroTerm (0))] .
  op _+_ : NzNat Nat -> NzNat [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _+_ : Nat Nat -> Nat [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _+_ : Int Int -> Int [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : Nat Nat -> Nat [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : NzInt NzInt -> NzInt [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : Int Int -> Int [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _quo_ : Nat NzNat -> Nat [prec 31 gather (E e) special (
    id-hook NumberOpSymbol (quo)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 ~> NzInt))] .
  op _rem_ : Nat NzNat -> Nat [prec 31 gather (E e) special (
    id-hook NumberOpSymbol (rem)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 ~> NzInt))] .
  op _^_ : Nat Nat -> Nat [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : NzNat Nat -> NzNat [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : Int Nat -> Int [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : NzInt Nat -> NzInt [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op modExp : [Foo] [Foo] [Foo] -> [Foo] [special (
    id-hook NumberOpSymbol (modExp)
    op-hook succSymbol (s_ : Nat ~> NzNat))] .
  op gcd : NzNat Nat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : NzInt Int -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : Int Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : NzNat NzNat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : NzInt NzInt -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : Int Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : NzNat NzNat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : NzInt NzInt -> NzInt [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : Int Int -> Int [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzNat Nat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzInt NzInt -> NzInt [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Int Int -> Int [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzNat Int -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Nat Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _xor_ : Nat Nat -> Nat [assoc comm prec 55 gather (e E) special (
    id-hook ACU_NumberOpSymbol (xor)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _xor_ : Int Int -> Int [assoc comm prec 55 gather (e E) special (
    id-hook ACU_NumberOpSymbol (xor)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Nat Nat -> Nat [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Nat Int -> Nat [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Int Int -> Int [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : NzNat Nat -> NzNat [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : Nat Nat -> Nat [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : NzInt Int -> NzInt [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : Int Int -> Int [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _>>_ : Nat Nat -> Nat [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (>>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _>>_ : Int Nat -> Int [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (>>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<<_ : Nat Nat -> Nat [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (<<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<<_ : Int Nat -> Int [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (<<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<=_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<=_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>=_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>=_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _divides_ : NzNat Nat -> Bool [prec 51 gather (E E) special (
    id-hook NumberOpSymbol (divides)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _divides_ : NzInt Int -> Bool [prec 51 gather (E E) special (
    id-hook NumberOpSymbol (divides)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op -_ : NzNat -> NzInt [ctor prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op -_ : NzInt -> NzInt [prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op -_ : Int -> Int [prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _-_ : Int Int -> Int [prec 33 gather (E e) special (
    id-hook NumberOpSymbol (-)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op abs : NzInt -> NzNat [special (
    id-hook NumberOpSymbol (abs)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op abs : Int -> Nat [special (
    id-hook NumberOpSymbol (abs)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op ~_ : Int -> Int [prec 15 gather (E) special (
    id-hook NumberOpSymbol (~)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op f : Int Int -> Int [assoc comm id: 1] .
  var Z : Int .
  var X : Int .
  var Y : Int .
  mb f(X, X) : NzInt .
  cmb f(X, Y) : NzInt if _=/=_(X, Y) = true .
  eq f(X, X, Y) = f(Y, Y) .
  ceq f(X, Y, Y) = f(X, Y) if _=/=_(X, Y) = true .
  eq _and_(true, A:Bool) = A:Bool .
  eq _and_(false, A:Bool) = false .
  eq _and_(A:Bool, A:Bool) = A:Bool .
  eq _xor_(false, A:Bool) = A:Bool .
  eq _xor_(A:Bool, A:Bool) = false .
  eq _and_(A:Bool, _xor_(B:Bool, C:Bool)) = _xor_(_and_(A:Bool, B:Bool), _and_(
    A:Bool, C:Bool)) .
  eq not_(A:Bool) = _xor_(true, A:Bool) .
  eq _or_(A:Bool, B:Bool) = _xor_(_and_(A:Bool, B:Bool), _xor_(A:Bool, B:Bool))
    .
  eq _implies_(A:Bool, B:Bool) = not_(_xor_(A:Bool, _and_(A:Bool, B:Bool))) .
  rl f(X, X, Y) => f(Y, Y) .
  crl f(X, Y, Y) => f(Z, X) if _=/=_(Z, Y) = true [nonexec] .
endm
mod FOO is
  sorts Bool Zero NzNat Nat NzInt Int Foo .
  subsorts Zero NzNat NzNat < Nat .
  subsort NzNat < NzInt .
  subsorts NzInt Nat < Int .
  subsort Int < Foo .
  op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
    0 gather (& & &) special (
    id-hook BranchSymbol
    term-hook 1 (true)
    term-hook 2 (false))] .
  op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
    special (
    id-hook EqualitySymbol
    term-hook equalTerm (true)
    term-hook notEqualTerm (false))] .
  op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
    special (
    id-hook EqualitySymbol
    term-hook equalTerm (false)
    term-hook notEqualTerm (true))] .
  op true : -> Bool [ctor special (
    id-hook SystemTrue)] .
  op false : -> Bool [ctor special (
    id-hook SystemFalse)] .
  op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
  op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
  op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
  op not_ : Bool -> Bool [prec 53 gather (E)] .
  op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
  op 0 : -> Zero [ctor] .
  op s_ : Nat -> NzNat [ctor iter prec 15 gather (E) special (
    id-hook SuccSymbol
    term-hook zeroTerm (0))] .
  op _+_ : NzNat Nat -> NzNat [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _+_ : Nat Nat -> Nat [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _+_ : Int Int -> Int [assoc comm prec 33 gather (e E) special (
    id-hook ACU_NumberOpSymbol (+)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : Nat Nat -> Nat [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : NzInt NzInt -> NzInt [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _*_ : Int Int -> Int [assoc comm prec 31 gather (e E) special (
    id-hook ACU_NumberOpSymbol (*)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _quo_ : Nat NzNat -> Nat [prec 31 gather (E e) special (
    id-hook NumberOpSymbol (quo)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 ~> NzInt))] .
  op _rem_ : Nat NzNat -> Nat [prec 31 gather (E e) special (
    id-hook NumberOpSymbol (rem)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  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 ~> NzInt))] .
  op _^_ : Nat Nat -> Nat [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : NzNat Nat -> NzNat [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : Int Nat -> Int [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _^_ : NzInt Nat -> NzInt [prec 29 gather (E e) special (
    id-hook NumberOpSymbol (^)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op modExp : [Foo] [Foo] [Foo] -> [Foo] [special (
    id-hook NumberOpSymbol (modExp)
    op-hook succSymbol (s_ : Nat ~> NzNat))] .
  op gcd : NzNat Nat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : NzInt Int -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op gcd : Int Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (gcd)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : NzNat NzNat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : NzInt NzInt -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op lcm : Int Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (lcm)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : NzNat NzNat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : NzInt NzInt -> NzInt [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op min : Int Int -> Int [assoc comm special (
    id-hook ACU_NumberOpSymbol (min)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzNat Nat -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Nat Nat -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzInt NzInt -> NzInt [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Int Int -> Int [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : NzNat Int -> NzNat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op max : Nat Int -> Nat [assoc comm special (
    id-hook ACU_NumberOpSymbol (max)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _xor_ : Nat Nat -> Nat [assoc comm prec 55 gather (e E) special (
    id-hook ACU_NumberOpSymbol (xor)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _xor_ : Int Int -> Int [assoc comm prec 55 gather (e E) special (
    id-hook ACU_NumberOpSymbol (xor)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Nat Nat -> Nat [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Nat Int -> Nat [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _&_ : Int Int -> Int [assoc comm prec 53 gather (e E) special (
    id-hook ACU_NumberOpSymbol (&)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : NzNat Nat -> NzNat [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : Nat Nat -> Nat [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : NzInt Int -> NzInt [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _|_ : Int Int -> Int [assoc comm prec 57 gather (e E) special (
    id-hook ACU_NumberOpSymbol (|)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _>>_ : Nat Nat -> Nat [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (>>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _>>_ : Int Nat -> Int [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (>>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<<_ : Nat Nat -> Nat [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (<<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<<_ : Int Nat -> Int [prec 35 gather (E e) special (
    id-hook NumberOpSymbol (<<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _<_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<=_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _<=_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (<=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>=_ : Nat Nat -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _>=_ : Int Int -> Bool [prec 37 gather (E E) special (
    id-hook NumberOpSymbol (>=)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _divides_ : NzNat Nat -> Bool [prec 51 gather (E E) special (
    id-hook NumberOpSymbol (divides)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op _divides_ : NzInt Int -> Bool [prec 51 gather (E E) special (
    id-hook NumberOpSymbol (divides)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt)
    term-hook trueTerm (true)
    term-hook falseTerm (false))] .
  op -_ : NzNat -> NzInt [ctor prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op -_ : NzInt -> NzInt [prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op -_ : Int -> Int [prec 15 gather (E) special (
    id-hook MinusSymbol
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op _-_ : Int Int -> Int [prec 33 gather (E e) special (
    id-hook NumberOpSymbol (-)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op abs : NzInt -> NzNat [special (
    id-hook NumberOpSymbol (abs)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op abs : Int -> Nat [special (
    id-hook NumberOpSymbol (abs)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op ~_ : Int -> Int [prec 15 gather (E) special (
    id-hook NumberOpSymbol (~)
    op-hook succSymbol (s_ : Nat ~> NzNat)
    op-hook minusSymbol (-_ : NzNat ~> NzInt))] .
  op f : Int Int -> Int [assoc comm id: 1] .
  var Z : Int .
  var X : Int .
  var Y : Int .
  mb f(X, X) : NzInt .
  cmb f(X, Y) : NzInt if (X =/= Y) = true .
  eq f(X, X, Y) = f(Y, Y) .
  ceq f(X, Y, Y) = f(X, Y) if (X =/= Y) = true .
  eq (true and A:Bool) = A:Bool .
  eq (false and A:Bool) = false .
  eq (A:Bool and A:Bool) = A:Bool .
  eq (false xor A:Bool) = A:Bool .
  eq (A:Bool xor A:Bool) = false .
  eq (A:Bool and (B:Bool xor C:Bool)) = ((A:Bool and B:Bool) xor (A:Bool and
    C:Bool)) .
  eq (not A:Bool) = (true xor A:Bool) .
  eq (A:Bool or B:Bool) = ((A:Bool and B:Bool) xor (A:Bool xor B:Bool)) .
  eq (A:Bool implies B:Bool) = (not (A:Bool xor (A:Bool and B:Bool))) .
  rl f(X, X, Y) => f(Y, Y) .
  crl f(X, Y, Y) => f(Z, X) if (Z =/= Y) = true [nonexec] .
endm
Bye.