#####################################
#                                   #
#  Test file for the unify-library  #
#                                   #
#####################################


#
# Tests for: Introduction (?unify)
#
# Examples from the help file:
#
sigma := {x=f(a),y=x,z=h(z)}:
bool := type( sigma , substitution ):
if bool = true then print(okay) else print(bool) fi;
bool := type( sigma , isubstitution ):
if bool = false then print(okay) else print(bool) fi;
delta := compose( sigma , sigma ):
if equivalent(delta,{x=f(a), y=f(a), z=h(h(z))})  then print(okay) else print(delta) fi;
bool := evalb( sigma = delta ):
if bool = false then print(okay) else print(bool) fi;
bool := equivalent( sigma , delta ):
if bool = true then print(okay) else print(bool) fi;
bool := type( sigma , msubstitution ):
if bool = false then print(okay) else print(bool) fi;
bool := type( delta , msubstitution ):
if bool = false then print(okay) else print(bool) fi;
if equivalent(Eunify( f(x,y)=f(a,b) , {x,y} ),{x=a, y=b})  then print(okay) else print(`not equivalent`) fi;
s := f(y,a):
t := f(g(x),x):
mu := Eunify( s=t , {x,y} ):
if equivalent(mu,{x=a, y=g(a)})  then print(okay) else print(mu) fi;
if evalb(subst(mu,s) = subst(mu,t)) then print(okay) else print(`not identical`) fi;
theta := mu union { z=h(y) }:
bool := generalization( mu , theta ):
if bool = true then print(okay) else print(bool) fi;
theta := idempotent( theta ):
if equivalent(theta,{x=a, y=g(a), z=h(g(a))}) then print(okay) else print(theta) fi;
r := rank( theta , {x,y,z} ):
if r = 3 then print(okay) else print(r) fi;
sigma := theta union { y=g(x) }:
r := rank( sigma , {x,y,z} ):
if r = 3 then print(okay) else print(r) fi;
red := Eunify( sigma minus redundant( sigma , {x,y,z} ) , {x,y,z} ):
if equivalent(red,{x=a, y=g(a), z=h(g(a))}) then print(okay) else print(red) fi;
mu  := { x=g(y) , z=y }:
phi := { x=g(z) , y=z }:
alpha := inversion(mu,phi):
if equivalent(alpha,{z=y, y=z}) then print(okay) else print(alpha) fi;
mu = compose( phi , alpha ):
if equivalent(mu,{x=g(y) ,z=y }) then print(okay) else print(mu) fi;
phi = compose( mu , inverse(alpha) ):
if equivalent(phi,{x=g(z) ,y=z }) then print(okay) else print(phi) fi;


#
# Tests for: substitution, isubstitution, psubstitution, msubstitution
#
# Examples from the help file:
#
bool := type( x=f(a) , substitution ):
if bool = true then print(okay) else print(bool) fi;
bool := type( x=x , substitution ):
if bool = false then print(okay) else print(bool) fi;
bool := type( {x=f(a),x=z} , substitution ):
if bool = false then print(okay) else print(bool) fi;
bool := type( {x=f(a),y=x,z=h(z)} , substitution ):
if bool = true then print(okay) else print(bool) fi;
bool := type( {x=f(a),y=x,z=h(z)} , isubstitution ):
if bool = false then print(okay) else print(bool) fi;
bool := type( {x=f(y),y=x} , psubstitution ):
if bool = false then print(okay) else print(bool) fi;
bool := type( {x=a,y=x,z=x} , msubstitution ):
if bool = true then print(okay) else print(bool) fi;
bool := type( x=f(x) , msubstitution ):
if bool = false then print(okay) else print(bool) fi;
#
# Additional tests:
#
bool := type( {x=y,y=z,z=x,u=v,v=u} , psubstitution ):
if bool = true then print(okay) else print(bool) fi;
bool := type( {v=f(a),x=v,y=f(v)} , msubstitution ):
if bool = true then print(okay) else print(bool) fi;


#
# Tests for: subst
#
# Examples from the help file:
#
t := subst( x=f(a) , f(x) ):
if t = f(f(a)) then print(okay) else print(t) fi;
t := subst( {x=y,y=x}, x=a , f(x,y) ):
if t = f(y,a) then print(okay) else print(t) fi;


#
# Tests for: compose
#
# Examples from the help file:
#
sigma := compose( x=f(y) , y=h(a) ):
if equivalent(sigma,{x = f(h(a)), y = h(a)}) then print(okay) else print(sigma) fi;
sigma := compose( x=f(z) , {z=a,y=v} , v=c ):
if equivalent(sigma,{x = f(a), z = a, y = c, v = c}) then print(okay) else print(sigma) fi;
sigma := compose( {x=y,y=x}, {x=y,y=x} ):
if equivalent(sigma,{ }) then print(okay) else print(sigma) fi;
#
# Additional tests:
#
sigma := compose( x=a , x=b ):
if equivalent(sigma,x=a) then print(okay) else print(sigma) fi;
sigma := compose( {u=f(y),x=y,v=f(x)} , y=x ):
if equivalent(sigma,{u=f(x),v=f(x),y=x}) then print(okay) else print(sigma) fi;


#
# Tests for: inverse
#
# Examples from the help file:
#
sigma := {x=y,y=z,z=x,u=v,v=u}:
delta := inverse(sigma):
theta := compose(sigma,delta):
if theta = { } then print(okay) else print(theta) fi;
theta := compose(delta,sigma):
if theta = { } then print(okay) else print(theta) fi;


#
# Tests for: idempotent
#
# Examples from the help file:
#
sigma := idempotent( {x=f(y),y=g(z),z=a} ):
if equivalent(sigma,{x = f(g(a)), y = g(a), z = a}) then print(okay) else print(sigma) fi;
sigma := idempotent( x=a ):
if equivalent(sigma,{x = a}) then print(okay) else print(sigma) fi;
sigma := idempotent( x=f(x) ):
if sigma=NULL then print(okay) else print(sigma) fi;
#
# Additional tests:
#
sigma := idempotent( {x = f(g(a)), y = g(a), z = a} ):
if equivalent(sigma,{x = f(g(a)), y = g(a), z = a}) then print(okay) else print(sigma) fi;
sigma := idempotent( { } ):
if sigma={} then print(okay) else print(sigma) fi;


#
# Tests for: generalization, equivalent
#
# Examples from the help file:
#
bool := equivalent( x=y , y=x ):
if bool = true then print(okay) else print(bool) fi;
bool := equivalent( {x=y,y=a} , {x=a,y=a} ):
if bool = true then print(okay) else print(bool) fi;
bool := generalization( x=y , {x=a,y=a} ):
if bool = true then print(okay) else print(bool) fi;
bool := generalization( {x=a,y=a} , x=y ):
if bool = false then print(okay) else print(bool) fi;
bool := generalization( { } , x=f(x) ):
if bool = true then print(okay) else print(bool) fi;
#
# Additional tests:
#
bool := equivalent( x=f(x) , y=f(y) ):
if bool = true then print(okay) else print(bool) fi;
bool := equivalent( x=a , y=f(y) ):
if bool = false then print(okay) else print(bool) fi;
bool := equivalent( x=f(x) , y=b ):
if bool = false then print(okay) else print(bool) fi;


#
# Tests for: minimal
#
# Examples from the help file:
#
sigma := minimal( {x=y} , {x=a,y=a} ):
if equivalent(sigma,{x = y}) then print(okay) else print(sigma) fi;
sigma := minimal( {x=f(y),y=c} , {x=f(c)} , {z=a} ):
if {sigma} = {{x = f(c)} , {z = a}} then print(okay) else print(sigma) fi;
sigma := minimal( { } , x=a ):
if sigma = { } then print(okay) else print(sigma) fi;
sigma := minimal( x=f(x) ):
if sigma=NULL then print(okay) else print(sigma) fi;
#
# Additional tests:
#
sigma := minimal( {x=f(y),y=a} ):
if equivalent(sigma,{x=f(a),y=a}) then print(okay) else print(sigma) fi;
sigma := minimal( ):
if sigma=NULL then print(okay) else print(sigma) fi;


#
# Tests for: inversion
#
# Examples from the help file:
#
sigma := inversion( {x=y} , {y=x} ):
if equivalent(sigma,{x=y, y=x}) then print(okay) else print(sigma) fi;
mu    := { x=g(y) , z=y }:
theta := { x=g(z) , y=z }:
alpha := inversion(mu,theta):
mu = compose( theta , alpha ):
if equivalent(mu,{x=g(y) ,z=y }) then print(okay) else print(mu) fi;
theta = compose( mu , inverse(alpha) ):
if equivalent(theta,{x=g(z) ,y=z }) then print(okay) else print(theta) fi;
#
# Additional tests:
#
sigma := inversion( {x=f(a),y=b} , {x=f(a),y=b} ):
if sigma={} then print(okay) else print(sigma) fi;


#
# Tests for: Eunify
#
# Examples from the help file:
#
s := f(a,g(x,y)):
t := f(z,g(b,b)):
mu := Eunify( s = t , {x,y,z} ):
if equivalent(mu,{ x=b, y=b, z=a }) then print(okay) else print(mu) fi;
sigma := Eunify( x = f(x) , x ):
if sigma=NULL then print(okay) else print(sigma) fi;
sigma := Eunify( {f(a) = g(a), c=c} , x ):
if sigma=NULL then print(okay) else print(sigma) fi;
sigma := Eunify( f(x) = f(a) , x ):
if equivalent(sigma,x=a) then print(okay) else print(sigma) fi;
sigma := Eunify( f(x) = f(a) , x , 'map' ):
if sigma=NULL then print(okay) else print(sigma) fi;
#
# Additional tests:
#
mu := Eunify( x=a , x ):
if equivalent(mu,x=a) then print(okay) else print(mu) fi;
mu := Eunify( a=x , x ):
if equivalent(mu,x=a) then print(okay) else print(mu) fi;
mu := Eunify( x=y , {x,y} ):
if equivalent(mu,x=y) then print(okay) else print(mu) fi;
mu := Eunify( a=b , { } ):
if mu=NULL then print(okay) else print(mu) fi;
mu := Eunify( f(a)=f(b) , { } ):
if mu=NULL then print(okay) else print(mu) fi;
mu := Eunify( {x=f(y),y=g(z),z=a} , {x,y,z} ):
if equivalent(mu,{x=f(g(a)),y=g(a),z=a}) then print(okay) else print(mu) fi;
mu := Eunify( {x=f(y),y=g(z),z=h(x)} , {x,y,z} ):
if mu=NULL then print(okay) else print(mu) fi;
mu := Eunify( f(x1,x2,x3)=f(y1,y2,y3) , {x1,x2,x3,y1,y2,y3} ):
if equivalent(mu,{x1=y1,x2=y2,x3=y3}) then print(okay) else print(mu) fi;
sigma := Eunify( f(a) = f(x) , x , 'map' ):
if equivalent(sigma,x=a) then print(okay) else print(sigma) fi;
sigma := Eunify( f(y) = f(x) , {x,y} , 'map' ):
if sigma = {x=y} then print(okay) else print(sigma) fi;
sigma := Eunify( f(x) = f(y) , {x,y} , 'map' ):
if sigma = {y=x} then print(okay) else print(sigma) fi;


#
# Tests for: rank
#
# Examples from the help file:
#
r := rank( f(x,y,z)=f(a,b,c) , {x,y,z} ):
if r = 3 then print(okay) else print(r) fi;
r := rank( {f(a)=f(a),c=c} , x ):
if r = 0 then print(okay) else print(r) fi;


#
# Tests for: redundant
#
# Examples from the help file:
#
sigma := redundant( {x=y,y=x,a=a} , {x,y} ):
if nops(sigma)=2 then print(okay) else print(sigma) fi;
sigma := redundant( {x=y,x=a,y=a} , {x,y} ):
if nops(sigma)=1 then print(okay) else print(sigma) fi;
sigma := redundant( {x=a,x=a} , x ):
if nops(sigma)=0 then print(okay) else print(sigma) fi;
#
# Additional tests:
#
sigma := redundant( {x=a,y=b} , {x,y} ):
if nops(sigma)=0 then print(okay) else print(sigma) fi;
sigma := redundant( a=a , { } ):
if nops(sigma)=1 then print(okay) else print(sigma) fi;


##########################
#                        #
#  End of the test file  #
#                        #
##########################