def EqCheckingAbstractInterpretation.FiniteEvaluator.tableStep {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (marked : Set Config) : Set Config

Proof-facing inflationary extension of a finite-domain marker table.

Equations

• EqCheckingAbstractInterpretation.FiniteEvaluator.tableStep domain marks marked = marked ∪ {config : Config | config ∈ domain ∧ marks marked config}

def EqCheckingAbstractInterpretation.FiniteEvaluator.tableStepHom {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (hMarksMono : ∀ {left right : Set Config}, left ⊆ right → ∀ (config : Config), marks left config → marks right config) : Set Config →o Set Config

The table extension is monotone whenever the marker relation is monotone.

Equations

• EqCheckingAbstractInterpretation.FiniteEvaluator.tableStepHom domain marks hMarksMono = { toFun := EqCheckingAbstractInterpretation.FiniteEvaluator.tableStep domain marks, monotone' := ⋯ }

def EqCheckingAbstractInterpretation.FiniteEvaluator.tableLfp {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (hMarksMono : ∀ {left right : Set Config}, left ⊆ right → ∀ (config : Config), marks left config → marks right config) : Set Config

The least marker table induced by a monotone finite-domain marker relation.

Equations

• EqCheckingAbstractInterpretation.FiniteEvaluator.tableLfp domain marks hMarksMono = OrderHom.lfp (EqCheckingAbstractInterpretation.FiniteEvaluator.tableStepHom domain marks ⋯)

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableStep_tableLfp {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (hMarksMono : ∀ {left right : Set Config}, left ⊆ right → ∀ (config : Config), marks left config → marks right config) : tableStep domain marks (tableLfp domain marks ⋯) = tableLfp domain marks ⋯

The Mathlib least marker table is a fixed point of the inflationary extension.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableLfp_subset_of_prefixed {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (hMarksMono : ∀ {left right : Set Config}, left ⊆ right → ∀ (config : Config), marks left config → marks right config) (marked : Set Config) (hPrefixed : tableStep domain marks marked ⊆ marked) : tableLfp domain marks ⋯ ⊆ marked

Any pre-fixed marker table contains the Mathlib least marker table.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.saturateStep_toFinset {Config : Type u} [DecidableEq Config] (configs marked : List Config) (contains : Config → List Config → Bool) (marks : List Config → Config → Bool) (marksSet : Set Config → Config → Prop) (hContains : ∀ (config : Config) (marked : List Config), contains config marked = true ↔ config ∈ marked) (hMarks : ∀ (marked : List Config) (config : Config), marks marked config = true ↔ marksSet (↑marked.toFinset) config) : ↑(saturateStep configs contains marks marked).toFinset = tableStep (↑configs.toFinset) marksSet ↑marked.toFinset

One executable saturation pass denotes the proof-facing tableStep whenever the Boolean membership and marking tests reflect their propositional forms.

def EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) : ℕ → Set Config

The proof-facing approximation after a fixed number of marker-table rounds.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter domain marks 0 = ∅

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter_subset_domain {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (count : ℕ) : tableIter domain marks count ⊆ domain

Every table approximation is contained in its finite configuration domain.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter_subset_succ {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (count : ℕ) : tableIter domain marks count ⊆ tableIter domain marks (count + 1)

Table iteration is inflationary at every round.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter_add_eq_of_prefixed {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (count : ℕ) (hPrefixed : tableStep domain marks (tableIter domain marks count) ⊆ tableIter domain marks count) (extra : ℕ) : tableIter domain marks (count + extra) = tableIter domain marks count

A pre-fixed iteration remains unchanged in all later rounds.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter_ssubset_succ_of_not_prefixed {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (count : ℕ) (hNotPrefixed : ¬tableStep domain marks (tableIter domain marks count) ⊆ tableIter domain marks count) : tableIter domain marks count ⊂ tableIter domain marks (count + 1)

A non-pre-fixed round strictly enlarges the marker table.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter_prefixed_at_card {Config : Type u} (domain : Finset Config) (marks : Set Config → Config → Prop) : tableStep (↑domain) marks (tableIter (↑domain) marks domain.card) ⊆ tableIter (↑domain) marks domain.card

Inflationary iteration over a finite domain reaches a pre-fixed table by its cardinality.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter_prefixed_of_card_le {Config : Type u} (domain : Finset Config) (marks : Set Config → Config → Prop) (count : ℕ) (hCount : domain.card ≤ count) : tableStep (↑domain) marks (tableIter (↑domain) marks count) ⊆ tableIter (↑domain) marks count

Once the finite-cardinality bound is reached, every later round is pre-fixed too.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.saturateN_toFinset {Config : Type u} [DecidableEq Config] (configs : List Config) (contains : Config → List Config → Bool) (marks : List Config → Config → Bool) (marksSet : Set Config → Config → Prop) (hContains : ∀ (config : Config) (marked : List Config), contains config marked = true ↔ config ∈ marked) (hMarks : ∀ (marked : List Config) (config : Config), marks marked config = true ↔ marksSet (↑marked.toFinset) config) (count : ℕ) : ↑(saturateN configs contains marks count).toFinset = tableIter (↑configs.toFinset) marksSet count

Executable saturation rounds denote the corresponding proof-facing table iteration.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.tableIter_subset_tableLfp {Config : Type u} (domain : Set Config) (marks : Set Config → Config → Prop) (hMarksMono : ∀ {left right : Set Config}, left ⊆ right → ∀ (config : Config), marks left config → marks right config) (count : ℕ) : tableIter domain marks count ⊆ tableLfp domain marks ⋯

Every finite table approximation is contained in Mathlib's least fixed point.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.saturateN_eq_tableLfp_of_prefixed {Config : Type u} [DecidableEq Config] (configs : List Config) (contains : Config → List Config → Bool) (marks : List Config → Config → Bool) (marksSet : Set Config → Config → Prop) (hContains : ∀ (config : Config) (marked : List Config), contains config marked = true ↔ config ∈ marked) (hMarks : ∀ (marked : List Config) (config : Config), marks marked config = true ↔ marksSet (↑marked.toFinset) config) (hMarksMono : ∀ {left right : Set Config}, left ⊆ right → ∀ (config : Config), marksSet left config → marksSet right config) (count : ℕ) (hPrefixed : tableStep (↑configs.toFinset) marksSet (tableIter (↑configs.toFinset) marksSet count) ⊆ tableIter (↑configs.toFinset) marksSet count) : ↑(saturateN configs contains marks count).toFinset = tableLfp (↑configs.toFinset) marksSet ⋯

A pre-fixed finite approximation is exactly Mathlib's least marker table.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.saturate_toFinset_eq_tableLfp {Config : Type u} [DecidableEq Config] (configs : List Config) (contains : Config → List Config → Bool) (marks : List Config → Config → Bool) (marksSet : Set Config → Config → Prop) (hContains : ∀ (config : Config) (marked : List Config), contains config marked = true ↔ config ∈ marked) (hMarks : ∀ (marked : List Config) (config : Config), marks marked config = true ↔ marksSet (↑marked.toFinset) config) (hMarksMono : ∀ {left right : Set Config}, left ⊆ right → ∀ (config : Config), marksSet left config → marksSet right config) : ↑(saturate configs contains marks).toFinset = tableLfp (↑configs.toFinset) marksSet ⋯

Bounded executable saturation computes the Mathlib least marker table.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.powerset_member_subset {Element : Type u} [DecidableEq Element] (elements : List Element) (subset : FSet Element) (hSubset : subset ∈ powerset elements) : subset ⊆ elements.toFinset

Every Finset produced by the ordered powerset enumerator lies in its source list.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.subset_mem_powerset {Element : Type u} [DecidableEq Element] (elements : List Element) (subset : FSet Element) (hSubset : subset ⊆ elements.toFinset) : subset ∈ powerset elements

The ordered powerset enumerator contains every subset of its source list.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.configMem_iff {State : Type u} [DecidableEq State] (config : StateConfig State) (configs : List (StateConfig State)) : configMem config configs = true ↔ config ∈ configs

Boolean configuration membership reflects list membership.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.mem_shift_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (competitors : FSet State) (action : Action) (target : State) : target ∈ shift lts competitors action ↔ ∃ competitor ∈ competitors, target ∈ lts.next competitor action

Shifted competitors come from one transition row.

theorem EqCheckingAbstractInterpretation.FiniteEvaluator.mem_configUniverse_iff {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] (lts : CCS.FiniteLTS Action State) (state : State) (competitors : FSet State) : (state, competitors) ∈ configUniverse lts ↔ state ∈ lts.states ∧ competitors ⊆ lts.states.toFinset

The finite configuration universe is the represented state powerset.