update in ground

+ arith restyled
+ recomm updated

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/Makefile b/matita/matita/contribs/lambdadelta/bin/recomm/Makefile
index cb3deebf664f0ffe5facc56325c2703559ab37b1..6fdc32c44de4ec0d335e07a6a0d8a9741ace44f5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/Makefile
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/Makefile
@@ -15,7 +15,7 @@ MRCS = $(wildcard *.mrc)
 mrc: $(MRCS:%.mrc=recommGc%.ml)
        @./mrc.native .
 
 mrc: $(MRCS:%.mrc=recommGc%.ml)
        @./mrc.native .
 

-recommGc%.ml recommGc%.mli: %.mrc mrc.ml
+recommGc%.ml recommGc%.mli: %.mrc mrc*.ml mrc*.mli

        @./mrc.native $<
 
 .PHONY: test mrc
        @./mrc.native $<
 
 .PHONY: test mrc

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc
new file mode 100644 (file)
index 0000000..561d9f9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundArith.mrc
@@ -0,0 +1,16 @@
+PcsAnd b "" true false
+niter
+ntri
+nsucc
+npred
+nplus
+nminus
+nmax
+nle
+nlt
+ysucc
+ypred
+yplus
+ylminus, yminus
+yle
+ylt

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundArith.mrc
new file mode 100644 (file)
index 0000000..2a721cf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundArith.mrc
@@ -0,0 +1,7 @@
+PccFor d "" true false
+POSITIVE INTEGERS
+NON-NEGATIVE INTEGERS
+NON-NEGATIVE INTEGERS WITH INFINITY
+WELL-FOUNDED INDUCTION
+λδ-2A
+λδ-2B

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
index abece29bbb6c5473a66f4a0750862dbd68dbb236..19128fb6397a2eb0721d052a03672ba57871588a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
@@ -2,8 +2,8 @@ module ET = MrcTypes
 
 let cap = String.capitalize_ascii
 
 
 let cap = String.capitalize_ascii
 

-let ok b =
-  if b then "true" else "ok"
+let ko b =
+  if b then "KO" else "OO"

 
 let write_mli name = 
   let file = name ^ ".mli" in
 
 let write_mli name = 
   let file = name ^ ".mli" in


@@ -17,8 +17,8 @@ let write_subst st och subst =
   let iter hd words =
     let lhs = List.map (Printf.sprintf "%S :: ") words in
     let rhs = List.map (Printf.sprintf "%S :: ") hd in
   let iter hd words =
     let lhs = List.map (Printf.sprintf "%S :: ") words in
     let rhs = List.map (Printf.sprintf "%S :: ") hd in

-    Printf.fprintf och "  | %stl -> k %s (%souts) tl\n"
-      (String.concat "" lhs) (ok st.ET.para) (String.concat "" rhs)
+    Printf.fprintf och "  | %stl -> k T.OK (%souts) tl\n"
+      (String.concat "" lhs) (String.concat "" rhs)

   in
   match subst with
   | []      -> ()
   in
   match subst with
   | []      -> ()


@@ -27,16 +27,23 @@ let write_subst st och subst =
 let write_component st =
   let cmod = "recommGc" ^ st.ET.cmod in
   let och = open_out (cmod ^ ".ml") in
 let write_component st =
   let cmod = "recommGc" ^ st.ET.cmod in
   let och = open_out (cmod ^ ".ml") in

+  Printf.fprintf och "module T = RecommTypes\n";
+  Printf.fprintf och "module R = Recomm%s\n" (cap st.ET.rmod);

   if st.ET.dmod <> "" then begin
   if st.ET.dmod <> "" then begin

-    Printf.fprintf och "module D = Recomm%s\n\n" (cap st.ET.dmod)
+    Printf.fprintf och "module D = Recomm%s\n" (cap st.ET.dmod)
+  end;
+  Printf.fprintf och "\n";
+  Printf.fprintf och "let step k st outs ins =\n";
+  if st.ET.para then begin
+    Printf.fprintf och "  if st <> T.OO then k st outs ins else\n"
+  end else begin
+    Printf.fprintf och "  if st = T.KO then k st outs ins else\n"

   end;
   end;

-  Printf.fprintf och "let step k ok outs ins =\n";
-  Printf.fprintf och "  if ok then k ok outs ins else\n";

   Printf.fprintf och "  match ins with\n";
   List.iter (write_subst st och) st.ET.substs;
   Printf.fprintf och "  match ins with\n";
   List.iter (write_subst st och) st.ET.substs;

-  Printf.fprintf och "  | _ -> k %s outs ins\n\n" (ok st.ET.optn);
+  Printf.fprintf och "  | _ -> k T.%s outs ins\n\n" (ko st.ET.optn);

   Printf.fprintf och "let main =\n";
   Printf.fprintf och "let main =\n";

-  Printf.fprintf och "  Recomm%s.register_%s step\n" (cap st.ET.rmod) st.ET.rfun;
+  Printf.fprintf och "  R.register_%s step\n" st.ET.rfun;

   close_out och;
   write_mli cmod
 
   close_out och;
   write_mli cmod
 


@@ -44,7 +51,7 @@ let write_index st =
   let cmod = Filename.concat st.ET.cdir "recommGc" in
   let och = open_out (cmod ^ ".ml") in
   let iter i name =
   let cmod = Filename.concat st.ET.cdir "recommGc" in
   let och = open_out (cmod ^ ".ml") in
   let iter i name =

-    Printf.fprintf och "module G%u = RecommGc%s\n" (succ i) name
+    Printf.fprintf och "module G%03u = RecommGc%s\n" (succ i) name

   in
   List.iteri iter st.ET.mods;
   close_out och;
   in
   List.iteri iter st.ET.mods;
   close_out och;

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc
new file mode 100644 (file)
index 0000000..226e772
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundArith.mrc
@@ -0,0 +1,2 @@
+PcsPar p "" true false
+(semigroup properties)

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc
new file mode 100644 (file)
index 0000000..bfc2730
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc
@@ -0,0 +1,14 @@
+PccFor r "" true false
+DISCRIMINATOR
+ITERATED FUNCTION
+TRICHOTOMY OPERATOR
+NAT-INJECTION
+SUCCESSOR
+PREDECESSOR
+ADDITION
+SUBTRACTION
+LEFT SUBTRACTION
+MAXIMUM, MAXIMUN
+ORDER
+STRICT ORDER
+ARITHMETICAL PROPERTIES

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc
index 72b0713509312bdd8000e68181219dc0668786f6..35503a9f366669d0db3d6597b815944edcc268c8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc
@@ -1,4 +1,2 @@
 PccFor r "" true false
 PccFor r "" true false

-ADDITION
-MAXIMUM, MAXIMUN

 SHIFT
 SHIFT

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml
index bac315438dea9bc465fbeff79c7946e982c43128..ce971dd452bb8a4cc304e53a63c39c574575c07f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml
@@ -5,6 +5,7 @@ module EO = RecommOutput
 
 module P1 = RecommPccFor
 module P2 = RecommPcsAnd
 
 module P1 = RecommPccFor
 module P2 = RecommPcsAnd

+module P3 = RecommPcsPar

 
 module G = RecommGc
 
 
 module G = RecommGc
 

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
index e5629ccc8468b509b75c3fdb3254c21486185cbf..655ff8095324a1a779f619bcaeef95f3ce2e41ac 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
@@ -5,7 +5,7 @@ let c_line = ref ES.id
 
 let s_line = ref ES.id
 
 
 let s_line = ref ES.id
 

-let k_final b ws1 ws2 = b, ws1, ws2  
+let k_final r ws1 ws2 = r, ws1, ws2

 
 type status =
   {
 
 type status =
   {


@@ -29,16 +29,17 @@ let middle st =
   | _              -> true
 
 let mute_o = [|
   | _              -> true
 
 let mute_o = [|

-  "___                                                              ";
-  "||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                  ";
+  "                                                                        ";
+  "       ___                                                              ";
+  "      ||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                  ";

   "";
 |]
 
   "";
 |]
 


@@ -78,9 +79,9 @@ let rec recomm srcs st =
     recomm tl @@ add hd @@ st
   | ET.Title ss :: tl              ->
     if middle st then Printf.eprintf "middle: TITLE\n";
     recomm tl @@ add hd @@ st
   | 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 r, ss1, ss2 = !c_line k_final ET.OO [] ss in

     let ss2 =
     let ss2 =

-      if ss2 = [] then ss2 else "*" :: ss2
+      if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2

     in
     let ss = List.rev_append ss1 ss2 in
     let s = String.concat " " ss in
     in
     let ss = List.rev_append ss1 ss2 in
     let s = String.concat " " ss in


@@ -88,9 +89,9 @@ let rec recomm srcs st =
     recomm tl @@ add (ET.Title ss) @@ st
   | ET.Slice ss :: tl              ->
     if middle st then Printf.eprintf "middle: Section\n";
     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 r, ss1, ss2 = !s_line k_final ET.OO [] ss in

     let ss2 =
     let ss2 =

-      if ss2 = [] then ss2 else "*" :: ss2
+      if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2

     in
     let ss = List.rev_append ss1 ss2 in
     let s = String.capitalize_ascii (String.concat " " ss) in
     in
     let ss = List.rev_append ss1 ss2 in
     let s = String.capitalize_ascii (String.concat " " ss) in

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml
index 12a3ec66491ba8a703ac5186e57417602e85c4a3..b3fd0b550641f48edaf6e55306eb9cde8560793b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml
@@ -1,6 +1,10 @@
-module G1 = RecommGcbGroundCounters
-module G2 = RecommGcdGroundCounters
-module G3 = RecommGcrGroundCounters
-module G4 = RecommGcsAttr
-module G5 = RecommGcsMain
-module G6 = RecommGcsWith
+module G001 = RecommGcbGroundArith
+module G002 = RecommGcbGroundCounters
+module G003 = RecommGcdGroundArith
+module G004 = RecommGcdGroundCounters
+module G005 = RecommGcpGroundArith
+module G006 = RecommGcrGroundArith
+module G007 = RecommGcrGroundCounters
+module G008 = RecommGcsAttr
+module G009 = RecommGcsMain
+module G010 = RecommGcsWith

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
new file mode 100644 (file)
index 0000000..1528eb2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
@@ -0,0 +1,26 @@
+module T = RecommTypes
+module R = RecommPcsAnd
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "ylt" :: tl -> k T.OK ("ylt" :: outs) tl
+  | "yle" :: tl -> k T.OK ("yle" :: outs) tl
+  | "ylminus" :: tl -> k T.OK ("ylminus" :: outs) tl
+  | "yminus" :: tl -> k T.OK ("ylminus" :: outs) tl
+  | "yplus" :: tl -> k T.OK ("yplus" :: outs) tl
+  | "ypred" :: tl -> k T.OK ("ypred" :: outs) tl
+  | "ysucc" :: tl -> k T.OK ("ysucc" :: outs) tl
+  | "nlt" :: tl -> k T.OK ("nlt" :: outs) tl
+  | "nle" :: tl -> k T.OK ("nle" :: outs) tl
+  | "nmax" :: tl -> k T.OK ("nmax" :: outs) tl
+  | "nminus" :: tl -> k T.OK ("nminus" :: outs) tl
+  | "nplus" :: tl -> k T.OK ("nplus" :: outs) tl
+  | "npred" :: tl -> k T.OK ("npred" :: outs) tl
+  | "nsucc" :: tl -> k T.OK ("nsucc" :: outs) tl
+  | "ntri" :: tl -> k T.OK ("ntri" :: outs) tl
+  | "niter" :: tl -> k T.OK ("niter" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_b step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.mli
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml
index 53a98c92e2f30b1297b3f8bd218b2fddab8a726a..8391c7da928a96bce36f497025da181abf5ca391 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml
@@ -1,10 +1,13 @@
-let step k ok outs ins =
-  if ok then k ok outs ins else
+module T = RecommTypes
+module R = RecommPcsAnd
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else

   match ins with
   match ins with

-  | "rtc_plus" :: tl -> k true ("rtc_plus" :: outs) tl
-  | "rtc_max" :: tl -> k true ("rtc_max" :: outs) tl
-  | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl
-  | _ -> k ok outs ins
+  | "rtc_plus" :: tl -> k T.OK ("rtc_plus" :: outs) tl
+  | "rtc_max" :: tl -> k T.OK ("rtc_max" :: outs) tl
+  | "rtc_shift" :: tl -> k T.OK ("rtc_shift" :: outs) tl
+  | _ -> k T.OO outs ins

 
 let main =
 
 let main =

-  RecommPcsAnd.register_b step
+  R.register_b step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.ml
new file mode 100644 (file)
index 0000000..b3ed0f2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.ml
@@ -0,0 +1,16 @@
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "\206\187\206\180-2B" :: tl -> k T.OK ("\206\187\206\180-2B" :: outs) tl
+  | "\206\187\206\180-2A" :: tl -> k T.OK ("\206\187\206\180-2A" :: outs) tl
+  | "WELL-FOUNDED" :: "INDUCTION" :: tl -> k T.OK ("INDUCTION" :: "WELL-FOUNDED" :: outs) tl
+  | "NON-NEGATIVE" :: "INTEGERS" :: "WITH" :: "INFINITY" :: tl -> k T.OK ("INFINITY" :: "WITH" :: "INTEGERS" :: "NON-NEGATIVE" :: outs) tl
+  | "NON-NEGATIVE" :: "INTEGERS" :: tl -> k T.OK ("INTEGERS" :: "NON-NEGATIVE" :: outs) tl
+  | "POSITIVE" :: "INTEGERS" :: tl -> k T.OK ("INTEGERS" :: "POSITIVE" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_d step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundArith.mli
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml
index 796c21168adf2238cbea618af9ac36e2722a0dfd..bcbbc71028f28d0e6815b7b74b162df64c55072e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml
@@ -1,10 +1,13 @@
-let step k ok outs ins =
-  if ok then k ok outs ins else
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else

   match ins with
   match ins with

-  | "T-TRANSITION" :: "COUNTERS" :: 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" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: outs) tl
-  | _ -> k ok outs ins
+  | "T-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "T-TRANSITION" :: outs) tl
+  | "T-BOUND" :: "RT-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl
+  | "RT-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "RT-TRANSITION" :: outs) tl
+  | _ -> k T.OO outs ins

 
 let main =
 
 let main =

-  RecommPccFor.register_d step
+  R.register_d step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
new file mode 100644 (file)
index 0000000..7005e5c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.ml
@@ -0,0 +1,11 @@
+module T = RecommTypes
+module R = RecommPcsPar
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "(semigroup" :: "properties)" :: tl -> k T.OK ("properties)" :: "(semigroup" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_p step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundArith.mli
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
new file mode 100644 (file)
index 0000000..091cc7f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
@@ -0,0 +1,24 @@
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "ARITHMETICAL" :: "PROPERTIES" :: tl -> k T.OK ("PROPERTIES" :: "ARITHMETICAL" :: outs) tl
+  | "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl
+  | "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl
+  | "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
+  | "MAXIMUN" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
+  | "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
+  | "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
+  | "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
+  | "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
+  | "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
+  | "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl
+  | "TRICHOTOMY" :: "OPERATOR" :: tl -> k T.OK ("OPERATOR" :: "TRICHOTOMY" :: outs) tl
+  | "ITERATED" :: "FUNCTION" :: tl -> k T.OK ("FUNCTION" :: "ITERATED" :: outs) tl
+  | "DISCRIMINATOR" :: tl -> k T.OK ("DISCRIMINATOR" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_r step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.mli
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml
index d85161fa42a43f0af45c60bb721f3e1169d967d3..4defad66e5cf178d12ba4f5f104350373f46d0fa 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml
@@ -1,11 +1,11 @@
-let step k ok outs ins =
-  if ok then k ok outs ins else
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else

   match ins with
   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
+  | "SHIFT" :: tl -> k T.OK ("SHIFT" :: outs) tl
+  | _ -> k T.OO outs ins

 
 let main =
 
 let main =

-  RecommPccFor.register_r step
+  R.register_r step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml
index cb7037f678271f91f9621755b0fe6b98a2a39d1c..83c402ebb2ef459c68daafec1bb1975dd23e8ed4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsAttr.ml
@@ -1,10 +1,14 @@
-let step k ok outs ins =
-  if ok then k ok outs ins else
+module T = RecommTypes
+module R = RecommCheck
+
+let step k st outs ins =
+  if st = T.KO then k st outs ins else

   match ins with
   match ins with

-  | "main" :: tl -> k ok ("main" :: outs) tl
-  | "basic" :: tl -> k ok ("basic" :: outs) tl
-  | "advanced" :: tl -> k ok ("advanced" :: outs) tl
-  | _ -> k ok outs ins
+  | "main" :: tl -> k T.OK ("main" :: outs) tl
+  | "helper" :: tl -> k T.OK ("helper" :: outs) tl
+  | "basic" :: tl -> k T.OK ("basic" :: outs) tl
+  | "advanced" :: tl -> k T.OK ("advanced" :: outs) tl
+  | _ -> k T.OO outs ins

 
 let main =
 
 let main =

-  RecommCheck.register_s step
+  R.register_s step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml
index 82905b8406570b6ea0138d7515daeb15a7e16f47..d308df8dbaa55a604fdef8fa33eb6a59ba0d6166 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsMain.ml
@@ -1,19 +1,24 @@
+module T = RecommTypes
+module R = RecommCheck

 module D = RecommGcsAttr
 
 module D = RecommGcsAttr
 

-let step k ok outs ins =
-  if ok then k ok outs ins else
+let step k st outs ins =
+  if st = T.KO then k st outs ins else

   match ins with
   match ins with

-  | "eliminations" :: tl -> k ok ("eliminations" :: outs) tl
-  | "eliminators" :: tl -> k ok ("eliminations" :: outs) tl
-  | "destructions" :: tl -> k ok ("destructions" :: outs) tl
-  | "forward" :: "properties" :: tl -> k ok ("destructions" :: outs) tl
-  | "forward" :: "lemmas" :: tl -> k ok ("destructions" :: outs) tl
-  | "inversions" :: tl -> k ok ("inversions" :: outs) tl
-  | "inversion" :: "properties" :: tl -> k ok ("inversions" :: outs) tl
-  | "inversion" :: "lemmas" :: tl -> k ok ("inversions" :: outs) tl
-  | "constructions" :: tl -> k ok ("constructions" :: outs) tl
-  | "properties" :: tl -> k ok ("constructions" :: outs) tl
-  | _ -> k true outs ins
+  | "iterators" :: tl -> k T.OK ("iterators" :: outs) tl
+  | "eliminations" :: tl -> k T.OK ("eliminations" :: outs) tl
+  | "eliminators" :: tl -> k T.OK ("eliminations" :: outs) tl
+  | "equalities" :: tl -> k T.OK ("equalities" :: outs) tl
+  | "destructions" :: tl -> k T.OK ("destructions" :: outs) tl
+  | "forward" :: "properties" :: tl -> k T.OK ("destructions" :: outs) tl
+  | "forward" :: "lemmas" :: tl -> k T.OK ("destructions" :: outs) tl
+  | "inversions" :: tl -> k T.OK ("inversions" :: outs) tl
+  | "inversion" :: "properties" :: tl -> k T.OK ("inversions" :: outs) tl
+  | "inversion" :: "lemmas" :: tl -> k T.OK ("inversions" :: outs) tl
+  | "inversion" :: tl -> k T.OK ("inversions" :: outs) tl
+  | "constructions" :: tl -> k T.OK ("constructions" :: outs) tl
+  | "properties" :: tl -> k T.OK ("constructions" :: outs) tl
+  | _ -> k T.KO outs ins

 
 let main =
 
 let main =

-  RecommCheck.register_s step
+  R.register_s step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml
index 8e1d810a2bf92d225b57f07e721fd39a64c77155..091bb2d12a447aa129d300813f77b68e2cf4d485 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml
@@ -1,10 +1,12 @@
+module T = RecommTypes
+module R = RecommCheck

 module D = RecommGcsMain
 
 module D = RecommGcsMain
 

-let step k ok outs ins =
-  if ok then k ok outs ins else
+let step k st outs ins =
+  if st = T.KO then k st outs ins else

   match ins with
   match ins with

-  | "with" :: tl -> k ok ("with" :: outs) tl
-  | _ -> k true outs ins
+  | "with" :: tl -> k T.OK ("with" :: outs) tl
+  | _ -> k T.OO outs ins

 
 let main =
 
 let main =

-  RecommCheck.register_s step
+  R.register_s step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
index 21cca9c6c21529ea6a4a3b0d5f7e1ad387496d53..99ff840af11fddea6f36185c88ce325d03a0c248 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
@@ -8,15 +8,18 @@
   |]
 
   let heads = [|
   |]
 
   let heads = [|

-    "Advanved";
+    "Advanced";

     "Basic";
     "Constructions";
     "Forward";
     "Destructions";
     "Eliminations";
     "Eliminators";
     "Basic";
     "Constructions";
     "Forward";
     "Destructions";
     "Eliminations";
     "Eliminators";

+    "Equalities";
+    "Helper";

     "Inversion";
     "Inversions";
     "Inversion";
     "Inversions";

+    "Iterators";

     "Main";
     "Properties";
   |]
     "Main";
     "Properties";
   |]


@@ -53,7 +56,7 @@ let CR = "\r"
 let SP = " "
 let NL = "\n"
 let SR = "*"
 let SP = " "
 let NL = "\n"
 let SR = "*"

-let OP = "(*" SP*
+let OP = "(*"

 let CP = SR* "*)"  
 let PP = CP SP* OP
 let WF = ['A'-'Z' 'a'-'z']
 let CP = SR* "*)"  
 let PP = CP SP* OP
 let WF = ['A'-'Z' 'a'-'z']

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
index fe8bebe945148fdd03ce6450c4b8b3f1bdbc56ec..e0f3f1d70397327d87a3dd60e1181a238e44cdb7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
@@ -4,8 +4,17 @@ let width = ref 78
 
 let replace = ref false
 
 
 let replace = ref false
 

+let string_length_utf8 s =
+  let l = String.length s in
+  let rec aux r i =
+    if i >= l then r else
+    if '\x80' <= s.[i] && s.[i] <= '\xBF'
+    then aux (succ r) (succ i) else aux r (succ i)  
+  in
+  l - aux 0 0
+

 let complete s =
 let complete s =

-  let l = !width - String.length s - 6 in
+  let l = !width - string_length_utf8 s - 6 in

   if l < 0 then begin
     Printf.eprintf "overfull: %S\n" s;
     ""
   if l < 0 then begin
     Printf.eprintf "overfull: %S\n" s;
     ""


@@ -19,7 +28,7 @@ let out_src och = function
   | ET.Text s             ->
     Printf.fprintf och "%s" s
   | ET.Mark s             ->
   | ET.Text s             ->
     Printf.fprintf och "%s" s
   | ET.Mark s             ->

-    Printf.fprintf och "(* %s**)" s
+    Printf.fprintf och "(* *%s*)" s

   | ET.Key (s1, s2)       ->
     Printf.fprintf och "(* %s%s*)" s1 s2
   | ET.Title ss           ->
   | ET.Key (s1, s2)       ->
     Printf.fprintf och "(* %s%s*)" s1 s2
   | ET.Title ss           ->

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly b/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly
index 5686e747effbe3efe959aaf0203f3dc1f33dcbd1..79512c7c4db97c1250390960fe9ec6ad94116e6d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly
@@ -14,17 +14,21 @@
 
 %%
 
 
 %%
 

-inn_r:
+sp:
+  |    { "" }

   | SP { $1 }
   | SP { $1 }

+
+inn_r:

   | NL { $1 }
   | SW { $1 }
   | OT { $1 }
 
 inn:
   | inn_r { $1 }
   | NL { $1 }
   | SW { $1 }
   | OT { $1 }
 
 inn:
   | inn_r { $1 }

-  | KW      { $1 }
-  | CW      { $1 }
-  | HW      { $1 }
+  | SP    { $1 }
+  | KW    { $1 }
+  | CW    { $1 }
+  | HW    { $1 }

 
 inns_r:
   | inn_r      { $1      }
 
 inns_r:
   | inn_r      { $1      }


@@ -47,14 +51,27 @@ outs:
   | out      { $1      }
   | out outs { $1 ^ $2 } 
 
   | out      { $1      }
   | out outs { $1 ^ $2 } 
 

-sw:
-  | HW { lc $1 }
-  | SW { lc $1 }
+cc:
+  | CW { $1 }
+  | OT { $1 }
+
+cw:
+  | cc    { $1      }
+  | cc cw { $1 ^ $2 }

 
 cws:
   |           { []       }
   | SP        { []       }
 
 cws:
   |           { []       }
   | SP        { []       }

-  | SP CW cws { $2 :: $3 }
+  | SP cw cws { $2 :: $3 }
+
+sc:
+  | HW { lc $1 }
+  | SW { lc $1 }
+  | OT { $1    }
+
+sw:
+  | sc    { $1      }
+  | sc sw { $1 ^ $2 }

 
 sws:
   |           { []       }
 
 sws:
   |           { []       }


@@ -63,14 +80,15 @@ sws:
 
 src_l:
   | NL               { ET.Line  $1                     }
 
 src_l:
   | NL               { ET.Line  $1                     }

-  | OP PP inns CP    { ET.Mark  $3                     }
-  | OP KW inns CP    { ET.Key   ($2, $3)               }
-  | OP CW cws CP     { ET.Title ($2 :: $3)             }
-  | OP HW sws CP     { ET.Slice (lc $2 :: $3)          }
-  | OP CP            { ET.Other ($1, "", $2)           }
-  | OP inns_r CP     { ET.Other ($1, $2, $3)           }
+  | OP sp PP inns CP { ET.Mark  $4                     }
+  | OP sp KW inns CP { ET.Key   ($3, $4)               }
+  | OP sp CW cws CP  { ET.Title ($3 :: $4)             }
+  | OP sp HW sws CP  { ET.Slice (lc $3 :: $4)          }
+  | OP sp CP         { ET.Other ($1, $2, $3)           }
+  | OP sp inns_r CP  { ET.Other ($1, $2 ^ $3, $4)      }

   | OP SR inns CP    { ET.Other ($1, $2 ^ $3, $4)      }
   | OP SR SR inns CP { ET.Other ($1, $2 ^ $3 ^ $4, $5) }
   | OP SR inns CP    { ET.Other ($1, $2 ^ $3, $4)      }
   | OP SR SR inns CP { ET.Other ($1, $2 ^ $3 ^ $4, $5) }

+  | OP SP SR inns CP { ET.Mark  $4                     }

 
 src:
   | outs { ET.Text $1 }
 
 src:
   | outs { ET.Text $1 }

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
index cdad8df5599a13ce628bc91706fc2a74fba35482..41a787dbd3c5dbeea522cb341b9b838723a56731 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
@@ -1,26 +1,28 @@
 module EC = RecommCheck
 module ES = RecommStep
 module EC = RecommCheck
 module ES = RecommStep

+module ET = RecommTypes

 
 let d_line = ref ES.id
 
 let r_line = ref ES.id
 
 
 let d_line = ref ES.id
 
 let r_line = ref ES.id
 

-let k_for k ok outs ins =
-  if ok then begin
-    match ins with
-    | "FOR" :: tl -> !d_line k false ("FOR" :: outs) tl
-    | _           -> k true outs ins
-  end else begin
-    k true outs ins
-  end
-
-let k_or k ok outs ins =
-  if ok then k ok outs ins else
-  !r_line (k_for k) ok outs ins
-
-let step k ok outs ins =
-  if ok then k ok outs ins else
-  !d_line (k_or k) ok outs ins
+let k_exit k st out ins =
+  if st <> ET.OK then k ET.KO out ins else
+  k st out ins
+
+let k_for k st outs ins =
+  if st <> ET.OK then k ET.KO outs ins else
+  match ins with
+  | "FOR" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl
+  | _           -> k ET.KO outs ins
+
+let k_or k st outs ins =
+  if st <> ET.OO then k st outs ins else
+  !r_line (k_for k) st outs ins
+
+let step k st outs ins =
+  if st = ET.KO then k st outs ins else
+  !d_line (k_or k) ET.OO outs ins

 
 let register_d =
   ES.register d_line
 
 let register_d =
   ES.register d_line

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml
index de05255a557f8690b491f2f4452539b216449f89..cf09e52ce1dd850817c238608a6bd0989f9eccba 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsAnd.ml
@@ -1,22 +1,20 @@
 module EC = RecommCheck
 module ES = RecommStep
 module EC = RecommCheck
 module ES = RecommStep

+module ET = RecommTypes

 
 module D = RecommGcsWith
 
 let b_line = ref ES.id
 
 
 module D = RecommGcsWith
 
 let b_line = ref ES.id
 

-let rec k_and k ok outs ins =
-  if ok then begin
-    match ins with
-    | "and" :: tl -> step k false ("and" :: outs) tl
-    | _           -> k true outs ins
-  end else begin
-    k true outs ins
-  end
+let rec k_and k st outs ins =
+  if st <> ET.OK then k ET.KO outs ins else
+  match ins with
+  | "and" :: tl -> step k ET.OK ("and" :: outs) tl
+  | _           -> k ET.OK outs ins

 
 

-and step k ok outs ins =
-  if ok then k ok outs ins else
-  !b_line (k_and k) ok outs ins
+and step k st outs ins =
+  if st <> ET.OK then k st outs ins else
+  !b_line (k_and k) ET.OO outs ins 

 
 let register_b =
   ES.register b_line
 
 let register_b =
   ES.register b_line

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml
new file mode 100644 (file)
index 0000000..52a1c00
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.ml
@@ -0,0 +1,17 @@
+module EC = RecommCheck
+module ES = RecommStep
+module ET = RecommTypes
+
+module D = RecommPcsAnd
+
+let p_line = ref ES.id
+
+let step k st outs ins =
+  if st = ET.KO then k st outs ins else
+  !p_line k ET.OO outs ins
+
+let register_p =
+  ES.register p_line
+
+let main =
+  EC.register_s step

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.mli
new file mode 100644 (file)
index 0000000..451e242
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPcsPar.mli
@@ -0,0 +1 @@
+val register_p: RecommTypes.step -> unit

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli
index df91cd169b4068e08ad00376928d775f9289228d..76003832a090ec7331f373cbf0733c04e8ecfbbc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommStep.mli
@@ -1,4 +1,3 @@
 val id: ('s, 't) RecommTypes.astep
 
 val register: ('s, 't) RecommTypes.astep ref -> ('s, 't) RecommTypes.astep -> unit
 val id: ('s, 't) RecommTypes.astep
 
 val register: ('s, 't) RecommTypes.astep ref -> ('s, 't) RecommTypes.astep -> unit

- 

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml
index f2f8e87a9bfcb4fe6012932313d6a5c438de2ec1..7225e916e2368aff21821118aea7e5f05bd82187 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml
@@ -26,4 +26,8 @@ type ('s, 't) aproc = 's -> words -> words -> 't
 
 type ('s, 't) astep = ('s, 't) aproc -> ('s, 't) aproc
 
 
 type ('s, 't) astep = ('s, 't) aproc -> ('s, 't) aproc
 

-type step = (bool, bool * words * words) astep
+type return = KO
+            | OK
+            | OO
+
+type step = (return, return * words * words) astep

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc
index 4daa8ba06acadd01320ca6e95bfcf8b5e6f93adf..7d8aadcfffd03c58c4cfc1b8902a2b993ff5a029 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/sAttr.mrc
@@ -1,4 +1,5 @@
 check s "" false false
 advanced
 basic
 check s "" false false
 advanced
 basic

+helper

 main
 main

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc
index 8ed0ff28d1198edcfc9fd285821e98c61a97e021..fbb9e2dc552c5692c9a7c4f00e1df247601b53d8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/sMain.mrc
@@ -1,5 +1,7 @@
 check s "GcsAttr" false true
 constructions, properties
 check s "GcsAttr" false true
 constructions, properties

-inversions, inversion properties, inversion lemmas
+inversions,  inversion properties, inversion lemmas, inversion

 destructions, forward properties, forward lemmas
 destructions, forward properties, forward lemmas

+equalities

 eliminations, eliminators
 eliminations, eliminators

+iterators

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc
index 1a7d1fbfbeb58667b280f78d41bdc0b6ad2576b6..ecd022556a42570ee3385df55ca897630fa9b0de 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc
@@ -1,2 +1,2 @@
-check s "GcsMain" false true
+check s "GcsMain" false false

 with
 with

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
index 5e131af37b8f211f269a83f77eca4e5f1ebb3fd9..d54738f250b4100fea5bbdde0c20518572aad361 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
@@ -15,9 +15,9 @@
 include "ground/arith/nat_plus.ma".
 include "ground/arith/nat_le.ma".
 
 include "ground/arith/nat_plus.ma".
 include "ground/arith/nat_le.ma".
 

-(* ORDER FOR NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)

 
 

-(* Constructions with nplus ***********************************************************)
+(* Constructions with nplus *************************************************)

 
 (*** monotonic_le_plus_l *)
 lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.
 
 (*** monotonic_le_plus_l *)
 lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
index 44c3539b9eb0035c26509880827f14df182de90e..cb902736e1de5bbc7c1c02d33a2a79d4fadc4fad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
@@ -39,7 +39,7 @@ qed.
 (*** max_SS *)
 lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
 #n1 #n2
 (*** max_SS *)
 lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
 #n1 #n2

-@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion gets in the way *)
+@trans_eq [3: @ntri_succ_bi | skip ] (* * rewrite fails because δ-expansion gets in the way *)

 <ntri_f_tri //
 qed.
 
 <ntri_f_tri //
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index 2f0f4b658a7251e0f5b69ea023505dfdbb647b6e..75ff371fb108a84e9847927ca670fd2af4c822f5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -50,7 +50,7 @@ lemma niter_plus (A) (f) (n1) (n2):
 /3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
 qed.
 
 /3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
 qed.
 

-(* Advanved constructions (semigroup properties) ****************************)
+(* Advanced constructions (semigroup properties) ****************************)

 
 (*** plus_S1 *)
 lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
 
 (*** plus_S1 *)
 lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.


@@ -65,7 +65,7 @@ qed.
 (*** commutative_plus *)
 lemma nplus_comm: commutative … nplus.
 #m @(nat_ind_succ … m) -m //
 (*** commutative_plus *)
 lemma nplus_comm: commutative … nplus.
 #m @(nat_ind_succ … m) -m //

-qed-. (**) (* gets in the way with auto *)
+qed-. (* * gets in the way with auto *)

 
 (*** associative_plus *)
 lemma nplus_assoc: associative … nplus.
 
 (*** associative_plus *)
 lemma nplus_assoc: associative … nplus.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
index b7f9918b08d0191cf52391c310700d278be31116..3d79e371ebb0561e12510868a5af77df236c3868 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
@@ -24,7 +24,7 @@ lemma npred_succ (n): n = ↓↑n.
 * //
 qed.
 
 * //
 qed.
 

-(* Inversion with nsucc *****************************************************)
+(* Inversions with nsucc ****************************************************)

 
 (*** nat_split *)
 lemma nat_split_zero_pos (n): ∨∨ 𝟎 = n | n = ↑↓n.
 
 (*** nat_split *)
 lemma nat_split_zero_pos (n): ∨∨ 𝟎 = n | n = ↑↓n.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
index 63627965422fbdbc5a604e86c774497d3516f433..bb2300f021a2e549d6f25bbb13dd49ace62a07cc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
@@ -60,7 +60,7 @@ lemma nat_ind_2_succ (Q:relation2 …):
 #m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
 qed-.
 
 #m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
 qed-.
 

-(* Basic inversions ***************************************************************)
+(* Basic inversions *********************************************************)

 
 (*** injective_S *)
 lemma eq_inv_nsucc_bi: injective … nsucc.
 
 (*** injective_S *)
 lemma eq_inv_nsucc_bi: injective … nsucc.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index 1babf8eea5ea43544d48c15efe6894d50c7fca4d..8fd6b5c47034a1cf6783ab55845b669dce8e9513 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -43,7 +43,7 @@ qed.
 
 lemma pplus_comm: commutative … pplus.
 #p elim p -p //
 
 lemma pplus_comm: commutative … pplus.
 #p elim p -p //

-qed-. (**) (* gets in the way with auto *)
+qed-. (* * gets in the way with auto *)

 
 lemma pplus_assoc: associative … pplus.
 #p #q #r elim r -r //
 
 lemma pplus_assoc: associative … pplus.
 #p #q #r elim r -r //

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma
index b4aac4eff753341a1dfa8b702cebf4ca96b1b632..7522eb6971c8a1d26f3ada54712c01e3e7f5f73e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat.ma
@@ -35,7 +35,7 @@ interpretation
   "infinity (non-negative integers with infinity)"
   'Infinity = yinf.
 
   "infinity (non-negative integers with infinity)"
   'Infinity = yinf.
 

-(* Inversion lemmas *********************************************************)
+(* Inversions ***************************************************************)

 
 (* Note: destruct *)
 (*** yinj_inj *)
 
 (* Note: destruct *)
 (*** yinj_inj *)


@@ -43,7 +43,7 @@ lemma eq_inv_yinj_bi (y1) (y2): yinj y1 = yinj y2 → y1 = y2.
 #x #y #H destruct //
 qed-.
 
 #x #y #H destruct //
 qed-.
 

-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)

 
 (*** eq_ynat_dec *)
 lemma eq_ynat_dec (y1,y2:ynat): Decidable (y1 = y2).
 
 (*** eq_ynat_dec *)
 lemma eq_ynat_dec (y1,y2:ynat): Decidable (y1 = y2).

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_plus.ma
index b45afa8d4deb232523e1dd0a70ac95a8d3582476..3b56c47488929387c84997f87e8830f3866f572d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_le_lminus_plus.ma
@@ -19,7 +19,7 @@ include "ground/arith/ynat_le_lminus.ma".
 
 (* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
 
 
 (* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
 

-(* Constructions with yminus and yplus **************************************)
+(* Constructions with ylminus and yplus *************************************)

 
 (*** yle_plus1_to_minus_inj2 *)
 lemma yle_plus_sn_dx_lminus_dx (n) (x) (z):
 
 (*** yle_plus1_to_minus_inj2 *)
 lemma yle_plus_sn_dx_lminus_dx (n) (x) (z):


@@ -43,7 +43,7 @@ lemma yle_plus_dx_sn_lminus_sn (o) (x) (y):
       x ≤ yinj_nat o + y → x - o ≤ y.
 /2 width=1 by yle_plus_dx_dx_lminus_sn/ qed.
 
       x ≤ yinj_nat o + y → x - o ≤ y.
 /2 width=1 by yle_plus_dx_dx_lminus_sn/ qed.
 

-(* Destructions with yminus and yplus ***************************************)
+(* Destructions with ylminus and yplus **************************************)

 
 (*** yplus_minus_comm_inj *)
 lemma ylminus_plus_comm_23 (n) (x) (z):
 
 (*** yplus_minus_comm_inj *)
 lemma ylminus_plus_comm_23 (n) (x) (z):


@@ -77,7 +77,7 @@ lemma ylminus_assoc_comm_23 (n) (o) (x):
 ]
 qed-.
 
 ]
 qed-.
 

-(* Inversions with yminus and yplus *****************************************)
+(* Inversions with ylminus and yplus ****************************************)

 
 (*** yminus_plus *)
 lemma yplus_lminus_sn_refl_sn (n) (x):
 
 (*** yminus_plus *)
 lemma yplus_lminus_sn_refl_sn (n) (x):


@@ -95,7 +95,7 @@ lemma eq_inv_yplus_bi_inj_md (n1) (m2) (x1) (y2):
 #n1 #m2 #x1 #y2 #Hnx1 #H12
 lapply (yle_plus_bi_dx (yinj_nat m2) … Hnx1) >H12 #H
 lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2
 #n1 #m2 #x1 #y2 #Hnx1 #H12
 lapply (yle_plus_bi_dx (yinj_nat m2) … Hnx1) >H12 #H
 lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2

-generalize in match H12; -H12 (**) (* rewrite in hyp *)
+generalize in match H12; -H12 (* * rewrite in hyp *)

 >(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
 lapply (eq_inv_yplus_bi_dx_inj … H) -H
 >(yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H
 >(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
 lapply (eq_inv_yplus_bi_dx_inj … H) -H
 >(yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
index 15e58fd55809d51b2eee55ac68bc048d96ffc215..04cd607c9b2269c4317007342b06b3c85983dc33 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
@@ -61,7 +61,7 @@ qed.
 
 (* Advanced constructions ***************************************************)
 
 
 (* Advanced constructions ***************************************************)
 

-(* yminus_O1 *)
+(*** yminus_O1 *)

 lemma ylminus_zero_sn (n): 𝟎 = 𝟎 - n.
 // qed.
 
 lemma ylminus_zero_sn (n): 𝟎 = 𝟎 - n.
 // qed.
 

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma
index a76ccd946a82befad658be803bd70bea315ea11f..e9531df33e6ba4f7725878675d7d060120d2c14f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt.ma
@@ -29,7 +29,7 @@ interpretation
 
 (* Basic destructions *******************************************************)
 
 
 (* Basic destructions *******************************************************)
 

-(* ylt_fwd_gen ylt_inv_Y2 *)
+(*** ylt_fwd_gen ylt_inv_Y2 *)

 lemma ylt_des_gen_sn (x) (y):
       x < y → ∃m. x = yinj_nat m.
 #x #y * -x -y
 lemma ylt_des_gen_sn (x) (y):
       x < y → ∃m. x = yinj_nat m.
 #x #y * -x -y

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma
index 84edec50f6725d45c748eb6d8c4e1570fb654935..9c4939f47b8000ad9fda18f1a537d48f6bece3f6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma
@@ -67,7 +67,7 @@ lemma nle_ylt_trans (m) (n) (z):
 
 (* Inversions with yle ******************************************************)
 
 
 (* Inversions with yle ******************************************************)
 

-(* ylt_yle_false *)
+(*** ylt_yle_false *)

 lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥.
 /3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-.
 
 lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥.
 /3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
index 04e0c4c3c8003ff0442c3bd5035b5531f15e250d..7c7b64f1ab3d6c4d4a3b22cf8f1d0fd38f7c2078 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
@@ -19,7 +19,7 @@ include "ground/arith/ynat_lt.ma".
 
 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
 
 
 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
 

-(* Cobstructions with yle and ylminus  **************************************)
+(* Constructions with yle and ylminus ***************************************)

 
 (*** monotonic_ylt_minus_dx *)
 lemma ylt_lminus_bi_dx (o) (x) (y):
 
 (*** monotonic_ylt_minus_dx *)
 lemma ylt_lminus_bi_dx (o) (x) (y):

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma
index 6a66bded3d53f813a9aab4ab7b86a19dcb2edbcc..c39589b9986a5f00cdb245c9a4d5a64e734e307a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma
@@ -17,7 +17,7 @@ include "ground/arith/ynat_lt_le_lminus.ma".
 
 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
 
 
 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
 

-(* Constructions with yle and ylminus and yplus  ****************************)
+(* Constructions with yle and ylminus and yplus *****************************)

 
 (*** ylt_plus2_to_minus_inj2 *)
 lemma ylt_plus_dx_dx_lminus_sn (o) (x) (y):
 
 (*** ylt_plus2_to_minus_inj2 *)
 lemma ylt_plus_dx_dx_lminus_sn (o) (x) (y):

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma
index 73e38daeb4d5648f85521c8e3162f4d0789b4a16..56a6dadc9f1f6f759808075c71587f6701861544 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma
@@ -24,7 +24,7 @@ lemma ylt_le_succ_sn (x) (y):
       x < ∞ → ↑x ≤ y → x < y.
 /3 width=3 by ylt_yle_trans, ylt_succ_dx_refl/ qed.
 
       x < ∞ → ↑x ≤ y → x < y.
 /3 width=3 by ylt_yle_trans, ylt_succ_dx_refl/ qed.
 

-(* Inversions and destructions on yle ***************************************)
+(* Inversions with yle and ysucc ********************************************)

 
 (*** ylt_inv_le *)
 lemma ylt_inv_le_succ_sn (x) (y):
 
 (*** ylt_inv_le *)
 lemma ylt_inv_le_succ_sn (x) (y):

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma
index 8f8ecd3aa07322142f444cdb9a90192285137a09..06e7d081326ffecc2b5f2b3e3a870271888a9f41 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma
@@ -88,7 +88,7 @@ lemma yplus_inv_plus_bi_23 (z) (x1) (x2) (y1) (y2):
       z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
 #z #x1 #x2 #y1 #y2 #Hz
 <yplus_plus_comm_23 <yplus_plus_comm_23 in ⊢ (???%→?); #H
       z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
 #z #x1 #x2 #y1 #y2 #Hz
 <yplus_plus_comm_23 <yplus_plus_comm_23 in ⊢ (???%→?); #H

-@(eq_inv_yplus_bi_dx … H) // (**) (* auto does not work *)
+@(eq_inv_yplus_bi_dx … H) // (* * auto does not work *)

 qed-.
 
 (*** ylt_inv_plus_Y *)
 qed-.
 
 (*** ylt_inv_plus_Y *)

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_nat.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_nat.ma
index decfe5918bbcdd66f483309bae167e17db4d5795..172d8cf2ac206801dd7d0f27179bba48d7cab3b8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_nat.ma
@@ -15,7 +15,7 @@
 include "ground/arith/nat.ma".
 include "ground/arith/ynat.ma".
 
 include "ground/arith/nat.ma".
 include "ground/arith/ynat.ma".
 

-(* NON-NEGATIVE INTEGERS TO NON-NEGATIVE INTEGERS WITH INFINITY *************)
+(* NAT-INJECTION FOR NON-NEGATIVE INTEGERS WITH INFINITY ********************)

 
 (*** yinj *)
 definition yinj_nat (n) ≝ match n with
 
 (*** yinj *)
 definition yinj_nat (n) ≝ match n with

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index 61dd0b4b1752b85f19fe000527f2580d5a19868b..f76cbc115bb118588de873b61010498f0680be55 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
@@ -78,7 +78,7 @@ lemma yplus_inj_bi (n) (m):
 <nplus_succ_dx >ysucc_inj >ysucc_inj <yplus_succ_dx //
 qed.
 
 <nplus_succ_dx >ysucc_inj >ysucc_inj <yplus_succ_dx //
 qed.
 

-(* Advaced constructions ****************************************************)
+(* Advanced constructions ***************************************************)

 
 (*** ysucc_iter_Y yplus_Y1 *)
 lemma yplus_inf_sn (x): ∞ = ∞ + x.
 
 (*** ysucc_iter_Y yplus_Y1 *)
 lemma yplus_inf_sn (x): ∞ = ∞ + x.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma
index b03fe0d595a965521ce5033874a4f15978b4126e..065f8e8af7426b4c2abda8a1d5f76d4ef30fcf50 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_pred_succ.ma
@@ -25,7 +25,7 @@ lemma ypred_succ (x): x = ↓↑x.
 #x @(ynat_split_nat_inf … x) -x //
 qed.
 
 #x @(ynat_split_nat_inf … x) -x //
 qed.
 

-(* Inversion with ysucc *****************************************************)
+(* Inversions with ysucc ****************************************************)

 
 (*** ynat_cases *)
 lemma ynat_split_zero_pos (x): ∨∨ 𝟎 = x | x = ↑↓x.
 
 (*** ynat_cases *)
 lemma ynat_split_zero_pos (x): ∨∨ 𝟎 = x | x = ↑↓x.

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
index 9e4fb430cf71182640720323b20ffb472c656b25..b642bc56ba9109fab574af9db164bd59f9238d4c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
@@ -39,7 +39,7 @@ qed.
 lemma ysucc_inf: ∞ = ↑(∞).
 // qed.
 
 lemma ysucc_inf: ∞ = ↑(∞).
 // qed.
 

-(* Inversion lemmas *********************************************************)
+(* Inversions ***************************************************************)

 
 (*** ysucc_inv_inj_sn *)
 lemma eq_inv_inj_ysucc (n1) (x2):
 
 (*** ysucc_inv_inj_sn *)
 lemma eq_inv_inj_ysucc (n1) (x2):


@@ -96,7 +96,7 @@ qed-.
 lemma eq_inv_ysucc_zero (x): ↑x = 𝟎 → ⊥.
 /2 width=2 by eq_inv_zero_ysucc/ qed-.
 
 lemma eq_inv_ysucc_zero (x): ↑x = 𝟎 → ⊥.
 /2 width=2 by eq_inv_zero_ysucc/ qed-.
 

-(* Eliminators **************************************************************)
+(* Eliminations *************************************************************)

 
 (*** ynat_ind *)
 lemma ynat_ind_succ (Q:predicate …):
 
 (*** ynat_ind *)
 lemma ynat_ind_succ (Q:predicate …):

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqg_length.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqg_length.ma
index 0a1175ad007e7ae831726d4a0e278bf2c6beb356..e654410f881cdeb55aa48116dd7bc0e24b636a22 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/reqg_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/reqg_length.ma
@@ -19,7 +19,7 @@ include "static_2/static/reqg.ma".
 
 (* GENERIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***********)
 
 
 (* GENERIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***********)
 

-(* Advanved properties with free variables inclusion ************************)
+(* Advanced properties with free variables inclusion ************************)

 
 lemma reqg_fsge_comp (S):
       reflexive … S →
 
 lemma reqg_fsge_comp (S):
       reflexive … S →