OAI/Computability/WeisfeilerLeman/Writer.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.Marking.rectangleAdj line 10
  2. theorem OAI.WLTime.Marking.decodeSlots_adj line 14
  3. def OAI.WLTime.NatCode.Expr.add line 50
  4. def OAI.WLTime.NatCode.Expr.mul line 51
  5. theorem OAI.WLTime.NatCode.Expr.add_eval line 52
  6. theorem OAI.WLTime.NatCode.Expr.mul_eval line 54
  7. def OAI.WLTime.NatCode.Predicate.le line 59
  8. theorem OAI.WLTime.NatCode.Predicate.le_holds line 60
  9. def OAI.WLTime.NatCode.Predicate.rectangular line 64
  10. theorem OAI.WLTime.NatCode.Predicate.rectangular_holds line 69
  11. def OAI.WLTime.OneTape.Symbolic.coefficient line 85
  12. def OAI.WLTime.OneTape.Symbolic.countExpr line 88
  13. theorem OAI.WLTime.OneTape.Symbolic.countExpr_correct line 92
  14. def OAI.WLTime.OneTape.Symbolic.sameRect line 101
  15. theorem OAI.WLTime.OneTape.Symbolic.sameRect_correct line 105
  16. def OAI.WLTime.OneTape.Symbolic.slotPredicate line 114
  17. theorem OAI.WLTime.OneTape.Symbolic.slotPredicate_correct line 120
  18. theorem OAI.WLTime.UnaryPrograms.countdown_indexed line 162
  19. theorem OAI.WLTime.UnaryPrograms.repeat_indexed line 182
  20. theorem OAI.WLTime.TypedStack.Program.repeat_indexed line 202
  21. inductive OAI.WLTime.NatCode.Writer line 222
  22. def OAI.WLTime.NatCode.Writer.eval line 230
  23. def OAI.WLTime.NatCode.Writer.depth line 235
  24. def OAI.WLTime.NatCode.Writer.charge line 240
  25. def OAI.WLTime.NatCode.Writer.Safe line 245
  26. def OAI.WLTime.NatCode.Writer.compile line 250
  27. theorem OAI.WLTime.NatCode.Writer.numeral_bool_head line 263
  28. theorem OAI.WLTime.NatCode.Writer.emit_exec line 266
  29. theorem OAI.WLTime.NatCode.Writer.compile_exec line 296
  30. def OAI.WLTime.NatCode.Expr.rename line 403
  31. theorem OAI.WLTime.NatCode.Expr.rename_eval line 404
  32. theorem OAI.WLTime.NatCode.Expr.rename_bounded line 406
  33. def OAI.WLTime.NatCode.Writer.empty line 421
  34. theorem OAI.WLTime.NatCode.Writer.empty_eval line 422
  35. theorem OAI.WLTime.NatCode.Writer.empty_depth line 423
  36. theorem OAI.WLTime.NatCode.Writer.empty_safe line 424
  37. def OAI.WLTime.NatCode.Writer.each line 426
  38. theorem OAI.WLTime.NatCode.Writer.each_eval line 427
  39. theorem OAI.WLTime.NatCode.Writer.each_safe line 434
  40. theorem OAI.WLTime.NatCode.Writer.each_depth_le line 439
  41. def OAI.WLTime.NatCode.Writer.grid line 445
  42. theorem OAI.WLTime.NatCode.Writer.grid_eval line 447
  43. theorem OAI.WLTime.NatCode.Writer.grid_safe line 454
  44. theorem OAI.WLTime.NatCode.Writer.grid_depth line 464