Step | Hyp | Ref
| Expression |
1 | | erclwwlkn.w |
. . . . 5
⢠ð = (ð ClWWalksN ðº) |
2 | | erclwwlkn.r |
. . . . 5
⢠⌠=
{âšð¡, ð¢â© ⣠(ð¡ â ð â§ ð¢ â ð â§ âð â (0...ð)ð¡ = (ð¢ cyclShift ð))} |
3 | 1, 2 | eclclwwlkn1 29872 |
. . . 4
⢠(ð â (ð / ⌠) â (ð â (ð / ⌠) â
âð¥ â ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)})) |
4 | | rabeq 3441 |
. . . . . . . . . 10
⢠(ð = (ð ClWWalksN ðº) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
5 | 1, 4 | mp1i 13 |
. . . . . . . . 9
⢠((ð â â â§ ð¥ â ð) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
6 | | prmnn 16636 |
. . . . . . . . . . 11
⢠(ð â â â ð â
â) |
7 | 6 | nnnn0d 12554 |
. . . . . . . . . 10
⢠(ð â â â ð â
â0) |
8 | 1 | eleq2i 2820 |
. . . . . . . . . . 11
⢠(ð¥ â ð â ð¥ â (ð ClWWalksN ðº)) |
9 | 8 | biimpi 215 |
. . . . . . . . . 10
⢠(ð¥ â ð â ð¥ â (ð ClWWalksN ðº)) |
10 | | clwwlknscsh 29859 |
. . . . . . . . . 10
⢠((ð â â0
â§ ð¥ â (ð ClWWalksN ðº)) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
11 | 7, 9, 10 | syl2an 595 |
. . . . . . . . 9
⢠((ð â â â§ ð¥ â ð) â {ðŠ â (ð ClWWalksN ðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
12 | 5, 11 | eqtrd 2767 |
. . . . . . . 8
⢠((ð â â â§ ð¥ â ð) â {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)}) |
13 | 12 | eqeq2d 2738 |
. . . . . . 7
⢠((ð â â â§ ð¥ â ð) â (ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)})) |
14 | | simpll 766 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â ð¥ â Word (Vtxâðº)) |
15 | | elnnne0 12508 |
. . . . . . . . . . . . . . . . . 18
⢠(ð â â â (ð â â0
â§ ð â
0)) |
16 | | eqeq1 2731 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð = (â¯âð¥) â (ð = 0 â (â¯âð¥) = 0)) |
17 | 16 | eqcoms 2735 |
. . . . . . . . . . . . . . . . . . . . 21
â¢
((â¯âð¥) =
ð â (ð = 0 â (â¯âð¥) = 0)) |
18 | | hasheq0 14346 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ð¥ â Word (Vtxâðº) â ((â¯âð¥) = 0 â ð¥ = â
)) |
19 | 17, 18 | sylan9bbr 510 |
. . . . . . . . . . . . . . . . . . . 20
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â (ð = 0 â ð¥ = â
)) |
20 | 19 | necon3bid 2980 |
. . . . . . . . . . . . . . . . . . 19
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â (ð â 0 â ð¥ â â
)) |
21 | 20 | biimpcd 248 |
. . . . . . . . . . . . . . . . . 18
⢠(ð â 0 â ((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â ð¥ â â
)) |
22 | 15, 21 | simplbiim 504 |
. . . . . . . . . . . . . . . . 17
⢠(ð â â â ((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â ð¥ â â
)) |
23 | 22 | impcom 407 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â ð¥ â â
) |
24 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â (â¯âð¥) = ð) |
25 | 24 | eqcomd 2733 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â ð = (â¯âð¥)) |
26 | 14, 23, 25 | 3jca 1126 |
. . . . . . . . . . . . . . 15
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â§ ð â â) â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥))) |
27 | 26 | ex 412 |
. . . . . . . . . . . . . 14
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â (ð â â â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥)))) |
28 | | eqid 2727 |
. . . . . . . . . . . . . . 15
â¢
(Vtxâðº) =
(Vtxâðº) |
29 | 28 | clwwlknbp 29832 |
. . . . . . . . . . . . . 14
⢠(ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð)) |
30 | 27, 29 | syl11 33 |
. . . . . . . . . . . . 13
⢠(ð â â â (ð¥ â (ð ClWWalksN ðº) â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥)))) |
31 | 8, 30 | biimtrid 241 |
. . . . . . . . . . . 12
⢠(ð â â â (ð¥ â ð â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥)))) |
32 | 6, 31 | syl 17 |
. . . . . . . . . . 11
⢠(ð â â â (ð¥ â ð â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥)))) |
33 | 32 | imp 406 |
. . . . . . . . . 10
⢠((ð â â â§ ð¥ â ð) â (ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥))) |
34 | | scshwfzeqfzo 14801 |
. . . . . . . . . 10
⢠((ð¥ â Word (Vtxâðº) â§ ð¥ â â
â§ ð = (â¯âð¥)) â {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)}) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⢠((ð â â â§ ð¥ â ð) â {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)}) |
36 | 35 | eqeq2d 2738 |
. . . . . . . 8
⢠((ð â â â§ ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)})) |
37 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . . . . . 23
⢠(ð = ð â (ð¥ cyclShift ð) = (ð¥ cyclShift ð)) |
38 | 37 | eqeq2d 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ð = ð â (ðŠ = (ð¥ cyclShift ð) â ðŠ = (ð¥ cyclShift ð))) |
39 | 38 | cbvrexvw 3230 |
. . . . . . . . . . . . . . . . . . . . 21
â¢
(âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)) |
40 | | eqeq1 2731 |
. . . . . . . . . . . . . . . . . . . . . . 23
⢠(ðŠ = ð¢ â (ðŠ = (ð¥ cyclShift ð) â ð¢ = (ð¥ cyclShift ð))) |
41 | | eqcom 2734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⢠(ð¢ = (ð¥ cyclShift ð) â (ð¥ cyclShift ð) = ð¢) |
42 | 40, 41 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . 22
⢠(ðŠ = ð¢ â (ðŠ = (ð¥ cyclShift ð) â (ð¥ cyclShift ð) = ð¢)) |
43 | 42 | rexbidv 3173 |
. . . . . . . . . . . . . . . . . . . . 21
⢠(ðŠ = ð¢ â (âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢)) |
44 | 39, 43 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . 20
⢠(ðŠ = ð¢ â (âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢)) |
45 | 44 | cbvrabv 3437 |
. . . . . . . . . . . . . . . . . . 19
⢠{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} = {ð¢ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))(ð¥ cyclShift ð) = ð¢} |
46 | 45 | cshwshash 17065 |
. . . . . . . . . . . . . . . . . 18
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) â â) â
((â¯â{ðŠ â
Word (Vtxâðº) â£
âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥) âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1)) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) â â) â§ ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â ((â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥) âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1)) |
48 | 47 | orcomd 870 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) â â) â§ ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â ((â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1 âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥))) |
49 | | fveqeq2 6900 |
. . . . . . . . . . . . . . . . . 18
⢠(ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 â (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1)) |
50 | | fveqeq2 6900 |
. . . . . . . . . . . . . . . . . 18
⢠(ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = (â¯âð¥) â (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥))) |
51 | 49, 50 | orbi12d 917 |
. . . . . . . . . . . . . . . . 17
⢠(ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â (((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)) â ((â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1 âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥)))) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . 16
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) â â) â§ ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â (((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)) â ((â¯â{ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = 1 âš (â¯â{ðŠ â Word (Vtxâðº) ⣠âð â
(0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) = (â¯âð¥)))) |
53 | 48, 52 | mpbird 257 |
. . . . . . . . . . . . . . 15
⢠(((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) â â) â§ ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥))) |
54 | 53 | ex 412 |
. . . . . . . . . . . . . 14
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) â â) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))) |
55 | 54 | ex 412 |
. . . . . . . . . . . . 13
⢠(ð¥ â Word (Vtxâðº) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥))))) |
56 | 55 | adantr 480 |
. . . . . . . . . . . 12
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥))))) |
57 | | eleq1 2816 |
. . . . . . . . . . . . . . 15
⢠(ð = (â¯âð¥) â (ð â â â (â¯âð¥) â
â)) |
58 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . 19
⢠(ð = (â¯âð¥) â (0..^ð) = (0..^(â¯âð¥))) |
59 | 58 | rexeqdv 3321 |
. . . . . . . . . . . . . . . . . 18
⢠(ð = (â¯âð¥) â (âð â (0..^ð)ðŠ = (ð¥ cyclShift ð) â âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð))) |
60 | 59 | rabbidv 3435 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)}) |
61 | 60 | eqeq2d 2738 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)})) |
62 | | eqeq2 2739 |
. . . . . . . . . . . . . . . . 17
⢠(ð = (â¯âð¥) â ((â¯âð) = ð â (â¯âð) = (â¯âð¥))) |
63 | 62 | orbi2d 914 |
. . . . . . . . . . . . . . . 16
⢠(ð = (â¯âð¥) â (((â¯âð) = 1 âš (â¯âð) = ð) â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))) |
64 | 61, 63 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⢠(ð = (â¯âð¥) â ((ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð)) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥))))) |
65 | 57, 64 | imbi12d 344 |
. . . . . . . . . . . . . 14
⢠(ð = (â¯âð¥) â ((ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))))) |
66 | 65 | eqcoms 2735 |
. . . . . . . . . . . . 13
â¢
((â¯âð¥) =
ð â ((ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))))) |
67 | 66 | adantl 481 |
. . . . . . . . . . . 12
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â ((ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) â ((â¯âð¥) â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^(â¯âð¥))ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = (â¯âð¥)))))) |
68 | 56, 67 | mpbird 257 |
. . . . . . . . . . 11
⢠((ð¥ â Word (Vtxâðº) â§ (â¯âð¥) = ð) â (ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð)))) |
69 | 29, 68 | syl 17 |
. . . . . . . . . 10
⢠(ð¥ â (ð ClWWalksN ðº) â (ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð)))) |
70 | 69, 1 | eleq2s 2846 |
. . . . . . . . 9
⢠(ð¥ â ð â (ð â â â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð)))) |
71 | 70 | impcom 407 |
. . . . . . . 8
⢠((ð â â â§ ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0..^ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) |
72 | 36, 71 | sylbid 239 |
. . . . . . 7
⢠((ð â â â§ ð¥ â ð) â (ð = {ðŠ â Word (Vtxâðº) ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) |
73 | 13, 72 | sylbid 239 |
. . . . . 6
⢠((ð â â â§ ð¥ â ð) â (ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) |
74 | 73 | rexlimdva 3150 |
. . . . 5
⢠(ð â â â
(âð¥ â ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â ((â¯âð) = 1 âš (â¯âð) = ð))) |
75 | 74 | com12 32 |
. . . 4
â¢
(âð¥ â
ð ð = {ðŠ â ð ⣠âð â (0...ð)ðŠ = (ð¥ cyclShift ð)} â (ð â â â ((â¯âð) = 1 âš (â¯âð) = ð))) |
76 | 3, 75 | biimtrdi 252 |
. . 3
⢠(ð â (ð / ⌠) â (ð â (ð / ⌠) â (ð â â â
((â¯âð) = 1 âš
(â¯âð) = ð)))) |
77 | 76 | pm2.43i 52 |
. 2
⢠(ð â (ð / ⌠) â (ð â â â
((â¯âð) = 1 âš
(â¯âð) = ð))) |
78 | 77 | impcom 407 |
1
⢠((ð â â â§ ð â (ð / ⌠)) â
((â¯âð) = 1 âš
(â¯âð) = ð)) |