def EqCheckingAbstractInterpretation.Ready.AbsSysRSLe {Action : Type u} {Name : Type v} (ρa σa : AbsSysRS Action Name) : Prop

Pointwise order on abstract capability systems via upward-closure inclusion.

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.gammaDRSAbs {Action : Type u} {Name : Type v} (ρa : AbsSysRS Action Name) : DiffSysRS Action Name (RSObs Action)

Exact concretization of a capability antichain back to RS observations. An observation is represented whenever one abstract capability is below its exact required capability.

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.abstractDRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) : AbsSysRS Action Name

Exact abstract predecessor transformer on minimal capability antichains.

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.abstractDRSRawExplicit {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) : AbsSysRS Action Name

Raw explicit expansion of abstractDRS: choose one-step RS observations together with child capabilities justifying their membership in the concretization.

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.abstractDRSExplicit {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) : AbsSysRS Action Name

Minimal-capability pruning of the explicit paper-style predecessor transformer.

Equations

• One or more equations did not get rendered due to their size.

theorem EqCheckingAbstractInterpretation.Ready.abstractDRSRawExplicit_spec {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) : abstractDRSRawExplicit env ρa p Q c ↔ alphaCapRaw rsObsCap (DRS env (gammaDRSAbs ρa) p Q) c

Pointwise equivalence between the explicit raw transformer and alphaCapRaw.

theorem EqCheckingAbstractInterpretation.Ready.abstractDRSExplicit_iff {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) : abstractDRSExplicit env ρa p Q c ↔ abstractDRS env ρa p Q c

The explicit paper-style transformer agrees pointwise with abstractDRS.

theorem EqCheckingAbstractInterpretation.Ready.abstractDRSExplicit_eq_abstractDRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) : abstractDRSExplicit env ρa = abstractDRS env ρa

The explicit paper-style transformer equals abstractDRS by extensionality.

def EqCheckingAbstractInterpretation.Ready.AbstractDRSPrefixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) : Prop

Abstract pre-fixpoints of abstractDRS with respect to the antichain order.

Equations

• EqCheckingAbstractInterpretation.Ready.AbstractDRSPrefixpoint env ρa = EqCheckingAbstractInterpretation.Ready.AbsSysRSLe (EqCheckingAbstractInterpretation.Ready.abstractDRS env ρa) ρa

def EqCheckingAbstractInterpretation.Ready.lfpAbstractDRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : AbsSysRS Action Name

Least abstract fixpoint of abstractDRS, defined via intersection of upward closures.

Equations

• One or more equations did not get rendered due to their size.

theorem EqCheckingAbstractInterpretation.Ready.abstractDRS_spec {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) : abstractDRS env ρa p Q c ↔ alphaCap rsObsCap (DRS env (gammaDRSAbs ρa) p Q) c

Pointwise expansion of the exact abstract predecessor transformer.

def EqCheckingAbstractInterpretation.Ready.lfpDRSAbsCanon {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : AbsSysRS Action Name

Canonical abstract lfp induced by concrete lfp via alphaCapRaw.

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Ready.lfpDRSAbsExactCanon {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : AbsSysRS Action Name

Exact canonical abstract difference induced by the concrete lfp via alphaCap.

Equations

• One or more equations did not get rendered due to their size.

theorem EqCheckingAbstractInterpretation.Ready.lfpDRSAbsCanon_spec {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) : lfpDRSAbsCanon env p Q c ↔ alphaCapRaw rsObsCap (lfpDRS env p Q) c

Pointwise specification of the canonical abstract lfp.

theorem EqCheckingAbstractInterpretation.Ready.lfpDRSAbsExactCanon_spec {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) : lfpDRSAbsExactCanon env p Q c ↔ alphaCap rsObsCap (lfpDRS env p Q) c

Pointwise specification of the exact canonical abstract lfp.