OAI/Computability/WeisfeilerLeman/Simulation.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.CircuitEncoding.Tableau.run_reindex line 11
  2. theorem OAI.WLTime.Digits.value_lt_base_iff line 23
  3. theorem OAI.WLTime.Digits.finEquiv_val line 37
  4. theorem OAI.WLTime.Digits.finEquiv_shift line 43
  5. def OAI.WLTime.OneTape.blankCell line 65
  6. def OAI.WLTime.OneTape.inputCell line 67
  7. theorem OAI.WLTime.OneTape.ring_initial_digits line 71
  8. theorem OAI.WLTime.OneTape.product_simulation line 95
  9. def OAI.WLTime.CircuitEncoding.BoxTableau.Formula.labelDomain line 128
  10. def OAI.WLTime.CircuitEncoding.BoxTableau.Formula.labelCoord line 139
  11. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.labelDomain_correct line 149
  12. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.labelCoord_correct line 168
  13. def OAI.WLTime.CircuitEncoding.BoxTableau.Formula.position line 187
  14. def OAI.WLTime.CircuitEncoding.BoxTableau.Formula.seed line 193
  15. def OAI.WLTime.CircuitEncoding.BoxTableau.Formula.test line 197
  16. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.position_correct line 200
  17. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.seed_correct line 216
  18. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.test_correct line 226
  19. def OAI.WLTime.OneTape.inputPredicate line 240
  20. theorem OAI.WLTime.OneTape.inputPredicate_correct line 247
  21. theorem OAI.WLTime.NatCode.Predicate.bounded_mono line 259
  22. theorem OAI.WLTime.NatCode.Predicate.bounded_disj line 268
  23. theorem OAI.WLTime.NatCode.Predicate.bounded_all line 271
  24. theorem OAI.WLTime.NatCode.Predicate.bounded_any line 279
  25. theorem OAI.WLTime.NatCode.Expr.addOne_bounded line 284
  26. theorem OAI.WLTime.NatCode.Expr.subOne_bounded line 290
  27. theorem OAI.WLTime.NatCode.Expr.incCode_bounded line 294
  28. theorem OAI.WLTime.NatCode.Expr.decCode_bounded line 302
  29. theorem OAI.WLTime.ProductBox.Formula.carryDomain_bounded line 315
  30. theorem OAI.WLTime.ProductBox.Formula.carryCoord_bounded line 324
  31. theorem OAI.WLTime.ProductBox.Formula.borrowCoord_bounded line 333
  32. theorem OAI.WLTime.ProductBox.Formula.borrowDomain_bounded line 342
  33. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.labelDomain_bounded line 353
  34. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.labelCoord_bounded line 377
  35. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.position_bounded line 403
  36. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.seed_bounded line 419
  37. theorem OAI.WLTime.CircuitEncoding.BoxTableau.Formula.test_bounded line 428