(sorts Int, Nat, s

sorts Nat < Int

op 0 : Nat

op __-__ : Nat * Nat -> Int,[ . forall v1: Nat . def v1 - 0 ])

*** Warning 8.8, known variable shadowed 'a'