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

integer_pred and mailing list



The following is a TCC that was not automatically discharged.  It seems 
to be saying "prove that the results of these operations is an integer" 
but  I'm not sure what the integer_pred bit means and what I can do with
it.

Also, is it possible to set up a text archive of these emails so that they
can all be downloaded in one fell swoop for offline perusal?

sum_TCC1: OBLIGATION
      (FORALL (a: int, b: int, uId: [int, int]):
         a = PROJ_1(uId) AND b = PROJ_2(uId)
             IMPLIES
           integer_pred(((((PROJ_1(uId) + PROJ_2(uId)))
                              *
                            (((PROJ_2(uId)
                                   - PROJ_1(uId))
                                  + 1)))
                             / 2)));

arising from:

% testing various ways of typing lambda expressions
lambda_type_test : THEORY
	BEGIN
	
%	double: [int -> int] = 
%	   (LAMBDA (uId: int): (LAMBDA (x1: int): +(( x1, x1
))(int))(uId))

	double: [int -> int] = 
	   (LAMBDA (uId: int): (LAMBDA (x1: int): +(( x1, x1 )):int)(uId))

 sum: [[int,int] -> int] = 	
  (LAMBDA (uId: [int,int]):
     (LAMBDA (a:int,b:int): 
        /(( *(( ( +(( a, b )) ), ( +(( -(( b, a )), 1 )) ) )), 2 )))(uId))

% sum: [[# lab_1:int, lab_2:int #] -> int] = 	
%  (LAMBDA (uId: [# lab_1:int, lab_2:int #]):
%     (LAMBDA ((# lab_1:=a, lab_2:=b #): [# lab_1:int, lab_2:int #]): 
%        div(( *(( ( +(( a, b )) ), ( +(( -(( b, a )), 1 )) ) )), 2
)))(uId))

  sum210 : LEMMA sum(2,10) = 54
  
END lambda_type_test

Ben Kleinman
bkleinman@writeme.com
http://www.dcs.ed.ac.uk/home/bkk