---

Step * 1 1 of Lemma l_before_no_repeats

.....antecedent..... 
1. T : Type
2. L : T List@i
3. i : ℕ||L||@i
4. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
5. f : ℕ2 ⟶ ℕ||L||
6. increasing(f;2)
7. ∀j:ℕ2. ([L[i]; L[i]][j] = L[f j] ∈ T)
⊢ ¬((f 0) = (f 1) ∈ ℕ)
BY
{ (InstLemma `increasing_implies` [⌜2⌝;⌜f⌝]⋅ THEN Auto THEN InstHyp [⌜0⌝;⌜1⌝] (-1)⋅ THEN Auto') }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  L  :  T  List@i
3.  i  :  \mBbbN{}||L||@i
4.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(L[i]  =  L[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||L||  and  i  <  ||L||)
5.  f  :  \mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||L||
6.  increasing(f;2)
7.  \mforall{}j:\mBbbN{}2.  ([L[i];  L[i]][j]  =  L[f  j])
\mvdash{}  \mneg{}((f  0)  =  (f  1))


By

---

Latex:
(InstLemma  `increasing\_implies`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto')

---

Home Index