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 "paths/trace.ma".
16 include "paths/standard_order.ma".
18 (* STANDARD TRACE ***********************************************************)
20 (* Note: to us, a "standard" computation contracts redexes in non-decreasing positions *)
21 definition is_standard: predicate trace ≝ Allr … sle.
23 lemma is_standard_compatible: ∀c,s. is_standard s → is_standard (c:::s).
24 #c #s elim s -s // #p * //
25 #q #s #IHs * /3 width=1/
28 lemma is_standard_cons: ∀p,s. is_standard s → is_standard ((dx::p)::sn:::s).
29 #p #s elim s -s // #q1 * /2 width=1/
30 #q2 #s #IHs * /4 width=1/
33 lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_standard ((dx:::r)@sn:::s).
34 #r elim r -r /3 width=1/ #p * /2 width=1/
35 #q #r #IHr * /3 width=1/
38 theorem is_whd_is_standard: ∀s. is_whd s → is_standard s.
39 #s elim s -s // #p * //
40 #q #s #IHs * /3 width=1/
43 lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
44 #p #Hp * // /3 width=1/
47 theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
50 | #q #r #IHr * /3 width=1/