fact: Definition trans' : state' * Vector.t (option Σ) (S n) -> state' * Vector.t (option Σ * move) (S n) := fun '((d, p), bs) => match sval (Fin.to_nat p) with | 0 => match d with | false => ((d, p), TM_facts.nop_action) | true => (toState false 1, Vector.const (Some false, Nmove) (S n)) end | S m' => match nth_error M m' with | None => ((d, p), TM_facts.nop_action) | Some (mm_inc i) => match d with | false => ((true, p), vec_change TM_facts.nop_action i (Some true, Lmove)) | true => (toState false (S (S m')), vec_change TM_facts.nop_action i (Some false, Nmove)) end | Some (mm_dec i q) => match d with | false => ((true, p), vec_change TM_facts.nop_action i (None, Rmove)) | true => match Vector.nth bs i with | Some true => (toState false q, vec_change TM_facts.nop_action i (Some false, Nmove)) | _ => (toState false (S (S m')), vec_change TM_facts.nop_action i (Some false, Nmove)) end end end end.
imports: Undecidability.TM(TM) Undecidability.MinskyMachines(MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL(CompoundFinTypes) Undecidability.Shared.Libs.PSL.EqDec List Lia PeanoNat Compare_dec Relations ssreflect ssrbool ssrfun