def EqCheckingAbstractInterpretation.Ready.DiffSysRSLe {Action : Type u} {Name : Type v} (ρ σ : DiffSysRS Action Name (RSObs Action)) : Prop

Pointwise order on RS difference systems.

Equations

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

def EqCheckingAbstractInterpretation.Ready.DRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρ : DiffSysRS Action Name (RSObs Action)) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : RSObs Action → Prop

Concrete predecessor transformer for ready-style observations. This mirrors the paper's RS predecessor intuition at the concrete level.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.DRS env ρ p Q EqCheckingAbstractInterpretation.Ready.RSObs.tt = ∀ (q : EqCheckingAbstractInterpretation.CCS.CCS Action Name), ¬Q q

theorem EqCheckingAbstractInterpretation.Ready.dRS_mono {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) {ρ σ : DiffSysRS Action Name (RSObs Action)} (hLe : DiffSysRSLe ρ σ) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) : DRS env ρ p Q o → DRS env σ p Q o

DRS is monotone in the difference-system argument.

def EqCheckingAbstractInterpretation.Ready.lfpDRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : DiffSysRS Action Name (RSObs Action)

Least fixpoint of DRS, defined as intersection of all pre-fixpoints.

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.lfpDRS_prefixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) : DRS env (lfpDRS env) p Q o → lfpDRS env p Q o

lfpDRS is a pre-fixpoint of DRS.

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

αcap(lfpDRS) is itself a pre-fixpoint: one DRS step stays within αcap(lfpDRS). This is the RS analogue of alpha_lfpDTr_is_prefixpoint.

theorem EqCheckingAbstractInterpretation.Ready.alpha_lfpDRS_le_of_abstract_prefixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) (hρa : ∀ (p' : CCS.CCS Action Name) (Q' : ProcSet Action Name) (c' : Capability), alphaCapRaw rsObsCap (lfpDRS env p' Q') c' → ρa p' Q' c') (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) (hAlpha : alphaCapRaw rsObsCap (lfpDRS env p Q) c) : ρa p Q c

αcap(lfpDRS(p,Q)) is below every abstract pre-fixpoint of DRS. Combined with alpha_lfpDRS_is_prefixpoint, this yields lfpDRSAbsCanon_spec. This is the RS analogue of alpha_lfpDTr_le_of_abstract_prefixpoint.