theory Result imports Soundness Completeness begin
theorem prover_soundness_completeness: fixes A B :: ‹fm list› defines‹t ≡ prover (A, B)› shows‹tfinite t ∧ wf t ⟷ (∀(E :: _ ==> tm) F G. sc (E, F, G) (A, B))› using assms prover_soundness prover_completeness unfolding prover_def by fastforce
corollary fixes p :: fm defines‹t ≡ prover ([], [p])› shows‹tfinite t ∧ wf t ⟷ (∀(E :: _ ==> tm) F G. [E, F, G] p)› using assms prover_soundness_completeness by simp
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
Suchen
