theorem bv_AddSub_1043 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.add (LLVM.add (LLVM.xor (LLVM.and e_2 e_1) e_1) (LLVM.const? 1)) e ⊑ LLVM.sub e (LLVM.or e_2 (LLVM.not e_1))

theorem bv_AddSub_1152 (e : LLVM.IntW 1) (e_1 : LLVM.IntW 1) : LLVM.add e_1 e ⊑ LLVM.xor e_1 e

theorem bv_AddSub_1156 {w : ℕ} (e : LLVM.IntW w) : LLVM.add e e ⊑ LLVM.shl e (LLVM.const? 1)

theorem bv_AddSub_1164 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.add (LLVM.sub (LLVM.const? 0) e_1) e ⊑ LLVM.sub e e_1

theorem bv_AddSub_1165 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.add (LLVM.sub (LLVM.const? 0) e_1) (LLVM.sub (LLVM.const? 0) e) ⊑ LLVM.sub (LLVM.const? 0) (LLVM.add e_1 e)

theorem bv_AddSub_1176 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.add e_1 (LLVM.sub (LLVM.const? 0) e) ⊑ LLVM.sub e_1 e

theorem bv_AddSub_1202 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.add (LLVM.xor e_1 (LLVM.const? (-1))) e ⊑ LLVM.sub (LLVM.sub e (LLVM.const? 1)) e_1

theorem bv_AddSub_1295 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.add (LLVM.and e_1 e) (LLVM.xor e_1 e) ⊑ LLVM.or e_1 e

theorem bv_AddSub_1309 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.add (LLVM.and e_1 e) (LLVM.or e_1 e) ⊑ LLVM.add e_1 e

theorem bv_AddSub_1539 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.sub e_1 (LLVM.sub (LLVM.const? 0) e) ⊑ LLVM.add e_1 e

theorem bv_AddSub_1539_2 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.sub e_1 e ⊑ LLVM.add e_1 (LLVM.neg e)

theorem bv_AddSub_1556 (e : LLVM.IntW 1) (e_1 : LLVM.IntW 1) : LLVM.sub e_1 e ⊑ LLVM.xor e_1 e

theorem bv_AddSub_1560 {w : ℕ} (e : LLVM.IntW w) : LLVM.sub (LLVM.const? (-1)) e ⊑ LLVM.xor e (LLVM.const? (-1))

theorem bv_AddSub_1564 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.sub e_1 (LLVM.xor e (LLVM.const? (-1))) ⊑ LLVM.add e (LLVM.add e_1 (LLVM.const? 1))

theorem bv_AddSub_1574 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.sub e_2 (LLVM.add e_1 e) ⊑ LLVM.sub (LLVM.sub e_2 e) e_1

theorem bv_AddSub_1614 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.sub e_1 (LLVM.add e_1 e) ⊑ LLVM.sub (LLVM.const? 0) e

theorem bv_AddSub_1619 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.sub (LLVM.sub e_1 e) e_1 ⊑ LLVM.sub (LLVM.const? 0) e

theorem bv_AddSub_1624 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.sub (LLVM.or e_1 e) (LLVM.xor e_1 e) ⊑ LLVM.and e_1 e

theorem bv_AndOrXor_135 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.and (LLVM.xor e_2 e_1) e ⊑ LLVM.xor (LLVM.and e_2 e) (LLVM.and e_1 e)

theorem bv_AndOrXor_144 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.and (LLVM.or e_2 e_1) e ⊑ LLVM.and (LLVM.or e_2 (LLVM.and e_1 e)) e

theorem bv_AndOrXor_698 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.and (LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 e_1) (LLVM.const? 0)) (LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 e) (LLVM.const? 0)) ⊑ LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 (LLVM.or e_1 e)) (LLVM.const? 0)

theorem bv_AndOrXor_709 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.and (LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 e_1) e_1) (LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 e) e) ⊑ LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 (LLVM.or e_1 e)) (LLVM.or e_1 e)

theorem bv_AndOrXor_716 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.and (LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 e_1) e_2) (LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 e) e_2) ⊑ LLVM.icmp LLVM.IntPredicate.eq (LLVM.and e_2 (LLVM.and e_1 e)) e_2

theorem bv_AndOrXor_794 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.icmp LLVM.IntPredicate.sgt e_1 e) (LLVM.icmp LLVM.IntPredicate.ne e_1 e) ⊑ LLVM.icmp LLVM.IntPredicate.sgt e_1 e

theorem bv_AndOrXor_827 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.icmp LLVM.IntPredicate.eq e_1 (LLVM.const? 0)) (LLVM.icmp LLVM.IntPredicate.eq e (LLVM.const? 0)) ⊑ LLVM.icmp LLVM.IntPredicate.eq (LLVM.or e_1 e) (LLVM.const? 0)

theorem bv_AndOrXor_887_2 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.icmp LLVM.IntPredicate.eq e_1 e) (LLVM.icmp LLVM.IntPredicate.ne e_1 e) ⊑ LLVM.const? 0

theorem bv_AndOrXor_1230__A__B___A__B {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) (LLVM.xor e (LLVM.const? (-1))) ⊑ LLVM.xor (LLVM.or e_1 e) (LLVM.const? (-1))

theorem bv_AndOrXor_1241_AB__AB__AB {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.or e_1 e) (LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1))) ⊑ LLVM.xor e_1 e

theorem bv_AndOrXor_1247_AB__AB__AB {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1))) (LLVM.or e_1 e) ⊑ LLVM.xor e_1 e

theorem bv_AndOrXor_1253_A__AB___A__B {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.xor e_1 e) e_1 ⊑ LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_1280_ABA___AB {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e) e_1 ⊑ LLVM.and e_1 e

theorem bv_AndOrXor_1288_A__B__B__C__A___A__B__C {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.and (LLVM.xor e_2 e_1) (LLVM.xor (LLVM.xor e_1 e) e_2) ⊑ LLVM.and (LLVM.xor e_2 e_1) (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_1294_A__B__A__B___A__B {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.and (LLVM.or e_1 e) (LLVM.xor (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.and e_1 e

theorem bv_AndOrXor_1683_1 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.icmp LLVM.IntPredicate.ugt e_1 e) (LLVM.icmp LLVM.IntPredicate.eq e_1 e) ⊑ LLVM.icmp LLVM.IntPredicate.uge e_1 e

theorem bv_AndOrXor_1683_2 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.icmp LLVM.IntPredicate.uge e_1 e) (LLVM.icmp LLVM.IntPredicate.ne e_1 e) ⊑ LLVM.const? 1

theorem bv_AndOrXor_1704 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.icmp LLVM.IntPredicate.eq e_1 (LLVM.const? 0)) (LLVM.icmp LLVM.IntPredicate.ult e e_1) ⊑ LLVM.icmp LLVM.IntPredicate.uge (LLVM.add e_1 (LLVM.const? (-1))) e

theorem bv_AndOrXor_1705 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.icmp LLVM.IntPredicate.eq e_1 (LLVM.const? 0)) (LLVM.icmp LLVM.IntPredicate.ugt e_1 e) ⊑ LLVM.icmp LLVM.IntPredicate.uge (LLVM.add e_1 (LLVM.const? (-1))) e

theorem bv_AndOrXor_1733 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.icmp LLVM.IntPredicate.ne e_1 (LLVM.const? 0)) (LLVM.icmp LLVM.IntPredicate.ne e (LLVM.const? 0)) ⊑ LLVM.icmp LLVM.IntPredicate.ne (LLVM.or e_1 e) (LLVM.const? 0)

theorem bv_AndOrXor_2063__X__C1__C2____X__C2__C1__C2 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.or (LLVM.xor e_2 e_1) e ⊑ LLVM.xor (LLVM.or e_2 e) (LLVM.and e_1 (LLVM.not e))

theorem bv_AndOrXor_2113___A__B__A___A__B {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e) e_1 ⊑ LLVM.or e_1 e

theorem bv_AndOrXor_2118___A__B__A___A__B {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.and e_1 e) (LLVM.xor e_1 (LLVM.const? (-1))) ⊑ LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e

theorem bv_AndOrXor_2123___A__B__A__B___A__B {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.xor e_1 e) ⊑ LLVM.xor e_1 e

theorem bv_AndOrXor_2188 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.xor e_1 e

theorem bv_AndOrXor_2231__A__B__B__C__A___A__B__C {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.or (LLVM.xor e_2 e_1) (LLVM.xor (LLVM.xor e_1 e) e_2) ⊑ LLVM.or (LLVM.xor e_2 e_1) e

theorem bv_AndOrXor_2243__B__C__A__B___B__A__C {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.or (LLVM.and (LLVM.or e_2 e_1) e) e_2 ⊑ LLVM.or e_2 (LLVM.and e e_1)

theorem bv_AndOrXor_2247__A__B__A__B {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) (LLVM.xor e (LLVM.const? (-1))) ⊑ LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1))

theorem bv_AndOrXor_2263 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or e_1 (LLVM.xor e_1 e) ⊑ LLVM.or e_1 e

theorem bv_AndOrXor_2264 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or e_1 (LLVM.xor (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_2265 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.and e_1 e) (LLVM.xor e_1 e) ⊑ LLVM.or e_1 e

theorem bv_AndOrXor_2284 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or e_1 (LLVM.xor (LLVM.or e_1 e) (LLVM.const? (-1))) ⊑ LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_2285 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or e_1 (LLVM.xor (LLVM.xor e_1 e) (LLVM.const? (-1))) ⊑ LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_2297 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.or (LLVM.and e_1 e) (LLVM.xor (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.xor (LLVM.xor e_1 (LLVM.const? (-1))) e

theorem bv_AndOrXor_2367 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.or (LLVM.or e_2 e_1) e ⊑ LLVM.or (LLVM.or e_2 e) e_1

theorem bv_AndOrXor_2416 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e) (LLVM.const? (-1)) ⊑ LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_2417 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e) (LLVM.const? (-1)) ⊑ LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_2429 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1)) ⊑ LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_2430 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.or e_1 e) (LLVM.const? (-1)) ⊑ LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_2443 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.ashr (LLVM.xor e_1 (LLVM.const? (-1))) e) (LLVM.const? (-1)) ⊑ LLVM.ashr e_1 e

theorem bv_AndOrXor_2453 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.icmp LLVM.IntPredicate.slt e_1 e) (LLVM.const? (-1)) ⊑ LLVM.icmp LLVM.IntPredicate.sge e_1 e

theorem bv_AndOrXor_2475 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.sub e_1 e) (LLVM.const? (-1)) ⊑ LLVM.add e (LLVM.sub (LLVM.const? (-1)) e_1)

theorem bv_AndOrXor_2486 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.add e_1 e) (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.sub (LLVM.const? (-1)) e) e_1

theorem bv_AndOrXor_2581__BAB___A__B {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.or e_1 e) e ⊑ LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))

theorem bv_AndOrXor_2587__BAA___B__A {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.and e_1 e) e ⊑ LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e

theorem bv_AndOrXor_2595 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.and e_1 e) (LLVM.or e_1 e) ⊑ LLVM.xor e_1 e

theorem bv_AndOrXor_2607 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.xor e_1 e

theorem bv_AndOrXor_2617 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.xor e_1 e

theorem bv_AndOrXor_2627 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.xor (LLVM.xor e_2 e_1) (LLVM.or e_2 e) ⊑ LLVM.xor (LLVM.and (LLVM.xor e_2 (LLVM.const? (-1))) e) e_1

theorem bv_AndOrXor_2647 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.and e_1 e) (LLVM.xor e_1 e) ⊑ LLVM.or e_1 e

theorem bv_AndOrXor_2658 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.xor e_1 (LLVM.const? (-1))) ⊑ LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1))

theorem bv_AndOrXor_2663 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.xor (LLVM.icmp LLVM.IntPredicate.ule e_1 e) (LLVM.icmp LLVM.IntPredicate.ne e_1 e) ⊑ LLVM.icmp LLVM.IntPredicate.uge e_1 e

theorem bv_152 {w : ℕ} (e : LLVM.IntW w) : LLVM.mul e (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.const? 0) e

theorem bv_229 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.mul (LLVM.add e_2 e_1) e ⊑ LLVM.add (LLVM.mul e_2 e) (LLVM.mul e_1 e)

theorem bv_239 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.mul (LLVM.sub (LLVM.const? 0) e_1) (LLVM.sub (LLVM.const? 0) e) ⊑ LLVM.mul e_1 e

theorem bv_275 (e : LLVM.IntW 5) (e_1 : LLVM.IntW 5) : LLVM.mul (LLVM.udiv e_1 e) e ⊑ LLVM.sub e_1 (LLVM.urem e_1 e)

theorem bv_275_2 (e : LLVM.IntW 5) (e_1 : LLVM.IntW 5) : LLVM.mul (LLVM.sdiv e_1 e) e ⊑ LLVM.sub e_1 (LLVM.srem e_1 e)

theorem bv_276 (e : LLVM.IntW 5) (e_1 : LLVM.IntW 5) : LLVM.mul (LLVM.sdiv e_1 e) (LLVM.sub (LLVM.const? 0) e) ⊑ LLVM.sub (LLVM.srem e_1 e) e_1

theorem bv_276_2 (e : LLVM.IntW 5) (e_1 : LLVM.IntW 5) : LLVM.mul (LLVM.udiv e_1 e) (LLVM.sub (LLVM.const? 0) e) ⊑ LLVM.sub (LLVM.urem e_1 e) e_1

theorem bv_283 (e : LLVM.IntW 1) (e_1 : LLVM.IntW 1) : LLVM.mul e_1 e ⊑ LLVM.and e_1 e

theorem bv_290__292 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.mul (LLVM.shl (LLVM.const? 1) e_1) e ⊑ LLVM.shl e e_1

theorem bv_820 (e : LLVM.IntW 9) (e_1 : LLVM.IntW 9) : LLVM.sdiv (LLVM.sub e_1 (LLVM.srem e_1 e)) e ⊑ LLVM.sdiv e_1 e

theorem bv_820' (e : LLVM.IntW 9) (e_1 : LLVM.IntW 9) : LLVM.udiv (LLVM.sub e_1 (LLVM.urem e_1 e)) e ⊑ LLVM.udiv e_1 e

theorem bv_1030 {w : ℕ} (e : LLVM.IntW w) : LLVM.sdiv e (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.const? 0) e

theorem bv_Select_858 (e : LLVM.IntW 1) (e_1 : LLVM.IntW 1) : LLVM.select e_1 (LLVM.xor e_1 (LLVM.const? (-1))) e ⊑ LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e

theorem bv_Select_859' (e : LLVM.IntW 1) (e_1 : LLVM.IntW 1) : LLVM.select e_1 e (LLVM.xor e_1 (LLVM.const? (-1))) ⊑ LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e

theorem bv_select_1100 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.select (LLVM.const? 1) e_1 e ⊑ e_1

theorem bv_Select_1105 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.select (LLVM.const? 0) e_1 e ⊑ e

theorem bv_InstCombineShift__239 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.lshr (LLVM.shl e_1 e) e ⊑ LLVM.and e_1 (LLVM.lshr (LLVM.const? (-1)) e)

theorem bv_InstCombineShift__279 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.shl (LLVM.lshr e_1 e) e ⊑ LLVM.and e_1 (LLVM.shl (LLVM.const? (-1)) e)

theorem bv_InstCombineShift__440 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) (e_3 : LLVM.IntW w) : LLVM.shl (LLVM.xor e_3 (LLVM.and (LLVM.lshr e_2 e_1) e)) e_1 ⊑ LLVM.xor (LLVM.and e_2 (LLVM.shl e e_1)) (LLVM.shl e_3 e_1)

theorem bv_InstCombineShift__476 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) (e_3 : LLVM.IntW w) : LLVM.shl (LLVM.or (LLVM.and (LLVM.lshr e_3 e_2) e_1) e) e_2 ⊑ LLVM.or (LLVM.and e_3 (LLVM.shl e_1 e_2)) (LLVM.shl e e_2)

theorem bv_InstCombineShift__497 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.lshr (LLVM.xor e_2 e_1) e ⊑ LLVM.xor (LLVM.lshr e_2 e) (LLVM.lshr e_1 e)

theorem bv_InstCombineShift__497''' {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) (e_2 : LLVM.IntW w) : LLVM.shl (LLVM.add e_2 e_1) e ⊑ LLVM.add (LLVM.shl e_2 e) (LLVM.shl e_1 e)

theorem bv_InstCombineShift__582 {w : ℕ} (e : LLVM.IntW w) (e_1 : LLVM.IntW w) : LLVM.lshr (LLVM.shl e_1 e) e ⊑ LLVM.and e_1 (LLVM.lshr (LLVM.const? (-1)) e)