# Re: [PVS-Help] How to avoid/discharge an Existence TCC for my subtype

```Hi Mark,

One simple "solution" is to state MyConstant /= SecondConstant as an axiom
and then use the axiom to prove the TCC1:
test : THEORY
BEGIN
q: TYPE+
r: TYPE+ FROM q
MyConstant, SecondConstant : r
MyAxiom : AXIOM
MyConstant /= SecondConstant
s: TYPE+ = { ra: r | ra /= MyConstant }
firstrs : s
END test

Obviously, using axioms is not a very good idea in general. An alternative
solution may be to declare the types and the constants as parameters of
the theory and to state MyConstant /= SecondConstant as an assumption in
the assuming clause:

test2[q:TYPE+,r:TYPE+ from q, MyConstant,SecondConstant:r] : THEORY
BEGIN
ASSUMING
MyAssumption : ASSUMPTION
MyConstant /= SecondConstant
ENDASSUMING

s: TYPE+ = { ra: r | ra /= MyConstant }

firstrs : s

END test2

In either case, you may introduce inconsitencies. Therefore, it is a good
idea to provide a model of your theory. If you use axioms, you can provide
a model by using theory interpretations:

itest : THEORY
BEGIN
IMPORTING test {{ q := int,
r_pred := LAMBDA(ra:int) : ra >= 0,
MyConstant := 0,
SecondConstant := 1 }}

END itest

If you use assumptions, you could define a theory that instantiate the
types and constants with concrete elements:

itest2 : THEORY
BEGIN
IMPORTING test2[int,nat,0,1]
END itest2

Hope that this helps,
Cesar

Mark Brown said:
> Hello,
>
> I am having trouble discharging or avoiding this existence TCC:
>
> % Existence TCC generated (at line 199, column 2) for firstrs: s
>   % unfinished
> Firstrs_TCC1: OBLIGATION EXISTS (x: s): TRUE;
>
> The TCC is generated when I declare my first constant of type s:
>
> [199]  firstrs: s
>
> I have declared s to be a subtype of a subtype as follows:
>
> q: TYPE+
> r: TYPE+ FROM q
> MyConstant, SecondConstant: r
> s: TYPE = { ra: r | ra /= MyConstant }
>
> Alternatively, I get a slightly different Existence TCC that I don't
> know how to discharge if I declare s as a "TYPE+" as in:
>
> s: TYPE+ = { ra: r | ra /= MyConstant }
>
> Either way, I'd like to create the TYPE s which contains everything in
> TYPE r, except for one member.  Thanks in advance,
>
> Mark

--
Cesar A. Munoz H., Senior Staff Scientist
National Institute of Aerospace
100 Exploration Way
Hampton, VA 23666, USA
Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988

```