OAI/Combinatorics/IndependentSets/Machines/MachineUnaryEqualityBit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.Alphabet line 14
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.State line 15
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.clean line 17
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.compareStateEquiv line 19
  5. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.Label line 25
  6. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.(instance at line 31) line 31
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.exitAt line 36
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.bitEncoding line 41
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.emit line 43
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.instruction line 48
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.copySteps line 66
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.compareSteps line 67
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.steps line 68
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.steps_le line 70
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.encodeWord_eq_iff line 74
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.emit_step line 83
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.joinTrace line 95
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityTrace line 99
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.equalityInTime line 201
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.machine line 220
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryEqualityBit.machineInTime line 231