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