Theory finite_map

⊢ ∀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⟩

⊢ ∀f x. f⟨x⟩ = OUTL (fmap_REP f x)

⊢ ∀fm. FCARD fm = CARD (FDOM fm)

⊢ ∀f1 s. FDIFF f1 s = DRESTRICT f1 (COMPL s)

⊢ ∀f x. FDOM f x ⇔ ISL (fmap_REP f x)

⊢ FEMPTY = fmap_ABS (λa. INR ())

⊢ ∀P f. FEVERY P f ⇔ ∀x. x ∈ FDOM f ⇒ P (x,f⟨x⟩)

⊢ ∀f x. FLOOKUP f x = if x ∈ FDOM f then SOME f⟨x⟩ else NONE

⊢ ∀f m. FMAP_MAP2 f m = FUN_FMAP (λx. f (x,m⟨x⟩)) (FDOM m)

⊢ ∀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⟩

⊢ ∀f m1 m2.
    FDOM (FMERGE_WITH_KEY f m1 m2) = FDOM m1 ∪ FDOM m2 ∧
    ∀x. (FMERGE_WITH_KEY f m1 m2)⟨x⟩ =
        if x ∈ FDOM m1 ∧ x ∈ FDOM m2 then f x m1⟨x⟩ m2⟨x⟩
        else if x ∈ FDOM m1 then m1⟨x⟩
        else m2⟨x⟩

⊢ ∀f. FRANGE f = {y | ∃x. x ∈ FDOM f ∧ f⟨x⟩ = y}

⊢ ∀f g.
    FDOM (f ⊌ g) = FDOM f ∪ FDOM g ∧
    ∀x. (f ⊌ g)⟨x⟩ = if x ∈ FDOM f then f⟨x⟩ else g⟨x⟩

⊢ ∀f P.
    FINITE P ⇒
    FDOM (FUN_FMAP f P) = P ∧ ∀x. x ∈ P ⇒ (FUN_FMAP f P)⟨x⟩ = f x

⊢ ∀f x y. f⟨x ↦ y⟩ = fmap_ABS (λa. if a = x then INL y else fmap_REP f a)

⊢ $|++ = FOLDL $|+

⊢ ∀f fm A0. ITFMAP f fm A0 = @A. ITFMAPR f fm A0 A

⊢ ∀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⟩)

⊢ ∀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⟩

⊢ ∀f g. f ⊑ g ⇔ ∀x. x ∈ FDOM f ⇒ x ∈ FDOM g ∧ f⟨x⟩ = g⟨x⟩

⊢ ∀f g. f f_o g = f f_o_f FUN_FMAP g {x | g x ∈ FDOM f}

⊢ ∀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⟩⟩

⊢ ∀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⟩

⊢ (∀a. fmap_ABS (fmap_REP a) = a) ∧
  ∀r. is_fmap r ⇔ fmap_REP (fmap_ABS r) = r

⊢ ∃rep. TYPE_DEFINITION is_fmap rep

⊢ ∀fm k. fm \\ k = DRESTRICT fm (COMPL {k})

⊢ ∀m1 m2.
    fmap_inverse m1 m2 ⇔
    ∀k. k ∈ FDOM m1 ⇒ ∃v. FLOOKUP m1 k = SOME v ∧ FLOOKUP m2 v = SOME k

⊢ ∀R f1 f2.
    fmap_rel R f1 f2 ⇔ FDOM f2 = FDOM f1 ∧ ∀x. x ∈ FDOM f1 ⇒ R f1⟨x⟩ f2⟨x⟩

⊢ ∀kz vz fm. fmap_size kz vz fm = ∑ (λk. kz k + vz fm⟨k⟩) (FDOM fm)

⊢ ∀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

⊢ ∀l R x y. lbound l R x y ⇔ R꙳ l x ∧ R꙳ l y ∧ R x y

⊢ ∀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 (FDOM m1) (FDOM m2) ⇒
  (FEVERY P (m1 ⊌ m2) ⇔ FEVERY P m1 ∧ FEVERY P m2)

⊢ fm \\ k1 \\ k2 = fm \\ k2 \\ k1

⊢ ∀fm k. (fm \\ k)⟨k⟩ = FEMPTY⟨k⟩

⊢ ∀fm k1 k2. k1 ≠ k2 ⇒ (fm \\ k1)⟨k2⟩ = fm⟨k2⟩

⊢ ∀fm k1 k2. (fm \\ k1)⟨k2⟩ = if k1 = k2 then FEMPTY⟨k2⟩ else fm⟨k2⟩

⊢ ∀k. FEMPTY \\ k = FEMPTY

⊢ ∀fm k. FLOOKUP (fm \\ k) k = NONE

⊢ ∀fm k1 k2. k1 ≠ k2 ⇒ FLOOKUP (fm \\ k1) k2 = FLOOKUP fm k2

⊢ ∀fm k1 k2.
    FLOOKUP (fm \\ k1) k2 = if k1 = k2 then NONE else FLOOKUP fm k2

⊢ ∀f m s. FMAP_MAP2 f m \\ s = FMAP_MAP2 f (m \\ s)

⊢ (f ⊌ g) \\ k = f \\ k ⊌ g \\ k

⊢ ∀fm k v. fm⟨k ↦ v⟩ \\ k = fm \\ k

⊢ ∀l m x. (m |++ l) \\ x = m \\ x |++ FILTER ((λy. x ≠ y) ∘ FST) l

⊢ ∀fm k1 k2 v. k1 ≠ k2 ⇒ fm⟨k1 ↦ v⟩ \\ k2 = (fm \\ k2)⟨k1 ↦ v⟩

⊢ ∀fm k1 k2 v.
    fm⟨k1 ↦ v⟩ \\ k2 = if k1 = k2 then fm \\ k2 else (fm \\ k2)⟨k1 ↦ v⟩

⊢ fm \\ k \\ k = fm \\ k

⊢ BIJ f 𝕌(:α) 𝕌(:β) ⇒ MAP_KEYS f fm \\ f s = MAP_KEYS f (fm \\ s)

⊢ k ∉ FDOM fm ⇒ fm \\ k = fm

⊢ ∀f g x. f ⊑ g ∧ x ∉ FDOM f ⇒ f ⊑ g \\ x

⊢ ∀f1 f2 s.
    DRESTRICT (f1 ⊌ f2) s = DRESTRICT f1 s ⊌ DRESTRICT f2 (s DIFF FDOM f1)

⊢ ∀f s k. DRESTRICT f s \\ k = DRESTRICT f (s DELETE k)

⊢ ∀f P Q. DRESTRICT (DRESTRICT f P) Q = DRESTRICT f (P ∩ Q)

⊢ ∀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 f1 s = DRESTRICT f2 s ⇔
  s ∩ FDOM f1 = s ∩ FDOM f2 ∧ ∀x. x ∈ FDOM f1 ∧ x ∈ s ⇒ f1⟨x⟩ = f2⟨x⟩

⊢ ∀m s. DISJOINT s (FDOM m) ⇔ DRESTRICT m s = FEMPTY

⊢ ∀h h1 h2.
    DISJOINT (FDOM h1) (FDOM h2) ∧ h1 ⊌ h2 = h ⇒
    h2 = DRESTRICT h (COMPL (FDOM h1))

⊢ ∀f. DRESTRICT f (FDOM f) = f

⊢ ∀r. DRESTRICT FEMPTY r = FEMPTY

⊢ ∀h s1 s2. DRESTRICT h s1 ⊌ DRESTRICT h s2 = DRESTRICT h (s1 ∪ s2)

⊢ DRESTRICT f s ⊌ DRESTRICT f (COMPL s) = f

⊢ ∀fm s. DRESTRICT fm s ⊌ fm = fm

⊢ s2 ⊆ s1 ⇒ ∃h. DRESTRICT f s1 ⊌ g = DRESTRICT f s2 ⊌ h

⊢ ∀f r x y.
    DRESTRICT f⟨x ↦ y⟩ r =
    if x ∈ r then (DRESTRICT f r)⟨x ↦ y⟩ else DRESTRICT f r

⊢ ∀s vs. DRESTRICT (DRESTRICT s vs) vs = DRESTRICT s vs

⊢ ∀f. DRESTRICT f ∅ = FEMPTY

⊢ INJ f 𝕌(:α) 𝕌(:β) ⇒
  DRESTRICT (MAP_KEYS f fm) (IMAGE f s) = MAP_KEYS f (DRESTRICT fm s)

⊢ ∀f r. DRESTRICT f r ⊑ f

⊢ f ⊑ g ⇒ DRESTRICT f P ⊑ g

⊢ ∀f1 f2 s t.
    DRESTRICT f1 s = DRESTRICT f2 s ∧ t ⊆ s ⇒
    DRESTRICT f1 t = DRESTRICT f2 t

⊢ s1 ⊆ s2 ⇒ DRESTRICT f s1 ⊑ DRESTRICT f s2

⊢ ∀f1 f2 s t.
    DRESTRICT f1 s ⊑ DRESTRICT f2 s ∧ t ⊆ s ⇒
    DRESTRICT f1 t ⊑ DRESTRICT f2 t

⊢ ∀f. DRESTRICT f 𝕌(:α) = f

⊢ f = g ⇔ f ⊑ g ∧ FDOM f = FDOM g

⊢ ∀f x y. f⟨x ↦ y⟩⟨x⟩ = y

⊢ ∀f a b x. f⟨a ↦ b⟩⟨x⟩ = if x = a then b else f⟨x⟩

⊢ ∀f g.
    FINITE {x | g x ∈ FDOM f} ⇒
    ∀x. x ∈ FDOM (f f_o g) ⇒ (f f_o g)⟨x⟩ = f⟨g x⟩

⊢ ∀f. FCARD f = 0 ⇔ f = FEMPTY

⊢ FCARD FEMPTY = 0

⊢ ∀fm a b. FCARD fm⟨a ↦ b⟩ = if a ∈ FDOM fm then FCARD fm else 1 + FCARD fm

⊢ ∀f n.
    FCARD f = SUC n ⇔ ∃f' x y. x ∉ FDOM f' ∧ FCARD f' = n ∧ f = f'⟨x ↦ y⟩

⊢ FDIFF f p = FDIFF f (p ∩ FDOM f)

⊢ ∀f. FDIFF f ∅ = f

⊢ ∀fm s1 s2. FDIFF (FDIFF fm s1) s2 = FDIFF fm (s1 ∪ s2)

⊢ FDIFF (f \\ x) p = FDIFF f p \\ x

⊢ FDIFF (f \\ x) p = FDIFF f (x INSERT p)

⊢ FDIFF FEMPTY s = FEMPTY

⊢ ∀f m s. FDIFF (FMAP_MAP2 f m) s = FMAP_MAP2 f (FDIFF m s)

⊢ ∀fm1 fm2 s. FDIFF (fm1 ⊌ fm2) s = FDIFF fm1 s ⊌ FDIFF fm2 s

⊢ FDIFF fm⟨k ↦ v⟩ s = if k ∈ s then FDIFF fm s else (FDIFF fm s)⟨k ↦ v⟩

⊢ ∀fm k. FDOM (fm \\ k) = FDOM fm DELETE k

⊢ ∀f r x. FDOM (DRESTRICT f r) = FDOM f ∩ r

⊢ ∀f. FDOM f = ∅ ⇔ f = FEMPTY

⊢ ∀f. ∅ = FDOM f ⇔ f = FEMPTY

⊢ ∀f x. x ∈ FDOM f ⇒ ∀y. FDOM f⟨x ↦ y⟩ = FDOM f

⊢ x ∈ FDOM (FDIFF refs f2) ⇔ x ∈ FDOM refs ∧ x ∉ f2

⊢ FDOM FEMPTY = ∅

⊢ ∀fm. FINITE (FDOM fm)

⊢ ∀f s. FINITE s ⇒ FDOM (FUN_FMAP f s) = s

⊢ ∀m f g. FDOM (FMERGE m f g) = FDOM f ∪ FDOM g

⊢ ∀ls fm. FDOM (FOLDR (λk m. m \\ k) fm ls) = FDOM fm DIFF set ls

⊢ FDOM (f ⊌ g) = FDOM f ∪ FDOM g

⊢ ∀f a b. FDOM f⟨a ↦ b⟩ = a INSERT FDOM f

⊢ ∀kvl fm. FDOM (fm |++ kvl) = FDOM fm ∪ set (MAP FST kvl)

⊢ ∀f g. FDOM (f f_o_f g) ⊆ FDOM g

⊢ ∀f. (∀a. a ∉ FDOM f) ⇔ f = FEMPTY

⊢ ∀f g. FINITE {x | g x ∈ FDOM f} ⇒ FDOM (f f_o g) = {x | g x ∈ FDOM f}

⊢ ∀f g. FDOM (f o_f g) = FDOM g

⊢ ∀x y. FEMPTY |+ x = FEMPTY |+ y ⇔ x = y

⊢ ∀h. h ⊑ FEMPTY ⇔ h = FEMPTY

⊢ ∀P f. FEVERY P f ⇔ ∀k v. FLOOKUP f k = SOME v ⇒ P (k,v)

⊢ FEVERY P (DRESTRICT f⟨k ↦ v⟩ (COMPL s)) ⇔
  (k ∉ s ⇒ P (k,v)) ∧ FEVERY P (DRESTRICT f (COMPL (k INSERT s)))

⊢ ∀P. FEVERY P FEMPTY

⊢ FEVERY P f ∧ FLOOKUP f k = SOME v ⇒ P (k,v)

⊢ ∀P f x y.
    FEVERY P f⟨x ↦ y⟩ ⇔ P (x,y) ∧ FEVERY P (DRESTRICT f (COMPL {x}))

⊢ ALL_DISTINCT (MAP FST kvl) ⇒
  (FEVERY P (fm |++ kvl) ⇔
   EVERY P kvl ∧ FEVERY P (DRESTRICT fm (COMPL (set (MAP FST kvl)))))

⊢ FEVERY P FEMPTY ∧ (FEVERY P f ∧ P (x,y) ⇒ FEVERY P f⟨x ↦ y⟩)

⊢ FEVERY P fm ∧ fm0 ⊑ fm ⇒ FEVERY P fm0

⊢ ∀m P f. FEVERY P (f o_f m) ⇔ FEVERY (λx. P (FST x,f (SND x))) m

⊢ ∀fm. FINITE (FRANGE fm)

⊢ (∀f x y. FLOOKUP f x = SOME y ⇒ y ∈ FRANGE f) ∧
  ∀f x. x ∈ FDOM f ⇒ f⟨x⟩ ∈ FRANGE f

⊢ ∀g. (∀x y. g x = g y ⇔ x = y) ⇒ ∀f. FINITE {x | g x ∈ FDOM f}

⊢ ∀fm s k.
    FLOOKUP (DRESTRICT fm s) k = if k ∈ s then FLOOKUP fm k else NONE

⊢ FLOOKUP FEMPTY k = NONE

⊢ f1 = f2 ⇔ FLOOKUP f1 = FLOOKUP f2

⊢ FLOOKUP (FDIFF fm s) k = if k ∈ s then NONE else FLOOKUP fm k

⊢ ∀f m k.
    FLOOKUP (FMAP_MAP2 f m) k = OPTION_MAP (λv. f (k,v)) (FLOOKUP m k)

⊢ FLOOKUP (FMERGE f m1 m2) k =
  case FLOOKUP m1 k of
    NONE => FLOOKUP m2 k
  | SOME v1 =>
    case FLOOKUP m2 k of NONE => SOME v1 | SOME v2 => SOME (f v1 v2)

⊢ FLOOKUP (FMERGE_WITH_KEY f m1 m2) k =
  case FLOOKUP m1 k of
    NONE => FLOOKUP m2 k
  | SOME v1 =>
    case FLOOKUP m2 k of NONE => SOME v1 | SOME v2 => SOME (f k v1 v2)

⊢ ASSOC (FMERGE_WITH_KEY f) ⇔ ∀k. ASSOC (f k)

⊢ COMM (FMERGE_WITH_KEY f) ⇔ ∀k. COMM (f k)

⊢ 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 (f1 ⊌ f2) k =
  case FLOOKUP f1 k of NONE => FLOOKUP f2 k | SOME v => SOME v

⊢ FINITE P ⇒ FLOOKUP (FUN_FMAP f P) k = if k ∈ P then SOME (f k) else NONE

⊢ INJ f (FDOM m) 𝕌(:β) ⇒
  FLOOKUP (MAP_KEYS f m) k =
  OPTION_BIND (some x. k = f x ∧ x ∈ FDOM m) (FLOOKUP m)

⊢ INJ f 𝕌(:α) 𝕌(:β) ⇒ FLOOKUP (MAP_KEYS f m) (f k) = FLOOKUP m k

⊢ FLOOKUP FEMPTY k = NONE ∧
  FLOOKUP fm⟨k1 ↦ v⟩ k2 = (if k1 = k2 then SOME v else FLOOKUP fm k2) ∧
  FDIFF f1 s = DRESTRICT f1 (COMPL s) ∧
  FLOOKUP (FMAP_MAP2 f m) k = OPTION_MAP (λv. f (k,v)) (FLOOKUP m k) ∧
  FLOOKUP (DRESTRICT fm s) k = (if k ∈ s then FLOOKUP fm k else NONE) ∧
  FLOOKUP (FDIFF m d) k = (if k ∈ d then NONE else FLOOKUP m k) ∧
  FLOOKUP (f1 ⊌ f2) k =
  (case FLOOKUP f1 k of NONE => FLOOKUP f2 k | SOME v => SOME v) ∧
  (FINITE P ⇒ FLOOKUP (FUN_FMAP f P) k = if k ∈ P then SOME (f k) else NONE) ∧
  FLOOKUP (FMAP_MAP2 f m) k = OPTION_MAP (λv. f (k,v)) (FLOOKUP m k) ∧
  FLOOKUP (FMERGE f m1 m2) k =
  case FLOOKUP m1 k of
    NONE => FLOOKUP m2 k
  | SOME v1 =>
    case FLOOKUP m2 k of NONE => SOME v1 | SOME v2 => SOME (f v1 v2)

⊢ f ⊑ g ∧ FLOOKUP f k = SOME v ⇒ FLOOKUP g k = SOME v

⊢ FLOOKUP fm⟨k1 ↦ v⟩ k2 = if k1 = k2 then SOME v else FLOOKUP fm k2

⊢ FLOOKUP (f o_f fm) k =
  case FLOOKUP fm k of NONE => NONE | SOME v => SOME (f v)

⊢ FMAP_MAP2 f FEMPTY = FEMPTY

⊢ FMAP_MAP2 f m⟨x ↦ v⟩ = (FMAP_MAP2 f m)⟨x ↦ f (x,v)⟩

⊢ ∀l m f.
    FMAP_MAP2 f (m |++ l) = FMAP_MAP2 f m |++ MAP (λ(k,v). (k,f (k,v))) l

⊢ FDOM (FMAP_MAP2 f m) = FDOM m ∧
  ∀x. x ∈ FDOM m ⇒ (FMAP_MAP2 f m)⟨x⟩ = f (x,m⟨x⟩)

⊢ ∀f1 kvl p. f1 |+ p = FEMPTY |++ kvl ⇒ MEM p kvl

⊢ ∀fm k v ck cv.
    fm⟨k ↦ v⟩ = FEMPTY⟨ck ↦ cv⟩ ⇔
    k = ck ∧ v = cv ∧ (fm = FEMPTY ∨ ∃v'. fm = FEMPTY⟨k ↦ v'⟩)

⊢ ∀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⟩

⊢ ASSOC (FMERGE m) ⇔ ASSOC m

⊢ COMM (FMERGE m) ⇔ COMM m

⊢ ∀m m1 m2 k. FMERGE m m1 m2 \\ k = FMERGE m (m1 \\ k) (m2 \\ k)

⊢ DRESTRICT (FMERGE f st1 st2) vs =
  FMERGE f (DRESTRICT st1 vs) (DRESTRICT st2 vs)

⊢ FMERGE m f g = FEMPTY ⇔ f = FEMPTY ∧ g = FEMPTY

⊢ FMERGE m f FEMPTY = f ∧ FMERGE m FEMPTY f = f

⊢ FUNION = FMERGE (λx y. x)

⊢ (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⟩)

⊢ DRESTRICT (FMERGE_WITH_KEY f m1 m2) vs =
  FMERGE_WITH_KEY f (DRESTRICT m1 vs) (DRESTRICT m2 vs)

⊢ FMERGE_WITH_KEY f m1 m2 = FEMPTY ⇔ m1 = FEMPTY ∧ m2 = FEMPTY

⊢ FMERGE_WITH_KEY f FEMPTY m2 = m2 ∧ FMERGE_WITH_KEY f m1 FEMPTY = m1

⊢ FMERGE f = FMERGE_WITH_KEY (λk v1 v2. f v1 v2)

⊢ FMERGE_WITH_KEY f (m1 ⊌ m2) m3 =
  FMERGE_WITH_KEY f m1 (DRESTRICT m3 (FDOM m1)) ⊌ FMERGE_WITH_KEY f m2 m3

⊢ FMERGE_WITH_KEY f (m1 ⊌ m2) m3 =
  FMERGE_WITH_KEY f m1 (DRESTRICT m3 (FDOM m1)) ⊌
  FMERGE_WITH_KEY f m2 (FDIFF m3 (FDOM m1))

⊢ FMERGE_WITH_KEY f m1⟨k ↦ v1⟩ m2 =
  (FMERGE_WITH_KEY f m1 m2)⟨
    k ↦ (case FLOOKUP m2 k of NONE => v1 | SOME v2 => f k v1 v2)
  ⟩

⊢ (FMERGE_WITH_KEY f m1 m2 = m1 ⇔
   ∀x. x ∈ FDOM m2 ⇒ x ∈ FDOM m1 ∧ f x m1⟨x⟩ m2⟨x⟩ = m1⟨x⟩) ∧
  (FMERGE_WITH_KEY f m1 m2 = m2 ⇔
   ∀x. x ∈ FDOM m1 ⇒ x ∈ FDOM m2 ∧ f x m1⟨x⟩ m2⟨x⟩ = m2⟨x⟩)

⊢ ∀fm k. k ∈ FDOM fm ⇒ ∃fm0 v. fm = fm0⟨k ↦ v⟩ ∧ k ∉ FDOM fm0

⊢ ∀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)

⊢ ∀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)

⊢ ∀f1 f2 ls a.
    FOLDL (λfm k. fm⟨f1 k ↦ f2 k⟩) a ls = a |++ MAP (λk. (f1 k,f2 k)) ls

⊢ FRANGE (fm \\ k) ⊆ FRANGE fm

⊢ FRANGE (DRESTRICT fm s) ⊆ FRANGE fm

⊢ FRANGE FEMPTY = ∅

⊢ v ∈ FRANGE f ⇔ ∃k. FLOOKUP f k = SOME v

⊢ FINITE P ⇒ FRANGE (FUN_FMAP f P) = IMAGE f P

⊢ DISJOINT (FDOM fm1) (FDOM fm2) ⇒
  FRANGE (fm1 ⊌ fm2) = FRANGE fm1 ∪ FRANGE fm2

⊢ FRANGE (f1 ⊌ f2) ⊆ FRANGE f1 ∪ FRANGE f2

⊢ ∀f x y. FRANGE f⟨x ↦ y⟩ = y INSERT FRANGE (DRESTRICT f (COMPL {x}))

⊢ ∀fm k v. FRANGE fm⟨k ↦ v⟩ = v INSERT FRANGE (fm \\ k)

⊢ ∀ls fm. FRANGE (fm |++ ls) ⊆ FRANGE fm ∪ set (MAP SND ls)

⊢ FRANGE (fm |+ kv) ⊆ FRANGE fm ∪ {SND kv}

⊢ ∀f g. FRANGE g ⊆ FDOM f ⇒ FDOM (f f_o_f g) = FDOM g

⊢ ∀f g h. f ⊌ (g ⊌ h) = f ⊌ g ⊌ h

⊢ ∀f g. DISJOINT (FDOM f) (FDOM g) ⇒ f ⊌ g = g ⊌ f

⊢ ∀f1 f2 f3.
    DISJOINT (FDOM f1) (FDOM f2) ∧ DISJOINT (FDOM f1) (FDOM f3) ⇒
    (f1 ⊌ f2 = f1 ⊌ f3 ⇔ f2 = f3)

⊢ ∀h1 h2. h1 ⊌ h2 = FEMPTY ⇔ h1 = FEMPTY ∧ h2 = FEMPTY

⊢ ∀f1 f2 f3.
    DISJOINT (FDOM f1) (FDOM f2) ∧ DISJOINT (FDOM f1) (FDOM f3) ∧ f2 = f3 ⇒
    f1 ⊌ f2 = f1 ⊌ f3

⊢ ∀g. FEMPTY ⊌ g = g

⊢ ∀f. f ⊌ FEMPTY = f

⊢ ∀f1 f2 m. DISJOINT (FDOM f1) (FDOM f2) ⇒ FMERGE m f1 f2 = f1 ⊌ f2

⊢ ∀m1 m2 f.
    DISJOINT (FDOM m1) (FDOM m2) ⇒ FMERGE_WITH_KEY f m1 m2 = m1 ⊌ m2

⊢ ∀f g x y. f⟨x ↦ y⟩ ⊌ g = (f ⊌ g)⟨x ↦ y⟩

⊢ ∀f g x y. f ⊌ g⟨x ↦ y⟩ = if x ∈ FDOM f then f ⊌ g else (f ⊌ g)⟨x ↦ y⟩

⊢ fm ⊌ fm = fm

⊢ FUN_FMAP f ∅ = FEMPTY

⊢ ∀f e s.
    FINITE s ∧ e ∉ s ⇒ FUN_FMAP f (e INSERT s) = (FUN_FMAP f s)⟨e ↦ f e⟩

⊢ ∀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

⊢ ∀f k v1 v2. f⟨k ↦ v1⟩ = f⟨k ↦ v2⟩ ⇔ v1 = v2

⊢ ∀f1 f2 k v1 v2.
    k ∉ FDOM f1 ∧ k ∉ FDOM f2 ⇒
    (f1⟨k ↦ v1⟩ = f2⟨k ↦ v2⟩ ⇔ f1 = f2 ∧ v1 = v2)

⊢ ∀f1 f2 k v.
    f1⟨k ↦ v⟩ = f2⟨k ↦ v⟩ ⇔
    DRESTRICT f1 (COMPL {k}) = DRESTRICT f2 (COMPL {k})

⊢ ∀f a b c d. a ≠ c ⇒ f⟨c ↦ d; a ↦ b⟩ = f⟨a ↦ b; c ↦ d⟩

⊢ ∀f x y. f⟨x ↦ y⟩ = (DRESTRICT f (COMPL {x}))⟨x ↦ y⟩

⊢ ∀k v f. k ∈ FDOM f ∧ f⟨k⟩ = v ⇒ f⟨k ↦ v⟩ = f

⊢ ∀f a b c. f⟨a ↦ c; a ↦ b⟩ = f⟨a ↦ c⟩

⊢ ∀fm kv. fm |+ kv = FEMPTY |+ kv ⊌ fm

⊢ ∀fm kv. fm |+ kv = fm |++ [kv]

⊢ ¬MEM k (MAP FST kvl) ⇒ fm⟨k ↦ v⟩ |++ kvl = (fm |++ kvl)⟨k ↦ v⟩

⊢ MEM k (MAP FST kvl) ⇒ fm⟨k ↦ v⟩ |++ kvl = fm |++ kvl

⊢ ∀P ls k v fm.
    ALL_DISTINCT (MAP FST ls) ∧ MEM (k,v) ls ∧ P v ⇒ P (fm |++ ls)⟨k⟩

⊢ ∀ls ls' fm.
    ALL_DISTINCT (MAP FST ls) ∧ PERM ls ls' ⇒ fm |++ ls = fm |++ ls'

⊢ ∀ls. ALL_DISTINCT (MAP FST ls) ⇒ ∀fm. fm |++ REVERSE ls = fm |++ ls

⊢ fm |++ (kvl1 ⧺ kvl2) = fm |++ kvl1 |++ kvl2

⊢ ∀l1 l2 fm.
    DISJOINT (set (MAP FST l1)) (set (MAP FST l2)) ⇒
    fm |++ l1 |++ l2 = fm |++ l2 |++ l1

⊢ ∀P f kvl k.
    (∃n. n < LENGTH kvl ∧ k = (MAP FST kvl)❲n❳ ∧ P (MAP SND kvl)❲n❳ ∧
         ∀m. n < m ∧ m < LENGTH kvl ⇒ (MAP FST kvl)❲m❳ ≠ k) ∨
    ¬MEM k (MAP FST kvl) ∧ P f⟨k⟩ ⇒
    P (f |++ kvl)⟨k⟩

⊢ ∀kvl f k v n.
    n < LENGTH kvl ∧ k = (MAP FST kvl)❲n❳ ∧ v = (MAP SND kvl)❲n❳ ∧
    (∀m. n < m ∧ m < LENGTH kvl ⇒ (MAP FST kvl)❲m❳ ≠ k) ⇒
    (f |++ kvl)⟨k⟩ = v

⊢ ∀kvl f k. ¬MEM k (MAP FST kvl) ⇒ (f |++ kvl)⟨k⟩ = f⟨k⟩

⊢ ∀kvl f k v. ¬MEM k (MAP FST kvl) ∧ v = f⟨k⟩ ⇒ (f |++ kvl)⟨k⟩ = v

⊢ ∀ls1 fm ls2.
    (∀k. MEM k (MAP FST ls1) ⇒ MEM k (MAP FST ls2)) ⇒
    fm |++ ls1 |++ ls2 = fm |++ ls2

⊢ ∀fm ls. fm |++ ls = FEMPTY ⇔ fm = FEMPTY ∧ ls = []

⊢ ∀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

⊢ ∀kvl f1 f2.
    f1 |++ kvl = f2 |++ kvl ⇔
    DRESTRICT f1 (COMPL (set (MAP FST kvl))) =
    DRESTRICT f2 (COMPL (set (MAP FST kvl)))

⊢ ∀xs x fm. fm |++ SNOC x xs = (fm |++ xs) |+ x

⊢ ∀f. f |++ [] = f ∧ ∀h t. f |++ (h::t) = f |+ h |++ t

⊢ ∀f x y. f⟨x ↦ y⟩ = (f \\ x)⟨x ↦ y⟩

⊢ ∀f x y. (f \\ x)⟨x ↦ y⟩ = f⟨x ↦ y⟩

⊢ x = FST kv ∨ fm1⟨x⟩ = fm2⟨x⟩ ⇒ (fm1 |+ kv)⟨x⟩ = (fm2 |+ kv)⟨x⟩

⊢ ∀kvl fm1 fm2 x. MEM x (MAP FST kvl) ⇒ (fm1 |++ kvl)⟨x⟩ = (fm2 |++ kvl)⟨x⟩

⊢ ∀f1 f2 k v1 v2.
    f1⟨k ↦ v1⟩ = f2⟨k ↦ v2⟩ ⇒ v1 = v2 ∧ ∀v. f1⟨k ↦ v⟩ = f2⟨k ↦ v⟩

⊢ ∀f fm. IMAGE f (FRANGE fm) = FRANGE (f o_f fm)

⊢ ∀x hL. x ∈ FDOM (FOLDR FUNION FEMPTY hL) ⇔ ∃h. MEM h hL ∧ x ∈ FDOM h

⊢ ∀f v. v ∈ FRANGE f ⇔ ∃k. k ∈ FDOM f ∧ f⟨k⟩ = v

⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ⇒ ∀v. v ∈ FRANGE (fm \\ k) ⇒ P v

⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ⇒ ∀v. v ∈ FRANGE (DRESTRICT fm s) ⇒ P v

⊢ ∀f v. v ∈ FRANGE f ⇔ ∃k. FLOOKUP f k = SOME v

⊢ (∀v. v ∈ FRANGE f1 ⇒ P v) ∧ (∀v. v ∈ FRANGE f2 ⇒ P v) ⇒
  ∀v. v ∈ FRANGE (f1 ⊌ f2) ⇒ P v

⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ∧ (∀v. MEM v (MAP SND ls) ⇒ P v) ⇒
  ∀v. v ∈ FRANGE (fm |++ ls) ⇒ P v

⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ∧ P (SND kv) ⇒ ∀v. v ∈ FRANGE (fm |+ kv) ⇒ P v

⊢ (∀v. v ∈ FRANGE fm ⇒ P (f v)) ⇒ ∀v. v ∈ FRANGE (f o_f fm) ⇒ P v

⊢ ITFMAPR f FEMPTY A1 A2 ⇔ A1 = A2

⊢ ∀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

⊢ ∀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

⊢ ∀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)

⊢ ∀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

⊢ ∀fm r0. ∃r. ITFMAPR f fm r0 r

⊢ (∀k1 k2 v1 v2 A. k1 ≠ k2 ⇒ 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 f FEMPTY A = A

⊢ ITFMAP f FEMPTY A = A ∧
  ((∀k1 k2 v1 v2 A. k1 ≠ k2 ⇒ 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 ptr. ptr ∉ FDOM refs) ∉ FDOM refs

⊢ f PERMUTES 𝕌(:num) ⇒ MAP_KEYS f (MAP_KEYS (LINV f 𝕌(:num)) t) = t

⊢ ∀f. MAP_KEYS f FEMPTY = FEMPTY

⊢ ∀f fm k v.
    INJ f (k INSERT FDOM fm) 𝕌(:β) ⇒
    MAP_KEYS f fm⟨k ↦ v⟩ = (MAP_KEYS f fm)⟨f k ↦ v⟩

⊢ ∀f fm.
    INJ f (FDOM fm) 𝕌(:β) ⇒
    MAP_KEYS f fm =
    fm f_o_f FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm))

⊢ 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⟩)

⊢ ∀f a x y. a ≠ x ⇒ f⟨x ↦ y⟩⟨a⟩ = f⟨a⟩

⊢ ∀f a b. FEMPTY ≠ f⟨a ↦ b⟩

⊢ ∀f x. x ∉ FDOM f ⇒ DRESTRICT f (COMPL {x}) = f

⊢ ∀f x. x ∉ FDOM f ⇒ f⟨x⟩ = FEMPTY⟨x⟩

⊢ ∃x. x ∉ FDOM f

⊢ ∀r. RRESTRICT FEMPTY r = FEMPTY

⊢ ∀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

⊢ ∀f1 f2 k v1 v2. v1 ≠ v2 ⇒ f1⟨k ↦ v1⟩ ≠ f2⟨k ↦ v2⟩

⊢ ∀f r x y.
    x ∈ r ⇒ DRESTRICT f⟨x ↦ y⟩ r = (DRESTRICT f (r DELETE x))⟨x ↦ y⟩

⊢ ∀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)

⊢ ∀f g. f ⊑ g ∧ g ⊑ f ⇔ f = g

⊢ f \\ k ⊑ f

⊢ ∀f g k. f \\ k ⊑ g ⇔ f \\ k ⊑ g \\ k

⊢ DRESTRICT f P ⊑ f

⊢ f1 ⊑ f2 ∧ s1 ⊆ s2 ⇒ DRESTRICT f1 s1 ⊑ DRESTRICT f2 s2

⊢ f1 ⊑ f2 ⇒ FDOM f1 ⊆ FDOM f2

⊢ ∀f. FEMPTY ⊑ f

⊢ f ⊑ g ⇔ ∀x y. FLOOKUP f x = SOME y ⇒ FLOOKUP g x = SOME y

⊢ ∀f g. f ⊑ g ⇒ FRANGE f ⊆ FRANGE g

⊢ ∀f1 f2 f3.
    f1 ⊑ f2 ∨ DISJOINT (FDOM f1) (FDOM f2) ∧ f1 ⊑ f3 ⇒ f1 ⊑ f2 ⊌ f3

⊢ ∀f g. f ⊑ g ⇔ f ⊌ g = g

⊢ (∀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)

⊢ (∀f1 f2. f1 ⊑ f1 ⊌ f2) ∧
  ∀f1 f2. DISJOINT (FDOM f1) (FDOM f2) ⇒ f2 ⊑ f1 ⊌ f2

⊢ ∀f g x y. f⟨x ↦ y⟩ ⊑ g ⇔ x ∈ FDOM g ∧ g⟨x⟩ = y ∧ f \\ x ⊑ g \\ x

⊢ f ⊑ f⟨x ↦ y⟩ ⇔ x ∉ FDOM f ∨ f⟨x⟩ = y ∧ x ∈ FDOM f

⊢ k ∉ FDOM f ⇒ f ⊑ f⟨k ↦ v⟩

⊢ f ⊑ f⟨x ↦ y⟩ ⇔ FLOOKUP f x = NONE ∨ FLOOKUP f x = SOME y

⊢ ∀f. f ⊑ f

⊢ ∀f g h. f ⊑ g ∧ g ⊑ h ⇒ f ⊑ h

⊢ ∀f g x y. f \\ x ⊑ g \\ x ⇒ f⟨x ↦ y⟩ ⊑ g⟨x ↦ y⟩

⊢ (x ∈ FDOM m ⇔ FLOOKUP m x ≠ NONE) ∧
  (y ∈ FRANGE m ⇔ ∃k. FLOOKUP m k = SOME y) ∧
  (FLOOKUP m x ≠ NONE ⇒ m⟨x⟩ = THE (FLOOKUP m x)) ∧
  (m = m' ⇔ FLOOKUP m = FLOOKUP m') ∧
  (m ⊑ m' ⇔ ∀k v. FLOOKUP m k = SOME v ⇒ FLOOKUP m' k = SOME v) ∧
  (FEVERY P m ⇔ ∀k v. FLOOKUP m k = SOME v ⇒ P (k,v))

⊢ FINITE s ⇒ WF (lbound s $PSUBSETᵀ)

⊢ ∀s m. DISJOINT s (FDOM m) ⇒ DRESTRICT m (COMPL s) = m

⊢ ∀m l. FOLDR (λk m. m \\ k) m l = DRESTRICT m (COMPL (set l))

⊢ (∀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

⊢ ∀g. FEMPTY f_o g = FEMPTY

⊢ ∀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. FEMPTY f_o_f f = FEMPTY

⊢ ∀f. f f_o_f FEMPTY = FEMPTY

⊢ ∀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⟩

⊢ ∀kvl fm.
    FDOM (fm |++ kvl) = FDOM fm DIFF set (MAP FST kvl) ∪ set (MAP FST kvl)

⊢ ∀P m1 m2. FEVERY P m1 ∧ FEVERY P m2 ⇒ FEVERY P (m1 ⊌ m2)

⊢ ∀f x v.
    (FLOOKUP f x = NONE ⇔ x ∉ FDOM f) ∧
    (FLOOKUP f x = SOME v ⇔ x ∈ FDOM f ∧ f⟨x⟩ = v)

⊢ ∀f. f = FEMPTY ∨ ∃g x y. f = g⟨x ↦ y⟩

⊢ ∀f g. FDOM f = FDOM g ∧ FAPPLY f = FAPPLY g ⇔ f = g

⊢ ∀f g. FDOM f = FDOM g ∧ (∀x. x ∈ FDOM f ⇒ f⟨x⟩ = g⟨x⟩) ⇔ f = g

⊢ ∀f1 f2. fmap_EQ_UPTO f1 f2 ∅ ⇔ f1 = f2

⊢ ∀vs f. fmap_EQ_UPTO f f vs

⊢ ∀f1 f2 ks k v.
    fmap_EQ_UPTO f1 f2 ks ⇒ fmap_EQ_UPTO f1⟨k ↦ v⟩ f2⟨k ↦ v⟩ (ks DELETE k)

⊢ ∀f1 f2 ks k v.
    fmap_EQ_UPTO f1 f2 ks ⇒ fmap_EQ_UPTO f1⟨k ↦ v⟩ f2⟨k ↦ v⟩ ks

⊢ ∀f1 f2 ks k v.
    fmap_EQ_UPTO f1 f2 ks ⇒ fmap_EQ_UPTO f1⟨k ↦ v⟩ f2 (k INSERT ks)

⊢ ∀f g. f = g ⇔ FDOM f = FDOM g ∧ ∀x. x ∈ FDOM f ⇒ f⟨x⟩ = g⟨x⟩

⊢ ∀P. P FEMPTY ∧ (∀f. P f ⇒ ∀x y. x ∉ FDOM f ⇒ P f⟨x ↦ y⟩) ⇒ ∀f. P f

⊢ ∀P. P FEMPTY ∧ (∀f. P f ⇒ ∀x y. P f⟨x ↦ y⟩) ⇒ ∀f. P f

⊢ ∀fm. fm = FEMPTY ∨ ∃k v fm0. k ∉ FDOM fm0 ∧ fm = fm0⟨k ↦ v⟩

⊢ f1 = f2 ⇔ ∀x. FLOOKUP f1 x = FLOOKUP f2 x

⊢ (fmap_rel R FEMPTY f2 ⇔ f2 = FEMPTY) ∧
  (fmap_rel R f1 FEMPTY ⇔ f1 = FEMPTY)

⊢ 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 R f1 f2 ∧ fmap_rel R f3 f4 ⇒ fmap_rel R (f1 ⊌ f3) (f2 ⊌ f4)

⊢ fmap_rel R (f1 \\ k) (f2 \\ k) ∧ R v1 v2 ⇔
  fmap_rel R f1⟨k ↦ v1⟩ f2⟨k ↦ v2⟩

⊢ fmap_rel R (f1 \\ k) (f2 \\ k) ∧ R v1 v2 ⇒
  fmap_rel R f1⟨k ↦ v1⟩ f2⟨k ↦ v2⟩

⊢ ∀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 R f1 f2 ∧ R v1 v2 ⇒ fmap_rel R f1⟨k ↦ v1⟩ f2⟨k ↦ v2⟩

⊢ fmap_rel R f1 f2 ⇔ ∀k. OPTREL R (FLOOKUP f1 k) (FLOOKUP f2 k)

⊢ ∀R FR.
    FR FEMPTY FEMPTY ∧
    (∀k v1 v2 f1 f2.
       R v1 v2 ∧ FR (f1 \\ k) (f2 \\ k) ⇒ FR f1⟨k ↦ v1⟩ f2⟨k ↦ v2⟩) ⇒
    ∀f1 f2. fmap_rel R f1 f2 ⇒ FR f1 f2

⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ fmap_rel R1 f1 f2 ⇒ fmap_rel R2 f1 f2

⊢ (∀x. R x x) ⇒ fmap_rel R x x

⊢ (∀x y. R x y ⇒ R y x) ⇒ ∀x y. fmap_rel R x y ⇒ fmap_rel R y x

⊢ (∀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

⊢ ∀m. ∃l. ALL_DISTINCT (MAP FST l) ∧ m = FEMPTY |++ l

⊢ ∀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

⊢ ∀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

⊢ (∀k v. FLOOKUP fm k = SOME v ⇒ f k v A = A) ⇒
  (fmlfpR f fm A fm A B ⇔ A = B)

⊢ ∀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

⊢ ∀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

⊢ ∀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)

⊢ 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 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

⊢ ∀m l. FOLDL (λenv (k,v). env⟨k ↦ v⟩) m l = m |++ l

⊢ ∀m l. FOLDR (λ(k,v) env. env⟨k ↦ v⟩) m l = m |++ REVERSE l

⊢ ∀l f x y.
    x ∈ FDOM (FEMPTY |++ l) ⇒
    (FEMPTY |++ MAP (λ(a,b). (a,f b)) l)⟨x⟩ = f (FEMPTY |++ l)⟨x⟩

⊢ ∀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'.
    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 (λa. INR ()) ∧
  ∀f a b. is_fmap f ⇒ is_fmap (λx. if x = a then INL b else f x)

⊢ ∀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

⊢ g o_f fm \\ k = g o_f (fm \\ k)

⊢ ∀f g x. x ∈ FDOM g ⇒ (f o_f g)⟨x⟩ = f g⟨x⟩

⊢ ∀f g. FDOM g = FDOM (f o_f g)

⊢ f o_f FEMPTY = FEMPTY

⊢ x ∈ FRANGE g ⇒ f x ∈ FRANGE (f o_f g)

⊢ f o_f (f1 ⊌ f2) = f o_f f1 ⊌ f o_f f2

⊢ f o_f fm⟨k ↦ v⟩ = (f o_f fm)⟨k ↦ f v⟩

⊢ ∀f fm f' fm'.
    fm = fm' ∧ (∀v. v ∈ FRANGE fm ⇒ f v = f' v) ⇒ f o_f fm = f' o_f fm'

⊢ ∀m. (λx. x) o_f m = m

⊢ f o_f g o_f h = (f ∘ g) o_f h