Step | Hyp | Ref
| Expression |
1 | | lencl 12684 |
. . . . 5
 Word       |
2 | | eqeq2 2461 |
. . . . . . . . 9
     
       |
3 | 2 | anbi2d 709 |
. . . . . . . 8
               
        
        |
4 | 3 | imbi1d 319 |
. . . . . . 7
                 
         
         |
5 | 4 | 2ralbidv 2831 |
. . . . . 6
  
Word  
Word                   Word  
Word                     |
6 | | eqeq2 2461 |
. . . . . . . . 9
     
       |
7 | 6 | anbi2d 709 |
. . . . . . . 8
               
        
        |
8 | 7 | imbi1d 319 |
. . . . . . 7
                 
         
         |
9 | 8 | 2ralbidv 2831 |
. . . . . 6
  
Word  
Word                   Word  
Word                     |
10 | | eqeq2 2461 |
. . . . . . . . 9
       
         |
11 | 10 | anbi2d 709 |
. . . . . . . 8
                 
        
          |
12 | 11 | imbi1d 319 |
. . . . . . 7
                   
         
           |
13 | 12 | 2ralbidv 2831 |
. . . . . 6
    
Word  
Word                   Word  
Word                       |
14 | | eqeq2 2461 |
. . . . . . . . 9
    
                |
15 | 14 | anbi2d 709 |
. . . . . . . 8
    
         
                          |
16 | 15 | imbi1d 319 |
. . . . . . 7
    
                                        |
17 | 16 | 2ralbidv 2831 |
. . . . . 6
    
 
Word   Word           
     
 Word   Word           
             |
18 | | eqeq1 2454 |
. . . . . . . . . . . 12
                     |
19 | 18 | adantl 468 |
. . . . . . . . . . 11
   Word
Word                       |
20 | | eqcom 2457 |
. . . . . . . . . . . . . . 15
           |
21 | | hasheq0 12541 |
. . . . . . . . . . . . . . 15
 Word     
   |
22 | 20, 21 | syl5bb 261 |
. . . . . . . . . . . . . 14
 Word     
   |
23 | | hasheq0 12541 |
. . . . . . . . . . . . . . . 16
 Word     
   |
24 | | wrd2ind.6 |
. . . . . . . . . . . . . . . . . 18
 |
25 | | wrd2ind.1 |
. . . . . . . . . . . . . . . . . 18
       |
26 | 24, 25 | mpbiri 237 |
. . . . . . . . . . . . . . . . 17
     |
27 | 26 | ex 436 |
. . . . . . . . . . . . . . . 16


   |
28 | 23, 27 | syl6bi 232 |
. . . . . . . . . . . . . . 15
 Word           |
29 | 28 | com13 83 |
. . . . . . . . . . . . . 14

      Word
    |
30 | 22, 29 | syl6bi 232 |
. . . . . . . . . . . . 13
 Word            Word
     |
31 | 30 | com24 90 |
. . . . . . . . . . . 12
 Word  Word
               |
32 | 31 | imp31 434 |
. . . . . . . . . . 11
   Word
Word           
   |
33 | 19, 32 | sylbid 219 |
. . . . . . . . . 10
   Word
Word                   |
34 | 33 | ex 436 |
. . . . . . . . 9
  Word
Word                    |
35 | 34 | com23 81 |
. . . . . . . 8
  Word
Word                    |
36 | 35 | impd 433 |
. . . . . . 7
  Word
Word                    |
37 | 36 | rgen2 2812 |
. . . . . 6
 Word   Word           
       |
38 | | fveq2 5863 |
. . . . . . . . . . . . 13
           |
39 | | fveq2 5863 |
. . . . . . . . . . . . 13
           |
40 | 38, 39 | eqeqan12d 2466 |
. . . . . . . . . . . 12
 
         
           |
41 | 38 | eqeq1d 2452 |
. . . . . . . . . . . . 13
     
       |
42 | 41 | adantr 467 |
. . . . . . . . . . . 12
 
     
       |
43 | 40, 42 | anbi12d 716 |
. . . . . . . . . . 11
 
                                 |
44 | | wrd2ind.2 |
. . . . . . . . . . 11
 
 
   |
45 | 43, 44 | imbi12d 322 |
. . . . . . . . . 10
 
           
     
         
         |
46 | 45 | ancoms 455 |
. . . . . . . . 9
 
           
     
         
         |
47 | 46 | cbvraldva 3024 |
. . . . . . . 8
  
Word                   Word                     |
48 | 47 | cbvralv 3018 |
. . . . . . 7
 
Word   Word           
     
 Word   Word           
        |
49 | | swrdcl 12770 |
. . . . . . . . . . . . . . . . 17
 Word  substr          
Word   |
50 | 49 | adantr 467 |
. . . . . . . . . . . . . . . 16
  Word
Word   substr           Word   |
51 | 50 | ad2antrl 733 |
. . . . . . . . . . . . . . 15
    Word Word 
        
          substr          
Word   |
52 | | simprll 771 |
. . . . . . . . . . . . . . . 16
    Word Word 
        
         Word   |
53 | | eqeq1 2454 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
54 | | nn0p1nn 10906 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
55 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
     |
56 | 55 | eqcoms 2458 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
          |
57 | 54, 56 | syl5ibr 225 |
. . . . . . . . . . . . . . . . . . . . . 22
      

       |
58 | 53, 57 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . . . 21
               

        |
59 | 58 | impcom 432 |
. . . . . . . . . . . . . . . . . . . 20
                         |
60 | 59 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
   Word
Word                  

       |
61 | 60 | impcom 432 |
. . . . . . . . . . . . . . . . . 18
    Word Word 
        
               |
62 | 61 | nnge1d 10649 |
. . . . . . . . . . . . . . . . 17
    Word Word 
        
               |
63 | | wrdlenge1n0 12699 |
. . . . . . . . . . . . . . . . . 18
 Word 
       |
64 | 52, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
    Word Word 
        
         
       |
65 | 62, 64 | mpbird 236 |
. . . . . . . . . . . . . . . 16
    Word Word 
        
           |
66 | | lswcl 12712 |
. . . . . . . . . . . . . . . 16
  Word  lastS     |
67 | 52, 65, 66 | syl2anc 666 |
. . . . . . . . . . . . . . 15
    Word Word 
        
         lastS     |
68 | 51, 67 | jca 535 |
. . . . . . . . . . . . . 14
    Word Word 
        
           substr
         
Word lastS      |
69 | | swrdcl 12770 |
. . . . . . . . . . . . . . . 16
 Word  substr          
Word   |
70 | 69 | adantl 468 |
. . . . . . . . . . . . . . 15
  Word
Word   substr           Word   |
71 | 70 | ad2antrl 733 |
. . . . . . . . . . . . . 14
    Word Word 
        
          substr          
Word   |
72 | | simprlr 772 |
. . . . . . . . . . . . . . 15
    Word Word 
        
         Word   |
73 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . 20
           
     |
74 | 54, 73 | syl5ibr 225 |
. . . . . . . . . . . . . . . . . . 19
               |
75 | 74 | ad2antll 734 |
. . . . . . . . . . . . . . . . . 18
   Word
Word                  

       |
76 | 75 | impcom 432 |
. . . . . . . . . . . . . . . . 17
    Word Word 
        
               |
77 | 76 | nnge1d 10649 |
. . . . . . . . . . . . . . . 16
    Word Word 
        
               |
78 | | wrdlenge1n0 12699 |
. . . . . . . . . . . . . . . . 17
 Word 
       |
79 | 72, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
    Word Word 
        
         
       |
80 | 77, 79 | mpbird 236 |
. . . . . . . . . . . . . . 15
    Word Word 
        
           |
81 | | lswcl 12712 |
. . . . . . . . . . . . . . 15
  Word  lastS     |
82 | 72, 80, 81 | syl2anc 666 |
. . . . . . . . . . . . . 14
    Word Word 
        
         lastS     |
83 | 68, 71, 82 | jca32 538 |
. . . . . . . . . . . . 13
    Word Word 
        
            substr           Word
lastS      substr           Word
lastS       |
84 | 83 | adantlr 720 |
. . . . . . . . . . . 12
    Word  
Word                     Word
Word                       substr           Word
lastS      substr           Word
lastS       |
85 | | simprl 763 |
. . . . . . . . . . . . . 14
    Word  
Word                     Word
Word                     Word
Word    |
86 | | simplr 761 |
. . . . . . . . . . . . . 14
    Word  
Word                     Word
Word                     Word   Word           
        |
87 | | simprrl 773 |
. . . . . . . . . . . . . . . . 17
    Word  
Word                     Word
Word                              |
88 | 87 | oveq1d 6303 |
. . . . . . . . . . . . . . . 16
    Word  
Word                     Word
Word                                  |
89 | | simprlr 772 |
. . . . . . . . . . . . . . . . 17
    Word  
Word                     Word
Word                    Word   |
90 | | fzossfz 11935 |
. . . . . . . . . . . . . . . . . 18
 ..^              |
91 | | simprrr 774 |
. . . . . . . . . . . . . . . . . . . 20
    Word  
Word                     Word
Word                            |
92 | 54 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . 20
    Word  
Word                     Word
Word                        |
93 | 91, 92 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . . 19
    Word  
Word                     Word
Word                          |
94 | | fzo0end 12000 |
. . . . . . . . . . . . . . . . . . 19
    
       ..^       |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . 18
    Word  
Word                     Word
Word                           ..^       |
96 | 90, 95 | sseldi 3429 |
. . . . . . . . . . . . . . . . 17
    Word  
Word                     Word
Word                                    |
97 | | swrd0len 12773 |
. . . . . . . . . . . . . . . . 17
  Word                    substr                    |
98 | 89, 96, 97 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
    Word  
Word                     Word
Word                        substr                    |
99 | | simprll 771 |
. . . . . . . . . . . . . . . . 17
    Word  
Word                     Word
Word                    Word   |
100 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . 22
        
              |
101 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . . . 22
        
                  |
102 | 100, 101 | eleq12d 2522 |
. . . . . . . . . . . . . . . . . . . . 21
        
                                |
103 | 102 | eqcoms 2458 |
. . . . . . . . . . . . . . . . . . . 20
        
                                |
104 | 103 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
                               
                 |
105 | 104 | ad2antll 734 |
. . . . . . . . . . . . . . . . . 18
    Word  
Word                     Word
Word                                  
                 |
106 | 96, 105 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
    Word  
Word                     Word
Word                                    |
107 | | swrd0len 12773 |
. . . . . . . . . . . . . . . . 17
  Word                    substr                    |
108 | 99, 106, 107 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
    Word  
Word                     Word
Word                        substr                    |
109 | 88, 98, 108 | 3eqtr4d 2494 |
. . . . . . . . . . . . . . 15
    Word  
Word                     Word
Word                        substr                substr              |
110 | 91 | oveq1d 6303 |
. . . . . . . . . . . . . . . 16
    Word  
Word                     Word
Word                                |
111 | | nn0cn 10876 |
. . . . . . . . . . . . . . . . . 18

  |
112 | 111 | ad2antrr 731 |
. . . . . . . . . . . . . . . . 17
    Word  
Word                     Word
Word                      |
113 | | ax-1cn 9594 |
. . . . . . . . . . . . . . . . 17
 |
114 | | pncan 9878 |
. . . . . . . . . . . . . . . . 17
 
       |
115 | 112, 113,
114 | sylancl 667 |
. . . . . . . . . . . . . . . 16
    Word  
Word                     Word
Word                          |
116 | 98, 110, 115 | 3eqtrd 2488 |
. . . . . . . . . . . . . . 15
    Word  
Word                     Word
Word                        substr              |
117 | 109, 116 | jca 535 |
. . . . . . . . . . . . . 14
    Word  
Word                     Word
Word                         substr                substr                substr               |
118 | 70 | adantr 467 |
. . . . . . . . . . . . . . . 16
   Word
Word   substr             substr          
Word   |
119 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . 22
  substr                   substr              |
120 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . . 22
  substr                   substr              |
121 | 119, 120 | eqeqan12d 2466 |
. . . . . . . . . . . . . . . . . . . . 21
   substr          

substr                         substr                substr               |
122 | 121 | expcom 437 |
. . . . . . . . . . . . . . . . . . . 20
  substr             substr          
             substr                substr                |
123 | 122 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
   Word
Word   substr              substr          
             substr                substr                |
124 | 123 | imp 431 |
. . . . . . . . . . . . . . . . . 18
    Word Word 

substr             substr                    
    substr                substr               |
125 | 119 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . . . 19
  substr               
    substr               |
126 | 125 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
    Word Word 

substr             substr                
    substr               |
127 | 124, 126 | anbi12d 716 |
. . . . . . . . . . . . . . . . 17
    Word Word 

substr             substr                                substr                substr                substr                |
128 | | vex 3047 |
. . . . . . . . . . . . . . . . . . . . 21
 |
129 | | vex 3047 |
. . . . . . . . . . . . . . . . . . . . 21
 |
130 | 128, 129,
44 | sbc2ie 3334 |
. . . . . . . . . . . . . . . . . . . 20
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  |
131 | 130 | bicomi 206 |
. . . . . . . . . . . . . . . . . . 19
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
    Word Word 

substr             substr            
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
133 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
    Word Word 

substr             substr             substr             |
134 | 133 | sbceq1d 3271 |
. . . . . . . . . . . . . . . . . 18
    Word Word 

substr             substr               ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
135 | | dfsbcq 3268 |
. . . . . . . . . . . . . . . . . . . . 21
  substr            
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)    |
136 | 135 | sbcbidv 3321 |
. . . . . . . . . . . . . . . . . . . 20
  substr              substr            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)    |
137 | 136 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
   Word
Word   substr               substr            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)    |
138 | 137 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
    Word Word 

substr             substr               substr            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)    |
139 | 132, 134,
138 | 3bitrd 283 |
. . . . . . . . . . . . . . . . 17
    Word Word 

substr             substr            
  substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)    |
140 | 127, 139 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
    Word Word 

substr             substr                      
     
      substr                substr                substr               substr          
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     |
141 | 118, 140 | rspcdv 3152 |
. . . . . . . . . . . . . . 15
   Word
Word   substr             
Word                        substr                substr                substr               substr          
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     |
142 | 50, 141 | rspcimdv 3150 |
. . . . . . . . . . . . . 14
  Word
Word    Word   Word                        substr                substr                substr               substr          
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     |
143 | 85, 86, 117, 142 | syl3c 63 |
. . . . . . . . . . . . 13
    Word  
Word                     Word
Word                      substr          
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   |
144 | 143, 109 | jca 535 |
. . . . . . . . . . . 12
    Word  
Word                     Word
Word                       substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     substr                substr               |
145 | | dfsbcq 3268 |
. . . . . . . . . . . . . . . 16
  substr            
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
146 | | sbccom 3338 |
. . . . . . . . . . . . . . . 16
  
substr          
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   |
147 | 145, 146 | syl6bb 265 |
. . . . . . . . . . . . . . 15
  substr            
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)    |
148 | 120 | eqeq2d 2460 |
. . . . . . . . . . . . . . 15
  substr                            substr               |
149 | 147, 148 | anbi12d 716 |
. . . . . . . . . . . . . 14
  substr               ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)             ![]. ].](_drbrack.gif)   substr          
 ![]. ].](_drbrack.gif)         substr                |
150 | | oveq1 6295 |
. . . . . . . . . . . . . . 15
  substr            ++        substr           ++        |
151 | 150 | sbceq1d 3271 |
. . . . . . . . . . . . . 14
  substr              ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)
   substr           ++
      ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)    |
152 | 149, 151 | imbi12d 322 |
. . . . . . . . . . . . 13
  substr                ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)            ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)         substr                substr           ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)     |
153 | | s1eq 12736 |
. . . . . . . . . . . . . . . . 17
 lastS  
      lastS       |
154 | 153 | oveq2d 6304 |
. . . . . . . . . . . . . . . 16
 lastS  
  substr           ++
       substr           ++   lastS        |
155 | 154 | sbceq1d 3271 |
. . . . . . . . . . . . . . 15
 lastS  
    substr           ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)
   substr           ++
  lastS       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)    |
156 | 155 | imbi2d 318 |
. . . . . . . . . . . . . 14
 lastS  
     ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)         substr                substr           ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)         substr                substr           ++   lastS       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)     |
157 | | sbccom 3338 |
. . . . . . . . . . . . . . . 16
    substr           ++   lastS       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)   |
158 | 157 | a1i 11 |
. . . . . . . . . . . . . . 15
 lastS  
    substr           ++   lastS       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)    |
159 | 158 | imbi2d 318 |
. . . . . . . . . . . . . 14
 lastS  
     ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)         substr                substr           ++   lastS       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif) 
  
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)         substr               ++       ![]. ].](_drbrack.gif)    substr           ++   lastS       ![]. ].](_drbrack.gif)     |
160 | 156, 159 | bitrd 257 |
. . . . . . . . . . . . 13
 lastS  
     ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)         substr                substr           ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)         substr               ++       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)     |
161 | | dfsbcq 3268 |
. . . . . . . . . . . . . . 15
  substr            
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)    |
162 | 119 | eqeq1d 2452 |
. . . . . . . . . . . . . . 15
  substr                    substr           
    substr                substr               |
163 | 161, 162 | anbi12d 716 |
. . . . . . . . . . . . . 14
  substr               ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)         substr            
  
substr          
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     substr                substr                |
164 | | oveq1 6295 |
. . . . . . . . . . . . . . 15
  substr            ++        substr           ++        |
165 | 164 | sbceq1d 3271 |
. . . . . . . . . . . . . 14
  substr              ++       ![]. ].](_drbrack.gif)    substr           ++   lastS       ![]. ].](_drbrack.gif)
   substr           ++
      ![]. ].](_drbrack.gif)    substr           ++   lastS       ![]. ].](_drbrack.gif)    |
166 | 163, 165 | imbi12d 322 |
. . . . . . . . . . . . 13
  substr                ![]. ].](_drbrack.gif)   substr          
 ![]. ].](_drbrack.gif)         substr               ++       ![]. ].](_drbrack.gif)    substr           ++   lastS       ![]. ].](_drbrack.gif)      substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     substr                substr                substr           ++       ![]. ].](_drbrack.gif)    substr           ++   lastS       ![]. ].](_drbrack.gif)     |
167 | | s1eq 12736 |
. . . . . . . . . . . . . . . 16
 lastS  
      lastS       |
168 | 167 | oveq2d 6304 |
. . . . . . . . . . . . . . 15
 lastS  
  substr           ++
       substr           ++   lastS        |
169 | 168 | sbceq1d 3271 |
. . . . . . . . . . . . . 14
 lastS  
    substr           ++       ![]. ].](_drbrack.gif)    substr           ++   lastS       ![]. ].](_drbrack.gif)
   substr           ++
  lastS       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)    |
170 | 169 | imbi2d 318 |
. . . . . . . . . . . . 13
 lastS  
     substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     substr                substr                substr           ++       ![]. ].](_drbrack.gif)    substr           ++   lastS       ![]. ].](_drbrack.gif)      substr            ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     substr                substr                substr           ++   lastS       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)     |
171 | | simplr 761 |
. . . . . . . . . . . . . . . . . 18
    Word 
 Word             Word
   |
172 | | simpll 759 |
. . . . . . . . . . . . . . . . . 18
    Word 
 Word             Word
   |
173 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
    Word 
 Word                      |
174 | | wrd2ind.7 |
. . . . . . . . . . . . . . . . . 18
   Word

 Word               |
175 | 171, 172,
173, 174 | syl3anc 1267 |
. . . . . . . . . . . . . . . . 17
    Word 
 Word                |
176 | 44 | ancoms 455 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
177 | 129, 128,
176 | sbc2ie 3334 |
. . . . . . . . . . . . . . . . 17
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  |
178 | | ovex 6316 |
. . . . . . . . . . . . . . . . . 18
 ++     
 |
179 | | ovex 6316 |
. . . . . . . . . . . . . . . . . 18
 ++     
 |
180 | | wrd2ind.3 |
. . . . . . . . . . . . . . . . . . 19
   ++       ++       
   |
181 | 180 | ancoms 455 |
. . . . . . . . . . . . . . . . . 18
   ++       ++       
   |
182 | 178, 179,
181 | sbc2ie 3334 |
. . . . . . . . . . . . . . . . 17
   ++
      ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)
  |
183 | 175, 177,
182 | 3imtr4g 274 |
. . . . . . . . . . . . . . . 16
    Word 
 Word             
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)    |
184 | 183 | ex 436 |
. . . . . . . . . . . . . . 15
   Word

 Word             
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)     |
185 | 184 | com23 81 |
. . . . . . . . . . . . . 14
   Word

 Word      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
        
  ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)     |
186 | 185 | impd 433 |
. . . . . . . . . . . . 13
   Word

 Word       ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)            ++       ![]. ].](_drbrack.gif)   ++       ![]. ].](_drbrack.gif)    |
187 | 152, 160,
166, 170, 186 | vtocl4ga 3118 |
. . . . . . . . . . . 12
    substr           Word
lastS      substr           Word
lastS        
substr          
 ![]. ].](_drbrack.gif)   substr            ![]. ].](_drbrack.gif)     substr                substr                substr           ++   lastS       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)    |
188 | 84, 144, 187 | sylc 62 |
. . . . . . . . . . 11
    Word  
Word                     Word
Word                       substr
          ++
  lastS       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)   |
189 | | eqtr2 2470 |
. . . . . . . . . . . . . . . 16
                         |
190 | 189 | ad2antll 734 |
. . . . . . . . . . . . . . 15
    Word  
Word                     Word
Word                            |
191 | 190, 92 | eqeltrd 2528 |
. . . . . . . . . . . . . 14
    Word  
Word                     Word
Word                          |
192 | | wrdfin 12683 |
. . . . . . . . . . . . . . . . 17
 Word   |
193 | 192 | adantr 467 |
. . . . . . . . . . . . . . . 16
  Word
Word    |
194 | 193 | ad2antrl 733 |
. . . . . . . . . . . . . . 15
    Word  
Word                     Word
Word                      |
195 | | hashnncl 12544 |
. . . . . . . . . . . . . . 15
     
   |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . 14
    Word  
Word                     Word
Word                        
   |
197 | 191, 196 | mpbid 214 |
. . . . . . . . . . . . 13
    Word  
Word                     Word
Word                      |
198 | | swrdccatwrd 12819 |
. . . . . . . . . . . . . 14
  Word    substr
          ++
  lastS     
  |
199 | 198 | eqcomd 2456 |
. . . . . . . . . . . . 13
  Word    substr           ++   lastS        |
200 | 99, 197, 199 | syl2anc 666 |
. . . . . . . . . . . 12
    Word  
Word                     Word
Word                      substr           ++   lastS        |
201 | | wrdfin 12683 |
. . . . . . . . . . . . . . . . 17
 Word   |
202 | 201 | adantl 468 |
. . . . . . . . . . . . . . . 16
  Word
Word    |
203 | 202 | ad2antrl 733 |
. . . . . . . . . . . . . . 15
    Word  
Word                     Word
Word                      |
204 | | hashnncl 12544 |
. . . . . . . . . . . . . . 15
     
   |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . 14
    Word  
Word                     Word
Word                        
   |
206 | 93, 205 | mpbid 214 |
. . . . . . . . . . . . 13
    Word  
Word                     Word
Word                      |
207 | | swrdccatwrd 12819 |
. . . . . . . . . . . . . 14
  Word    substr
          ++
  lastS     
  |
208 | 207 | eqcomd 2456 |
. . . . . . . . . . . . 13
  Word    substr           ++   lastS        |
209 | 89, 206, 208 | syl2anc 666 |
. . . . . . . . . . . 12
    Word  
Word                     Word
Word                      substr           ++   lastS        |
210 | | sbceq1a 3277 |
. . . . . . . . . . . . 13
   substr           ++   lastS      
   substr           ++
  lastS       ![]. ].](_drbrack.gif)    |
211 | | sbceq1a 3277 |
. . . . . . . . . . . . 13
   substr           ++   lastS          substr           ++
  lastS       ![]. ].](_drbrack.gif)
   substr           ++
  lastS       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)    |
212 | 210, 211 | sylan9bb 705 |
. . . . . . . . . . . 12
    substr           ++
  lastS        substr           ++   lastS           substr           ++   lastS       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)    |
213 | 200, 209,
212 | syl2anc 666 |
. . . . . . . . . . 11
    Word  
Word                     Word
Word                        substr           ++   lastS       ![]. ].](_drbrack.gif)    substr
          ++
  lastS       ![]. ].](_drbrack.gif)    |
214 | 188, 213 | mpbird 236 |
. . . . . . . . . 10
    Word  
Word                     Word
Word                      |
215 | 214 | expr 619 |
. . . . . . . . 9
    Word  
Word                    Word
Word  
         
          |
216 | 215 | ralrimivva 2808 |
. . . . . . . 8
   Word  
Word                    Word   Word           
          |
217 | 216 | ex 436 |
. . . . . . 7

 
Word   Word           
      
Word  
Word                       |
218 | 48, 217 | syl5bi 221 |
. . . . . 6

 
Word   Word           
       Word   Word           
           |
219 | 5, 9, 13, 17, 37, 218 | nn0ind 11027 |
. . . . 5
    
 Word   Word           
            |
220 | 1, 219 | syl 17 |
. . . 4
 Word  Word   Word           
            |
221 | 220 | 3ad2ant1 1028 |
. . 3
  Word
Word           Word   Word           
            |
222 | | fveq2 5863 |
. . . . . . . . 9
           |
223 | 222 | eqeq2d 2460 |
. . . . . . . 8
                     |
224 | 223 | anbi1d 710 |
. . . . . . 7
                   
        
            |
225 | | wrd2ind.5 |
. . . . . . 7
     |
226 | 224, 225 | imbi12d 322 |
. . . . . 6
                     
         
             |
227 | 226 | ralbidv 2826 |
. . . . 5
  
Word                       Word                         |
228 | 227 | rspcv 3145 |
. . . 4
 Word  
Word  
Word                       Word                         |
229 | 228 | 3ad2ant2 1029 |
. . 3
  Word
Word           
Word  
Word                       Word                         |
230 | 221, 229 | mpd 15 |
. 2
  Word
Word           Word           
            |
231 | | eqidd 2451 |
. 2
  Word
Word                    |
232 | | fveq2 5863 |
. . . . . . . . . . 11
           |
233 | 232 | eqeq1d 2452 |
. . . . . . . . . 10
                     |
234 | 232 | eqeq1d 2452 |
. . . . . . . . . 10
                     |
235 | 233, 234 | anbi12d 716 |
. . . . . . . . 9
                   
        
            |
236 | | wrd2ind.4 |
. . . . . . . . 9
     |
237 | 235, 236 | imbi12d 322 |
. . . . . . . 8
                     
         
             |
238 | 237 | rspcv 3145 |
. . . . . . 7
 Word  
Word                               
             |
239 | 238 | com23 81 |
. . . . . 6
 Word                     
Word                          |
240 | 239 | expd 438 |
. . . . 5
 Word         
        
 
Word                           |
241 | 240 | com34 86 |
. . . 4
 Word         
 
Word                                    |
242 | 241 | imp 431 |
. . 3
  Word           
Word                                   |
243 | 242 | 3adant2 1026 |
. 2
  Word
Word           
Word                                   |