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