---

Step * of Lemma assert-equal-upto-finite-nat-seq

∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℕ].  (↑equal-upto-finite-nat-seq(n;f;g) ⇐⇒ f = g ∈ (ℕn ⟶ ℕ))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``equal-upto-finite-nat-seq`` 0
   THEN NatInd 1
   THEN (UnivCD THENA Auto)
   THEN Reduce 0) }

1
1. n : ℤ
2. f : ℕ0 ⟶ ℕ
3. g : ℕ0 ⟶ ℕ
⊢ True ⇐⇒ f = g ∈ (ℕ0 ⟶ ℕ)

2
1. n : ℤ
2. 0 < n
3. ∀f,g:ℕn - 1 ⟶ ℕ.  (↑primrec(n - 1;tt;λi,b. (b ∧b (f i =z g i))) ⇐⇒ f = g ∈ (ℕn - 1 ⟶ ℕ))
4. f : ℕn ⟶ ℕ
5. g : ℕn ⟶ ℕ
⊢ ↑primrec(n;tt;λi,b. (b ∧b (f i =z g i))) ⇐⇒ f = g ∈ (ℕn ⟶ ℕ)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}].    (\muparrow{}equal-upto-finite-nat-seq(n;f;g)  \mLeftarrow{}{}\mRightarrow{}  f  =  g)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``equal-upto-finite-nat-seq``  0
  THEN  NatInd  1
  THEN  (UnivCD  THENA  Auto)
  THEN  Reduce  0)

---

Home Index