# [isabelle] lemma about finitely-branching finite sequences

```Hi,

I have a relation "↝" representing the reductions of a small-step operational semantics. By construction, every configuration can only reduce to finitely-many next configurations.

Given an initial configuration C, I would like to prove that if every execution starting from C gets stuck after a finite number of steps, then there are only finitely-many executions of C0.

I'm having quite a bit of difficulty getting my head round how to prove this. I can do it if I assume that the entire "↝" relation is well-founded, but that's too strong an assumption, since I need it to be possible for *some* executions to diverge, just not those that start from C.

I have a sense that my lemma, if it is indeed true, will have been proven before, perhaps in the context of graph theory, or computability theory.

I'd really appreciate any hints the Isabelle community might have for how I might prove this, or where/whether it has already been proven.

Thanks!
John

ps. In case more precision is appropriate...

I'm defining executions like this:

> definition executions :: "config ⇒ (nat ⇒ config option) set"
> where
>  "executions C ≡ {π.  π 0 = Some C ∧ (∀i.
>  case π i of None ⇒ π (i+1) = None | Some C ⇒
>  if reduce C=[] then π (i+1) = None
>                 else π (i+1) ∈ Some ` set (reduce C))}"

and my lemma is:

> lemma
>  assumes "∀π ∈ executions C. ∃i > 0. finite_seq i π"
>  shows "finite (executions C)"

and I define finite_seq like so:

> fun finite_seq where
>  "finite_seq 0 π = (∀i. π i = None)"
> | "finite_seq (Suc i) π = (π 0 ≠ None ∧ finite_seq i (λi. π (Suc i)))"

```

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