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

[PVS-Help] Induction on FSA

Dear all,


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
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?


Diego Martinoia