---

Step * of Lemma C_LVALUE-definition

∀[A:Type]. ∀[R:A ⟶ C_LVALUE() ⟶ ℙ].
  ((∀loc:C_LOCATION(). {x:A| R[x;LV_Ground(loc)]} )
  ⇒ (∀lval:C_LVALUE(). ∀idx:ℤ.  ({x:A| R[x;lval]}  ⇒ {x:A| R[x;LV_Index(lval;idx)]} ))
  ⇒ (∀lval:C_LVALUE(). ∀comp:Atom.  ({x:A| R[x;lval]}  ⇒ {x:A| R[x;LV_Scomp(lval;comp)]} ))
  ⇒ {∀v:C_LVALUE(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `C_LVALUE-induction` }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeDefinition  `C\_LVALUE-induction`

---

Home Index