proposition: Lemma Fin4_cases (P : pos 4 -> Prop) : P Fin0 -> P Fin1 -> P Fin2 -> P Fin3 -> forall p, P p.
proof: Proof. intros H0 H1 H2 H3. repeat (intros p; eapply (Fin.caseS' p); clear p; [ eauto | ]). intros p. inversion p. Qed.
imports: Undecidability.StackMachines.BSM Undecidability.StackMachines.Util.BSM_computable Undecidability.TM.TM Undecidability.TM.Util.TM_facts Undecidability.TM.Util.TM_computable Undecidability.TM(TM Arbitrary_to_Binary mTM_to_TM HaltTM_1_to_HaltKOSBTM HaltKOSBTM_to_HaltBSM) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Undecidability(bsm_utils bsm_defs) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes)