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

2 questions on pvs - proofstrategies !!

1.) How do i use an induct scheme on finite-sequences: ther is noone
defined, and I donŽt know how to use the Conversion !

2.) During one proof I got the subgoal:

[-1] is_finite?({y:Word| y = w!1 or y = member (d_b!1)})
[1] is_finite?({w:Word| w!1 = w or w = member (d_b!1)})

Which should be trivialy true, but IŽm not able do proof this subgoal !!

Thank you for your help

     Gernot Lepuschitz alias gernot@sbox.tu-graz.ac.at