- scc_lemma_1_4_3_8_2_1
-
|- ∀s t. s ≠ ∅ ∧ s ⊆ t ⇒ ¬DISJOINT s t
- card_union'
-
|- FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒ (CARD (s ∪ t) = CARD s + CARD t)
- CARD_INJ_IMAGE_2
-
|- ∀f s.
FINITE s ⇒
(∀x y. x ∈ s ∧ y ∈ s ⇒ ((f x = f y) ⇔ (x = y))) ⇒
(CARD (IMAGE f s) = CARD s)
- scc_main_lemma_x
-
|- ∀s t x. x ∈ s ∧ x ∉ t ⇒ s ≠ t
- inter_diff_contains
-
|- s ∩ (s DIFF t) = s DIFF t
- scc_lemma_1_4_2_1_1_1_2_1
-
|- ∀s t u. s ⊆ t ∧ s ⊆ t DIFF u ⇒ DISJOINT s u
- scc_lemma_1_4_2_1_2_1_2_1
-
|- ∀s S'. s ∉ S' ⇒ ∀s'. s' ∈ S' ⇒ s ≠ s'
- scc_lemma_1_4_2_1_3_1_4_3
-
|- ∀vs vs' v v'. DISJOINT vs vs' ∧ v ∈ vs ∧ v' ∈ vs' ⇒ v ≠ v'
- scc_lemma_1_4_3_2_1
-
|- ∀s t. ¬(s ⊆ t) ⇒ s ≠ t
- scc_lemma_1_4_3_8_1
-
|- ∀S t.
(∀x y. x ∈ S ∧ y ∈ S ∧ x ≠ y ⇒ DISJOINT x y) ∧
(∀y. y ∈ S ∧ t ≠ y ⇒ DISJOINT t y) ∧ t ⊆ BIGUNION S ∧ S ≠ ∅ ⇒
∃u. u ∈ S ∧ t ⊆ u
- scc_lemma_1_4_3_9
-
|- ∀s t. (s = t) ⇒ s ⊆ t
- scc_lemma_1_4_3_10
-
|- ∀s t u. s ⊆ t ⇒ s ⊆ t ∪ u
- scc_lemma_1_4_3_13
-
|- ∀s S. DISJOINT s (BIGUNION S) ∧ s ≠ ∅ ⇒ s ∉ S
- scc_lemma_1_4_4
-
|- ∀s t. (∀x. x ∉ s ⇒ x ∉ t) ⇒ (t DIFF s = ∅)
- scc_lemma_1_4_5
-
|- ∀x s t. (x INSERT s = t) ⇒ x ∈ t
- scc_lemma_1_4_8
-
|- ∀s t x y. (∀y. y ∉ s ⇒ y ∉ t) ∧ x ∉ t ⇒ y ∉ s DELETE x ⇒ y ∉ t
- scc_lemma_1_4_10
-
|- ∀s t u v x.
u ⊆ s ∪ t ∧ x ∉ v ∧ t DELETE x ⊆ v ∧ v ⊆ u DIFF s ⇒ (v = t DELETE x)
- scc_main_lemma_1_5_1
-
|- ∀s t u. s ⊆ t ⇒ s DIFF u ⊆ t DIFF u
- scc_lemma_1_6_1
-
|- ∀s t.
(∀x y. x ∈ s ∧ y ∈ t ∧ x ≠ y ⇒ DISJOINT x y) ⇒
(BIGUNION (s DIFF t) = BIGUNION s DIFF BIGUNION t)
- eq_funs_eq_images
-
|- (∀x. x ∈ s ⇒ (f1 x = f2 x)) ⇒ (IMAGE f1 s = IMAGE f2 s)
- neq_funs_neq_images
-
|- (∀x. x ∈ s ⇒ ∀y. y ∈ s ⇒ f1 x ≠ f2 y) ∧ (∃x. x ∈ s) ⇒
IMAGE f1 s ≠ IMAGE f2 s
- two_children_parent_bound_main_lemma_2_3
-
|- ∀s t. DISJOINT (s DIFF t) t
- two_children_parent_bound_main_lemma_3_1_2
-
|- ∀s t. t ⊆ s ⇒ (s DIFF (s DIFF t) = t)
- two_children_parent_bound_main_lemma_6
-
|- ∀vs vs'. DISJOINT vs vs' ⇒ (vs DIFF vs' = vs)
- bound_child_parent_lemma_1_1_1_3_1_3
-
|- ∀a b. a ⊆ b ⇒ (a ∩ b = a)
- parent_children_lemma_1_1_1_6_2
-
|- ∀s t u. DISJOINT s t ⇒ ((u DIFF t) ∩ s = u ∩ s)
- parent_children_main_lemma_1_1_1
-
|- ∀s t. DISJOINT s t ⇒ (s DIFF t = s)
- parent_children_main_lemma_1_1_8_2
-
|- ∀x y z. DISJOINT x y ⇒ (x ∪ y DIFF (x ∪ z) = y DIFF z)
- parent_children_main_lemma_1_1_15_2
-
|- ∀s t. s ⊆ t ⇒ BIGUNION s ⊆ BIGUNION t
- invariant_prob_reachable_states_thm_9
-
|- ∀x s. s ⊆ x INSERT s
- invariant_prob_reachable_states_thm_3
-
|- ∀P f x s.
(∀x y. P x ∧ P y ∧ x ≠ y ⇒ f x ≠ f y) ∧ P x ∧ x ∉ s ∧ (∀x. x ∈ s ⇒ P x) ⇒
f x ∉ IMAGE f s
- bound_main_lemma_2_1
-
|- ∀s k. (∀x. x ∈ s ⇒ x ≤ k) ⇒ FINITE s
- bound_main_lemma_1_2
-
|- ∀s k. (∃x. x ∈ s ∧ x ≤ k) ⇒ MIN_SET s ≤ k
- bound_child_parent_lemma_2_1_2
-
|- ∀s k. (∃x. x ∈ s ∧ x < k) ⇒ MIN_SET s < k
- bound_child_parent_lemma_2_2_1
-
|- ∀s k. (∀x. x ∈ s ⇒ x < k) ⇒ FINITE s
- bounded_imp_finite
-
|- ∀s k. (∀x. x ∈ s ⇒ x ≤ k) ⇒ FINITE s
- bound_main_lemma_2
-
|- ∀s k. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x ≤ k) ⇒ MAX_SET s ≤ k
- bound_child_parent_lemma_2_2
-
|- ∀s k. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x < k) ⇒ MAX_SET s < k
- MAX_SET_LEQ_MAX_SET
-
|- s ≠ ∅ ∧ FINITE t ∧ (∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ x ≤ y) ⇒ MAX_SET s ≤ MAX_SET t
- FINITE_ALL_DISTINCT_LISTS
-
|- FINITE P ⇒ FINITE {p | ALL_DISTINCT p ∧ set p ⊆ P}
- DISJOINT_UNION_thm
-
|- ∀s t u. DISJOINT s t ∧ DISJOINT s u ⇒ DISJOINT s (t ∪ u)
- CARD_IMAGE
-
|- ∀f s. FINITE s ⇒ CARD (IMAGE f s) ≤ CARD s
- in_not_in_neq
-
|- x ∈ s ∧ y ∉ s ⇒ x ≠ y
- finite_card_bounded
-
|- FINITE s ⇒ ∃k. CARD s ≤ k
- PROD_IMAGE_MONO_LESS_EQ
-
|- FINITE s ⇒ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ Π f s ≤ Π g s
- PROD_IMAGE_MONO_LESS_EQ'
-
|- FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ Π f s ≤ Π g s
- CARD_SING_REST_INSERT
-
|- FINITE s ⇒ e ∉ s ⇒ SING (REST (e INSERT s)) ⇒ SING s
- TWO_SET_CASES
-
|- ∀a b c d. ({a; b} = {c; d}) ⇒ (a = c) ∧ (b = d) ∨ (a = d) ∧ (b = c)
- INSERT_EQ_TWO_SET
-
|- e ∉ s ∧ a ≠ b ∧ (e INSERT s = {a; b}) ⇒ (s = {a}) ∨ (s = {b})
- CARD_TWO_HAS_TWO_MEM
-
|- FINITE s ⇒ ((CARD s = 2) ⇔ ∃x y. x ≠ y ∧ (s = {x; y}))
- CHOICE_OF_TWO
-
|- ∀a b. (CHOICE {a; b} = a) ∨ (CHOICE {a; b} = b)
- CHOICE_OF_THREE
-
|- ∀a b c.
(CHOICE {a; b; c} = a) ∨ (CHOICE {a; b; c} = b) ∨ (CHOICE {a; b; c} = c)
- CHOICE_AND_REST_OF_TWO
-
|- ∀a b. a ≠ b ⇒ ((CHOICE {a; b} = a) ⇔ (REST {a; b} = {b}))
- CHOICE_AND_REST_OF_THREE
-
|- ∀a b c.
a ≠ b ∧ a ≠ c ∧ b ≠ c ⇒
((CHOICE {a; b; c} = a) ⇔ (REST {a; b; c} = {b; c}))
- SET_TWO_COMM
-
|- {a; b} = {b; a}
- SET_THREE_COMM
-
|- ({a; b; c} = {b; a; c}) ∧ ({a; b; c} = {b; c; a}) ∧ ({a; b; c} = {a; c; b})
- CARD_NZERO_EMPTY
-
|- FINITE s ⇒ s ≠ ∅ ⇒ CARD s > 0
- INSERT_DELETE
-
|- (e INSERT s) DELETE e = s DELETE e
- INSERT_DELETE_2
-
|- e ≠ e' ⇒ ((e' INSERT s) DELETE e = e' INSERT s DELETE e)
- DELETE_DELETE_2
-
|- e' ∉ s ⇒ (s DELETE e DELETE e' = s DELETE e)
- PROD_DELET_LEQ_PROD
-
|- ∀f s e. FINITE s ⇒ (∀x. x ∈ s ⇒ f x > 0) ⇒ Π f (s DELETE e) ≤ Π f s
- PRED_IMG_PRED_COMPOSE
-
|- (∀x. x ∈ s ⇒ P ((f ∘ g) x)) ⇔ ∀y. y ∈ IMAGE g s ⇒ P (f y)
- PROD_IMAGE_COMPOSE
-
|- FINITE s ⇒ (∀x. x ∈ s ⇒ (f ∘ g) x > 0) ⇒ Π f (IMAGE g s) ≤ Π (f ∘ g) s
- PROD_IMAGE_COMPOSE'
-
|- FINITE s ∧ (∀x. x ∈ s ⇒ (f ∘ g) x > 0) ⇒ Π f (IMAGE g s) ≤ Π (f ∘ g) s
- CARD_SUBSET'
-
|- ∀s. FINITE s ∧ t ⊆ s ⇒ CARD t ≤ CARD s
- subset_inter_diff_empty
-
|- s ⊆ t ⇒ (s ∩ (u DIFF t) = ∅)
- UNION_SUBSET_UNION
-
|- s ⊆ u ⇒ s ∪ t ⊆ u ∪ t
- IMAGE_INTER_EQ
-
|- INJ f 𝕌(:α) 𝕌(:β) ⇒ (IMAGE f (s ∩ t) = IMAGE f s ∩ IMAGE f t)