| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/FOL_Seq_Calc3/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 698 B |
|
Quelle Result.thy Sprache: 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.1 Sekunden (vorverarbeitet am 2026-11-03) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01