proposition: Lemma DECODE_NAT_spec offset n xs s k w : flatten (closure xs s) = L.nat_enc n -> (offset, DECODE_NAT offset) // (offset, Vector.append w (0 ## 0 ## 0 ## k ## enc_cs xs ## enc_term s ## vec_nil)) ->> (DECODE_NAT_len+offset, Vector.append w (0 ## 0 ## 0 ## k+n ## 0 ## 0 ## vec_nil)).
proof: Proof. rewrite /DECODE_NAT. move=> /decode_nat_nat_enc H. elim: H k. - move=> >. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 0). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 1). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 2). { by apply: JZ_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 20). { by apply: ZERO_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 21). { by apply: ZERO_spec. } rewrite ?vec_simpl Nat.add_0_r. by apply: sss_compute_refl. - move=> > _ IH ?. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 0). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 1). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 2). { by apply: JZ_spec. } rewrite ?vec_simpl enc_pair_match. apply: (compose_sss_compute_trans 3). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 4). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 5). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 6). { by apply: JMP_spec. } by apply: IH. - move=> > _ IH ?. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 0). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 1). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 2). { by apply: JZ_spec. } rewrite ?vec_simpl enc_pair_match. apply: (compose_sss_compute_trans 3). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 7). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 8). { by apply: ZERO_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 9). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 10). { by apply: JMP_spec. } by apply: IH. - move=> > _ IH ?. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 0). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 1). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 11). { by apply: DEC_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: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 14). { by apply: PACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 15). { by apply: JMP_spec. } by apply: IH. - move=> > _ IH k. rewrite ?vec_simpl. apply: (compose_sss_compute_trans 0). { by apply: UNPACK_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 1). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 11). { by apply: DEC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 16). { by apply: INC_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 17). { by apply: ZERO_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 18). { by apply: MOVE_spec. } rewrite ?vec_simpl. apply: (compose_sss_compute_trans 19). { by apply: JMP_spec. } rewrite -/enc_term -(Nat.add_succ_comm k). by apply: IH. 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