update in delayed updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / preterm.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index 44d923d9bb742b2b8b49fc247031c9e8c40916d4..aabb5adae086e3bf10d98b1fe4f87783c8c3bda1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
@@ -14,6 +14,7 @@
 
 include "ground/lib/subset.ma".
 include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/pitchfork_2.ma".
 include "delayed_updating/notation/functions/uptriangle_1.ma".
 
 (* PRETERM ******************************************************************)
@@ -21,8 +22,15 @@ include "delayed_updating/notation/functions/uptriangle_1.ma".
 (* Note: preterms are subsets of complete paths *)
 definition preterm: Type[0] ≝ 𝒫❨path❩.
 
+definition preterm_grafted: path → preterm → preterm ≝
+           λp,t,q. p;;q ϵ t.
+
+interpretation
+  "grafted (preterm)"
+  'Pitchfork t p = (preterm_grafted p t).
+
 definition preterm_root: preterm → preterm ≝
-           λt,p. ∃q. p;;q ϵ t.
+           λt,q. ∃r. q;;r ϵ t.
 
 interpretation
   "root (preterm)"