# 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
>
>
>

```

• References:
• TCCs
• From: Magesh Narayanan <mnarayan@ececs.uc.edu>