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

TCCs



Sorry for the previous mail.
The theory is
ud_list_theory [T : TYPE+ ] : THEORY

BEGIN
	ud_list : TYPE+
        l: VAR ud_list 
        e, x : VAR T

	null : ud_list
	cons?(l) : bool = l /= null
	
	cons : [T, ud_list -> (cons?)]
	car  : [(cons?) -> T]
	cdr  : [(cons?) -> ud_list ]
	
	car_cons : axiom car(cons(e, l)) = e
	cdr_cons : axiom cdr(cons(e, l)) = l
	
	car_cdr_cons : theorem car(cdr(cons(x,cons(e,l))))= e
END ud_list_theory
and the tccs are 
% Existence TCC generated (line 11) for  cons: [T, ud_list -> (cons?)]
    % 
% May need to add an assuming clause to prove this.
  % unfinished
cons_TCC1: OBLIGATION (EXISTS (x: [[T, ud_list] -> (cons?)]): TRUE);

% Subtype TCC generated (line 18) for  cdr(cons(x, cons(e, l)))
  % unfinished
car_cdr_cons_TCC1: OBLIGATION
      (FORALL (e: T, l: ud_list, x: T): cons?(cdr(cons(x, cons(e, l)))));

How do I discharge them or prove them.
Thanks.
Magesh



> Hi,
> 	When I type check the following theory, 
> ud_list_theory [T : TYPE+ ] : THEORY
> 
> BEGIN
> 	ud_list : TYPE+
>         l: VAR ud_list 
>         e, x : VAR T
> 
> 	null : ud_list
> 	cons?(l) : bool = l /= null
> 	
> 	cons : [T, ud_list -> (cons?)]
> 	car  : [(cons?) -> T]
> 	cdr  : [(cons?) -> ud_list ]
> 	
> 	car_cons : axiom car(cons(e, l)) = e
> 	cdr_cons : axiom cdr(cons(e, l)) = l
> 	
> 	car_cdr_cons : theorem car(cdr(cons(x,cons(e,l))))= e
> END ud_list_theory
> 
> I get the following tccs eventhough I have put TYPE+.
> How to discharge or prove these tccs?
> I would appreciate any help.
> Thanks
> Magesh
> 
> 
>