Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover
theory CSP_rule_rw = CSP_law_etc:(*-------------------------------------------* | CSP-Prover | | December 2004 | | February 2005 (modified) | | Yoshinao Isobe (AIST JAPAN) | *-------------------------------------------*) theory CSP_rule_rw = CSP_law_etc: (***************************************************************** 1. 2. 3. 4. *****************************************************************) (*-------------------------------------------------------* | | | use these rules "csp_rule_..." as follows: | | | | lemmas new_rule = rule[THEN csp_rule_... ] or | | lemmas new_rule = csp_rule_...[OF rule] | | | *-------------------------------------------------------*) lemma csp_rule_rw_left_eq: "R1 =F R2 ==> (R1 =F R0) = (R2 =F R0)" by (simp add: eqF_def) lemma csp_rule_rw_left_ref: "R1 =F R2 ==> (R1 <=F R0) = (R2 <=F R0)" by (simp add: eqF_def refF_def) lemma csp_rule_rw_right_eq: "R1 =F R2 ==> (R0 =F R1) = (R0 =F R2)" by (simp add: eqF_def) lemma csp_rule_rw_right_ref: "R1 =F R2 ==> (R0 <=F R1) = (R0 <=F R2)" by (simp add: eqF_def refF_def) lemmas csp_rule_rw_left = csp_rule_rw_left_eq csp_rule_rw_left_ref lemmas csp_rule_rw_right = csp_rule_rw_right_eq csp_rule_rw_right_ref lemmas csp_rule_rw = csp_rule_rw_left csp_rule_rw_right lemmas csp_rule_rev_rw = csp_rule_rw[THEN sym] (********************************************************* Step laws *********************************************************) lemmas csp_step = csp_STOP_step csp_Act_prefix_step csp_Ext_choice_step csp_Parallel_step csp_Hiding_step csp_Renaming_step csp_Seq_compo_step lemmas csp_step_rw_left_eq = csp_step[THEN csp_rule_rw_left_eq] lemmas csp_step_rw_left_ref = csp_step[THEN csp_rule_rw_left_ref] lemmas csp_step_rw_right_eq = csp_step[THEN csp_rule_rw_right_eq] lemmas csp_step_rw_right_ref = csp_step[THEN csp_rule_rw_right_ref] lemmas csp_step_rw_left = csp_step_rw_left_eq csp_step_rw_left_ref lemmas csp_step_rw_right = csp_step_rw_right_eq csp_step_rw_right_ref lemmas csp_step_rw = csp_step_rw_left csp_step_rw_right (********************************************************* light Step laws for Act_prefix and STOP *********************************************************) lemmas csp_light_step = csp_STOP_step csp_Act_prefix_step lemmas csp_light_step_rw_left_eq = csp_light_step[THEN csp_rule_rw_left_eq] lemmas csp_light_step_rw_left_ref = csp_light_step[THEN csp_rule_rw_left_ref] lemmas csp_light_step_rw_right_eq = csp_light_step[THEN csp_rule_rw_right_eq] lemmas csp_light_step_rw_right_ref = csp_light_step[THEN csp_rule_rw_right_ref] lemmas csp_light_step_rw_left = csp_light_step_rw_left_eq csp_light_step_rw_left_ref lemmas csp_light_step_rw_right = csp_light_step_rw_right_eq csp_light_step_rw_right_ref lemmas csp_light_step_rw = csp_light_step_rw_left csp_light_step_rw_right (********************************************************* SKIP laws *********************************************************) lemmas csp_SKIP = csp_Seq_compo_unit_l csp_Seq_compo_unit_r csp_Parallel_preterm_l csp_Parallel_preterm_r csp_Parallel_term csp_SKIP_Hiding_Id csp_SKIP_Renaming_Id lemmas csp_SKIP_rw_left_eq = csp_SKIP[THEN csp_rule_rw_left_eq] lemmas csp_SKIP_rw_left_ref = csp_SKIP[THEN csp_rule_rw_left_ref] lemmas csp_SKIP_rw_right_eq = csp_SKIP[THEN csp_rule_rw_right_eq] lemmas csp_SKIP_rw_right_ref = csp_SKIP[THEN csp_rule_rw_right_ref] lemmas csp_SKIP_rw_left = csp_SKIP_rw_left_eq csp_SKIP_rw_left_ref lemmas csp_SKIP_rw_right = csp_SKIP_rw_right_eq csp_SKIP_rw_right_ref lemmas csp_SKIP_rw = csp_SKIP_rw_left csp_SKIP_rw_right (********************************************************* name unwinding function *********************************************************) lemmas csp_unwind_rw_left_eq = csp_unwind[THEN csp_rule_rw_left_eq] lemmas csp_unwind_rw_left_ref = csp_unwind[THEN csp_rule_rw_left_ref] lemmas csp_unwind_rw_right_eq = csp_unwind[THEN csp_rule_rw_right_eq] lemmas csp_unwind_rw_right_ref = csp_unwind[THEN csp_rule_rw_right_ref] lemmas csp_unwind_rw_left = csp_unwind_rw_left_eq csp_unwind_rw_left_ref lemmas csp_unwind_rw_right = csp_unwind_rw_right_eq csp_unwind_rw_right_ref lemmas csp_unwind_rw = csp_unwind_rw_left csp_unwind_rw_right (*** cpo ***) lemmas csp_unwind_cpo_rw_left_eq = csp_unwind_cpo[THEN csp_rule_rw_left_eq] lemmas csp_unwind_cpo_rw_left_ref = csp_unwind_cpo[THEN csp_rule_rw_left_ref] lemmas csp_unwind_cpo_rw_right_eq = csp_unwind_cpo[THEN csp_rule_rw_right_eq] lemmas csp_unwind_cpo_rw_right_ref = csp_unwind_cpo[THEN csp_rule_rw_right_ref] lemmas csp_unwind_cpo_rw_left = csp_unwind_cpo_rw_left_eq csp_unwind_cpo_rw_left_ref lemmas csp_unwind_cpo_rw_right = csp_unwind_cpo_rw_right_eq csp_unwind_cpo_rw_right_ref lemmas csp_unwind_cpo_rw = csp_unwind_cpo_rw_left csp_unwind_cpo_rw_right (********************************************************* dist laws *********************************************************) lemmas csp_dist = csp_Ext_choice_dist_l csp_Ext_choice_dist_r csp_Parallel_dist_l csp_Parallel_dist_r csp_Hiding_dist csp_Renaming_dist csp_Seq_compo_dist lemmas csp_dist_rw_left_eq = csp_dist[THEN csp_rule_rw_left_eq] lemmas csp_dist_rw_right_eq = csp_dist[THEN csp_rule_rw_right_eq] lemmas csp_dist_rw_left_ref = csp_dist[THEN csp_rule_rw_left_ref] lemmas csp_dist_rw_right_ref = csp_dist[THEN csp_rule_rw_right_ref] lemmas csp_dist_rw_left = csp_dist_rw_left_eq csp_dist_rw_left_ref lemmas csp_dist_rw_right = csp_dist_rw_right_eq csp_dist_rw_right_ref lemmas csp_dist_rw = csp_dist_rw_left csp_dist_rw_right (********************************************************* Rep_dist laws *********************************************************) lemmas csp_Rep_dist = csp_Ext_choice_Rep_dist_l csp_Ext_choice_Rep_dist_r csp_Parallel_Rep_dist_l csp_Parallel_Rep_dist_r csp_Hiding_Rep_dist csp_Renaming_Rep_dist csp_Seq_compo_Rep_dist lemmas csp_Rep_dist_rw_left_eq = csp_Rep_dist[THEN csp_rule_rw_left_eq] lemmas csp_Rep_dist_rw_right_eq = csp_Rep_dist[THEN csp_rule_rw_right_eq] lemmas csp_Rep_dist_rw_left_ref = csp_Rep_dist[THEN csp_rule_rw_left_ref] lemmas csp_Rep_dist_rw_right_ref = csp_Rep_dist[THEN csp_rule_rw_right_ref] lemmas csp_Rep_dist_rw_left = csp_Rep_dist_rw_left_eq csp_Rep_dist_rw_left_ref lemmas csp_Rep_dist_rw_right = csp_Rep_dist_rw_right_eq csp_Rep_dist_rw_right_ref lemmas csp_Rep_dist_rw = csp_Rep_dist_rw_left csp_Rep_dist_rw_right (********************************************************* Conditional *********************************************************) lemmas csp_Conditional_split_rw_left_eq = csp_Conditional_split[THEN csp_rule_rw_left_eq] lemmas csp_Conditional_split_rw_left_ref = csp_Conditional_split[THEN csp_rule_rw_left_ref] lemmas csp_Conditional_split_rw_right_eq = csp_Conditional_split[THEN csp_rule_rw_right_eq] lemmas csp_Conditional_split_rw_right_ref = csp_Conditional_split[THEN csp_rule_rw_right_ref] lemmas csp_Conditional_split_rw_left = csp_Conditional_split_rw_left_eq csp_Conditional_split_rw_left_ref lemmas csp_Conditional_split_rw_right = csp_Conditional_split_rw_right_eq csp_Conditional_split_rw_right_ref lemmas csp_Conditional_split_rw = csp_Conditional_split_rw_left csp_Conditional_split_rw_right (*** True or False ***) lemmas csp_Conditional = csp_Conditional_True csp_Conditional_False lemmas csp_Conditional_rw_left_eq = csp_Conditional[THEN csp_rule_rw_left_eq] lemmas csp_Conditional_rw_left_ref = csp_Conditional[THEN csp_rule_rw_left_ref] lemmas csp_Conditional_rw_right_eq = csp_Conditional[THEN csp_rule_rw_right_eq] lemmas csp_Conditional_rw_right_ref = csp_Conditional[THEN csp_rule_rw_right_ref] lemmas csp_Conditional_rw_left = csp_Conditional_rw_left_eq csp_Conditional_rw_left_ref lemmas csp_Conditional_rw_right = csp_Conditional_rw_right_eq csp_Conditional_rw_right_ref lemmas csp_Conditional_rw = csp_Conditional_rw_left csp_Conditional_rw_right (********************************************************* Int_simp *********************************************************) lemmas csp_Int_simp = csp_DIV_unwind csp_Rep_int_choice_unique csp_Int_choice_idem_weak lemmas csp_Int_simp_rw_left_eq = csp_Int_simp[THEN csp_rule_rw_left_eq] lemmas csp_Int_simp_rw_left_ref = csp_Int_simp[THEN csp_rule_rw_left_ref] lemmas csp_Int_simp_rw_right_eq = csp_Int_simp[THEN csp_rule_rw_right_eq] lemmas csp_Int_simp_rw_right_ref = csp_Int_simp[THEN csp_rule_rw_right_ref] lemmas csp_Int_simp_rw_left = csp_Int_simp_rw_left_eq csp_Int_simp_rw_left_ref lemmas csp_Int_simp_rw_right = csp_Int_simp_rw_right_eq csp_Int_simp_rw_right_ref lemmas csp_Int_simp_rw = csp_Int_simp_rw_left csp_Int_simp_rw_right (********************************************************* Ext_simp *********************************************************) lemmas csp_Ext_simp = csp_Ext_choice_unit_l_weak csp_Ext_choice_unit_r_weak lemmas csp_Ext_simp_rw_left_eq = csp_Ext_simp[THEN csp_rule_rw_left_eq] lemmas csp_Ext_simp_rw_left_ref = csp_Ext_simp[THEN csp_rule_rw_left_ref] lemmas csp_Ext_simp_rw_right_eq = csp_Ext_simp[THEN csp_rule_rw_right_eq] lemmas csp_Ext_simp_rw_right_ref = csp_Ext_simp[THEN csp_rule_rw_right_ref] lemmas csp_Ext_simp_rw_left = csp_Ext_simp_rw_left_eq csp_Ext_simp_rw_left_ref lemmas csp_Ext_simp_rw_right = csp_Ext_simp_rw_right_eq csp_Ext_simp_rw_right_ref lemmas csp_Ext_simp_rw = csp_Ext_simp_rw_left csp_Ext_simp_rw_right (********************************************************* Timeout_simp *********************************************************) lemmas csp_Mix_simp = csp_STOP_Timeout_weak lemmas csp_Mix_simp_rw_left_eq = csp_Mix_simp[THEN csp_rule_rw_left_eq] lemmas csp_Mix_simp_rw_left_ref = csp_Mix_simp[THEN csp_rule_rw_left_ref] lemmas csp_Mix_simp_rw_right_eq = csp_Mix_simp[THEN csp_rule_rw_right_eq] lemmas csp_Mix_simp_rw_right_ref = csp_Mix_simp[THEN csp_rule_rw_right_ref] lemmas csp_Mix_simp_rw_left = csp_Mix_simp_rw_left_eq csp_Mix_simp_rw_left_ref lemmas csp_Mix_simp_rw_right = csp_Mix_simp_rw_right_eq csp_Mix_simp_rw_right_ref lemmas csp_Mix_simp_rw = csp_Mix_simp_rw_left csp_Mix_simp_rw_right (********************************************************* csp_simp *********************************************************) lemmas csp_simp = csp_Int_simp csp_Ext_simp csp_Mix_simp lemmas csp_simp_rw_left = csp_Int_simp_rw_left csp_Ext_simp_rw_left csp_Mix_simp_rw_left lemmas csp_simp_rw_right = csp_Int_simp_rw_right csp_Ext_simp_rw_right csp_Mix_simp_rw_right lemmas csp_simp_rw = csp_simp_rw_left csp_simp_rw_right (*-------------------------------------------------------* | | | decompostion controlled by Not_Decompo_Flag | | | *-------------------------------------------------------*) consts Not_Decompo_Flag :: bool defs Not_Decompo_Flag_def : "Not_Decompo_Flag == True" lemma on_Not_Decompo_Flag: "Not_Decompo_Flag & R ==> R" by (simp) lemma off_Not_Decompo_Flag: "R ==> Not_Decompo_Flag & R" by (simp add: Not_Decompo_Flag_def) lemma off_Not_Decompo_Flag_True: "Not_Decompo_Flag" by (simp add: Not_Decompo_Flag_def) (*----------------------------------------------* | "Not_Decompo_Flag" is used for avoiding | | infinite decompositions in csp_tactics. | *----------------------------------------------*) lemma csp_rule_flag_left_eq: "(R1 =F R2) ==> (Not_Decompo_Flag & (R2 =F R0) ==> (R1 =F R0))" by (simp add: eqF_def Not_Decompo_Flag_def) lemma csp_rule_flag_left_ref: "R1 <=F R2 ==> (Not_Decompo_Flag & (R2 <=F R0) ==> (R1 <=F R0))" by (simp add: eqF_def refF_def Not_Decompo_Flag_def) lemma csp_rule_flag_right_eq: "R2 =F R1 ==> (Not_Decompo_Flag & (R0 =F R2) ==> (R0 =F R1))" by (simp add: eqF_def Not_Decompo_Flag_def) lemma csp_rule_flag_right_ref: "R2 <=F R1 ==> (Not_Decompo_Flag & (R0 <=F R2) ==> (R0 <=F R1))" by (simp add: eqF_def refF_def Not_Decompo_Flag_def) lemmas csp_rule_flag_left = csp_rule_flag_left_eq csp_rule_flag_left_ref lemmas csp_rule_flag_right = csp_rule_flag_right_eq csp_rule_flag_right_ref lemmas csp_rule_flag = csp_rule_flag_left csp_rule_flag_right (*** no flag ***) lemma csp_rule_tr_left_eq: "R1 =F R2 ==> ((R2 =F R0) ==> (R1 =F R0))" by (simp add: eqF_def) lemma csp_rule_tr_left_ref: "R1 <=F R2 ==> ((R2 <=F R0) ==> (R1 <=F R0))" by (simp add: eqF_def refF_def) lemma csp_rule_tr_right_eq: "R2 =F R1 ==> ((R0 =F R2) ==> (R0 =F R1))" by (simp add: eqF_def) lemma csp_rule_tr_right_ref: "R2 <=F R1 ==> ((R0 <=F R2) ==> (R0 <=F R1))" by (simp add: eqF_def refF_def) lemmas csp_rule_tr_left = csp_rule_tr_left_eq csp_rule_tr_left_ref lemmas csp_rule_tr_right = csp_rule_tr_right_eq csp_rule_tr_right_ref lemmas csp_rule_tr = csp_rule_tr_left csp_rule_tr_right lemmas csp_rule_tr_eq = csp_rule_tr_left_eq csp_rule_tr_right_eq lemmas csp_rule_tr_ref = csp_rule_tr_left_ref csp_rule_tr_right_ref (*------------------------------------------------* | laws for monotonicity (all) | *------------------------------------------------*) lemmas csp_free_mono_left = csp_free_mono[THEN csp_rule_tr_left_ref] lemmas csp_free_mono_right = csp_free_mono[THEN csp_rule_tr_right_ref] lemmas csp_mono_left = csp_mono[THEN csp_rule_tr_left_ref] lemmas csp_mono_right = csp_mono[THEN csp_rule_tr_right_ref] lemmas csp_free_mono_flag_left = csp_free_mono[THEN csp_rule_flag_left_ref] lemmas csp_free_mono_flag_right = csp_free_mono[THEN csp_rule_flag_right_ref] lemmas csp_mono_flag_left = csp_mono[THEN csp_rule_flag_left_ref] lemmas csp_mono_flag_right = csp_mono[THEN csp_rule_flag_right_ref] (*------------------------------------------------* | laws for congruence (all) | *------------------------------------------------*) lemmas csp_free_cong_left = csp_free_cong[THEN csp_rule_tr_left_eq] lemmas csp_free_cong_right = csp_free_cong[THEN csp_rule_tr_right_eq] lemmas csp_cong_left = csp_cong[THEN csp_rule_tr_left_eq] lemmas csp_cong_right = csp_cong[THEN csp_rule_tr_right_eq] lemmas csp_free_cong_flag_left = csp_free_cong[THEN csp_rule_flag_left_eq] lemmas csp_free_cong_flag_right = csp_free_cong[THEN csp_rule_flag_right_eq] lemmas csp_cong_flag_left = csp_cong[THEN csp_rule_flag_left_eq] lemmas csp_cong_flag_right = csp_cong[THEN csp_rule_flag_right_eq] (*------------------------------------------------* | laws for decompo (ALL) | *------------------------------------------------*) lemmas csp_free_decompo_left = csp_free_mono_left csp_free_cong_left lemmas csp_free_decompo_right = csp_free_mono_right csp_free_cong_right lemmas csp_decompo_left = csp_mono_left csp_cong_left lemmas csp_decompo_right = csp_mono_right csp_cong_right lemmas csp_free_decompo_flag_left = csp_free_mono_flag_left csp_free_cong_flag_left lemmas csp_free_decompo_flag_right = csp_free_mono_flag_right csp_free_cong_flag_right lemmas csp_decompo_flag_left = csp_mono_flag_left csp_cong_flag_left lemmas csp_decompo_flag_right = csp_mono_flag_right csp_cong_flag_right (*------------------------------------------------* | trans with Flag | *------------------------------------------------*) (*** rewrite (eq) ***) lemma csp_rw_flag_left_eq: "[| R1 =F R2 ; Not_Decompo_Flag & R2 =F R3 |] ==> R1 =F R3" by (simp add: eqF_def Not_Decompo_Flag_def) lemma csp_rw_flag_left_ref: "[| R1 =F R2 ; Not_Decompo_Flag & R2 <=F R3 |] ==> R1 <=F R3" by (simp add: refF_def eqF_def Not_Decompo_Flag_def) lemmas csp_rw_flag_left = csp_rw_flag_left_eq csp_rw_flag_left_ref lemma csp_rw_flag_right_eq: "[| R3 =F R2 ; Not_Decompo_Flag & R1 =F R2 |] ==> R1 =F R3" by (simp add: eqF_def Not_Decompo_Flag_def) lemma csp_rw_flag_right_ref: "[| R3 =F R2 ; Not_Decompo_Flag & R1 <=F R2 |] ==> R1 <=F R3" by (simp add: refF_def eqF_def Not_Decompo_Flag_def) lemmas csp_rw_flag_right = csp_rw_flag_right_eq csp_rw_flag_right_ref (*** rewrite (ref) ***) lemma csp_tr_flag_left_eq: "[| R1 =F R2 ; Not_Decompo_Flag & R2 =F R3 |] ==> R1 =F R3" by (simp add: eqF_def Not_Decompo_Flag_def) lemma csp_tr_flag_left_ref: "[| R1 <=F R2 ; Not_Decompo_Flag & R2 <=F R3 |] ==> R1 <=F R3" by (simp add: refF_def eqF_def Not_Decompo_Flag_def) lemmas csp_tr_flag_left = csp_tr_flag_left_eq csp_tr_flag_left_ref lemma csp_tr_flag_right_eq: "[| R2 =F R3 ; Not_Decompo_Flag & R1 =F R2 |] ==> R1 =F R3" by (simp add: eqF_def Not_Decompo_Flag_def) lemma csp_tr_flag_right_ref: "[| R2 <=F R3 ; Not_Decompo_Flag & R1 <=F R2 |] ==> R1 <=F R3" by (simp add: refF_def eqF_def Not_Decompo_Flag_def) lemmas csp_tr_flag_right = csp_tr_flag_right_eq csp_tr_flag_right_ref end
lemma csp_rule_rw_left_eq:
R1 =F R2 ==> (R1 =F R0) = (R2 =F R0)
lemma csp_rule_rw_left_ref:
R1 =F R2 ==> (R1 <=F R0) = (R2 <=F R0)
lemma csp_rule_rw_right_eq:
R1 =F R2 ==> (R0 =F R1) = (R0 =F R2)
lemma csp_rule_rw_right_ref:
R1 =F R2 ==> (R0 <=F R1) = (R0 <=F R2)
lemmas csp_rule_rw_left:
R1 =F R2 ==> (R1 =F R0) = (R2 =F R0)
R1 =F R2 ==> (R1 <=F R0) = (R2 <=F R0)
lemmas csp_rule_rw_right:
R1 =F R2 ==> (R0 =F R1) = (R0 =F R2)
R1 =F R2 ==> (R0 <=F R1) = (R0 <=F R2)
lemmas csp_rule_rw:
R1 =F R2 ==> (R1 =F R0) = (R2 =F R0)
R1 =F R2 ==> (R1 <=F R0) = (R2 <=F R0)
R1 =F R2 ==> (R0 =F R1) = (R0 =F R2)
R1 =F R2 ==> (R0 <=F R1) = (R0 <=F R2)
lemmas csp_rule_rev_rw:
R1_1 =F R2_1 ==> (R2_1 =F R0_1) = (R1_1 =F R0_1)
R1_1 =F R2_1 ==> (R2_1 <=F R0_1) = (R1_1 <=F R0_1)
R1_1 =F R2_1 ==> (R0_1 =F R2_1) = (R0_1 =F R1_1)
R1_1 =F R2_1 ==> (R0_1 <=F R2_1) = (R0_1 <=F R1_1)
lemmas csp_step:
LET:fp df IN STOP =F LET:fp df IN ? x:{} -> DIV
LET:fp df IN a -> P =F LET:fp df IN ? x:{a} -> P
LET:fp df IN ? :X -> Pf [+] ? :Y -> Qf =F LET:fp df IN Ext_choice_step X Y Pf Qf
LET:fp df IN ? :Y -> Pf |[X]| ? :Z -> Qf =F LET:fp df IN Parallel_step X Y Z Pf Qf
LET:fp df IN (? :Y -> Pf) -- X =F LET:fp df IN Hiding_step X Y Pf
LET:fp df IN (? :X -> Pf) [[r]] =F LET:fp df IN Renaming_step r X Pf
LET:fp df IN ? :X -> Pf ;; Q =F LET:fp df IN Seq_compo_step X Pf Q
lemmas csp_step_rw_left_eq:
( LET:fp_1 df_1 IN STOP =F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV =F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 =F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 =F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1 =F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1 =F R0)
( LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1 =F R0)
( LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1 =F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1 =F R0)
lemmas csp_step_rw_left_ref:
( LET:fp_1 df_1 IN STOP <=F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV <=F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 <=F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1 <=F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1 <=F R0)
( LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1 <=F R0)
( LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1 <=F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1 <=F R0)
lemmas csp_step_rw_right_eq:
(R0 =F LET:fp_1 df_1 IN STOP) = (R0 =F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 =F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 =F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
(R0 =F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1)
(R0 =F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1)
(R0 =F LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1)
(R0 =F LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1)
(R0 =F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1) = (R0 =F LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1)
lemmas csp_step_rw_right_ref:
(R0 <=F LET:fp_1 df_1 IN STOP) = (R0 <=F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 <=F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 <=F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
(R0 <=F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1)
(R0 <=F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1)
(R0 <=F LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1)
(R0 <=F LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1)
(R0 <=F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1)
lemmas csp_step_rw_left:
( LET:fp_1 df_1 IN STOP =F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV =F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 =F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 =F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1 =F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1 =F R0)
( LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1 =F R0)
( LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1 =F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1 =F R0)
( LET:fp_1 df_1 IN STOP <=F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV <=F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 <=F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1 <=F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1 <=F R0)
( LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1 <=F R0)
( LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1 <=F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1 <=F R0)
lemmas csp_step_rw_right:
(R0 =F LET:fp_1 df_1 IN STOP) = (R0 =F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 =F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 =F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
(R0 =F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1)
(R0 =F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1)
(R0 =F LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1)
(R0 =F LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1)
(R0 =F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1) = (R0 =F LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1)
(R0 <=F LET:fp_1 df_1 IN STOP) = (R0 <=F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 <=F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 <=F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
(R0 <=F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1)
(R0 <=F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1)
(R0 <=F LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1)
(R0 <=F LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1)
(R0 <=F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1)
lemmas csp_step_rw:
( LET:fp_1 df_1 IN STOP =F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV =F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 =F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 =F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1 =F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1 =F R0)
( LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1 =F R0)
( LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1 =F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1 =F R0)
( LET:fp_1 df_1 IN STOP <=F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV <=F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 <=F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1 <=F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1 <=F R0)
( LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1 <=F R0)
( LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1 <=F R0)
( LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1 <=F R0)
(R0 =F LET:fp_1 df_1 IN STOP) = (R0 =F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 =F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 =F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
(R0 =F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1)
(R0 =F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1)
(R0 =F LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1)
(R0 =F LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1)
(R0 =F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1) = (R0 =F LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1)
(R0 <=F LET:fp_1 df_1 IN STOP) = (R0 <=F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 <=F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 <=F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
(R0 <=F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1)
(R0 <=F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1)
(R0 <=F LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1)
(R0 <=F LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1)
(R0 <=F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1)
lemmas csp_light_step:
LET:fp df IN STOP =F LET:fp df IN ? x:{} -> DIV
LET:fp df IN a -> P =F LET:fp df IN ? x:{a} -> P
lemmas csp_light_step_rw_left_eq:
( LET:fp_1 df_1 IN STOP =F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV =F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 =F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 =F R0)
lemmas csp_light_step_rw_left_ref:
( LET:fp_1 df_1 IN STOP <=F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV <=F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 <=F R0)
lemmas csp_light_step_rw_right_eq:
(R0 =F LET:fp_1 df_1 IN STOP) = (R0 =F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 =F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 =F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
lemmas csp_light_step_rw_right_ref:
(R0 <=F LET:fp_1 df_1 IN STOP) = (R0 <=F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 <=F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 <=F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
lemmas csp_light_step_rw_left:
( LET:fp_1 df_1 IN STOP =F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV =F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 =F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 =F R0)
( LET:fp_1 df_1 IN STOP <=F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV <=F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 <=F R0)
lemmas csp_light_step_rw_right:
(R0 =F LET:fp_1 df_1 IN STOP) = (R0 =F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 =F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 =F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
(R0 <=F LET:fp_1 df_1 IN STOP) = (R0 <=F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 <=F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 <=F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
lemmas csp_light_step_rw:
( LET:fp_1 df_1 IN STOP =F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV =F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 =F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 =F R0)
( LET:fp_1 df_1 IN STOP <=F R0) = ( LET:fp_1 df_1 IN ? x:{} -> DIV <=F R0)
( LET:fp_1 df_1 IN a_1 -> P_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:{a_1} -> P_1 <=F R0)
(R0 =F LET:fp_1 df_1 IN STOP) = (R0 =F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 =F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 =F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
(R0 <=F LET:fp_1 df_1 IN STOP) = (R0 <=F LET:fp_1 df_1 IN ? x:{} -> DIV)
(R0 <=F LET:fp_1 df_1 IN a_1 -> P_1) = (R0 <=F LET:fp_1 df_1 IN ? x:{a_1} -> P_1)
lemmas csp_SKIP:
LET:fp df IN SKIP ;; P =F LET:fp df IN P
LET:fp df IN P ;; SKIP =F LET:fp df IN P
LET:fp df IN SKIP |[X]| ? :Y -> Qf =F LET:fp df IN ? x:(Y - X) -> (SKIP |[X]| Qf x)
LET:fp df IN ? :Y -> Pf |[X]| SKIP =F LET:fp df IN ? x:(Y - X) -> (Pf x |[X]| SKIP)
LET:fp df IN SKIP |[X]| SKIP =F LET:fp df IN SKIP
LET:fp df IN SKIP -- X =F LET:fp df IN SKIP
LET:fp df IN SKIP [[r]] =F LET:fp df IN SKIP
lemmas csp_SKIP_rw_left_eq:
( LET:fp_1 df_1 IN SKIP ;; P_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN P_1 ;; SKIP =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x) =F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP =F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP) =F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| SKIP =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
( LET:fp_1 df_1 IN SKIP -- X_1 =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
( LET:fp_1 df_1 IN SKIP [[r_1]] =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
lemmas csp_SKIP_rw_left_ref:
( LET:fp_1 df_1 IN SKIP ;; P_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN P_1 ;; SKIP <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x) <=F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP <=F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP) <=F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| SKIP <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
( LET:fp_1 df_1 IN SKIP -- X_1 <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
( LET:fp_1 df_1 IN SKIP [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
lemmas csp_SKIP_rw_right_eq:
(R0 =F LET:fp_1 df_1 IN SKIP ;; P_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN P_1 ;; SKIP) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x))
(R0 =F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP) = (R0 =F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP))
(R0 =F LET:fp_1 df_1 IN SKIP |[X_1]| SKIP) = (R0 =F LET:fp_1 df_1 IN SKIP)
(R0 =F LET:fp_1 df_1 IN SKIP -- X_1) = (R0 =F LET:fp_1 df_1 IN SKIP)
(R0 =F LET:fp_1 df_1 IN SKIP [[r_1]]) = (R0 =F LET:fp_1 df_1 IN SKIP)
lemmas csp_SKIP_rw_right_ref:
(R0 <=F LET:fp_1 df_1 IN SKIP ;; P_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN P_1 ;; SKIP) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x))
(R0 <=F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP) = (R0 <=F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP))
(R0 <=F LET:fp_1 df_1 IN SKIP |[X_1]| SKIP) = (R0 <=F LET:fp_1 df_1 IN SKIP)
(R0 <=F LET:fp_1 df_1 IN SKIP -- X_1) = (R0 <=F LET:fp_1 df_1 IN SKIP)
(R0 <=F LET:fp_1 df_1 IN SKIP [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN SKIP)
lemmas csp_SKIP_rw_left:
( LET:fp_1 df_1 IN SKIP ;; P_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN P_1 ;; SKIP =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x) =F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP =F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP) =F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| SKIP =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
( LET:fp_1 df_1 IN SKIP -- X_1 =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
( LET:fp_1 df_1 IN SKIP [[r_1]] =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
( LET:fp_1 df_1 IN SKIP ;; P_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN P_1 ;; SKIP <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x) <=F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP <=F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP) <=F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| SKIP <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
( LET:fp_1 df_1 IN SKIP -- X_1 <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
( LET:fp_1 df_1 IN SKIP [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
lemmas csp_SKIP_rw_right:
(R0 =F LET:fp_1 df_1 IN SKIP ;; P_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN P_1 ;; SKIP) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x))
(R0 =F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP) = (R0 =F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP))
(R0 =F LET:fp_1 df_1 IN SKIP |[X_1]| SKIP) = (R0 =F LET:fp_1 df_1 IN SKIP)
(R0 =F LET:fp_1 df_1 IN SKIP -- X_1) = (R0 =F LET:fp_1 df_1 IN SKIP)
(R0 =F LET:fp_1 df_1 IN SKIP [[r_1]]) = (R0 =F LET:fp_1 df_1 IN SKIP)
(R0 <=F LET:fp_1 df_1 IN SKIP ;; P_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN P_1 ;; SKIP) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x))
(R0 <=F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP) = (R0 <=F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP))
(R0 <=F LET:fp_1 df_1 IN SKIP |[X_1]| SKIP) = (R0 <=F LET:fp_1 df_1 IN SKIP)
(R0 <=F LET:fp_1 df_1 IN SKIP -- X_1) = (R0 <=F LET:fp_1 df_1 IN SKIP)
(R0 <=F LET:fp_1 df_1 IN SKIP [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN SKIP)
lemmas csp_SKIP_rw:
( LET:fp_1 df_1 IN SKIP ;; P_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN P_1 ;; SKIP =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1 =F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x) =F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP =F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP) =F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| SKIP =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
( LET:fp_1 df_1 IN SKIP -- X_1 =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
( LET:fp_1 df_1 IN SKIP [[r_1]] =F R0) = ( LET:fp_1 df_1 IN SKIP =F R0)
( LET:fp_1 df_1 IN SKIP ;; P_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN P_1 ;; SKIP <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1 <=F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x) <=F R0)
( LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP <=F R0) = ( LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP) <=F R0)
( LET:fp_1 df_1 IN SKIP |[X_1]| SKIP <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
( LET:fp_1 df_1 IN SKIP -- X_1 <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
( LET:fp_1 df_1 IN SKIP [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN SKIP <=F R0)
(R0 =F LET:fp_1 df_1 IN SKIP ;; P_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN P_1 ;; SKIP) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1) = (R0 =F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x))
(R0 =F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP) = (R0 =F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP))
(R0 =F LET:fp_1 df_1 IN SKIP |[X_1]| SKIP) = (R0 =F LET:fp_1 df_1 IN SKIP)
(R0 =F LET:fp_1 df_1 IN SKIP -- X_1) = (R0 =F LET:fp_1 df_1 IN SKIP)
(R0 =F LET:fp_1 df_1 IN SKIP [[r_1]]) = (R0 =F LET:fp_1 df_1 IN SKIP)
(R0 <=F LET:fp_1 df_1 IN SKIP ;; P_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN P_1 ;; SKIP) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1) = (R0 <=F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x))
(R0 <=F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP) = (R0 <=F LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP))
(R0 <=F LET:fp_1 df_1 IN SKIP |[X_1]| SKIP) = (R0 <=F LET:fp_1 df_1 IN SKIP)
(R0 <=F LET:fp_1 df_1 IN SKIP -- X_1) = (R0 <=F LET:fp_1 df_1 IN SKIP)
(R0 <=F LET:fp_1 df_1 IN SKIP [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN SKIP)
lemmas csp_unwind_rw_left_eq:
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> ( LET:fp_1 df_1 IN <C_1> =F R0) = ( LET:fp_1 df_1 IN df_1 C_1 =F R0)
lemmas csp_unwind_rw_left_ref:
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> ( LET:fp_1 df_1 IN <C_1> <=F R0) = ( LET:fp_1 df_1 IN df_1 C_1 <=F R0)
lemmas csp_unwind_rw_right_eq:
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> (R0 =F LET:fp_1 df_1 IN <C_1>) = (R0 =F LET:fp_1 df_1 IN df_1 C_1)
lemmas csp_unwind_rw_right_ref:
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> (R0 <=F LET:fp_1 df_1 IN <C_1>) = (R0 <=F LET:fp_1 df_1 IN df_1 C_1)
lemmas csp_unwind_rw_left:
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> ( LET:fp_1 df_1 IN <C_1> =F R0) = ( LET:fp_1 df_1 IN df_1 C_1 =F R0)
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> ( LET:fp_1 df_1 IN <C_1> <=F R0) = ( LET:fp_1 df_1 IN df_1 C_1 <=F R0)
lemmas csp_unwind_rw_right:
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> (R0 =F LET:fp_1 df_1 IN <C_1>) = (R0 =F LET:fp_1 df_1 IN df_1 C_1)
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> (R0 <=F LET:fp_1 df_1 IN <C_1>) = (R0 <=F LET:fp_1 df_1 IN df_1 C_1)
lemmas csp_unwind_rw:
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> ( LET:fp_1 df_1 IN <C_1> =F R0) = ( LET:fp_1 df_1 IN df_1 C_1 =F R0)
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> ( LET:fp_1 df_1 IN <C_1> <=F R0) = ( LET:fp_1 df_1 IN df_1 C_1 <=F R0)
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> (R0 =F LET:fp_1 df_1 IN <C_1>) = (R0 =F LET:fp_1 df_1 IN df_1 C_1)
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> (R0 <=F LET:fp_1 df_1 IN <C_1>) = (R0 <=F LET:fp_1 df_1 IN df_1 C_1)
lemmas csp_unwind_cpo_rw_left_eq:
( LET:Lfp df_1 IN <C_1> =F R0) = ( LET:Lfp df_1 IN df_1 C_1 =F R0)
lemmas csp_unwind_cpo_rw_left_ref:
( LET:Lfp df_1 IN <C_1> <=F R0) = ( LET:Lfp df_1 IN df_1 C_1 <=F R0)
lemmas csp_unwind_cpo_rw_right_eq:
(R0 =F LET:Lfp df_1 IN <C_1>) = (R0 =F LET:Lfp df_1 IN df_1 C_1)
lemmas csp_unwind_cpo_rw_right_ref:
(R0 <=F LET:Lfp df_1 IN <C_1>) = (R0 <=F LET:Lfp df_1 IN df_1 C_1)
lemmas csp_unwind_cpo_rw_left:
( LET:Lfp df_1 IN <C_1> =F R0) = ( LET:Lfp df_1 IN df_1 C_1 =F R0)
( LET:Lfp df_1 IN <C_1> <=F R0) = ( LET:Lfp df_1 IN df_1 C_1 <=F R0)
lemmas csp_unwind_cpo_rw_right:
(R0 =F LET:Lfp df_1 IN <C_1>) = (R0 =F LET:Lfp df_1 IN df_1 C_1)
(R0 <=F LET:Lfp df_1 IN <C_1>) = (R0 <=F LET:Lfp df_1 IN df_1 C_1)
lemmas csp_unwind_cpo_rw:
( LET:Lfp df_1 IN <C_1> =F R0) = ( LET:Lfp df_1 IN df_1 C_1 =F R0)
( LET:Lfp df_1 IN <C_1> <=F R0) = ( LET:Lfp df_1 IN df_1 C_1 <=F R0)
(R0 =F LET:Lfp df_1 IN <C_1>) = (R0 =F LET:Lfp df_1 IN df_1 C_1)
(R0 <=F LET:Lfp df_1 IN <C_1>) = (R0 <=F LET:Lfp df_1 IN df_1 C_1)
lemmas csp_dist:
LET:fp df IN (P1 |~| P2) [+] Q =F LET:fp df IN P1 [+] Q |~| P2 [+] Q
LET:fp df IN P [+] (Q1 |~| Q2) =F LET:fp df IN P [+] Q1 |~| P [+] Q2
LET:fp df IN (P1 |~| P2) |[X]| Q =F LET:fp df IN P1 |[X]| Q |~| P2 |[X]| Q
LET:fp df IN P |[X]| (Q1 |~| Q2) =F LET:fp df IN P |[X]| Q1 |~| P |[X]| Q2
LET:fp df IN (P1 |~| P2) -- X =F LET:fp df IN P1 -- X |~| P2 -- X
LET:fp df IN (P1 |~| P2) [[r]] =F LET:fp df IN P1 [[r]] |~| P2 [[r]]
LET:fp df IN (P1 |~| P2) ;; Q =F LET:fp df IN P1 ;; Q |~| P2 ;; Q
lemmas csp_dist_rw_left_eq:
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 =F R0)
( LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1) =F R0) = ( LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 =F R0)
( LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1) =F R0) = ( LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 =F R0)
lemmas csp_dist_rw_right_eq:
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1)
(R0 =F LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)) = (R0 =F LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1)
(R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)) = (R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]])
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1)
lemmas csp_dist_rw_left_ref:
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 <=F R0)
( LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1) <=F R0) = ( LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 <=F R0)
( LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1) <=F R0) = ( LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 <=F R0)
lemmas csp_dist_rw_right_ref:
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1)
(R0 <=F LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)) = (R0 <=F LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1)
(R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)) = (R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]])
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1)
lemmas csp_dist_rw_left:
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 =F R0)
( LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1) =F R0) = ( LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 =F R0)
( LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1) =F R0) = ( LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 <=F R0)
( LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1) <=F R0) = ( LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 <=F R0)
( LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1) <=F R0) = ( LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 <=F R0)
lemmas csp_dist_rw_right:
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1)
(R0 =F LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)) = (R0 =F LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1)
(R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)) = (R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]])
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1)
(R0 <=F LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)) = (R0 <=F LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1)
(R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)) = (R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]])
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1)
lemmas csp_dist_rw:
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 =F R0)
( LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1) =F R0) = ( LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 =F R0)
( LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1) =F R0) = ( LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 =F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 <=F R0)
( LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1) <=F R0) = ( LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 <=F R0)
( LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1) <=F R0) = ( LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] <=F R0)
( LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 <=F R0)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1)
(R0 =F LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)) = (R0 =F LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1)
(R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)) = (R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1)
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]])
(R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1) = (R0 =F LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1)
(R0 <=F LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)) = (R0 <=F LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1)
(R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)) = (R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1)
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]])
(R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1)
lemmas csp_Rep_dist:
X ≠ {} ==> LET:fp df IN (! :X .. Pf) [+] Q =F LET:fp df IN ! x:X .. Pf x [+] Q
X ≠ {} ==> LET:fp df IN P [+] (! :X .. Qf) =F LET:fp df IN ! x:X .. P [+] Qf x
Y ≠ {} ==> LET:fp df IN (! :Y .. Pf) |[X]| Q =F LET:fp df IN ! x:Y .. Pf x |[X]| Q
Y ≠ {} ==> LET:fp df IN P |[X]| (! :Y .. Qf) =F LET:fp df IN ! x:Y .. P |[X]| Qf x
LET:fp df IN (! :Y .. Pf) -- X =F LET:fp df IN ! x:Y .. Pf x -- X
LET:fp df IN (! :X .. Pf) [[r]] =F LET:fp df IN ! x:X .. Pf x [[r]]
LET:fp df IN (! :X .. Pf) ;; Q =F LET:fp df IN ! x:X .. Pf x ;; Q
lemmas csp_Rep_dist_rw_left_eq:
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 =F R0)
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1) =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x =F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 =F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1) =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x =F R0)
( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 =F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] =F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 =F R0)
lemmas csp_Rep_dist_rw_right_eq:
X_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1)
X_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x)
Y_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1)
Y_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x)
(R0 =F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1)
(R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]])
(R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1)
lemmas csp_Rep_dist_rw_left_ref:
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 <=F R0)
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1) <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x <=F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 <=F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1) <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x <=F R0)
( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 <=F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] <=F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 <=F R0)
lemmas csp_Rep_dist_rw_right_ref:
X_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1)
X_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x)
Y_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1)
Y_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x)
(R0 <=F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1)
(R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]])
(R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1)
lemmas csp_Rep_dist_rw_left:
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 =F R0)
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1) =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x =F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 =F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1) =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x =F R0)
( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 =F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] =F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 =F R0)
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 <=F R0)
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1) <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x <=F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 <=F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1) <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x <=F R0)
( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 <=F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] <=F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 <=F R0)
lemmas csp_Rep_dist_rw_right:
X_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1)
X_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x)
Y_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1)
Y_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x)
(R0 =F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1)
(R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]])
(R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1)
X_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1)
X_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x)
Y_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1)
Y_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x)
(R0 <=F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1)
(R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]])
(R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1)
lemmas csp_Rep_dist_rw:
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 =F R0)
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1) =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x =F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 =F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1) =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x =F R0)
( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1 =F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 =F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]] =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] =F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1 =F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 =F R0)
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 <=F R0)
X_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1) <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x <=F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 <=F R0)
Y_1 ≠ {} ==> ( LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1) <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x <=F R0)
( LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 <=F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]] <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] <=F R0)
( LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1 <=F R0) = ( LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 <=F R0)
X_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1)
X_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x)
Y_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1)
Y_1 ≠ {} ==> (R0 =F LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x)
(R0 =F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1) = (R0 =F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1)
(R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]])
(R0 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1) = (R0 =F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1)
X_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1)
X_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x)
Y_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1)
Y_1 ≠ {} ==> (R0 <=F LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x)
(R0 <=F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1) = (R0 <=F LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1)
(R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]])
(R0 <=F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1) = (R0 <=F LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1)
lemmas csp_Conditional_split_rw_left_eq:
( LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1) =F R0)
lemmas csp_Conditional_split_rw_left_ref:
( LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1) <=F R0)
lemmas csp_Conditional_split_rw_right_eq:
(R0 =F LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1))
lemmas csp_Conditional_split_rw_right_ref:
(R0 <=F LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1))
lemmas csp_Conditional_split_rw_left:
( LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1) =F R0)
( LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1) <=F R0)
lemmas csp_Conditional_split_rw_right:
(R0 =F LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1))
(R0 <=F LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1))
lemmas csp_Conditional_split_rw:
( LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1) =F R0)
( LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1) <=F R0)
(R0 =F LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1))
(R0 <=F LET:fp_1 df_1 IN IF b_1 THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN (if b_1 then P_1 else Q_1))
lemmas csp_Conditional:
LET:fp df IN IF True THEN P ELSE Q =F LET:fp df IN P
LET:fp df IN IF False THEN P ELSE Q =F LET:fp df IN Q
lemmas csp_Conditional_rw_left_eq:
( LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN Q_1 =F R0)
lemmas csp_Conditional_rw_left_ref:
( LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN Q_1 <=F R0)
lemmas csp_Conditional_rw_right_eq:
(R0 =F LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN Q_1)
lemmas csp_Conditional_rw_right_ref:
(R0 <=F LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN Q_1)
lemmas csp_Conditional_rw_left:
( LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN Q_1 =F R0)
( LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN Q_1 <=F R0)
lemmas csp_Conditional_rw_right:
(R0 =F LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN Q_1)
(R0 <=F LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN Q_1)
lemmas csp_Conditional_rw:
( LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1 =F R0) = ( LET:fp_1 df_1 IN Q_1 =F R0)
( LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
( LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1 <=F R0) = ( LET:fp_1 df_1 IN Q_1 <=F R0)
(R0 =F LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 =F LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1) = (R0 =F LET:fp_1 df_1 IN Q_1)
(R0 <=F LET:fp_1 df_1 IN IF True THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN IF False THEN P_1 ELSE Q_1) = (R0 <=F LET:fp_1 df_1 IN Q_1)
lemmas csp_Int_simp:
LET:fp df IN DIV =F LET:fp df IN ! x:{} .. DIV
LET:fp df IN ! :{a} .. Pf =F LET:fp df IN Pf a
LET:fp df IN P =F LET:fp df IN Q ==> LET:fp df IN P |~| Q =F LET:fp df IN P
lemmas csp_Int_simp_rw_left_eq:
( LET:fp_1 df_1 IN DIV =F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV =F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 =F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 =F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
lemmas csp_Int_simp_rw_left_ref:
( LET:fp_1 df_1 IN DIV <=F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV <=F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 <=F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 <=F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
lemmas csp_Int_simp_rw_right_eq:
(R0 =F LET:fp_1 df_1 IN DIV) = (R0 =F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 =F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 =F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 =F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
lemmas csp_Int_simp_rw_right_ref:
(R0 <=F LET:fp_1 df_1 IN DIV) = (R0 <=F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 <=F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 <=F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 <=F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
lemmas csp_Int_simp_rw_left:
( LET:fp_1 df_1 IN DIV =F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV =F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 =F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 =F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN DIV <=F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV <=F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 <=F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 <=F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
lemmas csp_Int_simp_rw_right:
(R0 =F LET:fp_1 df_1 IN DIV) = (R0 =F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 =F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 =F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 =F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN DIV) = (R0 <=F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 <=F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 <=F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 <=F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
lemmas csp_Int_simp_rw:
( LET:fp_1 df_1 IN DIV =F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV =F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 =F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 =F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN DIV <=F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV <=F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 <=F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 <=F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
(R0 =F LET:fp_1 df_1 IN DIV) = (R0 =F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 =F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 =F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 =F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN DIV) = (R0 <=F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 <=F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 <=F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 <=F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
lemmas csp_Ext_simp:
LET:fp df IN Q =F LET:fp df IN STOP ==> LET:fp df IN Q [+] P =F LET:fp df IN P
LET:fp df IN Q =F LET:fp df IN STOP ==> LET:fp df IN P [+] Q =F LET:fp df IN P
lemmas csp_Ext_simp_rw_left_eq:
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
lemmas csp_Ext_simp_rw_left_ref:
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
lemmas csp_Ext_simp_rw_right_eq:
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
lemmas csp_Ext_simp_rw_right_ref:
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
lemmas csp_Ext_simp_rw_left:
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
lemmas csp_Ext_simp_rw_right:
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
lemmas csp_Ext_simp_rw:
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
lemmas csp_Mix_simp:
[| LET:fp df IN P1 =F LET:fp df IN STOP; LET:fp df IN P2 =F LET:fp df IN STOP |] ==> LET:fp df IN (P1 |~| P2) [+] Q =F LET:fp df IN Q
lemmas csp_Mix_simp_rw_left_eq:
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN Q_1 =F R0)
lemmas csp_Mix_simp_rw_left_ref:
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN Q_1 <=F R0)
lemmas csp_Mix_simp_rw_right_eq:
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN Q_1)
lemmas csp_Mix_simp_rw_right_ref:
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN Q_1)
lemmas csp_Mix_simp_rw_left:
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN Q_1 =F R0)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN Q_1 <=F R0)
lemmas csp_Mix_simp_rw_right:
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN Q_1)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN Q_1)
lemmas csp_Mix_simp_rw:
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN Q_1 =F R0)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN Q_1 <=F R0)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN Q_1)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN Q_1)
lemmas csp_simp:
LET:fp df IN DIV =F LET:fp df IN ! x:{} .. DIV
LET:fp df IN ! :{a} .. Pf =F LET:fp df IN Pf a
LET:fp df IN P =F LET:fp df IN Q ==> LET:fp df IN P |~| Q =F LET:fp df IN P
LET:fp df IN Q =F LET:fp df IN STOP ==> LET:fp df IN Q [+] P =F LET:fp df IN P
LET:fp df IN Q =F LET:fp df IN STOP ==> LET:fp df IN P [+] Q =F LET:fp df IN P
[| LET:fp df IN P1 =F LET:fp df IN STOP; LET:fp df IN P2 =F LET:fp df IN STOP |] ==> LET:fp df IN (P1 |~| P2) [+] Q =F LET:fp df IN Q
lemmas csp_simp_rw_left:
( LET:fp_1 df_1 IN DIV =F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV =F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 =F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 =F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN DIV <=F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV <=F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 <=F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 <=F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN Q_1 =F R0)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN Q_1 <=F R0)
lemmas csp_simp_rw_right:
(R0 =F LET:fp_1 df_1 IN DIV) = (R0 =F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 =F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 =F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 =F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN DIV) = (R0 <=F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 <=F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 <=F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 <=F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN Q_1)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN Q_1)
lemmas csp_simp_rw:
( LET:fp_1 df_1 IN DIV =F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV =F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 =F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 =F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
( LET:fp_1 df_1 IN DIV <=F R0) = ( LET:fp_1 df_1 IN ! x:{} .. DIV <=F R0)
( LET:fp_1 df_1 IN ! :{a_1} .. Pf_1 <=F R0) = ( LET:fp_1 df_1 IN Pf_1 a_1 <=F R0)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> ( LET:fp_1 df_1 IN P_1 |~| Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN P_1 =F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN Q_1 [+] P_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> ( LET:fp_1 df_1 IN P_1 [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN P_1 <=F R0)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 =F R0) = ( LET:fp_1 df_1 IN Q_1 =F R0)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> ( LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1 <=F R0) = ( LET:fp_1 df_1 IN Q_1 <=F R0)
(R0 =F LET:fp_1 df_1 IN DIV) = (R0 =F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 =F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 =F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 =F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
(R0 <=F LET:fp_1 df_1 IN DIV) = (R0 <=F LET:fp_1 df_1 IN ! x:{} .. DIV)
(R0 <=F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1) = (R0 <=F LET:fp_1 df_1 IN Pf_1 a_1)
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> (R0 <=F LET:fp_1 df_1 IN P_1 |~| Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 =F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 =F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN Q_1 [+] P_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> (R0 <=F LET:fp_1 df_1 IN P_1 [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN P_1)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 =F LET:fp_1 df_1 IN Q_1)
[| LET:fp_1 df_1 IN P1_1 =F LET:fp_1 df_1 IN STOP; LET:fp_1 df_1 IN P2_1 =F LET:fp_1 df_1 IN STOP |] ==> (R0 <=F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1) = (R0 <=F LET:fp_1 df_1 IN Q_1)
lemma on_Not_Decompo_Flag:
Not_Decompo_Flag ∧ R ==> R
lemma off_Not_Decompo_Flag:
R ==> Not_Decompo_Flag ∧ R
lemma off_Not_Decompo_Flag_True:
Not_Decompo_Flag
lemma csp_rule_flag_left_eq:
[| R1 =F R2; Not_Decompo_Flag ∧ R2 =F R0 |] ==> R1 =F R0
lemma csp_rule_flag_left_ref:
[| R1 <=F R2; Not_Decompo_Flag ∧ R2 <=F R0 |] ==> R1 <=F R0
lemma csp_rule_flag_right_eq:
[| R2 =F R1; Not_Decompo_Flag ∧ R0 =F R2 |] ==> R0 =F R1
lemma csp_rule_flag_right_ref:
[| R2 <=F R1; Not_Decompo_Flag ∧ R0 <=F R2 |] ==> R0 <=F R1
lemmas csp_rule_flag_left:
[| R1 =F R2; Not_Decompo_Flag ∧ R2 =F R0 |] ==> R1 =F R0
[| R1 <=F R2; Not_Decompo_Flag ∧ R2 <=F R0 |] ==> R1 <=F R0
lemmas csp_rule_flag_right:
[| R2 =F R1; Not_Decompo_Flag ∧ R0 =F R2 |] ==> R0 =F R1
[| R2 <=F R1; Not_Decompo_Flag ∧ R0 <=F R2 |] ==> R0 <=F R1
lemmas csp_rule_flag:
[| R1 =F R2; Not_Decompo_Flag ∧ R2 =F R0 |] ==> R1 =F R0
[| R1 <=F R2; Not_Decompo_Flag ∧ R2 <=F R0 |] ==> R1 <=F R0
[| R2 =F R1; Not_Decompo_Flag ∧ R0 =F R2 |] ==> R0 =F R1
[| R2 <=F R1; Not_Decompo_Flag ∧ R0 <=F R2 |] ==> R0 <=F R1
lemma csp_rule_tr_left_eq:
[| R1 =F R2; R2 =F R0 |] ==> R1 =F R0
lemma csp_rule_tr_left_ref:
[| R1 <=F R2; R2 <=F R0 |] ==> R1 <=F R0
lemma csp_rule_tr_right_eq:
[| R2 =F R1; R0 =F R2 |] ==> R0 =F R1
lemma csp_rule_tr_right_ref:
[| R2 <=F R1; R0 <=F R2 |] ==> R0 <=F R1
lemmas csp_rule_tr_left:
[| R1 =F R2; R2 =F R0 |] ==> R1 =F R0
[| R1 <=F R2; R2 <=F R0 |] ==> R1 <=F R0
lemmas csp_rule_tr_right:
[| R2 =F R1; R0 =F R2 |] ==> R0 =F R1
[| R2 <=F R1; R0 <=F R2 |] ==> R0 <=F R1
lemmas csp_rule_tr:
[| R1 =F R2; R2 =F R0 |] ==> R1 =F R0
[| R1 <=F R2; R2 <=F R0 |] ==> R1 <=F R0
[| R2 =F R1; R0 =F R2 |] ==> R0 =F R1
[| R2 <=F R1; R0 <=F R2 |] ==> R0 <=F R1
lemmas csp_rule_tr_eq:
[| R1 =F R2; R2 =F R0 |] ==> R1 =F R0
[| R2 =F R1; R0 =F R2 |] ==> R0 =F R1
lemmas csp_rule_tr_ref:
[| R1 <=F R2; R2 <=F R0 |] ==> R1 <=F R0
[| R2 <=F R1; R0 <=F R2 |] ==> R0 <=F R1
lemmas csp_free_mono_left:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 -- Y_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 <=F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 [[r2_1]] <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 <=F R0
lemmas csp_free_mono_right:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
lemmas csp_mono_left:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 -- Y_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 <=F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 [[r2_1]] <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 <=F R0
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN b_1 -> Q_1 <=F R0 |] ==> LET:fp1_1 df_1 IN a_1 -> P_1 <=F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1 <=F R0 |] ==> LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 <=F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1 <=F R0 |] ==> LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 <=F R0
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 <=F R0
lemmas csp_mono_right:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN a_1 -> P_1 |] ==> R0 <=F LET:fp2_1 df_1 IN b_1 -> Q_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; R0 <=F LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 |] ==> R0 <=F LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; R0 <=F LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 |] ==> R0 <=F LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1
lemmas csp_free_mono_flag_left:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 -- Y_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 <=F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 [[r2_1]] <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 <=F R0
lemmas csp_free_mono_flag_right:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
lemmas csp_mono_flag_left:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 -- Y_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 <=F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 [[r2_1]] <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 <=F R0
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN b_1 -> Q_1 <=F R0 |] ==> LET:fp1_1 df_1 IN a_1 -> P_1 <=F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1 <=F R0 |] ==> LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 <=F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1 <=F R0 |] ==> LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 <=F R0
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 <=F R0
lemmas csp_mono_flag_right:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN a_1 -> P_1 |] ==> R0 <=F LET:fp2_1 df_1 IN b_1 -> Q_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 |] ==> R0 <=F LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 |] ==> R0 <=F LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1
lemmas csp_free_cong_left:
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 -- Y_1 =F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 =F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 [[r2_1]] =F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 =F R0
lemmas csp_free_cong_right:
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
lemmas csp_cong_left:
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 -- Y_1 =F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 =F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 [[r2_1]] =F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 =F R0
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN b_1 -> Q_1 =F R0 |] ==> LET:fp1_1 df_1 IN a_1 -> P_1 =F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1 =F R0 |] ==> LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 =F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1 =F R0 |] ==> LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 =F R0
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 =F R0
lemmas csp_cong_right:
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN a_1 -> P_1 |] ==> R0 =F LET:fp2_1 df_1 IN b_1 -> Q_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; R0 =F LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 |] ==> R0 =F LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; R0 =F LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 |] ==> R0 =F LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1
lemmas csp_free_cong_flag_left:
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 -- Y_1 =F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 =F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 [[r2_1]] =F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 =F R0
lemmas csp_free_cong_flag_right:
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
lemmas csp_cong_flag_left:
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 -- Y_1 =F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 =F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 [[r2_1]] =F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 =F R0
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN b_1 -> Q_1 =F R0 |] ==> LET:fp1_1 df_1 IN a_1 -> P_1 =F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1 =F R0 |] ==> LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 =F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1 =F R0 |] ==> LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 =F R0
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 =F R0
lemmas csp_cong_flag_right:
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN a_1 -> P_1 |] ==> R0 =F LET:fp2_1 df_1 IN b_1 -> Q_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 |] ==> R0 =F LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 |] ==> R0 =F LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1
lemmas csp_free_decompo_left:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 -- Y_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 <=F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 [[r2_1]] <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 -- Y_1 =F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 =F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 [[r2_1]] =F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 =F R0
lemmas csp_free_decompo_right:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
lemmas csp_decompo_left:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 -- Y_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 <=F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 [[r2_1]] <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 <=F R0
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN b_1 -> Q_1 <=F R0 |] ==> LET:fp1_1 df_1 IN a_1 -> P_1 <=F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1 <=F R0 |] ==> LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 <=F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1 <=F R0 |] ==> LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 <=F R0
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 -- Y_1 =F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 =F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN Q_1 [[r2_1]] =F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 =F R0
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; LET:fp2_1 df_1 IN b_1 -> Q_1 =F R0 |] ==> LET:fp1_1 df_1 IN a_1 -> P_1 =F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1 =F R0 |] ==> LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 =F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1 =F R0 |] ==> LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 =F R0
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 =F R0
lemmas csp_decompo_right:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; R0 <=F LET:fp1_1 df_1 IN a_1 -> P_1 |] ==> R0 <=F LET:fp2_1 df_1 IN b_1 -> Q_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; R0 <=F LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 |] ==> R0 <=F LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; R0 <=F LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 |] ==> R0 <=F LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; R0 <=F LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; R0 =F LET:fp1_1 df_1 IN a_1 -> P_1 |] ==> R0 =F LET:fp2_1 df_1 IN b_1 -> Q_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; R0 =F LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 |] ==> R0 =F LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; R0 =F LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 |] ==> R0 =F LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; R0 =F LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1
lemmas csp_free_decompo_flag_left:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 -- Y_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 <=F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 [[r2_1]] <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 -- Y_1 =F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 =F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 [[r2_1]] =F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 =F R0
lemmas csp_free_decompo_flag_right:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
lemmas csp_decompo_flag_left:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 <=F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 -- Y_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 <=F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 [[r2_1]] <=F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] <=F R0
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 <=F R0
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN b_1 -> Q_1 <=F R0 |] ==> LET:fp1_1 df_1 IN a_1 -> P_1 <=F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1 <=F R0 |] ==> LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 <=F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1 <=F R0 |] ==> LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 <=F R0
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1 <=F R0 |] ==> LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 <=F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 [+] Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 [+] P2_1 =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |~| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |~| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 =F R0
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 -- Y_1 =F R0 |] ==> LET:fp1_1 df_1 IN P_1 -- X_1 =F R0
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q_1 [[r2_1]] =F R0 |] ==> LET:fp1_1 df_1 IN P_1 [[r1_1]] =F R0
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN Q1_1 ;; Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN P1_1 ;; P2_1 =F R0
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN b_1 -> Q_1 =F R0 |] ==> LET:fp1_1 df_1 IN a_1 -> P_1 =F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1 =F R0 |] ==> LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 =F R0
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1 =F R0 |] ==> LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 =F R0
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1 =F R0 |] ==> LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 =F R0
lemmas csp_decompo_flag_right:
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 <=F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 <=F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN a_1 -> P_1 |] ==> R0 <=F LET:fp2_1 df_1 IN b_1 -> Q_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 |] ==> R0 <=F LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a <=F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 |] ==> R0 <=F LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 <=F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 <=F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 <=F LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 |] ==> R0 <=F LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 [+] P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 [+] Q2_1
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 |~| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |~| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 |[X_1]| P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 |[Y_1]| Q2_1
[| X_1 = Y_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P_1 -- X_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 -- Y_1
[| r1_1 = r2_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P_1 [[r1_1]] |] ==> R0 =F LET:fp2_1 df_1 IN Q_1 [[r2_1]]
[| LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN P1_1 ;; P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN Q1_1 ;; Q2_1
[| a_1 = b_1; LET:fp1_1 df_1 IN P_1 =F LET:fp2_1 df_1 IN Q_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN a_1 -> P_1 |] ==> R0 =F LET:fp2_1 df_1 IN b_1 -> Q_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN ? :X_1 -> Pf_1 |] ==> R0 =F LET:fp2_1 df_1 IN ? :Y_1 -> Qf_1
[| X_1 = Y_1; !!a. a ∈ Y_1 ==> LET:fp1_1 df_1 IN Pf_1 a =F LET:fp2_1 df_1 IN Qf_1 a; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN ! :X_1 .. Pf_1 |] ==> R0 =F LET:fp2_1 df_1 IN ! :Y_1 .. Qf_1
[| b1_1 = b2_1; LET:fp1_1 df_1 IN P1_1 =F LET:fp2_1 df_1 IN Q1_1; LET:fp1_1 df_1 IN P2_1 =F LET:fp2_1 df_1 IN Q2_1; Not_Decompo_Flag ∧ R0 =F LET:fp1_1 df_1 IN IF b1_1 THEN P1_1 ELSE P2_1 |] ==> R0 =F LET:fp2_1 df_1 IN IF b2_1 THEN Q1_1 ELSE Q2_1
lemma csp_rw_flag_left_eq:
[| R1 =F R2; Not_Decompo_Flag ∧ R2 =F R3 |] ==> R1 =F R3
lemma csp_rw_flag_left_ref:
[| R1 =F R2; Not_Decompo_Flag ∧ R2 <=F R3 |] ==> R1 <=F R3
lemmas csp_rw_flag_left:
[| R1 =F R2; Not_Decompo_Flag ∧ R2 =F R3 |] ==> R1 =F R3
[| R1 =F R2; Not_Decompo_Flag ∧ R2 <=F R3 |] ==> R1 <=F R3
lemma csp_rw_flag_right_eq:
[| R3 =F R2; Not_Decompo_Flag ∧ R1 =F R2 |] ==> R1 =F R3
lemma csp_rw_flag_right_ref:
[| R3 =F R2; Not_Decompo_Flag ∧ R1 <=F R2 |] ==> R1 <=F R3
lemmas csp_rw_flag_right:
[| R3 =F R2; Not_Decompo_Flag ∧ R1 =F R2 |] ==> R1 =F R3
[| R3 =F R2; Not_Decompo_Flag ∧ R1 <=F R2 |] ==> R1 <=F R3
lemma csp_tr_flag_left_eq:
[| R1 =F R2; Not_Decompo_Flag ∧ R2 =F R3 |] ==> R1 =F R3
lemma csp_tr_flag_left_ref:
[| R1 <=F R2; Not_Decompo_Flag ∧ R2 <=F R3 |] ==> R1 <=F R3
lemmas csp_tr_flag_left:
[| R1 =F R2; Not_Decompo_Flag ∧ R2 =F R3 |] ==> R1 =F R3
[| R1 <=F R2; Not_Decompo_Flag ∧ R2 <=F R3 |] ==> R1 <=F R3
lemma csp_tr_flag_right_eq:
[| R2 =F R3; Not_Decompo_Flag ∧ R1 =F R2 |] ==> R1 =F R3
lemma csp_tr_flag_right_ref:
[| R2 <=F R3; Not_Decompo_Flag ∧ R1 <=F R2 |] ==> R1 <=F R3
lemmas csp_tr_flag_right:
[| R2 =F R3; Not_Decompo_Flag ∧ R1 =F R2 |] ==> R1 =F R3
[| R2 <=F R3; Not_Decompo_Flag ∧ R1 <=F R2 |] ==> R1 <=F R3