Theory "invariantStateSpace"

Parents     invariantsPlusOne

Signature

Constant Type
invariant_ss :((α -> bool) -> bool) -> (α state -> bool) -> bool

Definitions

invariant_ss_def
|- ∀VS ss.
     invariant_ss VS ss ⇔
     ∀s. s ∈ ss ⇒ ∀vs. vs ∈ VS ⇒ invariant (DRESTRICT s vs)


Theorems

invariantStateSpace_thm_3
|- ∀ss vs VS dom.
     FINITE vs ∧ stateSpace ss dom ∧ invariant_ss VS ss ∧ vs ∈ VS ⇒
     ss_proj ss vs ⊆ ss_proj (invariant_states vs) dom
invariantStateSpace_thm_4
|- ∀ss VS1 VS2. invariant_ss VS1 ss ∧ VS2 ⊆ VS1 ⇒ invariant_ss VS2 ss
invariantStateSpace_thm_6
|- ∀ss vs VS. invariant_ss VS ss ⇒ invariant_ss VS (ss_proj ss vs)
invariantStateSpace_thm
|- ∀VS.
     FINITE VS ⇒
     (∀vs. vs ∈ VS ⇒ FINITE vs) ∧
     (∀vs1 vs2. vs1 ∈ VS ∧ vs2 ∈ VS ∧ vs1 ≠ vs2 ⇒ DISJOINT vs1 vs2) ⇒
     ∀vs dom ss.
       FINITE vs ∧ stateSpace ss dom ∧ dom ⊆ vs ∪ BIGUNION VS ∧
       invariant_ss (vs INSERT VS) ss ∧ (∀vs1. vs1 ∈ VS ⇒ DISJOINT vs vs1) ⇒
       ss ⊆
       ss_proj (PRODf (IMAGE invariant_states VS) (invariant_states vs)) dom