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/reduction/cpr.ma".
17 (* EXAMPLES *****************************************************************)
19 (* A reduction cycle in two steps: the term Omega ***************************)
21 definition Delta: term ≝ +ⓛ⋆0.ⓐ#0.#0.
23 definition Omega1: term ≝ ⓐDelta.Delta.
25 definition Omega2: term ≝ +ⓓⓝ⋆0.Delta.ⓐ#0.#0.
27 (* Basic properties *********************************************************)
29 lemma Delta_lift: ∀d,e. ⇧[d, e] Delta ≡ Delta.
30 /4 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
32 (* Main properties **********************************************************)
34 theorem cpr_Omega_12: ⦃⋆, ⋆⦄ ⊢ Omega1 ➡ Omega2.
35 /2 width=1 by cpr_beta/ qed.
37 theorem cpr_Omega_21: ⦃⋆, ⋆⦄ ⊢ Omega2 ➡ Omega1.
38 @(cpr_zeta … Omega1) /2 width=1 by lift_flat/
39 @cpr_flat @(cpr_delta … Delta ? 0)
40 [3,5,8,10: // |4,9: /2 width=1 by cpr_eps/ |*: skip ]