Re: [isabelle] a question of formalization of parameterized-word (bit-vector)


> How to formalize such a lemma? Or I can be shown some examples which
> formalize the  parameterized-word problems.

We did something quite similar:

But once you have an assumption, in your case "len_of TYPE('k) >= 3",
proofs get really hard because Word_Lib cannot help you much. Those
restrictions about a minimum length for a word probably only come from
hard-coded constants, maybe you can rephrase the complicated lemma without
the use of hard-coded constants?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.