- state_list_proj_eq_state_proj_as_proj
-
|- ∀s.
sat_precond_as (s,as) ⇒
(ss_proj (traversed_states (s,as)) vs =
traversed_states (DRESTRICT s vs,as_proj (as,vs)))
- traversed_states_is_stateSpace
-
|- ∀s.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
stateSpace (traversed_states (s,as)) (prob_dom PROB)
- traversed_states_subset_valid_states
-
|- s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
traversed_states (s,as) ⊆ valid_states PROB
- traversed_states_leq_td
-
|- s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
bounded_traversal_system PROB ⇒
CARD (traversed_states (s,as)) − 1 ≤ td PROB
- propositional_sys_bounded_traversal
-
|- FINITE PROB ⇒ bounded_traversal_system PROB
- bool_traversed_states_leq_td
-
|- FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
CARD (traversed_states (s,as)) − 1 ≤ td PROB
- bounded_traversal_system_proj
-
|- bounded_traversal_system PROB ⇒
bounded_traversal_system (prob_proj (PROB,vs))
- traversed_states_subset_proj_prodf
-
|- ∀VS.
FINITE VS ⇒
∀PROB s as.
(∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ⇒
traversed_states (s,as) ⊆
PRODf (IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS)
(ss_proj (traversed_states (s,as)) vs)
- traversed_states_subset_proj_prodf'
-
|- FINITE VS ∧ (∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ⇒
traversed_states (s,as) ⊆
PRODf (IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS)
(ss_proj (traversed_states (s,as)) vs)
- finite_ss_proj_prod
-
|- ∀VS.
FINITE VS ∧ vs ∉ VS ∧ (∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ⇒
FINITE
(PRODf (IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS)
(ss_proj (traversed_states (s,as)) vs))
- prod_traversed_states_proj_catd
-
|- ∀VS.
FINITE VS ⇒
∀PROB s as.
(∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧ vs ∉ VS ⇒
CARD
(PRODf (IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS)
(ss_proj (traversed_states (s,as)) vs)) ≤
Π CARD
(ss_proj (traversed_states (s,as)) vs INSERT
IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS)
- prod_traversed_states_proj_catd'
-
|- FINITE VS ∧ (∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧ vs ∉ VS ⇒
CARD
(PRODf (IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS)
(ss_proj (traversed_states (s,as)) vs)) ≤
Π CARD
(ss_proj (traversed_states (s,as)) vs INSERT
IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS)
- catd_traversed_states_leq_catd_comp_ss_proj
-
|- ∀VS.
FINITE VS ⇒
∀PROB s as.
(∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧ vs ∉ VS ⇒
Π CARD
(ss_proj (traversed_states (s,as)) vs INSERT
IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS) ≤
Π (CARD ∘ (λvs. ss_proj (traversed_states (s,as)) vs)) (vs INSERT VS)
- catd_traversed_states_leq_catd_comp_ss_proj'
-
|- FINITE VS ∧ (∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧ vs ∉ VS ⇒
Π CARD
(ss_proj (traversed_states (s,as)) vs INSERT
IMAGE (λvs. ss_proj (traversed_states (s,as)) vs) VS) ≤
Π (CARD ∘ (λvs. ss_proj (traversed_states (s,as)) vs)) (vs INSERT VS)
- catd_traversed_states_leq_prod_td_proj
-
|- ∀VS.
FINITE VS ⇒
∀PROB s as.
bounded_traversal_system PROB ∧ (∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧ vs ∉ VS ⇒
Π (CARD ∘ (λvs. ss_proj (traversed_states (s,as)) vs)) (vs INSERT VS) ≤
Π (λvs. td (prob_proj (PROB,vs)) + 1) (vs INSERT VS)
- catd_traversed_states_leq_prod_td_proj'
-
|- FINITE VS ∧ bounded_traversal_system PROB ∧
(∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ s ∈ valid_states PROB ∧
as ∈ valid_plans PROB ∧ sat_precond_as (s,as) ∧ vs ∉ VS ⇒
Π (CARD ∘ (λvs. ss_proj (traversed_states (s,as)) vs)) (vs INSERT VS) ≤
Π (λvs. td (prob_proj (PROB,vs)) + 1) (vs INSERT VS)
- prodValidtdS
-
|- ∀VS.
FINITE VS ∧ FINITE PROB ∧ vs ∉ VS ∧ bounded_traversal_system PROB ∧
(∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ vs ∉ VS ⇒
td PROB ≤ Π (λvs. td (prob_proj (PROB,vs)) + 1) (vs INSERT VS) − 1
- prodValidtd_propositional_sys
-
|- ∀VS.
FINITE VS ∧ FINITE PROB ∧ vs ∉ VS ∧ (∀vs'. vs' ∈ VS ⇒ DISJOINT vs vs') ∧
(∀vs vs'. vs ∈ VS ∧ vs' ∈ VS ∧ vs ≠ vs' ⇒ DISJOINT vs vs') ∧
(BIGUNION (vs INSERT VS) = prob_dom PROB) ∧ vs ∉ VS ⇒
td PROB ≤ Π (λvs. td (prob_proj (PROB,vs)) + 1) (vs INSERT VS) − 1