Theory "invariants"

Parents     factoredSystem

Signature

Constant Type
invariant :α state -> bool

Definitions

invariant_def
|- ∀fm.
     invariant fm ⇔
     (∀x. x ∈ FDOM fm ∧ fm ' x ⇒ ∀x'. x ≠ x' ∧ x' ∈ FDOM fm ⇒ ¬fm ' x') ∧
     ∃x. x ∈ FDOM fm ∧ fm ' x


Theorems

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 | (FDOM fm = {e}) ∧ invariant fm} = {fm}
invariant_lemma
|- ∀vs. FINITE vs ⇒ (CARD {fm | (FDOM fm = vs) ∧ invariant fm} = CARD vs)