Theory "SCCsystemAbstraction"

Parents     parentChildStructure   SCC

Signature

Constant Type
ancestors :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) -> α -> bool
childless_problem_scc_set :((α |-> β) # (α |-> γ) -> bool) -> (α -> bool) -> bool
childless_svs :((α |-> β) # (α |-> γ) -> bool) # ((α -> bool) -> bool) -> bool
childless_vs :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) -> bool
member_leaves :((α |-> β) # (α |-> γ) -> bool) # ((α -> bool) -> bool) -> (α -> bool) -> bool
problem_scc_set :((α |-> β) # (α |-> γ) -> bool) -> (α -> bool) -> bool
problem_wo_vs_ancestors :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) -> (α |-> β) # (α |-> γ) -> bool
scc_set :((α |-> β) # (α |-> γ) -> bool) -> ((α -> bool) -> bool) -> bool
scc_vs :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) -> bool
single_child_ancestors :((α |-> β) # (α |-> γ) -> bool) -> (α -> bool) -> (α -> bool) -> bool
single_child_parents :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) -> (α -> bool) -> bool
sum_scc_parents :((α |-> β) # (α |-> β) -> bool) # ((α -> bool) -> bool) -> num

Definitions

ancestors_def
|- ∀PROB vs.
     ancestors (PROB,vs) =
     {v |
      (∃v'. v' ∈ vs ∧ dep_tc PROB v v') ∧ ∀v'. v' ∈ vs ⇒ ¬dep_tc PROB v' v}
scc_vs_def
|- ∀PROB vs.
     scc_vs (PROB,vs) ⇔
     vs ⊆ prob_dom PROB ∧ SCC (λv1' v2'. dep (PROB,v1',v2')) vs
scc_set_def
|- ∀PROB S. scc_set PROB S ⇔ ∀vs. vs ∈ S ⇒ scc_vs (PROB,vs)
sum_scc_parents_def
|- ∀PROB S.
     sum_scc_parents (PROB,S) =
     ∑ (λvs. problem_plan_bound (prob_proj (PROB,vs ∪ ancestors (PROB,vs))))
       S + 1
childless_vs_def
|- ∀PROB vs. childless_vs (PROB,vs) ⇔ ∀vs'. ¬dep_var_set (PROB,vs,vs')
childless_svs_def
|- ∀PROB S. childless_svs (PROB,S) ⇔ ∀vs. vs ∈ S ⇒ childless_vs (PROB,vs)
problem_scc_set_def
|- ∀PROB. problem_scc_set PROB = {vs | scc_vs (PROB,vs)}
childless_problem_scc_set_def
|- ∀PROB.
     childless_problem_scc_set PROB =
     {vs | scc_vs (PROB,vs) ∧ childless_vs (PROB,vs)}
single_child_parents_def
|- ∀PROB vs.
     single_child_parents (PROB,vs) =
     {vs' |
      vs' ⊆ ancestors (PROB,vs) ∧
      childless_vs (prob_proj (PROB,prob_dom PROB DIFF vs),vs') ∧
      scc_vs (PROB,vs')}
single_child_ancestors_def
|- ∀PROB vs.
     single_child_ancestors PROB vs =
     {vs' |
      ¬(vs' ⊆ vs) ∧ scc_vs (PROB,vs') ∧
      (λvs vs'. dep_var_set (PROB,vs,vs') ∧ scc_vs (PROB,vs'))⁺ vs' vs ∧
      ∀vs''.
        (λvs vs'. dep_var_set (PROB,vs,vs') ∧ scc_vs (PROB,vs'))⁺ vs' vs'' ∧
        childless_vs (PROB,vs'') ⇒
        vs'' ⊆ vs}
member_leaves_def
|- ∀PROB S.
     member_leaves (PROB,S) =
     (λvs. scc_vs (PROB,vs) ∧ childless_vs (PROB,vs)) ∩ S
problem_wo_vs_ancestors_def
|- ∀PROB vs.
     problem_wo_vs_ancestors (PROB,vs) =
     prob_proj
       (PROB,
        prob_dom PROB DIFF (vs ∪ BIGUNION (single_child_ancestors PROB vs)))


Theorems

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'