OAI/Analysis/MatrixSigning/Machines/BinaryMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.KS.W29.StackAction line 9
  2. def OAI.KS.W29.StackAction.apply line 15
  3. theorem OAI.KS.W29.StackAction.length_apply_le line 20
  4. structure OAI.KS.W29.Instruction line 25
  5. def OAI.KS.W29.Instruction.action line 32
  6. def OAI.KS.W29.Instruction.halt line 35
  7. structure OAI.KS.W29.BinaryMachine line 38
  8. structure OAI.KS.W29.Config line 43
  9. def OAI.KS.W29.topCode line 47
  10. theorem OAI.KS.W29.topCode_lt_three line 52
  11. def OAI.KS.W29.headCode line 57
  12. theorem OAI.KS.W29.headCode_lt line 60
  13. def OAI.KS.W29.bitCode line 67
  14. def OAI.KS.W29.transitionIndex line 69
  15. theorem OAI.KS.W29.transitionIndex_lt line 72
  16. def OAI.KS.W29.BinaryMachine.step line 80
  17. def OAI.KS.W29.BinaryMachine.init line 88
  18. def OAI.KS.W29.BinaryMachine.run line 91
  19. def OAI.KS.W29.BinaryMachine.output line 95
  20. theorem OAI.KS.W29.BinaryMachine.step_halted line 98
  21. theorem OAI.KS.W29.BinaryMachine.run_halted line 102
  22. theorem OAI.KS.W29.BinaryMachine.run_append line 108
  23. theorem OAI.KS.W29.BinaryMachine.step_stack_length_le line 114
  24. theorem OAI.KS.W29.BinaryMachine.run_stack_length_le line 121
  25. theorem OAI.KS.W29.BinaryMachine.output_length_le line 132
  26. def OAI.KS.W29.polynomialFuel line 137
  27. abbrev OAI.KS.W29.FairSeed line 140
  28. def OAI.KS.W29.BinaryMachine.runSeed line 142
  29. def OAI.KS.W29.BinaryMachine.successCount line 145
  30. def OAI.KS.W29.BinaryMachine.HaltsWithin line 151
  31. def OAI.KS.W29.BinaryMachine.SucceedsTwoThirds line 154
  32. theorem OAI.KS.W29.BinaryMachine.haltsWithin_iff_bitLists line 158
  33. theorem OAI.KS.W29.BinaryMachine.run_append_of_halted line 168
  34. theorem OAI.KS.W29.BinaryMachine.haltsWithin_mono line 173
  35. theorem OAI.KS.W29.BinaryMachine.runSeed_output_length_le line 187