SemComm : Comm !$\rightarrow$! 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
    (!$\lambda$! (n : $mathbb{N}$) !$\rightarrow$!
      RelOpState.comp (RelOpState.repeat
        n
        (RelOpState.comp
          (RelOpState.delta (SemCond b))
          (SemComm c)))
      (RelOpState.delta (NotP (SemCond b))))

Satisfies : Cond !$\rightarrow$! Comm !$\rightarrow$! Cond !$\rightarrow$! Set
Satisfies bPre cm bPost
  = (s1 : State) !$\rightarrow$! (s2 : State) !$\rightarrow$!
    SemCond bPre s1 !$\rightarrow$! SemComm cm s1 s2 !$\rightarrow$! SemCond bPost s2