equal
deleted
inserted
replaced
229 |
229 |
230 |
230 |
231 writeln"Hard examples with quantifiers"; |
231 writeln"Hard examples with quantifiers"; |
232 |
232 |
233 (*The ones that have not been proved are not known to be valid! |
233 (*The ones that have not been proved are not known to be valid! |
234 SOME will require quantifier duplication -- not currently available*) |
234 Some will require quantifier duplication -- not currently available*) |
235 |
235 |
236 writeln"Problem ~~18"; |
236 writeln"Problem ~~18"; |
237 goal IFOLP.thy "?p : ~~(EX y. ALL x. P(y)-->P(x))"; |
237 goal IFOLP.thy "?p : ~~(EX y. ALL x. P(y)-->P(x))"; |
238 (*NOT PROVED*) |
238 (*NOT PROVED*) |
239 |
239 |