fact SoundPDSs {
  all P : PDS |
    with P {
    all c : components, s : Service |  --1
      let c' = c.schedule[s] {
        (some c' iff s in c.import) && (some c' => s in c'.export) }
    all c : components | c.requires = c.schedule[Service]  }  --2
}