X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ffr2_append.ma;h=b50a5cfa86dc2a7e38de61db956140f3a018c248;hb=12dc655b7f5321b33b93a310d53e23e60e090caa;hp=c2d7b9ed7d4ad532e173ca037626e5f87ab2b925;hpb=dd41efaab7f147d5673cc30a27d36375f9b52c9d;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma index c2d7b9ed7..b50a5cfa8 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/notation/functions/append_2.ma". +include "ground/notation/functions/double_semicolon_2.ma". include "ground/relocation/fr2_map.ma". (* CONCATENATION FOR FINITE RELOCATION MAPS WITH PAIRS **********************) @@ -20,22 +20,22 @@ include "ground/relocation/fr2_map.ma". (* Note: this is compose *) (*** fr2_append *) rec definition fr2_append f1 f2 on f1 ≝ match f1 with -[ fr2_nil ⇒ f2 -| fr2_cons d h f1 ⇒ ❨d, h❩; fr2_append f1 f2 +[ fr2_empty ⇒ f2 +| fr2_lcons d h f1 ⇒ ❨d, h❩; fr2_append f1 f2 ]. interpretation "append (finite relocation maps with pairs)" - 'Append f1 f2 = (fr2_append f1 f2). + 'DoubleSemicolon f1 f2 = (fr2_append f1 f2). (* Basic constructions ******************************************************) (*** mr2_append_nil *) -lemma fr2_append_nil (f2): - f2 = ◊ @@ f2. +lemma fr2_append_empty (f2): + f2 = 𝐞 ;; f2. // qed. (*** mr2_append_cons *) -lemma fr2_append_cons (d) (h) (f1) (f2): - ❨d, h❩; (f1 @@ f2) = (❨d, h❩; f1) @@ f2. +lemma fr2_append_lcons (d) (h) (f1) (f2): + ❨d, h❩; (f1 ;; f2) = (❨d, h❩; f1) ;; f2. // qed.