1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/notation/functions/updownarrowstar_1.ma".
16 include "ground_2/steps/rtc_isrt.ma".
18 (* RT-TRANSITION COUNTER ****************************************************)
20 definition shift (c:rtc): rtc ≝ match c with
21 [ mk_rtc ri rs ti ts ⇒ 〈ri∨rs,0,ti∨ts,0〉 ].
23 interpretation "shift (rtc)"
24 'UpDownArrowStar c = (shift c).
26 (* Basic properties *********************************************************)
28 lemma shift_rew: ∀ri,rs,ti,ts. 〈ri∨rs,0,ti∨ts,0〉 = ↕*〈ri,rs,ti,ts〉.
32 lemma shift_O: 𝟘𝟘 = ↕*𝟘𝟘.
35 (* Basic inversion properties ***********************************************)
37 lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri,rs,ti,ts〉 = ↕*c →
38 ∃∃ri0,rs0,ti0,ts0. (ri0∨rs0) = ri & 0 = rs & (ti0∨ts0) = ti & 0 = ts &
39 〈ri0,rs0,ti0,ts0〉 = c.
40 #ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <shift_rew #H destruct
41 /2 width=7 by ex5_4_intro/
44 (* Properties with test for costrained rt-transition counter ****************)
46 lemma isr_shift: ∀c. 𝐑𝐓⦃0,c⦄ → 𝐑𝐓⦃0,↕*c⦄.
47 #c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/
50 (* Inversion properties with test for costrained rt-counter *****************)
52 lemma isrt_inv_shift: ∀n,c. 𝐑𝐓⦃n,↕*c⦄ → 𝐑𝐓⦃0,c⦄ ∧ 0 = n.
54 elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3
55 elim (max_inv_O3 … H1) -H1 /3 width=3 by ex1_2_intro, conj/
58 lemma isr_inv_shift: ∀c. 𝐑𝐓⦃0,↕*c⦄ → 𝐑𝐓⦃0,c⦄.
59 #c #H elim (isrt_inv_shift … H) -H //