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

Concrete RS difference relation used in the current mechanization. At this stage it is taken to be the least model of the concrete predecessor transformer DRS.

Equations

• EqCheckingAbstractInterpretation.Ready.RSDifferenceToSet env = EqCheckingAbstractInterpretation.Ready.lfpDRS env

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

By definition of RSDifferenceToSet, the lfp characterization is immediate.

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

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.