Theory "fmsp"

Parents transfer sptree

Signature

Constant	Type
FMSP	:(α -> num -> bool) -> (β -> γ -> bool) -> (α \|-> β) -> γ spt -> bool

FMSP_def

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

FMSP_FDOM

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

FMSP_FEMPTY

⊢ FMSP AN BC FEMPTY LN

FMSP_FUPDATE

⊢ bi_unique AN ⇒
  FUN_REL (FMSP AN BC) (FUN_REL (PAIR_REL AN BC) (FMSP AN BC)) $|+
    (λsp (n,v). insert n v sp)

FMSP_bitotal

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

FMSP_FORALL

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

FMSP_FUNION

⊢ FUN_REL (FMSP AN BC) (FUN_REL (FMSP AN BC) (FMSP AN BC)) $FUNION union

FMSP_FDOMSUB

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