---

Step * of Lemma modify-combinator2_wf

∀[n:ℕ]. ∀[A:ℕn ─→ Type]. ∀[m:ℕ].
  ∀[B:ℕm ─→ Type]. ∀[T:Type]. ∀[f:(i:ℕn ─→ (A i + Top)) ─→ (i:ℕm ─→ (B i + Top)) ─→ T].
    (modify-combinator2(f) ∈ (i:ℕn ─→ (A i + Top))
     ─→ (i:ℕm - 1 ─→ if (i =z 0) then one_or_both(B 0;B 1) + Top else B (i + 1) + Top fi )
     ─→ T) 
  supposing 1 < m
BY
{ (Auto THEN ProveWfLemma) }

---

Latex:


\mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[m:\mBbbN{}].
    \mforall{}[B:\mBbbN{}m  {}\mrightarrow{}  Type].  \mforall{}[T:Type].  \mforall{}[f:(i:\mBbbN{}n  {}\mrightarrow{}  (A  i  +  Top))  {}\mrightarrow{}  (i:\mBbbN{}m  {}\mrightarrow{}  (B  i  +  Top))  {}\mrightarrow{}  T].
        (modify-combinator2(f)  \mmember{}  (i:\mBbbN{}n  {}\mrightarrow{}  (A  i  +  Top))
          {}\mrightarrow{}  (i:\mBbbN{}m  -  1  {}\mrightarrow{}  if  (i  =\msubz{}  0)  then  one\_or\_both(B  0;B  1)  +  Top  else  B  (i  +  1)  +  Top  fi  )
          {}\mrightarrow{}  T) 
    supposing  1  <  m


By

(Auto  THEN  ProveWfLemma)

---

Home Index