| Fri, 29 Jan 2010 19:42:07 +0100 |
Cezary Kaliszyk |
More in the LF example in the new nominal way, all is clear until support.
|
changeset |
files
|
| Fri, 29 Jan 2010 13:47:05 +0100 |
Cezary Kaliszyk |
Fixed the induction problem + some more proofs.
|
changeset |
files
|
| Fri, 29 Jan 2010 12:16:08 +0100 |
Cezary Kaliszyk |
equivariance of rfv and alpha.
|
changeset |
files
|
| Fri, 29 Jan 2010 10:13:07 +0100 |
Cezary Kaliszyk |
Added the experiments with fun and function.
|
changeset |
files
|
| Fri, 29 Jan 2010 07:09:52 +0100 |
Christian Urban |
now also final step is proved - the supp of lambdas is now completely characterised
|
changeset |
files
|
| Fri, 29 Jan 2010 00:22:00 +0100 |
Christian Urban |
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms
|
changeset |
files
|
| Thu, 28 Jan 2010 23:47:02 +0100 |
Christian Urban |
improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
|
changeset |
files
|
| Thu, 28 Jan 2010 23:36:58 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Thu, 28 Jan 2010 23:36:38 +0100 |
Christian Urban |
general abstraction operator and complete characterisation of its support and freshness
|
changeset |
files
|
| Thu, 28 Jan 2010 19:23:55 +0100 |
Cezary Kaliszyk |
Ported existing part of LF to new permutations and alphas.
|
changeset |
files
|
| Thu, 28 Jan 2010 15:47:35 +0100 |
Christian Urban |
attempt of a general abstraction operator
|
changeset |
files
|
| Thu, 28 Jan 2010 14:20:26 +0100 |
Christian Urban |
attempt to prove equivalence between alpha definitions
|
changeset |
files
|
| Thu, 28 Jan 2010 12:28:50 +0100 |
Cezary Kaliszyk |
End of renaming.
|
changeset |
files
|
| Thu, 28 Jan 2010 12:25:38 +0100 |
Cezary Kaliszyk |
Minor when looking at lam.distinct and lam.inject
|
changeset |
files
|
| Thu, 28 Jan 2010 12:24:49 +0100 |
Cezary Kaliszyk |
Renamed Bexeq to Bex1_rel
|
changeset |
files
|