# bitwright proof ledger v2. Generated; do not edit.
core.arith::add_and_or 231e32f29079f031059e35c9ff2c7c8d identity exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.arith::add_disjoint c21668d593d2958761d618170fb36e1a rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=991)
core.arith::add_xor_and 91a74de0aba7b7ddb91240edcadabeb2 identity exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.arith::mul_pow2 6496ccdcfe6d1bf9444d7f829bb87e6a rule exhaustive(inst=6,maxw=6,cases=5460,fired=642) sampled(inst=22,cases=1408,fired=891)
core.arith::neg_not 15e193fa568fc257d7e9a277953b4ad3 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.arith::not_neg 96eba82dd2b9705852f297d0e47405d2 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.arith::or_from_xor_and a443c4a7e3f9daf9bff105bcdadf5353 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.arith::sub_and f494f97854ab0848902d5d10e05d614e rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.arith::udiv_pow2 ba7f88934bfc987b78342932a53ee20c rule exhaustive(inst=6,maxw=6,cases=5460,fired=642) sampled(inst=22,cases=1408,fired=920)
core.arith::urem_pow2 dc139eed7a696ecabc31d530548007af rule exhaustive(inst=6,maxw=6,cases=5460,fired=642) sampled(inst=22,cases=1408,fired=892)
core.bitwise::and_absorb_or 9fd8d816ee32d581eb8d62a20c32876f rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::and_mask_disjoint 724ff9a4b679b662432c8d23dcd9fb85 rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=982)
core.bitwise::and_mask_redundant 4b04f26d37d4b772c21cf6f7c3c3c8dd rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=926)
core.bitwise::and_not_self a7155cc265a14fe9cc6247305f489835 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::or_absorb_and 0575f368bd8b21ed6f428408bf9277b9 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::or_known_ones ac0b9516b1f47ebda223602957a6db4d rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=914)
core.bitwise::or_not_self 18cda80f123e6c06993304f495dab989 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::xor_and_or 158833683befb8f7c053b44791d1009e rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::xor_not_self 30728f4168caab17ae4a4a889bcd36cb rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.casts::sext_from_sign_word ee0eb576cde4badf54fe874b005b357d rule exhaustive(inst=9,maxw=6,cases=98,fired=98) sampled(inst=190,cases=12160,fired=12160)
core.casts::trunc_and_zext 638d880dd6e9330bb45c32e910b73e9b rule exhaustive(inst=15,maxw=6,cases=1812,fired=1812) sampled(inst=359,cases=22976,fired=22976)
core.casts::zext_trunc 03adbad05bdae1e06b83d6d82f6cb943 rule exhaustive(inst=15,maxw=6,cases=516,fired=516) sampled(inst=350,cases=22400,fired=22400)
core.compare::eq_eq_distinct 6f255a110c3116629fa5e4079eb430d3 rule exhaustive(inst=5,maxw=5,cases=37448,fired=36084) sampled(inst=22,cases=1408,fired=1377)
core.compare::eq_sub_zero ca8026a4dea10e0d08061cffc2487da6 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::eq_xor_zero 17a6d95c209f639b59167b13239eaa14 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::eq_zext b39dea5b1d2ab79b1da6cc49558341c2 rule exhaustive(inst=15,maxw=6,cases=1812,fired=1812) sampled(inst=371,cases=23744,fired=23744)
core.compare::slt_sext 4357801fd5d32647845c78115b30f1c7 rule exhaustive(inst=15,maxw=6,cases=1812,fired=1812) sampled(inst=360,cases=23040,fired=23040)
core.compare::ult_one 2aed343e84cf6eef6c63488913bf5f5e rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.compare::ult_zext 8f96fb762bf7187a560b7f4b3e5cd61b rule exhaustive(inst=15,maxw=6,cases=1812,fired=1812) sampled(inst=357,cases=22848,fired=22848)
core.select::select_one_zero f389254f8f48d32f0573ee1a15809ada rule exhaustive(inst=5,maxw=6,cases=10,fired=10) sampled(inst=22,cases=1408,fired=1408)
core.select::select_ones_zero 2e36b373d0f0970a2e5fbe0ff85abc44 rule exhaustive(inst=5,maxw=6,cases=10,fired=10) sampled(inst=22,cases=1408,fired=1408)
core.shift::lshr_lshr 87af211bb3c75865cff47a3b491ddba9 rule exhaustive(inst=5,maxw=5,cases=37448,fired=702) sampled(inst=22,cases=1408,fired=86)
core.shift::lshr_shl a74d7b719fb9c7d2eb29c298c256a209 rule exhaustive(inst=6,maxw=6,cases=5460,fired=642) sampled(inst=22,cases=1408,fired=391)
core.shift::rotl_rotl 212c7db1879190f843986b16418f0f33 rule exhaustive(inst=5,maxw=5,cases=37448,fired=37448) sampled(inst=22,cases=1408,fired=1408)
core.shift::rotl_rotr 9937dde5021a4bece4aea51006fd3a78 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.shift::rotr_rotl 1811b7f0e3c2e1e5d95f0a8cddb8402a rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.shift::shl_shl efa9216e0faad669ca5020ba0de9e37d rule exhaustive(inst=5,maxw=5,cases=37448,fired=702) sampled(inst=22,cases=1408,fired=117)