% decompose the theory into clauses, and insert clauses
% *** Input for insertTheories/3 is EIs(the first argument). 
% with facts of candidateH, you can easily track back to fetch the corresponding whole theory.


% Input is EIs -- the first argument
insertTheories([],Tree,Tree).
insertTheories([EI|EIs],TreeSoFar,Tree):-
	findall(Index,candidateH0(EI,Index,T),Indexes),
	insertOneEI_Ts(Indexes,EI,TreeSoFar,NTreeSoFar),
	insertTheories(EIs,NTreeSoFar,Tree).

% TI here is the index of T within EI; rather than TI that translated into T
insertOneEI_Ts([],EI,Tree,Tree).
insertOneEI_Ts([TI|TIs],EI,TreeSoFar,Tree):-
	candidateH0(EI,TI,T),
	insertClas(T,EI-TI,TreeSoFar,NTreeSoFar,Position),
	insertOneEI_Ts(TIs,EI,NTreeSoFar,Tree).

insertClas([],EI-TI,Tree,Tree,0).
insertClas([ClaI|ClaIs],EI-TI,TreeSoFar,Tree,Position):-
	(rb_lookup(ClaI,EI_List,TreeSoFar)->
		%ClaI is there-> previous example, or the same example
		(append([EI-TIs],PreRecord,EI_List)->
			rb_update(TreeSoFar,ClaI,[EI-[TI-Position|TIs]|PreRecord],NTreeSoFar);
			rb_update(TreeSoFar,ClaI,[EI-[TI-Position]|EI_List],NTreeSoFar)
		);
				
		rb_insert(TreeSoFar,ClaI,[EI-[TI-Position]],NTreeSoFar)
	),	
	insertClas(ClaIs,EI-TI,NTreeSoFar,Tree,PrePosition),
	Position is PrePosition+1.



% what it is in the rest of is also important for .
% even the same EI, but different
% distinguish different TI EI-[T1,T2,T3]