[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