Step
*
1
1
of Lemma
nat-star-retract_wf
1. s : ℕ ⟶ ℕ
2. λn.if (∃i∈upto(n).0 <z s i)_b then 0 else s n fi ∈ ℕ ⟶ ℕ
3. i : ℕ
4. j : ℕ
5. (∃i∈upto(i). 0 < s i)
⊢ 0 < 0
⇒ 0 < if (∃i∈upto(j).0 <z s i)_b then 0 else s j fi
⇒ (i = j ∈ ℤ)
BY
{ Auto }
Latex:
Latex:
1. s : \mBbbN{} {}\mrightarrow{} \mBbbN{}
2. \mlambda{}n.if (\mexists{}i\mmember{}upto(n).0 <z s i)\_b then 0 else s n fi \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbN{}
3. i : \mBbbN{}
4. j : \mBbbN{}
5. (\mexists{}i\mmember{}upto(i). 0 < s i)
\mvdash{} 0 < 0 {}\mRightarrow{} 0 < if (\mexists{}i\mmember{}upto(j).0 <z s i)\_b then 0 else s j fi {}\mRightarrow{} (i = j)
By
Latex:
Auto
Home
Index