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)