OAI/Computability/WeisfeilerLeman/MatrixBounds.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.OneTape.matrixCoefficient line 11
  2. theorem OAI.WLTime.OneTape.computation_matrices line 18
  3. theorem OAI.WLTime.OneTape.bounded_acceptance line 47
  4. theorem OAI.WLTime.OneTape.product_bounded line 59
  5. theorem OAI.WLTime.OneTape.bounded_matrices line 85
  6. def OAI.WLTime.OneTape.Symbolic.baseOrder line 109
  7. theorem OAI.WLTime.OneTape.Symbolic.listing_length line 113
  8. def OAI.WLTime.OneTape.Symbolic.pairGraph line 125
  9. theorem OAI.WLTime.OneTape.Symbolic.pairGraph_diameter line 130
  10. theorem OAI.WLTime.OneTape.Symbolic.pairGraph_correct line 136
  11. def OAI.WLTime.OneTape.Symbolic.pairWriter line 155
  12. theorem OAI.WLTime.OneTape.Symbolic.pairWriter_eval line 158
  13. theorem OAI.WLTime.OneTape.Symbolic.pairWriter_depth line 170
  14. theorem OAI.WLTime.OneTape.Symbolic.pairWriter_safe line 173
  15. def OAI.WLTime.TypedStack.Code.controlSize line 184
  16. theorem OAI.WLTime.TypedStack.Code.card_state line 190
  17. theorem OAI.WLTime.TypedStack.Code.relabel_controlSize line 197
  18. def OAI.WLTime.TypedStack.Program.seqShared line 204
  19. theorem OAI.WLTime.TypedStack.Program.seqShared_exec line 208
  20. theorem OAI.WLTime.TypedStack.Program.seqShared_size line 212
  21. theorem OAI.WLTime.TypedStack.Program.pushes_scratch line 216
  22. theorem OAI.WLTime.TypedStack.Program.pushes_size line 219
  23. def OAI.WLTime.TypedStack.Program.doubleUnary line 224
  24. theorem OAI.WLTime.TypedStack.Program.doubleUnary_exec line 227
  25. theorem OAI.WLTime.TypedStack.Program.doubleUnary_scratch line 255
  26. def OAI.WLTime.TypedStack.Program.loadDigits line 257
  27. theorem OAI.WLTime.TypedStack.Program.loadDigits_scratch line 262
  28. theorem OAI.WLTime.TypedStack.Program.loadDigits_size line 267
  29. theorem OAI.WLTime.TypedStack.Program.loadDigits_exec line 277
  30. def OAI.WLTime.TypedStack.Program.loadNat line 299
  31. theorem OAI.WLTime.TypedStack.Program.loadNat_exec line 300
  32. theorem OAI.WLTime.TypedStack.Program.loadNat_size line 305
  33. def OAI.WLTime.TypedStack.Code.countLoop line 312
  34. theorem OAI.WLTime.TypedStack.Code.countLoop_exec line 313
  35. def OAI.WLTime.TypedStack.Program.countLength line 355
  36. theorem OAI.WLTime.TypedStack.Program.countLength_exec line 357
  37. def OAI.WLTime.NatCode.Expr.degree line 383
  38. def OAI.WLTime.NatCode.Expr.AtomsBounded line 388
  39. theorem OAI.WLTime.NatCode.Expr.degree_pos line 394
  40. theorem OAI.WLTime.NatCode.Expr.bounded_degree line 396