Theory "prodValidtd"

Parents     stateSpaceProduct

Signature

Constant Type
bounded_traversal_system :((α |-> β) # (α |-> β) -> bool) -> bool

Definitions

bounded_traversal_system_def
|- ∀PROB.
     bounded_traversal_system PROB ⇔
     ∀vs.
       ∃k.
         ∀s as.
           s ∈ valid_states (prob_proj (PROB,vs)) ∧
           as ∈ valid_plans (prob_proj (PROB,vs)) ⇒
           CARD (traversed_states (s,as)) ≤ k


Theorems

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