### Profile

 1 ```/*@ axiomatic Stream { ``` ``` @ type bstream; ``` ``` @ logic bstream tick (boolean b, bstream s); ``` ``` @ logic boolean head (bstream s); ``` ``` @ logic bstream tail (bstream s); ``` ``` @ axiom head_obs: \forall boolean b; \forall bstream s; head (tick (b, s)) == b; ``` ``` @ axiom tail_obs: \forall boolean b; \forall bstream s; tail (tick (b, s)) == s; ``` ``` @ axiom tick_obs: \forall bstream s; s == tick (head (s), tail(s)); ``` ``` @ logic bstream bnot (bstream b); ``` ``` @ axiom bnot_def: \forall boolean b; \forall bstream s; ``` ``` bnot (tick (b, s)) == tick ((b)?(\false):(\true), bnot (s)); ``` ``` @ logic boolean nth (integer i, bstream s) = ``` ``` (i==0)?(head(s)):(nth(i-1, tail(s))); ``` ``` @ predicate eq (bstream s1, bstream s2) = \forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2); ``` ``` @ axiom eq_obs: \forall bstream s1; \forall bstream s2; eq (s1, s2) ==> (s1 == s2); ``` ```@ lemma prout: \forall bstream s; bnot (bnot (s)) == s; ``` ```} ``` ```*/ ```