inductive EqCheckingAbstractInterpretation.Ready.RSSem {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : CCS.CCS Action Name → RSObs Action → Prop

A single process satisfies a ready-simulation observation.

• tt {Action : Type u} {Name : Type v} {env : CCS.Env Action Name} (p : CCS.CCS Action Name) : RSSem env p RSObs.tt
• node {Action : Type u} {Name : Type v} {env : CCS.Env Action Name} (p : CCS.CCS Action Name) (pos : List (Action × RSObs Action)) (neg : List Action) (next : Fin pos.length → CCS.CCS Action Name) (hDer : ∀ (i : Fin pos.length), CCS.Deriv env p (pos.get i).fst (next i)) (hNeg : ∀ (b : Action), b ∈ neg → ¬CCS.Enabled env p b) (hPos : ∀ (i : Fin pos.length), RSSem env (next i) (pos.get i).snd) : RSSem env p (RSObs.node pos neg)

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

Difference of independent single-process ready-simulation denotations.

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.rsDifferenceToSet_eq_lfpDRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) : RSDifferenceToSet env p Q o ↔ lfpDRS env p Q o

Independent denotational difference equals the concrete least fixpoint.

def EqCheckingAbstractInterpretation.Ready.RSWitnessPreorder {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p q : CCS.CCS Action Name) : Prop

Witness-preorder induced by RS difference lfp emptiness.

Equations

• EqCheckingAbstractInterpretation.Ready.RSWitnessPreorder env p q = ¬∃ (o : EqCheckingAbstractInterpretation.Ready.RSObs Action), EqCheckingAbstractInterpretation.Ready.lfpDRS env p {q} o

def EqCheckingAbstractInterpretation.Ready.RSWitnessPreorderAt {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (N : Capability) (p q : CCS.CCS Action Name) : Prop

Witness preorder restricted to observations expressible at a capability threshold.

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.rsWitnessPreorder_iff_rsDiffEmpty {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p q : CCS.CCS Action Name) : RSWitnessPreorder env p q ↔ ¬∃ (o : RSObs Action), RSDifferenceToSet env p {q} o

Corollary: witness-preorder equals emptiness of concrete RS difference.