User Tools
reference:rule_method
Differences
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 ==== | ||
reference/rule_method.1308737999.txt.gz ยท Last modified: 2011/06/22 12:19 by 131.246.161.187
Page Tools
