- two_children_parent_bound_main_lemma_1
-
|- ∀PROB vs_1 vs_2.
two_children_parent_rel (PROB,vs_1,vs_2) ⇒
child_parent_rel (PROB,vs_1 ∪ vs_2)
- two_children_parent_bound_main_lemma_2
-
|- ∀PROB vs_1 vs_2.
vs_1 ⊆ prob_dom PROB ∧ vs_2 ⊆ prob_dom PROB ∧ DISJOINT vs_1 vs_2 ∧
two_children_parent_rel (PROB,vs_1,vs_2) ⇒
indep_rel (prob_proj (PROB,vs_1 ∪ vs_2),vs_1)
- two_children_parent_bound_main_lemma_3_1_1
-
|- ∀PROB vs.
vs ⊆ prob_dom PROB ∧ indep_rel (PROB,vs) ⇒
child_parent_rel (PROB,vs) ∧
child_parent_rel (PROB,prob_dom PROB DIFF vs)