| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/LibreOffice/external/redland/rasqal/ (LibreOffice Version 25.8.3.2©) Datei vom 5.10.2025 mit Größe 443 B |
|
Impressum BDD_Examples.thy Sprache: Isabelle |
|||||||||||||||
|
section‹Tests and examples› theory BDD_Examples imports Level_Collapse begin text‹Just two simple examples:› lemma "<emp> do { s ← emptyci; (t,s) ← tci s; tautci t s } <λr. ↑(r = True)>t" by sep_auto lemma "<emp> do { s ← emptyci; (a,s) ← litci 0 s; (b,s) ← litci 1 s; (c,s) ← litci 2 s; (t1i,s) ← orci a b s; (t1,s) ← andci t1i c s; (t2i1,s) ← andci a c s; (t2i2,s) ← andci b c s; (t2,s) ← orci t2i1 t2i2 s; eqci t1 t2 } <↑>t" by sep_auto end
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.10Bemerkung: (vorverarbeitet am 2026-09-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-09