- replace_projected_single_primitive_def
-
|- replace_projected_single =
WFREC
(@R.
WF R ∧
(∀as_1 as a_1 a P. P (a,a_1) ⇒ R (P,as,as_1) (P,a::as,a_1::as_1)) ∧
∀as_1 as a_1 a P. ¬P (a,a_1) ⇒ R (P,as,a_1::as_1) (P,a::as,a_1::as_1))
(λreplace_projected_single a'.
case a' of
(P,[],as_1') => I []
| (P,a::as,[]) => I []
| (P,a::as,a_1::as_1) =>
I
(if P (a,a_1) then a::replace_projected_single (P,as,as_1)
else replace_projected_single (P,as,a_1::as_1)))
- replace_projected_dual_primitive_def
-
|- replace_projected_dual =
WFREC
(@R.
WF R ∧
(∀as_2 as_1 as a_2 P_2 a_1 a P_1.
P_1 (a,a_1) ∧ P_2 (a,a_2) ⇒
R (P_1,P_2,as,as_1,as_2) (P_1,P_2,a::as,a_1::as_1,a_2::as_2)) ∧
(∀as_2 as_1 as a_2 P_2 a_1 a P_1.
¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ P_1 (a,a_1) ⇒
R (P_1,P_2,as,as_1,a_2::as_2)
(P_1,P_2,a::as,a_1::as_1,a_2::as_2)) ∧
(∀as_2 as_1 as a_2 P_2 a_1 a P_1.
¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ ¬P_1 (a,a_1) ∧ P_2 (a,a_2) ⇒
R (P_1,P_2,as,a_1::as_1,as_2)
(P_1,P_2,a::as,a_1::as_1,a_2::as_2)) ∧
∀as_2 as_1 as a_2 P_2 a_1 a P_1.
¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ ¬P_1 (a,a_1) ∧ ¬P_2 (a,a_2) ⇒
R (P_1,P_2,as,a_1::as_1,a_2::as_2)
(P_1,P_2,a::as,a_1::as_1,a_2::as_2))
(λreplace_projected_dual a'.
case a' of
(P_1,P_2,[],v5) => I []
| (P_1,P_2,a::as,v14,[]) =>
I (replace_projected_single (P_1,a::as,v14))
| (P_1,P_2,a::as,[],a_2::as_2) =>
I (replace_projected_single (P_2,a::as,a_2::as_2))
| (P_1,P_2,a::as,a_1::as_1,a_2::as_2) =>
I
(if P_1 (a,a_1) ∧ P_2 (a,a_2) then
a::replace_projected_dual (P_1,P_2,as,as_1,as_2)
else if P_1 (a,a_1) then
a::replace_projected_dual (P_1,P_2,as,as_1,a_2::as_2)
else if P_2 (a,a_2) then
a::replace_projected_dual (P_1,P_2,as,a_1::as_1,as_2)
else replace_projected_dual (P_1,P_2,as,a_1::as_1,a_2::as_2)))
- full_ass_def
-
|- ∀PROB vs. full_ass (PROB,vs) ⇔ ∀a. a ∈ PROB ⇒ vs ⊆ FDOM (FST a)
- permutable_def
-
|- ∀PROB.
permutable PROB ⇔
(∀s as' as'' as.
as ∈ valid_plans PROB ∧ sublist as' as ∧ sublist as'' as ∧
sat_precond_as (s,as') ∧ sat_precond_as (s,as'') ∧
sat_precond_as (s,as) ⇒
sat_precond_as
(s,
replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,as',as''))) ∧
full_ass (PROB,prob_dom PROB)
- in_ass_union_def
-
|- ∀s s' s''.
in_ass_union (s,s',s'') ⇔
∀x. x ∈ FDOM s'' ⇒ (s'' ' x = s ' x) ∨ (s'' ' x = s' ' x)
- before_primitive_def
-
|- before =
WFREC
(@R.
WF R ∧
∀t t'' t' h'' h h'.
h' ≠ h ∧ ¬((h'' = h) ∧ h' ≠ h) ⇒
R (h'::t',h''::t'',t) (h'::t',h''::t'',h::t))
(λbefore a.
case a of
(v,[],v3) => ARB
| ([],h''::t'',[]) => ARB
| (h'''::t''',h''::t'',[]) => I F
| ([],h''::t'',h::t) => I F
| (h'::t',h''::t'',h::t) =>
I
(if h' = h then T
else if (h'' = h) ∧ h' ≠ h then F
else before (h'::t',h''::t'',t)))
- replace_projected_single_ind
-
|- ∀P'.
(∀P a as a_1 as_1.
(P (a,a_1) ⇒ P' (P,as,as_1)) ∧ (¬P (a,a_1) ⇒ P' (P,as,a_1::as_1)) ⇒
P' (P,a::as,a_1::as_1)) ∧ (∀P as_1. P' (P,[],as_1)) ∧
(∀P v4 v5. P' (P,v4::v5,[])) ⇒
∀v v1 v2. P' (v,v1,v2)
- replace_projected_single_def
-
|- (∀as_1 as a_1 a P.
replace_projected_single (P,a::as,a_1::as_1) =
if P (a,a_1) then a::replace_projected_single (P,as,as_1)
else replace_projected_single (P,as,a_1::as_1)) ∧
(∀as_1 P. replace_projected_single (P,[],as_1) = []) ∧
∀v5 v4 P. replace_projected_single (P,v4::v5,[]) = []
- replace_projected_dual_ind
-
|- ∀P.
(∀P_1 P_2 a as a_1 as_1 a_2 as_2.
(P_1 (a,a_1) ∧ P_2 (a,a_2) ⇒ P (P_1,P_2,as,as_1,as_2)) ∧
(¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ P_1 (a,a_1) ⇒
P (P_1,P_2,as,as_1,a_2::as_2)) ∧
(¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ ¬P_1 (a,a_1) ∧ P_2 (a,a_2) ⇒
P (P_1,P_2,as,a_1::as_1,as_2)) ∧
(¬(P_1 (a,a_1) ∧ P_2 (a,a_2)) ∧ ¬P_1 (a,a_1) ∧ ¬P_2 (a,a_2) ⇒
P (P_1,P_2,as,a_1::as_1,a_2::as_2)) ⇒
P (P_1,P_2,a::as,a_1::as_1,a_2::as_2)) ∧
(∀P_1 P_2 as_1 as_2. P (P_1,P_2,[],as_1,as_2)) ∧
(∀P_1 P_2 v6 v7 as_1. P (P_1,P_2,v6::v7,as_1,[])) ∧
(∀P_1 P_2 v8 v9 v16 v17. P (P_1,P_2,v8::v9,[],v16::v17)) ⇒
∀v v1 v2 v3 v4. P (v,v1,v2,v3,v4)
- replace_projected_dual_def
-
|- (∀as_2 as_1 as a_2 a_1 a P_2 P_1.
replace_projected_dual (P_1,P_2,a::as,a_1::as_1,a_2::as_2) =
if P_1 (a,a_1) ∧ P_2 (a,a_2) then
a::replace_projected_dual (P_1,P_2,as,as_1,as_2)
else if P_1 (a,a_1) then
a::replace_projected_dual (P_1,P_2,as,as_1,a_2::as_2)
else if P_2 (a,a_2) then
a::replace_projected_dual (P_1,P_2,as,a_1::as_1,as_2)
else replace_projected_dual (P_1,P_2,as,a_1::as_1,a_2::as_2)) ∧
(∀as_2 as_1 P_2 P_1. replace_projected_dual (P_1,P_2,[],as_1,as_2) = []) ∧
(∀v7 v6 as_1 P_2 P_1.
replace_projected_dual (P_1,P_2,v6::v7,as_1,[]) =
replace_projected_single (P_1,v6::v7,as_1)) ∧
∀v9 v8 v17 v16 P_2 P_1.
replace_projected_dual (P_1,P_2,v8::v9,[],v16::v17) =
replace_projected_single (P_2,v8::v9,v16::v17)
- vtx_cut_main_lemma_1_1_1
-
|- ∀P as_1 as. LENGTH (replace_projected_single (P,as,as_1)) ≤ LENGTH as_1
- vtx_cut_main_lemma_1_1
-
|- ∀P_1 P_2 as_1 as_2 as.
LENGTH (replace_projected_dual (P_1,P_2,as,as_1,as_2)) ≤
LENGTH as_1 + LENGTH as_2
- vtx_cut_main_lemma_1_2_1
-
|- ∀P as' as. sublist (replace_projected_single (P,as,as')) as
- vtx_cut_main_lemma_1_2
-
|- ∀P_1 P_2 as' as'' as.
sublist (replace_projected_dual (P_1,P_2,as,as',as'')) as
- vtx_cut_main_lemma_1_3
-
|- ∀P_1 P_2 as' as'' as.
replace_projected_dual (P_1,P_2,as,as',as'') =
replace_projected_dual (P_2,P_1,as,as'',as')
- vtx_cut_main_lemma_xx_4_1
-
|- ∀as as'.
sublist as' as ⇒
(replace_projected_single ((λ(a_1,a_2). a_1 = a_2),as,as') = as')
- vtx_cut_main_lemma_xx_1
-
|- ∀h h' as' as.
h ≠ h' ∧ sublist (h'::as') as ⇒
(replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),h::as,h'::as',[h]) =
h::h'::as')
- vtx_cut_main_lemma_xx_2
-
|- ∀PROB s s' as.
as ≠ [] ∧ full_ass (PROB,prob_dom PROB) ∧ as ∈ valid_plans PROB ∧
s ∈ valid_states PROB ∧ s' ∈ valid_states PROB ∧ sat_precond_as (s,as) ∧
sat_precond_as (s',as) ⇒
(s = s')
- vtx_cut_main_lemma_xx_3
-
|- ∀s s' s''. in_ass_union (s,s',s'') ⇔ in_ass_union (s',s,s'')
- vtx_cut_main_lemma_xx_4_2
-
|- ∀h h' as as' as''.
(replace_projected_single ((λ(a_1,a_2). a_1 = a_2),as,h::as') =
h'::as'') ⇒
(h = h')
- vtx_cut_main_lemma_xx_4_3
-
|- ∀h h' h'' t as as' as''.
(replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,h'::as',
h''::as'') =
h::t) ⇒
∃as_dis as_new.
(as = as_dis ⧺ [h] ⧺ as_new) ∧ ¬MEM h' as_dis ∧ ¬MEM h'' as_dis
- vtx_cut_main_lemma_xx_4_4
-
|- ∀h h' h'' t as as' as''.
(replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,h'::as',
h''::as'') =
h::t) ⇒
(h = h') ∨ (h = h'')
- vtx_cut_main_lemma_xx_4
-
|- ∀h h' h'' t as as' as''.
(replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,h'::as',
h''::as'') =
h::t) ⇒
(∃as_dis as_new.
(as = as_dis ⧺ [h] ⧺ as_new) ∧ ¬MEM h' as_dis ∧ ¬MEM h'' as_dis) ∧
((h = h') ∨ (h = h''))
- vtx_cut_main_lemma_xx_5
-
|- ∀h t as_dis as as' as''.
¬MEM h as_dis ∧
(replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as_dis ⧺ as,as',
as'') =
h::t) ⇒
(replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as_dis ⧺ as,as',
as'') =
replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,as',as''))
- vtx_cut_main_lemma_xx_6
-
|- ∀s s' h as as'.
full_ass (PROB,prob_dom PROB) ∧ h::as ∈ valid_plans PROB ∧
s ∈ valid_states PROB ∧ s' ∈ valid_states PROB ∧
sat_precond_as (s,h::as) ∧ sat_precond_as (s',h::as') ⇒
sat_precond_as (s,h::as')
- vtx_cut_main_lemma_xx_8_1
-
|- ∀h' as as'.
(replace_projected_single ((λ(a_1,a_2). a_1 = a_2),as,h'::as') = []) ⇒
¬MEM h' as
- vtx_cut_main_lemma_xx_8
-
|- ∀h' h'' as as' as''.
(replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,h'::as',
h''::as'') =
[]) ⇒
¬MEM h' as ∧ ¬MEM h'' as
- vtx_cut_main_lemma_xx_9
-
|- ∀s. in_ass_union (s,s,s)
- vtx_cut_main_lemma_xx_10
-
|- ∀s s'. in_ass_union (s,s',s')
- before_ind
-
|- ∀P.
(∀h' t' h'' t'' h t.
(h' ≠ h ∧ ¬((h'' = h) ∧ h' ≠ h) ⇒ P (h'::t',h''::t'',t)) ⇒
P (h'::t',h''::t'',h::t)) ∧ (∀h'' t'' h t. P ([],h''::t'',h::t)) ∧
(∀h' t' h'' t''. P (h'::t',h''::t'',[])) ∧ (∀v7 v6. P (v7,[],v6)) ∧
(∀v12 v13. P ([],v12::v13,[])) ⇒
∀v v1 v2. P (v,v1,v2)
- before_def
-
|- (∀t'' t' t h'' h' h.
before (h'::t',h''::t'',h::t) ⇔
if h' = h then T
else if (h'' = h) ∧ h' ≠ h then F
else before (h'::t',h''::t'',t)) ∧
(∀t'' t h'' h. before ([],h''::t'',h::t) ⇔ F) ∧
∀t'' t' h'' h'. before (h'::t',h''::t'',[]) ⇔ F
- vtx_cut_main_lemma_xx
-
|- ∀PROB as' as'' as s.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ permutable PROB ∧
sublist as' as ∧ sublist as'' as ∧ sat_precond_as (s,as') ∧
sat_precond_as (s,as'') ∧ sat_precond_as (s,as) ⇒
in_ass_union
(exec_plan (s,as'),exec_plan (s,as''),
exec_plan
(s,
replace_projected_dual
((λ(a_1,a_2). a_1 = a_2),(λ(a_1,a_2). a_1 = a_2),as,as',as'')))