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_no_self {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (hMember : Q p) (o : RSObs Action) : ¬lfpDRS env p Q o

A process already among the competitors has no distinguishing observation.

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.lfpDRS_postfixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) (hLfp : lfpDRS env p Q o) : DRS env (lfpDRS env) p Q o

A concrete least-fixed-point observation is generated by one DRS predecessor step.