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.bestDRS {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.bestDRSRawExplicit {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) : AbsSysRS Action Name

Raw explicit expansion of bestDRS: 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.bestDRSExplicit {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

• EqCheckingAbstractInterpretation.Ready.bestDRSExplicit env ρa p Q c = EqCheckingAbstractInterpretation.Ready.minimalCap (EqCheckingAbstractInterpretation.Ready.bestDRSRawExplicit env ρa p Q) c

theorem EqCheckingAbstractInterpretation.Ready.bestDRSRawExplicit_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) : bestDRSRawExplicit 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.bestDRSExplicit_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) : bestDRSExplicit env ρa p Q c ↔ bestDRS env ρa p Q c

The explicit paper-style transformer agrees pointwise with bestDRS.

theorem EqCheckingAbstractInterpretation.Ready.bestDRSExplicit_eq_bestDRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) : bestDRSExplicit env ρa = bestDRS env ρa

The explicit paper-style transformer is definitionally equivalent to bestDRS.

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

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

Equations

• EqCheckingAbstractInterpretation.Ready.BestDRSPrefixpoint env ρa = EqCheckingAbstractInterpretation.Ready.AbsSysRSLe (EqCheckingAbstractInterpretation.Ready.bestDRS env ρa) ρa

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

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

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.bestDRS_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) : bestDRS 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.