| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1370 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (121 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (369 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (461 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (62 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (77 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (47 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |
Global Index
A
app_incl_R [lemma, in Undecidability.Prelim.Prelim]app_incl_l [lemma, in Undecidability.Prelim.Prelim]
B
bic_POP_Zero_inv [lemma, in Undecidability.Mm.mm_comp_old]bic_POP_One_inv [lemma, in Undecidability.Mm.mm_comp_old]
bic_POP_void_inv [lemma, in Undecidability.Mm.mm_comp_old]
bic_PUSH_One_inv [lemma, in Undecidability.Mm.mm_comp_old]
bic_PUSH_Zero_inv [lemma, in Undecidability.Mm.mm_comp_old]
bic_POP_One [lemma, in Undecidability.Mm.mm_comp_old]
bic_POP_Zero [lemma, in Undecidability.Mm.mm_comp_old]
bic_POP_void [lemma, in Undecidability.Mm.mm_comp_old]
bic_PUSH_One [lemma, in Undecidability.Mm.mm_comp_old]
bic_PUSH_Zero [lemma, in Undecidability.Mm.mm_comp_old]
_ // _ ->> _ [notation, in Undecidability.Bsm.bsm_defs]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Bsm.bsm_defs]
_ // _ -1> _ [notation, in Undecidability.Bsm.bsm_defs]
Binary_Stack_Machine.n [variable, in Undecidability.Bsm.bsm_defs]
Binary_Stack_Machine [section, in Undecidability.Bsm.bsm_defs]
Binary_Stack_Machines.simulator.main_loop.C2_eq [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.iter_f_v [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.main_loop_complete_rec [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.main_loop_sound_rec [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.HP2 [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.HP1 [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.Hp [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.HC [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.C1 [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.C2 [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.Hf [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.f [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.spec [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.pre [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.lFD [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.p [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_init.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_init [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.increment_erase.p [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.increment_erase.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.increment_erase [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.lt [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hhl [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hal [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hah [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hsl [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hsh [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hsa [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.l [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.h [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.a [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.s [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.decoder_error [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.q [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.p [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.Hhl [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.Hcl [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.Hch [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.l [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.h [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.c [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.increment.Hxy [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.increment.y [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.increment.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.increment [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.q [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.p [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.Hxy [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.y [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.low [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.high [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.Hxy [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.y [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.half_tile.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.half_tile [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.cs_spec_rec [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.x' [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.q [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.p [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.Hxy [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.y [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.Hyz [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.Hxz [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.Hxy [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.z [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.y [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.y' [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.Hyz [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.Hxz [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.Hxy [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.z [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.y [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.y' [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.Hxy [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.y [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.empty_stack.i [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.empty_stack.x [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.empty_stack [section, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.n [variable, in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines [section, in Undecidability.Bsm.bsm_utils]
bitstring_false [lemma, in Undecidability.PCP_BPCP]
BPCP [definition, in Undecidability.Definitions]
BPCP_iBPCP [lemma, in Undecidability.BPCP_iBPCP]
BPCP_iBPCP [library]
bsm_simulator_correct [lemma, in Undecidability.Mm.mm_comp_old]
bsm_simulator [definition, in Undecidability.Mm.mm_comp_old]
bsm_compiler_correct2 [lemma, in Undecidability.Mm.mm_comp_old]
bsm_compiler_correct1 [lemma, in Undecidability.Mm.mm_comp_old]
bsm_compiler_complete [lemma, in Undecidability.Mm.mm_comp_old]
bsm_instr_compiler_complete [lemma, in Undecidability.Mm.mm_comp_old]
bsm_compiler_sound [lemma, in Undecidability.Mm.mm_comp_old]
bsm_instr_compiler_sound [lemma, in Undecidability.Mm.mm_comp_old]
bsm_state_enc [definition, in Undecidability.Mm.mm_comp_old]
bsm_linker_out_err [lemma, in Undecidability.Mm.mm_comp_old]
bsm_linker_out_code [lemma, in Undecidability.Mm.mm_comp_old]
bsm_linker_start [lemma, in Undecidability.Mm.mm_comp_old]
bsm_coherence [lemma, in Undecidability.Mm.mm_comp_old]
bsm_compiler_length [lemma, in Undecidability.Mm.mm_comp_old]
bsm_compiler [definition, in Undecidability.Mm.mm_comp_old]
bsm_linker [definition, in Undecidability.Mm.mm_comp_old]
bsm_instr_compile_length_geq [lemma, in Undecidability.Mm.mm_comp_old]
bsm_instr_compile_length_eq [lemma, in Undecidability.Mm.mm_comp_old]
bsm_instr_compile_length [definition, in Undecidability.Mm.mm_comp_old]
bsm_instr_compile [definition, in Undecidability.Mm.mm_comp_old]
BSM_MM_HALTING [lemma, in Undecidability.BSM_MM]
BSM_MM_HALTING.f [variable, in Undecidability.BSM_MM]
BSM_MM_HALTING [section, in Undecidability.BSM_MM]
BSM_HALTING [definition, in Undecidability.Bsm.bsm_defs]
BSM_PROBLEM [definition, in Undecidability.Bsm.bsm_defs]
bsm_steps_PUSH_inv [lemma, in Undecidability.Bsm.bsm_defs]
bsm_steps_POP_E_inv [lemma, in Undecidability.Bsm.bsm_defs]
bsm_steps_POP_any_inv [lemma, in Undecidability.Bsm.bsm_defs]
bsm_steps_POP_1_inv [lemma, in Undecidability.Bsm.bsm_defs]
bsm_steps_POP_0_inv [lemma, in Undecidability.Bsm.bsm_defs]
bsm_compute_PUSH [lemma, in Undecidability.Bsm.bsm_defs]
bsm_compute_POP_any [lemma, in Undecidability.Bsm.bsm_defs]
bsm_compute_POP_1 [lemma, in Undecidability.Bsm.bsm_defs]
bsm_compute_POP_0 [lemma, in Undecidability.Bsm.bsm_defs]
bsm_compute_POP_E [lemma, in Undecidability.Bsm.bsm_defs]
bsm_sss_stall [lemma, in Undecidability.Bsm.bsm_defs]
bsm_sss_total' [lemma, in Undecidability.Bsm.bsm_defs]
bsm_sss_total [lemma, in Undecidability.Bsm.bsm_defs]
bsm_sss_fun [lemma, in Undecidability.Bsm.bsm_defs]
bsm_sss [inductive, in Undecidability.Bsm.bsm_defs]
bsm_state [definition, in Undecidability.Bsm.bsm_defs]
bsm_push [constructor, in Undecidability.Bsm.bsm_defs]
bsm_pop [constructor, in Undecidability.Bsm.bsm_defs]
bsm_instr [inductive, in Undecidability.Bsm.bsm_defs]
bsm_mm_spec [lemma, in Undecidability.Mm.mm_comp]
bsm_mm [definition, in Undecidability.Mm.mm_comp]
bsm_instr_compile_sound [lemma, in Undecidability.Mm.mm_comp]
bsm_instr_compile_length_geq [lemma, in Undecidability.Mm.mm_comp]
bsm_instr_compile_length_eq [lemma, in Undecidability.Mm.mm_comp]
bsm_instr_compile_length [definition, in Undecidability.Mm.mm_comp]
bsm_instr_compile [definition, in Undecidability.Mm.mm_comp]
bsm_state_enc [definition, in Undecidability.Mm.mm_comp]
bsm_defs [library]
BSM_MM [library]
bsm_utils [library]
bsm_pcp [library]
BSRS [definition, in Undecidability.Definitions]
C
card [definition, in Undecidability.Definitions]card_eq [definition, in Undecidability.BPCP_iBPCP]
code [abbreviation, in Undecidability.Code.sss]
code [definition, in Undecidability.Code.subcode]
code_length [definition, in Undecidability.Code.subcode]
code_end [definition, in Undecidability.Code.subcode]
code_start [definition, in Undecidability.Code.subcode]
comp [abbreviation, in Undecidability.Mm.mm_comp_old]
comp [definition, in Undecidability.Code.compiler]
comp [section, in Undecidability.Code.compiler_correction]
compare_stack_spec [lemma, in Undecidability.Bsm.bsm_utils]
compare_stack_neq_spec [lemma, in Undecidability.Bsm.bsm_utils]
compare_stack_eq_spec [lemma, in Undecidability.Bsm.bsm_utils]
compare_stacks_length [lemma, in Undecidability.Bsm.bsm_utils]
compare_stacks [definition, in Undecidability.Bsm.bsm_utils]
compiler [section, in Undecidability.Mm.mm_comp_old]
compiler [definition, in Undecidability.Code.compiler]
compiler [library]
compiler_subcode [lemma, in Undecidability.Code.compiler]
compiler_length [lemma, in Undecidability.Code.compiler]
compiler_complete' [lemma, in Undecidability.Code.compiler_correction]
compiler_complete [lemma, in Undecidability.Code.compiler_correction]
compiler_complete_step [lemma, in Undecidability.Code.compiler_correction]
compiler_sound [lemma, in Undecidability.Code.compiler_correction]
compiler_correction [library]
compiler.bsm_end_sim [variable, in Undecidability.Mm.mm_comp_old]
compiler.bsm_comp_sim [variable, in Undecidability.Mm.mm_comp_old]
compiler.bsm_end_spec [variable, in Undecidability.Mm.mm_comp_old]
compiler.bsm_end [variable, in Undecidability.Mm.mm_comp_old]
compiler.bsm_enc_0 [variable, in Undecidability.Mm.mm_comp_old]
compiler.err [variable, in Undecidability.Mm.mm_comp_old]
compiler.Hc1 [variable, in Undecidability.Mm.mm_comp_old]
compiler.Hreg [variable, in Undecidability.Mm.mm_comp_old]
compiler.Hvr1 [variable, in Undecidability.Mm.mm_comp_old]
compiler.Hvr2 [variable, in Undecidability.Mm.mm_comp_old]
compiler.Hv12 [variable, in Undecidability.Mm.mm_comp_old]
compiler.length_nullify [variable, in Undecidability.Mm.mm_comp_old]
compiler.m [variable, in Undecidability.Mm.mm_comp_old]
compiler.n [variable, in Undecidability.Mm.mm_comp_old]
compiler.P [variable, in Undecidability.Mm.mm_comp_old]
compiler.reg [variable, in Undecidability.Mm.mm_comp_old]
compiler.tmp1 [variable, in Undecidability.Mm.mm_comp_old]
compiler.tmp2 [variable, in Undecidability.Mm.mm_comp_old]
comp_length [lemma, in Undecidability.Code.compiler]
comp_app [lemma, in Undecidability.Code.compiler]
comp.correctness [section, in Undecidability.Code.compiler_correction]
comp.correctness.HPQ [variable, in Undecidability.Code.compiler_correction]
comp.correctness.linker [variable, in Undecidability.Code.compiler_correction]
comp.correctness.P [variable, in Undecidability.Code.compiler_correction]
comp.correctness.Q [variable, in Undecidability.Code.compiler_correction]
comp.cP [variable, in Undecidability.Code.compiler_correction]
comp.err [variable, in Undecidability.Code.compiler_correction]
comp.Hicomp [variable, in Undecidability.Code.compiler_correction]
comp.Hilen [variable, in Undecidability.Code.compiler_correction]
comp.icomp [variable, in Undecidability.Code.compiler_correction]
comp.ilen [variable, in Undecidability.Code.compiler_correction]
comp.iP [variable, in Undecidability.Code.compiler_correction]
comp.iQ [variable, in Undecidability.Code.compiler_correction]
comp.P [variable, in Undecidability.Code.compiler_correction]
comp.P_eq [variable, in Undecidability.Code.compiler_correction]
comp.simul [variable, in Undecidability.Code.compiler_correction]
comp.state_Y [variable, in Undecidability.Code.compiler_correction]
comp.state_X [variable, in Undecidability.Code.compiler_correction]
comp.step_Y_fun [variable, in Undecidability.Code.compiler_correction]
comp.step_X_tot [variable, in Undecidability.Code.compiler_correction]
comp.step_Y [variable, in Undecidability.Code.compiler_correction]
comp.step_X [variable, in Undecidability.Code.compiler_correction]
comp.X [variable, in Undecidability.Code.compiler_correction]
comp.Y [variable, in Undecidability.Code.compiler_correction]
_ ⋈ _ [notation, in Undecidability.Code.compiler_correction]
_ /Y/ _ ↓ [notation, in Undecidability.Code.compiler_correction]
_ /Y/ _ ~~> _ [notation, in Undecidability.Code.compiler_correction]
_ /Y/ _ ->> _ [notation, in Undecidability.Code.compiler_correction]
_ /Y/ _ -+> _ [notation, in Undecidability.Code.compiler_correction]
_ /Y/ _ -[ _ ]-> _ [notation, in Undecidability.Code.compiler_correction]
_ /Y/ _ -1> _ [notation, in Undecidability.Code.compiler_correction]
_ /X/ _ ↓ [notation, in Undecidability.Code.compiler_correction]
_ /X/ _ ~~> _ [notation, in Undecidability.Code.compiler_correction]
_ /X/ _ ->> _ [notation, in Undecidability.Code.compiler_correction]
_ /X/ _ -+> _ [notation, in Undecidability.Code.compiler_correction]
_ /X/ _ -[ _ ]-> _ [notation, in Undecidability.Code.compiler_correction]
_ /X/ _ -1> _ [notation, in Undecidability.Code.compiler_correction]
cons_incl [lemma, in Undecidability.Prelim.Prelim]
copy_stack_spec [lemma, in Undecidability.Bsm.bsm_utils]
copy_stack_length [lemma, in Undecidability.Bsm.bsm_utils]
copy_stack [definition, in Undecidability.Bsm.bsm_utils]
copy_rev_stack_spec [lemma, in Undecidability.Bsm.bsm_utils]
copy_rev_stack [definition, in Undecidability.Bsm.bsm_utils]
count [definition, in Undecidability.Prelim.Prelim]
countSplit [lemma, in Undecidability.Prelim.Prelim]
cQ [abbreviation, in Undecidability.Code.compiler_correction]
D
DEC [abbreviation, in Undecidability.Mm.mm_defs]decoder [definition, in Undecidability.Bsm.bsm_utils]
decoder_spec_nok_2 [lemma, in Undecidability.Bsm.bsm_utils]
decoder_spec_nok_1 [lemma, in Undecidability.Bsm.bsm_utils]
decoder_spec_ok [lemma, in Undecidability.Bsm.bsm_utils]
decoder_spec_rec [lemma, in Undecidability.Bsm.bsm_utils]
decoder_length [lemma, in Undecidability.Bsm.bsm_utils]
Definitions [library]
Def_of_undec.undec_PCP [lemma, in Undecidability.UNDEC]
Def_of_undec.undec_compl [lemma, in Undecidability.UNDEC]
Def_of_undec.red_undec [lemma, in Undecidability.UNDEC]
Def_of_undec.undec_red [constructor, in Undecidability.UNDEC]
Def_of_undec.undec_seed [constructor, in Undecidability.UNDEC]
Def_of_undec.undec [inductive, in Undecidability.UNDEC]
Def_of_undec.red_turing [lemma, in Undecidability.UNDEC]
_ ⪯T _ [notation, in Undecidability.UNDEC]
Def_of_undec.compl [abbreviation, in Undecidability.UNDEC]
Def_of_undec.is_dec [constructor, in Undecidability.UNDEC]
Def_of_undec.dec [inductive, in Undecidability.UNDEC]
Def_of_undec [module, in Undecidability.UNDEC]
div2 [definition, in Undecidability.Utils.utils_nat]
div2_2p0 [definition, in Undecidability.Utils.utils_nat]
div2_2p1 [definition, in Undecidability.Utils.utils_nat]
div2_spec [lemma, in Undecidability.Utils.utils_nat]
E
eill [library]EILL_PROVABILITY [definition, in Undecidability.Ll.eill]
EILL_SEQUENT [definition, in Undecidability.Ll.eill]
eill_cmd_map [definition, in Undecidability.Ll.eill]
eill_cmd_vars [definition, in Undecidability.Ll.eill]
eill_cmd [inductive, in Undecidability.Ll.eill]
EILL_ILL_PROVABILITY [lemma, in Undecidability.EILL_ILL]
EILL_ILL [section, in Undecidability.EILL_ILL]
EILL_ILL [library]
eill_mm [library]
el_pos [lemma, in Undecidability.Prelim.Prelim]
empty_stack_spec [lemma, in Undecidability.Bsm.bsm_utils]
empty_stack_length [lemma, in Undecidability.Bsm.bsm_utils]
empty_stack [definition, in Undecidability.Bsm.bsm_utils]
eqdec [definition, in Undecidability.Utils.utils_tac]
F
f [definition, in Undecidability.BPCP_iBPCP]f [definition, in Undecidability.PCP_BPCP]
find_pow2_prop [lemma, in Undecidability.Utils.utils_nat]
find_pow2_geq [lemma, in Undecidability.Utils.utils_nat]
find_pow2 [definition, in Undecidability.Utils.utils_nat]
fix_X.X [variable, in Undecidability.Prelim.Prelim]
fix_X [section, in Undecidability.Prelim.Prelim]
flat_map_app [lemma, in Undecidability.Utils.utils_list]
focus [library]
Forall_rev [lemma, in Undecidability.Utils.utils_list]
Forall_app [lemma, in Undecidability.Utils.utils_list]
Forall2_Forall [lemma, in Undecidability.Utils.utils_list]
Forall2_map_both [lemma, in Undecidability.Utils.utils_list]
Forall2_map_right [lemma, in Undecidability.Utils.utils_list]
Forall2_map_left [lemma, in Undecidability.Utils.utils_list]
Forall2_cons_inv_r [lemma, in Undecidability.Utils.utils_list]
Forall2_cons_inv_l [lemma, in Undecidability.Utils.utils_list]
Forall2_app_inv_r [lemma, in Undecidability.Utils.utils_list]
Forall2_app_inv_l [lemma, in Undecidability.Utils.utils_list]
Forall2_cons_inv [lemma, in Undecidability.Utils.utils_list]
Forall2_nil_inv_r [lemma, in Undecidability.Utils.utils_list]
Forall2_nil_inv_l [lemma, in Undecidability.Utils.utils_list]
Forall2_mono [lemma, in Undecidability.Utils.utils_list]
full_decoder_ko_spec [lemma, in Undecidability.Bsm.bsm_utils]
full_dec_spec_rec2 [lemma, in Undecidability.Bsm.bsm_utils]
full_dec_spec_rec1 [lemma, in Undecidability.Bsm.bsm_utils]
full_decoder_ok_spec [lemma, in Undecidability.Bsm.bsm_utils]
full_dec_spec_rec [lemma, in Undecidability.Bsm.bsm_utils]
full_dec_start_spec_1 [lemma, in Undecidability.Bsm.bsm_utils]
full_dec_start_spec_0 [lemma, in Undecidability.Bsm.bsm_utils]
full_decoder_length [lemma, in Undecidability.Bsm.bsm_utils]
full_decoder [definition, in Undecidability.Bsm.bsm_utils]
f_g_subset [lemma, in Undecidability.PCP_BPCP]
f_subset [lemma, in Undecidability.PCP_BPCP]
f_g_s'_inv [lemma, in Undecidability.PCP_BPCP]
f_c [definition, in Undecidability.PCP_BPCP]
f_s_app [lemma, in Undecidability.PCP_BPCP]
f_s [definition, in Undecidability.PCP_BPCP]
G
g [definition, in Undecidability.BPCP_iBPCP]g [definition, in Undecidability.PCP_BPCP]
gen_compiler_correction [lemma, in Undecidability.Code.compiler_correction]
gen_compiler_terminates [lemma, in Undecidability.Code.compiler_correction]
gen_compiler_output [lemma, in Undecidability.Code.compiler_correction]
gen_compiler_complete [lemma, in Undecidability.Code.compiler_correction]
gen_compiler_sound [lemma, in Undecidability.Code.compiler_correction]
gen_linker_out [lemma, in Undecidability.Code.compiler_correction]
gen_compiler [definition, in Undecidability.Code.compiler_correction]
gen_linker [definition, in Undecidability.Code.compiler_correction]
G_eill_correct [lemma, in Undecidability.Ll.eill]
G_eill_complete [lemma, in Undecidability.Ll.eill]
g_eill_complete.Hvalid [variable, in Undecidability.Ll.eill]
g_eill_complete.x [variable, in Undecidability.Ll.eill]
g_eill_complete.w_surj [variable, in Undecidability.Ll.eill]
g_eill_complete.Hw [variable, in Undecidability.Ll.eill]
g_eill_complete.w [variable, in Undecidability.Ll.eill]
g_eill_complete.n [variable, in Undecidability.Ll.eill]
g_eill_complete.Hvv2 [variable, in Undecidability.Ll.eill]
g_eill_complete.Hvv1 [variable, in Undecidability.Ll.eill]
g_eill_complete.vv [variable, in Undecidability.Ll.eill]
g_eill_complete.Ga [variable, in Undecidability.Ll.eill]
g_eill_complete.Si [variable, in Undecidability.Ll.eill]
g_eill_complete [section, in Undecidability.Ll.eill]
G_eill_complete_bound [lemma, in Undecidability.Ll.eill]
[< _ |- _ >] [notation, in Undecidability.Ll.eill]
⟦ _ ⟧ [notation, in Undecidability.Ll.eill]
g_eill_complete_bound.s [variable, in Undecidability.Ll.eill]
g_eill_complete_bound.Hrx [variable, in Undecidability.Ll.eill]
g_eill_complete_bound.rx [variable, in Undecidability.Ll.eill]
g_eill_complete_bound.w_surj [variable, in Undecidability.Ll.eill]
g_eill_complete_bound.w [variable, in Undecidability.Ll.eill]
g_eill_complete_bound.n [variable, in Undecidability.Ll.eill]
g_eill_complete_bound.Ga [variable, in Undecidability.Ll.eill]
g_eill_complete_bound.Si [variable, in Undecidability.Ll.eill]
g_eill_complete_bound [section, in Undecidability.Ll.eill]
G_eill_sound [lemma, in Undecidability.Ll.eill]
g_eill_mono_Si [lemma, in Undecidability.Ll.eill]
G_eill [inductive, in Undecidability.Ll.eill]
g_c [definition, in Undecidability.PCP_BPCP]
g_s [definition, in Undecidability.PCP_BPCP]
g_s'_app [lemma, in Undecidability.PCP_BPCP]
g_s' [definition, in Undecidability.PCP_BPCP]
G_eill_mm [lemma, in Undecidability.Ll.eill_mm]
H
half_tile_spec [lemma, in Undecidability.Bsm.bsm_utils]half_tile_length [lemma, in Undecidability.Bsm.bsm_utils]
half_tile [definition, in Undecidability.Bsm.bsm_utils]
Hc [abbreviation, in Undecidability.Mm.mm_comp_old]
I
iBPCP [definition, in Undecidability.Definitions]iBPCP_BSM_HALTING [lemma, in Undecidability.iBPCP_BSM]
iBPCP_BSM_HALTING.f [variable, in Undecidability.iBPCP_BSM]
iBPCP_BSM_HALTING [section, in Undecidability.iBPCP_BSM]
iBPCP_BSM [library]
ill [library]
ILL_PROVABILITY [definition, in Undecidability.Ll.ill]
ILL_undec [lemma, in Undecidability.UNDEC]
INC [abbreviation, in Undecidability.Mm.mm_defs]
incl_sing [lemma, in Undecidability.Prelim.Prelim]
incl_nil [lemma, in Undecidability.Prelim.Prelim]
increment [definition, in Undecidability.Bsm.bsm_utils]
increment_erase_spec [lemma, in Undecidability.Bsm.bsm_utils]
increment_erase_length [lemma, in Undecidability.Bsm.bsm_utils]
increment_erase [definition, in Undecidability.Bsm.bsm_utils]
increment_spec [lemma, in Undecidability.Bsm.bsm_utils]
increment_spec_2 [lemma, in Undecidability.Bsm.bsm_utils]
increment_spec_1 [lemma, in Undecidability.Bsm.bsm_utils]
increment_length [lemma, in Undecidability.Bsm.bsm_utils]
Injective [definition, in Undecidability.Prelim.Prelim]
instruction_compiler_sound [definition, in Undecidability.Code.compiler_correction]
interval_dec [lemma, in Undecidability.Utils.utils_nat]
In_list_assoc [lemma, in Undecidability.Utils.utils_list]
in_prefix_1 [lemma, in Undecidability.Utils.utils_list]
in_prefix_0 [lemma, in Undecidability.Utils.utils_list]
In_perm [lemma, in Undecidability.Utils.utils_list]
In_list_repeat [lemma, in Undecidability.Utils.utils_list]
in_list_injective_1 [lemma, in Undecidability.Utils.utils_list]
in_list_injective_0 [lemma, in Undecidability.Utils.utils_list]
in_mm_sss_dec_1 [constructor, in Undecidability.Mm.mm_defs]
in_mm_sss_dec_0 [constructor, in Undecidability.Mm.mm_defs]
in_mm_sss_inc [constructor, in Undecidability.Mm.mm_defs]
in_eill_fork [constructor, in Undecidability.Ll.eill]
in_eill_dec [constructor, in Undecidability.Ll.eill]
in_eill_inc [constructor, in Undecidability.Ll.eill]
in_eill_perm [constructor, in Undecidability.Ll.eill]
in_eill_ax [constructor, in Undecidability.Ll.eill]
in_ll_cmd_fork [constructor, in Undecidability.Ll.eill]
in_ll_cmd_dec [constructor, in Undecidability.Ll.eill]
in_ll_cmd_inc [constructor, in Undecidability.Ll.eill]
in_omap_iff [lemma, in Undecidability.Prelim.Prelim]
in_llp_unit_r [constructor, in Undecidability.Ll.ill]
in_llp_unit_l [constructor, in Undecidability.Ll.ill]
in_llp_top_r [constructor, in Undecidability.Ll.ill]
in_llp_bot_l [constructor, in Undecidability.Ll.ill]
in_llp_plus_r2 [constructor, in Undecidability.Ll.ill]
in_llp_plus_r1 [constructor, in Undecidability.Ll.ill]
in_llp_plus_l [constructor, in Undecidability.Ll.ill]
in_llp_times_r [constructor, in Undecidability.Ll.ill]
in_llp_times_l [constructor, in Undecidability.Ll.ill]
in_llp_cut [constructor, in Undecidability.Ll.ill]
in_llp_cntr [constructor, in Undecidability.Ll.ill]
in_llp_weak [constructor, in Undecidability.Ll.ill]
in_llp_bang_r [constructor, in Undecidability.Ll.ill]
in_llp_bang_l [constructor, in Undecidability.Ll.ill]
in_llp_with_r [constructor, in Undecidability.Ll.ill]
in_llp_with_l2 [constructor, in Undecidability.Ll.ill]
in_llp_with_l1 [constructor, in Undecidability.Ll.ill]
in_llp_limp_r [constructor, in Undecidability.Ll.ill]
in_llp_limp_l [constructor, in Undecidability.Ll.ill]
in_llp_perm [constructor, in Undecidability.Ll.ill]
in_llp_ax [constructor, in Undecidability.Ll.ill]
in_bsm_sss_push [constructor, in Undecidability.Bsm.bsm_defs]
in_bsm_sss_pop_1 [constructor, in Undecidability.Bsm.bsm_defs]
in_bsm_sss_pop_0 [constructor, in Undecidability.Bsm.bsm_defs]
in_bsm_sss_pop_E [constructor, in Undecidability.Bsm.bsm_defs]
in_sss_steps_S [constructor, in Undecidability.Code.sss]
in_sss_steps_0 [constructor, in Undecidability.Code.sss]
in_sss_step [lemma, in Undecidability.Code.sss]
in_code_subcode [lemma, in Undecidability.Code.subcode]
in_out_code_dec [lemma, in Undecidability.Code.subcode]
in_out_code [lemma, in Undecidability.Code.subcode]
in_code [definition, in Undecidability.Code.subcode]
in_lbs_1 [constructor, in Undecidability.Bsm.list_bool]
in_lbs_0 [constructor, in Undecidability.Bsm.list_bool]
in_nat_sorted_3 [lemma, in Undecidability.Utils.utils_nat]
in_nat_sorted_2 [lemma, in Undecidability.Utils.utils_nat]
in_nat_sorted_1 [lemma, in Undecidability.Utils.utils_nat]
in_nat_sorted_0 [lemma, in Undecidability.Utils.utils_nat]
itau [section, in Undecidability.Definitions]
itau_tau2 [lemma, in Undecidability.BPCP_iBPCP]
itau_tau1 [lemma, in Undecidability.BPCP_iBPCP]
itau.P [variable, in Undecidability.Definitions]
itau1 [definition, in Undecidability.Definitions]
itau1_app [lemma, in Undecidability.Definitions]
itau2 [definition, in Undecidability.Definitions]
itau2_app [lemma, in Undecidability.Definitions]
iter [definition, in Undecidability.Utils.utils_list]
iter [section, in Undecidability.Utils.utils_list]
iter_plus [lemma, in Undecidability.Utils.utils_list]
iter_list_bool_next_nil [lemma, in Undecidability.Bsm.list_bool]
iter.f [variable, in Undecidability.Utils.utils_list]
iter.X [variable, in Undecidability.Utils.utils_list]
L
last_app_eq [lemma, in Undecidability.Prelim.Prelim]lemma_5_3 [lemma, in Undecidability.Ll.eill_mm]
lemma_5_5 [lemma, in Undecidability.Ll.eill_mm]
length [section, in Undecidability.Utils.utils_list]
length_cons [lemma, in Undecidability.Utils.utils_list]
length_nil [lemma, in Undecidability.Utils.utils_list]
length_compiler_app [lemma, in Undecidability.Code.compiler]
length_compiler [definition, in Undecidability.Code.compiler]
length_main_loop [definition, in Undecidability.Bsm.bsm_utils]
length_full_decoder [definition, in Undecidability.Bsm.bsm_utils]
length_decoder_size [lemma, in Undecidability.Bsm.bsm_utils]
length_decoder [definition, in Undecidability.Bsm.bsm_utils]
length_copy_rev_stack [lemma, in Undecidability.Bsm.bsm_utils]
length_move_rev_stack [lemma, in Undecidability.Bsm.bsm_utils]
length.X [variable, in Undecidability.Utils.utils_list]
link [definition, in Undecidability.Code.compiler]
linker [definition, in Undecidability.Code.compiler]
linker [section, in Undecidability.Code.compiler]
linker_out_err [lemma, in Undecidability.Code.compiler]
linker_out_code [lemma, in Undecidability.Code.compiler]
linker_code_end [lemma, in Undecidability.Code.compiler]
linker_middle [lemma, in Undecidability.Code.compiler]
linker_code_start [lemma, in Undecidability.Code.compiler]
linker_in_code [lemma, in Undecidability.Code.compiler]
linker_err_code [lemma, in Undecidability.Code.compiler]
linker_app [lemma, in Undecidability.Code.compiler]
linker.c [variable, in Undecidability.Code.compiler]
linker.comp [section, in Undecidability.Code.compiler]
linker.comp.lnk [variable, in Undecidability.Code.compiler]
linker.err [variable, in Undecidability.Code.compiler]
linker.Hc [variable, in Undecidability.Code.compiler]
linker.i [variable, in Undecidability.Code.compiler]
linker.lc [variable, in Undecidability.Code.compiler]
linker.linker_in_code.Hlc [variable, in Undecidability.Code.compiler]
linker.linker_in_code [section, in Undecidability.Code.compiler]
linker.P [variable, in Undecidability.Code.compiler]
linker.X [variable, in Undecidability.Code.compiler]
linker.Y [variable, in Undecidability.Code.compiler]
link_fst [lemma, in Undecidability.Code.compiler]
link_app [lemma, in Undecidability.Code.compiler]
list_first_dec [lemma, in Undecidability.Utils.utils_list]
list_choose_dec [lemma, in Undecidability.Utils.utils_list]
list_first_dec.Pdec [variable, in Undecidability.Utils.utils_list]
list_first_dec.P [variable, in Undecidability.Utils.utils_list]
list_first_dec.X [variable, in Undecidability.Utils.utils_list]
list_first_dec [section, in Undecidability.Utils.utils_list]
list_assoc_app [lemma, in Undecidability.Utils.utils_list]
list_assoc_In [lemma, in Undecidability.Utils.utils_list]
list_assoc_neq [lemma, in Undecidability.Utils.utils_list]
list_assoc_eq [lemma, in Undecidability.Utils.utils_list]
list_assoc [definition, in Undecidability.Utils.utils_list]
list_assoc.eq_X_dec [variable, in Undecidability.Utils.utils_list]
list_assoc.Y [variable, in Undecidability.Utils.utils_list]
list_assoc.X [variable, in Undecidability.Utils.utils_list]
list_assoc [section, in Undecidability.Utils.utils_list]
list_split_middle [lemma, in Undecidability.Utils.utils_list]
list_pick [lemma, in Undecidability.Utils.utils_list]
list_split_length [lemma, in Undecidability.Utils.utils_list]
list_app_inj [lemma, in Undecidability.Utils.utils_list]
list_app_cons_eq_inv [lemma, in Undecidability.Utils.utils_list]
list_app_eq_inv [lemma, in Undecidability.Utils.utils_list]
list_repeat_length [lemma, in Undecidability.Utils.utils_list]
list_repeat_plus [lemma, in Undecidability.Utils.utils_list]
list_repeat [definition, in Undecidability.Utils.utils_list]
list_injective_map [lemma, in Undecidability.Utils.utils_list]
list_injective_rect [lemma, in Undecidability.Utils.utils_list]
list_injective.HP1 [variable, in Undecidability.Utils.utils_list]
list_injective.HP0 [variable, in Undecidability.Utils.utils_list]
list_injective.P [variable, in Undecidability.Utils.utils_list]
list_injective_inv [lemma, in Undecidability.Utils.utils_list]
list_injective [definition, in Undecidability.Utils.utils_list]
list_injective.X [variable, in Undecidability.Utils.utils_list]
list_injective [section, in Undecidability.Utils.utils_list]
list_an_spec [lemma, in Undecidability.Utils.utils_list]
list_an_length [lemma, in Undecidability.Utils.utils_list]
list_an_plus [lemma, in Undecidability.Utils.utils_list]
list_an_S [lemma, in Undecidability.Utils.utils_list]
list_an [definition, in Undecidability.Utils.utils_list]
list_an [section, in Undecidability.Utils.utils_list]
list_vec [definition, in Undecidability.Vec.vec]
list_bool_next_total [lemma, in Undecidability.Bsm.list_bool]
list_bool_succ_rect [lemma, in Undecidability.Bsm.list_bool]
list_bool_succ_rect.list_bool_succ_rec [variable, in Undecidability.Bsm.list_bool]
list_bool_succ_rect.HPS [variable, in Undecidability.Bsm.list_bool]
list_bool_succ_rect.HP0 [variable, in Undecidability.Bsm.list_bool]
list_bool_succ_rect.P [variable, in Undecidability.Bsm.list_bool]
list_bool_succ_rect [section, in Undecidability.Bsm.list_bool]
list_bool_succ_nat [lemma, in Undecidability.Bsm.list_bool]
list_bool_next_neq_nil [lemma, in Undecidability.Bsm.list_bool]
list_bool_next_spec [definition, in Undecidability.Bsm.list_bool]
list_bool_next [definition, in Undecidability.Bsm.list_bool]
list_bool_next.list_bool_next_def [variable, in Undecidability.Bsm.list_bool]
list_bool_next [section, in Undecidability.Bsm.list_bool]
list_bool_succ_neq_nil [lemma, in Undecidability.Bsm.list_bool]
list_bool_succ_neq [lemma, in Undecidability.Bsm.list_bool]
list_bool_succ_nil [lemma, in Undecidability.Bsm.list_bool]
list_bool_succ_fun [lemma, in Undecidability.Bsm.list_bool]
list_One_inj [lemma, in Undecidability.Bsm.list_bool]
list_One_Zero_not [lemma, in Undecidability.Bsm.list_bool]
list_One_Zero_inj [lemma, in Undecidability.Bsm.list_bool]
list_bool_succ_props [section, in Undecidability.Bsm.list_bool]
list_bool_succ [inductive, in Undecidability.Bsm.list_bool]
list_bool_nat_ge_1 [lemma, in Undecidability.Bsm.list_bool]
list_bool_nat [definition, in Undecidability.Bsm.list_bool]
list_bool_valid_dec [lemma, in Undecidability.Bsm.list_bool]
list_bool_invalid [definition, in Undecidability.Bsm.list_bool]
list_bool_valid [definition, in Undecidability.Bsm.list_bool]
list_bool_decomp [lemma, in Undecidability.Bsm.list_bool]
list_nat_bool [definition, in Undecidability.Bsm.list_bool]
list_bool_choose_sym [lemma, in Undecidability.Bsm.list_bool]
list_bool_choose [lemma, in Undecidability.Bsm.list_bool]
list_bool_dec [lemma, in Undecidability.Bsm.list_bool]
list_bool [library]
list_focus [library]
ll_tps_vec_map_list [lemma, in Undecidability.Ll.eill]
ll_tps_vec_map_list_mono [lemma, in Undecidability.Ll.eill]
LL_FORK [abbreviation, in Undecidability.Ll.eill]
LL_DEC [abbreviation, in Undecidability.Ll.eill]
LL_INC [abbreviation, in Undecidability.Ll.eill]
ll_vars [definition, in Undecidability.Ll.eill]
ll_tps_sound [lemma, in Undecidability.Ll.ill]
ll_sequent_tps_eq [lemma, in Undecidability.Ll.ill]
ll_perm_tps [lemma, in Undecidability.Ll.ill]
ll_sequent_tps_mono [lemma, in Undecidability.Ll.ill]
ll_sequent_tps [definition, in Undecidability.Ll.ill]
ll_tps_perm [lemma, in Undecidability.Ll.ill]
ll_tps_list_bang_zero [lemma, in Undecidability.Ll.ill]
ll_tps_lbang [lemma, in Undecidability.Ll.ill]
ll_tps_app [lemma, in Undecidability.Ll.ill]
ll_tps_list [definition, in Undecidability.Ll.ill]
ll_tps [definition, in Undecidability.Ll.ill]
ll_tps_mult_mono [lemma, in Undecidability.Ll.ill]
ll_tps_mult [definition, in Undecidability.Ll.ill]
ll_tps_imp [definition, in Undecidability.Ll.ill]
ll_lbang [definition, in Undecidability.Ll.ill]
ll_bin [constructor, in Undecidability.Ll.ill]
ll_ban [constructor, in Undecidability.Ll.ill]
ll_zero [constructor, in Undecidability.Ll.ill]
ll_var [constructor, in Undecidability.Ll.ill]
ll_form [inductive, in Undecidability.Ll.ill]
ll_top [constructor, in Undecidability.Ll.ill]
ll_bot [constructor, in Undecidability.Ll.ill]
ll_one [constructor, in Undecidability.Ll.ill]
ll_cst [inductive, in Undecidability.Ll.ill]
ll_plus [constructor, in Undecidability.Ll.ill]
ll_times [constructor, in Undecidability.Ll.ill]
ll_limp [constructor, in Undecidability.Ll.ill]
ll_with [constructor, in Undecidability.Ll.ill]
ll_conn [inductive, in Undecidability.Ll.ill]
ll_vars [definition, in Undecidability.Ll.ill]
ll_tps_Sig_zero [lemma, in Undecidability.Ll.eill_mm]
lmax [definition, in Undecidability.Utils.utils_nat]
lng [abbreviation, in Undecidability.Mm.mm_comp_old]
lnk [abbreviation, in Undecidability.Mm.mm_comp_old]
lnk [abbreviation, in Undecidability.Code.compiler_correction]
lsum [abbreviation, in Undecidability.Code.compiler]
lsum [definition, in Undecidability.Utils.utils_nat]
lsum_app [lemma, in Undecidability.Utils.utils_nat]
M
main_loop_complete [lemma, in Undecidability.Bsm.bsm_utils]main_loop_sound [lemma, in Undecidability.Bsm.bsm_utils]
main_loop_ko_spec [lemma, in Undecidability.Bsm.bsm_utils]
main_loop_ok_spec [lemma, in Undecidability.Bsm.bsm_utils]
main_loop_size [lemma, in Undecidability.Bsm.bsm_utils]
main_loop_length [lemma, in Undecidability.Bsm.bsm_utils]
main_loop [definition, in Undecidability.Bsm.bsm_utils]
main_init_spec [lemma, in Undecidability.Bsm.bsm_utils]
main_init_length [lemma, in Undecidability.Bsm.bsm_utils]
main_init [definition, in Undecidability.Bsm.bsm_utils]
map [section, in Undecidability.Utils.utils_list]
map_middle_inv [lemma, in Undecidability.Utils.utils_list]
map_app_inv [lemma, in Undecidability.Utils.utils_list]
map_cons_inv [lemma, in Undecidability.Utils.utils_list]
map_cst_rev [lemma, in Undecidability.Utils.utils_list]
map_cst_snoc [lemma, in Undecidability.Utils.utils_list]
map_cst_repeat [lemma, in Undecidability.Utils.utils_list]
map_list_repeat [lemma, in Undecidability.Utils.utils_list]
map_inj [lemma, in Undecidability.Prelim.Prelim]
map_vec_map_list [lemma, in Undecidability.Vec.vec]
map.f [variable, in Undecidability.Utils.utils_list]
map.X [variable, in Undecidability.Utils.utils_list]
map.Y [variable, in Undecidability.Utils.utils_list]
measure_rect [lemma, in Undecidability.Utils.utils_tac]
Minsky [section, in Undecidability.Ll.eill_mm]
_ // _ ->> _ [notation, in Undecidability.Mm.mm_defs]
_ // _ -+> _ [notation, in Undecidability.Mm.mm_defs]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Mm.mm_defs]
_ // _ -1> _ [notation, in Undecidability.Mm.mm_defs]
Minsky_Machine.n [variable, in Undecidability.Mm.mm_defs]
Minsky_Machine [section, in Undecidability.Mm.mm_defs]
Minsky_Machine_utils.pop.src' [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.e [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.k [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.j [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.i [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.H2z [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.H1z [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.H12 [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.Hsz [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.Hs2 [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.Hs1 [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.zero [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.tmp2 [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.tmp1 [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.src [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop [section, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.i [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.Htz [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.Hsz [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.Hst [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.zero [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.tmp [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.src [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push [section, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.mm_mul2_spec [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.dst' [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.i [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.Hdz [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.Hsz [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.Hsd [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.zero [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.dst [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.src [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2 [section, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.mm_div2_spec_1 [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.mm_div2_spec_0 [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.i [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.Hqr [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.Hsr [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.Hsq [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.rem [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.quo [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.src [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2 [section, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.mm_transfert_spec [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.Hdz [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.Hsz [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.Hsd [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.zero [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.dst [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.src [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert [section, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_nullify.zero [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_nullify [section, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null.mm_null_spec [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null.Hsz [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null.zero [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null.src [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null [section, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.n [variable, in Undecidability.Mm.mm_utils]
Minsky_Machine_utils [section, in Undecidability.Mm.mm_utils]
Minsky.Hk [variable, in Undecidability.Ll.eill_mm]
Minsky.H_s_ry [variable, in Undecidability.Ll.eill_mm]
Minsky.H_s_rx [variable, in Undecidability.Ll.eill_mm]
Minsky.H_s_q [variable, in Undecidability.Ll.eill_mm]
Minsky.H_rx [variable, in Undecidability.Ll.eill_mm]
Minsky.k [variable, in Undecidability.Ll.eill_mm]
Minsky.n [variable, in Undecidability.Ll.eill_mm]
Minsky.P [variable, in Undecidability.Ll.eill_mm]
Minsky.prop_5_2_rec [variable, in Undecidability.Ll.eill_mm]
Minsky.q [variable, in Undecidability.Ll.eill_mm]
Minsky.rx [variable, in Undecidability.Ll.eill_mm]
Minsky.ry [variable, in Undecidability.Ll.eill_mm]
Minsky.sem_k_k_k [variable, in Undecidability.Ll.eill_mm]
Minsky.sem_k [variable, in Undecidability.Ll.eill_mm]
Minsky.sem_y_y_y [variable, in Undecidability.Ll.eill_mm]
Minsky.sem_x_y_y [variable, in Undecidability.Ll.eill_mm]
Minsky.SigI_zero [variable, in Undecidability.Ll.eill_mm]
Minsky.Sig0_zero [variable, in Undecidability.Ll.eill_mm]
_ // _ ->> _ [notation, in Undecidability.Ll.eill_mm]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Ll.eill_mm]
[[ _ ]] [notation, in Undecidability.Ll.eill_mm]
MM_HALTING_EILL_PROVABILITY [lemma, in Undecidability.MM_EILL]
MM_HALTING_EILL_PROVABILITY.f [variable, in Undecidability.MM_EILL]
MM_HALTING_EILL_PROVABILITY [section, in Undecidability.MM_EILL]
MM_HALTING [definition, in Undecidability.Mm.mm_defs]
MM_PROBLEM [definition, in Undecidability.Mm.mm_defs]
mm_steps_DEC_1_inv [lemma, in Undecidability.Mm.mm_defs]
mm_steps_DEC_0_inv [lemma, in Undecidability.Mm.mm_defs]
mm_steps_INC_inv [lemma, in Undecidability.Mm.mm_defs]
mm_compute_DEC_S [lemma, in Undecidability.Mm.mm_defs]
mm_progress_DEC_S [lemma, in Undecidability.Mm.mm_defs]
mm_compute_DEC_0 [lemma, in Undecidability.Mm.mm_defs]
mm_progress_DEC_0 [lemma, in Undecidability.Mm.mm_defs]
mm_compute_INC [lemma, in Undecidability.Mm.mm_defs]
mm_progress_INC [lemma, in Undecidability.Mm.mm_defs]
mm_sss_DEC1_inv [lemma, in Undecidability.Mm.mm_defs]
mm_sss_DEC0_inv [lemma, in Undecidability.Mm.mm_defs]
mm_sss_INC_inv [lemma, in Undecidability.Mm.mm_defs]
mm_sss_total [lemma, in Undecidability.Mm.mm_defs]
mm_sss_fun [lemma, in Undecidability.Mm.mm_defs]
mm_sss [inductive, in Undecidability.Mm.mm_defs]
mm_state [definition, in Undecidability.Mm.mm_defs]
mm_dec [constructor, in Undecidability.Mm.mm_defs]
mm_inc [constructor, in Undecidability.Mm.mm_defs]
mm_instr [inductive, in Undecidability.Mm.mm_defs]
mm_pop_One_progress [lemma, in Undecidability.Mm.mm_utils]
mm_pop_Zero_progress [lemma, in Undecidability.Mm.mm_utils]
mm_pop_void_progress [lemma, in Undecidability.Mm.mm_utils]
mm_pop_length [lemma, in Undecidability.Mm.mm_utils]
mm_pop [definition, in Undecidability.Mm.mm_utils]
mm_push_One_progress [lemma, in Undecidability.Mm.mm_utils]
mm_push_One_length [lemma, in Undecidability.Mm.mm_utils]
mm_push_One [definition, in Undecidability.Mm.mm_utils]
mm_push_Zero_progress [lemma, in Undecidability.Mm.mm_utils]
mm_push_Zero_length [lemma, in Undecidability.Mm.mm_utils]
mm_push_Zero [definition, in Undecidability.Mm.mm_utils]
mm_mul2_progress [lemma, in Undecidability.Mm.mm_utils]
mm_mul2_length [lemma, in Undecidability.Mm.mm_utils]
mm_mul2 [definition, in Undecidability.Mm.mm_utils]
mm_div2_progress_0 [lemma, in Undecidability.Mm.mm_utils]
mm_div2_progress_1 [lemma, in Undecidability.Mm.mm_utils]
mm_div2_progress [lemma, in Undecidability.Mm.mm_utils]
mm_div2_length [lemma, in Undecidability.Mm.mm_utils]
mm_div2 [definition, in Undecidability.Mm.mm_utils]
mm_transfert_progress [lemma, in Undecidability.Mm.mm_utils]
mm_transfert_length [lemma, in Undecidability.Mm.mm_utils]
mm_transfert [definition, in Undecidability.Mm.mm_utils]
mm_nullify_compute [lemma, in Undecidability.Mm.mm_utils]
mm_nullify_length [lemma, in Undecidability.Mm.mm_utils]
mm_nullify [definition, in Undecidability.Mm.mm_utils]
mm_null_progress [lemma, in Undecidability.Mm.mm_utils]
mm_null_length [lemma, in Undecidability.Mm.mm_utils]
mm_null [definition, in Undecidability.Mm.mm_utils]
mm_linstr_enc_spec [lemma, in Undecidability.Ll.eill_mm]
mm_linstr_enc_app [lemma, in Undecidability.Ll.eill_mm]
mm_linstr_enc [definition, in Undecidability.Ll.eill_mm]
mm_comp [library]
mm_utils [library]
mm_comp_old [library]
MM_EILL [library]
mm_defs [library]
move_rev_stack_spec [lemma, in Undecidability.Bsm.bsm_utils]
move_rev_stack [definition, in Undecidability.Bsm.bsm_utils]
N
natToDigit [definition, in Undecidability.Utils.utils_string]nat_pos [definition, in Undecidability.Vec.pos]
nat_sinc_inj [lemma, in Undecidability.Utils.utils_nat]
nat_sinc [lemma, in Undecidability.Utils.utils_nat]
nat_sort_sorted [lemma, in Undecidability.Utils.utils_nat]
nat_sort_eq [lemma, in Undecidability.Utils.utils_nat]
nat_sort_length [lemma, in Undecidability.Utils.utils_nat]
nat_sort [definition, in Undecidability.Utils.utils_nat]
nat_list_insert_sorted [lemma, in Undecidability.Utils.utils_nat]
nat_list_insert_Forall [lemma, in Undecidability.Utils.utils_nat]
nat_list_insert_incl [lemma, in Undecidability.Utils.utils_nat]
nat_list_insert_length [lemma, in Undecidability.Utils.utils_nat]
nat_list_insert [definition, in Undecidability.Utils.utils_nat]
nat_sorted_injective [lemma, in Undecidability.Utils.utils_nat]
nat_sorted_rect [lemma, in Undecidability.Utils.utils_nat]
nat_sorted.HP2 [variable, in Undecidability.Utils.utils_nat]
nat_sorted.HP1 [variable, in Undecidability.Utils.utils_nat]
nat_sorted.HP0 [variable, in Undecidability.Utils.utils_nat]
nat_sorted.P [variable, in Undecidability.Utils.utils_nat]
nat_sorted_head_inv [lemma, in Undecidability.Utils.utils_nat]
nat_sorted_Forall [lemma, in Undecidability.Utils.utils_nat]
nat_sorted_cons_inv [lemma, in Undecidability.Utils.utils_nat]
nat_sorted [definition, in Undecidability.Utils.utils_nat]
nat_sorted [section, in Undecidability.Utils.utils_nat]
nat_new_spec [lemma, in Undecidability.Utils.utils_nat]
nat_new [definition, in Undecidability.Utils.utils_nat]
nat2pos [definition, in Undecidability.Vec.pos]
nat2pos_pos2nat [lemma, in Undecidability.Vec.pos]
new [section, in Undecidability.Utils.utils_nat]
notInZero [lemma, in Undecidability.Prelim.Prelim]
not_In_list_assoc [lemma, in Undecidability.Utils.utils_list]
NToDigit [definition, in Undecidability.Utils.utils_string]
N_to_string.loop [variable, in Undecidability.Utils.utils_string]
N_to_string [section, in Undecidability.Utils.utils_string]
O
omap [definition, in Undecidability.Prelim.Prelim]One [abbreviation, in Undecidability.Bsm.list_bool]
One [abbreviation, in Undecidability.Utils.utils_nat]
out_code [definition, in Undecidability.Code.subcode]
P
PCP [definition, in Undecidability.Definitions]pcp_bsm_complete [lemma, in Undecidability.Bsm.bsm_pcp]
pcp_bsm_sound [lemma, in Undecidability.Bsm.bsm_pcp]
pcp_bsm_size [lemma, in Undecidability.Bsm.bsm_pcp]
pcp_bsm [definition, in Undecidability.Bsm.bsm_pcp]
PCP_BPCP [lemma, in Undecidability.PCP_BPCP]
PCP_BPCP [library]
pm_id [definition, in Undecidability.Vec.pos]
pm_comp_lift [lemma, in Undecidability.Vec.pos]
pm_comp [definition, in Undecidability.Vec.pos]
pm_lift_ext [lemma, in Undecidability.Vec.pos]
pm_lift_nxt [lemma, in Undecidability.Vec.pos]
pm_lift_fst [lemma, in Undecidability.Vec.pos]
pm_lift [definition, in Undecidability.Vec.pos]
pm_ext_eq [definition, in Undecidability.Vec.pos]
POP [abbreviation, in Undecidability.Bsm.bsm_defs]
pos [definition, in Undecidability.Prelim.Prelim]
pos [inductive, in Undecidability.Vec.pos]
pos [library]
pos_length [lemma, in Undecidability.Prelim.Prelim]
pos_nth [lemma, in Undecidability.Prelim.Prelim]
pos_not_diag_spec [lemma, in Undecidability.Vec.pos]
pos_not_diag [definition, in Undecidability.Vec.pos]
pos_prod.ll_prop [variable, in Undecidability.Vec.pos]
pos_prod.ll [variable, in Undecidability.Vec.pos]
pos_prod.n [variable, in Undecidability.Vec.pos]
pos_prod [section, in Undecidability.Vec.pos]
pos_sub2nat [lemma, in Undecidability.Vec.pos]
pos_sub [definition, in Undecidability.Vec.pos]
pos_nat [definition, in Undecidability.Vec.pos]
pos_nat [section, in Undecidability.Vec.pos]
pos_map [definition, in Undecidability.Vec.pos]
pos_map [section, in Undecidability.Vec.pos]
pos_eq_dec [definition, in Undecidability.Vec.pos]
pos_eq_dec [section, in Undecidability.Vec.pos]
pos_reif_t [lemma, in Undecidability.Vec.pos]
pos_reification [lemma, in Undecidability.Vec.pos]
pos_list_length [lemma, in Undecidability.Vec.pos]
pos_list_prop [lemma, in Undecidability.Vec.pos]
pos_list [definition, in Undecidability.Vec.pos]
pos_O_any [definition, in Undecidability.Vec.pos]
pos_S_invert [lemma, in Undecidability.Vec.pos]
pos_O_invert [lemma, in Undecidability.Vec.pos]
pos_invert.pos_invert [variable, in Undecidability.Vec.pos]
pos_invert.pos_invert_t [variable, in Undecidability.Vec.pos]
pos_invert [section, in Undecidability.Vec.pos]
pos_nxt_inj [definition, in Undecidability.Vec.pos]
pos_S_inv [definition, in Undecidability.Vec.pos]
pos_O_inv [definition, in Undecidability.Vec.pos]
pos_inv.pos_inv [variable, in Undecidability.Vec.pos]
pos_inv.pos_inv_t [variable, in Undecidability.Vec.pos]
pos_inv [section, in Undecidability.Vec.pos]
pos_iso [definition, in Undecidability.Vec.pos]
pos_nxt [constructor, in Undecidability.Vec.pos]
pos_fst [constructor, in Undecidability.Vec.pos]
pos0 [abbreviation, in Undecidability.Vec.pos]
pos1 [abbreviation, in Undecidability.Vec.pos]
pos10 [abbreviation, in Undecidability.Vec.pos]
pos11 [abbreviation, in Undecidability.Vec.pos]
pos12 [abbreviation, in Undecidability.Vec.pos]
pos13 [abbreviation, in Undecidability.Vec.pos]
pos14 [abbreviation, in Undecidability.Vec.pos]
pos15 [abbreviation, in Undecidability.Vec.pos]
pos16 [abbreviation, in Undecidability.Vec.pos]
pos17 [abbreviation, in Undecidability.Vec.pos]
pos18 [abbreviation, in Undecidability.Vec.pos]
pos19 [abbreviation, in Undecidability.Vec.pos]
pos2 [abbreviation, in Undecidability.Vec.pos]
pos2nat [definition, in Undecidability.Vec.pos]
pos2nat_nxt [lemma, in Undecidability.Vec.pos]
pos2nat_fst [lemma, in Undecidability.Vec.pos]
pos2nat_nat2pos [lemma, in Undecidability.Vec.pos]
pos2nat_inj [lemma, in Undecidability.Vec.pos]
pos2nat_prop [lemma, in Undecidability.Vec.pos]
pos20 [abbreviation, in Undecidability.Vec.pos]
pos3 [abbreviation, in Undecidability.Vec.pos]
pos4 [abbreviation, in Undecidability.Vec.pos]
pos5 [abbreviation, in Undecidability.Vec.pos]
pos6 [abbreviation, in Undecidability.Vec.pos]
pos7 [abbreviation, in Undecidability.Vec.pos]
pos8 [abbreviation, in Undecidability.Vec.pos]
pos9 [abbreviation, in Undecidability.Vec.pos]
pow2 [definition, in Undecidability.Utils.utils_nat]
pow2_bound.loop_prop [variable, in Undecidability.Utils.utils_nat]
pow2_bound.loop [variable, in Undecidability.Utils.utils_nat]
pow2_bound [section, in Undecidability.Utils.utils_nat]
prefix [section, in Undecidability.Utils.utils_list]
prefix [definition, in Undecidability.Utils.utils_list]
prefix_app_lft_inv [lemma, in Undecidability.Utils.utils_list]
prefix_spec [definition, in Undecidability.Utils.utils_list]
prefix_app_inv [lemma, in Undecidability.Utils.utils_list]
prefix_rect [definition, in Undecidability.Utils.utils_list]
prefix_trans [lemma, in Undecidability.Utils.utils_list]
prefix_refl [lemma, in Undecidability.Utils.utils_list]
prefix_list_inv [lemma, in Undecidability.Utils.utils_list]
prefix_inv [lemma, in Undecidability.Utils.utils_list]
prefix_app_lft [lemma, in Undecidability.Utils.utils_list]
prefix_length [lemma, in Undecidability.Utils.utils_list]
prefix.prefix_rect.HP1 [variable, in Undecidability.Utils.utils_list]
prefix.prefix_rect.HP0 [variable, in Undecidability.Utils.utils_list]
prefix.prefix_rect.P [variable, in Undecidability.Utils.utils_list]
prefix.prefix_rect [section, in Undecidability.Utils.utils_list]
prefix.X [variable, in Undecidability.Utils.utils_list]
Prelim [library]
prop_5_2 [lemma, in Undecidability.Ll.eill_mm]
PUSH [abbreviation, in Undecidability.Bsm.bsm_defs]
Q
Q [abbreviation, in Undecidability.Mm.mm_comp_old]R
reduces [definition, in Undecidability.Definitions]reduces_transitive [lemma, in Undecidability.Definitions]
rev_nil [lemma, in Undecidability.Prelim.Prelim]
rev_eq [lemma, in Undecidability.Prelim.Prelim]
S
s [definition, in Undecidability.Ll.eill_mm]Sig [definition, in Undecidability.Ll.eill_mm]
SigI [definition, in Undecidability.Ll.eill_mm]
Sig_zero [lemma, in Undecidability.Ll.eill_mm]
Sig0 [definition, in Undecidability.Ll.eill_mm]
simulator [abbreviation, in Undecidability.Bsm.bsm_pcp]
Simulator [section, in Undecidability.Bsm.bsm_pcp]
simulator [section, in Undecidability.Mm.mm_comp]
simulator_length [lemma, in Undecidability.Bsm.bsm_pcp]
Simulator.a [variable, in Undecidability.Bsm.bsm_pcp]
simulator.bsm_sim.cE_sim [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.cQ_sim [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.E_spec [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.cE [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.cN [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.iE [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.Q_spec2 [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.Q_spec1 [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.w_prop [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.w [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.v [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.HQ2 [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.HQ1 [variable, in Undecidability.Mm.mm_comp]
_ ⋈ _ [notation, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.Hlnk [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.Q [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.lnk [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.lnk_Q_pair [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.cP [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim.iP [variable, in Undecidability.Mm.mm_comp]
simulator.bsm_sim [section, in Undecidability.Mm.mm_comp]
Simulator.h [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.Hah [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.Hal [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.Hhl [variable, in Undecidability.Bsm.bsm_pcp]
simulator.Hreg [variable, in Undecidability.Mm.mm_comp]
Simulator.Hsa [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.Hsh [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.Hsl [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.HS1 [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.HS2 [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.HS3 [variable, in Undecidability.Bsm.bsm_pcp]
simulator.Hvr1 [variable, in Undecidability.Mm.mm_comp]
simulator.Hvr2 [variable, in Undecidability.Mm.mm_comp]
simulator.Hv12 [variable, in Undecidability.Mm.mm_comp]
Simulator.l [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.lML [variable, in Undecidability.Bsm.bsm_pcp]
Simulator.lt [variable, in Undecidability.Bsm.bsm_pcp]
simulator.m [variable, in Undecidability.Mm.mm_comp]
Simulator.n [variable, in Undecidability.Bsm.bsm_pcp]
simulator.n [variable, in Undecidability.Mm.mm_comp]
simulator.reg [variable, in Undecidability.Mm.mm_comp]
Simulator.s [variable, in Undecidability.Bsm.bsm_pcp]
simulator.tmp1 [variable, in Undecidability.Mm.mm_comp]
simulator.tmp2 [variable, in Undecidability.Mm.mm_comp]
size_induction [lemma, in Undecidability.Prelim.Prelim]
size_cards [definition, in Undecidability.Bsm.bsm_utils]
Small_Step_Semantics.sss_loop.HP2 [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.HP1 [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.Hp [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.p [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.i [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.HC [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.C2 [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.C1 [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.Hf [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.f [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.spec [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.pre [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.P [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop [section, in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind.HQ1 [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind.HQ0 [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind.R [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind.P [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind [section, in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind.HR1 [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind.HR0 [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind.R [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind.P [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind [section, in Undecidability.Code.sss]
_ // _ -]] _ [notation, in Undecidability.Code.sss]
_ // _ ↓ [notation, in Undecidability.Code.sss]
_ // _ ~~> _ [notation, in Undecidability.Code.sss]
_ // _ ->> _ [notation, in Undecidability.Code.sss]
_ // _ -+> _ [notation, in Undecidability.Code.sss]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Code.sss]
_ // _ :1> _ [notation, in Undecidability.Code.sss]
Small_Step_Semantics.sss_dec [variable, in Undecidability.Code.sss]
Small_Step_Semantics.sss_fun [variable, in Undecidability.Code.sss]
_ ⟬ _ ⦒ _ [notation, in Undecidability.Code.sss]
_ // _ -1> _ [notation, in Undecidability.Code.sss]
Small_Step_Semantics.one_step [variable, in Undecidability.Code.sss]
Small_Step_Semantics.data [variable, in Undecidability.Code.sss]
Small_Step_Semantics.instr [variable, in Undecidability.Code.sss]
Small_Step_Semantics [section, in Undecidability.Code.sss]
SRS [definition, in Undecidability.Definitions]
sss [library]
sss_loop_complete [lemma, in Undecidability.Code.sss]
sss_loop_sound [lemma, in Undecidability.Code.sss]
sss_output_fun [lemma, in Undecidability.Code.sss]
sss_compute_fun [lemma, in Undecidability.Code.sss]
sss_compute_stop [lemma, in Undecidability.Code.sss]
sss_steps_stop [lemma, in Undecidability.Code.sss]
sss_compute_step_out_inv [lemma, in Undecidability.Code.sss]
sss_compute_inv [lemma, in Undecidability.Code.sss]
sss_compute_max_ind [lemma, in Undecidability.Code.sss]
sss_terminates_ind [lemma, in Undecidability.Code.sss]
sss_steps_stall [lemma, in Undecidability.Code.sss]
sss_step_stall_inv [lemma, in Undecidability.Code.sss]
sss_stall_step_0 [lemma, in Undecidability.Code.sss]
sss_stall_step_stall [lemma, in Undecidability.Code.sss]
sss_out_step_stall [lemma, in Undecidability.Code.sss]
sss_compute_max [definition, in Undecidability.Code.sss]
sss_steps_stall_fun [lemma, in Undecidability.Code.sss]
sss_steps_stall_inv [lemma, in Undecidability.Code.sss]
sss_step_stall [definition, in Undecidability.Code.sss]
sss_stall [definition, in Undecidability.Code.sss]
sss_terminates [definition, in Undecidability.Code.sss]
sss_output [definition, in Undecidability.Code.sss]
sss_steps_compute [lemma, in Undecidability.Code.sss]
sss_step_in_code [lemma, in Undecidability.Code.sss]
sss_progress_trans [lemma, in Undecidability.Code.sss]
sss_compute_progress_trans [lemma, in Undecidability.Code.sss]
sss_progress_compute_trans [lemma, in Undecidability.Code.sss]
sss_compute_trans [lemma, in Undecidability.Code.sss]
sss_progress_compute [lemma, in Undecidability.Code.sss]
sss_compute [definition, in Undecidability.Code.sss]
sss_progress [definition, in Undecidability.Code.sss]
sss_steps_plus_inv [lemma, in Undecidability.Code.sss]
sss_steps_fun [lemma, in Undecidability.Code.sss]
sss_steps_S_inv' [lemma, in Undecidability.Code.sss]
sss_steps_inv [lemma, in Undecidability.Code.sss]
sss_steps_S_inv [lemma, in Undecidability.Code.sss]
sss_steps_0_inv [lemma, in Undecidability.Code.sss]
sss_steps_trans [lemma, in Undecidability.Code.sss]
sss_steps_1 [lemma, in Undecidability.Code.sss]
sss_steps_0 [lemma, in Undecidability.Code.sss]
sss_steps [inductive, in Undecidability.Code.sss]
sss_step_dec [lemma, in Undecidability.Code.sss]
sss_step_supcode [lemma, in Undecidability.Code.sss]
sss_step_subcode_inv [lemma, in Undecidability.Code.sss]
sss_step_fun [lemma, in Undecidability.Code.sss]
sss_step [definition, in Undecidability.Code.sss]
stack [definition, in Undecidability.Definitions]
stack_enc_S [lemma, in Undecidability.Mm.mm_utils]
stack_enc [definition, in Undecidability.Mm.mm_utils]
state [abbreviation, in Undecidability.Code.sss]
string [definition, in Undecidability.Definitions]
string_of_nat [definition, in Undecidability.Utils.utils_string]
string_of_N [definition, in Undecidability.Utils.utils_string]
subcode [definition, in Undecidability.Code.subcode]
subcode [section, in Undecidability.Code.subcode]
subcode [library]
subcode_sss_terminates [lemma, in Undecidability.Code.sss]
subcode_sss_steps_stop [lemma, in Undecidability.Code.sss]
subcode_sss_steps_inv_1 [lemma, in Undecidability.Code.sss]
subcode_sss_subcode_compute_inv [lemma, in Undecidability.Code.sss]
subcode_sss_progress_inv [lemma, in Undecidability.Code.sss]
subcode_sss_subcode_inv [lemma, in Undecidability.Code.sss]
subcode_sss_step_inv_1 [lemma, in Undecidability.Code.sss]
subcode_sss_compute_inv [lemma, in Undecidability.Code.sss]
subcode_sss_steps_inv [lemma, in Undecidability.Code.sss]
subcode_sss_step_inv [lemma, in Undecidability.Code.sss]
subcode_sss_compute_instr [lemma, in Undecidability.Code.sss]
subcode_sss_compute_linstr [lemma, in Undecidability.Code.sss]
subcode_sss_compute_trans [lemma, in Undecidability.Code.sss]
subcode_sss_compute [lemma, in Undecidability.Code.sss]
subcode_sss_progress [lemma, in Undecidability.Code.sss]
subcode_sss_steps [lemma, in Undecidability.Code.sss]
subcode_sss_step [lemma, in Undecidability.Code.sss]
subcode_mm_linstr_dec [lemma, in Undecidability.Ll.eill_mm]
subcode_mm_linstr_enc [lemma, in Undecidability.Ll.eill_mm]
subcode_snoc_inv [lemma, in Undecidability.Code.subcode]
subcode_cons_inv [lemma, in Undecidability.Code.subcode]
subcode_app_inv [lemma, in Undecidability.Code.subcode]
subcode_cons [lemma, in Undecidability.Code.subcode]
subcode_app_end [lemma, in Undecidability.Code.subcode]
subcode_right [lemma, in Undecidability.Code.subcode]
subcode_left [lemma, in Undecidability.Code.subcode]
subcode_out_code [lemma, in Undecidability.Code.subcode]
subcode_in_code [lemma, in Undecidability.Code.subcode]
subcode_trans [lemma, in Undecidability.Code.subcode]
subcode_refl [lemma, in Undecidability.Code.subcode]
subcode_start_in_code [lemma, in Undecidability.Code.subcode]
subcode_length_le [lemma, in Undecidability.Code.subcode]
subcode_length [lemma, in Undecidability.Code.subcode]
subcode.Q [variable, in Undecidability.Code.subcode]
subcode.X [variable, in Undecidability.Code.subcode]
_
swap [definition, in Undecidability.Utils.utils_tac]
symbol [definition, in Undecidability.Definitions]
S_ill_weak_cntr [lemma, in Undecidability.Ll.ill]
S_ill_cntr [lemma, in Undecidability.Ll.ill]
S_ill_weak [lemma, in Undecidability.Ll.ill]
S_ill [inductive, in Undecidability.Ll.ill]
T
tau_itau2 [lemma, in Undecidability.BPCP_iBPCP]tau_itau1 [lemma, in Undecidability.BPCP_iBPCP]
tau1 [definition, in Undecidability.Definitions]
tau1_g [lemma, in Undecidability.PCP_BPCP]
tau1_f [lemma, in Undecidability.PCP_BPCP]
tau2 [definition, in Undecidability.Definitions]
tau2_g [lemma, in Undecidability.PCP_BPCP]
tau2_f [lemma, in Undecidability.PCP_BPCP]
test [section, in Undecidability.Utils.focus]
test.a [variable, in Undecidability.Utils.focus]
test.b [variable, in Undecidability.Utils.focus]
test.c [variable, in Undecidability.Utils.focus]
test.x [variable, in Undecidability.Utils.focus]
test.X [variable, in Undecidability.Utils.focus]
test.y [variable, in Undecidability.Utils.focus]
test.z [variable, in Undecidability.Utils.focus]
tile [definition, in Undecidability.Bsm.bsm_utils]
tiles_solvable [definition, in Undecidability.Bsm.tiles_solvable]
tiles_solvable_iBPCP [lemma, in Undecidability.iBPCP_BSM]
tiles_solvable [library]
tile_concat [definition, in Undecidability.Bsm.tiles_solvable]
tile_concat_itau [lemma, in Undecidability.iBPCP_BSM]
tile_spec [lemma, in Undecidability.Bsm.bsm_utils]
tile_length [lemma, in Undecidability.Bsm.bsm_utils]
to_bitstring [definition, in Undecidability.PCP_BPCP]
TPS [section, in Undecidability.Ll.eill]
TPS.n [variable, in Undecidability.Ll.eill]
TPS.rx [variable, in Undecidability.Ll.eill]
TPS.s [variable, in Undecidability.Ll.eill]
transfer_ones_spec_2 [lemma, in Undecidability.Bsm.bsm_utils]
transfer_ones_spec_1 [lemma, in Undecidability.Bsm.bsm_utils]
transfer_ones_length [lemma, in Undecidability.Bsm.bsm_utils]
transfer_ones [definition, in Undecidability.Bsm.bsm_utils]
[< _ |- _ >] [notation, in Undecidability.Ll.ill]
[[ _ ]] [notation, in Undecidability.Ll.ill]
⟦ _ ⟧ [notation, in Undecidability.Ll.ill]
_ -* _ [notation, in Undecidability.Ll.ill]
_ ** _ [notation, in Undecidability.Ll.ill]
trivial_phase_semantics.s [variable, in Undecidability.Ll.ill]
trivial_phase_semantics.n [variable, in Undecidability.Ll.ill]
trivial_phase_semantics [section, in Undecidability.Ll.ill]
U
UNDEC [library]utils [library]
utils_tac [library]
utils_nat [library]
utils_list [library]
utils_string [library]
V
vars [abbreviation, in Undecidability.Ll.eill]vars [abbreviation, in Undecidability.Ll.eill]
vec [inductive, in Undecidability.Vec.vec]
vec [library]
vector [section, in Undecidability.Vec.vec]
vector.eq_X_dec [variable, in Undecidability.Vec.vec]
vector.vec_head_tail_prop [variable, in Undecidability.Vec.vec]
vector.vec_head_tail_type [variable, in Undecidability.Vec.vec]
vector.vec_split_type [variable, in Undecidability.Vec.vec]
vector.X [variable, in Undecidability.Vec.vec]
vec_map_list_plus [lemma, in Undecidability.Vec.vec]
vec_map_list_one [lemma, in Undecidability.Vec.vec]
vec_map_list_zero [lemma, in Undecidability.Vec.vec]
vec_map_list [definition, in Undecidability.Vec.vec]
vec_map_list.X [variable, in Undecidability.Vec.vec]
vec_map_list [section, in Undecidability.Vec.vec]
vec_nat_induction [lemma, in Undecidability.Vec.vec]
vec_nat_induction.HP2 [variable, in Undecidability.Vec.vec]
vec_nat_induction.HP1 [variable, in Undecidability.Vec.vec]
vec_nat_induction.HP0 [variable, in Undecidability.Vec.vec]
vec_nat_induction.P [variable, in Undecidability.Vec.vec]
vec_nat_induction.n [variable, in Undecidability.Vec.vec]
vec_nat_induction [section, in Undecidability.Vec.vec]
vec_sum_is_nzero [lemma, in Undecidability.Vec.vec]
vec_sum_is_zero [lemma, in Undecidability.Vec.vec]
vec_sum_one [lemma, in Undecidability.Vec.vec]
vec_sum_zero [lemma, in Undecidability.Vec.vec]
vec_sum_plus [lemma, in Undecidability.Vec.vec]
vec_sum [definition, in Undecidability.Vec.vec]
vec_change_pred [lemma, in Undecidability.Vec.vec]
vec_change_succ [lemma, in Undecidability.Vec.vec]
vec_plus_cons [lemma, in Undecidability.Vec.vec]
vec_one_nxt [lemma, in Undecidability.Vec.vec]
vec_one_fst [lemma, in Undecidability.Vec.vec]
vec_zero_S [lemma, in Undecidability.Vec.vec]
vec_one_spec_neq [lemma, in Undecidability.Vec.vec]
vec_one_spec_eq [lemma, in Undecidability.Vec.vec]
vec_one [definition, in Undecidability.Vec.vec]
vec_plus_is_zero [lemma, in Undecidability.Vec.vec]
vec_plus_assoc [lemma, in Undecidability.Vec.vec]
vec_plus_comm [lemma, in Undecidability.Vec.vec]
vec_zero_spec [lemma, in Undecidability.Vec.vec]
vec_zero_plus [lemma, in Undecidability.Vec.vec]
vec_pos_plus [lemma, in Undecidability.Vec.vec]
vec_zero [definition, in Undecidability.Vec.vec]
vec_plus [definition, in Undecidability.Vec.vec]
vec_plus.n [variable, in Undecidability.Vec.vec]
vec_plus [section, in Undecidability.Vec.vec]
vec_pos_map [lemma, in Undecidability.Vec.vec]
vec_map [definition, in Undecidability.Vec.vec]
vec_list_inv [lemma, in Undecidability.Vec.vec]
vec_list_length [lemma, in Undecidability.Vec.vec]
vec_list [definition, in Undecidability.Vec.vec]
vec_eq_dec [definition, in Undecidability.Vec.vec]
vec_change_same [lemma, in Undecidability.Vec.vec]
vec_change_idem [lemma, in Undecidability.Vec.vec]
vec_change_neq [lemma, in Undecidability.Vec.vec]
vec_change_eq [lemma, in Undecidability.Vec.vec]
vec_change [definition, in Undecidability.Vec.vec]
vec_pos_set [lemma, in Undecidability.Vec.vec]
vec_set_pos [definition, in Undecidability.Vec.vec]
vec_pos_ext [lemma, in Undecidability.Vec.vec]
vec_pos1 [lemma, in Undecidability.Vec.vec]
vec_pos_tail [lemma, in Undecidability.Vec.vec]
vec_pos0 [lemma, in Undecidability.Vec.vec]
vec_pos [definition, in Undecidability.Vec.vec]
vec_head_tail [lemma, in Undecidability.Vec.vec]
vec_0_nil [lemma, in Undecidability.Vec.vec]
vec_tail [definition, in Undecidability.Vec.vec]
vec_head [definition, in Undecidability.Vec.vec]
vec_split [definition, in Undecidability.Vec.vec]
vec_cons [constructor, in Undecidability.Vec.vec]
vec_nil [constructor, in Undecidability.Vec.vec]
W
writeNatAux [definition, in Undecidability.Utils.utils_string]writeNAux [definition, in Undecidability.Utils.utils_string]
Z
Zero [abbreviation, in Undecidability.Bsm.list_bool]Zero [abbreviation, in Undecidability.Utils.utils_nat]
other
_ /MM/ _ ~~> _ [notation, in Undecidability.MM_EILL]_ /MM/ _ ->> _ [notation, in Undecidability.MM_EILL]
_ // _ ~~> _ [notation, in Undecidability.Bsm.bsm_pcp]
_ // _ ->> _ [notation, in Undecidability.Bsm.bsm_pcp]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Bsm.bsm_pcp]
_ [ _ / _ ] [notation, in Undecidability.Bsm.bsm_pcp]
_ #> _ [notation, in Undecidability.Bsm.bsm_pcp]
_
[notation, in Undecidability.Utils.utils_list] [in Undecidability.Utils.utils_list]
_ ~p _ [notation, in Undecidability.Utils.utils_list]
_ // _ ~~> _ [notation, in Undecidability.Mm.mm_defs]
_ // _ ->> _ [notation, in Undecidability.Mm.mm_defs]
_ // _ -+> _ [notation, in Undecidability.Mm.mm_defs]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Mm.mm_defs]
_ [ _ / _ ] [notation, in Undecidability.Mm.mm_defs]
_ #> _ [notation, in Undecidability.Mm.mm_defs]
_ ; _ ⊦ _ [notation, in Undecidability.Ll.eill]
_ ~p _ [notation, in Undecidability.Ll.eill]
_ // _ -]] _ [notation, in Undecidability.Mm.mm_comp_old]
_ // _ ->> _ [notation, in Undecidability.Mm.mm_comp_old]
_ // _ -+> _ [notation, in Undecidability.Mm.mm_comp_old]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Mm.mm_comp_old]
_ /BSM/ _ ->> _ [notation, in Undecidability.Mm.mm_comp_old]
_ [ _ / _ ] [notation, in Undecidability.Mm.mm_comp_old]
_ #> _ [notation, in Undecidability.Mm.mm_comp_old]
_ /MM/ _ ->> _ [notation, in Undecidability.BSM_MM]
_ /BSM/ _ ->> _ [notation, in Undecidability.BSM_MM]
_ <<= _ [notation, in Undecidability.Prelim.Prelim]
_ el _ [notation, in Undecidability.Prelim.Prelim]
_ ⊢ _ [notation, in Undecidability.Ll.ill]
_ ⊸ _ [notation, in Undecidability.Ll.ill]
_ -o _ [notation, in Undecidability.Ll.ill]
_ ⊕ _ [notation, in Undecidability.Ll.ill]
_ ⊗ _ [notation, in Undecidability.Ll.ill]
_ ﹠ _ [notation, in Undecidability.Ll.ill]
_ & _ [notation, in Undecidability.Ll.ill]
_ ~p _ [notation, in Undecidability.Ll.ill]
_ // _ ↓ [notation, in Undecidability.Bsm.bsm_defs]
_ [ _ / _ ] [notation, in Undecidability.Bsm.bsm_defs]
_ #> _ [notation, in Undecidability.Bsm.bsm_defs]
_ // _ ↓ [notation, in Undecidability.iBPCP_BSM]
_ // _ ~~> _ [notation, in Undecidability.iBPCP_BSM]
_ // _ ->> _ [notation, in Undecidability.iBPCP_BSM]
_ // _ ->> _ [notation, in Undecidability.Mm.mm_utils]
_ // _ -+> _ [notation, in Undecidability.Mm.mm_utils]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Mm.mm_utils]
_ [ _ / _ ] [notation, in Undecidability.Mm.mm_utils]
_ #> _ [notation, in Undecidability.Mm.mm_utils]
_ [ _ / _ ] [notation, in Undecidability.Vec.vec]
_ #> _ [notation, in Undecidability.Vec.vec]
_ ## _ [notation, in Undecidability.Vec.vec]
_ ~p _ [notation, in Undecidability.Ll.eill_mm]
_
_ /MM/ _ ↓ [notation, in Undecidability.Mm.mm_comp]
_ /MM/ _ ~~> _ [notation, in Undecidability.Mm.mm_comp]
_ /MM/ _ ->> _ [notation, in Undecidability.Mm.mm_comp]
_ /MM/ _ -+> _ [notation, in Undecidability.Mm.mm_comp]
_ /BSM/ _ ↓ [notation, in Undecidability.Mm.mm_comp]
_ /BSM/ _ ~~> _ [notation, in Undecidability.Mm.mm_comp]
_ /BSM/ _ ->> _ [notation, in Undecidability.Mm.mm_comp]
_ /BSM/ _ -+> _ [notation, in Undecidability.Mm.mm_comp]
_ /BSM/ _ -1> _ [notation, in Undecidability.Mm.mm_comp]
_ [ _ / _ ] [notation, in Undecidability.Mm.mm_comp]
_ #> _ [notation, in Undecidability.Mm.mm_comp]
_ // _ ->> _ [notation, in Undecidability.Bsm.bsm_utils]
_ // _ -[ _ ]-> _ [notation, in Undecidability.Bsm.bsm_utils]
_ [ _ / _ ] [notation, in Undecidability.Bsm.bsm_utils]
_ #> _ [notation, in Undecidability.Bsm.bsm_utils]
_ / _ [notation, in Undecidability.Definitions]
_ ⪯ _ [notation, in Undecidability.Definitions]
!l _ [notation, in Undecidability.Ll.ill]
! _ [notation, in Undecidability.Ll.ill]
[i _ ] [notation, in Undecidability.Ll.eill]
| _ | [notation, in Undecidability.Prelim.Prelim]
‼ _ [notation, in Undecidability.Ll.ill]
∅ [notation, in Undecidability.Ll.ill]
❗ _ [notation, in Undecidability.Ll.ill]
⟘ [notation, in Undecidability.Ll.ill]
⟙ [notation, in Undecidability.Ll.ill]
£ [notation, in Undecidability.Ll.ill]
𝝐 [abbreviation, in Undecidability.Ll.ill]
Notation Index
B
_ // _ ->> _ [in Undecidability.Bsm.bsm_defs]
_ // _ -[ _ ]-> _ [in Undecidability.Bsm.bsm_defs]
_ // _ -1> _ [in Undecidability.Bsm.bsm_defs]
C
_ ⋈ _ [in Undecidability.Code.compiler_correction]
_ /Y/ _ ↓ [in Undecidability.Code.compiler_correction]
_ /Y/ _ ~~> _ [in Undecidability.Code.compiler_correction]
_ /Y/ _ ->> _ [in Undecidability.Code.compiler_correction]
_ /Y/ _ -+> _ [in Undecidability.Code.compiler_correction]
_ /Y/ _ -[ _ ]-> _ [in Undecidability.Code.compiler_correction]
_ /Y/ _ -1> _ [in Undecidability.Code.compiler_correction]
_ /X/ _ ↓ [in Undecidability.Code.compiler_correction]
_ /X/ _ ~~> _ [in Undecidability.Code.compiler_correction]
_ /X/ _ ->> _ [in Undecidability.Code.compiler_correction]
_ /X/ _ -+> _ [in Undecidability.Code.compiler_correction]
_ /X/ _ -[ _ ]-> _ [in Undecidability.Code.compiler_correction]
_ /X/ _ -1> _ [in Undecidability.Code.compiler_correction]
D
_ ⪯T _ [in Undecidability.UNDEC]
G
[< _ |- _ >] [in Undecidability.Ll.eill]
⟦ _ ⟧ [in Undecidability.Ll.eill]
M
_ // _ ->> _ [in Undecidability.Mm.mm_defs]
_ // _ -+> _ [in Undecidability.Mm.mm_defs]
_ // _ -[ _ ]-> _ [in Undecidability.Mm.mm_defs]
_ // _ -1> _ [in Undecidability.Mm.mm_defs]
_ // _ ->> _ [in Undecidability.Ll.eill_mm]
_ // _ -[ _ ]-> _ [in Undecidability.Ll.eill_mm]
[[ _ ]] [in Undecidability.Ll.eill_mm]
S
_ ⋈ _ [in Undecidability.Mm.mm_comp]
_ // _ -]] _ [in Undecidability.Code.sss]
_ // _ ↓ [in Undecidability.Code.sss]
_ // _ ~~> _ [in Undecidability.Code.sss]
_ // _ ->> _ [in Undecidability.Code.sss]
_ // _ -+> _ [in Undecidability.Code.sss]
_ // _ -[ _ ]-> _ [in Undecidability.Code.sss]
_ // _ :1> _ [in Undecidability.Code.sss]
_ ⟬ _ ⦒ _ [in Undecidability.Code.sss]
_ // _ -1> _ [in Undecidability.Code.sss]
_
T
[< _ |- _ >] [in Undecidability.Ll.ill]
[[ _ ]] [in Undecidability.Ll.ill]
⟦ _ ⟧ [in Undecidability.Ll.ill]
_ -* _ [in Undecidability.Ll.ill]
_ ** _ [in Undecidability.Ll.ill]
other
_ /MM/ _ ~~> _ [in Undecidability.MM_EILL]
_ /MM/ _ ->> _ [in Undecidability.MM_EILL]
_ // _ ~~> _ [in Undecidability.Bsm.bsm_pcp]
_ // _ ->> _ [in Undecidability.Bsm.bsm_pcp]
_ // _ -[ _ ]-> _ [in Undecidability.Bsm.bsm_pcp]
_ [ _ / _ ] [in Undecidability.Bsm.bsm_pcp]
_ #> _ [in Undecidability.Bsm.bsm_pcp]
_
_ ~p _ [in Undecidability.Utils.utils_list]
_ // _ ~~> _ [in Undecidability.Mm.mm_defs]
_ // _ ->> _ [in Undecidability.Mm.mm_defs]
_ // _ -+> _ [in Undecidability.Mm.mm_defs]
_ // _ -[ _ ]-> _ [in Undecidability.Mm.mm_defs]
_ [ _ / _ ] [in Undecidability.Mm.mm_defs]
_ #> _ [in Undecidability.Mm.mm_defs]
_ ; _ ⊦ _ [in Undecidability.Ll.eill]
_ ~p _ [in Undecidability.Ll.eill]
_ // _ -]] _ [in Undecidability.Mm.mm_comp_old]
_ // _ ->> _ [in Undecidability.Mm.mm_comp_old]
_ // _ -+> _ [in Undecidability.Mm.mm_comp_old]
_ // _ -[ _ ]-> _ [in Undecidability.Mm.mm_comp_old]
_ /BSM/ _ ->> _ [in Undecidability.Mm.mm_comp_old]
_ [ _ / _ ] [in Undecidability.Mm.mm_comp_old]
_ #> _ [in Undecidability.Mm.mm_comp_old]
_ /MM/ _ ->> _ [in Undecidability.BSM_MM]
_ /BSM/ _ ->> _ [in Undecidability.BSM_MM]
_ <<= _ [in Undecidability.Prelim.Prelim]
_ el _ [in Undecidability.Prelim.Prelim]
_ ⊢ _ [in Undecidability.Ll.ill]
_ ⊸ _ [in Undecidability.Ll.ill]
_ -o _ [in Undecidability.Ll.ill]
_ ⊕ _ [in Undecidability.Ll.ill]
_ ⊗ _ [in Undecidability.Ll.ill]
_ ﹠ _ [in Undecidability.Ll.ill]
_ & _ [in Undecidability.Ll.ill]
_ ~p _ [in Undecidability.Ll.ill]
_ // _ ↓ [in Undecidability.Bsm.bsm_defs]
_ [ _ / _ ] [in Undecidability.Bsm.bsm_defs]
_ #> _ [in Undecidability.Bsm.bsm_defs]
_ // _ ↓ [in Undecidability.iBPCP_BSM]
_ // _ ~~> _ [in Undecidability.iBPCP_BSM]
_ // _ ->> _ [in Undecidability.iBPCP_BSM]
_ // _ ->> _ [in Undecidability.Mm.mm_utils]
_ // _ -+> _ [in Undecidability.Mm.mm_utils]
_ // _ -[ _ ]-> _ [in Undecidability.Mm.mm_utils]
_ [ _ / _ ] [in Undecidability.Mm.mm_utils]
_ #> _ [in Undecidability.Mm.mm_utils]
_ [ _ / _ ] [in Undecidability.Vec.vec]
_ #> _ [in Undecidability.Vec.vec]
_ ## _ [in Undecidability.Vec.vec]
_ ~p _ [in Undecidability.Ll.eill_mm]
_
_ /MM/ _ ↓ [in Undecidability.Mm.mm_comp]
_ /MM/ _ ~~> _ [in Undecidability.Mm.mm_comp]
_ /MM/ _ ->> _ [in Undecidability.Mm.mm_comp]
_ /MM/ _ -+> _ [in Undecidability.Mm.mm_comp]
_ /BSM/ _ ↓ [in Undecidability.Mm.mm_comp]
_ /BSM/ _ ~~> _ [in Undecidability.Mm.mm_comp]
_ /BSM/ _ ->> _ [in Undecidability.Mm.mm_comp]
_ /BSM/ _ -+> _ [in Undecidability.Mm.mm_comp]
_ /BSM/ _ -1> _ [in Undecidability.Mm.mm_comp]
_ [ _ / _ ] [in Undecidability.Mm.mm_comp]
_ #> _ [in Undecidability.Mm.mm_comp]
_ // _ ->> _ [in Undecidability.Bsm.bsm_utils]
_ // _ -[ _ ]-> _ [in Undecidability.Bsm.bsm_utils]
_ [ _ / _ ] [in Undecidability.Bsm.bsm_utils]
_ #> _ [in Undecidability.Bsm.bsm_utils]
_ / _ [in Undecidability.Definitions]
_ ⪯ _ [in Undecidability.Definitions]
!l _ [in Undecidability.Ll.ill]
! _ [in Undecidability.Ll.ill]
[i _ ] [in Undecidability.Ll.eill]
| _ | [in Undecidability.Prelim.Prelim]
‼ _ [in Undecidability.Ll.ill]
∅ [in Undecidability.Ll.ill]
❗ _ [in Undecidability.Ll.ill]
⟘ [in Undecidability.Ll.ill]
⟙ [in Undecidability.Ll.ill]
£ [in Undecidability.Ll.ill]
Module Index
D
Def_of_undec [in Undecidability.UNDEC]
Variable Index
B
Binary_Stack_Machine.n [in Undecidability.Bsm.bsm_defs]
Binary_Stack_Machines.simulator.main_loop.C2_eq [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.iter_f_v [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.main_loop_complete_rec [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.main_loop_sound_rec [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.HP2 [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.HP1 [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.Hp [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.HC [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.C1 [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.C2 [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.Hf [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.f [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.spec [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.pre [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.lFD [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.p [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_loop.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_init.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.increment_erase.p [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.increment_erase.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.lt [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hhl [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hal [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hah [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hsl [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hsh [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.Hsa [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.l [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.h [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.a [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.s [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.decoder_error [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.q [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.p [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.Hhl [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.Hcl [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.Hch [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.l [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.h [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder.c [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.increment.Hxy [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.increment.y [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.increment.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.q [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.p [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.Hxy [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.y [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.low [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.high [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.Hxy [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.y [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.half_tile.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.cs_spec_rec [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.x' [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.q [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.p [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.Hxy [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.y [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.Hyz [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.Hxz [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.Hxy [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.z [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.y [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.y' [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.Hyz [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.Hxz [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.Hxy [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.z [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.y [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.y' [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.Hxy [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.y [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.empty_stack.i [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.empty_stack.x [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.n [in Undecidability.Bsm.bsm_utils]
BSM_MM_HALTING.f [in Undecidability.BSM_MM]
C
compiler.bsm_end_sim [in Undecidability.Mm.mm_comp_old]
compiler.bsm_comp_sim [in Undecidability.Mm.mm_comp_old]
compiler.bsm_end_spec [in Undecidability.Mm.mm_comp_old]
compiler.bsm_end [in Undecidability.Mm.mm_comp_old]
compiler.bsm_enc_0 [in Undecidability.Mm.mm_comp_old]
compiler.err [in Undecidability.Mm.mm_comp_old]
compiler.Hc1 [in Undecidability.Mm.mm_comp_old]
compiler.Hreg [in Undecidability.Mm.mm_comp_old]
compiler.Hvr1 [in Undecidability.Mm.mm_comp_old]
compiler.Hvr2 [in Undecidability.Mm.mm_comp_old]
compiler.Hv12 [in Undecidability.Mm.mm_comp_old]
compiler.length_nullify [in Undecidability.Mm.mm_comp_old]
compiler.m [in Undecidability.Mm.mm_comp_old]
compiler.n [in Undecidability.Mm.mm_comp_old]
compiler.P [in Undecidability.Mm.mm_comp_old]
compiler.reg [in Undecidability.Mm.mm_comp_old]
compiler.tmp1 [in Undecidability.Mm.mm_comp_old]
compiler.tmp2 [in Undecidability.Mm.mm_comp_old]
comp.correctness.HPQ [in Undecidability.Code.compiler_correction]
comp.correctness.linker [in Undecidability.Code.compiler_correction]
comp.correctness.P [in Undecidability.Code.compiler_correction]
comp.correctness.Q [in Undecidability.Code.compiler_correction]
comp.cP [in Undecidability.Code.compiler_correction]
comp.err [in Undecidability.Code.compiler_correction]
comp.Hicomp [in Undecidability.Code.compiler_correction]
comp.Hilen [in Undecidability.Code.compiler_correction]
comp.icomp [in Undecidability.Code.compiler_correction]
comp.ilen [in Undecidability.Code.compiler_correction]
comp.iP [in Undecidability.Code.compiler_correction]
comp.iQ [in Undecidability.Code.compiler_correction]
comp.P [in Undecidability.Code.compiler_correction]
comp.P_eq [in Undecidability.Code.compiler_correction]
comp.simul [in Undecidability.Code.compiler_correction]
comp.state_Y [in Undecidability.Code.compiler_correction]
comp.state_X [in Undecidability.Code.compiler_correction]
comp.step_Y_fun [in Undecidability.Code.compiler_correction]
comp.step_X_tot [in Undecidability.Code.compiler_correction]
comp.step_Y [in Undecidability.Code.compiler_correction]
comp.step_X [in Undecidability.Code.compiler_correction]
comp.X [in Undecidability.Code.compiler_correction]
comp.Y [in Undecidability.Code.compiler_correction]
F
fix_X.X [in Undecidability.Prelim.Prelim]
G
g_eill_complete.Hvalid [in Undecidability.Ll.eill]
g_eill_complete.x [in Undecidability.Ll.eill]
g_eill_complete.w_surj [in Undecidability.Ll.eill]
g_eill_complete.Hw [in Undecidability.Ll.eill]
g_eill_complete.w [in Undecidability.Ll.eill]
g_eill_complete.n [in Undecidability.Ll.eill]
g_eill_complete.Hvv2 [in Undecidability.Ll.eill]
g_eill_complete.Hvv1 [in Undecidability.Ll.eill]
g_eill_complete.vv [in Undecidability.Ll.eill]
g_eill_complete.Ga [in Undecidability.Ll.eill]
g_eill_complete.Si [in Undecidability.Ll.eill]
g_eill_complete_bound.s [in Undecidability.Ll.eill]
g_eill_complete_bound.Hrx [in Undecidability.Ll.eill]
g_eill_complete_bound.rx [in Undecidability.Ll.eill]
g_eill_complete_bound.w_surj [in Undecidability.Ll.eill]
g_eill_complete_bound.w [in Undecidability.Ll.eill]
g_eill_complete_bound.n [in Undecidability.Ll.eill]
g_eill_complete_bound.Ga [in Undecidability.Ll.eill]
g_eill_complete_bound.Si [in Undecidability.Ll.eill]
I
iBPCP_BSM_HALTING.f [in Undecidability.iBPCP_BSM]
itau.P [in Undecidability.Definitions]
iter.f [in Undecidability.Utils.utils_list]
iter.X [in Undecidability.Utils.utils_list]
L
length.X [in Undecidability.Utils.utils_list]
linker.c [in Undecidability.Code.compiler]
linker.comp.lnk [in Undecidability.Code.compiler]
linker.err [in Undecidability.Code.compiler]
linker.Hc [in Undecidability.Code.compiler]
linker.i [in Undecidability.Code.compiler]
linker.lc [in Undecidability.Code.compiler]
linker.linker_in_code.Hlc [in Undecidability.Code.compiler]
linker.P [in Undecidability.Code.compiler]
linker.X [in Undecidability.Code.compiler]
linker.Y [in Undecidability.Code.compiler]
list_first_dec.Pdec [in Undecidability.Utils.utils_list]
list_first_dec.P [in Undecidability.Utils.utils_list]
list_first_dec.X [in Undecidability.Utils.utils_list]
list_assoc.eq_X_dec [in Undecidability.Utils.utils_list]
list_assoc.Y [in Undecidability.Utils.utils_list]
list_assoc.X [in Undecidability.Utils.utils_list]
list_injective.HP1 [in Undecidability.Utils.utils_list]
list_injective.HP0 [in Undecidability.Utils.utils_list]
list_injective.P [in Undecidability.Utils.utils_list]
list_injective.X [in Undecidability.Utils.utils_list]
list_bool_succ_rect.list_bool_succ_rec [in Undecidability.Bsm.list_bool]
list_bool_succ_rect.HPS [in Undecidability.Bsm.list_bool]
list_bool_succ_rect.HP0 [in Undecidability.Bsm.list_bool]
list_bool_succ_rect.P [in Undecidability.Bsm.list_bool]
list_bool_next.list_bool_next_def [in Undecidability.Bsm.list_bool]
M
map.f [in Undecidability.Utils.utils_list]
map.X [in Undecidability.Utils.utils_list]
map.Y [in Undecidability.Utils.utils_list]
Minsky_Machine.n [in Undecidability.Mm.mm_defs]
Minsky_Machine_utils.pop.src' [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.e [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.k [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.j [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.i [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.H2z [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.H1z [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.H12 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.Hsz [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.Hs2 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.Hs1 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.zero [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.tmp2 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.tmp1 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.pop.src [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.i [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.Htz [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.Hsz [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.Hst [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.zero [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.tmp [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push.src [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.mm_mul2_spec [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.dst' [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.i [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.Hdz [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.Hsz [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.Hsd [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.zero [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.dst [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2.src [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.mm_div2_spec_1 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.mm_div2_spec_0 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.i [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.Hqr [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.Hsr [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.Hsq [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.rem [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.quo [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2.src [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.mm_transfert_spec [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.Hdz [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.Hsz [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.Hsd [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.zero [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.dst [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert.src [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_nullify.zero [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null.mm_null_spec [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null.Hsz [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null.zero [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null.src [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.n [in Undecidability.Mm.mm_utils]
Minsky.Hk [in Undecidability.Ll.eill_mm]
Minsky.H_s_ry [in Undecidability.Ll.eill_mm]
Minsky.H_s_rx [in Undecidability.Ll.eill_mm]
Minsky.H_s_q [in Undecidability.Ll.eill_mm]
Minsky.H_rx [in Undecidability.Ll.eill_mm]
Minsky.k [in Undecidability.Ll.eill_mm]
Minsky.n [in Undecidability.Ll.eill_mm]
Minsky.P [in Undecidability.Ll.eill_mm]
Minsky.prop_5_2_rec [in Undecidability.Ll.eill_mm]
Minsky.q [in Undecidability.Ll.eill_mm]
Minsky.rx [in Undecidability.Ll.eill_mm]
Minsky.ry [in Undecidability.Ll.eill_mm]
Minsky.sem_k_k_k [in Undecidability.Ll.eill_mm]
Minsky.sem_k [in Undecidability.Ll.eill_mm]
Minsky.sem_y_y_y [in Undecidability.Ll.eill_mm]
Minsky.sem_x_y_y [in Undecidability.Ll.eill_mm]
Minsky.SigI_zero [in Undecidability.Ll.eill_mm]
Minsky.Sig0_zero [in Undecidability.Ll.eill_mm]
MM_HALTING_EILL_PROVABILITY.f [in Undecidability.MM_EILL]
N
nat_sorted.HP2 [in Undecidability.Utils.utils_nat]
nat_sorted.HP1 [in Undecidability.Utils.utils_nat]
nat_sorted.HP0 [in Undecidability.Utils.utils_nat]
nat_sorted.P [in Undecidability.Utils.utils_nat]
N_to_string.loop [in Undecidability.Utils.utils_string]
P
pos_prod.ll_prop [in Undecidability.Vec.pos]
pos_prod.ll [in Undecidability.Vec.pos]
pos_prod.n [in Undecidability.Vec.pos]
pos_invert.pos_invert [in Undecidability.Vec.pos]
pos_invert.pos_invert_t [in Undecidability.Vec.pos]
pos_inv.pos_inv [in Undecidability.Vec.pos]
pos_inv.pos_inv_t [in Undecidability.Vec.pos]
pow2_bound.loop_prop [in Undecidability.Utils.utils_nat]
pow2_bound.loop [in Undecidability.Utils.utils_nat]
prefix.prefix_rect.HP1 [in Undecidability.Utils.utils_list]
prefix.prefix_rect.HP0 [in Undecidability.Utils.utils_list]
prefix.prefix_rect.P [in Undecidability.Utils.utils_list]
prefix.X [in Undecidability.Utils.utils_list]
S
Simulator.a [in Undecidability.Bsm.bsm_pcp]
simulator.bsm_sim.cE_sim [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.cQ_sim [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.E_spec [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.cE [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.cN [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.iE [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.Q_spec2 [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.Q_spec1 [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.w_prop [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.w [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.v [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.HQ2 [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.HQ1 [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.Hlnk [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.Q [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.lnk [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.lnk_Q_pair [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.cP [in Undecidability.Mm.mm_comp]
simulator.bsm_sim.iP [in Undecidability.Mm.mm_comp]
Simulator.h [in Undecidability.Bsm.bsm_pcp]
Simulator.Hah [in Undecidability.Bsm.bsm_pcp]
Simulator.Hal [in Undecidability.Bsm.bsm_pcp]
Simulator.Hhl [in Undecidability.Bsm.bsm_pcp]
simulator.Hreg [in Undecidability.Mm.mm_comp]
Simulator.Hsa [in Undecidability.Bsm.bsm_pcp]
Simulator.Hsh [in Undecidability.Bsm.bsm_pcp]
Simulator.Hsl [in Undecidability.Bsm.bsm_pcp]
Simulator.HS1 [in Undecidability.Bsm.bsm_pcp]
Simulator.HS2 [in Undecidability.Bsm.bsm_pcp]
Simulator.HS3 [in Undecidability.Bsm.bsm_pcp]
simulator.Hvr1 [in Undecidability.Mm.mm_comp]
simulator.Hvr2 [in Undecidability.Mm.mm_comp]
simulator.Hv12 [in Undecidability.Mm.mm_comp]
Simulator.l [in Undecidability.Bsm.bsm_pcp]
Simulator.lML [in Undecidability.Bsm.bsm_pcp]
Simulator.lt [in Undecidability.Bsm.bsm_pcp]
simulator.m [in Undecidability.Mm.mm_comp]
Simulator.n [in Undecidability.Bsm.bsm_pcp]
simulator.n [in Undecidability.Mm.mm_comp]
simulator.reg [in Undecidability.Mm.mm_comp]
Simulator.s [in Undecidability.Bsm.bsm_pcp]
simulator.tmp1 [in Undecidability.Mm.mm_comp]
simulator.tmp2 [in Undecidability.Mm.mm_comp]
Small_Step_Semantics.sss_loop.HP2 [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.HP1 [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.Hp [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.p [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.i [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.HC [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.C2 [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.C1 [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.Hf [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.f [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.spec [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.pre [in Undecidability.Code.sss]
Small_Step_Semantics.sss_loop.P [in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind.HQ1 [in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind.HQ0 [in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind.R [in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind.P [in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind.HR1 [in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind.HR0 [in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind.R [in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind.P [in Undecidability.Code.sss]
Small_Step_Semantics.sss_dec [in Undecidability.Code.sss]
Small_Step_Semantics.sss_fun [in Undecidability.Code.sss]
Small_Step_Semantics.one_step [in Undecidability.Code.sss]
Small_Step_Semantics.data [in Undecidability.Code.sss]
Small_Step_Semantics.instr [in Undecidability.Code.sss]
subcode.Q [in Undecidability.Code.subcode]
subcode.X [in Undecidability.Code.subcode]
T
test.a [in Undecidability.Utils.focus]
test.b [in Undecidability.Utils.focus]
test.c [in Undecidability.Utils.focus]
test.x [in Undecidability.Utils.focus]
test.X [in Undecidability.Utils.focus]
test.y [in Undecidability.Utils.focus]
test.z [in Undecidability.Utils.focus]
TPS.n [in Undecidability.Ll.eill]
TPS.rx [in Undecidability.Ll.eill]
TPS.s [in Undecidability.Ll.eill]
trivial_phase_semantics.s [in Undecidability.Ll.ill]
trivial_phase_semantics.n [in Undecidability.Ll.ill]
V
vector.eq_X_dec [in Undecidability.Vec.vec]
vector.vec_head_tail_prop [in Undecidability.Vec.vec]
vector.vec_head_tail_type [in Undecidability.Vec.vec]
vector.vec_split_type [in Undecidability.Vec.vec]
vector.X [in Undecidability.Vec.vec]
vec_map_list.X [in Undecidability.Vec.vec]
vec_nat_induction.HP2 [in Undecidability.Vec.vec]
vec_nat_induction.HP1 [in Undecidability.Vec.vec]
vec_nat_induction.HP0 [in Undecidability.Vec.vec]
vec_nat_induction.P [in Undecidability.Vec.vec]
vec_nat_induction.n [in Undecidability.Vec.vec]
vec_plus.n [in Undecidability.Vec.vec]
Library Index
B
BPCP_iBPCP
bsm_defs
BSM_MM
bsm_utils
bsm_pcp
C
compiler
compiler_correction
D
Definitions
E
eill
EILL_ILL
eill_mm
F
focus
I
iBPCP_BSM
ill
L
list_bool
list_focus
M
mm_comp
mm_utils
mm_comp_old
MM_EILL
mm_defs
P
PCP_BPCP
pos
Prelim
S
sss
subcode
T
tiles_solvable
U
UNDEC
utils
utils_tac
utils_nat
utils_list
utils_string
V
vec
Lemma Index
A
app_incl_R [in Undecidability.Prelim.Prelim]
app_incl_l [in Undecidability.Prelim.Prelim]
B
bic_POP_Zero_inv [in Undecidability.Mm.mm_comp_old]
bic_POP_One_inv [in Undecidability.Mm.mm_comp_old]
bic_POP_void_inv [in Undecidability.Mm.mm_comp_old]
bic_PUSH_One_inv [in Undecidability.Mm.mm_comp_old]
bic_PUSH_Zero_inv [in Undecidability.Mm.mm_comp_old]
bic_POP_One [in Undecidability.Mm.mm_comp_old]
bic_POP_Zero [in Undecidability.Mm.mm_comp_old]
bic_POP_void [in Undecidability.Mm.mm_comp_old]
bic_PUSH_One [in Undecidability.Mm.mm_comp_old]
bic_PUSH_Zero [in Undecidability.Mm.mm_comp_old]
bitstring_false [in Undecidability.PCP_BPCP]
BPCP_iBPCP [in Undecidability.BPCP_iBPCP]
bsm_simulator_correct [in Undecidability.Mm.mm_comp_old]
bsm_compiler_correct2 [in Undecidability.Mm.mm_comp_old]
bsm_compiler_correct1 [in Undecidability.Mm.mm_comp_old]
bsm_compiler_complete [in Undecidability.Mm.mm_comp_old]
bsm_instr_compiler_complete [in Undecidability.Mm.mm_comp_old]
bsm_compiler_sound [in Undecidability.Mm.mm_comp_old]
bsm_instr_compiler_sound [in Undecidability.Mm.mm_comp_old]
bsm_linker_out_err [in Undecidability.Mm.mm_comp_old]
bsm_linker_out_code [in Undecidability.Mm.mm_comp_old]
bsm_linker_start [in Undecidability.Mm.mm_comp_old]
bsm_coherence [in Undecidability.Mm.mm_comp_old]
bsm_compiler_length [in Undecidability.Mm.mm_comp_old]
bsm_instr_compile_length_geq [in Undecidability.Mm.mm_comp_old]
bsm_instr_compile_length_eq [in Undecidability.Mm.mm_comp_old]
BSM_MM_HALTING [in Undecidability.BSM_MM]
bsm_steps_PUSH_inv [in Undecidability.Bsm.bsm_defs]
bsm_steps_POP_E_inv [in Undecidability.Bsm.bsm_defs]
bsm_steps_POP_any_inv [in Undecidability.Bsm.bsm_defs]
bsm_steps_POP_1_inv [in Undecidability.Bsm.bsm_defs]
bsm_steps_POP_0_inv [in Undecidability.Bsm.bsm_defs]
bsm_compute_PUSH [in Undecidability.Bsm.bsm_defs]
bsm_compute_POP_any [in Undecidability.Bsm.bsm_defs]
bsm_compute_POP_1 [in Undecidability.Bsm.bsm_defs]
bsm_compute_POP_0 [in Undecidability.Bsm.bsm_defs]
bsm_compute_POP_E [in Undecidability.Bsm.bsm_defs]
bsm_sss_stall [in Undecidability.Bsm.bsm_defs]
bsm_sss_total' [in Undecidability.Bsm.bsm_defs]
bsm_sss_total [in Undecidability.Bsm.bsm_defs]
bsm_sss_fun [in Undecidability.Bsm.bsm_defs]
bsm_mm_spec [in Undecidability.Mm.mm_comp]
bsm_instr_compile_sound [in Undecidability.Mm.mm_comp]
bsm_instr_compile_length_geq [in Undecidability.Mm.mm_comp]
bsm_instr_compile_length_eq [in Undecidability.Mm.mm_comp]
C
compare_stack_spec [in Undecidability.Bsm.bsm_utils]
compare_stack_neq_spec [in Undecidability.Bsm.bsm_utils]
compare_stack_eq_spec [in Undecidability.Bsm.bsm_utils]
compare_stacks_length [in Undecidability.Bsm.bsm_utils]
compiler_subcode [in Undecidability.Code.compiler]
compiler_length [in Undecidability.Code.compiler]
compiler_complete' [in Undecidability.Code.compiler_correction]
compiler_complete [in Undecidability.Code.compiler_correction]
compiler_complete_step [in Undecidability.Code.compiler_correction]
compiler_sound [in Undecidability.Code.compiler_correction]
comp_length [in Undecidability.Code.compiler]
comp_app [in Undecidability.Code.compiler]
cons_incl [in Undecidability.Prelim.Prelim]
copy_stack_spec [in Undecidability.Bsm.bsm_utils]
copy_stack_length [in Undecidability.Bsm.bsm_utils]
copy_rev_stack_spec [in Undecidability.Bsm.bsm_utils]
countSplit [in Undecidability.Prelim.Prelim]
D
decoder_spec_nok_2 [in Undecidability.Bsm.bsm_utils]
decoder_spec_nok_1 [in Undecidability.Bsm.bsm_utils]
decoder_spec_ok [in Undecidability.Bsm.bsm_utils]
decoder_spec_rec [in Undecidability.Bsm.bsm_utils]
decoder_length [in Undecidability.Bsm.bsm_utils]
Def_of_undec.undec_PCP [in Undecidability.UNDEC]
Def_of_undec.undec_compl [in Undecidability.UNDEC]
Def_of_undec.red_undec [in Undecidability.UNDEC]
Def_of_undec.red_turing [in Undecidability.UNDEC]
div2_spec [in Undecidability.Utils.utils_nat]
E
EILL_ILL_PROVABILITY [in Undecidability.EILL_ILL]
el_pos [in Undecidability.Prelim.Prelim]
empty_stack_spec [in Undecidability.Bsm.bsm_utils]
empty_stack_length [in Undecidability.Bsm.bsm_utils]
F
find_pow2_prop [in Undecidability.Utils.utils_nat]
find_pow2_geq [in Undecidability.Utils.utils_nat]
flat_map_app [in Undecidability.Utils.utils_list]
Forall_rev [in Undecidability.Utils.utils_list]
Forall_app [in Undecidability.Utils.utils_list]
Forall2_Forall [in Undecidability.Utils.utils_list]
Forall2_map_both [in Undecidability.Utils.utils_list]
Forall2_map_right [in Undecidability.Utils.utils_list]
Forall2_map_left [in Undecidability.Utils.utils_list]
Forall2_cons_inv_r [in Undecidability.Utils.utils_list]
Forall2_cons_inv_l [in Undecidability.Utils.utils_list]
Forall2_app_inv_r [in Undecidability.Utils.utils_list]
Forall2_app_inv_l [in Undecidability.Utils.utils_list]
Forall2_cons_inv [in Undecidability.Utils.utils_list]
Forall2_nil_inv_r [in Undecidability.Utils.utils_list]
Forall2_nil_inv_l [in Undecidability.Utils.utils_list]
Forall2_mono [in Undecidability.Utils.utils_list]
full_decoder_ko_spec [in Undecidability.Bsm.bsm_utils]
full_dec_spec_rec2 [in Undecidability.Bsm.bsm_utils]
full_dec_spec_rec1 [in Undecidability.Bsm.bsm_utils]
full_decoder_ok_spec [in Undecidability.Bsm.bsm_utils]
full_dec_spec_rec [in Undecidability.Bsm.bsm_utils]
full_dec_start_spec_1 [in Undecidability.Bsm.bsm_utils]
full_dec_start_spec_0 [in Undecidability.Bsm.bsm_utils]
full_decoder_length [in Undecidability.Bsm.bsm_utils]
f_g_subset [in Undecidability.PCP_BPCP]
f_subset [in Undecidability.PCP_BPCP]
f_g_s'_inv [in Undecidability.PCP_BPCP]
f_s_app [in Undecidability.PCP_BPCP]
G
gen_compiler_correction [in Undecidability.Code.compiler_correction]
gen_compiler_terminates [in Undecidability.Code.compiler_correction]
gen_compiler_output [in Undecidability.Code.compiler_correction]
gen_compiler_complete [in Undecidability.Code.compiler_correction]
gen_compiler_sound [in Undecidability.Code.compiler_correction]
gen_linker_out [in Undecidability.Code.compiler_correction]
G_eill_correct [in Undecidability.Ll.eill]
G_eill_complete [in Undecidability.Ll.eill]
G_eill_complete_bound [in Undecidability.Ll.eill]
G_eill_sound [in Undecidability.Ll.eill]
g_eill_mono_Si [in Undecidability.Ll.eill]
g_s'_app [in Undecidability.PCP_BPCP]
G_eill_mm [in Undecidability.Ll.eill_mm]
H
half_tile_spec [in Undecidability.Bsm.bsm_utils]
half_tile_length [in Undecidability.Bsm.bsm_utils]
I
iBPCP_BSM_HALTING [in Undecidability.iBPCP_BSM]
ILL_undec [in Undecidability.UNDEC]
incl_sing [in Undecidability.Prelim.Prelim]
incl_nil [in Undecidability.Prelim.Prelim]
increment_erase_spec [in Undecidability.Bsm.bsm_utils]
increment_erase_length [in Undecidability.Bsm.bsm_utils]
increment_spec [in Undecidability.Bsm.bsm_utils]
increment_spec_2 [in Undecidability.Bsm.bsm_utils]
increment_spec_1 [in Undecidability.Bsm.bsm_utils]
increment_length [in Undecidability.Bsm.bsm_utils]
interval_dec [in Undecidability.Utils.utils_nat]
In_list_assoc [in Undecidability.Utils.utils_list]
in_prefix_1 [in Undecidability.Utils.utils_list]
in_prefix_0 [in Undecidability.Utils.utils_list]
In_perm [in Undecidability.Utils.utils_list]
In_list_repeat [in Undecidability.Utils.utils_list]
in_list_injective_1 [in Undecidability.Utils.utils_list]
in_list_injective_0 [in Undecidability.Utils.utils_list]
in_omap_iff [in Undecidability.Prelim.Prelim]
in_sss_step [in Undecidability.Code.sss]
in_code_subcode [in Undecidability.Code.subcode]
in_out_code_dec [in Undecidability.Code.subcode]
in_out_code [in Undecidability.Code.subcode]
in_nat_sorted_3 [in Undecidability.Utils.utils_nat]
in_nat_sorted_2 [in Undecidability.Utils.utils_nat]
in_nat_sorted_1 [in Undecidability.Utils.utils_nat]
in_nat_sorted_0 [in Undecidability.Utils.utils_nat]
itau_tau2 [in Undecidability.BPCP_iBPCP]
itau_tau1 [in Undecidability.BPCP_iBPCP]
itau1_app [in Undecidability.Definitions]
itau2_app [in Undecidability.Definitions]
iter_plus [in Undecidability.Utils.utils_list]
iter_list_bool_next_nil [in Undecidability.Bsm.list_bool]
L
last_app_eq [in Undecidability.Prelim.Prelim]
lemma_5_3 [in Undecidability.Ll.eill_mm]
lemma_5_5 [in Undecidability.Ll.eill_mm]
length_cons [in Undecidability.Utils.utils_list]
length_nil [in Undecidability.Utils.utils_list]
length_compiler_app [in Undecidability.Code.compiler]
length_decoder_size [in Undecidability.Bsm.bsm_utils]
length_copy_rev_stack [in Undecidability.Bsm.bsm_utils]
length_move_rev_stack [in Undecidability.Bsm.bsm_utils]
linker_out_err [in Undecidability.Code.compiler]
linker_out_code [in Undecidability.Code.compiler]
linker_code_end [in Undecidability.Code.compiler]
linker_middle [in Undecidability.Code.compiler]
linker_code_start [in Undecidability.Code.compiler]
linker_in_code [in Undecidability.Code.compiler]
linker_err_code [in Undecidability.Code.compiler]
linker_app [in Undecidability.Code.compiler]
link_fst [in Undecidability.Code.compiler]
link_app [in Undecidability.Code.compiler]
list_first_dec [in Undecidability.Utils.utils_list]
list_choose_dec [in Undecidability.Utils.utils_list]
list_assoc_app [in Undecidability.Utils.utils_list]
list_assoc_In [in Undecidability.Utils.utils_list]
list_assoc_neq [in Undecidability.Utils.utils_list]
list_assoc_eq [in Undecidability.Utils.utils_list]
list_split_middle [in Undecidability.Utils.utils_list]
list_pick [in Undecidability.Utils.utils_list]
list_split_length [in Undecidability.Utils.utils_list]
list_app_inj [in Undecidability.Utils.utils_list]
list_app_cons_eq_inv [in Undecidability.Utils.utils_list]
list_app_eq_inv [in Undecidability.Utils.utils_list]
list_repeat_length [in Undecidability.Utils.utils_list]
list_repeat_plus [in Undecidability.Utils.utils_list]
list_injective_map [in Undecidability.Utils.utils_list]
list_injective_rect [in Undecidability.Utils.utils_list]
list_injective_inv [in Undecidability.Utils.utils_list]
list_an_spec [in Undecidability.Utils.utils_list]
list_an_length [in Undecidability.Utils.utils_list]
list_an_plus [in Undecidability.Utils.utils_list]
list_an_S [in Undecidability.Utils.utils_list]
list_bool_next_total [in Undecidability.Bsm.list_bool]
list_bool_succ_rect [in Undecidability.Bsm.list_bool]
list_bool_succ_nat [in Undecidability.Bsm.list_bool]
list_bool_next_neq_nil [in Undecidability.Bsm.list_bool]
list_bool_succ_neq_nil [in Undecidability.Bsm.list_bool]
list_bool_succ_neq [in Undecidability.Bsm.list_bool]
list_bool_succ_nil [in Undecidability.Bsm.list_bool]
list_bool_succ_fun [in Undecidability.Bsm.list_bool]
list_One_inj [in Undecidability.Bsm.list_bool]
list_One_Zero_not [in Undecidability.Bsm.list_bool]
list_One_Zero_inj [in Undecidability.Bsm.list_bool]
list_bool_nat_ge_1 [in Undecidability.Bsm.list_bool]
list_bool_valid_dec [in Undecidability.Bsm.list_bool]
list_bool_decomp [in Undecidability.Bsm.list_bool]
list_bool_choose_sym [in Undecidability.Bsm.list_bool]
list_bool_choose [in Undecidability.Bsm.list_bool]
list_bool_dec [in Undecidability.Bsm.list_bool]
ll_tps_vec_map_list [in Undecidability.Ll.eill]
ll_tps_vec_map_list_mono [in Undecidability.Ll.eill]
ll_tps_sound [in Undecidability.Ll.ill]
ll_sequent_tps_eq [in Undecidability.Ll.ill]
ll_perm_tps [in Undecidability.Ll.ill]
ll_sequent_tps_mono [in Undecidability.Ll.ill]
ll_tps_perm [in Undecidability.Ll.ill]
ll_tps_list_bang_zero [in Undecidability.Ll.ill]
ll_tps_lbang [in Undecidability.Ll.ill]
ll_tps_app [in Undecidability.Ll.ill]
ll_tps_mult_mono [in Undecidability.Ll.ill]
ll_tps_Sig_zero [in Undecidability.Ll.eill_mm]
lsum_app [in Undecidability.Utils.utils_nat]
M
main_loop_complete [in Undecidability.Bsm.bsm_utils]
main_loop_sound [in Undecidability.Bsm.bsm_utils]
main_loop_ko_spec [in Undecidability.Bsm.bsm_utils]
main_loop_ok_spec [in Undecidability.Bsm.bsm_utils]
main_loop_size [in Undecidability.Bsm.bsm_utils]
main_loop_length [in Undecidability.Bsm.bsm_utils]
main_init_spec [in Undecidability.Bsm.bsm_utils]
main_init_length [in Undecidability.Bsm.bsm_utils]
map_middle_inv [in Undecidability.Utils.utils_list]
map_app_inv [in Undecidability.Utils.utils_list]
map_cons_inv [in Undecidability.Utils.utils_list]
map_cst_rev [in Undecidability.Utils.utils_list]
map_cst_snoc [in Undecidability.Utils.utils_list]
map_cst_repeat [in Undecidability.Utils.utils_list]
map_list_repeat [in Undecidability.Utils.utils_list]
map_inj [in Undecidability.Prelim.Prelim]
map_vec_map_list [in Undecidability.Vec.vec]
measure_rect [in Undecidability.Utils.utils_tac]
MM_HALTING_EILL_PROVABILITY [in Undecidability.MM_EILL]
mm_steps_DEC_1_inv [in Undecidability.Mm.mm_defs]
mm_steps_DEC_0_inv [in Undecidability.Mm.mm_defs]
mm_steps_INC_inv [in Undecidability.Mm.mm_defs]
mm_compute_DEC_S [in Undecidability.Mm.mm_defs]
mm_progress_DEC_S [in Undecidability.Mm.mm_defs]
mm_compute_DEC_0 [in Undecidability.Mm.mm_defs]
mm_progress_DEC_0 [in Undecidability.Mm.mm_defs]
mm_compute_INC [in Undecidability.Mm.mm_defs]
mm_progress_INC [in Undecidability.Mm.mm_defs]
mm_sss_DEC1_inv [in Undecidability.Mm.mm_defs]
mm_sss_DEC0_inv [in Undecidability.Mm.mm_defs]
mm_sss_INC_inv [in Undecidability.Mm.mm_defs]
mm_sss_total [in Undecidability.Mm.mm_defs]
mm_sss_fun [in Undecidability.Mm.mm_defs]
mm_pop_One_progress [in Undecidability.Mm.mm_utils]
mm_pop_Zero_progress [in Undecidability.Mm.mm_utils]
mm_pop_void_progress [in Undecidability.Mm.mm_utils]
mm_pop_length [in Undecidability.Mm.mm_utils]
mm_push_One_progress [in Undecidability.Mm.mm_utils]
mm_push_One_length [in Undecidability.Mm.mm_utils]
mm_push_Zero_progress [in Undecidability.Mm.mm_utils]
mm_push_Zero_length [in Undecidability.Mm.mm_utils]
mm_mul2_progress [in Undecidability.Mm.mm_utils]
mm_mul2_length [in Undecidability.Mm.mm_utils]
mm_div2_progress_0 [in Undecidability.Mm.mm_utils]
mm_div2_progress_1 [in Undecidability.Mm.mm_utils]
mm_div2_progress [in Undecidability.Mm.mm_utils]
mm_div2_length [in Undecidability.Mm.mm_utils]
mm_transfert_progress [in Undecidability.Mm.mm_utils]
mm_transfert_length [in Undecidability.Mm.mm_utils]
mm_nullify_compute [in Undecidability.Mm.mm_utils]
mm_nullify_length [in Undecidability.Mm.mm_utils]
mm_null_progress [in Undecidability.Mm.mm_utils]
mm_null_length [in Undecidability.Mm.mm_utils]
mm_linstr_enc_spec [in Undecidability.Ll.eill_mm]
mm_linstr_enc_app [in Undecidability.Ll.eill_mm]
move_rev_stack_spec [in Undecidability.Bsm.bsm_utils]
N
nat_sinc_inj [in Undecidability.Utils.utils_nat]
nat_sinc [in Undecidability.Utils.utils_nat]
nat_sort_sorted [in Undecidability.Utils.utils_nat]
nat_sort_eq [in Undecidability.Utils.utils_nat]
nat_sort_length [in Undecidability.Utils.utils_nat]
nat_list_insert_sorted [in Undecidability.Utils.utils_nat]
nat_list_insert_Forall [in Undecidability.Utils.utils_nat]
nat_list_insert_incl [in Undecidability.Utils.utils_nat]
nat_list_insert_length [in Undecidability.Utils.utils_nat]
nat_sorted_injective [in Undecidability.Utils.utils_nat]
nat_sorted_rect [in Undecidability.Utils.utils_nat]
nat_sorted_head_inv [in Undecidability.Utils.utils_nat]
nat_sorted_Forall [in Undecidability.Utils.utils_nat]
nat_sorted_cons_inv [in Undecidability.Utils.utils_nat]
nat_new_spec [in Undecidability.Utils.utils_nat]
nat2pos_pos2nat [in Undecidability.Vec.pos]
notInZero [in Undecidability.Prelim.Prelim]
not_In_list_assoc [in Undecidability.Utils.utils_list]
P
pcp_bsm_complete [in Undecidability.Bsm.bsm_pcp]
pcp_bsm_sound [in Undecidability.Bsm.bsm_pcp]
pcp_bsm_size [in Undecidability.Bsm.bsm_pcp]
PCP_BPCP [in Undecidability.PCP_BPCP]
pm_comp_lift [in Undecidability.Vec.pos]
pm_lift_ext [in Undecidability.Vec.pos]
pm_lift_nxt [in Undecidability.Vec.pos]
pm_lift_fst [in Undecidability.Vec.pos]
pos_length [in Undecidability.Prelim.Prelim]
pos_nth [in Undecidability.Prelim.Prelim]
pos_not_diag_spec [in Undecidability.Vec.pos]
pos_sub2nat [in Undecidability.Vec.pos]
pos_reif_t [in Undecidability.Vec.pos]
pos_reification [in Undecidability.Vec.pos]
pos_list_length [in Undecidability.Vec.pos]
pos_list_prop [in Undecidability.Vec.pos]
pos_S_invert [in Undecidability.Vec.pos]
pos_O_invert [in Undecidability.Vec.pos]
pos2nat_nxt [in Undecidability.Vec.pos]
pos2nat_fst [in Undecidability.Vec.pos]
pos2nat_nat2pos [in Undecidability.Vec.pos]
pos2nat_inj [in Undecidability.Vec.pos]
pos2nat_prop [in Undecidability.Vec.pos]
prefix_app_lft_inv [in Undecidability.Utils.utils_list]
prefix_app_inv [in Undecidability.Utils.utils_list]
prefix_trans [in Undecidability.Utils.utils_list]
prefix_refl [in Undecidability.Utils.utils_list]
prefix_list_inv [in Undecidability.Utils.utils_list]
prefix_inv [in Undecidability.Utils.utils_list]
prefix_app_lft [in Undecidability.Utils.utils_list]
prefix_length [in Undecidability.Utils.utils_list]
prop_5_2 [in Undecidability.Ll.eill_mm]
R
reduces_transitive [in Undecidability.Definitions]
rev_nil [in Undecidability.Prelim.Prelim]
rev_eq [in Undecidability.Prelim.Prelim]
S
Sig_zero [in Undecidability.Ll.eill_mm]
simulator_length [in Undecidability.Bsm.bsm_pcp]
size_induction [in Undecidability.Prelim.Prelim]
sss_loop_complete [in Undecidability.Code.sss]
sss_loop_sound [in Undecidability.Code.sss]
sss_output_fun [in Undecidability.Code.sss]
sss_compute_fun [in Undecidability.Code.sss]
sss_compute_stop [in Undecidability.Code.sss]
sss_steps_stop [in Undecidability.Code.sss]
sss_compute_step_out_inv [in Undecidability.Code.sss]
sss_compute_inv [in Undecidability.Code.sss]
sss_compute_max_ind [in Undecidability.Code.sss]
sss_terminates_ind [in Undecidability.Code.sss]
sss_steps_stall [in Undecidability.Code.sss]
sss_step_stall_inv [in Undecidability.Code.sss]
sss_stall_step_0 [in Undecidability.Code.sss]
sss_stall_step_stall [in Undecidability.Code.sss]
sss_out_step_stall [in Undecidability.Code.sss]
sss_steps_stall_fun [in Undecidability.Code.sss]
sss_steps_stall_inv [in Undecidability.Code.sss]
sss_steps_compute [in Undecidability.Code.sss]
sss_step_in_code [in Undecidability.Code.sss]
sss_progress_trans [in Undecidability.Code.sss]
sss_compute_progress_trans [in Undecidability.Code.sss]
sss_progress_compute_trans [in Undecidability.Code.sss]
sss_compute_trans [in Undecidability.Code.sss]
sss_progress_compute [in Undecidability.Code.sss]
sss_steps_plus_inv [in Undecidability.Code.sss]
sss_steps_fun [in Undecidability.Code.sss]
sss_steps_S_inv' [in Undecidability.Code.sss]
sss_steps_inv [in Undecidability.Code.sss]
sss_steps_S_inv [in Undecidability.Code.sss]
sss_steps_0_inv [in Undecidability.Code.sss]
sss_steps_trans [in Undecidability.Code.sss]
sss_steps_1 [in Undecidability.Code.sss]
sss_steps_0 [in Undecidability.Code.sss]
sss_step_dec [in Undecidability.Code.sss]
sss_step_supcode [in Undecidability.Code.sss]
sss_step_subcode_inv [in Undecidability.Code.sss]
sss_step_fun [in Undecidability.Code.sss]
stack_enc_S [in Undecidability.Mm.mm_utils]
subcode_sss_terminates [in Undecidability.Code.sss]
subcode_sss_steps_stop [in Undecidability.Code.sss]
subcode_sss_steps_inv_1 [in Undecidability.Code.sss]
subcode_sss_subcode_compute_inv [in Undecidability.Code.sss]
subcode_sss_progress_inv [in Undecidability.Code.sss]
subcode_sss_subcode_inv [in Undecidability.Code.sss]
subcode_sss_step_inv_1 [in Undecidability.Code.sss]
subcode_sss_compute_inv [in Undecidability.Code.sss]
subcode_sss_steps_inv [in Undecidability.Code.sss]
subcode_sss_step_inv [in Undecidability.Code.sss]
subcode_sss_compute_instr [in Undecidability.Code.sss]
subcode_sss_compute_linstr [in Undecidability.Code.sss]
subcode_sss_compute_trans [in Undecidability.Code.sss]
subcode_sss_compute [in Undecidability.Code.sss]
subcode_sss_progress [in Undecidability.Code.sss]
subcode_sss_steps [in Undecidability.Code.sss]
subcode_sss_step [in Undecidability.Code.sss]
subcode_mm_linstr_dec [in Undecidability.Ll.eill_mm]
subcode_mm_linstr_enc [in Undecidability.Ll.eill_mm]
subcode_snoc_inv [in Undecidability.Code.subcode]
subcode_cons_inv [in Undecidability.Code.subcode]
subcode_app_inv [in Undecidability.Code.subcode]
subcode_cons [in Undecidability.Code.subcode]
subcode_app_end [in Undecidability.Code.subcode]
subcode_right [in Undecidability.Code.subcode]
subcode_left [in Undecidability.Code.subcode]
subcode_out_code [in Undecidability.Code.subcode]
subcode_in_code [in Undecidability.Code.subcode]
subcode_trans [in Undecidability.Code.subcode]
subcode_refl [in Undecidability.Code.subcode]
subcode_start_in_code [in Undecidability.Code.subcode]
subcode_length_le [in Undecidability.Code.subcode]
subcode_length [in Undecidability.Code.subcode]
S_ill_weak_cntr [in Undecidability.Ll.ill]
S_ill_cntr [in Undecidability.Ll.ill]
S_ill_weak [in Undecidability.Ll.ill]
T
tau_itau2 [in Undecidability.BPCP_iBPCP]
tau_itau1 [in Undecidability.BPCP_iBPCP]
tau1_g [in Undecidability.PCP_BPCP]
tau1_f [in Undecidability.PCP_BPCP]
tau2_g [in Undecidability.PCP_BPCP]
tau2_f [in Undecidability.PCP_BPCP]
tiles_solvable_iBPCP [in Undecidability.iBPCP_BSM]
tile_concat_itau [in Undecidability.iBPCP_BSM]
tile_spec [in Undecidability.Bsm.bsm_utils]
tile_length [in Undecidability.Bsm.bsm_utils]
transfer_ones_spec_2 [in Undecidability.Bsm.bsm_utils]
transfer_ones_spec_1 [in Undecidability.Bsm.bsm_utils]
transfer_ones_length [in Undecidability.Bsm.bsm_utils]
V
vec_map_list_plus [in Undecidability.Vec.vec]
vec_map_list_one [in Undecidability.Vec.vec]
vec_map_list_zero [in Undecidability.Vec.vec]
vec_nat_induction [in Undecidability.Vec.vec]
vec_sum_is_nzero [in Undecidability.Vec.vec]
vec_sum_is_zero [in Undecidability.Vec.vec]
vec_sum_one [in Undecidability.Vec.vec]
vec_sum_zero [in Undecidability.Vec.vec]
vec_sum_plus [in Undecidability.Vec.vec]
vec_change_pred [in Undecidability.Vec.vec]
vec_change_succ [in Undecidability.Vec.vec]
vec_plus_cons [in Undecidability.Vec.vec]
vec_one_nxt [in Undecidability.Vec.vec]
vec_one_fst [in Undecidability.Vec.vec]
vec_zero_S [in Undecidability.Vec.vec]
vec_one_spec_neq [in Undecidability.Vec.vec]
vec_one_spec_eq [in Undecidability.Vec.vec]
vec_plus_is_zero [in Undecidability.Vec.vec]
vec_plus_assoc [in Undecidability.Vec.vec]
vec_plus_comm [in Undecidability.Vec.vec]
vec_zero_spec [in Undecidability.Vec.vec]
vec_zero_plus [in Undecidability.Vec.vec]
vec_pos_plus [in Undecidability.Vec.vec]
vec_pos_map [in Undecidability.Vec.vec]
vec_list_inv [in Undecidability.Vec.vec]
vec_list_length [in Undecidability.Vec.vec]
vec_change_same [in Undecidability.Vec.vec]
vec_change_idem [in Undecidability.Vec.vec]
vec_change_neq [in Undecidability.Vec.vec]
vec_change_eq [in Undecidability.Vec.vec]
vec_pos_set [in Undecidability.Vec.vec]
vec_pos_ext [in Undecidability.Vec.vec]
vec_pos1 [in Undecidability.Vec.vec]
vec_pos_tail [in Undecidability.Vec.vec]
vec_pos0 [in Undecidability.Vec.vec]
vec_head_tail [in Undecidability.Vec.vec]
vec_0_nil [in Undecidability.Vec.vec]
Constructor Index
B
bsm_push [in Undecidability.Bsm.bsm_defs]
bsm_pop [in Undecidability.Bsm.bsm_defs]
D
Def_of_undec.undec_red [in Undecidability.UNDEC]
Def_of_undec.undec_seed [in Undecidability.UNDEC]
Def_of_undec.is_dec [in Undecidability.UNDEC]
I
in_mm_sss_dec_1 [in Undecidability.Mm.mm_defs]
in_mm_sss_dec_0 [in Undecidability.Mm.mm_defs]
in_mm_sss_inc [in Undecidability.Mm.mm_defs]
in_eill_fork [in Undecidability.Ll.eill]
in_eill_dec [in Undecidability.Ll.eill]
in_eill_inc [in Undecidability.Ll.eill]
in_eill_perm [in Undecidability.Ll.eill]
in_eill_ax [in Undecidability.Ll.eill]
in_ll_cmd_fork [in Undecidability.Ll.eill]
in_ll_cmd_dec [in Undecidability.Ll.eill]
in_ll_cmd_inc [in Undecidability.Ll.eill]
in_llp_unit_r [in Undecidability.Ll.ill]
in_llp_unit_l [in Undecidability.Ll.ill]
in_llp_top_r [in Undecidability.Ll.ill]
in_llp_bot_l [in Undecidability.Ll.ill]
in_llp_plus_r2 [in Undecidability.Ll.ill]
in_llp_plus_r1 [in Undecidability.Ll.ill]
in_llp_plus_l [in Undecidability.Ll.ill]
in_llp_times_r [in Undecidability.Ll.ill]
in_llp_times_l [in Undecidability.Ll.ill]
in_llp_cut [in Undecidability.Ll.ill]
in_llp_cntr [in Undecidability.Ll.ill]
in_llp_weak [in Undecidability.Ll.ill]
in_llp_bang_r [in Undecidability.Ll.ill]
in_llp_bang_l [in Undecidability.Ll.ill]
in_llp_with_r [in Undecidability.Ll.ill]
in_llp_with_l2 [in Undecidability.Ll.ill]
in_llp_with_l1 [in Undecidability.Ll.ill]
in_llp_limp_r [in Undecidability.Ll.ill]
in_llp_limp_l [in Undecidability.Ll.ill]
in_llp_perm [in Undecidability.Ll.ill]
in_llp_ax [in Undecidability.Ll.ill]
in_bsm_sss_push [in Undecidability.Bsm.bsm_defs]
in_bsm_sss_pop_1 [in Undecidability.Bsm.bsm_defs]
in_bsm_sss_pop_0 [in Undecidability.Bsm.bsm_defs]
in_bsm_sss_pop_E [in Undecidability.Bsm.bsm_defs]
in_sss_steps_S [in Undecidability.Code.sss]
in_sss_steps_0 [in Undecidability.Code.sss]
in_lbs_1 [in Undecidability.Bsm.list_bool]
in_lbs_0 [in Undecidability.Bsm.list_bool]
L
ll_bin [in Undecidability.Ll.ill]
ll_ban [in Undecidability.Ll.ill]
ll_zero [in Undecidability.Ll.ill]
ll_var [in Undecidability.Ll.ill]
ll_top [in Undecidability.Ll.ill]
ll_bot [in Undecidability.Ll.ill]
ll_one [in Undecidability.Ll.ill]
ll_plus [in Undecidability.Ll.ill]
ll_times [in Undecidability.Ll.ill]
ll_limp [in Undecidability.Ll.ill]
ll_with [in Undecidability.Ll.ill]
M
mm_dec [in Undecidability.Mm.mm_defs]
mm_inc [in Undecidability.Mm.mm_defs]
P
pos_nxt [in Undecidability.Vec.pos]
pos_fst [in Undecidability.Vec.pos]
V
vec_cons [in Undecidability.Vec.vec]
vec_nil [in Undecidability.Vec.vec]
Inductive Index
B
bsm_sss [in Undecidability.Bsm.bsm_defs]
bsm_instr [in Undecidability.Bsm.bsm_defs]
D
Def_of_undec.undec [in Undecidability.UNDEC]
Def_of_undec.dec [in Undecidability.UNDEC]
E
eill_cmd [in Undecidability.Ll.eill]
G
G_eill [in Undecidability.Ll.eill]
L
list_bool_succ [in Undecidability.Bsm.list_bool]
ll_form [in Undecidability.Ll.ill]
ll_cst [in Undecidability.Ll.ill]
ll_conn [in Undecidability.Ll.ill]
M
mm_sss [in Undecidability.Mm.mm_defs]
mm_instr [in Undecidability.Mm.mm_defs]
P
pos [in Undecidability.Vec.pos]
S
sss_steps [in Undecidability.Code.sss]
S_ill [in Undecidability.Ll.ill]
V
vec [in Undecidability.Vec.vec]
Section Index
B
Binary_Stack_Machine [in Undecidability.Bsm.bsm_defs]
Binary_Stack_Machines.simulator.main_loop [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.main_init [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator.increment_erase [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.simulator [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.full_decoder [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.increment [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.transfer_ones [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.tile [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.half_tile [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.compare_stacks [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_stack [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.copy_rev_stack [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.move_rev [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines.empty_stack [in Undecidability.Bsm.bsm_utils]
Binary_Stack_Machines [in Undecidability.Bsm.bsm_utils]
BSM_MM_HALTING [in Undecidability.BSM_MM]
C
comp [in Undecidability.Code.compiler_correction]
compiler [in Undecidability.Mm.mm_comp_old]
comp.correctness [in Undecidability.Code.compiler_correction]
E
EILL_ILL [in Undecidability.EILL_ILL]
F
fix_X [in Undecidability.Prelim.Prelim]
G
g_eill_complete [in Undecidability.Ll.eill]
g_eill_complete_bound [in Undecidability.Ll.eill]
I
iBPCP_BSM_HALTING [in Undecidability.iBPCP_BSM]
itau [in Undecidability.Definitions]
iter [in Undecidability.Utils.utils_list]
L
length [in Undecidability.Utils.utils_list]
linker [in Undecidability.Code.compiler]
linker.comp [in Undecidability.Code.compiler]
linker.linker_in_code [in Undecidability.Code.compiler]
list_first_dec [in Undecidability.Utils.utils_list]
list_assoc [in Undecidability.Utils.utils_list]
list_injective [in Undecidability.Utils.utils_list]
list_an [in Undecidability.Utils.utils_list]
list_bool_succ_rect [in Undecidability.Bsm.list_bool]
list_bool_next [in Undecidability.Bsm.list_bool]
list_bool_succ_props [in Undecidability.Bsm.list_bool]
M
map [in Undecidability.Utils.utils_list]
Minsky [in Undecidability.Ll.eill_mm]
Minsky_Machine [in Undecidability.Mm.mm_defs]
Minsky_Machine_utils.pop [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.push [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mul2 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.div2 [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.transfert [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_nullify [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils.mm_null [in Undecidability.Mm.mm_utils]
Minsky_Machine_utils [in Undecidability.Mm.mm_utils]
MM_HALTING_EILL_PROVABILITY [in Undecidability.MM_EILL]
N
nat_sorted [in Undecidability.Utils.utils_nat]
new [in Undecidability.Utils.utils_nat]
N_to_string [in Undecidability.Utils.utils_string]
P
pos_prod [in Undecidability.Vec.pos]
pos_nat [in Undecidability.Vec.pos]
pos_map [in Undecidability.Vec.pos]
pos_eq_dec [in Undecidability.Vec.pos]
pos_invert [in Undecidability.Vec.pos]
pos_inv [in Undecidability.Vec.pos]
pow2_bound [in Undecidability.Utils.utils_nat]
prefix [in Undecidability.Utils.utils_list]
prefix.prefix_rect [in Undecidability.Utils.utils_list]
S
Simulator [in Undecidability.Bsm.bsm_pcp]
simulator [in Undecidability.Mm.mm_comp]
simulator.bsm_sim [in Undecidability.Mm.mm_comp]
Small_Step_Semantics.sss_loop [in Undecidability.Code.sss]
Small_Step_Semantics.sss_compute_max_ind [in Undecidability.Code.sss]
Small_Step_Semantics.sss_terminates_ind [in Undecidability.Code.sss]
Small_Step_Semantics [in Undecidability.Code.sss]
subcode [in Undecidability.Code.subcode]
T
test [in Undecidability.Utils.focus]
TPS [in Undecidability.Ll.eill]
trivial_phase_semantics [in Undecidability.Ll.ill]
V
vector [in Undecidability.Vec.vec]
vec_map_list [in Undecidability.Vec.vec]
vec_nat_induction [in Undecidability.Vec.vec]
vec_plus [in Undecidability.Vec.vec]
Abbreviation Index
C
code [in Undecidability.Code.sss]
comp [in Undecidability.Mm.mm_comp_old]
cQ [in Undecidability.Code.compiler_correction]
D
DEC [in Undecidability.Mm.mm_defs]
Def_of_undec.compl [in Undecidability.UNDEC]
H
Hc [in Undecidability.Mm.mm_comp_old]
I
INC [in Undecidability.Mm.mm_defs]
L
LL_FORK [in Undecidability.Ll.eill]
LL_DEC [in Undecidability.Ll.eill]
LL_INC [in Undecidability.Ll.eill]
lng [in Undecidability.Mm.mm_comp_old]
lnk [in Undecidability.Mm.mm_comp_old]
lnk [in Undecidability.Code.compiler_correction]
lsum [in Undecidability.Code.compiler]
O
One [in Undecidability.Bsm.list_bool]
One [in Undecidability.Utils.utils_nat]
P
POP [in Undecidability.Bsm.bsm_defs]
pos0 [in Undecidability.Vec.pos]
pos1 [in Undecidability.Vec.pos]
pos10 [in Undecidability.Vec.pos]
pos11 [in Undecidability.Vec.pos]
pos12 [in Undecidability.Vec.pos]
pos13 [in Undecidability.Vec.pos]
pos14 [in Undecidability.Vec.pos]
pos15 [in Undecidability.Vec.pos]
pos16 [in Undecidability.Vec.pos]
pos17 [in Undecidability.Vec.pos]
pos18 [in Undecidability.Vec.pos]
pos19 [in Undecidability.Vec.pos]
pos2 [in Undecidability.Vec.pos]
pos20 [in Undecidability.Vec.pos]
pos3 [in Undecidability.Vec.pos]
pos4 [in Undecidability.Vec.pos]
pos5 [in Undecidability.Vec.pos]
pos6 [in Undecidability.Vec.pos]
pos7 [in Undecidability.Vec.pos]
pos8 [in Undecidability.Vec.pos]
pos9 [in Undecidability.Vec.pos]
PUSH [in Undecidability.Bsm.bsm_defs]
Q
Q [in Undecidability.Mm.mm_comp_old]
S
simulator [in Undecidability.Bsm.bsm_pcp]
state [in Undecidability.Code.sss]
V
vars [in Undecidability.Ll.eill]
vars [in Undecidability.Ll.eill]
Z
Zero [in Undecidability.Bsm.list_bool]
Zero [in Undecidability.Utils.utils_nat]
other
𝝐 [in Undecidability.Ll.ill]
Definition Index
B
BPCP [in Undecidability.Definitions]
bsm_simulator [in Undecidability.Mm.mm_comp_old]
bsm_state_enc [in Undecidability.Mm.mm_comp_old]
bsm_compiler [in Undecidability.Mm.mm_comp_old]
bsm_linker [in Undecidability.Mm.mm_comp_old]
bsm_instr_compile_length [in Undecidability.Mm.mm_comp_old]
bsm_instr_compile [in Undecidability.Mm.mm_comp_old]
BSM_HALTING [in Undecidability.Bsm.bsm_defs]
BSM_PROBLEM [in Undecidability.Bsm.bsm_defs]
bsm_state [in Undecidability.Bsm.bsm_defs]
bsm_mm [in Undecidability.Mm.mm_comp]
bsm_instr_compile_length [in Undecidability.Mm.mm_comp]
bsm_instr_compile [in Undecidability.Mm.mm_comp]
bsm_state_enc [in Undecidability.Mm.mm_comp]
BSRS [in Undecidability.Definitions]
C
card [in Undecidability.Definitions]
card_eq [in Undecidability.BPCP_iBPCP]
code [in Undecidability.Code.subcode]
code_length [in Undecidability.Code.subcode]
code_end [in Undecidability.Code.subcode]
code_start [in Undecidability.Code.subcode]
comp [in Undecidability.Code.compiler]
compare_stacks [in Undecidability.Bsm.bsm_utils]
compiler [in Undecidability.Code.compiler]
copy_stack [in Undecidability.Bsm.bsm_utils]
copy_rev_stack [in Undecidability.Bsm.bsm_utils]
count [in Undecidability.Prelim.Prelim]
D
decoder [in Undecidability.Bsm.bsm_utils]
div2 [in Undecidability.Utils.utils_nat]
div2_2p0 [in Undecidability.Utils.utils_nat]
div2_2p1 [in Undecidability.Utils.utils_nat]
E
EILL_PROVABILITY [in Undecidability.Ll.eill]
EILL_SEQUENT [in Undecidability.Ll.eill]
eill_cmd_map [in Undecidability.Ll.eill]
eill_cmd_vars [in Undecidability.Ll.eill]
empty_stack [in Undecidability.Bsm.bsm_utils]
eqdec [in Undecidability.Utils.utils_tac]
F
f [in Undecidability.BPCP_iBPCP]
f [in Undecidability.PCP_BPCP]
find_pow2 [in Undecidability.Utils.utils_nat]
full_decoder [in Undecidability.Bsm.bsm_utils]
f_c [in Undecidability.PCP_BPCP]
f_s [in Undecidability.PCP_BPCP]
G
g [in Undecidability.BPCP_iBPCP]
g [in Undecidability.PCP_BPCP]
gen_compiler [in Undecidability.Code.compiler_correction]
gen_linker [in Undecidability.Code.compiler_correction]
g_c [in Undecidability.PCP_BPCP]
g_s [in Undecidability.PCP_BPCP]
g_s' [in Undecidability.PCP_BPCP]
H
half_tile [in Undecidability.Bsm.bsm_utils]
I
iBPCP [in Undecidability.Definitions]
ILL_PROVABILITY [in Undecidability.Ll.ill]
increment [in Undecidability.Bsm.bsm_utils]
increment_erase [in Undecidability.Bsm.bsm_utils]
Injective [in Undecidability.Prelim.Prelim]
instruction_compiler_sound [in Undecidability.Code.compiler_correction]
in_code [in Undecidability.Code.subcode]
itau1 [in Undecidability.Definitions]
itau2 [in Undecidability.Definitions]
iter [in Undecidability.Utils.utils_list]
L
length_compiler [in Undecidability.Code.compiler]
length_main_loop [in Undecidability.Bsm.bsm_utils]
length_full_decoder [in Undecidability.Bsm.bsm_utils]
length_decoder [in Undecidability.Bsm.bsm_utils]
link [in Undecidability.Code.compiler]
linker [in Undecidability.Code.compiler]
list_assoc [in Undecidability.Utils.utils_list]
list_repeat [in Undecidability.Utils.utils_list]
list_injective [in Undecidability.Utils.utils_list]
list_an [in Undecidability.Utils.utils_list]
list_vec [in Undecidability.Vec.vec]
list_bool_next_spec [in Undecidability.Bsm.list_bool]
list_bool_next [in Undecidability.Bsm.list_bool]
list_bool_nat [in Undecidability.Bsm.list_bool]
list_bool_invalid [in Undecidability.Bsm.list_bool]
list_bool_valid [in Undecidability.Bsm.list_bool]
list_nat_bool [in Undecidability.Bsm.list_bool]
ll_vars [in Undecidability.Ll.eill]
ll_sequent_tps [in Undecidability.Ll.ill]
ll_tps_list [in Undecidability.Ll.ill]
ll_tps [in Undecidability.Ll.ill]
ll_tps_mult [in Undecidability.Ll.ill]
ll_tps_imp [in Undecidability.Ll.ill]
ll_lbang [in Undecidability.Ll.ill]
ll_vars [in Undecidability.Ll.ill]
lmax [in Undecidability.Utils.utils_nat]
lsum [in Undecidability.Utils.utils_nat]
M
main_loop [in Undecidability.Bsm.bsm_utils]
main_init [in Undecidability.Bsm.bsm_utils]
MM_HALTING [in Undecidability.Mm.mm_defs]
MM_PROBLEM [in Undecidability.Mm.mm_defs]
mm_state [in Undecidability.Mm.mm_defs]
mm_pop [in Undecidability.Mm.mm_utils]
mm_push_One [in Undecidability.Mm.mm_utils]
mm_push_Zero [in Undecidability.Mm.mm_utils]
mm_mul2 [in Undecidability.Mm.mm_utils]
mm_div2 [in Undecidability.Mm.mm_utils]
mm_transfert [in Undecidability.Mm.mm_utils]
mm_nullify [in Undecidability.Mm.mm_utils]
mm_null [in Undecidability.Mm.mm_utils]
mm_linstr_enc [in Undecidability.Ll.eill_mm]
move_rev_stack [in Undecidability.Bsm.bsm_utils]
N
natToDigit [in Undecidability.Utils.utils_string]
nat_pos [in Undecidability.Vec.pos]
nat_sort [in Undecidability.Utils.utils_nat]
nat_list_insert [in Undecidability.Utils.utils_nat]
nat_sorted [in Undecidability.Utils.utils_nat]
nat_new [in Undecidability.Utils.utils_nat]
nat2pos [in Undecidability.Vec.pos]
NToDigit [in Undecidability.Utils.utils_string]
O
omap [in Undecidability.Prelim.Prelim]
out_code [in Undecidability.Code.subcode]
P
PCP [in Undecidability.Definitions]
pcp_bsm [in Undecidability.Bsm.bsm_pcp]
pm_id [in Undecidability.Vec.pos]
pm_comp [in Undecidability.Vec.pos]
pm_lift [in Undecidability.Vec.pos]
pm_ext_eq [in Undecidability.Vec.pos]
pos [in Undecidability.Prelim.Prelim]
pos_not_diag [in Undecidability.Vec.pos]
pos_sub [in Undecidability.Vec.pos]
pos_nat [in Undecidability.Vec.pos]
pos_map [in Undecidability.Vec.pos]
pos_eq_dec [in Undecidability.Vec.pos]
pos_list [in Undecidability.Vec.pos]
pos_O_any [in Undecidability.Vec.pos]
pos_nxt_inj [in Undecidability.Vec.pos]
pos_S_inv [in Undecidability.Vec.pos]
pos_O_inv [in Undecidability.Vec.pos]
pos_iso [in Undecidability.Vec.pos]
pos2nat [in Undecidability.Vec.pos]
pow2 [in Undecidability.Utils.utils_nat]
prefix [in Undecidability.Utils.utils_list]
prefix_spec [in Undecidability.Utils.utils_list]
prefix_rect [in Undecidability.Utils.utils_list]
R
reduces [in Undecidability.Definitions]
S
s [in Undecidability.Ll.eill_mm]
Sig [in Undecidability.Ll.eill_mm]
SigI [in Undecidability.Ll.eill_mm]
Sig0 [in Undecidability.Ll.eill_mm]
size_cards [in Undecidability.Bsm.bsm_utils]
SRS [in Undecidability.Definitions]
sss_compute_max [in Undecidability.Code.sss]
sss_step_stall [in Undecidability.Code.sss]
sss_stall [in Undecidability.Code.sss]
sss_terminates [in Undecidability.Code.sss]
sss_output [in Undecidability.Code.sss]
sss_compute [in Undecidability.Code.sss]
sss_progress [in Undecidability.Code.sss]
sss_step [in Undecidability.Code.sss]
stack [in Undecidability.Definitions]
stack_enc [in Undecidability.Mm.mm_utils]
string [in Undecidability.Definitions]
string_of_nat [in Undecidability.Utils.utils_string]
string_of_N [in Undecidability.Utils.utils_string]
subcode [in Undecidability.Code.subcode]
swap [in Undecidability.Utils.utils_tac]
symbol [in Undecidability.Definitions]
T
tau1 [in Undecidability.Definitions]
tau2 [in Undecidability.Definitions]
tile [in Undecidability.Bsm.bsm_utils]
tiles_solvable [in Undecidability.Bsm.tiles_solvable]
tile_concat [in Undecidability.Bsm.tiles_solvable]
to_bitstring [in Undecidability.PCP_BPCP]
transfer_ones [in Undecidability.Bsm.bsm_utils]
V
vec_map_list [in Undecidability.Vec.vec]
vec_sum [in Undecidability.Vec.vec]
vec_one [in Undecidability.Vec.vec]
vec_zero [in Undecidability.Vec.vec]
vec_plus [in Undecidability.Vec.vec]
vec_map [in Undecidability.Vec.vec]
vec_list [in Undecidability.Vec.vec]
vec_eq_dec [in Undecidability.Vec.vec]
vec_change [in Undecidability.Vec.vec]
vec_set_pos [in Undecidability.Vec.vec]
vec_pos [in Undecidability.Vec.vec]
vec_tail [in Undecidability.Vec.vec]
vec_head [in Undecidability.Vec.vec]
vec_split [in Undecidability.Vec.vec]
W
writeNatAux [in Undecidability.Utils.utils_string]
writeNAux [in Undecidability.Utils.utils_string]
Global Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(1370 entries)
Notation Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(121 entries)
Module Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(1 entry)
Variable Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(369 entries)
Library Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(34 entries)
Lemma Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(461 entries)
Constructor Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(62 entries)
Inductive Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(16 entries)
Section Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(77 entries)
Abbreviation Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(47 entries)
Definition Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(182 entries)