Finite Boolean core of bitonic cleaning

The eight-value closure lemma is proved by kernel reduction.

def Algebraic.MassProduction.Sorting.Semantics.Internal.boolHalfMin (sequence : Fin 8 → Bool) : Fin 4 → Bool

Pairwise minima of the two Boolean halves used by the finite cleaning check.

Equations

• Algebraic.MassProduction.Sorting.Semantics.Internal.boolHalfMin sequence i = min (sequence (Fin.castAdd 4 i)) (sequence (Fin.natAdd 4 i))

def Algebraic.MassProduction.Sorting.Semantics.Internal.boolHalfMax (sequence : Fin 8 → Bool) : Fin 4 → Bool

Pairwise maxima of the two Boolean halves used by the finite cleaning check.

Equations

• Algebraic.MassProduction.Sorting.Semantics.Internal.boolHalfMax sequence i = max (sequence (Fin.castAdd 4 i)) (sequence (Fin.natAdd 4 i))

theorem Algebraic.MassProduction.Sorting.Semantics.Internal.boolBitonicHalves (sequence : Fin 8 → Bool) (hsequence : SequenceBitonic sequence) : SequenceBitonic (boolHalfMin sequence) ∧ SequenceBitonic (boolHalfMax sequence)