Step | Hyp | Ref
| Expression |
1 | | efgredlemd.c |
. . . . . 6
β’ (π β πΆ β dom π) |
2 | | efgval.w |
. . . . . . . . 9
β’ π = ( I βWord (πΌ Γ
2o)) |
3 | | efgval.r |
. . . . . . . . 9
β’ βΌ = (
~FG βπΌ) |
4 | | efgval2.m |
. . . . . . . . 9
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
5 | | efgval2.t |
. . . . . . . . 9
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
6 | | efgred.d |
. . . . . . . . 9
β’ π· = (π β βͺ
π₯ β π ran (πβπ₯)) |
7 | | efgred.s |
. . . . . . . . 9
β’ π = (π β {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} β¦ (πβ((β―βπ) β 1))) |
8 | 2, 3, 4, 5, 6, 7 | efgsf 19597 |
. . . . . . . 8
β’ π:{π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))}βΆπ |
9 | 8 | fdmi 6730 |
. . . . . . . . 9
β’ dom π = {π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))} |
10 | 9 | feq2i 6710 |
. . . . . . . 8
β’ (π:dom πβΆπ β π:{π‘ β (Word π β {β
}) β£ ((π‘β0) β π· β§ βπ β
(1..^(β―βπ‘))(π‘βπ) β ran (πβ(π‘β(π β 1))))}βΆπ) |
11 | 8, 10 | mpbir 230 |
. . . . . . 7
β’ π:dom πβΆπ |
12 | 11 | ffvelcdmi 7086 |
. . . . . 6
β’ (πΆ β dom π β (πβπΆ) β π) |
13 | 1, 12 | syl 17 |
. . . . 5
β’ (π β (πβπΆ) β π) |
14 | | efgredlemb.q |
. . . . . . 7
β’ (π β π β (0...(β―β(π΅βπΏ)))) |
15 | | elfzuz 13497 |
. . . . . . 7
β’ (π β
(0...(β―β(π΅βπΏ))) β π β
(β€β₯β0)) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ (π β π β
(β€β₯β0)) |
17 | | efgredlemd.sc |
. . . . . . . . . 10
β’ (π β (πβπΆ) = (((π΅βπΏ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) |
18 | 17 | fveq2d 6896 |
. . . . . . . . 9
β’ (π β (β―β(πβπΆ)) = (β―β(((π΅βπΏ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)))) |
19 | | fviss 6969 |
. . . . . . . . . . . . 13
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
20 | 2, 19 | eqsstri 4017 |
. . . . . . . . . . . 12
β’ π β Word (πΌ Γ 2o) |
21 | | efgredlem.1 |
. . . . . . . . . . . . . 14
β’ (π β βπ β dom πβπ β dom π((β―β(πβπ)) < (β―β(πβπ΄)) β ((πβπ) = (πβπ) β (πβ0) = (πβ0)))) |
22 | | efgredlem.2 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β dom π) |
23 | | efgredlem.3 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β dom π) |
24 | | efgredlem.4 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ΄) = (πβπ΅)) |
25 | | efgredlem.5 |
. . . . . . . . . . . . . 14
β’ (π β Β¬ (π΄β0) = (π΅β0)) |
26 | | efgredlemb.k |
. . . . . . . . . . . . . 14
β’ πΎ = (((β―βπ΄) β 1) β
1) |
27 | | efgredlemb.l |
. . . . . . . . . . . . . 14
β’ πΏ = (((β―βπ΅) β 1) β
1) |
28 | 2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27 | efgredlemf 19609 |
. . . . . . . . . . . . 13
β’ (π β ((π΄βπΎ) β π β§ (π΅βπΏ) β π)) |
29 | 28 | simprd 497 |
. . . . . . . . . . . 12
β’ (π β (π΅βπΏ) β π) |
30 | 20, 29 | sselid 3981 |
. . . . . . . . . . 11
β’ (π β (π΅βπΏ) β Word (πΌ Γ 2o)) |
31 | | pfxcl 14627 |
. . . . . . . . . . 11
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β ((π΅βπΏ) prefix π) β Word (πΌ Γ 2o)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π΅βπΏ) prefix π) β Word (πΌ Γ 2o)) |
33 | 28 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β (π΄βπΎ) β π) |
34 | 20, 33 | sselid 3981 |
. . . . . . . . . . 11
β’ (π β (π΄βπΎ) β Word (πΌ Γ 2o)) |
35 | | swrdcl 14595 |
. . . . . . . . . . 11
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©) β Word (πΌ Γ 2o)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©) β Word (πΌ Γ 2o)) |
37 | | ccatlen 14525 |
. . . . . . . . . 10
β’ ((((π΅βπΏ) prefix π) β Word (πΌ Γ 2o) β§ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©) β Word (πΌ Γ 2o)) β
(β―β(((π΅βπΏ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) = ((β―β((π΅βπΏ) prefix π)) + (β―β((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)))) |
38 | 32, 36, 37 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (β―β(((π΅βπΏ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) = ((β―β((π΅βπΏ) prefix π)) + (β―β((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)))) |
39 | | pfxlen 14633 |
. . . . . . . . . . . 12
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ π β
(0...(β―β(π΅βπΏ)))) β (β―β((π΅βπΏ) prefix π)) = π) |
40 | 30, 14, 39 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (β―β((π΅βπΏ) prefix π)) = π) |
41 | | 2nn0 12489 |
. . . . . . . . . . . . . 14
β’ 2 β
β0 |
42 | | uzaddcl 12888 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β0) β§ 2 β β0) β
(π + 2) β
(β€β₯β0)) |
43 | 16, 41, 42 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β (π + 2) β
(β€β₯β0)) |
44 | | efgredlemb.p |
. . . . . . . . . . . . . . 15
β’ (π β π β (0...(β―β(π΄βπΎ)))) |
45 | | elfzuz3 13498 |
. . . . . . . . . . . . . . 15
β’ (π β
(0...(β―β(π΄βπΎ))) β (β―β(π΄βπΎ)) β
(β€β₯βπ)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (β―β(π΄βπΎ)) β
(β€β₯βπ)) |
47 | | efgredlemd.9 |
. . . . . . . . . . . . . 14
β’ (π β π β (β€β₯β(π + 2))) |
48 | | uztrn 12840 |
. . . . . . . . . . . . . 14
β’
(((β―β(π΄βπΎ)) β
(β€β₯βπ) β§ π β (β€β₯β(π + 2))) β
(β―β(π΄βπΎ)) β
(β€β₯β(π + 2))) |
49 | 46, 47, 48 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (β―β(π΄βπΎ)) β
(β€β₯β(π + 2))) |
50 | | elfzuzb 13495 |
. . . . . . . . . . . . 13
β’ ((π + 2) β
(0...(β―β(π΄βπΎ))) β ((π + 2) β
(β€β₯β0) β§ (β―β(π΄βπΎ)) β
(β€β₯β(π + 2)))) |
51 | 43, 49, 50 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ (π β (π + 2) β (0...(β―β(π΄βπΎ)))) |
52 | | lencl 14483 |
. . . . . . . . . . . . . . 15
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β
(β―β(π΄βπΎ)) β
β0) |
53 | 34, 52 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (β―β(π΄βπΎ)) β
β0) |
54 | | nn0uz 12864 |
. . . . . . . . . . . . . 14
β’
β0 = (β€β₯β0) |
55 | 53, 54 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
β’ (π β (β―β(π΄βπΎ)) β
(β€β₯β0)) |
56 | | eluzfz2 13509 |
. . . . . . . . . . . . 13
β’
((β―β(π΄βπΎ)) β (β€β₯β0)
β (β―β(π΄βπΎ)) β (0...(β―β(π΄βπΎ)))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (β―β(π΄βπΎ)) β (0...(β―β(π΄βπΎ)))) |
58 | | swrdlen 14597 |
. . . . . . . . . . . 12
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ (π + 2) β
(0...(β―β(π΄βπΎ))) β§ (β―β(π΄βπΎ)) β (0...(β―β(π΄βπΎ)))) β (β―β((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = ((β―β(π΄βπΎ)) β (π + 2))) |
59 | 34, 51, 57, 58 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (β―β((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = ((β―β(π΄βπΎ)) β (π + 2))) |
60 | 40, 59 | oveq12d 7427 |
. . . . . . . . . 10
β’ (π β ((β―β((π΅βπΏ) prefix π)) + (β―β((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) = (π + ((β―β(π΄βπΎ)) β (π + 2)))) |
61 | 14 | elfzelzd 13502 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
62 | 61 | zcnd 12667 |
. . . . . . . . . . 11
β’ (π β π β β) |
63 | 53 | nn0cnd 12534 |
. . . . . . . . . . 11
β’ (π β (β―β(π΄βπΎ)) β β) |
64 | | 2z 12594 |
. . . . . . . . . . . . 13
β’ 2 β
β€ |
65 | | zaddcl 12602 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ 2 β
β€) β (π + 2)
β β€) |
66 | 61, 64, 65 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β (π + 2) β β€) |
67 | 66 | zcnd 12667 |
. . . . . . . . . . 11
β’ (π β (π + 2) β β) |
68 | 62, 63, 67 | addsubassd 11591 |
. . . . . . . . . 10
β’ (π β ((π + (β―β(π΄βπΎ))) β (π + 2)) = (π + ((β―β(π΄βπΎ)) β (π + 2)))) |
69 | | 2cn 12287 |
. . . . . . . . . . . 12
β’ 2 β
β |
70 | 69 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 2 β
β) |
71 | 62, 63, 70 | pnpcand 11608 |
. . . . . . . . . 10
β’ (π β ((π + (β―β(π΄βπΎ))) β (π + 2)) = ((β―β(π΄βπΎ)) β 2)) |
72 | 60, 68, 71 | 3eqtr2d 2779 |
. . . . . . . . 9
β’ (π β ((β―β((π΅βπΏ) prefix π)) + (β―β((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) = ((β―β(π΄βπΎ)) β 2)) |
73 | 18, 38, 72 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β (β―β(πβπΆ)) = ((β―β(π΄βπΎ)) β 2)) |
74 | 44 | elfzelzd 13502 |
. . . . . . . . . 10
β’ (π β π β β€) |
75 | | zsubcl 12604 |
. . . . . . . . . 10
β’ ((π β β€ β§ 2 β
β€) β (π β
2) β β€) |
76 | 74, 64, 75 | sylancl 587 |
. . . . . . . . 9
β’ (π β (π β 2) β β€) |
77 | 64 | a1i 11 |
. . . . . . . . 9
β’ (π β 2 β
β€) |
78 | 74 | zcnd 12667 |
. . . . . . . . . . . 12
β’ (π β π β β) |
79 | | npcan 11469 |
. . . . . . . . . . . 12
β’ ((π β β β§ 2 β
β) β ((π β
2) + 2) = π) |
80 | 78, 69, 79 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β ((π β 2) + 2) = π) |
81 | 80 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π β
(β€β₯β((π β 2) + 2)) =
(β€β₯βπ)) |
82 | 46, 81 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (π β (β―β(π΄βπΎ)) β
(β€β₯β((π β 2) + 2))) |
83 | | eluzsub 12852 |
. . . . . . . . 9
β’ (((π β 2) β β€ β§
2 β β€ β§ (β―β(π΄βπΎ)) β
(β€β₯β((π β 2) + 2))) β
((β―β(π΄βπΎ)) β 2) β
(β€β₯β(π β 2))) |
84 | 76, 77, 82, 83 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((β―β(π΄βπΎ)) β 2) β
(β€β₯β(π β 2))) |
85 | 73, 84 | eqeltrd 2834 |
. . . . . . 7
β’ (π β (β―β(πβπΆ)) β
(β€β₯β(π β 2))) |
86 | | eluzsub 12852 |
. . . . . . . 8
β’ ((π β β€ β§ 2 β
β€ β§ π β
(β€β₯β(π + 2))) β (π β 2) β
(β€β₯βπ)) |
87 | 61, 77, 47, 86 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π β 2) β
(β€β₯βπ)) |
88 | | uztrn 12840 |
. . . . . . 7
β’
(((β―β(πβπΆ)) β
(β€β₯β(π β 2)) β§ (π β 2) β
(β€β₯βπ)) β (β―β(πβπΆ)) β
(β€β₯βπ)) |
89 | 85, 87, 88 | syl2anc 585 |
. . . . . 6
β’ (π β (β―β(πβπΆ)) β
(β€β₯βπ)) |
90 | | elfzuzb 13495 |
. . . . . 6
β’ (π β
(0...(β―β(πβπΆ))) β (π β (β€β₯β0)
β§ (β―β(πβπΆ)) β
(β€β₯βπ))) |
91 | 16, 89, 90 | sylanbrc 584 |
. . . . 5
β’ (π β π β (0...(β―β(πβπΆ)))) |
92 | | efgredlemb.v |
. . . . 5
β’ (π β π β (πΌ Γ 2o)) |
93 | 2, 3, 4, 5 | efgtval 19591 |
. . . . 5
β’ (((πβπΆ) β π β§ π β (0...(β―β(πβπΆ))) β§ π β (πΌ Γ 2o)) β (π(πβ(πβπΆ))π) = ((πβπΆ) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
94 | 13, 91, 92, 93 | syl3anc 1372 |
. . . 4
β’ (π β (π(πβ(πβπΆ))π) = ((πβπΆ) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
95 | | pfxcl 14627 |
. . . . . 6
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β ((π΄βπΎ) prefix π) β Word (πΌ Γ 2o)) |
96 | 34, 95 | syl 17 |
. . . . 5
β’ (π β ((π΄βπΎ) prefix π) β Word (πΌ Γ 2o)) |
97 | | wrd0 14489 |
. . . . . 6
β’ β
β Word (πΌ Γ
2o) |
98 | 97 | a1i 11 |
. . . . 5
β’ (π β β
β Word (πΌ Γ
2o)) |
99 | 4 | efgmf 19581 |
. . . . . . . 8
β’ π:(πΌ Γ 2o)βΆ(πΌ Γ
2o) |
100 | 99 | ffvelcdmi 7086 |
. . . . . . 7
β’ (π β (πΌ Γ 2o) β (πβπ) β (πΌ Γ 2o)) |
101 | 92, 100 | syl 17 |
. . . . . 6
β’ (π β (πβπ) β (πΌ Γ 2o)) |
102 | 92, 101 | s2cld 14822 |
. . . . 5
β’ (π β β¨βπ(πβπ)ββ© β Word (πΌ Γ
2o)) |
103 | 61 | zred 12666 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
104 | | nn0addge1 12518 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ 2 β
β0) β π β€ (π + 2)) |
105 | 103, 41, 104 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (π β π β€ (π + 2)) |
106 | | eluz2 12828 |
. . . . . . . . . . . . . . . 16
β’ ((π + 2) β
(β€β₯βπ) β (π β β€ β§ (π + 2) β β€ β§ π β€ (π + 2))) |
107 | 61, 66, 105, 106 | syl3anbrc 1344 |
. . . . . . . . . . . . . . 15
β’ (π β (π + 2) β
(β€β₯βπ)) |
108 | | uztrn 12840 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β(π + 2)) β§ (π + 2) β
(β€β₯βπ)) β π β (β€β₯βπ)) |
109 | 47, 107, 108 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β π β (β€β₯βπ)) |
110 | | elfzuzb 13495 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β (π β (β€β₯β0)
β§ π β
(β€β₯βπ))) |
111 | 16, 109, 110 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (π β π β (0...π)) |
112 | | ccatpfx 14651 |
. . . . . . . . . . . . 13
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ π β (0...π) β§ π β (0...(β―β(π΄βπΎ)))) β (((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, πβ©)) = ((π΄βπΎ) prefix π)) |
113 | 34, 111, 44, 112 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β (((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, πβ©)) = ((π΄βπΎ) prefix π)) |
114 | 113 | oveq1d 7424 |
. . . . . . . . . . 11
β’ (π β ((((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, πβ©)) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΄βπΎ) prefix π) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) |
115 | | pfxcl 14627 |
. . . . . . . . . . . . 13
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β ((π΄βπΎ) prefix π) β Word (πΌ Γ 2o)) |
116 | 34, 115 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((π΄βπΎ) prefix π) β Word (πΌ Γ 2o)) |
117 | | efgredlemb.u |
. . . . . . . . . . . . 13
β’ (π β π β (πΌ Γ 2o)) |
118 | 99 | ffvelcdmi 7086 |
. . . . . . . . . . . . . 14
β’ (π β (πΌ Γ 2o) β (πβπ) β (πΌ Γ 2o)) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (πβπ) β (πΌ Γ 2o)) |
120 | 117, 119 | s2cld 14822 |
. . . . . . . . . . . 12
β’ (π β β¨βπ(πβπ)ββ© β Word (πΌ Γ
2o)) |
121 | | swrdcl 14595 |
. . . . . . . . . . . . 13
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) β Word (πΌ Γ 2o)) |
122 | 34, 121 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) β Word (πΌ Γ 2o)) |
123 | | ccatass 14538 |
. . . . . . . . . . . 12
β’ ((((π΄βπΎ) prefix π) β Word (πΌ Γ 2o) β§
β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β§
((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) β Word (πΌ Γ 2o)) β ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = (((π΄βπΎ) prefix π) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) |
124 | 116, 120,
122, 123 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = (((π΄βπΎ) prefix π) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) |
125 | | efgredlemb.6 |
. . . . . . . . . . . . 13
β’ (π β (πβπ΄) = (π(πβ(π΄βπΎ))π)) |
126 | 2, 3, 4, 5 | efgtval 19591 |
. . . . . . . . . . . . . 14
β’ (((π΄βπΎ) β π β§ π β (0...(β―β(π΄βπΎ))) β§ π β (πΌ Γ 2o)) β (π(πβ(π΄βπΎ))π) = ((π΄βπΎ) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
127 | 33, 44, 117, 126 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (π(πβ(π΄βπΎ))π) = ((π΄βπΎ) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
128 | | splval 14701 |
. . . . . . . . . . . . . 14
β’ (((π΄βπΎ) β π β§ (π β (0...(β―β(π΄βπΎ))) β§ π β (0...(β―β(π΄βπΎ))) β§ β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o))) β
((π΄βπΎ) splice β¨π, π, β¨βπ(πβπ)ββ©β©) = ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) |
129 | 33, 44, 44, 120, 128 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ (π β ((π΄βπΎ) splice β¨π, π, β¨βπ(πβπ)ββ©β©) = ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) |
130 | 125, 127,
129 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β (πβπ΄) = ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) |
131 | | efgredlemb.7 |
. . . . . . . . . . . . 13
β’ (π β (πβπ΅) = (π(πβ(π΅βπΏ))π)) |
132 | 2, 3, 4, 5 | efgtval 19591 |
. . . . . . . . . . . . . 14
β’ (((π΅βπΏ) β π β§ π β (0...(β―β(π΅βπΏ))) β§ π β (πΌ Γ 2o)) β (π(πβ(π΅βπΏ))π) = ((π΅βπΏ) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
133 | 29, 14, 92, 132 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (π(πβ(π΅βπΏ))π) = ((π΅βπΏ) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) |
134 | | splval 14701 |
. . . . . . . . . . . . . 14
β’ (((π΅βπΏ) β π β§ (π β (0...(β―β(π΅βπΏ))) β§ π β (0...(β―β(π΅βπΏ))) β§ β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o))) β
((π΅βπΏ) splice β¨π, π, β¨βπ(πβπ)ββ©β©) = ((((π΅βπΏ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
135 | 29, 14, 14, 102, 134 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ (π β ((π΅βπΏ) splice β¨π, π, β¨βπ(πβπ)ββ©β©) = ((((π΅βπΏ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
136 | 131, 133,
135 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β (πβπ΅) = ((((π΅βπΏ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
137 | 24, 130, 136 | 3eqtr3d 2781 |
. . . . . . . . . . 11
β’ (π β ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = ((((π΅βπΏ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
138 | 114, 124,
137 | 3eqtr2d 2779 |
. . . . . . . . . 10
β’ (π β ((((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, πβ©)) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = ((((π΅βπΏ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
139 | | swrdcl 14595 |
. . . . . . . . . . . 12
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β ((π΄βπΎ) substr β¨π, πβ©) β Word (πΌ Γ 2o)) |
140 | 34, 139 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((π΄βπΎ) substr β¨π, πβ©) β Word (πΌ Γ 2o)) |
141 | | ccatcl 14524 |
. . . . . . . . . . . 12
β’
((β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β§
((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) β Word (πΌ Γ 2o)) β
(β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) β Word (πΌ Γ 2o)) |
142 | 120, 122,
141 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) β Word (πΌ Γ 2o)) |
143 | | ccatass 14538 |
. . . . . . . . . . 11
β’ ((((π΄βπΎ) prefix π) β Word (πΌ Γ 2o) β§ ((π΄βπΎ) substr β¨π, πβ©) β Word (πΌ Γ 2o) β§
(β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) β Word (πΌ Γ 2o)) β ((((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, πβ©)) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΄βπΎ) prefix π) ++ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))))) |
144 | 96, 140, 142, 143 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, πβ©)) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΄βπΎ) prefix π) ++ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))))) |
145 | | swrdcl 14595 |
. . . . . . . . . . . 12
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) |
146 | 30, 145 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) |
147 | | ccatass 14538 |
. . . . . . . . . . 11
β’ ((((π΅βπΏ) prefix π) β Word (πΌ Γ 2o) β§
β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β§
((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) β ((((π΅βπΏ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = (((π΅βπΏ) prefix π) ++ (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
148 | 32, 102, 146, 147 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((((π΅βπΏ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = (((π΅βπΏ) prefix π) ++ (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
149 | 138, 144,
148 | 3eqtr3d 2781 |
. . . . . . . . 9
β’ (π β (((π΄βπΎ) prefix π) ++ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) = (((π΅βπΏ) prefix π) ++ (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
150 | | ccatcl 14524 |
. . . . . . . . . . 11
β’ ((((π΄βπΎ) substr β¨π, πβ©) β Word (πΌ Γ 2o) β§
(β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) β Word (πΌ Γ 2o)) β (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) β Word (πΌ Γ 2o)) |
151 | 140, 142,
150 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) β Word (πΌ Γ 2o)) |
152 | | ccatcl 14524 |
. . . . . . . . . . 11
β’
((β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β§
((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) β
(β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) β Word (πΌ Γ 2o)) |
153 | 102, 146,
152 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) β Word (πΌ Γ 2o)) |
154 | | uztrn 12840 |
. . . . . . . . . . . . . 14
β’
(((β―β(π΄βπΎ)) β
(β€β₯βπ) β§ π β (β€β₯βπ)) β (β―β(π΄βπΎ)) β
(β€β₯βπ)) |
155 | 46, 109, 154 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (β―β(π΄βπΎ)) β
(β€β₯βπ)) |
156 | | elfzuzb 13495 |
. . . . . . . . . . . . 13
β’ (π β
(0...(β―β(π΄βπΎ))) β (π β (β€β₯β0)
β§ (β―β(π΄βπΎ)) β
(β€β₯βπ))) |
157 | 16, 155, 156 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ (π β π β (0...(β―β(π΄βπΎ)))) |
158 | | pfxlen 14633 |
. . . . . . . . . . . 12
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ π β
(0...(β―β(π΄βπΎ)))) β (β―β((π΄βπΎ) prefix π)) = π) |
159 | 34, 157, 158 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (β―β((π΄βπΎ) prefix π)) = π) |
160 | 159, 40 | eqtr4d 2776 |
. . . . . . . . . 10
β’ (π β (β―β((π΄βπΎ) prefix π)) = (β―β((π΅βπΏ) prefix π))) |
161 | | ccatopth 14666 |
. . . . . . . . . 10
β’
(((((π΄βπΎ) prefix π) β Word (πΌ Γ 2o) β§ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) β Word (πΌ Γ 2o)) β§ (((π΅βπΏ) prefix π) β Word (πΌ Γ 2o) β§
(β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) β Word (πΌ Γ 2o)) β§
(β―β((π΄βπΎ) prefix π)) = (β―β((π΅βπΏ) prefix π))) β ((((π΄βπΎ) prefix π) ++ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) = (((π΅βπΏ) prefix π) ++ (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) β (((π΄βπΎ) prefix π) = ((π΅βπΏ) prefix π) β§ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))))) |
162 | 96, 151, 32, 153, 160, 161 | syl221anc 1382 |
. . . . . . . . 9
β’ (π β ((((π΄βπΎ) prefix π) ++ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) = (((π΅βπΏ) prefix π) ++ (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) β (((π΄βπΎ) prefix π) = ((π΅βπΏ) prefix π) β§ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))))) |
163 | 149, 162 | mpbid 231 |
. . . . . . . 8
β’ (π β (((π΄βπΎ) prefix π) = ((π΅βπΏ) prefix π) β§ (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
164 | 163 | simpld 496 |
. . . . . . 7
β’ (π β ((π΄βπΎ) prefix π) = ((π΅βπΏ) prefix π)) |
165 | 164 | oveq1d 7424 |
. . . . . 6
β’ (π β (((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = (((π΅βπΏ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) |
166 | | ccatrid 14537 |
. . . . . . . 8
β’ (((π΄βπΎ) prefix π) β Word (πΌ Γ 2o) β (((π΄βπΎ) prefix π) ++ β
) = ((π΄βπΎ) prefix π)) |
167 | 96, 166 | syl 17 |
. . . . . . 7
β’ (π β (((π΄βπΎ) prefix π) ++ β
) = ((π΄βπΎ) prefix π)) |
168 | 167 | oveq1d 7424 |
. . . . . 6
β’ (π β ((((π΄βπΎ) prefix π) ++ β
) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = (((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) |
169 | 165, 168,
17 | 3eqtr4rd 2784 |
. . . . 5
β’ (π β (πβπΆ) = ((((π΄βπΎ) prefix π) ++ β
) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) |
170 | 159 | eqcomd 2739 |
. . . . 5
β’ (π β π = (β―β((π΄βπΎ) prefix π))) |
171 | | hash0 14327 |
. . . . . . 7
β’
(β―ββ
) = 0 |
172 | 171 | oveq2i 7420 |
. . . . . 6
β’ (π + (β―ββ
)) =
(π + 0) |
173 | 62 | addridd 11414 |
. . . . . 6
β’ (π β (π + 0) = π) |
174 | 172, 173 | eqtr2id 2786 |
. . . . 5
β’ (π β π = (π +
(β―ββ
))) |
175 | 96, 98, 36, 102, 169, 170, 174 | splval2 14707 |
. . . 4
β’ (π β ((πβπΆ) splice β¨π, π, β¨βπ(πβπ)ββ©β©) = ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) |
176 | | elfzuzb 13495 |
. . . . . . . . . . . . . 14
β’ (π β (0...(π + 2)) β (π β (β€β₯β0)
β§ (π + 2) β
(β€β₯βπ))) |
177 | 16, 107, 176 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (π β π β (0...(π + 2))) |
178 | | elfzuzb 13495 |
. . . . . . . . . . . . . 14
β’ ((π + 2) β (0...π) β ((π + 2) β
(β€β₯β0) β§ π β (β€β₯β(π + 2)))) |
179 | 43, 47, 178 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (π β (π + 2) β (0...π)) |
180 | | ccatswrd 14618 |
. . . . . . . . . . . . 13
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ (π β (0...(π + 2)) β§ (π + 2) β (0...π) β§ π β (0...(β―β(π΄βπΎ))))) β (((π΄βπΎ) substr β¨π, (π + 2)β©) ++ ((π΄βπΎ) substr β¨(π + 2), πβ©)) = ((π΄βπΎ) substr β¨π, πβ©)) |
181 | 34, 177, 179, 44, 180 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ (π β (((π΄βπΎ) substr β¨π, (π + 2)β©) ++ ((π΄βπΎ) substr β¨(π + 2), πβ©)) = ((π΄βπΎ) substr β¨π, πβ©)) |
182 | 181 | oveq1d 7424 |
. . . . . . . . . . 11
β’ (π β ((((π΄βπΎ) substr β¨π, (π + 2)β©) ++ ((π΄βπΎ) substr β¨(π + 2), πβ©)) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) |
183 | | swrdcl 14595 |
. . . . . . . . . . . . 13
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β ((π΄βπΎ) substr β¨π, (π + 2)β©) β Word (πΌ Γ 2o)) |
184 | 34, 183 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((π΄βπΎ) substr β¨π, (π + 2)β©) β Word (πΌ Γ 2o)) |
185 | | swrdcl 14595 |
. . . . . . . . . . . . 13
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β ((π΄βπΎ) substr β¨(π + 2), πβ©) β Word (πΌ Γ 2o)) |
186 | 34, 185 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((π΄βπΎ) substr β¨(π + 2), πβ©) β Word (πΌ Γ 2o)) |
187 | | ccatass 14538 |
. . . . . . . . . . . 12
β’ ((((π΄βπΎ) substr β¨π, (π + 2)β©) β Word (πΌ Γ 2o) β§ ((π΄βπΎ) substr β¨(π + 2), πβ©) β Word (πΌ Γ 2o) β§
(β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) β Word (πΌ Γ 2o)) β ((((π΄βπΎ) substr β¨π, (π + 2)β©) ++ ((π΄βπΎ) substr β¨(π + 2), πβ©)) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΄βπΎ) substr β¨π, (π + 2)β©) ++ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))))) |
188 | 184, 186,
142, 187 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β ((((π΄βπΎ) substr β¨π, (π + 2)β©) ++ ((π΄βπΎ) substr β¨(π + 2), πβ©)) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΄βπΎ) substr β¨π, (π + 2)β©) ++ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))))) |
189 | 163 | simprd 497 |
. . . . . . . . . . 11
β’ (π β (((π΄βπΎ) substr β¨π, πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
190 | 182, 188,
189 | 3eqtr3d 2781 |
. . . . . . . . . 10
β’ (π β (((π΄βπΎ) substr β¨π, (π + 2)β©) ++ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) = (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
191 | | ccatcl 14524 |
. . . . . . . . . . . 12
β’ ((((π΄βπΎ) substr β¨(π + 2), πβ©) β Word (πΌ Γ 2o) β§
(β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) β Word (πΌ Γ 2o)) β (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) β Word (πΌ Γ 2o)) |
192 | 186, 142,
191 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) β Word (πΌ Γ 2o)) |
193 | | swrdlen 14597 |
. . . . . . . . . . . . . 14
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ π β (0...(π + 2)) β§ (π + 2) β (0...(β―β(π΄βπΎ)))) β (β―β((π΄βπΎ) substr β¨π, (π + 2)β©)) = ((π + 2) β π)) |
194 | 34, 177, 51, 193 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (β―β((π΄βπΎ) substr β¨π, (π + 2)β©)) = ((π + 2) β π)) |
195 | | pncan2 11467 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ 2 β
β) β ((π + 2)
β π) =
2) |
196 | 62, 69, 195 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β ((π + 2) β π) = 2) |
197 | 194, 196 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β (β―β((π΄βπΎ) substr β¨π, (π + 2)β©)) = 2) |
198 | | s2len 14840 |
. . . . . . . . . . . 12
β’
(β―ββ¨βπ(πβπ)ββ©) = 2 |
199 | 197, 198 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π β (β―β((π΄βπΎ) substr β¨π, (π + 2)β©)) =
(β―ββ¨βπ(πβπ)ββ©)) |
200 | | ccatopth 14666 |
. . . . . . . . . . 11
β’
(((((π΄βπΎ) substr β¨π, (π + 2)β©) β Word (πΌ Γ 2o) β§ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) β Word (πΌ Γ 2o)) β§
(β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β§
((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) β§
(β―β((π΄βπΎ) substr β¨π, (π + 2)β©)) =
(β―ββ¨βπ(πβπ)ββ©)) β ((((π΄βπΎ) substr β¨π, (π + 2)β©) ++ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) = (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) β (((π΄βπΎ) substr β¨π, (π + 2)β©) = β¨βπ(πβπ)ββ© β§ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
201 | 184, 192,
102, 146, 199, 200 | syl221anc 1382 |
. . . . . . . . . 10
β’ (π β ((((π΄βπΎ) substr β¨π, (π + 2)β©) ++ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)))) = (β¨βπ(πβπ)ββ© ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) β (((π΄βπΎ) substr β¨π, (π + 2)β©) = β¨βπ(πβπ)ββ© β§ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
202 | 190, 201 | mpbid 231 |
. . . . . . . . 9
β’ (π β (((π΄βπΎ) substr β¨π, (π + 2)β©) = β¨βπ(πβπ)ββ© β§ (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
203 | 202 | simpld 496 |
. . . . . . . 8
β’ (π β ((π΄βπΎ) substr β¨π, (π + 2)β©) = β¨βπ(πβπ)ββ©) |
204 | 203 | oveq2d 7425 |
. . . . . . 7
β’ (π β (((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, (π + 2)β©)) = (((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©)) |
205 | | ccatpfx 14651 |
. . . . . . . 8
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ π β (0...(π + 2)) β§ (π + 2) β (0...(β―β(π΄βπΎ)))) β (((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, (π + 2)β©)) = ((π΄βπΎ) prefix (π + 2))) |
206 | 34, 177, 51, 205 | syl3anc 1372 |
. . . . . . 7
β’ (π β (((π΄βπΎ) prefix π) ++ ((π΄βπΎ) substr β¨π, (π + 2)β©)) = ((π΄βπΎ) prefix (π + 2))) |
207 | 204, 206 | eqtr3d 2775 |
. . . . . 6
β’ (π β (((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) = ((π΄βπΎ) prefix (π + 2))) |
208 | 207 | oveq1d 7424 |
. . . . 5
β’ (π β ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = (((π΄βπΎ) prefix (π + 2)) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©))) |
209 | | ccatpfx 14651 |
. . . . . 6
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ (π + 2) β
(0...(β―β(π΄βπΎ))) β§ (β―β(π΄βπΎ)) β (0...(β―β(π΄βπΎ)))) β (((π΄βπΎ) prefix (π + 2)) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = ((π΄βπΎ) prefix (β―β(π΄βπΎ)))) |
210 | 34, 51, 57, 209 | syl3anc 1372 |
. . . . 5
β’ (π β (((π΄βπΎ) prefix (π + 2)) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = ((π΄βπΎ) prefix (β―β(π΄βπΎ)))) |
211 | | pfxid 14634 |
. . . . . 6
β’ ((π΄βπΎ) β Word (πΌ Γ 2o) β ((π΄βπΎ) prefix (β―β(π΄βπΎ))) = (π΄βπΎ)) |
212 | 34, 211 | syl 17 |
. . . . 5
β’ (π β ((π΄βπΎ) prefix (β―β(π΄βπΎ))) = (π΄βπΎ)) |
213 | 208, 210,
212 | 3eqtrd 2777 |
. . . 4
β’ (π β ((((π΄βπΎ) prefix π) ++ β¨βπ(πβπ)ββ©) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = (π΄βπΎ)) |
214 | 94, 175, 213 | 3eqtrd 2777 |
. . 3
β’ (π β (π(πβ(πβπΆ))π) = (π΄βπΎ)) |
215 | 2, 3, 4, 5 | efgtf 19590 |
. . . . . . 7
β’ ((πβπΆ) β π β ((πβ(πβπΆ)) = (π β (0...(β―β(πβπΆ))), π β (πΌ Γ 2o) β¦ ((πβπΆ) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβ(πβπΆ)):((0...(β―β(πβπΆ))) Γ (πΌ Γ 2o))βΆπ)) |
216 | 13, 215 | syl 17 |
. . . . . 6
β’ (π β ((πβ(πβπΆ)) = (π β (0...(β―β(πβπΆ))), π β (πΌ Γ 2o) β¦ ((πβπΆ) splice β¨π, π, β¨βπ(πβπ)ββ©β©)) β§ (πβ(πβπΆ)):((0...(β―β(πβπΆ))) Γ (πΌ Γ 2o))βΆπ)) |
217 | 216 | simprd 497 |
. . . . 5
β’ (π β (πβ(πβπΆ)):((0...(β―β(πβπΆ))) Γ (πΌ Γ 2o))βΆπ) |
218 | 217 | ffnd 6719 |
. . . 4
β’ (π β (πβ(πβπΆ)) Fn ((0...(β―β(πβπΆ))) Γ (πΌ Γ 2o))) |
219 | | fnovrn 7582 |
. . . 4
β’ (((πβ(πβπΆ)) Fn ((0...(β―β(πβπΆ))) Γ (πΌ Γ 2o)) β§ π β
(0...(β―β(πβπΆ))) β§ π β (πΌ Γ 2o)) β (π(πβ(πβπΆ))π) β ran (πβ(πβπΆ))) |
220 | 218, 91, 92, 219 | syl3anc 1372 |
. . 3
β’ (π β (π(πβ(πβπΆ))π) β ran (πβ(πβπΆ))) |
221 | 214, 220 | eqeltrrd 2835 |
. 2
β’ (π β (π΄βπΎ) β ran (πβ(πβπΆ))) |
222 | | uztrn 12840 |
. . . . . . 7
β’ (((π β 2) β
(β€β₯βπ) β§ π β (β€β₯β0))
β (π β 2) β
(β€β₯β0)) |
223 | 87, 16, 222 | syl2anc 585 |
. . . . . 6
β’ (π β (π β 2) β
(β€β₯β0)) |
224 | | elfzuzb 13495 |
. . . . . 6
β’ ((π β 2) β
(0...(β―β(πβπΆ))) β ((π β 2) β
(β€β₯β0) β§ (β―β(πβπΆ)) β
(β€β₯β(π β 2)))) |
225 | 223, 85, 224 | sylanbrc 584 |
. . . . 5
β’ (π β (π β 2) β
(0...(β―β(πβπΆ)))) |
226 | 2, 3, 4, 5 | efgtval 19591 |
. . . . 5
β’ (((πβπΆ) β π β§ (π β 2) β
(0...(β―β(πβπΆ))) β§ π β (πΌ Γ 2o)) β ((π β 2)(πβ(πβπΆ))π) = ((πβπΆ) splice β¨(π β 2), (π β 2), β¨βπ(πβπ)ββ©β©)) |
227 | 13, 225, 117, 226 | syl3anc 1372 |
. . . 4
β’ (π β ((π β 2)(πβ(πβπΆ))π) = ((πβπΆ) splice β¨(π β 2), (π β 2), β¨βπ(πβπ)ββ©β©)) |
228 | | pfxcl 14627 |
. . . . . 6
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β ((π΅βπΏ) prefix (π β 2)) β Word (πΌ Γ 2o)) |
229 | 30, 228 | syl 17 |
. . . . 5
β’ (π β ((π΅βπΏ) prefix (π β 2)) β Word (πΌ Γ 2o)) |
230 | | swrdcl 14595 |
. . . . . 6
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) |
231 | 30, 230 | syl 17 |
. . . . 5
β’ (π β ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) |
232 | | ccatswrd 14618 |
. . . . . . . . . . 11
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ ((π + 2) β (0...π) β§ π β (0...(β―β(π΄βπΎ))) β§ (β―β(π΄βπΎ)) β (0...(β―β(π΄βπΎ))))) β (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) |
233 | 34, 179, 44, 57, 232 | syl13anc 1373 |
. . . . . . . . . 10
β’ (π β (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) |
234 | 202 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) |
235 | | elfzuzb 13495 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...(π β 2)) β (π β (β€β₯β0)
β§ (π β 2) β
(β€β₯βπ))) |
236 | 16, 87, 235 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (π β π β (0...(π β 2))) |
237 | 2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131 | efgredlemg 19610 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β―β(π΄βπΎ)) = (β―β(π΅βπΏ))) |
238 | 237, 46 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β―β(π΅βπΏ)) β
(β€β₯βπ)) |
239 | | 0le2 12314 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 β€
2 |
240 | 239 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 0 β€ 2) |
241 | 74 | zred 12666 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β) |
242 | | 2re 12286 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
243 | | subge02 11730 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ 2 β
β) β (0 β€ 2 β (π β 2) β€ π)) |
244 | 241, 242,
243 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0 β€ 2 β (π β 2) β€ π)) |
245 | 240, 244 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π β 2) β€ π) |
246 | | eluz2 12828 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β(π β 2)) β ((π β 2) β β€ β§ π β β€ β§ (π β 2) β€ π)) |
247 | 76, 74, 245, 246 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (β€β₯β(π β 2))) |
248 | | uztrn 12840 |
. . . . . . . . . . . . . . . . 17
β’
(((β―β(π΅βπΏ)) β
(β€β₯βπ) β§ π β (β€β₯β(π β 2))) β
(β―β(π΅βπΏ)) β
(β€β₯β(π β 2))) |
249 | 238, 247,
248 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―β(π΅βπΏ)) β
(β€β₯β(π β 2))) |
250 | | elfzuzb 13495 |
. . . . . . . . . . . . . . . 16
β’ ((π β 2) β
(0...(β―β(π΅βπΏ))) β ((π β 2) β
(β€β₯β0) β§ (β―β(π΅βπΏ)) β
(β€β₯β(π β 2)))) |
251 | 223, 249,
250 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (π β (π β 2) β
(0...(β―β(π΅βπΏ)))) |
252 | | lencl 14483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β
(β―β(π΅βπΏ)) β
β0) |
253 | 30, 252 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β―β(π΅βπΏ)) β
β0) |
254 | 253, 54 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―β(π΅βπΏ)) β
(β€β₯β0)) |
255 | | eluzfz2 13509 |
. . . . . . . . . . . . . . . 16
β’
((β―β(π΅βπΏ)) β (β€β₯β0)
β (β―β(π΅βπΏ)) β (0...(β―β(π΅βπΏ)))) |
256 | 254, 255 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (β―β(π΅βπΏ)) β (0...(β―β(π΅βπΏ)))) |
257 | | ccatswrd 14618 |
. . . . . . . . . . . . . . 15
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ (π β (0...(π β 2)) β§ (π β 2) β
(0...(β―β(π΅βπΏ))) β§ (β―β(π΅βπΏ)) β (0...(β―β(π΅βπΏ))))) β (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) |
258 | 30, 236, 251, 256, 257 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (π β (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) |
259 | 234, 258 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ (π β (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©))) |
260 | | swrdcl 14595 |
. . . . . . . . . . . . . . 15
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β ((π΅βπΏ) substr β¨π, (π β 2)β©) β Word (πΌ Γ
2o)) |
261 | 30, 260 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((π΅βπΏ) substr β¨π, (π β 2)β©) β Word (πΌ Γ
2o)) |
262 | | swrdcl 14595 |
. . . . . . . . . . . . . . 15
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) |
263 | 30, 262 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) |
264 | | swrdlen 14597 |
. . . . . . . . . . . . . . . 16
β’ (((π΄βπΎ) β Word (πΌ Γ 2o) β§ (π + 2) β (0...π) β§ π β (0...(β―β(π΄βπΎ)))) β (β―β((π΄βπΎ) substr β¨(π + 2), πβ©)) = (π β (π + 2))) |
265 | 34, 179, 44, 264 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (π β (β―β((π΄βπΎ) substr β¨(π + 2), πβ©)) = (π β (π + 2))) |
266 | | swrdlen 14597 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ π β (0...(π β 2)) β§ (π β 2) β
(0...(β―β(π΅βπΏ)))) β (β―β((π΅βπΏ) substr β¨π, (π β 2)β©)) = ((π β 2) β π)) |
267 | 30, 236, 251, 266 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―β((π΅βπΏ) substr β¨π, (π β 2)β©)) = ((π β 2) β π)) |
268 | 78, 62, 70 | sub32d 11603 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π β π) β 2) = ((π β 2) β π)) |
269 | 78, 62, 70 | subsub4d 11602 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π β π) β 2) = (π β (π + 2))) |
270 | 267, 268,
269 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . 15
β’ (π β (β―β((π΅βπΏ) substr β¨π, (π β 2)β©)) = (π β (π + 2))) |
271 | 265, 270 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ (π β (β―β((π΄βπΎ) substr β¨(π + 2), πβ©)) = (β―β((π΅βπΏ) substr β¨π, (π β 2)β©))) |
272 | | ccatopth 14666 |
. . . . . . . . . . . . . 14
β’
(((((π΄βπΎ) substr β¨(π + 2), πβ©) β Word (πΌ Γ 2o) β§
(β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) β Word (πΌ Γ 2o)) β§ (((π΅βπΏ) substr β¨π, (π β 2)β©) β Word (πΌ Γ 2o) β§
((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) β§
(β―β((π΄βπΎ) substr β¨(π + 2), πβ©)) = (β―β((π΅βπΏ) substr β¨π, (π β 2)β©))) β ((((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)) β (((π΄βπΎ) substr β¨(π + 2), πβ©) = ((π΅βπΏ) substr β¨π, (π β 2)β©) β§ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)))) |
273 | 186, 142,
261, 263, 271, 272 | syl221anc 1382 |
. . . . . . . . . . . . 13
β’ (π β ((((π΄βπΎ) substr β¨(π + 2), πβ©) ++ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©))) = (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)) β (((π΄βπΎ) substr β¨(π + 2), πβ©) = ((π΅βπΏ) substr β¨π, (π β 2)β©) β§ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)))) |
274 | 259, 273 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β (((π΄βπΎ) substr β¨(π + 2), πβ©) = ((π΅βπΏ) substr β¨π, (π β 2)β©) β§ (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©))) |
275 | 274 | simpld 496 |
. . . . . . . . . . 11
β’ (π β ((π΄βπΎ) substr β¨(π + 2), πβ©) = ((π΅βπΏ) substr β¨π, (π β 2)β©)) |
276 | 274 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)) |
277 | | elfzuzb 13495 |
. . . . . . . . . . . . . . . 16
β’ ((π β 2) β (0...π) β ((π β 2) β
(β€β₯β0) β§ π β (β€β₯β(π β 2)))) |
278 | 223, 247,
277 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (π β (π β 2) β (0...π)) |
279 | | elfzuz 13497 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(0...(β―β(π΄βπΎ))) β π β
(β€β₯β0)) |
280 | 44, 279 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
(β€β₯β0)) |
281 | | elfzuzb 13495 |
. . . . . . . . . . . . . . . 16
β’ (π β
(0...(β―β(π΅βπΏ))) β (π β (β€β₯β0)
β§ (β―β(π΅βπΏ)) β
(β€β₯βπ))) |
282 | 280, 238,
281 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (π β π β (0...(β―β(π΅βπΏ)))) |
283 | | ccatswrd 14618 |
. . . . . . . . . . . . . . 15
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ ((π β 2) β (0...π) β§ π β (0...(β―β(π΅βπΏ))) β§ (β―β(π΅βπΏ)) β (0...(β―β(π΅βπΏ))))) β (((π΅βπΏ) substr β¨(π β 2), πβ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)) |
284 | 30, 278, 282, 256, 283 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (π β (((π΅βπΏ) substr β¨(π β 2), πβ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = ((π΅βπΏ) substr β¨(π β 2), (β―β(π΅βπΏ))β©)) |
285 | 276, 284 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ (π β (β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = (((π΅βπΏ) substr β¨(π β 2), πβ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
286 | | swrdcl 14595 |
. . . . . . . . . . . . . . 15
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β ((π΅βπΏ) substr β¨(π β 2), πβ©) β Word (πΌ Γ 2o)) |
287 | 30, 286 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((π΅βπΏ) substr β¨(π β 2), πβ©) β Word (πΌ Γ 2o)) |
288 | | s2len 14840 |
. . . . . . . . . . . . . . 15
β’
(β―ββ¨βπ(πβπ)ββ©) = 2 |
289 | | swrdlen 14597 |
. . . . . . . . . . . . . . . . 17
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ (π β 2) β (0...π) β§ π β (0...(β―β(π΅βπΏ)))) β (β―β((π΅βπΏ) substr β¨(π β 2), πβ©)) = (π β (π β 2))) |
290 | 30, 278, 282, 289 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―β((π΅βπΏ) substr β¨(π β 2), πβ©)) = (π β (π β 2))) |
291 | | nncan 11489 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ 2 β
β) β (π β
(π β 2)) =
2) |
292 | 78, 69, 291 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (π β 2)) = 2) |
293 | 290, 292 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
β’ (π β 2 = (β―β((π΅βπΏ) substr β¨(π β 2), πβ©))) |
294 | 288, 293 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ (π β
(β―ββ¨βπ(πβπ)ββ©) = (β―β((π΅βπΏ) substr β¨(π β 2), πβ©))) |
295 | | ccatopth 14666 |
. . . . . . . . . . . . . 14
β’
(((β¨βπ(πβπ)ββ© β Word (πΌ Γ 2o) β§
((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) β Word (πΌ Γ 2o)) β§ (((π΅βπΏ) substr β¨(π β 2), πβ©) β Word (πΌ Γ 2o) β§ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) β§
(β―ββ¨βπ(πβπ)ββ©) = (β―β((π΅βπΏ) substr β¨(π β 2), πβ©))) β ((β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = (((π΅βπΏ) substr β¨(π β 2), πβ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) β (β¨βπ(πβπ)ββ© = ((π΅βπΏ) substr β¨(π β 2), πβ©) β§ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
296 | 120, 122,
287, 231, 294, 295 | syl221anc 1382 |
. . . . . . . . . . . . 13
β’ (π β ((β¨βπ(πβπ)ββ© ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = (((π΅βπΏ) substr β¨(π β 2), πβ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) β (β¨βπ(πβπ)ββ© = ((π΅βπΏ) substr β¨(π β 2), πβ©) β§ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
297 | 285, 296 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β (β¨βπ(πβπ)ββ© = ((π΅βπΏ) substr β¨(π β 2), πβ©) β§ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
298 | 297 | simprd 497 |
. . . . . . . . . . 11
β’ (π β ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©) = ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) |
299 | 275, 298 | oveq12d 7427 |
. . . . . . . . . 10
β’ (π β (((π΄βπΎ) substr β¨(π + 2), πβ©) ++ ((π΄βπΎ) substr β¨π, (β―β(π΄βπΎ))β©)) = (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
300 | 233, 299 | eqtr3d 2775 |
. . . . . . . . 9
β’ (π β ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©) = (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
301 | 300 | oveq2d 7425 |
. . . . . . . 8
β’ (π β (((π΅βπΏ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = (((π΅βπΏ) prefix π) ++ (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
302 | | ccatass 14538 |
. . . . . . . . 9
β’ ((((π΅βπΏ) prefix π) β Word (πΌ Γ 2o) β§ ((π΅βπΏ) substr β¨π, (π β 2)β©) β Word (πΌ Γ 2o) β§
((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©) β Word (πΌ Γ 2o)) β ((((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (π β 2)β©)) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = (((π΅βπΏ) prefix π) ++ (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
303 | 32, 261, 231, 302 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (π β 2)β©)) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = (((π΅βπΏ) prefix π) ++ (((π΅βπΏ) substr β¨π, (π β 2)β©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)))) |
304 | 301, 303 | eqtr4d 2776 |
. . . . . . 7
β’ (π β (((π΅βπΏ) prefix π) ++ ((π΄βπΎ) substr β¨(π + 2), (β―β(π΄βπΎ))β©)) = ((((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (π β 2)β©)) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
305 | | ccatpfx 14651 |
. . . . . . . . 9
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ π β (0...(π β 2)) β§ (π β 2) β
(0...(β―β(π΅βπΏ)))) β (((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (π β 2)β©)) = ((π΅βπΏ) prefix (π β 2))) |
306 | 30, 236, 251, 305 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (π β 2)β©)) = ((π΅βπΏ) prefix (π β 2))) |
307 | 306 | oveq1d 7424 |
. . . . . . 7
β’ (π β ((((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (π β 2)β©)) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = (((π΅βπΏ) prefix (π β 2)) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
308 | 17, 304, 307 | 3eqtrd 2777 |
. . . . . 6
β’ (π β (πβπΆ) = (((π΅βπΏ) prefix (π β 2)) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
309 | | ccatrid 14537 |
. . . . . . . 8
β’ (((π΅βπΏ) prefix (π β 2)) β Word (πΌ Γ 2o) β (((π΅βπΏ) prefix (π β 2)) ++ β
) = ((π΅βπΏ) prefix (π β 2))) |
310 | 229, 309 | syl 17 |
. . . . . . 7
β’ (π β (((π΅βπΏ) prefix (π β 2)) ++ β
) = ((π΅βπΏ) prefix (π β 2))) |
311 | 310 | oveq1d 7424 |
. . . . . 6
β’ (π β ((((π΅βπΏ) prefix (π β 2)) ++ β
) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = (((π΅βπΏ) prefix (π β 2)) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
312 | 308, 311 | eqtr4d 2776 |
. . . . 5
β’ (π β (πβπΆ) = ((((π΅βπΏ) prefix (π β 2)) ++ β
) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
313 | | pfxlen 14633 |
. . . . . . 7
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ (π β 2) β
(0...(β―β(π΅βπΏ)))) β (β―β((π΅βπΏ) prefix (π β 2))) = (π β 2)) |
314 | 30, 251, 313 | syl2anc 585 |
. . . . . 6
β’ (π β (β―β((π΅βπΏ) prefix (π β 2))) = (π β 2)) |
315 | 314 | eqcomd 2739 |
. . . . 5
β’ (π β (π β 2) = (β―β((π΅βπΏ) prefix (π β 2)))) |
316 | 171 | oveq2i 7420 |
. . . . . 6
β’ ((π β 2) +
(β―ββ
)) = ((π β 2) + 0) |
317 | 76 | zcnd 12667 |
. . . . . . 7
β’ (π β (π β 2) β β) |
318 | 317 | addridd 11414 |
. . . . . 6
β’ (π β ((π β 2) + 0) = (π β 2)) |
319 | 316, 318 | eqtr2id 2786 |
. . . . 5
β’ (π β (π β 2) = ((π β 2) +
(β―ββ
))) |
320 | 229, 98, 231, 120, 312, 315, 319 | splval2 14707 |
. . . 4
β’ (π β ((πβπΆ) splice β¨(π β 2), (π β 2), β¨βπ(πβπ)ββ©β©) = ((((π΅βπΏ) prefix (π β 2)) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
321 | 297 | simpld 496 |
. . . . . . . 8
β’ (π β β¨βπ(πβπ)ββ© = ((π΅βπΏ) substr β¨(π β 2), πβ©)) |
322 | 321 | oveq2d 7425 |
. . . . . . 7
β’ (π β (((π΅βπΏ) prefix (π β 2)) ++ β¨βπ(πβπ)ββ©) = (((π΅βπΏ) prefix (π β 2)) ++ ((π΅βπΏ) substr β¨(π β 2), πβ©))) |
323 | | ccatpfx 14651 |
. . . . . . . 8
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ (π β 2) β (0...π) β§ π β (0...(β―β(π΅βπΏ)))) β (((π΅βπΏ) prefix (π β 2)) ++ ((π΅βπΏ) substr β¨(π β 2), πβ©)) = ((π΅βπΏ) prefix π)) |
324 | 30, 278, 282, 323 | syl3anc 1372 |
. . . . . . 7
β’ (π β (((π΅βπΏ) prefix (π β 2)) ++ ((π΅βπΏ) substr β¨(π β 2), πβ©)) = ((π΅βπΏ) prefix π)) |
325 | 322, 324 | eqtrd 2773 |
. . . . . 6
β’ (π β (((π΅βπΏ) prefix (π β 2)) ++ β¨βπ(πβπ)ββ©) = ((π΅βπΏ) prefix π)) |
326 | 325 | oveq1d 7424 |
. . . . 5
β’ (π β ((((π΅βπΏ) prefix (π β 2)) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = (((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©))) |
327 | | ccatpfx 14651 |
. . . . . 6
β’ (((π΅βπΏ) β Word (πΌ Γ 2o) β§ π β
(0...(β―β(π΅βπΏ))) β§ (β―β(π΅βπΏ)) β (0...(β―β(π΅βπΏ)))) β (((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = ((π΅βπΏ) prefix (β―β(π΅βπΏ)))) |
328 | 30, 282, 256, 327 | syl3anc 1372 |
. . . . 5
β’ (π β (((π΅βπΏ) prefix π) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = ((π΅βπΏ) prefix (β―β(π΅βπΏ)))) |
329 | | pfxid 14634 |
. . . . . 6
β’ ((π΅βπΏ) β Word (πΌ Γ 2o) β ((π΅βπΏ) prefix (β―β(π΅βπΏ))) = (π΅βπΏ)) |
330 | 30, 329 | syl 17 |
. . . . 5
β’ (π β ((π΅βπΏ) prefix (β―β(π΅βπΏ))) = (π΅βπΏ)) |
331 | 326, 328,
330 | 3eqtrd 2777 |
. . . 4
β’ (π β ((((π΅βπΏ) prefix (π β 2)) ++ β¨βπ(πβπ)ββ©) ++ ((π΅βπΏ) substr β¨π, (β―β(π΅βπΏ))β©)) = (π΅βπΏ)) |
332 | 227, 320,
331 | 3eqtrd 2777 |
. . 3
β’ (π β ((π β 2)(πβ(πβπΆ))π) = (π΅βπΏ)) |
333 | | fnovrn 7582 |
. . . 4
β’ (((πβ(πβπΆ)) Fn ((0...(β―β(πβπΆ))) Γ (πΌ Γ 2o)) β§ (π β 2) β
(0...(β―β(πβπΆ))) β§ π β (πΌ Γ 2o)) β ((π β 2)(πβ(πβπΆ))π) β ran (πβ(πβπΆ))) |
334 | 218, 225,
117, 333 | syl3anc 1372 |
. . 3
β’ (π β ((π β 2)(πβ(πβπΆ))π) β ran (πβ(πβπΆ))) |
335 | 332, 334 | eqeltrrd 2835 |
. 2
β’ (π β (π΅βπΏ) β ran (πβ(πβπΆ))) |
336 | 221, 335 | jca 513 |
1
β’ (π β ((π΄βπΎ) β ran (πβ(πβπΆ)) β§ (π΅βπΏ) β ran (πβ(πβπΆ)))) |