- vars_change_cat
-
|- ∀s.
vars_change (as1 ⧺ as2) vs s =
vars_change as1 vs s ⧺ vars_change as2 vs (exec_plan (s,as1))
- empty_change_no_change
-
|- ∀s.
(vars_change as vs s = []) ⇒
(DRESTRICT (exec_plan (s,as)) vs = DRESTRICT s vs)
- zero_change_imp_all_effects_submap
-
|- ∀s s'.
(vars_change as vs s = []) ∧ sat_precond_as (s,as) ∧ MEM a as ∧
(DRESTRICT s vs = DRESTRICT s' vs) ⇒
DRESTRICT (SND a) vs ⊑ DRESTRICT s' vs
- zero_change_imp_all_preconds_submap
-
|- ∀s s'.
(vars_change as vs s = []) ∧ sat_precond_as (s,as) ∧ MEM a as ∧
(DRESTRICT s vs = DRESTRICT s' vs) ⇒
DRESTRICT (FST a) vs ⊑ DRESTRICT s' vs
- no_vs_change_valid_in_snapshot
-
|- as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧
(vars_change as vs s = []) ⇒
as ∈ valid_plans (snapshot PROB (DRESTRICT s vs))
- no_vs_change_snapshot_s_vs_is_valid_bound_1_1_1
-
|- FINITE PROB ∧ (vars_change as vs s = []) ∧ sat_precond_as (s,as) ∧
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (DRESTRICT s (prob_dom (snapshot PROB (DRESTRICT s vs))),as) =
exec_plan
(DRESTRICT s (prob_dom (snapshot PROB (DRESTRICT s vs))),as')) ∧
sublist as' as ∧
LENGTH as' ≤ problem_plan_bound (snapshot PROB (DRESTRICT s vs))
- no_vs_change_snapshot_s_vs_is_valid_bound_1_1
-
|- FINITE PROB ∧ (vars_change as vs s = []) ∧ sat_precond_as (s,as) ∧
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (DRESTRICT s (prob_dom (snapshot PROB (DRESTRICT s vs))),as) =
exec_plan
(DRESTRICT s (prob_dom (snapshot PROB (DRESTRICT s vs))),as')) ∧
sublist as' as ∧ sat_precond_as (s,as') ∧
LENGTH as' ≤ problem_plan_bound (snapshot PROB (DRESTRICT s vs))
- no_vs_change_snapshot_s_vs_is_valid_bound_1
-
|- FINITE PROB ∧ (vars_change as vs s = []) ∧ no_effectless_act as ∧
sat_precond_as (s,as) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(DRESTRICT (exec_plan (s,as))
(prob_dom (snapshot PROB (DRESTRICT s vs))) =
DRESTRICT (exec_plan (s,as'))
(prob_dom (snapshot PROB (DRESTRICT s vs)))) ∧ sublist as' as ∧
LENGTH as' ≤ problem_plan_bound (snapshot PROB (DRESTRICT s vs))
- no_vs_change_snapshot_s_vs_is_valid_bound
-
|- FINITE PROB ∧ (vars_change as vs s = []) ∧ no_effectless_act as ∧
sat_precond_as (s,as) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' ≤ problem_plan_bound (snapshot PROB (DRESTRICT s vs))
- snapshot_bound_leq_S
-
|- problem_plan_bound (snapshot PROB (DRESTRICT s vs)) ≤
S vs lss PROB (DRESTRICT s vs)
- S_geq_S_succ_plus_ell
-
|- s ∈ valid_states PROB ∧
top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧
s' ∈ state_successors (prob_proj (PROB,vs)) s ∧
(set lss = valid_states (prob_proj (PROB,vs))) ⇒
problem_plan_bound (snapshot PROB (DRESTRICT s vs)) +
S vs lss PROB (DRESTRICT s' vs) + 1 ≤ S vs lss PROB (DRESTRICT s vs)
- vars_change_cons
-
|- ∀s s'.
(vars_change as vs s = s'::ss) ⇒
∃as1 act as2.
(as = as1 ⧺ act::as2) ∧ (vars_change as1 vs s = []) ∧
(state_succ (exec_plan (s,as1)) act = s') ∧
(vars_change as2 vs (state_succ (exec_plan (s,as1)) act) = ss)
- vars_change_cons_2
-
|- ∀s s'. (vars_change as vs s = s'::ss) ⇒ DRESTRICT s' vs ≠ DRESTRICT s vs
- S_bound_main_lemma_1_1_1
-
|- top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧ FINITE PROB ∧
(set lss = valid_states (prob_proj (PROB,vs))) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ no_effectless_act as ∧ sat_precond_as (s,as) ⇒
∃as'.
(exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
LENGTH as' ≤ S vs lss PROB (DRESTRICT s vs)
- S_bound_main_lemma_1_1
-
|- top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧ FINITE PROB ∧
(set lss = valid_states (prob_proj (PROB,vs))) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
LENGTH as' ≤ S vs lss PROB (DRESTRICT s vs)
- S_bound_main_lemma_1
-
|- top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧ FINITE PROB ∧
(set lss = valid_states (prob_proj (PROB,vs))) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
LENGTH as' ≤
MAX_SET {S vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}
- S_bound_main_lemma
-
|- top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧ FINITE PROB ∧
(set lss = valid_states (prob_proj (PROB,vs))) ⇒
problem_plan_bound PROB ≤
MAX_SET {S vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}
- S_bound_main_lemma_1_1_thesis
-
|- FINITE PROB ∧ sspace_DAG (prob_proj (PROB,vs)) lss ∧
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
LENGTH as' ≤ S vs lss PROB (DRESTRICT s vs)
- S_bound_main_lemma_thesis
-
|- FINITE PROB ∧ sspace_DAG (prob_proj (PROB,vs)) lss ⇒
problem_plan_bound PROB ≤
MAX_SET {S vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}