law or_zero

lawful-words@0.1.0.0 · proof_word.bend:1064

import Base

1064law or_zero:
1065  for +n: Nat
1066  for +a: Word(n)
1067  for +b: Word(n)
1068  for +h: {Word.to_nat(n, b) == 0n : Nat}
1069  {Word.to_nat(n, Word.or(n, a, b)) == Word.to_nat(n, a) : Nat}