OAI/SetTheory/PartitionPrinciple/Definability/HistoryFieldFormulas.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.SetFormula.stateFieldFormulaline 12 - def
OAI.PartitionPilot.Forcing.SetFormula.historyFieldValueFormulaline 17 - def
OAI.PartitionPilot.Forcing.SetFormula.historyFieldPairFormulaline 21 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_stateFieldFormulaline 31 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_historyFieldValueFormulaline 60 - theorem
OAI.PartitionPilot.Forcing.TransitiveGround.realize_historyFieldPairFormulaline 89