Step |
Hyp |
Ref |
Expression |
0 |
|
cslmd |
|
1 |
|
vg |
|
2 |
|
ccmn |
|
3 |
|
cbs |
|
4 |
1
|
cv |
|
5 |
4 3
|
cfv |
|
6 |
|
vv |
|
7 |
|
cplusg |
|
8 |
4 7
|
cfv |
|
9 |
|
va |
|
10 |
|
cvsca |
|
11 |
4 10
|
cfv |
|
12 |
|
vs |
|
13 |
|
csca |
|
14 |
4 13
|
cfv |
|
15 |
|
vf |
|
16 |
15
|
cv |
|
17 |
16 3
|
cfv |
|
18 |
|
vk |
|
19 |
16 7
|
cfv |
|
20 |
|
vp |
|
21 |
|
cmulr |
|
22 |
16 21
|
cfv |
|
23 |
|
vt |
|
24 |
|
csrg |
|
25 |
16 24
|
wcel |
|
26 |
|
vq |
|
27 |
18
|
cv |
|
28 |
|
vr |
|
29 |
|
vx |
|
30 |
6
|
cv |
|
31 |
|
vw |
|
32 |
28
|
cv |
|
33 |
12
|
cv |
|
34 |
31
|
cv |
|
35 |
32 34 33
|
co |
|
36 |
35 30
|
wcel |
|
37 |
9
|
cv |
|
38 |
29
|
cv |
|
39 |
34 38 37
|
co |
|
40 |
32 39 33
|
co |
|
41 |
32 38 33
|
co |
|
42 |
35 41 37
|
co |
|
43 |
40 42
|
wceq |
|
44 |
26
|
cv |
|
45 |
20
|
cv |
|
46 |
44 32 45
|
co |
|
47 |
46 34 33
|
co |
|
48 |
44 34 33
|
co |
|
49 |
48 35 37
|
co |
|
50 |
47 49
|
wceq |
|
51 |
36 43 50
|
w3a |
|
52 |
23
|
cv |
|
53 |
44 32 52
|
co |
|
54 |
53 34 33
|
co |
|
55 |
44 35 33
|
co |
|
56 |
54 55
|
wceq |
|
57 |
|
cur |
|
58 |
16 57
|
cfv |
|
59 |
58 34 33
|
co |
|
60 |
59 34
|
wceq |
|
61 |
|
c0g |
|
62 |
16 61
|
cfv |
|
63 |
62 34 33
|
co |
|
64 |
4 61
|
cfv |
|
65 |
63 64
|
wceq |
|
66 |
56 60 65
|
w3a |
|
67 |
51 66
|
wa |
|
68 |
67 31 30
|
wral |
|
69 |
68 29 30
|
wral |
|
70 |
69 28 27
|
wral |
|
71 |
70 26 27
|
wral |
|
72 |
25 71
|
wa |
|
73 |
72 23 22
|
wsbc |
|
74 |
73 20 19
|
wsbc |
|
75 |
74 18 17
|
wsbc |
|
76 |
75 15 14
|
wsbc |
|
77 |
76 12 11
|
wsbc |
|
78 |
77 9 8
|
wsbc |
|
79 |
78 6 5
|
wsbc |
|
80 |
79 1 2
|
crab |
|
81 |
0 80
|
wceq |
|