Theory "instantiation"

Parents     planningProblem

Signature

Constant Type
action_image :(δ -> α) -> (δ |-> β) # (δ |-> γ) -> (α |-> β) # (α |-> γ)
as_image :(δ -> α) -> ((δ |-> β) # (δ |-> γ)) list -> ((α |-> β) # (α |-> γ)) list
common_vars :((α -> β) -> bool) -> (α -> bool) -> α -> bool
fun_INV :(α -> β) -> β -> α
planning_prob_image :(α -> α) -> (α, β) planningProblem -> (α, β) planningProblem
state_image :(γ -> α) -> (γ |-> β) -> (α |-> β)
sustainable_vars :(α, β) planningProblem -> (α -> bool) -> bool
system_image :(δ -> α) -> ((δ |-> β) # (δ |-> γ) -> bool) -> (α |-> β) # (α |-> γ) -> bool
valid_inst :(α -> β) -> bool
valid_instantiations :((α -> β) -> bool) -> (α -> bool) -> bool
well_defined_quot_fun :(α -> β) -> (α |-> γ) -> bool

Definitions

state_image_def
|- ∀f s. state_image f s = s f_o fun_INV f
common_vars_def
|- ∀fSet s.
     common_vars fSet s =
     {v | ∃f1 f2. f1 ∈ fSet ∧ f2 ∈ fSet ∧ f1 ≠ f2 ∧ v ∈ s ∧ (f1 v = f2 v)}
sustainable_vars_def
|- ∀planningPROB vs.
     sustainable_vars planningPROB vs ⇔
     (DRESTRICT planningPROB.I vs = DRESTRICT planningPROB.G vs)
fun_INV_def
|- ∀f x. fun_INV f x = CHOICE {y | f y = x}
valid_inst_def
|- ∀f. valid_inst f ⇔ BIJ f 𝕌(:α) 𝕌(:β)
well_defined_quot_fun_def
|- ∀f s. well_defined_quot_fun f s ⇔ ∀x y. (f x = f y) ⇒ (s ' x = s ' y)
action_image_def
|- ∀f p e. action_image f (p,e) = (state_image f p,state_image f e)
system_image_def
|- ∀f PROB. system_image f PROB = IMAGE (action_image f) PROB
planning_prob_image_def
|- ∀f planningPROB.
     planning_prob_image f planningPROB =
     planningPROB with
     <|I := state_image f planningPROB.I;
       PROB := system_image f planningPROB.PROB;
       G := state_image f planningPROB.G|>
as_image_def
|- ∀f as. as_image f as = MAP (action_image f) as
valid_instantiations_def
|- ∀fSet s.
     valid_instantiations fSet s ⇔
     ∀f1 f2 x y. f1 ∈ fSet ∧ f2 ∈ fSet ∧ x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ f1 x ≠ f2 y


Theorems

fun_INV_back_img
|- valid_inst f ⇒ ({x | fun_INV f x ∈ vs} = IMAGE f vs)
valid_inst_finite_fdom_bak_img
|- valid_inst f ⇒ FINITE {x | fun_INV f x ∈ FDOM fm}
fun_INV_INV
|- BIJ f 𝕌(:α) 𝕌(:β) ⇒ (fun_INV (fun_INV f) x = f x)
fun_INV_works_2
|- BIJ f 𝕌(:α) 𝕌(:β) ⇒ (fun_INV f (f x) = x)
fun_INV_works
|- BIJ f 𝕌(:α) 𝕌(:β) ⇒ (f (fun_INV f x) = x)
BIJ_INV_DET
|- BIJ f 𝕌(:α) 𝕌(:β) ⇒ ((fun_INV f x = y) ⇔ (f y = x))
BIJ_back_IMG
|- BIJ f 𝕌(:α) 𝕌(:β) ⇒ ∃z. {y | f y = x} = {z}
common_vars_subset
|- fSet1 ⊆ fSet2 ⇒ common_vars fSet1 s ⊆ common_vars fSet2 s
FINITE_PRED_12
|- ∀f.
     (∀x y. f x ∈ vs ⇒ ((f x = f y) ⇔ (x = y))) ∧ (∀y. y ∈ vs ⇒ ∃x. f x = y) ⇔
     BIJ f {x | f x ∈ vs} vs
FINITE_PRED_11
|- ∀g. (∀x y. (g x = g y) ⇔ (x = y)) ⇒ ∀f. FINITE {x | g x ∈ FDOM f}
fun_inv_img_3
|- ∀g vs. INJ g vs (IMAGE g vs) ⇒ IMAGE g vs ⊆ {x | LINV g vs x ∈ vs}
fun_inv_img_2
|- ∀g vs. INJ g vs (IMAGE g vs) ⇒ (vs = IMAGE (LINV g vs) (IMAGE g vs))
fun_inv_img
|- ∀g vs.
     BIJ g {x | g x ∈ vs} vs ⇒
     ({x | g x ∈ vs} = IMAGE (LINV g {x | g x ∈ vs}) vs)
sustainable_subset
|- vs1 ⊆ vs2 ∧ sustainable_vars planningPROB1 vs2 ⇒
   sustainable_vars planningPROB1 vs1
sustainable_prob_dom_inter
|- planning_problem planningPROB1 ⇒
   (sustainable_vars planningPROB1 vs ⇔
    sustainable_vars planningPROB1 (planning_prob_dom planningPROB1 ∩ vs))
sustain_imp_precede
|- planning_problem planningPROB1 ∧ planning_problem planningPROB2 ∧
   agree planningPROB1.I planningPROB2.I ∧
   (DRESTRICT planningPROB1.G (planning_prob_dom planningPROB2) =
    DRESTRICT planningPROB2.G (planning_prob_dom planningPROB1)) ∧
   sustainable_vars planningPROB1 (needed_vars planningPROB2) ⇒
   precede planningPROB1 planningPROB2
sustainable_init_goal
|- sustainable_vars planningPROB vs ⇒
   (FDOM planningPROB.I ∩ vs = FDOM planningPROB.G ∩ vs)
state_image_fdom
|- valid_inst f ⇒ (FDOM (state_image f s) = IMAGE f (FDOM s))
system_image_2
|- system_image f PROB = IMAGE (λa. action_image f a) PROB
as_image_2
|- as_image f as = MAP (λa. action_image f a) as
action_image_pair
|- action_image f a = (state_image f (FST a),state_image f (SND a))
f_o_ASSOC
|- (∀x y. (g x = g y) ⇔ (x = y)) ∧ (∀x y. (h x = h y) ⇔ (x = y)) ⇒
   ((f f_o g) f_o h = f f_o g ∘ h)
f_o_ID
|- (∀x. g x = x) ⇒ (f f_o g = f)
state_image_INV
|- valid_inst f ⇒ (state_image (fun_INV f) (state_image f s) = s)
action_image_INV
|- valid_inst f ⇒ (action_image (fun_INV f) (action_image f (p,e)) = (p,e))
system_image_INV
|- valid_inst f ∧ a ∈ system_image f PROB ⇒ action_image (fun_INV f) a ∈ PROB
fun_INV_INV_2
|- BIJ f 𝕌(:α) 𝕌(:β) ⇒ (fun_INV (fun_INV f) = f)
valid_INV
|- valid_inst f ⇒ valid_inst (fun_INV f)
FAPPLY_f_o_2
|- (∀x y. (f x = f y) ⇔ (x = y)) ∧ x ∈ {z | f z ∈ FDOM s} ⇒
   ((s f_o f) ' x = s ' (f x))
img_action_dom
|- valid_inst f ⇒ (action_dom (action_image f a) = IMAGE f (action_dom a))
img_prob_dom
|- valid_inst f ⇒ (prob_dom (system_image f PROB) = IMAGE f (prob_dom PROB))
img_planning_prob_dom
|- valid_inst f ⇒
   (planning_prob_dom (planning_prob_image f planningPROB) =
    IMAGE f (planning_prob_dom planningPROB))
FAPPLY_state_image
|- valid_inst f ∧ x ∈ FDOM s ⇒ (state_image f s ' (f x) = s ' x)
img_needed_vars
|- valid_inst f ⇒
   (needed_vars (planning_prob_image f planningPROB) =
    IMAGE f (needed_vars planningPROB))
valid_instantiations_works
|- valid_instantiations {f1; f2} s ∧ f1 ≠ f2 ⇒
   IMAGE f1 s ∩ IMAGE f2 s ⊆ IMAGE f1 s
valid_instantiations_works'
|- valid_instantiations {f1; f2} s ∧ f1 ≠ f2 ⇒
   IMAGE f1 s ∩ IMAGE f2 s ⊆ IMAGE f1 (common_vars {f1; f2} s)
valid_instantiations_works_2
|- valid_instantiations {f1; f2} s1 ∧ s2 ⊆ s1 ∧ f1 ≠ f2 ⇒
   IMAGE f1 s1 ∩ IMAGE f2 s2 ⊆ IMAGE f1 (s1 ∩ s2)
valid_instantiations_works_2'
|- valid_instantiations {f1; f2} s1 ∧ s2 ⊆ s1 ∧ f1 ≠ f2 ⇒
   IMAGE f1 s1 ∩ IMAGE f2 s2 ⊆ IMAGE f1 (common_vars {f1; f2} s1 ∩ s2)
img_dom_inter_subset_comm_vars_1
|- planning_problem planningPROB ∧ valid_inst f1 ∧ valid_inst f2 ∧
   valid_instantiations {f1; f2} (planning_prob_dom planningPROB) ∧ f1 ≠ f2 ⇒
   planning_prob_dom (planning_prob_image f1 planningPROB) ∩
   needed_vars (planning_prob_image f2 planningPROB) ⊆
   IMAGE f1
     (common_vars {f1; f2} (planning_prob_dom planningPROB) ∩
      needed_vars planningPROB)
valid_instantiations_subset
|- fSet1 ⊆ fSet2 ∧ valid_instantiations fSet2 s ⇒ valid_instantiations fSet1 s
img_dom_inter_subset_comm_vars
|- planning_problem planningPROB ∧ f1 ≠ f2 ∧ valid_inst f1 ∧ valid_inst f2 ∧
   valid_instantiations fSet (planning_prob_dom planningPROB) ∧ f1 ∈ fSet ∧
   f2 ∈ fSet ⇒
   planning_prob_dom (planning_prob_image f1 planningPROB) ∩
   needed_vars (planning_prob_image f2 planningPROB) ⊆
   IMAGE f1
     (common_vars fSet (planning_prob_dom planningPROB) ∩
      needed_vars planningPROB)
img_valid_states
|- valid_inst f ⇒
   (valid_states (system_image f PROB) =
    IMAGE (state_image f) (valid_states PROB))
img_is_planning_problem
|- valid_inst f ∧ planning_problem planningPROB ⇒
   planning_problem (planning_prob_image f planningPROB)
valid_instantiations_state_images_agree
|- valid_inst f1 ∧ valid_inst f2 ∧ valid_instantiations {f1; f2} (FDOM s) ⇒
   agree (state_image f1 s) (state_image f2 s)
prob_image_init_agree
|- planning_problem planningPROB ∧ valid_inst f1 ∧ valid_inst f2 ∧
   valid_instantiations {f1; f2} (planning_prob_dom planningPROB) ⇒
   agree (planning_prob_image f1 planningPROB).I
     (planning_prob_image f2 planningPROB).I
valid_instantiations_subset_2
|- valid_instantiations fSet vs1 ∧ vs2 ⊆ vs1 ⇒ valid_instantiations fSet vs2
valid_instantiations_images_inter
|- valid_inst f1 ∧ valid_inst f2 ∧ valid_instantiations {f1; f2} vs ∧
   vs' ⊆ vs ⇒
   (IMAGE f1 vs' ∩ IMAGE f2 vs = IMAGE f2 vs' ∩ IMAGE f1 vs)
prob_image_goals_same
|- planning_problem planningPROB ∧ valid_inst f1 ∧ valid_inst f2 ∧
   valid_instantiations {f1; f2} (planning_prob_dom planningPROB) ⇒
   (DRESTRICT (planning_prob_image f1 planningPROB).G
      (planning_prob_dom (planning_prob_image f2 planningPROB)) =
    DRESTRICT (planning_prob_image f2 planningPROB).G
      (planning_prob_dom (planning_prob_image f1 planningPROB)))
state_image_drestrict
|- valid_inst f ⇒
   (state_image f (DRESTRICT s vs) = DRESTRICT (state_image f s) (IMAGE f vs))
sustainable_img
|- valid_inst f ⇒
   sustainable_vars planningPROB vs ⇒
   sustainable_vars (planning_prob_image f planningPROB) (IMAGE f vs)
sustainable_quotient_preceding_imgs
|- valid_inst f1 ∧ valid_inst f2 ∧
   valid_instantiations fSet (planning_prob_dom planningPROB) ∧
   planning_problem planningPROB ∧ f1 ∈ fSet ∧ f2 ∈ fSet ∧ f1 ≠ f2 ∧
   sustainable_vars planningPROB
     (common_vars fSet (planning_prob_dom planningPROB) ∩
      needed_vars planningPROB) ⇒
   precede (planning_prob_image f1 planningPROB)
     (planning_prob_image f2 planningPROB)
sustainable_quotient_precede_imgs_list
|- ALL_DISTINCT instList ∧ (∀inst. MEM inst instList ⇒ valid_inst inst) ∧
   valid_instantiations (set instList) (planning_prob_dom planningPROB) ∧
   planning_problem planningPROB ∧
   sustainable_vars planningPROB
     (common_vars (set instList) (planning_prob_dom planningPROB) ∩
      needed_vars planningPROB) ⇒
   precede_prob_list
     (MAP (λinst. planning_prob_image inst planningPROB) instList)
state_succ_image
|- valid_inst f ⇒
   (state_image f s1 ⊌ state_image f s2 = state_image f (s1 ⊌ s2))
submap_image
|- valid_inst f ⇒ (s1 ⊑ s2 ⇔ state_image f s1 ⊑ state_image f s2)
state_image_state_succ
|- valid_inst f ⇒
   (state_succ (state_image f s) (action_image f a) =
    state_image f (state_succ s a))
as_image_exec
|- ∀s.
     valid_inst f ⇒
     (exec_plan (state_image f s,as_image f as) =
      state_image f (exec_plan (s,as)))
system_image_valid_plans
|- valid_inst f ⇒
   (valid_plans (system_image f PROB) = IMAGE (as_image f) (valid_plans PROB))
planning_prob_image_plan
|- valid_inst f ∧ plan planningPROB as ⇒
   plan (planning_prob_image f planningPROB) (as_image f as)
getting_burried_fun_in_MAP_2
|- INJ H2 (set fList) 𝕌(:β) ⇒
   ∃h.
     (MAP (λf. g (H1 f) (H2 f)) fList =
      MAP (λy. g (H1 (h y)) y) (MAP H2 fList)) ∧
     ∀f. MEM f fList ⇒ (h (H2 f) = f)
getting_burried_fun_in_MAP
|- INJ f (set fList) 𝕌(:β) ⇒ ∃h. MAP g fList = MAP (λx. g (h x)) (MAP f fList)
IJCAI_Theorem_4_1
|- INJ (λinst. planning_prob_image inst quotientPROB) (set instList)
     𝕌(:(α, β) planningProblem) ⇒
   ∃f.
     (MAP
        (λinst.
           rem_condless_act
             (needed_asses (planning_prob_image inst quotientPROB),[],
              as_image inst quotientPlan)) instList =
      MAP
        (λplanningPROB'.
           rem_condless_act (needed_asses planningPROB',[],f planningPROB'))
        (MAP (λinst. planning_prob_image inst quotientPROB) instList)) ∧
     ∀inst.
       MEM inst instList ⇒
       (f (planning_prob_image inst quotientPROB) =
        as_image inst quotientPlan)
IJCAI_Theorem_4
|- ALL_DISTINCT instList ∧
   INJ (λinst. planning_prob_image inst quotientPROB) (set instList)
     𝕌(:(α, β) planningProblem) ∧
   (∀inst. MEM inst instList ⇒ valid_inst inst) ∧
   valid_instantiations (set instList) (planning_prob_dom quotientPROB) ∧
   planning_problem quotientPROB ∧
   sustainable_vars quotientPROB
     (common_vars (set instList) (planning_prob_dom quotientPROB) ∩
      needed_vars quotientPROB) ∧
   covers (MAP (λinst. planning_prob_image inst quotientPROB) instList)
     planningPROB ∧ plan quotientPROB quotientPlan ⇒
   plan planningPROB
     (FLAT
        (MAP
           (λinst.
              rem_condless_act
                (needed_asses (planning_prob_image inst quotientPROB),[],
                 as_image inst quotientPlan)) instList))
augmented_prob_planning_problem
|- planning_problem planningPROB ⇒
   planning_problem
     (planningPROB with
      G :=
        DRESTRICT planningPROB.I
          (common_vars (set instList) (planning_prob_dom planningPROB) ∩
           needed_vars planningPROB) ⊌ planningPROB.G)
augmented_planning_prob_dom
|- planning_problem planningPROB ⇒
   (planning_prob_dom
      (planningPROB with
       G :=
         DRESTRICT planningPROB.I
           (common_vars (set instList) (planning_prob_dom planningPROB) ∩
            needed_vars planningPROB) ⊌ planningPROB.G) =
    planning_prob_dom planningPROB)
augmented_prob_sustains_vars_2
|- let
     augmentedQuotientPROB =
       quotientPROB with
       G :=
         DRESTRICT quotientPROB.I
           (common_vars (set instList) (planning_prob_dom quotientPROB) ∩
            needed_vars quotientPROB) ⊌ quotientPROB.G
   in
     sustainable_vars augmentedQuotientPROB
       (common_vars (set instList) (planning_prob_dom augmentedQuotientPROB) ∩
        needed_vars augmentedQuotientPROB)
IJCAI_goal_augmentation_works
|- let
     augmentedQuotientPROB =
       quotientPROB with
       G :=
         DRESTRICT quotientPROB.I
           (common_vars (set instList) (planning_prob_dom quotientPROB) ∩
            needed_vars quotientPROB) ⊌ quotientPROB.G
   in
     ALL_DISTINCT instList ∧ (∀inst. MEM inst instList ⇒ valid_inst inst) ∧
     planning_problem quotientPROB ⇒
     INJ (λinst. planning_prob_image inst augmentedQuotientPROB)
       (set instList) 𝕌(:(α, β) planningProblem) ∧
     valid_instantiations (set instList)
       (planning_prob_dom augmentedQuotientPROB) ∧
     covers
       (MAP (λinst. planning_prob_image inst augmentedQuotientPROB) instList)
       planningPROB ∧ plan augmentedQuotientPROB augmentedQuotientPlan ⇒
     plan planningPROB
       (FLAT
          (MAP
             (λinst.
                rem_condless_act
                  (needed_asses
                     (planning_prob_image inst augmentedQuotientPROB),[],
                   as_image inst augmentedQuotientPlan)) instList))