OAI/Combinatorics/VariableWL/BoundedLoop.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Computation.Stack.Code.put line 8
  2. theorem OAI.VariableWL.Computation.Stack.Code.put_apply line 12
  3. theorem OAI.VariableWL.Computation.Stack.Code.put_outside line 20
  4. theorem OAI.VariableWL.Computation.Stack.Code.put_self line 25
  5. theorem OAI.VariableWL.Computation.Stack.Code.put_put line 32
  6. def OAI.VariableWL.Computation.Stack.Code.liftAction line 40
  7. theorem OAI.VariableWL.Computation.Stack.Code.liftAction_apply line 44
  8. theorem OAI.VariableWL.Computation.Stack.Code.liftAction_outside line 52
  9. theorem OAI.VariableWL.Computation.Stack.Code.execute_liftAction line 57
  10. theorem OAI.VariableWL.Computation.Stack.Code.heads_put line 66
  11. def OAI.VariableWL.Computation.Stack.Code.rename line 71
  12. theorem OAI.VariableWL.Computation.Stack.Code.eval_rename line 78
  13. theorem OAI.VariableWL.Computation.Stack.Code.eval_rename_from line 95
  14. def OAI.VariableWL.Computation.Stack.BoundedLoop.embed line 105
  15. def OAI.VariableWL.Computation.Stack.BoundedLoop.counter line 106
  16. def OAI.VariableWL.Computation.Stack.BoundedLoop.scratch line 107
  17. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.counter_ne line 109
  18. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.scratch_ne line 115
  19. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.counter_scratch line 121
  20. def OAI.VariableWL.Computation.Stack.BoundedLoop.state line 127
  21. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.state_embed line 130
  22. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.state_counter line 133
  23. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.state_scratch line 140
  24. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.cases_index line 147
  25. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.update_counter line 158
  26. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.put_state line 166
  27. def OAI.VariableWL.Computation.Stack.BoundedLoop.loopBody line 169
  28. def OAI.VariableWL.Computation.Stack.BoundedLoop.loop line 170
  29. def OAI.VariableWL.Computation.Stack.BoundedLoop.program line 171
  30. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.eval_body line 174
  31. def OAI.VariableWL.Computation.Stack.BoundedLoop.total line 185
  32. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.eval_loop line 189
  33. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.eval_program line 203
  34. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.total_bound line 217
  35. theorem OAI.VariableWL.Computation.Stack.BoundedLoop.program_bound line 226
  36. def OAI.VariableWL.TupleAddress.encode line 235
  37. def OAI.VariableWL.TupleAddress.digit line 237
  38. def OAI.VariableWL.TupleAddress.replace line 239
  39. theorem OAI.VariableWL.TupleAddress.encode_lt line 241
  40. theorem OAI.VariableWL.TupleAddress.digit_encode line 244
  41. theorem OAI.VariableWL.TupleAddress.encode_sum line 249
  42. theorem OAI.VariableWL.TupleAddress.encode_update line 252
  43. theorem OAI.VariableWL.TupleAddress.digit_unpack line 269
  44. theorem OAI.VariableWL.TupleAddress.encode_unpack line 272
  45. theorem OAI.VariableWL.TupleAddress.replace_lt line 275
  46. theorem OAI.VariableWL.TupleAddress.decode_replace line 280