Changes between Version 72 and Version 73 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 28, 2008 2:34:48 PM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v72 v73  
    176176 where `x` occurs in `F s1..sn`.  (`co1` may be local or wanted.) 
    177177 
    178  NB: No normalisation required.  Afterwards, !SubstVarVar or !SubstVarFam may apply to `co1` and all rules, except !SubstVarVar, may apply to `co2'`.  However, !SubstVarFam cannot again apply to `co1` and `co2'`, as `t` cannot contain `x` -- cf. the definition of normal equalities.. 
     178 NB: No normalisation required.  Afterwards, !SubstVarVar or !SubstVarFam may apply to `co1` and all rules, except !SubstVarVar, may apply to `co2'`.  However, !SubstVarFam cannot again apply to `co1` and `co2'`, as `t` cannot contain `x` -- cf. the definition of normal equalities. 
     179 
     180NB: In the three substitution rules, it is never necessary to try using `co1` with any of the equalities derived from `co2'`.  Hence, after having considered one equality as `co1` with every other equality, we can immediately put `co1` into the list of residual equalities. 
    179181 
    180182