Email Gateway (Jun 29 2022 at 06:56): Email Gateway (Jun 29 2022 at 06:56):From: Valentin Springsklee <uidpn@student.kit.edu>
Hello,
I found the solution already. It turned out, that it is the same as
shoing termination of any function. I was just confused about the syntax
when appliyng the WHILET_rule.
I am fairly new to Isabelle and I should probably have posted this
kind of question on the Zulip chat. Sorry for theinconvenience
Kind regards,
Valentin Springsklee
Last updated: Jul 15 2022 at 23:21 UTC