Detailed syntax breakdown of Definition df-efg
Step | Hyp | Ref
| Expression |
1 | | cefg 18119 |
. 2
~FG |
2 | | vi |
. . 3
|
3 | | cvv 3200 |
. . 3
|
4 | 2 | cv 1482 |
. . . . . . . . 9
|
5 | | c2o 7554 |
. . . . . . . . 9
|
6 | 4, 5 | cxp 5112 |
. . . . . . . 8
|
7 | 6 | cword 13291 |
. . . . . . 7
Word |
8 | | vr |
. . . . . . . 8
|
9 | 8 | cv 1482 |
. . . . . . 7
|
10 | 7, 9 | wer 7739 |
. . . . . 6
Word |
11 | | vx |
. . . . . . . . . . . 12
|
12 | 11 | cv 1482 |
. . . . . . . . . . 11
|
13 | | vn |
. . . . . . . . . . . . . 14
|
14 | 13 | cv 1482 |
. . . . . . . . . . . . 13
|
15 | | vy |
. . . . . . . . . . . . . . . 16
|
16 | 15 | cv 1482 |
. . . . . . . . . . . . . . 15
|
17 | | vz |
. . . . . . . . . . . . . . . 16
|
18 | 17 | cv 1482 |
. . . . . . . . . . . . . . 15
|
19 | 16, 18 | cop 4183 |
. . . . . . . . . . . . . 14
|
20 | | c1o 7553 |
. . . . . . . . . . . . . . . 16
|
21 | 20, 18 | cdif 3571 |
. . . . . . . . . . . . . . 15
|
22 | 16, 21 | cop 4183 |
. . . . . . . . . . . . . 14
|
23 | 19, 22 | cs2 13586 |
. . . . . . . . . . . . 13
|
24 | 14, 14, 23 | cotp 4185 |
. . . . . . . . . . . 12
|
25 | | csplice 13296 |
. . . . . . . . . . . 12
splice |
26 | 12, 24, 25 | co 6650 |
. . . . . . . . . . 11
splice |
27 | 12, 26, 9 | wbr 4653 |
. . . . . . . . . 10
splice |
28 | 27, 17, 5 | wral 2912 |
. . . . . . . . 9
splice |
29 | 28, 15, 4 | wral 2912 |
. . . . . . . 8
splice |
30 | | cc0 9936 |
. . . . . . . . 9
|
31 | | chash 13117 |
. . . . . . . . . 10
|
32 | 12, 31 | cfv 5888 |
. . . . . . . . 9
|
33 | | cfz 12326 |
. . . . . . . . 9
|
34 | 30, 32, 33 | co 6650 |
. . . . . . . 8
|
35 | 29, 13, 34 | wral 2912 |
. . . . . . 7
splice |
36 | 35, 11, 7 | wral 2912 |
. . . . . 6
Word
splice |
37 | 10, 36 | wa 384 |
. . . . 5
Word
Word splice |
38 | 37, 8 | cab 2608 |
. . . 4
Word Word
splice |
39 | 38 | cint 4475 |
. . 3
Word Word
splice |
40 | 2, 3, 39 | cmpt 4729 |
. 2
Word Word
splice |
41 | 1, 40 | wceq 1483 |
1
~FG
Word Word
splice |