---

Step * of Lemma funtype-split

∀[T:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type].  (funtype(n;A;T) = funtype(m;A;funtype(n - m;λk.(A (k + m));T)) ∈ Type)
BY
{ (Auto
   THEN (Assert ⌜∃k:ℕ. (n = (m + k) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜n - m⌝]⋅ THEN Auto'))
   THEN RepeatFor 2 ((D (-3) THENA Auto))
   THEN RepeatFor 2 (MoveToConcl (-2))
   THEN D (-1)
   THEN HypSubst' (-1) 0
   THEN ThinVar `n'
   THEN (D 0 THENA Auto)
   THEN Thin (-1)
   THEN (Subst ⌜(m + k) - m ~ k⌝ 0⋅ THENA Auto)
   THEN MoveToConcl (-3)
   THEN MoveToConcl (-2)
   THEN NatInd (-1)
   THEN Auto) }

1
1. k : ℤ
2. T : Type
3. m : ℤ
4. 0 ≤ m
5. A : ℕm + 0 ⟶ Type
⊢ funtype(m + 0;A;T) = funtype(m;A;funtype(0;λk.(A (k + m));T)) ∈ Type

2
1. k : ℤ
2. 0 < k
3. ∀T:Type. ∀m:ℤ.
     ((0 ≤ m)
     ⇒ (∀A:ℕm + (k - 1) ⟶ Type. (funtype(m + (k - 1);A;T) = funtype(m;A;funtype(k - 1;λk.(A (k + m));T)) ∈ Type)))
4. T : Type
5. m : ℤ
6. 0 ≤ m
7. A : ℕm + k ⟶ Type
⊢ funtype(m + k;A;T) = funtype(m;A;funtype(k;λk.(A (k + m));T)) ∈ Type

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].
    (funtype(n;A;T)  =  funtype(m;A;funtype(n  -  m;\mlambda{}k.(A  (k  +  m));T)))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}.  (n  =  (m  +  k))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}n  -  m\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  RepeatFor  2  ((D  (-3)  THENA  Auto))
  THEN  RepeatFor  2  (MoveToConcl  (-2))
  THEN  D  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  ThinVar  `n'
  THEN  (D  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (Subst  \mkleeneopen{}(m  +  k)  -  m  \msim{}  k\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  MoveToConcl  (-2)
  THEN  NatInd  (-1)
  THEN  Auto)

---

Home Index