---

Step * 1 of Lemma l_contains-no_repeats-length


1. T : Type
2. as : T List
3. bs : T List
4. no_repeats(T;as)
5. ∀i@0:ℕ||as||. ∃i:ℕ. (i < ||bs|| c∧ (as[i@0] = bs[i] ∈ T))
6. f : i@0:ℕ||as|| ⟶ ℕ
7. ∀i@0:ℕ||as||. (f i@0 < ||bs|| c∧ (as[i@0] = bs[f i@0] ∈ T))
⊢ Inj(ℕ||as||;ℕ||bs||;f)
BY
{ (D 0
   THEN Auto
   THEN SupposeNot
   THEN OnMaybeHyp 4 (\h. (Unfold `no_repeats` h
                           THEN InstHyp [⌜a1⌝;⌜a2⌝] h⋅
                           THEN Auto
                           THEN Try (RepeatFor 2 (ParallelLast))
                           THEN D (-1)
                           THEN ((InstHyp [⌜a1⌝] (-5)⋅ THENA Auto) THEN D -1)
                           THEN (InstHyp [⌜a2⌝] (-7)⋅ THENA Auto)
                           THEN D -1
                           THEN Auto))) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  no\_repeats(T;as)
5.  \mforall{}i@0:\mBbbN{}||as||.  \mexists{}i:\mBbbN{}.  (i  <  ||bs||  c\mwedge{}  (as[i@0]  =  bs[i]))
6.  f  :  i@0:\mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}i@0:\mBbbN{}||as||.  (f  i@0  <  ||bs||  c\mwedge{}  (as[i@0]  =  bs[f  i@0]))
\mvdash{}  Inj(\mBbbN{}||as||;\mBbbN{}||bs||;f)


By

---

Latex:
(D  0
  THEN  Auto
  THEN  SupposeNot
  THEN  OnMaybeHyp  4  (\mbackslash{}h.  (Unfold  `no\_repeats`  h
                                                  THEN  InstHyp  [\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]  h\mcdot{}
                                                  THEN  Auto
                                                  THEN  Try  (RepeatFor  2  (ParallelLast))
                                                  THEN  D  (-1)
                                                  THEN  ((InstHyp  [\mkleeneopen{}a1\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)  THEN  D  -1)
                                                  THEN  (InstHyp  [\mkleeneopen{}a2\mkleeneclose{}]  (-7)\mcdot{}  THENA  Auto)
                                                  THEN  D  -1
                                                  THEN  Auto)))

---

Home Index