OAI/ModelTheory/Choiceless/TableMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.CPTSeparation.TableMachine.Index line 9
  2. instance OAI.CPTSeparation.TableMachine.(instance at line 13) line 13
  3. inductive OAI.CPTSeparation.TableMachine.Reg line 15
  4. abbrev OAI.CPTSeparation.TableMachine.CState line 22
  5. abbrev OAI.CPTSeparation.TableMachine.Prog line 24
  6. lemma OAI.CPTSeparation.TableMachine.tableInput_length line 26
  7. lemma OAI.CPTSeparation.TableMachine.tableInput_lookup line 29
  8. def OAI.CPTSeparation.TableMachine.readCell line 39
  9. lemma OAI.CPTSeparation.TableMachine.readCell_runs line 48
  10. inductive OAI.CPTSeparation.Bounded.Program line 90
  11. def OAI.CPTSeparation.Bounded.isOne line 100
  12. def OAI.CPTSeparation.Bounded.Program.WF line 102
  13. def OAI.CPTSeparation.Bounded.Program.eval line 110
  14. def OAI.CPTSeparation.Bounded.equalCode line 119
  15. def OAI.CPTSeparation.Bounded.Program.compile line 123
  16. def OAI.CPTSeparation.Bounded.Program.time line 132
  17. def OAI.CPTSeparation.Bounded.env line 140
  18. def OAI.CPTSeparation.Bounded.result line 142
  19. def OAI.CPTSeparation.Bounded.Ready line 145
  20. lemma OAI.CPTSeparation.Bounded.ready_result line 149
  21. lemma OAI.CPTSeparation.Bounded.env_result line 151
  22. lemma OAI.CPTSeparation.Bounded.result_result line 153
  23. lemma OAI.CPTSeparation.Bounded.ready_index line 155
  24. lemma OAI.CPTSeparation.Bounded.env_index line 171
  25. lemma OAI.CPTSeparation.Bounded.equalCode_runs line 175
  26. lemma OAI.CPTSeparation.Bounded.cell_runs line 195
  27. lemma OAI.CPTSeparation.Bounded.compile_runs line 211
  28. abbrev OAI.CPTSeparation.Bounded.Relation line 260
  29. def OAI.CPTSeparation.Bounded.readTable line 262
  30. def OAI.CPTSeparation.Bounded.Program.interpret line 265
  31. lemma OAI.CPTSeparation.Bounded.Program.eval_interpret line 274
  32. lemma OAI.CPTSeparation.Bounded.readTable_input line 288
  33. lemma OAI.CPTSeparation.Bounded.fold_emits line 293
  34. lemma OAI.CPTSeparation.Bounded.loop_emits line 303
  35. lemma OAI.CPTSeparation.Bounded.Program.time_polynomial line 311