Semantic correctness internals for Batcher sorting networks

@[simp]

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.finAppend_addNat_self {α : Sort u_1} {n : ℕ} (first second : Fin n → α) (i : Fin n) : Fin.append first second (i.addNat n) = second i

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.appendSequence_left_value {α : Sort u_1} {n m : ℕ} (first : Fin n → α) (second : Fin m → α) (index : Fin (n + m)) (hleft : ↑index < n) : appendSequence first second index = first ⟨↑index, hleft⟩

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.appendSequence_right_value {α : Sort u_1} {n m : ℕ} (first : Fin n → α) (second : Fin m → α) (index : Fin (n + m)) (hright : ¬↑index < n) : appendSequence first second index = second ⟨↑index - n, ⋯⟩

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.pointwiseMin_bitonic {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) (hsequence : SequenceBitonic (appendSequence first second)) : SequenceBitonic (pointwiseMin first second)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.pointwiseMax_bitonic {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) (hsequence : SequenceBitonic (appendSequence first second)) : SequenceBitonic (pointwiseMax first second)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.pointwiseMin_allLE_pointwiseMax {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) (hsequence : SequenceBitonic (appendSequence first second)) : SequenceAllLE (pointwiseMin first second) (pointwiseMax first second)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.increasing_append_decreasing_bitonic {α : Type u_1} [LinearOrder α] {n m : ℕ} (first : Fin n → α) (second : Fin m → α) (hfirst : SequenceIncreasing first) (hsecond : SequenceDecreasing second) : SequenceBitonic (appendSequence first second)

@[simp]

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.recordFirstHalf_joinRecordHalves {α : Sort u_1} {depth : ℕ} (first second : Fin (networkRecords depth) → α) : recordFirstHalf (joinRecordHalves first second) = first

@[simp]

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.recordSecondHalf_joinRecordHalves {α : Sort u_1} {depth : ℕ} (first second : Fin (networkRecords depth) → α) : recordSecondHalf (joinRecordHalves first second) = second

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.joinRecordHalves_split {α : Sort u_1} {depth : ℕ} (input : Fin (networkRecords (depth + 1)) → α) : joinRecordHalves (recordFirstHalf input) (recordSecondHalf input) = input

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.increasing_append {α : Type u_1} [Preorder α] {n m : ℕ} (first : Fin n → α) (second : Fin m → α) (hfirst : SequenceIncreasing first) (hsecond : SequenceIncreasing second) (hcross : SequenceAllLE first second) : SequenceIncreasing (appendSequence first second)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.decreasing_append {α : Type u_1} [Preorder α] {n m : ℕ} (first : Fin n → α) (second : Fin m → α) (hfirst : SequenceDecreasing first) (hsecond : SequenceDecreasing second) (hcross : SequenceAllLE second first) : SequenceDecreasing (appendSequence first second)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.append_rangeContained {α : Sort u_1} {n m n' m' : ℕ} {first : Fin n → α} {second : Fin m → α} {firstInput : Fin n' → α} {secondInput : Fin m' → α} (hfirst : SequenceRangeContained first firstInput) (hsecond : SequenceRangeContained second secondInput) : SequenceRangeContained (appendSequence first second) (appendSequence firstInput secondInput)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.append_rangeContained_same {α : Sort u_1} {n m k : ℕ} {first : Fin n → α} {second : Fin m → α} {input : Fin k → α} (hfirst : SequenceRangeContained first input) (hsecond : SequenceRangeContained second input) : SequenceRangeContained (appendSequence first second) input

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.pointwiseMin_rangeContained {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) : SequenceRangeContained (pointwiseMin first second) (appendSequence first second)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.pointwiseMax_rangeContained {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) : SequenceRangeContained (pointwiseMax first second) (appendSequence first second)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.orderedCompareLayer_rangeContained {α : Type u_1} [LinearOrder α] (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords (depth + 1)) → α) : SequenceRangeContained (orderedCompareLayer depth ascending input) input

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.orderedBitonicMerge_rangeContained {α : Type u_1} [LinearOrder α] (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : SequenceRangeContained (orderedBitonicMerge depth ascending input) input

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.orderedBitonicMerge_allLE {α : Type u_1} [LinearOrder α] {depth : ℕ} (ascending : Bool) (first second : Fin (networkRecords depth) → α) (hcross : SequenceAllLE first second) : SequenceAllLE (orderedBitonicMerge depth ascending first) (orderedBitonicMerge depth ascending second)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.orderedBitonicMerge_sorted {α : Type u_1} [LinearOrder α] (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) (hbitonic : SequenceBitonic input) : SequenceSorted ascending (orderedBitonicMerge depth ascending input)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.orderedBitonicSort_sorted {α : Type u_1} [LinearOrder α] (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : SequenceSorted ascending (orderedBitonicSort depth ascending input)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.keyedCompareLayer_permutes {κ : Type u_1} {α : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords (depth + 1)) → α) : SequencePermutes (keyedCompareLayer key depth ascending input) input

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.keyedBitonicMerge_permutes {κ : Type u_1} {α : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : SequencePermutes (keyedBitonicMerge key depth ascending input) input

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.keyedBitonicSort_permutes {κ : Type u_1} {α : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : SequencePermutes (keyedBitonicSort key depth ascending input) input

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.key_keyedBitonicSort {κ : Type u_1} {α : Sort u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : (fun (output : Fin (networkRecords depth)) => key (keyedBitonicSort key depth ascending input output)) = orderedBitonicSort depth ascending fun (index : Fin (networkRecords depth)) => key (input index)

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.keyedBitonicSort_sorted {κ : Type u_1} {α : Sort u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : SequenceSorted ascending fun (output : Fin (networkRecords depth)) => key (keyedBitonicSort key depth ascending input output)