| aed0a05 | Dominique Larchey-Wendling | 11 April 2020, 20:44:34 UTC | informative and non-informative reductions | 11 April 2020, 20:44:34 UTC |
| 237ea69 | Dominique Larchey-Wendling | 11 April 2020, 20:18:10 UTC | merging Problems/*.v and Shared/Prelims.v for the Trakhtenbrot devel | 11 April 2020, 20:18:10 UTC |
| 29b03ef | Dominique Larchey-Wendling | 11 April 2020, 20:10:02 UTC | Merge pull request #8 from DmxLarchey/ij1 Merge libs from trakhtenbrot | 11 April 2020, 20:10:02 UTC |
| 13c9b20 | Dominique Larchey-Wendling | 11 April 2020, 20:03:21 UTC | removed one cutrewrite | 11 April 2020, 20:03:21 UTC |
| 3b184e1 | Dominique Larchey-Wendling | 11 April 2020, 19:53:18 UTC | reverted orig libs | 11 April 2020, 19:53:18 UTC |
| 109cbb7 | Dominique Larchey-Wendling | 11 April 2020, 19:44:16 UTC | Revert "Delete vec.v" This reverts commit 1991a25ab6b82f256292db63ce90100454f212c7. | 11 April 2020, 19:44:16 UTC |
| 1991a25 | Dominique Larchey-Wendling | 11 April 2020, 19:38:32 UTC | Delete vec.v | 11 April 2020, 19:38:32 UTC |
| 6cbf46e | Dominique Larchey-Wendling | 11 April 2020, 19:29:10 UTC | to compare with the IJCAR lib | 11 April 2020, 19:29:10 UTC |
| 645aeb1 | Dominique Larchey-Wendling | 11 April 2020, 19:02:34 UTC | removed warnings | 11 April 2020, 19:02:34 UTC |
| ec2650d | Dominique Larchey-Wendling | 11 April 2020, 09:14:19 UTC | Merge pull request #5 from DmxLarchey/libs_update Libs update | 11 April 2020, 09:14:19 UTC |
| 12848be | Yannick Forster | 09 April 2020, 14:47:13 UTC | Update README.md | 09 April 2020, 14:47:13 UTC |
| 4a55a78 | Yannick Forster | 09 April 2020, 14:35:58 UTC | Update README.md | 09 April 2020, 14:35:58 UTC |
| 009c1ca | Yannick Forster | 06 April 2020, 13:38:25 UTC | Merge pull request #39 from mrhaandi/coq-8.11 PCP refactoring into PCP, SR, GFG | 06 April 2020, 13:38:25 UTC |
| 1ad3985 | mrhaandi | 31 March 2020, 15:29:53 UTC | removed outdated readme | 31 March 2020, 15:29:53 UTC |
| 1c7c739 | mrhaandi | 31 March 2020, 15:15:51 UTC | refactored PCP into PCP, SR, CFG removed Shared.Prelim from Problems.Reduction | 31 March 2020, 15:15:51 UTC |
| 825008f | Yannick Forster | 25 March 2020, 16:54:59 UTC | Update deps in opam file | 25 March 2020, 16:54:59 UTC |
| 8308954 | Yannick Forster | 25 March 2020, 16:53:22 UTC | remove a warning | 25 March 2020, 16:53:22 UTC |
| 0c0d47a | Yannick Forster | 25 March 2020, 16:26:36 UTC | Update travis | 25 March 2020, 16:26:36 UTC |
| 9fc277e | Yannick Forster | 25 March 2020, 16:24:32 UTC | port to 8.11 | 25 March 2020, 16:24:32 UTC |
| b9b3834 | Yannick Forster | 25 March 2020, 09:58:11 UTC | Fig global make targets | 25 March 2020, 09:58:11 UTC |
| b53b214 | Yannick Forster | 25 March 2020, 09:12:40 UTC | Fix travis file | 25 March 2020, 09:12:40 UTC |
| 137a367 | Yannick Forster | 25 March 2020, 08:33:29 UTC | Update README and opam file | 25 March 2020, 08:33:29 UTC |
| bef647d | Yannick Forster | 25 March 2020, 08:28:24 UTC | Update README | 25 March 2020, 08:28:24 UTC |
| 0de7d1c | Yannick Forster | 25 March 2020, 08:24:04 UTC | Fix versions in opam file | 25 March 2020, 08:24:04 UTC |
| ed09bee | Yannick Forster | 25 March 2020, 08:20:05 UTC | Removed submodules and updated opam file | 25 March 2020, 08:20:51 UTC |
| ed4ff57 | Yannick Forster | 24 March 2020, 18:14:33 UTC | Everything compiles under 8.10 | 24 March 2020, 18:14:33 UTC |
| 4481aea | Yannick Forster | 24 March 2020, 17:31:11 UTC | More changes for 8.10 | 24 March 2020, 17:31:11 UTC |
| 4c22f3d | Fabian Kunze | 24 March 2020, 16:14:55 UTC | Fixed bug bu changing undocumented tactical to another one | 24 March 2020, 16:14:55 UTC |
| c89ffe5 | Yannick Forster | 24 March 2020, 15:24:07 UTC | first steps in porting to 8.10 | 24 March 2020, 15:24:07 UTC |
| 0abe97a | Dominique Larchey-Wendling | 05 March 2020, 15:45:27 UTC | Merge pull request #37 from DmxLarchey/lmcs_ups changed name of lemma | 05 March 2020, 15:45:27 UTC |
| 599cb58 | Dominique Larchey-Wendling | 05 March 2020, 15:15:37 UTC | changed name of lemma | 05 March 2020, 15:15:37 UTC |
| 6bb9129 | Yannick Forster | 05 March 2020, 14:59:16 UTC | Merge pull request #36 from DmxLarchey/lmcs_ups Updates for the LMCS submission | 05 March 2020, 14:59:16 UTC |
| d80d1a8 | Dominique Larchey-Wendling | 05 March 2020, 12:54:14 UTC | Removed dependency on Equations for inverting vec and pos dependent types. Possibly inversion lemma for ra_ca_c should be properly laid out instead of hand hacking inversions on a per-need basis which clogs the code | 05 March 2020, 12:54:14 UTC |
| 57a48d0 | Dominique Larchey-Wendling | 05 March 2020, 10:30:39 UTC | changed the defs of H10 and H10Z to (pos n,pos 0) instead of (pos n,Empty_set) | 05 March 2020, 10:30:39 UTC |
| 1480669 | Dominique Larchey-Wendling | 04 March 2020, 14:43:25 UTC | Merge branch 'wip' into libs_update | 04 March 2020, 14:43:25 UTC |
| 462c3a4 | Yannick Forster | 04 March 2020, 08:47:33 UTC | Merge pull request #31 from uds-psl/more_dprm new version of the DPRM which shows all availalable equivalences | 04 March 2020, 08:47:33 UTC |
| 5c66f33 | Yannick Forster | 03 March 2020, 17:18:51 UTC | Merge pull request #33 from lgaeher/master Fix makefile and coqdoc compilation | 03 March 2020, 17:18:51 UTC |
| 28de3a4 | Yannick Forster | 03 March 2020, 17:18:20 UTC | Merge pull request #34 from DmxLarchey/cleanup_murec_compiler Cleanup murec compiler, faster compile | 03 March 2020, 17:18:20 UTC |
| 70f6378 | Yannick Forster | 03 March 2020, 17:17:56 UTC | Merge pull request #35 from yforster/remove_admits Remove all admits | 03 March 2020, 17:17:56 UTC |
| 83f7410 | Yannick Forster | 03 March 2020, 16:18:02 UTC | Remove admits | 03 March 2020, 16:19:37 UTC |
| ed1f939 | Yannick Forster | 03 March 2020, 10:40:12 UTC | remove axiom | 03 March 2020, 16:19:37 UTC |
| 19ba623 | Dominique Larchey-Wendling | 02 March 2020, 09:51:49 UTC | small updates | 02 March 2020, 09:51:49 UTC |
| 6a8aec1 | Dominique Larchey-Wendling | 01 March 2020, 23:14:18 UTC | changed Let in Local Definition in ra_mm_env. to avoid big environments than hinder the efficiency of the omega tactic | 01 March 2020, 23:14:18 UTC |
| ab9b33d | Lennard Gäher | 22 February 2020, 18:52:46 UTC | remove parse-comments flag from coqdoc as this breaks doc generation (seems to be a bug in coqdoc as 'unknown token' stuff should not happen according to its documentation?) | 22 February 2020, 18:52:46 UTC |
| d22f6f2 | Lennard Gäher | 22 February 2020, 18:50:55 UTC | fix makefile regression introduced by 6ddce394ca5bc2206f6e0e2bcecc0582e70fb6a3 | 22 February 2020, 18:50:55 UTC |
| 466d429 | Lennard Gäher | 22 February 2020, 18:03:30 UTC | fix html target in makefile | 22 February 2020, 18:03:30 UTC |
| d553555 | Dominique Larchey-Wendling | 14 February 2020, 20:56:02 UTC | reverted to vec_list_In | 14 February 2020, 20:56:02 UTC |
| 278820c | Dominique Larchey-Wendling | 14 February 2020, 18:02:20 UTC | more cleanup | 14 February 2020, 18:02:20 UTC |
| a96230d | Dominique Larchey-Wendling | 14 February 2020, 17:53:19 UTC | finished cleanup and merge | 14 February 2020, 17:53:19 UTC |
| 93972dc | Dominique Larchey-Wendling | 14 February 2020, 14:27:28 UTC | the git checkout informative_lift Shared did import whole files and did not perform a proper merge !!! I now have to cleanup the mess | 14 February 2020, 14:27:28 UTC |
| 5a7d71a | Dominique Larchey-Wendling | 14 February 2020, 12:06:23 UTC | a prime testing procedure and nxtprime reflection tactic a discussion about the shape of possible and impossible fractran RE predicates | 14 February 2020, 12:06:23 UTC |
| f6d4c4b | Dominique Larchey-Wendling | 13 February 2020, 22:54:16 UTC | added DPRM for unary predicates including fractran | 13 February 2020, 22:54:16 UTC |
| 8a3ceb3 | Dominique Larchey-Wendling | 11 February 2020, 13:54:48 UTC | new version of the DPRM which shows equivalence between the computational models of MM, µrec and the different variants of Diohantineness | 11 February 2020, 13:54:48 UTC |
| aec2f58 | Dominique Larchey-Wendling | 07 February 2020, 14:16:36 UTC | Merge pull request #29 from yforster/H10Z Reduction from H10 to H10Z | 07 February 2020, 14:16:36 UTC |
| 605fa43 | Dominique Larchey-Wendling | 07 February 2020, 13:04:14 UTC | redefined H10Z as P(x1,...,xn) = 0%Z and removed dependency over Equations for depelim the pos lib already has inversion for pos (S n) as the tactic "invert pos p" some cleanup as well | 07 February 2020, 13:04:14 UTC |
| e0b41e6 | Yannick Forster | 07 February 2020, 11:38:47 UTC | Reduction from H10 to H10Z | 07 February 2020, 11:38:47 UTC |
| d552a7f | Yannick Forster | 06 February 2020, 17:42:03 UTC | Merge pull request #22 from uds-psl/better_bezout_extraction Construction of an H10C-universal µ-recursive function | 06 February 2020, 17:42:03 UTC |
| 468a538 | Dominique Larchey-Wendling | 06 February 2020, 14:55:18 UTC | Merge branch 'master' into better_bezout_extraction resync with updated master | 06 February 2020, 14:55:18 UTC |
| 9dddee6 | Yannick Forster | 06 February 2020, 13:25:32 UTC | Merge pull request #28 from yforster/mu_to_lambda Mu to lambda | 06 February 2020, 13:25:32 UTC |
| c10a31c | Yannick Forster | 06 February 2020, 09:04:54 UTC | Merge remote-tracking branch 'origin/master' into mu_to_lambda | 06 February 2020, 09:04:54 UTC |
| 98cecb0 | Yannick Forster | 06 February 2020, 09:03:04 UTC | Merge pull request #26 from DmxLarchey/h10_journal A fork for smoother reduction dio_form -> dio_elem | 06 February 2020, 09:03:04 UTC |
| 2ef5eeb | Yannick Forster | 05 February 2020, 16:41:58 UTC | Added reduction from mu_halting to lambda calculus | 05 February 2020, 16:41:58 UTC |
| 91a93c4 | Yannick Forster | 04 February 2020, 11:54:14 UTC | progress | 04 February 2020, 11:54:14 UTC |
| d575c85 | Yannick Forster | 04 February 2020, 10:01:36 UTC | first chunk on mu -> L | 04 February 2020, 10:01:36 UTC |
| 4ae7c7a | Dominique Larchey-Wendling | 31 January 2020, 21:45:56 UTC | some more remarks | 31 January 2020, 21:45:56 UTC |
| 1094251 | Dominique Larchey-Wendling | 31 January 2020, 21:38:52 UTC | reworked and cleanup of the proof of Lagrange for better explanations | 31 January 2020, 21:38:52 UTC |
| 9bd5607 | Dominique Larchey-Wendling | 30 January 2020, 17:05:41 UTC | Merge pull request #1 from DmxLarchey/lagrange Added Lagrange's theorem | 30 January 2020, 17:05:41 UTC |
| f03e863 | Dominique Larchey-Wendling | 30 January 2020, 16:00:08 UTC | finished the proof of Lagrange's theorem on the sum of 4 squares !!! | 30 January 2020, 16:00:08 UTC |
| 13d8cc8 | Dominique Larchey-Wendling | 30 January 2020, 12:13:25 UTC | nearly completed Lagrange's theorem ! | 30 January 2020, 12:13:25 UTC |
| 49fc9fe | Dominique Larchey-Wendling | 29 January 2020, 14:48:26 UTC | added the full statement of Luca's theorem | 29 January 2020, 14:48:26 UTC |
| f7e9adc | Dominique Larchey-Wendling | 12 December 2019, 12:13:34 UTC | some cleanup in dio_logic and dio_bounded mostly better comments | 12 December 2019, 12:13:34 UTC |
| eba1051 | Dominique Larchey-Wendling | 11 December 2019, 12:32:56 UTC | tracking duplications in encodings | 11 December 2019, 12:32:56 UTC |
| 8732580 | Dominique Larchey-Wendling | 11 December 2019, 12:18:13 UTC | starting to make optimisation with a less dramatic effect | 11 December 2019, 12:18:13 UTC |
| 55ee683 | Dominique Larchey-Wendling | 11 December 2019, 12:09:47 UTC | further optimisations of the encoding algo | 11 December 2019, 12:09:47 UTC |
| 0f138dc | Dominique Larchey-Wendling | 11 December 2019, 11:55:30 UTC | reintroduced x = y for smaller encodings | 11 December 2019, 11:55:30 UTC |
| 3639c3c | Dominique Larchey-Wendling | 11 December 2019, 08:28:27 UTC | some cleanup | 11 December 2019, 08:28:27 UTC |
| 46b3729 | Dominique Larchey-Wendling | 11 December 2019, 08:13:30 UTC | improvement in the shapa analysis to produce shorter formulas | 11 December 2019, 08:13:30 UTC |
| 3594fa3 | Dominique Larchey-Wendling | 10 December 2019, 15:04:50 UTC | better notation for De Bruijn extensions wrt the paper | 10 December 2019, 15:04:50 UTC |
| fada11c | Dominique Larchey-Wendling | 10 December 2019, 13:17:10 UTC | a more systematic use of "dio by lemma" | 10 December 2019, 13:17:10 UTC |
| b816b09 | Dominique Larchey-Wendling | 10 December 2019, 13:08:59 UTC | some more comments | 10 December 2019, 13:08:59 UTC |
| c397f3e | Dominique Larchey-Wendling | 10 December 2019, 12:34:29 UTC | reworked the definitions dio_expr now becomes dio_fun which is much more acurate. It could be possible to rework the shape of the Diophantine characterization of alpha and expo to take dio_fun better into account ... | 10 December 2019, 12:34:29 UTC |
| 88e60c7 | Dominique Larchey-Wendling | 10 December 2019, 00:39:24 UTC | last cleanup for tonight | 10 December 2019, 00:39:24 UTC |
| 476e5f5 | Dominique Larchey-Wendling | 10 December 2019, 00:32:56 UTC | much more efficient and cleaner dio auto tactic the only problem is that the size of generate formula is increase at each cleaning changing atoms to elem simplified lost of proofs but got me much bigger encodings in the end ... it does really matter since efficiency is not the objective here | 10 December 2019, 00:32:56 UTC |
| 42b3c41 | Dominique Larchey-Wendling | 09 December 2019, 21:00:35 UTC | cleanup and replaced with dependent reduction ... maybe it would be good to move the definition of reduction_dependent from FRACTRAN_DIO.v to where is belongs ... somewhere in ILL.Definitions | 09 December 2019, 21:00:35 UTC |
| f386a03 | Dominique Larchey-Wendling | 09 December 2019, 15:16:50 UTC | started modifying dio_logic to simplify atoms to something close to dio_elem | 09 December 2019, 15:16:50 UTC |
| 5c8a306 | Dominique Larchey-Wendling | 05 November 2019, 08:55:04 UTC | completed the missing lemma about the godel_beta encoding of list of triples | 05 November 2019, 08:55:04 UTC |
| 0961c52 | Dominique Larchey-Wendling | 04 November 2019, 14:40:19 UTC | added a second universal MuRec based on the alternate constraints of Andrej Dudenhefner 1+x+y^2=z it is 1/4 of the size of the previous one thanks to a much lighter use of decomp_r (which a big MuRec) Unfinished is the fact that nat_h10luc_surj the encoding of list h10uc into nat is total not that hard but a bit tricky though because of the flat_map replacing (x,y,z) -> x##y##z##vec_nil | 04 November 2019, 14:40:19 UTC |
| d74c601 | Dominique Larchey-Wendling | 30 October 2019, 22:06:46 UTC | removed unneeded messages that were poluting the output of make | 30 October 2019, 22:06:46 UTC |
| 8c735b3 | Dominique Larchey-Wendling | 30 October 2019, 19:40:20 UTC | Merge branch 'master' into better_bezout_extraction | 30 October 2019, 19:40:20 UTC |
| 6ddce39 | Dominique Larchey-Wendling | 30 October 2019, 19:25:25 UTC | cleanup of the MM -> FRACTRAN_REG -> MMA2 reduction files remove some unneeded Check and Print Assumptions | 30 October 2019, 19:25:25 UTC |
| 50e31e6 | Dominique Larchey-Wendling | 30 October 2019, 17:40:18 UTC | removed .d files inherited from the CPP'19 developments | 30 October 2019, 17:40:18 UTC |
| 7750f3d | Dominique Larchey-Wendling | 29 October 2019, 23:43:21 UTC | Corrected for 8.8.2 and also cleanup of the mess arround FRACTRAN and MMA2 Now the reduction is MM -> FRACTRAN_REG -> MMA2 and FRACTRAN (non reg) halting could be removed but I also added the trivial FRACTRAN_REG -> FRACTRAN | 29 October 2019, 23:43:21 UTC |
| fc3ec56 | Dominique Larchey-Wendling | 29 October 2019, 20:18:32 UTC | large cleanup of the construction of the universal recalg | 29 October 2019, 20:18:32 UTC |
| ac854d0 | Yannick Forster | 29 October 2019, 11:04:00 UTC | Merge pull request #21 from uds-psl/murec A BIG commit containing the DIO_SINGLE -> µ-REC -> MM reductions | 29 October 2019, 11:04:00 UTC |
| 934f393 | Yannick Forster | 29 October 2019, 11:01:19 UTC | Merge pull request #18 from dominik-kirst/master Trakhtenbrot's theorem | 29 October 2019, 11:01:19 UTC |
| 992e9b1 | Dominique Larchey-Wendling | 28 October 2019, 22:07:51 UTC | added a universal µ-recursive algorithm of size 8708 and of arity 1 that can decide any H10C problem, hence its own termination problem must be undecidable | 28 October 2019, 22:07:51 UTC |
| f190272 | Dominique Larchey-Wendling | 27 October 2019, 11:27:28 UTC | updated gcd and extension of the CRT for preparation with Godel Beta encoding of lists of nats | 27 October 2019, 11:27:28 UTC |
| 3dc1281 | Dominique Larchey-Wendling | 25 October 2019, 21:35:48 UTC | A BIG commit containing the DIO_SINGLE -> µ-REC -> MM reductions The details are going to be comment in the PR Notice that to avoid having several definitions of MM, I needed to generalize the definition to an arbitrary type of registers of which we only use the instance nat and pos _ but this implies changing mm_instr n with mm_instr (pos n) at not so many but several places in the code the rest will be commented in the PR description | 25 October 2019, 21:35:48 UTC |
| 833b141 | Yannick Forster | 25 October 2019, 16:55:45 UTC | Delete .DS_Store | 25 October 2019, 16:55:45 UTC |
| 0aee30f | Yannick Forster | 25 October 2019, 15:28:32 UTC | Merge pull request #17 from uds-psl/induction_on_PR Fixing the induction-on mess | 25 October 2019, 15:28:32 UTC |
