OAI/Computability/MinUncut/PCP/AddressArithmetic.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressArithmetic.variable_rank line 12
  2. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressArithmetic.clause_rank line 16
  3. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressArithmetic.left_address line 20
  4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressArithmetic.right_address line 25
  5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressArithmetic.dummy_address line 31
  6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressArithmetic.left_address_radix line 38
  7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressArithmetic.right_address_radix line 45
  8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressArithmetic.nBits_eq_dummy_succ line 53
  9. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.rank line 66
  10. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.reverseDigits line 69
  11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.reverseDigits_apply line 72
  12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.horner_value_sum line 76
  13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.horner_reverse_eq_rank line 91
  14. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.reverseSlots line 110
  15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.reverseSlots_control line 113
  16. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.reverseSlots_digit line 116
  17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.clean_reverseSlots line 122
  18. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.statement line 129
  19. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.program line 134
  20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.rankTrace line 139
  21. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.rankInTime line 158
  22. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.rankInPolynomialTime line 175
  23. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.variableRankInTime line 194
  24. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.clauseRankInTime line 210
  25. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.programInTime line 226
  26. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.machine line 238
  27. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.machineInTime line 249
  28. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.clauseSlots line 263
  29. def OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.variableSlots line 280
  30. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.clauseSlots_control line 297
  31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.clauseSlots_digit line 300
  32. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.variableSlots_control line 303
  33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.variableSlots_digit line 306
  34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRankPhase.selectedDigits_loaded line 310
  35. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.Descriptor line 329
  36. def OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.descriptor line 331
  37. def OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.baseValue line 336
  38. def OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.realize line 343
  39. def OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.words line 345
  40. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.realize_descriptor line 349
  41. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.descriptor_offset_bound line 366
  42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.sourceEquation_numeric line 389
  43. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.sourceEquation_words line 398
  44. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.baseValue_lt line 407
  45. theorem OAI.MinUncutGames.Foundations.Hastad.SourceAddressDescriptors.equation_emit_steps_le line 424