OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryExecution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedQueryMemoResult line 9

   Source documentation

   The executed mixed binary memo at the final refinement root.

   def computedQueryMemoResult (source target : List ℕ) (N : ℕ)
       (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
       (input : ComputedFamilyInput source target N) :=
   …

   Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.ComputedFamilyInput

2. def OAI.EditApproximation.computedQueryLocalWork line 18
3. theorem OAI.EditApproximation.computedQueryMemoResult_decode line 37
4. theorem OAI.EditApproximation.computedQueryMemoResult_localWork line 55