User Tools
reference:drule
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
reference:drule [2011/06/22 12:29] 131.246.161.187 |
reference:drule [2011/06/22 12:34] 131.246.161.187 |
||
|---|---|---|---|
| Line 16: | Line 16: | ||
| * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ ; U(Q) |] \Longrightarrow U(C)$ | * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ ; U(Q) |] \Longrightarrow U(C)$ | ||
| * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$ \\ for each $k = 2, \dots, n$. | * $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots U(A_{j-1}); U(A_{j+1}); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$ \\ for each $k = 2, \dots, n$. | ||
| + | |||
| + | Note that ''drule'' is almost the same as ''[[frule]]''. The only difference is that ''frule'' keeps the assumption "used" by the used rule $A_j$ while ''drule'' drops it. This is useful if $A_j$ is needed to prove the new subgoals; ''drule'' is unsafe because of this. | ||
| ==== Example ==== | ==== Example ==== | ||
reference/drule.txt ยท Last modified: 2011/07/06 12:08 by 131.246.161.187
Page Tools
