- PLS_charles_def
-
|- ∀s as PROB.
PLS_charles (s,as,PROB) =
{LENGTH as' |
(exec_plan (s,as') = exec_plan (s,as)) ∧ as' ∈ valid_plans PROB}
- MPLS_charles_def
-
|- ∀PROB.
MPLS_charles PROB =
{MIN_SET (PLS_charles (s,as,PROB)) |
(s,as) |
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
- problem_plan_bound_charles_def
-
|- ∀PROB. problem_plan_bound_charles PROB = MAX_SET (MPLS_charles PROB)
- PLS_stage_1_def
-
|- ∀s as.
PLS_stage_1 (s,as) =
IMAGE LENGTH {as' | exec_plan (s,as') = exec_plan (s,as)}
- MPLS_stage_1_def
-
|- ∀PROB.
MPLS_stage_1 PROB =
IMAGE (λ(s,as). MIN_SET (PLS_stage_1 (s,as)))
{(s,as) | s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
- problem_plan_bound_stage_1_def
-
|- ∀PROB. problem_plan_bound_stage_1 PROB = MAX_SET (MPLS_stage_1 PROB)
- PLS_def
-
|- ∀s as.
PLS (s,as) =
IMAGE LENGTH
{as' | (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as}
- MPLS_def
-
|- ∀PROB.
MPLS PROB =
IMAGE (λ(s,as). MIN_SET (PLS (s,as)))
{(s,as) | s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
- problem_plan_bound_def
-
|- ∀PROB. problem_plan_bound PROB = MAX_SET (MPLS PROB)
- RD_def
-
|- ∀Pi. RD Pi = MAX_SET {LENGTH p − 1 | valid_path Pi p ∧ ALL_DISTINCT p}
- statelist'_def
-
|- (∀s. statelist' s [] = [s]) ∧
∀s a as. statelist' s (a::as) = s::statelist' (state_succ s a) as
- MPLS_s_def
-
|- ∀PROB s.
MPLS_s PROB s =
IMAGE (λ(s,as). MIN_SET (PLS (s,as))) {(s,as) | as ∈ valid_plans PROB}
- problem_plan_bound_s_def
-
|- ∀PROB s. problem_plan_bound_s PROB s = MAX_SET (MPLS_s PROB s)
- traversed_states_def
-
|- ∀s as. traversed_states (s,as) = set (state_list (s,as))
- td_def
-
|- ∀PROB.
td PROB =
MAX_SET
{CARD (traversed_states (s,as)) − 1 |
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
- bound_child_parent_lemma_s_1_1_1_1_1_1
-
|- ∀PROB as k s.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
problem_plan_bound_s PROB s ≤ k ⇒
MIN_SET (PLS (s,as)) ≤ problem_plan_bound_s PROB s
- bound_child_parent_lemma_s_1_1_1_1_1_1_1
-
|- ∀PROB as. as ∈ valid_plans PROB ⇒ MIN_SET (PLS (s,as)) ∈ MPLS_s PROB s
- expanded_problem_plan_bound_thm_1
-
|- ∀PROB.
problem_plan_bound PROB =
MAX_SET
(IMAGE (λ(s,as). MIN_SET (PLS (s,as)))
{(s,as) | s ∈ valid_states PROB ∧ as ∈ valid_plans PROB})
- expanded_problem_plan_bound_thm
-
|- ∀PROB.
problem_plan_bound PROB =
MAX_SET
{MIN_SET (PLS (s,as)) | s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
- valid_path_ind
-
|- ∀P.
(∀Pi. P Pi []) ∧ (∀Pi s. P Pi [s]) ∧
(∀Pi s1 s2 rest. P Pi (s2::rest) ⇒ P Pi (s1::s2::rest)) ⇒
∀v v1. P v v1
- valid_path_def
-
|- (∀Pi. valid_path Pi [] ⇔ T) ∧
(∀s Pi. valid_path Pi [s] ⇔ s ∈ valid_states Pi) ∧
∀s2 s1 rest Pi.
valid_path Pi (s1::s2::rest) ⇔
s1 ∈ valid_states Pi ∧ (∃a. a ∈ Pi ∧ (exec_plan (s1,[a]) = s2)) ∧
valid_path Pi (s2::rest)
- valid_path_ITP2015_def
-
|- (valid_path Pi [] ⇔ T) ∧ (valid_path Pi [s] ⇔ s ∈ valid_states Pi) ∧
(valid_path Pi (s1::s2::rest) ⇔
s1 ∈ valid_states Pi ∧ (∃a. a ∈ Pi ∧ (exec_plan (s1,[a]) = s2)) ∧
valid_path Pi (s2::rest))
- bound_main_lemma_1_1
-
|- ∀PROB s as.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃x. x ∈ PLS (s,as) ∧ x ≤ 2 ** CARD (prob_dom PROB) − 1
- bound_main_lemma_1
-
|- ∀PROB x. FINITE PROB ∧ x ∈ MPLS PROB ⇒ x ≤ 2 ** CARD (prob_dom PROB) − 1
- FINITE_MPLS
-
|- FINITE Pi ⇒ FINITE (MPLS Pi)
- LENGTH_statelist'
-
|- ∀as s. LENGTH (statelist' s as) = LENGTH as + 1
- valid_path_statelist'
-
|- ∀as s.
as ∈ valid_plans Pi ∧ s ∈ valid_states Pi ⇒
valid_path Pi (statelist' s as)
- statelist'_exec_plan
-
|- ∀as s p. (statelist' s as = p) ⇒ (exec_plan (s,as) = LAST p)
- statelist'_EQ_NIL
-
|- statelist' s as ≠ []
- statelist'_TAKE
-
|- ∀as s p.
(statelist' s as = p) ⇒
∀n. n ≤ LENGTH as ⇒ (exec_plan (s,TAKE n as) = EL n p)
- RD_bounds_sublistD
-
|- ∀Pi. FINITE Pi ⇒ problem_plan_bound Pi ≤ RD Pi
- bound_main_lemma_3
-
|- ∀PROB. FINITE PROB ⇒ MPLS PROB ≠ ∅
- bound_main_lemma
-
|- ∀PROB.
FINITE PROB ⇒ problem_plan_bound PROB ≤ 2 ** CARD (prob_dom PROB) − 1
- bound_child_parent_lemma_2_1_1
-
|- ∀P f.
(∀PROB as s.
P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ⇒
∀PROB s as.
P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃x. x ∈ PLS (s,as) ∧ x < f PROB
- bound_child_parent_lemma_2_1
-
|- ∀P f.
(∀PROB as s.
P PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ⇒
∀PROB x. P PROB ⇒ x ∈ MPLS PROB ⇒ x < f PROB
- bound_child_parent_lemma_2_1_1_finite
-
|- ∀P f.
(∀PROB as s.
P PROB ∧ FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ⇒
∀PROB s as.
P PROB ∧ FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃x. x ∈ PLS (s,as) ∧ x < f PROB
- bound_child_parent_lemma_2_1_finite
-
|- ∀P f.
(∀PROB as s.
P PROB ∧ FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ⇒
∀PROB x. P PROB ∧ FINITE PROB ⇒ x ∈ MPLS PROB ⇒ x < f PROB
- bound_child_parent_lemma_2
-
|- ∀P f.
(∀PROB as s.
P PROB ∧ FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ⇒
∀PROB. P PROB ∧ FINITE PROB ⇒ problem_plan_bound PROB < f PROB
- bound_child_parent_lemma_2_1_1_thesis
-
|- FINITE PROB ∧
(∀as s.
as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < k) ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃x. x ∈ PLS (s,as) ∧ x < k
- bound_child_parent_lemma_2_1_thesis
-
|- FINITE PROB ∧
(∀as s.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < k) ⇒
x ∈ MPLS PROB ⇒
x < k
- bound_child_parent_lemma_2_thesis'
-
|- FINITE PROB ∧
(∀as s.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < k) ⇒
problem_plan_bound PROB < k
- bound_child_parent_lemma_2_thesis
-
|- FINITE PROB ∧
(∀as s.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' ≤ k) ⇒
problem_plan_bound PROB ≤ k
- bound_child_parent_lemma_2_
-
|- ∀P f PROB.
(∀PROB' as s.
P PROB' ∧ FINITE PROB' ∧ s ∈ valid_states PROB' ∧
as ∈ valid_plans PROB' ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB') ∧ P PROB ∧ FINITE PROB ⇒
problem_plan_bound PROB < f PROB
- bound_child_parent_lemma_1_1_1_1_1_1_1
-
|- ∀PROB s as.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
MIN_SET (PLS (s,as)) ∈ MPLS PROB
- bound_child_parent_lemma_1_1_1_1_1_1
-
|- ∀PROB s as k.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
problem_plan_bound PROB ≤ k ⇒
MIN_SET (PLS (s,as)) ≤ problem_plan_bound PROB
- bound_child_parent_lemma_1_1_1_1_1_2_1
-
|- ∀s as. PLS (s,as) ≠ ∅
- bound_child_parent_lemma_1_1_1_1_1_2
-
|- ∀s as. ∃x. x ∈ PLS (s,as) ∧ (x = MIN_SET (PLS (s,as)))
- bound_child_parent_lemma_1_1_1_1_1_3
-
|- ∀x s as.
x ∈ PLS (s,as) ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ (LENGTH as' = x) ∧
sublist as' as
- bound_child_parent_lemma_1_1_1_1_1
-
|- ∀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' ≤ problem_plan_bound PROB
- bound_main_lemma_s_3
-
|- ∀PROB s. MPLS_s PROB s ≠ ∅
- bound_child_parent_lemma_s_2_1_1
-
|- ∀P f.
(∀PROB as s.
FINITE PROB ∧ P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB s) ⇒
∀PROB s as.
FINITE PROB ∧ P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃x. x ∈ PLS (s,as) ∧ x < f PROB s
- bound_child_parent_lemma_s_2_1
-
|- ∀P f.
(∀PROB as s.
FINITE PROB ∧ P PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB s) ⇒
∀PROB x s.
FINITE PROB ∧ P PROB ∧ s ∈ valid_states PROB ⇒
x ∈ MPLS_s PROB s ⇒
x < f PROB s
- bound_child_parent_lemma_s_2
-
|- ∀PROB s P f.
(∀PROB as s.
FINITE PROB ∧ P PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB s) ⇒
FINITE PROB ∧ P PROB ∧ s ∈ valid_states PROB ⇒
problem_plan_bound_s PROB s < f PROB s
- bound_main_lemma_reachability_s
-
|- ∀PROB s.
FINITE PROB ∧ s ∈ valid_states PROB ⇒
problem_plan_bound_s PROB s < CARD (reachable_s PROB s)
- problem_plan_bound_s_LESS_EQ_problem_plan_bound_thm
-
|- ∀PROB s.
FINITE PROB ∧ s ∈ valid_states PROB ⇒
problem_plan_bound_s PROB s < problem_plan_bound PROB + 1
- bound_main_lemma_s_1
-
|- ∀PROB x s.
FINITE PROB ∧ s ∈ valid_states PROB ⇒
x ∈ MPLS_s PROB s ⇒
x ≤ 2 ** CARD (prob_dom PROB) − 1
- bound_main_lemma_s
-
|- ∀PROB s.
FINITE PROB ∧ s ∈ valid_states PROB ⇒
problem_plan_bound_s PROB s ≤ 2 ** CARD (prob_dom PROB) − 1
- bound_child_parent_lemma_s_1_1_1_1_1
-
|- ∀PROB as s.
FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' ≤ problem_plan_bound_s PROB s
- PLS_def_ITP2015
-
|- ∀s as.
PLS (s,as) =
{LENGTH as' | (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as}
- expanded_problem_plan_bound_charles_thm
-
|- ∀PROB.
problem_plan_bound_charles PROB =
MAX_SET
{MIN_SET (PLS_charles (s,as,PROB)) |
(s,as) |
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
- bound_main_lemma_charles_3
-
|- ∀PROB. FINITE PROB ⇒ MPLS_charles PROB ≠ ∅
- bound_main_lemma_charles_1_1
-
|- ∀PROB s as.
FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃x. x ∈ PLS_charles (s,as,PROB) ∧ x ≤ 2 ** CARD (prob_dom PROB) − 1
- bound_main_lemma_charles_1
-
|- ∀PROB x.
FINITE PROB ⇒ x ∈ MPLS_charles PROB ⇒ x ≤ 2 ** CARD (prob_dom PROB) − 1
- bound_main_lemma_charles
-
|- ∀PROB.
FINITE PROB ⇒
problem_plan_bound_charles PROB ≤ 2 ** CARD (prob_dom PROB) − 1
- bound_child_parent_lemma_charles_2_1_1
-
|- ∀P f.
(∀PROB as s.
P PROB ∧ FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ⇒
∀PROB s as.
P PROB ∧ FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
∃x. x ∈ PLS_charles (s,as,PROB) ∧ x < f PROB
- bound_child_parent_lemma_charles_2_1
-
|- ∀P f.
(∀PROB as s.
P PROB ∧ FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ⇒
∀PROB x. P PROB ∧ FINITE PROB ⇒ x ∈ MPLS_charles PROB ⇒ x < f PROB
- bound_child_parent_lemma_charles_2
-
|- ∀P f.
(∀PROB as s.
P PROB ∧ FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ⇒
∀PROB. P PROB ∧ FINITE PROB ⇒ problem_plan_bound_charles PROB < f PROB
- sublistD_bounds_D
-
|- ∀PROB.
FINITE PROB ⇒ problem_plan_bound_charles PROB ≤ problem_plan_bound PROB
- sublistD_bounds_D_and_RD_bounds_sublistD
-
|- ∀PROB.
FINITE PROB ⇒
problem_plan_bound_charles PROB ≤ problem_plan_bound PROB ∧
problem_plan_bound PROB ≤ RD PROB
- empty_problem_bound
-
|- ∀PROB. (prob_dom PROB = ∅) ⇒ (problem_plan_bound PROB = 0)
- temp
-
|- (∀x. ∃x'. (rd x = ell x') ∧ (rd x = rd x')) ⇒
(∀x. P x (ell x)) ⇒
∃x'. (rd x = rd x') ∧ P x' (rd x')
- bound_child_parent_lemma_1_1_1_1_1'
-
|- ∀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' ≤ problem_plan_bound PROB ∧ sat_precond_as (s,as')
- problem_plan_bound_UBound
-
|- (∀as s.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
∃as'.
(exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
LENGTH as' < f PROB) ∧ FINITE PROB ⇒
problem_plan_bound PROB < f PROB
- finite_traversed_states
-
|- FINITE (traversed_states (s,as))
- traversed_states_nempty
-
|- traversed_states (s,as) ≠ ∅
- traversed_states_geq_1
-
|- ∀s as. 1 ≤ CARD (traversed_states (s,as))
- init_is_traversed
-
|- s ∈ traversed_states (s,as)
- traversed_states_rem_condless_act
-
|- ∀s.
traversed_states (s,rem_condless_act (s,[],as)) = traversed_states (s,as)
- td_UBound
-
|- FINITE PROB ∧
(∀s as.
sat_precond_as (s,as) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
CARD (traversed_states (s,as)) ≤ k) ⇒
td PROB ≤ k − 1