OAI/Computability/PerfectCompleteness/Foundations/SourceTupleData.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PerfectCompleteness.SourceTupleData.Tape line 12
  2. def OAI.PerfectCompleteness.SourceTupleData.localTape line 21
  3. theorem OAI.PerfectCompleteness.SourceTupleData.localTape_injective line 33
  4. def OAI.PerfectCompleteness.SourceTupleData.placedTape line 37
  5. theorem OAI.PerfectCompleteness.SourceTupleData.placedTape_injective line 40
  6. def OAI.PerfectCompleteness.SourceTupleData.selectedClause line 45
  7. def OAI.PerfectCompleteness.SourceTupleData.«stacks» line 49
  8. theorem OAI.PerfectCompleteness.SourceTupleData.table_at line 59
  9. theorem OAI.PerfectCompleteness.SourceTupleData.digits_at line 63
  10. theorem OAI.PerfectCompleteness.SourceTupleData.work_at line 69
  11. theorem OAI.PerfectCompleteness.SourceTupleData.variables_at line 73
  12. theorem OAI.PerfectCompleteness.SourceTupleData.coordinate_table line 81
  13. theorem OAI.PerfectCompleteness.SourceTupleData.coordinate_digit line 87
  14. theorem OAI.PerfectCompleteness.SourceTupleData.coordinate_initial_empty line 93
  15. theorem OAI.PerfectCompleteness.SourceTupleData.resultTapes_eq line 100
  16. def OAI.PerfectCompleteness.SourceTupleData.shapes line 129
  17. theorem OAI.PerfectCompleteness.SourceTupleData.shapes_update line 136