def EqCheckingAbstractInterpretation.Trace.ConcreteDiffNonempty {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : Prop

Concrete non-emptiness of trace difference for process-vs-set pairs.

Equations

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

theorem EqCheckingAbstractInterpretation.Trace.DTrSharp_eq_alpha_comp_DTr_comp_gamma {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (ρa : CCS.CCS Action Name → CCS.ProcSet Action Name → Prop) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : DTrSharp ρ ρa p Q ↔ alphaDiffSys (DTr ρ (gammaDiffSys ρa)) p Q

theorem EqCheckingAbstractInterpretation.Trace.alphaDiffSys_gammaDiffSys {Action : Type u} {Name : Type v} (ρa : AbsDiffSys Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : alphaDiffSys (gammaDiffSys ρa) p Q ↔ ρa p Q

alpha followed by gamma is pointwise the identity for the non-emptiness abstraction.

theorem EqCheckingAbstractInterpretation.Trace.backwardComplete_DTr {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (ρc : DiffSys Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : alphaDiffSys (DTr ρ ρc) p Q ↔ DTrSharp ρ (alphaDiffSys ρc) p Q

Backward completeness (pointwise) of the non-emptiness abstraction for DTr: α ∘ DTr = DTrSharp ∘ α.

theorem EqCheckingAbstractInterpretation.Trace.backwardComplete_DTr_funext {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (ρc : DiffSys Action Name) : alphaDiffSys (DTr ρ ρc) = DTrSharp ρ (alphaDiffSys ρc)

theorem EqCheckingAbstractInterpretation.Trace.gammaDiffSys_prefixpoint_of_abstract_prefixpoint {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (ρa : AbsDiffSys Action Name) (hρa : ∀ (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name), DTrSharp ρ ρa p Q → ρa p Q) (p : CCS.CCS Action Name) (Q : CCS.CCS Action Name → Prop) (tr : Trace Action) : DTr ρ (gammaDiffSys ρa) p Q tr → gammaDiffSys ρa p Q tr

Any abstract pre-fixpoint induces a concrete pre-fixpoint via gamma. This is the bridge from abstract pre-fixpoints to concrete ones used in the lfp-comparison chain (specifically in alpha_lfpDTr_le_of_abstract_prefixpoint).

theorem EqCheckingAbstractInterpretation.Trace.alpha_lfpDTr_is_prefixpoint {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : DTrSharp ρ (alphaDiffSys (lfpDTr ρ)) p Q → alphaDiffSys (lfpDTr ρ) p Q

alpha applied to the concrete lfp is a pre-fixpoint of DTrSharp. This is the "converse" direction in the lfp alignment proof.

theorem EqCheckingAbstractInterpretation.Trace.alpha_lfpDTr_le_of_abstract_prefixpoint {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (ρa : AbsDiffSys Action Name) (hρa : ∀ (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name), DTrSharp ρ ρa p Q → ρa p Q) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : alphaDiffSys (lfpDTr ρ) p Q → ρa p Q

alpha(lfpDTr) is below every abstract pre-fixpoint of DTrSharp. Combined with alpha_lfpDTr_is_prefixpoint, this yields lfpDTrSharp_iff_alpha_lfpDTr.

theorem EqCheckingAbstractInterpretation.Trace.lfpDTrSharp_iff_alpha_lfpDTr {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : lfpDTrSharp ρ p Q ↔ alphaDiffSys (lfpDTr ρ) p Q

The abstract least fixpoint coincides pointwise with alpha of the concrete lfp.

theorem EqCheckingAbstractInterpretation.Trace.markerPresence_iff_alpha_lfpDTr {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : AbstractDiff ρ p Q ↔ alphaDiffSys (lfpDTr ρ) p Q

Canonical best-correct-approximation statement, pointwise at (p,Q): marker derivability (the abstract lfp result) equals alpha applied to the concrete least fixpoint.

theorem EqCheckingAbstractInterpretation.Trace.markerPresence_iff_lfpDTr_nonempty {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : AbstractDiff ρ p Q ↔ ∃ (tr : Trace Action), lfpDTr ρ p Q tr

Best-abstraction view for marker analysis: AbstractDiff is exact for the abstraction "is the concrete lfp non-empty?".

theorem EqCheckingAbstractInterpretation.Trace.markerPresence_iff_concreteDiffNonempty {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.ProcSet Action Name) : AbstractDiff ρ p Q ↔ ConcreteDiffNonempty ρ p Q

Main correctness characterization from the note: marker presence is equivalent to concrete non-empty trace difference.

theorem EqCheckingAbstractInterpretation.Trace.markerPresence_singleton_iff_traceDifferenceNonempty {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : MarkerFailsPreorder ρ p q ↔ ∃ (tr : Trace Action), TraceDifference ρ p q tr

theorem EqCheckingAbstractInterpretation.Trace.tracePreorder_iff_no_marker {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : TracePreorder ρ p q ↔ ¬MarkerFailsPreorder ρ p q

theorem EqCheckingAbstractInterpretation.Trace.traceEquivalent_iff_no_markers {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : TraceEquivalent ρ p q ↔ ¬MarkerFailsPreorder ρ p q ∧ ¬MarkerFailsPreorder ρ q p

theorem EqCheckingAbstractInterpretation.Trace.markerFails_implies_not_tracePreorder {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : MarkerFailsPreorder ρ p q → ¬TracePreorder ρ p q

theorem EqCheckingAbstractInterpretation.Trace.not_tracePreorder_implies_markerFails {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : ¬TracePreorder ρ p q → MarkerFailsPreorder ρ p q

theorem EqCheckingAbstractInterpretation.Trace.markerFails_iff_not_tracePreorder {Action : Type u} {Name : Type v} (ρ : CCS.Env Action Name) (p q : CCS.CCS Action Name) : MarkerFailsPreorder ρ p q ↔ ¬TracePreorder ρ p q