(* RT-TRANSITION COUNTER ****************************************************)
-(* Properties with test for costrained rt-transition counter ****************)
+(* Properties with test for constrained rt-transition counter ***************)
lemma isr_shift: âc. ððâŠ0,câŦ â ððâŠ0,â*câŦ.
#c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/
qed.
-(* Inversion properties with test for costrained rt-counter *****************)
+(* Inversion properties with test for constrained rt-transition counter *****)
lemma isrt_inv_shift: ân,c. ððâŠn,â*câŦ â ððâŠ0,câŦ ⧠0 = n.
#n #c * #ri #rs #H