def blin
bend-osdev-gf@0.1.1.0 · PROOF.bend:173
import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
import Base
173def blin(+a: Bool, +b: Bool, +u: Bool, +v: Bool, +q: Bool) -> {Bool.xor(Bool.xor(a, b), Bool.and(Bool.xor(u, v), q)) == Bool.xor(Bool.xor(a, Bool.and(u, q)), Bool.xor(b, Bool.and(v, q))) : Bool}:
174 match a:
175 case True{}:
176 match b:
177 case True{}:
178 match u:
179 case True{}:
180 match v:
181 case True{}:
182 match q:
183 case True{}:
184 {==}
185 case False{}:
186 {==}
187 case False{}:
188 match q:
189 case True{}:
190 {==}
191 case False{}:
192 {==}
193 case False{}:
194 match v:
195 case True{}:
196 match q:
197 case True{}:
198 {==}
199 case False{}:
200 {==}
201 case False{}:
202 match q:
203 case True{}:
204 {==}
205 case False{}:
206 {==}
207 case False{}:
208 match u:
209 case True{}:
210 match v:
211 case True{}:
212 match q:
213 case True{}:
214 {==}
215 case False{}:
216 {==}
217 case False{}:
218 match q:
219 case True{}:
220 {==}
221 case False{}:
222 {==}
223 case False{}:
224 match v:
225 case True{}:
226 match q:
227 case True{}:
228 {==}
229 case False{}:
230 {==}
231 case False{}:
232 match q:
233 case True{}:
234 {==}
235 case False{}:
236 {==}
237 case False{}:
238 match b:
239 case True{}:
240 match u:
241 case True{}:
242 match v:
243 case True{}:
244 match q:
245 case True{}:
246 {==}
247 case False{}:
248 {==}
249 case False{}:
250 match q:
251 case True{}:
252 {==}
253 case False{}:
254 {==}
255 case False{}:
256 match v:
257 case True{}:
258 match q:
259 case True{}:
260 {==}
261 case False{}:
262 {==}
263 case False{}:
264 match q:
265 case True{}:
266 {==}
267 case False{}:
268 {==}
269 case False{}:
270 match u:
271 case True{}:
272 match v:
273 case True{}:
274 match q:
275 case True{}:
276 {==}
277 case False{}:
278 {==}
279 case False{}:
280 match q:
281 case True{}:
282 {==}
283 case False{}:
284 {==}
285 case False{}:
286 match v:
287 case True{}:
288 match q:
289 case True{}:
290 {==}
291 case False{}:
292 {==}
293 case False{}:
294 match q:
295 case True{}:
296 {==}
297 case False{}:
298 {==}