---

Step * of Lemma funtype-unroll

∀[T,A:Top]. ∀[n:ℕ].  (funtype(n;A;T) ~ if (n =z 0) then T else (A 0) ⟶ funtype(n - 1;λi.(A (i + 1));T) fi )
BY
{ ((Auto THEN RW (AddrC [1] (UnfoldC `funtype`)) 0)
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN Unfold `funtype` 0
   THEN AutoSplit
   THEN RepeatFor 2 (EqCD)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,A:Top].  \mforall{}[n:\mBbbN{}].
    (funtype(n;A;T)  \msim{}  if  (n  =\msubz{}  0)  then  T  else  (A  0)  {}\mrightarrow{}  funtype(n  -  1;\mlambda{}i.(A  (i  +  1));T)  fi  )


By

---

Latex:
((Auto  THEN  RW  (AddrC  [1]  (UnfoldC  `funtype`))  0)
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Unfold  `funtype`  0
  THEN  AutoSplit
  THEN  RepeatFor  2  (EqCD)
  THEN  Auto)

---

Home Index