---

Step * of Lemma C_LVALUE-proper-Scomp

∀env:C_TYPE_env(). ∀lval:C_LVALUE().
  ((↑LV_Scomp?(lval))
  ⇒ (↑C_LVALUE-proper(env;lval))
  ⇒ let lval' = LV_Scomp-lval(lval) in
      let a = LV_Scomp-comp(lval) in
      let typ = outl(C_TYPE-of-LVALUE(env;lval')) in
      (↑C_LVALUE-proper(env;lval')) ∧ (↑C_Struct?(typ)) ∧ (↑C_field_of(a;typ)))
BY
{ ((D 0 THENA Auto)
   THEN BLemma `C_LVALUE-induction`
   THEN RepUR ``let`` 0
   THEN Auto
   THEN OnMaybeHyp 6 (\h. ((RepUR ``C_LVALUE-proper C_TYPE-of-LVALUE`` h
                            THEN Fold `C_TYPE-of-LVALUE` h
                            THEN Fold `C_LVALUE-proper` h)
                           THEN Repeat ((SplitOnHypITE h  THEN Auto))
                           ))) }

1
.....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)))

---

Latex:

---

Latex:
\mforall{}env:C\_TYPE\_env().  \mforall{}lval:C\_LVALUE().
    ((\muparrow{}LV\_Scomp?(lval))
    {}\mRightarrow{}  (\muparrow{}C\_LVALUE-proper(env;lval))
    {}\mRightarrow{}  let  lval'  =  LV\_Scomp-lval(lval)  in
            let  a  =  LV\_Scomp-comp(lval)  in
            let  typ  =  outl(C\_TYPE-of-LVALUE(env;lval'))  in
            (\muparrow{}C\_LVALUE-proper(env;lval'))  \mwedge{}  (\muparrow{}C\_Struct?(typ))  \mwedge{}  (\muparrow{}C\_field\_of(a;typ)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  BLemma  `C\_LVALUE-induction`
  THEN  RepUR  ``let``  0
  THEN  Auto
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  ((RepUR  ``C\_LVALUE-proper  C\_TYPE-of-LVALUE``  h
                                                    THEN  Fold  `C\_TYPE-of-LVALUE`  h
                                                    THEN  Fold  `C\_LVALUE-proper`  h)
                                                  THEN  Repeat  ((SplitOnHypITE  h    THEN  Auto))
                                                  )))

---

Home Index