equal
deleted
inserted
replaced
1995 that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"} |
1995 that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"} |
1996 and we are done with this case. |
1996 and we are done with this case. |
1997 |
1997 |
1998 The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated. |
1998 The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated. |
1999 The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"}, |
1999 The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"}, |
2000 because @{text p} might contain names that are bound (by @{text bn}) and so are |
2000 because @{text p} might contain names bound by @{text bn}, but also some that are |
2001 free. To solve this problem we have to introduce a permutation function that only |
2001 free. To solve this problem we have to introduce a permutation function that only |
2002 permutes names bound by @{text bn} and leaves the other names unchanged. We do this again |
2002 permutes names bound by @{text bn} and leaves the other names unchanged. We do this again |
2003 by lifting. For a |
2003 by lifting. For a |
2004 clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define |
2004 clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define |
2005 % |
2005 % |