Theory fmaptree

⊢ ∀i fm. FTNode i fm = fromF (construct i (toF o_f fm))

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

⊢ ∀a kfm kl.
    construct a kfm kl =
    case kl of
      [] => SOME a
    | h::t => if h ∈ FDOM kfm then kfm⟨h⟩ t else NONE

⊢ (∀a. fromF (toF a) = a) ∧ ∀r. wf r ⇔ toF (fromF r) = r

⊢ ∃rep. TYPE_DEFINITION wf rep

⊢ ∀h ft. fmtreerec h ft = @r. relrec h ft r

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

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

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

⊢ FTNode i1 f1 = FTNode i2 f2 ⇔ i1 = i2 ∧ f1 = f2

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

⊢ ∀ft. ∃i fm. ft = FTNode i fm

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

⊢ ∀h a0 a1.
    relrec h a0 a1 ⇔
    ∃i fm rfm.
      a0 = FTNode i fm ∧ a1 = h i rfm fm ∧ FDOM rfm = FDOM fm ∧
      ∀d. d ∈ FDOM fm ⇒ relrec h fm⟨d⟩ rfm⟨d⟩

⊢ ∀h relrec'.
    (∀i fm rfm.
       FDOM rfm = FDOM fm ∧ (∀d. d ∈ FDOM fm ⇒ relrec' fm⟨d⟩ rfm⟨d⟩) ⇒
       relrec' (FTNode i fm) (h i rfm fm)) ⇒
    ∀a0 a1. relrec h a0 a1 ⇒ relrec' a0 a1

⊢ ∀h i fm rfm.
    FDOM rfm = FDOM fm ∧ (∀d. d ∈ FDOM fm ⇒ relrec h fm⟨d⟩ rfm⟨d⟩) ⇒
    relrec h (FTNode i fm) (h i rfm fm)

⊢ ∀h relrec'.
    (∀i fm rfm.
       FDOM rfm = FDOM fm ∧
       (∀d. d ∈ FDOM fm ⇒ relrec h fm⟨d⟩ rfm⟨d⟩ ∧ relrec' fm⟨d⟩ rfm⟨d⟩) ⇒
       relrec' (FTNode i fm) (h i rfm fm)) ⇒
    ∀a0 a1. relrec h a0 a1 ⇒ relrec' a0 a1

⊢ ∀a0. wf a0 ⇔ ∃a fm. a0 = construct a fm ∧ ∀k. k ∈ FDOM fm ⇒ wf fm⟨k⟩

⊢ ∀wf'.
    (∀a fm. (∀k. k ∈ FDOM fm ⇒ wf' fm⟨k⟩) ⇒ wf' (construct a fm)) ⇒
    ∀a0. wf a0 ⇒ wf' a0

⊢ ∀a fm. (∀k. k ∈ FDOM fm ⇒ wf fm⟨k⟩) ⇒ wf (construct a fm)

⊢ ∀wf'.
    (∀a fm. (∀k. k ∈ FDOM fm ⇒ wf fm⟨k⟩ ∧ wf' fm⟨k⟩) ⇒ wf' (construct a fm)) ⇒
    ∀a0. wf a0 ⇒ wf' a0