(* *)
(**************************************************************************)
-include "ground_2/notation/functions/successor_1.ma".
+include "ground_2/notation/constructors/successor_1.ma".
include "ground_2/notation/functions/predecessor_1.ma".
include "arithmetics/nat.ma".
include "ground_2/lib/relations.ma".
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ⫯ term 70 T )"
+ non associative with precedence 70
+ for @{ 'Successor $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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( ⫯ term 70 T )"
- non associative with precedence 70
- for @{ 'Successor $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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ⫯ * [ term 46 n ] term 70 T )"
+ non associative with precedence 70
+ for @{ 'SuccessorStar $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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝛀 ⦃ term 46 f ⦄ )"
+ non associative with precedence 45
+ for @{ 'IsDivergent $f }.
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) }.
+(* multiple existental quantifier (7, 6) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P6) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P6) }.
+
(* multiple existental quantifier (7, 7) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/relocation/rtmap_sand.ma".
--- /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 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/rtmap_sor.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+axiom union: rtmap → rtmap → rtmap.
+
+interpretation "union (nstream)"
+ 'union f1 f2 = (union f1 f2).
+
+(* Specific properties on sor ***********************************************)
+
+axiom sor_total: ∀f1,f2. f1 ⋓ f2 ≡ f1 ∪ f2.
f1 ≗ g1 → f2 ≗ g2 → f ≗ g.
/4 width=4 by coafter_mono, coafter_eq_repl_back1, coafter_eq_repl_back2/ qed-.
-(* Inversion lemmas with pushs **********************************************)
-
-lemma coafter_fwd_pushs: ∀n,g2,g1,g. g2 ~⊚ g1 ≡ g → @⦃0, g2⦄ ≡ n →
- ∃f. ↑*[n]f = g.
-#n elim n -n /2 width=2 by ex_intro/
-#n #IH #g2 #g1 #g #Hg #Hg2
-cases (at_inv_pxn … Hg2) -Hg2 [ |*: // ] #f2 #Hf2 #H2
-cases (coafter_inv_nxx … Hg … H2) -Hg -H2 #f #Hf #H0 destruct
-elim (IH … Hf Hf2) -g1 -g2 -f2 /2 width=2 by ex_intro/
+(* Forward lemmas with pushs ************************************************)
+
+lemma coafter_fwd_pushs: ∀j,i,g2,f1,g. g2 ~⊚ ↑*[i]f1 ≡ g → @⦃i, g2⦄ ≡ j →
+ ∃f. ↑*[j] f = g.
+#j elim j -j
+[ #i #g2 #f1 #g #Hg #H
+ elim (at_inv_xxp … H) -H [|*: // ] #f2 #H1 #H2 destruct
+ /2 width=2 by ex_intro/
+| #j #IH * [| #i ] #g2 #f1 #g #Hg #H
+ [ elim (at_inv_pxn … H) -H [|*: // ] #f2 #Hij #H destruct
+ elim (coafter_inv_nxx … Hg) -Hg [|*: // ] #f #Hf #H destruct
+ elim (IH … Hf Hij) -f1 -f2 -IH /2 width=2 by ex_intro/
+ | elim (at_inv_nxn … H) -H [1,4: * |*: // ] #f2 #Hij #H destruct
+ [ elim (coafter_inv_ppx … Hg) -Hg [|*: // ] #f #Hf #H destruct
+ elim (IH … Hf Hij) -f1 -f2 -i /2 width=2 by ex_intro/
+ | elim (coafter_inv_nxx … Hg) -Hg [|*: // ] #f #Hf #H destruct
+ elim (IH … Hf Hij) -f1 -f2 -i /2 width=2 by ex_intro/
+ ]
+ ]
+]
qed-.
(* Inversion lemmas with tail ***********************************************)
(* Properties with iterated tail ********************************************)
-lemma coafter_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n →
- f1 ~⊚ f2 ≡ f → ⫱*[n]f1 ~⊚ f2 ≡ ⫱*[n]f.
-#n elim n -n //
-#n #IH #f1 #f2 #f #Hf1 #Hf
-cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
-cases (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
-<tls_xn <tls_xn /2 width=1 by/
+lemma coafter_tls: ∀j,i,f1,f2,f. @⦃i, f1⦄ ≡ j →
+ f1 ~⊚ f2 ≡ f → ⫱*[j]f1 ~⊚ ⫱*[i]f2 ≡ ⫱*[j]f.
+#j elim j -j [ #i | #j #IH * [| #i ] ] #f1 #f2 #f #Hf1 #Hf
+[ elim (at_inv_xxp … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 destruct //
+| elim (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
+ elim (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
+ lapply (IH … Hg1 Hg) -IH -Hg1 -Hg //
+| elim (at_inv_nxn … Hf1) -Hf1 [1,4: * |*: // ] #g1 #Hg1 #H1
+ [ elim (coafter_inv_pxx … Hf … H1) -Hf * #g2 #g #Hg #H2 #H0 destruct
+ lapply (IH … Hg1 Hg) -IH -Hg1 -Hg #H //
+ | elim (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
+ lapply (IH … Hg1 Hg) -IH -Hg1 -Hg #H //
+ ]
+]
qed.
+lemma coafter_tls_O: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n →
+ f1 ~⊚ f2 ≡ f → ⫱*[n]f1 ~⊚ f2 ≡ ⫱*[n]f.
+/2 width=1 by coafter_tls/ qed.
+
lemma coafter_tls_succ: ∀g2,g1,g. g2 ~⊚ g1 ≡ g →
∀n. @⦃0, g2⦄ ≡ n → ⫱*[⫯n]g2 ~⊚ ⫱g1 ≡ ⫱*[⫯n]g.
#g2 #g1 #g #Hg #n #Hg2
<tls_S <tls_S <H2 <H0 -g2 -g -n //
qed.
-lemma coafter_fwd_xpx_pushs: ∀g2,f1,g,n. g2 ~⊚ ↑f1 ≡ g → @⦃0, g2⦄ ≡ n →
- ∃f. ↑*[⫯n]f = g.
-#g2 #g1 #g #n #Hg #Hg2
+lemma coafter_fwd_xpx_pushs: ∀g2,f1,g,i,j. @⦃i, g2⦄ ≡ j → g2 ~⊚ ↑*[⫯i]f1 ≡ g →
+ ∃∃f. ⫱*[⫯j]g2 ~⊚ f1 ≡ f & ↑*[⫯j]f = g.
+#g2 #g1 #g #i #j #Hg2 <pushs_xn #Hg
elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
-lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs #Hf
-lapply (at_pxx_tls … Hg2) -Hg2 #H
-elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
-elim (coafter_inv_pxx … Hf … H2) -Hf -H2 * #f1 #g #_ #H1 #H0 destruct
-[ /2 width=2 by ex_intro/
-| elim (discr_next_push … H1)
-]
+lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs <tls_pushs #Hf
+lapply (at_inv_tls … Hg2) -Hg2 #H
+lapply (coafter_eq_repl_fwd2 … Hf … H) -H -Hf #Hf
+elim (coafter_inv_ppx … Hf) [|*: // ] -Hf #g #Hg #H destruct
+/2 width=3 by ex2_intro/
qed-.
-lemma coafter_fwd_xnx_pushs: ∀g2,f1,g,n. g2 ~⊚ ⫯f1 ≡ g → @⦃0, g2⦄ ≡ n →
- ∃f. ↑*[n] ⫯f = g.
-#g2 #g1 #g #n #Hg #Hg2
+lemma coafter_fwd_xnx_pushs: ∀g2,f1,g,i,j. @⦃i, g2⦄ ≡ j → g2 ~⊚ ↑*[i]⫯f1 ≡ g →
+ ∃∃f. ⫱*[⫯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 #Hf
-lapply (at_pxx_tls … Hg2) -Hg2 #H
-elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
-elim (coafter_inv_pxx … Hf … H2) -Hf -H2 * #f1 #g #_ #H1 #H0 destruct
-[ elim (discr_push_next … H1)
-| /2 width=2 by ex_intro/
-]
+lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs <tls_pushs #Hf
+lapply (at_inv_tls … Hg2) -Hg2 #H
+lapply (coafter_eq_repl_fwd2 … Hf … H) -H -Hf #Hf
+elim (coafter_inv_pnx … Hf) [|*: // ] -Hf #g #Hg #H destruct
+/2 width=3 by ex2_intro/
qed-.
(* Properties with test for identity ****************************************)
cases (H2g1 0) #n #Hn
cases (coafter_inv_pxx … H … H1) -H * #g2 #g #H #H2 #H0
[ lapply (isid_inv_push … Hf … H0) -Hf #Hg
- @(isid_push … H2)
- /3 width=7 by coafter_tls, istot_tls, at_pxx_tls, isid_tls/
+ @(isid_push … H2) -H2
+ /3 width=7 by coafter_tls_O, at_pxx_tls, istot_tls, isid_tls/
| cases (isid_inv_next … Hf … H0)
]
qed-.
elim (Hg1 0) #n #Hn
[ elim (coafter_inv_ppx … Hf) | elim (coafter_inv_pnx … Hf)
] -Hf [1,6: |*: // ] #g #Hg #H0 destruct
-/5 width=6 by isfin_next, isfin_push, isfin_inv_tls, istot_tls, at_pxx_tls, coafter_tls/
+/5 width=6 by isfin_next, isfin_push, isfin_inv_tls, istot_tls, at_pxx_tls, coafter_tls_O/
qed-.
fact coafter_isfin2_fwd_aux: (∀f1. @⦃0, f1⦄ ≡ 0 → H_coafter_isfin2_fwd f1) →
--- /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 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/isdivergent_1.ma".
+include "ground_2/relocation/rtmap_nexts.ma".
+include "ground_2/relocation/rtmap_tls.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+coinductive isdiv: predicate rtmap ≝
+| isdiv_next: ∀f,g. isdiv f → ⫯f = g → isdiv g
+.
+
+interpretation "test for divergence (rtmap)"
+ 'IsDivergent f = (isdiv f).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma isdiv_inv_gen: ∀g. 𝛀⦃g⦄ → ∃∃f. 𝛀⦃f⦄ & ⫯f = g.
+#g * -g
+#f #g #Hf * /2 width=3 by ex2_intro/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma isdiv_inv_next: ∀g. 𝛀⦃g⦄ → ∀f. ⫯f = g → 𝛀⦃f⦄.
+#g #H elim (isdiv_inv_gen … H) -H
+#f #Hf * -g #g #H >(injective_next … H) -H //
+qed-.
+
+lemma isdiv_inv_push: ∀g. 𝛀⦃g⦄ → ∀f. ↑f = g → ⊥.
+#g #H elim (isdiv_inv_gen … H) -H
+#f #Hf * -g #g #H elim (discr_push_next … H)
+qed-.
+
+(* Main inversion lemmas ****************************************************)
+
+corec theorem isdiv_inv_eq_repl: ∀f1,f2. 𝛀⦃f1⦄ → 𝛀⦃f2⦄ → f1 ≗ f2.
+#f1 #f2 #H1 #H2
+cases (isdiv_inv_gen … H1) -H1
+cases (isdiv_inv_gen … H2) -H2
+/3 width=5 by eq_next/
+qed-.
+
+(* Basic properties *********************************************************)
+
+corec lemma isdiv_eq_repl_back: eq_repl_back … isdiv.
+#f1 #H cases (isdiv_inv_gen … H) -H
+#g1 #Hg1 #H1 #f2 #Hf cases (eq_inv_nx … Hf … H1) -f1
+/3 width=3 by isdiv_next/
+qed-.
+
+lemma isdiv_eq_repl_fwd: eq_repl_fwd … isdiv.
+/3 width=3 by isdiv_eq_repl_back, eq_repl_sym/ qed-.
+
+(* Alternative definition ***************************************************)
+
+corec lemma eq_next_isdiv: ∀f. ⫯f ≗ f → 𝛀⦃f⦄.
+#f #H cases (eq_inv_nx … H) -H /4 width=3 by isdiv_next, eq_trans/
+qed.
+
+corec lemma eq_next_inv_isdiv: ∀f. 𝛀⦃f⦄ → ⫯f ≗ f.
+#f * -f
+#f #g #Hf #Hg @(eq_next … Hg) [2: @eq_next_inv_isdiv // | skip ]
+@eq_f //
+qed-.
+
+(* Properties with iterated next ********************************************)
+
+lemma isdiv_nexts: ∀n,f. 𝛀⦃f⦄ → 𝛀⦃⫯*[n]f⦄.
+#n elim n -n /3 width=3 by isdiv_next/
+qed.
+
+(* Inversion lemmas with iterated next **************************************)
+
+lemma isdiv_inv_nexts: ∀n,g. 𝛀⦃⫯*[n]g⦄ → 𝛀⦃g⦄.
+#n elim n -n /3 width=3 by isdiv_inv_next/
+qed.
+
+(* Properties with tail *****************************************************)
+
+lemma isdiv_tl: ∀f. 𝛀⦃f⦄ → 𝛀⦃⫱f⦄.
+#f cases (pn_split f) * #g * -f #H
+[ elim (isdiv_inv_push … H) -H //
+| /2 width=3 by isdiv_inv_next/
+]
+qed.
+
+(* Properties with iterated tail ********************************************)
+
+lemma isdiv_tls: ∀n,g. 𝛀⦃g⦄ → 𝛀⦃⫱*[n]g⦄.
+#n elim n -n /3 width=1 by isdiv_tl/
+qed.
(* Basic inversion lemmas ***************************************************)
+lemma isfin_inv_push: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄.
+#g * /3 width=4 by fcla_inv_px, ex_intro/
+qed-.
+
lemma isfin_inv_next: ∀g. 𝐅⦃g⦄ → ∀f. ⫯f = g → 𝐅⦃f⦄.
#g * #n #H #f #H0 elim (fcla_inv_nx … H … H0) -g
/2 width=2 by ex_intro/
qed-.
-(* Basic forward lemmas *****************************************************)
-
-lemma isfin_fwd_push: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄.
-#g * /3 width=4 by fcla_inv_px, ex_intro/
-qed-.
-
(* Basic properties *********************************************************)
lemma isfin_eq_repl_back: eq_repl_back … isfin.
#f * /3 width=2 by fcla_next, ex_intro/
qed.
+(* Properties with iterated push ********************************************)
+
+lemma isfin_pushs: ∀n,f. 𝐅⦃f⦄ → 𝐅⦃↑*[n]f⦄.
+#n elim n -n /3 width=3 by isfin_push/
+qed.
+
+(* Inversion lemmas with iterated push **************************************)
+
+lemma isfin_inv_pushs: ∀n,g. 𝐅⦃↑*[n]g⦄ → 𝐅⦃g⦄.
+#n elim n -n /3 width=3 by isfin_inv_push/
+qed.
+
+(* Properties with tail *****************************************************)
+
lemma isfin_tl: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫱f⦄.
#f elim (pn_split f) * #g #H #Hf destruct
-/3 width=3 by isfin_fwd_push, isfin_inv_next/
+/3 width=3 by isfin_inv_push, isfin_inv_next/
qed.
(* Inversion lemmas with tail ***********************************************)
#f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/
qed-.
-(* Inversion lemmas with tls ********************************************************)
+(* Inversion lemmas with iterated tail **************************************)
lemma isfin_inv_tls: ∀n,f. 𝐅⦃⫱*[n]f⦄ → 𝐅⦃f⦄.
#n elim n -n /3 width=1 by isfin_inv_tl/
@eq_f //
qed-.
+(* Properties with iterated push ********************************************)
+
+lemma isid_pushs: ∀n,f. 𝐈⦃f⦄ → 𝐈⦃↑*[n]f⦄.
+#n elim n -n /3 width=3 by isid_push/
+qed.
+
+(* Inversion lemmas with iterated push **************************************)
+
+lemma isid_inv_pushs: ∀n,g. 𝐈⦃↑*[n]g⦄ → 𝐈⦃g⦄.
+#n elim n -n /3 width=3 by isid_inv_push/
+qed.
+
(* Properties with tail *****************************************************)
lemma isid_tl: ∀f. 𝐈⦃f⦄ → 𝐈⦃⫱f⦄.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/successorstar_2.ma".
+include "ground_2/relocation/rtmap_eq.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+rec definition nexts (f:rtmap) (n:nat) on n: rtmap ≝ match n with
+[ O ⇒ f | S m ⇒ ⫯(nexts f m) ].
+
+interpretation "nexts (rtmap)" 'SuccessorStar n f = (nexts f n).
+
+(* Basic_inversion lemmas *****************************************************)
+
+lemma eq_inv_nexts_sn: ∀n,f1,g2. ⫯*[n] f1 ≗ g2 →
+ ∃∃f2. f1 ≗ f2 & ⫯*[n] f2 = g2.
+#n elim n -n /2 width=3 by ex2_intro/
+#n #IH #f1 #g2 #H elim (eq_inv_nx … H) -H [|*: // ]
+#f0 #Hf10 #H1 elim (IH … Hf10) -IH -Hf10 #f2 #Hf12 #H2 destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma eq_inv_nexts_dx: ∀n,f2,g1. g1 ≗ ⫯*[n] f2 →
+ ∃∃f1. f1 ≗ f2 & ⫯*[n] f1 = g1.
+#n elim n -n /2 width=3 by ex2_intro/
+#n #IH #f2 #g1 #H elim (eq_inv_xn … H) -H [|*: // ]
+#f0 #Hf02 #H1 elim (IH … Hf02) -IH -Hf02 #f1 #Hf12 #H2 destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma nexts_O: ∀f. f = ⫯*[0] f.
+// qed.
+
+lemma nexts_S: ∀f,n. ⫯⫯*[n] f = ⫯*[⫯n] f.
+// qed.
+
+lemma nexts_eq_repl: ∀n. eq_repl (λf1,f2. ⫯*[n] f1 ≗ ⫯*[n] f2).
+#n elim n -n /3 width=5 by eq_next/
+qed.
+
+(* Advanced properties ******************************************************)
+
+lemma nexts_xn: ∀n,f. ⫯*[n] ⫯f = ⫯*[⫯n] f.
+#n elim n -n //
+qed.
interpretation "pushs (rtmap)" 'LiftStar n f = (pushs f n).
+(* Basic_inversion lemmas *****************************************************)
+
+lemma eq_inv_pushs_sn: ∀n,f1,g2. ↑*[n] f1 ≗ g2 →
+ ∃∃f2. f1 ≗ f2 & ↑*[n] f2 = g2.
+#n elim n -n /2 width=3 by ex2_intro/
+#n #IH #f1 #g2 #H elim (eq_inv_px … H) -H [|*: // ]
+#f0 #Hf10 #H1 elim (IH … Hf10) -IH -Hf10 #f2 #Hf12 #H2 destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma eq_inv_pushs_dx: ∀n,f2,g1. g1 ≗ ↑*[n] f2 →
+ ∃∃f1. f1 ≗ f2 & ↑*[n] f1 = g1.
+#n elim n -n /2 width=3 by ex2_intro/
+#n #IH #f2 #g1 #H elim (eq_inv_xp … H) -H [|*: // ]
+#f0 #Hf02 #H1 elim (IH … Hf02) -IH -Hf02 #f1 #Hf12 #H2 destruct
+/2 width=3 by ex2_intro/
+qed-.
+
(* Basic properties *********************************************************)
lemma pushs_O: ∀f. f = ↑*[0] f.
(**************************************************************************)
include "ground_2/relocation/rtmap_isid.ma".
+include "ground_2/relocation/rtmap_isdiv.ma".
(* RELOCATION MAP ***********************************************************)
(* Basic properties *********************************************************)
-corec lemma sle_refl: ∀f. f ⊆ f.
-#f cases (pn_split f) * #g #H
-[ @(sle_push … H H) | @(sle_next … H H) ] -H //
+corec lemma sle_refl: ∀f1,f2. f1 ≗ f2 → f1 ⊆ f2.
+#f1 #f2 * -f1 -f2
+#f1 #f2 #g1 #g2 #H12 #H1 #H2
+[ @(sle_push … H1 H2) | @(sle_next … H1 H2) ] -H1 -H2 /2 width=1 by/
qed.
(* Basic inversion lemmas ***************************************************)
lapply (isid_inv_push … H ??) -H
/3 width=3 by isid_push/
qed-.
+
+(* Properties with isdiv ****************************************************)
+
+corec lemma sle_isdiv_dx: ∀f2. 𝛀⦃f2⦄ → ∀f1. f1 ⊆ f2.
+#f2 * -f2
+#f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) *
+/3 width=5 by sle_weak, sle_next/
+qed.
+
+(* Inversion lemmas with isdiv **********************************************)
+
+corec lemma sle_inv_isdiv_sn: ∀f1,f2. f1 ⊆ f2 → 𝛀⦃f1⦄ → 𝛀⦃f2⦄.
+#f1 #f2 * -f1 -f2
+#f1 #f2 #g1 #g2 #Hf * * #H
+[1,3: elim (isdiv_inv_push … H) // ]
+lapply (isdiv_inv_next … H ??) -H
+/3 width=3 by isdiv_next/
+qed-.
[ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/
qed-.
-(* Main properties **********************************************************)
-
-axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 →
- ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g.
-
-axiom sor_trans1: ∀f0,f3,f4. f0 ⋓ f3 ≡ f4 →
- ∀f1,f2. f1 ⋓ f2 ≡ f0 →
- ∀f. f2 ⋓ f3 ≡ f → f1 ⋓ f ≡ f4.
-
-axiom sor_trans2: ∀f1,f0,f4. f1 ⋓ f0 ≡ f4 →
- ∀f2, f3. f2 ⋓ f3 ≡ f0 →
- ∀f. f1 ⋓ f2 ≡ f → f ⋓ f3 ≡ f4.
-
(* Properties with tail *****************************************************)
lemma sor_tl: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ⫱f1 ⋓ ⫱f2 ≡ ⫱f.
corec lemma sor_sle_sn: ∀f1,f2. f1 ⊆ f2 → f2 ⋓ f1 ≡ f2.
#f1 #f2 * -f1 -f2 /3 width=7 by sor_pp, sor_nn, sor_np/
qed.
+
+(* Main properties **********************************************************)
+
+axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 →
+ ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g.
+
+axiom sor_trans1: ∀f0,f3,f4. f0 ⋓ f3 ≡ f4 →
+ ∀f1,f2. f1 ⋓ f2 ≡ f0 →
+ ∀f. f2 ⋓ f3 ≡ f → f1 ⋓ f ≡ f4.
+
+axiom sor_trans2: ∀f1,f0,f4. f1 ⋓ f0 ≡ f4 →
+ ∀f2, f3. f2 ⋓ f3 ≡ f0 →
+ ∀f. f1 ⋓ f2 ≡ f → f ⋓ f3 ≡ f4.
+
+corec theorem sor_distr_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g1,g2,g. g1 ⋓ g2 ≡ g →
+ ∀g0. g1 ⋓ g0 ≡ f1 → g2 ⋓ g0 ≡ f2 → g ⋓ g0 ≡ f.
+#f1 #f2 #f cases (pn_split f) * #x #Hx #Hf #g1 #g2 #g #Hg #g0 #Hf1 #Hf2
+[ cases (sor_inv_xxp … Hf … Hx) -Hf #x1 #x2 #Hf #Hx1 #Hx2
+ cases (sor_inv_xxp … Hf1 … Hx1) -f1 #y1 #y0 #Hf1 #Hy1 #Hy0
+ cases (sor_inv_xpp … Hf2 … Hy0 … Hx2) -f2 #y2 #Hf2 #Hy2
+ cases (sor_inv_ppx … Hg … Hy1 Hy2) -g1 -g2 #y #Hg #Hy
+ @(sor_pp … Hy Hy0 Hx) -g -g0 -f /2 width=8 by/
+| cases (pn_split g) * #y #Hy
+ [ cases (sor_inv_xxp … Hg … Hy) -Hg #y1 #y2 #Hg #Hy1 #Hy2
+ cases (sor_xxn_tl … Hf … Hx) * #x1 #x2 #_ #Hx1 #Hx2
+ [ cases (sor_inv_pxn … Hf1 … Hy1 Hx1) -g1 #y0 #Hf1 #Hy0
+ cases (sor_inv_pnx … Hf2 … Hy2 Hy0) -g2 -x2 #x2 #Hf2 #Hx2
+ | cases (sor_inv_pxn … Hf2 … Hy2 Hx2) -g2 #y0 #Hf2 #Hy0
+ cases (sor_inv_pnx … Hf1 … Hy1 Hy0) -g1 -x1 #x1 #Hf1 #Hx1
+ ]
+ lapply (sor_inv_nnn … Hf … Hx1 Hx2 Hx) -f1 -f2 #Hf
+ @(sor_pn … Hy Hy0 Hx) -g -g0 -f /2 width=8 by/
+ | lapply (sor_tl … Hf) -Hf #Hf
+ lapply (sor_tl … Hg) -Hg #Hg
+ lapply (sor_tl … Hf1) -Hf1 #Hf1
+ lapply (sor_tl … Hf2) -Hf2 #Hf2
+ cases (pn_split g0) * #y0 #Hy0
+ [ @(sor_np … Hy Hy0 Hx) /2 width=8 by/
+ | @(sor_nn … Hy Hy0 Hx) /2 width=8 by/
+ ]
+ ]
+]
+qed-.
class "green"
[ { "multiple relocation" * } {
[ { "" * } {
- [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_pushs ( ↑*[?]? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" "rtmap_coafter ( ? ~⊚ ? ≡ ? )" * ]
- [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" * ]
+ [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_pushs ( ↑*[?]? )" "rtmap_nexts ( ⫯*[?]? )"
+ "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_isdiv ( 𝛀⦃?⦄ )"
+ "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )"
+ "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )"
+ "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" "rtmap_coafter ( ? ~⊚ ? ≡ ? )"
+ * ]
+ [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
+ "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
+ * ]
(*
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
<key name="ex">7 3</key>
<key name="ex">7 4</key>
<key name="ex">7 5</key>
+ <key name="ex">7 6</key>
<key name="ex">7 7</key>
<key name="ex">7 9</key>
<key name="ex">7 10</key>
interpretation "multiple existental quantifier (7, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+(* multiple existental quantifier (7, 6) *)
+
+inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝
+ | ex7_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → P6 x0 x1 x2 x3 x4 x5 → ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
(* multiple existental quantifier (7, 7) *)
inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝
projects / helm.git / commitdiff