invariant[
          STATE: TYPE, 
          ACTION: TYPE+
]:
THEORY begin

    importing IOA

    CC_IOA: TYPE = IOA[STATE, ACTION].IOA

    cc_ioa: VAR CC_IOA
    c0, c: VAR STATE
    alpha: VAR ACTION

    invariant(cc_ioa, (inv: pred[STATE])): bool = 
        (forall c: reachable?(cc_ioa, c) IMPLIES inv(c))

    combined_invariant(cc_ioa, (combined, inv: pred[STATE])): bool =
        (forall c0: reachable?(cc_ioa, c0) and combined(c0) IMPLIES
            (forall c, alpha: transition(c0, cc_ioa, alpha, c) IMPLIES inv(c)))

END invariant