Step * 1 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. Dec(∀j:ℕi + 1. (¬↑(P L[j])))
16. Dec(∀j:ℕj + 1. (¬↑(P L[j])))
⊢ i = j ∈ ℕ
BY
{ (D (-2)
   THEN D (-1)
   THEN Try (Complete (((D (-7) THENA Auto)
                        THEN (D (-6) THENA Auto)
                        THEN (RWO "-2" (-8) THENA Auto)
                        THEN (RWO "-1" (-8) THENA Auto)
                        THEN Decide ⌜i = j ∈ ℤ⌝⋅
                        THEN Auto
                        THEN (InstHyp [⌜i⌝;⌜j⌝] (-14)⋅ THEN Auto)⋅)))) }

1
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 ∈ ℕ

2
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 ∈ ℕ

3
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 ∈ ℕ

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.  Dec(\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  L[j])))
16.  Dec(\mforall{}j:\mBbbN{}j  +  1.  (\mneg{}\muparrow{}(P  L[j])))
\mvdash{}  i  =  j


By

Latex:
(D  (-2)
  THEN  D  (-1)
  THEN  Try  (Complete  (((D  (-7)  THENA  Auto)
                                            THEN  (D  (-6)  THENA  Auto)
                                            THEN  (RWO  "-2"  (-8)  THENA  Auto)
                                            THEN  (RWO  "-1"  (-8)  THENA  Auto)
                                            THEN  Decide  \mkleeneopen{}i  =  j\mkleeneclose{}\mcdot{}
                                            THEN  Auto
                                            THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  (-14)\mcdot{}  THEN  Auto)\mcdot{}))))



Home Index