Theory "fmsp"

Parents     transfer   sptree

Signature

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

Definitions

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

Theorems

FMSP_FUPDATE 
⊢ bi_unique AN ⇒
  (FMSP AN BC ===> AN ### BC ===> FMSP AN BC) $|+ (λsp (n,v). insert n v sp)
FMSP_FUNION 
⊢ (FMSP AN BC ===> FMSP AN BC ===> FMSP AN BC) $FUNION union
FMSP_FORALL 
⊢ bitotal AN ∧ bitotal BC ∧ bi_unique AN ⇒
  ((FMSP AN BC ===> $<=>) ===> $<=>) $! $!
FMSP_FEMPTY 
⊢ FMSP AN BC FEMPTY LN
FMSP_FDOMSUB 
⊢ bi_unique AN ⇒ (FMSP AN BC ===> AN ===> FMSP AN BC) $\\ (combin$C delete)
FMSP_FDOM 
⊢ (FMSP AN BC ===> AN ===> $<=>) FDOM domain
FMSP_bitotal 
⊢ bitotal AN ∧ bitotal BC ∧ bi_unique AN ⇒ bitotal (FMSP AN BC)