- invariant_lemma_2_1
-
|- ∀fm fm' x x'.
invariant fm ∧ invariant fm' ∧ (FDOM fm = FDOM fm') ∧ x ∈ FDOM fm ∧
fm ≠ fm' ∧ fm ' x ⇒
¬fm' ' x
- invariant_lemma_2_2
-
|- ∀fm x s.
invariant fm ∧ (FDOM fm = x INSERT s) ∧ ¬fm ' x ⇒ invariant (fm \\ x)
- invariant_lemma_2_3
-
|- ∀fm x s. invariant fm ∧ (FDOM fm = s) ∧ x ∉ s ⇒ invariant (fm |+ (x,F))
- invariant_lemma_2
-
|- ∀fm'' e vs.
vs ≠ ∅ ∧ e ∉ vs ∧ invariant fm'' ∧ (FDOM fm'' = e INSERT vs) ∧ fm'' ' e ⇒
({fm | (FDOM fm = e INSERT vs) ∧ invariant fm} =
fm'' INSERT
IMAGE (λfm'. fm' |+ (e,F)) {fm | (FDOM fm = vs) ∧ invariant fm})
- invariant_lemma_1
-
|- ∀vs.
FINITE vs ⇒
∀e. e ∉ vs ⇒ ∃fm. invariant fm ∧ (FDOM fm = e INSERT vs) ∧ fm ' e
- invariant_lemma_3
-
|- ∃fm fm'. ({fm | (FDOM fm = {e}) ∧ invariant fm} = {fm} ∪ {fm'}) ∧ fm ≠ fm'
- invariant_lemma
-
|- ∀vs. FINITE vs ⇒ (CARD (invariant_states vs) = CARD vs + 1)
- invariant_prob_reachable_states_thm_1
-
|- ∀vs. FINITE vs ⇒ ∃s. (FDOM s = vs) ∧ invariant s
- invariant_prob_reachable_states_thm_2
-
|- ∀vs1 vs2.
FINITE vs1 ∧ FINITE vs2 ∧ (invariant_states vs1 = invariant_states vs2) ⇒
(vs1 = vs2)
- invariantStateSpace_thm_3_1_1
-
|- ∀s vs. invariant s ⇒ invariant (DRESTRICT s vs)
- invariantStateSpace_thm_3_1
-
|- ∀vs.
FINITE vs ⇒
∀s.
FDOM s ⊆ vs ∧ invariant s ⇒
∃s'.
(FDOM s' = vs) ∧ invariant s' ∧ (DRESTRICT s' (FDOM s) = s) ∧
∀x. x ∈ FDOM s' DIFF FDOM s ⇒ ¬s' ' x
- invariantStateSpace_thm_13
-
|- ∀vs. FINITE vs ⇒ invariant_states vs ≠ ∅
- invariantStateSpace_DRESTRICT_SUBSET_thm
-
|- ∀s vs1 vs2.
invariant (DRESTRICT s vs1) ∧ vs2 ⊆ vs1 ⇒ invariant (DRESTRICT s vs2)
- invariant_states_stateSpace_thm
-
|- ∀vs. stateSpace (invariant_states vs) vs
- invariantStateSpace_thm_10_2
-
|- ∀vs1 vs2. ss_proj (invariant_states vs1) (vs1 ∪ vs2) = invariant_states vs1
- invariantStateSpace_thm_10_3
-
|- ∀vs VS.
(∀vs1 vs2. vs2 ∈ vs INSERT VS ∧ vs1 ∈ vs INSERT VS ⇒ DISJOINT vs1 vs2) ⇒
∀ss1 ss2.
ss1 ∈ IMAGE invariant_states (vs INSERT VS) ∧
ss2 ∈ IMAGE invariant_states (vs INSERT VS) ⇒
∃vs1 vs2.
vs1 ∈ vs INSERT VS ∧ stateSpace ss1 vs1 ∧ vs2 ∈ vs INSERT VS ∧
stateSpace ss2 vs2 ∧ DISJOINT vs1 vs2
- invariantStateSpace_thm_10
-
|- ∀VS.
FINITE VS ⇒
(∀vs. vs ∈ VS ⇒ FINITE vs) ∧
(∀vs1 vs2. vs1 ∈ VS ∧ vs2 ∈ VS ∧ vs1 ≠ vs2 ⇒ DISJOINT vs1 vs2) ⇒
∀vs vs2.
FINITE vs ∧ (∀vs1. vs1 ∈ VS ⇒ DISJOINT vs vs1) ⇒
(ss_proj (PRODf (IMAGE invariant_states VS) (invariant_states vs))
(vs2 ∪ vs ∪ BIGUNION VS) =
PRODf (IMAGE invariant_states VS) (invariant_states vs))
- invariantStateSpace_CARD
-
|- ∀VS.
FINITE VS ⇒
∀vs.
FINITE vs ∧ vs ∉ VS ∧ (∀vs'. vs' ∈ VS ⇒ FINITE vs') ⇒
(Π CARD (invariant_states vs INSERT IMAGE invariant_states VS) =
Π (λvs. CARD vs + 1) (vs INSERT VS))