| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/FOL_Seq_Calc3/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 698 B |
|
Quelle Result.thySprache: Isabelle |
|||||||||||||||
|
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
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09