theorem Auto.Embedding.Lam.BVLems.toNat_ofNat (n a : Nat) : (BitVec.ofNat n a).toNat = a % 2 ^ n

theorem Auto.Embedding.Lam.BVLems.toNat_ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : (i#'p).toNat = i

theorem Auto.Embedding.Lam.BVLems.toNat_le {n : Nat} (a : BitVec n) : a.toNat < 2 ^ n

theorem Auto.Embedding.Lam.BVLems.eq_of_val_eq {n : Nat} {a b : BitVec n} (h : a.toNat = b.toNat) : a = b

theorem Auto.Embedding.Lam.BVLems.val_eq_of_eq {n : Nat} {a b : BitVec n} (h : a = b) : a.toNat = b.toNat

theorem Auto.Embedding.Lam.BVLems.eq_iff_val_eq {n : Nat} {a b : BitVec n} : a = b ↔ a.toNat = b.toNat

theorem Auto.Embedding.Lam.BVLems.ne_of_val_ne {n : Nat} {a b : BitVec n} (h : a.toNat ≠ b.toNat) : a ≠ b

theorem Auto.Embedding.Lam.BVLems.val_ne_of_ne {n : Nat} {a b : BitVec n} (h : a ≠ b) : a.toNat ≠ b.toNat

theorem Auto.Embedding.Lam.BVLems.ne_iff_val_ne {n : Nat} {a b : BitVec n} : a ≠ b ↔ a.toNat ≠ b.toNat

theorem Auto.Embedding.Lam.BVLems.shiftLeft_def {n : Nat} (a : BitVec n) (i : Nat) : a <<< i = a.shiftLeft i

theorem Auto.Embedding.Lam.BVLems.smtshiftLeft_def {n m : Nat} (a : BitVec n) (b : BitVec m) : a <<< b = a <<< b.toNat

theorem Auto.Embedding.Lam.BVLems.ushiftRight_def {n : Nat} (a : BitVec n) (i : Nat) : a >>> i = a.ushiftRight i

theorem Auto.Embedding.Lam.BVLems.smtushiftRight_def {n m : Nat} (a : BitVec n) (b : BitVec m) : a >>> b = a >>> b.toNat

theorem Auto.Embedding.Lam.BVLems.neg_def {n : Nat} (a : BitVec n) : -a = a.neg

theorem Auto.Embedding.Lam.BVLems.sub_def {n : Nat} (a b : BitVec n) : a - b = a.sub b

theorem Auto.Embedding.Lam.BVLems.toNat_shiftLeft {n : Nat} {a : BitVec n} (i : Nat) : (a <<< i).toNat = a.toNat * 2 ^ i % 2 ^ n

theorem Auto.Embedding.Lam.BVLems.toNat_ushiftRight {n : Nat} {a : BitVec n} (i : Nat) : (a >>> i).toNat = a.toNat / 2 ^ i

theorem Auto.Embedding.Lam.BVLems.toNat_zeroExtend' {n m : Nat} {a : BitVec n} (le : n ≤ m) : (BitVec.setWidth' le a).toNat = a.toNat

theorem Auto.Embedding.Lam.BVLems.toNat_zeroExtend {n : Nat} {a : BitVec n} (i : Nat) : (BitVec.zeroExtend i a).toNat = a.toNat % 2 ^ i

theorem Auto.Embedding.Lam.BVLems.toNat_sub {n : Nat} (a b : BitVec n) : (a - b).toNat = (2 ^ n - b.toNat + a.toNat) % 2 ^ n

theorem Auto.Embedding.Lam.BVLems.toNat_sub' {n : Nat} (a b : BitVec n) : (a - b).toNat = (a.toNat + (2 ^ n - b.toNat)) % 2 ^ n

theorem Auto.Embedding.Lam.BVLems.toNat_neg {n : Nat} (a : BitVec n) : (-a).toNat = (2 ^ n - a.toNat) % 2 ^ n

theorem Auto.Embedding.Lam.BVLems.toNat_and {n : Nat} (a b : BitVec n) : (a &&& b).toNat = a.toNat &&& b.toNat

theorem Auto.Embedding.Lam.BVLems.toNat_or {n : Nat} (a b : BitVec n) : (a ||| b).toNat = a.toNat ||| b.toNat

theorem Auto.Embedding.Lam.BVLems.toNat_xor {n : Nat} (a b : BitVec n) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat

theorem Auto.Embedding.Lam.BVLems.toNat_not {n : Nat} (a : BitVec n) : (~~~a).toNat = 2 ^ n - 1 - a.toNat

theorem Auto.Embedding.Lam.BVLems.shiftLeft_ge_length_eq_zero {n : Nat} (a : BitVec n) (i : Nat) : i ≥ n → a <<< i = 0#n

theorem Auto.Embedding.Lam.BVLems.ushiftRight_ge_length_eq_zero {n : Nat} (a : BitVec n) (i : Nat) : i ≥ n → a >>> i = 0#n

theorem Auto.Embedding.Lam.BVLems.ushiftRight_ge_length_eq_zero' {n : Nat} (a : BitVec n) (i : Nat) : i ≥ n → BitVec.ofNat n (a.toNat >>> i) = 0#n

theorem Auto.Embedding.Lam.BVLems.msb_equiv_lt {n : Nat} (a : BitVec n) : (!a.msb) = true ↔ a.toNat < 2 ^ (n - 1)

theorem Auto.Embedding.Lam.BVLems.msb_equiv_lt' {n : Nat} (a : BitVec n) : (!a.msb) = true ↔ 2 * a.toNat < 2 ^ n

theorem Auto.Embedding.Lam.BVLems.sshiftRight_ge_length_eq_msb {n : Nat} (a : BitVec n) (i : Nat) : i ≥ n → a.sshiftRight i = if a.msb = true then (1#n).neg else 0#n

theorem Auto.Embedding.Lam.BVLems.shiftRight_eq_zero_iff {n : Nat} (a : BitVec n) (b : Nat) : a >>> b = 0#n ↔ a.toNat < 2 ^ b

theorem Auto.Embedding.Lam.BVLems.ofNat_toNat {n m : Nat} (a : BitVec n) : BitVec.ofNat m a.toNat = BitVec.zeroExtend m a

theorem Auto.Embedding.Lam.BVLems.ofNat_add (n a b : Nat) : BitVec.ofNat n (a + b) = BitVec.ofNat n a + BitVec.ofNat n b

theorem Auto.Embedding.Lam.BVLems.ofNat_mod_pow2 (n a : Nat) : BitVec.ofNat n (a % 2 ^ n) = BitVec.ofNat n a

theorem Auto.Embedding.Lam.BVLems.ofNat_sub (n a b : Nat) : BitVec.ofNat n (a - b) = if a < b then 0#n else BitVec.ofNat n a - BitVec.ofNat n b

theorem Auto.Embedding.Lam.BVLems.ofNat_sub' (n a b : Nat) : BitVec.ofNat n (a - b) = (Bool.ite' (a < b) { down := 0#n } { down := BitVec.ofNat n a - BitVec.ofNat n b }).down

theorem Auto.Embedding.Lam.BVLems.ofNat_mul (n a b : Nat) : BitVec.ofNat n (a * b) = BitVec.ofNat n a * BitVec.ofNat n b

theorem Auto.Embedding.Lam.BVLems.shl_equiv {n : Nat} (a : BitVec n) (b : Nat) : a <<< b = if b < n then a <<< BitVec.ofNat n b else 0

theorem Auto.Embedding.Lam.BVLems.shl_equiv' {n : Nat} (a : BitVec n) (b : Nat) : a <<< b = (Bool.ite' (b < n) { down := a <<< BitVec.ofNat n b } { down := 0 }).down

theorem Auto.Embedding.Lam.BVLems.shl_toNat_equiv_short {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a <<< b.toNat = a <<< BitVec.zeroExtend n b

theorem Auto.Embedding.Lam.BVLems.shl_toNat_equiv_long {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m > n) : a <<< b.toNat = if b >>> BitVec.ofNat m n = 0#m then a <<< BitVec.zeroExtend n b else 0

theorem Auto.Embedding.Lam.BVLems.shl_toNat_equiv_long' {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m > n) : a <<< b.toNat = (Bool.ite' ({ down := b >>> BitVec.ofNat m n } = { down := 0#m }) { down := a <<< BitVec.zeroExtend n b } { down := 0#n }).down

theorem Auto.Embedding.Lam.BVLems.lshr_equiv {n : Nat} (a : BitVec n) (b : Nat) : a >>> b = if b < n then a >>> BitVec.ofNat n b else 0

theorem Auto.Embedding.Lam.BVLems.lshr_equiv' {n : Nat} (a : BitVec n) (b : Nat) : a >>> b = (Bool.ite' (b < n) { down := a >>> BitVec.ofNat n b } { down := 0 }).down

theorem Auto.Embedding.Lam.BVLems.lshr_toNat_equiv_short {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a >>> b.toNat = a >>> BitVec.zeroExtend n b

theorem Auto.Embedding.Lam.BVLems.lshr_toNat_equiv_long {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m > n) : a >>> b.toNat = if b >>> BitVec.ofNat m n = 0#m then a >>> BitVec.zeroExtend n b else 0

theorem Auto.Embedding.Lam.BVLems.lshr_toNat_equiv_long' {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m > n) : a >>> b.toNat = (Bool.ite' ({ down := b >>> BitVec.ofNat m n } = { down := 0#m }) { down := a >>> BitVec.zeroExtend n b } { down := 0 }).down

theorem Auto.Embedding.Lam.BVLems.ashr_equiv {n : Nat} (a : BitVec n) (b : Nat) : a.sshiftRight b = if b < n then a.sshiftRight (BitVec.ofNat n b).toNat else if a.msb = true then (1#n).neg else 0#n

theorem Auto.Embedding.Lam.BVLems.ashr_equiv' {n : Nat} (a : BitVec n) (b : Nat) : a.sshiftRight b = (Bool.ite' (b < n) { down := a.sshiftRight (BitVec.ofNat n b).toNat } (Bool.ite' ({ down := a.msb } = { down := true }) { down := (1#n).neg } { down := 0#n })).down

theorem Auto.Embedding.Lam.BVLems.ashr_toNat_equiv_short {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a.sshiftRight b.toNat = a.sshiftRight (BitVec.zeroExtend n b).toNat

theorem Auto.Embedding.Lam.BVLems.ashr_toNat_equiv_long {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m > n) : a.sshiftRight b.toNat = if b >>> BitVec.ofNat m n = 0#m then a.sshiftRight (BitVec.zeroExtend n b).toNat else if a.msb = true then (1#n).neg else 0#n

theorem Auto.Embedding.Lam.BVLems.ashr_toNat_equiv_long' {n m : Nat} (a : BitVec n) (b : BitVec m) (h : m > n) : a.sshiftRight b.toNat = (Bool.ite' ({ down := b >>> BitVec.ofNat m n } = { down := 0#m }) { down := a.sshiftRight (BitVec.zeroExtend n b).toNat } (Bool.ite' ({ down := a.msb } = { down := true }) { down := (1#n).neg } { down := 0#n })).down

theorem Auto.Embedding.Lam.LamEquiv.bvofNat {lval : LamValuation} {lctx : Nat → LamSort} {n i : Nat} : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvofNat n (LamTerm.mkNatVal i)) (LamTerm.base (LamBaseTerm.bvVal n i))

theorem Auto.Embedding.Lam.LamEquiv.bvofNat_bvtoNat {lctx : Nat → LamSort} {t : LamTerm} {n : Nat} {lval : LamValuation} {m : Nat} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base (LamBaseSort.bv n) }) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv m)) (LamTerm.mkBvofNat m (LamTerm.mkBvUOp n (BitVecConst.bvtoNat n) t)) (LamTerm.app (LamSort.base (LamBaseSort.bv n)) (LamTerm.base (LamBaseTerm.bvzeroExtend n m)) t)

theorem Auto.Embedding.Lam.LamEquiv.bvofNat_nadd {lctx : Nat → LamSort} {a b : LamTerm} {lval : LamValuation} {n : Nat} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.nat }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.nat }) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvofNat n (LamTerm.mkNatBinOp NatConst.nadd a b)) (LamTerm.mkBvBinOp n (BitVecConst.bvadd n) (LamTerm.mkBvofNat n a) (LamTerm.mkBvofNat n b))

def Auto.Embedding.Lam.LamTerm.bvofNat_nsub (n : Nat) (a b bva bvb : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamEquiv.bvofNat_nsub {lctx : Nat → LamSort} {a b : LamTerm} {lval : LamValuation} {n : Nat} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.nat }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.nat }) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvofNat n (LamTerm.mkNatBinOp NatConst.nsub a b)) (LamTerm.bvofNat_nsub n a b (LamTerm.mkBvofNat n a) (LamTerm.mkBvofNat n b))

theorem Auto.Embedding.Lam.LamEquiv.bvofNat_nmul {lctx : Nat → LamSort} {a b : LamTerm} {lval : LamValuation} {n : Nat} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.nat }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.nat }) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvofNat n (LamTerm.mkNatBinOp NatConst.nmul a b)) (LamTerm.mkBvBinOp n (BitVecConst.bvmul n) (LamTerm.mkBvofNat n a) (LamTerm.mkBvofNat n b))

def Auto.Embedding.Lam.LamTerm.shl_equiv (n : Nat) (a b bbv : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_shl_equiv {a₁ a₂ b₁ b₂ bbv₁ bbv₂ : LamTerm} {n₁ n₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) (eqbbv : bbv₁.maxEVarSucc = bbv₂.maxEVarSucc) : (shl_equiv n₁ a₁ b₁ bbv₁).maxEVarSucc = (shl_equiv n₂ a₂ b₂ bbv₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_shl_equiv {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ b₁ b₂ bbv₁ bbv₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base LamBaseSort.nat) b₁ b₂) (eqbbv : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) bbv₁ bbv₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.shl_equiv n a₁ b₁ bbv₁) (LamTerm.shl_equiv n a₂ b₂ bbv₂)

theorem Auto.Embedding.Lam.LamEquiv.shl_equiv {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.nat }) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvshl n) a b) (LamTerm.shl_equiv n a b (LamTerm.mkBvofNat n b))

@[reducible, inline]

abbrev Auto.Embedding.Lam.LamTerm.shl_toNat_equiv_short (n : Nat) (a : LamTerm) (m : Nat) (b : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_shl_toNat_equiv_short {a₁ a₂ b₁ b₂ : LamTerm} {n₁ m₁ n₂ m₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) : (shl_toNat_equiv_short n₁ a₁ m₁ b₁).maxEVarSucc = (shl_toNat_equiv_short n₂ a₂ m₂ b₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_shl_toNat_equiv_short {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ : LamTerm} {m : Nat} {b₁ b₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv m)) b₁ b₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.shl_toNat_equiv_short n a₁ m b₁) (LamTerm.shl_toNat_equiv_short n a₂ m b₂)

theorem Auto.Embedding.Lam.LamEquiv.shl_toNat_equiv_short {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {m : Nat} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base (LamBaseSort.bv m) }) (h : m ≤ n) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvshl n) a (LamTerm.mkBvUOp m (BitVecConst.bvtoNat m) b)) (LamTerm.shl_toNat_equiv_short n a m b)

@[reducible, inline]

abbrev Auto.Embedding.Lam.LamTerm.shl_toNat_equiv_long (n : Nat) (a : LamTerm) (m : Nat) (b : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_shl_toNat_equiv_long {a₁ a₂ b₁ b₂ : LamTerm} {n₁ m₁ n₂ m₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) : (shl_toNat_equiv_long n₁ a₁ m₁ b₁).maxEVarSucc = (shl_toNat_equiv_long n₂ a₂ m₂ b₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_shl_toNat_equiv_long {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ : LamTerm} {m : Nat} {b₁ b₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv m)) b₁ b₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.shl_toNat_equiv_long n a₁ m b₁) (LamTerm.shl_toNat_equiv_long n a₂ m b₂)

theorem Auto.Embedding.Lam.LamEquiv.shl_toNat_equiv_long {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {m : Nat} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base (LamBaseSort.bv m) }) (h : m > n) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvshl n) a (LamTerm.mkBvUOp m (BitVecConst.bvtoNat m) b)) (LamTerm.shl_toNat_equiv_long n a m b)

def Auto.Embedding.Lam.LamTerm.lshr_equiv (n : Nat) (a b bbv : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_lshr_equiv {a₁ a₂ b₁ b₂ bbv₁ bbv₂ : LamTerm} {n₁ n₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) (eqbbv : bbv₁.maxEVarSucc = bbv₂.maxEVarSucc) : (lshr_equiv n₁ a₁ b₁ bbv₁).maxEVarSucc = (lshr_equiv n₂ a₂ b₂ bbv₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_lshr_equiv {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ b₁ b₂ bbv₁ bbv₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base LamBaseSort.nat) b₁ b₂) (eqbbv : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) bbv₁ bbv₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.lshr_equiv n a₁ b₁ bbv₁) (LamTerm.lshr_equiv n a₂ b₂ bbv₂)

theorem Auto.Embedding.Lam.LamEquiv.lshr_equiv {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.nat }) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvlshr n) a b) (LamTerm.lshr_equiv n a b (LamTerm.mkBvofNat n b))

@[reducible, inline]

abbrev Auto.Embedding.Lam.LamTerm.lshr_toNat_equiv_short (n : Nat) (a : LamTerm) (m : Nat) (b : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_lshr_toNat_equiv_short {a₁ a₂ b₁ b₂ : LamTerm} {n₁ m₁ n₂ m₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) : (lshr_toNat_equiv_short n₁ a₁ m₁ b₁).maxEVarSucc = (lshr_toNat_equiv_short n₂ a₂ m₂ b₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_lshr_toNat_equiv_short {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ : LamTerm} {m : Nat} {b₁ b₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv m)) b₁ b₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.lshr_toNat_equiv_short n a₁ m b₁) (LamTerm.lshr_toNat_equiv_short n a₂ m b₂)

theorem Auto.Embedding.Lam.LamEquiv.lshr_toNat_equiv_short {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {m : Nat} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base (LamBaseSort.bv m) }) (h : m ≤ n) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvlshr n) a (LamTerm.mkBvUOp m (BitVecConst.bvtoNat m) b)) (LamTerm.lshr_toNat_equiv_short n a m b)

@[reducible, inline]

abbrev Auto.Embedding.Lam.LamTerm.lshr_toNat_equiv_long (n : Nat) (a : LamTerm) (m : Nat) (b : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_lshr_toNat_equiv_long {a₁ a₂ b₁ b₂ : LamTerm} {n₁ m₁ n₂ m₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) : (lshr_toNat_equiv_long n₁ a₁ m₁ b₁).maxEVarSucc = (lshr_toNat_equiv_long n₂ a₂ m₂ b₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_lshr_toNat_equiv_long {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ : LamTerm} {m : Nat} {b₁ b₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv m)) b₁ b₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.lshr_toNat_equiv_long n a₁ m b₁) (LamTerm.lshr_toNat_equiv_long n a₂ m b₂)

theorem Auto.Embedding.Lam.LamEquiv.lshr_toNat_equiv_long {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {m : Nat} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base (LamBaseSort.bv m) }) (h : m > n) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvlshr n) a (LamTerm.mkBvUOp m (BitVecConst.bvtoNat m) b)) (LamTerm.lshr_toNat_equiv_long n a m b)

def Auto.Embedding.Lam.LamTerm.ashr_equiv (n : Nat) (a b bbv : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_ashr_equiv {a₁ a₂ b₁ b₂ bbv₁ bbv₂ : LamTerm} {n₁ n₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) (eqbbv : bbv₁.maxEVarSucc = bbv₂.maxEVarSucc) : (ashr_equiv n₁ a₁ b₁ bbv₁).maxEVarSucc = (ashr_equiv n₂ a₂ b₂ bbv₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_ashr_equiv {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ b₁ b₂ bbv₁ bbv₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base LamBaseSort.nat) b₁ b₂) (eqbbv : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) bbv₁ bbv₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.ashr_equiv n a₁ b₁ bbv₁) (LamTerm.ashr_equiv n a₂ b₂ bbv₂)

theorem Auto.Embedding.Lam.LamEquiv.ashr_equiv {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.nat }) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvashr n) a b) (LamTerm.ashr_equiv n a b (LamTerm.mkBvofNat n b))

@[reducible, inline]

abbrev Auto.Embedding.Lam.LamTerm.ashr_toNat_equiv_short (n : Nat) (a : LamTerm) (m : Nat) (b : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_ashr_toNat_equiv_short {a₁ a₂ b₁ b₂ : LamTerm} {n₁ m₁ n₂ m₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) : (ashr_toNat_equiv_short n₁ a₁ m₁ b₁).maxEVarSucc = (ashr_toNat_equiv_short n₂ a₂ m₂ b₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_ashr_toNat_equiv_short {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ : LamTerm} {m : Nat} {b₁ b₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv m)) b₁ b₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.ashr_toNat_equiv_short n a₁ m b₁) (LamTerm.ashr_toNat_equiv_short n a₂ m b₂)

theorem Auto.Embedding.Lam.LamEquiv.ashr_toNat_equiv_short {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {m : Nat} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base (LamBaseSort.bv m) }) (h : m ≤ n) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvashr n) a (LamTerm.mkBvUOp m (BitVecConst.bvtoNat m) b)) (LamTerm.ashr_toNat_equiv_short n a m b)

def Auto.Embedding.Lam.LamTerm.ashr_toNat_equiv_long (n : Nat) (a : LamTerm) (m : Nat) (b : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.

theorem Auto.Embedding.Lam.LamTerm.congr_maxEVarSucc_ashr_toNat_equiv_long {a₁ a₂ b₁ b₂ : LamTerm} {n₁ m₁ n₂ m₂ : Nat} (eqa : a₁.maxEVarSucc = a₂.maxEVarSucc) (eqb : b₁.maxEVarSucc = b₂.maxEVarSucc) : (ashr_toNat_equiv_long n₁ a₁ m₁ b₁).maxEVarSucc = (ashr_toNat_equiv_long n₂ a₂ m₂ b₂).maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.congr_ashr_toNat_equiv_long {lval : LamValuation} {lctx : Nat → LamSort} {n : Nat} {a₁ a₂ : LamTerm} {m : Nat} {b₁ b₂ : LamTerm} (eqa : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) a₁ a₂) (eqb : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv m)) b₁ b₂) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.ashr_toNat_equiv_long n a₁ m b₁) (LamTerm.ashr_toNat_equiv_long n a₂ m b₂)

theorem Auto.Embedding.Lam.LamEquiv.ashr_toNat_equiv_long {lctx : Nat → LamSort} {a : LamTerm} {n : Nat} {b : LamTerm} {m : Nat} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base (LamBaseSort.bv m) }) (h : m > n) : LamEquiv lval lctx (LamSort.base (LamBaseSort.bv n)) (LamTerm.mkBvNatBinOp n (BitVecConst.bvashr n) a (LamTerm.mkBvUOp m (BitVecConst.bvtoNat m) b)) (LamTerm.ashr_toNat_equiv_long n a m b)

inductive Auto.Embedding.Lam.BVCastType : Type

• ofNat : Nat → BVCastType
• ofInt : Nat → BVCastType
• none : BVCastType

def Auto.Embedding.Lam.LamTerm.applyBVCast (ct : BVCastType) (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.applyBVCast (Auto.Embedding.Lam.BVCastType.ofNat n) t = Auto.Embedding.Lam.LamTerm.mkBvofNat n t
• Auto.Embedding.Lam.LamTerm.applyBVCast (Auto.Embedding.Lam.BVCastType.ofInt n) t = Auto.Embedding.Lam.LamTerm.mkBvofInt n t
• Auto.Embedding.Lam.LamTerm.applyBVCast Auto.Embedding.Lam.BVCastType.none t = t

def Auto.Embedding.Lam.LamTerm.pushBVCast (ct : BVCastType) (t : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.pushBVCast (Auto.Embedding.Lam.BVCastType.ofNat n) t = Auto.Embedding.Lam.LamTerm.mkBvofNat n t
• Auto.Embedding.Lam.LamTerm.pushBVCast (Auto.Embedding.Lam.BVCastType.ofInt n) t = Auto.Embedding.Lam.LamTerm.mkBvofInt n t
• Auto.Embedding.Lam.LamTerm.pushBVCast Auto.Embedding.Lam.BVCastType.none t = t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_pushBVCast {ct : BVCastType} {t : LamTerm} : (pushBVCast ct t).maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamTerm.evarEquiv_pushBVCast {ct : BVCastType} : evarEquiv fun (t : LamTerm) => some (pushBVCast ct t)

theorem Auto.Embedding.Lam.LamEquiv.pushBVCast {lctx : Nat → LamSort} {ct : BVCastType} {t : LamTerm} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := LamTerm.applyBVCast ct t, rty := s }) : LamEquiv lval lctx s (LamTerm.applyBVCast ct t) (LamTerm.pushBVCast ct t)

theorem Auto.Embedding.Lam.LamGenConv.pushBVCast {lval : LamValuation} : LamGenConv lval fun (t : LamTerm) => some (LamTerm.pushBVCast BVCastType.none t)