proposition: Lemma HALF_spec A X p v offset : let x := vec_pos v X in A <> X -> (offset, HALF A X p offset) // (offset, v) ->> let '(m, b) := half x in (if b then p else HALF_len + offset, vec_change (vec_change v X m) A 0).
proof: Proof. move=> /= /[dup] HX /nesym H'X. apply: (compose_sss_compute_trans 0). { by apply: ZERO_spec. } apply: (compose_sss_compute_trans 1). { by apply: MOVE_spec. } apply: (compose_sss_compute_trans 2). { by apply: JMP_spec. } rewrite !(vec_norm HX) Nat.add_0_l. suff: forall w, (offset, HALF A X p offset) // (ZERO_len+MOVE_len+JMP_len+INC_len+offset, w) ->> (let '(m, b) := half (vec_pos w A) in (if b then p else HALF_len + offset, vec_change (vec_change w X (vec_pos w X+m)) A 0)). { move=> H. apply: sss_compute_trans; [apply: H|]. apply: sss_compute_refl'. rewrite !(vec_norm HX). case: (half _) => [? ?]. by rewrite !(vec_norm HX). } elim /(induction_ltof1 _ (fun w => vec_pos w A)) => {}v IH. case EA: (vec_pos v A) => [|[|n]]. - apply: (compose_sss_compute_trans 4). { by apply: DEC_spec. } rewrite EA. apply: (compose_sss_compute_trans 5). { by apply: JMP_spec. } rewrite Nat.add_0_r !(vec_norm HX) (vec_change_same' EA). by apply: sss_compute_refl. - apply: (compose_sss_compute_trans 4). { by apply: DEC_spec. } rewrite EA. apply: (compose_sss_compute_trans 6). { by apply: DEC_spec. } rewrite Nat.add_0_r !(vec_norm HX). by apply: sss_compute_refl. - apply: (compose_sss_compute_trans 4). { by apply: DEC_spec. } rewrite EA. apply: (compose_sss_compute_trans 6). { by apply: DEC_spec. } rewrite vec_change_eq //. apply: (compose_sss_compute_trans 3). { by apply: INC_spec. } apply: sss_compute_trans. { apply: IH. rewrite /= !(vec_norm HX) EA. lia. } apply: sss_compute_refl'. rewrite !(vec_norm HX) /=. case: (half n) => [m []]; congr pair; by rewrite !(vec_norm HX) Nat.add_succ_comm. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun