update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_sor_fcla.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_fcla.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_fcla.ma
index a1275f2cd97ed2a10e7b7b8223b12e97a616536c..f25b2363ea52db61bf55f73e8f6bc8dfb2657177 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_fcla.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_fcla.ma
@@ -25,8 +25,8 @@ include "ground/relocation/pr_sor_isi.ma".
 
 (*** sor_fcla_ex *)
 lemma pr_sor_fcla_bi:
-      â\88\80f1,n1. ð\9d\90\82â\9dªf1â\9d« â\89\98 n1 â\86\92 â\88\80f2,n2. ð\9d\90\82â\9dªf2â\9d« ≘ n2 →
-      â\88\83â\88\83f,n. f1 â\8b\93 f2 â\89\98 f & ð\9d\90\82â\9dªfâ\9d« ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
+      â\88\80f1,n1. ð\9d\90\82â\9d¨f1â\9d© â\89\98 n1 â\86\92 â\88\80f2,n2. ð\9d\90\82â\9d¨f2â\9d© ≘ n2 →
+      â\88\83â\88\83f,n. f1 â\8b\93 f2 â\89\98 f & ð\9d\90\82â\9d¨fâ\9d© ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
 #f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by pr_sor_isi_sn, ex4_2_intro/
 #f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by pr_fcla_push, pr_fcla_next, ex4_2_intro, pr_sor_isi_dx/
 #f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (* * full auto fails *)
@@ -41,8 +41,8 @@ qed-.
 
 (*** sor_fcla *)
 lemma pr_sor_inv_fcla_bi:
-      â\88\80f1,n1. ð\9d\90\82â\9dªf1â\9d« â\89\98 n1 â\86\92 â\88\80f2,n2. ð\9d\90\82â\9dªf2â\9d« ≘ n2 → ∀f. f1 ⋓ f2 ≘ f →
-      â\88\83â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
+      â\88\80f1,n1. ð\9d\90\82â\9d¨f1â\9d© â\89\98 n1 â\86\92 â\88\80f2,n2. ð\9d\90\82â\9d¨f2â\9d© ≘ n2 → ∀f. f1 ⋓ f2 ≘ f →
+      â\88\83â\88\83n. ð\9d\90\82â\9d¨fâ\9d© ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
 #f1 #n1 #Hf1 #f2 #n2 #Hf2 #f #Hf elim (pr_sor_fcla_bi … Hf1 … Hf2) -Hf1 -Hf2
 /4 width=6 by pr_sor_mono, pr_fcla_eq_repl_back, ex3_intro/
 qed-.
@@ -51,8 +51,8 @@ qed-.
 
 (*** sor_fwd_fcla_sn_ex *)
 lemma pr_sor_des_fcla_sn:
-      â\88\80f,n. ð\9d\90\82â\9dªfâ\9d« ≘ n → ∀f1,f2. f1 ⋓ f2 ≘ f →
-      â\88\83â\88\83n1. ð\9d\90\82â\9dªf1â\9d« ≘ n1 & n1 ≤ n.
+      â\88\80f,n. ð\9d\90\82â\9d¨fâ\9d© ≘ n → ∀f1,f2. f1 ⋓ f2 ≘ f →
+      â\88\83â\88\83n1. ð\9d\90\82â\9d¨f1â\9d© ≘ n1 & n1 ≤ n.
 #f #n #H elim H -f -n
 [ /4 width=4 by pr_sor_des_isi_sn, pr_fcla_isi, ex2_intro/
 | #f #n #_ #IH #f1 #f2 #H
@@ -66,6 +66,6 @@ qed-.
 
 (*** sor_fwd_fcla_dx_ex *)
 lemma pr_sor_des_fcla_dx:
-      â\88\80f,n. ð\9d\90\82â\9dªfâ\9d« ≘ n → ∀f1,f2. f1 ⋓ f2 ≘ f →
-      â\88\83â\88\83n2. ð\9d\90\82â\9dªf2â\9d« ≘ n2 & n2 ≤ n.
+      â\88\80f,n. ð\9d\90\82â\9d¨fâ\9d© ≘ n → ∀f1,f2. f1 ⋓ f2 ≘ f →
+      â\88\83â\88\83n2. ð\9d\90\82â\9d¨f2â\9d© ≘ n2 & n2 ≤ n.
 /3 width=4 by pr_sor_des_fcla_sn, pr_sor_comm/ qed-.