/***************************variable connection (BINDING) ********************************/
% bind to one of the list, no worry whether is ground or not 
binding(Hr,[nt_binding1|Hr],X,[X|_]). % can't have '!', otherwise, won't try the later ones.
binding(HrSoFar,Hr,X,[Y|Rest]):-
	binding([nt_binding2|HrSoFar],Hr,X, Rest).

bodyVarsUpdate(Hr,[nt_bUpdate1|Hr],NewVar,BodyVars,BodyVars):- member(NewVar,BodyVars),!.
bodyVarsUpdate(Hr,[nt_bUpdate2|Hr],NewVar,BodyVars,[NewVar|BodyVars]).



topCla(nt_bUpdate1,[bodyVarsUpdate(NewVar,BodyVars,BodyVars)]). % not to update since it is there
topCla(nt_bUpdate2,[bodyVarsUpdate(NewVar,BodyVars,[NewVar|BodyVars])]).

topCla(nt_binding1,[binding(X,[X|_])]).
topCla(nt_binding2,[binding(X,[Y|Rest]),binding(X,Rest)]).






% just extra control (compared with binding, so the same ID with binding)

% ???? what I was doing? this should be the control of the problem (within) top Theory
nLast_nReBinding([TClause|Hr],[nt_binding1,TClause|Hr],X,[X|Rest]):- 
	notMember(b2-Change-X,Hr),
	write('OK, it is allowed to be attached'),writeq({b2-Change-X,Hr}),nl,
/*
	(notMember(b2-Change-X,Hr)->
		write('OK, it is allowed to be attached'),nl;
		write('NO, can not be attached, it is already there'), writeq({b2-Change-X,Hr}),nl
	),
*/
	Rest\==[]. % at least one element in the Rest
	
nLast_nReBinding(HrSoFar,Hr,X,[Y|Rest]):-
	nLast_nReBinding([nt_binding2|HrSoFar],Hr,X, Rest).

notMember(_,[]).
notMember(b2-_-X,[b2-_-Y|Rest]):-
	X\==Y,
	notMember(b2-_-X,Rest).