And (Forall x p) (Forall y q) -> pullq True True fm Forall And x y p q
[Forum Game] Paste whatever's on your clipboard!
BLUbeans
#1830
public interface ConcurrentNavigableMap<K,V>
extends ConcurrentMap<K,V>, NavigableMap<K,V>
A ConcurrentMap supportin
Mynamerr
#1831
subst::(String->Term)->Formula FOL->Formula FOL
subst subfn fm=
case fm of
Bottom->Bottom
Top->Top
Atom(R p args)->Atom(R p (map (tsubst subfn) args))
Not p->Not (subst subfn p)
And p q->And (subst subfn p) (subst subfn q)
Or p q ->Or (subst subfn p) (subst subfn q)
Imp p q ->Imp (subst subfn p) (subst subfn q)
Iff p q ->Iff (subst subfn p) (subst subfn q)
Forall x p ->substq subfn mk_forall x p
Exists x p ->substq subfn mk_exists x p
where
substq subfn quant x p=
let x’=if (any (\y->elem x (fvt(subfn y ))) (filter (x/=) (fv p)))
then variant x (fv (subst (\z->if z==x then Var x else subfn z) p)) else x in
quant x’ (subst (\w->if w==x then Var x’ else subfn w) p)
Bulwqeajli
#1842
[ size=I see you’ve met GGaod. He’s quite… Unusually “active” in certain things…][/size]
