PcsAnd b "" true false
+psucc
+ppred
+pplus
ple
plt
niter
ntri
+npsucc
nsucc
npred
+nrplus, rplus
nplus
nminus
nmax
PcsPar p "" true false
(semigroup properties)
+(decidability)
NAT-INJECTION
SUCCESSOR
PREDECESSOR
+RIGHT ADDITION
ADDITION
SUBTRACTION
LEFT SUBTRACTION
| "nmax" :: tl -> k T.OK ("nmax" :: outs) tl
| "nminus" :: tl -> k T.OK ("nminus" :: outs) tl
| "nplus" :: tl -> k T.OK ("nplus" :: outs) tl
+ | "nrplus" :: tl -> k T.OK ("nrplus" :: outs) tl
+ | "rplus" :: tl -> k T.OK ("nrplus" :: outs) tl
| "npred" :: tl -> k T.OK ("npred" :: outs) tl
| "nsucc" :: tl -> k T.OK ("nsucc" :: outs) tl
+ | "npsucc" :: tl -> k T.OK ("npsucc" :: outs) tl
| "ntri" :: tl -> k T.OK ("ntri" :: outs) tl
| "niter" :: tl -> k T.OK ("niter" :: outs) tl
| "plt" :: tl -> k T.OK ("plt" :: outs) tl
| "ple" :: tl -> k T.OK ("ple" :: outs) tl
+ | "pplus" :: tl -> k T.OK ("pplus" :: outs) tl
+ | "ppred" :: tl -> k T.OK ("ppred" :: outs) tl
+ | "psucc" :: tl -> k T.OK ("psucc" :: outs) tl
| _ -> k T.OO outs ins
let main =
let step k st outs ins =
if st <> T.OO then k st outs ins else
match ins with
+ | "(decidability)" :: tl -> k T.OK ("(decidability)" :: outs) tl
| "(semigroup" :: "properties)" :: tl -> k T.OK ("properties)" :: "(semigroup" :: outs) tl
| _ -> k T.OO outs ins
| "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
| "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
| "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
+ | "RIGHT" :: "ADDITION" :: tl -> k T.OK ("ADDITION" :: "RIGHT" :: outs) tl
| "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
| "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
| "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl
(* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
-(* Constructions with rplus *************************************************)
+(* Constructions with nrplus ************************************************)
lemma nrplus_inj_sn (p) (n):
ninj (p + n) = ninj p + n.
#n #IH <nplus_succ_dx <IH //
qed.
-(* Constructions with rplus and npsucc **************************************)
+(* Constructions with nrplus and npsucc *************************************)
lemma nrplus_npsucc_sn (m) (n):
npsucc (m + n) = npsucc m + n.
(* ITERATED TAIL FOR STREAMS ************************************************)
-(* Properties with stream_eq *)
+(* Constructions with stream_eq *********************************************)
lemma stream_tls_eq_repl (A) (n):
stream_eq_repl A (λt1,t2. ⫰*[n] t1 ≗ ⫰*[n] t2).
include "ground/notation/functions/append_2.ma".
include "ground/relocation/fr2_map.ma".
-(* APPEND FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* CONCATENATION FOR FINITE RELOCATION MAPS WITH PAIRS **********************)
(* Note: this is compose *)
(*** fr2_append *)
"append (finite relocation maps with pairs)"
'Append f1 f2 = (fr2_append f1 f2).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** mr2_append_nil *)
lemma fr2_append_nil (f2):
include "ground/arith/nat_lt.ma".
include "ground/relocation/fr2_map.ma".
-(* RELATIONAL SUBTRACTION FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* RELATIONAL SUBTRACTION FOR FINITE RELOCATION MAPS WITH PAIRS *************)
(*** minuss *)
inductive fr2_minus: nat → relation fr2_map ≝
"minus (finite relocation maps with pairs)"
'RMinus f1 i f2 = (fr2_minus i f1 f2).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** minuss_inv_nil1 *)
lemma fr2_minus_inv_nil_sn (f2) (i):
include "ground/arith/nat_lt.ma".
include "ground/relocation/fr2_map.ma".
-(* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS ***********)
(*** at *)
inductive fr2_nat: fr2_map → relation nat ≝
"non-negative relational application (finite relocation maps with pairs)"
'RAt l1 f l2 = (fr2_nat f l1 l2).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** at_inv_nil *)
lemma fr2_nat_inv_nil (l1) (l2):
include "ground/relocation/fr2_nat.ma".
-(* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS *******************************************)
+(* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS ***********)
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
(*** at_mono *)
theorem fr2_nat_mono (f) (l):
include "ground/arith/nat_minus_plus.ma".
include "ground/relocation/fr2_map.ma".
-(* ADDITION FOR FINITE RELOCATION MAPS WITH PAIRS ******************************)
+(* ADDITION FOR FINITE RELOCATION MAPS WITH PAIRS ***************************)
(* Note: this is pushs *)
(*** pluss *)
"plus (finite relocation maps with pairs)"
'plus f n = (fr2_plus f n).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** pluss_SO2 *)
lemma fr2_plus_cons_unit (d) (h) (f):
((❨d,h❩;f)+𝟏) = ❨↑d,h❩;f+𝟏.
normalize // qed.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** pluss_inv_nil2 *)
lemma fr2_plus_inv_nil_dx (n) (f):
include "ground/xoa/ex_3_2.ma".
include "ground/relocation/gr_tl.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
(*** after *)
coinductive gr_after: relation3 gr_map gr_map gr_map ≝
"relational composition (generic relocation maps)"
'RAfter f1 f2 f = (gr_after f1 f2 f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** after_inv_ppx *)
lemma gr_after_inv_push_bi:
]
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** after_inv_ppp *)
lemma gr_after_inv_push_bi_push:
include "ground/relocation/gr_after_eq.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
(*** after_trans1 *)
corec theorem gr_after_trans_sn:
]
qed-.
-(* Main inversion lemmas ****************************************************)
+(* Main inversions **********************************************************)
(*** after_mono *)
corec theorem gr_after_mono:
include "ground/relocation/gr_ist_tls.ma".
include "ground/relocation/gr_after_pat_tls.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
(*** H_after_inj *)
definition H_gr_after_inj: predicate gr_map ≝
λf1. 𝐓❪f1❫ →
∀f,f21,f22. f1 ⊚ f21 ≘ f → f1 ⊚ f22 ≘ f → f21 ≡ f22.
-(* Main forward lemmas on istot **************************************************)
+(* Main destructions with gr_ist ********************************************)
(*** after_inj_O_aux *)
corec fact gr_after_inj_unit_aux:
include "ground/relocation/gr_basic.ma".
include "ground/relocation/gr_after_uni.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Properties with gr_basic **********************************************)
+(* Constructions with gr_basic **********************************************)
(*** after_basic_rc *)
lemma after_basic_rc (d2) (d1):
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_after.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
(*** after_eq_repl_back2 *)
corec lemma gr_after_eq_repl_back_sn:
include "ground/relocation/gr_isi.ma".
include "ground/relocation/gr_after_after.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Properties on isid *******************************************************)
+(* Constructions with gr_isi ************************************************)
(*** after_isid_sn *)
corec lemma gr_after_isi_sn:
]
qed.
-(* Destructions on isid *************************************************)
+(* Destructions with gr_isi *************************************************)
(*** after_isid_inv_sn *)
lemma gr_after_isi_inv_sn:
include "ground/relocation/gr_ist.ma".
include "ground/relocation/gr_after_pat.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Forward lemmas on istot **************************************************)
+(* Destructions with gr_ist *************************************************)
(*** after_istot_fwd *)
lemma gr_after_ist_des:
/3 width=8 by gr_after_des_pat, ex2_intro/
qed-.
-(* Inversions with gr_ist *)
+(* Inversions with gr_ist ***************************************************)
(*** after_inv_istot *)
lemma gr_after_inv_ist:
include "ground/relocation/gr_ist_isi.ma".
include "ground/relocation/gr_after_ist.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Forward lemmas on istot and isid **************************************************)
+(* Destructions with gr_ist and gr_isi **************************************)
(*** after_fwd_isid_sn *)
lemma gr_after_des_ist_eq_sn:
include "ground/relocation/gr_isu_uni.ma".
include "ground/relocation/gr_after_uni.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Properties on isuni ******************************************************)
+(* Constructions with gr_isu ************************************************)
(*** after_isid_isuni *)
lemma gr_after_isu_isi_next:
include "ground/relocation/gr_isi_uni.ma".
include "ground/relocation/gr_after_isi.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Properties with gr_nat and uni *)
+(* Constructions with gr_nat and gr_uni *************************************)
(*** after_uni_dx *)
lemma gr_after_nat_uni (l2) (l1):
include "ground/relocation/gr_pat_pat.ma".
include "ground/relocation/gr_after.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Forward lemmas on pat *****************************************************)
+(* Destructions with gr_pat *************************************************)
(*** after_at_fwd *)
lemma gr_after_pat_des (i) (i1):
include "ground/relocation/gr_pat.ma".
include "ground/relocation/gr_after.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Properties on pat and tls ********************************************************)
+(* Constructions with gr_pat and gr_tls *************************************)
(* Note: this requires ↑ on first n *)
(*** after_tls *)
include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_pat.ma".
-(**) (* it should not depend on gr_isi *)
+(* * it should not depend on gr_isi *)
include "ground/relocation/gr_isi_uni.ma".
include "ground/relocation/gr_after_isi.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Properties with pat and uni and tls *******************************************************)
+(* Constructions with gr_pat and gr_uni and gr_tls **************************)
(*** after_uni_succ_dx *)
lemma gr_after_pat_uni (i2) (i1):
]
qed-.
-(* Advanced properties with uni *)
+(* Advanced constructions with gr_uni ***************************************)
(*** after_uni_one_dx *)
lemma gr_after_push_unit:
(**************************************************************************)
include "ground/arith/nat_plus.ma".
-(**) (* it should not depend on gr_isi *)
+(* * it should not depend on gr_isi *)
include "ground/relocation/gr_isi_uni.ma".
include "ground/relocation/gr_after_isi.ma".
-(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************)
-(* Properties on uni ********************************************************)
+(* Constructions with gr_uni ************************************************)
(*** after_uni *)
lemma gr_after_uni (h1) (h2): 𝐮❨h1❩ ⊚ 𝐮❨h2❩ ≘ 𝐮❨h2+h1❩.
include "ground/relocation/gr_pushs.ma".
include "ground/relocation/gr_uni.ma".
-(* BASIC ELEMENTS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* BASIC ELEMENTS FOR GENERIC RELOCATION MAPS *******************************)
definition basic (d) (h): gr_map ≝ ⫯*[d] 𝐮❨h❩.
"basic elements (generic relocation maps)"
'ElementB d h = (basic d h).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** at_basic_succ_sn *)
lemma gr_basic_succ_sn (d) (h): ⫯𝐛❨d,h❩ = 𝐛❨↑d,h❩.
include "ground/xoa/ex_3_2.ma".
include "ground/relocation/gr_tl.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
(*** coafter *)
coinductive gr_coafter: relation3 gr_map gr_map gr_map ≝
"relational co-composition (generic relocation maps)"
'RCoAfter f1 f2 f = (gr_coafter f1 f2 f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** coafter_inv_ppx *)
lemma gr_coafter_inv_push_bi:
]
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** coafter_inv_ppp *)
lemma gr_coafter_inv_push_bi_push:
]
qed-.
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
(*** coafter_inv_tl1 *)
lemma gr_coafter_inv_tl_dx:
#g2 #g1 #g
elim (gr_map_split_tl g1) #H1 #H2
[ /3 width=7 by gr_coafter_refl, ex2_intro/
-| @(ex2_intro … (↑g)) /2 width=7 by gr_coafter_push/ (**) (* full auto fails *)
+| @(ex2_intro … (↑g)) /2 width=7 by gr_coafter_push/ (* * full auto fails *)
]
qed-.
#g2 #g1 #g
elim (gr_map_split_tl g) #H1 #H2
[ /3 width=7 by gr_coafter_refl, ex2_intro/
-| @(ex2_intro … (↑g1)) /2 width=7 by gr_coafter_push/ (**) (* full auto fails *)
+| @(ex2_intro … (↑g1)) /2 width=7 by gr_coafter_push/ (* * full auto fails *)
]
qed-.
include "ground/relocation/gr_coafter_eq.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Main inversion lemmas ****************************************************)
+(* Main inversions **********************************************************)
(*** coafter_mono *)
corec theorem gr_coafter_mono:
include "ground/relocation/gr_ist_tls.ma".
include "ground/relocation/gr_coafter_nat_tls.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
(*** H_coafter_inj *)
definition H_gr_coafter_inj: predicate gr_map ≝
λf1. 𝐓❪f1❫ →
∀f,f21,f22. f1 ~⊚ f21 ≘ f → f1 ~⊚ f22 ≘ f → f21 ≡ f22.
-(* Main Forward lemmas with istot ************************************************)
+(* Main destructions with gr_ist ********************************************)
(*** coafter_inj_O_aux *)
corec fact gr_coafter_inj_unit_aux:
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_coafter.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
(*** coafter_eq_repl_back2 *)
corec lemma gr_coafter_eq_repl_back_sn:
include "ground/relocation/gr_isi_id.ma".
include "ground/relocation/gr_coafter_coafter.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with test for identity ****************************************)
+(* Constructions with gr_isi ************************************************)
(*** coafter_isid_sn *)
corec lemma gr_coafter_isi_sn:
]
qed.
-(* Inversion lemmas with test for identity **********************************)
+(* Inversions with gr_isi ***************************************************)
(*** coafter_isid_inv_sn *)
lemma gr_coafter_isi_inv_sn:
include "ground/relocation/gr_coafter_nat_tls.ma".
include "ground/relocation/gr_coafter_isi.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
(*** H_coafter_isfin2_fwd *)
definition H_gr_coafter_des_ist_isf: predicate gr_map ≝
λf1. ∀f2. 𝐅❪f2❫ → 𝐓❪f1❫ → ∀f. f1 ~⊚ f2 ≘ f → 𝐅❪f❫.
-(* Forward lemmas with ist and isf *)
+(* Destructions with gr_ist and gr_isf **************************************)
(*** coafter_isfin2_fwd_O_aux *)
fact gr_coafter_des_ist_isf_unit_aux:
elim (gr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
elim (gr_coafter_inv_next_sn … Hf … H1) -Hf #g #Hg #H0
lapply (IH … Hg1 … Hg) -i2 -Hg
-/2 width=4 by gr_ist_inv_next, gr_isf_push/ (**) (* full auto fails *)
+/2 width=4 by gr_ist_inv_next, gr_isf_push/ (* * full auto fails *)
qed-.
(*** coafter_isfin2_fwd *)
include "ground/relocation/gr_ist_tls.ma".
include "ground/relocation/gr_coafter_nat_tls.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
(*** H_coafter_fwd_isid2 *)
definition H_gr_coafter_des_ist_sn_isi: predicate gr_map ≝
λf1. ∀f2,f. f1 ~⊚ f2 ≘ f → 𝐓❪f1❫ → 𝐈❪f❫ → 𝐈❪f2❫.
-(* Forward lemmas with ist and isi *)
+(* Destructions with gr_ist and gr_isi **************************************)
(*** coafter_fwd_isid2_O_aux *)
corec fact gr_coafter_des_ist_sn_isi_unit_aux:
#i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
elim (gr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
elim (gr_coafter_inv_next_sn … H … H1) -H #g #Hg #H0
-@(IH … Hg1 … Hg) /2 width=3 by gr_ist_inv_next, gr_isi_inv_push/ (**) (* full auto fails *)
+@(IH … Hg1 … Hg) /2 width=3 by gr_ist_inv_next, gr_isi_inv_push/ (* * full auto fails *)
qed-.
(*** coafter_fwd_isid2 *)
include "ground/relocation/gr_isu_uni.ma".
include "ground/relocation/gr_coafter_uni_pushs.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with test for uniform relocations and isi *****************************)
+(* Constructions with gr_isu and gr_isi *************************************)
(*** coafter_isuni_isid *)
lemma gr_coafter_isu_isi:
include "ground/relocation/gr_nat.ma".
include "ground/relocation/gr_coafter.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with nat and iterated tail ********************************************)
+(* Constructions with gr_nat and gr_tls *************************************)
(*** coafter_tls *)
lemma gr_coafter_tls_bi_tls (n2) (n1):
include "ground/relocation/gr_nat.ma".
include "ground/relocation/gr_coafter.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Forward lemmas with nat and iterated tail and pushs ************************************************)
+(* Destructions with gr_nat and gr_tls and gr_pushs *************************)
(*** coafter_fwd_pushs *)
lemma gr_coafter_des_pushs_dx (n) (m):
include "ground/relocation/gr_pat_tls.ma".
include "ground/relocation/gr_coafter_nat_tls.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with pat and iterated tail ********************************************)
+(* Constructions with gr_pat and gr_tls *************************************)
(* Note: this does not require ↑ first and second j *)
(*** coafter_tls_succ *)
include "ground/relocation/gr_pushs.ma".
include "ground/relocation/gr_uni.ma".
-(**) (* it should not depend on gr_isi *)
+(* * it should not depend on gr_isi *)
include "ground/relocation/gr_coafter_isi.ma".
-(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL CO-COMPOSITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with uniform relocations and pushs **************************************)
+(* Constructions with gr_uni and gr_pushs ***********************************)
(*** coafter_uni_sn *)
lemma gr_coafter_uni_sn_pushs (n):
definition gr_eq_repl_fwd (R:predicate …) ≝
∀f1. R f1 → ∀f2. f2 ≡ f1 → R f2.
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** eq_sym *)
corec lemma gr_eq_sym: symmetric … gr_eq.
gr_eq_repl_back R → gr_eq_repl_fwd R.
/3 width=3 by gr_eq_sym/ qed-.
-(* Alternative definition with stream_eq (specific) ***************************************************)
+(* Alternative definition with stream_eq (specific) *************************)
alias symbol "subseteq" (instance 1) = "relation inclusion".
include "ground/arith/nat_succ.ma".
include "ground/relocation/gr_isi.ma".
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
(*** fcla *)
inductive gr_fcla: relation2 gr_map nat ≝
"finite colength assignment (generic relocation maps)"
'RFunC f n = (gr_fcla f n).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** fcla_inv_px *)
lemma gr_fcla_inv_push (g) (m): 𝐂❪g❫ ≘ m → ∀f. ⫯f = g → 𝐂❪f❫ ≘ m.
]
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** cla_inv_nn *)
lemma gr_cla_inv_next_succ (g) (m): 𝐂❪g❫ ≘ m → ∀f,n. ↑f = g → ↑n = m → 𝐂❪f❫ ≘ n.
include "ground/relocation/gr_isi_eq.ma".
include "ground/relocation/gr_fcla.ma".
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
(*** fcla_eq_repl_back *)
lemma gr_fcla_eq_repl_back (n):
include "ground/relocation/gr_fcla.ma".
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
-(* Main forward lemmas ******************************************************)
+(* Main destructions ********************************************************)
(*** fcla_mono *)
theorem gr_fcla_mono (f):
include "ground/relocation/gr_isi_uni.ma".
include "ground/relocation/gr_fcla.ma".
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
-(* Properties with gr_uni ***************************)
+(* Constructions with gr_uni ************************************************)
(*** fcla_uni *)
lemma gr_fcla_uni (n): 𝐂❪𝐮❨n❩❫ ≘ n.
include "ground/notation/functions/element_i_0.ma".
include "ground/relocation/gr_map.ma".
-(* IDENTITY ELEMENT FOR GENERIC RELOCATION MAPS ******************************************************)
+(* IDENTITY ELEMENT FOR GENERIC RELOCATION MAPS *****************************)
(*** id *)
corec definition gr_id: gr_map ≝ ⫯gr_id.
"identity element (generic relocation streams)"
'ElementI = (gr_id).
-(* Basic properties (specific) *********************************************************)
+(* Basic constructions (specific) *******************************************)
(*** id_rew *)
lemma gr_id_unfold: ⫯𝐢 = 𝐢.
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_id.ma".
-(* IDENTITY ELEMENT FOR GENERIC RELOCATION MAPS ******************************************************)
+(* IDENTITY ELEMENT FOR GENERIC RELOCATION MAPS *****************************)
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
corec lemma gr_id_eq (f): ⫯f ≡ f → 𝐢 ≡ f.
cases gr_id_unfold #Hf
/3 width=5 by gr_eq_inv_push_bi/
qed.
-(* Inversions with gr_eq *)
+(* Inversions with gr_eq ****************************************************)
(* Note: this has the same proof of the previous *)
corec lemma gr_id_inv_eq (f): 𝐢 ≡ f → ⫯f ≡ f.
include "ground/notation/relations/predicate_omega_1.ma".
include "ground/relocation/gr_map.ma".
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
(*** isdiv *)
coinductive gr_isd: predicate gr_map ≝
"divergence condition (generic relocation maps)"
'PredicateOmega f = (gr_isd f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** isdiv_inv_gen *)
lemma gr_isd_inv_gen (g): 𝛀❪g❫ → ∃∃f. 𝛀❪f❫ & ↑f = g.
#f #g #Hf * /2 width=3 by ex2_intro/
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** isdiv_inv_next *)
lemma gr_isd_inv_next (g): 𝛀❪g❫ → ∀f. ↑f = g → 𝛀❪f❫.
include "ground/relocation/gr_tl_eq_eq.ma".
include "ground/relocation/gr_isd.ma".
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
(*** isdiv_eq_repl_back *)
corec lemma gr_isd_eq_repl_back:
gr_eq_repl_fwd … gr_isd.
/3 width=3 by gr_isd_eq_repl_back, gr_eq_repl_sym/ qed-.
-(* Main inversion lemmas with gr_eq ***************)
+(* Main inversions with gr_eq ***********************************************)
(*** isdiv_inv_eq_repl *)
corec theorem gr_isd_inv_eq_repl (g1) (g2): 𝛀❪g1❫ → 𝛀❪g2❫ → g1 ≡ g2.
/3 width=5 by gr_eq_next/
qed-.
-(* Alternative definition with gr_eq ***************************************************)
+(* Alternative definition with gr_eq ****************************************)
(*** eq_next_isdiv *)
corec lemma gr_eq_next_isd (f): ↑f ≡ f → 𝛀❪f❫.
include "ground/relocation/gr_nexts.ma".
include "ground/relocation/gr_isd.ma".
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with iterated next ********************************************)
+(* Constructions with gr_nexts **********************************************)
(*** isdiv_nexts *)
lemma gr_isd_nexts (n) (f): 𝛀❪f❫ → 𝛀❪↑*[n]f❫.
#n @(nat_ind_succ … n) -n /3 width=3 by gr_isd_next/
qed.
-(* Inversion lemmas with iterated next **************************************)
+(* Inversions with gr_nexts *************************************************)
(*** isdiv_inv_nexts *)
lemma gr_isd_inv_nexts (n) (g): 𝛀❪↑*[n]g❫ → 𝛀❪g❫.
include "ground/relocation/gr_tl.ma".
include "ground/relocation/gr_isd.ma".
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
(*** isdiv_tl *)
lemma gr_isd_tl (f): 𝛀❪f❫ → 𝛀❪⫱f❫.
include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_isd_tl.ma".
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
(*** isdiv_tls *)
lemma gr_isd_tls (n) (g): 𝛀❪g❫ → 𝛀❪⫱*[n]g❫.
include "ground/notation/relations/predicate_f_1.ma".
include "ground/relocation/gr_fcla.ma".
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
(*** isfin *)
definition gr_isf: predicate gr_map ≝
"finite colength condition (generic relocation maps)"
'PredicateF f = (gr_isf f).
-(* Basic eliminators ********************************************************)
+(* Basic eliminations *******************************************************)
(*** isfin_ind *)
lemma gr_isf_ind (Q:predicate …):
#n #H elim H -f -n /3 width=2 by ex_intro/
qed-.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** isfin_inv_push *)
lemma gr_isf_inv_push (g): 𝐅❪g❫ → ∀f. ⫯f = g → 𝐅❪f❫.
/2 width=2 by ex_intro/
qed-.
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** isfin_isid *)
lemma gr_isf_isi (f): 𝐈❪f❫ → 𝐅❪f❫.
include "ground/relocation/gr_fcla_eq.ma".
include "ground/relocation/gr_isf.ma".
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
(*** isfin_eq_repl_back *)
lemma gr_isf_eq_repl_back:
include "ground/relocation/gr_isu.ma".
include "ground/relocation/gr_isf.ma".
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with gr_isu *)
+(* Constructions with gr_isu ************************************************)
(*** isuni_fwd_isfin *)
lemma gr_isf_isu (f): 𝐔❪f❫ → 𝐅❪f❫.
include "ground/relocation/gr_pushs.ma".
include "ground/relocation/gr_isf.ma".
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with iterated push ********************************************)
+(* Constructions with gr_pushs **********************************************)
(*** isfin_pushs *)
lemma gr_isf_pushs (n) (f): 𝐅❪f❫ → 𝐅❪⫯*[n]f❫.
#n @(nat_ind_succ … n) -n /3 width=3 by gr_isf_push/
qed.
-(* Inversion lemmas with iterated push **************************************)
+(* Inversions with gr_pushs *************************************************)
(*** isfin_inv_pushs *)
lemma gr_isf_inv_pushs (n) (g): 𝐅❪⫯*[n]g❫ → 𝐅❪g❫.
include "ground/relocation/gr_tl.ma".
include "ground/relocation/gr_isf.ma".
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
(*** isfin_tl *)
lemma gr_isf_tl (f): 𝐅❪f❫ → 𝐅❪⫱f❫.
/3 width=3 by gr_isf_inv_push, gr_isf_inv_next/
qed.
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
(*** isfin_inv_tl *)
lemma gr_isf_inv_tl (g): 𝐅❪⫱g❫ → 𝐅❪g❫.
include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_isf_tl.ma".
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with iterated tail **************************************)
+(* Constructions with gr_tls ************************************************)
lemma gr_isf_tls (n) (f): 𝐅❪f❫ → 𝐅❪⫱*[n]f❫.
#n @(nat_ind_succ … n) -n /3 width=1 by gr_isf_tl/
qed.
-(* Inversion lemmas with iterated tail **************************************)
+(* Inversions with gr_tls ***************************************************)
(*** isfin_inv_tls *)
lemma gr_isf_inv_tls (n) (g): 𝐅❪⫱*[n]g❫ → 𝐅❪g❫.
include "ground/relocation/gr_fcla_uni.ma".
include "ground/relocation/gr_isf.ma".
-(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
+(* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS ********************)
-(* Properties with gr_uni ***************************)
+(* Constructions with gr_uni ************************************************)
(*** isfin_uni *)
lemma gr_isf_uni (n): 𝐅❪𝐮❨n❩❫.
include "ground/notation/relations/predicate_i_1.ma".
include "ground/relocation/gr_map.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
(*** isid *)
coinductive gr_isi: predicate gr_map ≝
"identity condition (generic relocation maps)"
'PredicateI f = (gr_isi f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** isid_inv_gen *)
lemma gr_isi_inv_gen (g): 𝐈❪g❫ → ∃∃f. 𝐈❪f❫ & ⫯f = g.
#f #g #Hf /2 width=3 by ex2_intro/
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** isid_inv_push *)
lemma gr_isi_inv_push (g): 𝐈❪g❫ → ∀f. ⫯f = g → 𝐈❪f❫.
include "ground/relocation/gr_tl_eq_eq.ma".
include "ground/relocation/gr_isi.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
(*** isid_eq_repl_back *)
corec lemma gr_isi_eq_repl_back:
gr_eq_repl_fwd … gr_isi.
/3 width=3 by gr_isi_eq_repl_back, gr_eq_repl_sym/ qed-.
-(* Main inversion lemmas with gr_eq ****************************************************)
+(* Main inversions with gr_eq ***********************************************)
(*** isid_inv_eq_repl *)
corec theorem gr_isi_inv_eq_repl (g1) (g2): 𝐈❪g1❫ → 𝐈❪g2❫ → g1 ≡ g2.
/3 width=5 by gr_eq_push/
qed-.
-(* Alternative definition with gr_eq ***************************************************)
+(* Alternative definition with gr_eq ****************************************)
(*** eq_push_isid *)
corec lemma gr_eq_push_isi (f): ⫯f ≡ f → 𝐈❪f❫.
include "ground/relocation/gr_id.ma".
include "ground/relocation/gr_isi_eq.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties with gr_id *********************************************************)
+(* Constructions with gr_id *************************************************)
(*** id_isid *)
lemma gr_isi_id: 𝐈❪𝐢❫.
/2 width=1 by gr_eq_push_isi/ qed.
-(* Alternative definition with gr_id and gr_eq *******************************************)
+(* Alternative definition with gr_id and gr_eq ******************************)
(*** eq_id_isid *)
lemma gr_eq_id_isi (f): 𝐢 ≡ f → 𝐈❪f❫.
include "ground/relocation/gr_isi_id.ma".
include "ground/relocation/gr_pat_pat_id.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Advanced properties on isid **********************************************)
+(* Advanced constructions with gr_isi ***************************************)
(*** isid_at *)
lemma gr_isi_pat (f): (∀i. @❪i,f❫ ≘ i) → 𝐈❪f❫.
/3 width=1 by gr_eq_id_isi, gr_pat_inv_id/
qed.
-(* Inversion lemmas on pat ****************************************)
+(* Inversions with gr_pat ***************************************************)
(*** isid_inv_at *)
lemma gr_isi_inv_pat (f) (i): 𝐈❪f❫ → @❪i,f❫ ≘ i.
/3 width=3 by gr_isi_inv_eq_id, gr_pat_id, gr_pat_eq_repl_back/
qed-.
-(* Destructions with pat *)
+(* Destructions with gr_pat *************************************************)
(*** isid_inv_at_mono *)
lemma gr_isi_pat_des (f) (i1) (i2): 𝐈❪f❫ → @❪i1,f❫ ≘ i2 → i1 = i2.
include "ground/relocation/gr_pushs.ma".
include "ground/relocation/gr_isi.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ******************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties with gr_pushs *)
+(* Constructions with gr_pushs **********************************************)
(*** isid_pushs *)
lemma gr_isi_pushs (n) (f): 𝐈❪f❫ → 𝐈❪⫯*[n]f❫.
#n @(nat_ind_succ … n) -n /3 width=3 by gr_isi_push/
qed.
-(* Inversion lemmas with iterated push **************************************)
+(* Inversions with gr_pushs *************************************************)
(*** isid_inv_pushs *)
lemma gr_isi_inv_pushs (n) (g): 𝐈❪⫯*[n]g❫ → 𝐈❪g❫.
include "ground/relocation/gr_tl.ma".
include "ground/relocation/gr_isi.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
(*** isid_tl *)
lemma gr_isi_tl (f): 𝐈❪f❫ → 𝐈❪⫱f❫.
include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_isi_tl.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
(*** isid_tls *)
lemma gr_isi_tls (n) (f): 𝐈❪f❫ → 𝐈❪⫱*[n]f❫.
include "ground/relocation/gr_uni.ma".
include "ground/relocation/gr_isi_id.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties with test for identity ****************************************)
+(* Constructions with gr_isi ************************************************)
(*** uni_inv_isid uni_isi *)
lemma gr_uni_isi (f): 𝐮❨𝟎❩ ≡ f → 𝐈❪f❫.
/2 width=1 by gr_eq_id_isi/ qed.
-(* Inversion lemmas with test for identity **********************************)
+(* Inversions with gr_isi ***************************************************)
(*** uni_isid isi_inv_uni *)
lemma gr_isi_inv_uni (f): 𝐈❪f❫ → 𝐮❨𝟎❩ ≡ f.
include "ground/notation/relations/predicate_t_1.ma".
include "ground/relocation/gr_pat.ma".
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
(*** istot *)
definition gr_ist: predicate gr_map ≝
"totality condition (generic relocation maps)"
'PredicateT f = (gr_ist f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** istot_inv_push *)
lemma gr_ist_inv_push (g): 𝐓❪g❫ → ∀f. ⫯f = g → 𝐓❪f❫.
#j #Hg elim (gr_pat_inv_next … Hg … H) -Hg -H /2 width=2 by ex_intro/
qed-.
-(* Properties on tl *********************************************************)
+(* Constructions with gr_tl *************************************************)
(*** istot_tl *)
lemma gr_ist_tl (f): 𝐓❪f❫ → 𝐓❪⫱f❫.
include "ground/relocation/gr_isi_pat.ma".
include "ground/relocation/gr_ist.ma".
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Advanced properties on isid **********************************************)
+(* Advanced constructions with gr_isi ***************************************)
(*** isid_at_total *)
lemma gr_isi_pat_total: ∀f. 𝐓❪f❫ → (∀i1,i2. @❪i1,f❫ ≘ i2 → i1 = i2) → 𝐈❪f❫.
include "ground/relocation/gr_pat_pat.ma".
include "ground/relocation/gr_ist.ma".
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Advanced properties on at ************************************************)
+(* Advanced constructions with gr_pat ***************************************)
(*** at_dec *)
lemma gr_pat_dec (f) (i1) (i2): 𝐓❪f❫ → Decidable (@❪i1,f❫ ≘ i2).
]
qed-.
-(* Main forward lemmas on at ************************************************)
+(* Main destructions with gr_pat ********************************************)
(*** at_ext *)
corec theorem gr_eq_ext_pat (f1) (f2): 𝐓❪f1❫ → 𝐓❪f2❫ →
include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_ist.ma".
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties on tls ********************************************************)
+(* Constructions with gr_tls ************************************************)
(*** istot_tls *)
lemma gr_ist_tls (n) (f): 𝐓❪f❫ → 𝐓❪⫱*[n]f❫.
include "ground/notation/relations/predicate_u_1.ma".
include "ground/relocation/gr_isi.ma".
-(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS *************************)
(*** isuni *)
inductive gr_isu: predicate gr_map ≝
"uniformity condition (generic relocation maps)"
'PredicateU f = (gr_isu f).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** isuni_inv_push *)
lemma gr_isu_inv_push (g): 𝐔❪g❫ → ∀f. ⫯f = g → 𝐈❪f❫.
]
qed-.
-(* Basic forward lemmas *****************************************************)
+(* Basic destructions *******************************************************)
(*** isuni_fwd_push *)
lemma gr_isu_fwd_push (g): 𝐔❪g❫ → ∀f. ⫯f = g → 𝐔❪f❫.
include "ground/relocation/gr_tl.ma".
include "ground/relocation/gr_isu.ma".
-(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
lemma gr_isu_tl (f): 𝐔❪f❫ → 𝐔❪⫱f❫.
#f cases (gr_map_split_tl f) * #H
]
qed.
-(* Advanced inversion lemmas ***************************************************)
+(* Advanced inversions ******************************************************)
(*** isuni_split *)
lemma gr_isu_split (g): 𝐔❪g❫ → ∨∨ (∃∃f. 𝐈❪f❫ & ⫯f = g) | (∃∃f.𝐔❪f❫ & ↑f = g).
include "ground/relocation/gr_isi_uni.ma".
include "ground/relocation/gr_isu.ma".
-(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORMITY CONDITION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with gr_uni **************************************)
+(* Constructions with gr_uni ************************************************)
(*** isuni_uni *)
lemma gr_isu_uni (n): 𝐔❪𝐮❨n❩❫.
gr_eq_repl_fwd … gr_isu.
/3 width=3 by gr_isu_eq_repl_back, gr_eq_repl_sym/ qed-.
-(* Inversion lemmas with gr_uni ********************************)
+(* Inversions with gr_uni ***************************************************)
(*** uni_isuni *)
lemma gr_isu_inv_uni (f): 𝐔❪f❫ → ∃n. 𝐮❨n❩ ≡ f.
"next (generic relocation maps)"
'UpArrow f = (gr_next f).
-(* Basic properties (specific) **********************************************)
+(* Basic constructions (specific) *******************************************)
(*** push_rew *)
lemma gr_push_unfold (f): Ⓕ⨮f = ⫯f.
lemma gr_next_unfold (f): Ⓣ⨮f = ↑f.
// qed.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** injective_push *)
lemma eq_inv_gr_push_bi: injective ? ? gr_push.
include "ground/arith/nat_pred_succ.ma".
include "ground/relocation/gr_pat.ma".
-(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *****************************)
+(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *********************)
definition gr_nat: relation3 gr_map nat nat ≝
λf,l1,l2. @❪↑l1,f❫ ≘ ↑l2.
"relational non-negative application (generic relocation maps)"
'RAtSucc l1 f l2 = (gr_nat f l1 l2).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
lemma gr_nat_refl (f) (g) (k1) (k2):
(⫯f) = g → 𝟎 = k1 → 𝟎 = k2 → @↑❪k1,g❫ ≘ k2.
//
qed.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** gr_nat_inv_ppx *)
lemma gr_nat_inv_zero_push (f) (l1) (l2):
@(ex2_intro … (↓k2)) //
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** gr_nat_inv_ppn *)
lemma gr_nat_inv_zero_push_succ (f) (l1) (l2):
include "ground/relocation/gr_basic.ma".
include "ground/relocation/gr_nat_uni.ma".
-(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *****************************)
+(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *********************)
-(* Properties with gr_basic **********************************************)
+(* Constructions with gr_basic **********************************************)
lemma gr_nat_basic_lt (m) (n) (l):
l < m → @↑❪l, 𝐛❨m,n❩❫ ≘ l.
/3 width=7 by gr_nat_push/
qed.
-(* Inversion lemmas with gr_basic ****************************************)
+(* Inversions with gr_basic *************************************************)
lemma gr_nat_basic_inv_lt (m) (n) (l) (k):
l < m → @↑❪l, 𝐛❨m,n❩❫ ≘ k → l = k.
include "ground/relocation/gr_pat_uni.ma".
include "ground/relocation/gr_nat_nat.ma".
-(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *****************************)
+(* NON-NEGATIVE APPLICATION FOR GENERIC RELOCATION MAPS *********************)
-(* Properties with uniform relocations **************************************)
+(* Constructions with gr_uni ************************************************)
lemma gr_nat_uni (n) (l):
@↑❪l,𝐮❨n❩❫ ≘ l+n.
/2 width=1 by gr_nat_pred_bi/
qed.
-(* Inversion lemmas with uniform relocations ********************************)
+(* Inversions with gr_uni ***************************************************)
lemma gr_nat_inv_uni (n) (l) (k):
@↑❪l,𝐮❨n❩❫ ≘ k → k = l+n.
include "ground/arith/nat_succ_iter.ma".
include "ground/relocation/gr_map.ma".
-(* ITERATED NEXT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED NEXT FOR GENERIC RELOCATION MAPS ********************************)
(*** nexts *)
definition gr_nexts (f:gr_map) (n:nat) ≝
"iterated next (generic relocation maps)"
'UpArrowStar n f = (gr_nexts f n).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** nexts_O *)
lemma gr_nexts_zero:
include "ground/relocation/gr_eq.ma".
include "ground/relocation/gr_nexts.ma".
-(* ITERATED NEXT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED NEXT FOR GENERIC RELOCATION MAPS ********************************)
-(* Properties with gr_eq ******************************************************)
+(* Constructions with gr_eq *************************************************)
(*** nexts_eq_repl *)
lemma gr_nexts_eq_repl (n):
include "ground/arith/pnat.ma".
include "ground/relocation/gr_tl.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
(*** at *)
coinductive gr_pat: relation3 gr_map pnat pnat ≝
∀jf,jg,j. @❪jf,f2❫ ≘ j → @❪jg,g2❫ ≘ j →
∃∃j0. @❪j0,f1❫ ≘ jf & @❪j0,g1❫ ≘ jg.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** at_inv_ppx *)
lemma gr_pat_inv_unit_push (f) (i1) (i2):
]
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** at_inv_ppn *)
lemma gr_pat_inv_unit_push_succ (f) (i1) (i2):
include "ground/relocation/gr_nat_basic.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with gr_basic **********************************************)
+(* Constructions with gr_basic **********************************************)
(*** at_basic_lt *)
lemma gr_pat_basic_lt (m) (n) (i):
/3 width=1 by gr_nat_basic_ge, nlt_inv_succ_dx/
qed.
-(* Inversion lemmas with gr_basic ****************************************)
+(* Inversions with gr_basic *************************************************)
(*** at_basic_inv_lt *)
lemma gr_pat_basic_inv_lt (m) (n) (i) (j):
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_pat_lt.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
(*** at_eq_repl_back *)
corec lemma gr_pat_eq_repl_back (i1) (i2):
]
qed.
-(* Inversions with gr_eq *)
+(* Inversions with gr_eq ****************************************************)
corec lemma gr_pat_inv_eq (f):
(∀i. @❪i,f❫ ≘ i) → ⫯f ≡ f.
include "ground/relocation/gr_id_eq.ma".
include "ground/relocation/gr_pat_eq.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties on id ************************************************)
+(* Constructions with gr_id *************************************************)
(*** id_at *)
lemma gr_pat_id (i): @❪i,𝐢❫ ≘ i.
/2 width=1 by gr_pat_eq, gr_eq_refl/ qed.
-(* Inversions with id *)
+(* Inversions with gr_id ****************************************************)
(*** id_inv_at *)
lemma gr_pat_inv_id (f):
include "ground/arith/pnat_lt.ma".
include "ground/relocation/gr_pat.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Forward lemmas with plt and ple *****************************************************)
+(* Destructions with plt and ple ********************************************)
(*** at_increasing *)
lemma gr_pat_increasing (i2) (i1) (f):
#H elim (plt_ge_false … H) -H //
qed-.
-(* Properties with ple *********************************************************)
+(* Constructions with ple ***************************************************)
(*** at_le_ex *)
lemma gr_pat_le_ex (j2) (i2) (f):
include "ground/arith/pnat_lt_pred.ma".
include "ground/relocation/gr_pat.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
(*** at_monotonic *)
theorem gr_pat_monotonic:
include "ground/relocation/gr_pat_id.ma".
include "ground/relocation/gr_pat_pat.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Advanced Forward lemmas on id ********************************************)
+(* Advanced destructions with gr_id *****************************************)
(*** at_id_fwd *)
lemma gr_pat_id_des (i1) (i2):
@❪i1,𝐢❫ ≘ i2 → i1 = i2.
/2 width=4 by gr_pat_mono/ qed-.
-(* Main properties on id ****************************************************)
+(* Main constructions with gr_id ********************************************)
(*** at_div_id_dx *)
theorem gr_pat_div_id_dx (f):
include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_pat_eq.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties on tls ********************************************************)
+(* Constructions with gr_tls ************************************************)
(* Note: this requires ↑ on first n *)
(*** at_pxx_tls *)
]
qed-.
-(* Inversion lemmas with tls ************************************************)
+(* Inversions with gr_tls ***************************************************)
(* Note: this does not require ↑ on second and third p *)
(*** at_inv_nxx *)
include "ground/relocation/gr_uni.ma".
include "ground/relocation/gr_pat_pat_id.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with uniform relocations **************************************)
+(* Constructions with gr_uni ************************************************)
(*** at_uni *)
lemma gr_pat_uni (n) (i):
/2 width=5 by gr_pat_next/
qed.
-(* Inversion lemmas with uniform relocations ********************************)
+(* Inversions with gr_uni ***************************************************)
(*** at_inv_uni *)
lemma gr_pat_inv_uni (n) (i) (j):
include "ground/arith/nat_succ_iter.ma".
include "ground/relocation/gr_map.ma".
-(* ITERATED PUSH FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED PUSH FOR GENERIC RELOCATION MAPS ********************************)
(*** pushs *)
definition gr_pushs (f:gr_map) (n:nat) ≝
"iterated push (generic relocation maps)"
'UpSpoonStar n f = (gr_pushs f n).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** pushs_O *)
lemma gr_pushs_zero:
include "ground/relocation/gr_eq.ma".
include "ground/relocation/gr_pushs.ma".
-(* ITERATED PUSH FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED PUSH FOR GENERIC RELOCATION MAPS ********************************)
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
(*** pushs_eq_repl *)
lemma gr_pushs_eq_repl (n):
include "ground/notation/relations/rintersection_3.ma".
include "ground/relocation/gr_tl.ma".
-(* RELATIONAL INTERSECTION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL INTERSECTION FOR GENERIC RELOCATION MAPS **********************)
(*** sand *)
coinductive gr_sand: relation3 gr_map gr_map gr_map ≝
"relational intersection (generic relocation maps)"
'RIntersection f1 f2 f = (gr_sand f1 f2 f).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** sand_refl *)
corec lemma gr_sand_idem:
] /2 width=7 by/
qed-.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** sand_inv_ppx *)
lemma gr_sand_inv_push_bi:
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_sand.ma".
-(* RELATIONAL INTERSECTION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL INTERSECTION FOR GENERIC RELOCATION MAPS **********************)
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
(*** sand_eq_repl_back1 *)
corec lemma gr_sand_eq_repl_back_sn:
include "ground/notation/relations/parallel_2.ma".
include "ground/relocation/gr_tl.ma".
-(* DISJOINTNESS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DISJOINTNESS FOR GENERIC RELOCATION MAPS *********************************)
(*** sdj *)
coinductive gr_sdj: relation gr_map ≝
"disjointness (generic relocation maps)"
'Parallel f1 f2 = (gr_sdj f1 f2).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** sdj_sym *)
corec lemma gr_sdj_sym:
/2 width=1 by/
qed-.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** sdj_inv_pp *)
lemma gr_sdj_inv_push_bi:
]
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** sdj_inv_nx *)
lemma gr_sdj_inv_next_sn:
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_sdj.ma".
-(* DISJOINTNESS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DISJOINTNESS FOR GENERIC RELOCATION MAPS *********************************)
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
(*** sdj_eq_repl_back1 *)
corec lemma gr_sdj_eq_repl_back_sn:
include "ground/relocation/gr_isi.ma".
include "ground/relocation/gr_sdj.ma".
-(* DISJOINTNESS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DISJOINTNESS FOR GENERIC RELOCATION MAPS *********************************)
-(* Properties with isid *****************************************************)
+(* Constructions with gr_isi ************************************************)
(*** sdj_isid_dx *)
corec lemma gr_sdj_isi_dx:
/3 width=5 by gr_sdj_push_next, gr_sdj_push_bi/
qed.
-(* Inversion lemmas with isid ***********************************************)
+(* Inversions with gr_isi ***************************************************)
(*** sdj_inv_refl *)
corec lemma gr_sdj_inv_refl:
include "ground/relocation/gr_tl.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
(*** sle *)
coinductive gr_sle: relation gr_map ≝
"inclusion (generic relocation maps)"
'subseteq f1 f2 = (gr_sle f1 f2).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** sle_refl *)
corec lemma gr_sle_refl:
[ @(gr_sle_push … H H) | @(gr_sle_next … H H) ] -H //
qed.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** sle_inv_xp *)
lemma gr_sle_inv_push_dx:
]
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** sle_inv_pp *)
lemma gr_sle_inv_push_bi:
/3 width=3 by ex2_intro, or_introl, or_intror/
qed-.
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
(*** sle_px_tl *)
lemma gr_sle_push_sn_tl:
]
qed.
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
(*** sle_inv_tl_sn *)
lemma gr_sle_inv_tl_sn:
(**************************************************************************)
include "ground/relocation/gr_sle.ma".
-(**) (* this should go first *)
+(* * this should go first *)
include "ground/relocation/gr_tl_eq.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
(*** sle_eq_repl_back1 *)
corec lemma gr_sle_eq_repl_back_sn:
include "ground/relocation/gr_isd.ma".
include "ground/relocation/gr_sle.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
-(* Properties with isdiv ****************************************************)
+(* Constructions with gr_isd ************************************************)
(*** sle_isdiv_dx *)
corec lemma gr_sle_isd_dx:
/3 width=5 by gr_sle_weak, gr_sle_next/
qed.
-(* Inversion lemmas with isdiv **********************************************)
+(* Inversions with gr_isd ***************************************************)
(*** sle_inv_isdiv_sn *)
corec lemma gr_sle_inv_isd_sn:
include "ground/relocation/gr_isi.ma".
include "ground/relocation/gr_sle.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
-(* Properties with isid *****************************************************)
+(* Constructions with gr_isi ************************************************)
(*** sle_isid_sn *)
corec lemma gr_sle_isi_sn:
/3 width=5 by gr_sle_weak, gr_sle_push/
qed.
-(* Inversion lemmas with isid ***********************************************)
+(* Inversions with gr_isi ***************************************************)
(*** sle_inv_isid_dx *)
corec lemma gr_sle_inv_isi_dx:
include "ground/relocation/gr_pushs.ma".
include "ground/relocation/gr_sle.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
-(* Properties with iterated push ********************************************)
+(* Constructions with gr_pushs **********************************************)
(*** sle_pushs *)
lemma gr_sle_pushs:
include "ground/relocation/gr_sle.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
(*** sle_trans *)
corec theorem gr_sle_trans:
include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_sle.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
(*** sle_tls *)
lemma gr_sle_tls:
include "ground/xoa/ex_3_2.ma".
include "ground/relocation/gr_tl.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
(*** sor *)
coinductive gr_sor: relation3 gr_map gr_map gr_map ≝
"relational union (generic relocation maps)"
'RUnion f1 f2 f = (gr_sor f1 f2 f).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** sor_idem *)
corec lemma gr_sor_idem:
[ @gr_sor_push_bi | @gr_sor_push_next | @gr_sor_next_push | @gr_sor_next_bi ] /2 width=7 by/
qed-.
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** sor_inv_ppx *)
lemma gr_sor_inv_push_bi:
/2 width=3 by ex2_intro/
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** sor_inv_ppn *)
lemma gr_sor_inv_push_bi_next:
]
qed-.
-(* Properties with tail *****************************************************)
+(* Constructions with gr_tl *************************************************)
(*** sor_tl *)
lemma gr_sor_tl:
/3 width=5 by ex3_2_intro/
qed-.
-(* Inversion lemmas with tail ***********************************************)
+(* Inversions with gr_tl ****************************************************)
(*** sor_inv_tl_sn *)
lemma gr_sor_inv_tl_sn:
include "ground/relocation/gr_coafter_ist_isi.ma".
include "ground/relocation/gr_sor_isi.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Properties with coafter and ist and isf ****************************************************)
+(* Constructions with gr_coafter and gr_ist and gr_isf **********************)
(*** coafter_sor *)
lemma gr_sor_coafter_dx_tans:
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_sor.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
(*** sor_eq_repl_back1 *)
corec lemma gr_sor_eq_repl_back_sn:
include "ground/relocation/gr_fcla_eq.ma".
include "ground/relocation/gr_sor_isi.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Properties with finite colength assignment *******************************)
+(* Constructions with gr_fcla ***********************************************)
(*** sor_fcla_ex *)
lemma gr_sor_fcla_bi:
∃∃f,n. f1 ⋓ f2 ≘ f & 𝐂❪f❫ ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
#f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by gr_sor_isi_sn, ex4_2_intro/
#f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by gr_fcla_push, gr_fcla_next, ex4_2_intro, gr_sor_isi_dx/
-#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (**) (* full auto fails *)
+#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (* * full auto fails *)
[ /3 width=7 by gr_fcla_next, gr_sor_push_next, nle_max_sn_succ_dx, nle_succ_bi, ex4_2_intro/
| /4 width=7 by gr_fcla_next, gr_sor_next_bi, nle_succ_dx, nle_succ_bi, ex4_2_intro/
| /3 width=7 by gr_fcla_push, gr_sor_push_bi, ex4_2_intro/
]
qed-.
-(* Forward lemmas with finite colength **************************************)
+(* Destructions with gr_fcla ************************************************)
(*** sor_fcla *)
lemma gr_sor_inv_fcla_bi:
/4 width=6 by gr_sor_mono, gr_fcla_eq_repl_back, ex3_intro/
qed-.
-(* Forward lemmas with finite colength **************************************)
+(* Destructions with gr_fcla ************************************************)
(*** sor_fwd_fcla_sn_ex *)
lemma gr_sor_des_fcla_sn:
include "ground/relocation/gr_isf_eq.ma".
include "ground/relocation/gr_sor_fcla.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Properties with test for finite colength *********************************)
+(* Constructions with gr_isf ************************************************)
(*** sor_isfin_ex *)
lemma gr_sor_isf_bi:
/3 width=4 by ex2_intro, ex_intro/
qed-.
-(* Forward lemmas with test for finite colength *****************************)
+(* Destructions with gr_isf *************************************************)
(*** sor_fwd_isfin_sn *)
lemma gr_sor_des_isf_sn:
elim (gr_sor_des_fcla_dx … Hf … H) -f -f1 /2 width=2 by ex_intro/
qed-.
-(* Inversion lemmas with test for finite colength ***************************)
+(* Inversions with gr_isf ***************************************************)
(*** sor_isfin *)
lemma gr_sor_inv_isf_bi:
include "ground/relocation/gr_sor_eq.ma".
include "ground/relocation/gr_sor_sor.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Properties with test for identity *****************************************)
+(* Constructions with gr_isi ************************************************)
(*** sor_isid_sn *)
corec lemma gr_sor_isi_sn:
/4 width=3 by gr_sor_eq_repl_back_dx, gr_sor_eq_repl_back_sn, gr_isi_inv_eq_repl/ qed.
-(* Forward lemmas with test for identity **********************************)
+(* Destructions with gr_isi *************************************************)
(*** sor_fwd_isid1 *)
corec lemma gr_sor_des_isi_sn:
cases (gr_isi_inv_next … Hg … H)
qed-.
-(* Inversion lemmas with test for identity **********************************)
+(* Inversions with gr_isi ***************************************************)
(*** sor_isid_inv_sn *)
lemma gr_sor_inv_isi_sn:
include "ground/relocation/gr_sle_sle.ma".
include "ground/relocation/gr_sor.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Inversion lemmas with inclusion ******************************************)
+(* Inversions with gr_sle ***************************************************)
(*** sor_inv_sle_sn *)
corec lemma gr_sor_inv_sle_sn:
axiom gr_sor_inv_sle_bi:
∀f1,f2,f. f1 ⋓ f2 ≘ f → ∀g. f1 ⊆ g → f2 ⊆ g → f ⊆ g.
-(* Properties with inclusion ************************************************)
+(* Constructions with gr_sle ************************************************)
(*** sor_sle_dx *)
corec lemma gr_sor_sle_dx:
include "ground/relocation/gr_eq.ma".
include "ground/relocation/gr_sor.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Main inversion lemmas ****************************************************)
+(* Main inversions **********************************************************)
(*** sor_mono *)
corec theorem gr_sor_mono:
/3 width=5 by gr_eq_push, gr_eq_next/
qed-.
-(* Main properties **********************************************************)
+(* Main constructions *******************************************************)
(*** sor_assoc_dx *)
axiom gr_sor_assoc_dx:
include "ground/relocation/gr_sle.ma".
include "ground/relocation/gr_sor.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Main inversion lemmas with inclusion ****************************************************)
+(* Main inversions with gr_sle **********************************************)
(*** monotonic_sle_sor *)
axiom gr_sor_monotonic_sle:
include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_sor.ma".
-(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* RELATIONAL UNION FOR GENERIC RELOCATION MAPS *****************************)
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
(*** sor_tls *)
lemma gr_sor_tls:
include "ground/lib/stream_hdtl.ma".
include "ground/relocation/gr_map.ma".
-(* TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
(*** tl *)
definition gr_tl (f): gr_map ≝ ⫰f.
"tail (generic relocation maps)"
'DropPred f = (gr_tl f).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** tl_push_rew *)
lemma gr_tl_push (f): f = ⫱⫯f.
lemma gr_tl_next (f): f = ⫱↑f.
// qed.
-(* Basic eliminators ********************************************************)
+(* Basic eliminations *******************************************************)
(*** pn_split gr_map_split *)
lemma gr_map_split_tl (f): ∨∨ ⫯⫱f = f | ↑⫱f = f.
include "ground/relocation/gr_eq.ma".
include "ground/relocation/gr_tl.ma".
-(* TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
-(* Properties with gr_eq *)
+(* Constructions with gr_eq *************************************************)
(*** eq_refl *)
corec lemma gr_eq_refl: reflexive … gr_eq.
#f1 #f2 * -f1 -f2 //
qed.
-(* Inversion lemmas with gr_eq ***************************************************)
+(* Inversions with gr_eq ****************************************************)
(*** eq_inv_gen *)
lemma gr_eq_inv_gen (g1) (g2):
/3 width=1 by and3_intro, or_introl, or_intror/
qed-.
-(* Advanced Inversion lemmas with gr_eq *)
+(* Advanced inversions with gr_eq *******************************************)
(*** gr_eq_inv_px *)
lemma gr_eq_inv_push_sn (g1) (g2):
include "ground/relocation/gr_tl_eq.ma".
-(* TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
-(* Main properties with gr_eq **********************************************************)
+(* Main constructions with gr_eq ********************************************)
(*** eq_trans *)
corec theorem gr_eq_trans: Transitive … gr_eq.
include "ground/lib/stream_tls.ma".
include "ground/relocation/gr_tl.ma".
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
(*** tls *)
definition gr_tls (n) (f:gr_map) ≝ ⫰*[n]f.
"iterated tail (generic relocation maps)"
'DropPreds n f = (gr_tls n f).
-(* Basic properties (specific) *********************************************************)
+(* Basic constructions (specific) *******************************************)
(*** tls_O *)
lemma gr_tls_zero (f): f = ⫱*[𝟎] f.
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_tls.ma".
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
-(* Properties with gr_eq ******************************************************)
+(* Constructions with gr_eq *************************************************)
(*** tls_eq_repl *)
lemma gr_tls_eq_repl (n):
include "ground/relocation/gr_nexts.ma".
include "ground/relocation/gr_tls_eq.ma".
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
-(* Inversion lemmas with gr_nexts and gr_eq *****************************************************)
+(* Inversions with gr_nexts and gr_eq ***************************************)
(*** eq_inv_nexts_sn *)
lemma gr_eq_inv_nexts_sn (n):
include "ground/relocation/gr_pushs.ma".
include "ground/relocation/gr_tls.ma".
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
-(* Properties with pushs ****************************************************)
+(* Constructions with gr_pushs **********************************************)
(*** tls_pushs *)
lemma gr_tls_pushs (n) (f): f = ⫱*[n] ⫯*[n] f.
include "ground/relocation/gr_tls_eq.ma".
include "ground/relocation/gr_pushs.ma".
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
-(* Inversion lemmas with gr_pushs and gr_eq *****************************************************)
+(* Inversions with gr_pushs and gr_eq ***************************************)
(*** eq_inv_pushs_sn *)
lemma gr_eq_inv_pushs_sn (n):
include "ground/relocation/gr_nexts.ma".
include "ground/relocation/gr_id.ma".
-(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS *****************************)
(*** uni *)
definition gr_uni (n) ≝ ↑*[n] 𝐢.
"uniform elements (generic relocation maps)"
'ElementU n = (gr_uni n).
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** uni_zero *)
lemma gr_uni_zero: 𝐢 = 𝐮❨𝟎❩.
include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_uni.ma".
-(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS *****************************)
-(* Inversion lemmas with gr_eq ***************************************************)
+(* Inversions with gr_eq ****************************************************)
(*** uni_inv_push_dx *)
lemma gr_eq_inv_uni_push (n) (g): 𝐮❨n❩ ≡ ⫯g → ∧∧ 𝟎 = n & 𝐢 ≡ g.
lemma gr_eq_inv_next_uni (n) (g): ↑g ≡ 𝐮❨n❩ → ∧∧ 𝐮❨↓n❩ ≡ g & ↑↓n = n.
/3 width=1 by gr_eq_inv_uni_next, gr_eq_sym/ qed-.
-(* Inversion lemmas with id and gr_eq *)
+(* Inversions with gr_id and gr_eq ******************************************)
(*** uni_inv_id_dx *)
lemma gr_eq_inv_uni_id (n): 𝐮❨n❩ ≡ 𝐢 → 𝟎 = n.
projects / helm.git / commitdiff