OAI/Computability/PerfectCompleteness/Machines/NormalizationEmitMachine.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.NormalizationEmitMachine.Alphabet line 21
  2. abbrev OAI.PerfectCompleteness.NormalizationEmitMachine.State line 22
  3. def OAI.PerfectCompleteness.NormalizationEmitMachine.clean line 24
  4. def OAI.PerfectCompleteness.NormalizationEmitMachine.sourceIndex line 26
  5. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.sourceIndex_ne_scratch line 30
  6. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.sourceIndex_ne_output line 40
  7. inductive OAI.PerfectCompleteness.NormalizationEmitMachine.LocalLabel line 50
  8. abbrev OAI.PerfectCompleteness.NormalizationEmitMachine.LocalLabel.enumList line 56
  9. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.LocalLabel.enumList_getElem?_ctorIdx_eq line 58
  10. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.LocalLabel.enumList_nodup line 62
  11. instance OAI.PerfectCompleteness.NormalizationEmitMachine.(instance at line 64) line 64
  12. def OAI.PerfectCompleteness.NormalizationEmitMachine.emitSign line 68
  13. def OAI.PerfectCompleteness.NormalizationEmitMachine.emit line 75
  14. def OAI.PerfectCompleteness.NormalizationEmitMachine.localInstruction line 80
  15. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.joinTrace line 89
  16. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.stepAux_emit line 93
  17. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.literalTrace line 124
  18. def OAI.PerfectCompleteness.NormalizationEmitMachine.result line 154
  19. def OAI.PerfectCompleteness.NormalizationEmitMachine.cost line 158
  20. def OAI.PerfectCompleteness.NormalizationEmitMachine.commandSteps line 161
  21. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.resultOf_eq line 164
  22. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.sequenceSteps_eq line 174
  23. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.sourceValue_le line 184
  24. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.commandSteps_le line 191
  25. abbrev OAI.PerfectCompleteness.NormalizationEmitMachine.Labels line 203
  26. def OAI.PerfectCompleteness.NormalizationEmitMachine.sequenceInstruction line 206
  27. def OAI.PerfectCompleteness.NormalizationEmitMachine.sequenceEntry line 212
  28. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.sequenceTrace line 217
  29. abbrev OAI.PerfectCompleteness.NormalizationEmitMachine.Label line 246
  30. def OAI.PerfectCompleteness.NormalizationEmitMachine.main line 248
  31. def OAI.PerfectCompleteness.NormalizationEmitMachine.instruction line 250
  32. def OAI.PerfectCompleteness.NormalizationEmitMachine.steps line 254
  33. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.steps_le line 256
  34. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.gadgetTrace line 262
  35. def OAI.PerfectCompleteness.NormalizationEmitMachine.gadgetInTime line 286
  36. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.label_finite line 306
  37. theorem OAI.PerfectCompleteness.NormalizationEmitMachine.state_finite line 308