--- /dev/null
+PcsAnd b "" true false
+eq
+land
+lsub
+compose, function composition
+ctc, contextual transitive closure
--- /dev/null
+PccFor d "" true false
+GROUND NOTATION, GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ
+RELATIONS
+FUNCTIONS
+LOGIC
+BOOLEANS
+LISTS
+STREAMS
+GENERATED LIBRARY
write_mli cmod
let write_index st =
+ let p = float (List.length st.ET.mods) in
+ let p =
+ if p > 0. then truncate (log10 p) else -1
+ in
+ let ps = Printf.sprintf "%%0%uu" (succ p) in
+ let fmt = Scanf.format_from_string ps "%u" in
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%03u = RecommGc%s\n" (succ i) name
+ Printf.fprintf och "module G%(%u%) = RecommGc%s\n" fmt (succ i) name
in
List.iteri iter st.ET.mods;
close_out och;
--- /dev/null
+PcsPar p "" true false
+(with reflexivity)
ADDITION
SUBTRACTION
LEFT SUBTRACTION
-MAXIMUM, MAXIMUN
+MAXIMUM
ORDER
STRICT ORDER
ARITHMETICAL PROPERTIES
--- /dev/null
+PccFor r "" true false
+CONJUNCTION
+DISJUNCTION
+EXTENSIONAL EQUIVALENCE
+TRANSITIVE CLOSURE
+LABELLED TRANSITIVE CLOSURE
+NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE
+HEAD AND TAIL
+ITERATED TAIL
+LENGTH
-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
+module G01 = RecommGcbGroundArith
+module G02 = RecommGcbGroundCounters
+module G03 = RecommGcbGroundLib
+module G04 = RecommGcdGroundArith
+module G05 = RecommGcdGroundCounters
+module G06 = RecommGcdGroundLib
+module G07 = RecommGcpGroundArith
+module G08 = RecommGcpGroundLib
+module G09 = RecommGcrGroundArith
+module G10 = RecommGcrGroundCounters
+module G11 = RecommGcrGroundLib
+module G12 = RecommGcsAttr
+module G13 = RecommGcsMain
+module G14 = RecommGcsWith
--- /dev/null
+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
+ | "ctc" :: tl -> k T.OK ("ctc" :: outs) tl
+ | "contextual" :: "transitive" :: "closure" :: tl -> k T.OK ("ctc" :: outs) tl
+ | "compose" :: tl -> k T.OK ("compose" :: outs) tl
+ | "function" :: "composition" :: tl -> k T.OK ("compose" :: outs) tl
+ | "lsub" :: tl -> k T.OK ("lsub" :: outs) tl
+ | "land" :: tl -> k T.OK ("land" :: outs) tl
+ | "eq" :: tl -> k T.OK ("eq" :: outs) tl
+ | _ -> k T.OO outs ins
+
+let main =
+ R.register_b step
--- /dev/null
+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
+ | "GENERATED" :: "LIBRARY" :: tl -> k T.OK ("LIBRARY" :: "GENERATED" :: outs) tl
+ | "STREAMS" :: tl -> k T.OK ("STREAMS" :: outs) tl
+ | "LISTS" :: tl -> k T.OK ("LISTS" :: outs) tl
+ | "BOOLEANS" :: tl -> k T.OK ("BOOLEANS" :: outs) tl
+ | "LOGIC" :: tl -> k T.OK ("LOGIC" :: outs) tl
+ | "FUNCTIONS" :: tl -> k T.OK ("FUNCTIONS" :: outs) tl
+ | "RELATIONS" :: tl -> k T.OK ("RELATIONS" :: outs) tl
+ | "GROUND" :: "NOTATION" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl
+ | "GENERAL" :: "NOTATION" :: "USED" :: "BY" :: "THE" :: "FORMAL" :: "SYSTEM" :: "\206\187\206\180" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl
+ | _ -> k T.OO outs ins
+
+let main =
+ R.register_d step
--- /dev/null
+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
+ | "(with" :: "reflexivity)" :: tl -> k T.OK ("reflexivity)" :: "(with" :: outs) tl
+ | _ -> k T.OO outs ins
+
+let main =
+ R.register_p step
| "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
--- /dev/null
+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
+ | "LENGTH" :: tl -> k T.OK ("LENGTH" :: outs) tl
+ | "ITERATED" :: "TAIL" :: tl -> k T.OK ("TAIL" :: "ITERATED" :: outs) tl
+ | "HEAD" :: "AND" :: "TAIL" :: tl -> k T.OK ("TAIL" :: "AND" :: "HEAD" :: outs) tl
+ | "NAT-LABELED" :: "REFLEXIVE" :: "AND" :: "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: "AND" :: "REFLEXIVE" :: "NAT-LABELED" :: outs) tl
+ | "LABELLED" :: "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: "LABELLED" :: outs) tl
+ | "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: outs) tl
+ | "EXTENSIONAL" :: "EQUIVALENCE" :: tl -> k T.OK ("EQUIVALENCE" :: "EXTENSIONAL" :: outs) tl
+ | "DISJUNCTION" :: tl -> k T.OK ("DISJUNCTION" :: outs) tl
+ | "CONJUNCTION" :: tl -> k T.OK ("CONJUNCTION" :: outs) tl
+ | _ -> k T.OO outs ins
+
+let main =
+ R.register_r step
if st = T.KO then k st outs ins else
match ins with
| "with" :: tl -> k T.OK ("with" :: outs) tl
+ | "of" :: tl -> k T.OK ("with" :: outs) tl
+ | "for" :: tl -> k T.OK ("with" :: outs) tl
| _ -> k T.OO outs ins
let main =
let keys = [|
"Note";
+ "NOTE";
|]
let heads = [|
aux (String.length s - 1)
let disambiguate_word s =
- if is_uppercase_ascii s then EP.CW s else
if Array.mem s keys then EP.KW s else
if Array.mem s heads then EP.HW s else
+ if is_uppercase_ascii s then EP.CW s else
EP.SW s
let log s =
in
l - aux 0 0
-let complete s =
- let l = !width - string_length_utf8 s - 6 in
+let complete s n =
+ let l = !width - string_length_utf8 s - 5 - n in
if l < 0 then begin
Printf.eprintf "overfull: %S\n" s;
""
| ET.Mark s ->
Printf.fprintf och "(* *%s*)" s
| ET.Key (s1, s2) ->
- Printf.fprintf och "(* %s%s*)" s1 s2
+ let s3 =
+ if s1 = "NOTE" then complete (s1^s2) 0 else ""
+ in
+ Printf.fprintf och "(* %s%s%s*)" s1 s2 s3
| ET.Title ss ->
let s = String.concat " " ss in
- Printf.fprintf och "(* %s %s*)" s (complete s)
+ Printf.fprintf och "(* %s %s*)" s (complete s 1)
| ET.Slice ss ->
let s = String.capitalize_ascii (String.concat " " ss) in
- Printf.fprintf och "(* %s %s*)" s (complete s)
+ Printf.fprintf och "(* %s %s*)" s (complete s 1)
| ET.Other (s1, s2, s3) ->
Printf.fprintf och "%s%s%s" s1 s2 s3
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
+ | "OF" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl
| _ -> k ET.KO outs ins
let k_or k st outs ins =
check s "GcsMain" false false
-with
+with, of, for
qed.
lemma nle_max_dx_refl_dx (m) (n): n ≤ (m ∨ n).
-#m #n @(nat_ind_2_succ … n m) -m -n //
-#m #n #IH <nmax_succ_bi /2 width=1 by nle_succ_bi/
-qed.
+// qed.
(* Basic destructions with nmax *********************************************)
--- /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 "basics/relations.ma".
+
+(* GENERATED LIBRARY ********************************************************)
+
+lemma insert_eq_1 (T1) (a1) (Q1,Q2:predicate T1):
+ (∀b1. Q1 b1 → a1 = b1 → Q2 b1) → Q1 a1 → Q2 a1.
+/2 width=1 by/ 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 "basics/pts.ma".
+
+(* GENERATED LIBRARY ********************************************************)
+
+lemma pull_2 (A1:Type[0])
+ (A2:Type[0])
+ (A:A1→A2→Type[0]):
+ (∀x2,x1. A x1 x2) →
+ (∀x1,x2. A x1 x2).
+/2 width=1 by/ 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 "basics/pts.ma".
+
+(* GENERATED LIBRARY ********************************************************)
+
+lemma pull_4 (A1:Type[0])
+ (A2:A1→Type[0])
+ (A3:∀x1.A2 x1→Type[0])
+ (A4:Type[0])
+ (A:∀x1:A1.∀x2:A2 x1.A3 x1 x2 → A4 → Type[0]):
+ (∀x4,x1,x2,x3. A x1 x2 x3 x4) →
+ (∀x1,x2,x3,x4. A x1 x2 x3 x4).
+/2 width=1 by/ 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 "basics/relations.ma".
-
-(* GENERATED LIBRARY ********************************************************)
-
-lemma insert_eq_1 (T1) (a1) (Q1,Q2:predicate T1):
- (∀b1. Q1 b1 → a1 = b1 → Q2 b1) → Q1 a1 → Q2 a1.
-/2 width=1 by/ qed-.
include "ground/notation/relations/doteq_4.ma".
include "ground/lib/relations.ma".
-(* EXTENSIONAL EQUIVALENCE **************************************************)
+(* EXTENSIONAL EQUIVALENCE FOR FUNCTIONS ************************************)
definition exteq (A,B:Type[0]): relation (A → B) ≝
λf1,f2. ∀a. f1 a = f2 a.
lemma exteq_canc_dx (A) (B): right_cancellable … (exteq A B).
/2 width=1 by exteq_repl/ qed-.
-(* Constructions with function composition **********************************)
+(* Constructions with compose ***********************************************)
lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):
f1 ≐{A,B} f2 → g ∘ f1 ≐{A,C} g ∘ f2.
include "ground/notation/relations/ringeq_3.ma".
include "ground/lib/list.ma".
-(* EXTENSIONAL EQUIVALENCE OF LISTS *****************************************)
+(* EXTENSIONAL EQUIVALENCE FOR LISTS ****************************************)
rec definition list_eq A (l1,l2:list A) on l1 ≝
match l1 with
(* LOGIC ********************************************************************)
-(* Constructions with And ***************************************************)
+(* Constructions with land **************************************************)
lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
#A #B * /2 width=1 by conj/
include "ground/lib/ltc.ma".
include "ground/arith/nat_plus.ma".
-(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR FOR λδ-2A ***************)
+(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR λδ-2A *******************)
definition lstar_aux (B) (R:relation B) (l): relation B ≝
λb1,b2. ∨∨ (∧∧ l = 𝟎 & b1 = b2) | (∧∧ l = 𝟏 & R b1 b2).
include "ground/insert_eq/insert_eq_1.ma".
include "ground/lib/functions.ma".
-(* LABELLED TRANSITIVE CLOSURE **********************************************)
+(* LABELLED TRANSITIVE CLOSURE FOR RELATIONS ********************************)
inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝
| ltc_rc : ∀a,b1,b2. R a b1 b2 → ltc … a b1 b2
elim H -a2 -b -b2 /4 width=4 by ltc_trans/
qed-.
-(* Advanced elimiations with reflexivity ************************************)
+(* Advanced eliminations (with reflexivity) *********************************)
lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2):
associative … f → right_identity … f i → reflexive B (R i) →
include "ground/lib/star.ma".
include "ground/lib/ltc.ma".
-(* LABELLED TRANSITIVE CLOSURE **********************************************)
+(* LABELLED TRANSITIVE CLOSURE FOR RELATIONS ********************************)
-alias symbol "subseteq" = "relation inclusion". (**)
+alias symbol "subseteq" = "relation inclusion". (* * alias *)
-(* Constructions with contextual transitive closure *************************)
+(* Constructions with ctc ***************************************************)
lemma ltc_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
left_identity … f i →
#b #b2 #_ #Hb2 #IH >(Hf i) -Hf /2 width=3 by ltc_dx/
qed.
-(* Inversions with contextual transitive closure ****************************)
+(* Inversions with ctc ******************************************************)
lemma ltc_inv_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
associative … f → annulment_2 … f i →
include "ground/xoa/ex_2_2.ma".
include "ground/lib/logic.ma".
-(* GENERIC RELATIONS ********************************************************)
-
-definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝
- λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2.
-
-(* Inclusion ****************************************************************)
-
-definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
- λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2).
-
-interpretation
- "2-relation inclusion"
- 'subseteq R1 R2 = (subR2 ?? R1 R2).
-
-definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝
- λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3).
-
-interpretation
- "3-relation inclusion"
- 'subseteq R1 R2 = (subR3 ??? R1 R2).
-
-(* Properties of relations **************************************************)
+(* RELATIONS ****************************************************************)
definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝
λA,B,C,D,E.A→B→C→D→E→Prop.
definition relation6: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝
λA,B,C,D,E,F.A→B→C→D→E→F→Prop.
-(**) (* we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *)
+definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝
+ λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2.
+
+(* * we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *)
definition c_reflexive (A) (B): predicate (relation3 A B B) ≝
λR. ∀a,b. R a b b.
definition is_inj2 (A,B:Type[0]): predicate (relation2 A B) ≝
λR. ∀a1,b. R a1 b → ∀a2. R a2 b → a1 = a2.
-(* Main properties of equality **********************************************)
-
-theorem canc_sn_eq (A): left_cancellable A (eq …).
-// qed-.
-
-theorem canc_dx_eq (A): right_cancellable A (eq …).
-// qed-.
-
-(* Normal form and strong normalization *************************************)
+(* NOTE: Normal form and strong normalization *******************************)
definition NF (A): relation A → relation A → predicate A ≝
λR,S,a1. ∀a2. R a1 a2 → S a1 a2.
elim HSa12 -HSa12 /2 width=1 by/
qed.
-(* Normal form and strong normalization with unboxed triples ****************)
+(* NOTE: Normal form and strong normalization with unboxed triples **********)
inductive SN3 (A) (B) (C) (R,S:relation6 A B C A B C): relation3 A B C ≝
| SN3_intro: ∀a1,b1,c1. (∀a2,b2,c2. R a1 b1 c1 a2 b2 c2 → (S a1 b1 c1 a2 b2 c2 → ⊥) → SN3 … R S a2 b2 c2) → SN3 … R S a1 b1 c1
.
-(* Relations with unboxed triples *******************************************)
+(* NOTE: Reflexive closure with unboxed triples *****************************)
definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝
λR,a1,b1,c1,a2,b2,c2.
lemma tri_RC_reflexive (A) (B) (C): ∀R. tri_reflexive A B C (tri_RC … R).
/3 width=1 by and3_intro, or_intror/ qed.
+
+(* NOTE: Inclusion for relations ********************************************)
+
+definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
+ λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2).
+
+interpretation
+ "2-relation inclusion"
+ 'subseteq R1 R2 = (subR2 ?? R1 R2).
+
+definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝
+ λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3).
+
+interpretation
+ "3-relation inclusion"
+ 'subseteq R1 R2 = (subR3 ??? R1 R2).
+
+(* Main constructions with eq ***********************************************)
+
+theorem canc_sn_eq (A): left_cancellable A (eq …).
+// qed-.
+
+theorem canc_dx_eq (A): right_cancellable A (eq …).
+// qed-.
include "basics/star1.ma".
include "ground/lib/relations.ma".
-(* TRANSITIVE CLOSURE *******************************************************)
+(* TRANSITIVE CLOSURE FOR RELATIONS *****************************************)
definition CTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝
λA,B,R,a. TC … (R a).
#_ #H1 #H2 #_ @H2 @HSR /3 width=3 by/
qed-.
-(* Normal form and strong normalization *************************************)
+(* NOTE: Normal form and strong normalization *******************************)
lemma SN_to_NF: ∀A,R,S. NF_dec A R S →
∀a1. SN A R S a1 →
* #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3 by star_compl, ex2_intro/
qed-.
-(* Relations with unboxed pairs *********************************************)
+(* NOTE: Relations with unboxed pairs ***************************************)
lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R →
∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 →
∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2.
#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1
[ /2 width=1 by or_introl/
-| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4 by ex2_2_intro, or_intror/ (**) (* auto fails without #_ *)
+| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4 by ex2_2_intro, or_intror/ (* * auto fails without #_ *)
]
qed-.
-(* Relations with unboxed triples *******************************************)
+(* NOTE: Relations with unboxed triples *************************************)
definition tri_star: ∀A,B,C,R. tri_relation A B C ≝
λA,B,C,R. tri_RC A B C (tri_TC … R).
lemma stream_rew (A) (t:stream A): match t with [ stream_cons a u ⇒ a ⨮ u ] = t.
#A * //
qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_stream_cons_bi (A) (a1,a2:A) (u1) (u2):
+ a1 ⨮ u1 = a2 ⨮ u2 → ∧∧ a1 = a2 & u1 = u2.
+#A #a1 #a2 #u1 #u2 #H destruct
+/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 "basics/pts.ma".
-
-(* GENERATED LIBRARY ********************************************************)
-
-lemma pull_2 (A1:Type[0])
- (A2:Type[0])
- (A:A1→A2→Type[0]):
- (∀x2,x1. A x1 x2) →
- (∀x1,x2. A x1 x2).
-/2 width=1 by/ 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 "basics/pts.ma".
-
-(* GENERATED LIBRARY ********************************************************)
-
-lemma pull_4 (A1:Type[0])
- (A2:A1→Type[0])
- (A3:∀x1.A2 x1→Type[0])
- (A4:Type[0])
- (A:∀x1:A1.∀x2:A2 x1.A3 x1 x2 → A4 → Type[0]):
- (∀x4,x1,x2,x3. A x1 x2 x3 x4) →
- (∀x1,x2,x3,x4. A x1 x2 x3 x4).
-/2 width=1 by/ qed-.
#R #a #b * //
qed.
-(* Specific properties ******************************************************)
+(* Poperties with stream_tl *************************************************)
lemma tl_push: ∀f. f = ⫰⫯f.
// qed.
projects / helm.git / commitdiff