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

Re: 2 questions on pvs - proofstrategies !!



gernot (gernot@sbox.tu-graz.ac.at) writes:
> 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)})

I prove things like this using

  (CASE-REPLACE "{y:Word| y = w!1 or y = member (d_b!1)} =
                 {w:Word| w!1 = w or w = member (d_b!1)}")

One case is completed with (ASSERT) and (APPLY-EXTENSIONALITY 1)
(GROUND) gets the other.

Rick