---

Step * 1 of Lemma C_LVALUE-proper-Scomp

.....truecase..... 
1. env : C_TYPE_env()@i
2. lval : C_LVALUE()@i
3. comp : Atom@i
4. (↑LV_Scomp?(lval))
⇒ (↑C_LVALUE-proper(env;lval))
⇒ ((↑C_LVALUE-proper(env;LV_Scomp-lval(lval)))
   ∧ (↑C_Struct?(outl(C_TYPE-of-LVALUE(env;LV_Scomp-lval(lval)))))
   ∧ (↑C_field_of(LV_Scomp-comp(lval);outl(C_TYPE-of-LVALUE(env;LV_Scomp-lval(lval))))))@i
5. True@i
6. ↑isl(apply-alist(AtomDeq;C_Struct-fields(outl(C_TYPE-of-LVALUE(env;lval)));comp))@i
7. ↑C_LVALUE-proper(env;lval)
8. ↑C_Struct?(outl(C_TYPE-of-LVALUE(env;lval)))
9. ↑C_LVALUE-proper(env;lval)
10. ↑C_Struct?(outl(C_TYPE-of-LVALUE(env;lval)))
⊢ ↑C_field_of(comp;outl(C_TYPE-of-LVALUE(env;lval)))
BY
{ (InstLemma `isl-apply-alist` [⌈C_TYPE()⌉;⌈Atom⌉;⌈AtomDeq⌉;⌈comp⌉;⌈C_Struct-fields(outl(C_TYPE-of-LVALUE(env;lval)))⌉]⋅
   THEN Auto
   THEN Unfold `C_field_of` 0
   THEN RWO "assert-deq-member" 0
   THEN Auto) }

---

Latex:


.....truecase..... 
1.  env  :  C\_TYPE\_env()@i
2.  lval  :  C\_LVALUE()@i
3.  comp  :  Atom@i
4.  (\muparrow{}LV\_Scomp?(lval))
{}\mRightarrow{}  (\muparrow{}C\_LVALUE-proper(env;lval))
{}\mRightarrow{}  ((\muparrow{}C\_LVALUE-proper(env;LV\_Scomp-lval(lval)))
      \mwedge{}  (\muparrow{}C\_Struct?(outl(C\_TYPE-of-LVALUE(env;LV\_Scomp-lval(lval)))))
      \mwedge{}  (\muparrow{}C\_field\_of(LV\_Scomp-comp(lval);outl(C\_TYPE-of-LVALUE(env;LV\_Scomp-lval(lval))))))@i
5.  True@i
6.  \muparrow{}isl(apply-alist(AtomDeq;C\_Struct-fields(outl(C\_TYPE-of-LVALUE(env;lval)));comp))@i
7.  \muparrow{}C\_LVALUE-proper(env;lval)
8.  \muparrow{}C\_Struct?(outl(C\_TYPE-of-LVALUE(env;lval)))
9.  \muparrow{}C\_LVALUE-proper(env;lval)
10.  \muparrow{}C\_Struct?(outl(C\_TYPE-of-LVALUE(env;lval)))
\mvdash{}  \muparrow{}C\_field\_of(comp;outl(C\_TYPE-of-LVALUE(env;lval)))


By

(InstLemma  `isl-apply-alist`  [\mkleeneopen{}C\_TYPE()\mkleeneclose{};\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}comp\mkleeneclose{};
  \mkleeneopen{}C\_Struct-fields(outl(C\_TYPE-of-LVALUE(env;lval)))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Unfold  `C\_field\_of`  0
  THEN  RWO  "assert-deq-member"  0
  THEN  Auto)

---

Home Index