def bits.bound_a
bend-osdev-caps@0.1.0.0 · PROOF.bend:218
import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C
218def bits.bound_a(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), a), Word.or(n, b, Word.or(n, i, a))) == True{} : Bool}:
219 match n:
220 case 0n:
221 {==}
222 case 1n+n1:
223 match i fi fp b a:
224 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
225 bits.bound_a(n1, it, fit, fpt, bt, at)
226 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
227 bits.bound_a(n1, it, fit, fpt, bt, at)
228 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
229 bits.bound_a(n1, it, fit, fpt, bt, at)
230 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
231 bits.bound_a(n1, it, fit, fpt, bt, at)
232 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
233 bits.bound_a(n1, it, fit, fpt, bt, at)
234 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
235 bits.bound_a(n1, it, fit, fpt, bt, at)
236 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
237 bits.bound_a(n1, it, fit, fpt, bt, at)
238 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
239 bits.bound_a(n1, it, fit, fpt, bt, at)
240 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
241 bits.bound_a(n1, it, fit, fpt, bt, at)
242 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
243 bits.bound_a(n1, it, fit, fpt, bt, at)
244 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
245 bits.bound_a(n1, it, fit, fpt, bt, at)
246 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
247 bits.bound_a(n1, it, fit, fpt, bt, at)
248 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
249 bits.bound_a(n1, it, fit, fpt, bt, at)
250 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
251 bits.bound_a(n1, it, fit, fpt, bt, at)
252 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
253 bits.bound_a(n1, it, fit, fpt, bt, at)
254 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
255 bits.bound_a(n1, it, fit, fpt, bt, at)
256 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
257 bits.bound_a(n1, it, fit, fpt, bt, at)
258 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
259 bits.bound_a(n1, it, fit, fpt, bt, at)
260 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
261 bits.bound_a(n1, it, fit, fpt, bt, at)
262 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
263 bits.bound_a(n1, it, fit, fpt, bt, at)
264 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
265 bits.bound_a(n1, it, fit, fpt, bt, at)
266 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
267 bits.bound_a(n1, it, fit, fpt, bt, at)
268 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
269 bits.bound_a(n1, it, fit, fpt, bt, at)
270 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
271 bits.bound_a(n1, it, fit, fpt, bt, at)
272 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
273 bits.bound_a(n1, it, fit, fpt, bt, at)
274 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
275 bits.bound_a(n1, it, fit, fpt, bt, at)
276 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
277 bits.bound_a(n1, it, fit, fpt, bt, at)
278 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
279 bits.bound_a(n1, it, fit, fpt, bt, at)
280 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
281 bits.bound_a(n1, it, fit, fpt, bt, at)
282 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
283 bits.bound_a(n1, it, fit, fpt, bt, at)
284 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
285 bits.bound_a(n1, it, fit, fpt, bt, at)
286 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
287 bits.bound_a(n1, it, fit, fpt, bt, at)