---

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


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 ⟶ ℕ
⊢ (f = g ∈ (ℕn - 1 ⟶ ℕ)) ∧ ((f (n - 1)) = (g (n - 1)) ∈ ℤ) ⇐⇒ f = g ∈ (ℕn ⟶ ℕ)
BY
{ (D 0 THEN Auto) }

1
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 ⟶ ℕ
6. f = g ∈ (ℕn - 1 ⟶ ℕ)
7. (f (n - 1)) = (g (n - 1)) ∈ ℤ
⊢ f = g ∈ (ℕn ⟶ ℕ)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}f,g:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbN{}.    (\muparrow{}primrec(n  -  1;tt;\mlambda{}i,b.  (b  \mwedge{}\msubb{}  (f  i  =\msubz{}  g  i)))  \mLeftarrow{}{}\mRightarrow{}  f  =  g)
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
5.  g  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  (f  =  g)  \mwedge{}  ((f  (n  -  1))  =  (g  (n  -  1)))  \mLeftarrow{}{}\mRightarrow{}  f  =  g


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index