---

Step * 2 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 ⟶ ℕ
⊢ ↑primrec(n;tt;λi,b. (b ∧b (f i =z g i))) ⇐⇒ f = g ∈ (ℕn ⟶ ℕ)
BY
{ ((RWO "primrec-unroll-1" 0 THENA Auto) THEN Reduce 0 THEN (RW assert_pushdownC 0 THENA 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 ⟶ ℕ
⊢ (↑primrec(n - 1;tt;λi,b. (b ∧b (f i =z g i)))) ∧ ((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{}  \muparrow{}primrec(n;tt;\mlambda{}i,b.  (b  \mwedge{}\msubb{}  (f  i  =\msubz{}  g  i)))  \mLeftarrow{}{}\mRightarrow{}  f  =  g


By

---

Latex:
((RWO  "primrec-unroll-1"  0  THENA  Auto)  THEN  Reduce  0  THEN  (RW  assert\_pushdownC  0  THENA  Auto))

---

Home Index