- sat_precond_as_ind
-
|- ∀P.
(∀s a as. P (state_succ s a,as) ⇒ P (s,a::as)) ∧ (∀s. P (s,[])) ⇒
∀v v1. P (v,v1)
- sat_precond_as_def
-
|- (∀s as a.
sat_precond_as (s,a::as) ⇔
FST a ⊑ s ∧ sat_precond_as (state_succ s a,as)) ∧
∀s. sat_precond_as (s,[]) ⇔ T
- sat_precond_as_pair
-
|- (sat_precond_as (s,(p,e)::as) ⇔
p ⊑ s ∧ sat_precond_as (state_succ s (p,e),as)) ∧
(sat_precond_as (s,[]) ⇔ T)
- graph_plan_lemma_4
-
|- ∀s s' as vs P.
(∀a. MEM a as ∧ P a ⇒ DISJOINT (FDOM (SND a)) vs) ∧
sat_precond_as (s,as) ∧ sat_precond_as (s',FILTER (λa. ¬P a) as) ∧
(DRESTRICT s vs = DRESTRICT s' vs) ⇒
(DRESTRICT (exec_plan (s,as)) vs =
DRESTRICT (exec_plan (s',FILTER (λa. ¬P a) as)) vs)
- rem_condless_act_ind
-
|- ∀P.
(∀s pfx_a a as.
(¬(FST a ⊑ exec_plan (s,pfx_a)) ⇒ P (s,pfx_a,as)) ∧
(FST a ⊑ exec_plan (s,pfx_a) ⇒ P (s,pfx_a ⧺ [a],as)) ⇒
P (s,pfx_a,a::as)) ∧ (∀s pfx_a. P (s,pfx_a,[])) ⇒
∀v v1 v2. P (v,v1,v2)
- rem_condless_act_def
-
|- (∀s pfx_a as a.
rem_condless_act (s,pfx_a,a::as) =
if FST a ⊑ exec_plan (s,pfx_a) then rem_condless_act (s,pfx_a ⧺ [a],as)
else rem_condless_act (s,pfx_a,as)) ∧
∀s pfx_a. rem_condless_act (s,pfx_a,[]) = pfx_a
- rem_condless_act_pair
-
|- (rem_condless_act (s,pfx_a,(p,e)::as) =
if p ⊑ exec_plan (s,pfx_a) then rem_condless_act (s,pfx_a ⧺ [(p,e)],as)
else rem_condless_act (s,pfx_a,as)) ∧
(rem_condless_act (s,pfx_a,[]) = pfx_a)
- graph_plan_lemma_7_1_1
-
|- ∀s h as pfx.
exec_plan (s,rem_condless_act (s,h::pfx,as)) =
exec_plan (state_succ s h,rem_condless_act (state_succ s h,pfx,as))
- graph_plan_lemma_7_1
-
|- ∀as s. exec_plan (s,as) = exec_plan (s,rem_condless_act (s,[],as))
- graph_plan_lemma_7_2_1_1
-
|- ∀h' pfx as s.
rem_condless_act (s,h'::pfx,as) =
h'::rem_condless_act (state_succ s h',pfx,as)
- graph_plan_lemma_7_2_1
-
|- ∀h h' as as' s.
h'::as' ≼ rem_condless_act (s,[h],as) ⇒
as' ≼ rem_condless_act (state_succ s h,[],as) ∧ (h' = h)
- graph_plan_lemma_7_2
-
|- ∀as s. sat_precond_as (s,rem_condless_act (s,[],as))
- graph_plan_lemma_7_3
-
|- ∀as s. LENGTH (rem_condless_act (s,[],as)) ≤ LENGTH as
- graph_plan_lemma_7_4
-
|- ∀as A s. set as ⊆ A ⇒ set (rem_condless_act (s,[],as)) ⊆ A
- graph_plan_lemma_7_6
-
|- ∀as s P.
LENGTH (FILTER P (rem_condless_act (s,[],as))) ≤ LENGTH (FILTER P as)
- graph_plan_lemma_7_7
-
|- ∀s P as as2.
EVERY P as ∧ EVERY P as2 ⇒ EVERY P (rem_condless_act (s,as2,as))
- graph_plan_lemma_7_8
-
|- ∀s as. sublist (rem_condless_act (s,[],as)) as
- graph_plan_lemma_7_10
-
|- ∀PROB as.
as ∈ valid_plans PROB ⇒ rem_condless_act (s,[],as) ∈ valid_plans PROB
- graph_plan_lemma_7
-
|- ∀as A s.
(exec_plan (s,as) = exec_plan (s,rem_condless_act (s,[],as))) ∧
sat_precond_as (s,rem_condless_act (s,[],as)) ∧
LENGTH (rem_condless_act (s,[],as)) ≤ LENGTH as ∧
(set as ⊆ A ⇒ set (rem_condless_act (s,[],as)) ⊆ A) ∧
∀P. LENGTH (FILTER P (rem_condless_act (s,[],as))) ≤ LENGTH (FILTER P as)
- parent_children_lemma_1_1_1_10_1
-
|- ∀s1 s2 as. s1 ⊑ s2 ∧ sat_precond_as (s1,as) ⇒ sat_precond_as (s2,as)
- submap_init_submap_exec
-
|- ∀s1 s2.
s1 ⊑ s2 ∧ sat_precond_as (s1,as) ⇒ exec_plan (s1,as) ⊑ exec_plan (s2,as)
- parent_children_lemma_1_1_1_10
-
|- ∀vs s as. sat_precond_as (DRESTRICT s vs,as) ⇒ sat_precond_as (s,as)
- varset_action_pair
-
|- varset_action ((p,e),vs) ⇔ FDOM e ⊆ vs
- graph_plan_lemma_14_2
-
|- ∀x y.
(SND x = SND y) ⇒
((λa. varset_action (a,vs)) x ⇔ (λa. varset_action (a,vs)) y)
- graph_plan_lemma_16_1
-
|- ∀s as. exec_plan (s,as) = exec_plan (s,rem_effectless_act as)
- graph_plan_lemma_16_2
-
|- ∀as s. sat_precond_as (s,as) ⇒ sat_precond_as (s,rem_effectless_act as)
- graph_plan_lemma_16_3
-
|- ∀as. LENGTH (rem_effectless_act as) ≤ LENGTH as
- graph_plan_lemma_16_4
-
|- ∀A as. set as ⊆ A ⇒ set (rem_effectless_act as) ⊆ A
- graph_plan_lemma_16_4'
-
|- ∀A as. as ∈ valid_plans A ⇒ rem_effectless_act as ∈ valid_plans A
- graph_plan_lemma_16_5
-
|- ∀P as. LENGTH (FILTER P (rem_effectless_act as)) ≤ LENGTH (FILTER P as)
- graph_plan_lemma_16_6
-
|- ∀as. no_effectless_act (rem_effectless_act as)
- graph_plan_lemma_16_7
-
|- ∀as. no_effectless_act as ⇔ EVERY (λa. FDOM (SND a) ≠ ∅) as
- graph_plan_lemma_16_8
-
|- ∀P as. EVERY P as ⇒ EVERY P (rem_effectless_act as)
- graph_plan_lemma_16_9
-
|- ∀as. sublist (rem_effectless_act as) as
- graph_plan_lemma_16_10
-
|- ∀as P. no_effectless_act as ⇒ no_effectless_act (FILTER P as)
- graph_plan_lemma_16_11
-
|- ∀as1 as2. sublist as1 (rem_effectless_act as2) ⇒ sublist as1 as2
- graph_plan_lemma_16_12
-
|- ∀as1 as2.
no_effectless_act (as1 ⧺ as2) ⇔
no_effectless_act as1 ∧ no_effectless_act as2
- graph_plan_lemma_16_13
-
|- ∀as1 as2. sublist as1 as2 ∧ no_effectless_act as2 ⇒ no_effectless_act as1
- graph_plan_lemma_16_14
-
|- ∀PROB as. exec_plan (s,as) = exec_plan (s,rem_effectless_act as)
- graph_plan_lemma_16
-
|- ∀s A as.
(exec_plan (s,as) = exec_plan (s,rem_effectless_act as)) ∧
(sat_precond_as (s,as) ⇒ sat_precond_as (s,rem_effectless_act as)) ∧
LENGTH (rem_effectless_act as) ≤ LENGTH as ∧
(set as ⊆ A ⇒ set (rem_effectless_act as) ⊆ A) ∧
no_effectless_act (rem_effectless_act as) ∧
∀P. LENGTH (FILTER P (rem_effectless_act as)) ≤ LENGTH (FILTER P as)
- rem_effectless_act_subset_rem_effectless_act_set_thm
-
|- ∀as A. set as ⊆ A ⇒ set (rem_effectless_act as) ⊆ rem_effectless_act_set A
- rem_effectless_act_set_no_empty_actions_thm
-
|- ∀A. rem_effectless_act_set A ⊆ {a | FDOM (SND a) ≠ ∅}
- graph_plan_lemma_7_9
-
|- ∀s as.
no_effectless_act as ⇒ no_effectless_act (rem_condless_act (s,[],as))
- graph_plan_lemma_17
-
|- ∀as_1 as_2 as s.
(as_1 ⧺ as_2 = as) ∧ sat_precond_as (s,as) ⇒
sat_precond_as (s,as_1) ∧ sat_precond_as (exec_plan (s,as_1),as_2)
- vtx_cut_main_lemma_1_1_1_1
-
|- ∀as.
no_effectless_act as ∧ (∀x. FDOM (SND (f x)) ≠ ∅) ⇒
EVERY (λa. f a ≠ (FEMPTY,FEMPTY)) as
- vtx_cut_main_lemma_xx_7
-
|- ∀s as as'.
sat_precond_as (s,as ⧺ as') ⇒ sat_precond_as (exec_plan (s,as),as')
- child_parent_lemma_1_1_5
-
|- ∀PROB a vs.
a ∈ PROB ∧ ¬varset_action (a,vs) ⇒
¬DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs)
- child_parent_lemma_xxx
-
|- ∀PROB a vs.
varset_action (a,vs) ⇒ DISJOINT (FDOM (SND a)) (prob_dom PROB DIFF vs)
- child_parent_lemma_xxxx
-
|- ∀PROB a vs.
varset_action (a,prob_dom PROB DIFF vs) ⇒ DISJOINT (FDOM (SND a)) vs
- child_parent_lemma_xxxxx
-
|- ∀PROB a vs.
varset_action (a,vs) ∧ FDOM (SND a) ≠ ∅ ⇒ ¬DISJOINT (FDOM (SND a)) vs
- child_parent_lemma_xxxxxx
-
|- ∀s a vs. varset_action (a,vs) ⇒ DISJOINT (FDOM (SND a)) (s DIFF vs)
- child_parent_lemma_2_1_2_2
-
|- ∀PROB vs as s.
EVERY (λa. varset_action (a,prob_dom PROB DIFF vs)) as ⇒
(DRESTRICT s vs = DRESTRICT (exec_plan (s,as)) vs)
- bound_child_parent_lemma_1_1_1_4_2_1
-
|- ∀as. no_effectless_act as ⇒ (FILTER (λa. FDOM (SND a) ≠ ∅) as = as)
- parent_children_lemma_1_1_1_7_1
-
|- ∀a vs vs' vs''.
varset_action (a,vs'' DIFF (vs' ∪ vs)) ⇒ varset_action (a,vs'' DIFF vs)
- parent_children_lemma_1_1_1_12_2
-
|- ∀s vs vs' a.
varset_action (a,s DIFF (vs ∪ vs')) ⇒ varset_action (a,s DIFF vs')
- parent_children_main_lemma_1_1_10
-
|- ∀PROB as.
as ∈ valid_plans PROB ⇒
(FILTER (λa. varset_action (a,prob_dom PROB)) as = as)
- parent_children_main_lemma_1_1_11_1
-
|- ∀a vs vs'. vs ⊆ vs' ∧ varset_action (a,vs) ⇒ varset_action (a,vs')
- sat_precond_as_pfx
-
|- ∀s. sat_precond_as (s,as ⧺ as') ⇒ sat_precond_as (s,as)