Structure finite_mapTheory


Source File Identifier index Theory binding index

signature finite_mapTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val DRESTRICT_DEF : thm
    val FAPPLY_DEF : thm
    val FCARD_DEF : thm
    val FDIFF_def : thm
    val FDOM_DEF : thm
    val FEMPTY_DEF : thm
    val FEVERY_DEF : thm
    val FLOOKUP_DEF : thm
    val FMAP_MAP2_def : thm
    val FMERGE_DEF : thm
    val FRANGE_DEF : thm
    val FUNION_DEF : thm
    val FUN_FMAP_DEF : thm
    val FUPDATE_DEF : thm
    val FUPDATE_LIST : thm
    val ITFMAPR_def : thm
    val ITFMAP_def : thm
    val MAP_KEYS_def : thm
    val RRESTRICT_DEF : thm
    val SUBMAP_DEF : thm
    val f_o_DEF : thm
    val f_o_f_DEF : thm
    val fmap_EQ_UPTO_def : thm
    val fmap_ISO_DEF : thm
    val fmap_TY_DEF : thm
    val fmap_domsub : thm
    val fmap_inverse_def : thm
    val fmap_rel_def : thm
    val fmap_size_def : thm
    val fmlfpR_def : thm
    val fp_soluble_def : thm
    val is_fmap_def : thm
    val lbound_def : thm
    val o_f_DEF : thm
  
  (*  Theorems  *)
    val DISJOINT_FEVERY_FUNION : thm
    val DOMSUB_COMMUTES : thm
    val DOMSUB_FAPPLY : thm
    val DOMSUB_FAPPLY_NEQ : thm
    val DOMSUB_FAPPLY_THM : thm
    val DOMSUB_FEMPTY : thm
    val DOMSUB_FLOOKUP : thm
    val DOMSUB_FLOOKUP_NEQ : thm
    val DOMSUB_FLOOKUP_THM : thm
    val DOMSUB_FUNION : thm
    val DOMSUB_FUPDATE : thm
    val DOMSUB_FUPDATE_NEQ : thm
    val DOMSUB_FUPDATE_THM : thm
    val DOMSUB_IDEM : thm
    val DOMSUB_MAP_KEYS : thm
    val DOMSUB_NOT_IN_DOM : thm
    val DOMSUB_SUBMAP : thm
    val DRESTRICTED_FUNION : thm
    val DRESTRICT_DOMSUB : thm
    val DRESTRICT_DRESTRICT : thm
    val DRESTRICT_EQ_DRESTRICT : thm
    val DRESTRICT_EQ_DRESTRICT_SAME : thm
    val DRESTRICT_EQ_FUNION : thm
    val DRESTRICT_FDOM : thm
    val DRESTRICT_FEMPTY : thm
    val DRESTRICT_FUNION : thm
    val DRESTRICT_FUNION_DRESTRICT_COMPL : thm
    val DRESTRICT_FUNION_SAME : thm
    val DRESTRICT_FUNION_SUBSET : thm
    val DRESTRICT_FUPDATE : thm
    val DRESTRICT_IDEMPOT : thm
    val DRESTRICT_IS_FEMPTY : thm
    val DRESTRICT_MAP_KEYS_IMAGE : thm
    val DRESTRICT_SUBMAP : thm
    val DRESTRICT_SUBMAP_gen : thm
    val DRESTRICT_SUBSET : thm
    val DRESTRICT_SUBSET_SUBMAP : thm
    val DRESTRICT_SUBSET_SUBMAP_gen : thm
    val DRESTRICT_UNIV : thm
    val EQ_FDOM_SUBMAP : thm
    val FAPPLY_FUPDATE : thm
    val FAPPLY_FUPDATE_THM : thm
    val FAPPLY_f_o : thm
    val FCARD_0_FEMPTY : thm
    val FCARD_FEMPTY : thm
    val FCARD_FUPDATE : thm
    val FCARD_SUC : thm
    val FDOM_DOMSUB : thm
    val FDOM_DRESTRICT : thm
    val FDOM_EQ_EMPTY : thm
    val FDOM_EQ_EMPTY_SYM : thm
    val FDOM_EQ_FDOM_FUPDATE : thm
    val FDOM_FDIFF : thm
    val FDOM_FEMPTY : thm
    val FDOM_FINITE : thm
    val FDOM_FMAP : thm
    val FDOM_FMERGE : thm
    val FDOM_FOLDR_DOMSUB : thm
    val FDOM_FUNION : thm
    val FDOM_FUPDATE : thm
    val FDOM_FUPDATE_LIST : thm
    val FDOM_F_FEMPTY1 : thm
    val FDOM_f_o : thm
    val FDOM_o_f : thm
    val FEMPTY_FUPDATE_EQ : thm
    val FEMPTY_SUBMAP : thm
    val FEVERY_ALL_FLOOKUP : thm
    val FEVERY_DRESTRICT_COMPL : thm
    val FEVERY_FEMPTY : thm
    val FEVERY_FLOOKUP : thm
    val FEVERY_FUPDATE : thm
    val FEVERY_FUPDATE_LIST : thm
    val FEVERY_STRENGTHEN_THM : thm
    val FEVERY_SUBMAP : thm
    val FEVERY_o_f : thm
    val FINITE_FRANGE : thm
    val FINITE_PRED_11 : thm
    val FLOOKUP_DRESTRICT : thm
    val FLOOKUP_EMPTY : thm
    val FLOOKUP_EXT : thm
    val FLOOKUP_FOLDR_UPDATE : thm
    val FLOOKUP_FUNION : thm
    val FLOOKUP_FUN_FMAP : thm
    val FLOOKUP_MAP_KEYS : thm
    val FLOOKUP_MAP_KEYS_MAPPED : thm
    val FLOOKUP_SUBMAP : thm
    val FLOOKUP_UPDATE : thm
    val FLOOKUP_o_f : thm
    val FMAP_MAP2_FEMPTY : thm
    val FMAP_MAP2_FUPDATE : thm
    val FMAP_MAP2_THM : thm
    val FMEQ_ENUMERATE_CASES : thm
    val FMEQ_SINGLE_SIMPLE_DISJ_ELIM : thm
    val FMEQ_SINGLE_SIMPLE_ELIM : thm
    val FMERGE_ASSOC : thm
    val FMERGE_COMM : thm
    val FMERGE_DOMSUB : thm
    val FMERGE_DRESTRICT : thm
    val FMERGE_EQ_FEMPTY : thm
    val FMERGE_FEMPTY : thm
    val FMERGE_FUNION : thm
    val FMERGE_NO_CHANGE : thm
    val FM_PULL_APART : thm
    val FOLDL2_FUPDATE_LIST : thm
    val FOLDL2_FUPDATE_LIST_paired : thm
    val FOLDL_FUPDATE_LIST : thm
    val FRANGE_DOMSUB_SUBSET : thm
    val FRANGE_DRESTRICT_SUBSET : thm
    val FRANGE_FEMPTY : thm
    val FRANGE_FLOOKUP : thm
    val FRANGE_FMAP : thm
    val FRANGE_FUNION : thm
    val FRANGE_FUNION_SUBSET : thm
    val FRANGE_FUPDATE : thm
    val FRANGE_FUPDATE_DOMSUB : thm
    val FRANGE_FUPDATE_LIST_SUBSET : thm
    val FRANGE_FUPDATE_SUBSET : thm
    val FUNION_ASSOC : thm
    val FUNION_COMM : thm
    val FUNION_EQ : thm
    val FUNION_EQ_FEMPTY : thm
    val FUNION_EQ_IMPL : thm
    val FUNION_FEMPTY_1 : thm
    val FUNION_FEMPTY_2 : thm
    val FUNION_FMERGE : thm
    val FUNION_FUPDATE_1 : thm
    val FUNION_FUPDATE_2 : thm
    val FUNION_IDEMPOT : thm
    val FUN_FMAP_EMPTY : thm
    val FUPD11_SAME_BASE : thm
    val FUPD11_SAME_KEY_AND_BASE : thm
    val FUPD11_SAME_NEW_KEY : thm
    val FUPD11_SAME_UPDATE : thm
    val FUPDATE_COMMUTES : thm
    val FUPDATE_DRESTRICT : thm
    val FUPDATE_ELIM : thm
    val FUPDATE_EQ : thm
    val FUPDATE_EQ_FUNION : thm
    val FUPDATE_EQ_FUPDATE_LIST : thm
    val FUPDATE_FUPDATE_LIST_COMMUTES : thm
    val FUPDATE_FUPDATE_LIST_MEM : thm
    val FUPDATE_LIST_ALL_DISTINCT_APPLY_MEM : thm
    val FUPDATE_LIST_ALL_DISTINCT_PERM : thm
    val FUPDATE_LIST_ALL_DISTINCT_REVERSE : thm
    val FUPDATE_LIST_APPEND : thm
    val FUPDATE_LIST_APPEND_COMMUTES : thm
    val FUPDATE_LIST_APPLY_HO_THM : thm
    val FUPDATE_LIST_APPLY_MEM : thm
    val FUPDATE_LIST_APPLY_NOT_MEM : thm
    val FUPDATE_LIST_APPLY_NOT_MEM_matchable : thm
    val FUPDATE_LIST_CANCEL : thm
    val FUPDATE_LIST_EQ_FEMPTY : thm
    val FUPDATE_LIST_SAME_KEYS_UNWIND : thm
    val FUPDATE_LIST_SAME_UPDATE : thm
    val FUPDATE_LIST_SNOC : thm
    val FUPDATE_LIST_THM : thm
    val FUPDATE_PURGE : thm
    val FUPDATE_PURGE' : thm
    val FUPDATE_SAME_APPLY : thm
    val FUPDATE_SAME_LIST_APPLY : thm
    val FUPD_SAME_KEY_UNWIND : thm
    val IMAGE_FRANGE : thm
    val IN_FDOM_FOLDR_UNION : thm
    val IN_FRANGE : thm
    val IN_FRANGE_DOMSUB_suff : thm
    val IN_FRANGE_DRESTRICT_suff : thm
    val IN_FRANGE_FLOOKUP : thm
    val IN_FRANGE_FUNION_suff : thm
    val IN_FRANGE_FUPDATE_LIST_suff : thm
    val IN_FRANGE_FUPDATE_suff : thm
    val IN_FRANGE_o_f_suff : thm
    val ITFMAPR_FEMPTY : thm
    val ITFMAPR_cases : thm
    val ITFMAPR_ind : thm
    val ITFMAPR_rules : thm
    val ITFMAPR_strongind : thm
    val ITFMAPR_total : thm
    val ITFMAPR_unique : thm
    val ITFMAP_FEMPTY : thm
    val ITFMAP_thm : thm
    val LEAST_NOTIN_FDOM : thm
    val MAP_KEYS_BIJ_LINV : thm
    val MAP_KEYS_FEMPTY : thm
    val MAP_KEYS_FUPDATE : thm
    val MAP_KEYS_using_LINV : thm
    val MAP_KEYS_witness : thm
    val NOT_EQ_FAPPLY : thm
    val NOT_EQ_FEMPTY_FUPDATE : thm
    val NOT_FDOM_DRESTRICT : thm
    val NOT_FDOM_FAPPLY_FEMPTY : thm
    val NUM_NOT_IN_FDOM : thm
    val RRESTRICT_FEMPTY : thm
    val RRESTRICT_FUPDATE : thm
    val SAME_KEY_UPDATES_DIFFER : thm
    val STRONG_DRESTRICT_FUPDATE : thm
    val STRONG_DRESTRICT_FUPDATE_THM : thm
    val SUBMAP_ANTISYM : thm
    val SUBMAP_DOMSUB : thm
    val SUBMAP_DOMSUB_gen : thm
    val SUBMAP_DRESTRICT : thm
    val SUBMAP_DRESTRICT_MONOTONE : thm
    val SUBMAP_FDOM_SUBSET : thm
    val SUBMAP_FEMPTY : thm
    val SUBMAP_FLOOKUP_EQN : thm
    val SUBMAP_FRANGE : thm
    val SUBMAP_FUNION : thm
    val SUBMAP_FUNION_ABSORPTION : thm
    val SUBMAP_FUNION_EQ : thm
    val SUBMAP_FUNION_ID : thm
    val SUBMAP_FUPDATE : thm
    val SUBMAP_FUPDATE_EQN : thm
    val SUBMAP_FUPDATE_FLOOKUP : thm
    val SUBMAP_REFL : thm
    val SUBMAP_TRANS : thm
    val SUBMAP_mono_FUPDATE : thm
    val WF_lbound_inv_SUBSET : thm
    val disjoint_drestrict : thm
    val drestrict_iter_list : thm
    val f_o_ASSOC : thm
    val f_o_FEMPTY : thm
    val f_o_FUPDATE : thm
    val f_o_f_FEMPTY_1 : thm
    val f_o_f_FEMPTY_2 : thm
    val f_o_f_FUPDATE_compose : thm
    val fdom_fupdate_list2 : thm
    val fevery_funion : thm
    val flookup_thm : thm
    val fmap_CASES : thm
    val fmap_EQ : thm
    val fmap_EQ_THM : thm
    val fmap_EQ_UPTO___EMPTY : thm
    val fmap_EQ_UPTO___EQ : thm
    val fmap_EQ_UPTO___FUPDATE_BOTH : thm
    val fmap_EQ_UPTO___FUPDATE_BOTH___NO_DELETE : thm
    val fmap_EQ_UPTO___FUPDATE_SING : thm
    val fmap_EXT : thm
    val fmap_INDUCT : thm
    val fmap_SIMPLE_INDUCT : thm
    val fmap_cases_NOTIN : thm
    val fmap_eq_flookup : thm
    val fmap_rel_FEMPTY : thm
    val fmap_rel_FEMPTY2 : thm
    val fmap_rel_FLOOKUP_imp : thm
    val fmap_rel_FUNION_rels : thm
    val fmap_rel_FUPDATE_I : thm
    val fmap_rel_FUPDATE_LIST_same : thm
    val fmap_rel_FUPDATE_same : thm
    val fmap_rel_OPTREL_FLOOKUP : thm
    val fmap_rel_mono : thm
    val fmap_rel_refl : thm
    val fmap_rel_sym : thm
    val fmap_rel_trans : thm
    val fmap_to_list : thm
    val fmlfpR_cases : thm
    val fmlfpR_ind : thm
    val fmlfpR_lastpass : thm
    val fmlfpR_rules : thm
    val fmlfpR_strongind : thm
    val fmlfpR_total : thm
    val fmlfpR_total_lemma : thm
    val fp_soluble_FOLDR1 : thm
    val fupdate_list_foldl : thm
    val fupdate_list_foldr : thm
    val fupdate_list_map : thm
    val is_fmap_cases : thm
    val is_fmap_ind : thm
    val is_fmap_rules : thm
    val is_fmap_strongind : thm
    val o_f_DOMSUB : thm
    val o_f_FAPPLY : thm
    val o_f_FDOM : thm
    val o_f_FEMPTY : thm
    val o_f_FRANGE : thm
    val o_f_FUNION : thm
    val o_f_FUPDATE : thm
    val o_f_cong : thm
    val o_f_id : thm
    val o_f_o_f : thm
  
  val finite_map_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [sorting] Parent theory of "finite_map"
   
   [DRESTRICT_DEF]  Definition
      
      ⊢ ∀f r.
          FDOM (DRESTRICT f r) = FDOM f ∩ r ∧
          ∀x. DRESTRICT f r ' x =
              if x ∈ FDOM f ∩ r then f ' x else FEMPTY ' x
   
   [FAPPLY_DEF]  Definition
      
      ⊢ ∀f x. f ' x = OUTL (fmap_REP f x)
   
   [FCARD_DEF]  Definition
      
      ⊢ ∀fm. FCARD fm = CARD (FDOM fm)
   
   [FDIFF_def]  Definition
      
      ⊢ ∀f1 s. FDIFF f1 s = DRESTRICT f1 (COMPL s)
   
   [FDOM_DEF]  Definition
      
      ⊢ ∀f x. FDOM f x ⇔ ISL (fmap_REP f x)
   
   [FEMPTY_DEF]  Definition
      
      ⊢ FEMPTY = fmap_ABS (λa. INR ())
   
   [FEVERY_DEF]  Definition
      
      ⊢ ∀P f. FEVERY P f ⇔ ∀x. x ∈ FDOM f ⇒ P (x,f ' x)
   
   [FLOOKUP_DEF]  Definition
      
      ⊢ ∀f x. FLOOKUP f x = if x ∈ FDOM f then SOME (f ' x) else NONE
   
   [FMAP_MAP2_def]  Definition
      
      ⊢ ∀f m. FMAP_MAP2 f m = FUN_FMAP (λx. f (x,m ' x)) (FDOM m)
   
   [FMERGE_DEF]  Definition
      
      ⊢ ∀m f g.
          FDOM (FMERGE m f g) = FDOM f ∪ FDOM g ∧
          ∀x. FMERGE m f g ' x =
              if x ∉ FDOM f then g ' x
              else if x ∉ FDOM g then f ' x
              else m (f ' x) (g ' x)
   
   [FRANGE_DEF]  Definition
      
      ⊢ ∀f. FRANGE f = {y | ∃x. x ∈ FDOM f ∧ f ' x = y}
   
   [FUNION_DEF]  Definition
      
      ⊢ ∀f g.
          FDOM (f ⊌ g) = FDOM f ∪ FDOM g ∧
          ∀x. (f ⊌ g) ' x = if x ∈ FDOM f then f ' x else g ' x
   
   [FUN_FMAP_DEF]  Definition
      
      ⊢ ∀f P.
          FINITE P ⇒
          FDOM (FUN_FMAP f P) = P ∧ ∀x. x ∈ P ⇒ FUN_FMAP f P ' x = f x
   
   [FUPDATE_DEF]  Definition
      
      ⊢ ∀f x y.
          f |+ (x,y) = fmap_ABS (λa. if a = x then INL y else fmap_REP f a)
   
   [FUPDATE_LIST]  Definition
      
      ⊢ $|++ = FOLDL $|+
   
   [ITFMAPR_def]  Definition
      
      ⊢ ITFMAPR =
        (λf a0 a1 a2.
             ∀ITFMAPR'.
               (∀a0 a1 a2.
                  a0 = FEMPTY ∧ a2 = a1 ∨
                  (∃A2 k v fm.
                     a0 = fm |+ (k,v) ∧ a2 = f k v A2 ∧ k ∉ FDOM fm ∧
                     ITFMAPR' fm a1 A2) ⇒
                  ITFMAPR' a0 a1 a2) ⇒
               ITFMAPR' a0 a1 a2)
   
   [ITFMAP_def]  Definition
      
      ⊢ ∀f fm A0. ITFMAP f fm A0 = @A. ITFMAPR f fm A0 A
   
   [MAP_KEYS_def]  Definition
      
      ⊢ ∀f fm.
          FDOM (MAP_KEYS f fm) = IMAGE f (FDOM fm) ∧
          (INJ f (FDOM fm) 𝕌(:β) ⇒
           ∀x. x ∈ FDOM fm ⇒ MAP_KEYS f fm ' (f x) = fm ' x)
   
   [RRESTRICT_DEF]  Definition
      
      ⊢ ∀f r.
          FDOM (RRESTRICT f r) = {x | x ∈ FDOM f ∧ f ' x ∈ r} ∧
          ∀x. RRESTRICT f r ' x =
              if x ∈ FDOM f ∧ f ' x ∈ r then f ' x else FEMPTY ' x
   
   [SUBMAP_DEF]  Definition
      
      ⊢ ∀f g. f ⊑ g ⇔ ∀x. x ∈ FDOM f ⇒ x ∈ FDOM g ∧ f ' x = g ' x
   
   [f_o_DEF]  Definition
      
      ⊢ ∀f g. f f_o g = f f_o_f FUN_FMAP g {x | g x ∈ FDOM f}
   
   [f_o_f_DEF]  Definition
      
      ⊢ ∀f g.
          FDOM (f f_o_f g) = FDOM g ∩ {x | g ' x ∈ FDOM f} ∧
          ∀x. x ∈ FDOM (f f_o_f g) ⇒ (f f_o_f g) ' x = f ' (g ' x)
   
   [fmap_EQ_UPTO_def]  Definition
      
      ⊢ ∀f1 f2 vs.
          fmap_EQ_UPTO f1 f2 vs ⇔
          FDOM f1 ∩ COMPL vs = FDOM f2 ∩ COMPL vs ∧
          ∀x. x ∈ FDOM f1 ∩ COMPL vs ⇒ f1 ' x = f2 ' x
   
   [fmap_ISO_DEF]  Definition
      
      ⊢ (∀a. fmap_ABS (fmap_REP a) = a) ∧
        ∀r. is_fmap r ⇔ fmap_REP (fmap_ABS r) = r
   
   [fmap_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION is_fmap rep
   
   [fmap_domsub]  Definition
      
      ⊢ ∀fm k. fm \\ k = DRESTRICT fm (COMPL {k})
   
   [fmap_inverse_def]  Definition
      
      ⊢ ∀m1 m2.
          fmap_inverse m1 m2 ⇔
          ∀k. k ∈ FDOM m1 ⇒
              ∃v. FLOOKUP m1 k = SOME v ∧ FLOOKUP m2 v = SOME k
   
   [fmap_rel_def]  Definition
      
      ⊢ ∀R f1 f2.
          fmap_rel R f1 f2 ⇔
          FDOM f2 = FDOM f1 ∧ ∀x. x ∈ FDOM f1 ⇒ R (f1 ' x) (f2 ' x)
   
   [fmap_size_def]  Definition
      
      ⊢ ∀kz vz fm.
          fmap_size kz vz fm = ∑ (λk. kz k + vz (fm ' k)) (FDOM fm)
   
   [fmlfpR_def]  Definition
      
      ⊢ fmlfpR =
        (λf fm0 a0 a1 a2 a3.
             ∀fmlfpR'.
               (∀a0 a1 a2 a3.
                  a1 = FEMPTY ∧ a3 = a0 ∧ a0 = a2 ∨
                  a1 = FEMPTY ∧ fmlfpR' a2 fm0 a2 a3 ∧ a0 ≠ a2 ∨
                  (∃fm k v.
                     a1 = fm |+ (k,v) ∧ fmlfpR' a0 (fm \\ k) (f k v a2) a3) ⇒
                  fmlfpR' a0 a1 a2 a3) ⇒
               fmlfpR' a0 a1 a2 a3)
   
   [fp_soluble_def]  Definition
      
      ⊢ ∀R P fm f.
          fp_soluble R P fm f ⇔
          transitive R ∧ WF (lbound P Rᵀ) ∧
          (∀k v A.
             FLOOKUP fm k = SOME v ∧ RC R A P ⇒
             RC R A (f k v A) ∧ RC R (f k v A) P) ∧
          ∀A. R A P ⇒ ∃k v. FLOOKUP fm k = SOME v ∧ f k v A ≠ A
   
   [is_fmap_def]  Definition
      
      ⊢ is_fmap =
        (λa0.
             ∀is_fmap'.
               (∀a0.
                  a0 = (λa. INR ()) ∨
                  (∃f a b.
                     a0 = (λx. if x = a then INL b else f x) ∧ is_fmap' f) ⇒
                  is_fmap' a0) ⇒
               is_fmap' a0)
   
   [lbound_def]  Definition
      
      ⊢ ∀l R x y. lbound l R x y ⇔ R꙳ l x ∧ R꙳ l y ∧ R x y
   
   [o_f_DEF]  Definition
      
      ⊢ ∀f g.
          FDOM (f o_f g) = FDOM g ∧
          ∀x. x ∈ FDOM (f o_f g) ⇒ (f o_f g) ' x = f (g ' x)
   
   [DISJOINT_FEVERY_FUNION]  Theorem
      
      ⊢ DISJOINT (FDOM m1) (FDOM m2) ⇒
        (FEVERY P (m1 ⊌ m2) ⇔ FEVERY P m1 ∧ FEVERY P m2)
   
   [DOMSUB_COMMUTES]  Theorem
      
      ⊢ fm \\ k1 \\ k2 = fm \\ k2 \\ k1
   
   [DOMSUB_FAPPLY]  Theorem
      
      ⊢ ∀fm k. (fm \\ k) ' k = FEMPTY ' k
   
   [DOMSUB_FAPPLY_NEQ]  Theorem
      
      ⊢ ∀fm k1 k2. k1 ≠ k2 ⇒ (fm \\ k1) ' k2 = fm ' k2
   
   [DOMSUB_FAPPLY_THM]  Theorem
      
      ⊢ ∀fm k1 k2.
          (fm \\ k1) ' k2 = if k1 = k2 then FEMPTY ' k2 else fm ' k2
   
   [DOMSUB_FEMPTY]  Theorem
      
      ⊢ ∀k. FEMPTY \\ k = FEMPTY
   
   [DOMSUB_FLOOKUP]  Theorem
      
      ⊢ ∀fm k. FLOOKUP (fm \\ k) k = NONE
   
   [DOMSUB_FLOOKUP_NEQ]  Theorem
      
      ⊢ ∀fm k1 k2. k1 ≠ k2 ⇒ FLOOKUP (fm \\ k1) k2 = FLOOKUP fm k2
   
   [DOMSUB_FLOOKUP_THM]  Theorem
      
      ⊢ ∀fm k1 k2.
          FLOOKUP (fm \\ k1) k2 = if k1 = k2 then NONE else FLOOKUP fm k2
   
   [DOMSUB_FUNION]  Theorem
      
      ⊢ (f ⊌ g) \\ k = f \\ k ⊌ g \\ k
   
   [DOMSUB_FUPDATE]  Theorem
      
      ⊢ ∀fm k v. fm |+ (k,v) \\ k = fm \\ k
   
   [DOMSUB_FUPDATE_NEQ]  Theorem
      
      ⊢ ∀fm k1 k2 v. k1 ≠ k2 ⇒ fm |+ (k1,v) \\ k2 = fm \\ k2 |+ (k1,v)
   
   [DOMSUB_FUPDATE_THM]  Theorem
      
      ⊢ ∀fm k1 k2 v.
          fm |+ (k1,v) \\ k2 =
          if k1 = k2 then fm \\ k2 else fm \\ k2 |+ (k1,v)
   
   [DOMSUB_IDEM]  Theorem
      
      ⊢ fm \\ k \\ k = fm \\ k
   
   [DOMSUB_MAP_KEYS]  Theorem
      
      ⊢ BIJ f 𝕌(:α) 𝕌(:β) ⇒ MAP_KEYS f fm \\ f s = MAP_KEYS f (fm \\ s)
   
   [DOMSUB_NOT_IN_DOM]  Theorem
      
      ⊢ k ∉ FDOM fm ⇒ fm \\ k = fm
   
   [DOMSUB_SUBMAP]  Theorem
      
      ⊢ ∀f g x. f ⊑ g ∧ x ∉ FDOM f ⇒ f ⊑ g \\ x
   
   [DRESTRICTED_FUNION]  Theorem
      
      ⊢ ∀f1 f2 s.
          DRESTRICT (f1 ⊌ f2) s =
          DRESTRICT f1 s ⊌ DRESTRICT f2 (s DIFF FDOM f1)
   
   [DRESTRICT_DOMSUB]  Theorem
      
      ⊢ ∀f s k. DRESTRICT f s \\ k = DRESTRICT f (s DELETE k)
   
   [DRESTRICT_DRESTRICT]  Theorem
      
      ⊢ ∀f P Q. DRESTRICT (DRESTRICT f P) Q = DRESTRICT f (P ∩ Q)
   
   [DRESTRICT_EQ_DRESTRICT]  Theorem
      
      ⊢ ∀f1 f2 s1 s2.
          DRESTRICT f1 s1 = DRESTRICT f2 s2 ⇔
          DRESTRICT f1 s1 ⊑ f2 ∧ DRESTRICT f2 s2 ⊑ f1 ∧
          s1 ∩ FDOM f1 = s2 ∩ FDOM f2
   
   [DRESTRICT_EQ_DRESTRICT_SAME]  Theorem
      
      ⊢ DRESTRICT f1 s = DRESTRICT f2 s ⇔
        s ∩ FDOM f1 = s ∩ FDOM f2 ∧
        ∀x. x ∈ FDOM f1 ∧ x ∈ s ⇒ f1 ' x = f2 ' x
   
   [DRESTRICT_EQ_FUNION]  Theorem
      
      ⊢ ∀h h1 h2.
          DISJOINT (FDOM h1) (FDOM h2) ∧ h1 ⊌ h2 = h ⇒
          h2 = DRESTRICT h (COMPL (FDOM h1))
   
   [DRESTRICT_FDOM]  Theorem
      
      ⊢ ∀f. DRESTRICT f (FDOM f) = f
   
   [DRESTRICT_FEMPTY]  Theorem
      
      ⊢ ∀r. DRESTRICT FEMPTY r = FEMPTY
   
   [DRESTRICT_FUNION]  Theorem
      
      ⊢ ∀h s1 s2. DRESTRICT h s1 ⊌ DRESTRICT h s2 = DRESTRICT h (s1 ∪ s2)
   
   [DRESTRICT_FUNION_DRESTRICT_COMPL]  Theorem
      
      ⊢ DRESTRICT f s ⊌ DRESTRICT f (COMPL s) = f
   
   [DRESTRICT_FUNION_SAME]  Theorem
      
      ⊢ ∀fm s. DRESTRICT fm s ⊌ fm = fm
   
   [DRESTRICT_FUNION_SUBSET]  Theorem
      
      ⊢ s2 ⊆ s1 ⇒ ∃h. DRESTRICT f s1 ⊌ g = DRESTRICT f s2 ⊌ h
   
   [DRESTRICT_FUPDATE]  Theorem
      
      ⊢ ∀f r x y.
          DRESTRICT (f |+ (x,y)) r =
          if x ∈ r then DRESTRICT f r |+ (x,y) else DRESTRICT f r
   
   [DRESTRICT_IDEMPOT]  Theorem
      
      ⊢ ∀s vs. DRESTRICT (DRESTRICT s vs) vs = DRESTRICT s vs
   
   [DRESTRICT_IS_FEMPTY]  Theorem
      
      ⊢ ∀f. DRESTRICT f ∅ = FEMPTY
   
   [DRESTRICT_MAP_KEYS_IMAGE]  Theorem
      
      ⊢ INJ f 𝕌(:α) 𝕌(:β) ⇒
        DRESTRICT (MAP_KEYS f fm) (IMAGE f s) = MAP_KEYS f (DRESTRICT fm s)
   
   [DRESTRICT_SUBMAP]  Theorem
      
      ⊢ ∀f r. DRESTRICT f r ⊑ f
   
   [DRESTRICT_SUBMAP_gen]  Theorem
      
      ⊢ f ⊑ g ⇒ DRESTRICT f P ⊑ g
   
   [DRESTRICT_SUBSET]  Theorem
      
      ⊢ ∀f1 f2 s t.
          DRESTRICT f1 s = DRESTRICT f2 s ∧ t ⊆ s ⇒
          DRESTRICT f1 t = DRESTRICT f2 t
   
   [DRESTRICT_SUBSET_SUBMAP]  Theorem
      
      ⊢ s1 ⊆ s2 ⇒ DRESTRICT f s1 ⊑ DRESTRICT f s2
   
   [DRESTRICT_SUBSET_SUBMAP_gen]  Theorem
      
      ⊢ ∀f1 f2 s t.
          DRESTRICT f1 s ⊑ DRESTRICT f2 s ∧ t ⊆ s ⇒
          DRESTRICT f1 t ⊑ DRESTRICT f2 t
   
   [DRESTRICT_UNIV]  Theorem
      
      ⊢ ∀f. DRESTRICT f 𝕌(:α) = f
   
   [EQ_FDOM_SUBMAP]  Theorem
      
      ⊢ f = g ⇔ f ⊑ g ∧ FDOM f = FDOM g
   
   [FAPPLY_FUPDATE]  Theorem
      
      ⊢ ∀f x y. (f |+ (x,y)) ' x = y
   
   [FAPPLY_FUPDATE_THM]  Theorem
      
      ⊢ ∀f a b x. (f |+ (a,b)) ' x = if x = a then b else f ' x
   
   [FAPPLY_f_o]  Theorem
      
      ⊢ ∀f g.
          FINITE {x | g x ∈ FDOM f} ⇒
          ∀x. x ∈ FDOM (f f_o g) ⇒ (f f_o g) ' x = f ' (g x)
   
   [FCARD_0_FEMPTY]  Theorem
      
      ⊢ ∀f. FCARD f = 0 ⇔ f = FEMPTY
   
   [FCARD_FEMPTY]  Theorem
      
      ⊢ FCARD FEMPTY = 0
   
   [FCARD_FUPDATE]  Theorem
      
      ⊢ ∀fm a b.
          FCARD (fm |+ (a,b)) =
          if a ∈ FDOM fm then FCARD fm else 1 + FCARD fm
   
   [FCARD_SUC]  Theorem
      
      ⊢ ∀f n.
          FCARD f = SUC n ⇔
          ∃f' x y. x ∉ FDOM f' ∧ FCARD f' = n ∧ f = f' |+ (x,y)
   
   [FDOM_DOMSUB]  Theorem
      
      ⊢ ∀fm k. FDOM (fm \\ k) = FDOM fm DELETE k
   
   [FDOM_DRESTRICT]  Theorem
      
      ⊢ ∀f r x. FDOM (DRESTRICT f r) = FDOM f ∩ r
   
   [FDOM_EQ_EMPTY]  Theorem
      
      ⊢ ∀f. FDOM f = ∅ ⇔ f = FEMPTY
   
   [FDOM_EQ_EMPTY_SYM]  Theorem
      
      ⊢ ∀f. ∅ = FDOM f ⇔ f = FEMPTY
   
   [FDOM_EQ_FDOM_FUPDATE]  Theorem
      
      ⊢ ∀f x. x ∈ FDOM f ⇒ ∀y. FDOM (f |+ (x,y)) = FDOM f
   
   [FDOM_FDIFF]  Theorem
      
      ⊢ x ∈ FDOM (FDIFF refs f2) ⇔ x ∈ FDOM refs ∧ x ∉ f2
   
   [FDOM_FEMPTY]  Theorem
      
      ⊢ FDOM FEMPTY = ∅
   
   [FDOM_FINITE]  Theorem
      
      ⊢ ∀fm. FINITE (FDOM fm)
   
   [FDOM_FMAP]  Theorem
      
      ⊢ ∀f s. FINITE s ⇒ FDOM (FUN_FMAP f s) = s
   
   [FDOM_FMERGE]  Theorem
      
      ⊢ ∀m f g. FDOM (FMERGE m f g) = FDOM f ∪ FDOM g
   
   [FDOM_FOLDR_DOMSUB]  Theorem
      
      ⊢ ∀ls fm. FDOM (FOLDR (λk m. m \\ k) fm ls) = FDOM fm DIFF set ls
   
   [FDOM_FUNION]  Theorem
      
      ⊢ FDOM (f ⊌ g) = FDOM f ∪ FDOM g
   
   [FDOM_FUPDATE]  Theorem
      
      ⊢ ∀f a b. FDOM (f |+ (a,b)) = a INSERT FDOM f
   
   [FDOM_FUPDATE_LIST]  Theorem
      
      ⊢ ∀kvl fm. FDOM (fm |++ kvl) = FDOM fm ∪ set (MAP FST kvl)
   
   [FDOM_F_FEMPTY1]  Theorem
      
      ⊢ ∀f. (∀a. a ∉ FDOM f) ⇔ f = FEMPTY
   
   [FDOM_f_o]  Theorem
      
      ⊢ ∀f g.
          FINITE {x | g x ∈ FDOM f} ⇒ FDOM (f f_o g) = {x | g x ∈ FDOM f}
   
   [FDOM_o_f]  Theorem
      
      ⊢ ∀f g. FDOM (f o_f g) = FDOM g
   
   [FEMPTY_FUPDATE_EQ]  Theorem
      
      ⊢ ∀x y. FEMPTY |+ x = FEMPTY |+ y ⇔ x = y
   
   [FEMPTY_SUBMAP]  Theorem
      
      ⊢ ∀h. h ⊑ FEMPTY ⇔ h = FEMPTY
   
   [FEVERY_ALL_FLOOKUP]  Theorem
      
      ⊢ ∀P f. FEVERY P f ⇔ ∀k v. FLOOKUP f k = SOME v ⇒ P (k,v)
   
   [FEVERY_DRESTRICT_COMPL]  Theorem
      
      ⊢ FEVERY P (DRESTRICT (f |+ (k,v)) (COMPL s)) ⇔
        (k ∉ s ⇒ P (k,v)) ∧ FEVERY P (DRESTRICT f (COMPL (k INSERT s)))
   
   [FEVERY_FEMPTY]  Theorem
      
      ⊢ ∀P. FEVERY P FEMPTY
   
   [FEVERY_FLOOKUP]  Theorem
      
      ⊢ FEVERY P f ∧ FLOOKUP f k = SOME v ⇒ P (k,v)
   
   [FEVERY_FUPDATE]  Theorem
      
      ⊢ ∀P f x y.
          FEVERY P (f |+ (x,y)) ⇔
          P (x,y) ∧ FEVERY P (DRESTRICT f (COMPL {x}))
   
   [FEVERY_FUPDATE_LIST]  Theorem
      
      ⊢ ALL_DISTINCT (MAP FST kvl) ⇒
        (FEVERY P (fm |++ kvl) ⇔
         EVERY P kvl ∧ FEVERY P (DRESTRICT fm (COMPL (set (MAP FST kvl)))))
   
   [FEVERY_STRENGTHEN_THM]  Theorem
      
      ⊢ FEVERY P FEMPTY ∧ (FEVERY P f ∧ P (x,y) ⇒ FEVERY P (f |+ (x,y)))
   
   [FEVERY_SUBMAP]  Theorem
      
      ⊢ FEVERY P fm ∧ fm0 ⊑ fm ⇒ FEVERY P fm0
   
   [FEVERY_o_f]  Theorem
      
      ⊢ ∀m P f. FEVERY P (f o_f m) ⇔ FEVERY (λx. P (FST x,f (SND x))) m
   
   [FINITE_FRANGE]  Theorem
      
      ⊢ ∀fm. FINITE (FRANGE fm)
   
   [FINITE_PRED_11]  Theorem
      
      ⊢ ∀g. (∀x y. g x = g y ⇔ x = y) ⇒ ∀f. FINITE {x | g x ∈ FDOM f}
   
   [FLOOKUP_DRESTRICT]  Theorem
      
      ⊢ ∀fm s k.
          FLOOKUP (DRESTRICT fm s) k = if k ∈ s then FLOOKUP fm k else NONE
   
   [FLOOKUP_EMPTY]  Theorem
      
      ⊢ FLOOKUP FEMPTY k = NONE
   
   [FLOOKUP_EXT]  Theorem
      
      ⊢ f1 = f2 ⇔ FLOOKUP f1 = FLOOKUP f2
   
   [FLOOKUP_FOLDR_UPDATE]  Theorem
      
      ⊢ ALL_DISTINCT (MAP FST kvl) ∧ DISJOINT (set (MAP FST kvl)) (FDOM fm) ⇒
        (FLOOKUP (FOLDR (flip $|+) fm kvl) k = SOME v ⇔
         MEM (k,v) kvl ∨ FLOOKUP fm k = SOME v)
   
   [FLOOKUP_FUNION]  Theorem
      
      ⊢ FLOOKUP (f1 ⊌ f2) k =
        case FLOOKUP f1 k of NONE => FLOOKUP f2 k | SOME v => SOME v
   
   [FLOOKUP_FUN_FMAP]  Theorem
      
      ⊢ FINITE P ⇒
        FLOOKUP (FUN_FMAP f P) k = if k ∈ P then SOME (f k) else NONE
   
   [FLOOKUP_MAP_KEYS]  Theorem
      
      ⊢ INJ f (FDOM m) 𝕌(:β) ⇒
        FLOOKUP (MAP_KEYS f m) k =
        OPTION_BIND (some x. k = f x ∧ x ∈ FDOM m) (FLOOKUP m)
   
   [FLOOKUP_MAP_KEYS_MAPPED]  Theorem
      
      ⊢ INJ f 𝕌(:α) 𝕌(:β) ⇒ FLOOKUP (MAP_KEYS f m) (f k) = FLOOKUP m k
   
   [FLOOKUP_SUBMAP]  Theorem
      
      ⊢ f ⊑ g ∧ FLOOKUP f k = SOME v ⇒ FLOOKUP g k = SOME v
   
   [FLOOKUP_UPDATE]  Theorem
      
      ⊢ FLOOKUP (fm |+ (k1,v)) k2 =
        if k1 = k2 then SOME v else FLOOKUP fm k2
   
   [FLOOKUP_o_f]  Theorem
      
      ⊢ FLOOKUP (f o_f fm) k =
        case FLOOKUP fm k of NONE => NONE | SOME v => SOME (f v)
   
   [FMAP_MAP2_FEMPTY]  Theorem
      
      ⊢ FMAP_MAP2 f FEMPTY = FEMPTY
   
   [FMAP_MAP2_FUPDATE]  Theorem
      
      ⊢ FMAP_MAP2 f (m |+ (x,v)) = FMAP_MAP2 f m |+ (x,f (x,v))
   
   [FMAP_MAP2_THM]  Theorem
      
      ⊢ FDOM (FMAP_MAP2 f m) = FDOM m ∧
        ∀x. x ∈ FDOM m ⇒ FMAP_MAP2 f m ' x = f (x,m ' x)
   
   [FMEQ_ENUMERATE_CASES]  Theorem
      
      ⊢ ∀f1 kvl p. f1 |+ p = FEMPTY |++ kvl ⇒ MEM p kvl
   
   [FMEQ_SINGLE_SIMPLE_DISJ_ELIM]  Theorem
      
      ⊢ ∀fm k v ck cv.
          fm |+ (k,v) = FEMPTY |+ (ck,cv) ⇔
          k = ck ∧ v = cv ∧ (fm = FEMPTY ∨ ∃v'. fm = FEMPTY |+ (k,v'))
   
   [FMEQ_SINGLE_SIMPLE_ELIM]  Theorem
      
      ⊢ ∀P k v ck cv nv.
          (∃fm. fm |+ (k,v) = FEMPTY |+ (ck,cv) ∧ P (fm |+ (k,nv))) ⇔
          k = ck ∧ v = cv ∧ P (FEMPTY |+ (ck,nv))
   
   [FMERGE_ASSOC]  Theorem
      
      ⊢ ASSOC (FMERGE m) ⇔ ASSOC m
   
   [FMERGE_COMM]  Theorem
      
      ⊢ COMM (FMERGE m) ⇔ COMM m
   
   [FMERGE_DOMSUB]  Theorem
      
      ⊢ ∀m m1 m2 k. FMERGE m m1 m2 \\ k = FMERGE m (m1 \\ k) (m2 \\ k)
   
   [FMERGE_DRESTRICT]  Theorem
      
      ⊢ DRESTRICT (FMERGE f st1 st2) vs =
        FMERGE f (DRESTRICT st1 vs) (DRESTRICT st2 vs)
   
   [FMERGE_EQ_FEMPTY]  Theorem
      
      ⊢ FMERGE m f g = FEMPTY ⇔ f = FEMPTY ∧ g = FEMPTY
   
   [FMERGE_FEMPTY]  Theorem
      
      ⊢ FMERGE m f FEMPTY = f ∧ FMERGE m FEMPTY f = f
   
   [FMERGE_FUNION]  Theorem
      
      ⊢ FUNION = FMERGE (λx y. x)
   
   [FMERGE_NO_CHANGE]  Theorem
      
      ⊢ (FMERGE m f1 f2 = f1 ⇔
         ∀x. x ∈ FDOM f2 ⇒ x ∈ FDOM f1 ∧ m (f1 ' x) (f2 ' x) = f1 ' x) ∧
        (FMERGE m f1 f2 = f2 ⇔
         ∀x. x ∈ FDOM f1 ⇒ x ∈ FDOM f2 ∧ m (f1 ' x) (f2 ' x) = f2 ' x)
   
   [FM_PULL_APART]  Theorem
      
      ⊢ ∀fm k. k ∈ FDOM fm ⇒ ∃fm0 v. fm = fm0 |+ (k,v) ∧ k ∉ FDOM fm0
   
   [FOLDL2_FUPDATE_LIST]  Theorem
      
      ⊢ ∀f1 f2 bs cs a.
          LENGTH bs = LENGTH cs ⇒
          FOLDL2 (λfm b c. fm |+ (f1 b c,f2 b c)) a bs cs =
          a |++ ZIP (MAP2 f1 bs cs,MAP2 f2 bs cs)
   
   [FOLDL2_FUPDATE_LIST_paired]  Theorem
      
      ⊢ ∀f1 f2 bs cs a.
          LENGTH bs = LENGTH cs ⇒
          FOLDL2 (λfm b (c,d). fm |+ (f1 b c d,f2 b c d)) a bs cs =
          a |++
          ZIP
            (MAP2 (λb. UNCURRY (f1 b)) bs cs,
             MAP2 (λb. UNCURRY (f2 b)) bs cs)
   
   [FOLDL_FUPDATE_LIST]  Theorem
      
      ⊢ ∀f1 f2 ls a.
          FOLDL (λfm k. fm |+ (f1 k,f2 k)) a ls =
          a |++ MAP (λk. (f1 k,f2 k)) ls
   
   [FRANGE_DOMSUB_SUBSET]  Theorem
      
      ⊢ FRANGE (fm \\ k) ⊆ FRANGE fm
   
   [FRANGE_DRESTRICT_SUBSET]  Theorem
      
      ⊢ FRANGE (DRESTRICT fm s) ⊆ FRANGE fm
   
   [FRANGE_FEMPTY]  Theorem
      
      ⊢ FRANGE FEMPTY = ∅
   
   [FRANGE_FLOOKUP]  Theorem
      
      ⊢ v ∈ FRANGE f ⇔ ∃k. FLOOKUP f k = SOME v
   
   [FRANGE_FMAP]  Theorem
      
      ⊢ FINITE P ⇒ FRANGE (FUN_FMAP f P) = IMAGE f P
   
   [FRANGE_FUNION]  Theorem
      
      ⊢ DISJOINT (FDOM fm1) (FDOM fm2) ⇒
        FRANGE (fm1 ⊌ fm2) = FRANGE fm1 ∪ FRANGE fm2
   
   [FRANGE_FUNION_SUBSET]  Theorem
      
      ⊢ FRANGE (f1 ⊌ f2) ⊆ FRANGE f1 ∪ FRANGE f2
   
   [FRANGE_FUPDATE]  Theorem
      
      ⊢ ∀f x y.
          FRANGE (f |+ (x,y)) = y INSERT FRANGE (DRESTRICT f (COMPL {x}))
   
   [FRANGE_FUPDATE_DOMSUB]  Theorem
      
      ⊢ ∀fm k v. FRANGE (fm |+ (k,v)) = v INSERT FRANGE (fm \\ k)
   
   [FRANGE_FUPDATE_LIST_SUBSET]  Theorem
      
      ⊢ ∀ls fm. FRANGE (fm |++ ls) ⊆ FRANGE fm ∪ set (MAP SND ls)
   
   [FRANGE_FUPDATE_SUBSET]  Theorem
      
      ⊢ FRANGE (fm |+ kv) ⊆ FRANGE fm ∪ {SND kv}
   
   [FUNION_ASSOC]  Theorem
      
      ⊢ ∀f g h. f ⊌ (g ⊌ h) = f ⊌ g ⊌ h
   
   [FUNION_COMM]  Theorem
      
      ⊢ ∀f g. DISJOINT (FDOM f) (FDOM g) ⇒ f ⊌ g = g ⊌ f
   
   [FUNION_EQ]  Theorem
      
      ⊢ ∀f1 f2 f3.
          DISJOINT (FDOM f1) (FDOM f2) ∧ DISJOINT (FDOM f1) (FDOM f3) ⇒
          (f1 ⊌ f2 = f1 ⊌ f3 ⇔ f2 = f3)
   
   [FUNION_EQ_FEMPTY]  Theorem
      
      ⊢ ∀h1 h2. h1 ⊌ h2 = FEMPTY ⇔ h1 = FEMPTY ∧ h2 = FEMPTY
   
   [FUNION_EQ_IMPL]  Theorem
      
      ⊢ ∀f1 f2 f3.
          DISJOINT (FDOM f1) (FDOM f2) ∧ DISJOINT (FDOM f1) (FDOM f3) ∧
          f2 = f3 ⇒
          f1 ⊌ f2 = f1 ⊌ f3
   
   [FUNION_FEMPTY_1]  Theorem
      
      ⊢ ∀g. FEMPTY ⊌ g = g
   
   [FUNION_FEMPTY_2]  Theorem
      
      ⊢ ∀f. f ⊌ FEMPTY = f
   
   [FUNION_FMERGE]  Theorem
      
      ⊢ ∀f1 f2 m. DISJOINT (FDOM f1) (FDOM f2) ⇒ FMERGE m f1 f2 = f1 ⊌ f2
   
   [FUNION_FUPDATE_1]  Theorem
      
      ⊢ ∀f g x y. f |+ (x,y) ⊌ g = (f ⊌ g) |+ (x,y)
   
   [FUNION_FUPDATE_2]  Theorem
      
      ⊢ ∀f g x y.
          f ⊌ g |+ (x,y) = if x ∈ FDOM f then f ⊌ g else (f ⊌ g) |+ (x,y)
   
   [FUNION_IDEMPOT]  Theorem
      
      ⊢ fm ⊌ fm = fm
   
   [FUN_FMAP_EMPTY]  Theorem
      
      ⊢ FUN_FMAP f ∅ = FEMPTY
   
   [FUPD11_SAME_BASE]  Theorem
      
      ⊢ ∀f k1 v1 k2 v2.
          f |+ (k1,v1) = f |+ (k2,v2) ⇔
          k1 = k2 ∧ v1 = v2 ∨
          k1 ≠ k2 ∧ k1 ∈ FDOM f ∧ k2 ∈ FDOM f ∧ f |+ (k1,v1) = f ∧
          f |+ (k2,v2) = f
   
   [FUPD11_SAME_KEY_AND_BASE]  Theorem
      
      ⊢ ∀f k v1 v2. f |+ (k,v1) = f |+ (k,v2) ⇔ v1 = v2
   
   [FUPD11_SAME_NEW_KEY]  Theorem
      
      ⊢ ∀f1 f2 k v1 v2.
          k ∉ FDOM f1 ∧ k ∉ FDOM f2 ⇒
          (f1 |+ (k,v1) = f2 |+ (k,v2) ⇔ f1 = f2 ∧ v1 = v2)
   
   [FUPD11_SAME_UPDATE]  Theorem
      
      ⊢ ∀f1 f2 k v.
          f1 |+ (k,v) = f2 |+ (k,v) ⇔
          DRESTRICT f1 (COMPL {k}) = DRESTRICT f2 (COMPL {k})
   
   [FUPDATE_COMMUTES]  Theorem
      
      ⊢ ∀f a b c d. a ≠ c ⇒ f |+ (a,b) |+ (c,d) = f |+ (c,d) |+ (a,b)
   
   [FUPDATE_DRESTRICT]  Theorem
      
      ⊢ ∀f x y. f |+ (x,y) = DRESTRICT f (COMPL {x}) |+ (x,y)
   
   [FUPDATE_ELIM]  Theorem
      
      ⊢ ∀k v f. k ∈ FDOM f ∧ f ' k = v ⇒ f |+ (k,v) = f
   
   [FUPDATE_EQ]  Theorem
      
      ⊢ ∀f a b c. f |+ (a,b) |+ (a,c) = f |+ (a,c)
   
   [FUPDATE_EQ_FUNION]  Theorem
      
      ⊢ ∀fm kv. fm |+ kv = FEMPTY |+ kv ⊌ fm
   
   [FUPDATE_EQ_FUPDATE_LIST]  Theorem
      
      ⊢ ∀fm kv. fm |+ kv = fm |++ [kv]
   
   [FUPDATE_FUPDATE_LIST_COMMUTES]  Theorem
      
      ⊢ ¬MEM k (MAP FST kvl) ⇒ fm |+ (k,v) |++ kvl = (fm |++ kvl) |+ (k,v)
   
   [FUPDATE_FUPDATE_LIST_MEM]  Theorem
      
      ⊢ MEM k (MAP FST kvl) ⇒ fm |+ (k,v) |++ kvl = fm |++ kvl
   
   [FUPDATE_LIST_ALL_DISTINCT_APPLY_MEM]  Theorem
      
      ⊢ ∀P ls k v fm.
          ALL_DISTINCT (MAP FST ls) ∧ MEM (k,v) ls ∧ P v ⇒
          P ((fm |++ ls) ' k)
   
   [FUPDATE_LIST_ALL_DISTINCT_PERM]  Theorem
      
      ⊢ ∀ls ls' fm.
          ALL_DISTINCT (MAP FST ls) ∧ PERM ls ls' ⇒ fm |++ ls = fm |++ ls'
   
   [FUPDATE_LIST_ALL_DISTINCT_REVERSE]  Theorem
      
      ⊢ ∀ls. ALL_DISTINCT (MAP FST ls) ⇒ ∀fm. fm |++ REVERSE ls = fm |++ ls
   
   [FUPDATE_LIST_APPEND]  Theorem
      
      ⊢ fm |++ (kvl1 ⧺ kvl2) = fm |++ kvl1 |++ kvl2
   
   [FUPDATE_LIST_APPEND_COMMUTES]  Theorem
      
      ⊢ ∀l1 l2 fm.
          DISJOINT (set (MAP FST l1)) (set (MAP FST l2)) ⇒
          fm |++ l1 |++ l2 = fm |++ l2 |++ l1
   
   [FUPDATE_LIST_APPLY_HO_THM]  Theorem
      
      ⊢ ∀P f kvl k.
          (∃n. n < LENGTH kvl ∧ k = EL n (MAP FST kvl) ∧
               P (EL n (MAP SND kvl)) ∧
               ∀m. n < m ∧ m < LENGTH kvl ⇒ EL m (MAP FST kvl) ≠ k) ∨
          ¬MEM k (MAP FST kvl) ∧ P (f ' k) ⇒
          P ((f |++ kvl) ' k)
   
   [FUPDATE_LIST_APPLY_MEM]  Theorem
      
      ⊢ ∀kvl f k v n.
          n < LENGTH kvl ∧ k = EL n (MAP FST kvl) ∧
          v = EL n (MAP SND kvl) ∧
          (∀m. n < m ∧ m < LENGTH kvl ⇒ EL m (MAP FST kvl) ≠ k) ⇒
          (f |++ kvl) ' k = v
   
   [FUPDATE_LIST_APPLY_NOT_MEM]  Theorem
      
      ⊢ ∀kvl f k. ¬MEM k (MAP FST kvl) ⇒ (f |++ kvl) ' k = f ' k
   
   [FUPDATE_LIST_APPLY_NOT_MEM_matchable]  Theorem
      
      ⊢ ∀kvl f k v. ¬MEM k (MAP FST kvl) ∧ v = f ' k ⇒ (f |++ kvl) ' k = v
   
   [FUPDATE_LIST_CANCEL]  Theorem
      
      ⊢ ∀ls1 fm ls2.
          (∀k. MEM k (MAP FST ls1) ⇒ MEM k (MAP FST ls2)) ⇒
          fm |++ ls1 |++ ls2 = fm |++ ls2
   
   [FUPDATE_LIST_EQ_FEMPTY]  Theorem
      
      ⊢ ∀fm ls. fm |++ ls = FEMPTY ⇔ fm = FEMPTY ∧ ls = []
   
   [FUPDATE_LIST_SAME_KEYS_UNWIND]  Theorem
      
      ⊢ ∀f1 f2 kvl1 kvl2.
          f1 |++ kvl1 = f2 |++ kvl2 ∧ MAP FST kvl1 = MAP FST kvl2 ∧
          ALL_DISTINCT (MAP FST kvl1) ⇒
          kvl1 = kvl2 ∧
          ∀kvl. MAP FST kvl = MAP FST kvl1 ⇒ f1 |++ kvl = f2 |++ kvl
   
   [FUPDATE_LIST_SAME_UPDATE]  Theorem
      
      ⊢ ∀kvl f1 f2.
          f1 |++ kvl = f2 |++ kvl ⇔
          DRESTRICT f1 (COMPL (set (MAP FST kvl))) =
          DRESTRICT f2 (COMPL (set (MAP FST kvl)))
   
   [FUPDATE_LIST_SNOC]  Theorem
      
      ⊢ ∀xs x fm. fm |++ SNOC x xs = (fm |++ xs) |+ x
   
   [FUPDATE_LIST_THM]  Theorem
      
      ⊢ ∀f. f |++ [] = f ∧ ∀h t. f |++ (h::t) = f |+ h |++ t
   
   [FUPDATE_PURGE]  Theorem
      
      ⊢ ∀f x y. f |+ (x,y) = f \\ x |+ (x,y)
   
   [FUPDATE_PURGE']  Theorem
      
      ⊢ ∀f x y. f \\ x |+ (x,y) = f |+ (x,y)
   
   [FUPDATE_SAME_APPLY]  Theorem
      
      ⊢ x = FST kv ∨ fm1 ' x = fm2 ' x ⇒ (fm1 |+ kv) ' x = (fm2 |+ kv) ' x
   
   [FUPDATE_SAME_LIST_APPLY]  Theorem
      
      ⊢ ∀kvl fm1 fm2 x.
          MEM x (MAP FST kvl) ⇒ (fm1 |++ kvl) ' x = (fm2 |++ kvl) ' x
   
   [FUPD_SAME_KEY_UNWIND]  Theorem
      
      ⊢ ∀f1 f2 k v1 v2.
          f1 |+ (k,v1) = f2 |+ (k,v2) ⇒
          v1 = v2 ∧ ∀v. f1 |+ (k,v) = f2 |+ (k,v)
   
   [IMAGE_FRANGE]  Theorem
      
      ⊢ ∀f fm. IMAGE f (FRANGE fm) = FRANGE (f o_f fm)
   
   [IN_FDOM_FOLDR_UNION]  Theorem
      
      ⊢ ∀x hL.
          x ∈ FDOM (FOLDR FUNION FEMPTY hL) ⇔ ∃h. MEM h hL ∧ x ∈ FDOM h
   
   [IN_FRANGE]  Theorem
      
      ⊢ ∀f v. v ∈ FRANGE f ⇔ ∃k. k ∈ FDOM f ∧ f ' k = v
   
   [IN_FRANGE_DOMSUB_suff]  Theorem
      
      ⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ⇒ ∀v. v ∈ FRANGE (fm \\ k) ⇒ P v
   
   [IN_FRANGE_DRESTRICT_suff]  Theorem
      
      ⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ⇒ ∀v. v ∈ FRANGE (DRESTRICT fm s) ⇒ P v
   
   [IN_FRANGE_FLOOKUP]  Theorem
      
      ⊢ ∀f v. v ∈ FRANGE f ⇔ ∃k. FLOOKUP f k = SOME v
   
   [IN_FRANGE_FUNION_suff]  Theorem
      
      ⊢ (∀v. v ∈ FRANGE f1 ⇒ P v) ∧ (∀v. v ∈ FRANGE f2 ⇒ P v) ⇒
        ∀v. v ∈ FRANGE (f1 ⊌ f2) ⇒ P v
   
   [IN_FRANGE_FUPDATE_LIST_suff]  Theorem
      
      ⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ∧ (∀v. MEM v (MAP SND ls) ⇒ P v) ⇒
        ∀v. v ∈ FRANGE (fm |++ ls) ⇒ P v
   
   [IN_FRANGE_FUPDATE_suff]  Theorem
      
      ⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ∧ P (SND kv) ⇒
        ∀v. v ∈ FRANGE (fm |+ kv) ⇒ P v
   
   [IN_FRANGE_o_f_suff]  Theorem
      
      ⊢ (∀v. v ∈ FRANGE fm ⇒ P (f v)) ⇒ ∀v. v ∈ FRANGE (f o_f fm) ⇒ P v
   
   [ITFMAPR_FEMPTY]  Theorem
      
      ⊢ ITFMAPR f FEMPTY A1 A2 ⇔ A1 = A2
   
   [ITFMAPR_cases]  Theorem
      
      ⊢ ∀f a0 a1 a2.
          ITFMAPR f a0 a1 a2 ⇔
          a0 = FEMPTY ∧ a2 = a1 ∨
          ∃A2 k v fm.
            a0 = fm |+ (k,v) ∧ a2 = f k v A2 ∧ k ∉ FDOM fm ∧
            ITFMAPR f fm a1 A2
   
   [ITFMAPR_ind]  Theorem
      
      ⊢ ∀f ITFMAPR'.
          (∀A. ITFMAPR' FEMPTY A A) ∧
          (∀A1 A2 k v fm.
             k ∉ FDOM fm ∧ ITFMAPR' fm A1 A2 ⇒
             ITFMAPR' (fm |+ (k,v)) A1 (f k v A2)) ⇒
          ∀a0 a1 a2. ITFMAPR f a0 a1 a2 ⇒ ITFMAPR' a0 a1 a2
   
   [ITFMAPR_rules]  Theorem
      
      ⊢ ∀f. (∀A. ITFMAPR f FEMPTY A A) ∧
            ∀A1 A2 k v fm.
              k ∉ FDOM fm ∧ ITFMAPR f fm A1 A2 ⇒
              ITFMAPR f (fm |+ (k,v)) A1 (f k v A2)
   
   [ITFMAPR_strongind]  Theorem
      
      ⊢ ∀f ITFMAPR'.
          (∀A. ITFMAPR' FEMPTY A A) ∧
          (∀A1 A2 k v fm.
             k ∉ FDOM fm ∧ ITFMAPR f fm A1 A2 ∧ ITFMAPR' fm A1 A2 ⇒
             ITFMAPR' (fm |+ (k,v)) A1 (f k v A2)) ⇒
          ∀a0 a1 a2. ITFMAPR f a0 a1 a2 ⇒ ITFMAPR' a0 a1 a2
   
   [ITFMAPR_total]  Theorem
      
      ⊢ ∀fm r0. ∃r. ITFMAPR f fm r0 r
   
   [ITFMAPR_unique]  Theorem
      
      ⊢ (∀k1 k2 v1 v2 A. f k1 v1 (f k2 v2 A) = f k2 v2 (f k1 v1 A)) ⇒
        ∀fm A0 A1 A2. ITFMAPR f fm A0 A1 ∧ ITFMAPR f fm A0 A2 ⇒ A1 = A2
   
   [ITFMAP_FEMPTY]  Theorem
      
      ⊢ ITFMAP f FEMPTY A = A
   
   [ITFMAP_thm]  Theorem
      
      ⊢ ITFMAP f FEMPTY A = A ∧
        ((∀k1 k2 v1 v2 A. f k1 v1 (f k2 v2 A) = f k2 v2 (f k1 v1 A)) ⇒
         ITFMAP f (fm |+ (k,v)) A = f k v (ITFMAP f (fm \\ k) A))
   
   [LEAST_NOTIN_FDOM]  Theorem
      
      ⊢ (LEAST ptr. ptr ∉ FDOM refs) ∉ FDOM refs
   
   [MAP_KEYS_BIJ_LINV]  Theorem
      
      ⊢ f PERMUTES 𝕌(:num) ⇒ MAP_KEYS f (MAP_KEYS (LINV f 𝕌(:num)) t) = t
   
   [MAP_KEYS_FEMPTY]  Theorem
      
      ⊢ ∀f. MAP_KEYS f FEMPTY = FEMPTY
   
   [MAP_KEYS_FUPDATE]  Theorem
      
      ⊢ ∀f fm k v.
          INJ f (k INSERT FDOM fm) 𝕌(:β) ⇒
          MAP_KEYS f (fm |+ (k,v)) = MAP_KEYS f fm |+ (f k,v)
   
   [MAP_KEYS_using_LINV]  Theorem
      
      ⊢ ∀f fm.
          INJ f (FDOM fm) 𝕌(:β) ⇒
          MAP_KEYS f fm =
          fm f_o_f FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm))
   
   [MAP_KEYS_witness]  Theorem
      
      ⊢ let
          m f fm =
            if INJ f (FDOM fm) 𝕌(:β) then
              fm f_o_f FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm))
            else FUN_FMAP ARB (IMAGE f (FDOM fm))
        in
          ∀f fm.
            FDOM (m f fm) = IMAGE f (FDOM fm) ∧
            (INJ f (FDOM fm) 𝕌(:β) ⇒
             ∀x. x ∈ FDOM fm ⇒ m f fm ' (f x) = fm ' x)
   
   [NOT_EQ_FAPPLY]  Theorem
      
      ⊢ ∀f a x y. a ≠ x ⇒ (f |+ (x,y)) ' a = f ' a
   
   [NOT_EQ_FEMPTY_FUPDATE]  Theorem
      
      ⊢ ∀f a b. FEMPTY ≠ f |+ (a,b)
   
   [NOT_FDOM_DRESTRICT]  Theorem
      
      ⊢ ∀f x. x ∉ FDOM f ⇒ DRESTRICT f (COMPL {x}) = f
   
   [NOT_FDOM_FAPPLY_FEMPTY]  Theorem
      
      ⊢ ∀f x. x ∉ FDOM f ⇒ f ' x = FEMPTY ' x
   
   [NUM_NOT_IN_FDOM]  Theorem
      
      ⊢ ∃x. x ∉ FDOM f
   
   [RRESTRICT_FEMPTY]  Theorem
      
      ⊢ ∀r. RRESTRICT FEMPTY r = FEMPTY
   
   [RRESTRICT_FUPDATE]  Theorem
      
      ⊢ ∀f r x y.
          RRESTRICT (f |+ (x,y)) r =
          if y ∈ r then RRESTRICT f r |+ (x,y)
          else RRESTRICT (DRESTRICT f (COMPL {x})) r
   
   [SAME_KEY_UPDATES_DIFFER]  Theorem
      
      ⊢ ∀f1 f2 k v1 v2. v1 ≠ v2 ⇒ f1 |+ (k,v1) ≠ f2 |+ (k,v2)
   
   [STRONG_DRESTRICT_FUPDATE]  Theorem
      
      ⊢ ∀f r x y.
          x ∈ r ⇒
          DRESTRICT (f |+ (x,y)) r = DRESTRICT f (r DELETE x) |+ (x,y)
   
   [STRONG_DRESTRICT_FUPDATE_THM]  Theorem
      
      ⊢ ∀f r x y.
          DRESTRICT (f |+ (x,y)) r =
          if x ∈ r then DRESTRICT f (COMPL {x} ∩ r) |+ (x,y)
          else DRESTRICT f (COMPL {x} ∩ r)
   
   [SUBMAP_ANTISYM]  Theorem
      
      ⊢ ∀f g. f ⊑ g ∧ g ⊑ f ⇔ f = g
   
   [SUBMAP_DOMSUB]  Theorem
      
      ⊢ f \\ k ⊑ f
   
   [SUBMAP_DOMSUB_gen]  Theorem
      
      ⊢ ∀f g k. f \\ k ⊑ g ⇔ f \\ k ⊑ g \\ k
   
   [SUBMAP_DRESTRICT]  Theorem
      
      ⊢ DRESTRICT f P ⊑ f
   
   [SUBMAP_DRESTRICT_MONOTONE]  Theorem
      
      ⊢ f1 ⊑ f2 ∧ s1 ⊆ s2 ⇒ DRESTRICT f1 s1 ⊑ DRESTRICT f2 s2
   
   [SUBMAP_FDOM_SUBSET]  Theorem
      
      ⊢ f1 ⊑ f2 ⇒ FDOM f1 ⊆ FDOM f2
   
   [SUBMAP_FEMPTY]  Theorem
      
      ⊢ ∀f. FEMPTY ⊑ f
   
   [SUBMAP_FLOOKUP_EQN]  Theorem
      
      ⊢ f ⊑ g ⇔ ∀x y. FLOOKUP f x = SOME y ⇒ FLOOKUP g x = SOME y
   
   [SUBMAP_FRANGE]  Theorem
      
      ⊢ ∀f g. f ⊑ g ⇒ FRANGE f ⊆ FRANGE g
   
   [SUBMAP_FUNION]  Theorem
      
      ⊢ ∀f1 f2 f3.
          f1 ⊑ f2 ∨ DISJOINT (FDOM f1) (FDOM f2) ∧ f1 ⊑ f3 ⇒ f1 ⊑ f2 ⊌ f3
   
   [SUBMAP_FUNION_ABSORPTION]  Theorem
      
      ⊢ ∀f g. f ⊑ g ⇔ f ⊌ g = g
   
   [SUBMAP_FUNION_EQ]  Theorem
      
      ⊢ (∀f1 f2 f3. DISJOINT (FDOM f1) (FDOM f2) ⇒ (f1 ⊑ f2 ⊌ f3 ⇔ f1 ⊑ f3)) ∧
        ∀f1 f2 f3.
          DISJOINT (FDOM f1) (FDOM f3 DIFF FDOM f2) ⇒
          (f1 ⊑ f2 ⊌ f3 ⇔ f1 ⊑ f2)
   
   [SUBMAP_FUNION_ID]  Theorem
      
      ⊢ (∀f1 f2. f1 ⊑ f1 ⊌ f2) ∧
        ∀f1 f2. DISJOINT (FDOM f1) (FDOM f2) ⇒ f2 ⊑ f1 ⊌ f2
   
   [SUBMAP_FUPDATE]  Theorem
      
      ⊢ ∀f g x y. f |+ (x,y) ⊑ g ⇔ x ∈ FDOM g ∧ g ' x = y ∧ f \\ x ⊑ g \\ x
   
   [SUBMAP_FUPDATE_EQN]  Theorem
      
      ⊢ f ⊑ f |+ (x,y) ⇔ x ∉ FDOM f ∨ f ' x = y ∧ x ∈ FDOM f
   
   [SUBMAP_FUPDATE_FLOOKUP]  Theorem
      
      ⊢ f ⊑ f |+ (x,y) ⇔ FLOOKUP f x = NONE ∨ FLOOKUP f x = SOME y
   
   [SUBMAP_REFL]  Theorem
      
      ⊢ ∀f. f ⊑ f
   
   [SUBMAP_TRANS]  Theorem
      
      ⊢ ∀f g h. f ⊑ g ∧ g ⊑ h ⇒ f ⊑ h
   
   [SUBMAP_mono_FUPDATE]  Theorem
      
      ⊢ ∀f g x y. f \\ x ⊑ g \\ x ⇒ f |+ (x,y) ⊑ g |+ (x,y)
   
   [WF_lbound_inv_SUBSET]  Theorem
      
      ⊢ FINITE s ⇒ WF (lbound s $PSUBSETᵀ)
   
   [disjoint_drestrict]  Theorem
      
      ⊢ ∀s m. DISJOINT s (FDOM m) ⇒ DRESTRICT m (COMPL s) = m
   
   [drestrict_iter_list]  Theorem
      
      ⊢ ∀m l. FOLDR (λk m. m \\ k) m l = DRESTRICT m (COMPL (set l))
   
   [f_o_ASSOC]  Theorem
      
      ⊢ (∀x y. g x = g y ⇔ x = y) ∧ (∀x y. h x = h y ⇔ x = y) ⇒
        (f f_o g) f_o h = f f_o g ∘ h
   
   [f_o_FEMPTY]  Theorem
      
      ⊢ ∀g. FEMPTY f_o g = FEMPTY
   
   [f_o_FUPDATE]  Theorem
      
      ⊢ ∀fm k v g.
          FINITE {x | g x ∈ FDOM fm} ∧ FINITE {x | g x = k} ⇒
          (fm |+ (k,v)) f_o g =
          FMERGE (flip K) (fm f_o g) (FUN_FMAP (K v) {x | g x = k})
   
   [f_o_f_FEMPTY_1]  Theorem
      
      ⊢ ∀f. FEMPTY f_o_f f = FEMPTY
   
   [f_o_f_FEMPTY_2]  Theorem
      
      ⊢ ∀f. f f_o_f FEMPTY = FEMPTY
   
   [f_o_f_FUPDATE_compose]  Theorem
      
      ⊢ ∀f1 f2 k x v.
          x ∉ FDOM f1 ∧ x ∉ FRANGE f2 ⇒
          (f1 |+ (x,v)) f_o_f (f2 |+ (k,x)) = f1 f_o_f f2 |+ (k,v)
   
   [fdom_fupdate_list2]  Theorem
      
      ⊢ ∀kvl fm.
          FDOM (fm |++ kvl) =
          FDOM fm DIFF set (MAP FST kvl) ∪ set (MAP FST kvl)
   
   [fevery_funion]  Theorem
      
      ⊢ ∀P m1 m2. FEVERY P m1 ∧ FEVERY P m2 ⇒ FEVERY P (m1 ⊌ m2)
   
   [flookup_thm]  Theorem
      
      ⊢ ∀f x v.
          (FLOOKUP f x = NONE ⇔ x ∉ FDOM f) ∧
          (FLOOKUP f x = SOME v ⇔ x ∈ FDOM f ∧ f ' x = v)
   
   [fmap_CASES]  Theorem
      
      ⊢ ∀f. f = FEMPTY ∨ ∃g x y. f = g |+ (x,y)
   
   [fmap_EQ]  Theorem
      
      ⊢ ∀f g. FDOM f = FDOM g ∧ $' f = $' g ⇔ f = g
   
   [fmap_EQ_THM]  Theorem
      
      ⊢ ∀f g. FDOM f = FDOM g ∧ (∀x. x ∈ FDOM f ⇒ f ' x = g ' x) ⇔ f = g
   
   [fmap_EQ_UPTO___EMPTY]  Theorem
      
      ⊢ ∀f1 f2. fmap_EQ_UPTO f1 f2 ∅ ⇔ f1 = f2
   
   [fmap_EQ_UPTO___EQ]  Theorem
      
      ⊢ ∀vs f. fmap_EQ_UPTO f f vs
   
   [fmap_EQ_UPTO___FUPDATE_BOTH]  Theorem
      
      ⊢ ∀f1 f2 ks k v.
          fmap_EQ_UPTO f1 f2 ks ⇒
          fmap_EQ_UPTO (f1 |+ (k,v)) (f2 |+ (k,v)) (ks DELETE k)
   
   [fmap_EQ_UPTO___FUPDATE_BOTH___NO_DELETE]  Theorem
      
      ⊢ ∀f1 f2 ks k v.
          fmap_EQ_UPTO f1 f2 ks ⇒
          fmap_EQ_UPTO (f1 |+ (k,v)) (f2 |+ (k,v)) ks
   
   [fmap_EQ_UPTO___FUPDATE_SING]  Theorem
      
      ⊢ ∀f1 f2 ks k v.
          fmap_EQ_UPTO f1 f2 ks ⇒
          fmap_EQ_UPTO (f1 |+ (k,v)) f2 (k INSERT ks)
   
   [fmap_EXT]  Theorem
      
      ⊢ ∀f g. f = g ⇔ FDOM f = FDOM g ∧ ∀x. x ∈ FDOM f ⇒ f ' x = g ' x
   
   [fmap_INDUCT]  Theorem
      
      ⊢ ∀P. P FEMPTY ∧ (∀f. P f ⇒ ∀x y. x ∉ FDOM f ⇒ P (f |+ (x,y))) ⇒
            ∀f. P f
   
   [fmap_SIMPLE_INDUCT]  Theorem
      
      ⊢ ∀P. P FEMPTY ∧ (∀f. P f ⇒ ∀x y. P (f |+ (x,y))) ⇒ ∀f. P f
   
   [fmap_cases_NOTIN]  Theorem
      
      ⊢ ∀fm. fm = FEMPTY ∨ ∃k v fm0. k ∉ FDOM fm0 ∧ fm = fm0 |+ (k,v)
   
   [fmap_eq_flookup]  Theorem
      
      ⊢ f1 = f2 ⇔ ∀x. FLOOKUP f1 x = FLOOKUP f2 x
   
   [fmap_rel_FEMPTY]  Theorem
      
      ⊢ fmap_rel R FEMPTY FEMPTY
   
   [fmap_rel_FEMPTY2]  Theorem
      
      ⊢ (fmap_rel R FEMPTY f ⇔ f = FEMPTY) ∧
        (fmap_rel R f FEMPTY ⇔ f = FEMPTY)
   
   [fmap_rel_FLOOKUP_imp]  Theorem
      
      ⊢ fmap_rel R f1 f2 ⇒
        (∀k. FLOOKUP f1 k = NONE ⇒ FLOOKUP f2 k = NONE) ∧
        ∀k v1.
          FLOOKUP f1 k = SOME v1 ⇒ ∃v2. FLOOKUP f2 k = SOME v2 ∧ R v1 v2
   
   [fmap_rel_FUNION_rels]  Theorem
      
      ⊢ fmap_rel R f1 f2 ∧ fmap_rel R f3 f4 ⇒
        fmap_rel R (f1 ⊌ f3) (f2 ⊌ f4)
   
   [fmap_rel_FUPDATE_I]  Theorem
      
      ⊢ fmap_rel R (f1 \\ k) (f2 \\ k) ∧ R v1 v2 ⇒
        fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))
   
   [fmap_rel_FUPDATE_LIST_same]  Theorem
      
      ⊢ ∀R ls1 ls2 f1 f2.
          fmap_rel R f1 f2 ∧ MAP FST ls1 = MAP FST ls2 ∧
          LIST_REL R (MAP SND ls1) (MAP SND ls2) ⇒
          fmap_rel R (f1 |++ ls1) (f2 |++ ls2)
   
   [fmap_rel_FUPDATE_same]  Theorem
      
      ⊢ fmap_rel R f1 f2 ∧ R v1 v2 ⇒
        fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))
   
   [fmap_rel_OPTREL_FLOOKUP]  Theorem
      
      ⊢ fmap_rel R f1 f2 ⇔ ∀k. OPTREL R (FLOOKUP f1 k) (FLOOKUP f2 k)
   
   [fmap_rel_mono]  Theorem
      
      ⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ fmap_rel R1 f1 f2 ⇒ fmap_rel R2 f1 f2
   
   [fmap_rel_refl]  Theorem
      
      ⊢ (∀x. R x x) ⇒ fmap_rel R x x
   
   [fmap_rel_sym]  Theorem
      
      ⊢ (∀x y. R x y ⇒ R y x) ⇒ ∀x y. fmap_rel R x y ⇒ fmap_rel R y x
   
   [fmap_rel_trans]  Theorem
      
      ⊢ (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
        ∀x y z. fmap_rel R x y ∧ fmap_rel R y z ⇒ fmap_rel R x z
   
   [fmap_to_list]  Theorem
      
      ⊢ ∀m. ∃l. ALL_DISTINCT (MAP FST l) ∧ m = FEMPTY |++ l
   
   [fmlfpR_cases]  Theorem
      
      ⊢ ∀f fm0 a0 a1 a2 a3.
          fmlfpR f fm0 a0 a1 a2 a3 ⇔
          a1 = FEMPTY ∧ a3 = a0 ∧ a0 = a2 ∨
          a1 = FEMPTY ∧ fmlfpR f fm0 a2 fm0 a2 a3 ∧ a0 ≠ a2 ∨
          ∃fm k v.
            a1 = fm |+ (k,v) ∧ fmlfpR f fm0 a0 (fm \\ k) (f k v a2) a3
   
   [fmlfpR_ind]  Theorem
      
      ⊢ ∀f fm0 fmlfpR'.
          (∀A0 A1. A0 = A1 ⇒ fmlfpR' A0 FEMPTY A1 A0) ∧
          (∀A0 A1 A2.
             fmlfpR' A1 fm0 A1 A2 ∧ A0 ≠ A1 ⇒ fmlfpR' A0 FEMPTY A1 A2) ∧
          (∀A0 A1 A2 fm k v.
             fmlfpR' A0 (fm \\ k) (f k v A1) A2 ⇒
             fmlfpR' A0 (fm |+ (k,v)) A1 A2) ⇒
          ∀a0 a1 a2 a3. fmlfpR f fm0 a0 a1 a2 a3 ⇒ fmlfpR' a0 a1 a2 a3
   
   [fmlfpR_lastpass]  Theorem
      
      ⊢ (∀k v. FLOOKUP fm k = SOME v ⇒ f k v A = A) ⇒
        (fmlfpR f fm A fm A B ⇔ A = B)
   
   [fmlfpR_rules]  Theorem
      
      ⊢ ∀f fm0.
          (∀A0 A1. A0 = A1 ⇒ fmlfpR f fm0 A0 FEMPTY A1 A0) ∧
          (∀A0 A1 A2.
             fmlfpR f fm0 A1 fm0 A1 A2 ∧ A0 ≠ A1 ⇒
             fmlfpR f fm0 A0 FEMPTY A1 A2) ∧
          ∀A0 A1 A2 fm k v.
            fmlfpR f fm0 A0 (fm \\ k) (f k v A1) A2 ⇒
            fmlfpR f fm0 A0 (fm |+ (k,v)) A1 A2
   
   [fmlfpR_strongind]  Theorem
      
      ⊢ ∀f fm0 fmlfpR'.
          (∀A0 A1. A0 = A1 ⇒ fmlfpR' A0 FEMPTY A1 A0) ∧
          (∀A0 A1 A2.
             fmlfpR f fm0 A1 fm0 A1 A2 ∧ fmlfpR' A1 fm0 A1 A2 ∧ A0 ≠ A1 ⇒
             fmlfpR' A0 FEMPTY A1 A2) ∧
          (∀A0 A1 A2 fm k v.
             fmlfpR f fm0 A0 (fm \\ k) (f k v A1) A2 ∧
             fmlfpR' A0 (fm \\ k) (f k v A1) A2 ⇒
             fmlfpR' A0 (fm |+ (k,v)) A1 A2) ⇒
          ∀a0 a1 a2 a3. fmlfpR f fm0 a0 a1 a2 a3 ⇒ fmlfpR' a0 a1 a2 a3
   
   [fmlfpR_total]  Theorem
      
      ⊢ ∀fm f R P A2 A0.
          fp_soluble R P fm f ⇒
          RC R A0 P ⇒
          (fmlfpR f fm A0 fm A0 A2 ⇔ A2 = P)
   
   [fmlfpR_total_lemma]  Theorem
      
      ⊢ fp_soluble R P fm0 f ⇒
        RC R A0 A1 ∧ RC R A1 P ∧ fm ⊑ fm0 ∧ A1 = FOLDR (UNCURRY f) A0 kvl ∧
        DISJOINT (set (MAP FST kvl)) (FDOM fm) ∧
        ALL_DISTINCT (MAP FST kvl) ∧ fm0 = FOLDR (flip $|+) fm kvl ⇒
        (fmlfpR f fm0 A0 fm A1 A2 ⇔ A2 = P)
   
   [fp_soluble_FOLDR1]  Theorem
      
      ⊢ fp_soluble R P fm0 f ∧ fm0 = FOLDR (flip $|+) fm kvl ∧
        DISJOINT (set (MAP FST kvl)) (FDOM fm) ∧ ALL_DISTINCT (MAP FST kvl) ⇒
        (∀s A.
           IS_SUFFIX kvl s ∧ RC R A P ⇒
           RC R A (FOLDR (UNCURRY f) A s) ∧ RC R (FOLDR (UNCURRY f) A s) P) ∧
        ∀s A k v.
          IS_SUFFIX kvl s ∧ RC R A P ∧ MEM (k,v) s ∧ f k v A ≠ A ⇒
          FOLDR (UNCURRY f) A s ≠ A
   
   [fupdate_list_foldl]  Theorem
      
      ⊢ ∀m l. FOLDL (λenv (k,v). env |+ (k,v)) m l = m |++ l
   
   [fupdate_list_foldr]  Theorem
      
      ⊢ ∀m l. FOLDR (λ(k,v) env. env |+ (k,v)) m l = m |++ REVERSE l
   
   [fupdate_list_map]  Theorem
      
      ⊢ ∀l f x y.
          x ∈ FDOM (FEMPTY |++ l) ⇒
          (FEMPTY |++ MAP (λ(a,b). (a,f b)) l) ' x = f ((FEMPTY |++ l) ' x)
   
   [is_fmap_cases]  Theorem
      
      ⊢ ∀a0.
          is_fmap a0 ⇔
          a0 = (λa. INR ()) ∨
          ∃f a b. a0 = (λx. if x = a then INL b else f x) ∧ is_fmap f
   
   [is_fmap_ind]  Theorem
      
      ⊢ ∀is_fmap'.
          is_fmap' (λa. INR ()) ∧
          (∀f a b. is_fmap' f ⇒ is_fmap' (λx. if x = a then INL b else f x)) ⇒
          ∀a0. is_fmap a0 ⇒ is_fmap' a0
   
   [is_fmap_rules]  Theorem
      
      ⊢ is_fmap (λa. INR ()) ∧
        ∀f a b. is_fmap f ⇒ is_fmap (λx. if x = a then INL b else f x)
   
   [is_fmap_strongind]  Theorem
      
      ⊢ ∀is_fmap'.
          is_fmap' (λa. INR ()) ∧
          (∀f a b.
             is_fmap f ∧ is_fmap' f ⇒
             is_fmap' (λx. if x = a then INL b else f x)) ⇒
          ∀a0. is_fmap a0 ⇒ is_fmap' a0
   
   [o_f_DOMSUB]  Theorem
      
      ⊢ g o_f fm \\ k = g o_f (fm \\ k)
   
   [o_f_FAPPLY]  Theorem
      
      ⊢ ∀f g x. x ∈ FDOM g ⇒ (f o_f g) ' x = f (g ' x)
   
   [o_f_FDOM]  Theorem
      
      ⊢ ∀f g. FDOM g = FDOM (f o_f g)
   
   [o_f_FEMPTY]  Theorem
      
      ⊢ f o_f FEMPTY = FEMPTY
   
   [o_f_FRANGE]  Theorem
      
      ⊢ x ∈ FRANGE g ⇒ f x ∈ FRANGE (f o_f g)
   
   [o_f_FUNION]  Theorem
      
      ⊢ f o_f (f1 ⊌ f2) = f o_f f1 ⊌ f o_f f2
   
   [o_f_FUPDATE]  Theorem
      
      ⊢ f o_f (fm |+ (k,v)) = f o_f fm |+ (k,f v)
   
   [o_f_cong]  Theorem
      
      ⊢ ∀f fm f' fm'.
          fm = fm' ∧ (∀v. v ∈ FRANGE fm ⇒ f v = f' v) ⇒
          f o_f fm = f' o_f fm'
   
   [o_f_id]  Theorem
      
      ⊢ ∀m. (λx. x) o_f m = m
   
   [o_f_o_f]  Theorem
      
      ⊢ f o_f g o_f h = (f ∘ g) o_f h
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14