equal
deleted
inserted
replaced
|
1 Correctness = Solve + Impl + Spec + "Lemmas" + |
|
2 |
|
3 consts |
|
4 |
|
5 hom :: "'m impl_state => 'm list" |
|
6 |
|
7 |
|
8 rules |
|
9 |
|
10 hom_def |
|
11 "hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), \ |
|
12 \ sq(sen(s)), \ |
|
13 \ ttl(sq(sen(s))))" |
|
14 |
|
15 end |