--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/steps/rtc_shift.ma".
+include "ground_2/steps/rtc_ist.ma".
+
+(* RT-TRANSITION COUNTER ****************************************************)
+
+(* Properties with test for t-transition counter ****************************)
+
+lemma ist_zero_shift: āc. šā¦0,cā¦ ā šā¦0,ā*cā¦.
+#c #H destruct //
+qed.
+
+(* Inversion properties with test for t-transition counter ******************)
+
+lemma ist_inv_shift: ān,c. šā¦n,ā*cā¦ ā ā§ā§ šā¦0,cā¦ & 0 = n.
+#n #c #H
+elim (shift_inv_dx ā¦ H) -H #rt0 #rs0 #ti0 #ts0 #H1 #_ #H2 #H3 #H4 destruct
+elim (max_inv_O3 ā¦ H1) -H1 #H11 #H12 destruct
+elim (max_inv_O3 ā¦ H2) -H2 #H21 #H22 destruct
+/2 width=1 by conj/
+qed-.
+
+lemma ist_inv_zero_shift: āc. šā¦0,ā*cā¦ ā šā¦0,cā¦.
+#c #H elim (ist_inv_shift ā¦ H) -H //
+qed-.