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