def bits.nonroot

bend-osdev-caps@0.1.0.0 · PROOF.bend:604

import Base

604def bits.nonroot(+n: Nat, +i: Word(n), +b: Word(n), +a: Word(n)) -> {Word.or(n, Word.or(n, Word.and(n, i, Word.zero(n)), Word.and(n, Word.zero(n), b)), a) == a : Word(n)}:
605  match n:
606    case 0n:
607      match i b a:
608        case WNil{} WNil{} WNil{}:
609          {==}
610    case 1n+n1:
611      match i b a:
612        case WCon{True{}, +it} WCon{True{}, +bt} WCon{True{}, +at}:
613          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
614        case WCon{True{}, +it} WCon{True{}, +bt} WCon{False{}, +at}:
615          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
616        case WCon{True{}, +it} WCon{False{}, +bt} WCon{True{}, +at}:
617          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
618        case WCon{True{}, +it} WCon{False{}, +bt} WCon{False{}, +at}:
619          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
620        case WCon{False{}, +it} WCon{True{}, +bt} WCon{True{}, +at}:
621          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
622        case WCon{False{}, +it} WCon{True{}, +bt} WCon{False{}, +at}:
623          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
624        case WCon{False{}, +it} WCon{False{}, +bt} WCon{True{}, +at}:
625          Equal.cong(Word(n1), Word(1n+n1), w => WCon{True{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))
626        case WCon{False{}, +it} WCon{False{}, +bt} WCon{False{}, +at}:
627          Equal.cong(Word(n1), Word(1n+n1), w => WCon{False{}, w}, Word.or(n1, Word.or(n1, Word.and(n1, it, Word.zero(n1)), Word.and(n1, Word.zero(n1), bt)), at), at, bits.nonroot(n1, it, bt, at))