1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/ext.ma".
17 (* STRONGLY NORMALIZING TERMS *************************************************)
19 (* SN(t) holds when t is strongly normalizing *)
20 (* FG: we axiomatize it for now because we dont have reduction yet *)
23 (* lists of strongly normalizing terms *)
24 definition SNl ≝ all ? SN.
26 (* saturation conditions ******************************************************)
28 definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
30 definition SAT0 ≝ λ(P:?→Prop). ∀n,l. SNl l → P (Appl (Sort n) l).
32 definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l).
34 definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L →
35 P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)).
37 theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
38 #P #n #H @(H n (nil ?) …) //
41 theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
42 #P #i #H @(H i (nil ?) …) //
45 (* axiomatization *************************************************************)
47 axiom sn_sort: SAT0 SN.
49 axiom sn_rel: SAT1 SN.
51 axiom sn_beta: SAT2 SN.
53 axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
55 axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
57 axiom sn_dummy: ∀M. SN M → SN (D M).
59 axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.