Metamath Proof Explorer


Theorem sadcaddlem

Description: Lemma for sadcadd . (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Hypotheses sadval.a φ A 0
sadval.b φ B 0
sadval.c C = seq 0 c 2 𝑜 , m 0 if cadd m A m B c 1 𝑜 n 0 if n = 0 n 1
sadcp1.n φ N 0
sadcadd.k K = bits 0 -1
sadcaddlem.1 φ C N 2 N K A 0 ..^ N + K B 0 ..^ N
Assertion sadcaddlem φ C N + 1 2 N + 1 K A 0 ..^ N + 1 + K B 0 ..^ N + 1

Proof

Step Hyp Ref Expression
1 sadval.a φ A 0
2 sadval.b φ B 0
3 sadval.c C = seq 0 c 2 𝑜 , m 0 if cadd m A m B c 1 𝑜 n 0 if n = 0 n 1
4 sadcp1.n φ N 0
5 sadcadd.k K = bits 0 -1
6 sadcaddlem.1 φ C N 2 N K A 0 ..^ N + K B 0 ..^ N
7 cad1 C N cadd N A N B C N N A N B
8 7 adantl φ C N cadd N A N B C N N A N B
9 2nn 2
10 9 a1i φ 2
11 10 4 nnexpcld φ 2 N
12 11 nnred φ 2 N
13 12 ad2antrr φ C N N A N B 2 N
14 inss1 A 0 ..^ N A
15 14 1 sstrid φ A 0 ..^ N 0
16 fzofi 0 ..^ N Fin
17 16 a1i φ 0 ..^ N Fin
18 inss2 A 0 ..^ N 0 ..^ N
19 ssfi 0 ..^ N Fin A 0 ..^ N 0 ..^ N A 0 ..^ N Fin
20 17 18 19 sylancl φ A 0 ..^ N Fin
21 elfpw A 0 ..^ N 𝒫 0 Fin A 0 ..^ N 0 A 0 ..^ N Fin
22 15 20 21 sylanbrc φ A 0 ..^ N 𝒫 0 Fin
23 bitsf1o bits 0 : 0 1-1 onto 𝒫 0 Fin
24 f1ocnv bits 0 : 0 1-1 onto 𝒫 0 Fin bits 0 -1 : 𝒫 0 Fin 1-1 onto 0
25 23 24 ax-mp bits 0 -1 : 𝒫 0 Fin 1-1 onto 0
26 f1oeq1 K = bits 0 -1 K : 𝒫 0 Fin 1-1 onto 0 bits 0 -1 : 𝒫 0 Fin 1-1 onto 0
27 5 26 ax-mp K : 𝒫 0 Fin 1-1 onto 0 bits 0 -1 : 𝒫 0 Fin 1-1 onto 0
28 25 27 mpbir K : 𝒫 0 Fin 1-1 onto 0
29 f1of K : 𝒫 0 Fin 1-1 onto 0 K : 𝒫 0 Fin 0
30 28 29 ax-mp K : 𝒫 0 Fin 0
31 30 ffvelrni A 0 ..^ N 𝒫 0 Fin K A 0 ..^ N 0
32 22 31 syl φ K A 0 ..^ N 0
33 inss1 B 0 ..^ N B
34 33 2 sstrid φ B 0 ..^ N 0
35 inss2 B 0 ..^ N 0 ..^ N
36 ssfi 0 ..^ N Fin B 0 ..^ N 0 ..^ N B 0 ..^ N Fin
37 17 35 36 sylancl φ B 0 ..^ N Fin
38 elfpw B 0 ..^ N 𝒫 0 Fin B 0 ..^ N 0 B 0 ..^ N Fin
39 34 37 38 sylanbrc φ B 0 ..^ N 𝒫 0 Fin
40 30 ffvelrni B 0 ..^ N 𝒫 0 Fin K B 0 ..^ N 0
41 39 40 syl φ K B 0 ..^ N 0
42 32 41 nn0addcld φ K A 0 ..^ N + K B 0 ..^ N 0
43 42 nn0red φ K A 0 ..^ N + K B 0 ..^ N
44 43 ad2antrr φ C N N A N B K A 0 ..^ N + K B 0 ..^ N
45 2nn0 2 0
46 45 a1i φ N A 2 0
47 4 adantr φ N A N 0
48 46 47 nn0expcld φ N A 2 N 0
49 0nn0 0 0
50 49 a1i φ ¬ N A 0 0
51 48 50 ifclda φ if N A 2 N 0 0
52 45 a1i φ N B 2 0
53 4 adantr φ N B N 0
54 52 53 nn0expcld φ N B 2 N 0
55 49 a1i φ ¬ N B 0 0
56 54 55 ifclda φ if N B 2 N 0 0
57 51 56 nn0addcld φ if N A 2 N 0 + if N B 2 N 0 0
58 57 nn0red φ if N A 2 N 0 + if N B 2 N 0
59 58 ad2antrr φ C N N A N B if N A 2 N 0 + if N B 2 N 0
60 6 biimpa φ C N 2 N K A 0 ..^ N + K B 0 ..^ N
61 60 adantr φ C N N A N B 2 N K A 0 ..^ N + K B 0 ..^ N
62 11 nnnn0d φ 2 N 0
63 ifcl 2 N 0 0 0 if N B 2 N 0 0
64 62 49 63 sylancl φ if N B 2 N 0 0
65 64 nn0ge0d φ 0 if N B 2 N 0
66 12 adantr φ N B 2 N
67 0red φ ¬ N B 0
68 66 67 ifclda φ if N B 2 N 0
69 12 68 addge01d φ 0 if N B 2 N 0 2 N 2 N + if N B 2 N 0
70 65 69 mpbid φ 2 N 2 N + if N B 2 N 0
71 70 ad2antrr φ C N N A 2 N 2 N + if N B 2 N 0
72 iftrue N A if N A 2 N 0 = 2 N
73 72 adantl φ C N N A if N A 2 N 0 = 2 N
74 73 oveq1d φ C N N A if N A 2 N 0 + if N B 2 N 0 = 2 N + if N B 2 N 0
75 71 74 breqtrrd φ C N N A 2 N if N A 2 N 0 + if N B 2 N 0
76 ifcl 2 N 0 0 0 if N A 2 N 0 0
77 62 49 76 sylancl φ if N A 2 N 0 0
78 77 nn0ge0d φ 0 if N A 2 N 0
79 12 adantr φ N A 2 N
80 0red φ ¬ N A 0
81 79 80 ifclda φ if N A 2 N 0
82 12 81 addge02d φ 0 if N A 2 N 0 2 N if N A 2 N 0 + 2 N
83 78 82 mpbid φ 2 N if N A 2 N 0 + 2 N
84 83 ad2antrr φ C N N B 2 N if N A 2 N 0 + 2 N
85 iftrue N B if N B 2 N 0 = 2 N
86 85 adantl φ C N N B if N B 2 N 0 = 2 N
87 86 oveq2d φ C N N B if N A 2 N 0 + if N B 2 N 0 = if N A 2 N 0 + 2 N
88 84 87 breqtrrd φ C N N B 2 N if N A 2 N 0 + if N B 2 N 0
89 75 88 jaodan φ C N N A N B 2 N if N A 2 N 0 + if N B 2 N 0
90 13 13 44 59 61 89 le2addd φ C N N A N B 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
91 90 ex φ C N N A N B 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
92 ioran ¬ N A N B ¬ N A ¬ N B
93 iffalse ¬ N A if N A 2 N 0 = 0
94 93 ad2antrl φ C N ¬ N A ¬ N B if N A 2 N 0 = 0
95 iffalse ¬ N B if N B 2 N 0 = 0
96 95 ad2antll φ C N ¬ N A ¬ N B if N B 2 N 0 = 0
97 94 96 oveq12d φ C N ¬ N A ¬ N B if N A 2 N 0 + if N B 2 N 0 = 0 + 0
98 00id 0 + 0 = 0
99 97 98 eqtrdi φ C N ¬ N A ¬ N B if N A 2 N 0 + if N B 2 N 0 = 0
100 99 oveq2d φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 = K A 0 ..^ N + K B 0 ..^ N + 0
101 32 nn0red φ K A 0 ..^ N
102 101 ad2antrr φ C N ¬ N A ¬ N B K A 0 ..^ N
103 41 nn0red φ K B 0 ..^ N
104 103 ad2antrr φ C N ¬ N A ¬ N B K B 0 ..^ N
105 102 104 readdcld φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N
106 105 recnd φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N
107 106 addid1d φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N + 0 = K A 0 ..^ N + K B 0 ..^ N
108 100 107 eqtrd φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 = K A 0 ..^ N + K B 0 ..^ N
109 5 fveq1i K A 0 ..^ N = bits 0 -1 A 0 ..^ N
110 109 fveq2i bits 0 K A 0 ..^ N = bits 0 bits 0 -1 A 0 ..^ N
111 32 fvresd φ bits 0 K A 0 ..^ N = bits K A 0 ..^ N
112 f1ocnvfv2 bits 0 : 0 1-1 onto 𝒫 0 Fin A 0 ..^ N 𝒫 0 Fin bits 0 bits 0 -1 A 0 ..^ N = A 0 ..^ N
113 23 22 112 sylancr φ bits 0 bits 0 -1 A 0 ..^ N = A 0 ..^ N
114 110 111 113 3eqtr3a φ bits K A 0 ..^ N = A 0 ..^ N
115 114 18 eqsstrdi φ bits K A 0 ..^ N 0 ..^ N
116 32 nn0zd φ K A 0 ..^ N
117 bitsfzo K A 0 ..^ N N 0 K A 0 ..^ N 0 ..^ 2 N bits K A 0 ..^ N 0 ..^ N
118 116 4 117 syl2anc φ K A 0 ..^ N 0 ..^ 2 N bits K A 0 ..^ N 0 ..^ N
119 115 118 mpbird φ K A 0 ..^ N 0 ..^ 2 N
120 elfzolt2 K A 0 ..^ N 0 ..^ 2 N K A 0 ..^ N < 2 N
121 119 120 syl φ K A 0 ..^ N < 2 N
122 5 fveq1i K B 0 ..^ N = bits 0 -1 B 0 ..^ N
123 122 fveq2i bits 0 K B 0 ..^ N = bits 0 bits 0 -1 B 0 ..^ N
124 41 fvresd φ bits 0 K B 0 ..^ N = bits K B 0 ..^ N
125 f1ocnvfv2 bits 0 : 0 1-1 onto 𝒫 0 Fin B 0 ..^ N 𝒫 0 Fin bits 0 bits 0 -1 B 0 ..^ N = B 0 ..^ N
126 23 39 125 sylancr φ bits 0 bits 0 -1 B 0 ..^ N = B 0 ..^ N
127 123 124 126 3eqtr3a φ bits K B 0 ..^ N = B 0 ..^ N
128 127 35 eqsstrdi φ bits K B 0 ..^ N 0 ..^ N
129 41 nn0zd φ K B 0 ..^ N
130 bitsfzo K B 0 ..^ N N 0 K B 0 ..^ N 0 ..^ 2 N bits K B 0 ..^ N 0 ..^ N
131 129 4 130 syl2anc φ K B 0 ..^ N 0 ..^ 2 N bits K B 0 ..^ N 0 ..^ N
132 128 131 mpbird φ K B 0 ..^ N 0 ..^ 2 N
133 elfzolt2 K B 0 ..^ N 0 ..^ 2 N K B 0 ..^ N < 2 N
134 132 133 syl φ K B 0 ..^ N < 2 N
135 101 103 12 12 121 134 lt2addd φ K A 0 ..^ N + K B 0 ..^ N < 2 N + 2 N
136 135 ad2antrr φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N < 2 N + 2 N
137 108 136 eqbrtrd φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 < 2 N + 2 N
138 81 ad2antrr φ C N ¬ N A ¬ N B if N A 2 N 0
139 68 ad2antrr φ C N ¬ N A ¬ N B if N B 2 N 0
140 138 139 readdcld φ C N ¬ N A ¬ N B if N A 2 N 0 + if N B 2 N 0
141 105 140 readdcld φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
142 12 ad2antrr φ C N ¬ N A ¬ N B 2 N
143 142 142 readdcld φ C N ¬ N A ¬ N B 2 N + 2 N
144 141 143 ltnled φ C N ¬ N A ¬ N B K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 < 2 N + 2 N ¬ 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
145 137 144 mpbid φ C N ¬ N A ¬ N B ¬ 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
146 145 ex φ C N ¬ N A ¬ N B ¬ 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
147 92 146 syl5bi φ C N ¬ N A N B ¬ 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
148 91 147 impcon4bid φ C N N A N B 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
149 8 148 bitrd φ C N cadd N A N B C N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
150 cad0 ¬ C N cadd N A N B C N N A N B
151 150 adantl φ ¬ C N cadd N A N B C N N A N B
152 42 nn0ge0d φ 0 K A 0 ..^ N + K B 0 ..^ N
153 12 12 readdcld φ 2 N + 2 N
154 153 43 addge02d φ 0 K A 0 ..^ N + K B 0 ..^ N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + 2 N + 2 N
155 152 154 mpbid φ 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + 2 N + 2 N
156 155 ad2antrr φ ¬ C N N A N B 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + 2 N + 2 N
157 72 85 oveqan12d N A N B if N A 2 N 0 + if N B 2 N 0 = 2 N + 2 N
158 157 adantl φ ¬ C N N A N B if N A 2 N 0 + if N B 2 N 0 = 2 N + 2 N
159 158 oveq2d φ ¬ C N N A N B K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 = K A 0 ..^ N + K B 0 ..^ N + 2 N + 2 N
160 156 159 breqtrrd φ ¬ C N N A N B 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
161 160 ex φ ¬ C N N A N B 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
162 101 adantr φ ¬ C N K A 0 ..^ N
163 103 adantr φ ¬ C N K B 0 ..^ N
164 162 163 readdcld φ ¬ C N K A 0 ..^ N + K B 0 ..^ N
165 12 adantr φ ¬ C N 2 N
166 12 43 lenltd φ 2 N K A 0 ..^ N + K B 0 ..^ N ¬ K A 0 ..^ N + K B 0 ..^ N < 2 N
167 6 166 bitrd φ C N ¬ K A 0 ..^ N + K B 0 ..^ N < 2 N
168 167 con2bid φ K A 0 ..^ N + K B 0 ..^ N < 2 N ¬ C N
169 168 biimpar φ ¬ C N K A 0 ..^ N + K B 0 ..^ N < 2 N
170 164 165 165 169 ltadd1dd φ ¬ C N K A 0 ..^ N + K B 0 ..^ N + 2 N < 2 N + 2 N
171 164 165 readdcld φ ¬ C N K A 0 ..^ N + K B 0 ..^ N + 2 N
172 153 adantr φ ¬ C N 2 N + 2 N
173 43 58 readdcld φ K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
174 173 adantr φ ¬ C N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
175 ltletr K A 0 ..^ N + K B 0 ..^ N + 2 N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 K A 0 ..^ N + K B 0 ..^ N + 2 N < 2 N + 2 N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 K A 0 ..^ N + K B 0 ..^ N + 2 N < K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
176 171 172 174 175 syl3anc φ ¬ C N K A 0 ..^ N + K B 0 ..^ N + 2 N < 2 N + 2 N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 K A 0 ..^ N + K B 0 ..^ N + 2 N < K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
177 170 176 mpand φ ¬ C N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 K A 0 ..^ N + K B 0 ..^ N + 2 N < K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
178 58 adantr φ ¬ C N if N A 2 N 0 + if N B 2 N 0
179 43 adantr φ ¬ C N K A 0 ..^ N + K B 0 ..^ N
180 165 178 179 ltadd2d φ ¬ C N 2 N < if N A 2 N 0 + if N B 2 N 0 K A 0 ..^ N + K B 0 ..^ N + 2 N < K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
181 177 180 sylibrd φ ¬ C N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 2 N < if N A 2 N 0 + if N B 2 N 0
182 12 58 ltnled φ 2 N < if N A 2 N 0 + if N B 2 N 0 ¬ if N A 2 N 0 + if N B 2 N 0 2 N
183 64 nn0cnd φ if N B 2 N 0
184 183 addid2d φ 0 + if N B 2 N 0 = if N B 2 N 0
185 12 leidd φ 2 N 2 N
186 62 nn0ge0d φ 0 2 N
187 breq1 2 N = if N B 2 N 0 2 N 2 N if N B 2 N 0 2 N
188 breq1 0 = if N B 2 N 0 0 2 N if N B 2 N 0 2 N
189 187 188 ifboth 2 N 2 N 0 2 N if N B 2 N 0 2 N
190 185 186 189 syl2anc φ if N B 2 N 0 2 N
191 184 190 eqbrtrd φ 0 + if N B 2 N 0 2 N
192 93 oveq1d ¬ N A if N A 2 N 0 + if N B 2 N 0 = 0 + if N B 2 N 0
193 192 breq1d ¬ N A if N A 2 N 0 + if N B 2 N 0 2 N 0 + if N B 2 N 0 2 N
194 191 193 syl5ibrcom φ ¬ N A if N A 2 N 0 + if N B 2 N 0 2 N
195 194 con1d φ ¬ if N A 2 N 0 + if N B 2 N 0 2 N N A
196 77 nn0cnd φ if N A 2 N 0
197 196 addid1d φ if N A 2 N 0 + 0 = if N A 2 N 0
198 breq1 2 N = if N A 2 N 0 2 N 2 N if N A 2 N 0 2 N
199 breq1 0 = if N A 2 N 0 0 2 N if N A 2 N 0 2 N
200 198 199 ifboth 2 N 2 N 0 2 N if N A 2 N 0 2 N
201 185 186 200 syl2anc φ if N A 2 N 0 2 N
202 197 201 eqbrtrd φ if N A 2 N 0 + 0 2 N
203 95 oveq2d ¬ N B if N A 2 N 0 + if N B 2 N 0 = if N A 2 N 0 + 0
204 203 breq1d ¬ N B if N A 2 N 0 + if N B 2 N 0 2 N if N A 2 N 0 + 0 2 N
205 202 204 syl5ibrcom φ ¬ N B if N A 2 N 0 + if N B 2 N 0 2 N
206 205 con1d φ ¬ if N A 2 N 0 + if N B 2 N 0 2 N N B
207 195 206 jcad φ ¬ if N A 2 N 0 + if N B 2 N 0 2 N N A N B
208 182 207 sylbid φ 2 N < if N A 2 N 0 + if N B 2 N 0 N A N B
209 208 adantr φ ¬ C N 2 N < if N A 2 N 0 + if N B 2 N 0 N A N B
210 181 209 syld φ ¬ C N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0 N A N B
211 161 210 impbid φ ¬ C N N A N B 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
212 151 211 bitrd φ ¬ C N cadd N A N B C N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
213 149 212 pm2.61dan φ cadd N A N B C N 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
214 1 2 3 4 sadcp1 φ C N + 1 cadd N A N B C N
215 2cnd φ 2
216 215 4 expp1d φ 2 N + 1 = 2 N 2
217 11 nncnd φ 2 N
218 217 times2d φ 2 N 2 = 2 N + 2 N
219 216 218 eqtrd φ 2 N + 1 = 2 N + 2 N
220 5 bitsinvp1 A 0 N 0 K A 0 ..^ N + 1 = K A 0 ..^ N + if N A 2 N 0
221 1 4 220 syl2anc φ K A 0 ..^ N + 1 = K A 0 ..^ N + if N A 2 N 0
222 5 bitsinvp1 B 0 N 0 K B 0 ..^ N + 1 = K B 0 ..^ N + if N B 2 N 0
223 2 4 222 syl2anc φ K B 0 ..^ N + 1 = K B 0 ..^ N + if N B 2 N 0
224 221 223 oveq12d φ K A 0 ..^ N + 1 + K B 0 ..^ N + 1 = K A 0 ..^ N + if N A 2 N 0 + K B 0 ..^ N + if N B 2 N 0
225 32 nn0cnd φ K A 0 ..^ N
226 41 nn0cnd φ K B 0 ..^ N
227 225 196 226 183 add4d φ K A 0 ..^ N + if N A 2 N 0 + K B 0 ..^ N + if N B 2 N 0 = K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
228 224 227 eqtrd φ K A 0 ..^ N + 1 + K B 0 ..^ N + 1 = K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
229 219 228 breq12d φ 2 N + 1 K A 0 ..^ N + 1 + K B 0 ..^ N + 1 2 N + 2 N K A 0 ..^ N + K B 0 ..^ N + if N A 2 N 0 + if N B 2 N 0
230 213 214 229 3bitr4d φ C N + 1 2 N + 1 K A 0 ..^ N + 1 + K B 0 ..^ N + 1