proposition: Fact mma_incs_compute k i v st : st = (k+i,v[(k+(v#>x))/x]) -> (i,mma_incs k) // (i,v) ->> st.
proof: Proof. revert i v st; induction k as [ | k IHk ]; intros i v st ?; subst. + mma sss stop; f_equal; auto. apply vec_pos_ext; intros p; dest p x. + simpl; mma sss INC with x. apply subcode_sss_compute with (P := (1+i,mma_incs k)); auto. apply IHk; f_equal; try lia. apply vec_pos_ext; intros p; dest p x. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)