---

Step * of Lemma C_TYPE-induction3

∀[P:C_TYPE() ─→ ℙ]
  (P[C_Void()]
  ⇒ P[C_Int()]
  ⇒ (∀fields:(Atom × C_TYPE()) List. ((∀ct∈map(λp.(snd(p));fields).P[ct]) ⇒ P[C_Struct(fields)]))
  ⇒ (∀length:ℕ. ∀elems:C_TYPE().  (P[elems] ⇒ P[C_Array(length;elems)]))
  ⇒ (∀to:C_TYPE(). (P[to] ⇒ P[C_Pointer(to)]))
  ⇒ {∀x:C_TYPE(). P[x]})
BY
{ (InstLemma `C_TYPE-induction2` [] THEN RepeatFor 4 ((ParallelLast' THENA Auto))) }

1
1. [P] : C_TYPE() ─→ ℙ
2. P[C_Void()]@i
3. P[C_Int()]@i
4. ∀fields:(Atom × C_TYPE()) List. ((∀ct∈map(λp.(snd(p));fields).P[ct]) ⇒ P[C_Struct(fields)])@i
5. fields : (Atom × C_TYPE()) List@i
6. ∀i:ℕ||fields||. P[snd(fields[i])]@i
⊢ P[C_Struct(fields)]

---

Latex:


\mforall{}[P:C\_TYPE()  {}\mrightarrow{}  \mBbbP{}]
    (P[C\_Void()]
    {}\mRightarrow{}  P[C\_Int()]
    {}\mRightarrow{}  (\mforall{}fields:(Atom  \mtimes{}  C\_TYPE())  List.  ((\mforall{}ct\mmember{}map(\mlambda{}p.(snd(p));fields).P[ct])  {}\mRightarrow{}  P[C\_Struct(fields)]))
    {}\mRightarrow{}  (\mforall{}length:\mBbbN{}.  \mforall{}elems:C\_TYPE().    (P[elems]  {}\mRightarrow{}  P[C\_Array(length;elems)]))
    {}\mRightarrow{}  (\mforall{}to:C\_TYPE().  (P[to]  {}\mRightarrow{}  P[C\_Pointer(to)]))
    {}\mRightarrow{}  \{\mforall{}x:C\_TYPE().  P[x]\})


By

(InstLemma  `C\_TYPE-induction2`  []  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto)))

---

Home Index