OAI/Combinatorics/EditApproximation/Geometry/RankedMemoSimulation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local recurrence equalities identify the complete table semantics of a lazy query program. No complete table is evaluated by the memo interpreter; it is used only as the mathematical specification.

  1. theorem OAI.EditApproximation.rankedProgramValue_eq line 11
  2. theorem OAI.EditApproximation.rankedMemoEvaluate_specification line 30