Theory BDD_Examples

theory BDD_Examples
imports Level_Collapse
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