Theory Result

section ‹Result›

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

end