---

Step * 1 of Lemma mk_applies_wf


1. T : Type
2. m : ℤ
3. m ≠ 0
4. 0 < m
5. ∀n:ℕ. ∀A:ℕ(m - 1) + n ⟶ Type. ∀G:k:ℕm - 1 ⟶ (A k). ∀F:funtype((m - 1) + n;A;T).
     (mk_applies(F;G;m - 1) ∈ funtype(n;λk.(A ((m - 1) + k));T))
6. n : ℕ
7. A : ℕm + n ⟶ Type
8. G : k:ℕm ⟶ (A k)
9. F : funtype(m + n;A;T)
⊢ mk_applies(F;G;m - 1) (G (m - 1)) ∈ funtype(n;λk.(A (m + k));T)
BY
{ ((InstHyp [⌜n + 1⌝;⌜A⌝;⌜G⌝;⌜F⌝] (-5)⋅ THENA Auto')
   THEN RepUR ``funtype`` (-1)
   THEN (RWO "primrec-unroll" (-1) THENA Auto)
   THEN SplitOnHypITE (-1)
   THEN Auto
   THEN Reduce (-2)
   THEN (Subst ⌜(m - 1) + ((n + 1) - 1 - (n + 1) - 1) ~ m - 1⌝ (-2)⋅ THENA Auto)
   THEN (Subst ⌜(n + 1) - 1 ~ n⌝ (-2)⋅ THENA Auto)
   THEN Assert ⌜mk_applies(F;G;m - 1) (G (m - 1)) ∈ primrec(n;T;λi,t. ((A ((m - 1) + (n - i))) ⟶ t))⌝⋅
   THEN Auto
   THEN DoSubsume
   THEN Auto
   THEN RepUR ``funtype`` 0)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  \mBbbZ{}
3.  m  \mneq{}  0
4.  0  <  m
5.  \mforall{}n:\mBbbN{}.  \mforall{}A:\mBbbN{}(m  -  1)  +  n  {}\mrightarrow{}  Type.  \mforall{}G:k:\mBbbN{}m  -  1  {}\mrightarrow{}  (A  k).  \mforall{}F:funtype((m  -  1)  +  n;A;T).
          (mk\_applies(F;G;m  -  1)  \mmember{}  funtype(n;\mlambda{}k.(A  ((m  -  1)  +  k));T))
6.  n  :  \mBbbN{}
7.  A  :  \mBbbN{}m  +  n  {}\mrightarrow{}  Type
8.  G  :  k:\mBbbN{}m  {}\mrightarrow{}  (A  k)
9.  F  :  funtype(m  +  n;A;T)
\mvdash{}  mk\_applies(F;G;m  -  1)  (G  (m  -  1))  \mmember{}  funtype(n;\mlambda{}k.(A  (m  +  k));T)


By

---

Latex:
((InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto')
  THEN  RepUR  ``funtype``  (-1)
  THEN  (RWO  "primrec-unroll"  (-1)  THENA  Auto)
  THEN  SplitOnHypITE  (-1)
  THEN  Auto
  THEN  Reduce  (-2)
  THEN  (Subst  \mkleeneopen{}(m  -  1)  +  ((n  +  1)  -  1  -  (n  +  1)  -  1)  \msim{}  m  -  1\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(n  +  1)  -  1  \msim{}  n\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}mk\_applies(F;G;m  -  1)  (G  (m  -  1))  \mmember{}  primrec(n;T;\mlambda{}i,t.  ((A  ((m  -  1)  +  (n  -  i)))  {}\mrightarrow{}  t))\mkleeneclose{}\000C\mcdot{}
  THEN  Auto
  THEN  DoSubsume
  THEN  Auto
  THEN  RepUR  ``funtype``  0)\mcdot{}

---

Home Index