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/relations/isredtype_2.ma".
16 include "ground_2/steps/rtc.ma".
18 (* RT-TRANSITION COUNTER ****************************************************)
20 definition isrt: relation2 nat rtc ≝ λts,c.
21 ∃∃ri,rs. 〈ri, rs, 0, ts〉 = c.
23 interpretation "test for costrained rt-transition counter (rtc)"
24 'IsRedType ts c = (isrt ts c).
26 (* Basic properties *********************************************************)
28 lemma isr_00: 𝐑𝐓⦃0, 𝟘𝟘⦄.
29 /2 width=3 by ex1_2_intro/ qed.
31 lemma isr_10: 𝐑𝐓⦃0, 𝟙𝟘⦄.
32 /2 width=3 by ex1_2_intro/ qed.
34 lemma isrt_01: 𝐑𝐓⦃1, 𝟘𝟙⦄.
35 /2 width=3 by ex1_2_intro/ qed.
37 lemma isrt_eq_t_trans: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → eq_t c1 c2 → 𝐑𝐓⦃n, c2⦄.
38 #n #c1 #c2 * #ri1 #rs1 #H destruct
39 #H elim (eq_t_inv_dx … H) -H /2 width=3 by ex1_2_intro/
42 (* Basic inversion properties ***********************************************)
44 lemma isrt_inv_00: ∀n. 𝐑𝐓⦃n, 𝟘𝟘⦄ → 0 = n.
45 #n * #ri #rs #H destruct //
48 lemma isrt_inv_10: ∀n. 𝐑𝐓⦃n, 𝟙𝟘⦄ → 0 = n.
49 #n * #ri #rs #H destruct //
52 lemma isrt_inv_01: ∀n. 𝐑𝐓⦃n, 𝟘𝟙⦄ → 1 = n.
53 #n * #ri #rs #H destruct //
56 (* Main inversion properties ************************************************)
58 theorem isrt_inj: ∀n1,n2,c. 𝐑𝐓⦃n1, c⦄ → 𝐑𝐓⦃n2, c⦄ → n1 = n2.
59 #n1 #n2 #c * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
62 theorem isrt_mono: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → 𝐑𝐓⦃n, c2⦄ → eq_t c1 c2.
63 #n #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //