---

Step * of Lemma C_TYPE-induction2

∀[P:C_TYPE() ─→ ℙ]
  (P[C_Void()]
  ⇒ P[C_Int()]
  ⇒ (∀fields:(Atom × C_TYPE()) List. ((∀i:ℕ||fields||. P[snd(fields[i])]) ⇒ 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-induction` [] THEN RepeatFor 4 ((ParallelLast' THENA Auto)) THEN BackThruSomeHyp) }

1
1. [P] : C_TYPE() ─→ ℙ
2. P[C_Void()]@i
3. P[C_Int()]@i
4. ∀fields:(Atom × C_TYPE()) List. ((∀i:ℕ||fields||. P[snd(fields[i])]) ⇒ P[C_Struct(fields)])@i
5. fields : (Atom × C_TYPE()) List@i
6. (∀u∈fields.let u1,u2 = u 
              in P[u2])@i
⊢ ∀i:ℕ||fields||. P[snd(fields[i])]

---

Latex:


\mforall{}[P:C\_TYPE()  {}\mrightarrow{}  \mBbbP{}]
    (P[C\_Void()]
    {}\mRightarrow{}  P[C\_Int()]
    {}\mRightarrow{}  (\mforall{}fields:(Atom  \mtimes{}  C\_TYPE())  List.  ((\mforall{}i:\mBbbN{}||fields||.  P[snd(fields[i])])  {}\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-induction`  []  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))  THEN  BackThruSomeHyp)

---

Home Index