proposition: Lemma mm2_step_intro {P i p} : mm2_instr_at i p P -> forall a b, mm2_step P (p, (a, b)) match i with | mm2_inc_a => (S p, (S a, b)) | mm2_inc_b => (S p, (a, S b)) | mm2_dec_a q => if a is S a' then (q, (a', b)) else (S p, (0, b)) | mm2_dec_b q => if b is S b' then (q, (a, b')) else (S p, (a, 0)) end.
proof: Proof. case: i => > ?. - move=> >. eexists. by split; [eassumption|constructor]. - move=> >. eexists. by split; [eassumption|constructor]. - move=> [|a] b; eexists; by split; [eassumption|constructor]. - move=> a [|b]; eexists; by split; [eassumption|constructor]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun