---

Step * of Lemma C_LVALUE-induction

∀[P:C_LVALUE() ─→ ℙ]
  ((∀loc:C_LOCATION(). P[LV_Ground(loc)])
  ⇒ (∀lval:C_LVALUE(). ∀idx:ℤ.  (P[lval] ⇒ P[LV_Index(lval;idx)]))
  ⇒ (∀lval:C_LVALUE(). ∀comp:Atom.  (P[lval] ⇒ P[LV_Scomp(lval;comp)]))
  ⇒ {∀v:C_LVALUE(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[P:C\_LVALUE()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}loc:C\_LOCATION().  P[LV\_Ground(loc)])
    {}\mRightarrow{}  (\mforall{}lval:C\_LVALUE().  \mforall{}idx:\mBbbZ{}.    (P[lval]  {}\mRightarrow{}  P[LV\_Index(lval;idx)]))
    {}\mRightarrow{}  (\mforall{}lval:C\_LVALUE().  \mforall{}comp:Atom.    (P[lval]  {}\mRightarrow{}  P[LV\_Scomp(lval;comp)]))
    {}\mRightarrow{}  \{\mforall{}v:C\_LVALUE().  P[v]\})


By

ProveDatatypeInd

---

Home Index