equal
deleted
inserted
replaced
1477 |
1477 |
1478 Unfolding the definition of supports on both sides of the equations we |
1478 Unfolding the definition of supports on both sides of the equations we |
1479 obtain by simple calculations the equalities. |
1479 obtain by simple calculations the equalities. |
1480 \end{proof} |
1480 \end{proof} |
1481 |
1481 |
1482 With the above equations we can substitute free variables for support in |
1482 %%% Without defining permute_bn, we cannot even write the substitution |
1483 the lifted free variable equations, which gives us the support equations |
1483 %%% of bindings in term constructors... |
1484 for the term constructors. With this we can show that for each binding in |
1484 |
1485 a constructors the bindings can be renamed. |
1485 % With the above equations we can substitute free variables for support in |
|
1486 % the lifted free variable equations, which gives us the support equations |
|
1487 % for the term constructors. With this we can show that for each binding in |
|
1488 % a constructors the bindings can be renamed. |
1486 |
1489 |
1487 *} |
1490 *} |
1488 |
1491 |
1489 text {* |
1492 text {* |
1490 %%% FIXME: The restricions should have already been described in previous sections? |
1493 %%% FIXME: The restricions should have already been described in previous sections? |