text: /**************************************************************/
  /* ********************************************************** */
  /* *                                                        * */
  /* *                       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-25 00:10:28 -0400 (Mon, 25 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;
  }
  