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 "basic_2/rt_transition/cpr.ma".
17 (* EXAMPLES *****************************************************************)
19 (* A reduction cycle in two steps: the term Omega ***************************)
21 definition Delta: term → term ≝ λW. +ⓛW.ⓐ#0.#0.
23 definition Omega1: term → term ≝ λW. ⓐ(Delta W).(Delta W).
25 definition Omega2: term → term ≝ λW. +ⓓⓝW.(Delta W).ⓐ#0.#0.
27 (* Basic properties *********************************************************)
29 lemma Delta_lifts: ∀W1,W2,f. ⬆*[f] W1 ≘ W2 →
30 ⬆*[f] (Delta W1) ≘ (Delta W2).
31 /4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed.
33 (* Main properties **********************************************************)
35 theorem cpr_Omega_12: ∀h,G,L,W. ⦃G, L⦄ ⊢ Omega1 W ➡[h] Omega2 W.
36 /2 width=1 by cpm_beta/ qed.
38 theorem cpr_Omega_21: ∀h,G,L,W. ⦃G, L⦄ ⊢ Omega2 W ➡[h] Omega1 W.
39 #h #G #L #W1 elim (lifts_total W1 (𝐔❴1❵))
40 /5 width=5 by lifts_flat, cpm_zeta, cpm_eps, cpm_appl, cpm_delta, Delta_lifts/