OAI/Analysis/MatrixSigning/Machines/ExpressionSyntax.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.KS.W13.ExpressionMachine.Op line 12
  2. def OAI.KS.W13.ExpressionMachine.Op.encode line 17
  3. def OAI.KS.W13.ExpressionMachine.encodeOps line 25
  4. def OAI.KS.W13.ExpressionMachine.postorder line 27
  5. def OAI.KS.W13.ExpressionMachine.encodeExpr line 35
  6. def OAI.KS.W13.ExpressionMachine.encodeStack line 37
  7. theorem OAI.KS.W13.ExpressionMachine.encodeOps_nil line 39
  8. theorem OAI.KS.W13.ExpressionMachine.encodeOps_cons line 40
  9. theorem OAI.KS.W13.ExpressionMachine.encodeOps_append line 42
  10. theorem OAI.KS.W13.ExpressionMachine.encodeStack_nil line 44
  11. theorem OAI.KS.W13.ExpressionMachine.encodeStack_cons line 45
  12. theorem OAI.KS.W13.ExpressionMachine.encodeOp_nonempty line 48
  13. theorem OAI.KS.W13.ExpressionMachine.encodeOps_cons_nonempty line 49
  14. theorem OAI.KS.W13.ExpressionMachine.postorder_length line 52
  15. theorem OAI.KS.W13.ExpressionMachine.encodeOps_length_ge line 55
  16. theorem OAI.KS.W13.ExpressionMachine.nodes_le_syntax_length line 63
  17. def OAI.KS.W13.ExpressionMachine.Op.step line 67
  18. def OAI.KS.W13.ExpressionMachine.exec line 76
  19. theorem OAI.KS.W13.ExpressionMachine.exec_append line 80
  20. theorem OAI.KS.W13.ExpressionMachine.exec_postorder line 88
  21. inductive OAI.KS.W13.ExpressionMachine.Trace line 93
  22. theorem OAI.KS.W13.ExpressionMachine.trace_iff_exec line 97
  23. theorem OAI.KS.W13.ExpressionMachine.trace_postorder line 115
  24. def OAI.KS.W13.ExpressionMachine.ValueBound line 118
  25. def OAI.KS.W13.ExpressionMachine.SubtreeBound line 120
  26. inductive OAI.KS.W13.ExpressionMachine.BoundedTrace line 123
  27. theorem OAI.KS.W13.ExpressionMachine.BoundedTrace.toTrace line 128
  28. theorem OAI.KS.W13.ExpressionMachine.BoundedTrace.start_bound line 133
  29. theorem OAI.KS.W13.ExpressionMachine.BoundedTrace.end_bound line 136
  30. theorem OAI.KS.W13.ExpressionMachine.BoundedTrace.append line 139
  31. theorem OAI.KS.W13.ExpressionMachine.bounded_trace_postorder line 145