/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                       DEFINITIONS                      * */
/* *                                                        * */
/* *  $Module:   DEFS                                       * */ 
/* *                                                        * */
/* *  Copyright (C) 1998, 1999, 2000, 2001                  * */
/* *  MPI fuer Informatik                                   * */
/* *                                                        * */
/* *  This program is free software; you can redistribute   * */
/* *  it and/or modify it under the terms of the GNU        * */
/* *  General Public License as published by the Free       * */
/* *  Software Foundation; either version 2 of the License, * */
/* *  or (at your option) any later version.                * */
/* *                                                        * */
/* *  This program is distributed in the hope that it will  * */
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
/* *  License for more details.                             * */
/* *                                                        * */
/* *  You should have received a copy of the GNU General    * */
/* *  Public License along with this program; if not, write * */
/* *  to the Free Software Foundation, Inc., 59 Temple      * */
/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
/* *                                                        * */
/* *                                                        * */
/* $Revision: 21527 $                                        * */
/* $State$                                            * */
/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $                             * */
/* $Author: duraid $                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile$ */

#include "cnf.h"
#include "defs.h"
#include "foldfg.h"

static void def_DeleteFromClauses(DEF);
static void def_DeleteFromTerm(DEF);

DEF def_CreateFromClauses(TERM ExpTerm, TERM PredTerm, LIST Clauses, LIST Lits,
			  BOOL Con)
/**********************************************************
  INPUT:   Two terms, a list of clausenumbers, a list of literal indices and
           a boolean saying whether all clauses derived by expanding the 
	   predicate should be conclauses.
  RETURNS: A definition consisting of the 2 terms as expansion term and
           predicate term and the list of parent clause numbers and a list
	   of the indices of the defined predicate in the parent clauses.
	   ToProve and label are set to NULL.
********************************************************/
{
  DEF  result;

#ifdef CHECK
  if (!term_IsTerm(ExpTerm) || !term_IsTerm(PredTerm)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_CreateFromClause: Illegal input.");
    misc_FinishErrorReport();
  }
  if (list_Empty(Clauses)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_CreateFromClause: No parent clause given.");
    misc_FinishErrorReport();
  }
#endif

  result                   = (DEF) memory_Malloc(sizeof(DEF_NODE));
  result->expansion        = ExpTerm;
  result->predicate        = PredTerm;
  result->toprove          = (TERM) NULL;
  result->parentclauses    = list_PairCreate(Clauses, Lits);
  result->label            = (const char*) NULL;
  result->conjecture       = Con;

  return result;
}

DEF def_CreateFromTerm(TERM ExpTerm, TERM PredTerm, TERM ToProve, const char* Label)
/**********************************************************
  INPUT:   3 terms and a term label.
  RETURNS: A definition consisting of the 3 terms as expansion term,
           predicate term and term to prove before applying the 
	   definition and the label of the parent term.
	   The list of clausenumbers is set to NULL.
********************************************************/
{
  DEF  result;

#ifdef CHECK
  if (!term_IsTerm(ExpTerm) || !term_IsTerm(PredTerm)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_CreateFromTerm: Illegal input.");
    misc_FinishErrorReport();
  }  
  if (Label ==  NULL) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_CreateFromTerm: No parent clause given.");
    misc_FinishErrorReport();
  }
#endif

  result                   = (DEF) memory_Malloc(sizeof(DEF_NODE));
  result->expansion        = ExpTerm;
  result->predicate        = PredTerm;
  result->toprove          = ToProve;
  result->parentclauses    = list_PairCreate(list_Nil(), list_Nil());
  result->label            = Label;
  result->conjecture       = FALSE;

  return result;
}

static void def_DeleteFromClauses(DEF D) 
/**********************************************************
  INPUT:   A definition derived from clauses.
  EFFECT:  The definition is deleted, INCLUDING THE TERMS AND
           THE LIST OF CLAUSE NUMBERS.
********************************************************/  
{
#ifdef CHECK
  if (!term_IsTerm(def_Expansion(D)) || !term_IsTerm(def_Predicate(D))) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_DeleteFormClauses: Illegal input.");
    misc_FinishErrorReport();
  }
#endif

  /* ToProve and Label are NULL */
  term_Delete(def_Expansion(D));
  term_Delete(def_Predicate(D));
  list_Delete(def_ClauseNumberList(D));
  list_Delete(def_ClauseLitsList(D));
  list_PairFree(D->parentclauses);

  memory_Free(D, sizeof(DEF_NODE));
}

static void def_DeleteFromTerm(DEF D) 
/**********************************************************
  INPUT:   A definition derived from a term.
  EFFECT:  The definition is deleted, INCLUDING THE TERMS.
           THE LABEL IS NOT FREED.
********************************************************/  
{
#ifdef CHECK
  if (!term_IsTerm(def_Expansion(D)) || !term_IsTerm(def_Predicate(D))) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_DeleteFromTerm: Illegal input.");
    misc_FinishErrorReport();
  }
#endif

  /* List of clausenumbers is NULL */
  term_Delete(def_Expansion(D));
  term_Delete(def_Predicate(D));
  if (def_ToProve(D) != (TERM) NULL)
    term_Delete(def_ToProve(D));
  list_PairFree(D->parentclauses);
  memory_Free(D, sizeof(DEF_NODE));
}

void def_Delete(DEF D)
/**********************************************************
  INPUT:   A definition derived from a term.
  EFFECT:  The definition is deleted.
  CAUTION: All elements of the definition except of the label are freed.
********************************************************/  
{
  if (!list_Empty(def_ClauseNumberList(D)))
    def_DeleteFromClauses(D);
  else
    def_DeleteFromTerm(D);
}

int def_PredicateOccurrences(TERM Term, SYMBOL P)
/****************************************************
  INPUT:   A term and a predicate symbol.
  RETURNS: The number of occurrences of the predicate symbol in Term
**************************************************/			       
{
  /* Quantifiers */
  if (fol_IsQuantifier(term_TopSymbol(Term)))
    return def_PredicateOccurrences(term_SecondArgument(Term), P);

  /* Junctors and NOT */
  if (fol_IsJunctor(term_TopSymbol(Term)) ||
      symbol_Equal(term_TopSymbol(Term),fol_Not())){
    LIST scan;
    int count;
    count = 0;
    for (scan=term_ArgumentList(Term); !list_Empty(scan); scan=list_Cdr(scan)) {
      count += def_PredicateOccurrences((TERM) list_Car(scan), P);
      /* Only the cases count==1 and count>1 are important */
      if (count > 1)
	return count;
    }
    return count;
  }
  
  if (symbol_Equal(term_TopSymbol(Term), P))
    return 1;
  return 0;
} 

LIST def_ExtractDefsFromTerm(TERM Term, const char* Label) 
/**************************************************************
  INPUT:   A term and its label.
  RETURNS: A list of definitions found in the term.
  NOTE:    The Term is not changed, the definitions contain copies.
***************************************************************/
{
  TERM andterm;
  BOOL found;
  int  pol;
  LIST univars, termlist, defslist, scan;
  
  /* First check if there is a top level and() so that the Term may
     contain several definitions */

  andterm = Term;
  found   = FALSE;
  pol     = 1;
  univars = list_Nil();

  /* Traverse top down universal quantifiers */
  while (!found) {
    if ((symbol_Equal(term_TopSymbol(andterm), fol_All()) && (pol == 1))
	|| (symbol_Equal(term_TopSymbol(andterm), fol_Exist()) && (pol == -1))) {
      univars = list_Nconc(univars, list_Copy(fol_QuantifierVariables(andterm)));
      andterm = term_SecondArgument(andterm);
    }
    else {
      if (symbol_Equal(term_TopSymbol(andterm), fol_Not())) {
	pol = -pol;
	andterm = term_FirstArgument(andterm);
      }
      else
	found = TRUE;
    }
  }

  termlist = list_Nil();
  /* Check if conjunction was found */
  if ((symbol_Equal(term_TopSymbol(andterm), fol_And()) && (pol == 1))
      || (symbol_Equal(term_TopSymbol(andterm), fol_Or()) && (pol == -1))) {
    LIST l;
    /* Flatten nested and/or */
    /* Make copy of relevant subterm */
    andterm = cnf_Flatten(term_Copy(andterm), term_TopSymbol(andterm));
    for (l=term_ArgumentList(andterm); !list_Empty(l); l=list_Cdr(l)) {
      TERM newterm;
      newterm = fol_CreateQuantifierAddFather(fol_All(), term_CopyTermList(univars),
					      list_List(list_Car(l)));
      termlist = list_Cons(newterm, termlist);
    }
    /* Arguments are used in new terms */
    list_Delete(term_ArgumentList(andterm));
    term_Free(andterm);
  }
  else
    termlist = list_List(term_Copy(Term));
  
  list_Delete(univars);

  /* Now we have a list of terms that may contain definitions */
  defslist = list_Nil();
  for (scan=termlist; !list_Empty(scan); scan=list_Cdr(scan)) {
    TERM cand;
    TERM foundpred, toprove;

    /* Candidate from list */
    cand = (TERM) list_Car(scan);
    term_AddFatherLinks(cand);

    if (cnf_ContainsDefinition(cand, &foundpred)) {
      DEF def;
#ifdef CHECK
      if (!fol_CheckFormula(cand)) {
	misc_StartErrorReport();
	misc_ErrorReport("\n In def_ExtractDefsFromTerm: Illegal term cand");
	misc_FinishErrorReport();
      }
#endif
      cand = cnf_DefConvert(cand, foundpred, &toprove);
#ifdef CHECK
      if (!fol_CheckFormula(cand)) {
	misc_StartErrorReport();
	misc_ErrorReport("\n In def_ExtractDefsFromTerm: Illegal term cand");
	misc_FinishErrorReport();
      }
#endif
      def  = def_CreateFromTerm(term_Copy(term_SecondArgument(term_Superterm(foundpred))), 
				term_Copy(foundpred), toprove, Label);

      if (def_PredicateOccurrences(cand, term_TopSymbol(foundpred)) > 1)
	def_RemoveAttribute(def, PREDOCCURONCE);
      else 
	def_AddAttribute(def, PREDOCCURONCE);
      if (symbol_Equal(term_TopSymbol(foundpred), fol_Equality()))
	def_AddAttribute(def, ISEQUALITY);
      else
	def_RemoveAttribute(def, ISEQUALITY);

      defslist = list_Cons(def, defslist);
    }
    term_Delete(cand);
  }
  
  list_Delete(termlist);
  return defslist;
}

void def_ExtractDefsFromClauselist(PROOFSEARCH Search, LIST Clauselist)
/**************************************************************
  INPUT:   A proofsearch object and a list of clauses
  RETURNS: Nothing.
  EFFECT:  The definitions found in the clauselist object are stored in
           the proofsearch object.
  NOTE:    The clause list is not changed.
           The old list of definitions in the proofsearch object is 
	   overwritten.
***************************************************************/
{
  LIST       scan, defslist;
  FLAGSTORE  FlagStore;
  PRECEDENCE Precedence;

  defslist   = list_Nil();
  FlagStore  = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);

  for (scan=Clauselist; !list_Empty(scan); scan=list_Cdr(scan)) {
    CLAUSE Clause;
    NAT index;
    LIST pair;

    Clause = (CLAUSE) list_Car(scan);
    /* Check if clause contains a predicate that may be part of a definition */
    if (clause_ContainsPotPredDef(Clause, FlagStore, Precedence, &index, &pair)) {
      LIST l, compl, compllits;
      BOOL done;

      compl = compllits = list_Nil();
      done = FALSE;
      
      /* Search for complement clauses */
      for (l=Clauselist; !list_Empty(l) && !done; l=list_Cdr(l)) {
	int predindex;
	if (clause_IsPartOfDefinition((CLAUSE) list_Car(l), 
				      clause_GetLiteralTerm(Clause, index), 
				      &predindex, pair)) {
	  compl     = list_Cons(list_Car(l), compl);
	  compllits = list_Cons((POINTER) predindex, compllits);
	  
	  if (list_Empty(list_PairFirst(pair)) &&
	      list_Empty(list_PairSecond(pair)))
	    done = TRUE;
	}
      }
      
      /* All complements found ? */ 
      if (done) {
	LIST l2, clausenumbers, args;
	DEF  def;
	NAT  i;
	TERM defterm, predterm;
	BOOL con;

	clausenumbers = list_Nil();
	con           = clause_GetFlag(Clause, CONCLAUSE);

	for (l2=compl; !list_Empty(l2); l2=list_Cdr(l2)) {
	  clausenumbers = list_Cons((POINTER) clause_Number((CLAUSE) list_Car(l2)), 
				    clausenumbers);	    
	  if (clause_GetFlag((CLAUSE) list_Car(l2), CONCLAUSE))
	    con = TRUE;
	}
	clausenumbers = list_Cons((POINTER) clause_Number(Clause), 
				  clausenumbers);
	compllits = list_Cons((POINTER) index, compllits);

	/* Build definition term */
	predterm = term_Copy(clause_GetLiteralTerm(Clause, index));
	args     = list_Nil();
	for (i = 0; i < clause_Length(Clause); i++) 
	  if (i != index)
	    args = list_Cons(term_Copy(clause_GetLiteralTerm(Clause, i)), args);
	defterm  = term_CreateAddFather(fol_Or(), args);
	/* The expansion is negative here, so it must be inverted */
	defterm  = term_Create(fol_Not(), list_List(defterm));
	defterm  = cnf_NegationNormalFormula(defterm);
	def      = def_CreateFromClauses(defterm, predterm, clausenumbers, compllits, con);
	defslist = list_Cons(def, defslist);
	if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) {
	  fputs("\nNew definition found :", stdout);
	  def_Print(def);
	}
      }
      else {
	list_Delete(compllits);
	list_Delete(list_PairSecond(pair));
	list_Delete(list_PairFirst(pair));
      }
      list_Delete(compl);
      list_PairFree(pair);
    }
  }

  if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) {
    if (!list_Empty(defslist)) {
      fputs("\nFound definitions :\n", stdout);
      for (scan = defslist; !list_Empty(scan); scan = list_Cdr(scan)) {
	def_Print((DEF) list_Car(scan));
	fputs("\n---\n", stdout);
      }
    }
  }

  for (scan=defslist; !list_Empty(scan); scan=list_Cdr(scan))
    symbol_AddProperty(term_TopSymbol(def_Predicate((DEF) list_Car(scan))), ISDEF);
  
  prfs_SetDefinitions(Search, list_Nconc(prfs_Definitions(Search), defslist));
}

TERM def_ApplyDefToTermOnce(DEF Def, TERM Term, FLAGSTORE FlagStore,
			    PRECEDENCE Precedence, BOOL* Complete)
/**************************************************************
  INPUT:   A DEF structure, a term and a boolean that is set
           to TRUE if no occurrences of the defined predicate
	   remain in the term. A flag store and a precedence.
  RETURNS: A term where all occurrences of the definitions
           predicate are expanded if possible.
  NOTE:    The Term is not changed.
***************************************************************/
{
  TERM newtarget, oldtarget, targetpredicate, totoplevel, toprove;
  LIST targettermvars, varsfortoplevel;
  BOOL applicable;

  oldtarget = Term;
  *Complete = TRUE;

  while (TRUE) {
    newtarget = term_Copy(oldtarget);
    term_AddFatherLinks(newtarget);
    targettermvars = varsfortoplevel = list_Nil();

    if (cnf_ContainsPredicate(newtarget, term_TopSymbol(def_Predicate(Def)),
			      &targetpredicate, &totoplevel, &targettermvars, 
			      &varsfortoplevel)) {
      *Complete  = FALSE;
      applicable = FALSE;
      /* Check if definition is not always applicable */
      if (term_Equal(def_ToProve(Def), term_Null())) { 
	applicable = TRUE;
	newtarget = cnf_ApplyDefinitionOnce(def_Predicate(Def), term_Copy(def_Expansion(Def)),
					 newtarget, targetpredicate, FlagStore);
	if (oldtarget != Term)
	  term_Delete(oldtarget);
	oldtarget = newtarget;
      	list_Delete(targettermvars);
	list_Delete(varsfortoplevel); 	
      }
      else {
	toprove = term_Copy(def_ToProve(Def));
	newtarget = cnf_DefTargetConvert(newtarget, totoplevel, toprove,
					 term_ArgumentList(def_Predicate(Def)),
					 term_ArgumentList(targetpredicate),
					 targettermvars, varsfortoplevel,
					 FlagStore, Precedence,
					 &applicable);
	list_Delete(targettermvars);
	list_Delete(varsfortoplevel); 	
	if (applicable) {
	  newtarget = cnf_ApplyDefinitionOnce(def_Predicate(Def), term_Copy(def_Expansion(Def)),
					   newtarget, targetpredicate, FlagStore);
	  if (oldtarget != Term)
	    term_Delete(oldtarget);
	  oldtarget = newtarget;
	}
	else {
	  /* Predicate still exists but cannot be expanded */
	  term_Delete(newtarget);
	  if (oldtarget == Term)
	    return NULL;
	  else {
	    oldtarget = cnf_ObviousSimplifications(oldtarget);
	    return oldtarget;
	  }
	}
      }
    }
    else {
      *Complete = TRUE;
      /* Predicate does no longer exist */
      term_Delete(newtarget);
      /* No expansion possible */
      if (oldtarget == Term)
	return NULL;
      else {
	oldtarget = cnf_ObviousSimplifications(oldtarget);
	return oldtarget;
      }
    }
  }
  return NULL; /* Unreachable */
}
    
TERM def_ApplyDefToTermExhaustive(PROOFSEARCH Search, TERM Term)
/**************************************************************
  INPUT:   A proofsearch object and a term.
  RETURNS: An expanded term.
  NOTE:    All occurences of defined predicates are expanded in the term,
           until no further changes are possible.
  CAUTION: If cyclic definitions exist, this will crash.
***************************************************************/
{
  TERM       oldterm, newterm;
  BOOL       done, complete;
  FLAGSTORE  FlagStore;
  PRECEDENCE Precedence;

  done       = FALSE;
  oldterm    = Term;
  FlagStore  = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);

  while (!done) {
    LIST l;
    done = TRUE;
    /* Apply all definitions to term until no more changes occur */
    for (l=prfs_Definitions(Search); !list_Empty(l); l=list_Cdr(l)) {
      newterm = def_ApplyDefToTermOnce((DEF) list_Car(l), oldterm,
				       FlagStore, Precedence, &complete);
      if (newterm != NULL) {
	if (oldterm != Term)
	  term_Delete(oldterm);
	oldterm = newterm;
	done = FALSE;
      }
    }
  }
  if (oldterm == Term)
    return NULL;
  else
    return oldterm;
}

LIST def_ApplyDefToClauseOnce(DEF Def, CLAUSE Clause,
			      FLAGSTORE FlagStore, PRECEDENCE Precedence)
/**************************************************************
  INPUT:   A DEF structure, a clause, a flag store and a
           precedence.
  RETURNS: A list of new clauses.
  NOTE:    The clause is not changed.
           All occurences of the defined predicate are expanded
	   in the clause and in the derived clauses.
***************************************************************/
{
  LIST result, l;
  
  result = list_List(Clause);

  for (l = result; !list_Empty(l); l = list_Cdr(l)) {
    if (clause_ContainsSymbol((CLAUSE) list_Car(l), 
			      term_TopSymbol(def_Predicate(Def)))) {
      result = list_Nconc(result, 
			  cnf_ApplyDefinitionToClause((CLAUSE) list_Car(l), 
						      def_Predicate(Def),
						      def_Expansion(Def),
						      FlagStore, Precedence));
      /* Remove temporary clause */
      if ((CLAUSE) list_Car(l) != Clause)
	clause_Delete((CLAUSE) list_Car(l));
      list_Rplaca(l, NULL);
    }
  }
  result = list_PointerDeleteElement(result, NULL);

  /* Make sure the original clause is no longer in the list */
  if (!list_Empty(result))
    if (list_First(result) == Clause)
      result = list_Pop(result);
  
  for (l = result; !list_Empty(l); l=list_Cdr(l)) {
    CLAUSE c;
    c = (CLAUSE) list_Car(l);
    if (def_Conjecture(Def))
      clause_SetFlag((CLAUSE) list_Car(l), CONCLAUSE);
    clause_SetFromDefApplication(c);
    clause_SetParentClauses(c, list_Cons((POINTER) clause_Number(Clause), 
					 list_Copy(def_ClauseNumberList(Def))));
    /* Parent literal is not available, as the predicate may occur several 
       times in the target clause */
    clause_SetParentLiterals(c, list_Cons((POINTER) 0, 
					  list_Copy(def_ClauseLitsList(Def))));
  }
  return result;
}

LIST def_ApplyDefToClauseExhaustive(PROOFSEARCH Search, CLAUSE Clause)
/**************************************************************
  INPUT:   A proofsearch object and a clause.
  RETURNS: A list of derived clauses.
  NOTE:    All occurences of defined predicates are expanded in the clause.
           until no further changes are possible.
  CAUTION: If cyclic definitions exist, this will crash.
***************************************************************/
{
  LIST       newclauses, scan, result;
  CLAUSE     orig;
  FLAGSTORE  FlagStore;
  PRECEDENCE Precedence;

  orig       = clause_Copy(Clause);
  newclauses = list_List(orig);
  result     = list_Nil();
  FlagStore  = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);

  while (!list_Empty(newclauses)) {
    /* Check all clauses */
    LIST l, nextlist;

    /* List of clauses derived from newclauses by expanding predicates */
    nextlist = list_Nil();

    for (l=newclauses; !list_Empty(l); l=list_Cdr(l)) {
      LIST clauses;
      CLAUSE c;
      
      c = (CLAUSE) list_Car(l);

      /* Apply all definitions to the clause */

      /* List of clauses derived from one clause in newclauses by */
      /* expanding all possible predicates */
      clauses  = list_Nil();

      for (scan=prfs_Definitions(Search); !list_Empty(scan); scan=list_Cdr(scan))
	clauses = list_Nconc(clauses, def_ApplyDefToClauseOnce((DEF) list_Car(scan), c, FlagStore, Precedence));
      
      /* If expansions were made delete old clause */
      if (!list_Empty(clauses)) {
	/* DOCPROOF ? */
	if (c != Clause) {
	  if (flag_GetFlagValue(FlagStore, flag_DOCPROOF)) {
	    prfs_InsertDocProofClause(Search, c);
	  }
	  else
	    clause_Delete(c);
	}
	nextlist = list_Nconc(nextlist, clauses);
      }
      else {
	/* No more expansions possible for this clause */
	/* If it is not the original clause, add it to the result list */
	if (c != Clause)
	  result = list_Cons(c, result);
      }
    }
    list_Delete(newclauses);
    newclauses = nextlist;
  }
      
  return result;
}
  

void def_Print(DEF D)
/**************************************************************
  INPUT:   A DEF structure.
  RETURNS: None.
  EFFECT:  Prints the definition to stdout. 
***************************************************************/
{
  LIST scan, scan2;
  fputs("\n\nAtom: ", stdout);
  fol_PrettyPrint(def_Predicate(D));
  fputs("\nExpansion: \n", stdout);
  fol_PrettyPrint(def_Expansion(D));
  if (!list_Empty(def_ClauseNumberList(D))) {
    fputs("\nParent clauses: ", stdout);
    for (scan = def_ClauseNumberList(D), scan2 = def_ClauseLitsList(D); 
	 !list_Empty(scan); scan = list_Cdr(scan), scan2 = list_Cdr(scan2)) 
      printf("%d.%d ", (NAT) list_Car(scan), (NAT) list_Car(scan2));
    if (D->conjecture)
      fputs("\nDerived from conjecture clauses.", stdout);
    else
      fputs("\nNot derived from conjecture clauses.", stdout);
  }
  else {
    fputs("\nLabel: ", stdout);
    fputs(def_Label(D), stdout);
    puts("\nGuard:");
    if (def_ToProve(D) != NULL) 
      fol_PrettyPrint(def_ToProve(D));
    else
      fputs("Nothing.", stdout);
  }

  fputs("\nAttributes: ", stdout);
  if (def_HasAttribute(D, ISEQUALITY) || def_HasAttribute(D, PREDOCCURONCE)) {
    if (def_HasAttribute(D, ISEQUALITY))
      fputs(" Equality ", stdout);
    if (def_HasAttribute(D, PREDOCCURONCE))
      fputs(" No Multiple Occurrences ", stdout);
  }
  else {
    fputs(" None ", stdout);
  }    
} 

LIST def_ApplyDefToClauselist(PROOFSEARCH Search, DEF Def, 
			      LIST Clauselist, BOOL Destructive)
/**************************************************************
  INPUT:   A proofsearch object, a DEF structure, a list of unshared clauses
           and a boolean saying whether the parent clause of an expansion
	   should be deleted.
  RETURNS: None.
  EFFECT:  For each occurrence of the defined predicate in a clause in the list,
  a new clause with expanded predicate is added to the list.
***************************************************************/
{
  LIST       l, newclauses, allnew;
  FLAGSTORE  FlagStore;
  PRECEDENCE Precedence;

  allnew     = list_Nil();
  FlagStore  = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);

  for (l = Clauselist; !list_Empty(l); l = list_Cdr(l)) {
    newclauses = def_ApplyDefToClauseOnce(Def, (CLAUSE) list_Car(l),
					  FlagStore, Precedence);
    /* Expansions were possible, delete the original clause */
    if (Destructive && !list_Empty(newclauses)) {
      if (flag_GetFlagValue(FlagStore, flag_DOCPROOF))
	prfs_InsertDocProofClause(Search, (CLAUSE) list_Car(l));
      else
	clause_Delete((CLAUSE) list_Car(l));
      list_Rplaca(l, NULL);
    }
    allnew = list_Nconc(allnew, newclauses);
  }
  if (Destructive)
    Clauselist = list_PointerDeleteElement(Clauselist, NULL);


  if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) {
    if (!list_Empty(allnew)) {
      fputs("\nNew clauses after applying definitions : \n", stdout);
      clause_ListPrint(allnew);
    }
  }

  Clauselist = list_Nconc(Clauselist, allnew);
  return Clauselist;
}

LIST def_ApplyDefToTermlist(DEF Def, LIST Termlist,
			    FLAGSTORE FlagStore, PRECEDENCE Precedence,
			    BOOL* Complete, BOOL Destructive)
/**************************************************************
  INPUT:   A DEF structure and a list of pairs (label, term),
           a flag store, a precedence and a pointer to a
	   boolean.
	   If Destructive is TRUE the father of an expanded
	   term is deleted.
  RETURNS: The changed list of terms.
  EFFECT:  For each occurrence of the defined predicate in a
           term in the list, a new term with expanded predicate
	   is added to the list.
	   If every occurrence of the predicate could be
	   expanded, Complete is set to TRUE.
***************************************************************/
{
  LIST l, newterms;
  
  newterms = list_Nil();

  *Complete = TRUE;
  for (l=Termlist; !list_Empty(l); l=list_Cdr(l)) {
    TERM newterm;
    TERM oldterm;
    BOOL complete;
    oldterm = list_PairSecond(list_Car(l));
    newterm = def_ApplyDefToTermOnce(Def, oldterm, FlagStore,
				     Precedence, &complete);
    if (!complete)
      *Complete = FALSE;
    /* destructive part of function */
    if (newterm != NULL) {
      newterms = list_Cons(list_PairCreate(NULL, newterm),newterms);
      if (Destructive) {
	/* Delete oldterm from Termlist */
	term_Delete(list_PairSecond(list_Car(l)));
	if (list_PairFirst(list_Car(l)) != NULL)
	  string_StringFree(list_PairFirst(list_Car(l)));
	
	list_PairFree(list_Car(l));
	list_Rplaca(l, NULL);
      }
    }
  }
  Termlist = list_PointerDeleteElement(Termlist, NULL);

  if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) {
    if (!list_Empty(newterms)) {
      fputs("\n\nNew terms after applying definitions : \n", stdout);
      for (l=newterms; !list_Empty(l); l=list_Cdr(l)) {
	fputs("\n", stdout);
	fol_PrettyPrint(list_PairSecond(list_Car(l)));
      }
    }
  }
  
  Termlist = list_Nconc(Termlist, newterms);
  return Termlist;
}

void def_ExtractDefsFromTermlist(PROOFSEARCH Search, LIST Axioms, LIST Conj)
/**************************************************************
  INPUT:   A proofsearch object and 2 lists of pairs label/term.
  RETURNS: None.
  EFFECT:  Add all found definitions to the proofsearch object.
           The old list of definitions in the proofsearch object is 
	   overwritten.
***************************************************************/
{ 
  LIST      l, deflist;
  FLAGSTORE FlagStore;

  deflist   = list_Nil();
  FlagStore = prfs_Store(Search);

  for (l=Axioms; !list_Empty(l); l=list_Cdr(l)) {
    fol_NormalizeVars(list_PairSecond(list_Car(l))); /* Is needed for proper variable match ! */
    deflist = list_Nconc(deflist,
			 def_ExtractDefsFromTerm(list_PairSecond(list_Car(l)),
						 list_PairFirst(list_Car(l))));
  }
  for (l=Conj; !list_Empty(l); l=list_Cdr(l)) {
    fol_NormalizeVars(list_PairSecond(list_Car(l))); /* Is needed for proper variable match ! */
    deflist = list_Nconc(deflist,
			 def_ExtractDefsFromTerm(list_PairSecond(list_Car(l)),
						 list_PairFirst(list_Car(l))));
  }
  for (l=deflist; !list_Empty(l); l=list_Cdr(l))
    symbol_AddProperty(term_TopSymbol(def_Predicate(list_Car(l))), ISDEF);

  prfs_SetDefinitions(Search, list_Nconc(prfs_Definitions(Search), deflist));  

  if (flag_GetFlagValue(FlagStore, flag_PAPPLYDEFS)) {
    if (!list_Empty(deflist)) {
      fputs("\nFound definitions :\n", stdout);
      for (l = prfs_Definitions(Search); !list_Empty(l); l = list_Cdr(l)) {
	def_Print(list_Car(l));
	fputs("\n---\n", stdout);
      }
    }
  }
}

LIST def_FlattenWithOneDefinition(PROOFSEARCH Search, DEF Def)
/**************************************************************
  INPUT:   A proofsearch object and one definition.
  RETURNS: The list of new definitions.
  EFFECT:  For every occurrence of the defined predicate among the other
           definitions an expansion is attempted.
	   A new definition is only created if the result of the expansion is 
	   again a definition. 
	   The proofsearch object is not changed.
***************************************************************/
{
  LIST       newdefinitions;
  FLAGSTORE  FlagStore;
  PRECEDENCE Precedence;

  newdefinitions = list_Nil();
  FlagStore      = prfs_Store(Search);
  Precedence     = prfs_Precedence(Search);

  if (def_ToProve(Def) == NULL) {
    LIST definitions, l;

    definitions = prfs_Definitions(Search);

    for (l = definitions; !list_Empty(l); l=list_Cdr(l)) {
      DEF d;

      d = (DEF) list_Car(l);      
      if (d != Def) {
	/* Expansion possible */
	if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) {
	  /* Resulting term is still a definition */
	  if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) {
	    TERM newexpansion;
	    BOOL complete;
	    DEF newdef;
	    newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d),
						  FlagStore, Precedence,
						  &complete);
	    
	    newdef = def_CreateFromTerm(newexpansion,
					term_Copy(def_Predicate(d)), 
					term_Copy(def_ToProve(d)), def_Label(d));
	    newdefinitions = list_Cons(newdef, newdefinitions);
	  }
	}
      }
      
    }
  }
  return newdefinitions;
}


void def_FlattenWithOneDefinitionDestructive(PROOFSEARCH Search, DEF Def)
/**************************************************************
  INPUT:   A proofsearch object and one definition.
  RETURNS: None.
  EFFECT:  If the definition is always applicable, every occurrence of the 
           defined predicate among the other definitions is expanded in place.
	   If the resulting term is no longer a definition, it is deleted from
	   the proofsearch object.
	   Def is deleted.
  CAUTION: This function changes the list entries in the list of definitions 
           in the proofsearch object, so do not call it from a loop over
           all definitions.
***************************************************************/
{
  FLAGSTORE  FlagStore;
  PRECEDENCE Precedence;

  FlagStore  = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);

  if (def_ToProve(Def) == NULL) {
    LIST definitions, l;

    definitions = prfs_Definitions(Search);    
    for (l = definitions; !list_Empty(l); l = list_Cdr(l)) {
      DEF d;

      d = (DEF) list_Car(l);      
      if (d != Def) {
	/* Expansion possible */
	if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) {
	  /* Resulting term is still a definition */
	  if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) {
	    TERM newexpansion;
	    BOOL complete;

	    newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d), FlagStore, Precedence, &complete);
	    term_Delete(def_Expansion(d));
	    def_RplacExp(d, newexpansion);
	  }
	  else {
	    symbol_RemoveProperty(term_TopSymbol(def_Predicate(d)), ISDEF);
	    def_Delete(d);
	    list_Rplaca(l, NULL);
	  }
	}
      }
      else {
	/* Remove given definition */
	list_Rplaca(l, NULL);
      }
    }
    symbol_RemoveProperty(term_TopSymbol(def_Predicate(Def)), ISDEF);
    def_Delete(Def);
    definitions = list_PointerDeleteElement(definitions, NULL);
    prfs_SetDefinitions(Search, definitions);
  }
}

void def_FlattenWithOneDefinitionSemiDestructive(PROOFSEARCH Search, DEF Def)
/**************************************************************
  INPUT:   A proofsearch object and one definition.
  RETURNS: Nothing.
  EFFECT:  If the definition can be applied to another definition
           in the search object, that definition is destructively changed.
	   If the resulting term is no longer a definition, it is deleted to
	   prevent cycles.
	   The applied definition Def is NOT deleted.
  CAUTION: After calling this function some entries of the definitions list
           in the proofsearch object may be NULL.
***************************************************************/
{
  FLAGSTORE  FlagStore;
  PRECEDENCE Precedence;

  FlagStore  = prfs_Store(Search);
  Precedence = prfs_Precedence(Search);
  
  if (def_ToProve(Def) == NULL) {
    LIST definitions, l;

    definitions = prfs_Definitions(Search);    
    for (l = definitions; !list_Empty(l); l=list_Cdr(l)) {
      DEF d;

      d = (DEF) list_Car(l);      
      if (d != Def) {
	/* Expansion possible */
	if (term_ContainsSymbol(def_Expansion(d), term_TopSymbol(def_Predicate(Def)))) {
	  /* Resulting term is still a definition */
	  if (!term_ContainsSymbol(def_Expansion(Def), term_TopSymbol(def_Predicate(d)))) {
	    TERM newexpansion;
	    BOOL complete;

	    newexpansion = def_ApplyDefToTermOnce(Def, def_Expansion(d),
						  FlagStore, Precedence,
						  &complete);
	    term_Delete(def_Expansion(d));
	    def_RplacExp(d, newexpansion);
	  }
	  else {
	    symbol_RemoveProperty(term_TopSymbol(def_Predicate(d)), ISDEF);
	    def_Delete(d);
	    list_Rplaca(l, NULL);
	  }
	}
      }
    }
  }
}

void def_FlattenDefinitionsDestructive(PROOFSEARCH Search)
/**************************************************************
  INPUT:   A proofsearch object.
  RETURNS: None.
  EFFECT:  For every definition that is always applicable try to 
           expand the predicate in other
           definitions if possible.
***************************************************************/
{
  LIST l;

  for (l = prfs_Definitions(Search); !list_Empty(l); l=list_Cdr(l)) {
    DEF d;

    d = (DEF) list_Car(l);
    fol_PrettyPrintDFG(def_Predicate(d));
    if (d != NULL)
      def_FlattenWithOneDefinitionSemiDestructive(Search, d);
  }
  prfs_SetDefinitions(Search, list_PointerDeleteElement(prfs_Definitions(Search), NULL));
}

LIST def_GetTermsForProof(TERM Term, TERM SubTerm, int Polarity)
/**************************************************************
  INPUT:   Two formulas, <Term> and <SubTerm> which must be subformula
           of <Term>,an int which is the polarity of <SubTerm> in its
	   superterm and a list of variables <Variables>.
  RETURN:  A list of formulas that are used to prove the guard of Atom.
  COMMENT: Helpfunction of def_FindProofFor Guard.
  CAUTION: Father links must be set. Free variables may exist in terms of
           return list.
	   Terms are copied.
***************************************************************/
{
  TERM   SuperTerm, AddToList;
  SYMBOL Top;
  LIST   Scan1, NewList;

  term_AddFatherLinks(Term);

#ifdef CHECK
  if (!fol_CheckFormula(Term)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_GetTermsForProof: Illegal input Term.");
    misc_FinishErrorReport();
  } 
#endif

  if (Term == SubTerm)
    return list_Nil();

  SuperTerm = term_Superterm(SubTerm);
  Top       = term_TopSymbol(SuperTerm);
  NewList   = list_Nil();
  AddToList = term_Null();

  if (symbol_Equal(Top, fol_Not()))
    return def_GetTermsForProof(Term, SuperTerm, -1*Polarity);

  if (symbol_Equal(Top, fol_Or()) && Polarity == 1) {
    /* Get and store AddToList */
    for (Scan1 = term_ArgumentList(SuperTerm); !list_Empty(Scan1); Scan1 = list_Cdr(Scan1)) {
      if (!term_HasPointerSubterm(list_Car(Scan1), SubTerm))
	NewList = list_Cons(term_Create(fol_Not(),list_List(term_Copy(list_Car(Scan1)))), NewList);
      /* NewList's elements have the form not(term) */
    }
    if (list_Length(NewList) == 1) {
      AddToList = list_Car(NewList);
      list_Delete(NewList);
    }
    else {
      AddToList = term_Create(fol_And(), NewList);
    }
    return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity));
  }
  if (symbol_Equal(Top, fol_And()) && Polarity == -1) {
    /* Get and store AddToList */
    if (list_Length(term_ArgumentList(SuperTerm)) == 2) {
      if (!term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm)) {
	AddToList = term_Copy(term_FirstArgument(SuperTerm));
      }
      else {
	AddToList = term_Copy(term_SecondArgument(SuperTerm));
      }
    }
    else if (list_Length(term_ArgumentList(SuperTerm)) > 2) {
      for (Scan1 = term_ArgumentList(SuperTerm); !list_Empty(Scan1); Scan1 = list_Cdr(Scan1)) {
	if (!term_HasPointerSubterm(list_Car(Scan1), SubTerm))
	  NewList = list_Cons(term_Copy(list_Car(Scan1)), NewList);
      }
      AddToList = term_Create(fol_And(), NewList);
    }
    else { /* Only one argument */
      AddToList = term_Copy(term_FirstArgument(SuperTerm));
    }
   return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity));
  }
  if (symbol_Equal(Top, fol_Implies())) {
    if (term_HasPointerSubterm(term_SecondArgument(SuperTerm), SubTerm) && Polarity == 1) {
      AddToList = term_Copy(term_FirstArgument(SuperTerm));
      return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity));
    }
    if (term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm) && Polarity == -1) {
      AddToList = term_Copy(term_SecondArgument(SuperTerm));
      AddToList = term_Create(fol_Not(), list_List(AddToList));
      return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, -1*Polarity));
    }
  }
  if (symbol_Equal(Top, fol_Implied())) { /* symmetric to fol_Implies */
    if (term_HasPointerSubterm(term_SecondArgument(SuperTerm), SubTerm) && Polarity == -1) {
      AddToList = term_Copy(term_FirstArgument(SuperTerm));
      AddToList = term_Create(fol_Not(), list_List(AddToList));
      return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, -1*Polarity)); 
    }
    if (term_HasPointerSubterm(term_FirstArgument(SuperTerm), SubTerm) && Polarity == 1) {
      AddToList = term_Copy(term_SecondArgument(SuperTerm));
      return list_Cons(AddToList, def_GetTermsForProof(Term, SuperTerm, Polarity));
    }
  }
  if (fol_IsQuantifier(Top))
    return def_GetTermsForProof(Term, SuperTerm, Polarity);

  /* In all other cases, SubTerm is the top level term in which Atom occurs disjunctively */

  return list_Nil();
}

BOOL def_FindProofForGuard(TERM Term, TERM Atom, TERM Guard, FLAGSTORE FlagStore, PRECEDENCE Precedence)
/**************************************************************************
  INPUT:   A formula Term, an atom Atom, a term Guard a flag store and a 
           precedence.
  RETURNS: True iff a proof can be found for Guard in Term.
***************************************************************************/
{
  BOOL LocallyTrue;
  TERM ToProve, Conjecture;
  LIST ArgList, FreeVars;

  ArgList    = list_Nil();
  FreeVars   = list_Nil();
  ToProve    = term_Null();
  Conjecture = term_Copy(Term);

#ifdef CHECK
  if (!fol_CheckFormula(Term)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_FindProofForGuard: No correct formula term.");
    misc_FinishErrorReport();
  }
  if (!term_HasPointerSubterm(Term, Atom)) {
    misc_StartErrorReport();
    misc_ErrorReport("\n In def_FindProofForGuard: Illegal input.");
    misc_FinishErrorReport();
  }
#endif
  
  ArgList = def_GetTermsForProof(Term, Atom, 1);

  if (!list_Empty(ArgList)) {
    ToProve  = term_Create(fol_And(), ArgList);
    FreeVars = list_Nconc(fol_FreeVariables(ToProve), fol_FreeVariables(Guard));
    FreeVars = term_DeleteDuplicatesFromList(FreeVars);
    term_CopyTermsInList(FreeVars);

    ArgList  = list_List(term_Copy(Guard));
    ArgList  = list_Cons(ToProve, ArgList);
    ToProve  = term_Create(fol_Implies(), ArgList);
    ToProve  = fol_CreateQuantifier(fol_All(), FreeVars, list_List(ToProve));

    /* Now ToProve has the form <forall[]: A implies Guard> */
    /*    puts("\n*ToProve: "); fol_PrettyPrintDFG(ToProve); */

#ifdef CHECK
    if (!fol_CheckFormula(ToProve)) {
      misc_StartErrorReport();
      misc_ErrorReport("\n In def_FindProofForGuard: No correct formula ToProve.");
      misc_FinishErrorReport();
    }
#endif

    LocallyTrue = cnf_HaveProof(list_Nil(), ToProve, FlagStore, Precedence);
    term_Delete(ToProve);
    term_Delete(Conjecture);
    if (LocallyTrue)
      return TRUE;
  }
  else {    /* empty list */
    term_DeleteTermList(ArgList);
    term_Delete(Conjecture);
  }

  return FALSE;
}

LIST def_ApplyDefinitionToTermList(LIST Defs, LIST Terms,
				   FLAGSTORE Flags, PRECEDENCE Precedence)
/**************************************************************************
  INPUT:   A list of definitions <Defs> and a list of pairs (Label.Formula),
           the maximal number <Applics> of expansions, a flag store and a
	   precedence.
  RETURNS: The possibly destructively changed list <Terms>.
  EFFECT:  In all formulas of Terms any definition of Defs is applied exactly
           once if possible.
           The terms are changed destructively if the expanded def_predicate 
	   is not an equality.
**************************************************************************/
{
  TERM ActTerm;             /* Actual term in Terms */
  TERM DefPredicate;        /* Actual definition predicate out of Defs */
  TERM Expansion;           /* Expansion term of the definition */
  TERM Target;              /* Target predicate to be replaced */
  LIST TargetList, Scan1, Scan2, Scan3;
  BOOL Apply;
  int  Applics;

  Apply      = TRUE;
  TargetList = list_Nil();
  Applics    = flag_GetFlagValue(Flags, flag_APPLYDEFS);

  while (Apply && Applics != 0) {
    Apply = FALSE;
    
    for (Scan1=Defs; !list_Empty(Scan1) && Applics != 0; Scan1=list_Cdr(Scan1)) {
      DefPredicate = term_Copy(def_Predicate(list_Car(Scan1)));

      /*      puts("\n----\nDefPred:"); fol_PrettyPrintDFG(DefPredicate);*/

      for (Scan2=Terms; !list_Empty(Scan2) && Applics != 0; Scan2=list_Cdr(Scan2)) {
	ActTerm   = list_PairSecond(list_Car(Scan2));
	TargetList = term_FindAllAtoms(ActTerm, term_TopSymbol(DefPredicate));
	term_AddFatherLinks(ActTerm);
	
	/*	puts("\nActTerm:"); fol_PrettyPrintDFG(ActTerm);*/

	for (Scan3=TargetList; !list_Empty(Scan3) && Applics != 0; Scan3=list_Cdr(Scan3)) {
	  Target = list_Car(Scan3);
	  cont_StartBinding();

	  /*	  puts("\nTarget:"); fol_PrettyPrintDFG(Target);*/

	  if (unify_Match(cont_LeftContext(), DefPredicate, Target)) {
	    cont_BackTrack();
	    Expansion = term_Copy(def_Expansion(list_Car(Scan1)));
	    fol_NormalizeVarsStartingAt(ActTerm, term_MaxVar(Expansion));
	    unify_Match(cont_LeftContext(), DefPredicate, Target);

	    if (fol_ApplyContextToTerm(cont_LeftContext(), Expansion)) { /* Matcher applied on Expansion */
	      if (!def_HasGuard(list_Car(Scan1))) {
		Applics--;
		Apply = TRUE;
		/*		puts("\n*no Guard!");*/
		term_RplacTop(Target, term_TopSymbol(Expansion));
		term_DeleteTermList(term_ArgumentList(Target));
		term_RplacArgumentList(Target, term_ArgumentList(Expansion));
		term_RplacArgumentList(Expansion, list_Nil());
		term_AddFatherLinks(ActTerm);
#ifdef CHECK
		if (!fol_CheckFormula(ActTerm)) {
		  misc_StartErrorReport();
		  misc_ErrorReport("\n In def_ApplyDefinitionToTermList:");
		  misc_ErrorReport(" No correct formula ActTerm.");
		  misc_FinishErrorReport();
		}
#endif
		if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
		  puts("\nApplied definition for");
		  fol_PrettyPrintDFG(def_Predicate(list_Car(Scan1)));
		  puts("\nNew formula:");
		  fol_PrettyPrintDFG(ActTerm);
		}
	      }
	      else {  /* check guard */
		TERM Guard;
		Guard = term_Copy(def_ToProve(list_Car(Scan1)));
		if (fol_ApplyContextToTerm(cont_LeftContext(), Guard)) {
		  cont_BackTrack(); 
		  if (def_FindProofForGuard(ActTerm, Target,Guard,
					    Flags, Precedence)) {
		    Applics--;
		    Apply = TRUE;
		    term_RplacTop(Target, term_TopSymbol(Expansion));
		    term_DeleteTermList(term_ArgumentList(Target));
		    term_RplacArgumentList(Target, term_ArgumentList(Expansion));
		    term_RplacArgumentList(Expansion, list_Nil());
		    term_AddFatherLinks(ActTerm);
#ifdef CHECK
		    if (!fol_CheckFormula(ActTerm)) {
		      misc_StartErrorReport();
		      misc_ErrorReport("\n In def_ApplyDefinitionToTermList:");
		      misc_ErrorReport(" No correct formula ActTerm");
		      misc_FinishErrorReport();
		    }
#endif
		    if (flag_GetFlagValue(Flags, flag_PAPPLYDEFS)) {
		      puts("\nApplied definition for");
		      fol_PrettyPrintDFG(def_Predicate(list_Car(Scan1)));
		      puts("\nNew formula:");
		      fol_PrettyPrintDFG(ActTerm);
		    }
		  }
		}
		term_Delete(Guard);
	      }
	    }
	    term_Delete(Expansion);	    
	  }
	  cont_BackTrack();
	}
	list_Delete(TargetList);
      }
      term_Delete(DefPredicate);
    }
  }
  return Terms;
}