OAI/Analysis/MatrixSigning/Machines/FixedBranch.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.KS.W29.FixedBranch.Choice line 12
  2. structure OAI.KS.W29.FixedBranch.SelectInstruction line 18
  3. def OAI.KS.W29.FixedBranch.start line 22
  4. def OAI.KS.W29.FixedBranch.leftState line 24
  5. def OAI.KS.W29.FixedBranch.rightState line 27
  6. def OAI.KS.W29.FixedBranch.selectInstruction line 30
  7. def OAI.KS.W29.FixedBranch.leftInstruction line 37
  8. def OAI.KS.W29.FixedBranch.rightInstruction line 40
  9. def OAI.KS.W29.FixedBranch.dispatch line 43
  10. def OAI.KS.W29.FixedBranch.branch line 54
  11. theorem OAI.KS.W29.FixedBranch.branch_toMachine line 58
  12. theorem OAI.KS.W29.FixedBranch.branch_initial line 63
  13. theorem OAI.KS.W29.FixedBranch.branch_states line 66
  14. theorem OAI.KS.W29.FixedBranch.dispatch_start line 69
  15. theorem OAI.KS.W29.FixedBranch.dispatch_left line 73
  16. theorem OAI.KS.W29.FixedBranch.dispatch_right line 79
  17. def OAI.KS.W29.FixedBranch.liftLeft line 86
  18. def OAI.KS.W29.FixedBranch.liftRight line 89
  19. theorem OAI.KS.W29.FixedBranch.step_start line 92
  20. theorem OAI.KS.W29.FixedBranch.step_left line 103
  21. theorem OAI.KS.W29.FixedBranch.step_right line 114
  22. theorem OAI.KS.W29.FixedBranch.step_liftLeft line 125
  23. theorem OAI.KS.W29.FixedBranch.step_liftRight line 134
  24. theorem OAI.KS.W29.FixedBranch.run_left line 143
  25. theorem OAI.KS.W29.FixedBranch.run_right line 156
  26. theorem OAI.KS.W29.FixedBranch.haltsFromWithin line 169