Theory EVAL_quote

⊢ (∀a0 f f0 v. index_CASE (Left_idx a0) f f0 v = f a0) ∧
  (∀a0 f f0 v. index_CASE (Right_idx a0) f f0 v = f0 a0) ∧
  ∀f f0 v. index_CASE End_idx f f0 v = v

⊢ ∀i1 i2. index_lt i1 i2 ⇔ index_compare i1 i2 = LESS

⊢ (∀a0. index_size (Left_idx a0) = 1 + index_size a0) ∧
  (∀a0. index_size (Right_idx a0) = 1 + index_size a0) ∧
  index_size End_idx = 0

⊢ ∀f af.
    varmapMAP f (varmap_CONS af) =
    varmap_CONS (SUM_MAP I (f ## varmapMAP f ## varmapMAP f) af)

⊢ varmapREL =
  (λR x y.
     ∃z. (∀p. p ∈ varmapSET z ⇒ R (FST p) (SND p)) ∧ varmapMAP FST z = x ∧
         varmapMAP SND z = y)

⊢ ∀af.
    varmapSET (varmap_CONS af) =
    S ($UNION ∘ BIMG (K ∅) ∘ setL)
      (BIMG
         (S ($UNION ∘ BIMG $= ∘ setFST)
            (BIMG (S ($UNION ∘ BIMG (K ∅) ∘ setFST) (BIMG (K ∅) ∘ setSND)) ∘
             setSND)) ∘ setR) af ∪
    BIGUNION
      (IMAGE varmapSET
         (S ($UNION ∘ BIMG (K ∅) ∘ setL)
            (BIMG
               (S ($UNION ∘ BIMG (K ∅) ∘ setFST)
                  (BIMG (S ($UNION ∘ BIMG $= ∘ setFST) (BIMG $= ∘ setSND)) ∘
                   setSND)) ∘ setR) af))

⊢ (∀v f. varmap_CASE Empty_vm v f = v) ∧
  ∀a0 a1 a2 v f. varmap_CASE (Node_vm a0 a1 a2) v f = f a0 a1 a2

⊢ (∀f0. varmap_size f0 Empty_vm = 0) ∧
  ∀f0 a0 a1 a2.
    varmap_size f0 (Node_vm a0 a1 a2) =
    1 + (f0 a0 + (varmap_size f0 a1 + varmap_size f0 a2))

⊢ ∀i1 i2. index_compare i1 i2 = EQUAL ⇔ i1 = i2

⊢ ∀l1 l2. list_compare index_compare l1 l2 = EQUAL ⇔ l1 = l2

⊢ DATATYPE (index Left_idx Right_idx End_idx)

⊢ DATATYPE (varmap Empty_vm Node_vm)

⊢ (∀a0 a0'. Left_idx a0 = Left_idx a0' ⇔ a0 = a0') ∧
  ∀a0 a0'. Right_idx a0 = Right_idx a0' ⇔ a0 = a0'

⊢ ∀f0 f1 f2. ∃h.
    (∀a0. h (Left_idx a0) = f0 a0 (h a0)) ∧
    (∀a0. h (Right_idx a0) = f1 a0 (h a0)) ∧ h End_idx = f2

⊢ ∀M M' f f0 v.
    M = M' ∧ (∀a0. M' = Left_idx a0 ⇒ f a0 = f' a0) ∧
    (∀a0. M' = Right_idx a0 ⇒ f0 a0 = f0' a0) ∧ (M' = End_idx ⇒ v = v') ⇒
    index_CASE M f f0 v = index_CASE M' f' f0' v'

⊢ index_CASE x f f0 v = v' ⇔
  (∃i. x = Left_idx i ∧ f i = v') ∨ (∃i. x = Right_idx i ∧ f0 i = v') ∨
  x = End_idx ∧ v = v'

⊢ index_compare End_idx End_idx = EQUAL ∧
  (∀v10. index_compare End_idx (Left_idx v10) = LESS) ∧
  (∀v11. index_compare End_idx (Right_idx v11) = LESS) ∧
  (∀v2. index_compare (Left_idx v2) End_idx = GREATER) ∧
  (∀v3. index_compare (Right_idx v3) End_idx = GREATER) ∧
  (∀n' m'. index_compare (Left_idx n') (Left_idx m') = index_compare n' m') ∧
  (∀n' m'. index_compare (Left_idx n') (Right_idx m') = LESS) ∧
  (∀n' m'.
     index_compare (Right_idx n') (Right_idx m') = index_compare n' m') ∧
  ∀n' m'. index_compare (Right_idx n') (Left_idx m') = GREATER

⊢ ∀P. P End_idx End_idx ∧ (∀v10. P End_idx (Left_idx v10)) ∧
      (∀v11. P End_idx (Right_idx v11)) ∧ (∀v2. P (Left_idx v2) End_idx) ∧
      (∀v3. P (Right_idx v3) End_idx) ∧
      (∀n' m'. P n' m' ⇒ P (Left_idx n') (Left_idx m')) ∧
      (∀n' m'. P (Left_idx n') (Right_idx m')) ∧
      (∀n' m'. P n' m' ⇒ P (Right_idx n') (Right_idx m')) ∧
      (∀n' m'. P (Right_idx n') (Left_idx m')) ⇒
      ∀v v1. P v v1

⊢ (∀a0' a0. Left_idx a0 ≠ Right_idx a0') ∧ (∀a0. Left_idx a0 ≠ End_idx) ∧
  ∀a0. Right_idx a0 ≠ End_idx

⊢ ∀P. (∀i. P i ⇒ P (Left_idx i)) ∧ (∀i. P i ⇒ P (Right_idx i)) ∧ P End_idx ⇒
      ∀i. P i

⊢ ∀ii. (∃i. ii = Left_idx i) ∨ (∃i. ii = Right_idx i) ∨ ii = End_idx

⊢ ∀P'.
    (∀f. P' f Empty_vm ∧
         ∀v v0. P' f v ∧ P' f v0 ⇒ ∀a. P' f (Node_vm a v v0)) ⇒
    ∀f v. P' f v

⊢ varmapMAP f Empty_vm = Empty_vm ∧
  varmapMAP f (Node_vm a0 a1 a2) =
  Node_vm (f a0) (varmapMAP f a1) (varmapMAP f a2)

⊢ ∀P'.
    P' Empty_vm ∧ (∀v v0. P' v ∧ P' v0 ⇒ ∀a. P' (Node_vm a v v0)) ⇒
    ∀v. P' v

⊢ varmapSET Empty_vm = ∅ ∧
  varmapSET (Node_vm a0 a1 a2) = a0 INSERT varmapSET a1 ∪ varmapSET a2

⊢ ∀a0 a1 a2 a0' a1' a2'.
    Node_vm a0 a1 a2 = Node_vm a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'

⊢ ∀f0 f1. ∃h.
    h Empty_vm = f0 ∧
    ∀a0 a1 a2. h (Node_vm a0 a1 a2) = f1 a0 a1 a2 (h a1) (h a2)

⊢ ∀f g x. (∀a. a ∈ varmapSET x ⇒ f a = g a) ⇒ varmapMAP f x = varmapMAP g x

⊢ varmapMAP I = I

⊢ ∀f n. varmapSET (varmapMAP f n) = IMAGE f (varmapSET n)

⊢ varmapMAP f ∘ varmapMAP g = varmapMAP (f ∘ g)

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

⊢ ∀M M' v f.
    M = M' ∧ (M' = Empty_vm ⇒ v = v') ∧
    (∀a0 a1 a2. M' = Node_vm a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
    varmap_CASE M v f = varmap_CASE M' v' f'

⊢ varmap_CASE x v f = v' ⇔
  x = Empty_vm ∧ v = v' ∨ ∃a v'' v0. x = Node_vm a v'' v0 ∧ f a v'' v0 = v'

⊢ ∀a2 a1 a0. Empty_vm ≠ Node_vm a0 a1 a2

⊢ (∀x v2 v1. varmap_find End_idx (Node_vm x v1 v2) = x) ∧
  (∀x v2 v1 i1.
     varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) ∧
  (∀x v2 v1 i1.
     varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1) ∧
  ∀i. varmap_find i Empty_vm = @x. T

⊢ ∀P. (∀x v1 v2. P End_idx (Node_vm x v1 v2)) ∧
      (∀i1 x v1 v2. P i1 v2 ⇒ P (Right_idx i1) (Node_vm x v1 v2)) ∧
      (∀i1 x v1 v2. P i1 v1 ⇒ P (Left_idx i1) (Node_vm x v1 v2)) ∧
      (∀i. P i Empty_vm) ⇒
      ∀v v1. P v v1

⊢ ∀P. P Empty_vm ∧ (∀v v0. P v ∧ P v0 ⇒ ∀a. P (Node_vm a v v0)) ⇒ ∀v. P v

⊢ ∀a2. a2 ∈ varmapSET ((λa2. varmap_CONS (INR (flip $, ARB a2))) a2)

⊢ ∀vv. vv = Empty_vm ∨ ∃a v v0. vv = Node_vm a v v0

⊢ ∀a. varmapSET ((λa. varmap_CONS ((K ∘ INL) ARB ARB)) a) ⊆ ∅