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