OAI/Combinatorics/IndependentSets/Machines/FinalCNFRow.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_zero line 11
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_one line 12
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_two line 13
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_three line 14
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_four line 15
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_five line 16
  7. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands line 18
  8. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowRelation line 22
  9. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowRest line 25
  10. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.preparedTapes line 28
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_input line 34
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_head line 40
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_tail line 48
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_reverse line 54
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_frame line 61
  16. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.emittedTapes line 69
  17. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowResultTapes line 75
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_input line 79
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_tail line 84
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_head line 89
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_reverse line 94
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_index line 99
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_accumulator line 104
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_frame line 111
  25. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.guardRowInTime line 122
  26. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.guardEndInTime line 135
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_operands line 146
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands_bounded line 175
  29. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime line 186
  30. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowInTime line 189