Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/0b0e2db0c83e9fe5854e2c27af2b8aee]
nat : type.
z : nat.
s : nat -> nat.
odd : nat -> type.
even : nat -> type.
z-e : even z.
s-o : {X:nat} even X -> odd (s X).
s-e : {X:nat} odd X -> even (s X).
even_or_odd : nat -> type.
eoo-e : {X:nat} even X -> even_or_odd X.
eoo-o : {X:nat} odd X -> even_or_odd X.
always_even_or_odd : {N:nat} even_or_odd N -> type.
%mode +{D:nat} -{P:even_or_odd D} (always_even_or_odd D P).
aeo_zero : always_even_or_odd z (eoo-e z-e).
aeo_even :
   {X:nat} {Y:odd X}
      always_even_or_odd X (eoo-o Y) -> always_even_or_odd (s X) (eoo-e (s-e Y)).
aeo_odd :
   {X:nat} {Y:even X}
      always_even_or_odd X (eoo-e Y) -> always_even_or_odd (s X) (eoo-o (s-o Y)).
%worlds () (always_even_or_odd D P).
[Closing file /home/www/twelfwiki/code/0b0e2db0c83e9fe5854e2c27af2b8aee]
/home/www/twelfwiki/code/0b0e2db0c83e9fe5854e2c27af2b8aee:24.9-24.38 Error: 
Totality: Output of subgoal not covered
Output coverage error --- missing cases:
{X1:nat} {X2:even X1} |- always_even_or_odd X1 (eoo-e X2).

%% ABORT %%