# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
#    R3 := {[x] -> [y] : (y = x) | (y = 3x)};
# 
# 
#    Rf := {[x] -> [y] : x <= y <= 3x};
# 
# 
#    R3;

{[x] -> [x] } union
 {[x] -> [3x] }

# 
# 
#    Rf;

{[x] -> [y] : x <= y <= 3x}

# 
# 
#    s12 := {[x] : 1 <= x <= 2};
# 
#    s12;

{[x]: 1 <= x <= 2}

# 
# 
#    sd3 := R3(s12);
# 
#    sd3;

{[y]: 1 <= y <= 2} union
 {[y]: Exists ( alpha : y = 3alpha && 3 <= y <= 6)}

# 
# 
#    sc3 := Rf(s12);
# 
#    sc3;

{[y]: 1 <= y <= 6}

# 
# 
#    sc3 intersection sd3;

{[y]: 1 <= y <= 2} union
 {[y]: Exists ( alpha : y = 3alpha && 3 <= y <= 6)}

# 
# 
#    # I think this is faulty
#    sc3 - sd3;

{[y]: 4 <= y <= 5}

# 
# 
#    # This is OK
#    sd3 - sc3;

{[y]  : FALSE }

# 
# 
#    complement sc3;

{[y]: y <= 0} union
 {[y]: 7 <= y}

# 
#    complement sd3;

{[y]: y <= 0} union
 {[y]: 7 <= y} union
 {[y]: 4 <= y <= 5}

# 
# 
#    sc3;

{[y]: 1 <= y <= 6}

# 
# 
#    sc3 intersection (complement sd3);

{[y]: 4 <= y <= 5}

# 
# 
#    # alternative description of sd3;
#    sd3' := {[y] : 1 <= y <= 3 | y = 6};
# 
#    sd3';

{[y]: 1 <= y <= 3} union
 {[6]}

# 
#    sc3 - sd3';

{[y]: 4 <= y <= 5}

# 
# 
#    # sd3 wrt sd3';
# 
#    sd3 - sd3';

{[y]  : FALSE }

# 
# 
#    sd3' - sd3;

{[y]  : FALSE }

#