# Structure fmspTheory

Source File Identifier index Theory binding index

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

(*  Definitions  *)
val FMSP_def : thm

(*  Theorems  *)
val FMSP_FDOM : thm
val FMSP_FDOMSUB : thm
val FMSP_FEMPTY : thm
val FMSP_FORALL : thm
val FMSP_FUNION : thm
val FMSP_FUPDATE : thm
val FMSP_bitotal : thm

val fmsp_grammars : type_grammar.grammar * term_grammar.grammar
(*
[sptree] Parent theory of "fmsp"

[transfer] Parent theory of "fmsp"

[FMSP_def]  Definition

⊢ ∀AN BC fm sp.
FMSP AN BC fm sp ⇔
∀a n. AN a n ⇒ OPTREL BC (FLOOKUP fm a) (lookup n sp)

[FMSP_FDOM]  Theorem

⊢ (FMSP AN BC ===> AN ===> \$<=>) FDOM domain

[FMSP_FDOMSUB]  Theorem

⊢ bi_unique AN ⇒
(FMSP AN BC ===> AN ===> FMSP AN BC) \$\\ (combin\$C delete)

[FMSP_FEMPTY]  Theorem

⊢ FMSP AN BC FEMPTY LN

[FMSP_FORALL]  Theorem

⊢ bitotal AN ∧ bitotal BC ∧ bi_unique AN ⇒
((FMSP AN BC ===> \$<=>) ===> \$<=>) \$! \$!

[FMSP_FUNION]  Theorem

⊢ (FMSP AN BC ===> FMSP AN BC ===> FMSP AN BC) FUNION union

[FMSP_FUPDATE]  Theorem

⊢ bi_unique AN ⇒
(FMSP AN BC ===> AN ### BC ===> FMSP AN BC) \$|+
(λsp (n,v). insert n v sp)

[FMSP_bitotal]  Theorem

⊢ bitotal AN ∧ bitotal BC ∧ bi_unique AN ⇒ bitotal (FMSP AN BC)

*)
end

```

Source File Identifier index Theory binding index