Theory "depGraphVtxCut"

Signature

Definitions

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)))

Theorems

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'')))