- 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