Correctness = Solve + Impl + Spec + "Lemmas" + consts hom :: "'m impl_state => 'm list" rules hom_def "hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), \ \ sq(sen(s)), \ \ ttl(sq(sen(s))))" end