JSON: {"tool":"check_kill","tool_version":4,"result":"PASS","exit":0,"file":"/home/dennis/projects/bb6-hunt/astra/decisions-20261016/w61/publication/Nonhalting.v","sha256":"cd0bfee325f897047164a4cc11325ca3e30d2acfadedf4c2abecec0a859327ca","tm":"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF","mode":"nonhalt","theorem":"nonhalt","framework_head":"0940bb9cf434ba68f0c025dabfde45a219999973","coqc":"/home/dennis/projects/bb6-hunt/astra/audit-coqc","coqc_version":"8.20.1","compile_seconds":113.08,"native_compiler":"yes","coqchk":"pass","coqchk_timeout":600,"coqchk_seconds":18.76,"ml_modules":["ltac_plugin.cmxs","number_string_notation_plugin.cmxs","tauto_plugin.cmxs","cc_plugin.cmxs","firstorder_plugin.cmxs","ring_plugin.cmxs","zify_plugin.cmxs","micromega_core_plugin.cmxs","micromega_plugin.cmxs","btauto_plugin.cmxs"],"fqns":{"halts":"BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts","c0":"BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0","TM_from_str":"BusyCoq.Individual62.TM_from_str"},"assumptions":["Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g"],"checked_at":"2026-10-16T18:52:29Z","checks":[{"id":"args","status":"PASS","summary":"6x2 machine, framework module Individual62, mode nonhalt","details":[],"warnings":[]},{"id":"input","status":"PASS","summary":"264052 bytes, 7149 lines, 4779 sentences","details":[],"warnings":[]},{"id":"framework","status":"PASS","summary":"HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/","details":[],"warnings":[]},{"id":"framework_build","status":"PASS","summary":"14 needed framework .vo files present and fresh, with native code no older than the .vo","details":[],"warnings":[]},{"id":"forbidden","status":"PASS","summary":"none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)","details":[],"warnings":[]},{"id":"structure","status":"PASS","summary":"244 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced","details":["line 11: From BusyCoq Require Individual62 -> framework Individual62.v","line 11: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 12: Require ZifyNat -> Coq stdlib","line 12: Require Lia -> Coq stdlib","line 12: Require Arith -> Coq stdlib","line 12: Require Ring -> Coq stdlib","line 12: Require ZArith -> Coq stdlib","line 12: Require String -> Coq stdlib","line 12: Require List -> Coq stdlib","line 12: Require Bool -> Coq stdlib","line 13: Require ZifyNat -> Coq stdlib","line 13: Require Lia -> Coq stdlib","line 13: Require Arith -> Coq stdlib","line 13: Require List -> Coq stdlib","line 14: From BusyCoq Require Individual62 -> framework Individual62.v","line 14: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 14: From BusyCoq Require Flip -> framework Flip.v","line 14: From BusyCoq Require Permute -> framework Permute.v","line 15: Require ZifyNat -> Coq stdlib","line 15: Require Lia -> Coq stdlib","line 15: Require Arith -> Coq stdlib","line 15: Require ZArith -> Coq stdlib","line 15: Require String -> Coq stdlib","line 15: Require List -> Coq stdlib","line 16: Require ZifyNat -> Coq stdlib","line 16: Require Lia -> Coq stdlib","line 16: Require Arith -> Coq stdlib","line 16: Require ZArith -> Coq stdlib","line 16: Require List -> Coq stdlib","line 16: Require Bool -> Coq stdlib","line 17: Require Lia -> Coq stdlib","line 17: Require Arith -> Coq stdlib","line 17: Require NArith -> Coq stdlib","line 17: Require List -> Coq stdlib","line 18: Require ZifyNat -> Coq stdlib","line 18: Require Lia -> Coq stdlib","line 18: Require Arith -> Coq stdlib","line 18: Require Ring -> Coq stdlib","line 18: Require ZArith -> Coq stdlib","line 18: Require List -> Coq stdlib","line 18: Require Bool -> Coq stdlib","line 19: Require ZifyNat -> Coq stdlib","line 19: Require Lia -> Coq stdlib","line 19: Require Arith -> Coq stdlib","line 19: Require ZArith -> Coq stdlib","line 19: Require NArith -> Coq stdlib","line 19: Require List -> Coq stdlib","line 19: Require Bool -> Coq stdlib","line 20: Require Lia -> Coq stdlib","line 20: Require Arith -> Coq stdlib","line 20: Require List -> Coq stdlib","line 21: Require Lia -> Coq stdlib","line 21: Require ZArith -> Coq stdlib","line 21: Require NArith -> Coq stdlib","line 21: Require List -> Coq stdlib","line 22: Require Lia -> Coq stdlib","line 22: Require List -> Coq stdlib","line 23: Require String -> Coq stdlib","line 23: Require List -> Coq stdlib","line 26: From BusyCoq Require Individual62 -> framework Individual62.v","line 26: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 27: Require ZifyNat -> Coq stdlib","line 27: Require Lia -> Coq stdlib","line 27: Require Arith -> Coq stdlib","line 27: Require Ring -> Coq stdlib","line 27: Require ZArith -> Coq stdlib","line 27: Require String -> Coq stdlib","line 27: Require List -> Coq stdlib","line 27: Require Bool -> Coq stdlib","line 4283: From BusyCoq Require Individual62 -> framework Individual62.v","line 4283: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4285: Require ZifyNat -> Coq stdlib","line 4285: Require Lia -> Coq stdlib","line 4285: Require Arith -> Coq stdlib","line 4285: Require List -> Coq stdlib","line 4634: From BusyCoq Require Individual62 -> framework Individual62.v","line 4634: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4634: From BusyCoq Require Flip -> framework Flip.v","line 4634: From BusyCoq Require Permute -> framework Permute.v","line 4636: Require ZifyNat -> Coq stdlib","line 4636: Require Lia -> Coq stdlib","line 4636: Require Arith -> Coq stdlib","line 4636: Require ZArith -> Coq stdlib","line 4636: Require String -> Coq stdlib","line 4636: Require List -> Coq stdlib","line 4715: From BusyCoq Require Individual62 -> framework Individual62.v","line 4715: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4717: Require ZifyNat -> Coq stdlib","line 4717: Require Lia -> Coq stdlib","line 4717: Require Arith -> Coq stdlib","line 4717: Require ZArith -> Coq stdlib","line 4717: Require List -> Coq stdlib","line 4717: Require Bool -> Coq stdlib","line 4823: From BusyCoq Require Individual62 -> framework Individual62.v","line 4823: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4825: Require ZifyNat -> Coq stdlib","line 4825: Require Lia -> Coq stdlib","line 4825: Require Arith -> Coq stdlib","line 4825: Require ZArith -> Coq stdlib","line 4825: Require List -> Coq stdlib","line 4825: Require Bool -> Coq stdlib","line 4961: From BusyCoq Require Individual62 -> framework Individual62.v","line 4961: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4963: Require Lia -> Coq stdlib","line 4963: Require Arith -> Coq stdlib","line 4963: Require NArith -> Coq stdlib","line 4963: Require List -> Coq stdlib","line 5049: From BusyCoq Require Individual62 -> framework Individual62.v","line 5049: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5051: Require ZifyNat -> Coq stdlib","line 5051: Require Lia -> Coq stdlib","line 5051: Require Arith -> Coq stdlib","line 5051: Require Ring -> Coq stdlib","line 5051: Require ZArith -> Coq stdlib","line 5051: Require List -> Coq stdlib","line 5051: Require Bool -> Coq stdlib","line 5268: From BusyCoq Require Individual62 -> framework Individual62.v","line 5268: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5270: Require ZifyNat -> Coq stdlib","line 5270: Require Lia -> Coq stdlib","line 5270: Require Arith -> Coq stdlib","line 5270: Require ZArith -> Coq stdlib","line 5270: Require NArith -> Coq stdlib","line 5270: Require List -> Coq stdlib","line 5270: Require Bool -> Coq stdlib","line 5362: From BusyCoq Require Individual62 -> framework Individual62.v","line 5362: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5364: Require ZifyNat -> Coq stdlib","line 5364: Require Lia -> Coq stdlib","line 5364: Require Arith -> Coq stdlib","line 5364: Require ZArith -> Coq stdlib","line 5364: Require NArith -> Coq stdlib","line 5364: Require List -> Coq stdlib","line 5364: Require Bool -> Coq stdlib","line 5443: From BusyCoq Require Individual62 -> framework Individual62.v","line 5443: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5445: Require ZifyNat -> Coq stdlib","line 5445: Require Lia -> Coq stdlib","line 5445: Require Arith -> Coq stdlib","line 5445: Require ZArith -> Coq stdlib","line 5445: Require NArith -> Coq stdlib","line 5445: Require List -> Coq stdlib","line 5445: Require Bool -> Coq stdlib","line 5596: From BusyCoq Require Individual62 -> framework Individual62.v","line 5596: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5598: Require ZifyNat -> Coq stdlib","line 5598: Require Lia -> Coq stdlib","line 5598: Require Arith -> Coq stdlib","line 5598: Require Ring -> Coq stdlib","line 5598: Require ZArith -> Coq stdlib","line 5598: Require String -> Coq stdlib","line 5598: Require List -> Coq stdlib","line 5598: Require Bool -> Coq stdlib","line 5732: From BusyCoq Require Individual62 -> framework Individual62.v","line 5732: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5734: Require Lia -> Coq stdlib","line 5734: Require Arith -> Coq stdlib","line 5734: Require List -> Coq stdlib","line 5857: From BusyCoq Require Individual62 -> framework Individual62.v","line 5857: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5859: Require ZifyNat -> Coq stdlib","line 5859: Require Lia -> Coq stdlib","line 5859: Require Arith -> Coq stdlib","line 5859: Require ZArith -> Coq stdlib","line 5859: Require NArith -> Coq stdlib","line 5859: Require List -> Coq stdlib","line 5859: Require Bool -> Coq stdlib","line 6017: From BusyCoq Require Individual62 -> framework Individual62.v","line 6017: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6019: Require ZifyNat -> Coq stdlib","line 6019: Require Lia -> Coq stdlib","line 6019: Require Arith -> Coq stdlib","line 6019: Require ZArith -> Coq stdlib","line 6019: Require NArith -> Coq stdlib","line 6019: Require List -> Coq stdlib","line 6019: Require Bool -> Coq stdlib","line 6218: From BusyCoq Require Individual62 -> framework Individual62.v","line 6218: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6220: Require Lia -> Coq stdlib","line 6220: Require ZArith -> Coq stdlib","line 6220: Require NArith -> Coq stdlib","line 6220: Require List -> Coq stdlib","line 6312: From BusyCoq Require Individual62 -> framework Individual62.v","line 6312: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6314: Require ZifyNat -> Coq stdlib","line 6314: Require Lia -> Coq stdlib","line 6314: Require Arith -> Coq stdlib","line 6314: Require ZArith -> Coq stdlib","line 6314: Require NArith -> Coq stdlib","line 6314: Require List -> Coq stdlib","line 6314: Require Bool -> Coq stdlib","line 6449: From BusyCoq Require Individual62 -> framework Individual62.v","line 6449: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6451: Require ZifyNat -> Coq stdlib","line 6451: Require Lia -> Coq stdlib","line 6451: Require Arith -> Coq stdlib","line 6451: Require ZArith -> Coq stdlib","line 6451: Require List -> Coq stdlib","line 6451: Require Bool -> Coq stdlib","line 6515: From BusyCoq Require Individual62 -> framework Individual62.v","line 6515: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6517: Require ZifyNat -> Coq stdlib","line 6517: Require Lia -> Coq stdlib","line 6517: Require Arith -> Coq stdlib","line 6517: Require ZArith -> Coq stdlib","line 6517: Require NArith -> Coq stdlib","line 6517: Require List -> Coq stdlib","line 6517: Require Bool -> Coq stdlib","line 6667: From BusyCoq Require Individual62 -> framework Individual62.v","line 6667: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6669: Require ZifyNat -> Coq stdlib","line 6669: Require Lia -> Coq stdlib","line 6669: Require Arith -> Coq stdlib","line 6669: Require ZArith -> Coq stdlib","line 6669: Require List -> Coq stdlib","line 6669: Require Bool -> Coq stdlib","line 6819: From BusyCoq Require Individual62 -> framework Individual62.v","line 6819: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6821: Require ZifyNat -> Coq stdlib","line 6821: Require Lia -> Coq stdlib","line 6821: Require Arith -> Coq stdlib","line 6821: Require ZArith -> Coq stdlib","line 6821: Require NArith -> Coq stdlib","line 6821: Require List -> Coq stdlib","line 6821: Require Bool -> Coq stdlib","line 6883: From BusyCoq Require Individual62 -> framework Individual62.v","line 6883: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6885: Require ZifyNat -> Coq stdlib","line 6885: Require Lia -> Coq stdlib","line 6885: Require Arith -> Coq stdlib","line 6885: Require ZArith -> Coq stdlib","line 6885: Require NArith -> Coq stdlib","line 6885: Require List -> Coq stdlib","line 6885: Require Bool -> Coq stdlib","line 7048: From BusyCoq Require Individual62 -> framework Individual62.v","line 7048: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 7050: Require Lia -> Coq stdlib","line 7050: Require List -> Coq stdlib","line 7090: From BusyCoq Require Individual62 -> framework Individual62.v","line 7090: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 7090: From BusyCoq Require Flip -> framework Flip.v","line 7090: From BusyCoq Require Permute -> framework Permute.v","line 7092: Require String -> Coq stdlib","line 7092: Require List -> Coq stdlib"],"warnings":[]},{"id":"tm_text","status":"PASS","summary":"line 7124: TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\" == <tm> (41 bytes)","details":[],"warnings":["line 33: another TM_from_str literal '1LB0RD_1LC0RC_1RA1LC_1LE0RB_1LF---_0LA0LE' (a different machine)"]},{"id":"theorem_text","status":"PASS","summary":"line 7139: nonhalt : ~halts tm c0","details":[],"warnings":[]},{"id":"coq","status":"PASS","summary":"coqc 8.20.1 (/home/dennis/projects/bb6-hunt/astra/audit-coqc)","details":[],"warnings":[]},{"id":"names","status":"PASS","summary":"halts, c0, TM_from_str resolved inside Individual62","details":["halts = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts","c0 = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0","TM_from_str = BusyCoq.Individual62.TM_from_str"],"warnings":[]},{"id":"compile","status":"PASS","summary":"compiled in 113.1s with all appended checks","details":["command: /home/dennis/projects/bb6-hunt/astra/audit-coqc -q -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify BusyCoq -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt BigInt -Q /tmp/check_kill.zdo7jcir/kill BB6Kill -native-compiler yes Candidate.v","wall time: 113.1s"],"warnings":["-native-compiler yes: native code is in the trusted base unless coqchk finishes (policy A)","Warning: /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt was","Warning: The native-compiler option is deprecated. To compile native files","Warning: Use of \u201cRequire\u201d inside a module is fragile. It is not recommended (x44)","Warning: To avoid stack overflow, large numbers in nat are interpreted as (x28)"]},{"id":"tm_rocq","status":"PASS","summary":"BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\" by eq_refl (in-file and isolated)","details":["in-file tm_conv: ok","isolated tm_conv: ok"],"warnings":[]},{"id":"theorem_rocq","status":"PASS","summary":"nonhalt : ~ halts (TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\") c0 with absolute names (in-file and isolated)","details":["in-file nonhalt : ~ halts tm c0: ok","in-file nonhalt : ~ halts (TM_from_str lit) c0: ok","isolated nonhalt : ~ halts tm c0: ok","isolated nonhalt : ~ halts (TM_from_str lit) c0: ok"],"warnings":[]},{"id":"isolation","status":"PASS","summary":"only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off","details":["isolated checker plugins and typing flags: ok","ML modules: ltac_plugin.cmxs, number_string_notation_plugin.cmxs, tauto_plugin.cmxs, cc_plugin.cmxs, firstorder_plugin.cmxs, ring_plugin.cmxs, zify_plugin.cmxs, micromega_core_plugin.cmxs, micromega_plugin.cmxs, btauto_plugin.cmxs"],"warnings":[]},{"id":"assumptions","status":"PASS","summary":"1 assumption(s), all in the baseline","details":["isolated Print Assumptions (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g","baseline entries (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g"],"warnings":[]},{"id":"coqchk","status":"PASS","summary":"coqchk -norec BB6Kill.Candidate ok (18.8s); its context summary lists nothing of the file's own","details":[],"warnings":[]},{"id":"integrity","status":"PASS","summary":"input sha256 and framework HEAD/cleanliness identical before and after","details":[],"warnings":[]}]}
JSON: {"tool":"check_kill","tool_version":4,"result":"PASS","exit":0,"file":"/home/dennis/projects/bb6-hunt/astra/decisions-20261016/w61/publication/Nonhalting.v","sha256":"cd0bfee325f897047164a4cc11325ca3e30d2acfadedf4c2abecec0a859327ca","tm":"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF","mode":"nonhalt","theorem":"nonhalt","framework_head":"0940bb9cf434ba68f0c025dabfde45a219999973","coqc":"/home/dennis/projects/bb6-hunt/astra/audit-coqc","coqc_version":"8.20.1","compile_seconds":114.26,"native_compiler":"yes","coqchk":"pass","coqchk_timeout":600,"coqchk_seconds":18.65,"ml_modules":["ltac_plugin.cmxs","number_string_notation_plugin.cmxs","tauto_plugin.cmxs","cc_plugin.cmxs","firstorder_plugin.cmxs","ring_plugin.cmxs","zify_plugin.cmxs","micromega_core_plugin.cmxs","micromega_plugin.cmxs","btauto_plugin.cmxs"],"fqns":{"halts":"BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts","c0":"BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0","TM_from_str":"BusyCoq.Individual62.TM_from_str"},"assumptions":["Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g"],"checked_at":"2026-10-16T18:54:23Z","checks":[{"id":"args","status":"PASS","summary":"6x2 machine, framework module Individual62, mode nonhalt","details":[],"warnings":[]},{"id":"input","status":"PASS","summary":"264052 bytes, 7149 lines, 4779 sentences","details":[],"warnings":[]},{"id":"framework","status":"PASS","summary":"HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/","details":[],"warnings":[]},{"id":"framework_build","status":"PASS","summary":"14 needed framework .vo files present and fresh, with native code no older than the .vo","details":[],"warnings":[]},{"id":"forbidden","status":"PASS","summary":"none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)","details":[],"warnings":[]},{"id":"structure","status":"PASS","summary":"244 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced","details":["line 11: From BusyCoq Require Individual62 -> framework Individual62.v","line 11: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 12: Require ZifyNat -> Coq stdlib","line 12: Require Lia -> Coq stdlib","line 12: Require Arith -> Coq stdlib","line 12: Require Ring -> Coq stdlib","line 12: Require ZArith -> Coq stdlib","line 12: Require String -> Coq stdlib","line 12: Require List -> Coq stdlib","line 12: Require Bool -> Coq stdlib","line 13: Require ZifyNat -> Coq stdlib","line 13: Require Lia -> Coq stdlib","line 13: Require Arith -> Coq stdlib","line 13: Require List -> Coq stdlib","line 14: From BusyCoq Require Individual62 -> framework Individual62.v","line 14: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 14: From BusyCoq Require Flip -> framework Flip.v","line 14: From BusyCoq Require Permute -> framework Permute.v","line 15: Require ZifyNat -> Coq stdlib","line 15: Require Lia -> Coq stdlib","line 15: Require Arith -> Coq stdlib","line 15: Require ZArith -> Coq stdlib","line 15: Require String -> Coq stdlib","line 15: Require List -> Coq stdlib","line 16: Require ZifyNat -> Coq stdlib","line 16: Require Lia -> Coq stdlib","line 16: Require Arith -> Coq stdlib","line 16: Require ZArith -> Coq stdlib","line 16: Require List -> Coq stdlib","line 16: Require Bool -> Coq stdlib","line 17: Require Lia -> Coq stdlib","line 17: Require Arith -> Coq stdlib","line 17: Require NArith -> Coq stdlib","line 17: Require List -> Coq stdlib","line 18: Require ZifyNat -> Coq stdlib","line 18: Require Lia -> Coq stdlib","line 18: Require Arith -> Coq stdlib","line 18: Require Ring -> Coq stdlib","line 18: Require ZArith -> Coq stdlib","line 18: Require List -> Coq stdlib","line 18: Require Bool -> Coq stdlib","line 19: Require ZifyNat -> Coq stdlib","line 19: Require Lia -> Coq stdlib","line 19: Require Arith -> Coq stdlib","line 19: Require ZArith -> Coq stdlib","line 19: Require NArith -> Coq stdlib","line 19: Require List -> Coq stdlib","line 19: Require Bool -> Coq stdlib","line 20: Require Lia -> Coq stdlib","line 20: Require Arith -> Coq stdlib","line 20: Require List -> Coq stdlib","line 21: Require Lia -> Coq stdlib","line 21: Require ZArith -> Coq stdlib","line 21: Require NArith -> Coq stdlib","line 21: Require List -> Coq stdlib","line 22: Require Lia -> Coq stdlib","line 22: Require List -> Coq stdlib","line 23: Require String -> Coq stdlib","line 23: Require List -> Coq stdlib","line 26: From BusyCoq Require Individual62 -> framework Individual62.v","line 26: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 27: Require ZifyNat -> Coq stdlib","line 27: Require Lia -> Coq stdlib","line 27: Require Arith -> Coq stdlib","line 27: Require Ring -> Coq stdlib","line 27: Require ZArith -> Coq stdlib","line 27: Require String -> Coq stdlib","line 27: Require List -> Coq stdlib","line 27: Require Bool -> Coq stdlib","line 4283: From BusyCoq Require Individual62 -> framework Individual62.v","line 4283: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4285: Require ZifyNat -> Coq stdlib","line 4285: Require Lia -> Coq stdlib","line 4285: Require Arith -> Coq stdlib","line 4285: Require List -> Coq stdlib","line 4634: From BusyCoq Require Individual62 -> framework Individual62.v","line 4634: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4634: From BusyCoq Require Flip -> framework Flip.v","line 4634: From BusyCoq Require Permute -> framework Permute.v","line 4636: Require ZifyNat -> Coq stdlib","line 4636: Require Lia -> Coq stdlib","line 4636: Require Arith -> Coq stdlib","line 4636: Require ZArith -> Coq stdlib","line 4636: Require String -> Coq stdlib","line 4636: Require List -> Coq stdlib","line 4715: From BusyCoq Require Individual62 -> framework Individual62.v","line 4715: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4717: Require ZifyNat -> Coq stdlib","line 4717: Require Lia -> Coq stdlib","line 4717: Require Arith -> Coq stdlib","line 4717: Require ZArith -> Coq stdlib","line 4717: Require List -> Coq stdlib","line 4717: Require Bool -> Coq stdlib","line 4823: From BusyCoq Require Individual62 -> framework Individual62.v","line 4823: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4825: Require ZifyNat -> Coq stdlib","line 4825: Require Lia -> Coq stdlib","line 4825: Require Arith -> Coq stdlib","line 4825: Require ZArith -> Coq stdlib","line 4825: Require List -> Coq stdlib","line 4825: Require Bool -> Coq stdlib","line 4961: From BusyCoq Require Individual62 -> framework Individual62.v","line 4961: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4963: Require Lia -> Coq stdlib","line 4963: Require Arith -> Coq stdlib","line 4963: Require NArith -> Coq stdlib","line 4963: Require List -> Coq stdlib","line 5049: From BusyCoq Require Individual62 -> framework Individual62.v","line 5049: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5051: Require ZifyNat -> Coq stdlib","line 5051: Require Lia -> Coq stdlib","line 5051: Require Arith -> Coq stdlib","line 5051: Require Ring -> Coq stdlib","line 5051: Require ZArith -> Coq stdlib","line 5051: Require List -> Coq stdlib","line 5051: Require Bool -> Coq stdlib","line 5268: From BusyCoq Require Individual62 -> framework Individual62.v","line 5268: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5270: Require ZifyNat -> Coq stdlib","line 5270: Require Lia -> Coq stdlib","line 5270: Require Arith -> Coq stdlib","line 5270: Require ZArith -> Coq stdlib","line 5270: Require NArith -> Coq stdlib","line 5270: Require List -> Coq stdlib","line 5270: Require Bool -> Coq stdlib","line 5362: From BusyCoq Require Individual62 -> framework Individual62.v","line 5362: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5364: Require ZifyNat -> Coq stdlib","line 5364: Require Lia -> Coq stdlib","line 5364: Require Arith -> Coq stdlib","line 5364: Require ZArith -> Coq stdlib","line 5364: Require NArith -> Coq stdlib","line 5364: Require List -> Coq stdlib","line 5364: Require Bool -> Coq stdlib","line 5443: From BusyCoq Require Individual62 -> framework Individual62.v","line 5443: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5445: Require ZifyNat -> Coq stdlib","line 5445: Require Lia -> Coq stdlib","line 5445: Require Arith -> Coq stdlib","line 5445: Require ZArith -> Coq stdlib","line 5445: Require NArith -> Coq stdlib","line 5445: Require List -> Coq stdlib","line 5445: Require Bool -> Coq stdlib","line 5596: From BusyCoq Require Individual62 -> framework Individual62.v","line 5596: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5598: Require ZifyNat -> Coq stdlib","line 5598: Require Lia -> Coq stdlib","line 5598: Require Arith -> Coq stdlib","line 5598: Require Ring -> Coq stdlib","line 5598: Require ZArith -> Coq stdlib","line 5598: Require String -> Coq stdlib","line 5598: Require List -> Coq stdlib","line 5598: Require Bool -> Coq stdlib","line 5732: From BusyCoq Require Individual62 -> framework Individual62.v","line 5732: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5734: Require Lia -> Coq stdlib","line 5734: Require Arith -> Coq stdlib","line 5734: Require List -> Coq stdlib","line 5857: From BusyCoq Require Individual62 -> framework Individual62.v","line 5857: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5859: Require ZifyNat -> Coq stdlib","line 5859: Require Lia -> Coq stdlib","line 5859: Require Arith -> Coq stdlib","line 5859: Require ZArith -> Coq stdlib","line 5859: Require NArith -> Coq stdlib","line 5859: Require List -> Coq stdlib","line 5859: Require Bool -> Coq stdlib","line 6017: From BusyCoq Require Individual62 -> framework Individual62.v","line 6017: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6019: Require ZifyNat -> Coq stdlib","line 6019: Require Lia -> Coq stdlib","line 6019: Require Arith -> Coq stdlib","line 6019: Require ZArith -> Coq stdlib","line 6019: Require NArith -> Coq stdlib","line 6019: Require List -> Coq stdlib","line 6019: Require Bool -> Coq stdlib","line 6218: From BusyCoq Require Individual62 -> framework Individual62.v","line 6218: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6220: Require Lia -> Coq stdlib","line 6220: Require ZArith -> Coq stdlib","line 6220: Require NArith -> Coq stdlib","line 6220: Require List -> Coq stdlib","line 6312: From BusyCoq Require Individual62 -> framework Individual62.v","line 6312: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6314: Require ZifyNat -> Coq stdlib","line 6314: Require Lia -> Coq stdlib","line 6314: Require Arith -> Coq stdlib","line 6314: Require ZArith -> Coq stdlib","line 6314: Require NArith -> Coq stdlib","line 6314: Require List -> Coq stdlib","line 6314: Require Bool -> Coq stdlib","line 6449: From BusyCoq Require Individual62 -> framework Individual62.v","line 6449: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6451: Require ZifyNat -> Coq stdlib","line 6451: Require Lia -> Coq stdlib","line 6451: Require Arith -> Coq stdlib","line 6451: Require ZArith -> Coq stdlib","line 6451: Require List -> Coq stdlib","line 6451: Require Bool -> Coq stdlib","line 6515: From BusyCoq Require Individual62 -> framework Individual62.v","line 6515: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6517: Require ZifyNat -> Coq stdlib","line 6517: Require Lia -> Coq stdlib","line 6517: Require Arith -> Coq stdlib","line 6517: Require ZArith -> Coq stdlib","line 6517: Require NArith -> Coq stdlib","line 6517: Require List -> Coq stdlib","line 6517: Require Bool -> Coq stdlib","line 6667: From BusyCoq Require Individual62 -> framework Individual62.v","line 6667: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6669: Require ZifyNat -> Coq stdlib","line 6669: Require Lia -> Coq stdlib","line 6669: Require Arith -> Coq stdlib","line 6669: Require ZArith -> Coq stdlib","line 6669: Require List -> Coq stdlib","line 6669: Require Bool -> Coq stdlib","line 6819: From BusyCoq Require Individual62 -> framework Individual62.v","line 6819: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6821: Require ZifyNat -> Coq stdlib","line 6821: Require Lia -> Coq stdlib","line 6821: Require Arith -> Coq stdlib","line 6821: Require ZArith -> Coq stdlib","line 6821: Require NArith -> Coq stdlib","line 6821: Require List -> Coq stdlib","line 6821: Require Bool -> Coq stdlib","line 6883: From BusyCoq Require Individual62 -> framework Individual62.v","line 6883: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6885: Require ZifyNat -> Coq stdlib","line 6885: Require Lia -> Coq stdlib","line 6885: Require Arith -> Coq stdlib","line 6885: Require ZArith -> Coq stdlib","line 6885: Require NArith -> Coq stdlib","line 6885: Require List -> Coq stdlib","line 6885: Require Bool -> Coq stdlib","line 7048: From BusyCoq Require Individual62 -> framework Individual62.v","line 7048: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 7050: Require Lia -> Coq stdlib","line 7050: Require List -> Coq stdlib","line 7090: From BusyCoq Require Individual62 -> framework Individual62.v","line 7090: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 7090: From BusyCoq Require Flip -> framework Flip.v","line 7090: From BusyCoq Require Permute -> framework Permute.v","line 7092: Require String -> Coq stdlib","line 7092: Require List -> Coq stdlib"],"warnings":[]},{"id":"tm_text","status":"PASS","summary":"line 7124: TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\" == <tm> (41 bytes)","details":[],"warnings":["line 33: another TM_from_str literal '1LB0RD_1LC0RC_1RA1LC_1LE0RB_1LF---_0LA0LE' (a different machine)"]},{"id":"theorem_text","status":"PASS","summary":"line 7139: nonhalt : ~halts tm c0","details":[],"warnings":[]},{"id":"coq","status":"PASS","summary":"coqc 8.20.1 (/home/dennis/projects/bb6-hunt/astra/audit-coqc)","details":[],"warnings":[]},{"id":"names","status":"PASS","summary":"halts, c0, TM_from_str resolved inside Individual62","details":["halts = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts","c0 = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0","TM_from_str = BusyCoq.Individual62.TM_from_str"],"warnings":[]},{"id":"compile","status":"PASS","summary":"compiled in 114.3s with all appended checks","details":["command: /home/dennis/projects/bb6-hunt/astra/audit-coqc -q -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify BusyCoq -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt BigInt -Q /tmp/check_kill.mjim_jub/kill BB6Kill -native-compiler yes Candidate.v","wall time: 114.3s"],"warnings":["-native-compiler yes: native code is in the trusted base unless coqchk finishes (policy A)","Warning: /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt was","Warning: The native-compiler option is deprecated. To compile native files","Warning: Use of \u201cRequire\u201d inside a module is fragile. It is not recommended (x44)","Warning: To avoid stack overflow, large numbers in nat are interpreted as (x28)"]},{"id":"tm_rocq","status":"PASS","summary":"BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\" by eq_refl (in-file and isolated)","details":["in-file tm_conv: ok","isolated tm_conv: ok"],"warnings":[]},{"id":"theorem_rocq","status":"PASS","summary":"nonhalt : ~ halts (TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\") c0 with absolute names (in-file and isolated)","details":["in-file nonhalt : ~ halts tm c0: ok","in-file nonhalt : ~ halts (TM_from_str lit) c0: ok","isolated nonhalt : ~ halts tm c0: ok","isolated nonhalt : ~ halts (TM_from_str lit) c0: ok"],"warnings":[]},{"id":"isolation","status":"PASS","summary":"only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off","details":["isolated checker plugins and typing flags: ok","ML modules: ltac_plugin.cmxs, number_string_notation_plugin.cmxs, tauto_plugin.cmxs, cc_plugin.cmxs, firstorder_plugin.cmxs, ring_plugin.cmxs, zify_plugin.cmxs, micromega_core_plugin.cmxs, micromega_plugin.cmxs, btauto_plugin.cmxs"],"warnings":[]},{"id":"assumptions","status":"PASS","summary":"1 assumption(s), all in the baseline","details":["isolated Print Assumptions (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g","baseline entries (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g"],"warnings":[]},{"id":"coqchk","status":"PASS","summary":"coqchk -norec BB6Kill.Candidate ok (18.6s); its context summary lists nothing of the file's own","details":[],"warnings":[]},{"id":"integrity","status":"PASS","summary":"input sha256 and framework HEAD/cleanliness identical before and after","details":[],"warnings":[]}]}
JSON: {"tool":"check_kill","tool_version":4,"result":"PASS","exit":0,"file":"/home/dennis/projects/bb6-hunt/astra/decisions-20261016/w61/publication/Nonhalting.v","sha256":"cd0bfee325f897047164a4cc11325ca3e30d2acfadedf4c2abecec0a859327ca","tm":"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF","mode":"nonhalt","theorem":"nonhalt","framework_head":"0940bb9cf434ba68f0c025dabfde45a219999973","coqc":"/home/dennis/projects/bb6-hunt/astra/audit-coqc","coqc_version":"8.20.1","compile_seconds":115.93,"native_compiler":"yes","coqchk":"pass","coqchk_timeout":600,"coqchk_seconds":18.81,"ml_modules":["ltac_plugin.cmxs","number_string_notation_plugin.cmxs","tauto_plugin.cmxs","cc_plugin.cmxs","firstorder_plugin.cmxs","ring_plugin.cmxs","zify_plugin.cmxs","micromega_core_plugin.cmxs","micromega_plugin.cmxs","btauto_plugin.cmxs"],"fqns":{"halts":"BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts","c0":"BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0","TM_from_str":"BusyCoq.Individual62.TM_from_str"},"assumptions":["Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g"],"checked_at":"2026-10-16T18:56:21Z","checks":[{"id":"args","status":"PASS","summary":"6x2 machine, framework module Individual62, mode nonhalt","details":[],"warnings":[]},{"id":"input","status":"PASS","summary":"264052 bytes, 7149 lines, 4779 sentences","details":[],"warnings":[]},{"id":"framework","status":"PASS","summary":"HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/","details":[],"warnings":[]},{"id":"framework_build","status":"PASS","summary":"14 needed framework .vo files present and fresh, with native code no older than the .vo","details":[],"warnings":[]},{"id":"forbidden","status":"PASS","summary":"none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)","details":[],"warnings":[]},{"id":"structure","status":"PASS","summary":"244 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced","details":["line 11: From BusyCoq Require Individual62 -> framework Individual62.v","line 11: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 12: Require ZifyNat -> Coq stdlib","line 12: Require Lia -> Coq stdlib","line 12: Require Arith -> Coq stdlib","line 12: Require Ring -> Coq stdlib","line 12: Require ZArith -> Coq stdlib","line 12: Require String -> Coq stdlib","line 12: Require List -> Coq stdlib","line 12: Require Bool -> Coq stdlib","line 13: Require ZifyNat -> Coq stdlib","line 13: Require Lia -> Coq stdlib","line 13: Require Arith -> Coq stdlib","line 13: Require List -> Coq stdlib","line 14: From BusyCoq Require Individual62 -> framework Individual62.v","line 14: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 14: From BusyCoq Require Flip -> framework Flip.v","line 14: From BusyCoq Require Permute -> framework Permute.v","line 15: Require ZifyNat -> Coq stdlib","line 15: Require Lia -> Coq stdlib","line 15: Require Arith -> Coq stdlib","line 15: Require ZArith -> Coq stdlib","line 15: Require String -> Coq stdlib","line 15: Require List -> Coq stdlib","line 16: Require ZifyNat -> Coq stdlib","line 16: Require Lia -> Coq stdlib","line 16: Require Arith -> Coq stdlib","line 16: Require ZArith -> Coq stdlib","line 16: Require List -> Coq stdlib","line 16: Require Bool -> Coq stdlib","line 17: Require Lia -> Coq stdlib","line 17: Require Arith -> Coq stdlib","line 17: Require NArith -> Coq stdlib","line 17: Require List -> Coq stdlib","line 18: Require ZifyNat -> Coq stdlib","line 18: Require Lia -> Coq stdlib","line 18: Require Arith -> Coq stdlib","line 18: Require Ring -> Coq stdlib","line 18: Require ZArith -> Coq stdlib","line 18: Require List -> Coq stdlib","line 18: Require Bool -> Coq stdlib","line 19: Require ZifyNat -> Coq stdlib","line 19: Require Lia -> Coq stdlib","line 19: Require Arith -> Coq stdlib","line 19: Require ZArith -> Coq stdlib","line 19: Require NArith -> Coq stdlib","line 19: Require List -> Coq stdlib","line 19: Require Bool -> Coq stdlib","line 20: Require Lia -> Coq stdlib","line 20: Require Arith -> Coq stdlib","line 20: Require List -> Coq stdlib","line 21: Require Lia -> Coq stdlib","line 21: Require ZArith -> Coq stdlib","line 21: Require NArith -> Coq stdlib","line 21: Require List -> Coq stdlib","line 22: Require Lia -> Coq stdlib","line 22: Require List -> Coq stdlib","line 23: Require String -> Coq stdlib","line 23: Require List -> Coq stdlib","line 26: From BusyCoq Require Individual62 -> framework Individual62.v","line 26: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 27: Require ZifyNat -> Coq stdlib","line 27: Require Lia -> Coq stdlib","line 27: Require Arith -> Coq stdlib","line 27: Require Ring -> Coq stdlib","line 27: Require ZArith -> Coq stdlib","line 27: Require String -> Coq stdlib","line 27: Require List -> Coq stdlib","line 27: Require Bool -> Coq stdlib","line 4283: From BusyCoq Require Individual62 -> framework Individual62.v","line 4283: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4285: Require ZifyNat -> Coq stdlib","line 4285: Require Lia -> Coq stdlib","line 4285: Require Arith -> Coq stdlib","line 4285: Require List -> Coq stdlib","line 4634: From BusyCoq Require Individual62 -> framework Individual62.v","line 4634: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4634: From BusyCoq Require Flip -> framework Flip.v","line 4634: From BusyCoq Require Permute -> framework Permute.v","line 4636: Require ZifyNat -> Coq stdlib","line 4636: Require Lia -> Coq stdlib","line 4636: Require Arith -> Coq stdlib","line 4636: Require ZArith -> Coq stdlib","line 4636: Require String -> Coq stdlib","line 4636: Require List -> Coq stdlib","line 4715: From BusyCoq Require Individual62 -> framework Individual62.v","line 4715: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4717: Require ZifyNat -> Coq stdlib","line 4717: Require Lia -> Coq stdlib","line 4717: Require Arith -> Coq stdlib","line 4717: Require ZArith -> Coq stdlib","line 4717: Require List -> Coq stdlib","line 4717: Require Bool -> Coq stdlib","line 4823: From BusyCoq Require Individual62 -> framework Individual62.v","line 4823: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4825: Require ZifyNat -> Coq stdlib","line 4825: Require Lia -> Coq stdlib","line 4825: Require Arith -> Coq stdlib","line 4825: Require ZArith -> Coq stdlib","line 4825: Require List -> Coq stdlib","line 4825: Require Bool -> Coq stdlib","line 4961: From BusyCoq Require Individual62 -> framework Individual62.v","line 4961: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 4963: Require Lia -> Coq stdlib","line 4963: Require Arith -> Coq stdlib","line 4963: Require NArith -> Coq stdlib","line 4963: Require List -> Coq stdlib","line 5049: From BusyCoq Require Individual62 -> framework Individual62.v","line 5049: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5051: Require ZifyNat -> Coq stdlib","line 5051: Require Lia -> Coq stdlib","line 5051: Require Arith -> Coq stdlib","line 5051: Require Ring -> Coq stdlib","line 5051: Require ZArith -> Coq stdlib","line 5051: Require List -> Coq stdlib","line 5051: Require Bool -> Coq stdlib","line 5268: From BusyCoq Require Individual62 -> framework Individual62.v","line 5268: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5270: Require ZifyNat -> Coq stdlib","line 5270: Require Lia -> Coq stdlib","line 5270: Require Arith -> Coq stdlib","line 5270: Require ZArith -> Coq stdlib","line 5270: Require NArith -> Coq stdlib","line 5270: Require List -> Coq stdlib","line 5270: Require Bool -> Coq stdlib","line 5362: From BusyCoq Require Individual62 -> framework Individual62.v","line 5362: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5364: Require ZifyNat -> Coq stdlib","line 5364: Require Lia -> Coq stdlib","line 5364: Require Arith -> Coq stdlib","line 5364: Require ZArith -> Coq stdlib","line 5364: Require NArith -> Coq stdlib","line 5364: Require List -> Coq stdlib","line 5364: Require Bool -> Coq stdlib","line 5443: From BusyCoq Require Individual62 -> framework Individual62.v","line 5443: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5445: Require ZifyNat -> Coq stdlib","line 5445: Require Lia -> Coq stdlib","line 5445: Require Arith -> Coq stdlib","line 5445: Require ZArith -> Coq stdlib","line 5445: Require NArith -> Coq stdlib","line 5445: Require List -> Coq stdlib","line 5445: Require Bool -> Coq stdlib","line 5596: From BusyCoq Require Individual62 -> framework Individual62.v","line 5596: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5598: Require ZifyNat -> Coq stdlib","line 5598: Require Lia -> Coq stdlib","line 5598: Require Arith -> Coq stdlib","line 5598: Require Ring -> Coq stdlib","line 5598: Require ZArith -> Coq stdlib","line 5598: Require String -> Coq stdlib","line 5598: Require List -> Coq stdlib","line 5598: Require Bool -> Coq stdlib","line 5732: From BusyCoq Require Individual62 -> framework Individual62.v","line 5732: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5734: Require Lia -> Coq stdlib","line 5734: Require Arith -> Coq stdlib","line 5734: Require List -> Coq stdlib","line 5857: From BusyCoq Require Individual62 -> framework Individual62.v","line 5857: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 5859: Require ZifyNat -> Coq stdlib","line 5859: Require Lia -> Coq stdlib","line 5859: Require Arith -> Coq stdlib","line 5859: Require ZArith -> Coq stdlib","line 5859: Require NArith -> Coq stdlib","line 5859: Require List -> Coq stdlib","line 5859: Require Bool -> Coq stdlib","line 6017: From BusyCoq Require Individual62 -> framework Individual62.v","line 6017: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6019: Require ZifyNat -> Coq stdlib","line 6019: Require Lia -> Coq stdlib","line 6019: Require Arith -> Coq stdlib","line 6019: Require ZArith -> Coq stdlib","line 6019: Require NArith -> Coq stdlib","line 6019: Require List -> Coq stdlib","line 6019: Require Bool -> Coq stdlib","line 6218: From BusyCoq Require Individual62 -> framework Individual62.v","line 6218: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6220: Require Lia -> Coq stdlib","line 6220: Require ZArith -> Coq stdlib","line 6220: Require NArith -> Coq stdlib","line 6220: Require List -> Coq stdlib","line 6312: From BusyCoq Require Individual62 -> framework Individual62.v","line 6312: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6314: Require ZifyNat -> Coq stdlib","line 6314: Require Lia -> Coq stdlib","line 6314: Require Arith -> Coq stdlib","line 6314: Require ZArith -> Coq stdlib","line 6314: Require NArith -> Coq stdlib","line 6314: Require List -> Coq stdlib","line 6314: Require Bool -> Coq stdlib","line 6449: From BusyCoq Require Individual62 -> framework Individual62.v","line 6449: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6451: Require ZifyNat -> Coq stdlib","line 6451: Require Lia -> Coq stdlib","line 6451: Require Arith -> Coq stdlib","line 6451: Require ZArith -> Coq stdlib","line 6451: Require List -> Coq stdlib","line 6451: Require Bool -> Coq stdlib","line 6515: From BusyCoq Require Individual62 -> framework Individual62.v","line 6515: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6517: Require ZifyNat -> Coq stdlib","line 6517: Require Lia -> Coq stdlib","line 6517: Require Arith -> Coq stdlib","line 6517: Require ZArith -> Coq stdlib","line 6517: Require NArith -> Coq stdlib","line 6517: Require List -> Coq stdlib","line 6517: Require Bool -> Coq stdlib","line 6667: From BusyCoq Require Individual62 -> framework Individual62.v","line 6667: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6669: Require ZifyNat -> Coq stdlib","line 6669: Require Lia -> Coq stdlib","line 6669: Require Arith -> Coq stdlib","line 6669: Require ZArith -> Coq stdlib","line 6669: Require List -> Coq stdlib","line 6669: Require Bool -> Coq stdlib","line 6819: From BusyCoq Require Individual62 -> framework Individual62.v","line 6819: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6821: Require ZifyNat -> Coq stdlib","line 6821: Require Lia -> Coq stdlib","line 6821: Require Arith -> Coq stdlib","line 6821: Require ZArith -> Coq stdlib","line 6821: Require NArith -> Coq stdlib","line 6821: Require List -> Coq stdlib","line 6821: Require Bool -> Coq stdlib","line 6883: From BusyCoq Require Individual62 -> framework Individual62.v","line 6883: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 6885: Require ZifyNat -> Coq stdlib","line 6885: Require Lia -> Coq stdlib","line 6885: Require Arith -> Coq stdlib","line 6885: Require ZArith -> Coq stdlib","line 6885: Require NArith -> Coq stdlib","line 6885: Require List -> Coq stdlib","line 6885: Require Bool -> Coq stdlib","line 7048: From BusyCoq Require Individual62 -> framework Individual62.v","line 7048: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 7050: Require Lia -> Coq stdlib","line 7050: Require List -> Coq stdlib","line 7090: From BusyCoq Require Individual62 -> framework Individual62.v","line 7090: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 7090: From BusyCoq Require Flip -> framework Flip.v","line 7090: From BusyCoq Require Permute -> framework Permute.v","line 7092: Require String -> Coq stdlib","line 7092: Require List -> Coq stdlib"],"warnings":[]},{"id":"tm_text","status":"PASS","summary":"line 7124: TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\" == <tm> (41 bytes)","details":[],"warnings":["line 33: another TM_from_str literal '1LB0RD_1LC0RC_1RA1LC_1LE0RB_1LF---_0LA0LE' (a different machine)"]},{"id":"theorem_text","status":"PASS","summary":"line 7139: nonhalt : ~halts tm c0","details":[],"warnings":[]},{"id":"coq","status":"PASS","summary":"coqc 8.20.1 (/home/dennis/projects/bb6-hunt/astra/audit-coqc)","details":[],"warnings":[]},{"id":"names","status":"PASS","summary":"halts, c0, TM_from_str resolved inside Individual62","details":["halts = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts","c0 = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0","TM_from_str = BusyCoq.Individual62.TM_from_str"],"warnings":[]},{"id":"compile","status":"PASS","summary":"compiled in 115.9s with all appended checks","details":["command: /home/dennis/projects/bb6-hunt/astra/audit-coqc -q -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify BusyCoq -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt BigInt -Q /tmp/check_kill.3k2reldg/kill BB6Kill -native-compiler yes Candidate.v","wall time: 115.9s"],"warnings":["-native-compiler yes: native code is in the trusted base unless coqchk finishes (policy A)","Warning: /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt was","Warning: The native-compiler option is deprecated. To compile native files","Warning: Use of \u201cRequire\u201d inside a module is fragile. It is not recommended (x44)","Warning: To avoid stack overflow, large numbers in nat are interpreted as (x28)"]},{"id":"tm_rocq","status":"PASS","summary":"BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\" by eq_refl (in-file and isolated)","details":["in-file tm_conv: ok","isolated tm_conv: ok"],"warnings":[]},{"id":"theorem_rocq","status":"PASS","summary":"nonhalt : ~ halts (TM_from_str \"1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF\") c0 with absolute names (in-file and isolated)","details":["in-file nonhalt : ~ halts tm c0: ok","in-file nonhalt : ~ halts (TM_from_str lit) c0: ok","isolated nonhalt : ~ halts tm c0: ok","isolated nonhalt : ~ halts (TM_from_str lit) c0: ok"],"warnings":[]},{"id":"isolation","status":"PASS","summary":"only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off","details":["isolated checker plugins and typing flags: ok","ML modules: ltac_plugin.cmxs, number_string_notation_plugin.cmxs, tauto_plugin.cmxs, cc_plugin.cmxs, firstorder_plugin.cmxs, ring_plugin.cmxs, zify_plugin.cmxs, micromega_core_plugin.cmxs, micromega_plugin.cmxs, btauto_plugin.cmxs"],"warnings":[]},{"id":"assumptions","status":"PASS","summary":"1 assumption(s), all in the baseline","details":["isolated Print Assumptions (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g","baseline entries (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g"],"warnings":[]},{"id":"coqchk","status":"PASS","summary":"coqchk -norec BB6Kill.Candidate ok (18.8s); its context summary lists nothing of the file's own","details":[],"warnings":[]},{"id":"integrity","status":"PASS","summary":"input sha256 and framework HEAD/cleanliness identical before and after","details":[],"warnings":[]}],"temp_dir":"/tmp/check_kill.3k2reldg"}