---

Step * of Lemma eq-finite-seqs-iff-eq-upto

∀a,b:ℕ ⟶ ℕ. ∀x:ℕ.  (↑eq-finite-seqs(a;b;x) ⇐⇒ a = b ∈ (ℕx ⟶ ℕ))
BY
{ ((UnivCD THENA Auto) THEN NatInd (-1) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. x : ℤ
4. ↑eq-finite-seqs(a;b;0)
⊢ a = b ∈ (ℕ0 ⟶ ℕ)

2
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. x : ℤ
4. a = b ∈ (ℕ0 ⟶ ℕ)
⊢ ↑eq-finite-seqs(a;b;0)

3
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. x : ℤ
4. 0 < x
5. ↑eq-finite-seqs(a;b;x - 1) ⇐⇒ a = b ∈ (ℕx - 1 ⟶ ℕ)
6. ↑eq-finite-seqs(a;b;x)
⊢ a = b ∈ (ℕx ⟶ ℕ)

4
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. x : ℤ
4. 0 < x
5. ↑eq-finite-seqs(a;b;x - 1) ⇐⇒ a = b ∈ (ℕx - 1 ⟶ ℕ)
6. a = b ∈ (ℕx ⟶ ℕ)
⊢ ↑eq-finite-seqs(a;b;x)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x:\mBbbN{}.    (\muparrow{}eq-finite-seqs(a;b;x)  \mLeftarrow{}{}\mRightarrow{}  a  =  b)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  NatInd  (-1)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index