Theory fmaptree

⊢ (∀ft. apply_path [] ft = SOME ft) ∧
  ∀h t ft.
    apply_path (h::t) ft =
    if h ∈ FDOM (map ft) then apply_path t (map ft)⟨h⟩ else NONE

⊢ ∀f af.
    fmaptreeMAP f (fmaptree_CONS af) =
    fmaptree_CONS ((f ## $o_f (fmaptreeMAP f)) af)

⊢ fmaptreeREL =
  (λR x y.
     ∃z. (∀p. p ∈ fmaptreeSET z ⇒ R (FST p) (SND p)) ∧
         fmaptreeMAP FST z = x ∧ fmaptreeMAP SND z = y)

⊢ ∀af.
    fmaptreeSET (fmaptree_CONS af) =
    S ($UNION ∘ BIMG $= ∘ setFST) (BIMG (BIMG (K ∅) ∘ FRANGE) ∘ setSND) af ∪
    BIGUNION
      (IMAGE fmaptreeSET
         (S ($UNION ∘ BIMG (K ∅) ∘ setFST)
            (BIMG (BIMG $= ∘ FRANGE) ∘ setSND) af))

⊢ ∀a0 a1 f. fmaptree_CASE (FTNode a0 a1) f = f a0 a1

⊢ ∀f0 f1 a0 a1.
    fmaptree_size f0 f1 (FTNode a0 a1) =
    1 +
    (f1 a0 + fmap_size (λk. 0) (λv. 1 + v) (fmaptree_size f0 f1 o_f a1))

⊢ ∀h i fm. fmtreerec h (FTNode i fm) = h i (fmtreerec h o_f fm) fm

⊢ (∀f ft. fupd_at_path [] f ft = f ft) ∧
  ∀h t f ft.
    fupd_at_path (h::t) f ft =
    if h ∈ FDOM (map ft) then
      case fupd_at_path t f (map ft)⟨h⟩ of
        NONE => NONE
      | SOME ft' => SOME (FTNode (item ft) (map ft)⟨h ↦ ft'⟩)
    else NONE

⊢ ∀ff. ff = FTNode (item ff) (map ff)

⊢ (∀a ft. update_at_path [] a ft = SOME (FTNode a (map ft))) ∧
  ∀h t a ft.
    update_at_path (h::t) a ft =
    if h ∈ FDOM (map ft) then
      case update_at_path t a (map ft)⟨h⟩ of
        NONE => NONE
      | SOME ft' => SOME (FTNode (item ft) (map ft)⟨h ↦ ft'⟩)
    else NONE

⊢ ∀a0 a1 a0' a1'. FTNode a0 a1 = FTNode a0' a1' ⇔ a0 = a0' ∧ a1 = a1'

⊢ ∀ft. FINITE {p | (∃ft'. apply_path p ft = SOME ft')}

⊢ ∀ft x p.
    apply_path (p ⧺ [x]) ft =
    case apply_path p ft of NONE => NONE | SOME ft' => FLOOKUP (map ft') x

⊢ DATATYPE (fmaptree FTNode)

⊢ ∀P'.
    (∀f' f. (∀f0. f0 ∈ FRANGE f ⇒ P' f' f0) ⇒ ∀v. P' f' (FTNode v f)) ⇒
    ∀f' f. P' f' f

⊢ fmaptreeMAP f (FTNode a0 a1) = FTNode (f a0) (fmaptreeMAP f o_f a1)

⊢ ∀P'. (∀f. (∀f0. f0 ∈ FRANGE f ⇒ P' f0) ⇒ ∀v. P' (FTNode v f)) ⇒ ∀f. P' f

⊢ fmaptreeSET (FTNode a0 a1) =
  a0 INSERT BIGUNION (IMAGE fmaptreeSET (FRANGE a1))

⊢ ∀a0 a1 a0' a1'. FTNode a0 a1 = FTNode a0' a1' ⇔ a0 = a0' ∧ a1 = a1'

⊢ ∀f0. ∃h. ∀a0 a1. h (FTNode a0 a1) = f0 a0 a1 (h o_f a1)

⊢ ∀f g x.
    (∀a. a ∈ fmaptreeSET x ⇒ f a = g a) ⇒ fmaptreeMAP f x = fmaptreeMAP g x

⊢ fmaptreeMAP I = I

⊢ ∀f n. fmaptreeSET (fmaptreeMAP f n) = IMAGE f (fmaptreeSET n)

⊢ fmaptreeMAP f ∘ fmaptreeMAP g = fmaptreeMAP (f ∘ g)

⊢ ∀n. cardleq (fmaptreeSET n) 𝕌(:num)

⊢ ∀M M' f.
    M = M' ∧ (∀a0 a1. M' = FTNode a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒
    fmaptree_CASE M f = fmaptree_CASE M' f'

⊢ fmaptree_CASE x f = v ⇔ ∃v' f'. x = FTNode v' f' ∧ f v' f' = v

⊢ ∀P. (∀f. (∀f0. f0 ∈ FRANGE f ⇒ P f0) ⇒ ∀v. P (FTNode v f)) ⇒ ∀f. P f

⊢ ∀a2. a2 ∈ fmaptreeSET ((λa2. fmaptree_CONS (flip $, ARB a2)) a2)

⊢ ∀ff. ∃v f. ff = FTNode v f

⊢ ∀a. fmaptreeSET ((λa. fmaptree_CONS (a,K FEMPTY ARB)) a) ⊆ {a}

⊢ ∀h. ∃f. ∀i fm. f (FTNode i fm) = h i fm (f o_f fm)

⊢ fmtreerec h (FTNode i fm) = h i (fmtreerec h o_f fm) fm

⊢ ∀P. (∀a fm. (∀k. k ∈ FDOM fm ⇒ P fm⟨k⟩) ⇒ P (FTNode a fm)) ⇒ ∀ft. P ft

⊢ item (FTNode i fm) = i

⊢ map (FTNode i fm) = fm