type Bit = int 1;
type Byte = vector 0..7 of Bit;

zeroB = <<0,0,0,0,0,0,0,0>>;
oneB = <<0,0,0,0,0,0,0,1>>;

clearB () = zeroB;

add (0,0,0) = (0,0);
add (0,0,1) = (0,1);
add (0,1,0) = (0,1);
add (0,1,1) = (1,0);
add (1,0,0) = (0,1);
add (1,0,1) = (1,0);
add (1,1,0) = (1,0);
add (1,1,1) = (1,1);

addB <<v7,v6,v5,v4,v3,v2,v1,v0>> <<w7,w6,w5,w4,w3,w2,w1,w0>> =
 case add (v0,w0,0) of
 (c0,s0) ->
 case add (v1,w1,c0) of
 (c1,s1) ->
 case add (v2,w2,c1) of
 (c2,s2) ->
 case add (v3,w3,c2) of
 (c3,s3) ->
 case add (v4,w4,c3) of
 (c4,s4) ->
 case add (v5,w5,c4) of
 (c5,s5) ->
 case add (v6,w6,c5) of
  (c6,s6) ->
 case add (v7,w7,c6) of
  (c7,s7) ->
   (c7,<<s7,s6,s5,s4,s3,s2,s1,s0>>);

incB <<v7,v6,v5,v4,v3,v2,v1,v0>> =
 case addB <<v7,v6,v5,v4,v3,v2,v1,v0>> oneB of
  (_,i) -> i;

subB b1 b2 = addB b1 (incB (compB b2));

decB <<v7,v6,v5,v4,v3,v2,v1,v0>> =
 case subB <<v7,v6,v5,v4,v3,v2,v1,v0>> oneB of
 (_,d) -> d;

and (0,0) = 0;
and (0,1) = 0;
and (1,0) = 0;
and (1,1) = 1;

andB <<v7,v6,v5,v4,v3,v2,v1,v0>> <<w7,w6,w5,w4,w3,w2,w1,w0>> =
 <<and (v7,w7),and (v6,w6),and (v5,w5),and (v4,w4),
   and (v3,w3),and (v2,w2),and (v1,w1),and (v0,w0)>>;

ior (0,0) = 0;
ior (0,1) = 1;
ior (1,0) = 1;
ior (1,1) = 1;

iorB <<v7,v6,v5,v4,v3,v2,v1,v0>> <<w7,w6,w5,w4,w3,w2,w1,w0>> =
 <<ior (v7,w7),ior (v6,w6),ior (v5,w5),ior (v4,w4),
   ior (v3,w3),ior (v2,w2),ior (v1,w1),ior (v0,w0)>>;

xor (0,0) = 0;
xor (0,1) = 1;
xor (1,0) = 1;
xor (1,1) = 0;

xorB <<v7,v6,v5,v4,v3,v2,v1,v0>> <<w7,w6,w5,w4,w3,w2,w1,w0>> =
 <<xor (v7,w7),xor (v6,w6),xor (v5,w5),xor (v4,w4),
   xor (v3,w3),xor (v2,w2),xor (v1,w1),xor (v0,w0)>>;

neg 0 = 1;
neg 1 = 0;

compB <<v7,v6,v5,v4,v3,v2,v1,v0>> =
 <<neg v7,neg v6,neg v5,neg v4,neg v3,neg v2,neg v1,neg v0>>;

expression incB zeroB;
expression decB zeroB;
expression addB oneB (decB zeroB);
expression compB zeroB;
expression xorB oneB oneB;
expression iorB oneB oneB;
expression andB oneB oneB;