---

Step * 1 1 of Lemma step-function-example-member


1. step-function-example(corec(T.step-function-example(T))) ⊆r corec(T.step-function-example(T))
2. n : ℕ
3. ∀n:ℕn. (2 ∈ primrec(n;Top;λ,T. step-function-example(T)))
4. ¬(n = 0 ∈ ℤ)
⊢ 4 ∈ primrec(n - 1;Top;λ,T. step-function-example(T))
BY
{ ((Decide n = 1 ∈ ℤ THENA Auto)
   THEN Try (Complete (((Subst ⌜n ~ 1⌝ 0⋅ THENA Auto) THEN Reduce 0 THEN Auto)))
   THEN (RWO "primrec-unroll-1" 0 THENA Auto)
   THEN Reduce 0
   THEN RepeatFor 2 (UnfoldAtAddr [1] 0)
   THEN Reduce 0
   THEN MemTypeCD
   THEN Auto
   THEN (With ⌜2⌝ (D 0)⋅ THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  step-function-example(corec(T.step-function-example(T)))  \msubseteq{}r  corec(T.step-function-example(T))
2.  n  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}n.  (2  \mmember{}  primrec(n;Top;\mlambda{},T.  step-function-example(T)))
4.  \mneg{}(n  =  0)
\mvdash{}  4  \mmember{}  primrec(n  -  1;Top;\mlambda{},T.  step-function-example(T))


By

---

Latex:
((Decide  n  =  1  THENA  Auto)
  THEN  Try  (Complete  (((Subst  \mkleeneopen{}n  \msim{}  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  Auto)))
  THEN  (RWO  "primrec-unroll-1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepeatFor  2  (UnfoldAtAddr  [1]  0)
  THEN  Reduce  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  (With  \mkleeneopen{}2\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index