Theory "fmsp"

Parents transfer sptree

Signature

Constant	Type
FMSP	:(α -> num -> bool) -> (β -> γ -> bool) -> (α \|-> β) -> γ num_map -> 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

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

FMSP_FDOMSUB

⊢ bi_unique AN ⇒ (FMSP AN BC |==> AN |==> FMSP AN BC) $\\ (flip delete)

FMSP_FEMPTY

⊢ FMSP AN BC FEMPTY LN

FMSP_FUNION

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

FMSP_FUPDATE

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

FMSP_bitotal

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

FMSP_surj

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