OAI/Computability/SpaceSimulation/Evaluation/Ready.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Uniform circuit presentation. In contrast to lookup-table evaluation as a pure algebraic object, actual computation of a Boolean assignment's function value is needed.

  1. structure OAI.Fifths.Circuit.Ready line 14
  2. theorem OAI.Fifths.Circuit.slotMap line 52
  3. theorem OAI.Fifths.Circuit.which line 58
  4. theorem OAI.Fifths.Circuit.chooseSlot line 67
  5. theorem OAI.Fifths.Circuit.combinePool line 74
  6. theorem OAI.Fifths.Circuit.plusComp line 84
  7. theorem OAI.Fifths.Circuit.jump line 107
  8. theorem OAI.Fifths.Circuit.jumpOne line 117
  9. theorem OAI.Fifths.Circuit.formComp line 128
  10. theorem OAI.Fifths.Circuit.Ready.uniformDegree line 145
  11. theorem OAI.Fifths.Circuit.Ready.modulusN line 149
  12. theorem OAI.Fifths.Circuit.Ready.frameSpace line 153
  13. theorem OAI.Fifths.Circuit.Ready.poolSpace line 175