OAI/Combinatorics/IndependentSets/Machines/MachineExpanderRowEmit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.emitSteps line 11
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.affinePlan_bits line 13
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.affinePlan_steps line 24
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.emittedWord line 31
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.emittedWord_target line 35
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.emittedWord_other line 40
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.program_firstEmit line 48
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.program_secondEmit line 54
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.program_outputEmit line 60
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.firstEmitTraceAt line 70
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.secondEmitTraceAt line 101
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.outputEmitTraceAt line 132
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTimeAt line 163
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTimeAt line 181
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTimeAt line 199
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.firstEmitTrace line 219
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.secondEmitTrace line 231
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.outputEmitTrace line 243
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTime line 255
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTime line 267
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTime line 279