---

Step * 1 of Lemma assert-C_TYPE_eq


∀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())))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN (BLemma `C_TYPE-induction` THENA Auto) THEN Reduce 0 THEN Auto) }

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

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

---

Latex:

---

Latex:

\mforall{}fields:(Atom  \mtimes{}  C\_TYPE())  List
    ((\mforall{}u\mmember{}fields.let  u1,u2  =  u 
                            in  \mforall{}b:C\_TYPE().  uiff(\muparrow{}(C\_TYPE\_eq\_fun(u2)  b);u2  =  b))
    {}\mRightarrow{}  (\mforall{}b:C\_TYPE()
                uiff(\muparrow{}(C\_Struct?(b)
                \mwedge{}\msubb{}  (||fields||  =\msubz{}  ||C\_Struct-fields(b)||)
                \mwedge{}\msubb{}  (\mforall{}i\mmember{}upto(||fields||).fst(fields[i])  =a  fst(C\_Struct-fields(b)[i])
                            \mwedge{}\msubb{}  (let  v2,v3  =  fields[i] 
                                    in  C\_TYPE\_eq\_fun(v3) 
                                    (snd(C\_Struct-fields(b)[i]))))\_b);C\_Struct(fields)  =  b)))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  (BLemma  `C\_TYPE-induction`  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index