---

Step * 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)
⊢ primrec(n;b;c) ~ fix((λp,n. if (n) < (1)  then b  else (c (n - 1) (p (n - 1))))) n
BY
{ (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) BY
         ((D 0 THENA Auto)
          THEN ((Decide ⌜n1 ≤ 0⌝⋅ THENA Auto)
                THENL [(((Auto THEN ByComputation 2) THEN Reduce 0) THEN AutoSplit); (RWO "4" 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)
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

---

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)
\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:
(Assert  \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)))))  n)  BY
              ((D  0  THENA  Auto)
                THEN  ((Decide  \mkleeneopen{}n1  \mleq{}  0\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THENL  [(((Auto  THEN  ByComputation  2)  THEN  Reduce  0)  THEN  AutoSplit)
                                        ;  (RWO  "4"  0  THEN  Auto)]
                          )
                ))

---

Home Index