var1 $;
defaultwhere1(p) = p <= $;
defaultwhere2(P) = P sub {0,...,$};

# Circuit constructors as functions
pred not(var0 A) = ~A;
pred and(var0 A,var0 B) = A & B;
pred or(var0 A,var0 B) =  A | B;
pred xor(var0 A,var0 B) = or(and(not(A),B),and(A,not(B)));
pred nor(var0 A,var0 B) = not(or(A,B));
pred nand(var0 A,var0 B) = not(and(A,B));

# Circut constructors as relations
pred notrel(var0 A,var0 B) = not(A) <=> B;
pred andrel(var0 A,var0 B,var0 C) = and(A,B) <=> C;
pred orrel(var0 A,var0 B,var0 C) = or(A,B) <=> C;
pred xorrel(var0 A,var0 B,var0 C) = xor(A,B) <=> C;
pred norrel(var0 A,var0 B,var0 C) = nor(A,B) <=> C;
pred nandrel(var0 A,var0 B,var0 C) = nand(A,B) <=> C;

# classical one-bit multiplexer
pred mux1(var0 A,var0 B,var0 C,var0 S) = 
  ex0 W1, W2, W3:  
         andrel(A,S,W1) & notrel(S,W3) &
              andrel(B,W3,W2) & orrel(W1,W2,C) ;

# an n-bit mux is strung together from 1-bit muxes
pred muxn(var2 X, var2 Y, var2 Z, var0 S) = 
    all1 p: mux1(p in X, p in Y, p in Z, S); 

# theorems

var2  X, Y, Z;
assert X sub {0,...,$}; # restrict X to represent a bit-vectorsof length $+1
assert Y sub {0,...,$};
assert Z sub {0,...,$}; 
var0 S;

# Does the n-bit mux do the right thing?
#
((S & X=Z) | (~S & Y=Z)) <=> muxn(X,Y,Z,S);

# Example: MUX(19, 23, 0) = 23?
#
# X = {0,1,4} & Y = {0,1,2,4} & (S <=> false) & muxn(X,Y,Z,S);

# can output values always be calculated? (this might not be the case
# if the circuit was overconstrained)
#
# all2 X, Y: all0 S: ex2 Z: muxn(X,Y,Z,S);

# are these values unique? that is, does muxn denote a function
# of the input values?
#
#   all2 X, Y: all0 S: ex2 Z: 
#      muxn(X,Y,Z,S) &
#      all2 Z' : muxn(X,Y,Z',S) => (Z = Z');