data specification nat = 0 | . +1(. -1 : nat) ; variables n : nat; m : nat; order predicates . < . : nat × nat; end data specification