--- a/src/HOL/UNITY/Alloc.ML Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML Wed Oct 27 13:03:32 1999 +0200
@@ -402,8 +402,35 @@
by (auto_tac (claset(), simpset() addsimps [o_def]));
qed "Client_i_Progress";
+Goal "extend sysOfAlloc F \
+\ : (v o client) localTo[C] extend sysOfClient (lift_prog i Client)";
+br localTo_UNIV_imp_localTo 1;
+by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def,
+ stable_def, constrains_def,
+ image_eq_UN, extend_act_def,
+ sysOfAlloc_def, sysOfClient_def]) 1);
+by (Force_tac 1);
+qed "sysOfAlloc_in_client_localTo_xl_Client";
+
+Goal "extend sysOfClient (plam x: I. Client) : ((%z. z i) o client) \
+\ localTo[C] extend sysOfClient (lift_prog i Client)";
+br localTo_UNIV_imp_localTo 1;
+by (rtac (client_export (extend_set_UNIV_eq RS equalityD2 RSN
+ (2, extend_localTo_extend_I))) 1);
+br (rewrite_rule [sub_def] PLam_sub_localTo) 1;
+qed "sysOfClient_in_client_localTo_xl_Client";
+
xxxxxxxxxxxxxxxx;
+THIS PROOF requires an extra locality specification for Network:
+ Network : rel o sub i o client localTo[C]
+ extend sysOfClient (lift_prog i Client)
+and similarly for ask o sub i o client.
+
+The LeadsTo rule must be refined so as not to require the whole of client to
+be local, since giv is written by the Network.
+
+
Goalw [System_def]
"i < Nclients \
\ ==> System : (INT h. {s. h <= (giv o sub i o client) s & \
@@ -411,17 +438,23 @@
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
by (rtac (guarantees_PLam_I RS project_guarantees) 1);
-by (rtac Client_i_Progress 1);
+by (rtac Client_i_Progress 1);
by (Force_tac 1);
by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
by (rtac subset_refl 4);
by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
-by (rtac projecting_Int 1);
-by (rtac (client_export projecting_Increasing) 1);
-by (rtac (client_export projecting_localTo) 1);
+(*The next step goes wrong: it makes an impossible localTo subgoal*)
+(*blast_tac doesn't use HO unification*)
+by (fast_tac (claset() addIs [projecting_Int,
+ client_export projecting_Increasing,
+ component_PLam,
+ client_export projecting_LocalTo]) 1);
+by (asm_simp_tac
+ (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
+ LocalTo_def, Join_localTo,
+ sysOfClient_in_client_localTo_xl_Client,
+ sysOfAlloc_in_client_localTo_xl_Client]) 2);
+auto();
-by (simp_tac (simpset()addsimps [lift_prog_correct]) 1);
-by (rtac (client_export ) 1);
-Client_Progress;
--- a/src/HOL/UNITY/Comp.ML Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML Wed Oct 27 13:03:32 1999 +0200
@@ -56,6 +56,11 @@
by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
qed "Join_absorb2";
+Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
+by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by (Blast_tac 1);
+qed "JN_component_iff";
+
Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
by (blast_tac (claset() addIs [JN_absorb]) 1);
qed "component_JN";
@@ -84,4 +89,19 @@
simpset() addsimps [constrains_def, component_eq_subset]));
qed "component_constrains";
+(*Used in Guar.thy to show that programs are partially ordered*)
bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
+
+Goal "F' <= F ==> Diff C G (Acts F) <= Diff C G (Acts F')";
+by (auto_tac (claset(), simpset() addsimps [Diff_def, component_eq_subset]));
+qed "Diff_anti_mono";
+
+(*The LocalTo analogue fails unless
+ reachable (F Join G) <= reachable (F' Join G),
+ e.g. if the initial condition of F is stronger than that of F'*)
+Goalw [LOCALTO_def, stable_def]
+ "[| G : v localTo[C] F'; F' <= F |] ==> G : v localTo[C] F";
+by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains],
+ simpset()));
+qed "localTo_component";
+
--- a/src/HOL/UNITY/Extend.ML Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Wed Oct 27 13:03:32 1999 +0200
@@ -123,6 +123,13 @@
qed "extend_set_inverse";
Addsimps [extend_set_inverse];
+Goalw [extend_set_def, project_set_def]
+ "C <= extend_set h (project_set h C)";
+by (auto_tac (claset(),
+ simpset() addsimps [split_extended_all]));
+by (Blast_tac 1);
+qed "extend_set_project_set";
+
Goal "inj (extend_set h)";
by (rtac inj_on_inverseI 1);
by (rtac extend_set_inverse 1);
@@ -454,6 +461,12 @@
by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
qed "extend_localTo_extend_eq";
+Goal "[| F : v localTo[C] H; C' <= extend_set h C |] \
+\ ==> extend h F : (v o f) localTo[C'] extend h H";
+by (blast_tac (claset() addDs [extend_localTo_extend_eq RS iffD2,
+ impOfSubs localTo_anti_mono]) 1);
+qed "extend_localTo_extend_I";
+
(*USED?? opposite inclusion fails*)
Goal "Restrict C (extend_act h act) <= \
\ extend_act h (Restrict (project_set h C) act)";
--- a/src/HOL/UNITY/Guar.ML Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Guar.ML Wed Oct 27 13:03:32 1999 +0200
@@ -191,11 +191,6 @@
by (Blast_tac 1);
qed "guarantees_Join_Un";
-Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
-by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by (Blast_tac 1);
-qed "JN_component_iff";
-
Goalw [guar_def]
"[| ALL i:I. F i : X i guarantees Y i |] \
\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
--- a/src/HOL/UNITY/Lift_prog.ML Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Wed Oct 27 13:03:32 1999 +0200
@@ -30,21 +30,8 @@
Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set];
-(*Converse fails*)
-Goalw [drop_set_def] "f : A ==> f i : drop_set i A";
-by Auto_tac;
-qed "drop_set_I";
-
(** lift_act and drop_act **)
-Goalw [lift_act_def] "lift_act i Id = Id";
-by Auto_tac;
-by (etac rev_mp 1);
-by (dtac sym 1);
-by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
-qed "lift_act_Id";
-Addsimps [lift_act_Id];
-
(*For compatibility with the original definition and perhaps simpler proofs*)
Goalw [lift_act_def]
"((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
@@ -54,12 +41,6 @@
qed "lift_act_eq";
AddIffs [lift_act_eq];
-Goalw [drop_set_def, drop_act_def]
- "UNIV <= drop_set i C ==> drop_act i (Restrict C Id) = Id";
-by (Blast_tac 1);
-qed "drop_act_Id";
-Addsimps [drop_act_Id];
-
(** lift_prog and drop_prog **)
Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
@@ -86,7 +67,10 @@
(*** sub ***)
-Addsimps [sub_def];
+Goal "sub i f = f i";
+by (simp_tac (simpset() addsimps [sub_def]) 1);
+qed "sub_apply";
+Addsimps [sub_apply];
Goal "lift_set i {s. P s} = {s. P (sub i s)}";
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
@@ -338,8 +322,9 @@
Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \
\ (F : A Co B)";
-by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog,
- lift_prog_constrains]) 1);
+by (simp_tac
+ (simpset() addsimps [lift_prog_correct, lift_set_correct,
+ lift_export extend_Constrains]) 1);
qed "lift_prog_Constrains";
Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
@@ -453,14 +438,13 @@
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
qed "lift_prog_localTo_guar_increasing";
-(***
-Goal "F : (v LocalTo G) guarantees Increasing func \
-\ ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G) \
+Goal "[| F : (v LocalTo H) guarantees Increasing func; H <= F |] \
+\ ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i H) \
\ guarantees Increasing (func o sub i)";
by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
-by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [lift_prog_correct, o_def]));
qed "lift_prog_LocalTo_guar_Increasing";
-***)
Goal "F : Always A guarantees Always B \
\ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
--- a/src/HOL/UNITY/Lift_prog.thy Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Wed Oct 27 13:03:32 1999 +0200
@@ -39,7 +39,7 @@
(*simplifies the expression of specifications*)
constdefs
sub :: ['a, 'a=>'b] => 'b
- "sub i f == f i"
+ "sub == %i f. f i"
end
--- a/src/HOL/UNITY/PPROD.ML Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML Wed Oct 27 13:03:32 1999 +0200
@@ -18,13 +18,14 @@
Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
by Auto_tac;
qed "Init_PLam";
-Addsimps [Init_PLam];
Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
by (auto_tac (claset(),
simpset() addsimps [PLam_def]));
qed "Acts_PLam";
+Addsimps [Init_PLam, Acts_PLam];
+
Goal "PLam {} F = SKIP";
by (simp_tac (simpset() addsimps [PLam_def]) 1);
qed "PLam_empty";
@@ -40,6 +41,10 @@
by Auto_tac;
qed "PLam_insert";
+Goal "((PLam I F) <= H) = (ALL i: I. lift_prog i (F i) <= H)";
+by (simp_tac (simpset() addsimps [PLam_def, JN_component_iff]) 1);
+qed "PLam_component_iff";
+
Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)";
(*blast_tac doesn't use HO unification*)
by (fast_tac (claset() addIs [component_JN]) 1);
@@ -121,13 +126,20 @@
qed "const_PLam_invariant";
+(** localTo **)
+
+Goal "(PLam I F) : (sub i) localTo[C] lift_prog i (F i)";
+by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def,
+ stable_def, constrains_def]) 1);
+by (Force_tac 1);
+qed "PLam_sub_localTo";
+
+
(** Reachability **)
Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)";
by (etac reachable.induct 1);
-by (auto_tac
- (claset() addIs reachable.intrs,
- simpset() addsimps [Acts_PLam]));
+by (auto_tac (claset() addIs reachable.intrs, simpset()));
qed "reachable_PLam";
(*Result to justify a re-organization of this file*)
@@ -149,10 +161,10 @@
(*Init, Init case*)
by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
(*Init of F, action of PLam F case*)
-by (rtac reachable.Acts 1);
+by (res_inst_tac [("act","act")] reachable.Acts 1);
by (Force_tac 1);
by (assume_tac 1);
-by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1);
+by (force_tac (claset() addIs [ext], simpset()) 1);
(*induction over the 2nd "reachable" assumption*)
by (eres_inst_tac [("xa","f")] reachable.induct 1);
(*Init of PLam F, action of F case*)
@@ -161,10 +173,10 @@
by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
(*last case: an action of PLam I F*)
-by (rtac reachable.Acts 1);
+by (res_inst_tac [("act","acta")] reachable.Acts 1);
by (Force_tac 1);
by (assume_tac 1);
-by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1);
+by (force_tac (claset() addIs [ext], simpset()) 1);
qed_spec_mp "reachable_lift_Join_PLam";
--- a/src/HOL/UNITY/Project.ML Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Project.ML Wed Oct 27 13:03:32 1999 +0200
@@ -402,7 +402,6 @@
simpset() addsimps [project_set_def]) 1);
qed "reachable_project_imp_reachable";
-
Goal "project_set h (reachable (extend h F Join G)) = \
\ reachable (F Join project h (reachable (extend h F Join G)) G)";
by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project,
@@ -410,6 +409,13 @@
simpset() addsimps [project_set_def]));
qed "project_set_reachable_extend_eq";
+Goal "reachable (extend h F Join G) <= C \
+\ ==> reachable (extend h F Join G) <= \
+\ extend_set h (reachable (F Join project h C G))";
+by (auto_tac (claset() addDs [reachable_imp_reachable_project],
+ simpset()));
+qed "reachable_extend_Join_subset";
+
(*Perhaps should replace C by reachable...*)
Goalw [Constrains_def]
"[| C <= reachable (extend h F Join G); \
@@ -472,16 +478,14 @@
Collect_eq_extend_set RS sym]) 1);
qed "project_Increasing";
-(**
-Goal "extend h F Join G : (v o f) LocalTo extend h H \
+Goal "[| H <= F; extend h F Join G : (v o f) LocalTo extend h H |] \
\ ==> F Join project h (reachable (extend h F Join G)) G : v LocalTo H";
by (asm_full_simp_tac
- (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
- gen_project_localTo_I,
- Join_assoc RS sym]) 1);
-
+ (simpset() delsimps [extend_Join]
+ addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
+ gen_project_localTo_I, extend_Join RS sym,
+ Join_assoc RS sym, Join_absorb1]) 1);
qed "project_LocalTo_I";
-**)
(** A lot of redundant theorems: all are proved to facilitate reasoning
about guarantees. **)
@@ -510,13 +514,11 @@
by (blast_tac (claset() addIs [project_Increasing_I]) 1);
qed "projecting_Increasing";
-(**
Goalw [projecting_def]
- "projecting (%G. reachable (extend h F Join G)) h F \
-\ ((v o f) LocalTo extend h H) (v LocalTo H)";
+ "H <= F ==> projecting (%G. reachable (extend h F Join G)) h F \
+\ ((v o f) LocalTo extend h H) (v LocalTo H)";
by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
qed "projecting_LocalTo";
-**)
Goalw [extending_def]
"extending (%G. reachable (extend h F Join G)) h F X' \
@@ -625,32 +627,15 @@
simpset()) 1));
qed_spec_mp "Join_project_ensures";
-Goal "[| ALL D. project h C G : transient D --> F : transient D; \
-\ extend h F Join G : stable C; \
-\ F Join project h C G : A leadsTo B |] \
-\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
-by (etac leadsTo_induct 1);
-by (asm_simp_tac (simpset() delsimps UN_simps
- addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
-by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken,
- leadsTo_Trans]) 2);
-by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
-qed "project_leadsTo_lemma";
+(** Lemma useful for both STRONG and WEAK progress*)
-(*Instance of the previous theorem for STRONG progress*)
-Goal "[| ALL D. project h UNIV G : transient D --> F : transient D; \
-\ F Join project h UNIV G : A leadsTo B |] \
-\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
-by (dtac project_leadsTo_lemma 1);
-by Auto_tac;
-qed "project_UNIV_leadsTo_lemma";
-
-(** Towards the analogous theorem for WEAK progress*)
-
+(*The strange induction formula allows induction over the leadsTo
+ assumption's non-atomic precondition*)
Goal "[| ALL D. project h C G : transient D --> F : transient D; \
\ extend h F Join G : stable C; \
\ F Join project h C G : (project_set h C Int A) leadsTo B |] \
-\ ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
+\ ==> extend h F Join G : \
+\ C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
by (etac leadsTo_induct 1);
by (asm_simp_tac (simpset() delsimps UN_simps
addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
@@ -665,14 +650,14 @@
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
by (rtac (lemma RS leadsTo_weaken) 1);
by (auto_tac (claset() addIs [project_set_I], simpset()));
-val lemma2 = result();
+qed "project_leadsTo_lemma";
Goal "[| C = (reachable (extend h F Join G)); \
\ ALL D. project h C G : transient D --> F : transient D; \
\ F Join project h C G : A LeadsTo B |] \
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, lemma2, stable_reachable,
+ (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, stable_reachable,
project_set_reachable_extend_eq]) 1);
qed "Join_project_LeadsTo";
@@ -713,14 +698,12 @@
val [xguary,project,extend] =
Goal "[| F : X guarantees Y; \
\ !!G. extend h F Join G : X' ==> F Join proj G h G : X; \
-\ !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
-\ Disjoint UNIV (extend h F) G |] \
+\ !!G. [| F Join proj G h G : Y; extend h F Join G : X' |] \
\ ==> extend h F Join G : Y' |] \
\ ==> extend h F : X' guarantees Y'";
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
by (etac project 1);
by (assume_tac 1);
-by (assume_tac 1);
qed "project_guarantees_lemma";
Goal "[| F : X guarantees Y; \
@@ -761,16 +744,14 @@
by (rtac projecting_localTo 1);
qed "extend_localTo_guar_increasing";
-(**
-Goal "F : (v LocalTo G) guarantees Increasing func \
-\ ==> extend h F : (v o f) LocalTo (extend h G) \
+Goal "[| F : (v LocalTo H) guarantees Increasing func; H <= F |] \
+\ ==> extend h F : (v o f) LocalTo (extend h H) \
\ guarantees Increasing (func o f)";
by (etac project_guarantees 1);
by (rtac extending_Increasing 2);
by (rtac projecting_LocalTo 1);
by Auto_tac;
qed "extend_LocalTo_guar_Increasing";
-**)
Goal "F : Always A guarantees Always B \
\ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
@@ -808,9 +789,9 @@
Goal "[| F Join project h UNIV G : A leadsTo B; \
\ G : f localTo[UNIV] extend h F |] \
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
-by (rtac project_UNIV_leadsTo_lemma 1);
+by (res_inst_tac [("C1", "UNIV")] (project_leadsTo_lemma RS leadsTo_weaken) 1);
by (auto_tac (claset(),
- simpset() addsimps [impOfSubs (subset_UNIV RS localTo_anti_mono) RS
+ simpset() addsimps [localTo_UNIV_imp_localTo RS
localTo_project_transient_transient]));
qed "project_leadsTo_D";
--- a/src/HOL/UNITY/Project.thy Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Project.thy Wed Oct 27 13:03:32 1999 +0200
@@ -19,8 +19,7 @@
extending :: "['c program => 'c set, 'a*'b => 'c, 'a program,
'c program set, 'c program set, 'a program set] => bool"
"extending C h F X' Y' Y ==
- ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
- Disjoint UNIV (extend h F) G
+ ALL G. F Join project h (C G) G : Y & extend h F Join G : X'
--> extend h F Join G : Y'"
end
--- a/src/HOL/UNITY/Union.ML Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Union.ML Wed Oct 27 13:03:32 1999 +0200
@@ -325,6 +325,9 @@
by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
qed "localTo_anti_mono";
+bind_thm ("localTo_UNIV_imp_localTo",
+ impOfSubs (subset_UNIV RS localTo_anti_mono));
+
Goalw [LocalTo_def]
"G : v localTo[UNIV] F ==> G : v LocalTo F";
by (blast_tac (claset() addDs [impOfSubs localTo_anti_mono]) 1);
@@ -355,6 +358,15 @@
Diff_self_eq]) 1);
qed "self_localTo";
+Goal "(F Join G : v localTo[C] F) = (G : v localTo[C] F)";
+by (simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
+qed "self_Join_localTo";
+
+Goal "(F Join G : v LocalTo F) = (G : v LocalTo F)";
+by (simp_tac (simpset() addsimps [self_Join_localTo, LocalTo_def,
+ Join_left_absorb]) 1);
+qed "self_Join_LocalTo";
+
(*** Higher-level rules involving localTo and Join ***)
--- a/src/HOL/UNITY/Union.thy Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Union.thy Wed Oct 27 13:03:32 1999 +0200
@@ -8,6 +8,8 @@
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
Do we need a Meet operator? (Aka Intersection)
+
+CAN PROBABLY DELETE the "Disjoint" predicate
*)
Union = SubstAx + FP +