law or_split

lawful-words@0.1.0.0 · proof_word.bend:1151

import Base

1151# Or of a word with only bits from k up and a word below 2^k is their sum.
1152law or_split:
1153  for +n: Nat
1154  for +a: Word(n)
1155  for +b: Word(n)
1156  for +k: Nat
1157  for +ha: {Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) == 0n : Nat}
1158  for +hb: {Nat.is_lt(Word.to_nat(n, b), Nat.pow(2n, k)) == True{} : Bool}
1159  {Word.to_nat(n, Word.or(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}