[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Induction on FSA



2013/2/24 Diego Martinoia <diego.martinoia@xxxxxxxxx>:
> Dear all,
>
> Greetings.
>
> I'm quite new to PVS, and I was wondering if anyone could help me:
>
> I am working on a theory that involves simulating finite state
> automaton, and I have to prove a lemma in the form:
>
> s1 = terminal ( s2, lx )
>
> where s1 and s2 are states of the automaton, lx is a list of inputs
> (the labels on the automaton arches) and terminal is a recursive
> function defined as:
>
> terminal(s, lx) =
>
> IF null?(lx) THEN s
> ELSE
> terminal (next (s, car(lx)) , cdr(lx))
>
> where next is the single step function of the automaton, car and cdr
> are the list accessors for the head and the rest of the list.
>
> Unfortunately, I can't figure out which commands allow me to deal with
> this kind of structure. I have tried launching a
>
> induct-and-simplify "lx"
>
> command, as well as similar form involving using the name and
> generalize-skolem-constants commands to have more possible argument
> for the induction rules, but I always fail.
>
> Anyone has any suggestions on the matter?
>
> Thanks,
>
> Diego Martinoia