OAI/Computability/WeisfeilerLeman/Model.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.WLTime.Convention line 7

   Also declared: ComparatorChallenges/WeisfeilerLeman.lean:7 (same declaration text).

2. def OAI.WLTime.Graph line 11

   Also declared: ComparatorChallenges/WeisfeilerLeman.lean:11 (same declaration text).

3. def OAI.WLTime.Graph.adj line 17

   Also declared: ComparatorChallenges/WeisfeilerLeman.lean:17 (same declaration text).

4. def OAI.WLTime.Graph.diameterTwo line 19

   Also declared: ComparatorChallenges/WeisfeilerLeman.lean:19 (same declaration text).

5. instance OAI.WLTime.Graph.(instance at line 23) line 23
6. abbrev OAI.WLTime.AtomicColor line 30

   Also declared: ComparatorChallenges/WeisfeilerLeman.lean:30 (same declaration text).

7. def OAI.WLTime.Color line 33

   Also declared: ComparatorChallenges/WeisfeilerLeman.lean:33 (same declaration text).

8. def OAI.WLTime.tupleColor line 39

   Also declared: ComparatorChallenges/WeisfeilerLeman.lean:39 (same declaration text).

9. def OAI.WLTime.histogram line 50

   Also declared: ComparatorChallenges/WeisfeilerLeman.lean:50 (same declaration text).

10. def OAI.WLTime.Equivalent line 54

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:54 (same declaration text).

11. def OAI.WLTime.encodeNat line 57

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:57 (same declaration text).

12. def OAI.WLTime.matrixBits line 61

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:61 (same declaration text).

13. def OAI.WLTime.encodePair line 64

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:64 (same declaration text).

14. inductive OAI.WLTime.Move line 67

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:67 (same declaration text).

15. def OAI.WLTime.Move.displacement line 71

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:71 (same declaration text).

16. structure OAI.WLTime.TM line 76

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:76 (same declaration text).

17. structure OAI.WLTime.TM.Config line 88

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:88 (same declaration text).

18. def OAI.WLTime.TM.symbol line 93

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:93 (same declaration text).

19. def OAI.WLTime.TM.initial line 97

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:97 (same declaration text).

20. def OAI.WLTime.TM.halted line 103

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:103 (same declaration text).

21. instance OAI.WLTime.TM.(instance at line 105) line 105
22. def OAI.WLTime.TM.step line 108

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:108 (same declaration text).

23. def OAI.WLTime.TM.run line 115

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:115 (same declaration text).

24. def OAI.WLTime.TM.halts line 117

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:117 (same declaration text).

25. def OAI.WLTime.TM.time line 119

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:119 (same declaration text).

26. def OAI.WLTime.TM.accepts line 123

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:123 (same declaration text).

27. def OAI.WLTime.TM.outputs line 126

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:126 (same declaration text).

28. abbrev OAI.WLTime.Word line 133

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:133 (same declaration text).

29. def OAI.WLTime.wordBits line 135

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:135 (same declaration text).

30. def OAI.WLTime.registerBits line 138

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:138 (same declaration text).

31. structure OAI.WLTime.WordOperation line 141

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:141 (same declaration text).

32. inductive OAI.WLTime.RAMInstruction line 151

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:151 (same declaration text).

33. structure OAI.WLTime.WordWidth line 159

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:159 (same declaration text).

34. structure OAI.WLTime.RAM line 165

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:165 (same declaration text).

35. structure OAI.WLTime.RAM.Config line 176

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:176 (same declaration text).

36. def OAI.WLTime.RAM.packedWord line 182

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:182 (same declaration text).

37. def OAI.WLTime.RAM.initial line 186

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:186 (same declaration text).

38. def OAI.WLTime.RAM.execute line 192

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:192 (same declaration text).

39. def OAI.WLTime.RAM.step line 205

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:205 (same declaration text).

40. def OAI.WLTime.RAM.run line 210

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:210 (same declaration text).

41. def OAI.WLTime.RAM.halts line 213

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:213 (same declaration text).

42. def OAI.WLTime.RAM.time line 216

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:216 (same declaration text).

43. def OAI.WLTime.RAM.accepts line 220

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:220 (same declaration text).

44. inductive OAI.WLTime.Model line 225

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:225 (same declaration text).

45. def OAI.WLTime.Model.halts line 229

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:229 (same declaration text).

46. def OAI.WLTime.Model.accepts line 233

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:233 (same declaration text).

47. def OAI.WLTime.Model.time line 237

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:237 (same declaration text).

48. inductive OAI.WLTime.InputClass line 241

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:241 (same declaration text).

49. def OAI.WLTime.InputClass.contains line 245

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:245 (same declaration text).

50. def OAI.WLTime.Decides line 249

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:249 (same declaration text).

51. def OAI.WLTime.worstTime line 254

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:254 (same declaration text).

52. def OAI.WLTime.MainClaim line 259

    Also declared: ComparatorChallenges/WeisfeilerLeman.lean:259 (same declaration text).