OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixDecoding.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.MainPrefixGraphCode line 10
  2. def OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedLinked line 35
  3. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedLinked_code line 39
  4. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedLinked_entry line 44
  5. def OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransitionIndex line 49
  6. def OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransitionCode line 55
  7. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransitionCode_entry line 59
  8. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.exists_decodedTransition line 65
  9. def OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransition line 73
  10. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransition_code line 78
  11. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransition_coverage line 83
  12. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransition_entry line 88
  13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.linked_transition_code line 107
  14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageGraph_valid line 114
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.transitionGraph_valid line 119
  16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.transitionGraph_identity line 132
  17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.transitionGraph_composition line 142
  18. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.graph_code line 168
  19. def OAI.PartitionPilot.Forcing.mainPrefixCode line 183
  20. theorem OAI.PartitionPilot.Forcing.mainPrefixCode_inj line 186
  21. def OAI.PartitionPilot.Forcing.MainPrefixCode line 195
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainPrefixCode_mem line 201
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainPrefixCode_fields_mem line 206
  24. def OAI.PartitionPilot.Forcing.BoundedFormula.mainPrefixTupleFormula line 217
  25. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_mainPrefixTupleFormula line 220
  26. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_mainPrefixTupleFormula line 230
  27. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransition_self line 249
  28. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedTransition_comp line 260
  29. def OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedDiagram line 278
  30. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedDiagram_coverage line 289
  31. def OAI.PartitionPilot.Forcing.MainPrefixExtends line 300
  32. theorem OAI.PartitionPilot.Forcing.mainPrefixExtends_iff line 304
  33. theorem OAI.PartitionPilot.Forcing.MainPrefixExtends.refl line 315
  34. theorem OAI.PartitionPilot.Forcing.MainPrefixExtends.trans line 319
  35. theorem OAI.PartitionPilot.Forcing.MainPrefixExtends.antisymm line 327
  36. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.restriction_eq_of_subset line 335
  37. theorem OAI.PartitionPilot.Forcing.mainPrefixExtends_iff_restrictions line 350
  38. def OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedPrefix line 377
  39. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedPrefix_indices line 398
  40. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedPrefix_stageGraph line 403
  41. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedPrefix_transitionGraph line 408
  42. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphCode.decodedPrefix_code line 415