summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Ref/simp.tex

changeset 1100 | 74921c7613e7 |

parent 323 | 361a71713176 |

child 9695 | ec7d7f877712 |

equal
deleted
inserted
replaced

1099:f4335b56f772 | 1100:74921c7613e7 |
---|---|

53 {\bf Additional assumptions} are allowed: |
53 {\bf Additional assumptions} are allowed: |

54 \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} |
54 \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} |

55 \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}) |
55 \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}) |

56 \] |
56 \] |

57 This rule assumes $Q@1$, and any rewrite rules it contains, while |
57 This rule assumes $Q@1$, and any rewrite rules it contains, while |

58 simplifying~$P@2$. Such ``local'' assumptions are effective for rewriting |
58 simplifying~$P@2$. Such `local' assumptions are effective for rewriting |

59 formulae such as $x=0\imp y+x=y$. |
59 formulae such as $x=0\imp y+x=y$. |

60 |
60 |

61 {\bf Additional quantifiers} are allowed, typically for binding operators: |
61 {\bf Additional quantifiers} are allowed, typically for binding operators: |

62 \[ \List{\Forall z. \Var{P}(z) \bimp \Var{Q}(z)} \Imp |
62 \[ \List{\Forall z. \Var{P}(z) \bimp \Var{Q}(z)} \Imp |

63 \forall x.\Var{P}(x) \bimp \forall x.\Var{Q}(x) |
63 \forall x.\Var{P}(x) \bimp \forall x.\Var{Q}(x) |