OAI/SetTheory/PartitionPrinciple/Geometry/InitialCompressionAccounting.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Forcing.GroundCompressionState line 12
2. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.inputs_toState line 29
3. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.code_mem line 33
4. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_successor line 41
5. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.successor_unique_data line 58
6. def OAI.PartitionPilot.Forcing.FiniteCompressionAccounting line 70
7. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.accounting_next line 83
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialCompressionInvariant line 141
9. def OAI.PartitionPilot.Forcing.TransitiveGround.initialCompressionData line 220
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialCompressionState line 241
11. def OAI.PartitionPilot.Forcing.TransitiveGround.initialCompressionFieldsFormula line 286
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_initialCompressionFieldsFormula line 302
13. def OAI.PartitionPilot.Forcing.TransitiveGround.initialCompressionDataFormula line 351
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_initialCompressionDataFormula line 358
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.initialCompressionData_accounting line 401