- N_gen_is_wighted_longest_path
-
|- ∀vs.
N_gen b PROB vs lvs =
wlp (λvs1 vs2. dep_var_set (PROB,vs1,vs2)) (λvs. b (prob_proj (PROB,vs)))
$+ $* vs lvs
- N_gen_valid_thm_1
-
|- ∀b.
(∀PROB'. problem_plan_bound PROB' ≤ b PROB') ⇒
∀lvs vs. N (PROB,vs,lvs) ≤ N_gen b PROB vs lvs
- N_gen_valid_thm
-
|- ∀b.
(∀PROB'. problem_plan_bound PROB' ≤ b PROB') ⇒
∀lvs.
ALL_DISTINCT lvs ∧ disjoint_varset lvs ⇒
∀PROB.
FINITE PROB ∧ (prob_dom PROB = BIGUNION (set lvs)) ∧
top_sorted (PROB,lvs) ⇒
problem_plan_bound PROB <
SUM (MAP (λvs. N_gen b PROB vs lvs) lvs) + 1
- N_super_gen_valid_thm_1
-
|- ∀b P.
(∀PROB'. P PROB' ⇒ problem_plan_bound PROB' ≤ b PROB') ∧
(∀PROB' vs'.
vs' ∩ prob_dom PROB' ≠ ∅ ∧ P PROB' ⇒ P (prob_proj (PROB',vs'))) ⇒
∀PROB lvs vs.
P PROB ∧ vs ∩ prob_dom PROB ≠ ∅ ∧
EVERY (λvs. vs ∩ prob_dom PROB ≠ ∅) lvs ⇒
N (PROB,vs,lvs) ≤ N_gen b PROB vs lvs
- N_super_gen_valid_thm
-
|- ∀b P.
(∀PROB'. P PROB' ⇒ problem_plan_bound PROB' ≤ b PROB') ∧
(∀PROB' vs'.
vs' ∩ prob_dom PROB' ≠ ∅ ∧ P PROB' ⇒ P (prob_proj (PROB',vs'))) ⇒
∀lvs.
ALL_DISTINCT lvs ∧ disjoint_varset lvs ∧ lvs ≠ [] ⇒
∀PROB.
P PROB ∧ FINITE PROB ∧ (prob_dom PROB = BIGUNION (set lvs)) ∧
top_sorted (PROB,lvs) ∧ EVERY (λvs. vs ∩ prob_dom PROB ≠ ∅) lvs ⇒
problem_plan_bound PROB <
SUM (MAP (λvs. N_gen b PROB vs lvs) lvs) + 1
- N_more_gen_valid_thm_1
-
|- ∀vs.
problem_plan_bound (prob_proj (PROB,vs)) ≤ b (prob_proj (PROB,vs)) ∧
(∀vs'.
MEM vs' lvs ⇒
problem_plan_bound (prob_proj (PROB,vs')) ≤
b (prob_proj (PROB,vs'))) ⇒
N_curried PROB lvs vs ≤ N_gen b PROB vs lvs
- N_more_gen_valid_thm
-
|- (∀vs'.
MEM vs' lvs ⇒
problem_plan_bound (prob_proj (PROB,vs')) ≤ b (prob_proj (PROB,vs'))) ∧
FINITE PROB ∧ dep_DAG PROB lvs ⇒
problem_plan_bound PROB ≤ SUM (MAP (λvs. N_gen b PROB vs lvs) lvs)
- N_gen_eq
-
|- ∀b1 b2 PROB vs lvs.
(∀x. FINITE x ⇒ (b1 x = b2 x)) ∧ FINITE PROB ⇒
(N_gen b1 PROB vs lvs = N_gen b2 PROB vs lvs)
- N_gen_empty
-
|- (∀PROB'. b (prob_proj (PROB',∅)) = 0) ⇒ (N_gen b PROB ∅ lvs = 0)
- N_gen_def_ITP2015
-
|- (∀PROB'. b (prob_proj (PROB',∅)) = 0) ⇒
∀PROB vs lvs.
top_sorted (PROB,lvs) ⇒
(N_gen b PROB vs lvs =
b (prob_proj (PROB,vs)) *
(SUM (MAP (λvs'. N_gen b PROB vs' lvs) (children (PROB,vs,lvs))) + 1))
- N_curried_more_gen_valid_thm
-
|- (∀vs'.
MEM vs' lvs ⇒
problem_plan_bound (prob_proj (PROB,vs')) ≤ b (prob_proj (PROB,vs'))) ∧
FINITE PROB ∧ dep_DAG PROB lvs ⇒
problem_plan_bound PROB ≤ SUM (MAP (N_gen_curried b PROB lvs) lvs)
- N_gen_curried_valid_thm
-
|- ∀b.
(∀PROB'. problem_plan_bound PROB' ≤ b PROB') ∧ FINITE PROB ∧
dep_DAG PROB lvs ⇒
problem_plan_bound PROB ≤
SUM (MAP (λvs. N_gen_curried b PROB lvs vs) lvs)
- N_gen_curried_is_wighted_longest_path
-
|- ∀vs.
N_gen_curried b PROB lvs vs =
wlp (λvs1 vs2. dep_var_set (PROB,vs1,vs2)) (λvs. b (prob_proj (PROB,vs)))
$+ $* vs lvs
- N_gen_curried_CONG
-
|- ∀PROB1 PROB2 lvs1 lvs2 vs1 vs2 b1 b2.
(PROB1 = PROB2) ∧ (lvs1 = lvs2) ∧ (vs1 = vs2) ∧
(b1 (prob_proj (PROB1,vs1)) = b2 (prob_proj (PROB2,vs2))) ∧
(∀vs.
MEM vs lvs2 ⇒
(b1 (prob_proj (PROB1,vs)) = b2 (prob_proj (PROB2,vs)))) ⇒
(N_gen_curried b1 PROB1 lvs1 vs1 = N_gen_curried b2 PROB2 lvs2 vs2)
- N_gen_curried_def_ITP2015
-
|- (∀PROB'. b (prob_proj (PROB',∅)) = 0) ⇒
∀PROB vs lvs.
top_sorted_curried PROB lvs ⇒
(N_gen_curried b PROB lvs vs =
b (prob_proj (PROB,vs)) *
(SUM (MAP (N_gen_curried b PROB lvs) (children_curried PROB lvs vs)) +
1))
- hybrid_algorithm_valid
-
|- FINITE PROB ∧ ALL_DISTINCT (f1 PROB) ∧ disjoint_varset (f1 PROB) ∧
(prob_dom PROB = BIGUNION (set (f1 PROB))) ∧
top_sorted_curried PROB (f1 PROB) ∧
(∀vs lss.
(vs,lss) ∈ f2 PROB ⇒
top_sorted_abs (state_successors (prob_proj (PROB,vs))) lss ∧
(set lss = valid_states (prob_proj (PROB,vs)))) ⇒
problem_plan_bound PROB ≤ hybrid_algo f1 f2 PROB
- hybrid_algorithm_valid_thesis
-
|- FINITE PROB ∧ dep_DAG PROB (f1 PROB) ∧
(∀vs lss. (vs,lss) ∈ f2 PROB ⇒ sspace_DAG (prob_proj (PROB,vs)) lss) ⇒
problem_plan_bound PROB ≤ hybrid_algo f1 f2 PROB
- S_gen_ell_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_gen problem_plan_bound vs lss PROB (DRESTRICT s vs)
- S_gen_ell_bound_main_lemma
-
|- FINITE PROB ∧ sspace_DAG (prob_proj (PROB,vs)) lss ⇒
problem_plan_bound PROB ≤
MAX_SET
{S_gen problem_plan_bound vs lss PROB s' |
s' |
s' ∈ valid_states (prob_proj (PROB,vs))}
- S_gen_bound_main_lemma_1
-
|- FINITE PROB ∧ (set lss = valid_states (prob_proj (PROB,vs))) ∧
(∀s.
MEM s lss ⇒
problem_plan_bound (snapshot PROB s) ≤ b (snapshot PROB s)) ⇒
MAX_SET
{S_gen problem_plan_bound vs lss PROB s' |
s' |
s' ∈ valid_states (prob_proj (PROB,vs))} ≤
MAX_SET
{S_gen b vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}
- S_gen_bound_main_lemma
-
|- FINITE PROB ∧ sspace_DAG (prob_proj (PROB,vs)) lss ∧
(∀s.
MEM s lss ⇒
problem_plan_bound (snapshot PROB s) ≤ b (snapshot PROB s)) ⇒
problem_plan_bound PROB ≤
MAX_SET
{S_gen b vs lss PROB s' | s' | s' ∈ valid_states (prob_proj (PROB,vs))}
- parent_children_main_lemma_N_gen_curried_thesis
-
|- ∀lvs PROB.
FINITE PROB ∧ dep_DAG PROB lvs ⇒
problem_plan_bound PROB <
SUM (MAP (N_gen_curried problem_plan_bound PROB lvs) lvs) + 1
- termination_goal_1_1
-
|- ∀PROB f1 x projPROB.
(∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB) ∧ MEM x (f1 PROB) ∧
FINITE PROB ∧
(∃vs. MEM vs (f1 PROB) ∧ (projPROB = prob_proj (PROB,vs))) ⇒
CARD (prob_dom projPROB) < CARD (prob_dom PROB)
- termination_goal_1
-
|- ∀f1 PROB x projPROB.
FINITE PROB ∧ (∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB) ∧
MEM x (f1 PROB) ∧
(∃vs. MEM vs (f1 PROB) ∧ (projPROB = prob_proj (PROB,vs))) ⇒
CARD projPROB + CARD (prob_dom projPROB) <
CARD PROB + CARD (prob_dom PROB)
- termination_goal_2
-
|- ∀f2 f1 PROB p_1 p_2 snapshotPROB.
FINITE PROB ∧ (∃vs. MEM vs (f1 PROB) ∧ ¬(vs ⊂ prob_dom PROB)) ∧
(f2 PROB ≠ ∅ ∧
∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB) ∧
((p_1,p_2) = CHOICE (f2 PROB)) ∧
(∃s. MEM s p_2 ∧ (snapshotPROB = snapshot PROB s)) ⇒
CARD snapshotPROB + CARD (prob_dom snapshotPROB) <
CARD PROB + CARD (prob_dom PROB)
- hybrid_algo_gen_ind
-
|- ∀P.
(∀f1 f2 PROB.
(∀vs lss snapshotPROB.
FINITE PROB ∧ ¬(∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB) ∧
(f2 PROB ≠ ∅ ∧
∀vs lss s.
(vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB) ∧
((vs,lss) = CHOICE (f2 PROB)) ∧
(∃s. MEM s lss ∧ (snapshotPROB = snapshot PROB s)) ⇒
P f1 f2 snapshotPROB) ∧
(∀lvs x projPROB.
FINITE PROB ∧ (∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB) ∧
(lvs = f1 PROB) ∧ MEM x lvs ∧
(∃vs. MEM vs lvs ∧ (projPROB = prob_proj (PROB,vs))) ⇒
P f1 f2 projPROB) ⇒
P f1 f2 PROB) ⇒
∀v v1 v2. P v v1 v2
- hybrid_algo_gen_def
-
|- ∀f2 f1 PROB.
hybrid_algo_gen f1 f2 PROB =
if FINITE PROB then
if ∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB then
(let
lvs = f1 PROB
in
SUM
(MAP
(N_gen_curried
(λprojPROB.
if
∃vs. MEM vs lvs ∧ (projPROB = prob_proj (PROB,vs))
then
hybrid_algo_gen f1 f2 projPROB
else 0) PROB lvs) lvs))
else if
f2 PROB ≠ ∅ ∧
∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB
then
(let
(vs,lss) = CHOICE (f2 PROB)
in
MAX_SET
{S_gen
(λsnapshotPROB.
if ∃s. MEM s lss ∧ (snapshotPROB = snapshot PROB s) then
hybrid_algo_gen f1 f2 snapshotPROB
else 0) vs lss PROB s' |
s' |
s' ∈ valid_states (prob_proj (PROB,vs))})
else problem_plan_bound PROB
else 0
- FINITE_PROB_hybrid_algo_gen_def
-
|- FINITE PROB ⇒
(hybrid_algo_gen f1 f2 PROB =
if ∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB then
(let
lvs = f1 PROB
in
SUM
(MAP
(N_gen_curried
(λprojPROB.
if ∃vs. MEM vs lvs ∧ (projPROB = prob_proj (PROB,vs)) then
hybrid_algo_gen f1 f2 projPROB
else 0) PROB lvs) lvs))
else if
f2 PROB ≠ ∅ ∧
∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB
then
(let
(vs,lss) = CHOICE (f2 PROB)
in
MAX_SET
{S_gen
(λsnapshotPROB.
if ∃s. MEM s lss ∧ (snapshotPROB = snapshot PROB s) then
hybrid_algo_gen f1 f2 snapshotPROB
else 0) vs lss PROB s' |
s' |
s' ∈ valid_states (prob_proj (PROB,vs))})
else problem_plan_bound PROB)
- MAP_N_gen_remove_ite
-
|- ∀vs lss.
(set lss = valid_states (prob_proj (PROB,vs))) ⇒
(MAX_SET
{S_gen
(λsnapshotPROB.
if ∃s''. MEM s'' lss ∧ (snapshotPROB = snapshot PROB s'') then
hybrid_algo_gen f1 f2 snapshotPROB
else 0) vs lss PROB s' |
s' |
s' ∈ valid_states (prob_proj (PROB,vs))} =
MAX_SET
{S_gen (hybrid_algo_gen f1 f2) vs lss PROB s' |
s' |
s' ∈ valid_states (prob_proj (PROB,vs))})
- FINITE_no_ite_PROB_hybrid_algo_gen_def
-
|- FINITE PROB ∧
(∀vs lss.
(vs,lss) ∈ f2 PROB ⇒ (set lss = valid_states (prob_proj (PROB,vs)))) ⇒
(hybrid_algo_gen f1 f2 PROB =
if ∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB then
(let
lvs = f1 PROB
in
SUM (MAP (N_gen_curried (hybrid_algo_gen f1 f2) PROB lvs) lvs))
else if
f2 PROB ≠ ∅ ∧
∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB
then
(let
(vs,lss) = CHOICE (f2 PROB)
in
MAX_SET
{S_gen (hybrid_algo_gen f1 f2) vs lss PROB s' |
s' |
s' ∈ valid_states (prob_proj (PROB,vs))})
else problem_plan_bound PROB)
- FINITE_no_ite_PROB_hybrid_algo_gen_def_thesis
-
|- FINITE PROB ∧
(∀vs lss. (vs,lss) ∈ f2 PROB ⇒ sspace_DAG (prob_proj (PROB,vs)) lss) ⇒
(hybrid_algo_gen f1 f2 PROB =
if ∀vs. MEM vs (f1 PROB) ⇒ vs ⊂ prob_dom PROB then
(let
lvs = f1 PROB
in
SUM (MAP (N_gen_curried (hybrid_algo_gen f1 f2) PROB lvs) lvs))
else if
f2 PROB ≠ ∅ ∧
∀vs lss s. (vs,lss) ∈ f2 PROB ∧ MEM s lss ⇒ snapshot PROB s ⊂ PROB
then
(let
(vs,lss) = CHOICE (f2 PROB)
in
MAX_SET
{S_gen (hybrid_algo_gen f1 f2) vs lss PROB s' |
s' |
s' ∈ valid_states (prob_proj (PROB,vs))})
else problem_plan_bound PROB)
- recursive_hybrid_algorithm_valid_thesis
-
|- ∀f1 f2 PROB.
FINITE PROB ∧
(∀PROB'.
dep_DAG PROB' (f1 PROB') ∧
∀vs lss.
(vs,lss) ∈ f2 PROB' ⇒ sspace_DAG (prob_proj (PROB',vs)) lss) ⇒
problem_plan_bound PROB ≤ hybrid_algo_gen f1 f2 PROB