[isabelle] The last question- on isabelle/HOL

Dear professionals,
Than you for the kind consideration. It encourages me to try more. I corrected my model by the help of 
your answer. It gets realy like Otway-Rees.
But it is still too slow and can not prove the lemmas. It would be realy kind of you if you do me your last favor and tell me what is the reason and how I can fix it.
I have enclosed the file by this e-mail.
Thank you very much
Shadi Shiri


Attachment: Final Kryptonight.thy
Description: Binary data

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