Question 305

[Troy Pocklington]

if you have this in the conclusion

(forall e : ((mem e x) --> (mem e y)))

can you simplify it to

(mem e x) --> (mem e y)

or does it simplify to

((mem e x) --> (mem e y))

or are they the same...

--
-Troy

[Nathan Wetzler]

I'm not entirely sure, but I think it makes a difference. Promotion
requires (p --> (q --> r)).

[Anar Seyf]

If one of your hypotheses is:
(A e : ((mem e (cdr x)) --> (mem e y))),

and the conclusion is:
(A e : ((mem e x) --> (mem e y))),

what's the next step? Do you take the route of expanding (mem e x), or
do you use All-Concl to replace x with (cdr x)?

Anar

[dsny...@gmail.com]

I'm not sure, but I don't think you could replace x with (cdr x),
because if your formula looks like mine you already have some
hypotheses which depend on the value of (cdr x), which implies that
(cdr x) is free in the formula, and would be captured by that
instantiation. Please correct me someone if I am thinking
incorrectly.

[Nathan Wetzler]

You can use forall-concl at that point (possibly doing an alpha
conversion first, depending on your formula). Then you should be able
to expand mem and simplify with the hyp (consp x).

On Apr 21, 12:21 pm, Anar Seyf <anar.s...@gmail.com> wrote: