reference:rule_method

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] 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 ==== |

reference/rule_method.txt ยท Last modified: 2011/06/22 12:27 by 131.246.161.187