# [PVS-Help] Problem with completeness check of COND

```COND  FALSE -> FALSE ENDCOND should, presumably, be caught by the type checker as being incomplete. In  C_MD_ft_correct, below, that is what happens.

However, in  C_MD_ft_bad, all the type correctness proofs pass. This is presumably a bug?

Thanks,

Jonathan

===

foo_bar : THEORY

BEGIN

range_switch:  TYPE = {on, off}
range_mode:    TYPE = {md_off, init, normal, failed}

M_SW: VAR[nat -> range_switch]
C_MD: VAR[nat -> range_mode]

COND
i = 0 -> C_MD(0) = md_off,
i > 0 ->
COND
M_SW(i) = on -> C_MD(i) = md_off,
M_SW(i) = off ->
COND  FALSE -> FALSE ENDCOND
ENDCOND
ENDCOND

C_MD_ft_correct(M_SW, C_MD)(i:nat): bool =
COND
i = 0 -> C_MD(0) = md_off,
i > 0 ->
COND
M_SW(i) = off ->
COND  FALSE -> FALSE ENDCOND,
M_SW(i) = on -> C_MD(i) = md_off
ENDCOND
ENDCOND

% Proof summary for theory foo_bar
%    C_MD_ft_bad_TCC1......................proved - complete   [shostak](0.01 s)
%    C_MD_ft_bad_TCC2......................proved - complete   [shostak](0.01 s)
%    C_MD_ft_bad_TCC3......................proved - complete   [shostak](0.01 s)
%    C_MD_ft_bad_TCC4......................proved - complete   [shostak](0.00 s)
%    C_MD_ft_correct_TCC1..................unfinished          [shostak](0.02 s)
%    Theory totals: 5 formulas, 5 attempted, 4 succeeded (0.06 s)

END foo_bar

```