def or1

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sh.bend:285

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

285# setting bit 0: 1 + 2 half(x)
286def or1(+x: U32) -> {v(U32.or(x, 1)) == 1n+Nat.double(C.half(v(x))) : Nat}:
287  match x:
288    case U32{+w}:
289      match w:
290        case WCon{+b, +t}:
291          +e1 = Equal.cong(Word(31n), Nat, z => v(U32{WCon{True{}, z}}), Word.or(31n, t, WD.mask(31n, 0n)), t, or_zero(31n, t))
292          +ev = Equal.trans(Nat, v(U32{WCon{b, t}}), WD.uw(32n, WCon{b, t}), Nat.add(S.bit_value(b), Nat.double(WD.uw(31n, t))), UD.vw(WCon{b, t}), {==})
293          +eh = Equal.trans(Nat, C.half(v(U32{WCon{b, t}})), C.half(Nat.add(S.bit_value(b), Nat.double(WD.uw(31n, t)))), WD.uw(31n, t), Equal.cong(Nat, Nat, z => C.half(z), v(U32{WCon{b, t}}), Nat.add(S.bit_value(b), Nat.double(WD.uw(31n, t))), ev), half_bv(b, WD.uw(31n, t)))
294          +e0 = Equal.cong(Bool, Nat, z => v(U32{WCon{z, Word.or(31n, t, WD.mask(31n, 0n))}}), Bool.or(b, True{}), True{}, or_t(b))
295          Equal.trans(Nat, v(U32{WCon{Bool.or(b, True{}), Word.or(31n, t, WD.mask(31n, 0n))}}), v(U32{WCon{True{}, Word.or(31n, t, WD.mask(31n, 0n))}}), 1n+Nat.double(C.half(v(U32{WCon{b, t}}))), e0, Equal.trans(Nat, v(U32{WCon{True{}, Word.or(31n, t, WD.mask(31n, 0n))}}), v(U32{WCon{True{}, t}}), 1n+Nat.double(C.half(v(U32{WCon{b, t}}))), e1, Equal.trans(Nat, v(U32{WCon{True{}, t}}), 1n+Nat.double(WD.uw(31n, t)), 1n+Nat.double(C.half(v(U32{WCon{b, t}}))), UD.vw(WCon{True{}, t}), Equal.cong(Nat, Nat, z => 1n+Nat.double(z), WD.uw(31n, t), C.half(v(U32{WCon{b, t}})), Equal.sym(Nat, C.half(v(U32{WCon{b, t}})), WD.uw(31n, t), eh)))))