ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>cut : α → Ordering<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.All p t → Batteries.RBNode.All p (Batteries.RBNode.del cut t)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Ordered cmp (Batteries.RBNode.del cut t)
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>cut : α → Ordering<VAR>t : Batteries.RBNode α<VAR>h : t.Balanced c n<GOAL>Batteries.RBNode.DelProp t.isBlack (Batteries.RBNode.del cut t) n
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>t : Batteries.RBNode α<VAR>h : Batteries.RBNode.Ordered cmp t<GOAL>Batteries.RBNode.Ordered cmp (Batteries.RBNode.erase cut t)
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<VAR>cut : α → Ordering<VAR>t : Batteries.RBNode α<VAR>h : t.Balanced c n<GOAL>∃ n, (Batteries.RBNode.erase cut t).Balanced Batteries.RBColor.black n
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBNode α<VAR>h : Batteries.RBNode.WF cmp t<GOAL>Batteries.RBNode.Ordered cmp t ∧ ∃ c n, t.Balanced c n
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.WF cmp t ↔ Batteries.RBNode.Ordered cmp t ∧ ∃ c n, t.Balanced c n
<VAR>α : Type u_1<VAR>c : Batteries.RBColor<VAR>n : Nat<GOAL>∀ {α_1 : Type u_2} {f : α → α_1} {t : Batteries.RBNode α}, t.Balanced c n → (Batteries.RBNode.map f t).Balanced c n
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>cmpα : α → α → Ordering<VAR>cmpβ : β → β → Ordering<VAR>f : α → β<VAR>self : Batteries.RBSet.IsMonotone cmpα cmpβ f<VAR>x y : α<GOAL>Batteries.RBNode.cmpLT cmpα x y → Batteries.RBNode.cmpLT cmpβ (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>q : β → Prop<VAR>f : α → β<VAR>H : ∀ {x : α}, p x → q (f x)<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.All p t → Batteries.RBNode.All q (Batteries.RBNode.map f t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>cmpα : α → α → Ordering<VAR>cmpβ : β → β → Ordering<VAR>f : α → β<VAR>Batteries.RBSet.IsMonotone cmpα cmpβ f<VAR>t : Batteries.RBNode α<GOAL>Batteries.RBNode.Ordered cmpα t → Batteries.RBNode.Ordered cmpβ (Batteries.RBNode.map f t)
<VAR>α : Type u<VAR>Fam : α → Type v<VAR>a : α<VAR>β : semiOutParam (Type v)<VAR>self : Lake.FamilyDef Fam a β<GOAL>Fam a = β
<VAR>α : Type u<VAR>Fam : α → Type v<VAR>a : α<VAR>β : outParam (Type v)<VAR>self : Lake.FamilyOut Fam a β<GOAL>Fam a = β
<VAR>α : Type u<VAR>cmp : α → α → Ordering<VAR>self : Lake.EqOfCmp α cmp<VAR>a a' : α<GOAL>cmp a a' = Ordering.eq → a = a'
<VAR>α : Type u<VAR>cmp : α → α → Ordering<VAR>self : Lake.LawfulCmpEq α cmp<VAR>a : α<GOAL>cmp a a = Ordering.eq
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>a a' : α<VAR>Lake.LawfulCmpEq α cmp<GOAL>cmp a a' = Ordering.eq ↔ a = a'
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>cmp : α → α → Ordering<VAR>self : Lake.EqOfCmpWrt α f cmp<VAR>a a' : α<GOAL>cmp a a' = Ordering.eq → f a = f a'
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableEq α<VAR>a a' : α<VAR>Decidable (a < a')<VAR>h : compareOfLessAndEq a a' = Ordering.eq<GOAL>a = a'
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableEq α<VAR>a : α<VAR>Decidable (a < a)<VAR>lt_irrefl : ¬a < a<GOAL>compareOfLessAndEq a a = Ordering.eq
<VAR>m : Nat<VAR>n n' : Fin m<VAR>h : compare n n' = Ordering.eq<GOAL>n = n'
<VAR>α : Type u_1<VAR>LT α<VAR>irrefl_α : ∀ (a : α), ¬a < a<VAR>a : List α<GOAL>¬a < a
<VAR>m n : Lake.Name<GOAL>(m == n) = false ↔ ¬m = n
<VAR>n : Lake.Name<GOAL>n.isPrefixOf n = true
<VAR>n m : Lake.Name<GOAL>¬n.hasMacroScopes = true → ¬m.hasMacroScopes = true → n.isPrefixOf (n ++ m) = true
<VAR>n n' : Lake.Name<GOAL>n.quickCmpAux n' = Ordering.eq ↔ n = n'
<VAR>n n' : Lake.Name<GOAL>n.quickCmp n' = Ordering.eq → n = n'
<VAR>n : Lake.Name<GOAL>n.quickCmp n = Ordering.eq
<VAR>w x : Nat<VAR>lt : x < 2 ^ w<GOAL>{ toFin := ⟨x, lt⟩ } = BitVec.ofNat w x
<VAR>n : Nat<VAR>i j : BitVec n<GOAL>i.toNat = j.toNat → i = j
<VAR>w : Nat<VAR>x : BitVec w<GOAL>↑x.toFin = x.toNat
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x = y ↔ x.toNat = y.toNat
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x ≠ y ↔ x.toNat ≠ y.toNat
<VAR>w i : Nat<VAR>x : BitVec w<GOAL>x.toNat.testBit i = x.getLsb i
<VAR>n : Nat<VAR>x : Fin (2 ^ n)<VAR>i : Nat<GOAL>{ toFin := x }.getLsb i = (↑x).testBit i
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<VAR>ge : w ≤ i<GOAL>x.getLsb i = false
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<VAR>ge : w ≤ i<GOAL>x.getMsb i = false
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<GOAL>x.getLsb i = true → i < w
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<GOAL>x.getMsb i = true → i < w
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<GOAL>x.getMsb i = (decide (i < w) && x.getLsb (w - 1 - i))
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<GOAL>x.getLsb i = (decide (i < w) && x.getMsb (w - 1 - i))
<VAR>w : Nat<VAR>x y : BitVec w<VAR>pred : ∀ (i : Fin w), x.getLsb ↑i = y.getLsb ↑i<GOAL>x = y
<VAR>w : Nat<VAR>x y : BitVec w<VAR>pred : ∀ (i : Fin w), x.getMsb ↑i = y.getMsb ↑i<GOAL>x = y
<VAR>x : BitVec 0<GOAL>x = 0#0
<VAR>x : BitVec 0<GOAL>x.toNat = 0
<VAR>i : Nat<VAR>x : BitVec 0<GOAL>x.getLsb i = false
<VAR>i : Nat<VAR>x : BitVec 0<GOAL>x.getMsb i = false
<VAR>x : BitVec 0<GOAL>x.msb = false
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.toFin = y.toFin → x = y
<VAR>b : Bool<GOAL>(BitVec.ofBool b).toNat = b.toNat
<VAR>b : Bool<GOAL>(BitVec.ofBool b).msb = b
<VAR>n : Nat<GOAL>BitVec.ofNat 1 n = BitVec.ofBool (decide (n % 2 = 1))
<VAR>b b' : Bool<GOAL>BitVec.ofBool b = BitVec.ofBool b' ↔ b = b'
<VAR>b : Bool<GOAL>~~~BitVec.ofBool b = BitVec.ofBool !b
<VAR>n : Nat<VAR>x : Fin (2 ^ n)<GOAL>{ toFin := x }.toNat = ↑x
<VAR>w : Nat<VAR>x : Nat<VAR>p : x < 2 ^ w<GOAL>(x#'p).toNat = x
<VAR>n : Nat<VAR>x : Nat<VAR>lt : x < 2 ^ n<VAR>i : Nat<GOAL>(x#'lt).getLsb i = x.testBit i
<VAR>x w : Nat<GOAL>(BitVec.ofNat w x).toNat = x % 2 ^ w
<VAR>w : Nat<VAR>x : Nat<GOAL>(BitVec.ofNat w x).toFin = Fin.ofNat' x ⋯
<VAR>n x i : Nat<GOAL>(BitVec.ofNat n x).getLsb i = (decide (i < n) && x.testBit i)
<VAR>n : Nat<GOAL>(0#n).toNat = 0
<VAR>w i : Nat<GOAL>(0#w).getLsb i = false
<VAR>w i : Nat<GOAL>(0#w).getMsb i = false
<VAR>n : Nat<VAR>x : BitVec n<GOAL>x.toNat % 2 ^ n = x.toNat
<VAR>x m n : Nat<VAR>lt : x < 2 ^ m<VAR>le : m ≤ n<GOAL>x < 2 ^ n
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.msb = x.getLsb (w - 1)
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.getLsb (w - 1) = decide (2 ^ (w - 1) ≤ x.toNat)
<VAR>w : Nat<VAR>x : BitVec (w + 1)<GOAL>x.getLsb w = decide (2 ^ w ≤ x.toNat)
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.msb = decide (2 ^ (w - 1) ≤ x.toNat)
<VAR>n : Nat<VAR>x : BitVec n<VAR>p : x.msb = true<GOAL>x.toNat ≥ 2 ^ (n - 1)
<VAR>w v : Nat<VAR>h : w = v<VAR>x : BitVec w<GOAL>(BitVec.cast h x).toNat = x.toNat
<VAR>w v : Nat<VAR>h : w = v<VAR>x : BitVec w<GOAL>(BitVec.cast h x).toFin = Fin.cast ⋯ x.toFin
<VAR>w v i : Nat<VAR>h : w = v<VAR>x : BitVec w<GOAL>(BitVec.cast h x).getLsb i = x.getLsb i
<VAR>w v i : Nat<VAR>h : w = v<VAR>x : BitVec w<GOAL>(BitVec.cast h x).getMsb i = x.getMsb i
<VAR>w v : Nat<VAR>h : w = v<VAR>x : BitVec w<GOAL>(BitVec.cast h x).msb = x.msb
<VAR>n : Nat<VAR>i : BitVec n<GOAL>i.toInt = if 2 * i.toNat < 2 ^ n then ↑i.toNat else ↑i.toNat - ↑(2 ^ n)
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.msb = false ↔ 2 * x.toNat < 2 ^ w
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.msb = true ↔ 2 * x.toNat ≥ 2 ^ w
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
<VAR>n : Nat<VAR>x : BitVec n<GOAL>x.toInt = (↑x.toNat).bmod (2 ^ n)
<VAR>n : Nat<VAR>i j : BitVec n<GOAL>i.toInt = j.toInt → i = j
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x.toInt = y.toInt ↔ x = y
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x.toInt ≠ y.toInt ↔ x ≠ y
<VAR>n : Nat<VAR>i : Int<GOAL>(BitVec.ofInt n i).toNat = (i % ↑(2 ^ n)).toNat
<VAR>n : Nat<VAR>x : Nat<GOAL>(BitVec.ofNat n x).toInt = (↑x).bmod (2 ^ n)
<VAR>n : Nat<VAR>i : Int<GOAL>(BitVec.ofInt n i).toInt = i.bmod (2 ^ n)
<VAR>w n : Nat<GOAL>BitVec.ofInt w ↑n = BitVec.ofNat w n
<VAR>m n : Nat<VAR>p : m ≤ n<VAR>x : BitVec m<GOAL>(BitVec.zeroExtend' p x).toNat = x.toNat
<VAR>n : Nat<VAR>i : Nat<VAR>x : BitVec n<GOAL>(BitVec.zeroExtend i x).toNat = x.toNat % 2 ^ i
<VAR>w v : Nat<VAR>x : BitVec w<VAR>h : w ≤ v<GOAL>BitVec.zeroExtend' h x = BitVec.zeroExtend v x
<VAR>n i : Nat<VAR>x : BitVec n<GOAL>(BitVec.truncate i x).toNat = x.toNat % 2 ^ i
<VAR>n : Nat<VAR>x : BitVec n<GOAL>BitVec.zeroExtend n x = x
<VAR>m n : Nat<GOAL>BitVec.zeroExtend m 0#n = 0#m
<VAR>n : Nat<VAR>x : BitVec n<GOAL>BitVec.truncate n x = x
<VAR>n : Nat<VAR>m : Nat<VAR>x : BitVec n<GOAL>BitVec.ofNat m x.toNat = BitVec.truncate m x
<VAR>w : Nat<VAR>x : BitVec w<VAR>y : Nat<GOAL>x.toNat = y ↔ y < 2 ^ w ∧ x = BitVec.ofNat w y
<VAR>w : Nat<VAR>x : BitVec w<VAR>y : Nat<GOAL>y = x.toNat ↔ y < 2 ^ w ∧ x = BitVec.ofNat w y
<VAR>m n : Nat<VAR>ge : m ≥ n<VAR>x : BitVec n<VAR>i : Nat<GOAL>(BitVec.zeroExtend' ge x).getLsb i = x.getLsb i
<VAR>m n : Nat<VAR>ge : m ≥ n<VAR>x : BitVec n<VAR>i : Nat<GOAL>(BitVec.zeroExtend' ge x).getMsb i = (decide (i ≥ m - n) && x.getMsb (i - (m - n)))
<VAR>n : Nat<VAR>m : Nat<VAR>x : BitVec n<VAR>i : Nat<GOAL>(BitVec.zeroExtend m x).getLsb i = (decide (i < m) && x.getLsb i)
<VAR>w k i : Nat<VAR>x : BitVec w<VAR>h : k ≤ i<GOAL>(BitVec.zeroExtend (w + k) x).getMsb i = x.getMsb (i - k)
<VAR>n : Nat<VAR>m : Nat<VAR>x : BitVec n<VAR>i : Nat<GOAL>(BitVec.truncate m x).getLsb i = (decide (i < m) && x.getLsb i)
<VAR>w k : Nat<VAR>x : BitVec w<GOAL>(BitVec.truncate (k + 1) x).msb = x.getLsb k
<VAR>w k l : Nat<VAR>x : BitVec w<VAR>h : k ≤ l<GOAL>BitVec.zeroExtend k (BitVec.zeroExtend l x) = BitVec.zeroExtend k x
<VAR>w k l : Nat<VAR>x : BitVec w<VAR>h : k ≤ l<GOAL>BitVec.truncate k (BitVec.truncate l x) = BitVec.truncate k x
<VAR>w v : Nat<VAR>x : BitVec w<VAR>k : Nat<VAR>h : w = v<GOAL>BitVec.truncate k (BitVec.cast h x) = BitVec.truncate k x
<VAR>w v : Nat<VAR>x : BitVec w<GOAL>(BitVec.zeroExtend v x).msb = (decide (0 < v) && x.getLsb (v - 1))
<VAR>w v : Nat<VAR>x : BitVec w<VAR>h : w ≤ v<GOAL>(BitVec.zeroExtend' h x).msb = (decide (0 < v) && x.getLsb (v - 1))
<VAR>n : Nat<VAR>x : Fin (2 ^ n)<VAR>hi lo : Nat<GOAL>BitVec.extractLsb hi lo { toFin := x } = BitVec.ofNat (hi - lo + 1) (↑x >>> lo)
<VAR>x n hi lo : Nat<GOAL>BitVec.extractLsb hi lo (BitVec.ofNat n x) = BitVec.ofNat (hi - lo + 1) ((x % 2 ^ n) >>> lo)
<VAR>n : Nat<VAR>s m : Nat<VAR>x : BitVec n<GOAL>(BitVec.extractLsb' s m x).toNat = x.toNat >>> s % 2 ^ m
<VAR>n : Nat<VAR>hi lo : Nat<VAR>x : BitVec n<GOAL>(BitVec.extractLsb hi lo x).toNat = x.toNat >>> lo % 2 ^ (hi - lo + 1)
<VAR>n : Nat<VAR>hi lo : Nat<VAR>x : BitVec n<VAR>i : Nat<GOAL>(BitVec.extractLsb hi lo x).getLsb i = (decide (i ≤ hi - lo) && x.getLsb (lo + i))
<VAR>v : Nat<GOAL>(BitVec.allOnes v).toNat = 2 ^ v - 1
<VAR>v i : Nat<GOAL>(BitVec.allOnes v).getLsb i = decide (i < v)
<VAR>v : Nat<VAR>x y : BitVec v<GOAL>(x ||| y).toNat = x.toNat ||| y.toNat
<VAR>v : Nat<VAR>x y : BitVec v<GOAL>(x ||| y).toFin = x.toFin ||| y.toFin
<VAR>v i : Nat<VAR>x y : BitVec v<GOAL>(x ||| y).getLsb i = (x.getLsb i || y.getLsb i)
<VAR>w i : Nat<VAR>x y : BitVec w<GOAL>(x ||| y).getMsb i = (x.getMsb i || y.getMsb i)
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>(x ||| y).msb = (x.msb || y.msb)
<VAR>w k : Nat<VAR>x y : BitVec w<GOAL>BitVec.truncate k (x ||| y) = BitVec.truncate k x ||| BitVec.truncate k y
<VAR>w : Nat<VAR>x y z : BitVec w<GOAL>x ||| y ||| z = x ||| (y ||| z)
<VAR>v : Nat<VAR>x y : BitVec v<GOAL>(x &&& y).toNat = x.toNat &&& y.toNat
<VAR>v : Nat<VAR>x y : BitVec v<GOAL>(x &&& y).toFin = x.toFin &&& y.toFin
<VAR>v i : Nat<VAR>x y : BitVec v<GOAL>(x &&& y).getLsb i = (x.getLsb i && y.getLsb i)
<VAR>w i : Nat<VAR>x y : BitVec w<GOAL>(x &&& y).getMsb i = (x.getMsb i && y.getMsb i)
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>(x &&& y).msb = (x.msb && y.msb)
<VAR>w k : Nat<VAR>x y : BitVec w<GOAL>BitVec.truncate k (x &&& y) = BitVec.truncate k x &&& BitVec.truncate k y
<VAR>w : Nat<VAR>x y z : BitVec w<GOAL>x &&& y &&& z = x &&& (y &&& z)
<VAR>v : Nat<VAR>x y : BitVec v<GOAL>(x ^^^ y).toNat = x.toNat ^^^ y.toNat
<VAR>v : Nat<VAR>x y : BitVec v<GOAL>(x ^^^ y).toFin = x.toFin ^^^ y.toFin
<VAR>v i : Nat<VAR>x y : BitVec v<GOAL>(x ^^^ y).getLsb i = xor (x.getLsb i) (y.getLsb i)
<VAR>w k : Nat<VAR>x y : BitVec w<GOAL>BitVec.truncate k (x ^^^ y) = BitVec.truncate k x ^^^ BitVec.truncate k y
<VAR>w : Nat<VAR>x y z : BitVec w<GOAL>x ^^^ y ^^^ z = x ^^^ (y ^^^ z)
<VAR>v : Nat<VAR>x : BitVec v<GOAL>~~~x = BitVec.allOnes v ^^^ x
<VAR>v : Nat<VAR>x : BitVec v<GOAL>(~~~x).toNat = 2 ^ v - 1 - x.toNat
<VAR>w : Nat<VAR>x : BitVec w<GOAL>(~~~x).toFin = x.toFin.rev
<VAR>v i : Nat<VAR>x : BitVec v<GOAL>(~~~x).getLsb i = (decide (i < v) && !x.getLsb i)
<VAR>w k : Nat<VAR>x : BitVec w<VAR>h : k ≤ w<GOAL>BitVec.truncate k (~~~x) = ~~~BitVec.truncate k x
<VAR>w w' : Nat<VAR>x : BitVec w<VAR>h : w = w'<GOAL>~~~BitVec.cast h x = BitVec.cast h (~~~x)
<VAR>w w' : Nat<VAR>x y : BitVec w<VAR>h : w = w'<GOAL>BitVec.cast h x &&& BitVec.cast h y = BitVec.cast h (x &&& y)
<VAR>w w' : Nat<VAR>x y : BitVec w<VAR>h : w = w'<GOAL>BitVec.cast h x ||| BitVec.cast h y = BitVec.cast h (x ||| y)
<VAR>v n : Nat<VAR>x : BitVec v<GOAL>(x <<< n).toNat = x.toNat <<< n % 2 ^ v
<VAR>w n : Nat<VAR>x : BitVec w<GOAL>(x <<< n).toFin = Fin.ofNat' (x.toNat <<< n) ⋯
<VAR>m i : Nat<VAR>x : BitVec m<VAR>n : Nat<GOAL>(x <<< n).getLsb i = (decide (i < m) && !decide (i < n) && x.getLsb (i - n))
<VAR>w k : Nat<VAR>x : BitVec w<VAR>i : Nat<GOAL>(x <<< i).getMsb k = x.getMsb (k + i)
<VAR>w n : Nat<VAR>x : BitVec w<GOAL>x.shiftLeftZeroExtend n = BitVec.zeroExtend (w + n) x <<< n
<VAR>m i : Nat<VAR>x : BitVec m<VAR>n : Nat<GOAL>(x.shiftLeftZeroExtend n).getLsb i = (!decide (i < n) && x.getLsb (i - n))
<VAR>m i : Nat<VAR>x : BitVec m<VAR>n : Nat<GOAL>(x.shiftLeftZeroExtend n).getMsb i = x.getMsb i
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Nat<GOAL>(x.shiftLeftZeroExtend i).msb = x.msb
<VAR>w : Nat<VAR>x : BitVec w<VAR>n m : Nat<GOAL>x <<< (n + m) = x <<< n <<< m
<VAR>w : Nat<VAR>x : BitVec w<VAR>n m : Nat<GOAL>x <<< n <<< m = x <<< (n + m)
<VAR>n : Nat<VAR>x : BitVec n<VAR>i : Nat<GOAL>(x >>> i).toNat = x.toNat >>> i
<VAR>n : Nat<VAR>x : BitVec n<VAR>i j : Nat<GOAL>(x >>> i).getLsb j = x.getLsb (i + j)
<VAR>n : Nat<VAR>x : BitVec n<VAR>i : Nat<GOAL>x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i)
<VAR>w : Nat<VAR>x : BitVec w<VAR>s : Nat<VAR>h : x.msb = false<GOAL>x.sshiftRight s = x >>> s
<VAR>w : Nat<VAR>x : BitVec w<VAR>s : Nat<VAR>h : x.msb = true<GOAL>x.sshiftRight s = ~~~(~~~x >>> s)
<VAR>w : Nat<VAR>x : BitVec w<VAR>s i : Nat<GOAL>(x.sshiftRight s).getLsb i = (!decide (w ≤ i) && if s + i < w then x.getLsb (s + i) else x.msb)
<VAR>n m : Nat<VAR>hlt : n < m<GOAL>↑n - ↑m = -(↑(m - 1 - n) + 1)
<VAR>m : Nat<VAR>n : Int<GOAL>-(↑m + 1) % n = Int.subNatNat n.natAbs (m % n.natAbs + 1)
<VAR>w : Nat<VAR>x : BitVec w<VAR>v : Nat<VAR>hmsb : x.msb = false<GOAL>BitVec.signExtend v x = BitVec.zeroExtend v x
<VAR>w : Nat<VAR>x : BitVec w<VAR>v : Nat<VAR>hmsb : x.msb = true<GOAL>BitVec.signExtend v x = ~~~BitVec.zeroExtend v (~~~x)
<VAR>w : Nat<VAR>x : BitVec w<VAR>v i : Nat<GOAL>(BitVec.signExtend v x).getLsb i = (decide (i < v) && if i < w then x.getLsb i else x.msb)
<VAR>v w : Nat<VAR>x : BitVec v<VAR>y : BitVec w<GOAL>x ++ y = x.shiftLeftZeroExtend w ||| BitVec.zeroExtend' ⋯ y
<VAR>m n : Nat<VAR>x : BitVec m<VAR>y : BitVec n<GOAL>(x ++ y).toNat = x.toNat <<< n ||| y.toNat
<VAR>n m i : Nat<VAR>v : BitVec n<VAR>w : BitVec m<GOAL>(v ++ w).getLsb i = bif decide (i < m) then w.getLsb i else v.getLsb (i - m)
<VAR>n m i : Nat<VAR>v : BitVec n<VAR>w : BitVec m<GOAL>(v ++ w).getMsb i = bif decide (n ≤ i) then w.getMsb (i - n) else v.getMsb i
<VAR>w v : Nat<VAR>x : BitVec w<VAR>y : BitVec v<GOAL>(x ++ y).msb = bif w == 0 then y.msb else x.msb
<VAR>w v k : Nat<VAR>x : BitVec w<VAR>y : BitVec v<GOAL>BitVec.truncate k (x ++ y) = if h : k ≤ v then BitVec.truncate k y else BitVec.cast ⋯ (BitVec.truncate (k - v) x ++ y)
<VAR>w : Nat<VAR>a : Bool<VAR>x : BitVec w<GOAL>BitVec.truncate w (BitVec.cons a x) = x
<VAR>w v : Nat<VAR>x : BitVec w<VAR>y : BitVec v<GOAL>~~~(x ++ y) = ~~~x ++ ~~~y
<VAR>w v : Nat<VAR>x₁ x₂ : BitVec w<VAR>y₁ y₂ : BitVec v<GOAL>x₁ ++ y₁ &&& x₂ ++ y₂ = (x₁ &&& x₂) ++ (y₁ &&& y₂)
<VAR>w v : Nat<VAR>x₁ x₂ : BitVec w<VAR>y₁ y₂ : BitVec v<GOAL>x₁ ++ y₁ ||| x₂ ++ y₂ = (x₁ ||| x₂) ++ (y₁ ||| y₂)
<VAR>w v : Nat<VAR>x₁ x₂ : BitVec w<VAR>y₁ y₂ : BitVec v<GOAL>x₁ ++ y₁ ^^^ x₂ ++ y₂ = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)
<VAR>w : Nat<VAR>x : BitVec w<VAR>n m : Nat<GOAL>x >>> (n + m) = x >>> n >>> m
<VAR>w : Nat<VAR>x : BitVec w<VAR>n m : Nat<GOAL>x >>> n >>> m = x >>> (n + m)
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Fin w<GOAL>x.getLsb ↑i.rev = x.getMsb ↑i
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Fin w<GOAL>x.getMsb ↑i.rev = x.getLsb ↑i
<VAR>w : Nat<VAR>b : Bool<VAR>x : BitVec w<GOAL>(BitVec.cons b x).toNat = b.toNat <<< w ||| x.toNat
<VAR>w : Nat<VAR>a : Bool<VAR>x : BitVec w<GOAL>(BitVec.cons a x).toNat = a.toNat <<< w + x.toNat
<VAR>b : Bool<VAR>n : Nat<VAR>x : BitVec n<VAR>i : Nat<GOAL>(BitVec.cons b x).getLsb i = if i = n then b else x.getLsb i
<VAR>a : Bool<GOAL>∀ {w : Nat} {x : BitVec w}, (BitVec.cons a x).msb = a
<VAR>a : Bool<GOAL>∀ {w : Nat} {x : BitVec w}, (BitVec.cons a x).getMsb 0 = a
<VAR>a : Bool<GOAL>∀ {w : Nat} {x : BitVec w} {i : Nat}, (BitVec.cons a x).getMsb (i + 1) = x.getMsb i
<VAR>w i : Nat<VAR>x : BitVec w<GOAL>BitVec.truncate (i + 1) x = BitVec.cons (x.getLsb i) (BitVec.truncate i x)
<VAR>w : Nat<VAR>x : BitVec (w + 1)<GOAL>x = BitVec.cons x.msb (BitVec.truncate w x)
<VAR>w : Nat<VAR>x : BitVec w<VAR>b : Bool<GOAL>~~~BitVec.cons b x = BitVec.cons (!b) (~~~x)
<VAR>w : Nat<VAR>x y : BitVec w<VAR>a b : Bool<GOAL>BitVec.cons a x ||| BitVec.cons b y = BitVec.cons (a || b) (x ||| y)
<VAR>w : Nat<VAR>x y : BitVec w<VAR>a b : Bool<GOAL>BitVec.cons a x &&& BitVec.cons b y = BitVec.cons (a && b) (x &&& y)
<VAR>w : Nat<VAR>x y : BitVec w<VAR>a b : Bool<GOAL>BitVec.cons a x ^^^ BitVec.cons b y = BitVec.cons (xor a b) (x ^^^ y)
<VAR>w : Nat<VAR>x : BitVec w<VAR>b : Bool<GOAL>(x.concat b).toNat = x.toNat * 2 + b.toNat
<VAR>w : Nat<VAR>x : BitVec w<VAR>b : Bool<VAR>i : Nat<GOAL>(x.concat b).getLsb i = if i = 0 then b else x.getLsb (i - 1)
<GOAL>∀ {w : Nat} {x : BitVec w} {b : Bool}, (x.concat b).getLsb 0 = b
<GOAL>∀ {w : Nat} {x : BitVec w} {b : Bool} {i : Nat}, (x.concat b).getLsb (i + 1) = x.getLsb i
<VAR>w : Nat<VAR>x : BitVec w<VAR>b : Bool<GOAL>~~~x.concat b = (~~~x).concat !b
<VAR>w : Nat<VAR>x y : BitVec w<VAR>a b : Bool<GOAL>x.concat a ||| y.concat b = (x ||| y).concat (a || b)
<VAR>w : Nat<VAR>x y : BitVec w<VAR>a b : Bool<GOAL>x.concat a &&& y.concat b = (x &&& y).concat (a && b)
<VAR>w : Nat<VAR>x y : BitVec w<VAR>a b : Bool<GOAL>x.concat a ^^^ y.concat b = (x ^^^ y).concat (xor a b)
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x + y = BitVec.ofNat n (x.toNat + y.toNat)
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>(x + y).toNat = (x.toNat + y.toNat) % 2 ^ w
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>(x + y).toFin = x.toFin + y.toFin
<VAR>n : Nat<VAR>x : Fin (2 ^ n)<VAR>y : BitVec n<GOAL>{ toFin := x } + y = { toFin := x + y.toFin }
<VAR>n : Nat<VAR>x : BitVec n<VAR>y : Fin (2 ^ n)<GOAL>x + { toFin := y } = { toFin := x.toFin + y }
<VAR>n : Nat<VAR>x y : Nat<GOAL>BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y
<VAR>n : Nat<VAR>x y : Nat<GOAL>BitVec.ofNat n x + BitVec.ofNat n y = BitVec.ofNat n (x + y)
<VAR>n : Nat<VAR>x y z : BitVec n<GOAL>x + y + z = x + (y + z)
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x + y = y + x
<VAR>n : Nat<VAR>x : BitVec n<GOAL>x + 0#n = x
<VAR>n : Nat<VAR>x : BitVec n<GOAL>0#n + x = x
<VAR>w i : Nat<VAR>x y : BitVec w<VAR>h : i ≤ w<GOAL>BitVec.truncate i (x + y) = BitVec.truncate i x + BitVec.truncate i y
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>(x + y).toInt = (x.toInt + y.toInt).bmod (2 ^ w)
<VAR>n : Nat<VAR>x y : Int<GOAL>BitVec.ofInt n (x + y) = BitVec.ofInt n x + BitVec.ofInt n y
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x - y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>(x - y).toNat = (2 ^ n - y.toNat + x.toNat) % 2 ^ n
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>(x - y).toNat = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>(x - y).toFin = x.toFin - y.toFin
<VAR>n : Nat<VAR>x : Fin (2 ^ n)<VAR>y : BitVec n<GOAL>{ toFin := x } - y = { toFin := x - y.toFin }
<VAR>n : Nat<VAR>x : BitVec n<VAR>y : Fin (2 ^ n)<GOAL>x - { toFin := y } = { toFin := x.toFin - y }
<VAR>n : Nat<VAR>x y : Nat<GOAL>BitVec.ofNat n x - BitVec.ofNat n y = BitVec.ofNat n (2 ^ n - y % 2 ^ n + x)
<VAR>n : Nat<VAR>x : BitVec n<GOAL>x - 0#n = x
<VAR>n : Nat<VAR>x : BitVec n<GOAL>x - x = 0#n
<VAR>n : Nat<VAR>x : BitVec n<GOAL>(-x).toNat = (2 ^ n - x.toNat) % 2 ^ n
<VAR>n : Nat<VAR>x : BitVec n<GOAL>(-x).toFin = Fin.ofNat' (2 ^ n - x.toNat) ⋯
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x - y = x + -y
<VAR>n : Nat<GOAL>-0#n = 0#n
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x + y - y = x
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x - y + y = x
<VAR>w : Nat<VAR>x y z : BitVec w<GOAL>x = z - y ↔ x + y = z
<VAR>w : Nat<GOAL>-1#w = BitVec.allOnes w
<VAR>w : Nat<VAR>x : BitVec w<GOAL>-x = ~~~x + 1
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x * y = { toFin := x.toFin * y.toFin }
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>(x * y).toNat = x.toNat * y.toNat % 2 ^ n
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>(x * y).toFin = x.toFin * y.toFin
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x * y = y * x
<VAR>w : Nat<VAR>x y z : BitVec w<GOAL>x * y * z = x * (y * z)
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x * 1#w = x
<VAR>w : Nat<VAR>x : BitVec w<GOAL>1#w * x = x
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>(x * y).toInt = (x.toInt * y.toInt).bmod (2 ^ w)
<VAR>n : Nat<VAR>x y : Int<GOAL>BitVec.ofInt n (x * y) = BitVec.ofInt n x * BitVec.ofInt n y
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x ≤ y ↔ x.toNat ≤ y.toNat
<VAR>n : Nat<VAR>x : BitVec n<VAR>y : Fin (2 ^ n)<GOAL>x ≤ { toFin := y } ↔ x.toFin ≤ y
<VAR>n : Nat<VAR>x : Fin (2 ^ n)<VAR>y : BitVec n<GOAL>{ toFin := x } ≤ y ↔ x ≤ y.toFin
<VAR>n : Nat<VAR>x y : Nat<GOAL>BitVec.ofNat n x ≤ BitVec.ofNat n y ↔ x % 2 ^ n ≤ y % 2 ^ n
<VAR>n : Nat<VAR>x y : BitVec n<GOAL>x < y ↔ x.toNat < y.toNat
<VAR>n : Nat<VAR>x : BitVec n<VAR>y : Fin (2 ^ n)<GOAL>x < { toFin := y } ↔ x.toFin < y
<VAR>n : Nat<VAR>x : Fin (2 ^ n)<VAR>y : BitVec n<GOAL>{ toFin := x } < y ↔ x < y.toFin
<VAR>n : Nat<VAR>x y : Nat<GOAL>BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2 ^ n < y % 2 ^ n
<VAR>n : Nat<VAR>x y : BitVec n<VAR>h1 : x ≤ y<VAR>h2 : ¬x = y<GOAL>x < y
<VAR>i : Nat<VAR>w : Nat<GOAL>(BitVec.intMax w).getLsb i = decide (i < w)
<VAR>w : Nat<GOAL>(BitVec.intMax w).toNat = 2 ^ w - 1
<VAR>bs : List Bool<VAR>i : Nat<GOAL>(BitVec.ofBoolListBE bs).getMsb i = bs.getD i false
<VAR>bs : List Bool<VAR>i : Nat<GOAL>(BitVec.ofBoolListBE bs).getLsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)
<VAR>bs : List Bool<VAR>i : Nat<GOAL>(BitVec.ofBoolListLE bs).getLsb i = bs.getD i false
<VAR>bs : List Bool<VAR>i : Nat<GOAL>(BitVec.ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)
<VAR>w : Nat<VAR>x : BitVec w<VAR>r : Nat<GOAL>x.rotateLeft (r % w) = x.rotateLeft r
<VAR>w : Nat<VAR>x : BitVec w<VAR>r : Nat<VAR>hr : r < w<GOAL>x.rotateLeft r = x.rotateLeftAux r
<VAR>w : Nat<VAR>x : BitVec w<VAR>r i : Nat<VAR>hi : i < r<GOAL>(x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i)
<VAR>w : Nat<VAR>x : BitVec w<VAR>r i : Nat<VAR>hi : i ≥ r<GOAL>(x.rotateLeftAux r).getLsb i = (decide (i < w) && x.getLsb (i - r))
<VAR>w : Nat<VAR>x : BitVec w<VAR>r i : Nat<VAR>hr : r < w<GOAL>(x.rotateLeft r).getLsb i = bif decide (i < r) then x.getLsb (w - r + i) else decide (i < w) && x.getLsb (i - r)
<VAR>w : Nat<VAR>x : BitVec w<VAR>r i : Nat<GOAL>(x.rotateLeft r).getLsb i = bif decide (i < r % w) then x.getLsb (w - r % w + i) else decide (i < w) && x.getLsb (i - r % w)
<VAR>w : Nat<VAR>x : BitVec w<VAR>r i : Nat<VAR>hi : i < w - r<GOAL>(x.rotateRightAux r).getLsb i = x.getLsb (r + i)
<VAR>w : Nat<VAR>x : BitVec w<VAR>r i : Nat<VAR>hi : i ≥ w - r<GOAL>(x.rotateRightAux r).getLsb i = (decide (i < w) && x.getLsb (i - (w - r)))
<VAR>w : Nat<VAR>x : BitVec w<VAR>r : Nat<VAR>hr : r < w<GOAL>x.rotateRight r = x.rotateRightAux r
<VAR>w : Nat<VAR>x : BitVec w<VAR>r : Nat<GOAL>x.rotateRight (r % w) = x.rotateRight r
<VAR>w : Nat<VAR>x : BitVec w<VAR>r i : Nat<VAR>hr : r < w<GOAL>(x.rotateRight r).getLsb i = bif decide (i < w - r) then x.getLsb (r + i) else decide (i < w) && x.getLsb (i - (w - r))