$$$PVSTypes.pvs
PVSTypes  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  T:TYPE+%={x:int| x>5 & x<2}

  c:T  % T is a constant of type T

  m:VAR real
  myabs(m):nonneg_real = IF m < 0 THEN -m ELSE m ENDIF

%  abs(m): {n: nonneg_real | n >= m}
%    = IF m < 0 THEN -m ELSE m ENDIF
  sqrt(n:nonneg_real):nonneg_real

 h(m):nonneg_real=sqrt(myabs(m)-m)

 h2(m):nonneg_real=sqrt(abs(m)-m)

% f(i:subrange(0,4)):real

% f(x,y:real):nonneg_real = sqrt(x-y)
 g(x:real, y:{y:real|x>=y}):nonneg_real = sqrt(x-y)

  PwrCond(Prev:bool, Power, Kin, Kout:posreal):bool = TABLE
    %---------------------------------------------------%
    |[Power<=Kout | Power>Kout & Power<Kin | Power>=Kin]|
    %---------------------------------------------------%
    |   FALSE      |        Prev            |   TRUE   ||
    %---------------------------------------------------%
  ENDTABLE

  DisjointnessCounterExample: THEOREM

   EXISTS (Power, Kin, Kout:posreal): Power>0 & Kin>0 & Kout>0 &
        Kin<= Power & Power <= Kout

  PwrCond_TCC1CounterExample: THEOREM
  NOT FORALL (Kin, Kout: posreal, Power:posreal):
    NOT (Power <= Kout AND Power > Kout & Power < Kin) AND
     NOT (Power <= Kout AND Power >= Kin) AND
      NOT ((Power > Kout & Power < Kin) AND Power >= Kin);

    FixedPwrCond(Prev:bool, Power, Kin:posreal, 
          Kout:{x:posreal| x<Kin}):bool = TABLE
    %---------------------------------------------------%
    |[Power<=Kout | Power>Kout & Power<Kin | Power>=Kin]|
    %---------------------------------------------------%
    |   FALSE      |        Prev            |   TRUE   ||
    %---------------------------------------------------%
  ENDTABLE

 %using Fixed powercond with Kin<=Kout generates an unprovable TCC
  myKin,myKout:posreal
  myPower:VAR posreal
  myPrev:VAR bool

  Validation: THEOREM myPower>myKin => FixedPwrCond(myPrev,myPower,myKin,myKout)

  END PVSTypes

$$$PVSTypes.prf
(|PVSTypes| (|myabs_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|myabs_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|h_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|h2_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|g_TCC1| "" (SKOLEM!) (("" (TYPEPRED "y!1") (("" (ASSERT) NIL NIL)) NIL))
  NIL)
 (|PwrCond_TCC1| "" (COND-DISJOINT-TCC))
 (|PwrCond_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (|DisjointnessCounterExample| "" (INST 1 "2" "1" "3") (("" (GRIND) NIL NIL))
  NIL)
 (|PwrCond_TCC1CounterExample| "" (INST -1 "1" "3" "2") (("" (GRIND) NIL NIL))
  NIL)
 (|FixedPwrCond_TCC1| "" (COND-DISJOINT-TCC) NIL NIL)
 (|FixedPwrCond_TCC2| "" (COND-COVERAGE-TCC) NIL NIL)
 (|Validation_TCC1| "" (SUBTYPE-TCC)))