(* Properties with extensional equivalence **********************************)
-lemma mf_gc_id: â\88\80j. â\87¡[j]mf_gi â\89\90 mf_gi.
+lemma mf_gc_id: â\88\80j. â\87¡[j]mf_gi â\8a\9c mf_gi.
// qed.
lemma mf_vlift_comp (l): compatible_2 … (mf_vlift l) (exteq …) (exteq …).
(* Main properties with extensional equivalence *****************************)
-theorem mf_vlift_swap: â\88\80l1,l2. l2 â\89¤ l1 â\86\92 â\88\80v. â\87¡[l2]â\87¡[l1]v â\89\90 ⇡[↑l1]⇡[l2]v.
+theorem mf_vlift_swap: â\88\80l1,l2. l2 â\89¤ l1 â\86\92 â\88\80v. â\87¡[l2]â\87¡[l1]v â\8a\9c ⇡[↑l1]⇡[l2]v.
/2 width=1 by flifts_basic_swap/ qed-.
(* Properties with extensional equivalence **********************************)
-lemma mf_lc_id: â\87¡[0â\86\90#0]mf_li â\89\90 mf_li.
+lemma mf_lc_id: â\87¡[0â\86\90#0]mf_li â\8a\9c mf_li.
#i elim (eq_or_gt i) #Hi destruct //
>mf_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
qed.
(* Main properties with extensional equivalence *****************************)
theorem mf_vpush_swap: ∀l1,l2. l2 ≤ l1 →
- â\88\80v,T1,T2. â\87¡[l2â\86\90T2]â\87¡[l1â\86\90T1]v â\89\90 ⇡[↑l1←↑[l2,1]T1]⇡[l2←T2]v.
+ â\88\80v,T1,T2. â\87¡[l2â\86\90T2]â\87¡[l1â\86\90T1]v â\8a\9c ⇡[↑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
(* Properties with multiple filling lift ************************************)
-lemma mf_vpush_vlift_swap_O (v) (T) (l): â\87¡[0â\86\90â\86\91[â\86\91l,1]T]â\87¡[l]v â\89\90⇡[↑l]⇡[0←T]v.
+lemma mf_vpush_vlift_swap_O (v) (T) (l): â\87¡[0â\86\90â\86\91[â\86\91l,1]T]â\87¡[l]v â\8a\9c⇡[↑l]⇡[0←T]v.
#v #T #l #i
elim (eq_or_gt i) #Hi destruct
[ >mf_vpush_eq >mf_vlift_rw >mf_vpush_eq //
]
qed.
-lemma mf_vpush_vlift_swap_O_lref_O (v) (l): â\87¡[0â\86\90#0]â\87¡[l]v â\89\90⇡[↑l]⇡[0←#0]v.
+lemma mf_vpush_vlift_swap_O_lref_O (v) (l): â\87¡[0â\86\90#0]â\87¡[l]v â\8a\9c⇡[↑l]⇡[0←#0]v.
#v #l @(mf_vpush_vlift_swap_O … (#0))
qed.
(* Properties with push for model evaluation ********************************)
-lemma tm_vpush_vlift_join_O (h) (v) (T): â\87¡[0]⫯{TM h}[0â\86\90T]v â\89\90 ⇡[0←↑[1]T]v.
+lemma tm_vpush_vlift_join_O (h) (v) (T): â\87¡[0]⫯{TM h}[0â\86\90T]v â\8a\9c ⇡[0←↑[1]T]v.
#h #v #T #i
elim (eq_or_gt i) #Hi destruct
[ >mf_vpush_eq >mf_vlift_rw >vpush_eq //
lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
// qed.
-lemma niter_inj (A) (f) (p): f^p â\89\90 f^{A}(ninj p).
+lemma niter_inj (A) (f) (p): f^p â\8a\9c f^{A}(ninj p).
// qed.
(* Advanced constructions ***************************************************)
(*** iter_n_Sm *)
-lemma niter_appl (A) (f) (n): f â\88\98 f^n â\89\90 f^{A}n ∘ f.
+lemma niter_appl (A) (f) (n): f â\88\98 f^n â\8a\9c 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 â\88\98 f â\89\90 g â\88\98 h â\86\92 h â\88\98 (f^{A}n) â\89\90 (g^{B}n) ∘ h.
+ h â\88\98 f â\8a\9c g â\88\98 h â\86\92 h â\88\98 (f^{A}n) â\8a\9c (g^{B}n) ∘ h.
#A #B #f #g #h * //
#p #H @exteq_repl
/2 width=5 by piter_compose, compose_repl_fwd_dx/
(*** iter_plus *)
lemma niter_plus (A) (f) (n1) (n2):
- f^n2 â\88\98 f^n1 â\89\90 f^{A}(n1+n2).
+ f^n2 â\88\98 f^n1 â\8a\9c f^{A}(n1+n2).
#A #f #n1 #n2 @(nat_ind_succ … n2) -n2 //
#n2 #IH <nplus_succ_dx
@exteq_repl
(* Constructions with niter *************************************************)
(*** iter_S *)
-lemma niter_succ (A) (f) (n): f â\88\98 f^n â\89\90 f^{A}(↑n).
+lemma niter_succ (A) (f) (n): f â\88\98 f^n â\8a\9c f^{A}(↑n).
#A #f * //
qed.
(* Basic constructions ******************************************************)
-lemma piter_unit (A) (f): f â\89\90 f^{A}𝟏.
+lemma piter_unit (A) (f): f â\8a\9c f^{A}𝟏.
// qed.
-lemma piter_succ (A) (f) (p): f â\88\98 f^p â\89\90 f^{A}(↑p).
+lemma piter_succ (A) (f) (p): f â\88\98 f^p â\8a\9c f^{A}(↑p).
// qed.
(* Advanced constructions ***************************************************)
-lemma piter_appl (A) (f) (p): f â\88\98 f^p â\89\90 f^{A}p ∘ f.
+lemma piter_appl (A) (f) (p): f â\88\98 f^p â\8a\9c 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 â\88\98 f â\89\90 g â\88\98 h â\86\92 h â\88\98 (f^{A}p) â\89\90 (g^{B}p) ∘ h.
+ h â\88\98 f â\8a\9c g â\88\98 h â\86\92 h â\88\98 (f^{A}p) â\8a\9c (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/
(* *)
(**************************************************************************)
-include "ground/notation/relations/doteq_4.ma".
+include "ground/notation/relations/circled_eq_4.ma".
include "ground/lib/relations.ma".
(* EXTENSIONAL EQUIVALENCE FOR FUNCTIONS ************************************)
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 ******************************************************)
(* Constructions with compose ***********************************************)
lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):
- f1 â\89\90{A,B} f2 â\86\92 g â\88\98 f1 â\89\90{A,C} g ∘ f2.
+ f1 â\8a\9c{A,B} f2 â\86\92 g â\88\98 f1 â\8a\9c{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 â\89\90{A,B} f2 â\86\92 g â\88\98 f2 â\89\90{A,C} g ∘ f1.
+ f1 â\8a\9c{A,B} f2 â\86\92 g â\88\98 f2 â\8a\9c{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 â\89\90{B,C} g2 â\86\92 g1 â\88\98 f â\89\90{A,C} g2 ∘ f.
+ g1 â\8a\9c{B,C} g2 â\86\92 g1 â\88\98 f â\8a\9c{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 â\89\90{B,C} g2 â\86\92 g2 â\88\98 f â\89\90{A,C} g1 ∘ f.
+ g1 â\8a\9c{B,C} g2 â\86\92 g2 â\88\98 f â\8a\9c{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 â\88\98 (f2 â\88\98 f1) â\89\90 f3 ∘ f2 ∘ f1.
+ f3 â\88\98 (f2 â\88\98 f1) â\8a\9c f3 ∘ f2 ∘ f1.
// qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
(* *)
(**************************************************************************)
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
(* GROUND NOTATION **********************************************************)
notation < "hvbox( a ϵ break term 46 u )"
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
(*** after_mono *)
corec theorem pr_after_mono:
- â\88\80f1,f2,x,y. f1 â\8a\9a f2 â\89\98 x â\86\92 f1 â\8a\9a f2 â\89\98 y â\86\92 x â\89¡ y.
+ â\88\80f1,f2,x,y. f1 â\8a\9a f2 â\89\98 x â\86\92 f1 â\8a\9a f2 â\89\98 y â\86\92 x â\89\90 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/
(*** after_mono_eq *)
lemma pr_after_mono_eq:
∀f1,f2,f. f1 ⊚ f2 ≘ f → ∀g1,g2,g. g1 ⊚ g2 ≘ g →
- f1 â\89¡ g1 â\86\92 f2 â\89¡ g2 â\86\92 f â\89¡ g.
+ f1 â\89\90 g1 â\86\92 f2 â\89\90 g2 â\86\92 f â\89\90 g.
/4 width=4 by pr_after_mono, pr_after_eq_repl_back_dx, pr_after_eq_repl_back_sn/ qed-.
(*** H_after_inj *)
definition H_pr_after_inj: predicate pr_map ≝
λf1. 𝐓❨f1❩ →
- â\88\80f,f21,f22. f1 â\8a\9a f21 â\89\98 f â\86\92 f1 â\8a\9a f22 â\89\98 f â\86\92 f21 â\89¡ f22.
+ â\88\80f,f21,f22. f1 â\8a\9a f21 â\89\98 f â\86\92 f1 â\8a\9a f22 â\89\98 f â\86\92 f21 â\89\90 f22.
(* Main destructions with pr_ist ********************************************)
(*** after_isid_inv_sn *)
lemma pr_after_isi_inv_sn:
- â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89¡ f.
+ â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89\90 f.
/3 width=6 by pr_after_isi_sn, pr_after_mono/ qed-.
(*** after_isid_inv_dx *)
lemma pr_after_isi_inv_dx:
- â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 f1 â\89¡ f.
+ â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 f1 â\89\90 f.
/3 width=6 by pr_after_isi_dx, pr_after_mono/ qed-.
(*** after_fwd_isid1 *)
(*** after_fwd_isid_sn *)
lemma pr_after_des_ist_eq_sn:
- â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f1 â\89¡ f → 𝐈❨f2❩.
+ â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f1 â\89\90 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
(*** after_fwd_isid_dx *)
lemma pr_after_des_ist_eq_dx:
- â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\89¡ f → 𝐈❨f1❩.
+ â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\89\90 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
(*** coafter_mono *)
corec theorem pr_coafter_mono:
- â\88\80f1,f2,x,y. f1 ~â\8a\9a f2 â\89\98 x â\86\92 f1 ~â\8a\9a f2 â\89\98 y â\86\92 x â\89¡ y.
+ â\88\80f1,f2,x,y. f1 ~â\8a\9a f2 â\89\98 x â\86\92 f1 ~â\8a\9a f2 â\89\98 y â\86\92 x â\89\90 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/
(*** coafter_mono_eq *)
lemma pr_coafter_mono_eq:
∀f1,f2,f. f1 ~⊚ f2 ≘ f → ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
- f1 â\89¡ g1 â\86\92 f2 â\89¡ g2 â\86\92 f â\89¡ g.
+ f1 â\89\90 g1 â\86\92 f2 â\89\90 g2 â\86\92 f â\89\90 g.
/4 width=4 by pr_coafter_mono, pr_coafter_eq_repl_back_dx, pr_coafter_eq_repl_back_sn/ qed-.
(*** H_coafter_inj *)
definition H_pr_coafter_inj: predicate pr_map ≝
λf1. 𝐓❨f1❩ →
- â\88\80f,f21,f22. f1 ~â\8a\9a f21 â\89\98 f â\86\92 f1 ~â\8a\9a f22 â\89\98 f â\86\92 f21 â\89¡ f22.
+ â\88\80f,f21,f22. f1 ~â\8a\9a f21 â\89\98 f â\86\92 f1 ~â\8a\9a f22 â\89\98 f â\86\92 f21 â\89\90 f22.
(* Main destructions with pr_ist ********************************************)
(*** coafter_isid_inv_sn *)
lemma pr_coafter_isi_inv_sn:
- â\88\80f1,f2,f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89¡ f.
+ â\88\80f1,f2,f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89\90 f.
/3 width=6 by pr_coafter_isi_sn, pr_coafter_mono/ qed-.
(*** coafter_isid_inv_dx *)
(* Main inversions **********************************************************)
(*** after_inv_total *)
-lemma pr_after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89¡ f.
+lemma pr_after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89\90 f.
/2 width=4 by pr_after_mono/ qed-.
(**************************************************************************)
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".
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 …) ≝
- â\88\80f1,f2. f1 â\89¡ f2 → R f1 f2.
+ â\88\80f1,f2. f1 â\89\90 f2 → R f1 f2.
(*** eq_repl_back *)
definition pr_eq_repl_back (R:predicate …) ≝
- â\88\80f1. R f1 â\86\92 â\88\80f2. f1 â\89¡ f2 → R f2.
+ â\88\80f1. R f1 â\86\92 â\88\80f2. f1 â\89\90 f2 → R f2.
(*** eq_repl_fwd *)
definition pr_eq_repl_fwd (R:predicate …) ≝
- â\88\80f1. R f1 â\86\92 â\88\80f2. f2 â\89¡ f1 → R f2.
+ â\88\80f1. R f1 â\86\92 â\88\80f2. f2 â\89\90 f1 → R f2.
(* Basic constructions ******************************************************)
(* Constructions with pr_eq *************************************************)
-corec lemma pr_id_eq (f): ⫯f â\89¡ f â\86\92 ð\9d\90¢ â\89¡ f.
+corec lemma pr_id_eq (f): ⫯f â\89\90 f â\86\92 ð\9d\90¢ â\89\90 f.
cases pr_id_unfold #Hf
cases (pr_eq_inv_push_sn … Hf) [|*: // ] #_ #H
cases H in Hf; -H #Hf
(* Inversions with pr_eq ****************************************************)
(* Note: this has the same proof of the previous *)
-corec lemma pr_id_inv_eq (f): ð\9d\90¢ â\89¡ f â\86\92 ⫯f â\89¡ f.
+corec lemma pr_id_inv_eq (f): ð\9d\90¢ â\89\90 f â\86\92 ⫯f â\89\90 f.
cases pr_id_unfold #Hf
cases (pr_eq_inv_push_sn … Hf) [|*: // ] #_ #H
cases H in Hf; -H #Hf
(* Main inversions with pr_eq ***********************************************)
(*** isdiv_inv_eq_repl *)
-corec theorem pr_isd_inv_eq_repl (g1) (g2): ð\9d\9b\80â\9d¨g1â\9d© â\86\92 ð\9d\9b\80â\9d¨g2â\9d© â\86\92 g1 â\89¡ g2.
+corec theorem pr_isd_inv_eq_repl (g1) (g2): ð\9d\9b\80â\9d¨g1â\9d© â\86\92 ð\9d\9b\80â\9d¨g2â\9d© â\86\92 g1 â\89\90 g2.
#H1 #H2
cases (pr_isd_inv_gen … H1) -H1
cases (pr_isd_inv_gen … H2) -H2
(* Alternative definition with pr_eq ****************************************)
(*** eq_next_isdiv *)
-corec lemma pr_eq_next_isd (f): â\86\91f â\89¡ f → 𝛀❨f❩.
+corec lemma pr_eq_next_isd (f): â\86\91f â\89\90 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): ð\9d\9b\80â\9d¨gâ\9d© â\86\92 â\86\91g â\89¡ g.
+corec lemma pr_eq_next_inv_isd (g): ð\9d\9b\80â\9d¨gâ\9d© â\86\92 â\86\91g â\89\90 g.
* -g #f #g #Hf *
/3 width=5 by pr_eq_next/
qed-.
(* Main inversions with pr_eq ***********************************************)
(*** isid_inv_eq_repl *)
-corec theorem pr_isi_inv_eq_repl (g1) (g2): ð\9d\90\88â\9d¨g1â\9d© â\86\92 ð\9d\90\88â\9d¨g2â\9d© â\86\92 g1 â\89¡ g2.
+corec theorem pr_isi_inv_eq_repl (g1) (g2): ð\9d\90\88â\9d¨g1â\9d© â\86\92 ð\9d\90\88â\9d¨g2â\9d© â\86\92 g1 â\89\90 g2.
#H1 #H2
cases (pr_isi_inv_gen … H1) -H1
cases (pr_isi_inv_gen … H2) -H2
(* Alternative definition with pr_eq ****************************************)
(*** eq_push_isid *)
-corec lemma pr_eq_push_isi (f): ⫯f â\89¡ f → 𝐈❨f❩.
+corec lemma pr_eq_push_isi (f): ⫯f â\89\90 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): ð\9d\90\88â\9d¨gâ\9d© â\86\92 ⫯g â\89¡ g.
+corec lemma pr_isi_inv_eq_push (g): ð\9d\90\88â\9d¨gâ\9d© â\86\92 ⫯g â\89\90 g.
* -g #f #g #Hf *
/3 width=5 by pr_eq_push/
qed-.
(* Alternative definition with pr_id and pr_eq ******************************)
(*** eq_id_isid *)
-lemma pr_eq_id_isi (f): ð\9d\90¢ â\89¡ f → 𝐈❨f❩.
+lemma pr_eq_id_isi (f): ð\9d\90¢ â\89\90 f → 𝐈❨f❩.
/2 width=3 by pr_isi_eq_repl_back/ qed.
(*** eq_id_inv_isid *)
-lemma pr_isi_inv_eq_id (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90¢ â\89¡ f.
+lemma pr_isi_inv_eq_id (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90¢ â\89\90 f.
/2 width=1 by pr_isi_inv_eq_repl/ qed-.
(* Constructions with pr_isi ************************************************)
(*** uni_inv_isid uni_isi *)
-lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f → 𝐈❨f❩.
+lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89\90 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): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f.
+lemma pr_isi_inv_uni (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89\90 f.
/2 width=1 by pr_isi_inv_eq_id/ 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 â\89¡ f2.
+ f1 â\89\90 f2.
cases (pr_map_split_tl f1) #H1
cases (pr_map_split_tl f2) #H2
#Hf1 #Hf2 #Hi
(* Inversions with pr_uni ***************************************************)
(*** uni_isuni *)
-lemma pr_isu_inv_uni (f): ð\9d\90\94â\9d¨fâ\9d© â\86\92 â\88\83n. ð\9d\90®â\9d¨nâ\9d© â\89¡ f.
+lemma pr_isu_inv_uni (f): ð\9d\90\94â\9d¨fâ\9d© â\86\92 â\88\83n. ð\9d\90®â\9d¨nâ\9d© â\89\90 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/
(*** nexts_eq_repl *)
lemma pr_nexts_eq_repl (n):
- pr_eq_repl (λf1,f2. â\86\91*[n] f1 â\89¡ ↑*[n] f2).
+ pr_eq_repl (λf1,f2. â\86\91*[n] f1 â\89\90 ↑*[n] f2).
#n @(nat_ind_succ … n) -n
/3 width=5 by pr_eq_next/
qed.
(* Inversions with pr_eq ****************************************************)
lemma pr_eq_inv_nexts_push_bi (f1) (f2) (n1) (n2):
- â\86\91*[n1] ⫯f1 â\89¡ ↑*[n2] ⫯f2 →
- â\88§â\88§ n1 = n2 & f1 â\89¡ f2.
+ â\86\91*[n1] ⫯f1 â\89\90 ↑*[n2] ⫯f2 →
+ â\88§â\88§ n1 = n2 & f1 â\89\90 f2.
#f1 #f2
#n1 @(nat_ind_succ … n1) -n1 [| #n1 #IH ]
#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]
#i1 #i2 @pr_eq_repl_sym /2 width=3 by pr_pat_eq_repl_back/
qed-.
-lemma pr_pat_eq (f): ⫯f â\89¡ f → ∀i. @❨i,f❩ ≘ i.
+lemma pr_pat_eq (f): ⫯f â\89\90 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/
(* Inversions with pr_eq ****************************************************)
corec lemma pr_pat_inv_eq (f):
- (â\88\80i. @â\9d¨i,fâ\9d© â\89\98 i) â\86\92 ⫯f â\89¡ f.
+ (â\88\80i. @â\9d¨i,fâ\9d© â\89\98 i) â\86\92 ⫯f â\89\90 f.
#Hf
lapply (Hf (𝟏)) #H
lapply (pr_pat_des_id … H) -H #H
(*** id_inv_at *)
lemma pr_pat_inv_id (f):
- (â\88\80i. @â\9d¨i,fâ\9d© â\89\98 i) â\86\92 ð\9d\90¢ â\89¡ f.
+ (â\88\80i. @â\9d¨i,fâ\9d© â\89\98 i) â\86\92 ð\9d\90¢ â\89\90 f.
/3 width=1 by pr_pat_inv_eq, pr_id_eq/
qed-.
(* Note: this requires ↑ on third n2 *)
(*** at_tls *)
-lemma pr_pat_tls (n2) (f): ⫯⫰*[â\86\91n2]f â\89¡ ⫰*[n2]f → ∃i1. @❨i1,f❩ ≘ ↑n2.
+lemma pr_pat_tls (n2) (f): ⫯⫰*[â\86\91n2]f â\89\90 ⫰*[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
(* Note: this requires ↑ on first n2 *)
(*** at_inv_tls *)
lemma pr_pat_inv_succ_dx_tls (n2) (i1) (f):
- @â\9d¨i1,fâ\9d© â\89\98 â\86\91n2 â\86\92 ⫯⫰*[â\86\91n2]f â\89¡ ⫰*[n2]f.
+ @â\9d¨i1,fâ\9d© â\89\98 â\86\91n2 â\86\92 ⫯⫰*[â\86\91n2]f â\89\90 ⫰*[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/
(*** pushs_eq_repl *)
lemma pr_pushs_eq_repl (n):
- pr_eq_repl (λf1,f2. ⫯*[n] f1 â\89¡ ⫯*[n] f2).
+ pr_eq_repl (λf1,f2. ⫯*[n] f1 â\89\90 ⫯*[n] f2).
#n @(nat_ind_succ … n) -n
/3 width=5 by pr_eq_push/
qed-.
(*** sle_refl_eq *)
lemma pr_sle_refl_eq:
- â\88\80f1,f2. f1 â\89¡ f2 → f1 ⊆ f2.
+ â\88\80f1,f2. f1 â\89\90 f2 → f1 ⊆ f2.
/2 width=3 by pr_sle_eq_repl_back_dx/ qed.
(*** sor_isid_inv_sn *)
lemma pr_sor_inv_isi_sn:
- â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89¡ f.
+ â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89\90 f.
/3 width=4 by pr_sor_isi_sn, pr_sor_mono/
qed-.
(*** sor_isid_inv_dx *)
lemma pr_sor_inv_isi_dx:
- â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 f1 â\89¡ f.
+ â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 f1 â\89\90 f.
/3 width=4 by pr_sor_isi_dx, pr_sor_mono/
qed-.
(*** sor_mono *)
corec theorem pr_sor_mono:
- â\88\80f1,f2,x,y. f1 â\8b\93 f2 â\89\98 x â\86\92 f1 â\8b\93 f2 â\89\98 y â\86\92 x â\89¡ y.
+ â\88\80f1,f2,x,y. f1 â\8b\93 f2 â\89\98 x â\86\92 f1 â\8b\93 f2 â\89\98 y â\86\92 x â\89\90 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)
(*** tl_eq_repl *)
lemma pr_tl_eq_repl:
- pr_eq_repl â\80¦ (λf1,f2. â«°f1 â\89¡ ⫰f2).
+ pr_eq_repl â\80¦ (λf1,f2. â«°f1 â\89\90 ⫰f2).
#f1 #f2 * -f1 -f2 //
qed.
(*** eq_inv_gen *)
lemma pr_eq_inv_gen (g1) (g2):
- g1 â\89¡ g2 →
- â\88¨â\88¨ â\88§â\88§ â«°g1 â\89¡ ⫰g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
- | â\88§â\88§ â«°g1 â\89¡ ⫰g2 & ↑⫰g1 = g1 & ↑⫰g2 = g2.
+ g1 â\89\90 g2 →
+ â\88¨â\88¨ â\88§â\88§ â«°g1 â\89\90 ⫰g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
+ | â\88§â\88§ â«°g1 â\89\90 ⫰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-.
(*** pr_eq_inv_px *)
lemma pr_eq_inv_push_sn (g1) (g2):
- g1 â\89¡ g2 → ∀f1. ⫯f1 = g1 →
- â\88§â\88§ f1 â\89¡ ⫰g2 & ⫯⫰g2 = g2.
+ g1 â\89\90 g2 → ∀f1. ⫯f1 = g1 →
+ â\88§â\88§ f1 â\89\90 ⫰g2 & ⫯⫰g2 = g2.
#g1 #g2 #H #f1 #Hf1
elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
[ /2 width=1 by conj/
(*** pr_eq_inv_nx *)
lemma pr_eq_inv_next_sn (g1) (g2):
- g1 â\89¡ g2 → ∀f1. ↑f1 = g1 →
- â\88§â\88§ f1 â\89¡ ⫰g2 & ↑⫰g2 = g2.
+ g1 â\89\90 g2 → ∀f1. ↑f1 = g1 →
+ â\88§â\88§ f1 â\89\90 ⫰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)
(*** pr_eq_inv_xp *)
lemma pr_eq_inv_push_dx (g1) (g2):
- g1 â\89¡ g2 → ∀f2. ⫯f2 = g2 →
- â\88§â\88§ â«°g1 â\89¡ f2 & ⫯⫰g1 = g1.
+ g1 â\89\90 g2 → ∀f2. ⫯f2 = g2 →
+ â\88§â\88§ â«°g1 â\89\90 f2 & ⫯⫰g1 = g1.
#g1 #g2 #H #f2 #Hf2
elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
[ /2 width=1 by conj/
(*** pr_eq_inv_xn *)
lemma pr_eq_inv_next_dx (g1) (g2):
- g1 â\89¡ g2 → ∀f2. ↑f2 = g2 →
- â\88§â\88§ â«°g1 â\89¡ f2 & ↑⫰g1 = g1.
+ g1 â\89\90 g2 → ∀f2. ↑f2 = g2 →
+ â\88§â\88§ â«°g1 â\89\90 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)
(*** pr_eq_inv_pp *)
lemma pr_eq_inv_push_bi (g1) (g2):
- g1 â\89¡ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 ⫯f2 = g2 â\86\92 f1 â\89¡ f2.
+ g1 â\89\90 g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 ⫯f2 = g2 â\86\92 f1 â\89\90 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 //
(*** pr_eq_inv_nn *)
lemma pr_eq_inv_next_bi (g1) (g2):
- g1 â\89¡ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 â\86\92 f1 â\89¡ f2.
+ g1 â\89\90 g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 â\86\92 f1 â\89\90 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 //
(*** pr_eq_inv_pn *)
lemma pr_eq_inv_push_next (g1) (g2):
- g1 â\89¡ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
+ g1 â\89\90 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)
(*** pr_eq_inv_np *)
lemma pr_eq_inv_next_push (g1) (g2):
- g1 â\89¡ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
+ g1 â\89\90 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)
qed-.
(*** eq_canc_sn *)
-theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f â\89¡ f2).
+theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f â\89\90 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 â\89¡ f).
+theorem pr_eq_canc_dx (f1): pr_eq_repl_fwd (λf. f1 â\89\90 f).
/3 width=5 by pr_eq_canc_sn, pr_eq_repl_sym/ qed-.
(*** tls_eq_repl *)
lemma pr_tls_eq_repl (n):
- pr_eq_repl (λf1,f2. â«°*[n] f1 â\89¡ ⫰*[n] f2).
+ pr_eq_repl (λf1,f2. â«°*[n] f1 â\89\90 ⫰*[n] f2).
#n @(nat_ind_succ … n) -n /3 width=1 by pr_tl_eq_repl/
qed.
(*** eq_inv_nexts_sn *)
lemma pr_eq_inv_nexts_sn (n):
- â\88\80f1,g2. â\86\91*[n] f1 â\89¡ g2 →
- â\88§â\88§ f1 â\89¡ ⫰*[n]g2 & ↑*[n]⫰*[n]g2 = g2.
+ â\88\80f1,g2. â\86\91*[n] f1 â\89\90 g2 →
+ â\88§â\88§ f1 â\89\90 ⫰*[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 *
(*** eq_inv_nexts_dx *)
lemma pr_eq_inv_nexts_dx (n):
- â\88\80f2,g1. g1 â\89¡ ↑*[n] f2 →
- â\88§â\88§ â«°*[n]g1 â\89¡ f2 & ↑*[n]⫰*[n]g1 = g1.
+ â\88\80f2,g1. g1 â\89\90 ↑*[n] f2 →
+ â\88§â\88§ â«°*[n]g1 â\89\90 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 *
(*** eq_inv_pushs_sn *)
lemma pr_eq_inv_pushs_sn (n):
- â\88\80f1,g2. ⫯*[n] f1 â\89¡ g2 →
- â\88§â\88§ f1 â\89¡ ⫰*[n]g2 & ⫯*[n]⫰*[n]g2 = g2.
+ â\88\80f1,g2. ⫯*[n] f1 â\89\90 g2 →
+ â\88§â\88§ f1 â\89\90 ⫰*[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 *
(*** eq_inv_pushs_dx *)
lemma pr_eq_inv_pushs_dx (n):
- â\88\80f2,g1. g1 â\89¡ ⫯*[n] f2 →
- â\88§â\88§ â«°*[n]g1 â\89¡ f2 & ⫯*[n]⫰*[n]g1 = g1.
+ â\88\80f2,g1. g1 â\89\90 ⫯*[n] f2 →
+ â\88§â\88§ â«°*[n]g1 â\89\90 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 *
(* Inversions with pr_eq ****************************************************)
(*** uni_inv_push_dx *)
-lemma pr_eq_inv_uni_push (n) (g): ð\9d\90®â\9d¨nâ\9d© â\89¡ ⫯g â\86\92 â\88§â\88§ ð\9d\9f\8e = n & ð\9d\90¢ â\89¡ g.
+lemma pr_eq_inv_uni_push (n) (g): ð\9d\90®â\9d¨nâ\9d© â\89\90 ⫯g â\86\92 â\88§â\88§ ð\9d\9f\8e = n & ð\9d\90¢ â\89\90 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 //
qed-.
(*** uni_inv_push_sn *)
-lemma pr_eq_inv_push_uni (n) (g): ⫯g â\89¡ ð\9d\90®â\9d¨nâ\9d© â\86\92 â\88§â\88§ ð\9d\9f\8e = n & ð\9d\90¢ â\89¡ g.
+lemma pr_eq_inv_push_uni (n) (g): ⫯g â\89\90 ð\9d\90®â\9d¨nâ\9d© â\86\92 â\88§â\88§ ð\9d\9f\8e = n & ð\9d\90¢ â\89\90 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): ð\9d\90®â\9d¨nâ\9d© â\89¡ â\86\91g â\86\92 â\88§â\88§ ð\9d\90®â\9d¨â\86\93nâ\9d© â\89¡ g & ↑↓n = n.
+lemma pr_eq_inv_uni_next (n) (g): ð\9d\90®â\9d¨nâ\9d© â\89\90 â\86\91g â\86\92 â\88§â\88§ ð\9d\90®â\9d¨â\86\93nâ\9d© â\89\90 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/
qed-.
(*** uni_inv_next_sn *)
-lemma pr_eq_inv_next_uni (n) (g): â\86\91g â\89¡ ð\9d\90®â\9d¨nâ\9d© â\86\92 â\88§â\88§ ð\9d\90®â\9d¨â\86\93nâ\9d© â\89¡ g & ↑↓n = n.
+lemma pr_eq_inv_next_uni (n) (g): â\86\91g â\89\90 ð\9d\90®â\9d¨nâ\9d© â\86\92 â\88§â\88§ ð\9d\90®â\9d¨â\86\93nâ\9d© â\89\90 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): ð\9d\90®â\9d¨nâ\9d© â\89¡ 𝐢 → 𝟎 = n.
+lemma pr_eq_inv_uni_id (n): ð\9d\90®â\9d¨nâ\9d© â\89\90 𝐢 → 𝟎 = 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): ð\9d\90¢ â\89¡ 𝐮❨n❩ → 𝟎 = n.
+lemma pr_eq_inv_id_uni (n): ð\9d\90¢ â\89\90 𝐮❨n❩ → 𝟎 = n.
/3 width=1 by pr_eq_inv_uni_id, pr_eq_sym/ qed-.
]
qed-.
-lemma after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89¡ f.
+lemma after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89\90 f.
/2 width=4 by gr_after_mono/ qed-.
(* Forward lemmas on after (specific) *****************************************)
(* Constructions with pr_eq and stream_eq ***********************************)
-corec lemma eq_tr_inj_bi (f1) (f2): f1 â\89\97 f2 â\86\92 ð\9d\90â\9d¨f1â\9d© â\89¡ 𝐭❨f2❩.
+corec lemma eq_tr_inj_bi (f1) (f2): f1 â\89\97 f2 â\86\92 ð\9d\90â\9d¨f1â\9d© â\89\90 𝐭❨f2❩.
* -f1 -f2 #p1 #p2 #f1 #f2 * -p2 #H
cases p1 -p1
[ @pr_eq_push /2 width=5 by/
(* Inversions with pr_eq and stream_eq **************************************)
-corec lemma eq_inv_tr_inj_bi (f1) (f2): ð\9d\90â\9d¨f1â\9d© â\89¡ 𝐭❨f2❩ → f1 ≗ f2.
+corec lemma eq_inv_tr_inj_bi (f1) (f2): ð\9d\90â\9d¨f1â\9d© â\89\90 𝐭❨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
[ "pr_nexts ( ↑*[?]? )" "pr_nexts_eq" * ]
[ "pr_pushs ( ⫯*[?]? )" "pr_pushs_eq" * ]
[ "pr_tl ( ⫰? )" "pr_tl_eq" "pr_tl_eq_eq" * ]
- [ "pr_eq ( ? â\89¡ ? )" * ]
+ [ "pr_eq ( ? â\89\90 ? )" * ]
[ "pr_map ( ⫯? ) ( ↑? )" * ]
}
]
[ { "" * } {
[ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
[ "ltc" "ltc_ctc" * ]
- [ "logic ( â\8a¥ ) ( â\8a¤ )" "relations ( ? â\8a\86 ? )" "functions" "exteq ( ? â\89\90{?,?} ? )" "star" "lstar_2a" * ]
+ [ "logic ( â\8a¥ ) ( â\8a¤ )" "relations ( ? â\8a\86 ? )" "functions" "exteq ( ? â\8a\9c{?,?} ? )" "star" "lstar_2a" * ]
}
]
}
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
(* *)
(**************************************************************************)
-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 *******************************************)
["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ];
["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
- ["="; "â\89\9d"; "â\89¡"; "â\89\98"; "â\89\97"; "â\89\90"; "â\89\91"; "â\89\9b"; "â\89\9a"; "â\89\99"; "â\8c\86"; "⧦"; "â\8a\9c"; "â\89\8b"; "⩳"; "â\89\85"; "⩬"; "â\89\82"; "â\89\83"; "â\89\88"; ];
+ ["="; "â\89\9d"; "â\89¡"; "â\89\98"; "â\8a\9c"; "â\89\97"; "â\89\90"; "â\89\91"; "â\89\9b"; "â\89\9a"; "â\89\99"; "â\8c\86"; "⧦"; "â\89\8b"; "⩳"; "â\89\85"; "⩬"; "â\89\82"; "â\89\83"; "â\89\88"; ];
["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
["⇒"; "⤇"; "➾"; "⇨"; "⬀"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ;
["^"; "↑"; "⇡"; "↥"; "▵"; ] ;
projects / helm.git / commitdiff