Stream: Beginner Questions

Topic: ✔ solve by assumption

view this post on Zulip Robert Soeldner (Dec 13 2021 at 20:01):

Hi,
shouldn't the goal be solved directly by the two assumptions?
I struggle understanding the current "problem" :-)

using this:
    ?x ∈ E ⟹ t ?x = Some ?y ⟶ ?y ∈ V
    ?x ∉ E ⟹ t ?x = None

goal (1 subgoal):
 1. ran t = V

view this post on Zulip Wolfgang Jeltsch (Dec 14 2021 at 00:56):

You can only have the goal solved by assumption if the goal is literally one of the assumptions, which in your example it’s apparently not.

In fact, the goal does not even follow from the assumptions. Consider the situation where t x is None for every x. Then both assumptions are true independently of V, but the goal would be equivalent to V = {}.

view this post on Zulip Notification Bot (Dec 14 2021 at 18:26):

Robert Soeldner has marked this topic as resolved.

Last updated: Apr 19 2024 at 12:27 UTC