proposition: Lemma NAT_ENC_spec offset p n c w : (offset, NAT_ENC p offset) // (offset, Vector.append w (0 ## 0 ## 0 ## n ## c ## 0 ## vec_nil)) ->> (p, Vector.append w (0 ## 0 ## 0 ## 0 ## c ## enc_term (L.nat_enc n) ## vec_nil)).
proof: Proof. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 0). { by apply: ZERO_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 1). { by apply: ZERO_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 2). { by apply: ZERO_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 3). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 4). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 5). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 6). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 7). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 8). { by apply: PACK_spec. } rewrite ?vec_simpl. suff : forall m, (offset, compose (NAT_ENC_codes p offset) offset) // ((ZERO_len+ZERO_len+ZERO_len+INC_len+PACK_len+INC_len+PACK_len+INC_len+PACK_len) + offset, Vector.append w (0 ## 0 ## 0 ## n ## c ## enc_term (L.nat_enc m) ## vec_nil)) ->> (p, Vector.append w (0 ## 0 ## 0 ## 0 ## c ## enc_term (L.nat_enc (m+n)) ## vec_nil)). { move=> /(_ 0). by apply. } elim: n. { move=> m. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 9). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 10). { by apply: JMP_spec. } rewrite Nat.add_0_r. by apply: sss_compute_refl. } move=> n IH m. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 9). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 11). { by apply: ZERO_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 12). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 13). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 14). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 15). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 16). { by apply: MOVE_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 17). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 18). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 19). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 20). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 21). { by apply: JMP_spec. } rewrite -(Nat.add_succ_comm m n). by apply: (IH (S m)). Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun