OAI/Computability/WeisfeilerLeman/Circuits.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLTime.CircuitEncoding.Bit line 8
  2. def OAI.WLTime.CircuitEncoding.zeroSet line 10
  3. theorem OAI.WLTime.CircuitEncoding.zeroSet_nonempty line 13
  4. theorem OAI.WLTime.CircuitEncoding.image_singleton_of_forall line 16
  5. theorem OAI.WLTime.CircuitEncoding.const_image line 25
  6. theorem OAI.WLTime.CircuitEncoding.value_of_image_singleton line 29
  7. theorem OAI.WLTime.CircuitEncoding.zeroSet_coord_image line 36
  8. theorem OAI.WLTime.CircuitEncoding.zeroSet_sum_image line 51
  9. def OAI.WLTime.CircuitEncoding.diode line 71
  10. theorem OAI.WLTime.CircuitEncoding.diode_nonempty line 73
  11. theorem OAI.WLTime.CircuitEncoding.diode_coord_image line 77
  12. theorem OAI.WLTime.CircuitEncoding.diode_sum_image line 88
  13. inductive OAI.WLTime.CircuitEncoding.Kind line 95
  14. def OAI.WLTime.CircuitEncoding.Kind.dim line 99
  15. theorem OAI.WLTime.CircuitEncoding.Kind.dim_pos line 103
  16. structure OAI.WLTime.CircuitEncoding.Circuit line 105
  17. def OAI.WLTime.CircuitEncoding.Circuit.TrueAt line 121
  18. def OAI.WLTime.CircuitEncoding.Circuit.PortTrue line 131
  19. def OAI.WLTime.CircuitEncoding.Circuit.Forced line 134
  20. abbrev OAI.WLTime.CircuitEncoding.Circuit.Value line 137
  21. def OAI.WLTime.CircuitEncoding.Circuit.output line 139
  22. structure OAI.WLTime.CircuitEncoding.Circuit.Witness line 141
  23. theorem OAI.WLTime.CircuitEncoding.Circuit.all_forced_iff line 158
  24. theorem OAI.WLTime.CircuitEncoding.Circuit.port_true_forced line 165
  25. theorem OAI.WLTime.CircuitEncoding.Circuit.true_of_seed line 174
  26. theorem OAI.WLTime.CircuitEncoding.Circuit.output_scalar_eq_port line 178
  27. theorem OAI.WLTime.CircuitEncoding.Circuit.Witness.port_zero line 195
  28. theorem OAI.WLTime.CircuitEncoding.Circuit.Witness.output_zero line 203
  29. theorem OAI.WLTime.CircuitEncoding.Circuit.Witness.true_output_zero line 213
  30. theorem OAI.WLTime.CircuitEncoding.Circuit.Witness.all_tests_false line 236
  31. def OAI.WLTime.CircuitEncoding.Circuit.canonicalGate line 245
  32. theorem OAI.WLTime.CircuitEncoding.Circuit.canonicalGate_nonempty line 248
  33. theorem OAI.WLTime.CircuitEncoding.Circuit.canonicalGate_output line 256
  34. theorem OAI.WLTime.CircuitEncoding.Circuit.canonicalGate_port_true line 266
  35. def OAI.WLTime.CircuitEncoding.Circuit.canonicalBuffer line 280
  36. theorem OAI.WLTime.CircuitEncoding.Circuit.canonicalBuffer_nonempty line 284
  37. theorem OAI.WLTime.CircuitEncoding.Circuit.canonicalBuffer_coord line 291
  38. theorem OAI.WLTime.CircuitEncoding.Circuit.canonicalBuffer_sum line 301
  39. def OAI.WLTime.CircuitEncoding.Circuit.canonicalWitness line 311
  40. theorem OAI.WLTime.CircuitEncoding.Circuit.witness_iff_tests_false line 327
  41. theorem OAI.WLTime.CircuitEncoding.Circuit.truth_iff_of_equations line 335
  42. def OAI.WLTime.CircuitEncoding.Tableau.update line 369
  43. def OAI.WLTime.CircuitEncoding.Tableau.run line 370
  44. theorem OAI.WLTime.CircuitEncoding.Tableau.run_zero line 374
  45. theorem OAI.WLTime.CircuitEncoding.Tableau.run_succ line 375
  46. inductive OAI.WLTime.CircuitEncoding.Tableau.Gate line 379
  47. abbrev OAI.WLTime.CircuitEncoding.Tableau.Node line 385
  48. def OAI.WLTime.CircuitEncoding.Tableau.Gate.kind line 387
  49. def OAI.WLTime.CircuitEncoding.Tableau.Gate.phase line 391
  50. def OAI.WLTime.CircuitEncoding.Tableau.prevTime line 396
  51. inductive OAI.WLTime.CircuitEncoding.Tableau.Connection line 398
  52. def OAI.WLTime.CircuitEncoding.Tableau.source line 407
  53. def OAI.WLTime.CircuitEncoding.Tableau.target line 414
  54. def OAI.WLTime.CircuitEncoding.Tableau.port line 421
  55. def OAI.WLTime.CircuitEncoding.Tableau.rank line 428
  56. theorem OAI.WLTime.CircuitEncoding.Tableau.forward line 430
  57. def OAI.WLTime.CircuitEncoding.Tableau.seed line 434
  58. def OAI.WLTime.CircuitEncoding.Tableau.test line 439
  59. def OAI.WLTime.CircuitEncoding.Tableau.circuit line 444
  60. def OAI.WLTime.CircuitEncoding.Tableau.expected line 463
  61. theorem OAI.WLTime.CircuitEncoding.Tableau.incoming_first line 473
  62. theorem OAI.WLTime.CircuitEncoding.Tableau.incoming_second line 497
  63. theorem OAI.WLTime.CircuitEncoding.Tableau.incoming_scalar line 520
  64. theorem OAI.WLTime.CircuitEncoding.Tableau.expected_equations line 537
  65. theorem OAI.WLTime.CircuitEncoding.Tableau.truth_iff_expected line 593
  66. theorem OAI.WLTime.CircuitEncoding.Tableau.tests_false_iff line 598