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