[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Induction on FSA
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
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?