X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_shift.ma;h=cb2c3828425b9902209891b7148d79899c5f6b0e;hb=89ea663d91904f483f8248cfaeaed5eda8715da2;hp=f7c56a3e1f50438a7734b09959d12295237626b7;hpb=9a6cf8c3b53fe33515acd1aef8e7c7a10d71ae71;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma index f7c56a3e1..cb2c38284 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma @@ -18,14 +18,14 @@ include "ground_2/steps/rtc_isrt.ma". (* RT-TRANSITION COUNTER ****************************************************) definition shift (c:rtc): rtc ≝ match c with -[ mk_rtc ri rs ti ts ⇒ 〈ri+rs, 0, ti+ts, 0〉 ]. +[ mk_rtc ri rs ti ts ⇒ 〈ri∨rs, 0, ti∨ts, 0〉 ]. interpretation "shift (rtc)" 'Drop c = (shift c). (* Basic properties *********************************************************) -lemma shift_rew: ∀ri,rs,ti,ts. 〈ri+rs, 0, ti+ts, 0〉 = ↓〈ri, rs, ti, ts〉. +lemma shift_rew: ∀ri,rs,ti,ts. 〈ri∨rs, 0, ti∨ts, 0〉 = ↓〈ri, rs, ti, ts〉. normalize // qed. @@ -35,7 +35,7 @@ lemma shift_O: 𝟘𝟘 = ↓𝟘𝟘. (* Basic inversion properties ***********************************************) lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri, rs, ti, ts〉 = ↓c → - ∃∃ri0,rs0,ti0,ts0. ri0+rs0 = ri & 0 = rs & ti0+ts0 = ti & 0 = ts & + ∃∃ri0,rs0,ti0,ts0. (ri0∨rs0) = ri & 0 = rs & (ti0∨ts0) = ti & 0 = ts & 〈ri0, rs0, ti0, ts0〉 = c. #ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0