OAI/Combinatorics/VariableWL/Procedure.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Computation.Stack.Procedure.extend line 9
  2. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_front line 12
  3. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_back line 16
  4. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_zero line 19
  5. def OAI.VariableWL.Computation.Stack.Procedure.widen line 23
  6. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_project line 26
  7. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_put line 31
  8. theorem OAI.VariableWL.Computation.Stack.Procedure.eval_widen line 49
  9. def OAI.VariableWL.Computation.Stack.Procedure.Realizes line 57
  10. theorem OAI.VariableWL.Computation.Stack.Procedure.monotone line 60
  11. theorem OAI.VariableWL.Computation.Stack.Procedure.direct line 67
  12. theorem OAI.VariableWL.Computation.Stack.Procedure.identity line 72
  13. theorem OAI.VariableWL.Computation.Stack.Procedure.seq line 75
  14. theorem OAI.VariableWL.Computation.Stack.Procedure.clear line 87
  15. theorem OAI.VariableWL.Computation.Stack.Procedure.push line 91
  16. theorem OAI.VariableWL.Computation.Stack.Procedure.pop line 95
  17. theorem OAI.VariableWL.Computation.Stack.Procedure.action line 99
  18. theorem OAI.VariableWL.Computation.Stack.Procedure.outputs line 103
  19. def OAI.VariableWL.Computation.Stack.Procedure.front line 134
  20. theorem OAI.VariableWL.Computation.Stack.Procedure.heads_extend line 136
  21. theorem OAI.VariableWL.Computation.Stack.Procedure.branch line 141
  22. theorem OAI.VariableWL.Computation.Stack.Procedure.state_extend line 162
  23. theorem OAI.VariableWL.Computation.Stack.Procedure.total_mono line 173
  24. theorem OAI.VariableWL.Computation.Stack.Procedure.countedLoop line 183
  25. theorem OAI.VariableWL.Computation.Stack.Procedure.countedLoop_bound line 204
  26. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_front' line 217
  27. theorem OAI.VariableWL.Computation.Stack.Procedure.state_base line 220
  28. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_update line 225
  29. theorem OAI.VariableWL.Computation.Stack.Procedure.reverseCopy line 242
  30. theorem OAI.VariableWL.Computation.Stack.Procedure.transfer line 259
  31. def OAI.VariableWL.Computation.Stack.Procedure.pushWord line 264
  32. theorem OAI.VariableWL.Computation.Stack.Procedure.eval_pushWord line 268
  33. theorem OAI.VariableWL.Computation.Stack.Procedure.prepend line 277
  34. theorem OAI.VariableWL.Computation.Stack.Procedure.constant line 281
  35. theorem OAI.VariableWL.Computation.Stack.Procedure.lengthAdd line 286
  36. theorem OAI.VariableWL.Computation.Stack.Procedure.copy line 291
  37. def OAI.VariableWL.Computation.Stack.Procedure.join line 339
  38. theorem OAI.VariableWL.Computation.Stack.Procedure.extend_nested line 341
  39. theorem OAI.VariableWL.Computation.Stack.Procedure.put_nested line 348
  40. theorem OAI.VariableWL.Computation.Stack.Procedure.localRegisters line 356
  41. theorem OAI.VariableWL.Computation.Stack.Procedure.iterate_update line 369
  42. theorem OAI.VariableWL.Computation.Stack.Procedure.iterate_tail line 377
  43. theorem OAI.VariableWL.Computation.Stack.Procedure.countedPop line 382