This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
reference:rule_method [2011/06/22 12:19] 131.246.161.187 |
reference:rule_method [2011/06/22 12:27] (current) 131.246.161.187 [Example] |
||
---|---|---|---|
Line 16: | Line 16: | ||
==== Example ==== | ==== Example ==== | ||
+ | Assume we have a goal | ||
+ | |||
+ | $\quad[|\ A |] \Longrightarrow A \vee B$ | ||
+ | |||
+ | Applying ''apply (rule disjI1)'' yields the new subgoal | ||
+ | |||
+ | $\quad [|\ A\ |] \Longrightarrow A$ | ||
+ | |||
+ | which can obviously be solved by one application of ''[[assumption]]''. Note that ''apply (rule(1) disjI)'' is a shortcut for this and immediately solves the goal. | ||
+ | |||
==== Non-Example ==== | ==== Non-Example ==== |