metarule1(property,[P/1,X],([P,X] :- []),Pre,Prog) :-   %***
    Prog=ps(_,sig(Ps,_),_,_), Pre=element(P/1,Ps).
metarule1(instance,[P/A,X,Y],([P,X,Y] :- []),Pre,Prog) :-
	Prog=ps(_,sig(Ps,_),_,_), Pre=element(P/A,Ps).
metarule1(base1,[P/2,Q/1],([P,X,X] :- [[Q,X]]-true),Pre,Prog) :-
	Pre=pred_above(P/2,Q/1,Prog).
metarule1(base,[P/2,Q/Qa|U],([P,X,Y] :- [A-true]),Pre,Prog) :-
	A=[Q,X,Y|U], arity(A,Qa),
	Pre=pred_above(P/2,Q/Qa,Prog).
metarule1(inverse,[P/2,Q/Qa|U],([P,X,Y] :- [A-true]),Pre,Prog) :-
    A=[Q,Y,X|U], arity(A,Qa),
    Pre=pred_above(P/2,Q/Qa,Prog).
metarule1(precon,[P/2,Q/1,R/2],
		([P,X,Y] :- [[Q,X]-true,[R,X,Y]-true]),Pre,Prog) :-
	Pre=(pred_above(P/2,Q/1,Prog), pred_above(P/2,R/2,Prog)).
metarule1(postcon,[P/2,Q/2,R/1],
		([P,X,Y] :- [[Q,X,Y]-true,[R,Y]-true]),Pre,Prog) :-
	Pre=(pred_above(P/2,Q/2,Prog), pred_above(P/2,R/1,Prog)).
metarule1(tailrec,[P/2,Q/Qa|U],
		([P,X,Y] :- [A-Post1, [P,Z,Y]-Post2]),Pre,Prog) :-
	A=[Q,X,Z|U], arity(A,Qa),
	Pre=(pred_above(P/2,Q/Qa,Prog),get_midState(X,Y,Z)),
	obj_gt(ObjGT), obj_gte(ObjGTE),
        Post1 =.. [ObjGT,X,Z,Prog],
        Post2 =.. [ObjGTE,Z,Y,Prog].
metarule1(chain,[P/2,Q/Qa,R/Ra|UV],([P,X,Y] :- [A-Post1,B-Post2]),Pre,Prog) :-
	A=[Q,X,Z|U], B=[R,Z,Y|V],
	arity(A,Qa), arity(B,Ra), append(U,V,UV),
	Pre=(pred_above(P/2,Q/Qa,Prog), pred_above(P/2,R/Ra,Prog),get_midState(X,Y,Z)),
    obj_gt(ObjGT1),obj_gt(ObjGT2),
    Post1 =.. [ObjGT1,X,Z,Prog],
    Post2 =.. [ObjGT2,Z,Y,Prog].

% decomposed
metarule1(unary2,[P/1,Q/1,R/1],([P,X] :- [[Q,X]-true,[R,X]-true]),Pre,Prog) :-
    Pre=(pred_above(P/1,Q/1,Prog), pred_above(P/1,R/1,Prog)).