def flag_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divq.bend:36

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

36def flag_v(+d1: U32, +d2: U32, +r2w: WU.U64) -> {Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))) == Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))) : Bool}:
37  +f1 = Equal.cong(Bool, Bool, t => Bool.or(Bool.not(t), Bool.not(U32.is_zero(U32.and(d2, 3)))), X.is_zero(r2w), Nat.is_eq(SW.value(r2w), 0n), WA.is_zero_value(r2w))
38  +f2 = Equal.cong(Bool, Bool, t => Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(t)), U32.is_zero(U32.and(d2, 3)), Nat.is_eq(v(U32.and(d2, 3)), 0n), LW.zero_nat(U32.and(d2, 3)))
39  +f3 = Equal.cong(Nat, Bool, t => Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(t, 0n))), v(U32.and(d2, 3)), C.low(2n, SW.value(WU.U64{d2, d1})), Equal.trans(Nat, v(U32.and(d2, 3)), C.low(2n, v(d2)), C.low(2n, SW.value(WU.U64{d2, d1})), FB.andm(d2, 2n, 3, {==}), lowq(d1, d2)))
40  Equal.trans(Bool, Bool.or(F.nz(r2w), Bool.not(U32.is_zero(U32.and(d2, 3)))), Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(U32.is_zero(U32.and(d2, 3)))), Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))), f1, Equal.trans(Bool, Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(U32.is_zero(U32.and(d2, 3)))), Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(v(U32.and(d2, 3)), 0n))), Bool.or(Bool.not(Nat.is_eq(SW.value(r2w), 0n)), Bool.not(Nat.is_eq(C.low(2n, SW.value(WU.U64{d2, d1})), 0n))), f2, f3))