theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_competitorsOf_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : StateSet State) (state : State) : state ∈ competitorsOf lts competitors ↔ state ∈ lts.states ∧ state ∈ competitors

The executable competitor list enumerates exactly the listed finite competitors.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.competitorsOf_nodup {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (competitors : StateSet State) : (competitorsOf lts competitors).Nodup

competitorsOf inherits duplicate-freeness from the finite LTS state list.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.configSuccessors_subset_configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (config : ReadyConfig State) (hConfig : config ∈ configUniverse lts) (successor : ReadyConfig State) : successor ∈ configSuccessors lts config → successor ∈ configUniverse lts

Generated Ready successor configurations remain inside the represented universe.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_configSuccessors {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (config : ReadyConfig State) (selected : StateSet State) (action : Action) (target : State) (hSelected : selected ∈ FiniteEvaluator.powerset (competitorsOf lts config.2)) (hAction : action ∈ lts.actions) (hTarget : target ∈ lts.next config.1 action) (hNotSelf : config.1 ∉ config.2) : (target, shift lts selected action) ∈ configSuccessors lts config

Every enumerated positive branch contributes its derivative configuration.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_assignmentsWithSlots_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (slots : List ℕ) (competitors : List State) (assignment : Assignment Action) : assignment ∈ assignmentsWithSlots lts slots competitors ↔ List.length assignment = competitors.length ∧ ∀ choice ∈ assignment, choice ∈ assignmentChoices lts slots

assignmentsWithSlots enumerates exactly the assignments with one allowed choice for every competitor.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_assignmentChoices_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (slots : List ℕ) (choice : Option (ℕ × Action × Capability)) : choice ∈ assignmentChoices lts slots ↔ choice = none ∨ ∃ slot ∈ slots, ∃ action ∈ lts.actions, ∃ capability ∈ capabilities, choice = some (slot, action, capability)

The non-negative choices contain exactly one listed slot, action, and capability.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_assignments_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : StateSet State) (assignment : Assignment Action) : assignment ∈ assignments lts competitors ↔ List.length assignment = (competitorsOf lts competitors).length ∧ ∀ choice ∈ assignment, choice ∈ assignmentChoices lts (List.range (competitorsOf lts competitors).length)

assignments is the exhaustive assignment enumerator for its finite competitors.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentsAny_eq_any {Action : Type u} {State : Type v} (choices : List (Option (ℕ × Action × Capability))) (competitors : List State) (accept : Assignment Action → Bool) : assignmentsAny choices competitors accept = (EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentsWithChoices✝ choices competitors).any accept

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentWellFormed_sound {Action : Type u} [DecidableEq Action] (assignment : Assignment Action) (hWellFormed : assignmentWellFormed assignment = true) (slot otherSlot : ℕ) (action otherAction : Action) (capability otherCapability : Capability) (hEntry : some (slot, action, capability) ∈ assignment) (hOtherEntry : some (otherSlot, otherAction, otherCapability) ∈ assignment) (hSlot : slot = otherSlot) : action = otherAction ∧ capability = otherCapability

Well-formed assignments give each slot one consistent action and capability label.

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.NegativeAssignmentCondition {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (negative : List Action) (competitor : State) (choice : Option (ℕ × Action × Capability)) : Prop

Semantic condition imposed on one competitor by the negative assignment group.

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.NegativeAssignmentCondition lts negative competitor choice = (choice = none → ∃ action ∈ negative, (lts.next competitor action).isEmpty = false)

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeAssignmentValid_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : List State) (negative : List Action) (assignment : Assignment Action) : negativeAssignmentValid lts competitors negative assignment = true ↔ List.Forall₂ (NegativeAssignmentCondition lts negative) competitors assignment

The Boolean negative-group validator is exactly its pointwise partition condition.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeCompetitors_subset {Action : Type u} {State : Type v} [DecidableEq State] (competitors : List State) (assignment : Assignment Action) : (negativeCompetitors competitors assignment).toFinset ⊆ competitors.toFinset

The negative partition never introduces competitors outside its source list.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.negativeCompetitors_enabled {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (negative : List Action) (competitors : List State) (assignment : Assignment Action) (hValid : List.Forall₂ (NegativeAssignmentCondition lts negative) competitors assignment) (competitor : State) (hCompetitor : competitor ∈ negativeCompetitors competitors assignment) : ∃ action ∈ negative, (lts.next competitor action).isEmpty = false

Every negative-partition competitor enables one selected negative action.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_branchInsert_competitors {Action : Type u} {State : Type v} [DecidableEq State] (slot : ℕ) (action : Action) (capability : Capability) (competitor : State) (branches : List (Branch Action State)) (branch : Branch Action State) (member : State) (hBranch : branch ∈ branchInsert slot action capability competitor branches) (hMember : member ∈ branch.competitors) : member = competitor ∨ ∃ prior ∈ branches, member ∈ prior.competitors

Every competitor in an inserted branch comes from the new entry or a prior branch.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_branchInsert_label {Action : Type u} {State : Type v} [DecidableEq State] (slot : ℕ) (action : Action) (capability : Capability) (competitor : State) (branches : List (Branch Action State)) (branch : Branch Action State) (hBranch : branch ∈ branchInsert slot action capability competitor branches) : branch.slot = slot ∧ branch.action = action ∧ branch.capability = capability ∨ ∃ prior ∈ branches, branch.slot = prior.slot ∧ branch.action = prior.action ∧ branch.capability = prior.capability

An inserted branch keeps either the new label or the label of a prior branch.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentBranches_competitors_subset {Action : Type u} {State : Type v} [DecidableEq State] (competitors : List State) (assignment : Assignment Action) (branch : Branch Action State) (member : State) (hBranch : branch ∈ assignmentBranches competitors assignment) (hMember : member ∈ branch.competitors) : member ∈ competitors

Grouped positive branches contain only competitors from their aligned source list.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentBranches_label_origin {Action : Type u} {State : Type v} [DecidableEq State] (competitors : List State) (assignment : Assignment Action) (branch : Branch Action State) (hBranch : branch ∈ assignmentBranches competitors assignment) : some (branch.slot, branch.action, branch.capability) ∈ assignment

Every grouped branch label originates in a positive assignment entry.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentBranches_label_consistent {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (competitors : List State) (assignment : Assignment Action) (hWellFormed : assignmentWellFormed assignment = true) (branch : Branch Action State) (hBranch : branch ∈ assignmentBranches competitors assignment) (slot : ℕ) (action : Action) (capability : Capability) (hEntry : some (slot, action, capability) ∈ assignment) (hSlot : slot = branch.slot) : action = branch.action ∧ capability = branch.capability

A well-formed assignment gives every branch the unique label for its slot.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchInsert_covers_competitor {Action : Type u} {State : Type v} [DecidableEq State] (slot : ℕ) (action : Action) (capability : Capability) (competitor : State) (branches : List (Branch Action State)) (hLabels : ∀ branch ∈ branches, branch.slot = slot → action = branch.action ∧ capability = branch.capability) : ∃ branch ∈ branchInsert slot action capability competitor branches, branch.slot = slot ∧ branch.action = action ∧ branch.capability = capability ∧ competitor ∈ branch.competitors

Inserting a positive assignment covers its competitor with a branch of that label.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchInsert_preserves_member {Action : Type u} {State : Type v} [DecidableEq State] (slot : ℕ) (action : Action) (capability : Capability) (competitor : State) (branches : List (Branch Action State)) (source : Branch Action State) : source ∈ branches → ∀ member ∈ source.competitors, ∃ updated ∈ branchInsert slot action capability competitor branches, updated.slot = source.slot ∧ updated.action = source.action ∧ updated.capability = source.capability ∧ member ∈ updated.competitors

Adding a competitor preserves each prior branch's label and members.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentBranches_cover_positive {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (competitors : List State) (assignment : Assignment Action) (hLength : List.length assignment = competitors.length) (hWellFormed : assignmentWellFormed assignment = true) : List.Forall₂ (fun (competitor : State) (choice : Option (ℕ × Action × Capability)) => ∀ (slot : ℕ) (action : Action) (capability : Capability), choice = some (slot, action, capability) → ∃ branch ∈ assignmentBranches competitors assignment, branch.slot = slot ∧ branch.action = action ∧ branch.capability = capability ∧ competitor ∈ branch.competitors) competitors assignment

Every positive choice in an aligned assignment occurs in its grouped branch.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignmentBranches_partition {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (competitors : List State) (assignment : Assignment Action) (hLength : List.length assignment = competitors.length) (hWellFormed : assignmentWellFormed assignment = true) (member : State) (hMember : member ∈ competitors) : member ∈ negativeCompetitors competitors assignment ∨ ∃ branch ∈ assignmentBranches competitors assignment, member ∈ branch.competitors

An aligned assignment partitions its competitors into negative and positive groups.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.decodeSet_shift_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (competitors : StateSet State) (action : Action) (process : CCS.CCS Action Name) (hCompetitors : ∀ competitor ∈ competitors, competitor ∈ lts.states) : CCS.FiniteLTS.decodeSet decode (shift lts competitors action) process ↔ CCS.DerivSetOf env (CCS.FiniteLTS.decodeSet decode competitors) action process

Decoding an executable shift is exactly the semantic lifted derivative.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.next_isEmpty_iff_not_enabled {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (action : Action) (hState : state ∈ lts.states) : (lts.next state action).isEmpty = true ↔ ¬CCS.Enabled env (decode state) action

An empty transition row is exactly a disabled semantic action on listed states.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.refuses_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (negative : List Action) (hState : state ∈ lts.states) : marks.refuses lts state negative = true ↔ ∀ action ∈ negative, ¬CCS.Enabled env (decode state) action

The executable refusal check is the negative premise of a Ready observation.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignment_to_DRS_partition {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (negative : List Action) (assignment : Assignment Action) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) (hAssignment : assignment ∈ assignments lts competitors) (hWellFormed : assignmentWellFormed assignment = true) (hValid : negativeAssignmentValid lts (competitorsOf lts competitors) negative assignment = true) (hRefuses : marks.refuses lts state negative = true) : have branches := assignmentBranches (competitorsOf lts competitors) assignment; ∃ (Qneg : ProcSet Action Name) (Qpos : Fin branches.length → ProcSet Action Name), (∀ action ∈ negative, ¬CCS.Enabled env (decode state) action) ∧ (∀ (process : CCS.CCS Action Name), Qneg process → ∃ action ∈ negative, CCS.Enabled env process action) ∧ (∀ (process : CCS.CCS Action Name), CCS.FiniteLTS.decodeSet decode competitors process → Qneg process ∨ ∃ (i : Fin branches.length), Qpos i process) ∧ ∀ (i : Fin branches.length), Qpos i = CCS.FiniteLTS.decodeSet decode (branches.get i).competitors

Finite assignment groups provide the refusal, enabledness, and cover premises of a DRS node.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.lfpDRS_tt_of_empty {Action : Type u} {Name : Type u_1} (env : CCS.Env Action Name) (process : CCS.CCS Action Name) : lfpDRS env process (fun (x : CCS.CCS Action Name) => False) RSObs.tt

The terminal Ready observation belongs to the concrete lfp over an empty competitor set.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.empty_competitors_raw_sound {Action : Type u} {State : Type v} {Name : Type w} (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (state : State) : alphaCapRaw rsObsCap (lfpDRS env (decode state) (CCS.FiniteLTS.decodeSet decode ∅)) Capability.T

An empty finite competitor set is semantically witnessed by raw capability T.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.raw_sound_of_lfpDRS {Action : Type u} {Name : Type u_1} (env : CCS.Env Action Name) (process : CCS.CCS Action Name) (competitors : ProcSet Action Name) (observation : RSObs Action) (capability : Capability) (hObservation : lfpDRS env process competitors observation) (hCapability : capLe (reqOfObs observation) capability) : alphaCapRaw rsObsCap (lfpDRS env process competitors) capability

A concrete lfp Ready observation witnesses every capability above its requirement.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.empty_mark_raw_sound {Action : Type u} {State : Type v} {Name : Type w} (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (config : ReadyConfig State) (capability : Capability) (hEmpty : config.2 = ∅) (hCapability : capability = Capability.T) : alphaCapRaw rsObsCap (lfpDRS env (decode config.1) (CCS.FiniteLTS.decodeSet decode config.2)) capability

The empty-competitor finite marking rule is sound for the raw Ready abstraction.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLeBool_iff (left right : Capability) : capLeBool left right = true ↔ capLe left right

Boolean capability comparison agrees with the semantic capability order.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capLe_antisymm {left right : Capability} (hLeftRight : capLe left right) (hRightLeft : capLe right left) : left = right

The capability order is antisymmetric.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.minimalCap_iff_of_sound_and_cofinal (finite semantic : Capability → Prop) (hSound : ∀ (capability : Capability), finite capability → semantic capability) (hCofinal : ∀ (capability : Capability), semantic capability → ∃ (finiteCapability : Capability), finite finiteCapability ∧ capLe finiteCapability capability) (capability : Capability) : minimalCap finite capability ↔ minimalCap semantic capability

Equal minimal antichains follow from raw soundness and downward cofinality.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.reqOfObs_branches_le {Action : Type u} {State : Type v} (negative : List Action) (branches : List (Branch Action State)) (observation : Branch Action State → RSObs Action) (hObservation : ∀ branch ∈ branches, capLe (reqOfObs (observation branch)) branch.capability) : capLe (reqOfObs (RSObs.node (List.map (fun (branch : Branch Action State) => (branch.action, observation branch)) branches) negative)) (branchesRequirement negative branches)

Grouped branch requirements bound the requirement of any matching semantic node.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.configMem_iff {State : Type v} [DecidableEq State] (config : ReadyConfig State) (configs : List (ReadyConfig State)) : configMem config configs = true ↔ config ∈ configs

Boolean configuration membership is ordinary membership in the table.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_configInsert_iff {State : Type v} [DecidableEq State] (config entry : ReadyConfig State) (configs : List (ReadyConfig State)) : entry ∈ configInsert config configs ↔ entry = config ∨ entry ∈ configs

Configuration insertion adds exactly its argument when it was absent.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_configUnion_iff {State : Type v} [DecidableEq State] (entry : ReadyConfig State) (left right : List (ReadyConfig State)) : entry ∈ configUnion left right ↔ entry ∈ left ∨ entry ∈ right

Configuration union denotes ordinary membership union.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_foldl_expand_of_mem {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (drivers initial : List (ReadyConfig State)) (entry : ReadyConfig State) (hEntry : entry ∈ initial) : entry ∈ List.foldl (fun (closure : List (ReadyConfig State)) (config : ReadyConfig State) => configUnion (configSuccessors lts config) closure) initial drivers

Folding configuration expansion never removes an already present configuration.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_expandConfigs_of_mem {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (configs : List (ReadyConfig State)) (entry : ReadyConfig State) (hEntry : entry ∈ configs) : entry ∈ expandConfigs lts configs

One expansion keeps every seed configuration.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_foldl_expand_of_successor {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (drivers initial : List (ReadyConfig State)) (config entry : ReadyConfig State) (hConfig : config ∈ drivers) (hSuccessor : entry ∈ configSuccessors lts config) : entry ∈ List.foldl (fun (closure : List (ReadyConfig State)) (config : ReadyConfig State) => configUnion (configSuccessors lts config) closure) initial drivers

Folding expansion includes direct successors of any configuration it visits.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_expandConfigs_of_successor {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (configs : List (ReadyConfig State)) (config entry : ReadyConfig State) (hConfig : config ∈ configs) (hSuccessor : entry ∈ configSuccessors lts config) : entry ∈ expandConfigs lts configs

One expansion includes every direct successor of one of its seeds.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_foldl_expandConfigs_of_mem {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (rounds : List Unit) (initial : List (ReadyConfig State)) (entry : ReadyConfig State) (hEntry : entry ∈ initial) : entry ∈ List.foldl (fun (configs : List (ReadyConfig State)) (x : Unit) => expandConfigs lts configs) initial rounds

Repeated configuration expansion preserves every member of its initial seed list.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_queryConfigsN {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) (count : ℕ) : (state, competitors) ∈ queryConfigsN lts state competitors count

Every recursive query expansion round retains its original query configuration.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigs_eq_queryConfigsN {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : queryConfigs lts state competitors = queryConfigsN lts state competitors (lts.states.length * 2 ^ lts.states.length)

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_queryConfigs {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : (state, competitors) ∈ queryConfigs lts state competitors

The bounded query domain always contains the queried configuration.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.foldl_expand_subset_configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (drivers initial : List (ReadyConfig State)) (hDrivers : ∀ config ∈ drivers, config ∈ configUniverse lts) (hInitial : ∀ config ∈ initial, config ∈ configUniverse lts) (config : ReadyConfig State) : config ∈ List.foldl (fun (closure : List (ReadyConfig State)) (config : ReadyConfig State) => configUnion (configSuccessors lts config) closure) initial drivers → config ∈ configUniverse lts

Folding expansion preserves containment in the represented configuration universe.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.expandConfigs_subset_configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (configs : List (ReadyConfig State)) (hConfigs : ∀ config ∈ configs, config ∈ configUniverse lts) (config : ReadyConfig State) : config ∈ expandConfigs lts configs → config ∈ configUniverse lts

One Ready configuration expansion stays within the represented universe.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.foldl_expandConfigs_subset_configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (rounds : List Unit) (initial : List (ReadyConfig State)) (hInitial : ∀ config ∈ initial, config ∈ configUniverse lts) (config : ReadyConfig State) : config ∈ List.foldl (fun (configs : List (ReadyConfig State)) (x : Unit) => expandConfigs lts configs) initial rounds → config ∈ configUniverse lts

Repeated configuration expansion remains within the represented universe.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigsN_subset_configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) (count : ℕ) (config : ReadyConfig State) : config ∈ queryConfigsN lts state competitors count → config ∈ configUniverse lts

Every recursive query expansion round stays inside the represented universe.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigs_subset_configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) (config : ReadyConfig State) : config ∈ queryConfigs lts state competitors → config ∈ configUniverse lts

The bounded query domain only contains configurations represented by the finite LTS.

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.configStepSet {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : Set (ReadyConfig State)) (config : ReadyConfig State) : Prop

Proof-facing direct configuration closure used by query-domain expansion.

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.configStepSet lts marked config = ∃ source ∈ marked, config ∈ EqCheckingAbstractInterpretation.Ready.FiniteLTS.configSuccessors lts source

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.configStepSet_mono {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) {left right : Set (ReadyConfig State)} (hSubset : left ⊆ right) (config : ReadyConfig State) : configStepSet lts left config → configStepSet lts right config

Direct configuration closure is monotone in the already-known configurations.

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigStepSet {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (seed : ReadyConfig State) (marked : Set (ReadyConfig State)) (config : ReadyConfig State) : Prop

Configuration closure seeded by the query configuration itself.

Equations

• EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigStepSet lts seed marked config = (config = seed ∨ EqCheckingAbstractInterpretation.Ready.FiniteLTS.configStepSet lts marked config)

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigStepSet_mono {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (seed : ReadyConfig State) {left right : Set (ReadyConfig State)} (hSubset : left ⊆ right) (config : ReadyConfig State) : queryConfigStepSet lts seed left config → queryConfigStepSet lts seed right config

The seeded configuration closure relation is monotone.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.tableStep_queryConfigStepSet_eq_tableStep {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (domain marked : Set (ReadyConfig State)) (seed : ReadyConfig State) (hSeed : seed ∈ marked) : FiniteEvaluator.tableStep domain (queryConfigStepSet lts seed) marked = FiniteEvaluator.tableStep domain (configStepSet lts) marked

Once the seed is marked, the seeded step is the ordinary successor step.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_foldl_expand_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (drivers initial : List (ReadyConfig State)) (entry : ReadyConfig State) : entry ∈ List.foldl (fun (closure : List (ReadyConfig State)) (config : ReadyConfig State) => configUnion (configSuccessors lts config) closure) initial drivers ↔ entry ∈ initial ∨ ∃ source ∈ drivers, entry ∈ configSuccessors lts source

Folding expansion adds only direct successors of configurations it visits.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.expandConfigs_toFinset_eq_tableStep {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (configs : List (ReadyConfig State)) : (∀ config ∈ configs, config ∈ configUniverse lts) → ↑(expandConfigs lts configs).toFinset = FiniteEvaluator.tableStep (↑(configUniverse lts).toFinset) (configStepSet lts) ↑configs.toFinset

One executable expansion is precisely one proof-facing configuration closure step.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigsN_toFinset_eq_tableIter {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) (count : ℕ) : ↑(queryConfigsN lts state competitors count).toFinset = FiniteEvaluator.tableIter (↑(configUniverse lts).toFinset) (queryConfigStepSet lts (state, competitors)) (count + 1)

Recursive query expansion is the singleton-seeded generic table iteration.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.length_powerset {State : Type v} [DecidableEq State] (elements : List State) : (FiniteEvaluator.powerset elements).length = 2 ^ elements.length

The ordered powerset enumerator has the expected binary cardinality.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.length_flatMap_map {Element : Type u_1} {Value : Type u_2} {Result : Type u_3} (elements : List Element) (values : List Value) (map : Element → Value → Result) : (List.flatMap (fun (element : Element) => List.map (map element) values) elements).length = elements.length * values.length

Flat-mapping a fixed-length mapped list multiplies the input and output lengths.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.length_configUniverse {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : (configUniverse lts).length = lts.states.length * 2 ^ lts.states.length

The global configuration enumeration has the query expansion bound as its length.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.card_configUniverse_toFinset_le {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) : (configUniverse lts).toFinset.card ≤ lts.states.length * 2 ^ lts.states.length

The represented configuration universe has no more distinct entries than the query bound.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.queryConfigs_closed {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) (config child : ReadyConfig State) (hConfig : config ∈ queryConfigs lts state competitors) (hChild : child ∈ configSuccessors lts config) : child ∈ queryConfigs lts state competitors

The bounded query domain is closed under one Ready configuration successor.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_queryConfigs_of_configSuccessor {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) (config : ReadyConfig State) (hConfig : config ∈ queryConfigs lts state competitors) (selected : StateSet State) (action : Action) (target : State) (hSelected : selected ∈ FiniteEvaluator.powerset (competitorsOf lts config.2)) (hAction : action ∈ lts.actions) (hTarget : target ∈ lts.next config.1 action) (hNotSelf : config.1 ∉ config.2) : (target, shift lts selected action) ∈ queryConfigs lts state competitors

Every enumerated positive branch from a query configuration stays in its query domain.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_capabilityConfigs_iff {State : Type v} [DecidableEq State] (configs : List (ReadyConfig State)) (config : ReadyConfig State) (capability : Capability) : (config, capability) ∈ capabilityConfigs configs ↔ config ∈ configs ∧ capability ∈ capabilities ∧ config.1 ∉ config.2

Capability-domain enumeration contains exactly each query configuration at each capability.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityConfigMem_iff {State : Type v} [DecidableEq State] (config : CapabilityConfig State) (marked : CapabilityTable State) : capabilityConfigMem config marked = true ↔ config ∈ marked

Boolean capability-table membership is ordinary membership in the table.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityConfigMem_eq_false_iff {State : Type v} [DecidableEq State] (config : CapabilityConfig State) (marked : CapabilityTable State) : capabilityConfigMem config marked = false ↔ config ∉ marked

Boolean capability-table non-membership is ordinary non-membership.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.markedAt_iff {State : Type v} [DecidableEq State] (marked : CapabilityTable State) (config : ReadyConfig State) (threshold : Capability) : markedAt marked config threshold = true ↔ ∃ (capability : Capability), (config, capability) ∈ marked ∧ capLe capability threshold

Boolean threshold lookup is table membership below that threshold.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.filter_mem_listPowerset {Action : Type u} (actions : List Action) (selected : Action → Bool) : List.filter selected actions ∈ FiniteEvaluator.listPowerset actions

Filtering an action list selects a member of its list-valued powerset.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchesValid_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : CapabilityTable State) (state : State) (branches : List (Branch Action State)) : branchesValid lts marked state branches = true ↔ ∀ branch ∈ branches, ∃ successor ∈ lts.next state branch.action, ∃ (capability : Capability), ((successor, shift lts branch.competitors branch.action), capability) ∈ marked ∧ capLe capability branch.capability

Positive branch validation is exactly a table witness for every grouped branch.

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.marksSet {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : Set (CapabilityConfig State)) (config : ReadyConfig State) (capability : Capability) : Prop

Proof-facing form of one executable Ready marker step, independent of table order.

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.marks_iff_marksSet {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (marked : CapabilityTable State) (config : ReadyConfig State) (capability : Capability) : marks lts marked config capability = true ↔ marksSet lts (↑(List.toFinset marked)) config capability

Executable marking is exactly the order-independent proof-facing marker relation.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.marksSet_mono {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) {left right : Set (CapabilityConfig State)} (hSubset : left ⊆ right) (config : ReadyConfig State) (capability : Capability) : marksSet lts left config capability → marksSet lts right config capability

Ready marking is monotone in the set of previously marked child configurations.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.marksSet_raw_sound {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (marked : Set (CapabilityConfig State)) (hMarked : ∀ (config : ReadyConfig State) (childCapability : Capability), (config, childCapability) ∈ marked → alphaCapRaw rsObsCap (lfpDRS env (decode config.1) (CCS.FiniteLTS.decodeSet decode config.2)) childCapability) (config : ReadyConfig State) (capability : Capability) (hState : config.1 ∈ lts.states) (hCompetitors : config.2 ⊆ lts.states.toFinset) (hMarks : marksSet lts marked config capability) : alphaCapRaw rsObsCap (lfpDRS env (decode config.1) (CCS.FiniteLTS.decodeSet decode config.2)) capability

A finite marking step preserves semantic raw soundness of all child marks.

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityTableLfp {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : Set (CapabilityConfig State)

The Mathlib least fixed point of the query-local Ready marker relation.

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityTable_eq_saturate {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : capabilityTable lts state competitors = FiniteEvaluator.saturate (capabilityConfigs (queryConfigs lts state competitors)) capabilityConfigMem fun (marked : List (CapabilityConfig State)) (config : CapabilityConfig State) => marks lts marked config.1 config.2

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityTable_eq_capabilityTableLfp {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) : ↑(List.toFinset (capabilityTable lts state competitors)) = capabilityTableLfp lts state competitors

The bounded Ready evaluator computes the Mathlib least marker table.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityTable_closed {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : StateSet State) (config : ReadyConfig State) (capability : Capability) (hConfig : config ∈ queryConfigs lts state competitors) (hCapability : capability ∈ capabilities) (hNotSelf : config.1 ∉ config.2) (hMarks : marks lts (capabilityTable lts state competitors) config capability = true) : capabilityConfigMem (config, capability) (capabilityTable lts state competitors) = true

A valid final-table Ready mark is recorded in the executable capability table.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.mem_minimalCapabilities_iff {State : Type v} [DecidableEq State] (marked : CapabilityTable State) (config : ReadyConfig State) (capability : Capability) : capability ∈ minimalCapabilities marked config ↔ minimalCap (fun (candidate : Capability) => (config, candidate) ∈ marked) capability

Executable capability pruning is semantic minimality over the raw marker table.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capabilityTable_raw_sound {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : competitors ⊆ lts.states.toFinset) (entry : CapabilityConfig State) (hEntry : entry ∈ capabilityTable lts state competitors) : alphaCapRaw rsObsCap (lfpDRS env (decode entry.1.1) (CCS.FiniteLTS.decodeSet decode entry.1.2)) entry.2

Every entry computed by the finite Ready table has a concrete lfp observation.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.refusal_only_step_cofinal {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (root : State) (initial : StateSet State) (state : State) (competitors : StateSet State) (neg : List Action) (hState : state ∈ lts.states) (hConfig : (state, competitors) ∈ queryConfigs lts root initial) (hNotSelf : state ∉ competitors) (Q : ProcSet Action Name) (hSubset : ∀ (process : CCS.CCS Action Name), CCS.FiniteLTS.decodeSet decode competitors process → Q process) {ρ : DiffSysRS Action Name (RSObs Action)} (hStep : DRS env ρ (decode state) Q (RSObs.node [] neg)) : ∃ (finiteCapability : Capability), ((state, competitors), finiteCapability) ∈ capabilityTable lts root initial ∧ capLe finiteCapability (reqOfObs (RSObs.node [] neg))

Refusal-only semantic steps use the all-negative assignment in the root query table.

def EqCheckingAbstractInterpretation.Ready.FiniteLTS.finiteCofinalRelation {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (decode : State → CCS.CCS Action Name) (root : State) (initial : StateSet State) : DiffSysRS Action Name (RSObs Action)

Cofinality at every represented subset in one query-local marker table.

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.finiteCofinalRelation_step_no_self {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (root : State) (initial : StateSet State) (process : CCS.CCS Action Name) (Q : ProcSet Action Name) (observation : RSObs Action) (hStep : DRS env (finiteCofinalRelation lts decode root initial) process Q observation) : ¬Q process

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.finiteCofinalRelation_tt {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (root : State) (initial : StateSet State) (process : CCS.CCS Action Name) (Q : ProcSet Action Name) (hStep : DRS env (finiteCofinalRelation lts decode root initial) process Q RSObs.tt) : finiteCofinalRelation lts decode root initial process Q RSObs.tt

The terminal DRS step is cofinal in a fixed query table.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.finiteCofinalRelation_child {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (root : State) (initial : StateSet State) (hRoot : root ∈ lts.states) (hInitial : initial ⊆ lts.states.toFinset) (config : ReadyConfig State) (hConfig : config ∈ queryConfigs lts root initial) (action : Action) (Qpos : ProcSet Action Name) (observation : RSObs Action) (hChild : ∃ (process' : CCS.CCS Action Name), CCS.Deriv env (decode config.1) action process' ∧ finiteCofinalRelation lts decode root initial process' (CCS.DerivSetOf env Qpos action) observation) (selected : StateSet State) (hSelected : selected ⊆ config.2) (hQpos : ∀ source ∈ selected, Qpos (decode source)) (hNotSelf : config.1 ∉ config.2) : ∃ successor ∈ lts.next config.1 action, ∃ (childCapability : Capability), ((successor, shift lts selected action), childCapability) ∈ capabilityTable lts root initial ∧ capLe childCapability (reqOfObs observation)

A semantic child restricted to listed competitors is marked in the root query table.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.capJoin_least {left right upper : Capability} (hLeft : capLe left upper) (hRight : capLe right upper) : capLe (capJoin left right) upper

The capability join is the least common upper bound.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.branchesRequirement_le_of_origins {Action : Type u} {State : Type v} (negative neg : List Action) (branches : List (Branch Action State)) (pos : List (Action × RSObs Action)) (hNegEmpty : negative.isEmpty = neg.isEmpty) (hLength : branches.length ≤ pos.length) (hOrigins : ∀ branch ∈ branches, ∃ (i : Fin pos.length), capLe branch.capability (reqOfObs (pos.get i).2)) : capLe (branchesRequirement negative branches) (reqOfObs (RSObs.node pos neg))

A compressed finite branch cover stays below the semantic node requirement.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.assignment_node_cofinal {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (root : State) (initial : StateSet State) (config : ReadyConfig State) (hConfig : config ∈ queryConfigs lts root initial) (hNotSelf : config.1 ∉ config.2) (pos : List (Action × RSObs Action)) (neg negative : List Action) (assignment : Assignment Action) (hNegative : negative ∈ FiniteEvaluator.listPowerset lts.actions) (hRefuses : marks.refuses lts config.1 negative = true) (hAssignment : assignment ∈ assignments lts config.2) (hWellFormed : assignmentWellFormed assignment = true) (hValid : negativeAssignmentValid lts (competitorsOf lts config.2) negative assignment = true) (hChildren : ∀ branch ∈ assignmentBranches (competitorsOf lts config.2) assignment, ∃ successor ∈ lts.next config.1 branch.action, ∃ (childCapability : Capability), ((successor, shift lts branch.competitors branch.action), childCapability) ∈ capabilityTable lts root initial ∧ capLe childCapability branch.capability) (hNegEmpty : negative.isEmpty = neg.isEmpty) (hLength : (assignmentBranches (competitorsOf lts config.2) assignment).length ≤ pos.length) (hOrigins : ∀ branch ∈ assignmentBranches (competitorsOf lts config.2) assignment, ∃ (index : Fin pos.length), capLe branch.capability (reqOfObs (pos.get index).2)) : ∃ (finiteCapability : Capability), (config, finiteCapability) ∈ capabilityTable lts root initial ∧ capLe finiteCapability (reqOfObs (RSObs.node pos neg))

A finite partition satisfying the semantic node bounds produces a cofinal table entry.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.semantic_node_choices {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (decode : State → CCS.CCS Action Name) (config : ReadyConfig State) (Q Qneg : ProcSet Action Name) (pos : List (Action × RSObs Action)) (Qpos : Fin pos.length → ProcSet Action Name) (hSubset : ∀ (process : CCS.CCS Action Name), CCS.FiniteLTS.decodeSet decode config.2 process → Q process) (hCover : ∀ (process : CCS.CCS Action Name), Q process → Qneg process ∨ ∃ (i : Fin pos.length), Qpos i process) : ∃ (choice : State → Option (Fin pos.length)), ∀ source ∈ competitorsOf lts config.2, match choice source with | none => Qneg (decode source) | some index => Qpos index (decode source)

Semantic cover chooses one positive index or the negative group for each finite competitor.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.readyCapabilities_correct {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (state : State) (competitors : StateSet State) (capability : Capability) (hState : state ∈ lts.states) (hCompetitors : ∀ competitor ∈ competitors, competitor ∈ lts.states) : capability ∈ readyCapabilities lts state competitors ↔ lfpDRSAbsExactCanon env (decode state) (CCS.FiniteLTS.decodeSet decode competitors) capability

A realized finite Ready evaluator computes the exact concrete lfp capability antichain.

theorem EqCheckingAbstractInterpretation.Ready.FiniteLTS.failsAt_correct {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : CCS.FiniteLTS Action State) (env : CCS.Env Action Name) (decode : State → CCS.CCS Action Name) (realizes : lts.Realizes env decode) (threshold : Capability) (state : State) (competitors : StateSet State) (hState : state ∈ lts.states) (hCompetitors : ∀ competitor ∈ competitors, competitor ∈ lts.states) : failsAt lts threshold state competitors = true ↔ abstractFailsAt (lfpDRSAbsExactCanon env) threshold (decode state) (CCS.FiniteLTS.decodeSet decode competitors)

A realized finite threshold query is equivalent to semantic Ready failure.