OAI/Computability/WeisfeilerLeman/Expressions.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.UnaryPrograms.skipFieldLoop line 11
  2. def OAI.WLTime.UnaryPrograms.skipField line 12
  3. theorem OAI.WLTime.UnaryPrograms.skipFieldLoop_exec line 14
  4. theorem OAI.WLTime.UnaryPrograms.skipField_exec line 41
  5. theorem OAI.WLTime.UnaryPrograms.scan_tail_le line 47
  6. def OAI.WLTime.UnaryPrograms.tailField line 52
  7. def OAI.WLTime.UnaryPrograms.skipEntry line 54
  8. theorem OAI.WLTime.UnaryPrograms.skipEntry_exec line 57
  9. def OAI.WLTime.UnaryPrograms.seek line 73
  10. theorem OAI.WLTime.UnaryPrograms.tailField_iterate_le line 75
  11. theorem OAI.WLTime.UnaryPrograms.seek_exec line 83
  12. def OAI.WLTime.UnaryPrograms.prependRecord line 109
  13. theorem OAI.WLTime.UnaryPrograms.prependRecord_exec line 111
  14. theorem OAI.WLTime.UnaryPrograms.numeral_length line 119
  15. theorem OAI.WLTime.UnaryPrograms.numeral_add line 121
  16. def OAI.WLTime.UnaryPrograms.mulAdd line 124
  17. theorem OAI.WLTime.UnaryPrograms.mulAdd_exec line 126
  18. def OAI.WLTime.TypedStack.Program.relabel line 158
  19. theorem OAI.WLTime.TypedStack.Program.relabel_exec line 161
  20. def OAI.WLTime.TypedStack.Program.pushes line 177
  21. theorem OAI.WLTime.TypedStack.Program.pushes_exec line 181
  22. def OAI.WLTime.TypedStack.Program.overwrite line 191
  23. theorem OAI.WLTime.TypedStack.Program.overwrite_exec line 193
  24. def OAI.WLTime.TypedStack.Program.putNat line 199
  25. theorem OAI.WLTime.TypedStack.Program.putNat_exec line 201
  26. def OAI.WLTime.TypedStack.Program.dropN line 208
  27. theorem OAI.WLTime.TypedStack.Program.dropN_exec line 210
  28. def OAI.WLTime.TypedStack.Program.putBit line 227
  29. theorem OAI.WLTime.TypedStack.Program.putBit_exec line 230
  30. inductive OAI.WLTime.NatCode.Binary line 259
  31. def OAI.WLTime.NatCode.Binary.eval line 263
  32. def OAI.WLTime.NatCode.core line 270
  33. theorem OAI.WLTime.NatCode.core_exec line 276
  34. def OAI.WLTime.NatCode.binary line 309
  35. theorem OAI.WLTime.NatCode.binary_exec line 312
  36. def OAI.WLTime.NatCode.bitAt line 326
  37. theorem OAI.WLTime.NatCode.bitAt_exec line 331
  38. inductive OAI.WLTime.NatCode.Expr line 380
  39. def OAI.WLTime.NatCode.Expr.eval line 389
  40. def OAI.WLTime.NatCode.Expr.Bounded line 395
  41. theorem OAI.WLTime.NatCode.Expr.eval_le line 401
  42. def OAI.WLTime.NatCode.Expr.charge line 409
  43. def OAI.WLTime.NatCode.Expr.compile line 414
  44. theorem OAI.WLTime.NatCode.Expr.compile_exec line 426