---

Step * of Lemma null-class-program_wf

∀[Info,B:Type].  (null-class-program() ∈ LocalClass(Null))
BY
{ (Auto
   THEN RepUR ``null-class-program null-class hdf-return`` 0
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``class-ap`` 0
   THEN RecUnfold `es-before` 0
   THEN AutoSplit
   THEN GenConclAtAddr [3;1;1;2]
   THEN (Assert ⌜0 < ||v||⌝⋅
         THENA ((RWO "map_append_sq" (-1) THENA Auto) THEN (RevHypSubst' (-1) 0 THENA Auto) THEN Reduce 0 THEN Auto')
         )
   THEN Thin (-2)
   THEN D (-2)
   THEN Reduce (-1)
   THEN Auto
   THEN RepUR ``hdf-run hdf-ap`` 0
   THEN (RWO "iterate-hdf-halt" 0 THENA Auto)
   THEN RepUR ``hdf-halt`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].    (null-class-program()  \mmember{}  LocalClass(Null))


By

---

Latex:
(Auto
  THEN  RepUR  ``null-class-program  null-class  hdf-return``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``class-ap``  0
  THEN  RecUnfold  `es-before`  0
  THEN  AutoSplit
  THEN  GenConclAtAddr  [3;1;1;2]
  THEN  (Assert  \mkleeneopen{}0  <  ||v||\mkleeneclose{}\mcdot{}
              THENA  ((RWO  "map\_append\_sq"  (-1)  THENA  Auto)
                            THEN  (RevHypSubst'  (-1)  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  Auto')
              )
  THEN  Thin  (-2)
  THEN  D  (-2)
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  RepUR  ``hdf-run  hdf-ap``  0
  THEN  (RWO  "iterate-hdf-halt"  0  THENA  Auto)
  THEN  RepUR  ``hdf-halt``  0
  THEN  Auto)

---

Home Index