- 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