# [PVS-Help] Induction by a recursive function?

```
Dear All,
While working with finseq, i came accross a problem. I have a finseq[finseq[T]] and a finseq[T], first I divide finseq[T] and get finseq[finseq[T]] and then try to construct the finseq[T] from it. My theory is as below:

In lemma, i use induction on length of finseq[T] and in induction step, when I need to initialize but this may be another recursive function. How can I do so? Can some help me?

example[T: TYPE] : THEORY
BEGIN
importing seqown
% in finseq own, i ve parent and last, parent returns all the ancestors
% and last returns last seq.
SEQ: TYPE = finseq[T]
t : VAR T
fs:VAR finseq[finseq[T]]
s:VAR SEQ
i,j : VAR nat

extrt(s,i):SEQ=
IF i< s`length THEN
LET len = s`length IN
(#length :=len,
seq := (LAMBDA (n:below[len]) :
seq(s)(n))#)
ELSE
empty_seq
ENDIF

extr(s): finseq[SEQ]=
IF s`length>0 THEN
LET len = s`length IN
(#length := len,
seq := (LAMBDA (i:below[len]):
extrt(s,i))#)
ELSE empty_seq ENDIF

concat(fs):RECURSIVE finseq[T]=
IF length(fs) = 0 THEN empty_seq
ELSE
concat(parent(fs)) o last(fs)
ENDIF
MEASURE length(fs)

concat_Extr:LEMMA
FORALL j: j= length(extr(s)) AND ne_seq?(concat(extr(s)))
IMPLIES s=concat(extr(s))

END example
-----------

{1}   FORALL (j_1: nat):
(FORALL (s: SEQ):
j_1 = length(extr(s)) AND length(s) > 0 IMPLIES
s = concat(extr(s)))
IMPLIES
(FORALL (s: SEQ):
j_1 + 1 = length(extr(s)) AND length(s) > 0 IMPLIES
s = concat(extr(s)))

Rule? (skosimp*)
Repeatedly Skolemizing and flattening,
this simplifies to:
concat_Extr.2 :

{-1}  FORALL (s: SEQ):
j!1 = length(extr(s)) AND length(s) > 0 IMPLIES s = concat(extr(s))
{-2}  j!1 + 1 = length(extr(s!1))
{-3}  length(s!1) > 0
|-------
{1}   s!1 = concat(extr(s!1))

Rule? (expand "concat" +)
Expanding the definition of concat,
this simplifies to:
concat_Extr.2 :

[-1]  FORALL (s: SEQ):
j!1 = length(extr(s)) AND length(s) > 0 IMPLIES s = concat(extr(s))
[-2]  j!1 + 1 = length(extr(s!1))
[-3]  length(s!1) > 0
|-------
{1}   s!1 =
IF length(extr(s!1)) = 0 THEN empty_seq
ELSE concat(parent(extr(s!1))) o last(extr(s!1))
ENDIF

Rule? (lift-if )
Lifting IF-conditions to the top level,
this simplifies to:
concat_Extr.2 :

[-1]  FORALL (s: SEQ):
j!1 = length(extr(s)) AND length(s) > 0 IMPLIES s = concat(extr(s))
[-2]  j!1 + 1 = length(extr(s!1))
[-3]  length(s!1) > 0
|-------
{1}   IF length(extr(s!1)) = 0 THEN s!1 = empty_seq
ELSE s!1 = concat(parent(extr(s!1))) o last(extr(s!1))
ENDIF

Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to:
concat_Extr.2 :

[-1]  FORALL (s: SEQ):
j!1 = length(extr(s)) AND length(s) > 0 IMPLIES s = concat(extr(s))
{-2}  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
|-------
{1}   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))

Rule? (inst - "concat(parent(extr(s!1)))")
Instantiating the top quantifier in - with the terms:
concat(parent(extr(s!1))),
this simplifies to:
concat_Extr.2 :

{-1}  j!1 = length(extr(concat(parent(extr(s!1))))) AND
length(concat(parent(extr(s!1)))) > 0
IMPLIES
concat(parent(extr(s!1))) = concat(extr(concat(parent(extr(s!1)))))
[-2]  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
|-------
[1]   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))

Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to:
concat_Extr.2 :

[-1]  j!1 = length(extr(concat(parent(extr(s!1))))) AND
length(concat(parent(extr(s!1)))) > 0
IMPLIES
concat(parent(extr(s!1))) = concat(extr(concat(parent(extr(s!1)))))
[-2]  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
|-------
[1]   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))

Rule? (prop)
Applying propositional simplification,
this yields  3 subgoals:
concat_Extr.2.1 :

{-1}  concat(parent(extr(s!1))) = concat(extr(concat(parent(extr(s!1)))))
[-2]  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
|-------
[1]   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))

Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to:
concat_Extr.2.1 :

[-1]  concat(parent(extr(s!1))) = concat(extr(concat(parent(extr(s!1)))))
[-2]  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
|-------
[1]   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))

Rule?

Best Regards,

M Ikram

```