Hi all, I am studying Isabelle/HOL. I would like to have one question. Can we use Isabelle to formalize "finite paths" of a transition system (or formalize finite run of a finite automaton) ? Please help me if you have a solution on this problem? Thank you in advance, Bests, Tang.