OAI/Analysis/PeriodicLattice/Tape.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Tape digits, stack evolution and effective local transition tables.

  1. theorem OAI.PeriodicLattice.MachineFacts.lookup_bounds line 16
  2. def OAI.PeriodicLattice.TapeDigits.digit line 37
  3. theorem OAI.PeriodicLattice.TapeDigits.digit_zero line 39
  4. theorem OAI.PeriodicLattice.TapeDigits.digit_blank line 41
  5. theorem OAI.PeriodicLattice.TapeDigits.digit_succ line 43
  6. theorem OAI.PeriodicLattice.TapeDigits.digit_cons_zero line 46
  7. theorem OAI.PeriodicLattice.TapeDigits.digit_cons_succ line 49
  8. theorem OAI.PeriodicLattice.TapeDigits.sub_top line 54
  9. theorem OAI.PeriodicLattice.TapeDigits.digit_ofDigits line 58
  10. def OAI.PeriodicLattice.StackCode.Represents line 79
  11. def OAI.PeriodicLattice.StackCode.initialCode line 84
  12. theorem OAI.PeriodicLattice.StackCode.initial_represents line 87
  13. theorem OAI.PeriodicLattice.StackCode.scan_eq line 100
  14. theorem OAI.PeriodicLattice.StackCode.step_represents line 103
  15. def OAI.PeriodicLattice.StackCode.machineStackStep line 176
  16. def OAI.PeriodicLattice.StackCode.stackExecution line 179
  17. theorem OAI.PeriodicLattice.StackCode.stackExecution_zero line 182
  18. theorem OAI.PeriodicLattice.StackCode.stackExecution_succ line 185
  19. theorem OAI.PeriodicLattice.StackCode.stackExecution_represents line 189
  20. theorem OAI.PeriodicLattice.StackCode.stackExecution_bounds line 208
  21. def OAI.PeriodicLattice.StackCode.configurationCode line 238
  22. theorem OAI.PeriodicLattice.StackCode.configurationCode_bound line 241
  23. theorem OAI.PeriodicLattice.StackCode.decode_configurationCode line 247
  24. def OAI.PeriodicLattice.RuleTable.halt line 259
  25. def OAI.PeriodicLattice.RuleTable.next line 263
  26. theorem OAI.PeriodicLattice.RuleTable.halt_periodic line 267
  27. theorem OAI.PeriodicLattice.RuleTable.next_periodic line 272
  28. theorem OAI.PeriodicLattice.RuleTable.next_bound line 277
  29. theorem OAI.PeriodicLattice.RuleTable.halt_code line 294
  30. theorem OAI.PeriodicLattice.RuleTable.next_code line 301
  31. theorem OAI.PeriodicLattice.Planar.codes_prefix line 317
  32. theorem OAI.PeriodicLattice.Planar.codes_flag_iff line 326