% Free variable tester
% freevars.pl

fvs(~(Expr), N) :- !,
   fvs(Expr, N).

fvs(QuantExpr, N) :-
   QuantExpr =.. [Qfier, Var, Body],
   quantifier(Qfier), !,
   Var = '@var'(N),
   N1 is N + 1,
   fvs(Body, N1).

fvs(CompExpr, N) :-
   CompExpr =.. [Connective, Expr1, Expr2],
   connective(Connective), !,
   (fvs(Expr1, N)
   ;
    fvs(Expr2, N)).

fvs(Expr, N) :-
   Expr =.. [Pred|Args],
   fvs(Args).

fvs([A|As]) :- var(A), !.

fvs([A|As]) :- fvs(As).