GapCVP proof, part 08, continuation 02

def GapCVP.CNFAnnotatedSourceCompleteBubbleSortTM.annotatedCompleteBubbleSortState (pending count sorted : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CNFAnnotatedSourceCompleteBubbleSortTM.flatAnnotatedCompleteBubbleCount (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.CNFAnnotatedSourceCompleteBubbleSortTM.flatAnnotatedCompleteBubbleCount input = GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldAt 1 input

@[simp]

theorem GapCVP.CNFAnnotatedSourceCompleteBubbleSortTM.flatAnnotatedCompleteBubbleSortState_count (pending count sorted : List Bool) : flatAnnotatedCompleteBubbleCount (annotatedCompleteBubbleSortState pending count sorted) = count

Internal support shared across GapCVP continuation modules.

@[irreducible]

def GapCVP.CNFAnnotatedSourceCompleteBubbleSortSourceCert.flatAnnotatedOriginalBubbleSortAux {T S : ℕ} (pending sorted : List (CL.Clause T S)) : List (CL.Clause T S)

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CNFAnnotatedSourceCompleteBubbleSortSourceCert.flatAnnotatedOriginalBubbleSortAux [] sorted = sorted

theorem GapCVP.CNFAnnotatedSourceCompleteBubbleSortSourceCert.flatAnnotatedOriginalBubbleSortAux_perm {T S : ℕ} (pending sorted : List (CL.Clause T S)) : (flatAnnotatedOriginalBubbleSortAux pending sorted).Perm (pending ++ sorted)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFAnnotatedSourceCompleteBubbleSortSourceCert.flatAnnotatedOriginalBubbleSort_pairwise {T S : ℕ} (pending : List (CL.Clause T S)) : List.Pairwise (fun (first second : CL.Clause T S) => Encodable.encode first ≤ Encodable.encode second) (flatAnnotatedOriginalBubbleSortAux pending [])

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFAnnotatedSourceCompleteBubbleSortSourceCert.annotatedCompleteBubbleSortedSourceOutput : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CNFAnnotatedSourceCompleteBubbleSortSourceCert.flatAnnotatedCompleteBubbleSortedSourceComputable : BitTM annotatedCompleteBubbleSortedSourceOutput

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CNFAnnotatedSourceCompleteBubbleSortSourceCert.flatAnnotatedCompleteBubbleSortedSourceOutput_valid {T S : ℕ} (pending sorted : List (CL.Clause T S)) : annotatedCompleteBubbleSortedSourceOutput (CNFAnnotatedSourceCompleteBubbleSortTM.annotatedCompleteBubbleSortState (CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledClauseStream pending) (List.replicate pending.length true) (CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledClauseStream sorted)) = CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledClauseStream (flatAnnotatedOriginalBubbleSortAux pending sorted)

Internal support shared across GapCVP continuation modules.