OAI/Computability/MinUncut/Machines/CodeFiniteMachine.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Costed.codeMachine line 15
  2. lemma OAI.MinUncut.Costed.codeMachine_finiteAlphabet line 27
  3. lemma OAI.MinUncut.Costed.codeMachine_init line 30
  4. lemma OAI.MinUncut.Costed.codeMachine_halt line 38
  5. def OAI.MinUncut.Costed.CodeRun.finiteMachine line 46
  6. def OAI.MinUncut.Costed.BooleanAdapter.encodedWord line 80
  7. def OAI.MinUncut.Costed.BooleanAdapter.encodeMachine line 81
  8. lemma OAI.MinUncut.Costed.BooleanAdapter.encode_output line 84
  9. def OAI.MinUncut.Costed.BooleanAdapter.next line 94
  10. def OAI.MinUncut.Costed.BooleanAdapter.emit line 99
  11. def OAI.MinUncut.Costed.BooleanAdapter.decodeMachine line 103
  12. lemma OAI.MinUncut.Costed.BooleanAdapter.decode_output line 105
  13. lemma OAI.MinUncut.Costed.BooleanAdapter.trList_bool_length line 112
  14. def OAI.MinUncut.Costed.BooleanAdapter.encode_run line 119
  15. def OAI.MinUncut.Costed.BooleanAdapter.decode_run line 126
  16. def OAI.MinUncut.Costed.booleanCodeMachine line 136
  17. lemma OAI.MinUncut.Costed.sequential_finiteAlphabet line 141
  18. lemma OAI.MinUncut.Costed.booleanCodeMachine_finiteAlphabet line 151
  19. def OAI.MinUncut.Costed.CodeRun.booleanMachine line 158