### Profile

 1 ```//@ type point = real; ``` ```//@ type triangle = point[3]; ``` ```/* axiomatic Stream { ``` ``` @ type prout = boolean[3]; ``` ``` @ type bstream = S(prout, integer); ``` ``` @ logic bstream bnot (bstream s) ``` ``` @ logic boolean head (bstream s) = s[0]; ``` ``` @ logic boolean * tail (boolean * s) = s + 1; ``` ``` @ 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; ``` ```} ``` ```*/ ```