- 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