we started Kashima's proof of standardization

[helm.git] / matita / matita / contribs / lambda / redex_pointer_sequence.ma

diff --git a/matita/matita/contribs/lambda/redex_pointer_sequence.ma b/matita/matita/contribs/lambda/redex_pointer_sequence.ma
index 5b05f47966477a78c0420054225809e70150b067..e32c6d2baa9ee274dabaaea774d5e19f64f69a84 100644 (file)
--- 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.