Detailed syntax breakdown of Definition df-hdmap1
Step | Hyp | Ref
| Expression |
1 | | chdma1 35354 |
. 2
HDMap1 |
2 | | vk |
. . 3
 |
3 | | cvv 3044 |
. . 3
 |
4 | | vw |
. . . 4
 |
5 | 2 | cv 1442 |
. . . . 5
 |
6 | | clh 33543 |
. . . . 5
 |
7 | 5, 6 | cfv 5581 |
. . . 4
     |
8 | | va |
. . . . . . . . . . . . . 14
 |
9 | 8 | cv 1442 |
. . . . . . . . . . . . 13
 |
10 | | vx |
. . . . . . . . . . . . . 14
 |
11 | | vv |
. . . . . . . . . . . . . . . . 17
 |
12 | 11 | cv 1442 |
. . . . . . . . . . . . . . . 16
 |
13 | | vd |
. . . . . . . . . . . . . . . . 17
 |
14 | 13 | cv 1442 |
. . . . . . . . . . . . . . . 16
 |
15 | 12, 14 | cxp 4831 |
. . . . . . . . . . . . . . 15
   |
16 | 15, 12 | cxp 4831 |
. . . . . . . . . . . . . 14
     |
17 | 10 | cv 1442 |
. . . . . . . . . . . . . . . . 17
 |
18 | | c2nd 6789 |
. . . . . . . . . . . . . . . . 17
 |
19 | 17, 18 | cfv 5581 |
. . . . . . . . . . . . . . . 16
     |
20 | | vu |
. . . . . . . . . . . . . . . . . 18
 |
21 | 20 | cv 1442 |
. . . . . . . . . . . . . . . . 17
 |
22 | | c0g 15331 |
. . . . . . . . . . . . . . . . 17
 |
23 | 21, 22 | cfv 5581 |
. . . . . . . . . . . . . . . 16
     |
24 | 19, 23 | wceq 1443 |
. . . . . . . . . . . . . . 15
         |
25 | | vc |
. . . . . . . . . . . . . . . . 17
 |
26 | 25 | cv 1442 |
. . . . . . . . . . . . . . . 16
 |
27 | 26, 22 | cfv 5581 |
. . . . . . . . . . . . . . 15
     |
28 | 19 | csn 3967 |
. . . . . . . . . . . . . . . . . . . 20
       |
29 | | vn |
. . . . . . . . . . . . . . . . . . . . 21
 |
30 | 29 | cv 1442 |
. . . . . . . . . . . . . . . . . . . 20
 |
31 | 28, 30 | cfv 5581 |
. . . . . . . . . . . . . . . . . . 19
           |
32 | | vm |
. . . . . . . . . . . . . . . . . . . 20
 |
33 | 32 | cv 1442 |
. . . . . . . . . . . . . . . . . . 19
 |
34 | 31, 33 | cfv 5581 |
. . . . . . . . . . . . . . . . . 18
               |
35 | | vh |
. . . . . . . . . . . . . . . . . . . . 21
 |
36 | 35 | cv 1442 |
. . . . . . . . . . . . . . . . . . . 20
 |
37 | 36 | csn 3967 |
. . . . . . . . . . . . . . . . . . 19
   |
38 | | vj |
. . . . . . . . . . . . . . . . . . . 20
 |
39 | 38 | cv 1442 |
. . . . . . . . . . . . . . . . . . 19
 |
40 | 37, 39 | cfv 5581 |
. . . . . . . . . . . . . . . . . 18
       |
41 | 34, 40 | wceq 1443 |
. . . . . . . . . . . . . . . . 17
                     |
42 | | c1st 6788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
43 | 17, 42 | cfv 5581 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
44 | 43, 42 | cfv 5581 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
45 | | csg 16664 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
46 | 21, 45 | cfv 5581 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
47 | 44, 19, 46 | co 6288 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
48 | 47 | csn 3967 |
. . . . . . . . . . . . . . . . . . . 20
                       |
49 | 48, 30 | cfv 5581 |
. . . . . . . . . . . . . . . . . . 19
                           |
50 | 49, 33 | cfv 5581 |
. . . . . . . . . . . . . . . . . 18
                               |
51 | 43, 18 | cfv 5581 |
. . . . . . . . . . . . . . . . . . . . 21
         |
52 | 26, 45 | cfv 5581 |
. . . . . . . . . . . . . . . . . . . . 21
     |
53 | 51, 36, 52 | co 6288 |
. . . . . . . . . . . . . . . . . . . 20
                 |
54 | 53 | csn 3967 |
. . . . . . . . . . . . . . . . . . 19
                   |
55 | 54, 39 | cfv 5581 |
. . . . . . . . . . . . . . . . . 18
                       |
56 | 50, 55 | wceq 1443 |
. . . . . . . . . . . . . . . . 17
                                                     |
57 | 41, 56 | wa 371 |
. . . . . . . . . . . . . . . 16
                    
                                                      |
58 | 57, 35, 14 | crio 6249 |
. . . . . . . . . . . . . . 15
                      
                                                       |
59 | 24, 27, 58 | cif 3880 |
. . . . . . . . . . . . . 14
                                      
                                                        |
60 | 10, 16, 59 | cmpt 4460 |
. . . . . . . . . . . . 13
                                           
                                                         |
61 | 9, 60 | wcel 1886 |
. . . . . . . . . . . 12
                      
                                                                              |
62 | 4 | cv 1442 |
. . . . . . . . . . . . 13
 |
63 | | cmpd 35186 |
. . . . . . . . . . . . . 14
mapd |
64 | 5, 63 | cfv 5581 |
. . . . . . . . . . . . 13
mapd   |
65 | 62, 64 | cfv 5581 |
. . . . . . . . . . . 12
 mapd      |
66 | 61, 32, 65 | wsbc 3266 |
. . . . . . . . . . 11
  mapd      ![]. ].](_drbrack.gif)
                                           
                                                         |
67 | | clspn 18187 |
. . . . . . . . . . . 12
 |
68 | 26, 67 | cfv 5581 |
. . . . . . . . . . 11
     |
69 | 66, 38, 68 | wsbc 3266 |
. . . . . . . . . 10
      ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                                                                                     |
70 | | cbs 15114 |
. . . . . . . . . . 11
 |
71 | 26, 70 | cfv 5581 |
. . . . . . . . . 10
     |
72 | 69, 13, 71 | wsbc 3266 |
. . . . . . . . 9
      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                                                                                     |
73 | | clcd 35148 |
. . . . . . . . . . 11
LCDual |
74 | 5, 73 | cfv 5581 |
. . . . . . . . . 10
LCDual   |
75 | 62, 74 | cfv 5581 |
. . . . . . . . 9
 LCDual      |
76 | 72, 25, 75 | wsbc 3266 |
. . . . . . . 8
  LCDual      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                           
                                                         |
77 | 21, 67 | cfv 5581 |
. . . . . . . 8
     |
78 | 76, 29, 77 | wsbc 3266 |
. . . . . . 7
      ![]. ].](_drbrack.gif)   LCDual      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                           
                                                         |
79 | 21, 70 | cfv 5581 |
. . . . . . 7
     |
80 | 78, 11, 79 | wsbc 3266 |
. . . . . 6
      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   LCDual      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                           
                                                         |
81 | | cdvh 34640 |
. . . . . . . 8
 |
82 | 5, 81 | cfv 5581 |
. . . . . . 7
     |
83 | 62, 82 | cfv 5581 |
. . . . . 6
         |
84 | 80, 20, 83 | wsbc 3266 |
. . . . 5
          ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   LCDual      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                           
                                                         |
85 | 84, 8 | cab 2436 |
. . . 4
           ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   LCDual      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                           
                                                          |
86 | 4, 7, 85 | cmpt 4460 |
. . 3
                ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   LCDual      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                           
                                                           |
87 | 2, 3, 86 | cmpt 4460 |
. 2
                 ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   LCDual      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                           
                                                            |
88 | 1, 87 | wceq 1443 |
1
HDMap1                  ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   LCDual      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   mapd      ![]. ].](_drbrack.gif)
                                           
                                                            |