---

Step * of Lemma funtype-unroll-last

∀[T,A:Top]. ∀[n:ℕ].  (funtype(n;A;T) ~ if (n =z 0) then T else funtype(n - 1;A;(A (n - 1)) ⟶ T) fi )
BY
{ (Auto
   THEN RepeatFor 2 (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Try (Complete ((Unfold `funtype` 0 THEN Reduce 0 THEN Auto)))
   THEN Auto
   THEN AutoSplit
   THEN SplitOnHypITE (-3)
   THEN Try (Complete (Auto))
   THEN Try (Complete (((Subst ⌜n ~ 1⌝ 0⋅ THENA Auto) THEN Reduce 0 THEN Unfold `funtype` 0 THEN Reduce 0 THEN Auto)))
   THEN (InstHyp [⌜T⌝;⌜λn.(A (n + 1))⌝] (-4)⋅ THENA Auto)
   THEN Unfold `funtype` (-1)
   THEN Unfold `funtype` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Repeat (AutoSplit)
   THEN EqCD
   THEN Try (Complete (Auto))
   THEN NthHypSq (-2)
   THEN EqCD
   THEN Reduce 0
   THEN EqCD
   THEN Try (Complete (Auto))
   THEN RepeatFor 4 (EqCD)
   THEN Try (Trivial)
   THEN (RWO "general_arith_equation2" 0 THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Try  (Complete  ((Unfold  `funtype`  0  THEN  Reduce  0  THEN  Auto)))
  THEN  Auto
  THEN  AutoSplit
  THEN  SplitOnHypITE  (-3)
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Complete  (((Subst  \mkleeneopen{}n  \msim{}  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                                            THEN  Reduce  0
                                            THEN  Unfold  `funtype`  0
                                            THEN  Reduce  0
                                            THEN  Auto)))
  THEN  (InstHyp  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(A  (n  +  1))\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  Unfold  `funtype`  (-1)
  THEN  Unfold  `funtype`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Repeat  (AutoSplit)
  THEN  EqCD
  THEN  Try  (Complete  (Auto))
  THEN  NthHypSq  (-2)
  THEN  EqCD
  THEN  Reduce  0
  THEN  EqCD
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  4  (EqCD)
  THEN  Try  (Trivial)
  THEN  (RWO  "general\_arith\_equation2"  0  THEN  Auto)\mcdot{})

---

Home Index