---

Step * of Lemma iterate-null-process

∀[n:Top]. ∀[inputs:Top List].  (null-process(n)*(inputs) ~ null-process(n))
BY
{ (RepUR ``iterate-process null-process rec-process`` 0
   THEN (InductionOnList
         THEN Reduce 0
         THEN Try (Trivial)
         THEN NthHypSq (-1)
         THEN RepeatFor 2 (EqCD)
         THEN Try (Trivial)
         THEN RW (AddrC [1;1] UnrollRecursionC) 0
         THEN Reduce 0
         THEN Auto)
   ) }

---

Latex:


\mforall{}[n:Top].  \mforall{}[inputs:Top  List].    (null-process(n)*(inputs)  \msim{}  null-process(n))


By

(RepUR  ``iterate-process  null-process  rec-process``  0
  THEN  (InductionOnList
              THEN  Reduce  0
              THEN  Try  (Trivial)
              THEN  NthHypSq  (-1)
              THEN  RepeatFor  2  (EqCD)
              THEN  Try  (Trivial)
              THEN  RW  (AddrC  [1;1]  UnrollRecursionC)  0
              THEN  Reduce  0
              THEN  Auto)
  )

---

Home Index