- notation is now in a separate file

[helm.git] / matita / matita / lib / lambda / sn.ma

diff --git a/matita/matita/lib/lambda/sn.ma b/matita/matita/lib/lambda/sn.ma
index 26b1f9e77690aafaafed20ad6121de8bb3a7943d..c30cfecc7619d6714779ca165ffd96d59562390f 100644 (file)
--- a/matita/matita/lib/lambda/sn.ma
+++ b/matita/matita/lib/lambda/sn.ma
@@ -14,39 +14,46 @@
 
 include "lambda/ext.ma".
 
-(* saturation conditions on an explicit subset ********************************)
+(* STRONGLY NORMALIZING TERMS *************************************************)
+
+(* SN(t) holds when t is strongly normalizing *)
+(* FG: we axiomatize it for now because we dont have reduction yet *)
+axiom SN: T → Prop.
 
-definition SAT0 ≝ λP. ∀l,n. all P l → P (Appl (Sort n) l).
+(* lists of strongly normalizing terms *)
+definition SNl ≝ all ? SN.
 
-definition SAT1 ≝ λP. ∀l,i. all P l → P (Appl (Rel i) l).
+(* saturation conditions ******************************************************)
 
-definition SAT2 ≝ λ(P:?→Prop). ∀F,A,B,l. P B → P A → 
-                  P (Appl F[0:=A] l) → P (Appl (Lambda B F) (A::l)).
+definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
+
+definition SAT0 ≝ λ(P:?→Prop). ∀n,l. SNl l → P (Appl (Sort n) l).
+
+definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l).
+
+definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L → 
+                  P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)).
 
 theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
-#P #n #H @(H (nil ?) …) //
+#P #n #H @(H n (nil ?) …) //
 qed.
 
 theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
-#P #i #H @(H (nil ?) …) //
+#P #i #H @(H i (nil ?) …) //
 qed.
 
-(* STRONGLY NORMALIZING TERMS *************************************************)
-
-(* SN(t) holds when t is strongly normalizing *)
-(* FG: we axiomatize it for now because we dont have reduction yet *)
-axiom SN: T → Prop.
-
-definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
+(* axiomatization *************************************************************)
 
 axiom sn_sort: SAT0 SN.
 
 axiom sn_rel: SAT1 SN.
 
-axiom sn_lambda: ∀B,F. SN B → SN F → SN (Lambda B F).
-
 axiom sn_beta: SAT2 SN.
 
-(* FG: do we need this?
-axiom sn_lift: ∀t,k,p. SN t → SN (lift t p k).
-*)
+axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
+
+axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
+
+axiom sn_dummy: ∀M. SN M → SN (D M).
+
+axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.