Theory bft

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

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

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

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

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

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

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

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

⊢ ∀seen fringe f acc G.
    BFT G f seen fringe acc =
    if FINITE (Parents G) then
      case fringe of
        [] => acc
      | h::t =>
        if MEM h seen then BFT G f seen t acc
        else BFT G f (h::seen) (t ⧺ G h) (f h acc)
    else ARB

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

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