exp : type.
typ : type.
of  : exp -> typ -> type.

0 : exp.
1 : exp.
bit : typ.
void : typ.
of1 : of 1 bit.
of0 : of 0 bit.



%% implicit version
translate-i : of M A -> of M' A -> type.
%mode translate-i +D -D'.

%% explicit version
translate-e : {m : exp}{a : typ} {m' : exp}
              of m a -> of m' a -> type.
%mode translate-e +M +A -M' +D -D'.



% implicit version
translate-i : of M A -> of M' A -> type.
%mode translate-i +D -D'.

translate-i1 : translate-i of1 of0.
translate-i0 : translate-i of0 of1.


% explicit version
translate-e : {m : exp}{a : typ} {m' : exp}
              of m a -> of m' a -> type.
%mode translate-e +M +A -M' +D -D'.

translate-e/i : translate-e M A M' D D' <- translate-i D D'.

%worlds () (translate-i _ _) (translate-e _ _ _ _ _).
%total D (translate-i D _).

%total D (translate-e _ _ _ D _).



% explicit version
translate2-e : {m : exp}{a : typ} {m' : exp}
               of m a -> of m' a -> type.
%mode translate2-e +M +A -M' +D -D'.

translate2-e1 : translate2-e 1 bit 0 of1 of0.
translate2-e1 : translate2-e 0 bit 1 of0 of1.

% implicit version
translate2-i : of M A -> of M' A -> type.
%mode translate2-i +D -D'.

translate2-i/e : translate2-i D D' <- translate2-e _ _ _ D D'.

%worlds () (translate2-i _ _) (translate2-e _ _ _ _ _).

%total D (translate2-e _ _ _ D _).
%total D (translate2-i D _).


translate2-i/e : translate2-i (D : of M A) D' <- translate2-e M A M' D D'.