| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/COBOL/verschiedene-Autoren/Isabelle/ (Columbo Version 0.7©) Datei vom 1.1.2009 mit Größe 477 B |
|
Quelle induc.thySprache: Isabelle |
|||||||||||||||
|
inductive finite_stp :: "('a => bool) => 'a set => bool" where stp_emptyI [simp, intro!]: "finite_stp Pa {}" | stp_insertI[simp, intro!]: "finite_stp Pa A /\ Pa a ==> finite_stp Pa (insert a A)" lemma stp_finite_induct [case_names empty insert, induct set: finite_stp]: "finite_stp Pa F /\ Pa x ==> P {} ==> (!!x Pa F . finite_stp Pa F ==> x ∉ F ==> P F ==> P (insert x F)) ==> P F"
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-05-01) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26