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 : id-bit B B.

bit-flip-unique : bit-flip B1 B2
               -> bit-flip B1 B2'
               -> id-bit B2 B2'
               -> type.
%mode 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 : id-bit B1 B1'
                 -> id-bit B2 B2'
                 -> bit-flip B1 B2
                 -> bit-flip B1' B2'
                 -> type.
%mode bit-flip-resp +D0 +D1 +D2 -D3.

- : bit-flip-resp id-bit/refl id-bit/refl D D.

%worlds () (bit-flip-resp _ _ _ _).
%total {} (bit-flip-resp _ _ _ _).

bit-flip-unique-alt : id-bit B1 B1' 
                       -> bit-flip B1 B2
                       -> bit-flip B1' B2'
                       -> id-bit B2 B2'
                       -> type.
%mode bit-flip-unique-alt +D0 +D1 +D2 -D3.

- : bit-flip-unique-alt ID1 (BF: bit-flip B1 B2) (BF': bit-flip B1' B2') ID2
     <- bit-flip-resp ID1 id-bit/refl BF (BF'': bit-flip B1' B2)
     <- bit-flip-unique BF'' BF' (ID2: id-bit B2 B2').

%worlds () (bit-flip-unique-alt _ _ _ _).
%total {} (bit-flip-unique-alt _ _ _ _).