(sorts Int, Nat, s

sorts Nat < Int

op 0 : Nat

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

### Hint 8.8, known variable shadowed 'a'