- 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)