- inv_precede_prob_list_def
-
|- (∀planningPROB planningPROBList.
inv_precede_prob_list (planningPROB::planningPROBList) ⇔
(∀planningPROB'.
MEM planningPROB' planningPROBList ⇒
precede planningPROB' planningPROB) ∧
inv_precede_prob_list planningPROBList) ∧ (inv_precede_prob_list [] ⇔ T)
- planningProblem_TY_DEF
-
|- ∃rep.
TYPE_DEFINITION
(λa0'.
∀'planningProblem' .
(∀a0'.
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR 0 (a0,a1,a2) (λn. ind_type$BOTTOM)) a0 a1
a2) ⇒
'planningProblem' a0') ⇒
'planningProblem' a0') rep
- planningProblem_case_def
-
|- ∀a0 a1 a2 f. planningProblem_CASE (planningProblem a0 a1 a2) f = f a0 a1 a2
- planningProblem_size_def
-
|- ∀f f1 a0 a1 a2.
planningProblem_size f f1 (planningProblem a0 a1 a2) =
1 +
(fmap_size (λk. 0) (λv. 1 + f1 v) a0 +
fmap_size (λk. 0) (λv. 1 + f1 v) a2)
- planningProblem_I
-
|- ∀f f0 f1. (planningProblem f f0 f1).I = f
- planningProblem_PROB
-
|- ∀f f0 f1. (planningProblem f f0 f1).PROB = f0
- planningProblem_G
-
|- ∀f f0 f1. (planningProblem f f0 f1).G = f1
- planningProblem_I_fupd
-
|- ∀f2 f f0 f1.
planningProblem f f0 f1 with I updated_by f2 =
planningProblem (f2 f) f0 f1
- planningProblem_PROB_fupd
-
|- ∀f2 f f0 f1.
planningProblem f f0 f1 with PROB updated_by f2 =
planningProblem f (f2 f0) f1
- planningProblem_G_fupd
-
|- ∀f2 f f0 f1.
planningProblem f f0 f1 with G updated_by f2 =
planningProblem f f0 (f2 f1)
- planning_prob_dom_def
-
|- ∀planningPROB. planning_prob_dom planningPROB = prob_dom planningPROB.PROB
- plan_def
-
|- ∀planningPROB as.
plan planningPROB as ⇔
as ∈ valid_plans planningPROB.PROB ∧
planningPROB.G ⊑ exec_plan (planningPROB.I,as)
- needed_vars_def
-
|- ∀planningPROB.
needed_vars planningPROB =
{v |
v ∈ FDOM planningPROB.I ∧
((∃a.
a ∈ planningPROB.PROB ∧ v ∈ FDOM (FST a) ∧
(FST a ' v = planningPROB.I ' v)) ∨
v ∈ FDOM planningPROB.G ∧ (planningPROB.I ' v = planningPROB.G ' v))}
- needed_asses_def
-
|- ∀planningPROB.
needed_asses planningPROB =
DRESTRICT planningPROB.I (needed_vars planningPROB)
- precede_def
-
|- ∀planningPROB1 planningPROB2.
precede planningPROB1 planningPROB2 ⇔
(DRESTRICT planningPROB1.G (needed_vars planningPROB2) =
DRESTRICT (needed_asses planningPROB2)
(planning_prob_dom planningPROB1)) ∧
(DRESTRICT planningPROB1.G (planning_prob_dom planningPROB2) =
DRESTRICT planningPROB2.G (planning_prob_dom planningPROB1))
- precede_prob_list_def
-
|- (∀planningPROB planningPROBList.
precede_prob_list (planningPROB::planningPROBList) ⇔
(∀planningPROB'.
MEM planningPROB' planningPROBList ⇒
precede planningPROB planningPROB') ∧
precede_prob_list planningPROBList) ∧ (precede_prob_list [] ⇔ T)
- planning_problem_def
-
|- ∀planningPROB.
planning_problem planningPROB ⇔
planningPROB.I ∈ valid_states planningPROB.PROB ∧
FDOM planningPROB.G ⊆ planning_prob_dom planningPROB
- planning_prob_union_def
-
|- ∀planningPROB1 planningPROB2.
planning_prob_union planningPROB1 planningPROB2 =
<|I := planningPROB1.I ⊌ planningPROB2.I;
PROB := planningPROB1.PROB ∪ planningPROB2.PROB;
G := planningPROB1.G ⊌ planningPROB2.G|>
- planningPROBEMPTY_def
-
|- planningPROBEMPTY = <|I := FEMPTY; PROB := ∅; G := FEMPTY|>
- prob_list_union_def
-
|- ∀planningPROBList.
prob_list_union planningPROBList =
FOLDR planning_prob_union planningPROBEMPTY planningPROBList
- subprob_def
-
|- ∀planningPROB1 planningPROB2.
subprob planningPROB1 planningPROB2 ⇔
planningPROB1.I ⊑ planningPROB2.I ∧
planningPROB1.PROB ⊆ planningPROB2.PROB
- covers_def
-
|- ∀planningPROBList planningPROB.
covers planningPROBList planningPROB ⇔
(∀x.
x ∈ FDOM planningPROB.G ⇒
∃planningPROB'.
MEM planningPROB' planningPROBList ∧ x ∈ FDOM planningPROB'.G ∧
(planningPROB.G ' x = planningPROB'.G ' x)) ∧
∀planningPROB'.
MEM planningPROB' planningPROBList ⇒ subprob planningPROB' planningPROB
- inv_precede_list_cons
-
|- inv_precede_prob_list (h::planningPROBList) ⇒
inv_precede_prob_list planningPROBList
- state_with_needed_asses_eq_init_1
-
|- planning_problem planningPROB ∧ needed_asses planningPROB ⊑ s ∧
sat_precond_as (needed_asses planningPROB,as) ⇒
plan planningPROB as ⇒
planningPROB.G ⊑ exec_plan (s,as)
- precede_prob_list_union'
-
|- ∀planningPROB.
planning_problem planningPROB ∧
(∀planningPROB'.
MEM planningPROB' planningPROBList ⇒
planning_problem planningPROB' ∧ precede planningPROB planningPROB') ∧
(∀planningPROB' planningPROB''.
MEM planningPROB' planningPROBList ∧
MEM planningPROB'' planningPROBList ⇒
agree planningPROB'.I planningPROB''.I ∧
agree planningPROB'.G planningPROB''.G) ⇒
precede planningPROB (prob_list_union planningPROBList)
- precede_prob_list_union
-
|- precede_prob_list planningPROBList ∧
inv_precede_prob_list planningPROBList ⇒
∀planningPROB.
planning_problem planningPROB ∧
(∀planningPROB'.
MEM planningPROB' planningPROBList ⇒
planning_problem planningPROB' ∧ precede planningPROB planningPROB' ∧
planningPROB'.I ⊑ s) ⇒
precede planningPROB (prob_list_union planningPROBList)
- planning_prob_union_precede
-
|- precede planningPROB1 planningPROB ∧ precede planningPROB2 planningPROB ⇒
precede (planning_prob_union planningPROB1 planningPROB2) planningPROB
- precede_planning_prob_union'
-
|- planning_problem planningPROB ∧ planning_problem planningPROB1 ∧
planning_problem planningPROB2 ∧ agree planningPROB1.I planningPROB2.I ∧
agree planningPROB1.G planningPROB2.G ∧
precede planningPROB planningPROB1 ∧ precede planningPROB planningPROB2 ⇒
precede planningPROB (planning_prob_union planningPROB1 planningPROB2)
- precede_planning_prob_union
-
|- planning_problem planningPROB ∧ planning_problem planningPROB1 ∧
planning_problem planningPROB2 ∧ planningPROB1.I ⊑ s ∧
planningPROB2.I ⊑ s ∧ precede planningPROB planningPROB1 ∧
precede planningPROB planningPROB2 ∧ precede planningPROB2 planningPROB1 ∧
precede planningPROB1 planningPROB2 ⇒
precede planningPROB (planning_prob_union planningPROB1 planningPROB2)
- needed_vars_subset
-
|- needed_vars planningPROB ⊆ FDOM planningPROB.I
- planning_prob_dom_union
-
|- planning_prob_dom (planning_prob_union planningPROB1 planningPROB2) =
planning_prob_dom planningPROB1 ∪ planning_prob_dom planningPROB2
- planning_prob_union_needed_vars'
-
|- planning_problem planningPROB1 ∧ planning_problem planningPROB2 ∧
agree planningPROB1.I planningPROB2.I ∧
agree planningPROB1.G planningPROB2.G ⇒
(needed_vars planningPROB1 ∪ needed_vars planningPROB2 =
needed_vars (planning_prob_union planningPROB1 planningPROB2))
- init_union_submap
-
|- planningPROB1.I ⊑ s ∧ planningPROB2.I ⊑ s ⇒
(planning_prob_union planningPROB1 planningPROB2).I ⊑ s
- planningProblem_accessors
-
|- (∀f f0 f1. (planningProblem f f0 f1).I = f) ∧
(∀f f0 f1. (planningProblem f f0 f1).PROB = f0) ∧
∀f f0 f1. (planningProblem f f0 f1).G = f1
- planningProblem_fn_updates
-
|- (∀f2 f f0 f1.
planningProblem f f0 f1 with I updated_by f2 =
planningProblem (f2 f) f0 f1) ∧
(∀f2 f f0 f1.
planningProblem f f0 f1 with PROB updated_by f2 =
planningProblem f (f2 f0) f1) ∧
∀f2 f f0 f1.
planningProblem f f0 f1 with G updated_by f2 =
planningProblem f f0 (f2 f1)
- planningProblem_accfupds
-
|- (∀p f. (p with PROB updated_by f).I = p.I) ∧
(∀p f. (p with G updated_by f).I = p.I) ∧
(∀p f. (p with I updated_by f).PROB = p.PROB) ∧
(∀p f. (p with G updated_by f).PROB = p.PROB) ∧
(∀p f. (p with I updated_by f).G = p.G) ∧
(∀p f. (p with PROB updated_by f).G = p.G) ∧
(∀p f. (p with I updated_by f).I = f p.I) ∧
(∀p f. (p with PROB updated_by f).PROB = f p.PROB) ∧
∀p f. (p with G updated_by f).G = f p.G
- planningProblem_fupdfupds
-
|- (∀p g f.
p with <|I updated_by f; I updated_by g|> = p with I updated_by f ∘ g) ∧
(∀p g f.
p with <|PROB updated_by f; PROB updated_by g|> =
p with PROB updated_by f ∘ g) ∧
∀p g f.
p with <|G updated_by f; G updated_by g|> = p with G updated_by f ∘ g
- planningProblem_fupdfupds_comp
-
|- ((∀g f. I_fupd f ∘ I_fupd g = I_fupd (f ∘ g)) ∧
∀h g f. I_fupd f ∘ I_fupd g ∘ h = I_fupd (f ∘ g) ∘ h) ∧
((∀g f. PROB_fupd f ∘ PROB_fupd g = PROB_fupd (f ∘ g)) ∧
∀h g f. PROB_fupd f ∘ PROB_fupd g ∘ h = PROB_fupd (f ∘ g) ∘ h) ∧
(∀g f. G_fupd f ∘ G_fupd g = G_fupd (f ∘ g)) ∧
∀h g f. G_fupd f ∘ G_fupd g ∘ h = G_fupd (f ∘ g) ∘ h
- planningProblem_fupdcanon
-
|- (∀p g f.
p with <|PROB updated_by f; I updated_by g|> =
p with <|I updated_by g; PROB updated_by f|>) ∧
(∀p g f.
p with <|G updated_by f; I updated_by g|> =
p with <|I updated_by g; G updated_by f|>) ∧
∀p g f.
p with <|G updated_by f; PROB updated_by g|> =
p with <|PROB updated_by g; G updated_by f|>
- planningProblem_fupdcanon_comp
-
|- ((∀g f. PROB_fupd f ∘ I_fupd g = I_fupd g ∘ PROB_fupd f) ∧
∀h g f. PROB_fupd f ∘ I_fupd g ∘ h = I_fupd g ∘ PROB_fupd f ∘ h) ∧
((∀g f. G_fupd f ∘ I_fupd g = I_fupd g ∘ G_fupd f) ∧
∀h g f. G_fupd f ∘ I_fupd g ∘ h = I_fupd g ∘ G_fupd f ∘ h) ∧
(∀g f. G_fupd f ∘ PROB_fupd g = PROB_fupd g ∘ G_fupd f) ∧
∀h g f. G_fupd f ∘ PROB_fupd g ∘ h = PROB_fupd g ∘ G_fupd f ∘ h
- planningProblem_component_equality
-
|- ∀p1 p2. (p1 = p2) ⇔ (p1.I = p2.I) ∧ (p1.PROB = p2.PROB) ∧ (p1.G = p2.G)
- planningProblem_updates_eq_literal
-
|- ∀p f1 f0 f.
p with <|I := f1; PROB := f0; G := f|> = <|I := f1; PROB := f0; G := f|>
- planningProblem_literal_nchotomy
-
|- ∀p. ∃f1 f0 f. p = <|I := f1; PROB := f0; G := f|>
- FORALL_planningProblem
-
|- ∀P. (∀p. P p) ⇔ ∀f1 f0 f. P <|I := f1; PROB := f0; G := f|>
- EXISTS_planningProblem
-
|- ∀P. (∃p. P p) ⇔ ∃f1 f0 f. P <|I := f1; PROB := f0; G := f|>
- planningProblem_literal_11
-
|- ∀f11 f01 f1 f12 f02 f2.
(<|I := f11; PROB := f01; G := f1|> =
<|I := f12; PROB := f02; G := f2|>) ⇔
(f11 = f12) ∧ (f01 = f02) ∧ (f1 = f2)
- datatype_planningProblem
-
|- DATATYPE (record planningProblem I PROB G)
- planningProblem_11
-
|- ∀a0 a1 a2 a0' a1' a2'.
(planningProblem a0 a1 a2 = planningProblem a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')
- planningProblem_case_cong
-
|- ∀M M' f.
(M = M') ∧
(∀a0 a1 a2.
(M' = planningProblem a0 a1 a2) ⇒ (f a0 a1 a2 = f' a0 a1 a2)) ⇒
(planningProblem_CASE M f = planningProblem_CASE M' f')
- planningProblem_caseeq
-
|- (planningProblem_CASE x f = v) ⇔
∃f' f0 f1. (x = planningProblem f' f0 f1) ∧ (f f' f0 f1 = v)
- planningProblem_nchotomy
-
|- ∀pp. ∃f f0 f1. pp = planningProblem f f0 f1
- planningProblem_Axiom
-
|- ∀f. ∃fn. ∀a0 a1 a2. fn (planningProblem a0 a1 a2) = f a0 a1 a2
- planningProblem_induction
-
|- ∀P. (∀f f0 f1. P (planningProblem f f0 f1)) ⇒ ∀p. P p
- needed_vars_pair
-
|- needed_vars planningPROB =
{v |
v ∈ FDOM planningPROB.I ∧
((∃p e.
(p,e) ∈ planningPROB.PROB ∧ v ∈ FDOM p ∧
(p ' v = planningPROB.I ' v)) ∨
v ∈ FDOM planningPROB.G ∧ (planningPROB.I ' v = planningPROB.G ' v))}
- precede_prob_list_cons
-
|- precede_prob_list (planningPROB::planningPROBList) ⇒
precede_prob_list planningPROBList
- planning_problem_dom
-
|- planning_problem planningPROB ⇒
(planning_prob_dom planningPROB = FDOM planningPROB.I)
- precede_preserve_goals
-
|- precede planningPROB1 planningPROB2 ∧ plan planningPROB2 as ∧
planningPROB2.I ⊑ s ∧ planning_problem planningPROB2 ⇒
planningPROB1.G ⊑ exec_plan (s,as) ∨ ¬(planningPROB1.G ⊑ s)
- needed_asses_submap_succ
-
|- planning_problem planningPROB ∧ a ∈ planningPROB.PROB ⇒
needed_asses (planningPROB with I := state_succ planningPROB.I a) ⊑
state_succ (needed_asses planningPROB) a
- planning_prob_with_succ_init
-
|- planning_problem planningPROB ∧ h ∈ planningPROB.PROB ⇒
planning_problem (planningPROB with I := state_succ planningPROB.I h)
- plan_works_from_needed_asses
-
|- ∀planningPROB.
planning_problem planningPROB ∧ plan planningPROB as ⇒
planningPROB.G ⊑ exec_plan (needed_asses planningPROB,as)
- precede_preserve_goals_gen
-
|- ∀planningPROB2 as s.
precede planningPROB1 planningPROB2 ∧ plan planningPROB2 as ∧
(needed_asses planningPROB2 = system_needed_asses planningPROB2.PROB s) ∧
planning_problem planningPROB2 ∧ planningPROB1.G ⊑ s ⇒
planningPROB1.G ⊑ exec_plan (s,as)
- precede_preserve_goals_gen'
-
|- ∀planningPROB2 as s.
precede planningPROB1 planningPROB2 ∧
planningPROB2.G ⊑ exec_plan (s,as) ∧
as ∈ valid_plans planningPROB2.PROB ∧ planning_problem planningPROB2 ∧
planningPROB1.G ⊑ s ⇒
planningPROB1.G ⊑ exec_plan (s,as)
- precede_preserve_needed_asses
-
|- ∀planningPROB1 as s.
precede planningPROB1 planningPROB2 ∧ plan planningPROB1 as ∧
(needed_asses planningPROB1 = system_needed_asses planningPROB1.PROB s) ∧
needed_asses planningPROB2 ⊑ s ∧ planning_problem planningPROB1 ⇒
needed_asses planningPROB2 ⊑ exec_plan (s,as)
- precede_preserve_needed_asses'
-
|- ∀planningPROB1 as s.
precede planningPROB1 planningPROB2 ∧
planningPROB1.G ⊑ exec_plan (s,as) ∧
as ∈ valid_plans planningPROB1.PROB ∧ needed_asses planningPROB2 ⊑ s ∧
planning_problem planningPROB1 ⇒
needed_asses planningPROB2 ⊑ exec_plan (s,as)
- prob_list_union_goal
-
|- (prob_list_union planningPROBList).G =
FOLDR FUNION FEMPTY (MAP (λplanningPROB. planningPROB.G) planningPROBList)
- planning_prob_goals_submap_list_union_goal_submap
-
|- (∀planningPROB. MEM planningPROB planningPROBList ⇒ planningPROB.G ⊑ s) ⇒
(prob_list_union planningPROBList).G ⊑ s
- prob_list_union_init
-
|- (prob_list_union planningPROBList).I =
FOLDR FUNION FEMPTY (MAP (λplanningPROB. planningPROB.I) planningPROBList)
- planning_prob_init_submap_list_union_goal_submap
-
|- (∀planningPROB. MEM planningPROB planningPROBList ⇒ planningPROB.I ⊑ s) ⇒
(prob_list_union planningPROBList).I ⊑ s
- needed_asses_submap_init
-
|- needed_asses planningPROB ⊑ planningPROB.I
- planning_prob_union_planning_prob
-
|- planning_problem planningPROB1 ∧ planning_problem planningPROB2 ⇒
planning_problem (planning_prob_union planningPROB1 planningPROB2)
- planning_problem_list_union_is_planning_problem
-
|- (∀planningPROB.
MEM planningPROB planningPROBList ⇒ planning_problem planningPROB) ⇒
planning_problem (prob_list_union planningPROBList)
- planning_prob_union_needed_vars_1
-
|- planning_problem planningPROB1 ∧ planning_problem planningPROB2 ∧
planningPROB1.I ⊑ s ∧ planningPROB2.I ⊑ s ⇒
needed_vars (planning_prob_union planningPROB1 planningPROB2) ⊆
needed_vars planningPROB1 ∪ needed_vars planningPROB2
- planning_prob_union_needed_vars_1'
-
|- planning_problem planningPROB1 ∧ planning_problem planningPROB2 ∧
agree planningPROB1.I planningPROB2.I ⇒
needed_vars (planning_prob_union planningPROB1 planningPROB2) ⊆
needed_vars planningPROB1 ∪ needed_vars planningPROB2
- planning_prob_union_needed_vars_2
-
|- planning_problem planningPROB1 ∧ planning_problem planningPROB2 ∧
planningPROB1.I ⊑ s ∧ planningPROB2.I ⊑ s ∧
precede planningPROB1 planningPROB2 ∧ precede planningPROB2 planningPROB1 ⇒
needed_vars planningPROB1 ∪ needed_vars planningPROB2 ⊆
needed_vars (planning_prob_union planningPROB1 planningPROB2)
- planning_prob_union_needed_vars_2''
-
|- planning_problem planningPROB1 ∧ planning_problem planningPROB2 ∧
agree planningPROB1.I planningPROB2.I ∧
agree planningPROB1.G planningPROB2.G ⇒
needed_vars planningPROB1 ∪ needed_vars planningPROB2 ⊆
needed_vars (planning_prob_union planningPROB1 planningPROB2)
- planning_prob_union_needed_vars
-
|- planning_problem planningPROB1 ∧ planning_problem planningPROB2 ∧
agree planningPROB1.I planningPROB2.I ∧
agree planningPROB1.G planningPROB2.G ∧ needed_asses planningPROB1 ⊑ s ∧
needed_asses planningPROB2 ⊑ s ⇒
needed_asses (planning_prob_union planningPROB1 planningPROB2) ⊑ s
- prob_needed_asses_submap_list_union_submap
-
|- (∀planningPROB' planningPROB''.
MEM planningPROB' planningPROBList ∧
MEM planningPROB'' planningPROBList ⇒
agree planningPROB'.I planningPROB''.I ∧
agree planningPROB'.G planningPROB''.G) ⇒
(∀planningPROB.
MEM planningPROB planningPROBList ⇒
needed_asses planningPROB ⊑ s ∧ planning_problem planningPROB) ⇒
needed_asses (prob_list_union planningPROBList) ⊑ s
- valid_plan_valid_in_plan_list_union
-
|- ∀planningPROB.
MEM planningPROB planningPROBList ∧ a ∈ planningPROB.PROB ⇒
a ∈ (prob_list_union planningPROBList).PROB
- IJCAI_Lemma_2_1_1
-
|- precede_prob_list planningPROBList ∧
(∀planningPROB' planningPROB''.
MEM planningPROB' planningPROBList ∧
MEM planningPROB'' planningPROBList ⇒
agree planningPROB'.I planningPROB''.I ∧
agree planningPROB'.G planningPROB''.G) ⇒
∀s.
(∀planningPROB.
MEM planningPROB planningPROBList ⇒
plan planningPROB (f planningPROB) ∧ planning_problem planningPROB ∧
needed_asses planningPROB ⊑ s ∧
sat_precond_as (needed_asses planningPROB,f planningPROB)) ⇒
∀planningPROB.
MEM planningPROB planningPROBList ⇒
planningPROB.G ⊑ exec_plan (s,FLAT (MAP f planningPROBList))
- precede_prob_list_members
-
|- precede_prob_list planningPROBList ∧ MEM planningPROB1 planningPROBList ∧
MEM planningPROB2 planningPROBList ∧ planningPROB1 ≠ planningPROB2 ⇒
precede planningPROB1 planningPROB2 ∨ precede planningPROB2 planningPROB1
- IJCAI_Lemma_2_1
-
|- precede_prob_list planningPROBList ∧
(∀planningPROB' planningPROB''.
MEM planningPROB' planningPROBList ∧
MEM planningPROB'' planningPROBList ⇒
agree planningPROB'.I planningPROB''.I) ⇒
∀s.
(∀planningPROB.
MEM planningPROB planningPROBList ⇒
plan planningPROB (f planningPROB) ∧ planning_problem planningPROB ∧
needed_asses planningPROB ⊑ s ∧
sat_precond_as (needed_asses planningPROB,f planningPROB)) ⇒
∀planningPROB.
MEM planningPROB planningPROBList ⇒
planningPROB.G ⊑ exec_plan (s,FLAT (MAP f planningPROBList))
- IJCAI_Lemma_2
-
|- precede_prob_list planningPROBList ⇒
∀s.
(∀planningPROB.
MEM planningPROB planningPROBList ⇒
planning_problem planningPROB ∧ planningPROB.I ⊑ s ∧
plan planningPROB (f planningPROB) ∧
sat_precond_as (needed_asses planningPROB,f planningPROB)) ⇒
∀planningPROB.
MEM planningPROB planningPROBList ⇒
planningPROB.G ⊑ exec_plan (s,FLAT (MAP f planningPROBList))
- IJCAI_Lemma_2_ITP
-
|- let
subProbPlans = MAP f planningPROBList ;
concatenatedPlans = FLAT subProbPlans
in
precede_prob_list planningPROBList ⇒
(∀planningPROB.
MEM planningPROB planningPROBList ⇒
planning_problem planningPROB ∧ planningPROB.I ⊑ s ∧
plan planningPROB (f planningPROB) ∧
sat_precond_as (needed_asses planningPROB,f planningPROB)) ⇒
∀planningPROB.
MEM planningPROB planningPROBList ⇒
planningPROB.G ⊑ exec_plan (s,concatenatedPlans)
- IJCAI_Theorem_3_1
-
|- covers planningPROBList planningPROB ∧ precede_prob_list planningPROBList ⇒
∀s.
(∀planningPROB.
MEM planningPROB planningPROBList ⇒
planning_problem planningPROB ∧ planningPROB.I ⊑ s ∧
plan planningPROB (f planningPROB) ∧
sat_precond_as (needed_asses planningPROB,f planningPROB)) ⇒
plan planningPROB (FLAT (MAP f planningPROBList))
- IJCAI_Theorem_3
-
|- covers planningPROBList planningPROB ∧ precede_prob_list planningPROBList ⇒
(∀planningPROB.
MEM planningPROB planningPROBList ⇒
planning_problem planningPROB ∧ plan planningPROB (f planningPROB) ∧
sat_precond_as (needed_asses planningPROB,f planningPROB)) ⇒
plan planningPROB (FLAT (MAP f planningPROBList))
- IJCAI_Theorem_3'
-
|- covers planningPROBList planningPROB ∧ precede_prob_list planningPROBList ⇒
(∀planningPROB.
MEM planningPROB planningPROBList ⇒
planning_problem planningPROB ∧ plan planningPROB (f planningPROB)) ⇒
plan planningPROB
(FLAT
(MAP
(λplanningPROB'.
rem_condless_act
(needed_asses planningPROB',[],f planningPROB'))
planningPROBList))