---

Step * of Lemma length-interpolate-list

∀[T:Type]
  ∀[f:T ⟶ T ⟶ T]. ∀[L:T List].  (||interpolate-list(x,y.f[x;y];L)|| = if null(L) then 0 else (2 * ||L||) - 1 fi  ∈ ℤ) 
  supposing value-type(T)
BY
{ (InductionOnList
   THEN Unfold `interpolate-list` 0
   THEN Reduce 0
   THEN ((Fold `member` 0 THEN Auto)
   ORELSE ((D -2 THEN Reduce 0)
           THEN Auto
           THEN Reduce -1
           THEN RepeatFor 2 (((CallByValueReduce 0 THENA Auto) THEN Reduce 0))
           THEN Auto)
   )) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[L:T  List].
        (||interpolate-list(x,y.f[x;y];L)||  =  if  null(L)  then  0  else  (2  *  ||L||)  -  1  fi  ) 
    supposing  value-type(T)


By

---

Latex:
(InductionOnList
  THEN  Unfold  `interpolate-list`  0
  THEN  Reduce  0
  THEN  ((Fold  `member`  0  THEN  Auto)
  ORELSE  ((D  -2  THEN  Reduce  0)
                  THEN  Auto
                  THEN  Reduce  -1
                  THEN  RepeatFor  2  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))
                  THEN  Auto)
  ))

---

Home Index