Step | Hyp | Ref
| Expression |
1 | | preaddccan2lem1 4454 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn ![{](lbrace.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif) ![)](rp.gif) ![_V](rmcv.gif) ![)](rp.gif) |
2 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) ![N](_cn.gif)
0c
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
3 | 2 | neeq1d 2529 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
0c ![N](_cn.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) ![P](_cp.gif)
0c
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 2, 4 | eqeq12d 2367 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif) 0c ![N](_cn.gif)
0c
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 3, 5 | anbi12d 691 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![(](lp.gif) 0c ![N](_cn.gif)
0c ![N](_cn.gif)
0c ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 6 | imbi1d 308 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif)
![(](lp.gif) ![(](lp.gif) 0c ![N](_cn.gif) 0c ![N](_cn.gif)
0c ![P](_cp.gif) ![)](rp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | neeq1d 2529 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 8, 10 | eqeq12d 2367 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 9, 11 | anbi12d 691 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | imbi1d 308 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | addceq1 4383 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![(](lp.gif) 1c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
15 | | addc32 4416 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c
![N](_cn.gif)
![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c![)](rp.gif) |
16 | 14, 15 | syl6eq 2401 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c![)](rp.gif) ![)](rp.gif) |
17 | 16 | neeq1d 2529 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | addceq1 4383 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![P](_cp.gif)
![(](lp.gif) ![(](lp.gif) 1c ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | addc32 4416 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c
![P](_cp.gif)
![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) |
20 | 18, 19 | syl6eq 2401 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![P](_cp.gif)
![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) |
21 | 16, 20 | eqeq12d 2367 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c
![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 17, 21 | anbi12d 691 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | imbi1d 308 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif)
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | neeq1d 2529 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 24, 26 | eqeq12d 2367 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 25, 27 | anbi12d 691 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 28 | imbi1d 308 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | addcid2 4407 |
. . . . . . . . 9
0c ![N](_cn.gif)
![N](_cn.gif) |
31 | | addcid2 4407 |
. . . . . . . . 9
0c ![P](_cp.gif)
![P](_cp.gif) |
32 | 30, 31 | eqeq12i 2366 |
. . . . . . . 8
![(](lp.gif) 0c ![N](_cn.gif) 0c ![P](_cp.gif) ![P](_cp.gif) ![)](rp.gif) |
33 | 32 | biimpi 186 |
. . . . . . 7
![(](lp.gif) 0c ![N](_cn.gif) 0c ![P](_cp.gif) ![P](_cp.gif) ![)](rp.gif) |
34 | 33 | adantl 452 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 0c ![N](_cn.gif) 0c ![N](_cn.gif)
0c ![P](_cp.gif) ![)](rp.gif) ![P](_cp.gif) ![)](rp.gif) |
35 | 34 | a1i 10 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) 0c ![N](_cn.gif) 0c ![N](_cn.gif)
0c ![P](_cp.gif) ![)](rp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | addcnnul 4453 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | simpld 445 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![N](_cn.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
38 | 37 | ad2antrl 708 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![N](_cn.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
39 | | simpll 730 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) |
40 | | simplrl 736 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) |
41 | | nncaddccl 4419 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![N](_cn.gif) Nn ![)](rp.gif) |
42 | 39, 40, 41 | syl2anc 642 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![N](_cn.gif) Nn ![)](rp.gif) |
43 | | simplrr 737 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) |
44 | | nncaddccl 4419 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![P](_cp.gif) Nn ![)](rp.gif) |
45 | 39, 43, 44 | syl2anc 642 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![P](_cp.gif) Nn ![)](rp.gif) |
46 | | simprr 733 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) |
47 | | simprl 732 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
48 | | prepeano4 4451 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
Nn ![(](lp.gif) ![P](_cp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 42, 45, 46, 47, 48 | syl22anc 1183 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 38, 49 | jca 518 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 50 | ex 423 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
1c
![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 51 | imim1d 69 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
1c
![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) 1c ![(](lp.gif) ![(](lp.gif) ![P](_cp.gif) 1c![)](rp.gif)
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 1, 7, 13, 23, 29, 35, 52 | findsd 4410 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | 53 | 3impb 1147 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif)
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 54 | expdimp 426 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![N](_cn.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif)
![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
56 | | addceq2 4384 |
. 2
![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![(](lp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 55, 56 | impbid1 194 |
1
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![N](_cn.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![(](lp.gif) ![P](_cp.gif) ![P](_cp.gif) ![)](rp.gif) ![)](rp.gif) |