- child_parent_lemma_1_1_1
-
|- ∀a vs. varset_action (a,vs) ⇒ (DRESTRICT (SND a) vs = SND a)
- child_parent_lemma_1_1_2
-
|- ∀PROB a vs.
a ∈ PROB ∧ child_parent_rel (PROB,vs) ∧ FDOM (SND a) ≠ ∅ ⇒
(varset_action (a,vs) ⇔ ¬varset_action (a,prob_dom PROB DIFF vs))
- child_parent_lemma_1_4_1
-
|- ∀PROB a vs.
child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧
¬DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs) ⇒
DISJOINT (FDOM (SND a)) vs
- child_parent_lemma_1_1
-
|- ∀PROB as vs.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
(as_proj_child (as,vs) = as_proj (as,vs))
- graph_plan_lemma_3
-
|- ∀vs as.
no_effectless_act as ⇒
(LENGTH (FILTER (λa. varset_action (a,vs)) as) =
LENGTH (as_proj_child (as,vs)))
- graph_plan_lemma_18_1
-
|- ∀as vs.
as_proj_child (as,vs) =
FILTER (λa. varset_action (a,vs) ∧ FDOM (SND a) ≠ ∅)
(MAP (λa. (DRESTRICT (FST a) vs,SND a)) as)
- graph_plan_lemma_18
-
|- ∀as vs.
as_proj_child (rem_effectless_act as,vs) =
FILTER (λa. varset_action (a,vs))
(MAP (λa. (DRESTRICT (FST a) vs,SND a)) (rem_effectless_act as))
- child_parent_lemma_1_2_1_1
-
|- ∀PROB vs a.
child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧
¬DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs) ⇒
DISJOINT (FDOM (FST a)) vs
- child_parent_lemma_1_2_1
-
|- ∀PROB vs a.
child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧
varset_action (a,prob_dom PROB DIFF vs) ∧ FDOM (SND a) ≠ ∅ ⇒
FDOM (FST a) ⊆ prob_dom PROB DIFF vs
- child_parent_lemma_1_2
-
|- ∀PROB as vs.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
(as_proj_parent (as,vs) = as_proj (as,prob_dom PROB DIFF vs))
- child_parent_lemma_1
-
|- ∀PROB as vs.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
(as_proj_child (as,vs) = as_proj (as,vs)) ∧
(as_proj_parent (as,vs) = as_proj (as,prob_dom PROB DIFF vs))
- child_parent_lemma_xx
-
|- ∀PROB a vs.
child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧ ¬varset_action (a,vs) ⇒
DISJOINT (FDOM (SND a)) vs
- child_parent_lemma_2_1_1_1_1_1
-
|- ∀PROB s as vs.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
(DRESTRICT s vs = DRESTRICT (exec_plan (s,as_proj_parent (as,vs))) vs)
- child_parent_lemma_2_1_1_1_1
-
|- ∀PROB s s' as vs.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ∧
(DRESTRICT s vs = DRESTRICT (exec_plan (s,as)) vs) ⇒
(DRESTRICT s vs = DRESTRICT (exec_plan (s,as_proj_parent (as,vs))) vs)
- child_parent_lemma_2_1_1_1_3
-
|- ∀as vs.
(∃a. MEM a as ∧ (λa. varset_action (a,vs)) a) ⇒
LENGTH (FILTER (λa. varset_action (a,vs)) (as_proj_parent (as,vs))) <
LENGTH (FILTER (λa. varset_action (a,vs)) as)
- child_parent_lemma_2_1_1_1
-
|- ∀PROB s as vs.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ∧
(DRESTRICT s vs = DRESTRICT (exec_plan (s,as)) vs) ∧
(∃a. MEM a as ∧ (λa. varset_action (a,vs)) a) ⇒
(DRESTRICT (exec_plan (s,as)) vs =
DRESTRICT (exec_plan (s,as_proj_parent (as,vs))) vs) ∧
LENGTH (FILTER (λa. varset_action (a,vs)) (as_proj_parent (as,vs))) <
LENGTH (FILTER (λa. varset_action (a,vs)) as)
- child_parent_lemma_2_1_1_2
-
|- ∀PROB s as vs.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ∧
sat_precond_as (s,as) ⇒
sat_precond_as (s,as_proj_parent (as,vs))
- child_parent_lemma_2_1_2_1
-
|- ∀PROB vs as.
child_parent_rel (PROB,vs) ∧ as ∈ valid_plans PROB ⇒
(as_proj_parent (as,vs) =
FILTER (λa. varset_action (a,prob_dom PROB DIFF vs) ∧ FDOM (SND a) ≠ ∅)
as)
- child_parent_lemma_2_1_2_4
-
|- ∀PROB as vs.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ⇒
(FILTER (λa. varset_action (a,prob_dom PROB DIFF vs) ∧ FDOM (SND a) ≠ ∅)
as =
FILTER (λa. ¬varset_action (a,vs) ∧ FDOM (SND a) ≠ ∅) as)
- replace_projected_ind
-
|- ∀P.
(∀as'' a' as' a as vs.
(¬varset_action (a,vs) ⇒ P (as'' ⧺ [a],a'::as',as,vs)) ∧
(varset_action (a,vs) ∧ a' ≠ action_proj (a,vs) ⇒
P (as'',a'::as',as,vs)) ∧
(varset_action (a,vs) ∧ (a' = action_proj (a,vs)) ⇒
P (as'' ⧺ [a],as',as,vs)) ⇒
P (as'',a'::as',a::as,vs)) ∧ (∀as'' as vs. P (as'',[],as,vs)) ∧
(∀as'' v6 v7 vs. P (as'',v6::v7,[],vs)) ⇒
∀v v1 v2 v3. P (v,v1,v2,v3)
- replace_projected_def
-
|- (∀vs as'' as' as a' a.
replace_projected (as'',a'::as',a::as,vs) =
if varset_action (a,vs) then
if a' = action_proj (a,vs) then
replace_projected (as'' ⧺ [a],as',as,vs)
else replace_projected (as'',a'::as',as,vs)
else replace_projected (as'' ⧺ [a],a'::as',as,vs)) ∧
(∀vs as'' as.
replace_projected (as'',[],as,vs) =
as'' ⧺ FILTER (λa. ¬varset_action (a,vs)) as) ∧
∀vs v7 v6 as''. replace_projected (as'',v6::v7,[],vs) = as''
- stitch_ind
-
|- ∀P.
(∀a' as' vs a as.
(¬varset_action (a,vs) ⇒ P (a'::as') vs as) ∧
(varset_action (a,vs) ∧ a' ≠ action_proj (a,vs) ⇒ P (a'::as') vs as) ∧
(varset_action (a,vs) ∧ (a' = action_proj (a,vs)) ⇒ P as' vs as) ⇒
P (a'::as') vs (a::as)) ∧ (∀vs as. P [] vs as) ∧
(∀a' as' vs. P (a'::as') vs []) ⇒
∀v v1 v2. P v v1 v2
- stitch_def
-
|- (∀vs as' as a' a.
stitch (a'::as') vs (a::as) =
if varset_action (a,vs) then
if a' = action_proj (a,vs) then a::stitch as' vs as
else stitch (a'::as') vs as
else a::stitch (a'::as') vs as) ∧
(∀vs as. stitch [] vs as = FILTER (λa. ¬varset_action (a,vs)) as) ∧
∀vs as' a'. stitch (a'::as') vs [] = []
- replace_projected_stitch
-
|- ∀as as' acc. replace_projected (acc,as',as,vs) = acc ⧺ stitch as' vs as
- graph_plan_lemma_22_1
-
|- ∀as as' as'' vs s.
set as ⊆ s ∧ set as'' ⊆ s ⇒ set (replace_projected (as'',as',as,vs)) ⊆ s
- graph_plan_lemma_22_1'
-
|- ∀as as' as'' vs s.
as ∈ valid_plans s ∧ as'' ∈ valid_plans s ⇒
replace_projected (as'',as',as,vs) ∈ valid_plans s
- graph_plan_lemma_22_2_1
-
|- ∀as as' as'' as''' as'''' vs.
sublist (replace_projected (as'',as',as,vs)) as''' ⇒
sublist (replace_projected (as'''' ⧺ as'',as',as,vs)) (as'''' ⧺ as''')
- graph_plan_lemma_22_2
-
|- ∀as as' vs s. sublist (replace_projected ([],as',as,vs)) as
- graph_plan_lemma_22_3_1
-
|- ∀as''' as'' as' as vs.
replace_projected (as''' ⧺ as'',as',as,vs) =
as''' ⧺ replace_projected (as'',as',as,vs)
- graph_plan_lemma_22_3
-
|- ∀PROB vs as' as.
no_effectless_act as ∧ as ∈ valid_plans PROB ⇒
no_effectless_act (replace_projected ([],as',as,vs))
- graph_plan_lemma_22_4
-
|- ∀PROB vs as as'.
as ∈ valid_plans PROB ∧ child_parent_rel (PROB,vs) ∧
no_effectless_act as ⇒
replace_projected ([],as',as,vs) ∈ valid_plans PROB
- bound_child_parent_lemma_1_1_1_2_1_1
-
|- ∀PROB as vs.
no_effectless_act as ∧ child_parent_rel (PROB,vs) ∧
as ∈ valid_plans PROB ⇒
(as_proj (FILTER (λa. ¬varset_action (a,vs)) as,vs) = [])
- bound_child_parent_lemma_1_1_1_2_1
-
|- ∀PROB as as' vs.
no_effectless_act as ∧ child_parent_rel (PROB,vs) ∧
as ∈ valid_plans PROB ∧ sublist as' (as_proj (as,vs)) ⇒
(as' = as_proj (replace_projected ([],as',as,vs),vs))
- bound_child_parent_lemma_1_1_1_2
-
|- ∀PROB s as vs as'.
child_parent_rel (PROB,vs) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sublist as' (as_proj (as,vs)) ∧
no_effectless_act as ⇒
(LENGTH as' =
LENGTH
(FILTER (λa. varset_action (a,vs))
(replace_projected ([],as',as,vs))))
- bound_child_parent_lemma_1_1_1_3_1_1
-
|- ∀PROB vs a s s'.
child_parent_rel (PROB,vs) ∧ a ∈ PROB ∧ FDOM (SND a) ≠ ∅ ∧
s ∈ valid_states PROB ∧ s' ∈ valid_states PROB ∧
(DRESTRICT s (prob_dom PROB DIFF vs) =
DRESTRICT s' (prob_dom PROB DIFF vs)) ∧ ¬varset_action (a,vs) ∧
FST a ⊑ s ⇒
FST a ⊑ s'
- bound_child_parent_lemma_1_1_1_3_1
-
|- ∀PROB vs sa sc as as_c.
sublist as_c (as_proj (as,vs)) ∧ sa ∈ valid_states PROB ∧
sc ∈ valid_states PROB ∧ child_parent_rel (PROB,vs) ∧
as ∈ valid_plans PROB ∧ no_effectless_act as ∧
(DRESTRICT sa (prob_dom PROB DIFF vs) =
DRESTRICT sc (prob_dom PROB DIFF vs)) ∧ sat_precond_as (sa,as) ∧
sat_precond_as (sc,as_c) ⇒
sat_precond_as (sc,replace_projected ([],as_c,as,vs))
- bound_child_parent_lemma_1_1_1_3
-
|- ∀PROB s as vs as'.
child_parent_rel (PROB,vs) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧
sublist as' (as_proj (as,vs)) ∧ no_effectless_act as ∧
sat_precond_as (s,as') ⇒
(DRESTRICT (exec_plan (s,replace_projected ([],as',as,vs))) vs =
exec_plan (DRESTRICT s vs,as'))
- bound_child_parent_lemma_1_1_1_4_1_1
-
|- ∀PROB vs as_c as.
child_parent_rel (PROB,vs) ∧ as ∈ valid_plans PROB ⇒
(FILTER (λa. ¬varset_action (a,vs)) as =
FILTER (λa. ¬varset_action (a,vs)) (replace_projected ([],as_c,as,vs)))
- bound_child_parent_lemma_1_1_1_4_1_2
-
|- ∀PROB vs as.
child_parent_rel (PROB,vs) ∧ no_effectless_act as ∧
as ∈ valid_plans PROB ⇒
(FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as =
FILTER (λa. ¬varset_action (a,vs)) as)
- bound_child_parent_lemma_1_1_1_4_1
-
|- ∀PROB vs as_c as.
child_parent_rel (PROB,vs) ∧ no_effectless_act as ∧
as ∈ valid_plans PROB ⇒
(FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as =
FILTER (λa. varset_action (a,prob_dom PROB DIFF vs))
(replace_projected ([],as_c,as,vs)))
- bound_child_parent_lemma_1_1_1_4_2
-
|- ∀PROB vs as.
child_parent_rel (PROB,vs) ∧ as ∈ valid_plans PROB ∧
no_effectless_act as ⇒
(as_proj (as,prob_dom PROB DIFF vs) =
FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as)
- bound_child_parent_lemma_1_1_1_4_3
-
|- ∀PROB vs s as.
child_parent_rel (PROB,vs) ∧ as ∈ valid_plans PROB ∧
s ∈ valid_states PROB ∧ sat_precond_as (s,as) ∧ no_effectless_act as ⇒
sat_precond_as
(s,FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as)
- bound_child_parent_lemma_1_1_1_4
-
|- ∀PROB vs s as_c as.
child_parent_rel (PROB,vs) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sublist as_c (as_proj (as,vs)) ∧
sat_precond_as (s,as) ∧ sat_precond_as (s,as_c) ∧ no_effectless_act as ⇒
(DRESTRICT (exec_plan (s,as)) (prob_dom PROB DIFF vs) =
DRESTRICT (exec_plan (s,replace_projected ([],as_c,as,vs)))
(prob_dom PROB DIFF vs)) ∧
(FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as =
FILTER (λa. varset_action (a,prob_dom PROB DIFF vs))
(replace_projected ([],as_c,as,vs)))
- bound_child_parent_lemma_1_1_1'
-
|- ∀PROB as vs s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
child_parent_rel (PROB,vs) ∧ sat_precond_as (s,as) ∧
no_effectless_act as ⇒
∃as'.
(exec_plan (s,as') = exec_plan (s,as)) ∧
(LENGTH (FILTER (λa. varset_action (a,vs)) as') ≤
problem_plan_bound (prob_proj (PROB,vs)) ∧
(FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as' =
FILTER (λa. varset_action (a,prob_dom PROB DIFF vs)) as)) ∧
sublist as' as ∧ no_effectless_act as' ∧ as' ∈ valid_plans PROB ∧
sat_precond_as (s,as')
- parent_children_lemma_1_1_1_11_5
-
|- ∀P P2 P3 vs.
(∀a. P3 a ∧ P2 (action_proj (a,vs)) ⇒ (P a ⇔ P (action_proj (a,vs)))) ∧
(∀a. P a ∧ P2 a ∧ P3 a ⇒ varset_action (a,vs)) ∧
(∀a. P2 a ∧ P3 a ∧ ¬varset_action (a,vs) ⇒ DISJOINT (FDOM (SND a)) vs) ⇒
∀as' as''.
sublist as' (as_proj (as'',vs)) ∧ EVERY P2 as' ∧ EVERY P2 as'' ∧
EVERY P3 as'' ⇒
(LENGTH (FILTER P (replace_projected ([],as',as'',vs))) =
LENGTH (FILTER P as'))
- bound_child_parent_lemma_1_1_1''
-
|- ∀PROB as as' vs s.
child_parent_rel (PROB,vs) ∧ s ∈ valid_states PROB ∧
no_effectless_act as ∧ sublist as' (as_proj (as,vs)) ∧
as ∈ valid_plans PROB ∧
(DRESTRICT (exec_plan (s,as)) vs = exec_plan (DRESTRICT s vs,as')) ∧
sat_precond_as (s,as) ∧ sat_precond_as (s,as') ⇒
(exec_plan (s,replace_projected ([],as',as,vs)) = exec_plan (s,as))