- scc_main_lemma_xx
-
|- ∀PROB vs vs'.
scc_vs (PROB,vs) ∧ scc_vs (PROB,vs') ∧ vs ≠ vs' ⇒ DISJOINT vs vs'
- scc_lemma_1_1
-
|- ∀PROB S. FINITE S ⇒ FINITE (member_leaves (PROB,S))
- scc_lemma_1_2
-
|- ∀PROB vs S. vs ∈ member_leaves (PROB,S) ⇒ scc_vs (PROB,vs)
- scc_lemma_1_3
-
|- ∀PROB vs S. vs ∈ member_leaves (PROB,S) ⇒ vs ∈ S
- scc_lemma_1_5
-
|- ∀PROB vs S. vs ∈ member_leaves (PROB,S) ⇒ childless_vs (PROB,vs)
- scc_lemma_1_4_1_1_1
-
|- ∀PROB vs vs'.
scc_vs (PROB,vs') ∧ childless_vs (PROB,vs') ⇒
DISJOINT vs' (BIGUNION (single_child_ancestors PROB vs))
- scc_lemma_1_4_1_1_2_1_2
-
|- ∀PROB vs v v'.
v ∈ vs ∧ v' ∈ vs ∧ scc_vs (PROB,vs) ⇒
(λv v'. dep (PROB,v,v') ∧ v ∈ vs ∧ v' ∈ vs)⁺ v v'
- scc_lemma_1_4_1_1_2_1
-
|- ∀PROB vs vs'.
scc_vs (PROB,vs') ∧ DISJOINT vs vs' ⇒
scc_vs (prob_proj (PROB,prob_dom PROB DIFF vs),vs')
- scc_lemma_1_4_1_1_2_2
-
|- ∀PROB vs vs'.
childless_vs (PROB,vs') ⇒
childless_vs (prob_proj (PROB,prob_dom PROB DIFF vs),vs')
- scc_lemma_1_4_1_1_2
-
|- ∀PROB vs vs' S.
DISJOINT vs vs' ∧ vs' ∈ member_leaves (PROB,S) ⇒
vs' ∈ member_leaves (prob_proj (PROB,prob_dom PROB DIFF vs),S)
- scc_lemma_1_4_1_1
-
|- ∀PROB vs vs' S.
scc_vs (PROB,vs) ∧ vs ≠ vs' ∧ vs' ∈ member_leaves (PROB,S) ⇒
vs' ∈ member_leaves (problem_wo_vs_ancestors (PROB,vs),S)
- scc_lemma_1_4_1
-
|- ∀PROB S vs.
scc_vs (PROB,vs) ⇒
member_leaves (PROB,S) DELETE vs ⊆
member_leaves (problem_wo_vs_ancestors (PROB,vs),S)
- scc_lemma_1_4_2_1_1_1_1
-
|- ∀PROB vs. scc_vs (PROB,vs) ⇒ vs ⊆ prob_dom PROB
- scc_lemma_1_4_2_1_1_1
-
|- ∀PROB S vs.
scc_set PROB S ∧
scc_vs (prob_proj (PROB,prob_dom PROB DIFF BIGUNION S),vs) ⇒
scc_vs (PROB,vs)
- scc_lemma_1_4_2_1_1
-
|- ∀PROB S.
scc_set PROB S ⇒
problem_scc_set (prob_proj (PROB,prob_dom PROB DIFF BIGUNION S)) ⊆
problem_scc_set PROB
- scc_lemma_1_4_2_1_2_1_2
-
|- ∀PROB S vs.
scc_vs (PROB,vs) ∧ scc_set PROB S ∧ vs ∉ S ⇒ DISJOINT vs (BIGUNION S)
- scc_lemma_1_4_2_1_2_1
-
|- ∀PROB S vs.
scc_set PROB S ∧ scc_vs (PROB,vs) ∧ vs ∉ S ⇒
∀vs'.
scc_vs (PROB,vs') ∧ vs' ∉ S ⇒
¬dep_var_set (prob_proj (PROB,prob_dom PROB DIFF BIGUNION S),vs,vs') ⇒
¬dep_var_set (PROB,vs,vs')
- scc_lemma_1_4_2_1_2
-
|- ∀PROB vs S.
childless_vs (prob_proj (PROB,prob_dom PROB DIFF BIGUNION S),vs) ∧
scc_set PROB S ∧ scc_vs (PROB,vs) ∧ vs ∉ S ⇒
∀vs'. dep_var_set (PROB,vs,vs') ∧ scc_vs (PROB,vs') ⇒ vs' ∈ S
- scc_lemma_1_4_2_1_3_1_1
-
|- ∀PROB vs vs' S.
dep_var_set (PROB,vs,vs') ∧ scc_set PROB S ∧ vs' ∈ S ∧ vs ∉ S ∧
scc_vs (PROB,vs) ⇒
dep_var_set (PROB,vs,BIGUNION S)
- scc_lemma_1_4_2_1_3_1_2_1
-
|- ∀PROB vs vs' S.
dep_var_set (PROB,vs,vs') ∧ scc_set PROB S ∧ vs ∈ S ∧ vs' ∉ S ∧
scc_vs (PROB,vs') ⇒
dep_var_set (PROB,BIGUNION S,vs')
- scc_lemma_1_4_2_1_3_1_2
-
|- ∀PROB S vs vs'.
scc_set PROB S ∧ childless_vs (PROB,BIGUNION S) ∧
dep_var_set (PROB,vs,vs') ∧ scc_vs (PROB,vs') ∧ vs ∈ S ⇒
vs' ∈ S
- scc_lemma_1_4_2_1_3_1_4_2
-
|- ∀PROB v. v ∈ prob_dom PROB ⇒ ∃vs. scc_vs (PROB,vs) ∧ v ∈ vs
- scc_lemma_1_4_2_1_3_1_4
-
|- ∀PROB vs vs'.
dep_var_set (PROB,vs,vs') ∧ scc_vs (PROB,vs) ⇒
∃vs''.
scc_vs (PROB,vs'') ∧ dep_var_set (PROB,vs,vs'') ∧ ¬DISJOINT vs' vs''
- scc_lemma_1_4_2_1
-
|- ∀PROB S vs.
childless_vs (PROB,vs) ∧ scc_vs (PROB,vs) ⇒
member_leaves (prob_proj (PROB,prob_dom PROB DIFF vs),S) ⊆
member_leaves (PROB,S) ∪ single_child_ancestors PROB vs
- scc_lemma_1_4_2
-
|- ∀PROB S vs vs'.
scc_vs (PROB,vs) ∧ childless_vs (PROB,vs) ∧
vs' ∉ single_child_ancestors PROB vs ∧ vs' ∉ member_leaves (PROB,S) ⇒
vs' ∉ member_leaves (prob_proj (PROB,prob_dom PROB DIFF vs),S)
- scc_lemma_1_4_3_2
-
|- ∀PROB vs vs'.
scc_vs (PROB,vs) ∧ vs' ∈ single_child_ancestors PROB vs ⇒
DISJOINT vs vs' ∧ vs' ≠ ∅
- scc_lemma_1_4_3_3_3_1
-
|- ∀PROB vs vs'.
(λvs vs'. dep_var_set (PROB,vs,vs') ∧ scc_vs (PROB,vs'))⁺ vs vs' ⇒
(λvs vs'. dep_var_set (PROB,vs,vs'))⁺ vs vs'
- scc_lemma_1_4_3_3_3
-
|- ∀PROB vs vs'.
vs' ∈ single_child_ancestors PROB vs ⇒
(λvs vs'. dep_var_set (PROB,vs,vs'))⁺ vs' vs
- scc_lemma_1_4_3_3
-
|- ∀PROB vs vs'.
(λvs vs'. dep_var_set (PROB,vs,vs'))⁺ vs
(vs' ∪ BIGUNION (single_child_ancestors PROB vs')) ⇒
(λvs vs'. dep_var_set (PROB,vs,vs'))⁺ vs vs'
- scc_lemma_1_4_3_8_2
-
|- ∀PROB vs vs'. vs ⊆ vs' ∧ scc_vs (PROB,vs) ∧ scc_vs (PROB,vs') ⇒ (vs = vs')
- scc_lemma_1_4_3_8
-
|- ∀PROB vs vs'.
childless_vs (PROB,vs') ∧ scc_vs (PROB,vs) ∧ scc_vs (PROB,vs') ∧
vs' ⊆ vs ∪ BIGUNION (single_child_ancestors PROB vs) ⇒
(vs' = vs)
- scc_lemma_1_4_3_12_1
-
|- ∀PROB vs.
scc_vs (PROB,vs) ⇒
DISJOINT vs (BIGUNION (single_child_ancestors PROB vs))
- scc_lemma_1_4_3_12
-
|- ∀PROB vs.
scc_vs (PROB,vs) ⇒
scc_set (prob_proj (PROB,prob_dom PROB DIFF vs))
(single_child_ancestors PROB vs)
- scc_lemma_1_4_3_14
-
|- ∀PROB S vs vs'.
scc_vs (PROB,vs) ∧ scc_vs (PROB,vs') ∧ vs' ≠ vs ∧
(∀vs''.
dep_var_set (prob_proj (PROB,prob_dom PROB DIFF vs),vs',vs'') ∧
scc_vs (prob_proj (PROB,prob_dom PROB DIFF vs),vs'') ⇒
vs'' ∈ S) ⇒
∀vs''.
dep_var_set (PROB,vs',vs'') ∧ scc_vs (PROB,vs'') ⇒ vs'' ∈ vs INSERT S
- scc_lemma_1_4_3_15_1
-
|- ∀PROB vs vs'.
scc_vs (PROB,vs) ∧ scc_vs (PROB,vs') ∧ childless_vs (PROB,vs) ∧
(∃vs''. dep_var_set (PROB,vs',vs'')) ∧ vs ≠ vs' ∧
(∀vs''.
dep_var_set (PROB,vs',vs'') ∧ scc_vs (PROB,vs'') ⇒
vs'' ∈ vs INSERT single_child_ancestors PROB vs) ⇒
vs' ∈ single_child_ancestors PROB vs
- scc_lemma_1_4_3_15
-
|- ∀PROB vs vs'.
scc_vs (PROB,vs) ∧ scc_vs (PROB,vs') ∧ childless_vs (PROB,vs) ∧
¬childless_vs (PROB,vs') ∧ vs ≠ vs' ∧
(∀vs''.
dep_var_set (PROB,vs',vs'') ∧ scc_vs (PROB,vs'') ⇒
vs'' ∈ vs INSERT single_child_ancestors PROB vs) ⇒
vs' ∈ single_child_ancestors PROB vs
- scc_lemma_1_4_3
-
|- ∀PROB vs S.
scc_vs (PROB,vs) ∧ childless_vs (PROB,vs) ∧ scc_set PROB S ⇒
member_leaves
(prob_proj
(PROB,
prob_dom PROB DIFF
(vs ∪ BIGUNION (single_child_ancestors PROB vs))),S) ⊆
member_leaves (prob_proj (PROB,prob_dom PROB DIFF vs),S) DIFF
single_child_ancestors PROB vs
- scc_lemma_1_4_6
-
|- ∀PROB vs.
scc_vs (PROB,vs) ⇒
scc_set PROB (vs INSERT single_child_ancestors PROB vs)
- scc_lemma_1_4_7_2
-
|- ∀PROB vs. scc_set PROB (single_child_ancestors PROB vs)
- scc_lemma_1_4_9
-
|- ∀PROB vs vs'.
vs ⊆ vs' ⇒ ¬scc_vs (prob_proj (PROB,prob_dom PROB DIFF vs'),vs)
- scc_lemma_1_4
-
|- ∀S.
FINITE S ⇒
∀PROB vs S'.
scc_set PROB S ∧ scc_vs (PROB,vs) ∧ vs ∉ S' ∧
(member_leaves (PROB,S) = vs INSERT S') ⇒
(member_leaves (problem_wo_vs_ancestors (PROB,vs),S) = S')
- scc_lemma_1_6
-
|- ∀PROB S S'.
scc_set PROB S ∧ scc_set PROB S' ⇒
(BIGUNION (S DIFF S') = BIGUNION S DIFF BIGUNION S')
- scc_lemma_1_7_1
-
|- ∀PROB vs vs'.
member_leaves (PROB,vs) DIFF vs' = member_leaves (PROB,vs DIFF vs')
- scc_lemma_1_7_2
-
|- ∀PROB vs S. vs ∉ member_leaves (problem_wo_vs_ancestors (PROB,vs),S)
- scc_lemma_1_7_3
-
|- ∀PROB vs S.
DISJOINT (single_child_ancestors PROB vs)
(member_leaves (problem_wo_vs_ancestors (PROB,vs),S))
- scc_lemma_1_7
-
|- ∀PROB vs S.
scc_vs (PROB,vs) ∧ childless_vs (PROB,vs) ∧ scc_set PROB S ⇒
(member_leaves (problem_wo_vs_ancestors (PROB,vs),S) =
member_leaves
(problem_wo_vs_ancestors (PROB,vs),
S DIFF (vs INSERT single_child_ancestors PROB vs)))
- scc_lemma_1_8
-
|- ∀PROB vs vs'. member_leaves (PROB,vs) ∩ vs' = member_leaves (PROB,vs ∩ vs')
- scc_main_lemma_1_1_1_1
-
|- ∀PROB vs. scc_vs (PROB,vs) ⇒ vs ⊆ prob_dom PROB
- scc_main_lemma_1_1_1_2
-
|- ∀PROB vs vs'.
¬DISJOINT vs vs' ∧ scc_vs (PROB,vs) ∧ scc_vs (PROB,vs') ⇒ (vs = vs')
- scc_main_lemma_1_1_1
-
|- ∀PROB S vs.
prob_dom PROB ⊆ BIGUNION S ∧ scc_set PROB S ∧ scc_vs (PROB,vs) ⇒ vs ∈ S
- scc_main_lemma_1_1
-
|- ∀PROB S.
prob_dom PROB ⊆ BIGUNION S ∧ scc_set PROB S ⇒
(childless_problem_scc_set PROB = member_leaves (PROB,S))
- scc_main_lemma_1_2_1
-
|- ∀PROB. (prob_dom PROB = ∅) ⇒ ∀vs. ¬scc_vs (PROB,vs)
- scc_main_lemma_1_4
-
|- ∀PROB vs S.
scc_set PROB S ∧ scc_vs (PROB,vs) ∧ prob_dom PROB ⊆ BIGUNION S ⇒
single_child_ancestors PROB vs ⊆ S
- scc_main_lemma_1_5
-
|- ∀PROB vs vs'.
prob_dom PROB ⊆ vs ⇒
prob_dom (prob_proj (PROB,prob_dom PROB DIFF vs')) ⊆ vs DIFF vs'