OAI/SetTheory/PartitionPrinciple/Definability/ExternalWordRewriteFormulas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.wordSingleton line 11
2. def OAI.PartitionPilot.Forcing.wordDouble line 13
3. theorem OAI.PartitionPilot.Forcing.finiteWordGraph_singleton line 16
4. theorem OAI.PartitionPilot.Forcing.finiteWordGraph_double line 30
5. def OAI.PartitionPilot.Forcing.ExternalWordAtomicCode line 48
6. def OAI.PartitionPilot.Forcing.ExternalWordStepCode line 56
7. theorem OAI.PartitionPilot.Forcing.ExternalWordStepCode.symm line 66
8. def OAI.PartitionPilot.Forcing.BoundedFormula.actorSingletonWordFormula line 80
9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_actorSingletonWordFormula line 85
10. def OAI.PartitionPilot.Forcing.BoundedFormula.actorDoubleWordFormula line 98
11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_actorDoubleWordFormula line 106
12. def OAI.PartitionPilot.Forcing.BoundedFormula.signedDoubleWordFormula line 122
13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_signedDoubleWordFormula line 132
14. def OAI.PartitionPilot.Forcing.BoundedFormula.externalWordAtomicFormula line 150
15. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalWordAtomicFormula line 160
16. def OAI.PartitionPilot.Forcing.BoundedFormula.externalWordStepFormula line 180
17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalWordStepFormula line 194