Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/1190889dd5a456d66a40d15efdbaeffc]
bit : type.
bit/0 : bit.
bit/1 : bit.
bit-flip : bit -> bit -> type.
bit-flip/01 : bit-flip bit/0 bit/1.
bit-flip/10 : bit-flip bit/1 bit/0.
id-bit : bit -> bit -> type.
id-bit/refl : {B:bit} id-bit B B.
tp : type.
unit : tp.
arrow : tp -> tp -> tp.
tm : type.
empty : tm.
lam : tp -> (tm -> tm) -> tm.
app : tm -> tm -> tm.
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).
id : tm -> tm -> type.
refl : {E:tm} id E E.
id_app_cong :
   {E1:tm} {E1':tm} {E2:tm} {E2':tm}
      id E1 E1' -> id E2 E2' -> id (app E1 E2) (app E1' E2') -> type.
%mode +{E1:tm} +{E1':tm} +{E2:tm} +{E2':tm} +{X1:id E1 E1'} +{X2:id E2 E2'}
   -{X3:id (app E1 E2) (app E1' E2')} (id_app_cong X1 X2 X3).
- : {X1:tm} {X2:tm} id_app_cong refl refl refl.
%worlds () (id_app_cong _ _ _).
%total {} (id_app_cong _ _ _).
det : {E:tm} {E':tm} {E'':tm} step E E' -> step E E'' -> id E' E'' -> type.
%mode +{E:tm} +{E':tm} +{E'':tm} +{X1:step E E'} +{X2:step E E''} -{X3:id E' E''}
   (det X1 X2 X3).
det-1 :
   {X1:tm} {X2:tm} {X3:tm} {DidE1:id X1 X2} {DidApp:id (app X1 X3) (app X2 X3)}
      {X4:tm} {DstepE1':step X4 X1} {DstepE1'':step X4 X2}
      id_app_cong DidE1 refl DidApp -> det DstepE1' DstepE1'' DidE1
         -> det (step_app_1 DstepE1') (step_app_1 DstepE1'') DidApp.
det-2 :
   {X1:tm} {X2:tm} {X3:tm} {DidE2:id X2 X3} {DidApp:id (app X1 X2) (app X1 X3)}
      {X4:tm} {DstepE2':step X4 X2} {DstepE2'':step X4 X3} {X5:value X1}
      {X6:value X1}
      id_app_cong refl DidE2 DidApp -> det DstepE2' DstepE2'' DidE2
         -> det (step_app_2 X5 DstepE2') (step_app_2 X6 DstepE2'') DidApp.
det-b :
   {X1:tp} {X2:tm -> tm} {X3:tm} {X4:value X3} {X5:value X3}
      det (step_app_beta X4) (step_app_beta X5) refl.
%worlds () (det _ _ _).
%total D (det D _ _).
[Closing file /home/www/twelfwiki/code/1190889dd5a456d66a40d15efdbaeffc]
%% OK %%