User Tools
reference:attribute_examples
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
reference:attribute_examples [2011/07/06 13:07] 131.246.161.187 [THEN] |
reference:attribute_examples [2011/07/07 12:10] 131.246.161.187 [of] |
||
|---|---|---|---|
| Line 9: | Line 9: | ||
| Using | Using | ||
| - | | ||
| mp [of _ "C ∨ D"] | mp [of _ "C ∨ D"] | ||
| - | | ||
| yields the more specific theorem | yields the more specific theorem | ||
| Line 24: | Line 22: | ||
| Using | Using | ||
| - | | ||
| mp [where Q="C ∨ D"] | mp [where Q="C ∨ D"] | ||
| - | | ||
| yields the more specific theorem | yields the more specific theorem | ||
| Line 60: | Line 56: | ||
| which allows substitutions from right to left. | which allows substitutions from right to left. | ||
| ==== simplified ==== | ==== simplified ==== | ||
| + | Consider theorem ''Nat.le_square'': | ||
| + | |||
| + | $\quad ?m \leq\ ?m\ \cdot\ ?m$ | ||
| + | |||
| + | Using | ||
| + | |||
| + | Nat.le_square [simplified] | ||
| + | you get | ||
| + | |||
| + | $\quad 0 <\ ?m \longrightarrow Suc\ 0 \leq\ ?m$ | ||
| + | |||
| + | Wether or not this is actually "simpler" is certainly open to discussion, especially because the original form does say something about $?m=0$ while the ''simplified'' version does not. | ||
| ==== rotated ==== | ==== rotated ==== | ||
| Consider rule ''disjE'': | Consider rule ''disjE'': | ||
| Line 68: | Line 76: | ||
| disjE [rotated 2] | disjE [rotated 2] | ||
| - | | ||
| yields | yields | ||
| Line 79: | Line 86: | ||
| Then, | Then, | ||
| - | test [symmetric] | + | test [symmetric] |
| - | + | ||
| yields | yields | ||
| $\quad ?X ?x = (?x \in ?X)$. | $\quad ?X ?x = (?x \in ?X)$. | ||
reference/attribute_examples.txt · Last modified: 2011/07/25 12:32 by 131.246.41.159
Page Tools
