bin : type. 

e : bin. 
1 : bin -> bin. 
0 : bin -> bin.

bin-eq : bin -> bin -> type.
bin-eq/ : bin-eq N N.

% note: not defined unless the numbers are the same length
and : bin -> bin -> bin -> type.
%mode and +N1 +N2 -N3.

and/e : and e e e.
and/00 : and (0 M) (0 N) (0 P) <- and M N P.
and/01 : and (0 M) (1 N) (0 P) <- and M N P.
and/10 : and (1 M) (0 N) (0 P) <- and M N P.
and/11 : and (1 M) (1 N) (1 P) <- and M N P.

%{
The respects lemma: the and relation respects equality
}%

and-resp : bin-eq M M' -> bin-eq N N' -> bin-eq O O' -> and M N O -> and M' N' O' -> type.
%mode and-resp +EQM +EQN +EQO +A -A'.

- : and-resp bin-eq/ bin-eq/ bin-eq/ A A.

%worlds () (and-resp _ _ _ _ _).
%total {} (and-resp _ _ _ _ _).

and-first-resp : bin-eq M M' -> and M N O -> and M' N O -> type.
%mode and-first-resp +EQ +A -A'.

- : and-first-resp EQ A A' <- and-resp EQ bin-eq/ bin-eq/ A A'.
%worlds () (and-first-resp _ _ _).
%total D (and-first-resp D _ _).

1-compat : bin-eq M M' -> bin-eq (1 M) (1 M') -> type.
%mode 1-compat +EQ -EQ'.
- : 1-compat bin-eq/ bin-eq/.

0-compat : bin-eq M M' -> bin-eq (0 M) (0 M') -> type.
%mode 0-compat +EQ -EQ'.
- : 0-compat bin-eq/ bin-eq/.

%worlds () (1-compat _ _) (0-compat _ _).
%total (D E) (1-compat D _) (0-compat E _).

not : bin -> bin -> type.
%mode not +B -B'.
not/e : not e e.
not/1 : not (1 B) (0 B') <- not B B'.
not/0 : not (0 B) (1 B') <- not B B'.

notnot : not A B -> not B C -> bin-eq A C -> type.
%mode notnot +N +N' -EQ.

notnot/e : notnot not/e not/e bin-eq/.
notnot/1 : notnot (not/1 N1) (not/0 N2) EQ'
        <- notnot N1 N2 (EQ : bin-eq A' C')
        <- 1-compat EQ (EQ' : bin-eq (1 A') (1 C')).
notnot/0 : notnot (not/0 N1) (not/1 N2) EQ'
        <- notnot N1 N2 (EQ : bin-eq A' C')
        <- 0-compat EQ (EQ' : bin-eq (0 A') (0 C')).

%worlds () (notnot _ _ _).
%total D (notnot D _ _).

f-compat : {EQ  : bin-eq M M'}
           {F   : bin -> bin} 
           {EQ' : bin-eq (F M) (F M')}
           type.
%mode f-compat +EQ +F -EQ'.
- : f-compat bin-eq/ _ bin-eq/.
%worlds () (f-compat _ _ _).
%total D (f-compat D _ _).

notnot : not A B -> not B C -> bin-eq A C -> type.
%mode notnot +N +N' -EQ.

notnot/e : notnot not/e not/e bin-eq/.
notnot/1 : notnot (not/1 N1) (not/0 N2) EQ'
        <- notnot N1 N2 EQ
        <- f-compat EQ 1 EQ'.
notnot/0 : notnot (not/0 N1) (not/1 N2) EQ'
        <- notnot N1 N2 EQ
        <- f-compat EQ 0 EQ'.

%worlds () (notnot _ _ _).
%total D (notnot D _ _).