matita/matita/lib/lambda/.depend
matita/matita/contribs/lambdadelta/.depend
+matita/matita/contribs/lambdadelta/bin/recomm/srcs
+matita/matita/contribs/lambdadelta/bin/recomm/log.txt
matita/matita/contribs/lambdadelta/bin/nodes
matita/matita/contribs/lambdadelta/bin/token
matita/matita/contribs/lambdadelta/*/probe.txt
include "ground/xoa/ex_6_9.ma".
include "ground/xoa/ex_7_10.ma".
include "ground/xoa/or_5.ma".
-include "ground/steps/rtc_shift.ma".
-include "ground/steps/rtc_plus.ma".
-include "ground/steps/rtc_max.ma".
+include "ground/counters/rtc_shift.ma".
+include "ground/counters/rtc_plus.ma".
+include "ground/counters/rtc_max.ma".
include "basic_2/notation/relations/predty_7.ma".
include "static_2/syntax/lenv.ma".
include "static_2/syntax/genv.ma".
include "ground/xoa/ex_4_3.ma".
include "ground/xoa/ex_5_6.ma".
include "ground/xoa/ex_6_7.ma".
-include "ground/steps/rtc_max_shift.ma".
-include "ground/steps/rtc_isrt_plus.ma".
-include "ground/steps/rtc_isrt_max_shift.ma".
+include "ground/counters/rtc_max_shift.ma".
+include "ground/counters/rtc_isrt_plus.ma".
+include "ground/counters/rtc_isrt_max_shift.ma".
include "static_2/syntax/sh.ma".
include "basic_2/notation/relations/pred_6.ma".
include "basic_2/rt_transition/cpg.ma".
(**************************************************************************)
include "ground/xoa/ex_4_3.ma".
-include "ground/steps/rtc_ist_shift.ma".
-include "ground/steps/rtc_ist_plus.ma".
-include "ground/steps/rtc_ist_max.ma".
+include "ground/counters/rtc_ist_shift.ma".
+include "ground/counters/rtc_ist_plus.ma".
+include "ground/counters/rtc_ist_max.ma".
include "static_2/syntax/sh.ma".
include "basic_2/notation/relations/pty_6.ma".
include "basic_2/rt_transition/cpg.ma".
@$(RM) recommGc*.ml*
test:
- @./recomm.native $(O) -C ../../ground/steps . | sort | uniq > log.txt
+ @./recomm.native -r $(O) -C srcs . | sort | uniq > log.txt
MRCS = $(wildcard *.mrc)
PcsAnd b "" true false
-rtc_max, max
-rtc_shift, shift
-rtc_ism, test for constrained rt-transition counter
-rtc_ist, test for t-transition counter
+rtc_shift
+rtc_max
+rtc_plus
PccFor d "" true false
-T-BOUND RT-TRANSITION COUNTERS, RT-TRANSITION COUNTER
-T-TRANSITION COUNTERS, T-TRANSITION COUNTER
+RT-TRANSITION COUNTERS
+T-BOUND RT-TRANSITION COUNTERS
+T-TRANSITION COUNTERS
--- /dev/null
+PccFor r "" true false
+ADDITION
+MAXIMUM, MAXIMUN
+SHIFT
let write = ref false
+let force = ref false
+
let chdir path =
Sys.chdir path
Printf.eprintf "processing: %S\n" file;
let orig = EI.read_srcs file in
let lint = EC.recomm_srcs orig in
- if !write && lint <> orig then EO.write_srcs file lint
+ if !force || (!write && lint <> orig) then EO.write_srcs file lint
end else begin
Printf.eprintf "skipping: %S\n" file
end
let msg_L = " Log lexer tokens (default: no)"
let msg_c = "<int> Set these output columns (default: 78)"
let msg_d = " Log with dark colors (default: no)"
+let msg_f = " Write all output files (default: no)"
let msg_k = " Log key comments (default: no)"
let msg_m = " Log mark comments (default: no)"
let msg_n = " Log with no colors (default: yes)"
let msg_o = " Log other comments (default: no)"
+let msg_r = " Replace the input files (default: no)"
let msg_s = " Log section comments (default: no)"
let msg_t = " Log title comments (default: no)"
-let msg_w = " Write the output files (default: no)"
+let msg_w = " Write the changed output files (default: no)"
let main =
Arg.parse [
"-L", Arg.Set EL.debug, msg_m;
"-c", Arg.Int ((:=) EO.width), msg_c;
"-d", Arg.Clear EC.bw, msg_d;
+ "-f", Arg.Set force, msg_f;
"-k", Arg.Set EC.log_k, msg_k;
"-m", Arg.Set EC.log_m, msg_m;
"-n", Arg.Set EC.bw, msg_n;
"-o", Arg.Set EC.log_o, msg_o;
+ "-r", Arg.Set EO.replace, msg_r;
"-s", Arg.Set EC.log_s, msg_s;
"-t", Arg.Set EC.log_t, msg_t;
"-w", Arg.Set write, msg_w;
if middle st then Printf.eprintf "middle: %S\n" s1;
if !log_k then log prune (s1^s2);
recomm tl @@ add hd @@ st
- | ET.Title ss as hd :: tl ->
+ | ET.Title ss :: tl ->
if middle st then Printf.eprintf "middle: TITLE\n";
let b, ss1, ss2 = !c_line k_final false [] ss in
let ss2 =
let ss = List.rev_append ss1 ss2 in
let s = String.concat " " ss in
if !log_t then log blue s;
- recomm tl @@ add hd @@ st
- | ET.Slice ss as hd :: tl ->
+ recomm tl @@ add (ET.Title ss) @@ st
+ | ET.Slice ss :: tl ->
if middle st then Printf.eprintf "middle: Section\n";
let b, ss1, ss2 = !s_line k_final false [] ss in
let ss2 =
let ss = List.rev_append ss1 ss2 in
let s = String.capitalize_ascii (String.concat " " ss) in
if !log_s then log sky s;
- recomm tl @@ add hd @@ st
+ recomm tl @@ add (ET.Slice ss) @@ st
| ET.Other (_, s, _) as hd :: tl ->
if !log_o && not (Array.mem s mute_o) then log black s;
recomm tl @@ add hd @@ st
module G1 = RecommGcbGroundCounters
module G2 = RecommGcdGroundCounters
-module G3 = RecommGcsAttr
-module G4 = RecommGcsMain
-module G5 = RecommGcsWith
+module G3 = RecommGcrGroundCounters
+module G4 = RecommGcsAttr
+module G5 = RecommGcsMain
+module G6 = RecommGcsWith
let step k ok outs ins =
if ok then k ok outs ins else
match ins with
- | "rtc_ist" :: tl -> k true ("rtc_ist" :: outs) tl
- | "test" :: "for" :: "t-transition" :: "counter" :: tl -> k true ("rtc_ist" :: outs) tl
- | "rtc_ism" :: tl -> k true ("rtc_ism" :: outs) tl
- | "test" :: "for" :: "constrained" :: "rt-transition" :: "counter" :: tl -> k true ("rtc_ism" :: outs) tl
- | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl
- | "shift" :: tl -> k true ("rtc_shift" :: outs) tl
+ | "rtc_plus" :: tl -> k true ("rtc_plus" :: outs) tl
| "rtc_max" :: tl -> k true ("rtc_max" :: outs) tl
- | "max" :: tl -> k true ("rtc_max" :: outs) tl
+ | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl
| _ -> k ok outs ins
let main =
if ok then k ok outs ins else
match ins with
| "T-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl
- | "T-TRANSITION" :: "COUNTER" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl
| "T-BOUND" :: "RT-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl
- | "RT-TRANSITION" :: "COUNTER" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl
+ | "RT-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: outs) tl
| _ -> k ok outs ins
let main =
--- /dev/null
+let step k ok outs ins =
+ if ok then k ok outs ins else
+ match ins with
+ | "SHIFT" :: tl -> k true ("SHIFT" :: outs) tl
+ | "MAXIMUM" :: tl -> k true ("MAXIMUM" :: outs) tl
+ | "MAXIMUN" :: tl -> k true ("MAXIMUM" :: outs) tl
+ | "ADDITION" :: tl -> k true ("ADDITION" :: outs) tl
+ | _ -> k ok outs ins
+
+let main =
+ RecommPccFor.register_r step
let heads = [|
"Advanved";
"Basic";
+ "Constructions";
"Forward";
"Destructions";
"Eliminations";
let width = ref 78
+let replace = ref false
+
let complete s =
let l = !width - String.length s - 6 in
if l < 0 then begin
| ET.Mark s ->
Printf.fprintf och "(* %s**)" s
| ET.Key (s1, s2) ->
- Printf.fprintf och "(* %s1%s2*)" s1 s2
+ Printf.fprintf och "(* %s%s*)" s1 s2
| ET.Title ss ->
let s = String.concat " " ss in
Printf.fprintf och "(* %s %s*)" s (complete s)
Printf.fprintf och "%s%s%s" s1 s2 s3
let write_srcs file srcs =
- let och = open_out (file ^ ".new") in
+ let target =
+ if !replace then begin
+ Sys.rename file (file ^ ".old");
+ file
+ end else begin
+ file ^ ".new"
+ end
+ in
+ let och = open_out target in
List.iter (out_src och) srcs;
close_out och
val width: int ref
+val replace: bool ref
+
val write_srcs: string -> RecommTypes.srcs -> unit
let k_for k ok outs ins =
if ok then begin
match ins with
- | "for" :: tl -> !d_line k false ("for" :: outs) tl
+ | "FOR" :: tl -> !d_line k false ("FOR" :: outs) tl
| _ -> k true outs ins
end else begin
k true outs ins
#n1 #n2 #IH #n3 @(nat_ind_succ β¦ n3) -n3 //
qed.
+lemma nmax_max_comm_23 (o:nat) (m) (n): (o β¨ m β¨ n) = (o β¨ n β¨ m).
+#o #m #n >nmax_assoc >nmax_assoc <nmax_comm in β’ (??(??%)?); //
+qed.
+
(* Basic inversions *********************************************************)
-(*** max_inv_O3 *)
-lemma nmax_inv_zero (n1) (n2): π = (n1 β¨ n2) β β§β§ π = n1 & π = n2.
+lemma eq_inv_zero_nmax (n1) (n2): π = (n1 β¨ n2) β β§β§ π = n1 & π = n2.
#n1 #n2 @(nat_ind_2_succ β¦ n1 n2) -n1 -n2 /2 width=1 by conj/
#n1 #n2 #_ <nmax_succ_bi #H
elim (eq_inv_zero_nsucc β¦ H)
qed-.
+
+(*** max_inv_O3 *)
+lemma eq_inv_nmax_zero (n1) (n2): (n1 β¨ n2) = π β β§β§ π = n1 & π = n2.
+/2 width=1 by eq_inv_zero_nmax/ qed-.
#n <nplus_comm // qed.
lemma nplus_succ_shift (m) (n): βm + n = m + βn.
-// qed-.
+// qed.
(*** assoc_plus1 *)
lemma nplus_plus_comm_12 (o) (m) (n): m + n + o = n + (m + o).
(*** plus_plus_comm_23 *)
lemma nplus_plus_comm_23 (o) (m) (n): o + m + n = o + n + m.
#o #m #n >nplus_assoc >nplus_assoc <nplus_comm in β’ (??(??%)?); //
-qed-.
+qed.
(* Basic inversions *********************************************************)
-(*** plus_inv_O3 zero_eq_plus *)
+(*** zero_eq_plus *)
lemma eq_inv_zero_nplus (m) (n): π = m + n β β§β§ π = m & π = n.
#m #n @(nat_ind_succ β¦ n) -n
[ /2 width=1 by conj/
]
qed-.
+(*** plus_inv_O3 *)
+lemma eq_inv_nplus_zero (m) (n):
+ m + n = π β β§β§ π = m & π = n.
+/2 width=1 by eq_inv_zero_nplus/ qed-.
+
(*** injective_plus_l *)
lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o β m = n.
#o @(nat_ind_succ β¦ o) -o /3 width=1 by eq_inv_nsucc_bi/
--- /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/xoa/ex_1_2.ma".
+include "ground/notation/functions/tuple_4.ma".
+include "ground/notation/functions/zerozero_0.ma".
+include "ground/notation/functions/zeroone_0.ma".
+include "ground/notation/functions/onezero_0.ma".
+include "ground/insert_eq/insert_eq_1.ma".
+include "ground/arith/nat.ma".
+
+(* RT-TRANSITION COUNTERS ***************************************************)
+
+record rtc: Type[0] β {
+(* Note: inner r-steps *)
+ ri: nat;
+(* Note: spine r-steps *)
+ rs: nat;
+(* Note: inner t-steps *)
+ ti: nat;
+(* Note: spine t-steps *)
+ ts: nat
+}.
+
+interpretation
+ "constructor (rtc)"
+ 'Tuple ri rs ti ts = (mk_rtc ri rs ti ts).
+
+interpretation
+ "one structural step (rtc)"
+ 'ZeroZero = (mk_rtc nzero nzero nzero nzero).
+
+interpretation
+ "one r-step (rtc)"
+ 'OneZero = (mk_rtc nzero (ninj punit) nzero nzero).
+
+interpretation
+ "one t-step (rtc)"
+ 'ZeroOne = (mk_rtc nzero nzero nzero (ninj punit)).
+
+definition rtc_eq_f: relation rtc β Ξ»c1,c2. β€.
+
+inductive rtc_eq_t: relation rtc β
+| eq_t_intro: βri1,ri2,rs1,rs2,ti,ts.
+ rtc_eq_t (β©ri1,rs1,ti,tsβͺ) (β©ri2,rs2,ti,tsβͺ)
+.
+
+(* Basic constructions ******************************************************)
+
+lemma rtc_eq_t_refl: reflexive β¦ rtc_eq_t.
+* // qed.
+
+(* Basic inversions *********************************************************)
+
+lemma rtc_eq_t_inv_dx:
+ βri1,rs1,ti,ts,y. rtc_eq_t (β©ri1,rs1,ti,tsβͺ) y β
+ ββri2,rs2. y = β©ri2,rs2,ti,tsβͺ.
+#ri0 #rs0 #ti0 #ts0 #y @(insert_eq_1 β¦ (β©ri0,rs0,ti0,ts0βͺ))
+#x * -x -y
+#ri1 #ri2 #rs1 #rs2 #ti1 #ts1 #H destruct -ri1 -rs1
+/2 width=3 by ex1_2_intro/
+qed-.
--- /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/notation/relations/ism_2.ma".
+include "ground/counters/rtc.ma".
+
+(* T-BOUND RT-TRANSITION COUNTERS *******************************************)
+
+definition rtc_ism: relation2 nat rtc β Ξ»ts,c.
+ ββri,rs. β©ri,rs,π,tsβͺ = c.
+
+interpretation
+ "t-bound rt-transition counters (rtc)"
+ 'IsM ts c = (rtc_ism ts c).
+
+(* Basic constructions ******************************************************)
+
+lemma rtc_ism_zz: πβͺπ,ππβ«.
+/2 width=3 by ex1_2_intro/ qed.
+
+lemma rtc_ism_zu: πβͺπ,ππβ«.
+/2 width=3 by ex1_2_intro/ qed.
+
+lemma rtc_ism_uz: πβͺπ,ππβ«.
+/2 width=3 by ex1_2_intro/ qed.
+
+lemma rtc_ism_eq_t_trans (n) (c1) (c2): πβͺn,c1β« β rtc_eq_t c1 c2 β πβͺn,c2β«.
+#n #c1 #c2 * #ri1 #rs1 #H destruct
+#H elim (rtc_eq_t_inv_dx β¦ H) -H /2 width=3 by ex1_2_intro/
+qed-.
+
+(* Basic destructions *******************************************************)
+
+lemma rtc_ism_des_zz (n): πβͺn,ππβ« β π = n.
+#n * #ri #rs #H destruct //
+qed-.
+
+lemma rtc_ism_des_uz (n): πβͺn,ππβ« β π = n.
+#n * #ri #rs #H destruct //
+qed-.
+
+lemma rtc_ism_des_01 (n): πβͺn,ππβ« β ninj (π) = n.
+#n * #ri #rs #H destruct //
+qed-.
+
+(* Main inversions **********************************************************)
+
+theorem rtc_ism_inj (n1) (n2) (c): πβͺn1,cβ« β πβͺn2,cβ« β n1 = n2.
+#n1 #n2 #c * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
+qed-.
+
+theorem rtc_ism_mono (n) (c1) (c2): πβͺn,c1β« β πβͺn,c2β« β rtc_eq_t c1 c2.
+#n #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
+qed-.
--- /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/xoa/ex_3_2.ma".
+include "ground/counters/rtc_max.ma".
+include "ground/counters/rtc_ism.ma".
+
+(* T-BOUND RT-TRANSITION COUNTERS *******************************************)
+
+(* Constructions with rtc_max ***********************************************)
+
+lemma rtc_ism_max (n1) (n2) (c1) (c2): πβͺn1,c1β« β πβͺn2,c2β« β πβͺn1β¨n2,c1β¨c2β«.
+#n1 #n2 #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct
+/2 width=3 by ex1_2_intro/
+qed.
+
+lemma rtc_ism_max_zero_sn (n) (c1) (c2): πβͺπ,c1β« β πβͺn,c2β« β πβͺn,c1β¨c2β«.
+/2 width=1 by rtc_ism_max/ qed.
+
+lemma rtc_ism_max_zero_dx (n) (c1) (c2): πβͺn,c1β« β πβͺπ,c2β« β πβͺn,c1β¨c2β«.
+#n #c1 #c2 #H1 #H2 >(nmax_zero_dx n) /2 width=1 by rtc_ism_max/
+qed.
+
+lemma rtc_ism_max_idem_sn (n) (c1) (c2): πβͺn,c1β« β πβͺn,c2β« β πβͺn,c1β¨c2β«.
+#n #c1 #c2 #H1 #H2 >(nmax_idem n) /2 width=1 by rtc_ism_max/
+qed.
+
+(* Inversions with rtc_max **************************************************)
+
+lemma rtc_ism_inv_max (n) (c1) (c2): πβͺn,c1 β¨ c2β« β
+ ββn1,n2. πβͺn1,c1β« & πβͺn2,c2β« & (n1 β¨ n2) = n.
+#n #c1 #c2 * #ri #rs #H
+elim (rtc_max_inv_dx β¦ H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4
+elim (eq_inv_nmax_zero β¦ H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/
+qed-.
+
+lemma rtc_isr_inv_max (c1) (c2): πβͺπ,c1 β¨ c2β« β β§β§ πβͺπ,c1β« & πβͺπ,c2β«.
+#c1 #c2 #H
+elim (rtc_ism_inv_max β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H
+elim (eq_inv_nmax_zero β¦ H) -H #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
+
+lemma rtc_ism_inv_max_zero_dx (n) (c1) (c2): πβͺn,c1 β¨ c2β« β πβͺπ,c2β« β πβͺn,c1β«.
+#n #c1 #c2 #H #H2
+elim (rtc_ism_inv_max β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
+lapply (rtc_ism_inj β¦ Hn2 H2) -c2 #H destruct //
+qed-.
+
+lemma rtc_ism_inv_max_eq_t (n) (c1) (c2): πβͺn,c1 β¨ c2β« β rtc_eq_t c1 c2 β
+ β§β§ πβͺn,c1β« & πβͺn,c2β«.
+#n #c1 #c2 #H #Hc12
+elim (rtc_ism_inv_max β¦ H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
+lapply (rtc_ism_eq_t_trans β¦ Hc1 β¦ Hc12) -Hc12 #H
+<(rtc_ism_inj β¦ H β¦ Hc2) -Hc2
+<nmax_idem /2 width=1 by conj/
+qed-.
--- /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/counters/rtc_ism_shift.ma".
+include "ground/counters/rtc_ism_max.ma".
+
+(* T-BOUND RT-TRANSITION COUNTERS *******************************************)
+
+(* Inversions with rtc_max and rtc_shift ************************************)
+
+lemma rtc_ism_inv_max_shift_sn (n) (c1) (c2): πβͺn,β*c1 β¨ c2β« β
+ β§β§ πβͺπ,c1β« & πβͺn,c2β«.
+#n #c1 #c2 #H
+elim (rtc_ism_inv_max β¦ H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
+elim (rtc_ism_inv_shift β¦ Hc1) -Hc1 #Hc1 * -n1 <nmax_zero_sn
+/2 width=1 by conj/
+qed-.
--- /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/xoa/ex_3_2.ma".
+include "ground/counters/rtc_plus.ma".
+include "ground/counters/rtc_ism.ma".
+
+(* T-BOUND RT-TRANSITION COUNTERS *******************************************)
+
+(* Constructions with rtc_plus **********************************************)
+
+lemma rtc_ism_plus (n1) (n2) (c1) (c2): πβͺn1,c1β« β πβͺn2,c2β« β πβͺn1+n2,c1+c2β«.
+#n1 #n2 #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct
+/2 width=3 by ex1_2_intro/
+qed.
+
+lemma rtc_ism_plus_zero_sn (n) (c1) (c2): πβͺπ,c1β« β πβͺn,c2β« β πβͺn,c1+c2β«.
+#n #c1 #c2 #H1 #H2 >(nplus_zero_sn n) /2 width=1 by rtc_ism_plus/
+qed.
+
+lemma rtc_ism_plus_zero_dx (n) (c1) (c2): πβͺn,c1β« β πβͺπ,c2β« β πβͺn,c1+c2β«.
+/2 width=1 by rtc_ism_plus/ qed.
+
+lemma rtc_ism_succ (n) (c): πβͺn,cβ« β πβͺβn,c+ππβ«.
+#n #c #H >nplus_one_dx
+/2 width=1 by rtc_ism_plus/
+qed.
+
+(* Inversions with rtc_plus *************************************************)
+
+lemma rtc_ism_inv_plus (n) (c1) (c2): πβͺn,c1 + c2β« β
+ ββn1,n2. πβͺn1,c1β« & πβͺn2,c2β« & n1 + n2 = n.
+#n #c1 #c2 * #ri #rs #H
+elim (rtc_plus_inv_dx β¦ H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4
+elim (eq_inv_nplus_zero β¦ H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/
+qed-.
+
+lemma rtc_ism_inv_plus_zero_dx (n) (c1) (c2): πβͺn,c1 + c2β« β πβͺπ,c2β« β πβͺn,c1β«.
+#n #c1 #c2 #H #H2
+elim (rtc_ism_inv_plus β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
+lapply (rtc_ism_inj β¦ Hn2 H2) -c2 #H destruct //
+qed-.
+
+lemma rtc_ism_inv_plus_unit_dx (n) (c1) (c2): πβͺn,c1 + c2β« β πβͺπ,c2β« β
+ ββm. πβͺm,c1β« & n = βm.
+#n #c1 #c2 #H #H2
+elim (rtc_ism_inv_plus β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
+lapply (rtc_ism_inj β¦ Hn2 H2) -c2 #H destruct
+/2 width=3 by ex2_intro/
+qed-.
--- /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/counters/rtc_shift.ma".
+include "ground/counters/rtc_ism.ma".
+
+(* T-BOUND RT-TRANSITION COUNTERS *******************************************)
+
+(* Constructions with rtc_shift *********************************************)
+
+lemma rtc_isr_shift (c): πβͺπ,cβ« β πβͺπ,β*cβ«.
+#c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/
+qed.
+
+(* Inversions with rtc_shift ************************************************)
+
+lemma rtc_ism_inv_shift (n) (c): πβͺn,β*cβ« β β§β§ πβͺπ,cβ« & π = n.
+#n #c * #ri #rs #H
+elim (rtc_shift_inv_dx β¦ H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3
+elim (eq_inv_nmax_zero β¦ H1) -H1 /3 width=3 by ex1_2_intro, conj/
+qed-.
+
+lemma rtc_isr_inv_shift (c): πβͺπ,β*cβ« β πβͺπ,cβ«.
+#c #H elim (rtc_ism_inv_shift β¦ H) -H //
+qed-.
--- /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/notation/relations/ist_2.ma".
+include "ground/counters/rtc.ma".
+
+(* T-TRANSITION COUNTERS ****************************************************)
+
+definition rtc_ist: relation2 nat rtc β
+ Ξ»ts,c. β©π,π,π,tsβͺ = c.
+
+interpretation
+ "t-transition counters (rtc)"
+ 'IsT ts c = (rtc_ist ts c).
+
+(* Basic constructions ******************************************************)
+
+lemma rtc_ist_zz: πβͺπ,ππβ«.
+// qed.
+
+lemma rtc_ist_zu: πβͺπ,ππβ«.
+// qed.
+
+(* Basic inversions *********************************************************)
+
+lemma rtc_ist_inv_zz (n): πβͺn,ππβ« β π = n.
+#n #H destruct //
+qed-.
+
+lemma rtc_ist_inv_zu (n): πβͺn,ππβ« β ninj (π) = n.
+#n #H destruct //
+qed-.
+
+lemma rtc_ist_inv_uz (n): πβͺn,ππβ« β β₯.
+#h #H destruct
+qed-.
+
+(* Main inversions **********************************************************)
+
+theorem rtc_ist_inj (n1) (n2) (c): πβͺn1,cβ« β πβͺn2,cβ« β n1 = n2.
+#n1 #n2 #c #H1 #H2 destruct //
+qed-.
+
+theorem rtc_ist_mono (n) (c1) (c2): πβͺn,c1β« β πβͺn,c2β« β c1 = c2.
+#n #c1 #c2 #H1 #H2 destruct //
+qed-.
--- /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/xoa/ex_3_2.ma".
+include "ground/counters/rtc_max.ma".
+include "ground/counters/rtc_ist.ma".
+
+(* T-BOUND RT-TRANSITION COUNTERS *******************************************)
+
+(* Constructions with rtc_max ***********************************************)
+
+lemma rtc_ist_max (n1) (n2) (c1) (c2): πβͺn1,c1β« β πβͺn2,c2β« β πβͺn1β¨n2,c1β¨c2β«.
+#n1 #n2 #c1 #c2 #H1 #H2 destruct //
+qed.
+
+lemma rtc_ist_max_zero_sn (n) (c1) (c2): πβͺπ,c1β« β πβͺn,c2β« β πβͺn,c1β¨c2β«.
+/2 width=1 by rtc_ist_max/ qed.
+
+lemma rtc_ist_max_zero_dx (n) (c1) (c2): πβͺn,c1β« β πβͺπ,c2β« β πβͺn,c1β¨c2β«.
+// qed.
+
+lemma rtc_ist_max_idem_sn (n) (c1) (c2): πβͺn,c1β« β πβͺn,c2β« β πβͺn,c1β¨c2β«.
+#n #c1 #c2 #H1 #H2 >(nmax_idem n) /2 width=1 by rtc_ist_max/
+qed.
+
+(* Inversions with rtc_max **************************************************)
+
+lemma rtc_ist_inv_max (n) (c1) (c2): πβͺn,c1 β¨ c2β« β
+ ββn1,n2. πβͺn1,c1β« & πβͺn2,c2β« & (n1 β¨ n2) = n.
+#n #c1 #c2 #H
+elim (rtc_max_inv_dx β¦ H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct
+elim (eq_inv_nmax_zero β¦ H1) -H1 #H11 #H12 destruct
+elim (eq_inv_nmax_zero β¦ H2) -H2 #H21 #H22 destruct
+elim (eq_inv_nmax_zero β¦ H3) -H3 #H31 #H32 destruct
+/2 width=5 by ex3_2_intro/
+qed-.
+
+lemma rtc_ist_inv_zero_max (c1) (c2): πβͺπ,c1 β¨ c2β« β β§β§ πβͺπ,c1β« & πβͺπ,c2β«.
+#c1 #c2 #H
+elim (rtc_ist_inv_max β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H
+elim (eq_inv_nmax_zero β¦ H) -H #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
+
+lemma rtc_ist_inv_max_zero_dx (n) (c1) (c2): πβͺn,c1 β¨ c2β« β πβͺπ,c2β« β πβͺn,c1β«.
+#n #c1 #c2 #H #H2
+elim (rtc_ist_inv_max β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct //
+qed-.
--- /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/xoa/ex_3_2.ma".
+include "ground/counters/rtc_plus.ma".
+include "ground/counters/rtc_ist.ma".
+
+(* T-BOUND RT-TRANSITION COUNTERS *******************************************)
+
+(* Constructions with rtc_plus **********************************************)
+
+lemma rtc_ist_plus (n1) (n2) (c1) (c2): πβͺn1,c1β« β πβͺn2,c2β« β πβͺn1+n2,c1+c2β«.
+#n1 #n2 #c1 #c2 #H1 #H2 destruct //
+qed.
+
+lemma rtc_ist_plus_zero_sn (n) (c1) (c2): πβͺπ,c1β« β πβͺn,c2β« β πβͺn,c1+c2β«.
+#n #c1 #c2 #H1 #H2 >(nplus_zero_sn n)
+/2 width=1 by rtc_ist_plus/
+qed.
+
+lemma rtc_ist_plus_zero_dx (n) (c1) (c2): πβͺn,c1β« β πβͺπ,c2β« β πβͺn,c1+c2β«.
+/2 width=1 by rtc_ist_plus/ qed.
+
+lemma rtc_ist_succ (n) (c): πβͺn,cβ« β πβͺβn,c+ππβ«.
+#n #c #H >nplus_one_dx
+/2 width=1 by rtc_ist_plus/
+qed.
+
+(* Inversions with rtc_plus *************************************************)
+
+lemma rtc_ist_inv_plus (n) (c1) (c2): πβͺn,c1 + c2β« β
+ ββn1,n2. πβͺn1,c1β« & πβͺn2,c2β« & n1 + n2 = n.
+#n #c1 #c2 #H
+elim (rtc_plus_inv_dx β¦ H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct
+elim (eq_inv_nplus_zero β¦ H1) -H1 #H11 #H12 destruct
+elim (eq_inv_nplus_zero β¦ H2) -H2 #H21 #H22 destruct
+elim (eq_inv_nplus_zero β¦ H3) -H3 #H31 #H32 destruct
+/3 width=5 by ex3_2_intro/
+qed-.
+
+lemma rtc_ist_inv_plus_zero_dx (n) (c1) (c2): πβͺn,c1 + c2β« β πβͺπ,c2β« β πβͺn,c1β«.
+#n #c1 #c2 #H #H2
+elim (rtc_ist_inv_plus β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct //
+qed-.
+
+lemma rtc_ist_inv_plus_one_dx:
+ βn,c1,c2. πβͺn,c1 + c2β« β πβͺπ,c2β« β
+ ββm. πβͺm,c1β« & n = βm.
+#n #c1 #c2 #H #H2 destruct
+elim (rtc_ist_inv_plus β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma rtc_ist_inv_plus_zu_dx (n) (c): πβͺn,c+ππβ« β β₯.
+#n #c #H
+elim (rtc_ist_inv_plus β¦ H) -H #n1 #n2 #_ #H #_
+/2 width=2 by rtc_ist_inv_uz/
+qed-.
--- /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/counters/rtc_shift.ma".
+include "ground/counters/rtc_ist.ma".
+
+(* T-BOUND RT-TRANSITION COUNTERS *******************************************)
+
+(* Constructions with rtc_shift *********************************************)
+
+lemma rtc_ist_zero_shift (c): πβͺπ,cβ« β πβͺπ,β*cβ«.
+#c #H destruct //
+qed.
+
+(* Inversions with rtc_shift ************************************************)
+
+lemma rtc_ist_inv_shift (n) (c): πβͺn,β*cβ« β β§β§ πβͺπ,cβ« & π = n.
+#n #c #H
+elim (rtc_shift_inv_dx β¦ H) -H #rt0 #rs0 #ti0 #ts0 #H1 #_ #H2 #H3 #H4 destruct
+elim (eq_inv_nmax_zero β¦ H1) -H1 #H11 #H12 destruct
+elim (eq_inv_nmax_zero β¦ H2) -H2 #H21 #H22 destruct
+/2 width=1 by conj/
+qed-.
+
+lemma rtc_ist_inv_zero_shift (c): πβͺπ,β*cβ« β πβͺπ,cβ«.
+#c #H elim (rtc_ist_inv_shift β¦ H) -H //
+qed-.
--- /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/xoa/ex_6_8.ma".
+include "ground/arith/nat_max.ma".
+include "ground/counters/rtc.ma".
+
+(* MAXIMUM FOR RT-TRANSITION COUNTERS ***************************************)
+
+definition rtc_max (c1:rtc) (c2:rtc): rtc β
+match c1 with
+[ mk_rtc ri1 rs1 ti1 ts1 β
+ match c2 with
+ [ mk_rtc ri2 rs2 ti2 ts2 β β©ri1β¨ri2,rs1β¨rs2,ti1β¨ti2,ts1β¨ts2βͺ
+ ]
+].
+
+interpretation
+ "maximum (rtc)"
+ 'or c1 c2 = (rtc_max c1 c2).
+
+(* Basic constructions ******************************************************)
+
+lemma rtc_max_rew (ri1) (ri2) (rs1) (rs2) (ti1) (ti2) (ts1) (ts2):
+ β©ri1β¨ri2,rs1β¨rs2,ti1β¨ti2,ts1β¨ts2βͺ =
+ (β©ri1,rs1,ti1,ts1βͺ β¨ β©ri2,rs2,ti2,ts2βͺ).
+// qed.
+
+lemma rtc_max_zz_dx (c): c = (c β¨ ππ).
+* #ri #rs #ti #ts <rtc_max_rew //
+qed.
+
+lemma rtc_max_idem (c): c = (c β¨ c).
+* #ri #rs #ti #ts <rtc_max_rew //
+qed.
+
+(* Basic inversions *********************************************************)
+
+lemma rtc_max_inv_dx (ri) (rs) (ti) (ts) (c1) (c2):
+ β©ri,rs,ti,tsβͺ = (c1 β¨ c2) β
+ ββri1,rs1,ti1,ts1,ri2,rs2,ti2,ts2.
+ (ri1β¨ri2) = ri & (rs1β¨rs2) = rs & (ti1β¨ti2) = ti & (ts1β¨ts2) = ts &
+ β©ri1,rs1,ti1,ts1βͺ = c1 & β©ri2,rs2,ti2,ts2βͺ = c2.
+#ri #rs #ti #ts * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
+<rtc_max_rew #H destruct /2 width=14 by ex6_8_intro/
+qed-.
+
+(* Main constructions *******************************************************)
+
+theorem rtc_max_assoc: associative β¦ rtc_max.
+* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
+<rtc_max_rew <rtc_max_rew //
+qed.
--- /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/counters/rtc_shift.ma".
+include "ground/counters/rtc_max.ma".
+
+(* MAXIMUM FOR RT-TRANSITION COUNTERS ***************************************)
+
+(* Constructions with rtc_shift *********************************************)
+
+lemma rtc_max_shift (c1) (c2): ((β*c1) β¨ (β*c2)) = β*(c1β¨c2).
+* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
+<rtc_shift_rew <rtc_shift_rew <rtc_shift_rew <rtc_max_rew
+<nmax_assoc <nmax_assoc <nmax_assoc <nmax_assoc //
+qed.
--- /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/xoa/ex_6_8.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/counters/rtc.ma".
+
+(* ADDITION FOR RT-TRANSITION COUNTERS **************************************)
+
+definition rtc_plus (c1:rtc) (c2:rtc): rtc β
+match c1 with
+[ mk_rtc ri1 rs1 ti1 ts1 β
+ match c2 with
+ [ mk_rtc ri2 rs2 ti2 ts2 β β©ri1+ri2,rs1+rs2,ti1+ti2,ts1+ts2βͺ
+ ]
+].
+
+interpretation
+ "plus (rtc)"
+ 'plus c1 c2 = (rtc_plus c1 c2).
+
+(* Basic constructions ******************************************************)
+
+lemma rtc_plus_rew (ri1) (ri2) (rs1) (rs2) (ti1) (ti2) (ts1) (ts2):
+ β©ri1+ri2,rs1+rs2,ti1+ti2,ts1+ts2βͺ = β©ri1,rs1,ti1,ts1βͺ+β©ri2,rs2,ti2,ts2βͺ.
+// qed.
+
+lemma rtc_plus_zz_dx (c): c = c + ππ.
+* #ri #rs #ti #ts <rtc_plus_rew //
+qed.
+
+(* Basic inversions *********************************************************)
+
+lemma rtc_plus_inv_dx (ri) (rs) (ti) (ts) (c1) (c2):
+ β©ri,rs,ti,tsβͺ = c1 + c2 β
+ ββri1,rs1,ti1,ts1,ri2,rs2,ti2,ts2.
+ ri1+ri2 = ri & rs1+rs2 = rs & ti1+ti2 = ti & ts1+ts2 = ts &
+ β©ri1,rs1,ti1,ts1βͺ = c1 & β©ri2,rs2,ti2,ts2βͺ = c2.
+#ri #rs #ti #ts * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
+<rtc_plus_rew #H destruct /2 width=14 by ex6_8_intro/
+qed-.
+
+(* Main constructions *******************************************************)
+
+theorem rtc_plus_assoc: associative β¦ rtc_plus.
+* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
+<rtc_plus_rew //
+qed.
--- /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/xoa/ex_5_4.ma".
+include "ground/notation/functions/updownarrowstar_1.ma".
+include "ground/arith/nat_max.ma".
+include "ground/counters/rtc.ma".
+
+(* SHIFT FOR RT-TRANSITION COUNTERS *****************************************)
+
+definition rtc_shift (c:rtc): rtc β
+match c with
+[ mk_rtc ri rs ti ts β β©ri β¨ rs, π, ti β¨ ts, πβͺ
+].
+
+interpretation
+ "shift (rtc)"
+ 'UpDownArrowStar c = (rtc_shift c).
+
+(* Basic constructions ******************************************************)
+
+lemma rtc_shift_rew (ri) (rs) (ti) (ts):
+ β©ri β¨ rs, π, ti β¨ ts, πβͺ = β*β©ri,rs,ti,tsβͺ.
+//
+qed.
+
+lemma rtc_shift_zz: ππ = β*ππ.
+// qed.
+
+(* Basic inversions *********************************************************)
+
+lemma rtc_shift_inv_dx (ri) (rs) (ti) (ts) (c):
+ β©ri,rs,ti,tsβͺ = β*c β
+ ββri0,rs0,ti0,ts0.
+ (ri0β¨rs0) = ri & π = rs & (ti0β¨ts0) = ti & π = ts & β©ri0,rs0,ti0,ts0βͺ = c.
+#ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <rtc_shift_rew #H destruct
+/2 width=7 by ex5_4_intro/
+qed-.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( πβͺ term 46 n, break term 46 c β« )"
+ non associative with precedence 45
+ for @{ 'IsM $n $c }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( ππβͺ term 46 n, break term 46 c β« )"
- non associative with precedence 45
- for @{ 'IsRedType $n $c }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( πβͺ term 46 f β« )"
+ non associative with precedence 45
+ for @{ 'IsT $f }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( πβͺ term 46 n, break term 46 c β« )"
+ non associative with precedence 45
+ for @{ 'IsT $n $c }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( πβͺ term 46 f β« )"
- non associative with precedence 45
- for @{ 'IsTotal $f }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( πβͺ term 46 n, break term 46 c β« )"
- non associative with precedence 45
- for @{ 'IsType $n $c }.
+++ /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/xoa/ex_1_2.ma".
-include "ground/notation/functions/tuple_4.ma".
-include "ground/notation/functions/zerozero_0.ma".
-include "ground/notation/functions/zeroone_0.ma".
-include "ground/notation/functions/onezero_0.ma".
-include "ground/lib/arith.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-record rtc: Type[0] β {
- ri: nat; (* Note: inner r-steps *)
- rs: nat; (* Note: spine r-steps *)
- ti: nat; (* Note: inner t-steps *)
- ts: nat (* Note: spine t-steps *)
-}.
-
-interpretation "constructor (rtc)"
- 'Tuple ri rs ti ts = (mk_rtc ri rs ti ts).
-
-interpretation "one structural step (rtc)"
- 'ZeroZero = (mk_rtc O O O O).
-
-interpretation "one r-step (rtc)"
- 'OneZero = (mk_rtc O (S O) O O).
-
-interpretation "one t-step (rtc)"
- 'ZeroOne = (mk_rtc O O O (S O)).
-
-definition rtc_eq_f: relation rtc β Ξ»c1,c2. β€.
-
-inductive rtc_eq_t: relation rtc β
-| eq_t_intro: βri1,ri2,rs1,rs2,ti,ts.
- rtc_eq_t (β©ri1,rs1,ti,tsβͺ) (β©ri2,rs2,ti,tsβͺ)
-.
-
-(* Basic properties *********************************************************)
-
-lemma rtc_eq_t_refl: reflexive β¦ rtc_eq_t.
-* // qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact rtc_eq_t_inv_dx_aux:
- βx,y. rtc_eq_t x y β
- βri1,rs1,ti,ts. x = β©ri1,rs1,ti,tsβͺ β
- ββri2,rs2. y = β©ri2,rs2,ti,tsβͺ.
-#x #y * -x -y
-#ri1 #ri #rs1 #rs #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H destruct -ri2 -rs2
-/2 width=3 by ex1_2_intro/
-qed-.
-
-lemma rtc_eq_t_inv_dx:
- βri1,rs1,ti,ts,y. rtc_eq_t (β©ri1,rs1,ti,tsβͺ) y β
- ββri2,rs2. y = β©ri2,rs2,ti,tsβͺ.
-/2 width=5 by rtc_eq_t_inv_dx_aux/ qed-.
+++ /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/notation/relations/isredtype_2.ma".
-include "ground/steps/rtc.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-definition isrt: relation2 nat rtc β Ξ»ts,c.
- ββri,rs. β©ri,rs,0,tsβͺ = c.
-
-interpretation "test for constrained rt-transition counter (rtc)"
- 'IsRedType ts c = (isrt ts c).
-
-(* Basic properties *********************************************************)
-
-lemma isrt_00: ππβͺ0,ππβ«.
-/2 width=3 by ex1_2_intro/ qed.
-
-lemma isrt_10: ππβͺ0,ππβ«.
-/2 width=3 by ex1_2_intro/ qed.
-
-lemma isrt_01: ππβͺ1,ππβ«.
-/2 width=3 by ex1_2_intro/ qed.
-
-lemma isrt_eq_t_trans: βn,c1,c2. ππβͺn,c1β« β rtc_eq_t c1 c2 β ππβͺn,c2β«.
-#n #c1 #c2 * #ri1 #rs1 #H destruct
-#H elim (rtc_eq_t_inv_dx β¦ H) -H /2 width=3 by ex1_2_intro/
-qed-.
-
-(* Basic inversion properties ***********************************************)
-
-lemma isrt_inv_00: βn. ππβͺn,ππβ« β 0 = n.
-#n * #ri #rs #H destruct //
-qed-.
-
-lemma isrt_inv_10: βn. ππβͺn,ππβ« β 0 = n.
-#n * #ri #rs #H destruct //
-qed-.
-
-lemma isrt_inv_01: βn. ππβͺn,ππβ« β 1 = n.
-#n * #ri #rs #H destruct //
-qed-.
-
-(* Main inversion properties ************************************************)
-
-theorem isrt_inj: βn1,n2,c. ππβͺn1,cβ« β ππβͺn2,cβ« β n1 = n2.
-#n1 #n2 #c * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
-qed-.
-
-theorem isrt_mono: βn,c1,c2. ππβͺn,c1β« β ππβͺn,c2β« β rtc_eq_t c1 c2.
-#n #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
-qed-.
+++ /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/xoa/ex_3_2.ma".
-include "ground/steps/rtc_max.ma".
-include "ground/steps/rtc_isrt.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-(* Properties with test for constrained rt-transition counter ***************)
-
-lemma isrt_max: βn1,n2,c1,c2. ππβͺn1,c1β« β ππβͺn2,c2β« β ππβͺn1β¨n2,c1β¨c2β«.
-#n1 #n2 #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct
-/2 width=3 by ex1_2_intro/
-qed.
-
-lemma isrt_max_O1: βn,c1,c2. ππβͺ0,c1β« β ππβͺn,c2β« β ππβͺn,c1β¨c2β«.
-/2 width=1 by isrt_max/ qed.
-
-lemma isrt_max_O2: βn,c1,c2. ππβͺn,c1β« β ππβͺ0,c2β« β ππβͺn,c1β¨c2β«.
-#n #c1 #c2 #H1 #H2 >(max_O2 n) /2 width=1 by isrt_max/
-qed.
-
-lemma isrt_max_idem1: βn,c1,c2. ππβͺn,c1β« β ππβͺn,c2β« β ππβͺn,c1β¨c2β«.
-#n #c1 #c2 #H1 #H2 >(idempotent_max n) /2 width=1 by isrt_max/
-qed.
-
-(* Inversion properties with test for constrained rt-transition counter *****)
-
-lemma isrt_inv_max: βn,c1,c2. ππβͺn,c1 β¨ c2β« β
- ββn1,n2. ππβͺn1,c1β« & ππβͺn2,c2β« & (n1 β¨ n2) = n.
-#n #c1 #c2 * #ri #rs #H
-elim (max_inv_dx β¦ H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4
-elim (max_inv_O3 β¦ H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/
-qed-.
-
-lemma isrt_O_inv_max: βc1,c2. ππβͺ0,c1 β¨ c2β« β β§β§ ππβͺ0,c1β« & ππβͺ0,c2β«.
-#c1 #c2 #H
-elim (isrt_inv_max β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H
-elim (max_inv_O3 β¦ H) -H #H1 #H2 destruct
-/2 width=1 by conj/
-qed-.
-
-lemma isrt_inv_max_O_dx: βn,c1,c2. ππβͺn,c1 β¨ c2β« β ππβͺ0,c2β« β ππβͺn,c1β«.
-#n #c1 #c2 #H #H2
-elim (isrt_inv_max β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_inj β¦ Hn2 H2) -c2 #H destruct //
-qed-.
-
-lemma isrt_inv_max_eq_t: βn,c1,c2. ππβͺn,c1 β¨ c2β« β rtc_eq_t c1 c2 β
- β§β§ ππβͺn,c1β« & ππβͺn,c2β«.
-#n #c1 #c2 #H #Hc12
-elim (isrt_inv_max β¦ H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
-lapply (isrt_eq_t_trans β¦ Hc1 β¦ Hc12) -Hc12 #H
-<(isrt_inj β¦ H β¦ Hc2) -Hc2
-<idempotent_max /2 width=1 by conj/
-qed-.
+++ /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/steps/rtc_isrt_shift.ma".
-include "ground/steps/rtc_isrt_max.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-(* Inversion properties with test for constrained rt-transition counter *****)
-
-lemma isrt_inv_max_shift_sn: βn,c1,c2. ππβͺn,β*c1 β¨ c2β« β
- β§β§ ππβͺ0,c1β« & ππβͺn,c2β«.
-#n #c1 #c2 #H
-elim (isrt_inv_max β¦ H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
-elim (isrt_inv_shift β¦ Hc1) -Hc1 #Hc1 * -n1
-/2 width=1 by conj/
-qed-.
+++ /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/xoa/ex_3_2.ma".
-include "ground/steps/rtc_plus.ma".
-include "ground/steps/rtc_isrt.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-(* Properties with test for constrained rt-transition counter ***************)
-
-lemma isrt_plus: βn1,n2,c1,c2. ππβͺn1,c1β« β ππβͺn2,c2β« β ππβͺn1+n2,c1+c2β«.
-#n1 #n2 #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct
-/2 width=3 by ex1_2_intro/
-qed.
-
-lemma isrt_plus_O1: βn,c1,c2. ππβͺ0,c1β« β ππβͺn,c2β« β ππβͺn,c1+c2β«.
-/2 width=1 by isrt_plus/ qed.
-
-lemma isrt_plus_O2: βn,c1,c2. ππβͺn,c1β« β ππβͺ0,c2β« β ππβͺn,c1+c2β«.
-#n #c1 #c2 #H1 #H2 >(plus_n_O n) /2 width=1 by isrt_plus/
-qed.
-
-lemma isrt_succ: βn,c. ππβͺn,cβ« β ππβͺβn,c+ππβ«.
-/2 width=1 by isrt_plus/ qed.
-
-(* Inversion properties with test for constrained rt-transition counter *****)
-
-lemma isrt_inv_plus: βn,c1,c2. ππβͺn,c1 + c2β« β
- ββn1,n2. ππβͺn1,c1β« & ππβͺn2,c2β« & n1 + n2 = n.
-#n #c1 #c2 * #ri #rs #H
-elim (plus_inv_dx β¦ H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4
-elim (plus_inv_O3 β¦ H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/
-qed-.
-
-lemma isrt_inv_plus_O_dx: βn,c1,c2. ππβͺn,c1 + c2β« β ππβͺ0,c2β« β ππβͺn,c1β«.
-#n #c1 #c2 #H #H2
-elim (isrt_inv_plus β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_inj β¦ Hn2 H2) -c2 #H destruct //
-qed-.
-
-lemma isrt_inv_plus_SO_dx: βn,c1,c2. ππβͺn,c1 + c2β« β ππβͺ1,c2β« β
- ββm. ππβͺm,c1β« & n = βm.
-#n #c1 #c2 #H #H2
-elim (isrt_inv_plus β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_inj β¦ Hn2 H2) -c2 #H destruct
-/2 width=3 by ex2_intro/
-qed-.
+++ /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/steps/rtc_shift.ma".
-include "ground/steps/rtc_isrt.ma".
-
-(* 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 constrained rt-transition counter *****)
-
-lemma isrt_inv_shift: βn,c. ππβͺn,β*cβ« β ππβͺ0,cβ« β§ 0 = n.
-#n #c * #ri #rs #H
-elim (shift_inv_dx β¦ H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3
-elim (max_inv_O3 β¦ H1) -H1 /3 width=3 by ex1_2_intro, conj/
-qed-.
-
-lemma isr_inv_shift: βc. ππβͺ0,β*cβ« β ππβͺ0,cβ«.
-#c #H elim (isrt_inv_shift β¦ H) -H //
-qed-.
+++ /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/notation/relations/istype_2.ma".
-include "ground/steps/rtc.ma".
-
-(* T-TRANSITION COUNTER *****************************************************)
-
-definition ist: relation2 nat rtc β
- Ξ»ts,c. β©0,0,0,tsβͺ = c.
-
-interpretation "test for t-transition counter (rtc)"
- 'IsType ts c = (ist ts c).
-
-(* Basic properties *********************************************************)
-
-lemma ist_00: πβͺ0,ππβ«.
-// qed.
-
-lemma ist_01: πβͺ1,ππβ«.
-// qed.
-
-(* Basic inversion properties ***********************************************)
-
-lemma ist_inv_00: βn. πβͺn,ππβ« β 0 = n.
-#n #H destruct //
-qed-.
-
-lemma ist_inv_01: βn. πβͺn,ππβ« β 1 = n.
-#n #H destruct //
-qed-.
-
-lemma ist_inv_10: βn. πβͺn,ππβ« β β₯.
-#h #H destruct
-qed-.
-
-(* Main inversion properties ************************************************)
-
-theorem ist_inj: βn1,n2,c. πβͺn1,cβ« β πβͺn2,cβ« β n1 = n2.
-#n1 #n2 #c #H1 #H2 destruct //
-qed-.
-
-theorem ist_mono: βn,c1,c2. πβͺn,c1β« β πβͺn,c2β« β c1 = c2.
-#n #c1 #c2 #H1 #H2 destruct //
-qed-.
+++ /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/xoa/ex_3_2.ma".
-include "ground/steps/rtc_max.ma".
-include "ground/steps/rtc_ist.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-(* Properties with test for t-transition counter ****************************)
-
-lemma ist_max: βn1,n2,c1,c2. πβͺn1,c1β« β πβͺn2,c2β« β πβͺn1β¨n2,c1β¨c2β«.
-#n1 #n2 #c1 #c2 #H1 #H2 destruct //
-qed.
-
-lemma ist_max_O1: βn,c1,c2. πβͺ0,c1β« β πβͺn,c2β« β πβͺn,c1β¨c2β«.
-/2 width=1 by ist_max/ qed.
-
-lemma ist_max_O2: βn,c1,c2. πβͺn,c1β« β πβͺ0,c2β« β πβͺn,c1β¨c2β«.
-#n #c1 #c2 #H1 #H2 >(max_O2 n) /2 width=1 by ist_max/
-qed.
-
-lemma ist_max_idem1: βn,c1,c2. πβͺn,c1β« β πβͺn,c2β« β πβͺn,c1β¨c2β«.
-#n #c1 #c2 #H1 #H2 >(idempotent_max n) /2 width=1 by ist_max/
-qed.
-
-(* Inversion properties with test for t-transition counter ******************)
-
-lemma ist_inv_max:
- βn,c1,c2. πβͺn,c1 β¨ c2β« β
- ββn1,n2. πβͺn1,c1β« & πβͺn2,c2β« & (n1 β¨ n2) = n.
-#n #c1 #c2 #H
-elim (max_inv_dx β¦ H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct
-elim (max_inv_O3 β¦ H1) -H1 #H11 #H12 destruct
-elim (max_inv_O3 β¦ H2) -H2 #H21 #H22 destruct
-elim (max_inv_O3 β¦ H3) -H3 #H31 #H32 destruct
-/2 width=5 by ex3_2_intro/
-qed-.
-
-lemma ist_O_inv_max: βc1,c2. πβͺ0,c1 β¨ c2β« β β§β§ πβͺ0,c1β« & πβͺ0,c2β«.
-#c1 #c2 #H
-elim (ist_inv_max β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H
-elim (max_inv_O3 β¦ H) -H #H1 #H2 destruct
-/2 width=1 by conj/
-qed-.
-
-lemma ist_inv_max_O_dx: βn,c1,c2. πβͺn,c1 β¨ c2β« β πβͺ0,c2β« β πβͺn,c1β«.
-#n #c1 #c2 #H #H2
-elim (ist_inv_max β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct //
-qed-.
+++ /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/xoa/ex_3_2.ma".
-include "ground/steps/rtc_plus.ma".
-include "ground/steps/rtc_ist.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-(* Properties with test for t-transition counter ****************************)
-
-lemma ist_plus: βn1,n2,c1,c2. πβͺn1,c1β« β πβͺn2,c2β« β πβͺn1+n2,c1+c2β«.
-#n1 #n2 #c1 #c2 #H1 #H2 destruct //
-qed.
-
-lemma ist_plus_O1: βn,c1,c2. πβͺ0,c1β« β πβͺn,c2β« β πβͺn,c1+c2β«.
-/2 width=1 by ist_plus/ qed.
-
-lemma ist_plus_O2: βn,c1,c2. πβͺn,c1β« β πβͺ0,c2β« β πβͺn,c1+c2β«.
-#n #c1 #c2 #H1 #H2 >(plus_n_O n) /2 width=1 by ist_plus/
-qed.
-
-lemma ist_succ: βn,c. πβͺn,cβ« β πβͺβn,c+ππβ«.
-/2 width=1 by ist_plus/ qed.
-
-(* Inversion properties with test for constrained rt-transition counter *****)
-
-lemma ist_inv_plus:
- βn,c1,c2. πβͺn,c1 + c2β« β
- ββn1,n2. πβͺn1,c1β« & πβͺn2,c2β« & n1 + n2 = n.
-#n #c1 #c2 #H
-elim (plus_inv_dx β¦ H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct
-elim (plus_inv_O3 β¦ H1) -H1 #H11 #H12 destruct
-elim (plus_inv_O3 β¦ H2) -H2 #H21 #H22 destruct
-elim (plus_inv_O3 β¦ H3) -H3 #H31 #H32 destruct
-/3 width=5 by ex3_2_intro/
-qed-.
-
-lemma ist_inv_plus_O_dx: βn,c1,c2. πβͺn,c1 + c2β« β πβͺ0,c2β« β πβͺn,c1β«.
-#n #c1 #c2 #H #H2
-elim (ist_inv_plus β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct //
-qed-.
-
-lemma ist_inv_plus_SO_dx:
- βn,c1,c2. πβͺn,c1 + c2β« β πβͺ1,c2β« β
- ββm. πβͺm,c1β« & n = βm.
-#n #c1 #c2 #H #H2 destruct
-elim (ist_inv_plus β¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-/2 width=3 by ex2_intro/
-qed-.
-
-lemma ist_inv_plus_10_dx: βn,c. πβͺn,c+ππβ« β β₯.
-#n #c #H
-elim (ist_inv_plus β¦ H) -H #n1 #n2 #_ #H #_
-/2 width=2 by ist_inv_10/
-qed-.
+++ /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/steps/rtc_shift.ma".
-include "ground/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-.
+++ /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/xoa/ex_6_8.ma".
-include "ground/steps/rtc.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-definition max (c1:rtc) (c2:rtc): rtc β match c1 with [
- mk_rtc ri1 rs1 ti1 ts1 β match c2 with [
- mk_rtc ri2 rs2 ti2 ts2 β β©ri1β¨ri2,rs1β¨rs2,ti1β¨ti2,ts1β¨ts2βͺ
- ]
-].
-
-interpretation "maximum (rtc)"
- 'or c1 c2 = (max c1 c2).
-
-(* Basic properties *********************************************************)
-
-lemma max_rew: βri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2.
- β©ri1β¨ri2,rs1β¨rs2,ti1β¨ti2,ts1β¨ts2βͺ =
- (β©ri1,rs1,ti1,ts1βͺ β¨ β©ri2,rs2,ti2,ts2βͺ).
-// qed.
-
-lemma max_O_dx: βc. c = (c β¨ ππ).
-* #ri #rs #ti #ts <max_rew //
-qed.
-
-lemma max_idem: βc. c = (c β¨ c).
-* #ri #rs #ti #ts <max_rew //
-qed.
-
-(* Basic inversion properties ***********************************************)
-
-lemma max_inv_dx: βri,rs,ti,ts,c1,c2. β©ri,rs,ti,tsβͺ = (c1 β¨ c2) β
- ββri1,rs1,ti1,ts1,ri2,rs2,ti2,ts2.
- (ri1β¨ri2) = ri & (rs1β¨rs2) = rs & (ti1β¨ti2) = ti & (ts1β¨ts2) = ts &
- β©ri1,rs1,ti1,ts1βͺ = c1 & β©ri2,rs2,ti2,ts2βͺ = c2.
-#ri #rs #ti #ts * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
-<max_rew #H destruct /2 width=14 by ex6_8_intro/
-qed-.
-
-(* Main Properties **********************************************************)
-
-theorem max_assoc: associative β¦ max.
-* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
-<max_rew <max_rew //
-qed.
+++ /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/steps/rtc_shift.ma".
-include "ground/steps/rtc_max.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-(* Properties with max and shift ********************************************)
-
-lemma max_shift: βc1,c2. ((β*c1) β¨ (β*c2)) = β*(c1β¨c2).
-* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
-<shift_rew <shift_rew <shift_rew <max_rew //
-qed.
+++ /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/xoa/ex_6_8.ma".
-include "ground/steps/rtc.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-definition plus (c1:rtc) (c2:rtc): rtc β match c1 with [
- mk_rtc ri1 rs1 ti1 ts1 β match c2 with [
- mk_rtc ri2 rs2 ti2 ts2 β β©ri1+ri2,rs1+rs2,ti1+ti2,ts1+ts2βͺ
- ]
-].
-
-interpretation "plus (rtc)"
- 'plus c1 c2 = (plus c1 c2).
-
-(* Basic properties *********************************************************)
-
-(**) (* plus is not disambiguated parentheses *)
-lemma plus_rew: βri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2.
- β©ri1+ri2,rs1+rs2,ti1+ti2,ts1+ts2βͺ =
- (β©ri1,rs1,ti1,ts1βͺ) + (β©ri2,rs2,ti2,ts2βͺ).
-// qed.
-
-lemma plus_O_dx: βc. c = c + ππ.
-* #ri #rs #ti #ts <plus_rew //
-qed.
-
-(* Basic inversion properties ***********************************************)
-
-lemma plus_inv_dx: βri,rs,ti,ts,c1,c2. β©ri,rs,ti,tsβͺ = c1 + c2 β
- ββri1,rs1,ti1,ts1,ri2,rs2,ti2,ts2.
- ri1+ri2 = ri & rs1+rs2 = rs & ti1+ti2 = ti & ts1+ts2 = ts &
- β©ri1,rs1,ti1,ts1βͺ = c1 & β©ri2,rs2,ti2,ts2βͺ = c2.
-#ri #rs #ti #ts * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
-<plus_rew #H destruct /2 width=14 by ex6_8_intro/
-qed-.
-
-(* Main Properties **********************************************************)
-
-theorem plus_assoc: associative β¦ plus.
-* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
-<plus_rew //
-qed.
+++ /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/xoa/ex_5_4.ma".
-include "ground/notation/functions/updownarrowstar_1.ma".
-include "ground/steps/rtc.ma".
-
-(* RT-TRANSITION COUNTER ****************************************************)
-
-definition shift (c:rtc): rtc β match c with
-[ mk_rtc ri rs ti ts β β©riβ¨rs,0,tiβ¨ts,0βͺ ].
-
-interpretation "shift (rtc)"
- 'UpDownArrowStar c = (shift c).
-
-(* Basic properties *********************************************************)
-
-lemma shift_rew: βri,rs,ti,ts. β©riβ¨rs,0,tiβ¨ts,0βͺ = β*β©ri,rs,ti,tsβͺ.
-normalize //
-qed.
-
-lemma shift_O: ππ = β*ππ.
-// qed.
-
-(* Basic inversion properties ***********************************************)
-
-lemma shift_inv_dx: βri,rs,ti,ts,c. β©ri,rs,ti,tsβͺ = β*c β
- ββri0,rs0,ti0,ts0. (ri0β¨rs0) = ri & 0 = rs & (ti0β¨ts0) = ti & 0 = ts &
- β©ri0,rs0,ti0,ts0βͺ = c.
-#ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <shift_rew #H destruct
-/2 width=7 by ex5_4_intro/
-qed-.
[ { "generic rt-transition counter" * } {
[ { "" * } {
[ "rtc_ist ( πβͺ?,?β« )" "rtc_ist_shift" "rtc_ist_plus" "rtc_ist_max" * ]
- [ "rtc_isrc ( ππβͺ?,?β« )" "rtc_isrt_shift" "rtc_isrt_plus" "rtc_isrt_max" "rtc_isrt_max_shift" * ]
+ [ "rtc_ism ( πβͺ?,?β« )" "rtc_ism_shift" "rtc_ism_plus" "rtc_ism_max" "rtc_ism_max_shift" * ]
[ "rtc ( β©?,?,?,?βͺ ) ( ππ ) ( ππ ) ( ππ )" "rtc_shift ( β*? )" "rtc_plus ( ? + ? )" "rtc_max ( ? β¨ ? )" "rtc_max_shift" * ]
}
]
(* pairs, projections *******************************************************)
-notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
-with precedence 90 for @{ 'pair $a $b}.
-
notation "hvbox(x break \times y)" with precedence 70
for @{ 'product $x $y}.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+(* Core notation *******************************************************)
+
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
+with precedence 90 for @{ 'pair $a $b}.
\ / GNU General Public License Version 2
V_______________________________________________________________ *)
+include "basics/core_notation/pair_2.ma".
include "basics/logic.ma".
(* void *)
(*
(* other notations **********************************************************)
-notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
-with precedence 90 for @{ 'pair $a $b}.
-
notation "hvbox(x break \times y)" with precedence 70
for @{ 'product $x $y}.
projects / helm.git / commitdiff