Step * 1 2 of Lemma no_repeats-remove-first


1. Type
2. List
3. {x:T| (x ∈ L)}  ⟶ 𝔹
4. ∀[i,j:ℕ].  (L[i] L[j] ∈ T)) supposing ((¬(i j ∈ ℕ)) and j < ||L|| and i < ||L||)
5. : ℕ
6. : ℕ
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:ℕ1. (¬↑(P L[j]))
11. remove-first(P;L)[i] L[i 1] supposing ∃j:ℕ1. (↑(P L[j]))
12. remove-first(P;L)[j] L[j] supposing ∀j:ℕ1. (¬↑(P L[j]))
13. remove-first(P;L)[j] L[j 1] supposing ∃j:ℕ1. (↑(P L[j]))
14. ||remove-first(P;L)|| ≤ ||L||
15. ¬(∀j:ℕ1. (¬↑(P L[j])))
16. ∀j:ℕ1. (¬↑(P L[j]))
⊢ j ∈ ℕ
BY
((Assert ⌜(i j ∈ ℤ) ∨ i < j ∨ (i > j)⌝⋅ THENA Auto)
   THEN (-1)
   THEN Auto
   THEN (-2)
   THEN (-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 
         THEN Auto'
         THEN (InstLemma `length-remove-first` [⌜T⌝;⌜L⌝;⌜P⌝]⋅ THENA Auto)
         THEN (-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