OAI/Computability/MaxCut/PCP/EquationEmit.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Emit one fixed descriptor equation from three preserved unary base registers. The output order is first address, second address, third address, RHS. The actual stack program emits those fields in reverse order.

  1. inductive OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.Label line 18
  2. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.Label.enumList line 23
  3. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.Label.enumList_getElem?_ctorIdx_eq line 26
  4. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.Label.enumList_nodup line 30
  5. instance OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.(instance at line 32) line 32
  6. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.Alphabet line 36
  7. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.State line 37
  8. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.rhsBit line 39
  9. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.steps line 41
  10. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.statement line 46
  11. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.program line 69
  12. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.prefixTapes line 73
  13. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.prefixTapes_other line 76
  14. theorem OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.equationTrace line 80
  15. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.equationInTime line 151
  16. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.programInTime line 170
  17. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.Tape line 185
  18. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.machine line 187
  19. def OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.machineInTime line 198