Step | Hyp | Ref
| Expression |
1 | | sadcp1.n |
. 2
β’ (π β π β
β0) |
2 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π₯ = 0 β (0..^π₯) = (0..^0)) |
3 | | fzo0 13602 |
. . . . . . . . . . 11
β’ (0..^0) =
β
|
4 | 2, 3 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π₯ = 0 β (0..^π₯) = β
) |
5 | 4 | ineq2d 4173 |
. . . . . . . . 9
β’ (π₯ = 0 β ((π΄ sadd π΅) β© (0..^π₯)) = ((π΄ sadd π΅) β© β
)) |
6 | | in0 4352 |
. . . . . . . . 9
β’ ((π΄ sadd π΅) β© β
) = β
|
7 | 5, 6 | eqtrdi 2789 |
. . . . . . . 8
β’ (π₯ = 0 β ((π΄ sadd π΅) β© (0..^π₯)) = β
) |
8 | 7 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = 0 β (πΎβ((π΄ sadd π΅) β© (0..^π₯))) = (πΎββ
)) |
9 | | sadcadd.k |
. . . . . . . . 9
β’ πΎ = β‘(bits βΎ
β0) |
10 | | 0nn0 12433 |
. . . . . . . . . . 11
β’ 0 β
β0 |
11 | | fvres 6862 |
. . . . . . . . . . 11
β’ (0 β
β0 β ((bits βΎ β0)β0) =
(bitsβ0)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
β’ ((bits
βΎ β0)β0) = (bitsβ0) |
13 | | 0bits 16324 |
. . . . . . . . . 10
β’
(bitsβ0) = β
|
14 | 12, 13 | eqtr2i 2762 |
. . . . . . . . 9
β’ β
=
((bits βΎ β0)β0) |
15 | 9, 14 | fveq12i 6849 |
. . . . . . . 8
β’ (πΎββ
) = (β‘(bits βΎ
β0)β((bits βΎ
β0)β0)) |
16 | | bitsf1o 16330 |
. . . . . . . . 9
β’ (bits
βΎ β0):β0β1-1-ontoβ(π« β0 β©
Fin) |
17 | | f1ocnvfv1 7223 |
. . . . . . . . 9
β’ (((bits
βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin)
β§ 0 β β0) β (β‘(bits βΎ
β0)β((bits βΎ β0)β0)) =
0) |
18 | 16, 10, 17 | mp2an 691 |
. . . . . . . 8
β’ (β‘(bits βΎ
β0)β((bits βΎ β0)β0)) =
0 |
19 | 15, 18 | eqtri 2761 |
. . . . . . 7
β’ (πΎββ
) =
0 |
20 | 8, 19 | eqtrdi 2789 |
. . . . . 6
β’ (π₯ = 0 β (πΎβ((π΄ sadd π΅) β© (0..^π₯))) = 0) |
21 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = 0 β (πΆβπ₯) = (πΆβ0)) |
22 | 21 | eleq2d 2820 |
. . . . . . 7
β’ (π₯ = 0 β (β
β
(πΆβπ₯) β β
β (πΆβ0))) |
23 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = 0 β (2βπ₯) = (2β0)) |
24 | 22, 23 | ifbieq1d 4511 |
. . . . . 6
β’ (π₯ = 0 β if(β
β
(πΆβπ₯), (2βπ₯), 0) = if(β
β (πΆβ0), (2β0), 0)) |
25 | 20, 24 | oveq12d 7376 |
. . . . 5
β’ (π₯ = 0 β ((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = (0 + if(β
β (πΆβ0), (2β0),
0))) |
26 | 4 | ineq2d 4173 |
. . . . . . . . . 10
β’ (π₯ = 0 β (π΄ β© (0..^π₯)) = (π΄ β© β
)) |
27 | | in0 4352 |
. . . . . . . . . 10
β’ (π΄ β© β
) =
β
|
28 | 26, 27 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π₯ = 0 β (π΄ β© (0..^π₯)) = β
) |
29 | 28 | fveq2d 6847 |
. . . . . . . 8
β’ (π₯ = 0 β (πΎβ(π΄ β© (0..^π₯))) = (πΎββ
)) |
30 | 29, 19 | eqtrdi 2789 |
. . . . . . 7
β’ (π₯ = 0 β (πΎβ(π΄ β© (0..^π₯))) = 0) |
31 | 4 | ineq2d 4173 |
. . . . . . . . . 10
β’ (π₯ = 0 β (π΅ β© (0..^π₯)) = (π΅ β© β
)) |
32 | | in0 4352 |
. . . . . . . . . 10
β’ (π΅ β© β
) =
β
|
33 | 31, 32 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π₯ = 0 β (π΅ β© (0..^π₯)) = β
) |
34 | 33 | fveq2d 6847 |
. . . . . . . 8
β’ (π₯ = 0 β (πΎβ(π΅ β© (0..^π₯))) = (πΎββ
)) |
35 | 34, 19 | eqtrdi 2789 |
. . . . . . 7
β’ (π₯ = 0 β (πΎβ(π΅ β© (0..^π₯))) = 0) |
36 | 30, 35 | oveq12d 7376 |
. . . . . 6
β’ (π₯ = 0 β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = (0 + 0)) |
37 | | 00id 11335 |
. . . . . 6
β’ (0 + 0) =
0 |
38 | 36, 37 | eqtrdi 2789 |
. . . . 5
β’ (π₯ = 0 β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = 0) |
39 | 25, 38 | eqeq12d 2749 |
. . . 4
β’ (π₯ = 0 β (((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) β (0 + if(β
β (πΆβ0), (2β0), 0)) =
0)) |
40 | 39 | imbi2d 341 |
. . 3
β’ (π₯ = 0 β ((π β ((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯))))) β (π β (0 + if(β
β (πΆβ0), (2β0), 0)) =
0))) |
41 | | oveq2 7366 |
. . . . . . . 8
β’ (π₯ = π β (0..^π₯) = (0..^π)) |
42 | 41 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = π β ((π΄ sadd π΅) β© (0..^π₯)) = ((π΄ sadd π΅) β© (0..^π))) |
43 | 42 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π β (πΎβ((π΄ sadd π΅) β© (0..^π₯))) = (πΎβ((π΄ sadd π΅) β© (0..^π)))) |
44 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = π β (πΆβπ₯) = (πΆβπ)) |
45 | 44 | eleq2d 2820 |
. . . . . . 7
β’ (π₯ = π β (β
β (πΆβπ₯) β β
β (πΆβπ))) |
46 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = π β (2βπ₯) = (2βπ)) |
47 | 45, 46 | ifbieq1d 4511 |
. . . . . 6
β’ (π₯ = π β if(β
β (πΆβπ₯), (2βπ₯), 0) = if(β
β (πΆβπ), (2βπ), 0)) |
48 | 43, 47 | oveq12d 7376 |
. . . . 5
β’ (π₯ = π β ((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0))) |
49 | 41 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = π β (π΄ β© (0..^π₯)) = (π΄ β© (0..^π))) |
50 | 49 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π β (πΎβ(π΄ β© (0..^π₯))) = (πΎβ(π΄ β© (0..^π)))) |
51 | 41 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = π β (π΅ β© (0..^π₯)) = (π΅ β© (0..^π))) |
52 | 51 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π β (πΎβ(π΅ β© (0..^π₯))) = (πΎβ(π΅ β© (0..^π)))) |
53 | 50, 52 | oveq12d 7376 |
. . . . 5
β’ (π₯ = π β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) |
54 | 48, 53 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π β (((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) |
55 | 54 | imbi2d 341 |
. . 3
β’ (π₯ = π β ((π β ((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯))))) β (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))))) |
56 | | oveq2 7366 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (0..^π₯) = (0..^(π + 1))) |
57 | 56 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = (π + 1) β ((π΄ sadd π΅) β© (0..^π₯)) = ((π΄ sadd π΅) β© (0..^(π + 1)))) |
58 | 57 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = (π + 1) β (πΎβ((π΄ sadd π΅) β© (0..^π₯))) = (πΎβ((π΄ sadd π΅) β© (0..^(π + 1))))) |
59 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (πΆβπ₯) = (πΆβ(π + 1))) |
60 | 59 | eleq2d 2820 |
. . . . . . 7
β’ (π₯ = (π + 1) β (β
β (πΆβπ₯) β β
β (πΆβ(π + 1)))) |
61 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = (π + 1) β (2βπ₯) = (2β(π + 1))) |
62 | 60, 61 | ifbieq1d 4511 |
. . . . . 6
β’ (π₯ = (π + 1) β if(β
β (πΆβπ₯), (2βπ₯), 0) = if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) |
63 | 58, 62 | oveq12d 7376 |
. . . . 5
β’ (π₯ = (π + 1) β ((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0))) |
64 | 56 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = (π + 1) β (π΄ β© (0..^π₯)) = (π΄ β© (0..^(π + 1)))) |
65 | 64 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = (π + 1) β (πΎβ(π΄ β© (0..^π₯))) = (πΎβ(π΄ β© (0..^(π + 1))))) |
66 | 56 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = (π + 1) β (π΅ β© (0..^π₯)) = (π΅ β© (0..^(π + 1)))) |
67 | 66 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = (π + 1) β (πΎβ(π΅ β© (0..^π₯))) = (πΎβ(π΅ β© (0..^(π + 1))))) |
68 | 65, 67 | oveq12d 7376 |
. . . . 5
β’ (π₯ = (π + 1) β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))) |
69 | 63, 68 | eqeq12d 2749 |
. . . 4
β’ (π₯ = (π + 1) β (((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))))) |
70 | 69 | imbi2d 341 |
. . 3
β’ (π₯ = (π + 1) β ((π β ((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯))))) β (π β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))))) |
71 | | oveq2 7366 |
. . . . . . . 8
β’ (π₯ = π β (0..^π₯) = (0..^π)) |
72 | 71 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = π β ((π΄ sadd π΅) β© (0..^π₯)) = ((π΄ sadd π΅) β© (0..^π))) |
73 | 72 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π β (πΎβ((π΄ sadd π΅) β© (0..^π₯))) = (πΎβ((π΄ sadd π΅) β© (0..^π)))) |
74 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = π β (πΆβπ₯) = (πΆβπ)) |
75 | 74 | eleq2d 2820 |
. . . . . . 7
β’ (π₯ = π β (β
β (πΆβπ₯) β β
β (πΆβπ))) |
76 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = π β (2βπ₯) = (2βπ)) |
77 | 75, 76 | ifbieq1d 4511 |
. . . . . 6
β’ (π₯ = π β if(β
β (πΆβπ₯), (2βπ₯), 0) = if(β
β (πΆβπ), (2βπ), 0)) |
78 | 73, 77 | oveq12d 7376 |
. . . . 5
β’ (π₯ = π β ((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0))) |
79 | 71 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = π β (π΄ β© (0..^π₯)) = (π΄ β© (0..^π))) |
80 | 79 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π β (πΎβ(π΄ β© (0..^π₯))) = (πΎβ(π΄ β© (0..^π)))) |
81 | 71 | ineq2d 4173 |
. . . . . . 7
β’ (π₯ = π β (π΅ β© (0..^π₯)) = (π΅ β© (0..^π))) |
82 | 81 | fveq2d 6847 |
. . . . . 6
β’ (π₯ = π β (πΎβ(π΅ β© (0..^π₯))) = (πΎβ(π΅ β© (0..^π)))) |
83 | 80, 82 | oveq12d 7376 |
. . . . 5
β’ (π₯ = π β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) |
84 | 78, 83 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π β (((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) |
85 | 84 | imbi2d 341 |
. . 3
β’ (π₯ = π β ((π β ((πΎβ((π΄ sadd π΅) β© (0..^π₯))) + if(β
β (πΆβπ₯), (2βπ₯), 0)) = ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯))))) β (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))))) |
86 | | sadval.a |
. . . . . . 7
β’ (π β π΄ β
β0) |
87 | | sadval.b |
. . . . . . 7
β’ (π β π΅ β
β0) |
88 | | sadval.c |
. . . . . . 7
β’ πΆ = seq0((π β 2o, π β β0 β¦
if(cadd(π β π΄, π β π΅, β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β
1)))) |
89 | 86, 87, 88 | sadc0 16339 |
. . . . . 6
β’ (π β Β¬ β
β
(πΆβ0)) |
90 | 89 | iffalsed 4498 |
. . . . 5
β’ (π β if(β
β (πΆβ0), (2β0), 0) =
0) |
91 | 90 | oveq2d 7374 |
. . . 4
β’ (π β (0 + if(β
β
(πΆβ0), (2β0),
0)) = (0 + 0)) |
92 | 91, 37 | eqtrdi 2789 |
. . 3
β’ (π β (0 + if(β
β
(πΆβ0), (2β0),
0)) = 0) |
93 | 86 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β0) β§ ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β π΄ β
β0) |
94 | 87 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β0) β§ ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β π΅ β
β0) |
95 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β β0) β§ ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β π β β0) |
96 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β β0) β§ ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) |
97 | 93, 94, 88, 95, 9, 96 | sadadd2lem 16344 |
. . . . . 6
β’ (((π β§ π β β0) β§ ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))) |
98 | 97 | ex 414 |
. . . . 5
β’ ((π β§ π β β0) β (((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))))) |
99 | 98 | expcom 415 |
. . . 4
β’ (π β β0
β (π β (((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))))) |
100 | 99 | a2d 29 |
. . 3
β’ (π β β0
β ((π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β (π β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β
β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))))) |
101 | 40, 55, 70, 85, 92, 100 | nn0ind 12603 |
. 2
β’ (π β β0
β (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) |
102 | 1, 101 | mpcom 38 |
1
β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β
β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) |