Project

General

Profile

Download (1.01 KB) Statistics
| Branch: | Tag: | Revision:
1

    
2
//@ type point = real;
3
//@ type triangle = point[3];
4

    
5
/* axiomatic Stream {
6

    
7
  @ type prout = boolean[3];
8

    
9
  @ type bstream = S(prout, integer);
10

    
11
  @ logic bstream bnot (bstream s) 
12

    
13
  @ logic boolean head (bstream s) = s[0];
14

    
15
  @ logic boolean * tail (boolean * s) = s + 1;
16

    
17
  @ axiom head_obs: \forall boolean b; \forall bstream s; head (tick (b, s)) == b;
18

    
19
  @ axiom tail_obs: \forall boolean b; \forall bstream s; tail (tick (b, s)) == s;
20

    
21
  @ axiom tick_obs: \forall bstream s; s == tick (head (s), tail(s));
22

    
23
  @ logic bstream bnot (bstream b);
24

    
25
  @ axiom bnot_def: \forall boolean b; \forall bstream s;
26
                    bnot (tick (b, s)) == tick ((b)?(\false):(\true), bnot (s));
27

    
28
  @ logic boolean nth (integer i, bstream s) =
29
      (i==0)?(head(s)):(nth(i-1, tail(s)));
30

    
31
  @ predicate eq (bstream s1, bstream s2) = \forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2);
32

    
33
  @ axiom eq_obs: \forall bstream s1; \forall bstream s2; eq (s1, s2) ==> (s1 == s2);
34

    
35
@ lemma prout: \forall bstream s; bnot (bnot (s)) == s;
36
}
37

    
38
*/
39

    
(14-14/25)