proposition: Lemma HALF_spec X p v offset : let x := vec_pos v X in let a := vec_pos v A in A <> X -> (offset, HALF 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 (a+m)) A 0).
proof: Proof. move=> /= HX. apply: (concat_sss_compute_trans 0). { by apply: JMP_spec. } move Hst: (st in _ // _ ->> st) => st. elim /(Nat.measure_induction _ (fun v => vec_pos v X)) : v st Hst. move=> v IH st <-. case EX: (vec_pos v X) => [|[|n]]. { apply: mma_step. rewrite /= EX. apply: (concat_sss_compute_trans 2). { by apply: MOVE_spec. } apply: (concat_sss_compute_trans 3). { by apply: JMP_spec. } apply: sss_compute_refl'. by rewrite /= EX !Nat.add_0_r. } { apply: mma_step. rewrite /= EX ?(Nat.add_assoc _ _ offset). apply: mma_step. rewrite /= (vec_change_eq erefl). apply: (concat_sss_compute_trans 5). { by apply: MOVE_spec. } apply: sss_compute_refl'. by rewrite /= !(vec_norm HX) !Nat.add_0_r. } apply: mma_step. rewrite /= EX ?(Nat.add_assoc _ _ offset). apply: mma_step. rewrite /= (vec_change_eq erefl). apply: mma_step. apply: IH. { rewrite !(vec_norm HX). lia. } rewrite !(vec_norm HX) /=. have := half_spec n. case: (half n) => m [] ->. - rewrite !(vec_norm HX). congr pair. do ? congr vec_change. lia. - rewrite !(vec_norm HX). congr pair. do ? congr vec_change. lia. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun