fact: Definition step' (x: mm2_state) : option mm2_state := match (index x) with | 0 => None | S p => match nth_error M p with | None => None | Some mm2_inc_a => Some (1 + (index x), (1 + (value1 x), (value2 x))) | Some mm2_inc_b => Some (1 + (index x), ((value1 x), 1 + (value2 x))) | Some (mm2_dec_a _) => if value1 x is 0 then Some (1 + (index x), (0, value2 x)) else None | Some (mm2_dec_b _) => if value2 x is 0 then Some (1 + (index x), (value1 x, 0)) else None end end.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun