OAI/Computability/PerfectCompleteness/Machines/SourceClauseReaderMachineLemmas.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceClauseReaderMachine.Signs line 18
  2. abbrev OAI.PerfectCompleteness.SourceClauseReaderMachine.State line 19
  3. abbrev OAI.PerfectCompleteness.SourceClauseReaderMachine.Alphabet line 20
  4. abbrev OAI.PerfectCompleteness.SourceClauseReaderMachine.clean line 21
  5. def OAI.PerfectCompleteness.SourceClauseReaderMachine.shape line 24
  6. def OAI.PerfectCompleteness.SourceClauseReaderMachine.clauseShape line 27
  7. theorem OAI.PerfectCompleteness.SourceClauseReaderMachine.clauseShape_eq line 30
  8. def OAI.PerfectCompleteness.SourceClauseReaderMachine.steps line 33
  9. inductive OAI.PerfectCompleteness.SourceClauseReaderMachine.Label line 36
  10. def OAI.PerfectCompleteness.SourceClauseReaderMachine.main line 41
  11. def OAI.PerfectCompleteness.SourceClauseReaderMachine.instruction line 47
  12. theorem OAI.PerfectCompleteness.SourceClauseReaderMachine.publishStep line 64
  13. theorem OAI.PerfectCompleteness.SourceClauseReaderMachine.readTrace line 73
  14. def OAI.PerfectCompleteness.SourceClauseReaderMachine.readInTime line 104
  15. theorem OAI.PerfectCompleteness.SourceClauseReaderMachine.steps_le_encoded_length line 122
  16. theorem OAI.PerfectCompleteness.SourceClauseReaderMachine.finiteState line 128
  17. theorem OAI.PerfectCompleteness.SourceClauseReaderMachine.finiteAlphabet line 130
  18. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.recordWords line 141
  19. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.records line 144
  20. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.recordBits line 148
  21. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.body line 151
  22. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.words line 154
  23. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.bits line 157
  24. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.recordWords_length line 159
  25. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.records_length line 162
  26. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.words_length line 168
  27. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.records_eq_finRange line 171
  28. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.body_nil line 187
  29. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.body_cons line 189
  30. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.recordBits_eq line 193
  31. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.bits_eq line 196
  32. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.parseRecords line 202
  33. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.parseRecords_encoded line 213
  34. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.decodeWords line 222
  35. def OAI.PerfectCompleteness.SourceOccurrenceEncoding.decode line 228
  36. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.decodeWords_words line 231
  37. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.decode_bits line 239
  38. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.bits_injective line 242
  39. theorem OAI.PerfectCompleteness.SourceOccurrenceEncoding.body_length_le line 247