OAI/Combinatorics/VariableWL/BinaryMachine.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Computation.Stack.BinaryMachine.store line 8
  2. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.update_input line 11
  3. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.update_accumulator line 16
  4. def OAI.VariableWL.Computation.Stack.BinaryMachine.double line 21
  5. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.eval_double line 23
  6. def OAI.VariableWL.Computation.Stack.BinaryMachine.addBit line 43
  7. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.eval_addBit line 45
  8. def OAI.VariableWL.Computation.Stack.BinaryMachine.body line 61
  9. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.eval_body line 63
  10. def OAI.VariableWL.Computation.Stack.BinaryMachine.program line 73
  11. def OAI.VariableWL.Computation.Stack.BinaryMachine.value line 75
  12. def OAI.VariableWL.Computation.Stack.BinaryMachine.time line 79
  13. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.eval_program line 83
  14. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.value_bound line 94
  15. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.time_bound line 103
  16. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.value_append line 120
  17. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.value_reverse line 125
  18. def OAI.VariableWL.Computation.Stack.BinaryMachine.machine line 133
  19. theorem OAI.VariableWL.Computation.Stack.BinaryMachine.outputs line 135
  20. def OAI.VariableWL.Computation.Stack.ArrayLookup.store line 159
  21. theorem OAI.VariableWL.Computation.Stack.ArrayLookup.update_query line 163
  22. theorem OAI.VariableWL.Computation.Stack.ArrayLookup.update_output line 168
  23. def OAI.VariableWL.Computation.Stack.ArrayLookup.clone line 173
  24. theorem OAI.VariableWL.Computation.Stack.ArrayLookup.eval_clone line 175
  25. def OAI.VariableWL.Computation.Stack.ArrayLookup.scan line 196
  26. theorem OAI.VariableWL.Computation.Stack.ArrayLookup.scan_action line 199
  27. theorem OAI.VariableWL.Computation.Stack.ArrayLookup.eval_scan line 205
  28. def OAI.VariableWL.Computation.Stack.ArrayLookup.readHead line 220
  29. theorem OAI.VariableWL.Computation.Stack.ArrayLookup.eval_readHead line 222
  30. def OAI.VariableWL.Computation.Stack.ArrayLookup.program line 232
  31. theorem OAI.VariableWL.Computation.Stack.ArrayLookup.eval_program line 234
  32. theorem OAI.VariableWL.Computation.Stack.ArrayLookup.time_bound line 250
  33. def OAI.VariableWL.Computation.Stack.Halving.store line 260
  34. def OAI.VariableWL.Computation.Stack.Halving.pair line 264
  35. def OAI.VariableWL.Computation.Stack.Halving.body line 267
  36. def OAI.VariableWL.Computation.Stack.Halving.program line 269
  37. theorem OAI.VariableWL.Computation.Stack.Halving.eval_pop_first line 271
  38. theorem OAI.VariableWL.Computation.Stack.Halving.eval_pair line 280
  39. theorem OAI.VariableWL.Computation.Stack.Halving.eval_last line 290
  40. theorem OAI.VariableWL.Computation.Stack.Halving.eval_body_pair line 298
  41. theorem OAI.VariableWL.Computation.Stack.Halving.eval_body_last line 303
  42. theorem OAI.VariableWL.Computation.Stack.Halving.eval_program line 308
  43. theorem OAI.VariableWL.Computation.Stack.Halving.time_bound line 330