# Structure bftTheory

Source File Identifier index Theory binding index

```signature bftTheory =
sig
type thm = Thm.thm

(*  Definitions  *)
val Rel_def : thm

(*  Theorems  *)
val BFT_ALL_DISTINCT : thm
val BFT_CONS : thm
val BFT_FOLD : thm
val BFT_REACH_1 : thm
val BFT_REACH_2 : thm
val BFT_REACH_THM : thm
val BFT_def : thm
val BFT_ind : thm

val bft_grammars : type_grammar.grammar * term_grammar.grammar
(*
[dirGraph] Parent theory of "bft"

[Rel_def]  Definition

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

[BFT_ALL_DISTINCT]  Theorem

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

[BFT_CONS]  Theorem

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

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

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

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

[BFT_REACH_THM]  Theorem

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

[BFT_def]  Theorem

⊢ 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]  Theorem

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

*)
end

```

Source File Identifier index Theory binding index