---

Step * 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 ∈ ℤ)
⊢ 2 ∈ primrec(n;Top;λ,T. step-function-example(T))
BY
{ ((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 ⌜4⌝ (D 0)⋅
   THEN Auto) }

1
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))

---

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{}  2  \mmember{}  primrec(n;Top;\mlambda{},T.  step-function-example(T))


By

---

Latex:
((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{}4\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index