improved example: Delta must be a family of terms

diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
index 84713bce6e4b23b6e2c7b9471bdd846ffd0d98a0..6a2586ff16fb2d24d2f8769b645e1cccb586b4e1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
@@ -18,24 +18,26 @@ include "basic_2/reduction/cpr.ma".
 
 (* A reduction cycle in two steps: the term Omega ***************************)
 
-definition Delta: term â\89\9d +â\93\9bâ\8b\860.ⓐ#0.#0.
+definition Delta: term â\86\92 term â\89\9d λW. +â\93\9bW.ⓐ#0.#0.
 
-definition Omega1: term â\89\9d â\93\90Delta.Delta.
+definition Omega1: term â\86\92 term â\89\9d λW. â\93\90(Delta W).(Delta W).
 
-definition Omega2: term â\89\9d +â\93\93â\93\9dâ\8b\860.Delta.ⓐ#0.#0.
+definition Omega2: term â\86\92 term â\89\9d λW. +â\93\93â\93\9dW.(Delta W).ⓐ#0.#0.
 
 (* Basic properties *********************************************************)
 
-lemma Delta_lift: ∀d,e. ⇧[d, e] Delta ≡ Delta.
+lemma Delta_lift: ∀W1,W2,d,e. ⇧[d, e] W1 ≡ W2 →
+                  ⇧[d, e] (Delta W1) ≡ (Delta W2).
 /4 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
 
 (* Main properties **********************************************************)
 
-theorem cpr_Omega_12: â¦\83â\8b\86, â\8b\86â¦\84 â\8a¢ Omega1 â\9e¡ Omega2.
+theorem cpr_Omega_12: â\88\80W. â¦\83â\8b\86, â\8b\86â¦\84 â\8a¢ Omega1 W â\9e¡ Omega2 W.
 /2 width=1 by cpr_beta/ qed.
 
-theorem cpr_Omega_21: ⦃⋆, ⋆⦄ ⊢ Omega2 ➡ Omega1.
-@(cpr_zeta … Omega1) /2 width=1 by lift_flat/
-@cpr_flat @(cpr_delta … Delta ? 0)
-[3,5,8,10: // |4,9: /2 width=1 by cpr_eps/ |*: skip ]
+theorem cpr_Omega_21: ∀W. ⦃⋆, ⋆⦄ ⊢ Omega2 W ➡ Omega1 W.
+#W1 elim (lift_total W1 0 1) #W2 #HW12
+@(cpr_zeta … (Omega1 W2)) /3 width=1 by Delta_lift, lift_flat/
+@cpr_flat @(cpr_delta … (Delta W1) ? 0)
+[3,5,8,10: /2 width=2 by Delta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ]
 qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 456a2b0e329badd42b2919a520d47746d52bb70d..7ff91fa2db329b9e2a100309e6639f40bbb35029 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -11,7 +11,7 @@ table {
    ]
    class "wine"
    [ { "examples" * } {
-        [ { "" * } {
+        [ { "terms with special features" * } {
              [ "ex_cpr_omega" * ]
           }
         ]