OAI/Combinatorics/IndependentSets/Machines/PoweringMachineRow.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.Field line 12
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.inputSize line 14
  3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.fieldEquiv line 16
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.inputEquiv line 20
  5. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.packData line 23
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.packData_inputEquiv line 26
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.basePredicate line 31
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.leftMatches line 35
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.rightMatches line 39
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.firstMatch line 43
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.firstMatch_spec line 46
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.firstMatch_none line 53
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.edgeAccept line 57
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.edgeAccept_of_matches line 63
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.rowAccept line 71
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.rowAccept_eq_true line 75
  17. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.rowBlock line 81
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.rowBlock_at line 87
  19. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.encodeBit line 94
  20. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.encodeBits line 96
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.encodeBits_append line 100
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.encodeBits_graphWords line 106
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.encodeBits_length_le line 113
  24. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.readEncodedSlots line 123
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedSlots line 136
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedAll line 155
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_readEncodedSlots line 171
  28. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.writeEncodedSlots line 179
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.stepAux_writeEncodedSlots line 187
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_writeEncodedSlots line 204