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