OAI/Combinatorics/EditApproximation/Binary/BitRankedNormalize.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The denominator condition is used only at the semantic values of smaller requests. Strong induction then establishes the actual binary program's value and normalized trace without assuming its own output.

  1. theorem OAI.EditApproximation.rankedNormalizeBody_correct line 26
  2. theorem OAI.EditApproximation.rankedNormalizeBody_width line 64