Theory "systemAbstraction"

Parents     topologicalProps   dependency

Signature

Constant Type
action_proj :((α |-> β) # (α |-> γ)) # (α -> bool) -> (α |-> β) # (α |-> γ)
agree :(α |-> β) -> (α |-> β) -> bool
as_proj :((α |-> β) # (α |-> γ)) list # (α -> bool) -> ((α |-> β) # (α |-> γ)) list
prob_proj :((α |-> β) # (α |-> γ) -> bool) # (α -> bool) -> (α |-> β) # (α |-> γ) -> bool
snapshot :((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> (α |-> β) # (α |-> β) -> bool
ss_proj :((α |-> β) -> bool) -> (α -> bool) -> (α |-> β) -> bool

Definitions

action_proj_def
|- ∀a vs. action_proj (a,vs) = (DRESTRICT (FST a) vs,DRESTRICT (SND a) vs)
prob_proj_def
|- ∀PROB vs. prob_proj (PROB,vs) = IMAGE (λa. action_proj (a,vs)) PROB
as_proj_primitive_def
|- as_proj =
   WFREC
     (@R.
        WF R ∧
        (∀as vs a.
           ¬(FDOM (DRESTRICT (SND a) vs) ≠ ∅) ⇒ R (as,vs) (a::as,vs)) ∧
        ∀as vs a. FDOM (DRESTRICT (SND a) vs) ≠ ∅ ⇒ R (as,vs) (a::as,vs))
     (λas_proj a'.
        case a' of
          ([],vs) => I []
        | (a::as,vs) =>
            I
              (if FDOM (DRESTRICT (SND a) vs) ≠ ∅ then
                 action_proj (a,vs)::as_proj (as,vs)
               else as_proj (as,vs)))
agree_def
|- ∀s1 s2. agree s1 s2 ⇔ ∀v. v ∈ FDOM s1 ∧ v ∈ FDOM s2 ⇒ (s1 ' v = s2 ' v)
snapshot_def
|- ∀PROB s.
     snapshot PROB s = {a | a ∈ PROB ∧ agree (FST a) s ∧ agree (SND a) s}
ss_proj_def
|- ∀ss vs. ss_proj ss vs = IMAGE (λs. DRESTRICT s vs) ss


Theorems

action_proj_pair
|- action_proj ((p,e),vs) = (DRESTRICT p vs,DRESTRICT e vs)
as_proj_ind
|- ∀P.
     (∀a as vs.
        (¬(FDOM (DRESTRICT (SND a) vs) ≠ ∅) ⇒ P (as,vs)) ∧
        (FDOM (DRESTRICT (SND a) vs) ≠ ∅ ⇒ P (as,vs)) ⇒
        P (a::as,vs)) ∧ (∀vs. P ([],vs)) ⇒
     ∀v v1. P (v,v1)
as_proj_def
|- (∀vs as a.
      as_proj (a::as,vs) =
      if FDOM (DRESTRICT (SND a) vs) ≠ ∅ then
        action_proj (a,vs)::as_proj (as,vs)
      else as_proj (as,vs)) ∧ ∀vs. as_proj ([],vs) = []
as_proj_pair
|- (as_proj ((p,e)::as,vs) =
    if FDOM (DRESTRICT e vs) ≠ ∅ then action_proj ((p,e),vs)::as_proj (as,vs)
    else as_proj (as,vs)) ∧ (as_proj ([],vs) = [])
graph_plan_lemma_1_1
|- ∀s a vs.
     FST a ⊑ s ⇒
     (state_succ (DRESTRICT s vs) (action_proj (a,vs)) =
      DRESTRICT (state_succ s a) vs)
graph_plan_lemma_1
|- ∀s vs as.
     sat_precond_as (s,as) ⇒
     (exec_plan (DRESTRICT s vs,as_proj (as,vs)) =
      DRESTRICT (exec_plan (s,as)) vs)
graph_plan_lemma_2_2_1_1
|- action_dom (action_proj (a,vs)) = action_dom a ∩ vs
graph_plan_lemma_2_2_1
|- prob_dom (prob_proj (PROB,vs)) = prob_dom PROB ∩ vs
graph_plan_lemma_2_2
|- ∀PROB vs.
     s ∈ valid_states PROB ⇒
     DRESTRICT s vs ∈ valid_states (prob_proj (PROB,vs))
graph_plan_lemma_2_3_7_1
|- ∀h s vs.
     FDOM (SND h) ⊆ FDOM s ⇒
     (FDOM (state_succ s (action_proj (h,vs))) = FDOM (state_succ s h))
graph_plan_lemma_2_3_7_2
|- ∀h s vs.
     FST h ⊑ s ∧ FDOM (SND h) ⊆ FDOM s ⇒
     (DRESTRICT (state_succ s (action_proj (h,vs))) vs =
      DRESTRICT (state_succ s h) vs)
graph_plan_lemma_2_3_8_1
|- ∀s vs a.
     FST a ⊑ s ⇒
     (state_succ (DRESTRICT s vs) (action_proj (a,vs)) =
      DRESTRICT (state_succ s a) vs)
graph_plan_lemma_2_3_8_2
|- ∀as PROB vs a.
     FST a ⊑ s ⇒
     (exec_plan (DRESTRICT s vs,action_proj (a,vs)::as) =
      exec_plan (DRESTRICT (state_succ s a) vs,as))
graph_plan_lemma_2_3_8
|- ∀as a vs.
     FST a ⊑ s ⇒
     (exec_plan (DRESTRICT (state_succ s a) vs,as) =
      exec_plan (DRESTRICT s vs,action_proj (a,vs)::as))
graph_plan_lemma_2_3_9
|- ∀as a vs.
     FDOM (DRESTRICT (SND a) vs) ≠ ∅ ⇒
     (as_proj (a::as,vs) = action_proj (a,vs)::as_proj (as,vs))
graph_plan_lemma_2_3_10
|- ∀as a vs.
     (FDOM (DRESTRICT (SND a) vs) = ∅) ⇒
     (as_proj (a::as,vs) = as_proj (as,vs))
graph_plan_lemma_2_3_11_1
|- ∀s a vs.
     (FDOM (DRESTRICT (SND a) vs) = ∅) ⇒
     (DRESTRICT (state_succ s (action_proj (a,vs))) vs = DRESTRICT s vs)
graph_plan_lemma_2_3
|- ∀as vs s.
     sat_precond_as (s,as) ⇒
     (exec_plan (DRESTRICT s vs,as_proj (as,vs)) =
      DRESTRICT (exec_plan (s,as)) vs)
graph_plan_lemma_2_4_1
|- a ∈ PROB ⇒ action_proj (a,vs) ∈ prob_proj (PROB,vs)
graph_plan_lemma_2_4
|- ∀PROB vs.
     as ∈ valid_plans PROB ⇒
     as_proj (as,vs) ∈ valid_plans (prob_proj (PROB,vs))
graph_plan_lemma_2_5
|- ∀PROB. FINITE PROB ⇒ FINITE (prob_proj (PROB,vs))
graph_plan_lemma_2
|- ∀PROB vs as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ FINITE vs ∧
     LENGTH (as_proj (as,vs)) > 2 ** CARD vs − 1 ∧ sat_precond_as (s,as) ⇒
     ∃as1 as2 as3.
       (as1 ⧺ as2 ⧺ as3 = as_proj (as,vs)) ∧
       (exec_plan (DRESTRICT s vs,as1 ⧺ as2) =
        exec_plan (DRESTRICT s vs,as1)) ∧ as2 ≠ []
graph_plan_lemma_8_2
|- ∀as vs.
     as_proj (as,vs) =
     FILTER (λa. FDOM (SND a) ≠ ∅) (MAP (λa. action_proj (a,vs)) as)
graph_plan_lemma_8
|- ∀as1 as2 as3 p vs.
     (as1 ⧺ as2 ⧺ as3 = as_proj (p,vs)) ⇒
     ∃p_1 p_2 p_3.
       (p_1 ⧺ p_2 ⧺ p_3 = p) ∧ (as2 = as_proj (p_2,vs)) ∧
       (as1 = as_proj (p_1,vs))
graph_plan_lemma_9_1_1
|- ∀a s vs.
     state_succ (DRESTRICT s vs) (action_proj (a,vs)) =
     DRESTRICT (state_succ s (action_proj (a,vs))) vs
graph_plan_lemma_9_1
|- ∀s as vs.
     DRESTRICT (exec_plan (DRESTRICT s vs,as_proj (as,vs))) vs =
     exec_plan (DRESTRICT s vs,as_proj (as,vs))
graph_plan_lemma_9_2
|- ∀s as vs.
     DRESTRICT (exec_plan (DRESTRICT s vs,as_proj (as,vs))) vs =
     DRESTRICT (exec_plan (s,as_proj (as,vs))) vs
graph_plan_lemma_9
|- ∀s as vs.
     DRESTRICT (exec_plan (s,as_proj (as,vs))) vs =
     exec_plan (DRESTRICT s vs,as_proj (as,vs))
graph_plan_lemma_10_1
|- ∀a vs. FDOM (SND (action_proj (a,vs))) ⊆ FDOM (SND a)
graph_plan_lemma_10
|- ∀as s PROB vs.
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     exec_plan (s,as_proj (as,vs)) ∈ valid_states PROB
graph_plan_lemma_11
|- ∀s as vs.
     sat_precond_as (s,as) ⇒
     (DRESTRICT (exec_plan (s,as_proj (as,vs))) vs =
      DRESTRICT (exec_plan (s,as)) vs)
graph_plan_lemma_12_2
|- ∀a vs. action_proj (action_proj (a,vs),vs) = action_proj (a,vs)
graph_plan_lemma_12_2'
|- ∀a vs. action_dom a ⊆ vs ⇒ (action_proj (a,vs) = a)
graph_plan_lemma_12_2''
|- ∀P vs. prob_dom P ⊆ vs ⇒ (prob_proj (P,vs) = P)
graph_plan_lemma_12
|- ∀as s s' vs.
     sat_precond_as (s,as) ∧ (DRESTRICT s vs = DRESTRICT s' vs) ⇒
     sat_precond_as (s',as_proj (as,vs))
graph_plan_lemma_13
|- ∀as s s' vs.
     sat_precond_as (s,as) ∧ (DRESTRICT s vs = DRESTRICT s' vs) ⇒
     sat_precond_as (DRESTRICT s' vs,as_proj (as,vs))
graph_plan_lemma_24_1
|- no_effectless_act as ∧ as ∈ valid_plans PROB ∧ prob_dom PROB ⊆ vs ⇒
   (as_proj (as,vs) = as)
graph_plan_lemma_24_2
|- ∀s.
     exec_plan (s,as_proj (rem_effectless_act as,vs)) =
     exec_plan (s,as_proj (as,vs))
graph_plan_lemma_24
|- ∀PROB as vs s.
     as ∈ valid_plans PROB ∧ prob_dom PROB ⊆ vs ⇒
     (exec_plan (s,as_proj (as,vs)) = exec_plan (s,as))
dom_prob_proj
|- prob_dom (prob_proj (PROB,vs)) ⊆ vs
subset_proj_absorb_1
|- vs1 ⊆ vs2 ⇒ (action_proj (action_proj (a,vs2),vs1) = action_proj (a,vs1))
subset_proj_absorb
|- ∀PROB vs1 vs2.
     vs1 ⊆ vs2 ⇒ (prob_proj (prob_proj (PROB,vs2),vs1) = prob_proj (PROB,vs1))
union_proj_absorb
|- ∀PROB vs vs'.
     prob_proj (prob_proj (PROB,vs ∪ vs'),vs) = prob_proj (PROB,vs)
scc_lemma_1_4_1_1_2_1_1_1
|- ∀PROB vs v a.
     v ∉ vs ∧ a ∈ PROB ⇒
     (v ∈ FDOM (FST a) ⇒
      v ∈ FDOM (FST (action_proj (a,prob_dom PROB DIFF vs)))) ∧
     (v ∈ FDOM (SND a) ⇒
      v ∈ FDOM (SND (action_proj (a,prob_dom PROB DIFF vs))))
scc_lemma_1_4_1_1_2_1_1
|- ∀PROB vs vs' v v'.
     v ∈ vs' ∧ v' ∈ vs' ∧ DISJOINT vs vs' ⇒
     dep (PROB,v,v') ⇒
     dep (prob_proj (PROB,prob_dom PROB DIFF vs),v,v')
scc_lemma_1_4_1_1_2_1_5
|- ∀PROB vs.
     prob_dom (prob_proj (PROB,prob_dom PROB DIFF vs)) = prob_dom PROB DIFF vs
two_children_parent_bound_main_lemma_2_1
|- ∀PROB vs. vs ⊆ prob_dom PROB ⇒ (prob_dom (prob_proj (PROB,vs)) = vs)
scc_lemma_1_4_1_1_2_2_1_1_1
|- ∀a vs.
     FDOM (FST (action_proj (a,vs))) ⊆ FDOM (FST a) ∧
     FDOM (SND (action_proj (a,vs))) ⊆ FDOM (SND a)
scc_lemma_1_4_1_1_2_2_1_1
|- ∀a v vs.
     (v ∉ FDOM (FST a) ⇒ v ∉ FDOM (FST (action_proj (a,vs)))) ∧
     (v ∉ FDOM (SND a) ⇒ v ∉ FDOM (SND (action_proj (a,vs))))
scc_lemma_1_4_1_1_2_2_1
|- ∀PROB vs vs' vs''.
     ¬dep_var_set (PROB,vs,vs') ⇒ ¬dep_var_set (prob_proj (PROB,vs''),vs,vs')
scc_lemma_1_4_2_1_1_1_2
|- ∀PROB vs vs'.
     vs ⊆ prob_dom (prob_proj (PROB,prob_dom PROB DIFF vs')) ⇒ DISJOINT vs vs'
scc_lemma_1_4_2_1_1_1_3_1
|- ∀PROB vs v v'.
     (v ∉ vs ∧ v' ∉ vs) ∧ dep (PROB,v,v') ⇒
     dep (prob_proj (PROB,prob_dom PROB DIFF vs),v,v')
scc_lemma_1_4_2_1_2_1_1
|- ∀PROB vs vs' vs''.
     DISJOINT vs vs'' ∧ DISJOINT vs vs' ∧
     ¬dep_var_set (prob_proj (PROB,prob_dom PROB DIFF vs),vs',vs'') ⇒
     ¬dep_var_set (PROB,vs',vs'')
scc_lemma_1_4_2_1_1_1_4
|- ∀PROB. prob_proj (PROB,prob_dom PROB) = PROB
scc_main_lemma_1_6_1_3
|- ∀PROB vs vs'.
     vs ⊆ vs' ⇒ (prob_proj (PROB,vs) = prob_proj (prob_proj (PROB,vs'),vs))
scc_lemma_1_4_3_11
|- ∀PROB vs vs'.
     prob_proj (PROB,prob_dom PROB DIFF (vs ∪ vs')) =
     prob_proj
       (prob_proj (PROB,prob_dom PROB DIFF vs),
        prob_dom (prob_proj (PROB,prob_dom PROB DIFF vs)) DIFF vs')
scc_lemma_1_4_1_1_2_1_4
|- ∀PROB vs v v'.
     dep (prob_proj (PROB,prob_dom PROB DIFF vs),v,v') ⇒ dep (PROB,v,v')
scc_lemma_1_4_2_1_1_1_3
|- ∀PROB vs v v'.
     ¬(λv1' v2'. dep (prob_proj (PROB,prob_dom PROB DIFF vs),v1',v2'))⁺ v v' ⇒
     ¬(λv1' v2'. dep (PROB,v1',v2'))⁺ v v' ∨
     ∃v''.
       v'' ∈ vs ∧ (λv1' v2'. dep (PROB,v1',v2'))⁺ v v'' ∧
       (λv1' v2'. dep (PROB,v1',v2'))⁺ v'' v'
graph_plan_lemma_23_2
|- ∀as vs. EVERY (λa. action_proj (a,vs) = a) (as_proj (as,vs))
graph_plan_lemma_23_3
|- ∀a as vs.
     (FDOM (SND (action_proj (a,vs))) = ∅) ⇒
     (as_proj (as,vs) = as_proj (a::as,vs))
graph_plan_lemma_23
|- ∀as' as vs. sublist as' (as_proj (as,vs)) ⇒ (as_proj (as',vs) = as')
bound_child_parent_lemma_1_1_1_3_1_4_1
|- ∀a s vs.
     DISJOINT (FDOM (SND a)) s ⇒ DISJOINT (FDOM (SND (action_proj (a,vs)))) s
bound_child_parent_lemma_1_1_1_3_1_4
|- ∀a s vs.
     varset_action (a,vs) ∧ FST a ⊑ s ∧ FDOM (SND a) ⊆ FDOM s ⇒
     (state_succ s (action_proj (a,vs)) = state_succ s a)
parent_children_lemma_1_1_1_1
|- ∀vs as. no_effectless_act (as_proj (as,vs))
parent_children_lemma_1_1_1_3
|- ∀PROB vs as.
     as ∈ valid_plans PROB ⇒
     as_proj (as,vs) ∈ valid_plans (prob_proj (PROB,vs))
parent_children_lemma_1_1_1_6_1
|- ∀PROB vs vs'.
     prob_proj (prob_proj (PROB,vs),vs') = prob_proj (prob_proj (PROB,vs'),vs)
parent_children_lemma_1_1_1_11_2
|- ∀vs vs' a.
     varset_action (a,vs') ∧ varset_action (action_proj (a,vs'),vs) ⇒
     varset_action (a,vs)
parent_children_lemma_1_1_1_11_3
|- ∀PROB vs vs' a.
     varset_action (a,vs) ⇒
     varset_action (action_proj (a,prob_dom PROB DIFF vs'),vs)
parent_children_lemma_1_1_1_6_3
|- action_dom a ⊆ vs1 ∧ DISJOINT vs2 vs3 ⇒
   (action_proj (action_proj (a,vs1 DIFF vs2),vs3) = action_proj (a,vs3))
parent_children_lemma_1_1_1_6
|- ∀PROB vs vs'.
     DISJOINT vs vs' ⇒
     (prob_proj (prob_proj (PROB,prob_dom PROB DIFF vs'),vs) =
      prob_proj (PROB,vs))
parent_children_main_lemma_1_1_11_2
|- ∀a vs vs'.
     vs ⊆ vs' ∧ varset_action (a,vs') ⇒
     (varset_action (action_proj (a,vs'),vs) ⇔ varset_action (a,vs))
empty_problem_proj_bound
|- ∀PROB. problem_plan_bound (prob_proj (PROB,∅)) = 0
bound_child_parent_lemma_1_1_1_1
|- ∀PROB s as vs.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     sat_precond_as (s,as) ⇒
     ∃as'.
       (exec_plan (DRESTRICT s vs,as') =
        exec_plan (DRESTRICT s vs,as_proj (as,vs))) ∧
       LENGTH as' ≤ problem_plan_bound (prob_proj (PROB,vs)) ∧
       sublist as' (as_proj (as,vs)) ∧ sat_precond_as (s,as') ∧
       no_effectless_act as'
action_proj_inter
|- action_proj (action_proj (a,vs1),vs2) = action_proj (a,vs1 ∩ vs2)
prob_proj_inter
|- prob_proj (prob_proj (PROB,vs1),vs2) = prob_proj (PROB,vs1 ∩ vs2)
agree_state_succ_idempot
|- a ∈ PROB ∧ s ∈ valid_states PROB ∧ agree (SND a) s ⇒ (state_succ s a = s)
agree_restrict_state_succ_idempot
|- a ∈ PROB ∧ s ∈ valid_states PROB ∧
   agree (DRESTRICT (SND a) vs) (DRESTRICT s vs) ⇒
   (DRESTRICT (state_succ s a) vs = DRESTRICT s vs)
agree_exec_idempot
|- as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ∧
   (∀a. MEM a as ⇒ agree (SND a) s) ⇒
   (exec_plan (s,as) = s)
agree_restrict_exec_idempot
|- ∀s s'.
     as ∈ valid_plans PROB ∧ s' ∈ valid_states PROB ∧ s ∈ valid_states PROB ∧
     (∀a. MEM a as ⇒ agree (DRESTRICT (SND a) vs) (DRESTRICT s vs)) ∧
     (DRESTRICT s' vs = DRESTRICT s vs) ⇒
     (DRESTRICT (exec_plan (s',as)) vs = DRESTRICT s vs)
agree_restrict_exec_idempot_pair
|- ∀s s'.
     as ∈ valid_plans PROB ∧ s' ∈ valid_states PROB ∧ s ∈ valid_states PROB ∧
     (∀p e. MEM (p,e) as ⇒ agree (DRESTRICT e vs) (DRESTRICT s vs)) ∧
     (DRESTRICT s' vs = DRESTRICT s vs) ⇒
     (DRESTRICT (exec_plan (s',as)) vs = DRESTRICT s vs)
agree_comm
|- agree x x' ⇔ agree x' x
restricted_agree_imp_agree
|- FDOM s2 ⊆ vs ∧ agree (DRESTRICT s1 vs) s2 ⇒ agree s1 s2
agree_imp_submap
|- f1 ⊑ f2 ⇒ agree f1 f2
agree_FUNION
|- agree fm fm1 ∧ agree fm fm2 ⇒ agree fm (fm1 ⊌ fm2)
agree_fm_list_union
|- ∀fm.
     (∀fm'. MEM fm' fmList ⇒ agree fm fm') ⇒
     agree fm (FOLDR FUNION FEMPTY fmList)
DRESTRICT_EQ_AGREE
|- FDOM s2 ⊆ vs2 ∧ FDOM s1 ⊆ vs1 ⇒
   (DRESTRICT s1 vs2 = DRESTRICT s2 vs1) ⇒
   agree s1 s2
SUBMAPS_AGREE
|- s1 ⊑ s ∧ s2 ⊑ s ⇒ agree s1 s2
snapshot_pair
|- snapshot PROB s = {(p,e) | (p,e) ∈ PROB ∧ agree p s ∧ agree e s}
action_agree_valid_in_snapshot
|- a ∈ PROB ∧ agree (FST a) s ∧ agree (SND a) s ⇒ a ∈ snapshot PROB s
as_mem_agree_valid_in_snapshot
|- (∀a. MEM a as ⇒ agree (FST a) s ∧ agree (SND a) s) ∧
   as ∈ valid_plans PROB ⇒
   as ∈ valid_plans (snapshot PROB s)
SUBMAP_FUNION_DRESTRICT'
|- agree fma fmb ∧ vsa ⊆ FDOM fma ∧ vsb ⊆ FDOM fmb ∧
   (DRESTRICT fm vsa = DRESTRICT fma (vsa ∩ vs)) ∧
   (DRESTRICT fm vsb = DRESTRICT fmb (vsb ∩ vs)) ⇒
   (DRESTRICT fm (vsa ∪ vsb) = DRESTRICT (fma ⊌ fmb) ((vsa ∪ vsb) ∩ vs))
UNION_FUNION_DRESTRICT_SUBMAP
|- vs1 ⊆ FDOM fma ∧ vs2 ⊆ FDOM fmb ∧ agree fma fmb ∧ DRESTRICT fma vs1 ⊑ s ∧
   DRESTRICT fmb vs2 ⊑ s ⇒
   DRESTRICT (fma ⊌ fmb) (vs1 ∪ vs2) ⊑ s
agree_DRESTRICT
|- agree s1 s2 ⇒ agree (DRESTRICT s1 vs) (DRESTRICT s2 vs)
agree_DRESTRICT_2
|- FDOM s1 ⊆ vs1 ∧ FDOM s2 ⊆ vs2 ∧ agree s1 s2 ⇒
   agree (DRESTRICT s1 vs2) (DRESTRICT s2 vs1)
FINITE_snapshot
|- FINITE PROB ⇒ FINITE (snapshot PROB s)
snapshot_subset
|- snapshot PROB s ⊆ PROB
dom_proj_snapshot
|- prob_dom (prob_proj (PROB,prob_dom (snapshot PROB s))) =
   prob_dom (snapshot PROB s)
valid_states_snapshot
|- valid_states (prob_proj (PROB,prob_dom (snapshot PROB s))) =
   valid_states (snapshot PROB s)
valid_proj_neq_succ_restricted_neq_succ
|- x' ∈ prob_proj (PROB,vs) ∧ state_succ s x' ≠ s ⇒
   DRESTRICT (state_succ s x') vs ≠ DRESTRICT s vs
proj_successors
|- IMAGE (λs. DRESTRICT s vs) (state_successors (prob_proj (PROB,vs)) s) ⊆
   state_successors (prob_proj (PROB,vs)) (DRESTRICT s vs)
state_in_successor_proj_in_state_in_successor
|- s' ∈ state_successors (prob_proj (PROB,vs)) s ⇒
   DRESTRICT s' vs ∈ state_successors (prob_proj (PROB,vs)) (DRESTRICT s vs)
proj_FDOM_eff_subset_FDOM_valid_states
|- ∀p e s.
     (p,e) ∈ prob_proj (PROB,vs) ∧ s ∈ valid_states PROB ⇒ FDOM e ⊆ FDOM s
valid_proj_action_valid_succ
|- h ∈ prob_proj (PROB,vs) ∧ s ∈ valid_states PROB ⇒
   state_succ s h ∈ valid_states PROB
proj_successors_of_valid_are_valid
|- s ∈ valid_states PROB ⇒
   state_successors (prob_proj (PROB,vs)) s ⊆ valid_states PROB
invariantStateSpace_thm_9
|- ∀ss vs1 vs2. ss_proj ss (vs1 ∩ vs2) = ss_proj (ss_proj ss vs2) vs1
FINITE_ss_proj
|- ∀ss vs. FINITE ss ⇒ FINITE (ss_proj ss vs)
nempty_stateSpace_nempty_ss_proj
|- ss ≠ ∅ ⇒ ss_proj ss vs ≠ ∅
invariantStateSpace_thm_5
|- ∀ss vs dom. stateSpace ss dom ⇒ stateSpace (ss_proj ss vs) (dom ∩ vs)
invariantStateSpace_thm_12
|- ∀ss dom vs. stateSpace ss dom ∧ dom ⊆ vs ⇒ (ss_proj ss vs = ss)
neq_vs_neq_ss_proj
|- ∀vs.
     ss ≠ ∅ ∧ stateSpace ss vs ∧ vs1 ⊆ vs ∧ vs2 ⊆ vs ∧ vs1 ≠ vs2 ⇒
     ss_proj ss vs1 ≠ ss_proj ss vs2
subset_dom_stateSpace_ss_proj
|- ∀vs1 vs2. vs1 ⊆ vs2 ∧ stateSpace ss vs2 ⇒ stateSpace (ss_proj ss vs1) vs1
card_proj_leq
|- FINITE PROB ⇒ CARD (prob_proj (PROB,vs)) ≤ CARD PROB