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