---

Step * 1 1 of Lemma primrec-as-fix


1. n : Top
2. b : Top
3. c : Top
4. ∀n:ℕ. ∀[b,c:Top].  (primrec(n;b;c) ~ fix((λp,n. if (n) < (1)  then b  else (c (n - 1) (p (n - 1))))) n)
5. ∀n:ℤ. ∀[b,c:Top].  (primrec(n;b;c) ~ fix((λp,n. if (n) < (1)  then b  else (c (n - 1) (p (n - 1))))) n)
⊢ primrec(n;b;c) ~ fix((λp,n. if (n) < (1)  then b  else (c (n - 1) (p (n - 1))))) n
BY
{ (SqEqualTopToBase
   THEN SqequalSqle⋅
   THEN AssumeHasValue⋅
   THEN ((RW (SweepUpC UnrollRecursionC) (-1) THEN Reduce -1) ORELSE (Unfold `primrec` -1 THEN Unfold `primtailrec` -1))
   THEN (HasValueD (-1) ORELSE SqReasoningSteps)
   THEN RWO "2<" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  Top
2.  b  :  Top
3.  c  :  Top
4.  \mforall{}n:\mBbbN{}
          \mforall{}[b,c:Top].    (primrec(n;b;c)  \msim{}  fix((\mlambda{}p,n.  if  (n)  <  (1)    then  b    else  (c  (n  -  1)  (p  (n  -  1)))))  \000Cn)
5.  \mforall{}n:\mBbbZ{}
          \mforall{}[b,c:Top].    (primrec(n;b;c)  \msim{}  fix((\mlambda{}p,n.  if  (n)  <  (1)    then  b    else  (c  (n  -  1)  (p  (n  -  1)))))  \000Cn)
\mvdash{}  primrec(n;b;c)  \msim{}  fix((\mlambda{}p,n.  if  (n)  <  (1)    then  b    else  (c  (n  -  1)  (p  (n  -  1)))))  n


By

---

Latex:
(SqEqualTopToBase
  THEN  SqequalSqle\mcdot{}
  THEN  AssumeHasValue\mcdot{}
  THEN  ((RW  (SweepUpC  UnrollRecursionC)  (-1)  THEN  Reduce  -1)
  ORELSE  (Unfold  `primrec`  -1  THEN  Unfold  `primtailrec`  -1)
  )
  THEN  (HasValueD  (-1)  ORELSE  SqReasoningSteps)
  THEN  RWO  "2<"  0
  THEN  Auto)

---

Home Index