@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.ProcSet (Action : Type u) (Name : Type v) : Type (max v u)

Equations

• EqCheckingAbstractInterpretation.Ready.ProcSet Action Name = (EqCheckingAbstractInterpretation.CCS.CCS Action Name → Prop)

@[instance_reducible]

instance EqCheckingAbstractInterpretation.Ready.instSingletonCCSProcSet {Action : Type u} {Name : Type v} : Singleton (CCS.CCS Action Name) (ProcSet Action Name)

Equations

• EqCheckingAbstractInterpretation.Ready.instSingletonCCSProcSet = { singleton := fun (q r : EqCheckingAbstractInterpretation.CCS.CCS Action Name) => r = q }

@[instance_reducible]

instance EqCheckingAbstractInterpretation.Ready.instEmptyCollectionProcSet {Action : Type u} {Name : Type v} : EmptyCollection (ProcSet Action Name)

Equations

• EqCheckingAbstractInterpretation.Ready.instEmptyCollectionProcSet = { emptyCollection := fun (x : EqCheckingAbstractInterpretation.CCS.CCS Action Name) => False }

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.ObsSet (Obs : Type w) : Type w

Equations

• EqCheckingAbstractInterpretation.Ready.ObsSet Obs = (Obs → Prop)

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.DiffSysRS (Action : Type u) (Name : Type v) (Obs : Type w) : Type (max (max v u) w)

Equations

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

inductive EqCheckingAbstractInterpretation.Ready.Capability : Type

Capability lattice elements from the paper: T, S, F, RS.

• T : Capability
• S : Capability
• F : Capability
• RS : Capability

@[instance_reducible]

instance EqCheckingAbstractInterpretation.Ready.instDecidableEqCapability : DecidableEq Capability

Equations

• EqCheckingAbstractInterpretation.Ready.instDecidableEqCapability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance EqCheckingAbstractInterpretation.Ready.instReprCapability : Repr Capability

Equations

• EqCheckingAbstractInterpretation.Ready.instReprCapability = { reprPrec := EqCheckingAbstractInterpretation.Ready.instReprCapability.repr }

def EqCheckingAbstractInterpretation.Ready.instReprCapability.repr : Capability → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Ready.AbsSysRS (Action : Type u) (Name : Type v) : Type (max v u)

Equations

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

def EqCheckingAbstractInterpretation.Ready.capLe : Capability → Capability → Prop

Order relation from the diamond lattice of capabilities.

Equations

• EqCheckingAbstractInterpretation.Ready.capLe EqCheckingAbstractInterpretation.Ready.Capability.T x✝ = True
• EqCheckingAbstractInterpretation.Ready.capLe EqCheckingAbstractInterpretation.Ready.Capability.S EqCheckingAbstractInterpretation.Ready.Capability.S = True
• EqCheckingAbstractInterpretation.Ready.capLe EqCheckingAbstractInterpretation.Ready.Capability.S EqCheckingAbstractInterpretation.Ready.Capability.RS = True
• EqCheckingAbstractInterpretation.Ready.capLe EqCheckingAbstractInterpretation.Ready.Capability.F EqCheckingAbstractInterpretation.Ready.Capability.F = True
• EqCheckingAbstractInterpretation.Ready.capLe EqCheckingAbstractInterpretation.Ready.Capability.F EqCheckingAbstractInterpretation.Ready.Capability.RS = True
• EqCheckingAbstractInterpretation.Ready.capLe EqCheckingAbstractInterpretation.Ready.Capability.RS EqCheckingAbstractInterpretation.Ready.Capability.RS = True
• EqCheckingAbstractInterpretation.Ready.capLe x✝¹ x✝ = False

@[instance_reducible]

instance EqCheckingAbstractInterpretation.Ready.instDecidableRelCapabilityCapLe : DecidableRel capLe

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.capLe_refl (c : Capability) : capLe c c

theorem EqCheckingAbstractInterpretation.Ready.capLe_trans {c d e : Capability} (hcd : capLe c d) (hde : capLe d e) : capLe c e

def EqCheckingAbstractInterpretation.Ready.capJoin : Capability → Capability → Capability

Join operation of the capability lattice.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.capJoin EqCheckingAbstractInterpretation.Ready.Capability.T x✝ = x✝
• EqCheckingAbstractInterpretation.Ready.capJoin x✝ EqCheckingAbstractInterpretation.Ready.Capability.T = x✝
• EqCheckingAbstractInterpretation.Ready.capJoin x✝¹ x✝ = EqCheckingAbstractInterpretation.Ready.Capability.RS

theorem EqCheckingAbstractInterpretation.Ready.capJoin_le {a b c : Capability} (h : capLe (capJoin a b) c) : capLe a c ∧ capLe b c

theorem EqCheckingAbstractInterpretation.Ready.capLe_left_capJoin (a b : Capability) : capLe a (capJoin a b)

theorem EqCheckingAbstractInterpretation.Ready.capLe_right_capJoin (a b : Capability) : capLe b (capJoin a b)

theorem EqCheckingAbstractInterpretation.Ready.capJoin_mono {a a' b b' : Capability} (ha : capLe a a') (hb : capLe b b') : capLe (capJoin a b) (capJoin a' b')

def EqCheckingAbstractInterpretation.Ready.req (needsSim needsFail : Bool) : Capability

Capability requirement contributed by observation shape information.

Equations

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

def EqCheckingAbstractInterpretation.Ready.upClosure (X : Capability → Prop) : Capability → Prop

Upward closure in the capability lattice.

Equations

• EqCheckingAbstractInterpretation.Ready.upClosure X d = ∃ (c : EqCheckingAbstractInterpretation.Ready.Capability), X c ∧ EqCheckingAbstractInterpretation.Ready.capLe c d

def EqCheckingAbstractInterpretation.Ready.alphaCapRaw {Obs : Type w} (ObsCap : Capability → Obs → Prop) (X : ObsSet Obs) : Capability → Prop

Capability abstraction without minimization/pruning.

Equations

• EqCheckingAbstractInterpretation.Ready.alphaCapRaw ObsCap X c = ∃ (o : Obs), X o ∧ ObsCap c o

def EqCheckingAbstractInterpretation.Ready.minimalCap (A : Capability → Prop) (c : Capability) : Prop

Minimal-capability pruning on capability predicates.

Equations

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

def EqCheckingAbstractInterpretation.Ready.alphaCap {Obs : Type w} (ObsCap : Capability → Obs → Prop) (X : ObsSet Obs) : Capability → Prop

Capability abstraction with pruning to minimal capabilities.

Equations

• EqCheckingAbstractInterpretation.Ready.alphaCap ObsCap X c = EqCheckingAbstractInterpretation.Ready.minimalCap (EqCheckingAbstractInterpretation.Ready.alphaCapRaw ObsCap X) c

def EqCheckingAbstractInterpretation.Ready.gammaCap {Obs : Type w} (ObsCap : Capability → Obs → Prop) (Y : Capability → Prop) : ObsSet Obs

Concretization by upward closure of capabilities.

Equations

• EqCheckingAbstractInterpretation.Ready.gammaCap ObsCap Y o = ∃ (c : EqCheckingAbstractInterpretation.Ready.Capability), EqCheckingAbstractInterpretation.Ready.upClosure Y c ∧ ObsCap c o

def EqCheckingAbstractInterpretation.Ready.thresholdWitness (A : Capability → Prop) (N : Capability) : Prop

Threshold reading for an abstract capability value.

Equations

• EqCheckingAbstractInterpretation.Ready.thresholdWitness A N = ∃ (c : EqCheckingAbstractInterpretation.Ready.Capability), A c ∧ EqCheckingAbstractInterpretation.Ready.capLe c N

theorem EqCheckingAbstractInterpretation.Ready.thresholdWitness_iff_upClosure (A : Capability → Prop) (N : Capability) : thresholdWitness A N ↔ upClosure A N

def EqCheckingAbstractInterpretation.Ready.notPreorderAt {Action : Type u} {Name : Type v} {Obs : Type w} (ObsCap : Capability → Obs → Prop) (Diff : DiffSysRS Action Name Obs) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : Prop

Concrete threshold failure criterion for a difference relation.

Equations

• EqCheckingAbstractInterpretation.Ready.notPreorderAt ObsCap Diff N p Q = ∃ (o : Obs), Diff p Q o ∧ ObsCap N o

def EqCheckingAbstractInterpretation.Ready.abstractFailsAt {Action : Type u} {Name : Type v} (Abs : AbsSysRS Action Name) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : Prop

Abstract threshold failure criterion for a capability-valued analysis result.

Equations

• EqCheckingAbstractInterpretation.Ready.abstractFailsAt Abs N p Q = EqCheckingAbstractInterpretation.Ready.thresholdWitness (Abs p Q) N

def EqCheckingAbstractInterpretation.Ready.ObsCapMonotone {Obs : Type w} (ObsCap : Capability → Obs → Prop) : Prop

Monotonicity condition needed for threshold soundness/completeness: if a capability can observe o, then every stronger capability can observe o.

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.thresholdWitness_alphaCapRaw_iff {Obs : Type w} (ObsCap : Capability → Obs → Prop) (hMono : ObsCapMonotone ObsCap) (X : ObsSet Obs) (N : Capability) : thresholdWitness (alphaCapRaw ObsCap X) N ↔ ∃ (o : Obs), X o ∧ ObsCap N o

Threshold reading for alphaCapRaw: it is equivalent to concrete intersection with the threshold fragment, under monotonicity of fragment observability.

theorem EqCheckingAbstractInterpretation.Ready.minimalCap_left (A : Capability → Prop) {c : Capability} (h : minimalCap A c) : A c

theorem EqCheckingAbstractInterpretation.Ready.thresholdWitness_minimalCap_of_mem (A : Capability → Prop) (N : Capability) (hAN : A N) : thresholdWitness (minimalCap A) N

theorem EqCheckingAbstractInterpretation.Ready.upClosure_minimalCap_iff (A : Capability → Prop) (N : Capability) : upClosure (minimalCap A) N ↔ upClosure A N

theorem EqCheckingAbstractInterpretation.Ready.alphaCapRaw_upward_closed {Obs : Type w} (ObsCap : Capability → Obs → Prop) (hMono : ObsCapMonotone ObsCap) (X : ObsSet Obs) (N : Capability) : upClosure (alphaCapRaw ObsCap X) N ↔ alphaCapRaw ObsCap X N

theorem EqCheckingAbstractInterpretation.Ready.upClosure_alphaCap_iff_alphaCapRaw {Obs : Type w} (ObsCap : Capability → Obs → Prop) (hMono : ObsCapMonotone ObsCap) (X : ObsSet Obs) (N : Capability) : upClosure (alphaCap ObsCap X) N ↔ alphaCapRaw ObsCap X N

theorem EqCheckingAbstractInterpretation.Ready.thresholdWitness_alphaCap_iff {Obs : Type w} (ObsCap : Capability → Obs → Prop) (hMono : ObsCapMonotone ObsCap) (X : ObsSet Obs) (N : Capability) : thresholdWitness (alphaCap ObsCap X) N ↔ ∃ (o : Obs), X o ∧ ObsCap N o

Threshold reading for alphaCap: pruning preserves threshold information.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_iff_notPreorderAt_of_alpha {Action : Type u} {Name : Type v} {Obs : Type w} (ObsCap : Capability → Obs → Prop) (hMono : ObsCapMonotone ObsCap) (Diff : DiffSysRS Action Name Obs) (Abs : AbsSysRS Action Name) (hAlpha : ∀ (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability), Abs p Q c ↔ alphaCapRaw ObsCap (Diff p Q) c) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt Abs N p Q ↔ notPreorderAt ObsCap Diff N p Q

Unified threshold theorem at the level used in Section 5: if abstract values are pointwise alphaCapRaw of concrete differences, then abstract threshold witnesses are exactly concrete threshold failures.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_iff_notPreorderAt_of_alphaExact {Action : Type u} {Name : Type v} {Obs : Type w} (ObsCap : Capability → Obs → Prop) (hMono : ObsCapMonotone ObsCap) (Diff : DiffSysRS Action Name Obs) (Abs : AbsSysRS Action Name) (hAlpha : ∀ (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability), Abs p Q c ↔ alphaCap ObsCap (Diff p Q) c) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt Abs N p Q ↔ notPreorderAt ObsCap Diff N p Q

Exact-pruned variant of the unified threshold theorem.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_iff_notPreorderAt_of_lfp {Action : Type u} {Name : Type v} {Obs : Type w} (ObsCap : Capability → Obs → Prop) (hMono : ObsCapMonotone ObsCap) (lfpConcrete : DiffSysRS Action Name Obs) (lfpAbs : AbsSysRS Action Name) (hLfp : ∀ (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability), lfpAbs p Q c ↔ alphaCapRaw ObsCap (lfpConcrete p Q) c) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt lfpAbs N p Q ↔ notPreorderAt ObsCap lfpConcrete N p Q

Least-fixpoint variant matching the paper's Section 5 statement shape. lfpAbs is the abstract lfp result, lfpConcrete the concrete one.

theorem EqCheckingAbstractInterpretation.Ready.abstractFailsAt_iff_notPreorderAt_of_lfpExact {Action : Type u} {Name : Type v} {Obs : Type w} (ObsCap : Capability → Obs → Prop) (hMono : ObsCapMonotone ObsCap) (lfpConcrete : DiffSysRS Action Name Obs) (lfpAbs : AbsSysRS Action Name) (hLfp : ∀ (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (c : Capability), lfpAbs p Q c ↔ alphaCap ObsCap (lfpConcrete p Q) c) (N : Capability) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) : abstractFailsAt lfpAbs N p Q ↔ notPreorderAt ObsCap lfpConcrete N p Q

Least-fixpoint threshold theorem for exact-pruned capability values.

inductive EqCheckingAbstractInterpretation.Ready.RSObs (Action : Type u) : Type u

Concrete observation syntax used to instantiate the unified capability framework: positive branching plus negative (refusal) tests.

• tt {Action : Type u} : RSObs Action
• node {Action : Type u} : List (Action × RSObs Action) → List Action → RSObs Action

@[instance_reducible]

instance EqCheckingAbstractInterpretation.Ready.instReprRSObs {Action✝ : Type u_1} [Repr Action✝] : Repr (RSObs Action✝)

Equations

• EqCheckingAbstractInterpretation.Ready.instReprRSObs = { reprPrec := EqCheckingAbstractInterpretation.Ready.instReprRSObs.repr }

partial def EqCheckingAbstractInterpretation.Ready.instReprRSObs.repr {Action✝ : Type u_1} [Repr Action✝] : RSObs Action✝ → Nat → Std.Format

def EqCheckingAbstractInterpretation.Ready.nodeRequirement (positiveCount : Nat) (hasNegative : Bool) (children : Capability) : Capability

Combine a node's branching, refusal, and child capability requirements.

Equations

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

def EqCheckingAbstractInterpretation.Ready.childrenReq {Action : Type u} : List (Action × RSObs Action) → Capability

Aggregate child capability requirements from positive branches.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.childrenReq [] = EqCheckingAbstractInterpretation.Ready.Capability.T

def EqCheckingAbstractInterpretation.Ready.reqOfObs {Action : Type u} : RSObs Action → Capability

Least capability needed to express a concrete ready-simulation observation.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.reqOfObs EqCheckingAbstractInterpretation.Ready.RSObs.tt = EqCheckingAbstractInterpretation.Ready.Capability.T

def EqCheckingAbstractInterpretation.Ready.rsObsCap {Action : Type u} (c : Capability) (o : RSObs Action) : Prop

Fragment membership predicate induced by capability thresholds.

Equations

• EqCheckingAbstractInterpretation.Ready.rsObsCap c o = EqCheckingAbstractInterpretation.Ready.capLe (EqCheckingAbstractInterpretation.Ready.reqOfObs o) c

def EqCheckingAbstractInterpretation.Ready.ObsTr {Action : Type u} : RSObs Action → Prop

Observation fragments corresponding to Tr/S/F/RS thresholds.

Equations

• EqCheckingAbstractInterpretation.Ready.ObsTr = EqCheckingAbstractInterpretation.Ready.rsObsCap EqCheckingAbstractInterpretation.Ready.Capability.T

def EqCheckingAbstractInterpretation.Ready.ObsS {Action : Type u} : RSObs Action → Prop

Equations

• EqCheckingAbstractInterpretation.Ready.ObsS = EqCheckingAbstractInterpretation.Ready.rsObsCap EqCheckingAbstractInterpretation.Ready.Capability.S

def EqCheckingAbstractInterpretation.Ready.ObsF {Action : Type u} : RSObs Action → Prop

Equations

• EqCheckingAbstractInterpretation.Ready.ObsF = EqCheckingAbstractInterpretation.Ready.rsObsCap EqCheckingAbstractInterpretation.Ready.Capability.F

def EqCheckingAbstractInterpretation.Ready.ObsRS {Action : Type u} : RSObs Action → Prop

Equations

• EqCheckingAbstractInterpretation.Ready.ObsRS = EqCheckingAbstractInterpretation.Ready.rsObsCap EqCheckingAbstractInterpretation.Ready.Capability.RS

theorem EqCheckingAbstractInterpretation.Ready.childrenReq_member_le {Action : Type u} {ao : Action × RSObs Action} {pos : List (Action × RSObs Action)} (hMem : ao ∈ pos) : capLe (reqOfObs ao.snd) (childrenReq pos)

theorem EqCheckingAbstractInterpretation.Ready.childrenReq_map_le {Action : Type u} (f : Action × RSObs Action → RSObs Action) (pos : List (Action × RSObs Action)) (hLe : ∀ (ao : Action × RSObs Action), ao ∈ pos → capLe (reqOfObs (f ao)) (reqOfObs ao.snd)) : capLe (childrenReq (List.map (fun (ao : Action × RSObs Action) => (ao.fst, f ao)) pos)) (childrenReq pos)

theorem EqCheckingAbstractInterpretation.Ready.reqOfObs_node_map_le {Action : Type u} (f : Action × RSObs Action → RSObs Action) (pos : List (Action × RSObs Action)) (neg : List Action) (hLe : ∀ (ao : Action × RSObs Action), ao ∈ pos → capLe (reqOfObs (f ao)) (reqOfObs ao.snd)) : capLe (reqOfObs (RSObs.node (List.map (fun (ao : Action × RSObs Action) => (ao.fst, f ao)) pos) neg)) (reqOfObs (RSObs.node pos neg))

def EqCheckingAbstractInterpretation.Ready.replaceChildren {Action : Type u} (pos : List (Action × RSObs Action)) (f : Fin pos.length → RSObs Action) : List (Action × RSObs Action)

Replace children by branch occurrence rather than branch value.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Ready.replaceChildren [] f_2 = []

theorem EqCheckingAbstractInterpretation.Ready.replaceChildren_length {Action : Type u} (pos : List (Action × RSObs Action)) (f : Fin pos.length → RSObs Action) : (replaceChildren pos f).length = pos.length

theorem EqCheckingAbstractInterpretation.Ready.replaceChildren_get {Action : Type u} (pos : List (Action × RSObs Action)) (f : Fin pos.length → RSObs Action) (i : Fin pos.length) : (replaceChildren pos f).get ⟨↑i, ⋯⟩ = ((pos.get i).fst, f i)

theorem EqCheckingAbstractInterpretation.Ready.childrenReq_replaceChildren_le {Action : Type u} (pos : List (Action × RSObs Action)) (f : Fin pos.length → RSObs Action) (hLe : ∀ (i : Fin pos.length), capLe (reqOfObs (f i)) (reqOfObs (pos.get i).snd)) : capLe (childrenReq (replaceChildren pos f)) (childrenReq pos)

theorem EqCheckingAbstractInterpretation.Ready.reqOfObs_node_replaceChildren_le {Action : Type u} (pos : List (Action × RSObs Action)) (neg : List Action) (f : Fin pos.length → RSObs Action) (hLe : ∀ (i : Fin pos.length), capLe (reqOfObs (f i)) (reqOfObs (pos.get i).snd)) : capLe (reqOfObs (RSObs.node (replaceChildren pos f) neg)) (reqOfObs (RSObs.node pos neg))

theorem EqCheckingAbstractInterpretation.Ready.rsObsCap_child {Action : Type u} {N : Capability} {pos : List (Action × RSObs Action)} {neg : List Action} {ao : Action × RSObs Action} (hCap : rsObsCap N (RSObs.node pos neg)) (hMem : ao ∈ pos) : rsObsCap N ao.snd

theorem EqCheckingAbstractInterpretation.Ready.rsObsCap_S_node_neg_nil {Action : Type u} {pos : List (Action × RSObs Action)} {neg : List Action} (hCap : rsObsCap Capability.S (RSObs.node pos neg)) : neg = []

theorem EqCheckingAbstractInterpretation.Ready.rsObsCap_T_node_neg_nil {Action : Type u} {pos : List (Action × RSObs Action)} {neg : List Action} (hCap : rsObsCap Capability.T (RSObs.node pos neg)) : neg = []

theorem EqCheckingAbstractInterpretation.Ready.rsObsCap_F_node_no_branching {Action : Type u} {pos : List (Action × RSObs Action)} {neg : List Action} (hCap : rsObsCap Capability.F (RSObs.node pos neg)) : ¬1 < pos.length

theorem EqCheckingAbstractInterpretation.Ready.rsObsCap_F_node_neg_nil_of_pos_ne_nil {Action : Type u} {pos : List (Action × RSObs Action)} {neg : List Action} (hCap : rsObsCap Capability.F (RSObs.node pos neg)) (hPos : pos ≠ []) : neg = []

A failure observation with a positive branch has no refusal at that node.

theorem EqCheckingAbstractInterpretation.Ready.rsObsCap_T_node_no_branching {Action : Type u} {pos : List (Action × RSObs Action)} {neg : List Action} (hCap : rsObsCap Capability.T (RSObs.node pos neg)) : ¬1 < pos.length

theorem EqCheckingAbstractInterpretation.Ready.rsObsCapMonotone {Action : Type u} : ObsCapMonotone rsObsCap