-- Andreas, 2013-10-24 Bug reported to me by Christoph-Simon Senjak module Issue924 where open import Level open import Data.Empty open import Data.Product open import Data.Sum open import Data.Bool open import Data.Maybe.Core import Data.Nat as ℕ open import Data.Nat using (ℕ) import Data.Nat.Divisibility as ℕ import Data.Nat.Properties as ℕ open import Data.Nat.DivMod import Data.Fin as F open import Data.Fin using (Fin) import Data.Fin.Properties as F import Data.List as L open import Data.List using (List) open import Data.Vec open import Relation.Nullary.Core open import Relation.Binary.PropositionalEquality open ≡-Reasoning open import Algebra open import Algebra.Structures Byte : Set Byte = Fin 256 _^_ : ℕ → ℕ → ℕ _ ^ 0 = 1 n ^ (ℕ.suc m) = n ℕ.* (n ^ m) BitVecToNat : {n : ℕ} → Vec Bool n → ℕ BitVecToNat [] = 0 BitVecToNat (true ∷ r) = ℕ.suc (2 ℕ.* (BitVecToNat r)) BitVecToNat (false ∷ r) = (2 ℕ.* (BitVecToNat r)) postulate ≤lem₁ : {a b : ℕ} → (a ℕ.< b) → (2 ℕ.* a) ℕ.< (2 ℕ.* b) postulate ≤lem₂ : {a b : ℕ} → (a ℕ.< (ℕ.suc b)) → (ℕ.suc (2 ℕ.* a)) ℕ.< (2 ℕ.* (ℕ.suc b)) postulate ≤lem₃ : {a b c : ℕ} → (c ℕ.+ (a ℕ.* 2) ℕ.< (2 ℕ.* b)) → a ℕ.< b ¬0