2010-03-22 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 14:07:07 +0100] rev 1573
fv_rsp proved automatically.
2010-03-22 more on the paper
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 11:55:29 +0100] rev 1572
more on the paper
2010-03-22 merged
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 10:21:14 +0100] rev 1571
merged
2010-03-22 tuned paper
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 10:20:57 +0100] rev 1570
tuned paper
2010-03-22 some tuning
Christian Urban <urbanc@in.tum.de> [Mon, 22 Mar 2010 09:16:25 +0100] rev 1569
some tuning
2010-03-22 Strong induction for Type Schemes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 10:15:46 +0100] rev 1568
Strong induction for Type Schemes.
2010-03-22 Fixed missing colon.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Mar 2010 09:02:30 +0100] rev 1567
Fixed missing colon.
2010-03-21 tuned paper
Christian Urban <urbanc@in.tum.de> [Sun, 21 Mar 2010 22:27:08 +0100] rev 1566
tuned paper
2010-03-20 merged
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 18:16:26 +0100] rev 1565
merged
2010-03-20 proved at_set_avoiding2 which is needed for strong induction principles
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 16:27:51 +0100] rev 1564
proved at_set_avoiding2 which is needed for strong induction principles
2010-03-20 moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 13:50:00 +0100] rev 1563
moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
2010-03-20 Size experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Mar 2010 10:12:09 +0100] rev 1562
Size experiments.
2010-03-20 Use 'alpha_bn_refl' to get rid of one of the sorrys.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Mar 2010 09:27:28 +0100] rev 1561
Use 'alpha_bn_refl' to get rid of one of the sorrys.
2010-03-20 Build alpha-->alphabn implications
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Mar 2010 08:56:07 +0100] rev 1560
Build alpha-->alphabn implications
2010-03-20 Prove reflp for all relations.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Mar 2010 08:04:59 +0100] rev 1559
Prove reflp for all relations.
2010-03-20 started cleaning up and introduced 3 versions of ~~gen
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 04:51:26 +0100] rev 1558
started cleaning up and introduced 3 versions of ~~gen
2010-03-20 moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
Christian Urban <urbanc@in.tum.de> [Sat, 20 Mar 2010 02:46:07 +0100] rev 1557
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
2010-03-19 more work on the paper
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 21:04:24 +0100] rev 1556
more work on the paper
2010-03-19 Described automatically created funs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 18:56:13 +0100] rev 1555
Described automatically created funs.
2010-03-19 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 18:43:29 +0100] rev 1554
merge
2010-03-19 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 18:42:57 +0100] rev 1553
Automatically derive support for datatypes with at-most one binding per constructor.
2010-03-19 picture
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 17:20:25 +0100] rev 1552
picture
2010-03-19 merged
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 15:43:59 +0100] rev 1551
merged
2010-03-19 polished
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 15:43:43 +0100] rev 1550
polished
2010-03-19 Update Test to use fset.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 15:01:01 +0100] rev 1549
Update Test to use fset.
2010-03-19 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 14:54:57 +0100] rev 1548
merge
2010-03-19 Use fs typeclass in showing finite support + some cheat cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 14:54:30 +0100] rev 1547
Use fs typeclass in showing finite support + some cheat cleaning.
2010-03-19 merged
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 12:31:55 +0100] rev 1546
merged
2010-03-19 more one the paper
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 12:31:17 +0100] rev 1545
more one the paper
2010-03-19 Keep only one copy of infinite_Un.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 12:28:35 +0100] rev 1544
Keep only one copy of infinite_Un.
2010-03-19 Added a missing 'import'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 12:24:16 +0100] rev 1543
Added a missing 'import'.
2010-03-19 Showed the instance: fset::(at) fs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 12:22:10 +0100] rev 1542
Showed the instance: fset::(at) fs
2010-03-19 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 10:24:49 +0100] rev 1541
merge
2010-03-19 Remove atom_decl from the parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 10:24:16 +0100] rev 1540
Remove atom_decl from the parser.
2010-03-19 TySch strong induction looks ok.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 10:23:52 +0100] rev 1539
TySch strong induction looks ok.
2010-03-19 Working on TySch strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 09:31:38 +0100] rev 1538
Working on TySch strong induction.
2010-03-19 Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 09:03:10 +0100] rev 1537
Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
2010-03-19 merged
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 09:40:57 +0100] rev 1536
merged
2010-03-19 more tuning on the paper
Christian Urban <urbanc@in.tum.de> [Fri, 19 Mar 2010 09:40:34 +0100] rev 1535
more tuning on the paper
2010-03-19 The nominal infrastructure for fset. 'fs' missing, but not needed so far.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 08:31:43 +0100] rev 1534
The nominal infrastructure for fset. 'fs' missing, but not needed so far.
2010-03-19 A few more theorems in FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 06:55:17 +0100] rev 1533
A few more theorems in FSet.
2010-03-18 merge 2
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 00:36:08 +0100] rev 1532
merge 2
2010-03-18 merge 1
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 00:35:58 +0100] rev 1531
merge 1
2010-03-18 support of fset_to_set, support of fmap_atom.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Mar 2010 00:35:20 +0100] rev 1530
support of fset_to_set, support of fmap_atom.
2010-03-18 merged
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 23:39:48 +0100] rev 1529
merged
2010-03-18 more tuning on the paper
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 23:39:26 +0100] rev 1528
more tuning on the paper
2010-03-18 added item about size functions
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 23:38:01 +0100] rev 1527
added item about size functions
2010-03-18 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 23:20:46 +0100] rev 1526
merge
2010-03-18 Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 23:19:55 +0100] rev 1525
Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
2010-03-18 tuned
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 22:06:28 +0100] rev 1524
tuned
2010-03-18 another little bit for the introduction
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 19:39:01 +0100] rev 1523
another little bit for the introduction
2010-03-18 Leroy96 supp=fv and fixes to make it compile
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 19:02:33 +0100] rev 1522
Leroy96 supp=fv and fixes to make it compile
2010-03-18 merged
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 18:43:21 +0100] rev 1521
merged
2010-03-18 more of the introduction
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 18:43:03 +0100] rev 1520
more of the introduction
2010-03-18 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 18:10:49 +0100] rev 1519
merge
2010-03-18 Added a cleaned version of FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 18:10:20 +0100] rev 1518
Added a cleaned version of FSet.
2010-03-18 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 16:22:10 +0100] rev 1517
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
2010-03-18 Continued description of alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 15:32:49 +0100] rev 1516
Continued description of alpha.
2010-03-18 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 15:13:20 +0100] rev 1515
Rename "_property" to ".property"
2010-03-18 First part of the description of alpha_ty.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 14:48:27 +0100] rev 1514
First part of the description of alpha_ty.
2010-03-18 Description of generation of alpha_bn.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 14:29:42 +0100] rev 1513
Description of generation of alpha_bn.
2010-03-18 case names also for _induct
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 14:05:49 +0100] rev 1512
case names also for _induct
2010-03-18 Case_Names for _inducts. Does not work for _induct yet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 12:32:03 +0100] rev 1511
Case_Names for _inducts. Does not work for _induct yet.
2010-03-18 Added fv,bn,distinct,perm to the simplifier.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 12:09:59 +0100] rev 1510
Added fv,bn,distinct,perm to the simplifier.
2010-03-18 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:37:10 +0100] rev 1509
merge
2010-03-18 Simplified the description.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:36:03 +0100] rev 1508
Simplified the description.
2010-03-18 merged
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 11:33:56 +0100] rev 1507
merged
2010-03-18 slightly more in the paper
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 11:33:37 +0100] rev 1506
slightly more in the paper
2010-03-18 Update the description of the generation of fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:29:12 +0100] rev 1505
Update the description of the generation of fv function.
2010-03-18 fv_bn may need to call other fv_bns.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:16:53 +0100] rev 1504
fv_bn may need to call other fv_bns.
2010-03-18 Update TODO.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 10:15:57 +0100] rev 1503
Update TODO.
2010-03-18 Which proofs need a 'sorry'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 10:12:41 +0100] rev 1502
Which proofs need a 'sorry'.
2010-03-18 added TODO
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 10:05:36 +0100] rev 1501
added TODO
2010-03-18 vixed variable names
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 10:02:21 +0100] rev 1500
vixed variable names
2010-03-18 simplified strong induction proof by using flip
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 09:31:31 +0100] rev 1499
simplified strong induction proof by using flip
2010-03-18 Rename bound variables + minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 08:32:55 +0100] rev 1498
Rename bound variables + minor cleaning.
2010-03-18 Move most of the exporting out of the parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 08:03:42 +0100] rev 1497
Move most of the exporting out of the parser.
2010-03-18 Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 07:43:44 +0100] rev 1496
Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
2010-03-18 Prove eqvts on exported terms.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 07:35:44 +0100] rev 1495
Prove eqvts on exported terms.
2010-03-18 Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 07:26:36 +0100] rev 1494
Clean 'Lift', start working only on exported things in Parser.
2010-03-17 slightly more of the paper
Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 00:17:21 +0100] rev 1493
slightly more of the paper
2010-03-17 merged
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 20:42:42 +0100] rev 1492
merged
2010-03-17 paper uses now a heap file - does not compile so long anymore
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 20:42:22 +0100] rev 1491
paper uses now a heap file - does not compile so long anymore
2010-03-17 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 18:53:23 +0100] rev 1490
merge
2010-03-17 compose_sym2 works also for term5
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 18:52:59 +0100] rev 1489
compose_sym2 works also for term5
2010-03-17 Updated Term1, including statement of strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 17:59:04 +0100] rev 1488
Updated Term1, including statement of strong induction.
2010-03-17 Proper compose_sym2
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 17:40:14 +0100] rev 1487
Proper compose_sym2
2010-03-17 merged
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 17:11:23 +0100] rev 1486
merged
2010-03-17 temporarily disabled tests in Nominal/ROOT
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 17:10:19 +0100] rev 1485
temporarily disabled tests in Nominal/ROOT
2010-03-17 made paper to compile
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 15:13:31 +0100] rev 1484
made paper to compile
2010-03-17 added partial proof for the strong induction principle
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 15:13:03 +0100] rev 1483
added partial proof for the strong induction principle
2010-03-17 Trying to find a compose lemma for 2 arguments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 17:09:01 +0100] rev 1482
Trying to find a compose lemma for 2 arguments.
2010-03-17 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 12:23:04 +0100] rev 1481
merge
2010-03-17 cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 12:18:35 +0100] rev 1480
cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
2010-03-17 merged
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 11:54:22 +0100] rev 1479
merged
2010-03-17 added proof of supp/fv for type schemes
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 11:53:56 +0100] rev 1478
added proof of supp/fv for type schemes
2010-03-17 Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 11:40:58 +0100] rev 1477
Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
2010-03-17 Remove Term5a, since it is now identical to Term5.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 11:20:24 +0100] rev 1476
Remove Term5a, since it is now identical to Term5.
2010-03-17 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 11:11:42 +0100] rev 1475
merge
2010-03-17 Finished all proofs in Term5 and Term5n.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 11:11:25 +0100] rev 1474
Finished all proofs in Term5 and Term5n.
2010-03-17 added partial proof of supp for type schemes
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 10:34:25 +0100] rev 1473
added partial proof of supp for type schemes
2010-03-17 Fix in alpha; support of the recursive Let works :)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:57:54 +0100] rev 1472
Fix in alpha; support of the recursive Let works :)
2010-03-17 The recursive supp just has one equation too much.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:42:56 +0100] rev 1471
The recursive supp just has one equation too much.
2010-03-17 Fix for the change of alpha_gen.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:25:01 +0100] rev 1470
Fix for the change of alpha_gen.
2010-03-17 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:18:27 +0100] rev 1469
merge
2010-03-17 Generate compound FV and Alpha for recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 09:17:55 +0100] rev 1468
Generate compound FV and Alpha for recursive bindings.
2010-03-17 Lifting theorems with compound fv and compound alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Mar 2010 08:39:46 +0100] rev 1467
Lifting theorems with compound fv and compound alpha.
2010-03-17 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 08:07:25 +0100] rev 1466
commented out examples that should not work; but for example type-scheme example should work
2010-03-17 added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de> [Wed, 17 Mar 2010 06:49:33 +0100] rev 1465
added another supp-proof for the non-recursive case
2010-03-16 Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 20:07:13 +0100] rev 1464
Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
2010-03-16 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 18:19:00 +0100] rev 1463
merge
2010-03-16 The old recursive alpha works fine.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 18:18:08 +0100] rev 1462
The old recursive alpha works fine.
2010-03-16 added the final unfolded result
Christian Urban <urbanc@in.tum.de> [Tue, 16 Mar 2010 18:13:34 +0100] rev 1461
added the final unfolded result
2010-03-16 merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de> [Tue, 16 Mar 2010 18:02:08 +0100] rev 1460
merge and proof of support for non-recursive case
2010-03-16 Added Term5 non-recursive. The bug is there only for the recursive case.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 17:20:46 +0100] rev 1459
Added Term5 non-recursive. The bug is there only for the recursive case.
2010-03-16 Alpha is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 17:11:32 +0100] rev 1458
Alpha is wrong.
2010-03-16 alpha_bn doesn't need the permutation in non-recursive case.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 16:51:06 +0100] rev 1457
alpha_bn doesn't need the permutation in non-recursive case.
2010-03-16 alpha5_transp and equivp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 16:17:05 +0100] rev 1456
alpha5_transp and equivp
2010-03-16 alpha5_symp proved.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 15:38:14 +0100] rev 1455
alpha5_symp proved.
2010-03-16 FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 15:27:47 +0100] rev 1454
FV_bn generated for recursive functions as well, and used in main fv for bindings.
2010-03-16 The proof in 'Test' gets simpler.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 12:08:37 +0100] rev 1453
The proof in 'Test' gets simpler.
2010-03-16 Removed pi o bn = bn' assumption in alpha
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Mar 2010 12:06:22 +0100] rev 1452
Removed pi o bn = bn' assumption in alpha
2010-03-15 merged (confirmed to work with Isabelle from 6th March)
Christian Urban <urbanc@in.tum.de> [Mon, 15 Mar 2010 23:42:56 +0100] rev 1451
merged (confirmed to work with Isabelle from 6th March)
2010-03-15 another synchronisation
Christian Urban <urbanc@in.tum.de> [Mon, 15 Mar 2010 17:52:31 +0100] rev 1450
another synchronisation
2010-03-15 proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de> [Mon, 15 Mar 2010 17:51:35 +0100] rev 1449
proof for support when bn-function is present, but fb_function is empty
2010-03-15 fv_eqvt_cheat no longer needed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Mar 2010 17:42:17 +0100] rev 1448
fv_eqvt_cheat no longer needed.
2010-03-15 derive "inducts" from "induct" instead of lifting again is much faster.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Mar 2010 14:32:05 +0100] rev 1447
derive "inducts" from "induct" instead of lifting again is much faster.
2010-03-15 build_eqvts works with recursive case if proper induction rule is used.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Mar 2010 13:56:17 +0100] rev 1446
build_eqvts works with recursive case if proper induction rule is used.
2010-03-15 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Mar 2010 11:50:12 +0100] rev 1445
cheat_alpha_eqvt no longer needed; the proofs work.
2010-03-15 LF works with new alpha...?
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Mar 2010 10:36:09 +0100] rev 1444
LF works with new alpha...?
2010-03-15 explicit flag "cheat_equivp"
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Mar 2010 10:07:15 +0100] rev 1443
explicit flag "cheat_equivp"
2010-03-15 Prove alpha_gen_compose_eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Mar 2010 10:02:19 +0100] rev 1442
Prove alpha_gen_compose_eqvt
2010-03-15 Use eqvt.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Mar 2010 09:27:25 +0100] rev 1441
Use eqvt.
2010-03-15 added preliminary test version....but Test works now
Christian Urban <urbanc@in.tum.de> [Mon, 15 Mar 2010 08:39:23 +0100] rev 1440
added preliminary test version....but Test works now
2010-03-15 added an eqvt-proof for bi
Christian Urban <urbanc@in.tum.de> [Mon, 15 Mar 2010 08:28:10 +0100] rev 1439
added an eqvt-proof for bi
2010-03-15 synchronised with main hg-repository; used add_typedef_global in nominal_atoms
Christian Urban <urbanc@in.tum.de> [Mon, 15 Mar 2010 06:11:35 +0100] rev 1438
synchronised with main hg-repository; used add_typedef_global in nominal_atoms
2010-03-14 localised the typedef in Attic (requires new Isabelle)
Christian Urban <urbanc@in.tum.de> [Sun, 14 Mar 2010 11:36:15 +0100] rev 1437
localised the typedef in Attic (requires new Isabelle)
2010-03-13 started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de> [Sat, 13 Mar 2010 13:49:15 +0100] rev 1436
started supp-fv proofs (is going to work)
2010-03-12 Even with pattern simplified to a single clause, the supp equation doesn't seem true.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 12 Mar 2010 17:42:31 +0100] rev 1435
Even with pattern simplified to a single clause, the supp equation doesn't seem true.
2010-03-12 Still don't know how to prove supp=fv for simplest Let...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 12 Mar 2010 12:42:35 +0100] rev 1434
Still don't know how to prove supp=fv for simplest Let...
2010-03-11 Do not fail if the finite support proof fails.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 20:49:31 +0100] rev 1433
Do not fail if the finite support proof fails.
2010-03-11 generalised the supp for atoms to all concrete atoms (not just names)
Christian Urban <urbanc@in.tum.de> [Thu, 11 Mar 2010 19:43:50 +0100] rev 1432
generalised the supp for atoms to all concrete atoms (not just names)
2010-03-11 support of atoms at the end of Abs.thy
Christian Urban <urbanc@in.tum.de> [Thu, 11 Mar 2010 19:41:11 +0100] rev 1431
support of atoms at the end of Abs.thy
2010-03-11 Trying to prove atom_image_fresh_swap
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 19:24:07 +0100] rev 1430
Trying to prove atom_image_fresh_swap
2010-03-11 Finite_support proof no longer needed in LF.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 17:49:07 +0100] rev 1429
Finite_support proof no longer needed in LF.
2010-03-11 Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 17:47:29 +0100] rev 1428
Show that the new types are in finite support typeclass.
2010-03-11 mk_supports_eq and supports_tac.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 16:50:44 +0100] rev 1427
mk_supports_eq and supports_tac.
2010-03-11 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 16:16:15 +0100] rev 1426
merge
2010-03-11 Fixes for term1 for new alpha. Still not able to show support equations.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 16:15:29 +0100] rev 1425
Fixes for term1 for new alpha. Still not able to show support equations.
2010-03-11 merged
Christian Urban <urbanc@in.tum.de> [Thu, 11 Mar 2010 16:12:15 +0100] rev 1424
merged
2010-03-11 finally the proof that new and old alpha agree
Christian Urban <urbanc@in.tum.de> [Thu, 11 Mar 2010 15:10:07 +0100] rev 1423
finally the proof that new and old alpha agree
2010-03-11 Remove "_raw" from lifted theorems.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 15:11:57 +0100] rev 1422
Remove "_raw" from lifted theorems.
2010-03-11 looking at trm5_equivp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 14:09:54 +0100] rev 1421
looking at trm5_equivp
2010-03-11 The cheats described explicitely.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 14:05:36 +0100] rev 1420
The cheats described explicitely.
2010-03-11 The alpha5_eqvt tactic works if I manage to build the goal.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 13:44:54 +0100] rev 1419
The alpha5_eqvt tactic works if I manage to build the goal.
2010-03-11 With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 13:34:45 +0100] rev 1418
With the 4 cheats, all examples fully lift.
2010-03-11 Lift alpha_bn_constants.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 12:30:53 +0100] rev 1417
Lift alpha_bn_constants.
2010-03-11 Lifting constants.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 12:26:24 +0100] rev 1416
Lifting constants.
2010-03-11 Proper error message.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:41:27 +0100] rev 1415
Proper error message.
2010-03-11 Lifting constants works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:32:37 +0100] rev 1414
Lifting constants works for all examples.
2010-03-11 Remove tracing from fv/alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:25:56 +0100] rev 1413
Remove tracing from fv/alpha.
2010-03-11 Equivp working only on the standard alpha-equivalences.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:25:18 +0100] rev 1412
Equivp working only on the standard alpha-equivalences.
2010-03-11 explicit cheat_fv_eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:20:50 +0100] rev 1411
explicit cheat_fv_eqvt
2010-03-11 extract build_eqvts_tac.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 11:15:14 +0100] rev 1410
extract build_eqvts_tac.
2010-03-11 build_eqvts no longer requires permutations.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:39:29 +0100] rev 1409
build_eqvts no longer requires permutations.
2010-03-11 Add explicit alpha_eqvt_cheat.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:22:24 +0100] rev 1408
Add explicit alpha_eqvt_cheat.
2010-03-11 Export tactic out of alpha_eqvt.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Mar 2010 10:10:23 +0100] rev 1407
Export tactic out of alpha_eqvt.
2010-03-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 16:59:08 +0100] rev 1406
merge
2010-03-10 More tries about the proofs in trm5
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 16:58:14 +0100] rev 1405
More tries about the proofs in trm5
2010-03-10 merged
Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 16:51:15 +0100] rev 1404
merged
2010-03-10 almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 16:50:42 +0100] rev 1403
almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
2010-03-10 alpha_equivp for trm5
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 15:40:15 +0100] rev 1402
alpha_equivp for trm5
2010-03-10 Undoing mistakenly committed parser experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 15:34:13 +0100] rev 1401
Undoing mistakenly committed parser experiments.
2010-03-10 alpha_eqvt for recursive term1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 15:32:51 +0100] rev 1400
alpha_eqvt for recursive term1.
2010-03-10 Looking at alpha_eqvt for term5, not much progress.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 14:47:04 +0100] rev 1399
Looking at alpha_eqvt for term5, not much progress.
2010-03-10 Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 14:24:27 +0100] rev 1398
Reordered examples in Test.
2010-03-10 Allows multiple bindings with same lhs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 13:29:12 +0100] rev 1397
Allows multiple bindings with same lhs.
2010-03-10 Linked parser to fv and alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 13:10:00 +0100] rev 1396
Linked parser to fv and alpha.
2010-03-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 12:53:44 +0100] rev 1395
merge
2010-03-10 A minor fix for shallow binders. LF works again.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 12:53:30 +0100] rev 1394
A minor fix for shallow binders. LF works again.
2010-03-10 merged
Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 12:48:55 +0100] rev 1393
merged
2010-03-10 parser produces ordered bn-fun information
Christian Urban <urbanc@in.tum.de> [Wed, 10 Mar 2010 12:48:38 +0100] rev 1392
parser produces ordered bn-fun information
2010-03-10 Testing equalities in trm5, all seems good.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 11:39:28 +0100] rev 1391
Testing equalities in trm5, all seems good.
2010-03-10 Fv&Alpha seem to work.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 11:19:59 +0100] rev 1390
Fv&Alpha seem to work.
2010-03-10 include alpha in the definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 10:47:21 +0100] rev 1389
include alpha in the definitions.
2010-03-10 Filled the algorithm for alpha_bn_arg
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 10:11:20 +0100] rev 1388
Filled the algorithm for alpha_bn_arg
2010-03-10 rhs of alpha_bn, and template for the arguments.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:58:43 +0100] rev 1387
rhs of alpha_bn, and template for the arguments.
2010-03-10 alpha_bn_constr template
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:45:38 +0100] rev 1386
alpha_bn_constr template
2010-03-10 exported template for alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:36:07 +0100] rev 1385
exported template for alpha_bn
2010-03-10 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:10:11 +0100] rev 1384
merge
2010-03-10 Use alpha_bns in normal alpha defs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 09:09:52 +0100] rev 1383
Use alpha_bns in normal alpha defs.
2010-03-10 alpha_bn_frees
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Mar 2010 08:44:19 +0100] rev 1382
alpha_bn_frees
2010-03-09 merged
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 22:10:10 +0100] rev 1381
merged
2010-03-09 added bn-information, but it is not yet ordered according to the dts
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 22:08:38 +0100] rev 1380
added bn-information, but it is not yet ordered according to the dts
2010-03-09 Separate lists for separate constructors, to match bn_eqs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 21:22:22 +0100] rev 1379
Separate lists for separate constructors, to match bn_eqs.
2010-03-09 All examples should work.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 17:25:35 +0100] rev 1378
All examples should work.
2010-03-09 Fix to get old alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 17:02:29 +0100] rev 1377
Fix to get old alpha.
2010-03-09 Separate primrecs in Fv.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 16:57:51 +0100] rev 1376
Separate primrecs in Fv.
2010-03-09 A version of Fv that takes into account recursive and non-recursive bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 16:24:39 +0100] rev 1375
A version of Fv that takes into account recursive and non-recursive bindings.
2010-03-09 Trying to prove that old alpha is the same as new recursive one. Lets still to do.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 11:36:40 +0100] rev 1374
Trying to prove that old alpha is the same as new recursive one. Lets still to do.
2010-03-09 fv_bi and alpha_bi
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 11:06:57 +0100] rev 1373
fv_bi and alpha_bi
2010-03-09 merged
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 09:55:19 +0100] rev 1372
merged
2010-03-09 added first test about new compat
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 09:54:58 +0100] rev 1371
added first test about new compat
2010-03-09 fv_compat
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 09 Mar 2010 09:38:49 +0100] rev 1370
fv_compat
2010-03-09 added another compat example
Christian Urban <urbanc@in.tum.de> [Tue, 09 Mar 2010 08:46:55 +0100] rev 1369
added another compat example
2010-03-08 added a test-file for compatibility
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 20:18:27 +0100] rev 1368
added a test-file for compatibility
2010-03-08 added compat definitions to some examples
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 16:11:42 +0100] rev 1367
added compat definitions to some examples
2010-03-08 Proper recognition of atoms and atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 15:28:25 +0100] rev 1366
Proper recognition of atoms and atom sets.
2010-03-08 deleted comments about "weird"
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 15:06:14 +0100] rev 1365
deleted comments about "weird"
2010-03-08 merged
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 15:01:26 +0100] rev 1364
merged
2010-03-08 updated to new Isabelle
Christian Urban <urbanc@in.tum.de> [Mon, 08 Mar 2010 15:01:01 +0100] rev 1363
updated to new Isabelle
2010-03-08 Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 14:31:04 +0100] rev 1362
Term5 written as nominal_datatype is the recursive let.
2010-03-08 With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 11:25:57 +0100] rev 1361
With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
2010-03-08 More fine-grained nominal restriction for debugging.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 11:12:15 +0100] rev 1360
More fine-grained nominal restriction for debugging.
2010-03-08 Fix permutation addition.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 11:10:43 +0100] rev 1359
Fix permutation addition.
2010-03-08 Update the comments
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 10:33:55 +0100] rev 1358
Update the comments
2010-03-08 Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 10:08:31 +0100] rev 1357
Gather bindings with same binder, and generate only one permutation for them.
2010-03-08 Undo effects of simp.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 02:40:16 +0100] rev 1356
Undo effects of simp.
2010-03-07 merged
Christian Urban <urbanc@in.tum.de> [Sun, 07 Mar 2010 21:30:57 +0100] rev 1355
merged
2010-03-07 updated to renamings in Isabelle
Christian Urban <urbanc@in.tum.de> [Sun, 07 Mar 2010 21:30:12 +0100] rev 1354
updated to renamings in Isabelle
2010-03-04 merged
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:56:58 +0100] rev 1353
merged
2010-03-04 merged
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:31:34 +0100] rev 1352
merged
2010-03-04 more proofs in Abs and work on Core Haskell
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:31:21 +0100] rev 1351
more proofs in Abs and work on Core Haskell
2010-03-03 added a lemma that permutations can be represented as sums of swapping
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 19:10:40 +0100] rev 1350
added a lemma that permutations can be represented as sums of swapping
2010-03-05 Still unable to show supp=fv for let with one existential.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 18:14:04 +0100] rev 1349
Still unable to show supp=fv for let with one existential.
2010-03-05 Ported LF to the parser interface.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 17:09:48 +0100] rev 1348
Ported LF to the parser interface.
2010-03-05 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 14:56:19 +0100] rev 1347
merge
2010-03-05 Lift fv and bn eqvts; no need to lift alpha_eqvt.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 14:55:21 +0100] rev 1346
Lift fv and bn eqvts; no need to lift alpha_eqvt.
2010-03-05 Not much progress about the single existential let case.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 13:04:47 +0100] rev 1345
Not much progress about the single existential let case.
2010-03-05 Fixed LF for one quantifier over 2 premises.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 10:23:40 +0100] rev 1344
Fixed LF for one quantifier over 2 premises.
2010-03-05 Trying to fix the proofs for the single existential... So far failed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 09:41:22 +0100] rev 1343
Trying to fix the proofs for the single existential... So far failed.
2010-03-04 Lift distinct.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 18:57:23 +0100] rev 1342
Lift distinct.
2010-03-04 Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 15:55:53 +0100] rev 1341
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
2010-03-04 Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 15:15:44 +0100] rev 1340
Lift BV,FV,Permutations and injection :).
2010-03-04 Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 12:00:11 +0100] rev 1339
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
2010-03-04 A version that just leaves the supp/\supp goal. Obviously not true.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 11:16:36 +0100] rev 1338
A version that just leaves the supp/\supp goal. Obviously not true.
2010-03-04 Prove symp and transp of weird without the supp /\ supp = {} assumption.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 10:59:52 +0100] rev 1337
Prove symp and transp of weird without the supp /\ supp = {} assumption.
2010-03-03 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:51:47 +0100] rev 1336
merge
2010-03-03 Experiments with proving weird transp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:49:34 +0100] rev 1335
Experiments with proving weird transp
2010-03-03 Code for solving symp goals with multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:47:29 +0100] rev 1334
Code for solving symp goals with multiple existentials.
(0) -1000 -240 +240 +1000 tip