 243        ∃ (O : PrimitiveObserver ℰ) (e₁ e₂ : ℰ),
 244          e₁ ≠ e₂ ∧ Separates O e₁ e₂
 245
 246def recognizerInducesLogicCert : RecognizerInducesLogicCert where
 247  identity_auto := fun r w => Recognizer.identity r w
 248  non_contradiction_auto := fun r w => Recognizer.non_contradiction r w
 249  totality_auto := fun r w => Recognizer.totality r w
 250  primitive_observer_auto := fun r h => Recognizer.induces_primitive_observer r h
 251
 252theorem recognizerInducesLogicCert_inhabited :
 253    Nonempty RecognizerInducesLogicCert :=
 254  ⟨recognizerInducesLogicCert⟩
 255
 256end RecognizerInducesLogic
 257end Foundation
 258end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.