Little-endian binary comparison -- proof internals

theorem Complexity.BitString.unsignedLE_eq_decide_internal {width : ℕ} (left right : BitString width) : left.unsignedLE right = decide (left.unsignedValue ≤ right.unsignedValue)

theorem Complexity.BoolFormula.eval_ofBool_internal (value : Bool) (assignment : ℕ → Bool) : eval assignment (ofBool value) = value

@[simp]

theorem Complexity.BoolFormula.size_ofBool_internal (value : Bool) : (ofBool value).size = 1

theorem Complexity.BoolFormula.eval_unsignedLEOf_internal {width : ℕ} (left right : Fin width → BoolFormula) (assignment : ℕ → Bool) : eval assignment (unsignedLEOf left right) = BitString.unsignedLE (fun (i : Fin width) => eval assignment (left i)) fun (i : Fin width) => eval assignment (right i)

theorem Complexity.BoolFormula.size_unsignedLEOf_internal {width : ℕ} (left right : Fin width → BoolFormula) : (∀ (i : Fin width), (left i).size = 1) → (∀ (i : Fin width), (right i).size = 1) → (unsignedLEOf left right).size = 15 * width + 1

theorem Complexity.BoolFormula.vars_unsignedLEOf_lt_internal {width : ℕ} (left right : Fin width → BoolFormula) (available : ℕ) : (∀ (i : Fin width), ∀ j ∈ (left i).vars, j < available) → (∀ (i : Fin width), ∀ j ∈ (right i).vars, j < available) → ∀ j ∈ (unsignedLEOf left right).vars, j < available

theorem Complexity.BoolFormula.eval_unsignedLELeftConstant_internal {width : ℕ} (left : BitString width) (rightBase : ℕ) (assignment : ℕ → Bool) : eval assignment (unsignedLELeftConstant left rightBase) = decide (left.unsignedValue ≤ BitString.unsignedValue fun (i : Fin width) => assignment (rightBase + ↑i))

theorem Complexity.BoolFormula.eval_unsignedLERightConstant_internal {width : ℕ} (leftBase : ℕ) (right : BitString width) (assignment : ℕ → Bool) : eval assignment (unsignedLERightConstant leftBase right) = decide ((BitString.unsignedValue fun (i : Fin width) => assignment (leftBase + ↑i)) ≤ right.unsignedValue)

theorem Complexity.BoolFormula.size_unsignedLELeftConstant_internal {width : ℕ} (left : BitString width) (rightBase : ℕ) : (unsignedLELeftConstant left rightBase).size = 15 * width + 1

theorem Complexity.BoolFormula.size_unsignedLERightConstant_internal {width : ℕ} (leftBase : ℕ) (right : BitString width) : (unsignedLERightConstant leftBase right).size = 15 * width + 1

theorem Complexity.BoolFormula.vars_unsignedLELeftConstant_lt_internal {width : ℕ} (left : BitString width) (rightBase available : ℕ) (hright : rightBase + width ≤ available) (j : ℕ) : j ∈ (unsignedLELeftConstant left rightBase).vars → j < available

theorem Complexity.BoolFormula.vars_unsignedLERightConstant_lt_internal {width : ℕ} (leftBase : ℕ) (right : BitString width) (available : ℕ) (hleft : leftBase + width ≤ available) (j : ℕ) : j ∈ (unsignedLERightConstant leftBase right).vars → j < available

theorem Complexity.BoolFormula.size_unsignedLEAux_internal (width leftBase rightBase : ℕ) : (unsignedLEAux width leftBase rightBase).size = 15 * width + 1

theorem Complexity.BoolFormula.size_unsignedLE_internal (width : ℕ) : (unsignedLE width).size = 15 * width + 1

theorem Complexity.BoolFormula.eval_unsignedLEAux_internal (width leftBase rightBase : ℕ) (assignment : ℕ → Bool) (left right : BitString width) (hleft : ∀ (i : Fin width), assignment (leftBase + ↑i) = left i) (hright : ∀ (i : Fin width), assignment (rightBase + ↑i) = right i) : eval assignment (unsignedLEAux width leftBase rightBase) = left.unsignedLE right

theorem Complexity.BoolFormula.eval_unsignedLE_internal (width : ℕ) (left right : BitString width) : eval (BitString.toTotal (Fin.append left right)) (unsignedLE width) = decide (left.unsignedValue ≤ right.unsignedValue)

theorem Complexity.BoolFormula.vars_unsignedLEAux_lt_internal (width leftBase rightBase available : ℕ) (hleft : leftBase + width ≤ available) (hright : rightBase + width ≤ available) (i : ℕ) : i ∈ (unsignedLEAux width leftBase rightBase).vars → i < available

theorem Complexity.BoolFormula.vars_unsignedLE_lt_internal (width i : ℕ) : i ∈ (unsignedLE width).vars → i < width + width

theorem Complexity.CircuitCode.length_unsignedLERawCircuit_internal (width : ℕ) : List.length (unsignedLERawCircuit width) = 15 * width + 1

theorem Complexity.CircuitCode.unsignedLERawCircuit_wellFormed_internal (width : ℕ) [NeZero width] : RawCircuit.WellFormed (width + width) (unsignedLERawCircuit width)

theorem Complexity.CircuitCode.eval?_unsignedLERawCircuit_internal (width : ℕ) [NeZero width] (left right : BitString width) : (unsignedLERawCircuit width).eval? (BitString.toList (Fin.append left right)) = some (decide (left.unsignedValue ≤ right.unsignedValue))