From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Thu, 30 Dec 2021 12:24:12 +0000 (+0100)
Subject: update in ground, static_2 and apps_2
X-Git-Tag: make_still_working~118
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=873fb39bdd21aa14877bf5d50db26e3a050c6d43;p=helm.git
update in ground, static_2 and apps_2
+ updated notation for extensional equality
---
diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
index d7d6211ec..2e0249286 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
@@ -20,7 +20,7 @@ include "apps_2/functional/mf_vlift.ma".
(* Properties with extensional equivalence **********************************)
-lemma mf_gc_id: âj. â¡[j]mf_gi â mf_gi.
+lemma mf_gc_id: âj. â¡[j]mf_gi â mf_gi.
// qed.
lemma mf_vlift_comp (l): compatible_2 ⦠(mf_vlift l) (exteq â¦) (exteq â¦).
@@ -30,5 +30,5 @@ qed.
(* Main properties with extensional equivalence *****************************)
-theorem mf_vlift_swap: âl1,l2. l2 ⤠l1 â âv. â¡[l2]â¡[l1]v â â¡[âl1]â¡[l2]v.
+theorem mf_vlift_swap: âl1,l2. l2 ⤠l1 â âv. â¡[l2]â¡[l1]v â â¡[âl1]â¡[l2]v.
/2 width=1 by flifts_basic_swap/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
index 855934ca2..ccc1c34f0 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
@@ -20,7 +20,7 @@ include "apps_2/functional/mf_vpush.ma".
(* Properties with extensional equivalence **********************************)
-lemma mf_lc_id: â¡[0â#0]mf_li â mf_li.
+lemma mf_lc_id: â¡[0â#0]mf_li â mf_li.
#i elim (eq_or_gt i) #Hi destruct //
>mf_vpush_gt // >(flifts_lref_uni 1) <(S_pred ⦠Hi) in ⢠(???%); -Hi //
qed.
@@ -37,7 +37,7 @@ qed-.
(* Main properties with extensional equivalence *****************************)
theorem mf_vpush_swap: âl1,l2. l2 ⤠l1 â
- âv,T1,T2. â¡[l2âT2]â¡[l1âT1]v â â¡[âl1ââ[l2,1]T1]â¡[l2âT2]v.
+ âv,T1,T2. â¡[l2âT2]â¡[l1âT1]v â â¡[âl1ââ[l2,1]T1]â¡[l2âT2]v.
#l1 #l2 #Hl21 #v #T1 #T2 #i
elim (lt_or_eq_or_gt i l2) #Hl2 destruct
[ lapply (lt_to_le_to_lt ⦠Hl2 Hl21) #Hl1
diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
index c1f6e76ce..1155e3487 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
@@ -19,7 +19,7 @@ include "apps_2/functional/mf_vpush.ma".
(* Properties with multiple filling lift ************************************)
-lemma mf_vpush_vlift_swap_O (v) (T) (l): â¡[0ââ[âl,1]T]â¡[l]v ââ¡[âl]â¡[0âT]v.
+lemma mf_vpush_vlift_swap_O (v) (T) (l): â¡[0ââ[âl,1]T]â¡[l]v ââ¡[âl]â¡[0âT]v.
#v #T #l #i
elim (eq_or_gt i) #Hi destruct
[ >mf_vpush_eq >mf_vlift_rw >mf_vpush_eq //
@@ -28,6 +28,6 @@ elim (eq_or_gt i) #Hi destruct
]
qed.
-lemma mf_vpush_vlift_swap_O_lref_O (v) (l): â¡[0â#0]â¡[l]v ââ¡[âl]â¡[0â#0]v.
+lemma mf_vpush_vlift_swap_O_lref_O (v) (l): â¡[0â#0]â¡[l]v ââ¡[âl]â¡[0â#0]v.
#v #l @(mf_vpush_vlift_swap_O ⦠(#0))
qed.
diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma
index 1eae07864..d0460b09c 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma
@@ -19,7 +19,7 @@ include "apps_2/models/tm.ma".
(* Properties with push for model evaluation ********************************)
-lemma tm_vpush_vlift_join_O (h) (v) (T): â¡[0]⫯{TM h}[0âT]v â â¡[0ââ[1]T]v.
+lemma tm_vpush_vlift_join_O (h) (v) (T): â¡[0]⫯{TM h}[0âT]v â â¡[0ââ[1]T]v.
#h #v #T #i
elim (eq_or_gt i) #Hi destruct
[ >mf_vpush_eq >mf_vlift_rw >vpush_eq //
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
index 6adaa148a..fc824317a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
@@ -35,20 +35,20 @@ interpretation
lemma niter_zero (A) (f) (a): a = (f^{A}ð) a.
// qed.
-lemma niter_inj (A) (f) (p): f^p â f^{A}(ninj p).
+lemma niter_inj (A) (f) (p): f^p â f^{A}(ninj p).
// qed.
(* Advanced constructions ***************************************************)
(*** iter_n_Sm *)
-lemma niter_appl (A) (f) (n): f â f^n â f^{A}n â f.
+lemma niter_appl (A) (f) (n): f â f^n â f^{A}n â f.
#A #f * //
#p @exteq_repl
/2 width=5 by piter_appl, compose_repl_fwd_dx/
qed.
lemma niter_compose (A) (B) (f) (g) (h) (n):
- h â f â g â h â h â (f^{A}n) â (g^{B}n) â h.
+ h â f â g â h â h â (f^{A}n) â (g^{B}n) â h.
#A #B #f #g #h * //
#p #H @exteq_repl
/2 width=5 by piter_compose, compose_repl_fwd_dx/
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index a9894fc62..19b8acdd0 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -43,7 +43,7 @@ qed.
(*** iter_plus *)
lemma niter_plus (A) (f) (n1) (n2):
- f^n2 â f^n1 â f^{A}(n1+n2).
+ f^n2 â f^n1 â f^{A}(n1+n2).
#A #f #n1 #n2 @(nat_ind_succ ⦠n2) -n2 //
#n2 #IH <nplus_succ_dx
@exteq_repl
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
index 7f47f9158..29e3e4d4f 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
@@ -20,6 +20,6 @@ include "ground/arith/nat_succ.ma".
(* Constructions with niter *************************************************)
(*** iter_S *)
-lemma niter_succ (A) (f) (n): f â f^n â f^{A}(ân).
+lemma niter_succ (A) (f) (n): f â f^n â f^{A}(ân).
#A #f * //
qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
index 5361dcef3..95425f8eb 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
@@ -31,22 +31,22 @@ interpretation
(* Basic constructions ******************************************************)
-lemma piter_unit (A) (f): f â f^{A}ð.
+lemma piter_unit (A) (f): f â f^{A}ð.
// qed.
-lemma piter_succ (A) (f) (p): f â f^p â f^{A}(âp).
+lemma piter_succ (A) (f) (p): f â f^p â f^{A}(âp).
// qed.
(* Advanced constructions ***************************************************)
-lemma piter_appl (A) (f) (p): f â f^p â f^{A}p â f.
+lemma piter_appl (A) (f) (p): f â f^p â f^{A}p â f.
#A #f #p elim p -p //
#p #IH @exteq_repl
/3 width=5 by compose_repl_fwd_dx, compose_repl_fwd_sn, exteq_canc_dx/
qed.
lemma piter_compose (A) (B) (f) (g) (h) (p):
- h â f â g â h â h â (f^{A}p) â (g^{B}p) â h.
+ h â f â g â h â h â (f^{A}p) â (g^{B}p) â h.
#A #B #f #g #h #p elim p -p
[ #H @exteq_repl
/2 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
index 81c5373a0..8c8f218a1 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
@@ -12,7 +12,7 @@
(* *)
(**************************************************************************)
-include "ground/notation/relations/doteq_4.ma".
+include "ground/notation/relations/circled_eq_4.ma".
include "ground/lib/relations.ma".
(* EXTENSIONAL EQUIVALENCE FOR FUNCTIONS ************************************)
@@ -22,7 +22,7 @@ definition exteq (A,B:Type[0]): relation (A â B) â
interpretation
"extensional equivalence"
- 'DotEq A B f1 f2 = (exteq A B f1 f2).
+ 'CircledEq A B f1 f2 = (exteq A B f1 f2).
(* Basic constructions ******************************************************)
@@ -53,27 +53,27 @@ lemma exteq_canc_dx (A) (B):
(* Constructions with compose ***********************************************)
lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):
- f1 â{A,B} f2 â g â f1 â{A,C} g â f2.
+ f1 â{A,B} f2 â g â f1 â{A,C} g â f2.
#A #B #C #g #f1 #f2 #Hf12 #a
whd in ⢠(??%%); //
qed.
lemma compose_repl_bak_dx (A) (B) (C) (g) (f1) (f2):
- f1 â{A,B} f2 â g â f2 â{A,C} g â f1.
+ f1 â{A,B} f2 â g â f2 â{A,C} g â f1.
/3 width=1 by compose_repl_fwd_dx, exteq_sym/
qed.
lemma compose_repl_fwd_sn (A) (B) (C) (g1) (g2) (f):
- g1 â{B,C} g2 â g1 â f â{A,C} g2 â f.
+ g1 â{B,C} g2 â g1 â f â{A,C} g2 â f.
#A #B #C #g1 #g2 #f #Hg12 #a
whd in ⢠(??%%); //
qed.
lemma compose_repl_bak_sn (A) (B) (C) (g1) (g2) (f):
- g1 â{B,C} g2 â g2 â f â{A,C} g1 â f.
+ g1 â{B,C} g2 â g2 â f â{A,C} g1 â f.
/3 width=1 by compose_repl_fwd_sn, exteq_sym/
qed.
lemma compose_assoc (A1) (A2) (A3) (A4) (f3:A3âA4) (f2:A2âA3) (f1:A1âA2):
- f3 â (f2 â f1) â f3 â f2 â f1.
+ f3 â (f2 â f1) â f3 â f2 â f1.
// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/circled_eq_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/circled_eq_4.ma
new file mode 100644
index 000000000..4f602ce15
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/circled_eq_4.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation < "hvbox( f1 â break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'CircledEq $A $B $f1 $f2 }.
+
+notation > "hvbox( f1 â break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'CircledEq ? ? $f1 $f2 }.
+
+notation > "hvbox( f1 â{ break term 46 A, break term 46 B } break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'CircledEq $A $B $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_2.ma
new file mode 100644
index 000000000..46cfbb51b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( f1 â break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'DotEq $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma
deleted file mode 100644
index 5ccb16c4b..000000000
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation < "hvbox( term 46 f1 â break term 46 f2 )"
- non associative with precedence 45
- for @{ 'DotEq $A $B $f1 $f2 }.
-
-notation > "hvbox( f1 â break term 46 f2 )"
- non associative with precedence 45
- for @{ 'DotEq ? ? $f1 $f2 }.
-
-notation > "hvbox( f1 â{ break term 46 A, break term 46 B } break term 46 f2 )"
- non associative with precedence 45
- for @{ 'DotEq $A $B $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma
index 2f5287d6b..97639a36c 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma
@@ -12,8 +12,6 @@
(* *)
(**************************************************************************)
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
(* GROUND NOTATION **********************************************************)
notation < "hvbox( a ϵ break term 46 u )"
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma
deleted file mode 100644
index 8ade3ee43..000000000
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( f1 â¡ break term 46 f2 )"
- non associative with precedence 45
- for @{ 'IdEq $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
index c048ec402..741da1062 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
@@ -74,7 +74,7 @@ qed-.
(*** after_mono *)
corec theorem pr_after_mono:
- âf1,f2,x,y. f1 â f2 â x â f1 â f2 â y â x â¡ y.
+ âf1,f2,x,y. f1 â f2 â x â f1 â f2 â y â x â y.
#f1 #f2 #x #y * -f1 -f2 -x
#f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
[ cases (pr_after_inv_push_bi ⦠Hy ⦠H1 H2) -g1 -g2 /3 width=8 by pr_eq_push/
@@ -86,5 +86,5 @@ qed-.
(*** after_mono_eq *)
lemma pr_after_mono_eq:
âf1,f2,f. f1 â f2 â f â âg1,g2,g. g1 â g2 â g â
- f1 â¡ g1 â f2 â¡ g2 â f â¡ g.
+ f1 â g1 â f2 â g2 â f â g.
/4 width=4 by pr_after_mono, pr_after_eq_repl_back_dx, pr_after_eq_repl_back_sn/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
index e67235f76..cb234dc2d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
@@ -22,7 +22,7 @@ include "ground/relocation/pr_after_pat_tls.ma".
(*** H_after_inj *)
definition H_pr_after_inj: predicate pr_map â
λf1. ðâ¨f1â© â
- âf,f21,f22. f1 â f21 â f â f1 â f22 â f â f21 â¡ f22.
+ âf,f21,f22. f1 â f21 â f â f1 â f22 â f â f21 â f22.
(* Main destructions with pr_ist ********************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma
index 494659038..f5457f3c3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma
@@ -41,12 +41,12 @@ qed.
(*** after_isid_inv_sn *)
lemma pr_after_isi_inv_sn:
- âf1,f2,f. f1 â f2 â f â ðâ¨f1â© â f2 â¡ f.
+ âf1,f2,f. f1 â f2 â f â ðâ¨f1â© â f2 â f.
/3 width=6 by pr_after_isi_sn, pr_after_mono/ qed-.
(*** after_isid_inv_dx *)
lemma pr_after_isi_inv_dx:
- âf1,f2,f. f1 â f2 â f â ðâ¨f2â© â f1 â¡ f.
+ âf1,f2,f. f1 â f2 â f â ðâ¨f2â© â f1 â f.
/3 width=6 by pr_after_isi_dx, pr_after_mono/ qed-.
(*** after_fwd_isid1 *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
index 4e17044de..16d2ebc8d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_after_ist.ma".
(*** after_fwd_isid_sn *)
lemma pr_after_des_ist_eq_sn:
- âf2,f1,f. ðâ¨fâ© â f2 â f1 â f â f1 â¡ f â ðâ¨f2â©.
+ âf2,f1,f. ðâ¨fâ© â f2 â f1 â f â f1 â f â ðâ¨f2â©.
#f2 #f1 #f #H #Hf elim (pr_after_inv_ist ⦠Hf H) -H
#Hf2 #Hf1 #H @pr_isi_pat_total // -Hf2
#i2 #i #Hf2 elim (Hf1 i2) -Hf1
@@ -32,7 +32,7 @@ qed-.
(*** after_fwd_isid_dx *)
lemma pr_after_des_ist_eq_dx:
- âf2,f1,f. ðâ¨fâ© â f2 â f1 â f â f2 â¡ f â ðâ¨f1â©.
+ âf2,f1,f. ðâ¨fâ© â f2 â f1 â f â f2 â f â ðâ¨f1â©.
#f2 #f1 #f #H #Hf elim (pr_after_inv_ist ⦠Hf H) -H
#Hf2 #Hf1 #H2 @pr_isi_pat_total // -Hf1
#i1 #i2 #Hi12 elim (pr_after_des_ist_pat ⦠Hi12 ⦠Hf) -f1
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
index 8ac9736a7..ff06a8c35 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_coafter_eq.ma".
(*** coafter_mono *)
corec theorem pr_coafter_mono:
- âf1,f2,x,y. f1 ~â f2 â x â f1 ~â f2 â y â x â¡ y.
+ âf1,f2,x,y. f1 ~â f2 â x â f1 ~â f2 â y â x â y.
#f1 #f2 #x #y * -f1 -f2 -x
#f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
[ cases (pr_coafter_inv_push_bi ⦠Hy ⦠H1 H2) -g1 -g2 /3 width=8 by pr_eq_push/
@@ -32,5 +32,5 @@ qed-.
(*** coafter_mono_eq *)
lemma pr_coafter_mono_eq:
âf1,f2,f. f1 ~â f2 â f â âg1,g2,g. g1 ~â g2 â g â
- f1 â¡ g1 â f2 â¡ g2 â f â¡ g.
+ f1 â g1 â f2 â g2 â f â g.
/4 width=4 by pr_coafter_mono, pr_coafter_eq_repl_back_dx, pr_coafter_eq_repl_back_sn/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
index d627e2597..e60d548e7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_coafter_nat_tls.ma".
(*** H_coafter_inj *)
definition H_pr_coafter_inj: predicate pr_map â
λf1. ðâ¨f1â© â
- âf,f21,f22. f1 ~â f21 â f â f1 ~â f22 â f â f21 â¡ f22.
+ âf,f21,f22. f1 ~â f21 â f â f1 ~â f22 â f â f21 â f22.
(* Main destructions with pr_ist ********************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
index 7bed357e1..5ed452f2b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
@@ -41,7 +41,7 @@ qed.
(*** coafter_isid_inv_sn *)
lemma pr_coafter_isi_inv_sn:
- âf1,f2,f. f1 ~â f2 â f â ðâ¨f1â© â f2 â¡ f.
+ âf1,f2,f. f1 ~â f2 â f â ðâ¨f1â© â f2 â f.
/3 width=6 by pr_coafter_isi_sn, pr_coafter_mono/ qed-.
(*** coafter_isid_inv_dx *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
index 12ce1a69c..71a256c10 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
@@ -63,5 +63,5 @@ qed.
(* Main inversions **********************************************************)
(*** after_inv_total *)
-lemma pr_after_inv_total: âf2,f1,f. f2 â f1 â f â f2 â f1 â¡ f.
+lemma pr_after_inv_total: âf2,f1,f. f2 â f1 â f â f2 â f1 â f.
/2 width=4 by pr_after_mono/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
index 610ba9c7d..c908a6ac3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
@@ -13,7 +13,7 @@
(**************************************************************************)
include "ground/xoa/ex_3_2.ma".
-include "ground/notation/relations/ideq_2.ma".
+include "ground/notation/relations/doteq_2.ma".
include "ground/lib/stream_eq.ma".
include "ground/relocation/pr_map.ma".
@@ -31,19 +31,19 @@ coinductive pr_eq: relation pr_map â
interpretation
"extensional equivalence (partial relocation maps)"
- 'IdEq f1 f2 = (pr_eq f1 f2).
+ 'DotEq f1 f2 = (pr_eq f1 f2).
(*** eq_repl *)
definition pr_eq_repl (R:relation â¦) â
- âf1,f2. f1 â¡ f2 â R f1 f2.
+ âf1,f2. f1 â f2 â R f1 f2.
(*** eq_repl_back *)
definition pr_eq_repl_back (R:predicate â¦) â
- âf1. R f1 â âf2. f1 â¡ f2 â R f2.
+ âf1. R f1 â âf2. f1 â f2 â R f2.
(*** eq_repl_fwd *)
definition pr_eq_repl_fwd (R:predicate â¦) â
- âf1. R f1 â âf2. f2 â¡ f1 â R f2.
+ âf1. R f1 â âf2. f2 â f1 â R f2.
(* Basic constructions ******************************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
index 1e1fd6af5..cb7ff5bf5 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
@@ -19,7 +19,7 @@ include "ground/relocation/pr_id.ma".
(* Constructions with pr_eq *************************************************)
-corec lemma pr_id_eq (f): ⫯f â¡ f â ð¢ â¡ f.
+corec lemma pr_id_eq (f): ⫯f â f â ð¢ â f.
cases pr_id_unfold #Hf
cases (pr_eq_inv_push_sn ⦠Hf) [|*: // ] #_ #H
cases H in Hf; -H #Hf
@@ -30,7 +30,7 @@ qed.
(* Inversions with pr_eq ****************************************************)
(* Note: this has the same proof of the previous *)
-corec lemma pr_id_inv_eq (f): ð¢ â¡ f â ⫯f â¡ f.
+corec lemma pr_id_inv_eq (f): ð¢ â f â ⫯f â f.
cases pr_id_unfold #Hf
cases (pr_eq_inv_push_sn ⦠Hf) [|*: // ] #_ #H
cases H in Hf; -H #Hf
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma
index a6000c810..9b00fda4d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma
@@ -35,7 +35,7 @@ lemma pr_isd_eq_repl_fwd:
(* Main inversions with pr_eq ***********************************************)
(*** isdiv_inv_eq_repl *)
-corec theorem pr_isd_inv_eq_repl (g1) (g2): ðâ¨g1â© â ðâ¨g2â© â g1 â¡ g2.
+corec theorem pr_isd_inv_eq_repl (g1) (g2): ðâ¨g1â© â ðâ¨g2â© â g1 â g2.
#H1 #H2
cases (pr_isd_inv_gen ⦠H1) -H1
cases (pr_isd_inv_gen ⦠H2) -H2
@@ -45,13 +45,13 @@ qed-.
(* Alternative definition with pr_eq ****************************************)
(*** eq_next_isdiv *)
-corec lemma pr_eq_next_isd (f): âf â¡ f â ðâ¨fâ©.
+corec lemma pr_eq_next_isd (f): âf â f â ðâ¨fâ©.
#H cases (pr_eq_inv_next_sn ⦠H) -H
/4 width=3 by pr_isd_next, pr_eq_trans/
qed.
(*** eq_next_inv_isdiv *)
-corec lemma pr_eq_next_inv_isd (g): ðâ¨gâ© â âg â¡ g.
+corec lemma pr_eq_next_inv_isd (g): ðâ¨gâ© â âg â g.
* -g #f #g #Hf *
/3 width=5 by pr_eq_next/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma
index 58317065d..189567290 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma
@@ -36,7 +36,7 @@ lemma pr_isi_eq_repl_fwd:
(* Main inversions with pr_eq ***********************************************)
(*** isid_inv_eq_repl *)
-corec theorem pr_isi_inv_eq_repl (g1) (g2): ðâ¨g1â© â ðâ¨g2â© â g1 â¡ g2.
+corec theorem pr_isi_inv_eq_repl (g1) (g2): ðâ¨g1â© â ðâ¨g2â© â g1 â g2.
#H1 #H2
cases (pr_isi_inv_gen ⦠H1) -H1
cases (pr_isi_inv_gen ⦠H2) -H2
@@ -46,13 +46,13 @@ qed-.
(* Alternative definition with pr_eq ****************************************)
(*** eq_push_isid *)
-corec lemma pr_eq_push_isi (f): ⫯f â¡ f â ðâ¨fâ©.
+corec lemma pr_eq_push_isi (f): ⫯f â f â ðâ¨fâ©.
#H cases (pr_eq_inv_push_sn ⦠H) -H
/4 width=3 by pr_isi_push, pr_eq_trans/
qed.
(*** eq_push_inv_isid *)
-corec lemma pr_isi_inv_eq_push (g): ðâ¨gâ© â ⫯g â¡ g.
+corec lemma pr_isi_inv_eq_push (g): ðâ¨gâ© â ⫯g â g.
* -g #f #g #Hf *
/3 width=5 by pr_eq_push/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
index 374fcdce4..9e3ffed09 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
@@ -26,9 +26,9 @@ lemma pr_isi_id: ðâ¨ð¢â©.
(* Alternative definition with pr_id and pr_eq ******************************)
(*** eq_id_isid *)
-lemma pr_eq_id_isi (f): ð¢ â¡ f â ðâ¨fâ©.
+lemma pr_eq_id_isi (f): ð¢ â f â ðâ¨fâ©.
/2 width=3 by pr_isi_eq_repl_back/ qed.
(*** eq_id_inv_isid *)
-lemma pr_isi_inv_eq_id (f): ðâ¨fâ© â ð¢ â¡ f.
+lemma pr_isi_inv_eq_id (f): ðâ¨fâ© â ð¢ â f.
/2 width=1 by pr_isi_inv_eq_repl/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
index 1db92adae..48c57a284 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
@@ -20,11 +20,11 @@ include "ground/relocation/pr_isi_id.ma".
(* Constructions with pr_isi ************************************************)
(*** uni_inv_isid uni_isi *)
-lemma pr_uni_isi (f): ð®â¨ðâ© â¡ f â ðâ¨fâ©.
+lemma pr_uni_isi (f): ð®â¨ðâ© â f â ðâ¨fâ©.
/2 width=1 by pr_eq_id_isi/ qed.
(* Inversions with pr_isi ***************************************************)
(*** uni_isid isi_inv_uni *)
-lemma pr_isi_inv_uni (f): ðâ¨fâ© â ð®â¨ðâ© â¡ f.
+lemma pr_isi_inv_uni (f): ðâ¨fâ© â ð®â¨ðâ© â f.
/2 width=1 by pr_isi_inv_eq_id/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
index cfb786adc..de3ecfe4e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
@@ -47,7 +47,7 @@ qed-.
(*** at_ext *)
corec theorem pr_eq_ext_pat (f1) (f2): ðâ¨f1â© â ðâ¨f2â© â
(âi,i1,i2. @â¨i,f1â© â i1 â @â¨i,f2â© â i2 â i1 = i2) â
- f1 â¡ f2.
+ f1 â f2.
cases (pr_map_split_tl f1) #H1
cases (pr_map_split_tl f2) #H2
#Hf1 #Hf2 #Hi
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
index 1e6706a8b..bb4cceede 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
@@ -43,7 +43,7 @@ lemma pr_isu_eq_repl_fwd:
(* Inversions with pr_uni ***************************************************)
(*** uni_isuni *)
-lemma pr_isu_inv_uni (f): ðâ¨fâ© â ân. ð®â¨nâ© â¡ f.
+lemma pr_isu_inv_uni (f): ðâ¨fâ© â ân. ð®â¨nâ© â f.
#f #H elim H -f
[ /3 width=2 by pr_isi_inv_uni, ex_intro/
| #f #_ #g #H * /3 width=6 by pr_eq_next, ex_intro/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
index 3ca8053d8..9e06b6fe7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_nexts.ma".
(*** nexts_eq_repl *)
lemma pr_nexts_eq_repl (n):
- pr_eq_repl (λf1,f2. â*[n] f1 â¡ â*[n] f2).
+ pr_eq_repl (λf1,f2. â*[n] f1 â â*[n] f2).
#n @(nat_ind_succ ⦠n) -n
/3 width=5 by pr_eq_next/
qed.
@@ -29,8 +29,8 @@ qed.
(* Inversions with pr_eq ****************************************************)
lemma pr_eq_inv_nexts_push_bi (f1) (f2) (n1) (n2):
- â*[n1] ⫯f1 â¡ â*[n2] ⫯f2 â
- â§â§ n1 = n2 & f1 â¡ f2.
+ â*[n1] ⫯f1 â â*[n2] ⫯f2 â
+ â§â§ n1 = n2 & f1 â f2.
#f1 #f2
#n1 @(nat_ind_succ ⦠n1) -n1 [| #n1 #IH ]
#n2 @(nat_ind_succ ⦠n2) -n2 [2,4: #n2 #_ ]
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
index 010fa0548..29620d121 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
@@ -38,7 +38,7 @@ lemma pr_pat_eq_repl_fwd (i1) (i2):
#i1 #i2 @pr_eq_repl_sym /2 width=3 by pr_pat_eq_repl_back/
qed-.
-lemma pr_pat_eq (f): ⫯f â¡ f â âi. @â¨i,fâ© â i.
+lemma pr_pat_eq (f): ⫯f â f â âi. @â¨i,fâ© â i.
#f #Hf #i elim i -i
[ /3 width=3 by pr_pat_eq_repl_back, pr_pat_refl/
| /3 width=7 by pr_pat_eq_repl_back, pr_pat_push/
@@ -48,7 +48,7 @@ qed.
(* Inversions with pr_eq ****************************************************)
corec lemma pr_pat_inv_eq (f):
- (âi. @â¨i,fâ© â i) â ⫯f â¡ f.
+ (âi. @â¨i,fâ© â i) â ⫯f â f.
#Hf
lapply (Hf (ð)) #H
lapply (pr_pat_des_id ⦠H) -H #H
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
index a63fb9355..013468796 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
@@ -27,6 +27,6 @@ lemma pr_pat_id (i): @â¨i,ð¢â© â i.
(*** id_inv_at *)
lemma pr_pat_inv_id (f):
- (âi. @â¨i,fâ© â i) â ð¢ â¡ f.
+ (âi. @â¨i,fâ© â i) â ð¢ â f.
/3 width=1 by pr_pat_inv_eq, pr_id_eq/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
index 81dfaeecd..eaaaf0501 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
@@ -32,7 +32,7 @@ qed.
(* Note: this requires â on third n2 *)
(*** at_tls *)
-lemma pr_pat_tls (n2) (f): ⫯⫰*[ân2]f â¡ â«°*[n2]f â âi1. @â¨i1,fâ© â ân2.
+lemma pr_pat_tls (n2) (f): ⫯⫰*[ân2]f â â«°*[n2]f â âi1. @â¨i1,fâ© â ân2.
#n2 @(nat_ind_succ ⦠n2) -n2
[ /4 width=4 by pr_pat_eq_repl_back, pr_pat_refl, ex_intro/
| #n2 #IH #f <pr_tls_swap <pr_tls_swap in ⢠(??%â?); #H
@@ -65,7 +65,7 @@ qed-.
(* Note: this requires â on first n2 *)
(*** at_inv_tls *)
lemma pr_pat_inv_succ_dx_tls (n2) (i1) (f):
- @â¨i1,fâ© â ân2 â ⫯⫰*[ân2]f â¡ â«°*[n2]f.
+ @â¨i1,fâ© â ân2 â ⫯⫰*[ân2]f â â«°*[n2]f.
#n2 @(nat_ind_succ ⦠n2) -n2
[ #i1 #f #Hf elim (pr_pat_inv_unit_dx ⦠Hf) -Hf // #g #H1 #H destruct
/2 width=1 by pr_eq_refl/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma
index 11f4036a2..dacdb9b69 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_pushs.ma".
(*** pushs_eq_repl *)
lemma pr_pushs_eq_repl (n):
- pr_eq_repl (λf1,f2. ⫯*[n] f1 ⡠⫯*[n] f2).
+ pr_eq_repl (λf1,f2. ⫯*[n] f1 â ⫯*[n] f2).
#n @(nat_ind_succ ⦠n) -n
/3 width=5 by pr_eq_push/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
index 383ad127f..aa826268e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
@@ -56,5 +56,5 @@ qed-.
(*** sle_refl_eq *)
lemma pr_sle_refl_eq:
- âf1,f2. f1 â¡ f2 â f1 â f2.
+ âf1,f2. f1 â f2 â f1 â f2.
/2 width=3 by pr_sle_eq_repl_back_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
index bc307df7e..98eaf1ed1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
@@ -66,13 +66,13 @@ qed-.
(*** sor_isid_inv_sn *)
lemma pr_sor_inv_isi_sn:
- âf1,f2,f. f1 â f2 â f â ðâ¨f1â© â f2 â¡ f.
+ âf1,f2,f. f1 â f2 â f â ðâ¨f1â© â f2 â f.
/3 width=4 by pr_sor_isi_sn, pr_sor_mono/
qed-.
(*** sor_isid_inv_dx *)
lemma pr_sor_inv_isi_dx:
- âf1,f2,f. f1 â f2 â f â ðâ¨f2â© â f1 â¡ f.
+ âf1,f2,f. f1 â f2 â f â ðâ¨f2â© â f1 â f.
/3 width=4 by pr_sor_isi_dx, pr_sor_mono/
qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
index ef667fd7e..c52154795 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sor.ma".
(*** sor_mono *)
corec theorem pr_sor_mono:
- âf1,f2,x,y. f1 â f2 â x â f1 â f2 â y â x â¡ y.
+ âf1,f2,x,y. f1 â f2 â x â f1 â f2 â y â x â y.
#f1 #f2 #x #y * -f1 -f2 -x
#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H
[ cases (pr_sor_inv_push_bi ⦠H ⦠H1 H2)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma
index 03c413e46..fe7e7b3a8 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma
@@ -27,7 +27,7 @@ qed.
(*** tl_eq_repl *)
lemma pr_tl_eq_repl:
- pr_eq_repl ⦠(λf1,f2. ⫰f1 ⡠⫰f2).
+ pr_eq_repl ⦠(λf1,f2. â«°f1 â â«°f2).
#f1 #f2 * -f1 -f2 //
qed.
@@ -35,9 +35,9 @@ qed.
(*** eq_inv_gen *)
lemma pr_eq_inv_gen (g1) (g2):
- g1 â¡ g2 â
- â¨â¨ â§â§ â«°g1 â¡ â«°g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
- | â§â§ â«°g1 â¡ â«°g2 & ââ«°g1 = g1 & ââ«°g2 = g2.
+ g1 â g2 â
+ â¨â¨ â§â§ â«°g1 â â«°g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
+ | â§â§ â«°g1 â â«°g2 & ââ«°g1 = g1 & ââ«°g2 = g2.
#g1 #g2 * -g1 -g2 #f1 #f2 #g1 #g2 #f * *
/3 width=1 by and3_intro, or_introl, or_intror/
qed-.
@@ -46,8 +46,8 @@ qed-.
(*** pr_eq_inv_px *)
lemma pr_eq_inv_push_sn (g1) (g2):
- g1 â¡ g2 â âf1. ⫯f1 = g1 â
- â§â§ f1 â¡ â«°g2 & ⫯⫰g2 = g2.
+ g1 â g2 â âf1. ⫯f1 = g1 â
+ â§â§ f1 â â«°g2 & ⫯⫰g2 = g2.
#g1 #g2 #H #f1 #Hf1
elim (pr_eq_inv_gen ⦠H) -H * #Hg #Hg1 #Hg2 destruct
[ /2 width=1 by conj/
@@ -57,8 +57,8 @@ qed-.
(*** pr_eq_inv_nx *)
lemma pr_eq_inv_next_sn (g1) (g2):
- g1 â¡ g2 â âf1. âf1 = g1 â
- â§â§ f1 â¡ â«°g2 & ââ«°g2 = g2.
+ g1 â g2 â âf1. âf1 = g1 â
+ â§â§ f1 â â«°g2 & ââ«°g2 = g2.
#g1 #g2 #H #f1 #Hf1
elim (pr_eq_inv_gen ⦠H) -H * #Hg #Hg1 #Hg2 destruct
[ elim (eq_inv_pr_push_next ⦠Hg1)
@@ -68,8 +68,8 @@ qed-.
(*** pr_eq_inv_xp *)
lemma pr_eq_inv_push_dx (g1) (g2):
- g1 â¡ g2 â âf2. ⫯f2 = g2 â
- â§â§ â«°g1 â¡ f2 & ⫯⫰g1 = g1.
+ g1 â g2 â âf2. ⫯f2 = g2 â
+ â§â§ â«°g1 â f2 & ⫯⫰g1 = g1.
#g1 #g2 #H #f2 #Hf2
elim (pr_eq_inv_gen ⦠H) -H * #Hg #Hg1 #Hg2 destruct
[ /2 width=1 by conj/
@@ -79,8 +79,8 @@ qed-.
(*** pr_eq_inv_xn *)
lemma pr_eq_inv_next_dx (g1) (g2):
- g1 â¡ g2 â âf2. âf2 = g2 â
- â§â§ â«°g1 â¡ f2 & ââ«°g1 = g1.
+ g1 â g2 â âf2. âf2 = g2 â
+ â§â§ â«°g1 â f2 & ââ«°g1 = g1.
#g1 #g2 #H #f2 #Hf2
elim (pr_eq_inv_gen ⦠H) -H * #Hg #Hg1 #Hg2 destruct
[ elim (eq_inv_pr_push_next ⦠Hg2)
@@ -90,7 +90,7 @@ qed-.
(*** pr_eq_inv_pp *)
lemma pr_eq_inv_push_bi (g1) (g2):
- g1 â¡ g2 â âf1,f2. ⫯f1 = g1 â ⫯f2 = g2 â f1 â¡ f2.
+ g1 â g2 â âf1,f2. ⫯f1 = g1 â ⫯f2 = g2 â f1 â f2.
#g1 #g2 #H #f1 #f2 #H1
elim (pr_eq_inv_push_sn ⦠H ⦠H1) -g1 #Hx2 * #H
lapply (eq_inv_pr_push_bi ⦠H) -H //
@@ -98,7 +98,7 @@ qed-.
(*** pr_eq_inv_nn *)
lemma pr_eq_inv_next_bi (g1) (g2):
- g1 â¡ g2 â âf1,f2. âf1 = g1 â âf2 = g2 â f1 â¡ f2.
+ g1 â g2 â âf1,f2. âf1 = g1 â âf2 = g2 â f1 â f2.
#g1 #g2 #H #f1 #f2 #H1
elim (pr_eq_inv_next_sn ⦠H ⦠H1) -g1 #Hx2 * #H
lapply (eq_inv_pr_next_bi ⦠H) -H //
@@ -106,7 +106,7 @@ qed-.
(*** pr_eq_inv_pn *)
lemma pr_eq_inv_push_next (g1) (g2):
- g1 â¡ g2 â âf1,f2. ⫯f1 = g1 â âf2 = g2 â â¥.
+ g1 â g2 â âf1,f2. ⫯f1 = g1 â âf2 = g2 â â¥.
#g1 #g2 #H #f1 #f2 #H1
elim (pr_eq_inv_push_sn ⦠H ⦠H1) -g1 #Hx2 * #H
elim (eq_inv_pr_next_push ⦠H)
@@ -114,7 +114,7 @@ qed-.
(*** pr_eq_inv_np *)
lemma pr_eq_inv_next_push (g1) (g2):
- g1 â¡ g2 â âf1,f2. âf1 = g1 â ⫯f2 = g2 â â¥.
+ g1 â g2 â âf1,f2. âf1 = g1 â ⫯f2 = g2 â â¥.
#g1 #g2 #H #f1 #f2 #H1
elim (pr_eq_inv_next_sn ⦠H ⦠H1) -g1 #Hx2 * #H
elim (eq_inv_pr_push_next ⦠H)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
index 94592fdfd..43b69b3f0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
@@ -29,9 +29,9 @@ corec theorem pr_eq_trans: Transitive ⦠pr_eq.
qed-.
(*** eq_canc_sn *)
-theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f ⡠f2).
+theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f â f2).
/3 width=3 by pr_eq_trans, pr_eq_sym/ qed-.
(*** eq_canc_dx *)
-theorem pr_eq_canc_dx (f1): pr_eq_repl_fwd (λf. f1 ⡠f).
+theorem pr_eq_canc_dx (f1): pr_eq_repl_fwd (λf. f1 â f).
/3 width=5 by pr_eq_canc_sn, pr_eq_repl_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma
index f3b5bc74d..ce9fc0ad0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma
@@ -21,6 +21,6 @@ include "ground/relocation/pr_tls.ma".
(*** tls_eq_repl *)
lemma pr_tls_eq_repl (n):
- pr_eq_repl (λf1,f2. ⫰*[n] f1 ⡠⫰*[n] f2).
+ pr_eq_repl (λf1,f2. â«°*[n] f1 â â«°*[n] f2).
#n @(nat_ind_succ ⦠n) -n /3 width=1 by pr_tl_eq_repl/
qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma
index 004b20fe7..b17dc66ee 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma
@@ -21,8 +21,8 @@ include "ground/relocation/pr_tls_eq.ma".
(*** eq_inv_nexts_sn *)
lemma pr_eq_inv_nexts_sn (n):
- âf1,g2. â*[n] f1 â¡ g2 â
- â§â§ f1 â¡ â«°*[n]g2 & â*[n]â«°*[n]g2 = g2.
+ âf1,g2. â*[n] f1 â g2 â
+ â§â§ f1 â â«°*[n]g2 & â*[n]â«°*[n]g2 = g2.
#n @(nat_ind_succ ⦠n) -n /2 width=1 by conj/
#n #IH #f1 #g2 #H
elim (pr_eq_inv_next_sn ⦠H) -H [|*: // ] #Hf10 *
@@ -32,8 +32,8 @@ qed-.
(*** eq_inv_nexts_dx *)
lemma pr_eq_inv_nexts_dx (n):
- âf2,g1. g1 â¡ â*[n] f2 â
- â§â§ â«°*[n]g1 â¡ f2 & â*[n]â«°*[n]g1 = g1.
+ âf2,g1. g1 â â*[n] f2 â
+ â§â§ â«°*[n]g1 â f2 & â*[n]â«°*[n]g1 = g1.
#n @(nat_ind_succ ⦠n) -n /2 width=1 by conj/
#n #IH #f2 #g1 #H
elim (pr_eq_inv_next_dx ⦠H) -H [|*: // ] #Hf02 *
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma
index 31055e9ad..37a657203 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma
@@ -21,8 +21,8 @@ include "ground/relocation/pr_pushs.ma".
(*** eq_inv_pushs_sn *)
lemma pr_eq_inv_pushs_sn (n):
- âf1,g2. ⫯*[n] f1 â¡ g2 â
- â§â§ f1 â¡ â«°*[n]g2 & ⫯*[n]â«°*[n]g2 = g2.
+ âf1,g2. ⫯*[n] f1 â g2 â
+ â§â§ f1 â â«°*[n]g2 & ⫯*[n]â«°*[n]g2 = g2.
#n @(nat_ind_succ ⦠n) -n /2 width=1 by conj/
#n #IH #f1 #g2 #H
elim (pr_eq_inv_push_sn ⦠H) -H [|*: // ] #Hf10 *
@@ -32,8 +32,8 @@ qed-.
(*** eq_inv_pushs_dx *)
lemma pr_eq_inv_pushs_dx (n):
- âf2,g1. g1 ⡠⫯*[n] f2 â
- â§â§ â«°*[n]g1 â¡ f2 & ⫯*[n]â«°*[n]g1 = g1.
+ âf2,g1. g1 â ⫯*[n] f2 â
+ â§â§ â«°*[n]g1 â f2 & ⫯*[n]â«°*[n]g1 = g1.
#n @(nat_ind_succ ⦠n) -n /2 width=1 by conj/
#n #IH #f2 #g1 #H
elim (pr_eq_inv_push_dx ⦠H) -H [|*: // ] #Hf02 *
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma
index 44e989101..f705ca84b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_uni.ma".
(* Inversions with pr_eq ****************************************************)
(*** uni_inv_push_dx *)
-lemma pr_eq_inv_uni_push (n) (g): ð®â¨n⩠⡠⫯g â â§â§ ð = n & ð¢ â¡ g.
+lemma pr_eq_inv_uni_push (n) (g): ð®â¨nâ© â ⫯g â â§â§ ð = n & ð¢ â g.
#n @(nat_ind_succ ⦠n) -n
[ /3 width=5 by pr_eq_inv_push_bi, conj/
| #n #_ #f <pr_uni_succ #H elim (pr_eq_inv_next_push ⦠H) -H //
@@ -29,11 +29,11 @@ lemma pr_eq_inv_uni_push (n) (g): ð®â¨n⩠⡠⫯g â â§â§ ð = n &
qed-.
(*** uni_inv_push_sn *)
-lemma pr_eq_inv_push_uni (n) (g): ⫯g â¡ ð®â¨nâ© â â§â§ ð = n & ð¢ â¡ g.
+lemma pr_eq_inv_push_uni (n) (g): ⫯g â ð®â¨nâ© â â§â§ ð = n & ð¢ â g.
/3 width=1 by pr_eq_inv_uni_push, pr_eq_sym/ qed-.
(*** uni_inv_next_dx *)
-lemma pr_eq_inv_uni_next (n) (g): ð®â¨nâ© â¡ âg â â§â§ ð®â¨ânâ© â¡ g & âân = n.
+lemma pr_eq_inv_uni_next (n) (g): ð®â¨nâ© â âg â â§â§ ð®â¨ânâ© â g & âân = n.
#n @(nat_ind_succ ⦠n) -n
[ #g <pr_uni_zero <pr_id_unfold #H elim (pr_eq_inv_push_next ⦠H) -H //
| #n #_ #g <pr_uni_succ /3 width=5 by pr_eq_inv_next_bi, conj/
@@ -41,16 +41,16 @@ lemma pr_eq_inv_uni_next (n) (g): ð®â¨nâ© â¡ âg â â§â§ ð®â¨ânâ©
qed-.
(*** uni_inv_next_sn *)
-lemma pr_eq_inv_next_uni (n) (g): âg â¡ ð®â¨nâ© â â§â§ ð®â¨ânâ© â¡ g & âân = n.
+lemma pr_eq_inv_next_uni (n) (g): âg â ð®â¨nâ© â â§â§ ð®â¨ânâ© â g & âân = n.
/3 width=1 by pr_eq_inv_uni_next, pr_eq_sym/ qed-.
(* Inversions with pr_id and pr_eq ******************************************)
(*** uni_inv_id_dx *)
-lemma pr_eq_inv_uni_id (n): ð®â¨nâ© â¡ ð¢ â ð = n.
+lemma pr_eq_inv_uni_id (n): ð®â¨nâ© â ð¢ â ð = n.
#n <pr_id_unfold #H elim (pr_eq_inv_uni_push ⦠H) -H //
qed-.
(*** uni_inv_id_sn *)
-lemma pr_eq_inv_id_uni (n): ð¢ â¡ ð®â¨nâ© â ð = n.
+lemma pr_eq_inv_id_uni (n): ð¢ â ð®â¨nâ© â ð = n.
/3 width=1 by pr_eq_inv_uni_id, pr_eq_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
index 663dfc9b6..4c8586c31 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
@@ -89,7 +89,7 @@ lemma after_inv_const: âf2,f1,f,p1,p.
]
qed-.
-lemma after_inv_total: âf2,f1,f. f2 â f1 â f â f2 â f1 â¡ f.
+lemma after_inv_total: âf2,f1,f. f2 â f1 â f â f2 â f1 â f.
/2 width=4 by gr_after_mono/ qed-.
(* Forward lemmas on after (specific) *****************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
index 869486b4a..262fe6167 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
@@ -19,7 +19,7 @@ include "ground/relocation/tr_nexts.ma".
(* Constructions with pr_eq and stream_eq ***********************************)
-corec lemma eq_tr_inj_bi (f1) (f2): f1 â f2 â ðâ¨f1â© â¡ ðâ¨f2â©.
+corec lemma eq_tr_inj_bi (f1) (f2): f1 â f2 â ðâ¨f1â© â ðâ¨f2â©.
* -f1 -f2 #p1 #p2 #f1 #f2 * -p2 #H
cases p1 -p1
[ @pr_eq_push /2 width=5 by/
@@ -31,7 +31,7 @@ qed.
(* Inversions with pr_eq and stream_eq **************************************)
-corec lemma eq_inv_tr_inj_bi (f1) (f2): ðâ¨f1â© â¡ ðâ¨f2â© â f1 â f2.
+corec lemma eq_inv_tr_inj_bi (f1) (f2): ðâ¨f1â© â ðâ¨f2â© â f1 â f2.
cases f1 -f1 #p1 #f1 cases f2 -f2 #p2 #f2
cases tr_inj_unfold cases tr_inj_unfold #H
cases (pr_eq_inv_nexts_push_bi ⦠H) -H #H1 #H2
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 2b655f20c..528c13cf4 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -60,7 +60,7 @@ table {
[ "pr_nexts ( â*[?]? )" "pr_nexts_eq" * ]
[ "pr_pushs ( ⫯*[?]? )" "pr_pushs_eq" * ]
[ "pr_tl ( â«°? )" "pr_tl_eq" "pr_tl_eq_eq" * ]
- [ "pr_eq ( ? â¡ ? )" * ]
+ [ "pr_eq ( ? â ? )" * ]
[ "pr_map ( ⫯? ) ( â? )" * ]
}
]
@@ -143,7 +143,7 @@ table {
[ { "" * } {
[ "bool ( â» ) ( â )" "bool_or" "bool_and" * ]
[ "ltc" "ltc_ctc" * ]
- [ "logic ( ⥠) ( ⤠)" "relations ( ? â ? )" "functions" "exteq ( ? â{?,?} ? )" "star" "lstar_2a" * ]
+ [ "logic ( ⥠) ( ⤠)" "relations ( ? â ? )" "functions" "exteq ( ? â{?,?} ? )" "star" "lstar_2a" * ]
}
]
}
diff --git a/matita/matita/contribs/lambdadelta/static_2/notation/relations/ideq_2.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/ideq_2.ma
new file mode 100644
index 000000000..ae7999266
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/notation/relations/ideq_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( f1 â¡ break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'IdEq $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma
index 6b4a58e82..be5f31895 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma
@@ -12,7 +12,7 @@
(* *)
(**************************************************************************)
-include "ground/notation/relations/ideq_2.ma".
+include "static_2/notation/relations/ideq_2.ma".
include "static_2/syntax/teqg.ma".
(* SYNTACTIC EQUIVALENCE ON TERMS *******************************************)
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 4dd5b0f5e..94f34fb10 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1512,7 +1512,7 @@ let predefined_classes = [
["#"; "â¯"; "â"; "⧣"; "⧤"; "â"; ];
["+"; "â¨"; "⨮"; "â¨"; "â"; "â"; ];
["-"; "÷"; "â¢"; "â©"; "â§"; "â"; ];
- ["="; "â"; "â¡"; "â"; "â"; "â"; "â"; "â"; "â"; "â"; "â"; "⧦"; "â"; "â"; "⩳"; "â
"; "⩬"; "â"; "â"; "â"; ];
+ ["="; "â"; "â¡"; "â"; "â"; "â"; "â"; "â"; "â"; "â"; "â"; "â"; "⧦"; "â"; "⩳"; "â
"; "⩬"; "â"; "â"; "â"; ];
["â"; "⥲"; "â¦"; "â"; "â¤"; "â¾"; "â¤"; "â¤"; "⤳"; ] ;
["â"; "â¤"; "â¾"; "â¨"; "â¬"; "â¡"; "â¬"; "â¤"; "â¸"; "â"; "⥰"; ] ;
["^"; "â"; "â¡"; "â¥"; "âµ"; ] ;