function Prove( search:mode; query, facts :tree; e :Env) :boolean;
   label 99; {success escape for Silent mode}
   var Satisfied :boolean;

   procedure ProveList( query, facts :tree; e :Env );
   
      procedure ProveLiteral(p, f :tree; e :Env);
         var newe :Env;
      begin
         if p^.tag = negate then                { negated atom eg. not l(...) }
         begin {negation by failure: not p(...) succeeds iff p(...) fails}
               if not Prove(Silent, cons(p^.l, nil), f, e) then
                  ProveList(query^.tl, f, e)                    {rest of query}
              {else do nothing at all}
         end
         else { positive atom  eg.  p(...) }
         if f <> nil then
         begin if unify(p, rename(f^.hd^.lhs, index), newe, e) then
                  ProveList(append(rename(f^.hd^.rhs, index),     {RHS of rule}
                                   query^.tl),             {plus rest of query}
                            facts, newe);
               ProveLiteral(p, f^.tl, e)         {also try for other solutions}
         end
      end {ProveLiteral};
   
   begin {ProveList}
      if query = nil then {nothing more to prove - success}
      case search of
      PrintAll:{print ALL solutions to query}
         begin printtree(prog^.query, e); writeln(' yes'); Satisfied:=true end;
      Silent:  {esp' for negation by failure, only need one success}
         begin Satisfied := true; goto 99 {!!! once is enough} end
      end
      else
         begin index:=index+1; ProveLiteral(query^.hd, facts, e) end
   end  {ProveList};
 
begin { Prove }
   Satisfied := false;
   ProveList( query, facts, e);
   99: Prove := Satisfied
end { Prove };

{\fB Depth-First, Left-to-Right Proof Strategy. \fP}
{Do not remove: Main.p, env*P, execute.P, unify.P, rename.P, prove.P, lex*P, }
{ syntax*P, tree.P are released under Gnu `copyleft' General Public Licence  }
{ - L. Allison, CSSE, Monash Uni., .au, 7/2003.                              }