Proof of Nuprl Lemma : no_repeats-remove-first

Step * 1 3 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
{ (Decide ⌜i = j ∈ ℤ⌝⋅ 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||)

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. \mneg{}(\mforall{}j:\mBbbN{}j + 1. (\mneg{}\muparrow{}(P L[j]))) \mvdash{} i = j By Latex: (Decide \mkleeneopen{}i = j\mkleeneclose{}\mcdot{} THEN Auto) Home Index