OAI/Analysis/PeriodicLattice/Machines.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Machine histories, encoded stacks and the open particle detector.

  1. def OAI.PeriodicLattice.History.address line 18
  2. def OAI.PeriodicLattice.History.coordinate line 21
  3. theorem OAI.PeriodicLattice.History.epsilon_ratio line 24
  4. theorem OAI.PeriodicLattice.History.read_coordinate line 31
  5. theorem OAI.PeriodicLattice.History.read_residue line 44
  6. theorem OAI.PeriodicLattice.History.lift_invariant_residue line 55
  7. theorem OAI.PeriodicLattice.History.read_any_lift line 66
  8. structure OAI.PeriodicLattice.StackCode.Code line 82
  9. def OAI.PeriodicLattice.StackCode.pack line 88
  10. def OAI.PeriodicLattice.StackCode.unpackNat line 91
  11. def OAI.PeriodicLattice.StackCode.residue line 96
  12. def OAI.PeriodicLattice.StackCode.unpack line 98
  13. theorem OAI.PeriodicLattice.StackCode.pack_eq line 100
  14. theorem OAI.PeriodicLattice.StackCode.pack_lt line 105
  15. theorem OAI.PeriodicLattice.StackCode.unpackNat_pack line 116
  16. theorem OAI.PeriodicLattice.StackCode.unpackNat_state line 123
  17. theorem OAI.PeriodicLattice.StackCode.residue_periodic line 127
  18. theorem OAI.PeriodicLattice.StackCode.unpack_periodic line 132
  19. theorem OAI.PeriodicLattice.StackCode.residue_lt line 137
  20. theorem OAI.PeriodicLattice.StackCode.unpack_pack line 146
  21. theorem OAI.PeriodicLattice.StackCode.tail_bound line 154
  22. def OAI.PeriodicLattice.StackCode.step line 168
  23. theorem OAI.PeriodicLattice.StackCode.step_stacks_lt line 177
  24. theorem OAI.PeriodicLattice.StackCode.step_state line 206
  25. theorem OAI.PeriodicLattice.StackCode.step_pack_lt line 211
  26. theorem OAI.PeriodicLattice.Detector.isOpen line 223
  27. theorem OAI.PeriodicLattice.Detector.mem_iff line 233
  28. theorem OAI.PeriodicLattice.Detector.initial_not_mem line 248