Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/ccc6461ab96bb7e7283cf8e5ab8ce704]
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.
bit-flip-unique-alt :
   {B1:bit} {B1':bit} {B2:bit} {B2':bit}
      id-bit B1 B1' -> bit-flip B1 B2 -> bit-flip B1' B2' -> id-bit B2 B2'
         -> type.
%mode +{B1:bit} +{B1':bit} +{B2:bit} +{B2':bit} +{D0:id-bit B1 B1'}
   +{D1:bit-flip B1 B2} +{D2:bit-flip B1' B2'} -{D3:id-bit B2 B2'}
   (bit-flip-unique-alt D0 D1 D2 D3).
- : bit-flip-unique-alt id-bit/refl bit-flip/01 bit-flip/01 id-bit/refl.
- : bit-flip-unique-alt id-bit/refl bit-flip/10 bit-flip/10 id-bit/refl.
%worlds () (bit-flip-unique-alt _ _ _ _).
%total {} (bit-flip-unique-alt _ _ _ _).
[Closing file /home/www/twelfwiki/code/ccc6461ab96bb7e7283cf8e5ab8ce704]
%% OK %%