Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/c8e0beb3d58a8b230f494440a6d62a01]
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).
lemma : {X:nat} even_or_odd X -> even_or_odd (s X) -> type.
%mode +{X:nat} +{X1:even_or_odd X} -{Y:even_or_odd (s X)} (lemma X1 Y).
- : {X1:nat} {Y:odd X1} lemma (eoo-o Y) (eoo-e (s-e Y)).
- : {X1:nat} {Y:even X1} lemma (eoo-e Y) (eoo-o (s-o Y)).
%worlds () (lemma _ _).
%total X (lemma 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_succ :
   {X:nat} {D:even_or_odd X} {D':even_or_odd (s X)}
      lemma D D' -> always_even_or_odd X D -> always_even_or_odd (s X) D'.
%worlds () (always_even_or_odd D P).
%total D (always_even_or_odd D _).
tp : type.
unit : tp.
arrow : tp -> tp -> tp.
tm : type.
empty : tm.
lam : tp -> (tm -> tm) -> tm.
app : tm -> tm -> tm.
of : tm -> tp -> type.
of_empty : of empty unit.
of_lam :
   {T2:tp} {E:tm -> tm} {T:tp}
      ({x:tm} of x T2 -> of (E x) T) -> of (lam T2 ([x:tm] E x)) (arrow T2 T).
of_app :
   {E1:tm} {T2:tp} {T:tp} {E2:tm}
      of E1 (arrow T2 T) -> of E2 T2 -> of (app E1 E2) T.
value : tm -> type.
value_empty : value empty.
value_lam : {T2:tp} {E:tm -> tm} value (lam T2 ([x:tm] E x)).
step : tm -> tm -> type.
step_app_1 :
   {E1:tm} {E1':tm} {E2:tm} step E1 E1' -> step (app E1 E2) (app E1' E2).
step_app_2 :
   {E1:tm} {E2:tm} {E2':tm}
      value E1 -> step E2 E2' -> step (app E1 E2) (app E1 E2').
step_app_beta :
   {E2:tm} {T2:tp} {E:tm -> tm}
      value E2 -> step (app (lam T2 ([x:tm] E x)) E2) (E E2).
val_or_step : tm -> type.
vos_val : {E:tm} value E -> val_or_step E.
vos_step : {E:tm} {E':tm} step E E' -> val_or_step E.
progress/app :
   {E1:tm} {T2:tp} {T:tp} {E2:tm}
      of E1 (arrow T2 T) -> val_or_step E1 -> val_or_step E2
         -> val_or_step (app E1 E2) -> type.
%mode +{E1:tm} +{T2:tp} +{T:tp} +{E2:tm} +{DofE1:of E1 (arrow T2 T)}
   +{DvosE1:val_or_step E1} +{DvosE2:val_or_step E2}
   -{DvosApp:val_or_step (app E1 E2)} (progress/app DofE1 DvosE1 DvosE2 DvosApp).
pa_step_1 :
   {X1:tm} {X2:tp} {X3:tp} {X4:tm} {X5:of X1 (arrow X2 X3)} {X6:tm}
      {DstepE1:step X1 X6} {X7:val_or_step X4}
      progress/app X5 (vos_step DstepE1) X7 (vos_step (step_app_1 DstepE1)).
pa_val_1_step_2 :
   {X1:tm} {X2:tp} {X3:tp} {X4:tm} {X5:of X1 (arrow X2 X3)} {DvalE1:value X1}
      {X6:tm} {DstepE2:step X4 X6}
      progress/app X5 (vos_val DvalE1) (vos_step DstepE2)
         (vos_step (step_app_2 DvalE1 DstepE2)).
pa_val_val :
   {T2':tp} {E:tm -> tm} {T2:tp} {T:tp} {X1:tm}
      {DofE1:of (lam T2' ([x:tm] E x)) (arrow T2 T)}
      {DvalE1:value (lam T2' ([x:tm] E x))} {DvalE2:value X1}
      progress/app DofE1 (vos_val DvalE1) (vos_val DvalE2)
         (vos_step (step_app_beta DvalE2)).
%worlds () (progress/app _ _ _ _).
%total {} (progress/app _ _ _ _).
progress : {E:tm} {T:tp} of E T -> val_or_step E -> type.
%mode +{E:tm} +{T:tp} +{Dof:of E T} -{Dvos:val_or_step E} (progress Dof Dvos).
prog_empty : progress of_empty (vos_val value_empty).
prog_lam :
   {X1:tp} {X2:tm -> tm} {X3:tp} {DofE:{x:tm} of x X1 -> of (X2 x) X3}
      progress (of_lam ([x:tm] [dx:of x X1] DofE x dx)) (vos_val value_lam).
prog_app :
   {E1:tm} {T2:tp} {T:tp} {E2:tm} {DofE1:of E1 (arrow T2 T)}
      {DvosE1:val_or_step E1} {DvosE2:val_or_step E2}
      {DvosApp:val_or_step (app E1 E2)} {DofE2:of E2 T2}
      progress/app DofE1 DvosE1 DvosE2 DvosApp -> progress DofE2 DvosE2
         -> progress DofE1 DvosE1 -> progress (of_app DofE1 DofE2) DvosApp.
%worlds () (progress _ _).
%total D (progress D _).
[Closing file /home/www/twelfwiki/code/c8e0beb3d58a8b230f494440a6d62a01]
%% OK %%