---

Step * 2 of Lemma assert-C_TYPE_eq


∀length:ℕ. ∀elems:C_TYPE().
  ((∀b:C_TYPE(). uiff(↑(C_TYPE_eq_fun(elems) b);elems = b ∈ C_TYPE()))
  ⇒ (∀b:C_TYPE()
        uiff(↑(C_Array?(b)
        ∧b (length =z C_Array-length(b))
        ∧b (C_TYPE_eq_fun(elems) C_Array-elems(b)));C_Array(length;elems) = b ∈ C_TYPE())))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (BLemma `C_TYPE-induction` THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN (RW assert_pushdownC (-1)⋅ THENA Auto)
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}length:\mBbbN{}.  \mforall{}elems:C\_TYPE().
    ((\mforall{}b:C\_TYPE().  uiff(\muparrow{}(C\_TYPE\_eq\_fun(elems)  b);elems  =  b))
    {}\mRightarrow{}  (\mforall{}b:C\_TYPE()
                uiff(\muparrow{}(C\_Array?(b)
                \mwedge{}\msubb{}  (length  =\msubz{}  C\_Array-length(b))
                \mwedge{}\msubb{}  (C\_TYPE\_eq\_fun(elems)  C\_Array-elems(b)));C\_Array(length;elems)  =  b)))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (BLemma  `C\_TYPE-induction`  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RW  assert\_pushdownC  (-1)\mcdot{}  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index