2010-01-30 Christian Urban merged
2010-01-30 Christian Urban introduced a generic alpha (but not sure whether it is helpful)
2010-01-29 Cezary Kaliszyk More in the LF example in the new nominal way, all is clear until support.
2010-01-29 Cezary Kaliszyk Fixed the induction problem + some more proofs.
2010-01-29 Cezary Kaliszyk equivariance of rfv and alpha.
2010-01-29 Cezary Kaliszyk Added the experiments with fun and function.
2010-01-29 Christian Urban now also final step is proved - the supp of lambdas is now completely characterised
2010-01-28 Christian Urban the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms
2010-01-28 Christian Urban improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
2010-01-28 Christian Urban merged
2010-01-28 Christian Urban general abstraction operator and complete characterisation of its support and freshness
2010-01-28 Cezary Kaliszyk Ported existing part of LF to new permutations and alphas.
2010-01-28 Christian Urban attempt of a general abstraction operator
2010-01-28 Christian Urban attempt to prove equivalence between alpha definitions
2010-01-28 Cezary Kaliszyk End of renaming.
Loading...
(0) -300 -100 -15 +15 +100 +300 +1000 tip