Theory "dft"

Signature

Definitions

Rel_def

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

Theorems

DFT_def

⊢ FINITE (Parents G) ⇒
  DFT G f seen [] acc = acc ∧
  DFT G f seen (visit_now::visit_later) acc =
  if MEM visit_now seen then DFT G f seen visit_later acc
  else
    DFT G f (visit_now::seen) (G visit_now ++ visit_later) (f visit_now acc)

DFT_ind

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

DFT_CONS

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

DFT_FOLD

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

DFT_ALL_DISTINCT

⊢ ∀G seen to_visit.
      FINITE (Parents G) ⇒ ALL_DISTINCT (DFT G CONS seen to_visit [])

DFT_REACH_1

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

DFT_REACH_2

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

DFT_REACH_THM

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