proposition: Lemma mma_instr_compile_sound : instruction_compiler_sound mma_instr_compile (@mma_sss _) (@mma_sss _) eq.
proof: Proof. intros lnk I i1 v1 i2 v2 w1 H; revert H w1. change v1 with (snd (i1,v1)) at 2. change i1 with (fst (i1,v1)) at 2 3 4 6 7 8. change v2 with (snd (i2,v2)) at 2. change i2 with (fst (i2,v2)) at 2. generalize (i1,v1) (i2,v2); clear i1 v1 i2 v2. induction 1 as [ i x k | i x k v H | i x k v u H ]; simpl; intros w1 H0 ->. + exists (w1 [(S (w1#>x))/x]); split; auto. mma sss INC with x. mma sss stop; now f_equal. + exists w1; split; auto. mma sss DEC zero with x (lnk k). mma sss stop; now f_equal. + exists (w1[u/x]); split; auto. mma sss DEC S with x (lnk k) u. mma sss stop. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss compiler_correction) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)