def ws.or_zero
bend-osdev-word64@0.1.1.0 · proof_shift.bend:332
import bend-osdev-word64@0.1.1.0/proof_shift.bend as ProofShift
import Base
332def ws.or_zero(n: Nat, w: Word(n)) -> {Word.or(n, w, Word.zero(n)) == w : Word(n)}:
333 match n:
334 case 0n:
335 match w:
336 case WNil{}:
337 {==}
338 case 1n+ +p:
339 match w:
340 case WCon{False{}, +t}:
341 ws.wcon_cong(p, False{}, Word.or(p, t, Word.zero(p)), t, ws.or_zero(p, t))
342 case WCon{True{}, +t}:
343 ws.wcon_cong(p, True{}, Word.or(p, t, Word.zero(p)), t, ws.or_zero(p, t))