Theory "bft"

Parents dirGraph

Signature

Constant	Type
BFT	:(β -> β list) -> (β -> α -> α) -> β list -> β list -> α -> α
Rel	:(α -> β list) # γ # α list # δ list # ε -> num # num

Definitions

Rel_def

⊢ ∀G f seen fringe acc.
    Rel (G,f,seen,fringe,acc) =
    (CARD (Parents G DIFF LIST_TO_SET seen),LENGTH fringe)

Theorems

BFT_ALL_DISTINCT

⊢ ∀G seen fringe.
    FINITE (Parents G) ⇒ ALL_DISTINCT (BFT G CONS seen fringe [])

BFT_CONS

⊢ ∀G f seen fringe acc a b.
    FINITE (Parents G) ∧ (f = CONS) ∧ (acc = a ++ b) ⇒
    (BFT G f seen fringe acc = BFT G f seen fringe a ++ b)

BFT_FOLD

⊢ ∀G f seen fringe acc.
    FINITE (Parents G) ⇒
    (BFT G f seen fringe acc = FOLDR f acc (BFT G CONS seen fringe []))

BFT_REACH_1

⊢ ∀G f seen fringe acc.
    FINITE (Parents G) ∧ (f = CONS) ⇒
    ∀x. MEM x (BFT G f seen fringe acc) ⇒ x ∈ REACH_LIST G fringe ∨ MEM x acc

BFT_REACH_2

⊢ ∀G f seen fringe acc x.
    FINITE (Parents G) ∧ (f = CONS) ∧
    x ∈ REACH_LIST (EXCLUDE G (LIST_TO_SET seen)) fringe ∧ ¬MEM x seen ⇒
    MEM x (BFT G f seen fringe acc)

BFT_REACH_THM

⊢ ∀G fringe.
    FINITE (Parents G) ⇒
    ∀x. x ∈ REACH_LIST G fringe ⇔ MEM x (BFT G CONS [] fringe [])

BFT_def

⊢ FINITE (Parents G) ⇒
  (BFT G f seen [] acc = acc) ∧
  (BFT G f seen (h::t) acc =
   if MEM h seen then BFT G f seen t acc
   else BFT G f (h::seen) (t ++ G h) (f h acc))

BFT_ind

⊢ ∀P. (∀G f seen h t acc.
         P G f seen [] acc ∧
         ((FINITE (Parents G) ∧ ¬MEM h seen ⇒
           P G f (h::seen) (t ++ G h) (f h acc)) ∧
          (FINITE (Parents G) ∧ MEM h seen ⇒ P G f seen t acc) ⇒
          P G f seen (h::t) acc)) ⇒
      ∀v v1 v2 v3 v4. P v v1 v2 v3 v4