Theory dft

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

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

⊢ ∀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

⊢ ∀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 [])

⊢ ∀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

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

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

⊢ 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)

⊢ ∀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

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

⊢ ∀to_visit seen f acc G.
    DFT G f seen to_visit acc =
    if FINITE (Parents G) then
      case to_visit of
        [] => acc
      | visit_now::visit_later =>
        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)
    else ARB