theorem EqCheckingAbstractInterpretation.Ready.concrete_of_gammaDRSAbsExact {Action : Type u} {Name : Type v} (ρ : DiffSysRS Action Name (RSObs Action)) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) (hGamma : gammaDRSAbs (fun (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) => alphaCap rsObsCap (ρ p Q) c) p Q o) : ∃ (o' : RSObs Action), ρ p Q o' ∧ capLe (reqOfObs o') (reqOfObs o)

Any observation admitted by the exact concretization of an exact capability abstraction has a concrete witness whose required capability is no larger.

theorem EqCheckingAbstractInterpretation.Ready.concrete_of_DRS_gammaDRSAbsExact {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) (o : RSObs Action) (hDRS : DRS env (gammaDRSAbs fun (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) => alphaCap rsObsCap (ρ p Q) c) p Q o) : ∃ (o' : RSObs Action), DRS env ρ p Q o' ∧ capLe (reqOfObs o') (reqOfObs o)

One DRS step over the exact concretization of an exact capability abstraction can be rebuilt as a concrete DRS step, possibly with smaller child observations at each positive branch occurrence.

theorem EqCheckingAbstractInterpretation.Ready.backwardComplete_bestDRS {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) (c : Capability) : alphaCap rsObsCap (DRS env ρ p Q) c ↔ bestDRS env (fun (p' : CCS.CCS Action Name) (Q' : ProcSet Action Name) (c' : Capability) => alphaCap rsObsCap (ρ p' Q') c') p Q c

Backward completeness (pointwise) of the capability abstraction for bestDRS: αcap ∘ DRS = bestDRS ∘ αcap.

theorem EqCheckingAbstractInterpretation.Ready.backwardComplete_bestDRS_funext {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρ : DiffSysRS Action Name (RSObs Action)) : (fun (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) => alphaCap rsObsCap (DRS env ρ p Q) c) = bestDRS env fun (p' : CCS.CCS Action Name) (Q' : ProcSet Action Name) (c' : Capability) => alphaCap rsObsCap (ρ p' Q') c'

Function-extensional form of backwardComplete_bestDRS.

theorem EqCheckingAbstractInterpretation.Ready.gammaDRSAbs_prefixpoint_of_abstract_prefixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) (hρa : BestDRSPrefixpoint env ρa) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) : DRS env (gammaDRSAbs ρa) p Q o → gammaDRSAbs ρa p Q o

Any abstract pre-fixpoint induces a concrete pre-fixpoint via gammaDRSAbs.

theorem EqCheckingAbstractInterpretation.Ready.concrete_of_gammaDRSAbsExactCanon {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) (hGamma : gammaDRSAbs (fun (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) => alphaCap rsObsCap (lfpDRS env p Q) c) p Q o) : ∃ (o' : RSObs Action), lfpDRS env p Q o' ∧ capLe (reqOfObs o') (reqOfObs o)

Any observation admitted by the exact concretization of the canonical abstract lfp has a concrete lfpDRS witness whose required capability is no larger.

theorem EqCheckingAbstractInterpretation.Ready.concrete_of_DRS_gammaDRSAbsExactCanon {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) (hDRS : DRS env (gammaDRSAbs fun (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) => alphaCap rsObsCap (lfpDRS env p Q) c) p Q o) : ∃ (o' : RSObs Action), DRS env (lfpDRS env) p Q o' ∧ capLe (reqOfObs o') (reqOfObs o)

One DRS step over the exact concretization of the canonical abstract lfp can be rebuilt as a concrete DRS step over lfpDRS, possibly with smaller child observations at each positive branch occurrence.

theorem EqCheckingAbstractInterpretation.Ready.lfpBestDRS_le_of_abstract_prefixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρa : AbsSysRS Action Name) (hρa : BestDRSPrefixpoint env ρa) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) (hLfp : lfpBestDRS env p Q c) : upClosure (ρa p Q) c

lfpBestDRS lies below every abstract pre-fixpoint of bestDRS.

theorem EqCheckingAbstractInterpretation.Ready.lfpDRSAbsExactCanon_prefixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : BestDRSPrefixpoint env (lfpDRSAbsExactCanon env)

The exact canonical abstraction induced by lfpDRS is a pre-fixpoint of bestDRS.

theorem EqCheckingAbstractInterpretation.Ready.below_all_abstract_prefixpoints_iff_alphaCapRaw_lfpDRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability) : (∀ (ρa : AbsSysRS Action Name), BestDRSPrefixpoint env ρa → upClosure (ρa p Q) c) ↔ alphaCapRaw rsObsCap (lfpDRS env p Q) c

theorem EqCheckingAbstractInterpretation.Ready.lfpBestDRS_eq_lfpDRSAbsExactCanon {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : lfpBestDRS env = lfpDRSAbsExactCanon env

The abstract lfp of bestDRS coincides with the canonical exact abstraction of lfpDRS.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_iff_notPreorderAt_rsObs_of_lfp {Action : Type u} {Name : Type v} (lfpConcrete : DiffSysRS Action Name (RSObs Action)) (lfpAbs : AbsSysRS Action Name) (hLfp : ∀ (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability), lfpAbs p Q c ↔ alphaCapRaw rsObsCap (lfpConcrete p Q) c) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt lfpAbs N p Q ↔ notPreorderAt rsObsCap lfpConcrete N p Q

Concrete instantiation of the unified lfp-level threshold theorem for the observation syntax RSObs.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_iff_notPreorderAt_rsObs_of_lfpCanon {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt (lfpDRSAbsCanon env) N p Q ↔ notPreorderAt rsObsCap (lfpDRS env) N p Q

Assumption-free canonical variant: instantiate the abstract side directly as alphaCapRaw applied to the concrete lfp.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_iff_notPreorderAt_rsObs_of_lfpExactCanon {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt (lfpDRSAbsExactCanon env) N p Q ↔ notPreorderAt rsObsCap (lfpDRS env) N p Q

Exact-pruned canonical variant: instantiate the abstract side as alphaCap.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_iff_rsDifferenceThreshold {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt (lfpDRSAbsCanon env) N p Q ↔ ∃ (o : RSObs Action), RSDifferenceToSet env p Q o ∧ rsObsCap N o

Concrete threshold exactness stated directly over RSDifferenceToSet.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAtExact_iff_rsDifferenceThreshold {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt (lfpDRSAbsExactCanon env) N p Q ↔ ∃ (o : RSObs Action), RSDifferenceToSet env p Q o ∧ rsObsCap N o

Exact-pruned threshold exactness stated directly over RSDifferenceToSet.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_lfpBestDRS_iff_rsDifferenceThreshold {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt (lfpBestDRS env) N p Q ↔ ∃ (o : RSObs Action), RSDifferenceToSet env p Q o ∧ rsObsCap N o

Exact-pruned threshold theorem stated over the abstract lfp lfpBestDRS.

theorem EqCheckingAbstractInterpretation.Ready.thresholdWitness_lfpBestDRS_iff_rsDifferenceThreshold {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : (∃ (c : Capability), lfpBestDRS env p Q c ∧ capLe c N) ↔ ∃ (o : RSObs Action), RSDifferenceToSet env p Q o ∧ rsObsCap N o

Paper-style threshold exactness for the abstract lfp lfpBestDRS.