Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F
theory CSP_F_law_aux (*-------------------------------------------*
| CSP-Prover on Isabelle2005 |
| April 2006 |
| March 2007 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_F_law_aux
imports CSP_F_law
begin
(*---------------------------------------------------------------*
| |
| convenient laws, especially for tactics |
| |
*---------------------------------------------------------------*)
(*****************************************************************
Internal
*****************************************************************)
(*------------------*
| singleton |
*------------------*)
(*** ! :{a} ***)
lemma cspF_Rep_int_choice_sum1_singleton:
"!! : type1 {c} .. Pf =F[M,M] Pf (type1 c)"
by (rule cspF_Rep_int_choice_const, auto)
lemma cspF_Rep_int_choice_sum2_singleton:
"!! : type2 {c} .. Pf =F[M,M] Pf (type2 c)"
by (rule cspF_Rep_int_choice_const, auto)
lemma cspF_Rep_int_choice_nat_singleton:
"!nat :{n} .. Pf =F[M,M] Pf n"
by (rule cspF_Rep_int_choice_const, auto)
lemma cspF_Rep_int_choice_set_singleton:
"!set :{X} .. Pf =F[M,M] Pf X"
by (rule cspF_Rep_int_choice_const, auto)
lemma cspF_Rep_int_choice_com_singleton:
"! :{a} .. Pf =F[M,M] Pf a"
by (rule cspF_Rep_int_choice_const, auto)
lemma cspF_Rep_int_choice_f_singleton:
"inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x"
by (rule cspF_Rep_int_choice_const, auto)
lemmas cspF_Rep_int_choice_singleton =
cspF_Rep_int_choice_sum1_singleton
cspF_Rep_int_choice_sum2_singleton
cspF_Rep_int_choice_nat_singleton
cspF_Rep_int_choice_set_singleton
cspF_Rep_int_choice_com_singleton
cspF_Rep_int_choice_f_singleton
lemma cspF_Rep_int_choice_const_sum_rule:
"!! c:C .. P =F[M,M] IF (sumset C={}) THEN DIV ELSE P"
apply (case_tac "sumset C={}")
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Rep_int_choice_empty)
apply (simp)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (rule cspF_Rep_int_choice_const)
apply (simp_all)
done
lemma cspF_Rep_int_choice_const_nat_rule:
"!nat n:N .. P =F[M,M] IF (N={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_ss_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const_sum_rule)
by (simp)
lemma cspF_Rep_int_choice_const_set_rule:
"!set X:Xs .. P =F[M,M] IF (Xs={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_ss_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const_sum_rule)
by (simp)
lemma cspF_Rep_int_choice_const_com_rule:
"! x:X .. P =F[M,M] IF (X={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const_set_rule)
by (simp)
lemma cspF_Rep_int_choice_const_f_rule:
"!<f> x:X .. P =F[M,M] IF (X={}) THEN DIV ELSE P"
apply (simp add: Rep_int_choice_f_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_const_com_rule)
by (simp)
lemmas cspF_Rep_int_choice_const_rule =
cspF_Rep_int_choice_const_sum_rule
cspF_Rep_int_choice_const_nat_rule
cspF_Rep_int_choice_const_set_rule
cspF_Rep_int_choice_const_com_rule
cspF_Rep_int_choice_const_f_rule
lemmas cspF_Int_choice_rule = cspF_Rep_int_choice_empty
cspF_Rep_int_choice_singleton
cspF_Int_choice_idem
cspF_Rep_int_choice_const_rule
(*****************************************************************
External
*****************************************************************)
(* to make produced process be concrete *)
lemma cspF_Ext_pre_choice_empty_DIV:
"? :{} -> Pf =F[M1,M2] ? a:{} -> DIV"
apply (rule cspF_rw_left)
apply (rule cspF_STOP_step[THEN cspF_sym])
apply (rule cspF_STOP_step)
done
lemma cspF_Ext_choice_unit_l_hsf:
"? :{} -> Qf [+] P =F[M,M] P"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_step[THEN cspF_sym])
apply (rule cspF_reflex)
apply (simp add: cspF_unit)
done
lemma cspF_Ext_choice_unit_r_hsf:
"P [+] ? :{} -> Qf =F[M,M] P"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (simp add: cspF_Ext_choice_unit_l_hsf)
done
lemmas cspF_Ext_choice_rule = cspF_Ext_pre_choice_empty_DIV
cspF_Ext_choice_unit_l
cspF_Ext_choice_unit_l_hsf
cspF_Ext_choice_unit_r
cspF_Ext_choice_unit_r_hsf
cspF_Ext_choice_idem
(*-----------------------------*
| simp rule for cspF |
*-----------------------------*)
lemmas cspF_choice_rule = cspF_Int_choice_rule cspF_Ext_choice_rule
(*****************************************************************
Timeout
*****************************************************************)
(*------------------*
| csp law |
*------------------*)
(*** <= Timeout ***)
lemma cspF_Timeout_right:
"[| P <=F[M1,M2] Q1 ; P <=F[M1,M2] Q2 |] ==> P <=F[M1,M2] Q1 [> Q2"
apply (rule cspF_rw_right)
apply (rule cspF_dist)
apply (rule cspF_Int_choice_right)
apply (rule cspF_Ext_choice_right, simp_all)
apply (rule cspF_rw_right)
apply (rule cspF_Ext_choice_unit_l, simp_all)
done
(*** STOP [> P = P ***)
lemma cspF_STOP_Timeout:
"STOP [> P =F[M,M] P"
apply (rule cspF_rw_left)
apply (rule cspF_dist)
apply (rule cspF_rw_left)
apply (rule cspF_Int_choice_idem)
apply (rule cspF_unit)
done
(*================================================*
| |
| auxiliary step laws |
| |
*================================================*)
(* split + resolve *)
lemma cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV:
"[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
((? :Y -> Pf) [+] P) |[X]| ((? :Z -> Qf) [+] Q) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] Q))
|~| (((? x:Y -> Pf x) [+] P) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] Q))
ELSE (((? x:Y -> Pf x) [+] P) |[X]| Qf x))
[> (((P |[X]| ((? :Z -> Qf) [+] Q)) |~|
(((? :Y -> Pf) [+] P) |[X]| Q)))"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Timeout_split)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
done
lemma cspF_Parallel_Timeout_split_resolve_SKIP_SKIP:
"((? :Y -> Pf) [+] SKIP) |[X]| ((? :Z -> Qf) [+] SKIP) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
|~| (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
ELSE (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
[> (((SKIP |[X]| ((? :Z -> Qf) [+] SKIP)) |~|
(((? :Y -> Pf) [+] SKIP) |[X]| SKIP)))"
by (simp add: cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV)
lemma cspF_Parallel_Timeout_split_resolve_DIV_DIV:
"((? :Y -> Pf) [+] DIV) |[X]| ((? :Z -> Qf) [+] DIV) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
|~| (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
ELSE (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
[> (((DIV |[X]| ((? :Z -> Qf) [+] DIV)) |~|
(((? :Y -> Pf) [+] DIV) |[X]| DIV)))"
by (simp add: cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV)
lemma cspF_Parallel_Timeout_split_resolve_SKIP_DIV:
"((? :Y -> Pf) [+] SKIP) |[X]| ((? :Z -> Qf) [+] DIV) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
|~| (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
ELSE (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
[> (((SKIP |[X]| ((? :Z -> Qf) [+] DIV)) |~|
(((? :Y -> Pf) [+] SKIP) |[X]| DIV)))"
by (simp add: cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV)
lemma cspF_Parallel_Timeout_split_resolve_DIV_SKIP:
"((? :Y -> Pf) [+] DIV) |[X]| ((? :Z -> Qf) [+] SKIP) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
|~| (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
ELSE (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
[> (((DIV |[X]| ((? :Z -> Qf) [+] SKIP)) |~|
(((? :Y -> Pf) [+] DIV) |[X]| SKIP)))"
by (simp add: cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV)
lemmas cspF_Parallel_Timeout_split_resolve =
cspF_Parallel_Timeout_split_resolve_SKIP_SKIP
cspF_Parallel_Timeout_split_resolve_DIV_DIV
cspF_Parallel_Timeout_split_resolve_SKIP_DIV
cspF_Parallel_Timeout_split_resolve_DIV_SKIP
(* input + resolve *)
lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_l:
"P = SKIP | P = DIV ==>
((? :Y -> Pf) [+] P) |[X]| (? :Z -> Qf) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| (? x:Z -> Qf x))
|~| (((? x:Y -> Pf x) [+] P) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| (? x:Z -> Qf x))
ELSE (((? x:Y -> Pf x) [+] P) |[X]| Qf x))
[> (((P |[X]| (? :Z -> Qf))))"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_reflex)
apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Timeout_input)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (simp)
apply (simp)
done
lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_r:
"Q = SKIP | Q = DIV ==>
(? :Y -> Pf) |[X]| ((? :Z -> Qf) [+] Q) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] Q))
|~| ((? x:Y -> Pf x) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] Q))
ELSE ((? x:Y -> Pf x) |[X]| Qf x))
[> ((((? :Y -> Pf) |[X]| Q)))"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_reflex)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_Parallel_Timeout_input)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve[THEN cspF_sym])
apply (simp)
apply (simp)
apply (simp)
apply (simp)
done
lemmas cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV =
cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_l
cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_r
lemma cspF_Parallel_Timeout_input_resolve_SKIP_l:
"((? :Y -> Pf) [+] SKIP) |[X]| (? :Z -> Qf) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| (? x:Z -> Qf x))
|~| (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| (? x:Z -> Qf x))
ELSE (((? x:Y -> Pf x) [+] SKIP) |[X]| Qf x))
[> (((SKIP |[X]| (? :Z -> Qf))))"
by (simp add: cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV)
lemma cspF_Parallel_Timeout_input_resolve_DIV_l:
"((? :Y -> Pf) [+] DIV) |[X]| (? :Z -> Qf) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| (? x:Z -> Qf x))
|~| (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| (? x:Z -> Qf x))
ELSE (((? x:Y -> Pf x) [+] DIV) |[X]| Qf x))
[> (((DIV |[X]| (? :Z -> Qf))))"
by (simp add: cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV)
lemma cspF_Parallel_Timeout_input_resolve_SKIP_r:
"(? :Y -> Pf) |[X]| ((? :Z -> Qf) [+] SKIP) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
|~| ((? x:Y -> Pf x) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] SKIP))
ELSE ((? x:Y -> Pf x) |[X]| Qf x))
[> ((((? :Y -> Pf) |[X]| SKIP)))"
by (simp add: cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV)
lemma cspF_Parallel_Timeout_input_resolve_DIV_r:
"(? :Y -> Pf) |[X]| ((? :Z -> Qf) [+] DIV) =F[M,M]
(? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
-> IF (x : X) THEN (Pf x |[X]| Qf x)
ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
|~| ((? x:Y -> Pf x) |[X]| Qf x))
ELSE IF (x : Y) THEN (Pf x |[X]| ((? x:Z -> Qf x) [+] DIV))
ELSE ((? x:Y -> Pf x) |[X]| Qf x))
[> ((((? :Y -> Pf) |[X]| DIV)))"
by (simp add: cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV)
lemmas cspF_Parallel_Timeout_input_resolve =
cspF_Parallel_Timeout_input_resolve_SKIP_l
cspF_Parallel_Timeout_input_resolve_SKIP_r
cspF_Parallel_Timeout_input_resolve_DIV_l
cspF_Parallel_Timeout_input_resolve_DIV_r
(**************** ;; + resolve ****************)
lemma cspF_SKIP_Seq_compo_step_resolve:
"((? :X -> Pf) [+] SKIP) ;; Q =F[M,M] (? x:X -> (Pf x ;; Q)) [> Q"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_reflex)
apply (rule cspF_SKIP_Seq_compo_step)
done
lemma cspF_DIV_Seq_compo_step_resolve:
"((? :X -> Pf) [+] DIV) ;; Q =F[M,M] (? x:X -> (Pf x ;; Q)) [+] DIV"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_Ext_choice_SKIP_or_DIV_resolve)
apply (simp)
apply (rule cspF_reflex)
apply (rule cspF_rw_left)
apply (rule cspF_DIV_Seq_compo_step)
apply (rule cspF_Ext_choice_SKIP_DIV_resolve[THEN cspF_sym])
done
lemmas cspF_SKIP_DIV_Seq_compo_step_resolve =
cspF_SKIP_Seq_compo_step_resolve
cspF_DIV_Seq_compo_step_resolve
(****** for sequentilising processes with SKIP or DIV ******)
lemmas cspF_SKIP_DIV_resolve =
cspF_SKIP_DIV
cspF_Parallel_Timeout_split_resolve
cspF_Parallel_Timeout_input_resolve
cspF_SKIP_DIV_Seq_compo_step_resolve
lemmas cspF_SKIP_or_DIV_resolve =
cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV
cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV
(*=========================================================*
| |
| for convenience, especially for fully sequntialising |
| |
*=========================================================*)
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_l:
"Q = SKIP | Q = DIV | Q = STOP ==>
(P [+] Q) |[X]| DIV =F[M,M] (P |[X]| DIV)"
apply (erule disjE)
apply (simp)
apply (rule cspF_SKIP_DIV)
apply (erule disjE)
apply (simp)
apply (rule cspF_SKIP_DIV)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (rule cspF_unit)
apply (rule cspF_reflex)
apply (rule cspF_reflex)
done
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_r:
"Q = SKIP | Q = DIV | Q = STOP ==>
DIV |[X]| (P [+] Q) =F[M,M] (DIV |[X]| P)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_right)
apply (rule cspF_commut)
apply (simp add: cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_l)
done
lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV =
cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_l
cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_r
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_l:
"Q = SKIP | Q = DIV | Q = STOP ==>
((? :Y -> Pf) [+] Q) |[X]| SKIP =F[M,M]
(? x:(Y - X) -> (Pf x |[X]| SKIP)) [+] Q"
apply (erule disjE)
apply (simp)
apply (rule cspF_SKIP_DIV)
apply (erule disjE)
apply (simp)
apply (rule cspF_SKIP_DIV)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp_all)
apply (rule cspF_unit)
apply (rule cspF_reflex)
apply (rule cspF_rw_right)
apply (rule cspF_unit)
apply (rule cspF_SKIP_DIV)
done
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_r:
"Q = SKIP | Q = DIV | Q = STOP ==>
SKIP |[X]| ((? :Y -> Pf) [+] Q) =F[M,M]
(? x:(Y - X) -> (SKIP |[X]| Pf x)) [+] Q"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_commut)
apply (rule cspF_reflex)
apply (simp add: cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_l)
done
lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP =
cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_l
cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_r
lemmas cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice =
cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV
cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP
(* renaming *)
lemma cspF_SKIP_or_DIV_or_STOP_Renaming_Id:
"P = SKIP | P = DIV | P = STOP ==> P [[r]] =F[M,M] P"
apply (erule disjE)
apply (simp add: cspF_SKIP_DIV)
apply (erule disjE)
apply (simp add: cspF_SKIP_DIV)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_step)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Ext_pre_choice_empty_DIV)
apply (rule cspF_rw_left)
apply (rule cspF_step)
apply (rule cspF_rw_right)
apply (rule cspF_step)
apply (rule cspF_decompo)
apply (auto)
done
(* restg *)
lemma cspF_STOP_Depth_rest:
"STOP |. Suc n =F[M,M] STOP"
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_step)
apply (rule cspF_rw_left)
apply (rule cspF_step)
apply (rule cspF_rw_right)
apply (rule cspF_step)
apply (rule cspF_decompo)
apply (auto)
done
(*==============================================================*
| |
| Associativity and Commutativity for SKIP and DIV |
| (for sequentialising) |
| |
*==============================================================*)
lemma cspF_Ext_pre_choice_SKIP_commut:
"SKIP [+] (? :X -> Pf) =F[M,M] (? :X -> Pf) [+] SKIP"
by (rule cspF_commut)
lemma cspF_Ext_pre_choice_DIV_commut:
"DIV [+] (? :X -> Pf) =F[M,M] (? :X -> Pf) [+] DIV"
by (rule cspF_commut)
lemma cspF_Ext_pre_choice_SKIP_assoc:
"((? :X -> Pf) [+] SKIP) [+] (? :Y -> Qf)
=F[M,M] ((? :X -> Pf) [+] (? :Y -> Qf)) [+] SKIP"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_commut)
apply (rule cspF_assoc)
done
lemma cspF_Ext_pre_choice_DIV_assoc:
"((? :X -> Pf) [+] DIV) [+] (? :Y -> Qf)
=F[M,M] ((? :X -> Pf) [+] (? :Y -> Qf)) [+] DIV"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_commut)
apply (rule cspF_assoc)
done
lemma cspF_Ext_choice_idem_assoc:
"(P [+] Q) [+] Q =F[M,M] (P [+] Q)"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_idem)
apply (rule cspF_reflex)
done
lemma cspF_Ext_choice_SKIP_DIV_assoc:
"(P [+] SKIP) [+] DIV =F[M,M] (P [+] SKIP)"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_SKIP_DIV)
apply (rule cspF_reflex)
done
lemma cspF_Ext_choice_DIV_SKIP_assoc:
"(P [+] DIV) [+] SKIP =F[M,M] (P [+] SKIP)"
apply (rule cspF_rw_left)
apply (rule cspF_assoc[THEN cspF_sym])
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_SKIP_DIV)
apply (rule cspF_reflex)
done
lemmas cspF_SKIP_DIV_sort =
cspF_Ext_choice_assoc
cspF_Ext_pre_choice_SKIP_commut
cspF_Ext_pre_choice_DIV_commut
cspF_Ext_pre_choice_SKIP_assoc
cspF_Ext_pre_choice_DIV_assoc
cspF_Ext_choice_idem_assoc
cspF_Ext_choice_SKIP_DIV_assoc
cspF_Ext_choice_DIV_SKIP_assoc
(*==============================================================*
| |
| decompostion control by the flag "Not_Decompo_Flag" |
| |
*==============================================================*)
(*------------------------------------------------*
| trans with Flag |
*------------------------------------------------*)
(*** rewrite (eq) ***)
lemma cspF_rw_flag_left_eq:
"[| R1 =F[M1,M1] R2 ; Not_Decompo_Flag & R2 =F[M1,M3] R3 |] ==> R1 =F[M1,M3] R3"
by (simp add: eqF_def Not_Decompo_Flag_def)
lemma cspF_rw_flag_left_ref:
"[| R1 =F[M1,M1] R2 ; Not_Decompo_Flag & R2 <=F[M1,M3] R3 |] ==> R1 <=F[M1,M3] R3"
by (simp add: refF_def eqF_def Not_Decompo_Flag_def)
lemmas cspF_rw_flag_left = cspF_rw_flag_left_eq cspF_rw_flag_left_ref
lemma cspF_rw_flag_right_eq:
"[| R3 =F[M3,M3] R2 ; Not_Decompo_Flag & R1 =F[M1,M3] R2 |] ==> R1 =F[M1,M3] R3"
by (simp add: eqF_def Not_Decompo_Flag_def)
lemma cspF_rw_flag_right_ref:
"[| R3 =F[M3,M3] R2 ; Not_Decompo_Flag & R1 <=F[M1,M3] R2 |] ==> R1 <=F[M1,M3] R3"
by (simp add: refF_def eqF_def Not_Decompo_Flag_def)
lemmas cspF_rw_flag_right = cspF_rw_flag_right_eq cspF_rw_flag_right_ref
(*------------------------------------------------*
| trans with Flag (ref) |
*------------------------------------------------*)
lemma cspF_tr_flag_left_eq:
"[| P1 =F[M1,M1] P2 ; Not_Decompo_Flag & P2 =F[M1,M3] P3 |] ==> P1 =F[M1,M3] P3"
by (simp add: eqF_def)
lemma cspF_tr_flag_left_ref:
"[| P1 <=F[M1,M1] P2 ; Not_Decompo_Flag & P2 <=F[M1,M3] P3 |] ==> P1 <=F[M1,M3] P3"
by (simp add: refF_def eqF_def Not_Decompo_Flag_def)
lemmas cspF_tr_flag_left = cspF_tr_flag_left_eq cspF_tr_flag_left_ref
lemma cspF_tr_flag_right_eq:
"[| P2 =F[M3,M3] P3 ; Not_Decompo_Flag & P1 =F[M1,M3] P2 |] ==> P1 =F[M1,M3] P3"
by (simp add: eqF_def)
lemma cspF_tr_flag_right_ref:
"[| P2 <=F[M3,M3] P3 ; Not_Decompo_Flag & P1 <=F[M1,M3] P2 |] ==> P1 <=F[M1,M3] P3"
by (simp add: refF_def eqF_def Not_Decompo_Flag_def)
lemmas cspF_tr_flag_right = cspF_tr_flag_right_eq cspF_tr_flag_right_ref
(*==============================================================*
| decompostion of Sequential composition with a flag |
| It is often useful that the second process is not expanded. |
*==============================================================*)
lemma cspF_Seq_compo_mono_flag:
"[| P1 <=F[M1,M2] Q1 ;
Not_Decompo_Flag & P2 <=F[M1,M2] Q2 |]
==> P1 ;; P2 <=F[M1,M2] Q1 ;; Q2"
by (simp add: cspF_Seq_compo_mono)
lemma cspF_Seq_compo_cong_flag:
"[| P1 =F[M1,M2] Q1 ;
Not_Decompo_Flag & P2 =F[M1,M2] Q2 |]
==> P1 ;; P2 =F[M1,M2] Q1 ;; Q2"
by (simp add: cspF_Seq_compo_cong)
lemmas cspF_free_mono_flag =
cspF_Ext_choice_mono cspF_Int_choice_mono cspF_Parallel_mono
cspF_Hiding_mono cspF_Renaming_mono cspF_Seq_compo_mono_flag
cspF_Depth_rest_mono
lemmas cspF_free_cong_flag =
cspF_Ext_choice_cong cspF_Int_choice_cong cspF_Parallel_cong
cspF_Hiding_cong cspF_Renaming_cong cspF_Seq_compo_cong_flag
cspF_Depth_rest_cong
lemmas cspF_free_decompo_flag = cspF_free_mono_flag cspF_free_cong_flag
end
lemma cspF_Rep_int_choice_sum1_singleton:
!! :type1 {c} .. Pf =F[M,M] Pf (type1 c)
lemma cspF_Rep_int_choice_sum2_singleton:
!! :type2 {c} .. Pf =F[M,M] Pf (type2 c)
lemma cspF_Rep_int_choice_nat_singleton:
!nat :{n} .. Pf =F[M,M] Pf n
lemma cspF_Rep_int_choice_set_singleton:
!set :{X} .. Pf =F[M,M] Pf X
lemma cspF_Rep_int_choice_com_singleton:
! :{a} .. Pf =F[M,M] Pf a
lemma cspF_Rep_int_choice_f_singleton:
inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x
lemma cspF_Rep_int_choice_singleton:
!! :type1 {c} .. Pf =F[M,M] Pf (type1 c)
!! :type2 {c} .. Pf =F[M,M] Pf (type2 c)
!nat :{n} .. Pf =F[M,M] Pf n
!set :{X} .. Pf =F[M,M] Pf X
! :{a} .. Pf =F[M,M] Pf a
inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x
lemma cspF_Rep_int_choice_const_sum_rule:
!! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P
lemma cspF_Rep_int_choice_const_nat_rule:
!nat n:N .. P =F[M,M] IF (N = {}) THEN DIV ELSE P
lemma cspF_Rep_int_choice_const_set_rule:
!set X:Xs .. P =F[M,M] IF (Xs = {}) THEN DIV ELSE P
lemma cspF_Rep_int_choice_const_com_rule:
! x:X .. P =F[M,M] IF (X = {}) THEN DIV ELSE P
lemma cspF_Rep_int_choice_const_f_rule:
!<f> x:X .. P =F[M,M] IF (X = {}) THEN DIV ELSE P
lemma cspF_Rep_int_choice_const_rule:
!! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P
!nat n:N .. P =F[M,M] IF (N = {}) THEN DIV ELSE P
!set X:Xs .. P =F[M,M] IF (Xs = {}) THEN DIV ELSE P
! x:X .. P =F[M,M] IF (X = {}) THEN DIV ELSE P
!<f> x:X .. P =F[M,M] IF (X = {}) THEN DIV ELSE P
lemma cspF_Int_choice_rule:
sumset C = {} ==> !! :C .. Pf =F[M1.0,M2.0] DIV
!nat :{} .. Pf =F[M1.0,M2.0] DIV
!set :{} .. Pf =F[M1.0,M2.0] DIV
! :{} .. Pf =F[M1.0,M2.0] DIV
inj f ==> !<f> :{} .. Pf =F[M1.0,M2.0] DIV
!! :type1 {c} .. Pf =F[M,M] Pf (type1 c)
!! :type2 {c} .. Pf =F[M,M] Pf (type2 c)
!nat :{n} .. Pf =F[M,M] Pf n
!set :{X} .. Pf =F[M,M] Pf X
! :{a} .. Pf =F[M,M] Pf a
inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x
P |~| P =F[M,M] P
!! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P
!nat n:N .. P =F[M,M] IF (N = {}) THEN DIV ELSE P
!set X:Xs .. P =F[M,M] IF (Xs = {}) THEN DIV ELSE P
! x:X .. P =F[M,M] IF (X = {}) THEN DIV ELSE P
!<f> x:X .. P =F[M,M] IF (X = {}) THEN DIV ELSE P
lemma cspF_Ext_pre_choice_empty_DIV:
? :{} -> Pf =F[M1.0,M2.0] ? a:{} -> DIV
lemma cspF_Ext_choice_unit_l_hsf:
? :{} -> Qf [+] P =F[M,M] P
lemma cspF_Ext_choice_unit_r_hsf:
P [+] ? :{} -> Qf =F[M,M] P
lemma cspF_Ext_choice_rule:
? :{} -> Pf =F[M1.0,M2.0] ? a:{} -> DIV
STOP [+] P =F[M,M] P
? :{} -> Qf [+] P =F[M,M] P
P [+] STOP =F[M,M] P
P [+] ? :{} -> Qf =F[M,M] P
P [+] P =F[M,M] P
lemma cspF_choice_rule:
sumset C = {} ==> !! :C .. Pf =F[M1.0,M2.0] DIV
!nat :{} .. Pf =F[M1.0,M2.0] DIV
!set :{} .. Pf =F[M1.0,M2.0] DIV
! :{} .. Pf =F[M1.0,M2.0] DIV
inj f ==> !<f> :{} .. Pf =F[M1.0,M2.0] DIV
!! :type1 {c} .. Pf =F[M,M] Pf (type1 c)
!! :type2 {c} .. Pf =F[M,M] Pf (type2 c)
!nat :{n} .. Pf =F[M,M] Pf n
!set :{X} .. Pf =F[M,M] Pf X
! :{a} .. Pf =F[M,M] Pf a
inj f ==> !<f> :{x} .. Pf =F[M,M] Pf x
P |~| P =F[M,M] P
!! c:C .. P =F[M,M] IF (sumset C = {}) THEN DIV ELSE P
!nat n:N .. P =F[M,M] IF (N = {}) THEN DIV ELSE P
!set X:Xs .. P =F[M,M] IF (Xs = {}) THEN DIV ELSE P
! x:X .. P =F[M,M] IF (X = {}) THEN DIV ELSE P
!<f> x:X .. P =F[M,M] IF (X = {}) THEN DIV ELSE P
? :{} -> Pf =F[M1.0,M2.0] ? a:{} -> DIV
STOP [+] P =F[M,M] P
? :{} -> Qf [+] P =F[M,M] P
P [+] STOP =F[M,M] P
P [+] ? :{} -> Qf =F[M,M] P
P [+] P =F[M,M] P
lemma cspF_Timeout_right:
[| P <=F[M1.0,M2.0] Q1.0; P <=F[M1.0,M2.0] Q2.0 |]
==> P <=F[M1.0,M2.0] Q1.0 [> Q2.0
lemma cspF_STOP_Timeout:
STOP [> P =F[M,M] P
lemma cspF_Parallel_Timeout_split_resolve_SKIP_or_DIV:
[| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
==> (? :Y -> Pf [+] P) |[X]| (? :Z -> Qf [+] Q) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] Q)
|~| (? :Y -> Pf [+] P) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] Q))
ELSE ((? :Y -> Pf [+] P) |[X]| Qf x)
[> (P |[X]| (? :Z -> Qf [+] Q) |~| (? :Y -> Pf [+] P) |[X]| Q)
lemma cspF_Parallel_Timeout_split_resolve_SKIP_SKIP:
(? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP)
|~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> (SKIP |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] SKIP) |[X]| SKIP)
lemma cspF_Parallel_Timeout_split_resolve_DIV_DIV:
(? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV)
|~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> (DIV |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] DIV) |[X]| DIV)
lemma cspF_Parallel_Timeout_split_resolve_SKIP_DIV:
(? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV)
|~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> (SKIP |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] SKIP) |[X]| DIV)
lemma cspF_Parallel_Timeout_split_resolve_DIV_SKIP:
(? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP)
|~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> (DIV |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] DIV) |[X]| SKIP)
lemma cspF_Parallel_Timeout_split_resolve:
(? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP)
|~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> (SKIP |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] SKIP) |[X]| SKIP)
(? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV)
|~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> (DIV |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] DIV) |[X]| DIV)
(? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV)
|~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> (SKIP |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] SKIP) |[X]| DIV)
(? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP)
|~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> (DIV |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] DIV) |[X]| SKIP)
lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_l:
P = SKIP ∨ P = DIV
==> (? :Y -> Pf [+] P) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] P) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] P) |[X]| Qf x)
[> P |[X]| ? :Z -> Qf
lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV_r:
Q = SKIP ∨ Q = DIV
==> ? :Y -> Pf |[X]| (? :Z -> Qf [+] Q) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] Q) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] Q))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| Q
lemma cspF_Parallel_Timeout_input_resolve_SKIP_or_DIV:
P = SKIP ∨ P = DIV
==> (? :Y -> Pf [+] P) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] P) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] P) |[X]| Qf x)
[> P |[X]| ? :Z -> Qf
Q = SKIP ∨ Q = DIV
==> ? :Y -> Pf |[X]| (? :Z -> Qf [+] Q) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] Q) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] Q))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| Q
lemma cspF_Parallel_Timeout_input_resolve_SKIP_l:
(? :Y -> Pf [+] SKIP) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> SKIP |[X]| ? :Z -> Qf
lemma cspF_Parallel_Timeout_input_resolve_DIV_l:
(? :Y -> Pf [+] DIV) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> DIV |[X]| ? :Z -> Qf
lemma cspF_Parallel_Timeout_input_resolve_SKIP_r:
? :Y -> Pf |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| SKIP
lemma cspF_Parallel_Timeout_input_resolve_DIV_r:
? :Y -> Pf |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| DIV
lemma cspF_Parallel_Timeout_input_resolve:
(? :Y -> Pf [+] SKIP) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> SKIP |[X]| ? :Z -> Qf
? :Y -> Pf |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| SKIP
(? :Y -> Pf [+] DIV) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> DIV |[X]| ? :Z -> Qf
? :Y -> Pf |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| DIV
lemma cspF_SKIP_Seq_compo_step_resolve:
(? :X -> Pf [+] SKIP) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> Q
lemma cspF_DIV_Seq_compo_step_resolve:
(? :X -> Pf [+] DIV) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [+] DIV
lemma cspF_SKIP_DIV_Seq_compo_step_resolve:
(? :X -> Pf [+] SKIP) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> Q
(? :X -> Pf [+] DIV) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [+] DIV
lemma cspF_SKIP_DIV_resolve:
SKIP |[X]| ? :Y -> Qf =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Qf x)
? :Y -> Pf |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP)
DIV |[X]| ? :Y -> Qf =F[M,M] ? x:(Y - X) -> (DIV |[X]| Qf x) [+] DIV
? :Y -> Qf |[X]| DIV =F[M,M] ? x:(Y - X) -> (Qf x |[X]| DIV) [+] DIV
SKIP [+] DIV =F[M1.0,M2.0] SKIP
DIV [+] SKIP =F[M1.0,M2.0] SKIP
SKIP |[X]| DIV =F[M1.0,M2.0] DIV
DIV |[X]| SKIP =F[M1.0,M2.0] DIV
SKIP |[X]| SKIP =F[M1.0,M2.0] SKIP
DIV |[X]| DIV =F[M1.0,M2.0] DIV
(? :Y -> Pf [+] SKIP) |[X]| SKIP =F[M,M]
? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP
SKIP |[X]| (? :Y -> Pf [+] SKIP) =F[M,M]
? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP
(? :Y -> Pf [+] DIV) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV
SKIP |[X]| (? :Y -> Pf [+] DIV) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV
(P [+] SKIP) |[X]| DIV =F[M,M] P |[X]| DIV
DIV |[X]| (P [+] SKIP) =F[M,M] DIV |[X]| P
(P [+] DIV) |[X]| DIV =F[M,M] P |[X]| DIV
DIV |[X]| (P [+] DIV) =F[M,M] DIV |[X]| P
SKIP -- X =F[M,M] SKIP
DIV -- X =F[M1.0,M2.0] DIV
(? :Y -> Pf [+] DIV) -- X =F[M,M]
? x:(Y - X) -> Pf x -- X [+] DIV |~| ! x:(Y ∩ X) .. Pf x -- X
(? :Y -> Pf [+] SKIP) -- X =F[M,M]
? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X
SKIP [[r]] =F[M1.0,M2.0] SKIP
DIV [[r]] =F[M1.0,M2.0] DIV
SKIP ;; P =F[M,M] P
P ;; SKIP =F[M,M] P
DIV ;; P =F[M1.0,M2.0] DIV
(? :X -> Pf [> SKIP) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> Q
(? :X -> Pf [> DIV) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> DIV
SKIP |. Suc n =F[M1.0,M2.0] SKIP
DIV |. n =F[M1.0,M2.0] DIV
(? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP)
|~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> (SKIP |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] SKIP) |[X]| SKIP)
(? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV)
|~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> (DIV |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] DIV) |[X]| DIV)
(? :Y -> Pf [+] SKIP) |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV)
|~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> (SKIP |[X]| (? :Z -> Qf [+] DIV) |~| (? :Y -> Pf [+] SKIP) |[X]| DIV)
(? :Y -> Pf [+] DIV) |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP)
|~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> (DIV |[X]| (? :Z -> Qf [+] SKIP) |~| (? :Y -> Pf [+] DIV) |[X]| SKIP)
(? :Y -> Pf [+] SKIP) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] SKIP) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] SKIP) |[X]| Qf x)
[> SKIP |[X]| ? :Z -> Qf
? :Y -> Pf |[X]| (? :Z -> Qf [+] SKIP) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] SKIP))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| SKIP
(? :Y -> Pf [+] DIV) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] DIV) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] DIV) |[X]| Qf x)
[> DIV |[X]| ? :Z -> Qf
? :Y -> Pf |[X]| (? :Z -> Qf [+] DIV) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] DIV) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] DIV))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| DIV
(? :X -> Pf [+] SKIP) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> Q
(? :X -> Pf [+] DIV) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [+] DIV
lemma cspF_SKIP_or_DIV_resolve:
[| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
==> (? :Y -> Pf [+] P) |[X]| (? :Z -> Qf [+] Q) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] Q)
|~| (? :Y -> Pf [+] P) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] Q))
ELSE ((? :Y -> Pf [+] P) |[X]| Qf x)
[> (P |[X]| (? :Z -> Qf [+] Q) |~| (? :Y -> Pf [+] P) |[X]| Q)
P = SKIP ∨ P = DIV
==> (? :Y -> Pf [+] P) |[X]| ? :Z -> Qf =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| ? :Z -> Qf |~| (? :Y -> Pf [+] P) |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| ? :Z -> Qf)
ELSE ((? :Y -> Pf [+] P) |[X]| Qf x)
[> P |[X]| ? :Z -> Qf
Q = SKIP ∨ Q = DIV
==> ? :Y -> Pf |[X]| (? :Z -> Qf [+] Q) =F[M,M]
? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X))
-> IF (x ∈ X) THEN (Pf x |[X]| Qf x)
ELSE IF (x ∈ Y ∧ x ∈ Z)
THEN (Pf x |[X]| (? :Z -> Qf [+] Q) |~| ? :Y -> Pf |[X]| Qf x)
ELSE IF (x ∈ Y) THEN (Pf x |[X]| (? :Z -> Qf [+] Q))
ELSE (? :Y -> Pf |[X]| Qf x)
[> ? :Y -> Pf |[X]| Q
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_l:
Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> (P [+] Q) |[X]| DIV =F[M,M] P |[X]| DIV
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV_r:
Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F[M,M] DIV |[X]| P
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_DIV:
Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> (P [+] Q) |[X]| DIV =F[M,M] P |[X]| DIV
Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F[M,M] DIV |[X]| P
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_l:
Q = SKIP ∨ Q = DIV ∨ Q = STOP
==> (? :Y -> Pf [+] Q) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP_r:
Q = SKIP ∨ Q = DIV ∨ Q = STOP
==> SKIP |[X]| (? :Y -> Pf [+] Q) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] Q
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice_SKIP:
Q = SKIP ∨ Q = DIV ∨ Q = STOP
==> (? :Y -> Pf [+] Q) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q
Q = SKIP ∨ Q = DIV ∨ Q = STOP
==> SKIP |[X]| (? :Y -> Pf [+] Q) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] Q
lemma cspF_SKIP_or_DIV_or_STOP_Parallel_Ext_choice:
Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> (P [+] Q) |[X]| DIV =F[M,M] P |[X]| DIV
Q = SKIP ∨ Q = DIV ∨ Q = STOP ==> DIV |[X]| (P [+] Q) =F[M,M] DIV |[X]| P
Q = SKIP ∨ Q = DIV ∨ Q = STOP
==> (? :Y -> Pf [+] Q) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] Q
Q = SKIP ∨ Q = DIV ∨ Q = STOP
==> SKIP |[X]| (? :Y -> Pf [+] Q) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] Q
lemma cspF_SKIP_or_DIV_or_STOP_Renaming_Id:
P = SKIP ∨ P = DIV ∨ P = STOP ==> P [[r]] =F[M,M] P
lemma cspF_STOP_Depth_rest:
STOP |. Suc n =F[M,M] STOP
lemma cspF_Ext_pre_choice_SKIP_commut:
SKIP [+] ? :X -> Pf =F[M,M] ? :X -> Pf [+] SKIP
lemma cspF_Ext_pre_choice_DIV_commut:
DIV [+] ? :X -> Pf =F[M,M] ? :X -> Pf [+] DIV
lemma cspF_Ext_pre_choice_SKIP_assoc:
? :X -> Pf [+] SKIP [+] ? :Y -> Qf =F[M,M] ? :X -> Pf [+] ? :Y -> Qf [+] SKIP
lemma cspF_Ext_pre_choice_DIV_assoc:
? :X -> Pf [+] DIV [+] ? :Y -> Qf =F[M,M] ? :X -> Pf [+] ? :Y -> Qf [+] DIV
lemma cspF_Ext_choice_idem_assoc:
P [+] Q [+] Q =F[M,M] P [+] Q
lemma cspF_Ext_choice_SKIP_DIV_assoc:
P [+] SKIP [+] DIV =F[M,M] P [+] SKIP
lemma cspF_Ext_choice_DIV_SKIP_assoc:
P [+] DIV [+] SKIP =F[M,M] P [+] SKIP
lemma cspF_SKIP_DIV_sort:
P [+] (Q [+] R) =F[M,M] P [+] Q [+] R
SKIP [+] ? :X -> Pf =F[M,M] ? :X -> Pf [+] SKIP
DIV [+] ? :X -> Pf =F[M,M] ? :X -> Pf [+] DIV
? :X -> Pf [+] SKIP [+] ? :Y -> Qf =F[M,M] ? :X -> Pf [+] ? :Y -> Qf [+] SKIP
? :X -> Pf [+] DIV [+] ? :Y -> Qf =F[M,M] ? :X -> Pf [+] ? :Y -> Qf [+] DIV
P [+] Q [+] Q =F[M,M] P [+] Q
P [+] SKIP [+] DIV =F[M,M] P [+] SKIP
P [+] DIV [+] SKIP =F[M,M] P [+] SKIP
lemma cspF_rw_flag_left_eq:
[| R1.0 =F[M1.0,M1.0] R2.0; Not_Decompo_Flag ∧ R2.0 =F[M1.0,M3.0] R3.0 |]
==> R1.0 =F[M1.0,M3.0] R3.0
lemma cspF_rw_flag_left_ref:
[| R1.0 =F[M1.0,M1.0] R2.0; Not_Decompo_Flag ∧ R2.0 <=F[M1.0,M3.0] R3.0 |]
==> R1.0 <=F[M1.0,M3.0] R3.0
lemma cspF_rw_flag_left:
[| R1.0 =F[M1.0,M1.0] R2.0; Not_Decompo_Flag ∧ R2.0 =F[M1.0,M3.0] R3.0 |]
==> R1.0 =F[M1.0,M3.0] R3.0
[| R1.0 =F[M1.0,M1.0] R2.0; Not_Decompo_Flag ∧ R2.0 <=F[M1.0,M3.0] R3.0 |]
==> R1.0 <=F[M1.0,M3.0] R3.0
lemma cspF_rw_flag_right_eq:
[| R3.0 =F[M3.0,M3.0] R2.0; Not_Decompo_Flag ∧ R1.0 =F[M1.0,M3.0] R2.0 |]
==> R1.0 =F[M1.0,M3.0] R3.0
lemma cspF_rw_flag_right_ref:
[| R3.0 =F[M3.0,M3.0] R2.0; Not_Decompo_Flag ∧ R1.0 <=F[M1.0,M3.0] R2.0 |]
==> R1.0 <=F[M1.0,M3.0] R3.0
lemma cspF_rw_flag_right:
[| R3.0 =F[M3.0,M3.0] R2.0; Not_Decompo_Flag ∧ R1.0 =F[M1.0,M3.0] R2.0 |]
==> R1.0 =F[M1.0,M3.0] R3.0
[| R3.0 =F[M3.0,M3.0] R2.0; Not_Decompo_Flag ∧ R1.0 <=F[M1.0,M3.0] R2.0 |]
==> R1.0 <=F[M1.0,M3.0] R3.0
lemma cspF_tr_flag_left_eq:
[| P1.0 =F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 =F[M1.0,M3.0] P3.0 |]
==> P1.0 =F[M1.0,M3.0] P3.0
lemma cspF_tr_flag_left_ref:
[| P1.0 <=F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 <=F[M1.0,M3.0] P3.0 |]
==> P1.0 <=F[M1.0,M3.0] P3.0
lemma cspF_tr_flag_left:
[| P1.0 =F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 =F[M1.0,M3.0] P3.0 |]
==> P1.0 =F[M1.0,M3.0] P3.0
[| P1.0 <=F[M1.0,M1.0] P2.0; Not_Decompo_Flag ∧ P2.0 <=F[M1.0,M3.0] P3.0 |]
==> P1.0 <=F[M1.0,M3.0] P3.0
lemma cspF_tr_flag_right_eq:
[| P2.0 =F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 =F[M1.0,M3.0] P2.0 |]
==> P1.0 =F[M1.0,M3.0] P3.0
lemma cspF_tr_flag_right_ref:
[| P2.0 <=F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 <=F[M1.0,M3.0] P2.0 |]
==> P1.0 <=F[M1.0,M3.0] P3.0
lemma cspF_tr_flag_right:
[| P2.0 =F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 =F[M1.0,M3.0] P2.0 |]
==> P1.0 =F[M1.0,M3.0] P3.0
[| P2.0 <=F[M3.0,M3.0] P3.0; Not_Decompo_Flag ∧ P1.0 <=F[M1.0,M3.0] P2.0 |]
==> P1.0 <=F[M1.0,M3.0] P3.0
lemma cspF_Seq_compo_mono_flag:
[| P1.0 <=F[M1.0,M2.0] Q1.0; Not_Decompo_Flag ∧ P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 <=F[M1.0,M2.0] Q1.0 ;; Q2.0
lemma cspF_Seq_compo_cong_flag:
[| P1.0 =F[M1.0,M2.0] Q1.0; Not_Decompo_Flag ∧ P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 =F[M1.0,M2.0] Q1.0 ;; Q2.0
lemma cspF_free_mono_flag:
[| P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 [+] P2.0 <=F[M1.0,M2.0] Q1.0 [+] Q2.0
[| P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 |~| P2.0 <=F[M1.0,M2.0] Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 |[X]| P2.0 <=F[M1.0,M2.0] Q1.0 |[Y]| Q2.0
[| X = Y; P <=F[M1.0,M2.0] Q |] ==> P -- X <=F[M1.0,M2.0] Q -- Y
[| r1.0 = r2.0; P <=F[M1.0,M2.0] Q |] ==> P [[r1.0]] <=F[M1.0,M2.0] Q [[r2.0]]
[| P1.0 <=F[M1.0,M2.0] Q1.0; Not_Decompo_Flag ∧ P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 <=F[M1.0,M2.0] Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F[M1.0,M2.0] Q |] ==> P |. n1.0 <=F[M1.0,M2.0] Q |. n2.0
lemma cspF_free_cong_flag:
[| P1.0 =F[M1.0,M2.0] Q1.0; P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 [+] P2.0 =F[M1.0,M2.0] Q1.0 [+] Q2.0
[| P1.0 =F[M1.0,M2.0] Q1.0; P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 |~| P2.0 =F[M1.0,M2.0] Q1.0 |~| Q2.0
[| X = Y; P1.0 =F[M1.0,M2.0] Q1.0; P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 |[X]| P2.0 =F[M1.0,M2.0] Q1.0 |[Y]| Q2.0
[| X = Y; P =F[M1.0,M2.0] Q |] ==> P -- X =F[M1.0,M2.0] Q -- Y
[| r1.0 = r2.0; P =F[M1.0,M2.0] Q |] ==> P [[r1.0]] =F[M1.0,M2.0] Q [[r2.0]]
[| P1.0 =F[M1.0,M2.0] Q1.0; Not_Decompo_Flag ∧ P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 =F[M1.0,M2.0] Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F[M1.0,M2.0] Q |] ==> P |. n1.0 =F[M1.0,M2.0] Q |. n2.0
lemma cspF_free_decompo_flag:
[| P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 [+] P2.0 <=F[M1.0,M2.0] Q1.0 [+] Q2.0
[| P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 |~| P2.0 <=F[M1.0,M2.0] Q1.0 |~| Q2.0
[| X = Y; P1.0 <=F[M1.0,M2.0] Q1.0; P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 |[X]| P2.0 <=F[M1.0,M2.0] Q1.0 |[Y]| Q2.0
[| X = Y; P <=F[M1.0,M2.0] Q |] ==> P -- X <=F[M1.0,M2.0] Q -- Y
[| r1.0 = r2.0; P <=F[M1.0,M2.0] Q |] ==> P [[r1.0]] <=F[M1.0,M2.0] Q [[r2.0]]
[| P1.0 <=F[M1.0,M2.0] Q1.0; Not_Decompo_Flag ∧ P2.0 <=F[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 <=F[M1.0,M2.0] Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=F[M1.0,M2.0] Q |] ==> P |. n1.0 <=F[M1.0,M2.0] Q |. n2.0
[| P1.0 =F[M1.0,M2.0] Q1.0; P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 [+] P2.0 =F[M1.0,M2.0] Q1.0 [+] Q2.0
[| P1.0 =F[M1.0,M2.0] Q1.0; P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 |~| P2.0 =F[M1.0,M2.0] Q1.0 |~| Q2.0
[| X = Y; P1.0 =F[M1.0,M2.0] Q1.0; P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 |[X]| P2.0 =F[M1.0,M2.0] Q1.0 |[Y]| Q2.0
[| X = Y; P =F[M1.0,M2.0] Q |] ==> P -- X =F[M1.0,M2.0] Q -- Y
[| r1.0 = r2.0; P =F[M1.0,M2.0] Q |] ==> P [[r1.0]] =F[M1.0,M2.0] Q [[r2.0]]
[| P1.0 =F[M1.0,M2.0] Q1.0; Not_Decompo_Flag ∧ P2.0 =F[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 =F[M1.0,M2.0] Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =F[M1.0,M2.0] Q |] ==> P |. n1.0 =F[M1.0,M2.0] Q |. n2.0