| c486697 | Andrej Dudenhefner | 05 September 2022, 15:18:06 UTC | Merge pull request #167 from mrhaandi/string-notation removed a universe inconsistency | 05 September 2022, 15:18:06 UTC |
| 347d1ef | Andrej Dudenhefner | 05 September 2022, 13:55:41 UTC | removed several universe inconsistencies | 05 September 2022, 14:40:41 UTC |
| b70cfa1 | Andrej Dudenhefner | 02 September 2022, 14:22:49 UTC | Merge pull request #163 from mrhaandi/rev-FRACTRAN Added decider for reversible FRACTRAN halting | 02 September 2022, 14:22:49 UTC |
| 0c3312d | Andrej Dudenhefner | 02 September 2022, 13:03:41 UTC | considered review comments by @DmxLarchey | 02 September 2022, 13:03:41 UTC |
| 6207468 | Andrej Dudenhefner | 01 September 2022, 08:30:14 UTC | Merge pull request #164 from mrhaandi/author-typo fixed typo | 01 September 2022, 08:30:14 UTC |
| 4bcee01 | Andrej Dudenhefner | 01 September 2022, 07:52:43 UTC | added decider for reversible FRACTRAN halting Co-authored-by: Hizbullah Abdul Aziz Jabbar <archbung@gmail.com> | 01 September 2022, 07:52:43 UTC |
| 805bd27 | Andrej Dudenhefner | 01 September 2022, 07:30:07 UTC | fixed typo "Aut[h]or(s)" | 01 September 2022, 07:30:07 UTC |
| 3868c9a | Yannick Forster | 27 July 2022, 14:14:00 UTC | Merge pull request #155 from yforster/equivalence_proofs | 27 July 2022, 14:14:00 UTC |
| 759c992 | Yannick Forster | 27 July 2022, 14:04:05 UTC | Update README.md and opam | 27 July 2022, 14:12:37 UTC |
| 3850561 | Yannick Forster | 27 July 2022, 10:13:48 UTC | rename Utils -> Util | 27 July 2022, 10:14:17 UTC |
| d8669c6 | Andrej Dudenhefner | 26 July 2022, 15:25:40 UTC | fixed vec universe inconsintency (#2) | 26 July 2022, 15:25:40 UTC |
| b1df922 | Yannick Forster | 26 July 2022, 12:59:07 UTC | Merge remote-tracking branch 'origin/coq-8.15' into equivalence_proofs | 26 July 2022, 12:59:07 UTC |
| 84e17ca | Yannick Forster | 26 July 2022, 12:57:39 UTC | Set Default Goal Selector "!" | 26 July 2022, 12:57:39 UTC |
| d4bb4ba | Yannick Forster | 06 July 2022, 10:59:23 UTC | Relax opam file to also allow Coq 8.15.2 (#159) | 06 July 2022, 10:59:23 UTC |
| cc35e6c | Yannick Forster | 06 July 2022, 08:58:27 UTC | Use MetaCoq 1.0 and run vos compilation as fast-failing target before vo, no vok anymore | 06 July 2022, 08:58:27 UTC |
| b1df4f6 | Yannick Forster | 05 July 2022, 09:35:41 UTC | CoqProject | 05 July 2022, 10:44:48 UTC |
| 12b0af7 | Yannick Forster | 05 July 2022, 08:34:48 UTC | file with all equivalence proofs | 05 July 2022, 08:34:48 UTC |
| ca00b4b | Yannick Forster | 05 July 2022, 08:12:26 UTC | move computable definitions to toplevel files | 05 July 2022, 08:20:38 UTC |
| a92b124 | Yannick Forster | 04 July 2022, 16:44:55 UTC | fix warnings | 04 July 2022, 16:44:55 UTC |
| 9aa6e16 | Yannick Forster | 04 July 2022, 16:31:27 UTC | Prepare to use MetaCoq 1.0 release (#156) | 04 July 2022, 16:31:27 UTC |
| 7879723 | Yannick Forster | 04 July 2022, 16:14:15 UTC | TM_computable -> BSM_computable | 04 July 2022, 16:26:42 UTC |
| 50e7e9b | Dominique Larchey-Wendling | 04 July 2022, 12:19:31 UTC | updated the proof of bsm_mm_compiler_strong to use for the new compiler_t structure | 04 July 2022, 12:19:31 UTC |
| 3ca9f89 | Yannick Forster | 04 July 2022, 10:17:01 UTC | fixes with fabian | 04 July 2022, 10:17:01 UTC |
| aad76fd | Yannick Forster | 04 July 2022, 09:11:19 UTC | Remove commented code | 04 July 2022, 09:11:19 UTC |
| edfe04e | Yannick Forster | 03 July 2022, 11:20:03 UTC | Merge branch 'forthethesis' into prepare-metacoq-opam | 04 July 2022, 09:09:31 UTC |
| 3039a4b | Yannick Forster | 03 July 2022, 10:29:22 UTC | Prepare to use MetaCoq 1.0 release | 03 July 2022, 10:39:52 UTC |
| 88849f1 | Andrej Dudenhefner | 02 July 2022, 11:51:33 UTC | Merge pull request #154 from mrhaandi/faster-HOU Faster HOU | 02 July 2022, 11:51:33 UTC |
| 41c1311 | Andrej Dudenhefner | 02 July 2022, 10:10:08 UTC | improved goal and side effect management | 02 July 2022, 10:54:09 UTC |
| e209965 | Andrej Dudenhefner | 02 July 2022, 10:28:33 UTC | improved import management | 02 July 2022, 10:28:33 UTC |
| eb7ec29 | Andrej Dudenhefner | 29 June 2022, 11:53:43 UTC | Merge pull request #153 from fakusb/complexity-8.15 Tweaks for use in the complexity library | 29 June 2022, 11:53:43 UTC |
| e3c69ac | Dominique Larchey-Wendling | 17 June 2022, 09:19:54 UTC | Merge pull request #144 from DmxLarchey/sbtm2_dlw SBTM to PCTM to BSM2 to MMA3 to MMA2 reductions and compilers cleanups | 17 June 2022, 09:19:54 UTC |
| 40e2ce3 | Dominique Larchey-Wendling | 17 June 2022, 08:50:51 UTC | RM | 17 June 2022, 08:50:51 UTC |
| 488918a | Dominique Larchey-Wendling | 17 June 2022, 08:49:38 UTC | documentation | 17 June 2022, 08:49:38 UTC |
| 2fc9259 | Dominique Larchey-Wendling | 16 June 2022, 14:02:42 UTC | Replaced Let ... Qed with Local Fact ... Qed. | 16 June 2022, 14:02:42 UTC |
| 68cc2cb | Dominique Larchey-Wendling | 16 June 2022, 13:47:47 UTC | - implemented a direct reduction BSM(n) to MMA(1+n) - remove the superfluous MMA(4) to MMA(2) reduction - implemented the reduction chain SBTM < PCTM < BSM(2) < MMA(3) < MMA(2) for the halting problems. | 16 June 2022, 13:47:47 UTC |
| 04bd734 | Dominique Larchey-Wendling | 16 June 2022, 10:56:32 UTC | starting a direct BSM(n) to MMA(1+n) compiler (remember that for MM, this was a BSM(n) to MM(2+n) compiler !!) | 16 June 2022, 10:56:32 UTC |
| 4c06ca8 | Dominique Larchey-Wendling | 15 June 2022, 15:54:25 UTC | move godel_coding.v where it more likely belongs, nearby gcd.v and prime.v removed the dependency on the FRACTRAN code which was only for two small lemmas which now belong to prime.v | 15 June 2022, 15:54:25 UTC |
| 9a499d6 | Fabian Kunze | 12 February 2021, 13:42:12 UTC | worked on compiler runtimes | 15 June 2022, 13:43:27 UTC |
| 93a2238 | Fabian Kunze | 11 February 2021, 13:25:13 UTC | updated uptoc | 15 June 2022, 13:43:27 UTC |
| c4ac1ae | Fabian Kunze | 10 February 2021, 15:26:07 UTC | -added analysis for TM Rev -Added subterm property | 15 June 2022, 13:43:24 UTC |
| 04a5958 | Fabian Kunze | 15 December 2020, 09:50:28 UTC | small tweaks for complexity library | 15 June 2022, 13:26:20 UTC |
| 72f7b50 | Fabian Kunze | 27 November 2020, 13:17:39 UTC | -seperated injectivity constrain from encodable into own class -combined registered and encodable typeclass into one, which has way better cbn-behaviour now | 15 June 2022, 13:26:17 UTC |
| 09463c1 | Dominique Larchey-Wendling | 14 June 2022, 13:34:50 UTC | Fixes related to review by @mrhaandi | 14 June 2022, 13:34:50 UTC |
| 38d220b | Dominique Larchey-Wendling | 14 June 2022, 13:10:15 UTC | fixed issues related to proof terms defined by Let. | 14 June 2022, 13:10:15 UTC |
| 0afe51a | Dominique Larchey-Wendling | 14 June 2022, 13:01:37 UTC | Abstracted away godel_coding through a Record type and then factored the MMA(3+n) to MMA(2+n) compiler into a MMA(k+n) to MMA (2+n) compiler, requiring a godel_coding : vec nat k -> nat. Generated: - godel_coding : vec 3 nat -> nat - godel_coding : vec 4 nat -> nat We trivially derive - MMA(3+n) to MMA(2+n) - MMA(4) to MMA(2) compilers as direct instances. | 14 June 2022, 13:01:37 UTC |
| 71ad9a3 | Dominique Larchey-Wendling | 13 June 2022, 20:19:47 UTC | Clean the "Proof using." issues | 13 June 2022, 20:19:47 UTC |
| 15c5d0b | Dominique Larchey-Wendling | 12 June 2022, 06:06:18 UTC | Merge branch 'coq-8.15' into sbtm2_dlw | 12 June 2022, 06:06:18 UTC |
| 300a653 | Dominique Larchey-Wendling | 12 June 2022, 05:59:26 UTC | some cleanup of the code + comments about usage of the generic compiler | 12 June 2022, 05:59:26 UTC |
| a6c6c1f | Dominique Larchey-Wendling | 11 June 2022, 12:02:19 UTC | added the reduction MMA_HALT(3+n) to MMA_HALT(2+n) | 11 June 2022, 12:02:19 UTC |
| 574817d | Dominique Larchey-Wendling | 11 June 2022, 11:40:02 UTC | Merge pull request #140 from DmxLarchey/typo_impact_naming_schemes Typo in the definition file PCP.v impacts naming schemes | 11 June 2022, 11:40:02 UTC |
| be3fccf | Dominique Larchey-Wendling | 10 June 2022, 14:04:26 UTC | a compiler from MMA3 to MMA2 using Gödel coding of first three registers into REG1. REG0 is used as a spare/0 register | 10 June 2022, 14:04:26 UTC |
| c05906c | Dominique Larchey-Wendling | 10 June 2022, 07:35:12 UTC | Merge branch 'coq-8.15' into test_merge | 10 June 2022, 07:35:12 UTC |
| 2a22342 | Dominique Larchey-Wendling | 10 June 2022, 07:33:19 UTC | combi_235 | 10 June 2022, 07:33:19 UTC |
| 7aabc5c | Dominique Larchey-Wendling | 09 June 2022, 13:14:00 UTC | hypotheses were not needed !!! | 09 June 2022, 13:14:00 UTC |
| 9e91e5d | Dominique Larchey-Wendling | 09 June 2022, 13:03:24 UTC | still soundness hypothesis (instr_compiler_sound) should not appear in the soundness of the compiler ??? | 09 June 2022, 13:03:24 UTC |
| 74548e2 | Dominique Larchey-Wendling | 09 June 2022, 12:50:32 UTC | Merge branch 'coq-8.15' into test_merge still needs so cleanup | 09 June 2022, 12:50:32 UTC |
| c99e8fa | Andrej Dudenhefner | 09 June 2022, 11:19:16 UTC | Merge pull request #149 from mrhaandi/faster-vos global Set Default Proof Using "Type" | 09 June 2022, 11:19:16 UTC |
| 0c71c9d | Andrej Dudenhefner | 09 June 2022, 07:38:25 UTC | moved ReductionChainNotations to ReducibilityFacts | 09 June 2022, 07:38:25 UTC |
| 66bf4f4 | Andrej Dudenhefner | 07 June 2022, 14:01:40 UTC | changed -arg in _CoqProject to support Proof General | 07 June 2022, 14:01:40 UTC |
| 2e66df2 | Andrej Dudenhefner | 31 May 2022, 08:22:55 UTC | global Set Default Proof Using "Type" removed individual Default Proof Using refactored ReducibilityFacts for minimal dependencies | 07 June 2022, 08:30:13 UTC |
| 79b95c9 | Andrej Dudenhefner | 07 June 2022, 08:07:32 UTC | Merge pull request #151 from mrhaandi/undec-leaves Intermediate files not require _undec files | 07 June 2022, 08:07:32 UTC |
| a39d143 | Andrej Dudenhefner | 04 June 2022, 19:51:06 UTC | fix for lia (weaker in 8.15.1) | 04 June 2022, 19:51:06 UTC |
| 25f8d98 | Andrej Dudenhefner | 04 June 2022, 11:47:48 UTC | established that intermediate files do not depend on _undec files do not unnecessarily Require Synthetic.Undecidability | 04 June 2022, 12:26:25 UTC |
| 672b6a7 | Andrej Dudenhefner | 24 May 2022, 11:10:48 UTC | Merge pull request #145 from mrhaandi/lambda-mm HaltL <= MMA_HALTING 5 ⪯ HaltTM 5 (natural and fast) | 24 May 2022, 11:10:48 UTC |
| f6095ee | Andrej Dudenhefner | 24 May 2022, 10:40:54 UTC | fix README.md | 24 May 2022, 10:40:54 UTC |
| 7d8643a | Andrej Dudenhefner | 24 May 2022, 08:13:11 UTC | added HaltL ⪯ HaltTM 5 | 24 May 2022, 08:13:11 UTC |
| 7d8c12d | Andrej Dudenhefner | 24 May 2022, 07:43:41 UTC | added MMA_HALTING n ⪯ HaltTM n | 24 May 2022, 07:45:39 UTC |
| da54451 | Andrej Dudenhefner | 13 April 2022, 10:30:30 UTC | simplified wCBN inverse_simulation simplified KrivineMclosed_HALT_to_MMA_HALTING simplified vec_change_comm proof | 24 May 2022, 07:45:38 UTC |
| 23bc15a | Andrej Dudenhefner | 13 April 2022, 10:22:29 UTC | strengthen sss_terminates_ind | 24 May 2022, 07:44:14 UTC |
| 7e60908 | Andrej Dudenhefner | 12 April 2022, 10:20:23 UTC | removed duplicate file | 24 May 2022, 07:44:14 UTC |
| 46873f0 | Andrej Dudenhefner | 15 March 2022, 15:29:43 UTC | simplifications | 24 May 2022, 07:44:13 UTC |
| 28ea594 | Andrej Dudenhefner | 15 March 2022, 13:20:58 UTC | updated README.md | 24 May 2022, 07:44:13 UTC |
| 449b287 | Andrej Dudenhefner | 11 March 2022, 14:02:50 UTC | factored out HaltL <= HaltLclosed from L_to_mTM | 24 May 2022, 07:44:13 UTC |
| cc71b5a | Andrej Dudenhefner | 11 March 2022, 11:53:00 UTC | added KrivineMclosed_HALT <= (@MMA_HALTING 5) | 24 May 2022, 07:44:12 UTC |
| 377674d | Andrej Dudenhefner | 11 March 2022, 11:42:57 UTC | added Krivine machine halting (KrivineM_HALT) | 24 May 2022, 07:44:12 UTC |
| b650c44 | Andrej Dudenhefner | 11 March 2022, 11:37:21 UTC | added weak call-by-name leftmost outermost normalization (wCBN) | 24 May 2022, 07:44:11 UTC |
| f9c03a0 | Andrej Dudenhefner | 16 May 2022, 13:35:49 UTC | Merge pull request #147 from mrhaandi/FMsetC_cleanup cleaned up proofs in SetConstraints | 16 May 2022, 13:35:49 UTC |
| 9136f46 | Andrej Dudenhefner | 03 May 2022, 15:24:44 UTC | cleaned up HSCFacts.v, FMsetC_SAT_to_LPolyNC_SAT.v, and proofs in SetConstraints removed obsolete files | 09 May 2022, 12:59:24 UTC |
| 7cd9197 | Dominique Larchey-Wendling | 12 April 2022, 13:17:51 UTC | Merge branch 'uds-psl:coq-8.15' into sbtm2_dlw | 12 April 2022, 13:17:51 UTC |
| 5a6d81e | Dominique Larchey-Wendling | 12 April 2022, 13:14:04 UTC | Merge pull request #143 from mrhaandi/sbtm2 Simple Binary Turing Machines (2) RFC | 12 April 2022, 13:14:04 UTC |
| c9da1b7 | Dominique Larchey-Wendling | 21 February 2022, 11:56:09 UTC | replaced JZ/JMP with the single BR(anch) instruction in PCTMs | 21 February 2022, 11:56:09 UTC |
| fa94a18 | Dominique Larchey-Wendling | 21 February 2022, 11:24:08 UTC | Merge branch 'sbtm2_dlw' of github.com:DmxLarchey/coq-library-undecidability into sbtm2_dlw | 21 February 2022, 11:24:08 UTC |
| 83c0604 | Dominique Larchey-Wendling | 20 February 2022, 21:16:44 UTC | added make targets: gitclean findclean mrproper | 20 February 2022, 21:16:44 UTC |
| 5dcc99b | Dominique Larchey-Wendling | 20 February 2022, 18:30:09 UTC | cleanup of the compiler + mma -> mma0 simulator | 20 February 2022, 18:30:09 UTC |
| 83ab151 | Dominique Larchey-Wendling | 20 February 2022, 13:21:56 UTC | added reduction chain SBTM < PCTM < BSM2 reworked generic compiler with a cleanup and the BSM to MM simulator is much shorter now | 20 February 2022, 13:21:56 UTC |
| f22fdec | Dominique Larchey-Wendling | 19 February 2022, 21:57:57 UTC | restruring arround compiler_t type | 19 February 2022, 21:57:57 UTC |
| e264624 | Dominique Larchey-Wendling | 19 February 2022, 11:53:21 UTC | reduction PCTM < BSM2 via a compiler | 19 February 2022, 11:53:21 UTC |
| a2a86b1 | Dominique Larchey-Wendling | 18 February 2022, 16:52:36 UTC | restructured sbtm2pctm | 18 February 2022, 16:52:36 UTC |
| 983a05f | Dominique Larchey-Wendling | 18 February 2022, 16:04:14 UTC | PC based Turing machines with a single tape (identical to the SBTM tape) and reduction from SBTM | 18 February 2022, 16:04:14 UTC |
| 73afc87 | Dominique Larchey-Wendling | 18 February 2022, 11:25:04 UTC | Merge branch 'sbtm2' into sbtm2_dlw | 18 February 2022, 11:25:04 UTC |
| a2711ba | Dominique Larchey-Wendling | 18 February 2022, 11:24:05 UTC | make superclean target | 18 February 2022, 11:24:05 UTC |
| c9ad5d4 | Dominique Larchey-Wendling | 18 February 2022, 10:55:15 UTC | Merge branch 'sbtm2' into sbtm2_dlw | 18 February 2022, 10:55:15 UTC |
| 3c27f45 | Andrej Dudenhefner | 18 February 2022, 08:39:46 UTC | updated readme | 18 February 2022, 08:39:46 UTC |
| e3149e1 | Andrej Dudenhefner | 18 February 2022, 08:36:01 UTC | updated documentation | 18 February 2022, 08:36:01 UTC |
| 016f5ad | Dominique Larchey-Wendling | 17 February 2022, 16:22:57 UTC | Merge branch 'sbtm2' into sbtm2_dlw | 17 February 2022, 16:22:57 UTC |
| 0504937 | Dominique Larchey-Wendling | 17 February 2022, 16:16:01 UTC | * correction for BPCP_SigBPCP.v. An exist was missing its first argument (now explicit ?) * correction for TRAKHTENBROT_to_FSAT.v. now intuition fails to solve easy goal ... add try firstorder also an equation was reversed?? removed symmetry | 17 February 2022, 16:16:01 UTC |
| 433f250 | Dominique Larchey-Wendling | 17 February 2022, 16:09:14 UTC | proved the step simulation of SBTM by BSM | 17 February 2022, 16:09:14 UTC |
| 1de2f3f | Andrej Dudenhefner | 17 February 2022, 16:02:38 UTC | tried to make SBTM_HALT the default seed (bugs) | 17 February 2022, 16:02:38 UTC |
| 956133c | Andrej Dudenhefner | 17 February 2022, 15:29:23 UTC | added SBTM_enum removes ssrfun.obind reference | 17 February 2022, 15:29:23 UTC |
| 1f0795b | Andrej Dudenhefner | 17 February 2022, 14:36:35 UTC | added enumerators for SBTM added SBTM_HALT complement consideration | 17 February 2022, 14:36:35 UTC |
