Step
*
1
of Lemma
nat-star-retract_wf
1. s : ℕ ⟶ ℕ
2. nat-star-retract(s) ∈ ℕ ⟶ ℕ
3. i : ℕ
4. j : ℕ
5. 0 < nat-star-retract(s) i
6. 0 < nat-star-retract(s) j
⊢ i = j ∈ ℤ
BY
{ ((RepeatFor 2 (MoveToConcl (-1)) THEN All (RepUR ``nat-star-retract``))
THEN (BoolCase ⌜(∃i∈upto(i).0 <z s i)_b⌝⋅ THENA Auto)
) }
1
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 ∈ ℤ)
2
1. s : ℕ ⟶ ℕ
2. λn.if (∃i∈upto(n).0 <z s i)_b then 0 else s n fi ∈ ℕ ⟶ ℕ
3. i : ℕ
4. ¬(∃i∈upto(i). 0 < s i)
5. j : ℕ
⊢ 0 < s i
⇒ 0 < if (∃i∈upto(j).0 <z s i)_b then 0 else s j fi
⇒ (i = j ∈ ℤ)
Latex:
Latex:
1. s : \mBbbN{} {}\mrightarrow{} \mBbbN{}
2. nat-star-retract(s) \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbN{}
3. i : \mBbbN{}
4. j : \mBbbN{}
5. 0 < nat-star-retract(s) i
6. 0 < nat-star-retract(s) j
\mvdash{} i = j
By
Latex:
((RepeatFor 2 (MoveToConcl (-1)) THEN All (RepUR ``nat-star-retract``))
THEN (BoolCase \mkleeneopen{}(\mexists{}i\mmember{}upto(i).0 <z s i)\_b\mkleeneclose{}\mcdot{} THENA Auto)
)
Home
Index