Theory "parentTwoChildrenStructure"

Parents     parentChildStructure

Signature

Constant Type
indep_rel :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) -> bool
two_children_parent_rel :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) # (α -> bool) -> bool

Definitions

two_children_parent_rel_def
|- ∀PROB vs_1 vs_2.
     two_children_parent_rel (PROB,vs_1,vs_2) ⇔
     ¬dep_var_set (PROB,vs_1,prob_dom PROB DIFF vs_1) ∧
     ¬dep_var_set (PROB,vs_2,prob_dom PROB DIFF vs_2)
indep_rel_def
|- ∀PROB vs_1.
     indep_rel (PROB,vs_1) ⇔
     ¬dep_var_set (PROB,vs_1,prob_dom PROB DIFF vs_1) ∧
     ¬dep_var_set (PROB,prob_dom PROB DIFF vs_1,vs_1)


Theorems

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)