Step
*
2
of Lemma
eq-finite-seqs-implies-eq-upto
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 ⟶ ℕ)
BY
{ D (-2) }
1
.....antecedent.....
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. x : ℤ
4. 0 < x
5. ↑eq-finite-seqs(a;b;x)
⊢ ↑eq-finite-seqs(a;b;x - 1)
2
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. x : ℤ
4. 0 < x
5. ↑eq-finite-seqs(a;b;x)
6. a = b ∈ (ℕx - 1 ⟶ ℕ)
⊢ a = b ∈ (ℕx ⟶ ℕ)
Latex:
Latex:
1. a : \mBbbN{} {}\mrightarrow{} \mBbbN{}
2. b : \mBbbN{} {}\mrightarrow{} \mBbbN{}
3. x : \mBbbZ{}
4. 0 < x
5. (\muparrow{}eq-finite-seqs(a;b;x - 1)) {}\mRightarrow{} (a = b)
6. \muparrow{}eq-finite-seqs(a;b;x)
\mvdash{} a = b
By
Latex:
D (-2)
Home
Index