Theory "acycDepGraph"

Parents     parentChildStructure   acyclicity

Signature

Constant Type
N :((α |-> β) # (α |-> β) -> bool) # (α -> bool) # (α -> bool) list -> num
N_curried :((α |-> β) # (α |-> β) -> bool) -> (α -> bool) list -> (α -> bool) -> num
children :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) # (α -> bool) list -> (α -> bool) list
children_curried :((α |-> β) # (α |-> γ) -> bool) -> (α -> bool) list -> (α -> bool) -> (α -> bool) list
dep_DAG :((α |-> β) # (α |-> γ) -> bool) -> (α -> bool) list -> bool
disjoint_varset :(α -> bool) list -> bool
gen_parent_child_rel :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) # (α -> bool) -> bool
n :(α -> bool) # (β # (α |-> γ)) list -> num
top_sorted :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) list -> bool
top_sorted_curried :((α |-> β) # (α |-> γ) -> bool) -> (α -> bool) list -> bool

Definitions

n_def
|- ∀vs as. n (vs,as) = LENGTH (FILTER (λa. varset_action (a,vs)) as)
gen_parent_child_rel_def
|- ∀PROB p c.
     gen_parent_child_rel (PROB,p,c) ⇔
     DISJOINT p c ∧ ¬dep_var_set (PROB,c,p) ∧
     ¬dep_var_set (PROB,p,prob_dom PROB DIFF (p ∪ c)) ∧
     ∀v1 v2.
       v1 ∈ c ∧ v2 ∈ prob_dom PROB DIFF (p ∪ c) ⇒
       ¬dep (PROB,v1,v2) ∨ ¬dep (PROB,v2,v1)
N_primitive_def
|- N =
   WFREC
     (@R.
        WF R ∧
        (∀lvs vs' vs PROB.
           dep_var_set (PROB,vs,vs') ⇒ R (PROB,vs,lvs) (PROB,vs,vs'::lvs)) ∧
        (∀lvs vs' vs PROB.
           dep_var_set (PROB,vs,vs') ⇒ R (PROB,vs',lvs) (PROB,vs,vs'::lvs)) ∧
        ∀lvs vs' vs PROB.
          ¬dep_var_set (PROB,vs,vs') ⇒ R (PROB,vs,lvs) (PROB,vs,vs'::lvs))
     (λN a.
        case a of
          (PROB,vs,[]) => I (problem_plan_bound (prob_proj (PROB,vs)))
        | (PROB,vs,vs'::lvs) =>
            I
              (if dep_var_set (PROB,vs,vs') then
                 problem_plan_bound (prob_proj (PROB,vs)) * N (PROB,vs',lvs) +
                 N (PROB,vs,lvs)
               else N (PROB,vs,lvs)))
top_sorted_primitive_def
|- top_sorted =
   WFREC (@R. WF R ∧ ∀vs lvs PROB. R (PROB,lvs) (PROB,vs::lvs))
     (λtop_sorted a.
        case a of
          (PROB,[]) => I T
        | (PROB,vs::lvs) =>
            I
              (FOLDL (λacc vs'. acc ∧ ¬dep_var_set (PROB,vs',vs)) T lvs ∧
               top_sorted (PROB,lvs)))
disjoint_varset_def
|- ∀lvs.
     disjoint_varset lvs ⇔
     ∀vs vs'. MEM vs lvs ∧ MEM vs' lvs ∧ vs' ≠ vs ⇒ DISJOINT vs vs'
children_def
|- ∀PROB vs lvs.
     children (PROB,vs,lvs) = FILTER (λvs'. dep_var_set (PROB,vs,vs')) lvs
N_curried_def
|- ∀PROB lvs vs. N_curried PROB lvs vs = N (PROB,vs,lvs)
top_sorted_curried_def
|- (∀PROB vs lvs.
      top_sorted_curried PROB (vs::lvs) ⇔
      FOLDL (λacc vs'. acc ∧ ¬dep_var_set (PROB,vs',vs)) T lvs ∧
      top_sorted_curried PROB lvs) ∧ ∀PROB. top_sorted_curried PROB [] ⇔ T
children_curried_def
|- ∀PROB lvs vs.
     children_curried PROB lvs vs =
     FILTER (λvs'. dep_var_set (PROB,vs,vs')) lvs
dep_DAG_def
|- ∀PROB lvs.
     dep_DAG PROB lvs ⇔
     (prob_dom PROB = BIGUNION (set lvs)) ∧ ALL_DISTINCT lvs ∧
     disjoint_varset lvs ∧
     top_sorted_abs (λvs1 vs2. dep_var_set (PROB,vs1,vs2)) lvs


Theorems

parent_children_lemma_1_1_1_2
|- ∀PROB vs vs'.
     gen_parent_child_rel (PROB,vs,vs') ⇒
     child_parent_rel (prob_proj (PROB,prob_dom PROB DIFF vs'),vs)
parent_children_lemma_1_1_1_4_1
|- ∀PROB a vs vs'.
     a ∈ PROB ∧ gen_parent_child_rel (PROB,vs,vs') ∧ FDOM (SND a) ≠ ∅ ⇒
     (varset_action (a,vs') ⇔ ¬varset_action (a,prob_dom PROB DIFF vs'))
parent_children_lemma_1_1_1_4
|- ∀PROB vs vs' s as.
     gen_parent_child_rel (PROB,vs,vs') ∧ as ∈ valid_plans PROB ∧
     no_effectless_act as ∧ EVERY (λa. ¬varset_action (a,vs')) as ⇒
     EVERY (λa. varset_action (a,prob_dom PROB DIFF vs')) as
parent_children_lemma_1_1_1_7_2
|- ∀PROB a vs vs' vs''.
     a ∈ PROB ∧ gen_parent_child_rel (PROB,vs,vs') ∧
     varset_action (a,prob_dom PROB DIFF vs) ⇒
     varset_action (a,vs') ∨ varset_action (a,prob_dom PROB DIFF (vs' ∪ vs))
parent_children_lemma_1_1_1_7
|- ∀PROB vs vs' as.
     gen_parent_child_rel (PROB,vs,vs') ∧ as ∈ valid_plans PROB ∧
     EVERY (λa. ¬varset_action (a,vs')) as ∧ no_effectless_act as ⇒
     (FILTER (λa. varset_action (a,prob_dom PROB DIFF (vs' ∪ vs))) as =
      FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as)
parent_children_lemma_1_1_1_8_1
|- ∀PROB vs vs' as.
     gen_parent_child_rel (PROB,vs,vs') ∧
     EVERY (λa. ¬varset_action (a,vs')) as ∧ as ∈ valid_plans PROB ∧
     no_effectless_act as ⇒
     (FILTER (λa. ¬varset_action (a,prob_dom PROB DIFF vs')) as = [])
parent_children_lemma_1_1_1_8
|- ∀PROB vs vs' s1 s2 as' as.
     s1 ∈ valid_states PROB ∧ s2 ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     EVERY (λa. ¬varset_action (a,vs')) as ∧
     gen_parent_child_rel (PROB,vs,vs') ∧
     sublist as' (as_proj (as,prob_dom PROB DIFF vs')) ∧
     sat_precond_as (s1,as') ∧ sat_precond_as (s2,as) ∧ no_effectless_act as ∧
     (DRESTRICT s1 vs' = DRESTRICT s2 vs') ⇒
     sat_precond_as (s1,replace_projected ([],as',as,prob_dom PROB DIFF vs'))
parent_children_lemma_1_1_1_9_1
|- ∀PROB a vs vs'.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧
     ¬varset_action (a,prob_dom PROB DIFF vs') ⇒
     DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs')
parent_children_lemma_1_1_1_9_2
|- ∀PROB as vs vs'.
     no_effectless_act as ∧ gen_parent_child_rel (PROB,vs,vs') ∧
     as ∈ valid_plans PROB ⇒
     (as_proj
        (FILTER (λa. ¬varset_action (a,prob_dom PROB DIFF vs')) as,
         prob_dom PROB DIFF vs') =
      [])
parent_children_lemma_1_1_1_9
|- ∀PROB vs vs' as' as.
     gen_parent_child_rel (PROB,vs,vs') ∧ as ∈ valid_plans PROB ∧
     no_effectless_act as ∧
     sublist as' (as_proj (as,prob_dom PROB DIFF vs')) ⇒
     (as' =
      as_proj
        (replace_projected ([],as',as,prob_dom PROB DIFF vs'),
         prob_dom PROB DIFF vs'))
parent_children_lemma_1_1_1_11_1
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧ FDOM (SND a) ≠ ∅ ∧
     ¬varset_action (a,prob_dom PROB DIFF vs') ⇒
     ¬varset_action (a,vs) ∧ ¬varset_action (a,prob_dom PROB DIFF (vs ∪ vs'))
parent_children_lemma_1_1_1_11_4
|- ∀PROB a vs vs'.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧ FDOM (SND a) ≠ ∅ ∧
     varset_action (a,prob_dom PROB DIFF vs') ⇒
     ¬DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs')
parent_children_lemma_1_1_1_11_6
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧
     FDOM (SND (action_proj (a,prob_dom PROB DIFF vs'))) ≠ ∅ ⇒
     (varset_action (a,vs) ⇔
      varset_action (action_proj (a,prob_dom PROB DIFF vs'),vs))
parent_children_lemma_1_1_1_11_7
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧ FDOM (SND a) ≠ ∅ ∧
     varset_action (a,vs) ⇒
     varset_action (a,prob_dom PROB DIFF vs')
parent_children_lemma_1_1_1_11
|- ∀PROB vs vs' as as'.
     gen_parent_child_rel (PROB,vs,vs') ∧ as ∈ valid_plans PROB ∧
     sublist as' (as_proj (as,prob_dom PROB DIFF vs')) ∧
     no_effectless_act as ⇒
     (LENGTH (FILTER (λa. varset_action (a,vs)) as') =
      LENGTH
        (FILTER (λa. varset_action (a,vs))
           (replace_projected ([],as',as,prob_dom PROB DIFF vs'))))
parent_children_lemma_1_1_1_12_1
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧
     FDOM (SND (action_proj (a,prob_dom PROB DIFF vs'))) ≠ ∅ ⇒
     (varset_action (a,prob_dom PROB DIFF (vs ∪ vs')) ⇔
      varset_action
        (action_proj (a,prob_dom PROB DIFF vs'),
         prob_dom PROB DIFF (vs ∪ vs')))
parent_children_lemma_1_1_1_12
|- ∀PROB vs vs' as as'.
     gen_parent_child_rel (PROB,vs,vs') ∧ as ∈ valid_plans PROB ∧
     sublist as' (as_proj (as,prob_dom PROB DIFF vs')) ∧
     no_effectless_act as ⇒
     (LENGTH
        (FILTER (λa. varset_action (a,prob_dom PROB DIFF (vs ∪ vs'))) as') =
      LENGTH
        (FILTER (λa. varset_action (a,prob_dom PROB DIFF (vs ∪ vs')))
           (replace_projected ([],as',as,prob_dom PROB DIFF vs'))))
parent_children_lemma_1_1_1_12_1'
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧
     FDOM (SND (action_proj (a,prob_dom PROB DIFF vs'))) ≠ ∅ ⇒
     (varset_action (a,prob_dom PROB DIFF vs') ⇔
      varset_action
        (action_proj (a,prob_dom PROB DIFF vs'),prob_dom PROB DIFF vs'))
parent_children_lemma_1_1_1_12_2'
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧ FDOM (SND a) ≠ ∅ ∧
     varset_action (a,prob_dom PROB DIFF vs') ⇒
     varset_action (a,prob_dom PROB DIFF vs')
parent_children_lemma_1_1_1_12'
|- ∀PROB vs vs' as as'.
     gen_parent_child_rel (PROB,vs,vs') ∧ as ∈ valid_plans PROB ∧
     sublist as' (as_proj (as,prob_dom PROB DIFF vs')) ∧
     no_effectless_act as ⇒
     (LENGTH (FILTER (λa. varset_action (a,prob_dom PROB DIFF vs')) as') =
      LENGTH
        (FILTER (λa. varset_action (a,prob_dom PROB DIFF vs'))
           (replace_projected ([],as',as,prob_dom PROB DIFF vs'))))
parent_children_lemma_1_1_1_13_1
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧
     FDOM (SND (action_proj (a,prob_dom PROB DIFF vs'))) ≠ ∅ ⇒
     (¬varset_action (a,prob_dom PROB DIFF (vs' ∪ vs)) ⇔
      ¬varset_action
         (action_proj (a,prob_dom PROB DIFF vs'),
          prob_dom PROB DIFF (vs' ∪ vs)))
parent_children_lemma_1_1_1_13_2
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧ FDOM (SND a) ≠ ∅ ∧
     varset_action (a,prob_dom PROB DIFF (vs' ∪ vs)) ⇒
     FDOM (DRESTRICT (SND a) (prob_dom PROB DIFF vs')) ≠ ∅
parent_children_lemma_1_1_1_13
|- ∀PROB vs vs' as.
     as ∈ valid_plans PROB ∧ gen_parent_child_rel (PROB,vs,vs') ∧
     EVERY (λa. ¬varset_action (a,vs')) as ∧ no_effectless_act as ⇒
     (LENGTH
        (FILTER (λa. varset_action (a,prob_dom PROB DIFF (vs' ∪ vs)))
           (as_proj (as,prob_dom PROB DIFF vs'))) =
      LENGTH
        (FILTER (λa. varset_action (a,prob_dom PROB DIFF (vs' ∪ vs))) as))
parent_children_lemma_1_1_1
|- ∀PROB as vs vs' s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     EVERY (λa. ¬varset_action (a,vs')) as ∧ sat_precond_as (s,as) ∧
     no_effectless_act as ∧ gen_parent_child_rel (PROB,vs,vs') ⇒
     ∃as'.
       (exec_plan (s,as') = exec_plan (s,as)) ∧
       n (vs,as') ≤ problem_plan_bound (prob_proj (PROB,vs)) ∧
       (n (prob_dom PROB DIFF vs,as') = n (prob_dom PROB DIFF vs,as)) ∧
       EVERY (λa. ¬varset_action (a,vs')) as' ∧ sublist as' as ∧
       no_effectless_act as' ∧ sat_precond_as (s,as')
parent_children_lemma_1_1_1'
|- ∀PROB as vs vs' s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     EVERY (λa. ¬varset_action (a,vs')) as ∧
     gen_parent_child_rel (PROB,vs,vs') ⇒
     ∃as'.
       (exec_plan (s,as') = exec_plan (s,as)) ∧
       n (vs,as') ≤ problem_plan_bound (prob_proj (PROB,vs)) ∧
       n (prob_dom PROB DIFF vs,as') ≤ n (prob_dom PROB DIFF vs,as) ∧
       EVERY (λa. ¬varset_action (a,vs')) as' ∧ sublist as' as ∧
       no_effectless_act as' ∧ sat_precond_as (s,as')
parent_children_lemma_1_1
|- ∀PROB as vs vs' s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     gen_parent_child_rel (PROB,vs,vs') ⇒
     ∃as'.
       (∀as''.
          list_frag (as',as'') ∧ EVERY (λa. ¬varset_action (a,vs')) as'' ⇒
          n (vs,as'') ≤ problem_plan_bound (prob_proj (PROB,vs))) ∧
       sublist as' as ∧
       n (prob_dom PROB DIFF vs,as') ≤ n (prob_dom PROB DIFF vs,as) ∧
       (exec_plan (s,as') = exec_plan (s,as))
parent_children_lemma_1_2
|- ∀PROB vs vs' a.
     gen_parent_child_rel (PROB,vs,vs') ∧ a ∈ PROB ∧ FDOM (SND a) ≠ ∅ ∧
     varset_action (a,vs') ⇒
     ¬varset_action (a,vs)
parent_children_lemma_1
|- ∀PROB vs vs' as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     gen_parent_child_rel (PROB,vs,vs') ⇒
     ∃as'.
       n (vs,as') ≤
       problem_plan_bound (prob_proj (PROB,vs)) * (n (vs',as') + 1) ∧
       sublist as' as ∧
       n (prob_dom PROB DIFF vs,as') ≤ n (prob_dom PROB DIFF vs,as) ∧
       (exec_plan (s,as') = exec_plan (s,as))
N_ind
|- ∀P.
     (∀PROB vs vs' lvs.
        (dep_var_set (PROB,vs,vs') ⇒ P (PROB,vs,lvs)) ∧
        (dep_var_set (PROB,vs,vs') ⇒ P (PROB,vs',lvs)) ∧
        (¬dep_var_set (PROB,vs,vs') ⇒ P (PROB,vs,lvs)) ⇒
        P (PROB,vs,vs'::lvs)) ∧ (∀PROB vs. P (PROB,vs,[])) ⇒
     ∀v v1 v2. P (v,v1,v2)
N_def
|- (∀vs' vs lvs PROB.
      N (PROB,vs,vs'::lvs) =
      if dep_var_set (PROB,vs,vs') then
        problem_plan_bound (prob_proj (PROB,vs)) * N (PROB,vs',lvs) +
        N (PROB,vs,lvs)
      else N (PROB,vs,lvs)) ∧
   ∀vs PROB. N (PROB,vs,[]) = problem_plan_bound (prob_proj (PROB,vs))
top_sorted_ind
|- ∀P.
     (∀PROB vs lvs. P (PROB,lvs) ⇒ P (PROB,vs::lvs)) ∧ (∀PROB. P (PROB,[])) ⇒
     ∀v v1. P (v,v1)
top_sorted_def
|- (∀vs lvs PROB.
      top_sorted (PROB,vs::lvs) ⇔
      FOLDL (λacc vs'. acc ∧ ¬dep_var_set (PROB,vs',vs)) T lvs ∧
      top_sorted (PROB,lvs)) ∧ ∀PROB. top_sorted (PROB,[]) ⇔ T
top_sorted_is_top_sorted_abs
|- top_sorted (PROB,lvs) ⇔
   top_sorted_abs (λvs1 vs2. dep_var_set (PROB,vs1,vs2)) lvs
parent_children_main_lemma_1_1_2
|- ∀h lvs.
     ALL_DISTINCT (h::lvs) ∧ disjoint_varset (h::lvs) ⇒
     DISJOINT h (BIGUNION (set lvs))
parent_children_main_lemma_1_1_3
|- ∀h lvs. disjoint_varset (h::lvs) ⇒ disjoint_varset lvs
parent_children_main_lemma_1_1_4
|- ∀PROB h lvs. top_sorted (PROB,h::lvs) ⇒ top_sorted (PROB,lvs)
parent_children_main_lemma_1_1_5
|- ∀PROB vs lvs. top_sorted (PROB,lvs) ⇒ top_sorted (prob_proj (PROB,vs),lvs)
parent_children_main_lemma_1_1_7_1_1
|- ∀PROB vs vs' lvs.
     top_sorted (PROB,vs::vs'::lvs) ⇒ top_sorted (PROB,vs::lvs)
parent_children_main_lemma_1_1_7_1
|- ∀PROB vs lvs vs'.
     top_sorted (PROB,vs::lvs) ∧ MEM vs' lvs ⇒ ¬dep_var_set (PROB,vs',vs)
parent_children_main_lemma_1_1_7
|- ∀PROB vs lvs.
     (prob_dom PROB = BIGUNION (set (vs::lvs))) ∧ ALL_DISTINCT (vs::lvs) ∧
     disjoint_varset (vs::lvs) ∧ top_sorted (PROB,vs::lvs) ⇒
     child_parent_rel (PROB,BIGUNION (set lvs))
parent_children_main_lemma_1_1_8_1
|- ∀vs lvs. sublist (children (PROB,vs,lvs)) lvs
parent_children_main_lemma_1_1_8_4
|- ∀lvs lvs'.
     sublist lvs' lvs ∧ disjoint_varset lvs ⇒
     ∀vs vs'. MEM vs lvs ∧ MEM vs' lvs' ∧ vs' ≠ vs ⇒ DISJOINT vs vs'
parent_children_main_lemma_1_1_8_5
|- ∀PROB vs vs' lvs.
     dep_var_set (PROB,vs,vs') ∧ MEM vs' lvs ⇒
     MEM vs' (children (PROB,vs,lvs))
parent_children_main_lemma_1_1_8_7
|- ∀PROB vs vs' pfx mid sfx.
     top_sorted (PROB,pfx ⧺ [vs] ⧺ mid ⧺ [vs'] ⧺ sfx) ⇒
     ¬dep_var_set (PROB,vs',vs)
parent_children_main_lemma_1_1_8
|- ∀PROB vs lvs.
     (prob_dom PROB = BIGUNION (set (vs::lvs))) ∧ ALL_DISTINCT (vs::lvs) ∧
     disjoint_varset (vs::lvs) ∧ top_sorted (PROB,vs::lvs) ⇒
     gen_parent_child_rel (PROB,vs,BIGUNION (set (children (PROB,vs,lvs))))
parent_children_main_lemma_1_1_11
|- ∀PROB vs lvs as as'.
     MEM vs lvs ⇒
     n (vs,replace_projected ([],as',as,BIGUNION (set lvs))) ≤ n (vs,as')
parent_children_main_lemma_1_1_12
|- ∀PROB vs vs' lvs.
     top_sorted (PROB,vs::lvs) ∧ MEM vs' lvs ⇒
     (N (PROB,vs',lvs) = N (PROB,vs',vs::lvs))
parent_children_main_lemma_1_1_14
|- ∀PROB vs' vs lvs.
     vs ⊆ vs' ∧ BIGUNION (set lvs) ⊆ vs' ⇒
     N (prob_proj (PROB,vs'),vs,lvs) ≤ N (PROB,vs,lvs)
parent_children_main_lemma_1_1_14'
|- ∀PROB lvs vs.
     MEM vs lvs ⇒
     N (prob_proj (PROB,BIGUNION (set lvs)),vs,lvs) ≤ N (PROB,vs,lvs)
parent_children_main_lemma_1_1_15_1
|- ∀PROB vs lvs.
     top_sorted (PROB,vs::lvs) ⇒ ¬dep_var_set (PROB,BIGUNION (set lvs),vs)
parent_children_main_lemma_1_1_15_4
|- ∀PROB as vs vs'.
     as ∈ valid_plans PROB ∧ DISJOINT vs vs' ∧
     (¬dep_var_set (PROB,vs',vs) ∨ ¬dep_var_set (PROB,vs,vs')) ⇒
     n (vs ∪ vs',as) ≤ n (vs,as) + n (vs',as)
parent_children_main_lemma_1_1_15
|- ∀P f PROB as lvs.
     as ∈ valid_plans PROB ∧ no_effectless_act as ∧ top_sorted (PROB,lvs) ∧
     disjoint_varset lvs ∧ ALL_DISTINCT lvs ∧
     EVERY (λvs. n (vs,as) ≤ f vs) lvs ⇒
     n (BIGUNION (set (FILTER P lvs)),as) ≤ SUM (MAP f (FILTER P lvs))
parent_children_main_lemma_1_1_16_1_non_empty_prob
|- ∀vs lvs PROB. vs ≠ ∅ ⇒ (N (PROB,vs,vs::lvs) = N (PROB,vs,lvs))
parent_children_main_lemma_1_1_16_1_empty_prob
|- ∀vs lvs PROB. (vs = ∅) ⇒ (N (PROB,vs,vs::lvs) = N (PROB,vs,lvs))
parent_children_main_lemma_1_1_16_1
|- ∀vs lvs PROB. N (PROB,vs,vs::lvs) = N (PROB,vs,lvs)
parent_children_main_lemma_1_1_16_non_empty_prob
|- ∀PROB vs lvs.
     EVERY (λvs. vs ≠ ∅) (vs::lvs) ∧ top_sorted (PROB,vs::lvs) ⇒
     (N (PROB,vs,vs::lvs) =
      problem_plan_bound (prob_proj (PROB,vs)) *
      (SUM (MAP (λvs'. N (PROB,vs',lvs)) (children (PROB,vs,lvs))) + 1))
parent_children_main_lemma_1_1_16
|- ∀PROB vs lvs.
     top_sorted (PROB,vs::lvs) ⇒
     (N (PROB,vs,vs::lvs) =
      problem_plan_bound (prob_proj (PROB,vs)) *
      (SUM (MAP (λvs'. N (PROB,vs',lvs)) (children (PROB,vs,lvs))) + 1))
parent_children_main_lemma_1_1_non_empty_equiv_classes
|- ∀PROB as lvs s.
     FINITE PROB ∧ EVERY (λvs. vs ≠ ∅) lvs ∧ s ∈ valid_states PROB ∧
     as ∈ valid_plans PROB ∧ ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧
     (prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted (PROB,lvs) ∧
     no_effectless_act as ∧ sat_precond_as (s,as) ∧ lvs ≠ [] ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       EVERY (λvs. n (vs,as') ≤ N (PROB,vs,lvs)) lvs ∧ sat_precond_as (s,as')
parent_children_main_lemma_1_1
|- ∀PROB as lvs s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧
     (prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted (PROB,lvs) ∧
     no_effectless_act as ∧ sat_precond_as (s,as) ∧ lvs ≠ [] ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       EVERY (λvs. n (vs,as') ≤ N (PROB,vs,lvs)) lvs ∧ sat_precond_as (s,as')
parent_children_main_lemma_1_2
|- ∀k as vs.
     EVERY (λa. varset_action (a,vs)) as ∧ n (vs,as) ≤ k ⇒ LENGTH as ≤ k
parent_children_main_lemma_1
|- ∀PROB as lvs s.
     FINITE PROB ∧ ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     (prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted (PROB,lvs) ∧
     no_effectless_act as ∧ sat_precond_as (s,as) ∧ lvs ≠ [] ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       LENGTH as' < SUM (MAP (λvs. N (PROB,vs,lvs)) lvs) + 1
parent_children_main_lemma_1'
|- ∀PROB as lvs s.
     FINITE PROB ∧ ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     (prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted (PROB,lvs) ∧
     sat_precond_as (s,as) ∧ lvs ≠ [] ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       LENGTH as' < SUM (MAP (λvs. N (PROB,vs,lvs)) lvs) + 1
parent_children_main_lemma_1''
|- ∀PROB as lvs s.
     FINITE PROB ∧ ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     (prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted (PROB,lvs) ∧ lvs ≠ [] ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       LENGTH as' < SUM (MAP (λvs. N (PROB,vs,lvs)) lvs) + 1
parent_children_main_lemma_non_empty_graph
|- ∀lvs.
     ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧ lvs ≠ [] ⇒
     ∀PROB.
       ((prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted (PROB,lvs)) ∧
       FINITE PROB ⇒
       problem_plan_bound PROB < SUM (MAP (λvs. N (PROB,vs,lvs)) lvs) + 1
parent_children_main_lemma_empty_graph
|- ∀lvs.
     ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧ (lvs = []) ⇒
     ∀PROB.
       (prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted (PROB,lvs) ⇒
       problem_plan_bound PROB < SUM (MAP (λvs. N (PROB,vs,lvs)) lvs) + 1
parent_children_main_lemma
|- ∀lvs.
     ALL_DISTINCT lvs ∧ disjoint_varset lvs ⇒
     ∀PROB.
       ((prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted (PROB,lvs)) ∧
       FINITE PROB ⇒
       problem_plan_bound PROB < SUM (MAP (λvs. N (PROB,vs,lvs)) lvs) + 1
N_empty
|- N (PROB,∅,lvs) = 0
N_def_ITP2015
|- ∀PROB vs lvs.
     top_sorted (PROB,lvs) ⇒
     (N (PROB,vs,lvs) =
      problem_plan_bound (prob_proj (PROB,vs)) *
      (SUM (MAP (λvs'. N (PROB,vs',lvs)) (children (PROB,vs,lvs))) + 1))
N_is_wighted_longest_path
|- ∀vs.
     N (PROB,vs,lvs) =
     wlp (λvs1 vs2. dep_var_set (PROB,vs1,vs2))
       (λvs. problem_plan_bound (prob_proj (PROB,vs))) $+ $* vs lvs
N_curried_is_wighted_longest_path
|- ∀vs.
     N_curried PROB lvs vs =
     wlp (λvs1 vs2. dep_var_set (PROB,vs1,vs2))
       (λvs. problem_plan_bound (prob_proj (PROB,vs))) $+ $* vs lvs
MAP_LAMBDA_ABSTRACTION_thm
|- MAP f l = MAP (λx. f x) l
top_sorted_curried_uncurried_equiv_thm
|- top_sorted_curried PROB lvs ⇔ top_sorted (PROB,lvs)
children_curried_uncurried_equiv_thm
|- children_curried PROB lvs vs = children (PROB,vs,lvs)
parent_children_main_lemma_curried_N
|- ∀lvs.
     ALL_DISTINCT lvs ∧ disjoint_varset lvs ⇒
     ∀PROB.
       (prob_dom PROB = BIGUNION (set lvs)) ∧ top_sorted_curried PROB lvs ∧
       FINITE PROB ⇒
       problem_plan_bound PROB < SUM (MAP (N_curried PROB lvs) lvs) + 1
N_curried_def_ITP2015
|- ∀PROB vs lvs.
     top_sorted_curried PROB lvs ⇒
     (N_curried PROB lvs vs =
      problem_plan_bound (prob_proj (PROB,vs)) *
      (SUM (MAP (N_curried PROB lvs) (children_curried PROB lvs vs)) + 1))
parent_children_main_lemma_curried_N_thesis
|- ∀lvs PROB.
     FINITE PROB ∧ dep_DAG PROB lvs ⇒
     problem_plan_bound PROB < SUM (MAP (N_curried PROB lvs) lvs) + 1