X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fredex_pointer_sequence.ma;h=e32c6d2baa9ee274dabaaea774d5e19f64f69a84;hb=984f552a6b54e8b870d6e32df8325345d0f1ea5b;hp=5b05f47966477a78c0420054225809e70150b067;hpb=80cb637c1470b71145d3329d74148a1cfc873e3f;p=helm.git

diff --git a/matita/matita/contribs/lambda/redex_pointer_sequence.ma b/matita/matita/contribs/lambda/redex_pointer_sequence.ma
index 5b05f4796..e32c6d2ba 100644
--- a/matita/matita/contribs/lambda/redex_pointer_sequence.ma
+++ b/matita/matita/contribs/lambda/redex_pointer_sequence.ma
@@ -18,4 +18,12 @@ include "redex_pointer.ma".
 
 (* Policy: pointer sequence metavariables: r, s *)
 
-definition rpseq: Type[0] \def list rpointer.
+definition rpseq: Type[0] \def list rptr.
+
+(* Note: a "spine" computation contracts just redexes in the spine *)
+definition is_spine: predicate rpseq ≝ λs.
+                     All … in_spine s.
+
+(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
+definition is_le: predicate rpseq ≝ λs.
+                  Allr … rple s.