matita/matita/contribs/lambdadelta/ground/counters/rtc_shift.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground/xoa/ex_5_4.ma".
  16 include "ground/notation/functions/updownarrowstar_1.ma".
  17 include "ground/arith/nat_max.ma".
  18 include "ground/counters/rtc.ma".
  19
  20 (* SHIFT FOR RT-TRANSITION COUNTERS *****************************************)
  21
  22 definition rtc_shift (c:rtc): rtc ≝
  23 match c with
  24 [ mk_rtc ri rs ti ts ⇒ 〈ri ∨ rs, 𝟎, ti ∨ ts, 𝟎〉
  25 ].
  26
  27 interpretation
  28   "shift (rt-transition counters)"
  29   'UpDownArrowStar c = (rtc_shift c).
  30
  31 (* Basic constructions ******************************************************)
  32
  33 (*** rtc_shift_rew *)
  34 lemma rtc_shift_unfold (ri) (rs) (ti) (ts):
  35       〈ri ∨ rs, 𝟎, ti ∨ ts, 𝟎〉 = ↕*〈ri,rs,ti,ts〉.
  36 //
  37 qed.
  38
  39 lemma rtc_shift_zz: 𝟘𝟘 = ↕*𝟘𝟘.
  40 // qed.
  41
  42 (* Basic inversions *********************************************************)
  43
  44 lemma rtc_shift_inv_dx (ri) (rs) (ti) (ts) (c):
  45       〈ri,rs,ti,ts〉 = ↕*c →
  46       ∃∃ri0,rs0,ti0,ts0.
  47       (ri0∨rs0) = ri & 𝟎 = rs & (ti0∨ts0) = ti & 𝟎 = ts & 〈ri0,rs0,ti0,ts0〉 = c.
  48 #ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <rtc_shift_unfold #H destruct
  49 /2 width=7 by ex5_4_intro/
  50 qed-.