Proof of Theorem swrdnd0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ianor 983 | . . 3
⊢ (¬
(𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) ↔ (¬ 𝐹 ∈ (0...𝐿) ∨ ¬ 𝐿 ∈ (0...(♯‘𝑆)))) | 
| 2 |  | 3ianor 1106 | . . . . 5
⊢ (¬
(𝐹 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝐹 ≤ 𝐿) ↔ (¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨
¬ 𝐹 ≤ 𝐿)) | 
| 3 |  | elfz2nn0 13659 | . . . . 5
⊢ (𝐹 ∈ (0...𝐿) ↔ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) | 
| 4 | 2, 3 | xchnxbir 333 | . . . 4
⊢ (¬
𝐹 ∈ (0...𝐿) ↔ (¬ 𝐹 ∈ ℕ0 ∨
¬ 𝐿 ∈
ℕ0 ∨ ¬ 𝐹 ≤ 𝐿)) | 
| 5 |  | 3ianor 1106 | . . . . 5
⊢ (¬
(𝐿 ∈
ℕ0 ∧ (♯‘𝑆) ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆)) ↔ (¬ 𝐿 ∈ ℕ0 ∨
¬ (♯‘𝑆)
∈ ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑆))) | 
| 6 |  | elfz2nn0 13659 | . . . . 5
⊢ (𝐿 ∈
(0...(♯‘𝑆))
↔ (𝐿 ∈
ℕ0 ∧ (♯‘𝑆) ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆))) | 
| 7 | 5, 6 | xchnxbir 333 | . . . 4
⊢ (¬
𝐿 ∈
(0...(♯‘𝑆))
↔ (¬ 𝐿 ∈
ℕ0 ∨ ¬ (♯‘𝑆) ∈ ℕ0 ∨ ¬
𝐿 ≤ (♯‘𝑆))) | 
| 8 | 4, 7 | orbi12i 914 | . . 3
⊢ ((¬
𝐹 ∈ (0...𝐿) ∨ ¬ 𝐿 ∈ (0...(♯‘𝑆))) ↔ ((¬ 𝐹 ∈ ℕ0 ∨
¬ 𝐿 ∈
ℕ0 ∨ ¬ 𝐹 ≤ 𝐿) ∨ (¬ 𝐿 ∈ ℕ0 ∨ ¬
(♯‘𝑆) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑆)))) | 
| 9 | 1, 8 | bitri 275 | . 2
⊢ (¬
(𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) ↔ ((¬ 𝐹 ∈ ℕ0 ∨
¬ 𝐿 ∈
ℕ0 ∨ ¬ 𝐹 ≤ 𝐿) ∨ (¬ 𝐿 ∈ ℕ0 ∨ ¬
(♯‘𝑆) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑆)))) | 
| 10 |  | df-3or 1087 | . . . . 5
⊢ ((¬
𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿) ↔ ((¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0)
∨ ¬ 𝐹 ≤ 𝐿)) | 
| 11 |  | ianor 983 | . . . . . . 7
⊢ (¬
(𝐹 ∈
ℕ0 ∧ 𝐿
∈ ℕ0) ↔ (¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈
ℕ0)) | 
| 12 |  | swrdnnn0nd 14695 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝑉 ∧ ¬ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
→ (𝑆 substr
〈𝐹, 𝐿〉) = ∅) | 
| 13 | 12 | expcom 413 | . . . . . . 7
⊢ (¬
(𝐹 ∈
ℕ0 ∧ 𝐿
∈ ℕ0) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 14 | 11, 13 | sylbir 235 | . . . . . 6
⊢ ((¬
𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 15 |  | anor 984 | . . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ↔ ¬ (¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈
ℕ0)) | 
| 16 |  | nn0re 12537 | . . . . . . . . . 10
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) | 
| 17 |  | nn0re 12537 | . . . . . . . . . 10
⊢ (𝐹 ∈ ℕ0
→ 𝐹 ∈
ℝ) | 
| 18 |  | ltnle 11341 | . . . . . . . . . 10
⊢ ((𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ) → (𝐿 < 𝐹 ↔ ¬ 𝐹 ≤ 𝐿)) | 
| 19 | 16, 17, 18 | syl2anr 597 | . . . . . . . . 9
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝐿 < 𝐹 ↔ ¬ 𝐹 ≤ 𝐿)) | 
| 20 |  | nn0z 12640 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ ℕ0
→ 𝐹 ∈
ℤ) | 
| 21 |  | nn0z 12640 | . . . . . . . . . . . . . . . . 17
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℤ) | 
| 22 | 20, 21 | anim12i 613 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) | 
| 23 | 22 | anim2i 617 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
→ (𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ))) | 
| 24 |  | 3anass 1094 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ↔ (𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ))) | 
| 25 | 23, 24 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
→ (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) | 
| 26 | 25 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
∧ 𝐿 < 𝐹) → (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) | 
| 27 | 17, 16 | anim12ci 614 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ)) | 
| 28 | 27 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
→ (𝐿 ∈ ℝ
∧ 𝐹 ∈
ℝ)) | 
| 29 |  | ltle 11350 | . . . . . . . . . . . . . . . 16
⊢ ((𝐿 ∈ ℝ ∧ 𝐹 ∈ ℝ) → (𝐿 < 𝐹 → 𝐿 ≤ 𝐹)) | 
| 30 | 28, 29 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
→ (𝐿 < 𝐹 → 𝐿 ≤ 𝐹)) | 
| 31 | 30 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
∧ 𝐿 < 𝐹) → 𝐿 ≤ 𝐹) | 
| 32 | 31 | 3mix2d 1337 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
∧ 𝐿 < 𝐹) → (𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑆) < 𝐿)) | 
| 33 |  | swrdnd 14693 | . . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑆) < 𝐿) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 34 | 26, 32, 33 | sylc 65 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
∧ 𝐿 < 𝐹) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅) | 
| 35 | 34 | ex 412 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0))
→ (𝐿 < 𝐹 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 36 | 35 | expcom 413 | . . . . . . . . . 10
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑆 ∈ Word 𝑉 → (𝐿 < 𝐹 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 37 | 36 | com23 86 | . . . . . . . . 9
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝐿 < 𝐹 → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 38 | 19, 37 | sylbird 260 | . . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (¬ 𝐹 ≤ 𝐿 → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 39 | 15, 38 | sylbir 235 | . . . . . . 7
⊢ (¬
(¬ 𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0) → (¬
𝐹 ≤ 𝐿 → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 40 | 39 | imp 406 | . . . . . 6
⊢ ((¬
(¬ 𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0) ∧ ¬
𝐹 ≤ 𝐿) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 41 | 14, 40 | jaoi3 1060 | . . . . 5
⊢ (((¬
𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0) ∨ ¬
𝐹 ≤ 𝐿) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 42 | 10, 41 | sylbi 217 | . . . 4
⊢ ((¬
𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 43 |  | 3anor 1107 | . . . . . 6
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) ↔ ¬ (¬
𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿)) | 
| 44 |  | pm2.24 124 | . . . . . . . . 9
⊢ (𝐿 ∈ ℕ0
→ (¬ 𝐿 ∈
ℕ0 → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 45 | 44 | 3ad2ant2 1134 | . . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) → (¬ 𝐿 ∈ ℕ0
→ (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 46 | 45 | com12 32 | . . . . . . 7
⊢ (¬
𝐿 ∈
ℕ0 → ((𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 47 |  | pm2.24 124 | . . . . . . . . 9
⊢
((♯‘𝑆)
∈ ℕ0 → (¬ (♯‘𝑆) ∈ ℕ0 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 48 |  | lencl 14572 | . . . . . . . . 9
⊢ (𝑆 ∈ Word 𝑉 → (♯‘𝑆) ∈
ℕ0) | 
| 49 | 47, 48 | syl11 33 | . . . . . . . 8
⊢ (¬
(♯‘𝑆) ∈
ℕ0 → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 50 | 49 | a1d 25 | . . . . . . 7
⊢ (¬
(♯‘𝑆) ∈
ℕ0 → ((𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 51 | 48 | nn0red 12590 | . . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝑉 → (♯‘𝑆) ∈ ℝ) | 
| 52 | 16 | 3ad2ant2 1134 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) → 𝐿 ∈
ℝ) | 
| 53 |  | ltnle 11341 | . . . . . . . . . . 11
⊢
(((♯‘𝑆)
∈ ℝ ∧ 𝐿
∈ ℝ) → ((♯‘𝑆) < 𝐿 ↔ ¬ 𝐿 ≤ (♯‘𝑆))) | 
| 54 | 51, 52, 53 | syl2anr 597 | . . . . . . . . . 10
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) ∧ 𝑆 ∈ Word 𝑉) → ((♯‘𝑆) < 𝐿 ↔ ¬ 𝐿 ≤ (♯‘𝑆))) | 
| 55 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) ∧ 𝑆 ∈ Word 𝑉) → 𝑆 ∈ Word 𝑉) | 
| 56 | 20 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) → 𝐹 ∈
ℤ) | 
| 57 | 56 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) ∧ 𝑆 ∈ Word 𝑉) → 𝐹 ∈ ℤ) | 
| 58 | 21 | 3ad2ant2 1134 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) → 𝐿 ∈
ℤ) | 
| 59 | 58 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) ∧ 𝑆 ∈ Word 𝑉) → 𝐿 ∈ ℤ) | 
| 60 | 55, 57, 59 | 3jca 1128 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) ∧ 𝑆 ∈ Word 𝑉) → (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) | 
| 61 |  | 3mix3 1332 | . . . . . . . . . . 11
⊢
((♯‘𝑆)
< 𝐿 → (𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑆) < 𝐿)) | 
| 62 | 60, 61, 33 | syl2im 40 | . . . . . . . . . 10
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) ∧ 𝑆 ∈ Word 𝑉) → ((♯‘𝑆) < 𝐿 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 63 | 54, 62 | sylbird 260 | . . . . . . . . 9
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝐹
≤ 𝐿) ∧ 𝑆 ∈ Word 𝑉) → (¬ 𝐿 ≤ (♯‘𝑆) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 64 | 63 | com12 32 | . . . . . . . 8
⊢ (¬
𝐿 ≤ (♯‘𝑆) → (((𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿) ∧ 𝑆 ∈ Word 𝑉) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 65 | 64 | expd 415 | . . . . . . 7
⊢ (¬
𝐿 ≤ (♯‘𝑆) → ((𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 66 | 46, 50, 65 | 3jaoi 1429 | . . . . . 6
⊢ ((¬
𝐿 ∈
ℕ0 ∨ ¬ (♯‘𝑆) ∈ ℕ0 ∨ ¬
𝐿 ≤ (♯‘𝑆)) → ((𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 67 | 43, 66 | biimtrrid 243 | . . . . 5
⊢ ((¬
𝐿 ∈
ℕ0 ∨ ¬ (♯‘𝑆) ∈ ℕ0 ∨ ¬
𝐿 ≤ (♯‘𝑆)) → (¬ (¬ 𝐹 ∈ ℕ0 ∨
¬ 𝐿 ∈
ℕ0 ∨ ¬ 𝐹 ≤ 𝐿) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 68 | 67 | impcom 407 | . . . 4
⊢ ((¬
(¬ 𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿) ∧ (¬ 𝐿 ∈ ℕ0 ∨ ¬
(♯‘𝑆) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑆))) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 69 | 42, 68 | jaoi3 1060 | . . 3
⊢ (((¬
𝐹 ∈
ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨ ¬ 𝐹 ≤ 𝐿) ∨ (¬ 𝐿 ∈ ℕ0 ∨ ¬
(♯‘𝑆) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑆))) → (𝑆 ∈ Word 𝑉 → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 70 | 69 | com12 32 | . 2
⊢ (𝑆 ∈ Word 𝑉 → (((¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ∨
¬ 𝐹 ≤ 𝐿) ∨ (¬ 𝐿 ∈ ℕ0 ∨ ¬
(♯‘𝑆) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑆))) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 71 | 9, 70 | biimtrid 242 | 1
⊢ (𝑆 ∈ Word 𝑉 → (¬ (𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅)) |