automaton PitchTwoA(s: Set[Nat])
  signature output pitch(n: Nat)
  states left: Set[Nat] := s
  transitions output pitch(n; local x: Nat) 
    pre n \in left /\ \E x: Nat (x \in left /\ n < x)
    eff left := choose s' 
          where \E x: Nat (x \in left /\ n < x /\ s' = delete(n, delete(x, left)))