- dep_var_set_self_empty
-
|- ∀PROB vs. dep_var_set (PROB,vs,vs) ⇒ (vs = ∅)
- scc_lemma_1_4_1_1_2_1_2_1
-
|- ∀PROB. reflexive (λv v'. dep (PROB,v,v'))
- scc_lemma_1_4_2_1_3_1_4_1
-
|- ∀PROB v v'.
v ≠ v' ∧ dep (PROB,v,v') ⇒ v ∈ prob_dom PROB ∧ v' ∈ prob_dom PROB
- scc_lemma_1_4_7_1
-
|- ∀PROB S vs.
dep_var_set (PROB,BIGUNION S,vs) ⇒
∃vs'. vs' ∈ S ∧ dep_var_set (PROB,vs',vs)
- scc_lemma_1_4_3_3_1
-
|- ∀PROB vs vs' vs''.
dep_var_set (PROB,vs,vs' ∪ vs'') ⇒
dep_var_set (PROB,vs,vs') ∨ dep_var_set (PROB,vs,vs'')
- scc_lemma_1_4_3_3_2
-
|- ∀PROB vs S.
dep_var_set (PROB,vs,BIGUNION S) ⇒
∃vs'. vs' ∈ S ∧ dep_var_set (PROB,vs,vs')
- scc_main_lemma_1_1_1_1_1
-
|- ∀PROB v1 v2. v1 ≠ v2 ∧ dep_tc PROB v1 v2 ⇒ v1 ∈ prob_dom PROB
- two_children_parent_bound_main_lemma_2_2
-
|- ∀PROB vs_1 vs_2 vs_3.
DISJOINT vs_1 vs_2 ∧ vs_3 ⊆ vs_2 ∧ ¬dep_var_set (PROB,vs_1,vs_2) ⇒
¬dep_var_set (PROB,vs_1,vs_3)
- parent_children_main_lemma_1_1_7_2
-
|- ∀PROB vs lvs.
dep_var_set (PROB,BIGUNION (set lvs),vs) ⇒
∃vs'. MEM vs' lvs ∧ dep_var_set (PROB,vs',vs)
- parent_children_main_lemma_1_1_15_3
-
|- ∀PROB vs svs.
(∀vs'. vs' ∈ svs ⇒ ¬dep_var_set (PROB,vs',vs)) ⇒
¬dep_var_set (PROB,BIGUNION svs,vs)
- parent_children_main_lemma_1_1_15_4_1
-
|- ∀PROB a vs vs'.
a ∈ PROB ∧ DISJOINT vs vs' ∧
(¬dep_var_set (PROB,vs',vs) ∨ ¬dep_var_set (PROB,vs,vs')) ∧
varset_action (a,vs ∪ vs') ⇒
varset_action (a,vs) ∨ varset_action (a,vs')