Step | Hyp | Ref
| Expression |
1 | | eulerpart.p |
. . . . 5
         
         |
2 | | eulerpart.o |
. . . . 5
         |
3 | | eulerpart.d |
. . . . 5
     
  |
4 | | eulerpart.j |
. . . . 5
   |
5 | | eulerpart.f |
. . . . 5
 
        |
6 | | eulerpart.h |
. . . . 5
       supp    |
7 | | eulerpart.m |
. . . . 5
    

        |
8 | | eulerpart.r |
. . . . 5
     
  |
9 | | eulerpart.t |
. . . . 5
          |
10 | | eulerpart.g |
. . . . 5
    𝟭          bits         |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemgv 29206 |
. . . 4
  
     𝟭          bits         |
12 | 11 | fveq1d 5867 |
. . 3
  
          𝟭          bits            |
13 | 12 | adantr 467 |
. 2
   
           𝟭          bits            |
14 | | nnex 10615 |
. . . 4
 |
15 | 14 | a1i 11 |
. . 3
   
   |
16 | | imassrn 5179 |
. . . . 5
      bits     
 |
17 | 4, 5 | oddpwdc 29187 |
. . . . . 6
       |
18 | | f1of 5814 |
. . . . . 6
      
        |
19 | | frn 5735 |
. . . . . 6
         |
20 | 17, 18, 19 | mp2b 10 |
. . . . 5
 |
21 | 16, 20 | sstri 3441 |
. . . 4
      bits     
 |
22 | 21 | a1i 11 |
. . 3
   
       bits        |
23 | | simpr 463 |
. . 3
   
   |
24 | | indfval 28838 |
. . 3
        bits         𝟭          bits                  bits           |
25 | 15, 22, 23, 24 | syl3anc 1268 |
. 2
   
   𝟭          bits                  bits           |
26 | | ffn 5728 |
. . . . . 6
           |
27 | 17, 18, 26 | mp2b 10 |
. . . . 5

  |
28 | | inss1 3652 |
. . . . . . . 8
         |
29 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemmf 29208 |
. . . . . . . . 9
  
bits 
    |
30 | 1, 2, 3, 4, 5, 6, 7 | eulerpartlem1 29200 |
. . . . . . . . . . 11
       
  |
31 | | f1of 5814 |
. . . . . . . . . . 11
                     |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . 10
          |
33 | 32 | ffvelrni 6021 |
. . . . . . . . 9
 bits   
   bits            |
34 | 29, 33 | syl 17 |
. . . . . . . 8
  
   bits            |
35 | 28, 34 | sseldi 3430 |
. . . . . . 7
  
   bits          |
36 | 35 | adantr 467 |
. . . . . 6
   
    bits      
   |
37 | 36 | elpwid 3961 |
. . . . 5
   
    bits         |
38 | | fvelimab 5921 |
. . . . 5
       bits 
             bits     
    bits             |
39 | 27, 37, 38 | sylancr 669 |
. . . 4
   
        bits     
    bits             |
40 | | ssrab2 3514 |
. . . . . . . . . 10
   |
41 | 4, 40 | eqsstri 3462 |
. . . . . . . . 9
 |
42 | 7 | a1i 11 |
. . . . . . . . . . . . . . . 16
  
    

         |
43 | | fveq1 5864 |
. . . . . . . . . . . . . . . . . . . 20
 bits         bits         |
44 | 43 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . 19
 bits          bits          |
45 | 44 | anbi2d 710 |
. . . . . . . . . . . . . . . . . 18
 bits          

 bits           |
46 | 45 | opabbidv 4466 |
. . . . . . . . . . . . . . . . 17
 bits        
          
 bits           |
47 | 46 | adantl 468 |
. . . . . . . . . . . . . . . 16
   
bits 
       
          
 bits           |
48 | 14, 41 | ssexi 4548 |
. . . . . . . . . . . . . . . . . 18
 |
49 | | abid2 2573 |
. . . . . . . . . . . . . . . . . . . 20
  bits         bits
       |
50 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . 20
 bits        |
51 | 49, 50 | eqeltri 2525 |
. . . . . . . . . . . . . . . . . . 19
  bits         |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   bits          |
53 | 48, 52 | opabex3 6772 |
. . . . . . . . . . . . . . . . 17
    
 bits          |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
  
    
 bits           |
55 | 42, 47, 29, 54 | fvmptd 5954 |
. . . . . . . . . . . . . . 15
  
   bits         
 bits           |
56 | | simpl 459 |
. . . . . . . . . . . . . . . . . 18
 
   |
57 | 56 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
 
     |
58 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
 
   |
59 | 56 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
 
  bits        bits         |
60 | 58, 59 | eleq12d 2523 |
. . . . . . . . . . . . . . . . 17
 
   bits      
 bits
         |
61 | 57, 60 | anbi12d 717 |
. . . . . . . . . . . . . . . 16
 
    bits        
 bits
          |
62 | 61 | cbvopabv 4472 |
. . . . . . . . . . . . . . 15
    
 bits             
 bits
         |
63 | 55, 62 | syl6eq 2501 |
. . . . . . . . . . . . . 14
  
   bits        

 bits           |
64 | 63 | eleq2d 2514 |
. . . . . . . . . . . . 13
  
    bits    
    
 bits
           |
65 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | eulerpartlemt0 29202 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               
   |
66 | 65 | simp1bi 1023 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    |
67 | | nn0ex 10875 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
68 | 67, 14 | elmap 7500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
      |
69 | 66, 68 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
      |
70 | | ffun 5731 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
71 | | funres 5621 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
72 | 69, 70, 71 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
  
    |
73 | 72 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
74 | | fssres 5749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
75 | 69, 41, 74 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
        |
76 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
    |
77 | 76 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
  
   |
78 | 75, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
  
  
   |
79 | 78 | biimpar 488 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
80 | | fvco 5941 |
. . . . . . . . . . . . . . . . . . . . 21
        bits       bits          |
81 | 73, 79, 80 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
   
  bits       bits          |
82 | | fvres 5879 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
83 | 82 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . 21
 bits        bits        |
84 | 83 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
   
 bits        bits        |
85 | 81, 84 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . 19
   
  bits       bits        |
86 | 85 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . 18
   
   bits      
bits         |
87 | 86 | pm5.32da 647 |
. . . . . . . . . . . . . . . . 17
  
 
 bits         bits          |
88 | 87 | opabbidv 4466 |
. . . . . . . . . . . . . . . 16
  
   

 bits             
bits          |
89 | 88 | eleq2d 2514 |
. . . . . . . . . . . . . . 15
  
       bits        
    
bits           |
90 | | elopab 4709 |
. . . . . . . . . . . . . . 15
    

bits       
        
bits          |
91 | 89, 90 | syl6bb 265 |
. . . . . . . . . . . . . 14
  
       bits                 
bits           |
92 | | ancom 452 |
. . . . . . . . . . . . . . . . 17
    

bits       
 
bits             |
93 | | anass 655 |
. . . . . . . . . . . . . . . . 17
  
bits      
   

 bits             |
94 | 92, 93 | bitri 253 |
. . . . . . . . . . . . . . . 16
    

bits       

 bits             |
95 | 94 | 2exbii 1719 |
. . . . . . . . . . . . . . 15
        

bits       
      bits     
       |
96 | | df-rex 2743 |
. . . . . . . . . . . . . . . . . 18
  bits         
   bits            |
97 | 96 | anbi2i 700 |
. . . . . . . . . . . . . . . . 17
   bits               bits     
       |
98 | 97 | exbii 1718 |
. . . . . . . . . . . . . . . 16
     bits                 bits     
       |
99 | | df-rex 2743 |
. . . . . . . . . . . . . . . 16
  
bits         
    bits             |
100 | | exdistr 1835 |
. . . . . . . . . . . . . . . 16
      
bits          
      bits     
       |
101 | 98, 99, 100 | 3bitr4i 281 |
. . . . . . . . . . . . . . 15
  
bits         
      bits     
       |
102 | 95, 101 | bitr4i 256 |
. . . . . . . . . . . . . 14
        

bits       

 bits            |
103 | 91, 102 | syl6bb 265 |
. . . . . . . . . . . . 13
  
       bits          
bits             |
104 | 64, 103 | bitrd 257 |
. . . . . . . . . . . 12
  
    bits    

 bits             |
105 | 104 | biimpa 487 |
. . . . . . . . . . 11
   
   bits     

 bits            |
106 | 105 | adantlr 721 |
. . . . . . . . . 10
         bits 
    

bits            |
107 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
                 |
108 | 107 | adantl 468 |
. . . . . . . . . . . . . . 15
           bits      
bits                         |
109 | | bitsss 14399 |
. . . . . . . . . . . . . . . . . . 19
bits     
 |
110 | 109 | sseli 3428 |
. . . . . . . . . . . . . . . . . 18
 bits     
  |
111 | 110 | anim2i 573 |
. . . . . . . . . . . . . . . . 17
 
bits       
   |
112 | 111 | ad2antlr 733 |
. . . . . . . . . . . . . . . 16
           bits      
bits            
   |
113 | | opelxp 4864 |
. . . . . . . . . . . . . . . . 17
      
   |
114 | 4, 5 | oddpwdcv 29188 |
. . . . . . . . . . . . . . . . . 18
                                   |
115 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . 21
 |
116 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . 21
 |
117 | 115, 116 | op2nd 6802 |
. . . . . . . . . . . . . . . . . . . 20
        |
118 | 117 | oveq2i 6301 |
. . . . . . . . . . . . . . . . . . 19
                |
119 | 115, 116 | op1st 6801 |
. . . . . . . . . . . . . . . . . . 19
        |
120 | 118, 119 | oveq12i 6302 |
. . . . . . . . . . . . . . . . . 18
                           |
121 | 114, 120 | syl6eq 2501 |
. . . . . . . . . . . . . . . . 17
                     |
122 | 113, 121 | sylbir 217 |
. . . . . . . . . . . . . . . 16
 
                |
123 | 112, 122 | syl 17 |
. . . . . . . . . . . . . . 15
           bits      
bits                           |
124 | 108, 123 | eqtr2d 2486 |
. . . . . . . . . . . . . 14
           bits      
bits                        |
125 | 124 | ex 436 |
. . . . . . . . . . . . 13
     

   bits      
bits                         |
126 | 125 | anassrs 654 |
. . . . . . . . . . . 12
           bits     

bits                        |
127 | 126 | reximdva 2862 |
. . . . . . . . . . 11
     

   bits     
   bits           bits                    |
128 | 127 | reximdva 2862 |
. . . . . . . . . 10
         bits 
       bits           
bits                    |
129 | 106, 128 | mpd 15 |
. . . . . . . . 9
         bits 
    

bits                   |
130 | | ssrexv 3494 |
. . . . . . . . 9

  
bits                   bits                    |
131 | 41, 129, 130 | mpsyl 65 |
. . . . . . . 8
         bits 
    
 bits                   |
132 | 131 | adantr 467 |
. . . . . . 7
     

   bits           
 bits                   |
133 | | eqeq2 2462 |
. . . . . . . . . 10
               
         |
134 | 133 | rexbidv 2901 |
. . . . . . . . 9
      
bits                  bits                |
135 | 134 | adantl 468 |
. . . . . . . 8
     

   bits             bits                
 bits                |
136 | 135 | rexbidv 2901 |
. . . . . . 7
     

   bits              bits                
  bits                |
137 | 132, 136 | mpbid 214 |
. . . . . 6
     

   bits           
 bits               |
138 | 137 | r19.29an 2931 |
. . . . 5
          bits             bits               |
139 | | simp-5l 778 |
. . . . . . . 8
       
   bits               bits             

   |
140 | | simpllr 769 |
. . . . . . . 8
       
   bits               bits             
  |
141 | | simplr 762 |
. . . . . . . . 9
       
   bits               bits             
bits        |
142 | 72 | adantr 467 |
. . . . . . . . . . . 12
   
     |
143 | 76 | eleq2d 2514 |
. . . . . . . . . . . . . 14
 
    
  
   |
144 | 75, 143 | syl 17 |
. . . . . . . . . . . . 13
  
  
   |
145 | 144 | biimpar 488 |
. . . . . . . . . . . 12
   
     |
146 | | fvco 5941 |
. . . . . . . . . . . 12
        bits       bits          |
147 | 142, 145,
146 | syl2anc 667 |
. . . . . . . . . . 11
   
  bits       bits          |
148 | | fvres 5879 |
. . . . . . . . . . . . 13
             |
149 | 148 | fveq2d 5869 |
. . . . . . . . . . . 12
 bits        bits        |
150 | 149 | adantl 468 |
. . . . . . . . . . 11
   
 bits        bits        |
151 | 147, 150 | eqtrd 2485 |
. . . . . . . . . 10
   
  bits       bits        |
152 | 139, 140,
151 | syl2anc 667 |
. . . . . . . . 9
       
   bits               bits             
 bits       bits        |
153 | 141, 152 | eleqtrrd 2532 |
. . . . . . . 8
       
   bits               bits             
 bits
        |
154 | 55 | eleq2d 2514 |
. . . . . . . . . 10
  
       bits 
  
  
    
 bits            |
155 | | opabid 4708 |
. . . . . . . . . 10
       

 bits           bits          |
156 | 154, 155 | syl6bb 265 |
. . . . . . . . 9
  
       bits 
  

 bits           |
157 | 156 | biimpar 488 |
. . . . . . . 8
    
 bits
              bits       |
158 | 139, 140,
153, 157 | syl12anc 1266 |
. . . . . . 7
       
   bits               bits             
  
   bits       |
159 | | simpr 463 |
. . . . . . . 8
       
   bits               bits             
        |
160 | 37 | ad4antr 738 |
. . . . . . . . 9
       
   bits               bits             
   bits         |
161 | 160, 158 | sseldd 3433 |
. . . . . . . 8
       
   bits               bits             
  
    |
162 | | opeq1 4166 |
. . . . . . . . . . . 12
         |
163 | 162 | eleq1d 2513 |
. . . . . . . . . . 11
               |
164 | 162 | fveq2d 5869 |
. . . . . . . . . . . 12
                 |
165 | | oveq2 6298 |
. . . . . . . . . . . 12
               |
166 | 164, 165 | eqeq12d 2466 |
. . . . . . . . . . 11
              
      
         |
167 | 163, 166 | imbi12d 322 |
. . . . . . . . . 10
       
      
                              |
168 | | opeq2 4167 |
. . . . . . . . . . . . 13
   
     |
169 | 168 | eleq1d 2513 |
. . . . . . . . . . . 12
               |
170 | 168 | fveq2d 5869 |
. . . . . . . . . . . . 13
                 |
171 | | oveq2 6298 |
. . . . . . . . . . . . . 14
           |
172 | 171 | oveq1d 6305 |
. . . . . . . . . . . . 13
               |
173 | 170, 172 | eqeq12d 2466 |
. . . . . . . . . . . 12
              
      
         |
174 | 169, 173 | imbi12d 322 |
. . . . . . . . . . 11
       
                   
      
          |
175 | 174, 121 | chvarv 2107 |
. . . . . . . . . 10
                     |
176 | 167, 175 | chvarv 2107 |
. . . . . . . . 9
                     |
177 | | eqeq2 2462 |
. . . . . . . . . 10
                    
      
   |
178 | 177 | biimpa 487 |
. . . . . . . . 9
                               |
179 | 176, 178 | sylan2 477 |
. . . . . . . 8
                       |
180 | 159, 161,
179 | syl2anc 667 |
. . . . . . 7
       
   bits               bits             
      
  |
181 | | fveq2 5865 |
. . . . . . . . 9
                 |
182 | 181 | eqeq1d 2453 |
. . . . . . . 8
                   |
183 | 182 | rspcev 3150 |
. . . . . . 7
        bits            
    bits            |
184 | 158, 180,
183 | syl2anc 667 |
. . . . . 6
       
   bits               bits             
    bits            |
185 | | oveq2 6298 |
. . . . . . . . . . 11
               |
186 | 185 | eqeq1d 2453 |
. . . . . . . . . 10
       
         |
187 | 171 | oveq1d 6305 |
. . . . . . . . . . 11
               |
188 | 187 | eqeq1d 2453 |
. . . . . . . . . 10
       
         |
189 | 186, 188 | sylan9bb 706 |
. . . . . . . . 9
 
                 |
190 | | simpl 459 |
. . . . . . . . . . 11
 
   |
191 | 190 | fveq2d 5869 |
. . . . . . . . . 10
 
           |
192 | 191 | fveq2d 5869 |
. . . . . . . . 9
 
 bits      bits        |
193 | 189, 192 | cbvrexdva2 3024 |
. . . . . . . 8
  
bits              bits                |
194 | 193 | cbvrexv 3020 |
. . . . . . 7
  
bits             
 bits               |
195 | | nfv 1761 |
. . . . . . . . . . . . . 14
    |
196 | | nfv 1761 |
. . . . . . . . . . . . . . 15
  |
197 | | nfre1 2848 |
. . . . . . . . . . . . . . 15
   bits              |
198 | 196, 197 | nfan 2011 |
. . . . . . . . . . . . . 14
    bits               |
199 | 195, 198 | nfan 2011 |
. . . . . . . . . . . . 13
       bits                |
200 | | simplr 762 |
. . . . . . . . . . . . . . . 16
      bits      
  |
201 | | n0i 3736 |
. . . . . . . . . . . . . . . . . . . 20
 bits     
bits        |
202 | 201 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
      bits       bits        |
203 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . 20
     bits      bits    |
204 | | 0bits 14413 |
. . . . . . . . . . . . . . . . . . . 20
bits   |
205 | 203, 204 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . 19
     bits        |
206 | 202, 205 | nsyl 125 |
. . . . . . . . . . . . . . . . . 18
      bits             |
207 | 69 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . . 22
   
       |
208 | 207 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
      bits             |
209 | | elnn0 10871 |
. . . . . . . . . . . . . . . . . . . . 21
    
            |
210 | 208, 209 | sylib 200 |
. . . . . . . . . . . . . . . . . . . 20
      bits                   |
211 | 210 | orcomd 390 |
. . . . . . . . . . . . . . . . . . 19
      bits                   |
212 | 211 | orcanai 924 |
. . . . . . . . . . . . . . . . . 18
     

bits                  |
213 | 206, 212 | mpdan 674 |
. . . . . . . . . . . . . . . . 17
      bits             |
214 | 65 | simp3bi 1025 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
       |
215 | 214 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
        |
216 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
217 | 216 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
218 | 217, 4 | elrab2 3198 |
. . . . . . . . . . . . . . . . . . . . . . . 24

    |
219 | 218 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
220 | 215, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     
  |
221 | 220 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . . . . 21
  
     
  |
222 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
223 | | elpreima 6002 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                |
224 | 69, 222, 223 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
     
         |
225 | 224 | imbi1d 319 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
      

      
    |
226 | | impexp 448 |
. . . . . . . . . . . . . . . . . . . . . . 23
       


    
    |
227 | 225, 226 | syl6bb 265 |
. . . . . . . . . . . . . . . . . . . . . 22
  
      


    
     |
228 | 227 | ralbidv2 2823 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
    
     
    |
229 | 221, 228 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . 20
  
     
   |
230 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
231 | 230 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
232 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
233 | 232 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
234 | 231, 233 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . 21
            
    |
235 | 234 | cbvralv 3019 |
. . . . . . . . . . . . . . . . . . . 20
 
      
        |
236 | 229, 235 | sylibr 216 |
. . . . . . . . . . . . . . . . . . 19
  
     
   |
237 | 236 | r19.21bi 2757 |
. . . . . . . . . . . . . . . . . 18
   
         |
238 | 237 | imp 431 |
. . . . . . . . . . . . . . . . 17
          
  |
239 | 213, 238 | syldan 473 |
. . . . . . . . . . . . . . . 16
      bits      
  |
240 | | breq2 4406 |
. . . . . . . . . . . . . . . . . 18
 
   |
241 | 240 | notbid 296 |
. . . . . . . . . . . . . . . . 17
 
   |
242 | 241, 4 | elrab2 3198 |
. . . . . . . . . . . . . . . 16

    |
243 | 200, 239,
242 | sylanbrc 670 |
. . . . . . . . . . . . . . 15
      bits      
  |
244 | 243 | adantlrr 727 |
. . . . . . . . . . . . . 14
       bits               bits      
  |
245 | 244 | adantr 467 |
. . . . . . . . . . . . 13
     
  bits               bits                |
246 | | simprr 766 |
. . . . . . . . . . . . 13
    
 bits               
bits               |
247 | 199, 245,
246 | r19.29af 2930 |
. . . . . . . . . . . 12
    
 bits              
  |
248 | 247, 246 | jca 535 |
. . . . . . . . . . 11
    
 bits                 bits                |
249 | 248 | ex 436 |
. . . . . . . . . 10
  
   bits             

 bits                 |
250 | 249 | reximdv2 2858 |
. . . . . . . . 9
  
 
 bits             
 bits                |
251 | 250 | imp 431 |
. . . . . . . 8
     
bits             

 bits               |
252 | 251 | adantlr 721 |
. . . . . . 7
        bits              

bits               |
253 | 194, 252 | sylan2b 478 |
. . . . . 6
        bits              

bits               |
254 | 184, 253 | r19.29vva 2934 |
. . . . 5
        bits              
   bits            |
255 | 138, 254 | impbida 843 |
. . . 4
   
      bits            bits                |
256 | 39, 255 | bitrd 257 |
. . 3
   
        bits     
  bits                |
257 | 256 | ifbid 3903 |
. 2
   
         bits             bits                  |
258 | 13, 25, 257 | 3eqtrd 2489 |
1
   
             bits                  |