class "italic" { 1 }
(*
[ { "evaluation drop" * } {
- [ "vdrop" + "( â«°{?}? )" + "( â«°{?}[?]? )" "vdrop_vlift" * ]
+ [ "vdrop" + "( â\87£{?}? )" + "( â\87£{?}[?]? )" "vdrop_vlift" * ]
}
]
[ { "reduction and type machine" * } {
(* *)
(**************************************************************************)
-include "ground/notation/functions/downspoon_2.ma".
+include "ground/notation/functions/downdashedarrow_2.ma".
include "ground/lib/stream.ma".
(* HEAD AND TAIL FOR STREAMS ************************************************)
interpretation
"tail (streams)"
- 'DownSpoon A t = (stream_tl A t).
+ 'DownDashedArrow A t = (stream_tl A t).
(* Basic constructions ******************************************************)
// qed.
lemma stream_tl_cons (A) (a) (t):
- t = â«°{A}(a⨮t).
+ t = â\87£{A}(a⨮t).
// qed.
lemma stream_split_tl (A) (t):
- stream_hd A t ⨮ ⫰t = t.
+ stream_hd A t ⨮ â\87£t = t.
#A * //
qed.
(* *)
(**************************************************************************)
-include "ground/notation/functions/downspoonstar_3.ma".
+include "ground/notation/functions/downdashedarrowstar_3.ma".
include "ground/lib/stream_hdtl.ma".
include "ground/arith/nat_succ_iter.ma".
interpretation
"iterated tail (strams)"
- 'DownSpoonStar A n f = (stream_tls A n f).
+ 'DownDashedArrowStar A n f = (stream_tls A n f).
(* Basic constructions ******************************************************)
lemma stream_tls_zero (A) (t):
- t = â«°*{A}[𝟎]t.
+ t = â\87£*{A}[𝟎]t.
// qed.
lemma stream_tls_tl (A) (n) (t):
- (â«°â«°*[n]t) = â«°*{A}[n]â«°t.
+ (â\87£â\87£*[n]t) = â\87£*{A}[n]â\87£t.
#A #n #t
@(niter_appl … (stream_tl …))
qed.
lemma stream_tls_succ (A) (n) (t):
- (â«°â«°*[n]t) = â«°*{A}[↑n]t.
+ (â\87£â\87£*[n]t) = â\87£*{A}[↑n]t.
#A #n #t
@(niter_succ … (stream_tl …))
qed.
lemma stream_tls_swap (A) (n) (t):
- (â«°*[n]â«°t) = â«°*{A}[↑n]t.
+ (â\87£*[n]â\87£t) = â\87£*{A}[↑n]t.
// qed.
(* Constructions with stream_eq *********************************************)
lemma stream_tls_eq_repl (A) (n):
- stream_eq_repl A (λt1,t2. â«°*[n] t1 â\89\97 â«°*[n] t2).
+ stream_eq_repl A (λt1,t2. â\87£*[n] t1 â\89\97 â\87£*[n] t2).
#A #n @(nat_ind_succ … n) -n //
#n #IH * #n1 #t1 * #n2 #t2 #H
elim (stream_eq_inv_cons_bi … H) /2 width=7 by/
--- /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 75 a )"
+ non associative with precedence 75
+ for @{ 'DownDashedArrow $S $a }.
+
+notation > "hvbox( ⇣ term 75 a )"
+ non associative with precedence 75
+ for @{ 'DownDashedArrow ? $a }.
+
+notation > "hvbox( ⇣{ term 46 S } break term 75 a )"
+ non associative with precedence 75
+ for @{ 'DownDashedArrow $S $a }.
--- /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( ⇣*[ break term 46 n ] break term 75 a )"
+ non associative with precedence 75
+ for @{ 'DownDashedArrowStar $S $n $a }.
+
+notation > "hvbox( ⇣*[ break term 46 n ] break term 75 a )"
+ non associative with precedence 75
+ for @{ 'DownDashedArrowStar ? $n $a }.
+
+notation > "hvbox( ⇣*{ term 46 S }[ break term 46 n ] break term 75 a )"
+ non associative with precedence 75
+ for @{ 'DownDashedArrowStar $S $n $a }.
--- /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 75 T )"
+ non associative with precedence 75
+ for @{ 'DownSpoon $T }.
+++ /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 75 a )"
- non associative with precedence 75
- for @{ 'DownSpoon $S $a }.
-
-notation > "hvbox( ⫰ term 75 a )"
- non associative with precedence 75
- for @{ 'DownSpoon ? $a }.
-
-notation > "hvbox( ⫰{ term 46 S } break term 75 a )"
- non associative with precedence 75
- for @{ 'DownSpoon $S $a }.
--- /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 n ] break term 75 T )"
+ non associative with precedence 75
+ for @{ 'DownSpoonStar $n $T }.
+++ /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( ⫰*[ break term 46 n ] break term 75 a )"
- non associative with precedence 75
- for @{ 'DownSpoonStar $S $n $a }.
-
-notation > "hvbox( ⫰*[ break term 46 n ] break term 75 a )"
- non associative with precedence 75
- for @{ 'DownSpoonStar ? $n $a }.
-
-notation > "hvbox( ⫰*{ term 46 S }[ break term 46 n ] break term 75 a )"
- non associative with precedence 75
- for @{ 'DownSpoonStar $S $n $a }.
+++ /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 75 T )"
- non associative with precedence 75
- for @{ 'DropPred $T }.
+++ /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 n ] break term 75 T )"
- non associative with precedence 75
- for @{ 'DropPreds $n $T }.
| cases (gr_after_inv_push_sn_next … H2f … H1 H) -f1 -f #g22 #H2g #H22
@(gr_eq_next … H21 H22) -f21 -f22
]
-@(gr_after_inj_unit_aux (⫱*[â\86\93p]g1) â\80¦ (⫱*[↓p]g)) -gr_after_inj_unit_aux
+@(gr_after_inj_unit_aux (â«°*[â\86\93p]g1) â\80¦ (â«°*[↓p]g)) -gr_after_inj_unit_aux
/2 width=1 by gr_after_tls_sn_tls, gr_ist_tls, gr_pat_unit_succ_tls/
qed-.
(*** after_uni_dx *)
lemma gr_after_nat_uni (l2) (l1):
∀f2. @↑❪l1, f2❫ ≘ l2 →
- â\88\80f. f2 â\8a\9a ð\9d\90®â\9d¨l1â\9d© â\89\98 f â\86\92 ð\9d\90®â\9d¨l2â\9d© â\8a\9a ⫱*[l2] f2 ≘ f.
+ â\88\80f. f2 â\8a\9a ð\9d\90®â\9d¨l1â\9d© â\89\98 f â\86\92 ð\9d\90®â\9d¨l2â\9d© â\8a\9a â«°*[l2] f2 ≘ f.
#l2 @(nat_ind_succ … l2) -l2
[ #l1 #f2 #Hf2 #f #Hf
elim (gr_nat_inv_zero_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
(*** after_uni_sn *)
lemma gr_nat_after_uni_tls (l2) (l1):
∀f2. @↑❪l1, f2❫ ≘ l2 →
- â\88\80f. ð\9d\90®â\9d¨l2â\9d© â\8a\9a ⫱*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
+ â\88\80f. ð\9d\90®â\9d¨l2â\9d© â\8a\9a â«°*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
#l2 @(nat_ind_succ … l2) -l2
[ #l1 #f2 #Hf2 #f #Hf
elim (gr_nat_inv_zero_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
(*** after_tls *)
lemma gr_after_tls_sn_tls (n):
∀f1,f2,f. @❪𝟏, f1❫ ≘ ↑n →
- f1 â\8a\9a f2 â\89\98 f â\86\92 ⫱*[n]f1 â\8a\9a f2 â\89\98 ⫱*[n]f.
+ f1 â\8a\9a f2 â\89\98 f â\86\92 â«°*[n]f1 â\8a\9a f2 â\89\98 â«°*[n]f.
#n @(nat_ind_succ … n) -n //
#n #IH #f1 #f2 #f #Hf1 #Hf
cases (gr_pat_inv_unit_succ … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
(*** after_uni_succ_dx *)
lemma gr_after_pat_uni (i2) (i1):
∀f2. @❪i1, f2❫ ≘ i2 →
- â\88\80f. f2 â\8a\9a ð\9d\90®â\9d¨i1â\9d© â\89\98 f â\86\92 ð\9d\90®â\9d¨i2â\9d© â\8a\9a ⫱*[i2] f2 ≘ f.
+ â\88\80f. f2 â\8a\9a ð\9d\90®â\9d¨i1â\9d© â\89\98 f â\86\92 ð\9d\90®â\9d¨i2â\9d© â\8a\9a â«°*[i2] f2 ≘ f.
#i2 elim i2 -i2
[ #i1 #f2 #Hf2 #f #Hf
elim (gr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
(*** after_uni_succ_sn *)
lemma gr_pat_after_uni_tls (i2) (i1):
∀f2. @❪i1, f2❫ ≘ i2 →
- â\88\80f. ð\9d\90®â\9d¨i2â\9d© â\8a\9a ⫱*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
+ â\88\80f. ð\9d\90®â\9d¨i2â\9d© â\8a\9a â«°*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
#i2 elim i2 -i2
[ #i1 #f2 #Hf2 #f #Hf
elim (gr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
(*** coafter_inv_tl1 *)
lemma gr_coafter_inv_tl_dx:
- â\88\80g2,g1,g. g2 ~â\8a\9a ⫱g1 ≘ g →
- â\88\83â\88\83f. ⫯g2 ~â\8a\9a g1 â\89\98 f & ⫱f = g.
+ â\88\80g2,g1,g. g2 ~â\8a\9a â«°g1 ≘ g →
+ â\88\83â\88\83f. ⫯g2 ~â\8a\9a g1 â\89\98 f & â«°f = g.
#g2 #g1 #g
elim (gr_map_split_tl g1) #H1 #H2
[ /3 width=7 by gr_coafter_refl, ex2_intro/
(*** coafter_inv_tl0 *)
lemma gr_coafter_inv_tl:
- â\88\80g2,g1,g. g2 ~â\8a\9a g1 â\89\98 ⫱g →
- â\88\83â\88\83f1. ⫯g2 ~â\8a\9a f1 â\89\98 g & ⫱f1 = g1.
+ â\88\80g2,g1,g. g2 ~â\8a\9a g1 â\89\98 â«°g →
+ â\88\83â\88\83f1. ⫯g2 ~â\8a\9a f1 â\89\98 g & â«°f1 = g1.
#g2 #g1 #g
elim (gr_map_split_tl g) #H1 #H2
[ /3 width=7 by gr_coafter_refl, ex2_intro/
| cases (gr_coafter_inv_push_sn_next … H2f … H1 H) -f1 -f #g22 #H2g #H22
@(gr_eq_next … H21 H22) -f21 -f22
]
-@(gr_coafter_inj_unit_aux (⫱*[â\86\93n]g1) â\80¦ (⫱*[↓n]g)) -gr_coafter_inj_unit_aux
+@(gr_coafter_inj_unit_aux (â«°*[â\86\93n]g1) â\80¦ (â«°*[↓n]g)) -gr_coafter_inj_unit_aux
/2 width=1 by gr_coafter_tls_bi_tls, gr_ist_tls, gr_pat_unit_succ_tls/
qed-.
(*** coafter_tls *)
lemma gr_coafter_tls_bi_tls (n2) (n1):
∀f1,f2,f. @↑❪n1, f1❫ ≘ n2 →
- f1 ~â\8a\9a f2 â\89\98 f â\86\92 ⫱*[n2]f1 ~â\8a\9a ⫱*[n1]f2 â\89\98 ⫱*[n2]f.
+ f1 ~â\8a\9a f2 â\89\98 f â\86\92 â«°*[n2]f1 ~â\8a\9a â«°*[n1]f2 â\89\98 â«°*[n2]f.
#n2 @(nat_ind_succ … n2) -n2 [ #n1 | #n2 #IH * [| #n1 ] ] #f1 #f2 #f #Hf1 #Hf
[ elim (gr_nat_inv_zero_dx … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 destruct //
| elim (gr_nat_inv_zero_succ … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
(*** coafter_tls_O *)
lemma gr_coafter_tls_sn_tls:
∀n,f1,f2,f. @↑❪𝟎, f1❫ ≘ n →
- f1 ~â\8a\9a f2 â\89\98 f â\86\92 ⫱*[n]f1 ~â\8a\9a f2 â\89\98 ⫱*[n]f.
+ f1 ~â\8a\9a f2 â\89\98 f â\86\92 â«°*[n]f1 ~â\8a\9a f2 â\89\98 â«°*[n]f.
/2 width=1 by gr_coafter_tls_bi_tls/ qed.
(*** coafter_fwd_pushs *)
lemma gr_coafter_des_pushs_dx (n) (m):
∀g2,f1,g. g2 ~⊚ ⫯*[m]f1 ≘ g → @↑❪m, g2❫ ≘ n →
- â\88\83â\88\83f. ⫱*[n]g2 ~⊚ f1 ≘ f & ⫯*[n] f = g.
+ â\88\83â\88\83f. â«°*[n]g2 ~⊚ f1 ≘ f & ⫯*[n] f = g.
#n @(nat_ind_succ … n) -n
[ #m #g2 #f1 #g #Hg #H
elim (gr_nat_inv_zero_dx … H) -H [|*: // ] #f2 #H1 #H2 destruct
(*** coafter_tls_succ *)
lemma gr_coafter_tls_tl_tls:
∀g2,g1,g. g2 ~⊚ g1 ≘ g →
- â\88\80j. @â\9dªð\9d\9f\8f, g2â\9d« â\89\98 j â\86\92 ⫱*[j]g2 ~â\8a\9a ⫱g1 â\89\98 ⫱*[j]g.
+ â\88\80j. @â\9dªð\9d\9f\8f, g2â\9d« â\89\98 j â\86\92 â«°*[j]g2 ~â\8a\9a â«°g1 â\89\98 â«°*[j]g.
#g2 #g1 #g #Hg #j #Hg2
lapply (gr_nat_pred_bi … Hg2) -Hg2 #Hg2
lapply (gr_coafter_tls_bi_tls … Hg2 … Hg) -Hg #Hg
(* Note: parked for now
lemma coafter_fwd_xpx_pushs:
∀g2,f1,g,i,j. @❪i, g2❫ ≘ j → g2 ~⊚ ⫯*[i]⫯f1 ≘ g →
- â\88\83â\88\83f. ⫱*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j]⫯f = g.
+ â\88\83â\88\83f. â«°*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j]⫯f = g.
#g2 #g1 #g #i #j #Hg2 <pushs_xn #Hg(coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs <tls_pushs #Hf
lapply (at_inv_tls … Hg2) -Hg2 #H
lemma coafter_fwd_xnx_pushs:
∀g2,f1,g,i,j. @❪i, g2❫ ≘ j → g2 ~⊚ ⫯*[i]↑f1 ≘ g →
- â\88\83â\88\83f. ⫱*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j] ↑f = g.
+ â\88\83â\88\83f. â«°*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j] ↑f = g.
#g2 #g1 #g #i #j #Hg2 #Hg
elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs <tls_pushs #Hf
(* Constructions with gr_tl *************************************************)
(*** isdiv_tl *)
-lemma gr_isd_tl (f): ð\9d\9b\80â\9dªfâ\9d« â\86\92 ð\9d\9b\80â\9dªâ«±f❫.
+lemma gr_isd_tl (f): ð\9d\9b\80â\9dªfâ\9d« â\86\92 ð\9d\9b\80â\9dªâ«°f❫.
#f cases (gr_map_split_tl f) * #H
[ elim (gr_isd_inv_push … H) -H //
| /2 width=3 by gr_isd_inv_next/
(* Constructions with gr_tls ************************************************)
(*** isdiv_tls *)
-lemma gr_isd_tls (n) (g): ð\9d\9b\80â\9dªgâ\9d« â\86\92 ð\9d\9b\80â\9dªâ«±*[n]g❫.
+lemma gr_isd_tls (n) (g): ð\9d\9b\80â\9dªgâ\9d« â\86\92 ð\9d\9b\80â\9dªâ«°*[n]g❫.
#n @(nat_ind_succ … n) -n /3 width=1 by gr_isd_tl/
qed.
(* Constructions with gr_tl *************************************************)
(*** isfin_tl *)
-lemma gr_isf_tl (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ«±f❫.
+lemma gr_isf_tl (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ«°f❫.
#f elim (gr_map_split_tl f) * #Hf
/3 width=3 by gr_isf_inv_push, gr_isf_inv_next/
qed.
(* Inversions with gr_tl ****************************************************)
(*** isfin_inv_tl *)
-lemma gr_isf_inv_tl (g): ð\9d\90\85â\9dªâ«±g❫ → 𝐅❪g❫.
+lemma gr_isf_inv_tl (g): ð\9d\90\85â\9dªâ«°g❫ → 𝐅❪g❫.
#f elim (gr_map_split_tl f) * #Hf
/2 width=1 by gr_isf_next, gr_isf_push/
qed-.
(* Constructions with gr_tls ************************************************)
-lemma gr_isf_tls (n) (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ«±*[n]f❫.
+lemma gr_isf_tls (n) (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ«°*[n]f❫.
#n @(nat_ind_succ … n) -n /3 width=1 by gr_isf_tl/
qed.
(* Inversions with gr_tls ***************************************************)
(*** isfin_inv_tls *)
-lemma gr_isf_inv_tls (n) (g): ð\9d\90\85â\9dªâ«±*[n]g❫ → 𝐅❪g❫.
+lemma gr_isf_inv_tls (n) (g): ð\9d\90\85â\9dªâ«°*[n]g❫ → 𝐅❪g❫.
#n @(nat_ind_succ … n) -n /3 width=1 by gr_isf_inv_tl/
qed-.
(* Constructions with gr_tl *************************************************)
(*** isid_tl *)
-lemma gr_isi_tl (f): ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\88â\9dªâ«±f❫.
+lemma gr_isi_tl (f): ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\88â\9dªâ«°f❫.
#f cases (gr_map_split_tl f) * #H
[ /2 width=3 by gr_isi_inv_push/
| elim (gr_isi_inv_next … H) -H //
(* Constructions with gr_tls ************************************************)
(*** isid_tls *)
-lemma gr_isi_tls (n) (f): ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\88â\9dªâ«±*[n]f❫.
+lemma gr_isi_tls (n) (f): ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\88â\9dªâ«°*[n]f❫.
#n @(nat_ind_succ … n) -n /3 width=1 by gr_isi_tl/
qed.
(* Constructions with gr_tl *************************************************)
(*** istot_tl *)
-lemma gr_ist_tl (f): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ«±f❫.
+lemma gr_ist_tl (f): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ«°f❫.
#f cases (gr_map_split_tl f) *
/2 width=3 by gr_ist_inv_next, gr_ist_inv_push/
qed.
(* Constructions with gr_tls ************************************************)
(*** istot_tls *)
-lemma gr_ist_tls (n) (f): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ«±*[n]f❫.
+lemma gr_ist_tls (n) (f): ð\9d\90\93â\9dªfâ\9d« â\86\92 ð\9d\90\93â\9dªâ«°*[n]f❫.
#n @(nat_ind_succ … n) -n //
#n #IH #f #Hf <gr_tls_succ
/3 width=1 by gr_ist_tl/
(* Constructions with gr_tl *************************************************)
-lemma gr_isu_tl (f): ð\9d\90\94â\9dªfâ\9d« â\86\92 ð\9d\90\94â\9dªâ«±f❫.
+lemma gr_isu_tl (f): ð\9d\90\94â\9dªfâ\9d« â\86\92 ð\9d\90\94â\9dªâ«°f❫.
#f cases (gr_map_split_tl f) * #H
[ /3 width=3 by gr_isu_inv_push, gr_isu_isi/
| /2 width=3 by gr_isu_inv_next/
qed-.
(*** at_fwd_id_ex *)
-lemma gr_pat_des_id (f) (i): @â\9dªi,fâ\9d« â\89\98 i â\86\92 ⫯⫱f = f.
+lemma gr_pat_des_id (f) (i): @â\9dªi,fâ\9d« â\89\98 i â\86\92 ⫯⫰f = f.
#f elim (gr_map_split_tl f) //
#H #i #Hf elim (gr_pat_inv_next … Hf … H) -Hf -H
#j2 #Hg #H destruct lapply (gr_pat_increasing … Hg) -Hg
(* Note: this requires ↑ on first n *)
(*** at_pxx_tls *)
lemma gr_pat_unit_succ_tls (n) (f):
- @â\9dªð\9d\9f\8f,fâ\9d« â\89\98 â\86\91n â\86\92 @â\9dªð\9d\9f\8f,⫱*[n]f❫ ≘ 𝟏.
+ @â\9dªð\9d\9f\8f,fâ\9d« â\89\98 â\86\91n â\86\92 @â\9dªð\9d\9f\8f,â«°*[n]f❫ ≘ 𝟏.
#n @(nat_ind_succ … n) -n //
#n #IH #f #Hf
elim (gr_pat_inv_unit_succ … Hf) -Hf [|*: // ] #g #Hg #H0 destruct
(* Note: this requires ↑ on third n2 *)
(*** at_tls *)
-lemma gr_pat_tls (n2) (f): ⫯⫱*[â\86\91n2]f â\89¡ ⫱*[n2]f → ∃i1. @❪i1,f❫ ≘ ↑n2.
+lemma gr_pat_tls (n2) (f): ⫯⫰*[â\86\91n2]f â\89¡ â«°*[n2]f → ∃i1. @❪i1,f❫ ≘ ↑n2.
#n2 @(nat_ind_succ … n2) -n2
[ /4 width=4 by gr_pat_eq_repl_back, gr_pat_refl, ex_intro/
| #n2 #IH #f <gr_tls_swap <gr_tls_swap in ⊢ (??%→?); #H
(*** at_inv_nxx *)
lemma gr_pat_inv_succ_sn (p) (g) (i1) (j2):
@❪↑i1,g❫ ≘ j2 → @❪𝟏,g❫ ≘ p →
- â\88\83â\88\83i2. @â\9dªi1,⫱*[p]g❫ ≘ i2 & p+i2 = j2.
+ â\88\83â\88\83i2. @â\9dªi1,â«°*[p]g❫ ≘ i2 & p+i2 = j2.
#p elim p -p
[ #g #i1 #j2 #Hg #H
elim (gr_pat_inv_unit_bi … H) -H [|*: // ] #f #H0
(* Note: this requires ↑ on first n2 *)
(*** at_inv_tls *)
lemma gr_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¡ â«°*[n2]f.
#n2 @(nat_ind_succ … n2) -n2
[ #i1 #f #Hf elim (gr_pat_inv_unit_dx … Hf) -Hf // #g #H1 #H destruct
/2 width=1 by gr_eq_refl/
(*** sle_px_tl *)
lemma gr_sle_push_sn_tl:
- â\88\80g1,g2. g1 â\8a\86 g2 â\86\92 â\88\80f1. ⫯f1 = g1 â\86\92 f1 â\8a\86 ⫱g2.
+ â\88\80g1,g2. g1 â\8a\86 g2 â\86\92 â\88\80f1. ⫯f1 = g1 â\86\92 f1 â\8a\86 â«°g2.
#g1 #g2 #H #f1 #H1
elim (gr_sle_inv_push_sn … H … H1) -H -H1 * //
qed.
(*** sle_xn_tl *)
lemma gr_sle_next_dx_tl:
- â\88\80g1,g2. g1 â\8a\86 g2 â\86\92 â\88\80f2. â\86\91f2 = g2 â\86\92 ⫱g1 ⊆ f2.
+ â\88\80g1,g2. g1 â\8a\86 g2 â\86\92 â\88\80f2. â\86\91f2 = g2 â\86\92 â«°g1 ⊆ f2.
#g1 #g2 #H #f2 #H2
elim (gr_sle_inv_next_dx … H … H2) -H -H2 * //
qed.
(*** sle_tl *)
lemma gr_sle_tl:
- â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 ⫱f1 â\8a\86 ⫱f2.
+ â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 â«°f1 â\8a\86 â«°f2.
#f1 elim (gr_map_split_tl f1) #H1 #f2 #H
[ lapply (gr_sle_push_sn_tl … H … H1) -H //
| elim (gr_sle_inv_next_sn … H … H1) -H //
(*** sle_inv_tl_sn *)
lemma gr_sle_inv_tl_sn:
- â\88\80f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ↑f2.
+ â\88\80f1,f2. â«°f1 ⊆ f2 → f1 ⊆ ↑f2.
#f1 elim (gr_map_split_tl f1) #H #f2 #Hf12
/2 width=5 by gr_sle_next, gr_sle_weak/
qed-.
(*** sle_inv_tl_dx *)
lemma gr_sle_inv_tl_dx:
- â\88\80f1,f2. f1 â\8a\86 ⫱f2 → ⫯f1 ⊆ f2.
+ â\88\80f1,f2. f1 â\8a\86 â«°f2 → ⫯f1 ⊆ f2.
#f1 #f2 elim (gr_map_split_tl f2) #H #Hf12
/2 width=5 by gr_sle_push, gr_sle_weak/
qed-.
(*** sle_tls *)
lemma gr_sle_tls:
- â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 â\88\80n. ⫱*[n] f1 â\8a\86 ⫱*[n] f2.
+ â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 â\88\80n. â«°*[n] f1 â\8a\86 â«°*[n] f2.
#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n
/2 width=5 by gr_sle_tl/
qed.
(*** sor_tl *)
lemma gr_sor_tl:
- â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ⫱f1 â\8b\93 ⫱f2 â\89\98 ⫱f.
+ â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 â«°f1 â\8b\93 â«°f2 â\89\98 â«°f.
#f1 cases (gr_map_split_tl f1) #H1
#f2 cases (gr_map_split_tl f2) #H2
#f #Hf
(*** sor_xxn_tl *)
lemma gr_sor_next_tl:
∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ↑f = g →
- (â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89\98 f & â\86\91f1 = g1 & ⫱g2 = f2) ∨
- (â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89\98 f & ⫱g1 = f1 & ↑f2 = g2).
+ (â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89\98 f & â\86\91f1 = g1 & â«°g2 = f2) ∨
+ (â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89\98 f & â«°g1 = f1 & ↑f2 = g2).
#g1 #g2 #g #H #f #H0 elim (gr_sor_inv_next … H … H0) -H -H0 *
/3 width=5 by ex3_2_intro, or_introl, or_intror/
qed-.
(*** sor_xnx_tl *)
lemma gr_sor_next_dx_tl:
∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f2. ↑f2 = g2 →
- â\88\83â\88\83f1,f. f1 â\8b\93 f2 â\89\98 f & ⫱g1 = f1 & ↑f = g.
+ â\88\83â\88\83f1,f. f1 â\8b\93 f2 â\89\98 f & â«°g1 = f1 & ↑f = g.
#g1 elim (gr_map_split_tl g1) #H1 #g2 #g #H #f2 #H2
[ elim (gr_sor_inv_push_next … H … H1 H2)
| elim (gr_sor_inv_next_bi … H … H1 H2)
(*** sor_nxx_tl *)
lemma gr_sor_next_sn_tl:
∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1. ↑f1 = g1 →
- â\88\83â\88\83f2,f. f1 â\8b\93 f2 â\89\98 f & ⫱g2 = f2 & ↑f = g.
+ â\88\83â\88\83f2,f. f1 â\8b\93 f2 â\89\98 f & â«°g2 = f2 & ↑f = g.
#g1 #g2 elim (gr_map_split_tl g2) #H2 #g #H #f1 #H1
[ elim (gr_sor_inv_next_push … H … H1 H2)
| elim (gr_sor_inv_next_bi … H … H1 H2)
(*** sor_inv_tl_sn *)
lemma gr_sor_inv_tl_sn:
- â\88\80f1,f2,f. ⫱f1 ⋓ f2 ≘ f → f1 ⋓ ↑f2 ≘ ↑f.
+ â\88\80f1,f2,f. â«°f1 ⋓ f2 ≘ f → f1 ⋓ ↑f2 ≘ ↑f.
#f1 #f2 #f elim (gr_map_split_tl f1)
/2 width=7 by gr_sor_push_next, gr_sor_next_bi/
qed-.
(*** sor_inv_tl_dx *)
lemma gr_sor_inv_tl_dx:
- â\88\80f1,f2,f. f1 â\8b\93 ⫱f2 ≘ f → ↑f1 ⋓ f2 ≘ ↑f.
+ â\88\80f1,f2,f. f1 â\8b\93 â«°f2 ≘ f → ↑f1 ⋓ f2 ≘ ↑f.
#f1 #f2 #f elim (gr_map_split_tl f2)
/2 width=7 by gr_sor_next_push, gr_sor_next_bi/
qed-.
(*** sor_tls *)
lemma gr_sor_tls:
∀f1,f2,f. f1 ⋓ f2 ≘ f →
- â\88\80n. ⫱*[n]f1 â\8b\93 ⫱*[n]f2 â\89\98 ⫱*[n]f.
+ â\88\80n. â«°*[n]f1 â\8b\93 â«°*[n]f2 â\89\98 â«°*[n]f.
#f1 #f2 #f #Hf #n @(nat_ind_succ … n) -n
/2 width=1 by gr_sor_tl/
qed.
(* *)
(**************************************************************************)
-include "ground/notation/functions/droppred_1.ma".
+include "ground/notation/functions/downspoon_1.ma".
include "ground/lib/stream_hdtl.ma".
include "ground/relocation/gr_map.ma".
(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
(*** tl *)
-definition gr_tl (f): gr_map â\89\9d â«°f.
+definition gr_tl (f): gr_map â\89\9d â\87£f.
interpretation
"tail (generic relocation maps)"
- 'DropPred f = (gr_tl f).
+ 'DownSpoon f = (gr_tl f).
(* Basic constructions ******************************************************)
(*** tl_push_rew *)
-lemma gr_tl_push (f): f = ⫱⫯f.
+lemma gr_tl_push (f): f = â«°⫯f.
// qed.
(*** tl_next_rew *)
-lemma gr_tl_next (f): f = ⫱↑f.
+lemma gr_tl_next (f): f = â«°↑f.
// qed.
(* Basic eliminations *******************************************************)
(*** pn_split gr_map_split *)
-lemma gr_map_split_tl (f): â\88¨â\88¨ ⫯⫱f = f | â\86\91⫱f = f.
+lemma gr_map_split_tl (f): â\88¨â\88¨ ⫯⫰f = f | â\86\91â«°f = f.
* * /2 width=1 by or_introl, or_intror/
qed-.
(*** tl_eq_repl *)
lemma gr_tl_eq_repl:
- gr_eq_repl â\80¦ (λf1,f2. ⫱f1 â\89¡ ⫱f2).
+ gr_eq_repl â\80¦ (λf1,f2. â«°f1 â\89¡ â«°f2).
#f1 #f2 * -f1 -f2 //
qed.
(*** eq_inv_gen *)
lemma gr_eq_inv_gen (g1) (g2):
g1 ≡ g2 →
- â\88¨â\88¨ â\88§â\88§ ⫱g1 â\89¡ ⫱g2 & ⫯⫱g1 = g1 & ⫯⫱g2 = g2
- | â\88§â\88§ ⫱g1 â\89¡ ⫱g2 & â\86\91⫱g1 = g1 & â\86\91⫱g2 = g2.
+ â\88¨â\88¨ â\88§â\88§ â«°g1 â\89¡ â«°g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
+ | â\88§â\88§ â«°g1 â\89¡ â«°g2 & â\86\91â«°g1 = g1 & â\86\91â«°g2 = g2.
#g1 #g2 * -g1 -g2 #f1 #f2 #g1 #g2 #f * *
/3 width=1 by and3_intro, or_introl, or_intror/
qed-.
(*** gr_eq_inv_px *)
lemma gr_eq_inv_push_sn (g1) (g2):
g1 ≡ g2 → ∀f1. ⫯f1 = g1 →
- â\88§â\88§ f1 â\89¡ ⫱g2 & ⫯⫱g2 = g2.
+ â\88§â\88§ f1 â\89¡ â«°g2 & ⫯⫰g2 = g2.
#g1 #g2 #H #f1 #Hf1
elim (gr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
[ /2 width=1 by conj/
(*** gr_eq_inv_nx *)
lemma gr_eq_inv_next_sn (g1) (g2):
g1 ≡ g2 → ∀f1. ↑f1 = g1 →
- â\88§â\88§ f1 â\89¡ ⫱g2 & â\86\91⫱g2 = g2.
+ â\88§â\88§ f1 â\89¡ â«°g2 & â\86\91â«°g2 = g2.
#g1 #g2 #H #f1 #Hf1
elim (gr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
[ elim (eq_inv_gr_push_next … Hg1)
(*** gr_eq_inv_xp *)
lemma gr_eq_inv_push_dx (g1) (g2):
g1 ≡ g2 → ∀f2. ⫯f2 = g2 →
- â\88§â\88§ ⫱g1 â\89¡ f2 & ⫯⫱g1 = g1.
+ â\88§â\88§ â«°g1 â\89¡ f2 & ⫯⫰g1 = g1.
#g1 #g2 #H #f2 #Hf2
elim (gr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
[ /2 width=1 by conj/
(*** gr_eq_inv_xn *)
lemma gr_eq_inv_next_dx (g1) (g2):
g1 ≡ g2 → ∀f2. ↑f2 = g2 →
- â\88§â\88§ ⫱g1 â\89¡ f2 & â\86\91⫱g1 = g1.
+ â\88§â\88§ â«°g1 â\89¡ f2 & â\86\91â«°g1 = g1.
#g1 #g2 #H #f2 #Hf2
elim (gr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
[ elim (eq_inv_gr_push_next … Hg2)
(* *)
(**************************************************************************)
-include "ground/notation/functions/droppreds_2.ma".
+include "ground/notation/functions/downspoonstar_2.ma".
include "ground/lib/stream_tls.ma".
include "ground/relocation/gr_tl.ma".
(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
(*** tls *)
-definition gr_tls (n) (f:gr_map) â\89\9d â«°*[n]f.
+definition gr_tls (n) (f:gr_map) â\89\9d â\87£*[n]f.
interpretation
"iterated tail (generic relocation maps)"
- 'DropPreds n f = (gr_tls n f).
+ 'DownSpoonStar n f = (gr_tls n f).
(* Basic constructions (specific) *******************************************)
(*** tls_O *)
-lemma gr_tls_zero (f): f = ⫱*[𝟎] f.
+lemma gr_tls_zero (f): f = â«°*[𝟎] f.
// qed.
(*** tls_swap *)
-lemma gr_tls_tl (n) (f): ⫱⫱*[n] f = ⫱*[n] ⫱f.
+lemma gr_tls_tl (n) (f): â«°â«°*[n] f = â«°*[n] â«°f.
/2 width=1 by stream_tls_tl/ qed.
(*** tls_S *)
-lemma gr_tls_succ (n) (f): ⫱⫱*[n] f = ⫱*[↑n] f.
+lemma gr_tls_succ (n) (f): â«°â«°*[n] f = â«°*[↑n] f.
/2 width=1 by stream_tls_succ/ qed.
(*** tls_xn *)
-lemma gr_tls_swap (n) (f): ⫱*[n] ⫱f = ⫱*[↑n] f.
+lemma gr_tls_swap (n) (f): â«°*[n] â«°f = â«°*[↑n] f.
// qed.
(*** tls_eq_repl *)
lemma gr_tls_eq_repl (n):
- gr_eq_repl (λf1,f2. ⫱*[n] f1 â\89¡ ⫱*[n] f2).
+ gr_eq_repl (λf1,f2. â«°*[n] f1 â\89¡ â«°*[n] f2).
#n @(nat_ind_succ … n) -n /3 width=1 by gr_tl_eq_repl/
qed.
(*** eq_inv_nexts_sn *)
lemma gr_eq_inv_nexts_sn (n):
∀f1,g2. ↑*[n] f1 ≡ g2 →
- â\88§â\88§ f1 â\89¡ ⫱*[n]g2 & â\86\91*[n]⫱*[n]g2 = g2.
+ â\88§â\88§ f1 â\89¡ â«°*[n]g2 & â\86\91*[n]â«°*[n]g2 = g2.
#n @(nat_ind_succ … n) -n /2 width=1 by conj/
#n #IH #f1 #g2 #H
elim (gr_eq_inv_next_sn … H) -H [|*: // ] #Hf10 *
(*** eq_inv_nexts_dx *)
lemma gr_eq_inv_nexts_dx (n):
∀f2,g1. g1 ≡ ↑*[n] f2 →
- â\88§â\88§ ⫱*[n]g1 â\89¡ f2 & â\86\91*[n]⫱*[n]g1 = g1.
+ â\88§â\88§ â«°*[n]g1 â\89¡ f2 & â\86\91*[n]â«°*[n]g1 = g1.
#n @(nat_ind_succ … n) -n /2 width=1 by conj/
#n #IH #f2 #g1 #H
elim (gr_eq_inv_next_dx … H) -H [|*: // ] #Hf02 *
(* Constructions with gr_pushs **********************************************)
(*** tls_pushs *)
-lemma gr_tls_pushs (n) (f): f = ⫱*[n] ⫯*[n] f.
+lemma gr_tls_pushs (n) (f): f = â«°*[n] ⫯*[n] f.
#n @(nat_ind_succ … n) -n //
#n #IH #f <gr_tls_swap <gr_pushs_succ <gr_tl_push //
qed.
(*** eq_inv_pushs_sn *)
lemma gr_eq_inv_pushs_sn (n):
∀f1,g2. ⫯*[n] f1 ≡ g2 →
- â\88§â\88§ f1 â\89¡ ⫱*[n]g2 & ⫯*[n]⫱*[n]g2 = g2.
+ â\88§â\88§ f1 â\89¡ â«°*[n]g2 & ⫯*[n]â«°*[n]g2 = g2.
#n @(nat_ind_succ … n) -n /2 width=1 by conj/
#n #IH #f1 #g2 #H
elim (gr_eq_inv_push_sn … H) -H [|*: // ] #Hf10 *
(*** eq_inv_pushs_dx *)
lemma gr_eq_inv_pushs_dx (n):
∀f2,g1. g1 ≡ ⫯*[n] f2 →
- â\88§â\88§ ⫱*[n]g1 â\89¡ f2 & ⫯*[n]⫱*[n]g1 = g1.
+ â\88§â\88§ â«°*[n]g1 â\89¡ f2 & ⫯*[n]â«°*[n]g1 = g1.
#n @(nat_ind_succ … n) -n /2 width=1 by conj/
#n #IH #f2 #g1 #H
elim (gr_eq_inv_push_dx … H) -H [|*: // ] #Hf02 *
[ "gr_basic ( 𝐛❨?,?❩ )" * ]
[ "gr_uni ( 𝐮❨?❩ )" "gr_uni_eq" * ]
[ "gr_id ( 𝐢 ) " "gr_id_eq" * ]
- [ "gr_tls ( ⫱*[?]? )" "gr_tls_eq" "gr_tls_pushs" "gr_tls_pushs_eq" "gr_tls_nexts_eq" * ]
+ [ "gr_tls ( â«°*[?]? )" "gr_tls_eq" "gr_tls_pushs" "gr_tls_pushs_eq" "gr_tls_nexts_eq" * ]
[ "gr_nexts ( ↑*[?]? )" "gr_nexts_eq" * ]
[ "gr_pushs ( ⫯*[?]? )" "gr_pushs_eq" * ]
- [ "gr_tl ( ⫱? )" "gr_tl_eq" "gr_tl_eq_eq" * ]
+ [ "gr_tl ( â«°? )" "gr_tl_eq" "gr_tl_eq_eq" * ]
[ "gr_eq ( ? ≡ ? )" * ]
[ "gr_map ( ⫯? ) ( ↑? )" * ]
}
class "yellow"
[ { "extensions to the library" * } {
[ { "streams" * } {
- [ "stream_tls ( â«°*{?}[?]? )" "stream_tls_eq" * ]
- [ "stream_hdtl ( â«°{?}? )" * ]
+ [ "stream_tls ( â\87£*{?}[?]? )" "stream_tls_eq" * ]
+ [ "stream_hdtl ( â\87£{?}? )" * ]
[ "stream_eq ( ? ≗{?} ? )" "stream_eq_eq" * ]
[ "stream ( ? ⨮{?} ? )" * ]
}
(* Properties with application **********************************************)
lemma drops_tls_at: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
- â\88\80b,L1,L2. â\87©*[b,⫱*[i2]f] L1 ≘ L2 →
- â\87©*[b,⫯⫱*[↑i2]f] L1 ≘ L2.
+ â\88\80b,L1,L2. â\87©*[b,â«°*[i2]f] L1 ≘ L2 →
+ â\87©*[b,⫯⫰*[↑i2]f] L1 ≘ L2.
/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❪O,f❫ ≘ i →
- â\88\83â\88\83J,K. â\87©[i]L â\89\98 K.â\93\98[J] & â\87©*[b,⫱*[â\86\91i]f] K â\89\98 K0 & â\87§*[⫱*[↑i]f] I ≘ J.
+ â\88\83â\88\83J,K. â\87©[i]L â\89\98 K.â\93\98[J] & â\87©*[b,â«°*[â\86\91i]f] K â\89\98 K0 & â\87§*[â«°*[↑i]f] I ≘ J.
#b #f #I #L #K0 #H #i #Hf
elim (drops_split_trans … H) -H [ |5: @(after_uni_dx … Hf) |2,3: skip ] /2 width=1 by after_isid_dx/ #Y #HLY #H
lapply (drops_tls_at … Hf … H) -H #H
lemma sex_sdj_split_dx (R1) (R2) (RP):
c_reflexive … R1 → c_reflexive … R2 → c_reflexive … RP →
∀L1,f1.
- (â\88\80g,I,K,n. â\87©[n] L1 â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
+ (â\88\80g,I,K,n. â\87©[n] L1 â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
#R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1
qed-.
lemma seq_inv_tl (f):
- â\88\80I,L1,L2. L1 â\89¡[⫱f] L2 → L1.ⓘ[I] ≡[f] L2.ⓘ[I].
+ â\88\80I,L1,L2. L1 â\89¡[â«°f] L2 → L1.ⓘ[I] ≡[f] L2.ⓘ[I].
/2 width=1 by sex_inv_tl/ qed-.
(* Basic_2A1: removed theorems 5:
qed-.
lemma sex_inv_tl (RN) (RP):
- â\88\80f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →
+ â\88\80f,I1,I2,L1,L2. L1 ⪤[RN,RP,â«°f] L2 →
RN L1 I1 I2 → RP L1 I1 I2 →
L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2].
#RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) *
lemma sex_fwd_bind (RN) (RP):
∀f,I1,I2,L1,L2.
- L1.â\93\98[I1] ⪤[RN,RP,f] L2.â\93\98[I2] â\86\92 L1 ⪤[RN,RP,⫱f] L2.
+ L1.â\93\98[I1] ⪤[RN,RP,f] L2.â\93\98[I2] â\86\92 L1 ⪤[RN,RP,â«°f] L2.
#RN #RP #f #I1 #I2 #L1 #L2 #Hf
elim (pn_split f) * #g #H destruct
[ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf //
lapply (sex_inv_atom1 … H) -H #H destruct
| #f @or_intror #H
lapply (sex_inv_atom2 … H) -H #H destruct
-| #L2 #I2 #f elim (IH L2 (⫱f)) -IH #HL12
+| #L2 #I2 #f elim (IH L2 (â«°f)) -IH #HL12
[2: /4 width=3 by sex_fwd_bind, or_intror/ ]
elim (pn_split f) * #g #H destruct
[ elim (HRP L1 I1 I2) | elim (HRN L1 I1 I2) ] -HRP -HRN #HV12
theorem sex_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP):
∀L1,f.
- (â\88\80g,I,K,n. â\87©[n] L1 â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[n] f → R_pw_transitive_sex RN1 RN2 RN RN1 RP1 g K I) →
- (â\88\80g,I,K,n. â\87©[n] L1 â\89\98 K.â\93\98[I] â\86\92 ⫯g = ⫱*[n] f → R_pw_transitive_sex RP1 RP2 RP RN1 RP1 g K I) →
+ (â\88\80g,I,K,n. â\87©[n] L1 â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[n] f → R_pw_transitive_sex RN1 RN2 RN RN1 RP1 g K I) →
+ (â\88\80g,I,K,n. â\87©[n] L1 â\89\98 K.â\93\98[I] â\86\92 ⫯g = â«°*[n] f → R_pw_transitive_sex RP1 RP2 RP RN1 RP1 g K I) →
∀L0. L1 ⪤[RN1,RP1,f] L0 →
∀L2. L0 ⪤[RN2,RP2,f] L2 →
L1 ⪤[RN,RP,f] L2.
theorem sex_conf (RN1) (RP1) (RN2) (RP2):
∀L,f.
- (â\88\80g,I,K,n. â\87©[n] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
- (â\88\80g,I,K,n. â\87©[n] L â\89\98 K.â\93\98[I] â\86\92 ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
+ (â\88\80g,I,K,n. â\87©[n] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
+ (â\88\80g,I,K,n. â\87©[n] L â\89\98 K.â\93\98[I] â\86\92 ⫯g = â«°*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
pw_confluent2 … (sex RN1 RP1 f) (sex RN2 RP2 f) L.
#RN1 #RP1 #RN2 #RP2 #L elim L -L
[ #f #_ #_ #L1 #H1 #L2 #H2 >(sex_inv_atom1 … H1) >(sex_inv_atom1 … H2) -H2 -H1
qed-.
lemma sex_repl (RN) (RP) (SN) (SP) (L1) (f):
- (â\88\80g,I,K1,n. â\87©[n] L1 â\89\98 K1.â\93\98[I] â\86\92 â\86\91g = ⫱*[n] f → R_pw_replace3_sex … RN SN RN RP SN SP g K1 I) →
- (â\88\80g,I,K1,n. â\87©[n] L1 â\89\98 K1.â\93\98[I] â\86\92 ⫯g = ⫱*[n] f → R_pw_replace3_sex … RP SP RN RP SN SP g K1 I) →
+ (â\88\80g,I,K1,n. â\87©[n] L1 â\89\98 K1.â\93\98[I] â\86\92 â\86\91g = â«°*[n] f → R_pw_replace3_sex … RN SN RN RP SN SP g K1 I) →
+ (â\88\80g,I,K1,n. â\87©[n] L1 â\89\98 K1.â\93\98[I] â\86\92 ⫯g = â«°*[n] f → R_pw_replace3_sex … RP SP RN RP SN SP g K1 I) →
∀L2. L1 ⪤[RN,RP,f] L2 → ∀K1. L1 ⪤[SN,SP,f] K1 →
∀K2. L2 ⪤[SN,SP,f] K2 → K1 ⪤[RN,RP,f] K2.
#RN #RP #SN #SP #L1 elim L1 -L1
frees (L.ⓘ[I]) (#↑i) (⫯f)
| frees_gref: ∀f,L,l. 𝐈❪f❫ → frees L (§l) f
| frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ[I]V) T f2 →
- f1 â\8b\93 ⫱f2 ≘ f → frees L (ⓑ[p,I]V.T) f
+ f1 â\8b\93 â«°f2 ≘ f → frees L (ⓑ[p,I]V.T) f
| frees_flat: ∀f1,f2,f,I,L,V,T. frees L V f1 → frees L T f2 →
f1 ⋓ f2 ≘ f → frees L (ⓕ[I]V.T) f
.
fact frees_inv_bind_aux:
∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀p,I,V,T. X = ⓑ[p,I]V.T →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
#f #L #X * -f -L -X
[ #f #L #s #_ #q #J #W #U #H destruct
| #f #i #_ #q #J #W #U #H destruct
lemma frees_inv_bind:
∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
/2 width=4 by frees_inv_bind_aux/ qed-.
fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,V,T. X = ⓕ[I]V.T →
lemma frees_inv_lifts_SO:
∀b,f,L,U. L ⊢ 𝐅+❪U❫ ≘ f →
∀K. ⇩*[b,𝐔❨1❩] L ≘ K → ∀T. ⇧[1] T ≘ U →
- K â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 ⫱f.
+ K â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 â«°f.
#b #f #L #U #H #K #HLK #T #HTU elim(frees_inv_lifts_ex … H … HLK … HTU) -b -L -U
#f1 #Hf #Hf1 elim (coafter_inv_nxx … Hf) -Hf
/3 width=5 by frees_eq_repl_back, coafter_isid_inv_sn/
lemma frees_inv_drops_next:
∀f1,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f1 →
∀I2,L2,V2,i. ⇩[i] L1 ≘ L2.ⓑ[I2]V2 →
- â\88\80g1. â\86\91g1 = ⫱*[i] f1 →
+ â\88\80g1. â\86\91g1 = â«°*[i] f1 →
∃∃g2. L2 ⊢ 𝐅+❪V2❫ ≘ g2 & g2 ⊆ g1.
#f1 #L1 #T1 #H elim H -f1 -L1 -T1
[ #f1 #L1 #s #Hf1 #I2 #L2 #V2 #j #_ #g1 #H1 -I2 -L1 -s
| #p #I #V #T #HG #HL #HT destruct
elim (IH G L V) // #f1 #HV
elim (IH G (L.ⓑ[I]V) T) -IH // #f2 #HT
- elim (sor_isfin_ex f1 (⫱f2))
+ elim (sor_isfin_ex f1 (â«°f2))
/3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
| #I #V #T #HG #HL #HT destruct
elim (IH G L V) // #f1 #HV
theorem frees_bind_void:
∀f1,L,V. L ⊢ 𝐅+❪V❫ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 →
- â\88\80f. f1 â\8b\93 ⫱f2 ≘ f → ∀p,I. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f.
+ â\88\80f. f1 â\8b\93 â«°f2 ≘ f → ∀p,I. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f.
#f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0
lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
lemma frees_inv_bind_void:
∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93§ â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93§ â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
#f #p #I #L #V #T #H
elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
elim (frees_total (L.ⓧ) T) #f0 #Hf0
∀f,L,l. 𝐈❪f❫ → Q L (§l) f
) → (
∀f1,f2,f,p,I,L,V,T.
- L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85+â\9dªTâ\9d«â\89\98 f2 â\86\92 f1 â\8b\93 ⫱f2 ≘ f →
+ L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85+â\9dªTâ\9d«â\89\98 f2 â\86\92 f1 â\8b\93 â«°f2 ≘ f →
Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ[p,I]V.T) f
) → (
∀f1,f2,f,I,L,V,T.
definition fsle: bi_relation lenv term ≝ λL1,T1,L2,T2.
∃∃n1,n2,f1,f2. L1 ⊢ 𝐅+❪T1❫ ≘ f1 & L2 ⊢ 𝐅+❪T2❫ ≘ f2 &
- L1 â\89\8bâ\93§*[n1,n2] L2 & ⫱*[n1]f1 â\8a\86 ⫱*[n2]f2.
+ L1 â\89\8bâ\93§*[n1,n2] L2 & â«°*[n1]f1 â\8a\86 â«°*[n2]f2.
interpretation "free variables inclusion (restricted closure)"
'SubSetEq L1 T1 L2 T2 = (fsle L1 T1 L2 T2).
* #n #m #f2 #g2 #Hf2 #Hg2 #HL #Hfg2 #p
elim (lveq_inv_pair_pair … HL) -HL #HL #H1 #H2 destruct
elim (frees_total L2 V2) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
lapply (frees_inv_lifts_SO (Ⓣ) … Hf2 … HTU1)
[1,2: /3 width=4 by drops_refl, drops_drop/ ] -U1 #Hf2
lapply (sor_inv_sle_dx … Hg) #H0g
elim (lveq_inj_length … H2L) // -H1L #H1 #H2 destruct
lapply (lveq_inv_bind_O … H2L) -H2L #HL
elim (frees_total L2 V) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
lapply (sor_inv_sle_dx … Hg) #H0g
/4 width=10 by frees_bind, lveq_void_sn, sle_tl, sle_trans, ex4_4_intro/
qed.
∀p,I,T2. ❪L1,V1❫ ⊆ ❪L2,ⓑ[p,I]V2.T2❫.
#L1 #L2 #V1 #V2 * #n1 #m1 #f1 #g1 #Hf1 #Hg1 #HL12 #Hfg1 #p #I #T2
elim (frees_total (L2.ⓧ) T2) #g2 #Hg2
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
@(ex4_4_intro … g Hf1 … HL12) (**) (* full auto too slow *)
/4 width=5 by frees_bind_void, sor_inv_sle_sn, sor_tls, sle_trans/
qed.
elim (lveq_inv_void_dx_length … H HL12) -H -HL12 #m1 #HL12 #H1 #H2 destruct
<tls_xn in Hfg2; #Hfg2
elim (frees_total L2 V2) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
@(ex4_4_intro … g Hf2 … HL12) (**) (* full auto too slow *)
/4 width=5 by frees_bind_void, sor_inv_sle_dx, sor_tls, sle_trans/
qed.
lemma fsle_frees_trans:
∀L1,L2,T1,T2. ❪L1,T1❫ ⊆ ❪L2,T2❫ →
∀f2. L2 ⊢ 𝐅+❪T2❫ ≘ f2 →
- â\88\83â\88\83n1,n2,f1. L1 â\8a¢ ð\9d\90\85+â\9dªT1â\9d« â\89\98 f1 & L1 â\89\8bâ\93§*[n1,n2] L2 & ⫱*[n1]f1 â\8a\86 ⫱*[n2]f2.
+ â\88\83â\88\83n1,n2,f1. L1 â\8a¢ ð\9d\90\85+â\9dªT1â\9d« â\89\98 f1 & L1 â\89\8bâ\93§*[n1,n2] L2 & â«°*[n1]f1 â\8a\86 â«°*[n2]f2.
#L1 #L2 #T1 #T2 * #n1 #n2 #f1 #g2 #Hf1 #Hg2 #HL #Hn #f2 #Hf2
lapply (frees_mono … Hg2 … Hf2) -Hg2 -Hf2 #Hgf2
lapply (tls_eq_repl n2 … Hgf2) -Hgf2 #Hgf2
lemma fsle_frees_conf:
∀L1,L2,T1,T2. ❪L1,T1❫ ⊆ ❪L2,T2❫ →
∀f1. L1 ⊢ 𝐅+❪T1❫ ≘ f1 →
- â\88\83â\88\83n1,n2,f2. L2 â\8a¢ ð\9d\90\85+â\9dªT2â\9d« â\89\98 f2 & L1 â\89\8bâ\93§*[n1,n2] L2 & ⫱*[n1]f1 â\8a\86 ⫱*[n2]f2.
+ â\88\83â\88\83n1,n2,f2. L2 â\8a¢ ð\9d\90\85+â\9dªT2â\9d« â\89\98 f2 & L1 â\89\8bâ\93§*[n1,n2] L2 & â«°*[n1]f1 â\8a\86 â«°*[n2]f2.
#L1 #L2 #T1 #T2 * #n1 #n2 #g1 #g2 #Hg1 #Hg2 #HL #Hn #f1 #Hf1
lapply (frees_mono … Hg1 … Hf1) -Hg1 -Hf1 #Hgf1
lapply (tls_eq_repl n1 … Hgf1) -Hgf1 #Hgf1
#L1 #L2 #HL #V1 #T1 #T * #n1 #x #f1 #g #Hf1 #Hg #H1n1 #H2n1 #H #p #I
elim (fsle_frees_trans … H … Hg) -H #n2 #n #f2 #Hf2 #H1n2 #H2n2
elim (lveq_inj_void_sn_ge … H1n1 … H1n2) -H1n2 // #H1 #H2 #H3 destruct
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex f1 (â«°f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
<tls_xn in H2n2; #H2n2
/4 width=12 by frees_bind_void, sor_inv_sle, sor_tls, ex4_4_intro/
qed.
* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p #I1
elim (lveq_inj_length … H1L) // #H1 #H2 destruct
elim (lveq_inj_length … H2L) // -HL -H2L #H1 #H2 destruct
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex f1 (â«°f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
/4 width=15 by frees_bind_void, frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
qed.
* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p
elim (lveq_inv_pair_pair … H2L) -H2L #H2L #H1 #H2 destruct
elim (lveq_inj … H2L … H1L) -H1L #H1 #H2 destruct
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex f1 (â«°f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
/4 width=15 by frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
qed.
(* Basic forward lemmas *****************************************************)
lemma lsubf_fwd_bind_tl:
- â\88\80f1,f2,I,L1,L2. â\9dªL1.â\93\98[I],f1â\9d« â«\83ð\9d\90\85+ â\9dªL2.â\93\98[I],f2â\9d« â\86\92 â\9dªL1,⫱f1â\9d« â«\83ð\9d\90\85+ â\9dªL2,⫱f2❫.
+ â\88\80f1,f2,I,L1,L2. â\9dªL1.â\93\98[I],f1â\9d« â«\83ð\9d\90\85+ â\9dªL2.â\93\98[I],f2â\9d« â\86\92 â\9dªL1,â«°f1â\9d« â«\83ð\9d\90\85+ â\9dªL2,â«°f2❫.
#f1 #f2 #I #L1 #L2 #H
elim (pn_split f1) * #g1 #H0 destruct
[ elim (lsubf_inv_push_sn … H) | elim (lsubf_inv_bind_sn … H) ] -H
/2 width=3 by lsubf_eq_repl_back2/ qed.
lemma lsubf_bind_tl_dx:
- â\88\80g1,f2,I,L1,L2. â\9dªL1,g1â\9d« â«\83ð\9d\90\85+ â\9dªL2,⫱f2❫ →
- â\88\83â\88\83f1. â\9dªL1.â\93\98[I],f1â\9d« â«\83ð\9d\90\85+ â\9dªL2.â\93\98[I],f2â\9d« & g1 = ⫱f1.
+ â\88\80g1,f2,I,L1,L2. â\9dªL1,g1â\9d« â«\83ð\9d\90\85+ â\9dªL2,â«°f2❫ →
+ â\88\83â\88\83f1. â\9dªL1.â\93\98[I],f1â\9d« â«\83ð\9d\90\85+ â\9dªL2.â\93\98[I],f2â\9d« & g1 = â«°f1.
#g1 #f2 #I #L1 #L2 #H
elim (pn_split f2) * #g2 #H2 destruct
@ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
lemma lsubf_beta_tl_dx:
∀f,f0,g1,L1,V. L1 ⊢ 𝐅+❪V❫ ≘ f → f0 ⋓ f ≘ g1 →
- â\88\80f2,L2,W. â\9dªL1,f0â\9d« â«\83ð\9d\90\85+ â\9dªL2,⫱f2❫ →
- â\88\83â\88\83f1. â\9dªL1.â\93\93â\93\9dW.V,f1â\9d« â«\83ð\9d\90\85+ â\9dªL2.â\93\9bW,f2â\9d« & ⫱f1 ⊆ g1.
+ â\88\80f2,L2,W. â\9dªL1,f0â\9d« â«\83ð\9d\90\85+ â\9dªL2,â«°f2❫ →
+ â\88\83â\88\83f1. â\9dªL1.â\93\93â\93\9dW.V,f1â\9d« â«\83ð\9d\90\85+ â\9dªL2.â\93\9bW,f2â\9d« & â«°f1 ⊆ g1.
#f #f0 #g1 #L1 #V #Hf #Hg1 #f2
elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
[ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
definition f_transitive_next:
relation3 … ≝ λR1,R2,R3.
∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
- â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[i] f →
+ â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[i] f →
R_pw_transitive_sex (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
definition f_confluent1_next: relation2 … ≝ λR1,R2.
∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
- â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[i] f →
+ â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[i] f →
R_pw_confluent1_sex (cext2 R1) (cext2 R1) (cext2 R2) cfull g K I.
(* Properties with generic slicing for local environments *******************)
∀L1,L2,V1,V2,T. L1 ⪤[R,V1] L2 → L1.ⓑ[I]V1 ⪤[R,T] L2.ⓑ[I]V2 →
L1 ⪤[R,ⓑ[p,I]V1.T] L2.
#R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
-lapply (sex_fwd_bind â\80¦ Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫱f2))
+lapply (sex_fwd_bind â\80¦ Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (â«°f2))
/3 width=7 by frees_fwd_isfin, frees_bind, sex_join, isfin_tl, ex2_intro/
qed.
theorem rex_bind_void (R) (p) (I):
∀L1,L2,V,T. L1 ⪤[R,V] L2 → L1.ⓧ ⪤[R,T] L2.ⓧ → L1 ⪤[R,ⓑ[p,I]V.T] L2.
#R #p #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
-lapply (sex_fwd_bind â\80¦ Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫱f2))
+lapply (sex_fwd_bind â\80¦ Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (â«°f2))
/3 width=7 by frees_fwd_isfin, frees_bind_void, sex_join, isfin_tl, ex2_intro/
qed.
["⇕"; "⇳"; "⬍"; "↕"; ];
["↔"; "⇔"; "⬄"; "⬌"; ] ;
["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ;
- ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["_"; "â\86\93"; "â\86\99"; "â\87£"; "â\8e½"; "â\8e¼"; "â\8e»"; "â\8eº"; ];
["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
["("; "❨"; "❪"; "❲"; "（"; ];
[")"; "❩"; "❫"; "❳"; "）"; ];
projects / helm.git / commitdiff