equal
deleted
inserted
replaced
6 The main correctness proof: Impl implements Spec |
6 The main correctness proof: Impl implements Spec |
7 *) |
7 *) |
8 |
8 |
9 Correctness = Solve + Impl + Spec + |
9 Correctness = Solve + Impl + Spec + |
10 |
10 |
11 consts |
11 constdefs |
12 |
12 |
13 hom :: 'm impl_state => 'm list |
13 hom :: 'm impl_state => 'm list |
14 |
14 "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) |
15 defs |
15 else ttl(sq(sen s)))" |
16 |
|
17 hom_def |
|
18 "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) |
|
19 else ttl(sq(sen s)))" |
|
20 |
16 |
21 end |
17 end |