Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:proofs_and_induction [2008/02/21 16:49] vkuncak |
sav08:proofs_and_induction [2008/02/21 16:49] vkuncak |
||
|---|---|---|---|
| Line 93: | Line 93: | ||
| If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term //t// (this is what "for all" means). You keep the original quantified assumption in case you need to instantiate it multiple times. | If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term //t// (this is what "for all" means). You keep the original quantified assumption in case you need to instantiate it multiple times. | ||
| \[ | \[ | ||
| - | \frac{P(t), \forall x.P(x)} | + | \frac{P(t), \forall x.P(x) \vdash} |
| {\forall x.P(x) \vdash} | {\forall x.P(x) \vdash} | ||
| \] | \] | ||