- graph_plan_lemma_22_4_1
-
|- as ∈ valid_plans PROB ⇒ FILTER P as ∈ valid_plans PROB
- graph_plan_lemma_10_2
-
|- ∀a. a ∈ PROB ⇒ action_dom a ⊆ prob_dom PROB
- graph_plan_lemma_16_1_1
-
|- ∀s a. (FDOM (SND a) = ∅) ⇒ (state_succ s a = s)
- graph_plan_lemma_4_1
-
|- ∀s s' vs a a'.
(DRESTRICT s vs = DRESTRICT s' vs) ∧ (FST a ⊑ s ⇔ FST a' ⊑ s') ∧
(DRESTRICT (SND a) vs = DRESTRICT (SND a') vs) ⇒
(DRESTRICT (state_succ s a) vs = DRESTRICT (state_succ s' a') vs)
- graph_plan_lemma_12_3
-
|- ∀s a vs.
(FDOM (DRESTRICT (SND a) vs) = ∅) ⇒
(DRESTRICT (state_succ s a) vs = DRESTRICT s vs)
- no_change_vs_eff_submap
-
|- ∀a vs s.
(DRESTRICT s vs = DRESTRICT (state_succ s a) vs) ∧ FST a ⊑ s ⇒
DRESTRICT (SND a) vs ⊑ DRESTRICT s vs
- graph_plan_lemma_1_2
-
|- ∀a vs s.
DISJOINT (FDOM (SND a)) vs ⇒
(DRESTRICT s vs = DRESTRICT (state_succ s a) vs)
- empty_prob_dom_finite
-
|- (prob_dom PROB = ∅) ⇒ FINITE PROB
- empty_prob_dom
-
|- (prob_dom PROB = ∅) ⇒ (PROB = {(FEMPTY,FEMPTY)}) ∨ (PROB = ∅)
- empty_prob_dom_imp_empty_plan_always_good
-
|- ∀PROB s.
(prob_dom PROB = ∅) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
(exec_plan (s,[]) = exec_plan (s,as))
- empty_prob_dom_single_val_state
-
|- (prob_dom PROB = ∅) ⇒ ∃s. valid_states PROB = {s}
- valid_states_nempty
-
|- FINITE PROB ⇒ ∃s. s ∈ valid_states PROB
- valid_plan_mems
-
|- as ∈ valid_plans PROB ∧ MEM a as ⇒ a ∈ PROB
- valid_as_submap_init_submap_exec
-
|- ∀s1 s2.
s1 ⊑ s2 ∧ (∀a. MEM a as ⇒ FDOM (FST a) ⊆ FDOM s1) ⇒
exec_plan (s1,as) ⊑ exec_plan (s2,as)
- pred_dom_subset_succ_submap
-
|- ∀a s1 s2.
FDOM (FST a) ⊆ FDOM s1 ∧ s1 ⊑ s2 ⇒ state_succ s1 a ⊑ state_succ s2 a
- parent_children_lemma_1_1_1_10_1_1
-
|- ∀a s1 s2. FST a ⊑ s1 ∧ s1 ⊑ s2 ⇒ state_succ s1 a ⊑ state_succ s2 a
- action_dom_pair
-
|- action_dom a = FDOM (FST a) ∪ FDOM (SND a)
- state_succ_pair
-
|- state_succ s (p,e) = if p ⊑ s then e ⊌ s else s
- exec_plan_ind
-
|- ∀P.
(∀s a as. P (state_succ s a,as) ⇒ P (s,a::as)) ∧ (∀s. P (s,[])) ⇒
∀v v1. P (v,v1)
- exec_plan_def
-
|- (∀s as a. exec_plan (s,a::as) = exec_plan (state_succ s a,as)) ∧
∀s. exec_plan (s,[]) = s
- exec_plan_Append
-
|- ∀as_a as_b s.
exec_plan (s,as_a ⧺ as_b) = exec_plan (exec_plan (s,as_a),as_b)
- cycle_removal_lemma
-
|- ∀s as1 as2 as3.
(exec_plan (s,as1 ⧺ as2) = exec_plan (s,as1)) ⇒
(exec_plan (s,as1 ⧺ as2 ⧺ as3) = exec_plan (s,as1 ⧺ as3))
- construction_of_all_possible_states_lemma
-
|- ∀e X.
e ∉ X ⇒
({s | FDOM s = e INSERT X} =
IMAGE (λs. s |+ (e,T)) {s | FDOM s = X} ∪
IMAGE (λs. s |+ (e,F)) {s | FDOM s = X})
- FINITE_states
-
|- ∀X. FINITE X ⇒ FINITE {s | FDOM s = X}
- card_of_set_of_all_possible_states
-
|- ∀X. FINITE X ⇒ (CARD {s | FDOM s = X} = 2 ** CARD X)
- state_list_ind
-
|- ∀P.
(∀s a as. P (state_succ s a,as) ⇒ P (s,a::as)) ∧ (∀s. P (s,[])) ⇒
∀v v1. P (v,v1)
- state_list_def
-
|- (∀s as a. state_list (s,a::as) = s::state_list (state_succ s a,as)) ∧
∀s. state_list (s,[]) = [s]
- empty_state_list_lemma
-
|- ∀as s. [] ≠ state_list (s,as)
- state_list_length_non_zero
-
|- ∀as s. 0 ≠ LENGTH (state_list (s,as))
- state_list_length_lemma
-
|- ∀as s. LENGTH as = LENGTH (state_list (s,as)) − 1
- state_list_length_lemma_2
-
|- ∀as s. LENGTH (state_list (s,as)) = LENGTH as + 1
- state_set_thm
-
|- ∀s1. s1 ∈ state_set s2 ⇔ s1 ≼ s2 ∧ s1 ≠ []
- state_set_finite
-
|- ∀X. FINITE (state_set X)
- LENGTH_state_set
-
|- ∀X e. e ∈ state_set X ⇒ LENGTH e ≤ LENGTH X
- lemma_temp
-
|- ∀x s as h.
x ∈ state_set (state_list (s,as)) ⇒
LENGTH (h::state_list (s,as)) > LENGTH x
- NIL_NOTIN_stateset
-
|- ∀X. [] ∉ state_set X
- state_set_card
-
|- ∀X. CARD (state_set X) = LENGTH X
- FDOM_state_succ
-
|- FDOM (SND a) ⊆ FDOM s ⇒ (FDOM (state_succ s a) = FDOM s)
- FDOM_state_succ_subset
-
|- FDOM (state_succ s a) ⊆ FDOM s ∪ FDOM (SND a)
- FDOM_eff_subset_FDOM_valid_states
-
|- ∀p e s. (p,e) ∈ PROB ∧ s ∈ valid_states PROB ⇒ FDOM e ⊆ FDOM s
- FDOM_eff_subset_FDOM_valid_states_pair
-
|- ∀a s. a ∈ PROB ∧ s ∈ valid_states PROB ⇒ FDOM (SND a) ⊆ FDOM s
- FDOM_pre_subset_FDOM_valid_states
-
|- ∀p e s. (p,e) ∈ PROB ∧ s ∈ valid_states PROB ⇒ FDOM p ⊆ FDOM s
- FDOM_pre_subset_FDOM_valid_states_pair
-
|- ∀a s. a ∈ PROB ∧ s ∈ valid_states PROB ⇒ FDOM (FST a) ⊆ FDOM s
- action_dom_subset_valid_states_FDOM
-
|- ∀p e s. (p,e) ∈ PROB ∧ s ∈ valid_states PROB ⇒ action_dom (p,e) ⊆ FDOM s
- FDOM_eff_subset_prob_dom
-
|- ∀p e. (p,e) ∈ PROB ⇒ FDOM e ⊆ prob_dom PROB
- FDOM_eff_subset_prob_dom_pair
-
|- ∀a. a ∈ PROB ⇒ FDOM (SND a) ⊆ prob_dom PROB
- FDOM_pre_subset_prob_dom
-
|- ∀p e. (p,e) ∈ PROB ⇒ FDOM p ⊆ prob_dom PROB
- FDOM_pre_subset_prob_dom_pair
-
|- ∀a. a ∈ PROB ⇒ FDOM (FST a) ⊆ prob_dom PROB
- valid_plan_valid_head
-
|- h::as ∈ valid_plans PROB ⇒ h ∈ PROB
- valid_plan_valid_tail
-
|- h::as ∈ valid_plans PROB ⇒ as ∈ valid_plans PROB
- valid_plan_pre_subset_prob_dom_pair
-
|- as ∈ valid_plans PROB ⇒ ∀a. MEM a as ⇒ FDOM (FST a) ⊆ prob_dom PROB
- valid_append_valid_suff
-
|- as1 ⧺ as2 ∈ valid_plans PROB ⇒ as2 ∈ valid_plans PROB
- valid_append_valid_pref
-
|- as1 ⧺ as2 ∈ valid_plans PROB ⇒ as1 ∈ valid_plans PROB
- valid_pref_suff_valid_append
-
|- as1 ∈ valid_plans PROB ∧ as2 ∈ valid_plans PROB ⇒
as1 ⧺ as2 ∈ valid_plans PROB
- MEM_statelist_FDOM
-
|- ∀PROB h as s0.
s0 ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
MEM h (state_list (s0,as)) ⇒
h ∈ valid_states PROB
- lemma_1
-
|- ∀as PROB.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
IMAGE LAST (state_set (state_list (s,as))) ⊆ valid_states PROB
- lemma_2_1_1_1
-
|- ∀as x PROB.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ as ≠ [] ⇒
x ∈ state_set (state_list (s,as)) ⇒
LENGTH x ≤ SUC (LENGTH as)
- lemma_2_1_1
-
|- ∀as s h.
CARD (state_set (state_list (s,h::as))) =
SUC (CARD (state_set (state_list (state_succ s h,as))))
- lemma_2_1
-
|- ∀as s. SUC (LENGTH as) = CARD (state_set (state_list (s,as)))
- lemma_2_2_1
-
|- ∀as x y s.
x ∈ state_set (state_list (s,as)) ∧ y ∈ state_set (state_list (s,as)) ∧
x ≠ y ⇒
LENGTH x ≠ LENGTH y
- lemma_2_2
-
|- ∀as PROB s.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
¬INJ LAST (state_set (state_list (s,as))) (valid_states PROB) ⇒
∃slist_1 slist_2.
slist_1 ∈ state_set (state_list (s,as)) ∧
slist_2 ∈ state_set (state_list (s,as)) ∧
(LAST slist_1 = LAST slist_2) ∧ LENGTH slist_1 ≠ LENGTH slist_2
- lemma_2_3_1_1
-
|- ∀sl. [] ∉ state_set sl
- lemma_2_3_1_2_1
-
|- ∀sl. sl ≠ [] ⇒ sl ∈ state_set sl
- lemma_2_3_1_2
-
|- ∀s slist h t.
slist ≠ [] ∧ s::slist ∈ state_set (state_list (s,h::t)) ⇒
slist ∈ state_set (state_list (state_succ s h,t))
- valid_action_valid_succ
-
|- h ∈ PROB ∧ s ∈ valid_states PROB ⇒ state_succ s h ∈ valid_states PROB
- lemma_2_3_1_thm
-
|- ∀slist as PROB s.
as ≠ [] ∧ slist ≠ [] ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
slist ∈ state_set (state_list (s,as)) ⇒
∃as'.
as' ≼ as ∧ (exec_plan (s,as') = LAST slist) ∧
(LENGTH slist = SUC (LENGTH as'))
- FINITE_prob_dom
-
|- FINITE PROB ⇒ FINITE (prob_dom PROB)
- CARD_valid_states
-
|- FINITE PROB ⇒ (CARD (valid_states PROB) = 2 ** CARD (prob_dom PROB))
- FINITE_valid_states
-
|- FINITE PROB ⇒ FINITE (valid_states PROB)
- lemma_2
-
|- ∀PROB as s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
LENGTH as > 2 ** CARD (FDOM s) − 1 ⇒
∃as1 as2 as3.
(as1 ⧺ as2 ⧺ as3 = as) ∧
(exec_plan (s,as1 ⧺ as2) = exec_plan (s,as1)) ∧ as2 ≠ []
- lemma_2_prob_dom
-
|- ∀PROB as s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
LENGTH as > 2 ** CARD (prob_dom PROB) − 1 ⇒
∃as1 as2 as3.
(as1 ⧺ as2 ⧺ as3 = as) ∧
(exec_plan (s,as1 ⧺ as2) = exec_plan (s,as1)) ∧ as2 ≠ []
- lemma_3
-
|- ∀as PROB s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
LENGTH as > 2 ** CARD (prob_dom PROB) − 1 ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ LENGTH as' < LENGTH as ∧
sublist as' as
- sublist_valid_is_valid
-
|- ∀as' as PROB.
as ∈ valid_plans PROB ∧ sublist as' as ⇒ as' ∈ valid_plans PROB
- main_lemma
-
|- ∀PROB as s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' ≤ 2 ** CARD (prob_dom PROB) − 1
- graph_plan_lemma_6_1
-
|- ∀as s PROB.
as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
exec_plan (s,as) ∈ valid_states PROB
- exec_plan_fdom_subset
-
|- ∀as s PROB.
as ∈ valid_plans PROB ⇒ FDOM (exec_plan (s,as)) ⊆ FDOM s ∪ prob_dom PROB
- reachable_s_finite_thm_1
-
|- s ∈ valid_states PROB ⇒ reachable_s PROB s ⊆ valid_states PROB
- reachable_s_finite_thm
-
|- ∀s. FINITE PROB ∧ s ∈ valid_states PROB ⇒ FINITE (reachable_s PROB s)
- empty_plan_is_valid
-
|- [] ∈ valid_plans PROB
- valid_head_and_tail_valid_plan
-
|- h ∈ PROB ∧ as ∈ valid_plans PROB ⇒ h::as ∈ valid_plans PROB
- lemma_1_reachability_s
-
|- ∀PROB s as.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
IMAGE LAST (state_set (state_list (s,as))) ⊆ reachable_s PROB s
- lemma_2_2_reachability_s
-
|- ∀as PROB s.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
¬INJ LAST (state_set (state_list (s,as))) (reachable_s PROB s) ⇒
∃slist_1 slist_2.
slist_1 ∈ state_set (state_list (s,as)) ∧
slist_2 ∈ state_set (state_list (s,as)) ∧
(LAST slist_1 = LAST slist_2) ∧ LENGTH slist_1 ≠ LENGTH slist_2
- lemma_2_reachability_s
-
|- ∀PROB as s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
LENGTH as > CARD (reachable_s PROB s) − 1 ⇒
∃as1 as2 as3.
(as1 ⧺ as2 ⧺ as3 = as) ∧
(exec_plan (s,as1 ⧺ as2) = exec_plan (s,as1)) ∧ as2 ≠ []
- lemma_3_reachability_s
-
|- ∀as PROB s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
LENGTH as > CARD (reachable_s PROB s) − 1 ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ LENGTH as' < LENGTH as ∧
sublist as' as
- main_lemma_reachability_s
-
|- ∀PROB as s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' ≤ CARD (reachable_s PROB s) − 1
- reachable_s_non_empty
-
|- reachable_s PROB s ≠ ∅
- card_reachable_s_non_zero
-
|- ∀s. FINITE PROB ∧ s ∈ valid_states PROB ⇒ 0 < CARD (reachable_s PROB s)
- exec_fdom_empty_prob
-
|- ∀s.
(prob_dom PROB = ∅) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
(exec_plan (s,as) = FEMPTY)
- reachable_s_empty_prob
-
|- ∀PROB s.
(prob_dom PROB = ∅) ∧ s ∈ valid_states PROB ⇒
reachable_s PROB s ⊆ {FEMPTY}
- sublist_valid_plan
-
|- sublist as' as ∧ as ∈ valid_plans PROB ⇒ as' ∈ valid_plans PROB
- prob_subset_dom_subset
-
|- PROB1 ⊆ PROB2 ⇒ prob_dom PROB1 ⊆ prob_dom PROB2
- state_succ_valid_act_disjoint
-
|- a ∈ PROB ∧ DISJOINT vs (prob_dom PROB) ⇒
(DRESTRICT (state_succ s a) vs = DRESTRICT s vs)
- exec_valid_as_disjoint
-
|- ∀s.
DISJOINT vs (prob_dom PROB) ∧ as ∈ valid_plans PROB ⇒
(DRESTRICT (exec_plan (s,as)) vs = DRESTRICT s vs)
- EQ_SS_DOM
-
|- ss ≠ ∅ ∧ stateSpace ss vs1 ∧ stateSpace ss vs2 ⇒ (vs1 = vs2)
- FINITE_SS
-
|- ∀ss. ss ≠ ∅ ∧ stateSpace ss dom ⇒ FINITE ss
- disjoint_effects_no_effects
-
|- ∀s.
(∀a. MEM a as ⇒ (FDOM (DRESTRICT (SND a) vs) = ∅)) ⇒
(DRESTRICT (exec_plan (s,as)) vs = DRESTRICT s vs)
- act_needed_asses_submap_succ_submap
-
|- ∀a s1 s2.
action_needed_asses a s2 ⊑ action_needed_asses a s1 ∧ s1 ⊑ s2 ⇒
state_succ s1 a ⊑ state_succ s2 a
- as_needed_asses_submap_exec
-
|- ∀s1 s2.
s1 ⊑ s2 ∧
(∀a. MEM a as ⇒ action_needed_asses a s2 ⊑ action_needed_asses a s1) ⇒
exec_plan (s1,as) ⊑ exec_plan (s2,as)
- action_needed_vars_subset_sys_needed_vars_subset
-
|- a ∈ PROB ⇒ action_needed_vars a s ⊆ system_needed_vars PROB s
- action_needed_asses_submap_sys_needed_asses
-
|- a ∈ PROB ⇒ action_needed_asses a s ⊑ system_needed_asses PROB s
- system_needed_asses_include_action_needed_asses_1
-
|- a ∈ PROB ⇒
(action_needed_vars a (DRESTRICT s (system_needed_vars PROB s)) =
action_needed_vars a s)
- system_needed_asses_include_action_needed_asses
-
|- a ∈ PROB ⇒
(action_needed_asses a (system_needed_asses PROB s) =
action_needed_asses a s)
- system_needed_asses_submap
-
|- system_needed_asses PROB s ⊑ s
- as_works_from_system_needed_asses
-
|- as ∈ valid_plans PROB ⇒
exec_plan (system_needed_asses PROB s,as) ⊑ exec_plan (s,as)