---

Step * 1 2 of Lemma no_repeats-remove-first


1. T : Type
2. L : T List
3. P : {x:T| (x ∈ L)}  ⟶ 𝔹
4. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
5. i : ℕ
6. j : ℕ
7. i < ||remove-first(P;L)||
8. j < ||remove-first(P;L)||
9. remove-first(P;L)[i] = remove-first(P;L)[j] ∈ T
10. remove-first(P;L)[i] ~ L[i] supposing ∀j:ℕi + 1. (¬↑(P L[j]))
11. remove-first(P;L)[i] ~ L[i + 1] supposing ∃j:ℕi + 1. (↑(P L[j]))
12. remove-first(P;L)[j] ~ L[j] supposing ∀j:ℕj + 1. (¬↑(P L[j]))
13. remove-first(P;L)[j] ~ L[j + 1] supposing ∃j:ℕj + 1. (↑(P L[j]))
14. ||remove-first(P;L)|| ≤ ||L||
15. ¬(∀j:ℕi + 1. (¬↑(P L[j])))
16. ∀j:ℕj + 1. (¬↑(P L[j]))
⊢ i = j ∈ ℕ
BY
{ ((Assert ⌜(i = j ∈ ℤ) ∨ i < j ∨ (i > j)⌝⋅ THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN D (-2)
   THEN D (-4)
   THEN Auto
   THEN (D 0⋅ THENA Auto)
   THEN MoveToConcl 9
   THEN ((D (-8) THENA Auto)
         THEN HypSubst (-1) 0
         THEN HypSubst (-4) 0
         THEN Fold `not` 0
         THEN BHyp 4 
         THEN Auto'
         THEN (InstLemma `length-remove-first` [⌜T⌝;⌜L⌝;⌜P⌝]⋅ THENA Auto)
         THEN D (-1)
         THEN Auto'
         THEN With ⌜j1⌝ (D (-2))⋅
         THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  P  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(L[i]  =  L[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||L||  and  i  <  ||L||)
5.  i  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  i  <  ||remove-first(P;L)||
8.  j  <  ||remove-first(P;L)||
9.  remove-first(P;L)[i]  =  remove-first(P;L)[j]
10.  remove-first(P;L)[i]  \msim{}  L[i]  supposing  \mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  L[j]))
11.  remove-first(P;L)[i]  \msim{}  L[i  +  1]  supposing  \mexists{}j:\mBbbN{}i  +  1.  (\muparrow{}(P  L[j]))
12.  remove-first(P;L)[j]  \msim{}  L[j]  supposing  \mforall{}j:\mBbbN{}j  +  1.  (\mneg{}\muparrow{}(P  L[j]))
13.  remove-first(P;L)[j]  \msim{}  L[j  +  1]  supposing  \mexists{}j:\mBbbN{}j  +  1.  (\muparrow{}(P  L[j]))
14.  ||remove-first(P;L)||  \mleq{}  ||L||
15.  \mneg{}(\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  L[j])))
16.  \mforall{}j:\mBbbN{}j  +  1.  (\mneg{}\muparrow{}(P  L[j]))
\mvdash{}  i  =  j


By

---

Latex:
((Assert  \mkleeneopen{}(i  =  j)  \mvee{}  i  <  j  \mvee{}  (i  >  j)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  D  (-2)
  THEN  D  (-4)
  THEN  Auto
  THEN  (D  0\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  9
  THEN  ((D  (-8)  THENA  Auto)
              THEN  HypSubst  (-1)  0
              THEN  HypSubst  (-4)  0
              THEN  Fold  `not`  0
              THEN  BHyp  4 
              THEN  Auto'
              THEN  (InstLemma  `length-remove-first`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  D  (-1)
              THEN  Auto'
              THEN  With  \mkleeneopen{}j1\mkleeneclose{}  (D  (-2))\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index