Step
*
1
1
of Lemma
kripke2b-seq_wf
.....set predicate.....
1. a : ℕ ⟶ ℕ
2. x : ℕ
3. F : ∀b:{b:ℕ ⟶ ℕ| a = b ∈ (ℕx ⟶ ℕ)} . ∃n:ℕ. ((b n) ≥ ((a x) + 1) )
4. b : ℕ ⟶ ℕ
5. eq-finite-seqs(a;b;x) ∈ 𝔹
6. ↑eq-finite-seqs(a;b;x)
⊢ a = b ∈ (ℕx ⟶ ℕ)
BY
{ (BLemma `eq-finite-seqs-implies-eq-upto` THEN Auto) }
Latex:
Latex:
.....set predicate.....
1. a : \mBbbN{} {}\mrightarrow{} \mBbbN{}
2. x : \mBbbN{}
3. F : \mforall{}b:\{b:\mBbbN{} {}\mrightarrow{} \mBbbN{}| a = b\} . \mexists{}n:\mBbbN{}. ((b n) \mgeq{} ((a x) + 1) )
4. b : \mBbbN{} {}\mrightarrow{} \mBbbN{}
5. eq-finite-seqs(a;b;x) \mmember{} \mBbbB{}
6. \muparrow{}eq-finite-seqs(a;b;x)
\mvdash{} a = b
By
Latex:
(BLemma `eq-finite-seqs-implies-eq-upto` THEN Auto)
Home
Index