(* *)
(**************************************************************************)
-include "ground_2/notation/functions/drop_1.ma".
+include "ground_2/xoa/ex_5_4.ma".
+include "ground_2/notation/functions/updownarrowstar_1.ma".
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).
+ 'UpDownArrowStar 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.
-lemma shift_O: ð\9d\9f\98ð\9d\9f\98 = â\86\93𝟘𝟘.
+lemma shift_O: ð\9d\9f\98ð\9d\9f\98 = â\86\95*𝟘𝟘.
// qed.
(* Basic inversion properties ***********************************************)
-lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri, rs, ti, ts〉 = ↓c →
+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〉 = c.
+ 〈ri0,rs0,ti0,ts0〉 = c.
#ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <shift_rew #H destruct
/2 width=7 by ex5_4_intro/
qed-.
(* Properties with test for costrained rt-transition counter ****************)
-lemma isr_shift: â\88\80c. ð\9d\90\91ð\9d\90\93â¦\830, câ¦\84 â\86\92 ð\9d\90\91ð\9d\90\93â¦\830, â\86\93câ¦\84.
+lemma isr_shift: â\88\80c. ð\9d\90\91ð\9d\90\93â\9dª0,câ\9d« â\86\92 ð\9d\90\91ð\9d\90\93â\9dª0,â\86\95*câ\9d«.
#c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/
qed.
(* Inversion properties with test for costrained rt-counter *****************)
-lemma isrt_inv_shift: â\88\80n,c. ð\9d\90\91ð\9d\90\93â¦\83n, â\86\93câ¦\84 â\86\92 ð\9d\90\91ð\9d\90\93â¦\830, câ¦\84 ∧ 0 = n.
+lemma isrt_inv_shift: â\88\80n,c. ð\9d\90\91ð\9d\90\93â\9dªn,â\86\95*câ\9d« â\86\92 ð\9d\90\91ð\9d\90\93â\9dª0,câ\9d« ∧ 0 = n.
#n #c * #ri #rs #H
elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3
elim (max_inv_O3 … H1) -H1 /3 width=3 by ex1_2_intro, conj/
qed-.
-lemma isr_inv_shift: â\88\80c. ð\9d\90\91ð\9d\90\93â¦\830, â\86\93câ¦\84 â\86\92 ð\9d\90\91ð\9d\90\93â¦\830, câ¦\84.
+lemma isr_inv_shift: â\88\80c. ð\9d\90\91ð\9d\90\93â\9dª0,â\86\95*câ\9d« â\86\92 ð\9d\90\91ð\9d\90\93â\9dª0,câ\9d«.
#c #H elim (isrt_inv_shift … H) -H //
qed-.