Theory "planningProblem"

Parents     systemAbstraction

Signature

Type Arity
planningProblem 2
Constant Type
covers :(α, β) planningProblem list -> (α, β) planningProblem -> bool
inv_precede_prob_list :(α, β) planningProblem list -> bool
needed_asses :(α, β) planningProblem -> (α |-> β)
needed_vars :(α, β) planningProblem -> α -> bool
plan :(α, β) planningProblem -> ((α |-> β) # (α |-> β)) list -> bool
planningPROBEMPTY :(α, β) planningProblem
planningProblem_CASE :(α, β) planningProblem -> ((α |-> β) -> ((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> γ) -> γ
planningProblem_G :(α, β) planningProblem -> (α |-> β)
planningProblem_G_fupd :((α |-> β) -> (α |-> β)) -> (α, β) planningProblem -> (α, β) planningProblem
planningProblem_I :(α, β) planningProblem -> (α |-> β)
planningProblem_I_fupd :((α |-> β) -> (α |-> β)) -> (α, β) planningProblem -> (α, β) planningProblem
planningProblem_PROB :(α, β) planningProblem -> (α |-> β) # (α |-> β) -> bool
planningProblem_PROB_fupd :(((α |-> β) # (α |-> β) -> bool) -> (α |-> β) # (α |-> β) -> bool) -> (α, β) planningProblem -> (α, β) planningProblem
planningProblem_size :(α -> num) -> (β -> num) -> (α, β) planningProblem -> num
planning_prob_dom :(α, β) planningProblem -> α -> bool
planning_prob_union :(α, β) planningProblem -> (α, β) planningProblem -> (α, β) planningProblem
planning_problem :(α, β) planningProblem -> bool
precede :(α, β) planningProblem -> (α, β) planningProblem -> bool
precede_prob_list :(α, β) planningProblem list -> bool
prob_list_union :(α, β) planningProblem list -> (α, β) planningProblem
recordtype.planningProblem :(α |-> β) -> ((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> (α, β) planningProblem
subprob :(α, β) planningProblem -> (α, β) planningProblem -> bool

Definitions

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


Theorems

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))