| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/ROBDD/ Datei vom 31.4.2026 mit Größe 651 B |
|
Quelle BDD_Examples.thySprache: 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
¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet am 2026-06-13) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-12