SemComm : Comm -> Rel State (Level.zero)
SemComm Skip = RelOpState.deltaGlob
SemComm Abort = RelOpState.emptyRel
SemComm (PComm pc) = PrimSemComm pc
SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
SemComm (If b c1 c2)
  = RelOpState.union
    (RelOpState.comp (RelOpState.delta (SemCond b))
                     (SemComm c1))
    (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
                     (SemComm c2))
SemComm (While b c)
  = RelOpState.unionInf
    (λ (n : $mathbb{N}$) ->
      RelOpState.comp (RelOpState.repeat
        n
        (RelOpState.comp
          (RelOpState.delta (SemCond b))
          (SemComm c)))
      (RelOpState.delta (NotP (SemCond b))))

Satisfies : Cond -> Comm -> Cond -> Set
Satisfies bPre cm bPost
  = (s1 : State) -> (s2 : State) ->
    SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2