---

Step * of Lemma assert-C_TYPE_eq

∀[a,b:C_TYPE()].  uiff(↑C_TYPE_eq(a;b);a = b ∈ C_TYPE())
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN Unfold `C_TYPE_eq` 0
   THEN (BLemma `C_TYPE-induction` THENA Auto)
   THEN Unfold `C_TYPE_eq_fun` 0
   THEN Reduce 0
   THEN Try (Fold `C_TYPE_eq_fun` 0)
   THEN Try (Complete (((BLemma `C_TYPE-induction` THENA Auto) THEN Reduce 0 THEN Auto)))) }

1
∀fields:(Atom × C_TYPE()) List
  ((∀u∈fields.let u1,u2 = u 
              in ∀b:C_TYPE(). uiff(↑(C_TYPE_eq_fun(u2) b);u2 = b ∈ C_TYPE()))
  ⇒ (∀b:C_TYPE()
        uiff(↑(C_Struct?(b)
        ∧b (||fields|| =z ||C_Struct-fields(b)||)
        ∧b (∀i∈upto(||fields||).fst(fields[i]) =a fst(C_Struct-fields(b)[i])
              ∧b (let v2,v3 = fields[i] in C_TYPE_eq_fun(v3) (snd(C_Struct-fields(b)[i]))))_b);C_Struct(fields)
        = b
        ∈ C_TYPE())))

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

3
∀to:C_TYPE()
  ((∀b:C_TYPE(). uiff(↑(C_TYPE_eq_fun(to) b);to = b ∈ C_TYPE()))
  ⇒ (∀b:C_TYPE(). uiff(↑(C_Pointer?(b) ∧b (C_TYPE_eq_fun(to) C_Pointer-to(b)));C_Pointer(to) = b ∈ C_TYPE())))

---

Latex:

---

Latex:
\mforall{}[a,b:C\_TYPE()].    uiff(\muparrow{}C\_TYPE\_eq(a;b);a  =  b)


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  Unfold  `C\_TYPE\_eq`  0
  THEN  (BLemma  `C\_TYPE-induction`  THENA  Auto)
  THEN  Unfold  `C\_TYPE\_eq\_fun`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `C\_TYPE\_eq\_fun`  0)
  THEN  Try  (Complete  (((BLemma  `C\_TYPE-induction`  THENA  Auto)  THEN  Reduce  0  THEN  Auto))))

---

Home Index