Library begcd_mips_halve
Require Import Epsilon.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type nodup.
Import MachineInt.
Require Import mips_bipl mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import begcd.
Require Import multi_add_signed_unsigned_prg.
Require Import multi_sub_signed_unsigned_prg.
Require Import multi_add_signed_unsigned_simu.
Require Import multi_sub_signed_unsigned_simu.
Require Import begcd_mips_init.
Require Import library_interfaces.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Local Open Scope nodup_scope.
Local Open Scope assoc_scope.
Definition halve_mips rk ru rv rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 :=
(multi_is_even_s_and rt1 rt2 a0 a1 a2 ;
while.ifte (bne a0 r0)
(multi_div2_s rt1 a0 a1 a2 a3 a4 ;
multi_div2_s rt2 a0 a1 a2 a3 a4 ;
multi_div2_s rt3 a0 a1 a2 a3 a4)
((multi_add_s_u rk rt1 rv a0 a1 a2 a3 a4 a5 a6 ;
multi_div2_s rt1 a0 a1 a2 a3 a4) ;
(multi_sub_s_u rk rt2 ru a0 a1 a2 a3 a4 a5 a6 ;
multi_div2_s rt2 a0 a1 a2 a3 a4) ;
multi_div2_s rt3 a0 a1 a2 a3 a4
))%mips_cmd.
Lemma fwd_sim_begcd_halve : forall vu vv g u v u1 u2 u3 v1 v2 v3 t1 t2 t3 L
rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6,
nodup(g,u,v,u1,u2,u3,v1,v2,v3,t1,t2,t3) ->
nodup(rk,rg,ru,rv,ru1,ru2,ru3,rv1,rv2,rv3,rt1,rt2,rt3,a0,a1,a2,a3,a4,a5,a6,r0) ->
0 < vu -> 0 < vv ->
fwd_sim (state_mint
(g |=> unsign rk rg \U+ (u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+
(u1 |=> signed L ru1 \U+ (u2 |=> signed L ru2 \U+ (u3 |=> signed L ru3 \U+
(v1 |=> signed L rv1 \U+ (v2 |=> signed L rv2 \U+ (v3 |=> signed L rv3 \U+
(t1 |=> signed L rt1 \U+ (t2 |=> signed L rt2 \U+ t3 |=> signed L rt3))))))))))))
(fun s st _ =>
(((EGCD.C2 vu vv u v g s /\
(Zodd ([u ]_ s) \/ Zodd ([v ]_ s)) /\
EGCD.CVectors u v u1 u2 u3 v1 v2 v3 t1 t2 t3 s /\
EGCD.C4 u3 v3 t3 s /\
EGCD.C5 u3 v3 s /\
Zgcd ([u ]_ s) ([v ]_ s) = Zgcd ([u3 ]_ s) ([v3 ]_ s) /\
EGCD.uivi_bounds u v u1 v1 u2 v2 u3 v3 s /\
EGCD.ti_bounds u v t1 t2 t3 s) /\ uv_bound rk st u v s L) /\
([var_e t3 <>e nat_e 0 ]b_ s)) /\
([var_e t3 mode nat_e 2 =e nat_e 0 ]b_ s))%seplog_expr
(EGCD.TAOCP.halve u v t1 t2 t3)
(halve_mips rk ru rv rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6).
Proof.
move=> vu vv g u v u1 u2 u3 v1 v2 v3 t1 t2 t3 L rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 Hvars Hregs Hvu Hvv.
rewrite /EGCD.TAOCP.halve /halve_mips.
apply fwd_sim_ifte => //.
- rewrite /inv_R => s st h s_st_h st' h' exec_asm; split.
+ eapply state_mint_invariant; [idtac | idtac | apply s_st_h | apply exec_asm] => //.
Disj_f_cdom2list Permutation_mints_regs.
rewrite [mips_frame.modified_regs _]/=.
Disj_remove_dup.
apply: nodup.nodup_disj. rewrite [List.app _ _]/=. by Nodup_nodup r0.
+ rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t2.
assoc_put_in_front t1.
apply fwd_sim_b_multi_is_even_s_and.
rewrite [Equality.sort _]/= /bipl.var.v in Hvars *. by Nodup_nodup O.
by Nodup_nodup r0.
- apply fwd_sim_seq with (fun s st h => True) => //.
+ assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
+ apply fwd_sim_seq with (fun s st h => True) => //.
* assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
* assoc_put_in_front t3.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
- apply fwd_sim_seq with (fun s st h => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([t2]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([u ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
move=> abs; rewrite abs u2Z_Z2u // in Hcond.
omega.
repeat (split; first by tauto).
rewrite /EGCD.ti_bounds in Hcond.
local_Var_unchanged t2 s.
rewrite Zabs_non_eq; last by omega.
local_Var_unchanged u s.
omega.
+ apply fwd_sim_pcode_equiv with (t1 <- var_e t1 +e var_e v ; t1 <- var_e t1 ./e nat_e 2)%seplog_expr%seplog_cmd; last by apply equivalent_pseudo_code_example; Nodup_neq.
apply fwd_sim_seq with (fun s st h => True) => //.
* assoc_put_in_front v.
assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last first.
by apply safe_termination_multi_add_s_u; Nodup_nodup r0.
apply pfwd_sim_stren with (fun s st h => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([t1 ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([v ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr.
move=> s st h H.
rewrite /uv_bound in H.
split.
move=> abs; rewrite abs u2Z_Z2u // in H.
omega.
repeat (split; first by tauto).
rewrite /EGCD.ti_bounds in H.
rewrite Zabs_eq; omega.
apply pfwd_sim_multi_add_s_u_wo_overflow.
- rewrite [Equality.sort _]/= /bipl.var.v in Hvars *. by Nodup_nodup O.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
* assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
* apply fwd_sim_seq with (fun s st h => True) => //.
- apply fwd_sim_pcode_equiv with (t2 <- var_e t2 .-e var_e u ; t2 <- var_e t2 ./e nat_e 2)%seplog_expr%seplog_cmd; last by apply equivalent_pseudo_code_example; Nodup_neq.
apply fwd_sim_seq with (fun s st h => True) => //.
+ assoc_put_in_front u.
assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_s_u; Nodup_nodup r0.
apply pfwd_sim_multi_sub_s_u_wo_overflow.
- rewrite [Equality.sort _]/= in Hvars *. by Nodup_nodup O.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
+ assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
- assoc_put_in_front t3.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
Qed.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type nodup.
Import MachineInt.
Require Import mips_bipl mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import begcd.
Require Import multi_add_signed_unsigned_prg.
Require Import multi_sub_signed_unsigned_prg.
Require Import multi_add_signed_unsigned_simu.
Require Import multi_sub_signed_unsigned_simu.
Require Import begcd_mips_init.
Require Import library_interfaces.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Local Open Scope nodup_scope.
Local Open Scope assoc_scope.
Definition halve_mips rk ru rv rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 :=
(multi_is_even_s_and rt1 rt2 a0 a1 a2 ;
while.ifte (bne a0 r0)
(multi_div2_s rt1 a0 a1 a2 a3 a4 ;
multi_div2_s rt2 a0 a1 a2 a3 a4 ;
multi_div2_s rt3 a0 a1 a2 a3 a4)
((multi_add_s_u rk rt1 rv a0 a1 a2 a3 a4 a5 a6 ;
multi_div2_s rt1 a0 a1 a2 a3 a4) ;
(multi_sub_s_u rk rt2 ru a0 a1 a2 a3 a4 a5 a6 ;
multi_div2_s rt2 a0 a1 a2 a3 a4) ;
multi_div2_s rt3 a0 a1 a2 a3 a4
))%mips_cmd.
Lemma fwd_sim_begcd_halve : forall vu vv g u v u1 u2 u3 v1 v2 v3 t1 t2 t3 L
rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6,
nodup(g,u,v,u1,u2,u3,v1,v2,v3,t1,t2,t3) ->
nodup(rk,rg,ru,rv,ru1,ru2,ru3,rv1,rv2,rv3,rt1,rt2,rt3,a0,a1,a2,a3,a4,a5,a6,r0) ->
0 < vu -> 0 < vv ->
fwd_sim (state_mint
(g |=> unsign rk rg \U+ (u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+
(u1 |=> signed L ru1 \U+ (u2 |=> signed L ru2 \U+ (u3 |=> signed L ru3 \U+
(v1 |=> signed L rv1 \U+ (v2 |=> signed L rv2 \U+ (v3 |=> signed L rv3 \U+
(t1 |=> signed L rt1 \U+ (t2 |=> signed L rt2 \U+ t3 |=> signed L rt3))))))))))))
(fun s st _ =>
(((EGCD.C2 vu vv u v g s /\
(Zodd ([u ]_ s) \/ Zodd ([v ]_ s)) /\
EGCD.CVectors u v u1 u2 u3 v1 v2 v3 t1 t2 t3 s /\
EGCD.C4 u3 v3 t3 s /\
EGCD.C5 u3 v3 s /\
Zgcd ([u ]_ s) ([v ]_ s) = Zgcd ([u3 ]_ s) ([v3 ]_ s) /\
EGCD.uivi_bounds u v u1 v1 u2 v2 u3 v3 s /\
EGCD.ti_bounds u v t1 t2 t3 s) /\ uv_bound rk st u v s L) /\
([var_e t3 <>e nat_e 0 ]b_ s)) /\
([var_e t3 mode nat_e 2 =e nat_e 0 ]b_ s))%seplog_expr
(EGCD.TAOCP.halve u v t1 t2 t3)
(halve_mips rk ru rv rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6).
Proof.
move=> vu vv g u v u1 u2 u3 v1 v2 v3 t1 t2 t3 L rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 Hvars Hregs Hvu Hvv.
rewrite /EGCD.TAOCP.halve /halve_mips.
apply fwd_sim_ifte => //.
- rewrite /inv_R => s st h s_st_h st' h' exec_asm; split.
+ eapply state_mint_invariant; [idtac | idtac | apply s_st_h | apply exec_asm] => //.
Disj_f_cdom2list Permutation_mints_regs.
rewrite [mips_frame.modified_regs _]/=.
Disj_remove_dup.
apply: nodup.nodup_disj. rewrite [List.app _ _]/=. by Nodup_nodup r0.
+ rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t2.
assoc_put_in_front t1.
apply fwd_sim_b_multi_is_even_s_and.
rewrite [Equality.sort _]/= /bipl.var.v in Hvars *. by Nodup_nodup O.
by Nodup_nodup r0.
- apply fwd_sim_seq with (fun s st h => True) => //.
+ assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
+ apply fwd_sim_seq with (fun s st h => True) => //.
* assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
* assoc_put_in_front t3.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
- apply fwd_sim_seq with (fun s st h => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([t2]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([u ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
move=> abs; rewrite abs u2Z_Z2u // in Hcond.
omega.
repeat (split; first by tauto).
rewrite /EGCD.ti_bounds in Hcond.
local_Var_unchanged t2 s.
rewrite Zabs_non_eq; last by omega.
local_Var_unchanged u s.
omega.
+ apply fwd_sim_pcode_equiv with (t1 <- var_e t1 +e var_e v ; t1 <- var_e t1 ./e nat_e 2)%seplog_expr%seplog_cmd; last by apply equivalent_pseudo_code_example; Nodup_neq.
apply fwd_sim_seq with (fun s st h => True) => //.
* assoc_put_in_front v.
assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last first.
by apply safe_termination_multi_add_s_u; Nodup_nodup r0.
apply pfwd_sim_stren with (fun s st h => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([t1 ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([v ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr.
move=> s st h H.
rewrite /uv_bound in H.
split.
move=> abs; rewrite abs u2Z_Z2u // in H.
omega.
repeat (split; first by tauto).
rewrite /EGCD.ti_bounds in H.
rewrite Zabs_eq; omega.
apply pfwd_sim_multi_add_s_u_wo_overflow.
- rewrite [Equality.sort _]/= /bipl.var.v in Hvars *. by Nodup_nodup O.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
* assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
* apply fwd_sim_seq with (fun s st h => True) => //.
- apply fwd_sim_pcode_equiv with (t2 <- var_e t2 .-e var_e u ; t2 <- var_e t2 ./e nat_e 2)%seplog_expr%seplog_cmd; last by apply equivalent_pseudo_code_example; Nodup_neq.
apply fwd_sim_seq with (fun s st h => True) => //.
+ assoc_put_in_front u.
assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_s_u; Nodup_nodup r0.
apply pfwd_sim_multi_sub_s_u_wo_overflow.
- rewrite [Equality.sort _]/= in Hvars *. by Nodup_nodup O.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
+ assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
- assoc_put_in_front t3.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2_s; Nodup_nodup r0.
apply pfwd_sim_div2_s.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
Qed.