|
>>> xPrime = GlueFormula("x1", "g")
>>> print(xPrime)
x1 : g
>>> xPrime_chases = chases.applyto(xPrime)
>>> print(xPrime_chases.simplify())
\y.chases(x1,y) : (h -o f)
>>> yPrime = GlueFormula("x2", "h")
>>> print(yPrime)
x2 : h
>>> xPrime_chases_yPrime = xPrime_chases.applyto(yPrime)
>>> print(xPrime_chases_yPrime.simplify())
chases(x1,x2) : f
>>> chases_yPrime = xPrime_chases_yPrime.lambda_abstract(xPrime)
>>> print(chases_yPrime.simplify())
\x1.chases(x1,x2) : (g -o f)
>>> every_girl_chases_yPrime = every_girl.applyto(chases_yPrime)
>>> print(every_girl_chases_yPrime.simplify())
all x.(girl(x) -> chases(x,x2)) : f
>>> every_girl_chases = every_girl_chases_yPrime.lambda_abstract(yPrime)
>>> print(every_girl_chases.simplify())
\x2.all x.(girl(x) -> chases(x,x2)) : (h -o f)
>>> every_girl_chases_a_dog = a_dog.applyto(every_girl_chases)
>>> r1 = every_girl_chases_a_dog.simplify()
>>> r2 = GlueFormula(r'exists x.(dog(x) & all z2.(girl(z2) -> chases(z2,x)))', 'f')
>>> r1 == r2
True
|