]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/steps/rtc_isrt.ma
update in ground_2, static_2, basic_2
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / steps / rtc_isrt.ma
index 1b6c7d3686535703ea34d42424e335765abffeb9..42a0ff52e2c221f241daf866d88220b67448ccd5 100644 (file)
@@ -25,10 +25,10 @@ interpretation "test for costrained rt-transition counter (rtc)"
 
 (* Basic properties *********************************************************)
 
-lemma isr_00: 𝐑𝐓❪0,𝟘𝟘❫.
+lemma isrt_00: 𝐑𝐓❪0,𝟘𝟘❫.
 /2 width=3 by ex1_2_intro/ qed.
 
-lemma isr_10: 𝐑𝐓❪0,𝟙𝟘❫.
+lemma isrt_10: 𝐑𝐓❪0,𝟙𝟘❫.
 /2 width=3 by ex1_2_intro/ qed.
 
 lemma isrt_01: 𝐑𝐓❪1,𝟘𝟙❫.