Theory "dependency"

Parents     rel_utils   actionSeqProcess

Signature

Constant Type
dep :((α |-> β) # (α |-> γ) -> bool) # α # α -> bool
dep_tc :((α |-> β) # (α |-> γ) -> bool) -> α -> α -> bool
dep_var_set :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) # (α -> bool) -> bool

Definitions

dep_def
|- ∀PROB v1 v2.
     dep (PROB,v1,v2) ⇔
     (∃a.
        a ∈ PROB ∧
        (v1 ∈ FDOM (FST a) ∧ v2 ∈ FDOM (SND a) ∨
         v1 ∈ FDOM (SND a) ∧ v2 ∈ FDOM (SND a))) ∨ (v1 = v2)
dep_var_set_def
|- ∀PROB vs1 vs2.
     dep_var_set (PROB,vs1,vs2) ⇔
     ∃v1 v2. v1 ∈ vs1 ∧ v2 ∈ vs2 ∧ DISJOINT vs1 vs2 ∧ dep (PROB,v1,v2)
dep_tc_def
|- ∀PROB. dep_tc PROB = (λv1' v2'. dep (PROB,v1',v2'))⁺


Theorems

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')