---

Step * of Lemma primrec-as-fix

∀[n,b,c:Top].  (primrec(n;b;c) ~ fix((λp,n. if (n) < (1)  then b  else (c (n - 1) (p (n - 1))))) n)
BY
{ (Auto
   THEN (Assert ∀n:ℕ. ∀[b,c:Top].  (primrec(n;b;c) ~ fix((λp,n. if (n) < (1)  then b  else (c (n - 1) (p (n - 1))))) n) \000CBY
               ((InductionOnNat THEN Reduce 0 THEN Auto)
                THENL [ByComputation 10
                      ; ((RWO "primrec-unroll" 0 THENA Auto)
                         THEN AutoSplit
                         THEN RW (AddrC [2;1] UnrollRecursionC) 0
                         THEN Reduce 0
                         THEN Auto)]
               ))
   ) }

1
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)
⊢ primrec(n;b;c) ~ fix((λp,n. if (n) < (1)  then b  else (c (n - 1) (p (n - 1))))) n

---

Latex:

---

Latex:
\mforall{}[n,b,c:Top].    (primrec(n;b;c)  \msim{}  fix((\mlambda{}p,n.  if  (n)  <  (1)    then  b    else  (c  (n  -  1)  (p  (n  -  1)))))  n)


By

---

Latex:
(Auto
  THEN  (Assert  \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))))) 
                                                                        n)  BY
                          ((InductionOnNat  THEN  Reduce  0  THEN  Auto)
                            THENL  [ByComputation  10
                                        ;  ((RWO  "primrec-unroll"  0  THENA  Auto)
                                              THEN  AutoSplit
                                              THEN  RW  (AddrC  [2;1]  UnrollRecursionC)  0
                                              THEN  Reduce  0
                                              THEN  Auto)]
                          ))
  )

---

Home Index