Numeric schedules for streaming tableau serialization -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_zero_internal (sizeAt : ℕ → ℕ) : prefixSize sizeAt 0 = 0

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_succ_internal (sizeAt : ℕ → ℕ) (count : ℕ) : prefixSize sizeAt (count + 1) = prefixSize sizeAt count + sizeAt count

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_eq_sum_range_internal (sizeAt : ℕ → ℕ) (count : ℕ) : prefixSize sizeAt count = (List.map sizeAt (List.range count)).sum

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_eq_sum_ofFn_internal (sizeAt : ℕ → ℕ) (count : ℕ) : prefixSize sizeAt count = (List.ofFn fun (index : Fin count) => sizeAt ↑index).sum

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_mono_internal (sizeAt : ℕ → ℕ) {first second : ℕ} (hbound : first ≤ second) : prefixSize sizeAt first ≤ prefixSize sizeAt second

theorem Complexity.CircuitUnrolling.Serializer.reverseMember_lt_internal {count rank : ℕ} (hrank : rank < count) : reverseMember count rank < count

theorem Complexity.CircuitUnrolling.Serializer.reverseMember_add_rank_internal {count rank : ℕ} (hrank : rank < count) : reverseMember count rank + rank + 1 = count

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_formulaSizeAt_internal (formulas : List BoolFormula) : prefixSize (fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0) formulas.length = (List.map BoolFormula.size formulas).sum

theorem Complexity.CircuitUnrolling.Serializer.length_indexedRightFoldConnectors_internal (op : AndOrOp) (available count : ℕ) (sizeAt : ℕ → ℕ) : List.length (indexedRightFoldConnectors op available count sizeAt) = count

theorem Complexity.CircuitUnrolling.Serializer.getElem_indexedRightFoldConnectors_internal (op : AndOrOp) (available count : ℕ) (sizeAt : ℕ → ℕ) (rank : Fin count) : (indexedRightFoldConnectors op available count sizeAt)[↑rank] = indexedRightFoldConnector op available count sizeAt ↑rank

theorem Complexity.CircuitUnrolling.Serializer.length_indexedBatchCopies_internal (available count : ℕ) (sizeAt : ℕ → ℕ) : List.length (indexedBatchCopies available count sizeAt) = count

theorem Complexity.CircuitUnrolling.Serializer.getElem_indexedBatchCopies_internal (available count : ℕ) (sizeAt : ℕ → ℕ) (index : Fin count) : (indexedBatchCopies available count sizeAt)[↑index] = indexedBatchCopy available sizeAt ↑index

theorem Complexity.CircuitUnrolling.Serializer.rightFoldConnectors_eq_indexed_internal (op : AndOrOp) (available : ℕ) (formulas : List BoolFormula) : BoolFormula.rightFoldConnectors op available formulas = indexedRightFoldConnectors op available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

theorem Complexity.CircuitUnrolling.Serializer.compileRawRightFold_eq_indexed_internal (op : AndOrOp) (identity : Bool) (available : ℕ) (formulas : List BoolFormula) : BoolFormula.compileRawRightFold op identity available formulas = (BoolFormula.compileRawOutputs available formulas).circuit ++ [CircuitCode.RawGate.constant 0 identity] ++ indexedRightFoldConnectors op available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_conjs_eq_indexed_internal (available : ℕ) (formulas : List BoolFormula) : BoolFormula.compileRaw available (BoolFormula.conjs formulas) = (BoolFormula.compileRawOutputs available formulas).circuit ++ [CircuitCode.RawGate.constant 0 true] ++ indexedRightFoldConnectors AndOrOp.and available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_disjs_eq_indexed_internal (available : ℕ) (formulas : List BoolFormula) : BoolFormula.compileRaw available (BoolFormula.disjs formulas) = (BoolFormula.compileRawOutputs available formulas).circuit ++ [CircuitCode.RawGate.constant 0 false] ++ indexedRightFoldConnectors AndOrOp.or available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

theorem Complexity.CircuitUnrolling.Serializer.compileRawOutputs_copies_eq_indexed_internal (available : ℕ) (formulas : List BoolFormula) : List.map (fun (input : ℕ) => CircuitCode.RawGate.copy input) (BoolFormula.compileRawOutputs available formulas).outputs = indexedBatchCopies available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

theorem Complexity.CircuitUnrolling.Serializer.compileRawBatch_eq_indexed_internal (available : ℕ) (formulas : List BoolFormula) : BoolFormula.compileRawBatch available formulas = (BoolFormula.compileRawOutputs available formulas).circuit ++ indexedBatchCopies available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0