OAI/GroupTheory/PeriodicGroups/Rules/CommittedWords.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.FiniteTable.Verification.binary_acquire_good line 14
  2. lemma OAI.SourceBurnside.FiniteTable.Verification.binary_read_left_good line 37
  3. lemma OAI.SourceBurnside.FiniteTable.Verification.binary_read_right_good line 64
  4. lemma OAI.SourceBurnside.FiniteTable.Verification.binary_undo_left_good line 86
  5. lemma OAI.SourceBurnside.FiniteTable.Verification.binary_undo_right_good line 108
  6. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_binary_fields line 136
  7. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_binary line 152
  8. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_cast line 184
  9. def OAI.SourceBurnside.FiniteTable.Verification.WordGood line 189
  10. lemma OAI.SourceBurnside.FiniteTable.Verification.wordGood_ofFn line 192
  11. lemma OAI.SourceBurnside.FiniteTable.Verification.coherent_of_syntax line 199
  12. lemma OAI.SourceBurnside.FiniteTable.Verification.get_of_context line 209
  13. lemma OAI.SourceBurnside.FiniteTable.Verification.off_of_context line 221
  14. lemma OAI.SourceBurnside.FiniteTable.Verification.unary_context_good line 236
  15. lemma OAI.SourceBurnside.FiniteTable.Verification.binary_context_good line 254
  16. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_step line 277
  17. lemma OAI.SourceBurnside.FiniteTable.Verification.wordGood_step line 291
  18. theorem OAI.SourceBurnside.FiniteTable.Verification.wordGood_reach line 305
  19. lemma OAI.SourceBurnside.FiniteTable.Verification.wordGood_idle line 312
  20. theorem OAI.SourceBurnside.FiniteTable.Verification.reach_clean_good line 317
  21. lemma OAI.SourceBurnside.FiniteTable.Connected.mono line 330
  22. def OAI.SourceBurnside.FiniteTable.Own line 336
  23. lemma OAI.SourceBurnside.FiniteTable.BinaryAt.everywhere line 339
  24. def OAI.SourceBurnside.FiniteTable.Committed.value line 351
  25. lemma OAI.SourceBurnside.FiniteTable.Committed.idle line 357
  26. lemma OAI.SourceBurnside.FiniteTable.Committed.owned line 361
  27. lemma OAI.SourceBurnside.FiniteTable.Committed.congr line 372
  28. lemma OAI.SourceBurnside.FiniteTable.Committed.fields line 390
  29. lemma OAI.SourceBurnside.FiniteTable.Committed.same_cuts_fields line 404
  30. lemma OAI.SourceBurnside.FiniteTable.Committed.unary_fields line 415
  31. lemma OAI.SourceBurnside.FiniteTable.Committed.unary_create line 427
  32. def OAI.SourceBurnside.FiniteTable.Committed.UnaryNonPivot line 447
  33. lemma OAI.SourceBurnside.FiniteTable.Committed.unary_nonpivot line 450
  34. lemma OAI.SourceBurnside.FiniteTable.Committed.moving_head line 468
  35. lemma OAI.SourceBurnside.FiniteTable.Committed.binary_acquire line 490
  36. lemma OAI.SourceBurnside.FiniteTable.Committed.binary_fields line 533
  37. theorem OAI.SourceBurnside.FiniteTable.Committed.binary line 548
  38. def OAI.SourceBurnside.FiniteTable.Committed.PivotAt line 594
  39. lemma OAI.SourceBurnside.FiniteTable.Committed.PivotAt.symm line 598
  40. lemma OAI.SourceBurnside.FiniteTable.Committed.PivotAt.unary line 602
  41. lemma OAI.SourceBurnside.FiniteTable.Committed.pivot line 607
  42. lemma OAI.SourceBurnside.FiniteTable.Committed.unary_classified line 638
  43. lemma OAI.SourceBurnside.FiniteTable.Committed.unaryAt_context line 648
  44. lemma OAI.SourceBurnside.FiniteTable.Committed.binaryAt_context line 663
  45. theorem OAI.SourceBurnside.FiniteTable.Committed.step_classified line 682
  46. lemma OAI.SourceBurnside.FiniteTable.Verification.good_success line 707
  47. lemma OAI.SourceBurnside.FiniteTable.Verification.good_semanticZero_sound line 713
  48. lemma OAI.SourceBurnside.FiniteTable.Verification.pivot_certified line 720