| Mon, 01 Feb 2010 11:16:31 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Mon, 01 Feb 2010 11:16:13 +0100 |
Cezary Kaliszyk |
More proofs in the LF example.
|
changeset |
files
|
| Mon, 01 Feb 2010 11:00:51 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Mon, 01 Feb 2010 10:00:03 +0100 |
Christian Urban |
slight tuning
|
changeset |
files
|
| Mon, 01 Feb 2010 09:47:46 +0100 |
Christian Urban |
renamed function according to the name of the constant
|
changeset |
files
|
| Mon, 01 Feb 2010 09:04:22 +0100 |
Christian Urban |
fixed problem with Bex1_rel renaming
|
changeset |
files
|
| Mon, 01 Feb 2010 09:56:32 +0100 |
Cezary Kaliszyk |
Ported LF to the generic lambda and solved the simpler _supp cases.
|
changeset |
files
|
| Sat, 30 Jan 2010 12:12:52 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Sat, 30 Jan 2010 11:44:25 +0100 |
Christian Urban |
introduced a generic alpha (but not sure whether it is helpful)
|
changeset |
files
|
| 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
|
| Thu, 28 Jan 2010 10:52:10 +0100 |
Cezary Kaliszyk |
Substracting bounds from free variables.
|
changeset |
files
|
| Thu, 28 Jan 2010 10:26:36 +0100 |
Cezary Kaliszyk |
Improper interface for datatype and function packages and proper interface lateron.
|
changeset |
files
|
| Thu, 28 Jan 2010 09:28:20 +0100 |
Christian Urban |
merged
|
changeset |
files
|
| Thu, 28 Jan 2010 09:28:06 +0100 |
Christian Urban |
minor
|
changeset |
files
|
| Thu, 28 Jan 2010 01:24:09 +0100 |
Christian Urban |
test about supp/freshness for lam (old proofs work in principle - for single binders)
|
changeset |
files
|
| Thu, 28 Jan 2010 08:13:39 +0100 |
Cezary Kaliszyk |
Recommited the changes for nitpick
|
changeset |
files
|