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

[PVS-Help] Help trying to prove a trivial lemma



I have the following PVS code:
=============================================
trival: THEORY
 BEGIN

 Z4: TYPE = {x: nat | x < 4}    % 0, 1, 2, or 3                                                                                                                                                                                            
 AR4: TYPE = [Z4 -> real]       % array of 4 reals                                                                                                                                                                                         

 minIndex(values: AR4): Z4 =
  {x: Z4 | FORALL(y: Z4): values(x) <= values(y)}

 % The smallest value is no larger than any other value                                                                                                                                                                                    
 smallestValueIsSmallest: LEMMA
  FORALL(x: Z4, values: AR4): values(minIndex(values)) <= values(x)

 END trival
=============================================
I want to prove the smallestValueIsSmallest lemma. I've tried (model-check) and (grind), but they don't get me very far.

Thanks,
-Ben