Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/1520e0be12dde931c6d426040d46dde6]
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.
%mode +{B:bit} -{B':bit} (bit-flip B B').
%worlds () (bit-flip _ _).
%total {} (bit-flip _ _).
can-bit-flip : {B':bit} {B:bit} bit-flip B B' -> type.
%mode -{B':bit} +{D1:bit} -{D2:bit-flip D1 B'} (can-bit-flip D1 D2).
- : can-bit-flip bit/0 bit-flip/01.
- : can-bit-flip bit/1 bit-flip/10.
%worlds () (can-bit-flip _ _).
%total {} (can-bit-flip _ _).
[Closing file /home/www/twelfwiki/code/1520e0be12dde931c6d426040d46dde6]
%% OK %%