Theory "topologicalProps"

Parents     actionSeqProcess

Signature

Constant Type
MPLS :((α |-> β) # (α |-> β) -> bool) -> num -> bool
MPLS_charles :((α |-> β) # (α |-> β) -> bool) -> num -> bool
MPLS_s :((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> num -> bool
MPLS_stage_1 :((α |-> β) # (α |-> β) -> bool) -> num -> bool
PLS :(α |-> β) # ((α |-> β) # (α |-> β)) list -> num -> bool
PLS_charles :(α |-> β) # ((α |-> β) # (α |-> β)) list # ((α |-> β) # (α |-> β) -> bool) -> num -> bool
PLS_stage_1 :(α |-> β) # ((α |-> β) # (α |-> β)) list -> num -> bool
RD :α problem -> num
problem_plan_bound :((α |-> β) # (α |-> β) -> bool) -> num
problem_plan_bound_charles :((α |-> β) # (α |-> β) -> bool) -> num
problem_plan_bound_s :((α |-> β) # (α |-> β) -> bool) -> (α |-> β) -> num
problem_plan_bound_stage_1 :α problem -> num
statelist' :(α |-> β) -> ((α |-> β) # (α |-> β)) list -> (α |-> β) list
td :((α |-> β) # (α |-> β) -> bool) -> num
traversed_states :(α |-> β) # ((α |-> β) # (α |-> β)) list -> (α |-> β) -> bool
valid_path :((α |-> β) # (α |-> β) -> bool) -> (α |-> β) list -> bool

Definitions

PLS_charles_def
|- ∀s as PROB.
     PLS_charles (s,as,PROB) =
     {LENGTH as' |
      (exec_plan (s,as') = exec_plan (s,as)) ∧ as' ∈ valid_plans PROB}
MPLS_charles_def
|- ∀PROB.
     MPLS_charles PROB =
     {MIN_SET (PLS_charles (s,as,PROB)) |
      (s,as) |
      s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
problem_plan_bound_charles_def
|- ∀PROB. problem_plan_bound_charles PROB = MAX_SET (MPLS_charles PROB)
PLS_stage_1_def
|- ∀s as.
     PLS_stage_1 (s,as) =
     IMAGE LENGTH {as' | exec_plan (s,as') = exec_plan (s,as)}
MPLS_stage_1_def
|- ∀PROB.
     MPLS_stage_1 PROB =
     IMAGE (λ(s,as). MIN_SET (PLS_stage_1 (s,as)))
       {(s,as) | s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
problem_plan_bound_stage_1_def
|- ∀PROB. problem_plan_bound_stage_1 PROB = MAX_SET (MPLS_stage_1 PROB)
PLS_def
|- ∀s as.
     PLS (s,as) =
     IMAGE LENGTH
       {as' | (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as}
MPLS_def
|- ∀PROB.
     MPLS PROB =
     IMAGE (λ(s,as). MIN_SET (PLS (s,as)))
       {(s,as) | s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
problem_plan_bound_def
|- ∀PROB. problem_plan_bound PROB = MAX_SET (MPLS PROB)
RD_def
|- ∀Pi. RD Pi = MAX_SET {LENGTH p − 1 | valid_path Pi p ∧ ALL_DISTINCT p}
statelist'_def
|- (∀s. statelist' s [] = [s]) ∧
   ∀s a as. statelist' s (a::as) = s::statelist' (state_succ s a) as
MPLS_s_def
|- ∀PROB s.
     MPLS_s PROB s =
     IMAGE (λ(s,as). MIN_SET (PLS (s,as))) {(s,as) | as ∈ valid_plans PROB}
problem_plan_bound_s_def
|- ∀PROB s. problem_plan_bound_s PROB s = MAX_SET (MPLS_s PROB s)
traversed_states_def
|- ∀s as. traversed_states (s,as) = set (state_list (s,as))
td_def
|- ∀PROB.
     td PROB =
     MAX_SET
       {CARD (traversed_states (s,as)) − 1 |
        s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}


Theorems

bound_child_parent_lemma_s_1_1_1_1_1_1
|- ∀PROB as k s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     problem_plan_bound_s PROB s ≤ k ⇒
     MIN_SET (PLS (s,as)) ≤ problem_plan_bound_s PROB s
bound_child_parent_lemma_s_1_1_1_1_1_1_1
|- ∀PROB as. as ∈ valid_plans PROB ⇒ MIN_SET (PLS (s,as)) ∈ MPLS_s PROB s
expanded_problem_plan_bound_thm_1
|- ∀PROB.
     problem_plan_bound PROB =
     MAX_SET
       (IMAGE (λ(s,as). MIN_SET (PLS (s,as)))
          {(s,as) | s ∈ valid_states PROB ∧ as ∈ valid_plans PROB})
expanded_problem_plan_bound_thm
|- ∀PROB.
     problem_plan_bound PROB =
     MAX_SET
       {MIN_SET (PLS (s,as)) | s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
valid_path_ind
|- ∀P.
     (∀Pi. P Pi []) ∧ (∀Pi s. P Pi [s]) ∧
     (∀Pi s1 s2 rest. P Pi (s2::rest) ⇒ P Pi (s1::s2::rest)) ⇒
     ∀v v1. P v v1
valid_path_def
|- (∀Pi. valid_path Pi [] ⇔ T) ∧
   (∀s Pi. valid_path Pi [s] ⇔ s ∈ valid_states Pi) ∧
   ∀s2 s1 rest Pi.
     valid_path Pi (s1::s2::rest) ⇔
     s1 ∈ valid_states Pi ∧ (∃a. a ∈ Pi ∧ (exec_plan (s1,[a]) = s2)) ∧
     valid_path Pi (s2::rest)
valid_path_ITP2015_def
|- (valid_path Pi [] ⇔ T) ∧ (valid_path Pi [s] ⇔ s ∈ valid_states Pi) ∧
   (valid_path Pi (s1::s2::rest) ⇔
    s1 ∈ valid_states Pi ∧ (∃a. a ∈ Pi ∧ (exec_plan (s1,[a]) = s2)) ∧
    valid_path Pi (s2::rest))
bound_main_lemma_1_1
|- ∀PROB s as.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     ∃x. x ∈ PLS (s,as) ∧ x ≤ 2 ** CARD (prob_dom PROB) − 1
bound_main_lemma_1
|- ∀PROB x. FINITE PROB ∧ x ∈ MPLS PROB ⇒ x ≤ 2 ** CARD (prob_dom PROB) − 1
FINITE_MPLS
|- FINITE Pi ⇒ FINITE (MPLS Pi)
LENGTH_statelist'
|- ∀as s. LENGTH (statelist' s as) = LENGTH as + 1
valid_path_statelist'
|- ∀as s.
     as ∈ valid_plans Pi ∧ s ∈ valid_states Pi ⇒
     valid_path Pi (statelist' s as)
statelist'_exec_plan
|- ∀as s p. (statelist' s as = p) ⇒ (exec_plan (s,as) = LAST p)
statelist'_EQ_NIL
|- statelist' s as ≠ []
statelist'_TAKE
|- ∀as s p.
     (statelist' s as = p) ⇒
     ∀n. n ≤ LENGTH as ⇒ (exec_plan (s,TAKE n as) = EL n p)
RD_bounds_sublistD
|- ∀Pi. FINITE Pi ⇒ problem_plan_bound Pi ≤ RD Pi
bound_main_lemma_3
|- ∀PROB. FINITE PROB ⇒ MPLS PROB ≠ ∅
bound_main_lemma
|- ∀PROB.
     FINITE PROB ⇒ problem_plan_bound PROB ≤ 2 ** CARD (prob_dom PROB) − 1
bound_child_parent_lemma_2_1_1
|- ∀P f.
     (∀PROB as s.
        P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB) ⇒
     ∀PROB s as.
       P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
       ∃x. x ∈ PLS (s,as) ∧ x < f PROB
bound_child_parent_lemma_2_1
|- ∀P f.
     (∀PROB as s.
        P PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB) ⇒
     ∀PROB x. P PROB ⇒ x ∈ MPLS PROB ⇒ x < f PROB
bound_child_parent_lemma_2_1_1_finite
|- ∀P f.
     (∀PROB as s.
        P PROB ∧ FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB) ⇒
     ∀PROB s as.
       P PROB ∧ FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
       ∃x. x ∈ PLS (s,as) ∧ x < f PROB
bound_child_parent_lemma_2_1_finite
|- ∀P f.
     (∀PROB as s.
        P PROB ∧ FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB) ⇒
     ∀PROB x. P PROB ∧ FINITE PROB ⇒ x ∈ MPLS PROB ⇒ x < f PROB
bound_child_parent_lemma_2
|- ∀P f.
     (∀PROB as s.
        P PROB ∧ FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB) ⇒
     ∀PROB. P PROB ∧ FINITE PROB ⇒ problem_plan_bound PROB < f PROB
bound_child_parent_lemma_2_1_1_thesis
|- FINITE PROB ∧
   (∀as s.
      as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
      ∃as'.
        (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
        LENGTH as' < k) ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
   ∃x. x ∈ PLS (s,as) ∧ x < k
bound_child_parent_lemma_2_1_thesis
|- FINITE PROB ∧
   (∀as s.
      s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
      ∃as'.
        (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
        LENGTH as' < k) ⇒
   x ∈ MPLS PROB ⇒
   x < k
bound_child_parent_lemma_2_thesis'
|- FINITE PROB ∧
   (∀as s.
      s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
      ∃as'.
        (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
        LENGTH as' < k) ⇒
   problem_plan_bound PROB < k
bound_child_parent_lemma_2_thesis
|- FINITE PROB ∧
   (∀as s.
      s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
      ∃as'.
        (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
        LENGTH as' ≤ k) ⇒
   problem_plan_bound PROB ≤ k
bound_child_parent_lemma_2_
|- ∀P f PROB.
     (∀PROB' as s.
        P PROB' ∧ FINITE PROB' ∧ s ∈ valid_states PROB' ∧
        as ∈ valid_plans PROB' ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB') ∧ P PROB ∧ FINITE PROB ⇒
     problem_plan_bound PROB < f PROB
bound_child_parent_lemma_1_1_1_1_1_1_1
|- ∀PROB s as.
     s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     MIN_SET (PLS (s,as)) ∈ MPLS PROB
bound_child_parent_lemma_1_1_1_1_1_1
|- ∀PROB s as k.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧
     problem_plan_bound PROB ≤ k ⇒
     MIN_SET (PLS (s,as)) ≤ problem_plan_bound PROB
bound_child_parent_lemma_1_1_1_1_1_2_1
|- ∀s as. PLS (s,as) ≠ ∅
bound_child_parent_lemma_1_1_1_1_1_2
|- ∀s as. ∃x. x ∈ PLS (s,as) ∧ (x = MIN_SET (PLS (s,as)))
bound_child_parent_lemma_1_1_1_1_1_3
|- ∀x s as.
     x ∈ PLS (s,as) ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ (LENGTH as' = x) ∧
       sublist as' as
bound_child_parent_lemma_1_1_1_1_1
|- ∀PROB as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       LENGTH as' ≤ problem_plan_bound PROB
bound_main_lemma_s_3
|- ∀PROB s. MPLS_s PROB s ≠ ∅
bound_child_parent_lemma_s_2_1_1
|- ∀P f.
     (∀PROB as s.
        FINITE PROB ∧ P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB s) ⇒
     ∀PROB s as.
       FINITE PROB ∧ P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
       ∃x. x ∈ PLS (s,as) ∧ x < f PROB s
bound_child_parent_lemma_s_2_1
|- ∀P f.
     (∀PROB as s.
        FINITE PROB ∧ P PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB s) ⇒
     ∀PROB x s.
       FINITE PROB ∧ P PROB ∧ s ∈ valid_states PROB ⇒
       x ∈ MPLS_s PROB s ⇒
       x < f PROB s
bound_child_parent_lemma_s_2
|- ∀PROB s P f.
     (∀PROB as s.
        FINITE PROB ∧ P PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB s) ⇒
     FINITE PROB ∧ P PROB ∧ s ∈ valid_states PROB ⇒
     problem_plan_bound_s PROB s < f PROB s
bound_main_lemma_reachability_s
|- ∀PROB s.
     FINITE PROB ∧ s ∈ valid_states PROB ⇒
     problem_plan_bound_s PROB s < CARD (reachable_s PROB s)
problem_plan_bound_s_LESS_EQ_problem_plan_bound_thm
|- ∀PROB s.
     FINITE PROB ∧ s ∈ valid_states PROB ⇒
     problem_plan_bound_s PROB s < problem_plan_bound PROB + 1
bound_main_lemma_s_1
|- ∀PROB x s.
     FINITE PROB ∧ s ∈ valid_states PROB ⇒
     x ∈ MPLS_s PROB s ⇒
     x ≤ 2 ** CARD (prob_dom PROB) − 1
bound_main_lemma_s
|- ∀PROB s.
     FINITE PROB ∧ s ∈ valid_states PROB ⇒
     problem_plan_bound_s PROB s ≤ 2 ** CARD (prob_dom PROB) − 1
bound_child_parent_lemma_s_1_1_1_1_1
|- ∀PROB as s.
     FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
     ∃as'.
       (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
       LENGTH as' ≤ problem_plan_bound_s PROB s
PLS_def_ITP2015
|- ∀s as.
     PLS (s,as) =
     {LENGTH as' | (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as}
expanded_problem_plan_bound_charles_thm
|- ∀PROB.
     problem_plan_bound_charles PROB =
     MAX_SET
       {MIN_SET (PLS_charles (s,as,PROB)) |
        (s,as) |
        s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}
bound_main_lemma_charles_3
|- ∀PROB. FINITE PROB ⇒ MPLS_charles PROB ≠ ∅
bound_main_lemma_charles_1_1
|- ∀PROB s as.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     ∃x. x ∈ PLS_charles (s,as,PROB) ∧ x ≤ 2 ** CARD (prob_dom PROB) − 1
bound_main_lemma_charles_1
|- ∀PROB x.
     FINITE PROB ⇒ x ∈ MPLS_charles PROB ⇒ x ≤ 2 ** CARD (prob_dom PROB) − 1
bound_main_lemma_charles
|- ∀PROB.
     FINITE PROB ⇒
     problem_plan_bound_charles PROB ≤ 2 ** CARD (prob_dom PROB) − 1
bound_child_parent_lemma_charles_2_1_1
|- ∀P f.
     (∀PROB as s.
        P PROB ∧ FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB) ⇒
     ∀PROB s as.
       P PROB ∧ FINITE PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⇒
       ∃x. x ∈ PLS_charles (s,as,PROB) ∧ x < f PROB
bound_child_parent_lemma_charles_2_1
|- ∀P f.
     (∀PROB as s.
        P PROB ∧ FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB) ⇒
     ∀PROB x. P PROB ∧ FINITE PROB ⇒ x ∈ MPLS_charles PROB ⇒ x < f PROB
bound_child_parent_lemma_charles_2
|- ∀P f.
     (∀PROB as s.
        P PROB ∧ FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
        ∃as'.
          (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
          LENGTH as' < f PROB) ⇒
     ∀PROB. P PROB ∧ FINITE PROB ⇒ problem_plan_bound_charles PROB < f PROB
sublistD_bounds_D
|- ∀PROB.
     FINITE PROB ⇒ problem_plan_bound_charles PROB ≤ problem_plan_bound PROB
sublistD_bounds_D_and_RD_bounds_sublistD
|- ∀PROB.
     FINITE PROB ⇒
     problem_plan_bound_charles PROB ≤ problem_plan_bound PROB ∧
     problem_plan_bound PROB ≤ RD PROB
empty_problem_bound
|- ∀PROB. (prob_dom PROB = ∅) ⇒ (problem_plan_bound PROB = 0)
temp
|- (∀x. ∃x'. (rd x = ell x') ∧ (rd x = rd x')) ⇒
   (∀x. P x (ell x)) ⇒
   ∃x'. (rd x = rd x') ∧ P x' (rd x')
bound_child_parent_lemma_1_1_1_1_1'
|- ∀PROB as s.
     FINITE PROB ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
     ∃as'.
       (exec_plan (s,as') = exec_plan (s,as)) ∧ sublist as' as ∧
       LENGTH as' ≤ problem_plan_bound PROB ∧ sat_precond_as (s,as')
problem_plan_bound_UBound
|- (∀as s.
      s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
      ∃as'.
        (exec_plan (s,as) = exec_plan (s,as')) ∧ sublist as' as ∧
        LENGTH as' < f PROB) ∧ FINITE PROB ⇒
   problem_plan_bound PROB < f PROB
finite_traversed_states
|- FINITE (traversed_states (s,as))
traversed_states_nempty
|- traversed_states (s,as) ≠ ∅
traversed_states_geq_1
|- ∀s as. 1 ≤ CARD (traversed_states (s,as))
init_is_traversed
|- s ∈ traversed_states (s,as)
traversed_states_rem_condless_act
|- ∀s.
     traversed_states (s,rem_condless_act (s,[],as)) = traversed_states (s,as)
td_UBound
|- FINITE PROB ∧
   (∀s as.
      sat_precond_as (s,as) ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ⇒
      CARD (traversed_states (s,as)) ≤ k) ⇒
   td PROB ≤ k − 1