- we enabled a notation for ex2

[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 e32c6d2baa9ee274dabaaea774d5e19f64f69a84..43b7aa1d42fb551c8d0540f373f7d2ff71964603 100644 (file)
--- a/matita/matita/contribs/lambda/redex_pointer_sequence.ma
+++ b/matita/matita/contribs/lambda/redex_pointer_sequence.ma
@@ -27,3 +27,7 @@ definition is_spine: predicate rpseq ≝ λs.
 (* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
 definition is_le: predicate rpseq ≝ λs.
                   Allr … rple s.
+
+(* Note: a normal spine computation *)
+definition is_spine_le: predicate rpseq ≝ λs.
+                        is_spine s ∧ is_le s.