---

Step * of Lemma simple-primrec-add

∀[b,F:Top]. ∀[n,m:ℕ].  (primrec(n + m;b;λi.F) ~ primrec(n;primrec(m;b;λi.F);λi.F))
BY
{ (InductionOnNat
   THEN Reduce 0
   THEN (D 0 THEN Try (Complete (Auto)))
   THEN (RW (SubC (LemmaC `primrec-unroll`)) 0 THENA Auto)
   THEN RepeatFor 2 (((SplitOnConclITE THENA Auto) THEN Try (Complete (Auto'))))
   THEN EqCD
   THEN Reduce 0
   THEN Try (Trivial)
   THEN Subst' (n + m) - 1 ~ (n - 1) + m 0
   THEN Try (BackThruSomeHyp)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[b,F:Top].  \mforall{}[n,m:\mBbbN{}].    (primrec(n  +  m;b;\mlambda{}i.F)  \msim{}  primrec(n;primrec(m;b;\mlambda{}i.F);\mlambda{}i.F))


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  (D  0  THEN  Try  (Complete  (Auto)))
  THEN  (RW  (SubC  (LemmaC  `primrec-unroll`))  0  THENA  Auto)
  THEN  RepeatFor  2  (((SplitOnConclITE  THENA  Auto)  THEN  Try  (Complete  (Auto'))))
  THEN  EqCD
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  Subst'  (n  +  m)  -  1  \msim{}  (n  -  1)  +  m  0
  THEN  Try  (BackThruSomeHyp)
  THEN  Auto)

---

Home Index