From: Ferruccio Guidi Date: Fri, 18 May 2007 15:55:49 +0000 (+0000) Subject: - new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated X-Git-Tag: 0.4.95@7852~469 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=51bcceed90882024de4c614d5f26d17eaaf7f18f;p=helm.git - new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated procedural representation of the proofs in contribs/LAMBDA-TYPES/Base-1 - template_makefile_devel.in: %.mo.opt now works - acic_procedural: some improvements - PrimitiveTactics: a part of the elim tactic was factorixed for use by the procedural reconstruction --- diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index 3ee088696..9815580b6 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -191,26 +191,38 @@ let mk_exp_args hd tl classes synth = let args = aux args in if args = [] then hd else C.AAppl ("", hd :: args) +let mk_convert st ?name sty ety note = + let e = Cn.hole "" in + let csty, cety = H.cic sty, H.cic ety in + let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s" + note (Pp.ppterm csty) (Pp.ppterm cety) + in + if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else + match name with + | None -> [T.Change (sty, ety, None, e, ""(*note*))] + | Some (id, i) -> + begin match get_entry st id with + | C.Def _ -> assert false (* [T.ClearBody (id, note)] *) + | C.Decl _ -> [T.Change (ety, sty, Some (id, Some id), e, "" (* note *))] + end + let convert st ?name v = match get_inner_types st v with - | None -> [] - | Some (sty, ety) -> - let e = Cn.hole "" in - let csty, cety = H.cic sty, H.cic ety in - if Ut.alpha_equivalence csty cety then [] else - match name with - | None -> [T.Change (sty, ety, None, e, "")] - | Some (id, i) -> - begin match get_entry st id with - | C.Def _ -> [T.ClearBody (id, "")] - | C.Decl w -> - let w = S.lift i w in - if Ut.alpha_equivalence csty w then [] - else - [T.Note (Pp.ppterm csty); T.Note (Pp.ppterm w); - T.Change (sty, ety, Some (id, Some id), e, "")] - end - + | None -> [(*T.Note "NORMAL: NO INNER TYPES"*)] + | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL" + +let convert_elim st ?name t v pattern = + match t, get_inner_types st t, get_inner_types st v with + | _, None, _ + | _, _, None -> [(* T.Note "ELIM: NO INNER TYPES"*)] + | C.AAppl (_, hd :: tl), Some (tsty, _), Some (vsty, _) -> + let where = List.hd (List.rev tl) in + let cty = Cn.elim_inferred_type + st.context (H.cic vsty) (H.cic where) (H.cic hd) (H.cic pattern) + in + mk_convert st ?name (Cn.fake_annotate "" st.context cty) tsty "ELIM" + | _, Some _, Some _ -> assert false + let get_intro = function | C.Anonymous -> None | C.Name s -> Some s @@ -230,23 +242,25 @@ let mk_arg st = function | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what | _ -> [] -let mk_fwd_rewrite st dtext name tl direction = +let mk_fwd_rewrite st dtext name tl direction t = assert (List.length tl = 6); let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in let e = Cn.mk_pattern 1 predicate in match where with - | C.ARel (_, _, _, premise) -> - let script = mk_arg st what in + | C.ARel (_, _, i, premise) as v -> let where = Some (premise, name) in + let _script = convert_elim st ~name:(premise, i) t v e in + let script = mk_arg st what @ mk_arg st v (* @ script *) in let st = {st with context = Cn.clear st.context premise} in st, T.Rewrite (direction, what, where, e, dtext) :: script | _ -> assert false -let mk_rewrite st dtext what qs tl direction = +let mk_rewrite st dtext where qs tl direction t = assert (List.length tl = 5); let predicate = List.nth tl 2 in let e = Cn.mk_pattern 1 predicate in - [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")] + let script = convert_elim st t t e in + script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")] let rec proc_lambda st name v t = let dno = DTI.does_not_occur 1 (H.cic t) in @@ -272,9 +286,9 @@ and proc_letin st what name v t = | Some (ity, _) -> let st, rqv = match v with | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl -> - mk_fwd_rewrite st dtext intro tl true + mk_fwd_rewrite st dtext intro tl true v | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl -> - mk_fwd_rewrite st dtext intro tl false + mk_fwd_rewrite st dtext intro tl false v | v -> let qs = [proc_proof (next st) v; [T.Id ""]] in st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] @@ -300,7 +314,7 @@ and proc_rel st what = and proc_mutconstruct st what = let _, dtext = test_depth st in let script = [T.Apply (what, dtext)] in - mk_intros st what script + mk_intros st what script and proc_appl st what hd tl = let proceed, dtext = test_depth st in @@ -329,14 +343,14 @@ and proc_appl st what hd tl = let names = get_ind_names uri tyno in let qs = proc_bkd_proofs (next st) synth names classes tl in if is_rewrite_right hd then - script @ mk_rewrite st dtext where qs tl false + script @ mk_rewrite st dtext where qs tl false what else if is_rewrite_left hd then - script @ mk_rewrite st dtext where qs tl true + script @ mk_rewrite st dtext where qs tl true what else let predicate = List.nth tl (parsno - i) in let e = Cn.mk_pattern j predicate in let using = Some hd in - script @ + convert_elim st what what e @ script @ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] | None -> let qs = proc_bkd_proofs (next st) synth [] classes tl in diff --git a/components/acic_procedural/proceduralConversion.ml b/components/acic_procedural/proceduralConversion.ml index b8cdc08ea..376313ac8 100644 --- a/components/acic_procedural/proceduralConversion.ml +++ b/components/acic_procedural/proceduralConversion.ml @@ -30,6 +30,8 @@ module TC = CicTypeChecker module D = Deannotate module UM = UriManager module Rd = CicReduction +module PEH = ProofEngineHelpers +module PT = PrimitiveTactics module DTI = DoubleTypeInference @@ -76,6 +78,46 @@ let lift k n = in lift_term k + let fake_annotate id c = + let get_binder c m = + try match List.nth c (pred m) with + | Some (C.Name s, _) -> s + | _ -> assert false + with + | Invalid_argument _ -> assert false + in + let mk_decl n v = Some (n, C.Decl v) in + let mk_def n v = Some (n, C.Def (v, None)) in + let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in + let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in + let rec ann_xns c (uri, t) = uri, ann_term c t + and ann_ms c = function + | None -> None + | Some t -> Some (ann_term c t) + and ann_fix newc c (name, i, ty, bo) = + id, name, i, ann_term c ty, ann_term (List.rev_append newc c) bo + and ann_cofix newc c (name, ty, bo) = + id, name, ann_term c ty, ann_term (List.rev_append newc c) bo + and ann_term c = function + | C.Sort sort -> C.ASort (id, sort) + | C.Implicit ann -> C.AImplicit (id, ann) + | C.Rel m -> C.ARel (id, id, m, get_binder c m) + | C.Const (uri, xnss) -> C.AConst (id, uri, List.map (ann_xns c) xnss) + | C.Var (uri, xnss) -> C.AVar (id, uri, List.map (ann_xns c) xnss) + | C.MutInd (uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (ann_xns c) xnss) + | C.MutConstruct (uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (ann_xns c) xnss) + | C.Meta (i, mss) -> C.AMeta(id, i, List.map (ann_ms c) mss) + | C.Appl ts -> C.AAppl (id, List.map (ann_term c) ts) + | C.Cast (te, ty) -> C.ACast (id, ann_term c te, ann_term c ty) + | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl) + | C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t) + | C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t) + | C.LetIn (n, s, t) -> C.ALetIn (id, n, ann_term c s, ann_term (mk_def n s :: c) t) + | C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl) + | C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl) + in + ann_term c + let clear_absts m = let rec aux k n = function | C.AImplicit (_, None) as t -> t @@ -196,3 +238,14 @@ let clear c hyp = | entry :: tail -> aux (entry :: c) tail in aux [] c + +let elim_inferred_type context goal arg using cpattern = + let metasenv, ugraph = [], Un.empty_ugraph in + let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in + let _splits, args_no = PEH.split_with_whd (context, ety) in + let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim + ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no + in + let ty = C.Appl (predicate :: actual_args) in + let upto = List.length actual_args in + Rd.head_beta_reduce ~delta:false ~upto ty diff --git a/components/acic_procedural/proceduralConversion.mli b/components/acic_procedural/proceduralConversion.mli index e5b2dcdcf..ffc55d45e 100644 --- a/components/acic_procedural/proceduralConversion.mli +++ b/components/acic_procedural/proceduralConversion.mli @@ -29,6 +29,8 @@ val hole: Cic.id -> Cic.annterm val lift: int -> int -> Cic.annterm -> Cic.annterm +val fake_annotate: Cic.id -> Cic.context -> Cic.term -> Cic.annterm + val mk_pattern: int -> Cic.annterm -> Cic.annterm val get_clears: @@ -36,3 +38,6 @@ val get_clears: Cic.context * string list val clear: Cic.context -> string -> Cic.context + +val elim_inferred_type: + Cic.context -> Cic.term -> Cic.term -> Cic.term -> Cic.term -> Cic.term diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index aeb0c0751..e17d6cb7b 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -494,6 +494,58 @@ module S = CicSubstitution module T = Tacticals module RT = ReductionTactics +let rec args_init n f = + if n <= 0 then [] else f n :: args_init (pred n) f + +let mk_predicate_for_elim + ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no = + let instantiated_eliminator = + let f n = if n = 1 then arg else C.Implicit None in + C.Appl (using :: args_init args_no f) + in + let _actual_arg, iety, _metasenv', _ugraph = + CicRefine.type_of_aux' metasenv context instantiated_eliminator ugraph + in + let _actual_meta, actual_args = match iety with + | C.Meta (i, _) -> i, [] + | C.Appl (C.Meta (i, _) :: args) -> i, args + | _ -> assert false + in +(* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *) + let rec mk_pred metasenv context' pred arg' = function + | [] -> metasenv, pred, arg' + | arg :: tail -> +(* FG: we find the predicate for the eliminator as in the rewrite tactic ****) + let argty, _ugraph = TC.type_of_aux' metasenv context' arg ugraph in + let argty = CicReduction.whd context' argty in + let fresh_name = + FreshNamesGenerator.mk_fresh_name + ~subst:[] metasenv context' C.Anonymous ~typ:argty + in + let hyp = Some (fresh_name, C.Decl argty) in + let lazy_term c m u = + let distance = List.length c - List.length context in + S.lift distance arg, m, u + in + let pattern = Some lazy_term, [], Some cpattern in + let subst, metasenv, _ugraph, _conjecture, selected_terms = + ProofEngineHelpers.select + ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern + in + let metasenv = MS.apply_subst_metasenv subst metasenv in + let map (_context_of_t, t) l = t :: l in + let what = List.fold_right map selected_terms [] in + let arg' = MS.apply_subst subst arg' in + let argty = MS.apply_subst subst argty in + let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in + let pred = MS.apply_subst subst pred in + let pred = C.Lambda (fresh_name, argty, pred) in + mk_pred metasenv (hyp :: context') pred arg' tail + in + let metasenv, pred, arg = mk_pred metasenv context goal arg actual_args in + HLog.debug ("PRED: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args)); + metasenv, pred, arg, actual_args + let beta_after_elim_tac upto predicate = let beta_after_elim_tac status = let proof, goal = status in @@ -559,9 +611,9 @@ let beta_after_elim_tac upto predicate = let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = let elim_tac (proof, goal) = - let cpatt = match pattern with - | None, [], Some cpatt -> cpatt - | _ -> raise (PET.Fail (lazy "not implemented")) + let cpattern = match pattern with + | None, [], Some cpattern -> cpattern + | _ -> raise (PET.Fail (lazy "not implemented")) in let ugraph = CicUniv.empty_ugraph in let curi, metasenv, _subst, proofbo, proofty, attrs = proof in @@ -610,67 +662,20 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = TC.type_of_aux' metasenv' context eliminator_ref ugraph in (* FG: ADDED PART ***********************************************************) (* FG: we can not assume eliminator is the default eliminator ***************) - let rec args_init n f = - if n <= 0 then [] else f n :: args_init (pred n) f - in let splits, args_no = PEH.split_with_whd (context, ety) in let pred_pos = match List.hd splits with | _, C.Rel i when i > 1 && i <= args_no -> i | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i | _ -> raise NotAnEliminator in - let upto, metasenv', pred, term = match pattern with + let metasenv', pred, term, actual_args = match pattern with | None, [], Some (C.Implicit (Some `Hole)) -> - 0, metasenv', C.Implicit None, term + metasenv', C.Implicit None, term, [] | _ -> - let instantiated_eliminator = - let f n = if n = 1 then term else C.Implicit None in - C.Appl (eliminator_ref :: args_init args_no f) - in - let _actual_term, iety, _metasenv'', _ugraph = - CicRefine.type_of_aux' metasenv' context instantiated_eliminator ugraph - in - let _actual_meta, actual_args = match iety with - | C.Meta (i, _) -> i, [] - | C.Appl (C.Meta (i, _) :: args) -> i, args - | _ -> assert false - in - (* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *) - let upto = List.length actual_args in - let rec mk_pred metasenv context' pred term' = function - | [] -> metasenv, pred, term' - | term :: tail -> -(* FG: we find the predicate for the eliminator as in the rewrite tactic ****) - let termty, _ugraph = TC.type_of_aux' metasenv context' term ugraph in - let termty = CicReduction.whd context' termty in - let fresh_name = - FreshNamesGenerator.mk_fresh_name - ~subst:[] metasenv context' C.Anonymous ~typ:termty - in - let hyp = Some (fresh_name, C.Decl termty) in - let lazy_term c m u = - let distance = List.length c - List.length context in - S.lift distance term, m, u - in - let pattern = Some lazy_term, [], Some cpatt in - let subst, metasenv, _ugraph, _conjecture, selected_terms = - ProofEngineHelpers.select - ~metasenv ~ugraph ~conjecture:(metano, context, pred) ~pattern - in - let metasenv = MS.apply_subst_metasenv subst metasenv in - let map (_context_of_t, t) l = t :: l in - let what = List.fold_right map selected_terms [] in - let term' = MS.apply_subst subst term' in - let termty = MS.apply_subst subst termty in - let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in - let pred = MS.apply_subst subst pred in - let pred = C.Lambda (fresh_name, termty, pred) in - mk_pred metasenv (hyp :: context') pred term' tail - in - let metasenv', pred, term = mk_pred metasenv' context ty term actual_args in - HLog.debug ("PRED: " ^ CicPp.ppterm ~metasenv:metasenv' pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv:metasenv') actual_args)); - upto, metasenv', pred, term - in + mk_predicate_for_elim + ~args_no ~context ~ugraph ~cpattern + ~metasenv:metasenv' ~arg:term ~using:eliminator_ref ~goal:ty + in (* FG: END OF ADDED PART ****************************************************) let term_to_refine = let f n = @@ -698,6 +703,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = new_goals @ new_goals' in let res = proof'', patched_new_goals in + let upto = List.length actual_args in if upto = 0 then res else let continuation = beta_after_elim_tac upto pred in let dummy_status = proof,goal in diff --git a/components/tactics/primitiveTactics.mli b/components/tactics/primitiveTactics.mli index 577ed7535..890874a89 100644 --- a/components/tactics/primitiveTactics.mli +++ b/components/tactics/primitiveTactics.mli @@ -91,3 +91,9 @@ val cases_intros_tac: (* inserts a hole in the context *) val letout_tac: ProofEngineTypes.tactic + +val mk_predicate_for_elim: + context:Cic.context -> metasenv:Cic.metasenv -> + ugraph:CicUniv.universe_graph -> goal:Cic.term -> + arg:Cic.term -> using:Cic.term -> cpattern:Cic.term -> args_no:int -> + Cic.metasenv * Cic.term * Cic.term * Cic.term list diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/Makefile b/matita/contribs/LAMBDA-TYPES/Base-2/Makefile new file mode 100644 index 000000000..2524510f3 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/Makefile @@ -0,0 +1,27 @@ +include ../../../../Makefile.defs + +H=@ + +MATITAC = $(RT_BASE_DIR)/matitac.opt + +MMAS = $(shell find -name "*.mma") +MAS = $(MMAS:%.mma=%.ma) + +all: OPTIONS = -bench + +log: OPTIONS = >> tmp.txt 2>&1 + +all: $(MAS) + +log: $(MAS) + $(H)mv tmp.txt log.txt + +clean: + $(H)rm -f $(MAS) + +%.ma: %.mma + $(H)$(MATITAC) -dump $@ $< $(OPTIONS) + +include depend + +.DELETE_ON_ERROR: diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma b/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma new file mode 100644 index 000000000..34839d833 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs". + +include "preamble.ma". + +(* object blt not inlined *) + + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma b/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma new file mode 100644 index 000000000..d24466394 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/props". + +include "blt/defs.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/le_bge.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/blt_lt.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/bge_le.con". + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/depend b/matita/contribs/LAMBDA-TYPES/Base-2/depend new file mode 100644 index 000000000..1f10a0079 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/depend @@ -0,0 +1,9 @@ +theory.ma: theory.mma ext/tactics.ma ext/arith.ma types/props.ma blt/props.ma plist/props.ma +ext/tactics.ma: ext/tactics.mma preamble.ma +ext/arith.ma: ext/arith.mma preamble.ma +types/defs.ma: types/defs.mma preamble.ma +types/props.ma: types/props.mma types/defs.ma +blt/defs.ma: blt/defs.mma preamble.ma +blt/props.ma: blt/props.mma blt/defs.ma +plist/defs.ma: plist/defs.mma preamble.ma +plist/props.ma: plist/props.mma plist/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma b/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma new file mode 100644 index 000000000..240f138d5 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma @@ -0,0 +1,106 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith". + +include "preamble.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_plus_r.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_plus_r.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3_assoc.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_O.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_SO.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/eq_nat_dec.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/neq_eq_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_false.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_Sx_x.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_le.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_plus_minus_sym.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_plus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_trans_plus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_gen_S.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_plus_x_Sy.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_lt_plus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_Sy.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_SO.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_x_pred_y.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_gt_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_gen_xS.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_lt_false.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_neq.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/arith0.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/O_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_plus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_S_minus.con". + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma b/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma new file mode 100644 index 000000000..18de7f71a --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics". + +include "preamble.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/unintro.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/xinduction.con". + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/log.txt b/matita/contribs/LAMBDA-TYPES/Base-2/log.txt new file mode 100644 index 000000000..2c20deb94 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/log.txt @@ -0,0 +1,744 @@ +Info: execution of blt/defs.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of blt/defs.mma completed in 1''. +Info: execution of blt/props.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt ...'' +Info: baseuri cic:/matita/LAMBDA-TYPES/Base-2/blt/props is not empty +Info: cleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/blt/props +Info: Removing: cic:/matita/LAMBDA-TYPES/Base-2/blt/props/* +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs" ...'' +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_blt +Pre Nodes : 257 +nat +nat +nat +nat +Warn: Optimizer: remove 3 +Warn: Optimizer: swap 2 +Warn: Optimizer: nested application +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq bool (blt y n) true)))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq bool (blt y O) true))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H0) in (False_ind (eq bool (blt y O) true) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq bool (blt y O) true)).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq bool (blt y O) true)) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq bool (blt y n) true))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq bool (blt n0 (S n)) true))) (\lambda _:(lt O (S n)).(refl_equal bool true)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq bool +match n0 return (\lambda n1:nat.bool) with + [ O => true + | (S (m:nat)) => (blt m n) +] true)).(\lambda H1:(lt (S n0) (S n)).(H n0 (le_S_n (S n0) n H1))))) y)))) x)) +Post Nodes: 272 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_bge +Pre Nodes : 255 +nat +nat +nat +nat +Warn: Optimizer: remove 3 +Warn: Optimizer: swap 2 +Warn: Optimizer: nested application +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le n y)\to (eq bool (blt y n) false)))) (\lambda y:nat.(\lambda _:(le O y).(refl_equal bool false))) (\lambda n:nat.(\lambda H:(\forall y:nat.((le n y)\to (eq bool (blt y n) false))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((le (S n) n0)\to (eq bool (blt n0 (S n)) false))) (\lambda H0:(le (S n) O). let H1 \def (le_ind (S n) (\lambda n0:nat.((eq nat n0 O)\to (eq bool (blt O (S n)) false))) (\lambda H1:(eq nat (S n) O). let H2 \def (eq_ind nat (S n) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H1) in (False_ind (eq bool (blt O (S n)) false) H2)) (\lambda m:nat.(\lambda H1:(le (S n) m).(\lambda _:((eq nat m O)\to (eq bool (blt O (S n)) false)).(\lambda H2:(eq nat (S m) O). let H3 \def (eq_ind nat (S m) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H2) in let DEFINED \def (False_ind ((le (S n) m)\to (eq bool (blt O (S n)) false)) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O))) (\lambda n0:nat.(\lambda _:((le (S n) n0)\to (eq bool (blt n0 (S n)) false)).(\lambda H1:(le (S n) (S n0)).(H n0 (le_S_n n n0 H1))))) y)))) x)) +Post Nodes: 272 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: blt_lt +Pre Nodes : 221 +bool +bool +Warn: Optimizer: remove 3 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq bool (blt y n) true)\to (lt y n)))) (\lambda y:nat.(\lambda H:(eq bool (blt y O) true). let H0 \def (eq_ind bool (blt y O) (\lambda b:bool.((eq bool b true)\to (lt y O))) (\lambda H0:(eq bool (blt y O) true). let H1 \def (eq_ind bool (blt y O) (\lambda e:bool. +match e return (\lambda _:bool.Prop) with + [ true => False + | false => True +]) I true H0) in (False_ind (lt y O) H1)) true H) in (H0 (refl_equal bool true)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((eq bool (blt y n) true)\to (lt y n))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((eq bool (blt n0 (S n)) true)\to (lt n0 (S n)))) (\lambda _:(eq bool true true).(le_S_n (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n))))) (\lambda n0:nat.(\lambda _:((eq bool +match n0 return (\lambda n1:nat.bool) with + [ O => true + | (S (m:nat)) => (blt m n) +] true)\to (lt n0 (S n))).(\lambda H1:(eq bool (blt n0 n) true).(lt_le_S (S n0) (S n) (lt_n_S n0 n (H n0 H1)))))) y)))) x)) +Post Nodes: 219 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: bge_le +Pre Nodes : 222 +bool +bool +Warn: Optimizer: remove 3 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq bool (blt y n) false)\to (le n y)))) (\lambda y:nat.(\lambda _:(eq bool (blt y O) false).(le_O_n y))) (\lambda n:nat.(\lambda H:(\forall y:nat.((eq bool (blt y n) false)\to (le n y))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((eq bool (blt n0 (S n)) false)\to (le (S n) n0))) (\lambda H0:(eq bool (blt O (S n)) false). let H1 \def (eq_ind bool (blt O (S n)) (\lambda b:bool.((eq bool b false)\to (le (S n) O))) (\lambda H1:(eq bool (blt O (S n)) false). let H2 \def (eq_ind bool (blt O (S n)) (\lambda e:bool. +match e return (\lambda _:bool.Prop) with + [ true => True + | false => False +]) I false H1) in (False_ind (le (S n) O) H2)) false H0) in (H1 (refl_equal bool false))) (\lambda n0:nat.(\lambda _:((eq bool (blt n0 (S n)) false)\to (le (S n) n0)).(\lambda H1:(eq bool (blt (S n0) (S n)) false).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0 H1))))))) y)))) x)) +Post Nodes: 220 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of blt/props.mma completed in 7''. +Info: execution of ext/arith.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext ...'' +Info: baseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/arith is not empty +Info: cleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/arith +Info: Removing: cic:/matita/LAMBDA-TYPES/Base-2/ext/arith/* +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...'' +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: nat_dec +Pre Nodes : 474 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda n1:nat.(nat_ind (\lambda n:nat.(\forall n2:nat.(or (eq nat n n2) ((eq nat n n2)\to (\forall P:Prop.P))))) (\lambda n2:nat.(nat_ind (\lambda n:nat.(or (eq nat O n) ((eq nat O n)\to (\forall P:Prop.P)))) (or_introl (eq nat O O) ((eq nat O O)\to (\forall P:Prop.P)) (refl_equal nat O)) (\lambda n3:nat.(\lambda _:(or (eq nat O n3) ((eq nat O n3)\to (\forall P:Prop.P))).(or_intror (eq nat O (S n3)) ((eq nat O (S n3))\to (\forall P:Prop.P)) (\lambda H0:(eq nat O (S n3)).(\lambda P:Prop. let H1 \def (eq_ind nat O (\lambda ee:nat. +match ee return (\lambda _:nat.Prop) with + [ O => True + | (S (_:nat)) => False +]) I (S n3) H0) in (False_ind P H1)))))) n2)) (\lambda n2:nat.(\lambda H:(\forall n2:nat.(or (eq nat n2 n2) ((eq nat n2 n2)\to (\forall P:Prop.P)))).(\lambda n3:nat.(nat_ind (\lambda n0:nat.(or (eq nat (S n2) n0) ((eq nat (S n2) n0)\to (\forall P:Prop.P)))) (or_intror (eq nat (S n2) O) ((eq nat (S n2) O)\to (\forall P:Prop.P)) (\lambda H0:(eq nat (S n2) O).(\lambda P:Prop. let H1 \def (eq_ind nat (S n2) (\lambda ee:nat. +match ee return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H0) in (False_ind P H1)))) (\lambda n4:nat.(\lambda H0:(or (eq nat (S n2) n4) ((eq nat (S n2) n4)\to (\forall P:Prop.P))). let DEFINED \def (H n4) in (or_ind (eq nat n2 n4) ((eq nat n2 n4)\to (\forall P:Prop.P)) (or (eq nat (S n2) (S n4)) ((eq nat (S n2) (S n4))\to (\forall P:Prop.P))) (\lambda H1:(eq nat n2 n4).(eq_ind nat n2 (\lambda n3:nat.(or (eq nat (S n2) (S n3)) ((eq nat (S n2) (S n3))\to (\forall P:Prop.P)))) (or_introl (eq nat (S n2) (S n2)) ((eq nat (S n2) (S n2))\to (\forall P:Prop.P)) (refl_equal nat (S n2))) n4 H1)) (\lambda H1:((eq nat n2 n4)\to (\forall P:Prop.P)).(or_intror (eq nat (S n2) (S n4)) ((eq nat (S n2) (S n4))\to (\forall P:Prop.P)) (\lambda H2:(eq nat (S n2) (S n4)).(\lambda P:Prop. let H3 \def (f_equal nat nat (\lambda e:nat. +match e return (\lambda _:nat.nat) with + [ O => n2 + | (S (n3:nat)) => n3 +]) (S n2) (S n4) H2) in let H4 \def (eq_ind_r nat n4 (\lambda n3:nat.((eq nat n2 n3)\to (\forall P0:Prop.P0))) H1 n2 H3) in (H4 (refl_equal nat n2) P))))) DEFINED))) n3)))) n1)) +Post Nodes: 476 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: simpl_plus_r +Pre Nodes : 85 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda n:nat.(\lambda m:nat.(\lambda p:nat.(\lambda H:(eq nat (plus m n) (plus p n)). let DEFINED \def (plus_comm n m) in (plus_reg_l n m p (eq_ind_r nat (plus m n) (\lambda n0:nat.(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda n0:nat.(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_comm n p)) (plus m n) H) (plus n m) DEFINED)))))) +Post Nodes: 87 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: minus_plus_r +Pre Nodes : 33 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda m:nat.(\lambda n:nat. let DEFINED \def (plus_comm m n) in (eq_ind_r nat (plus n m) (\lambda n0:nat.(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) DEFINED))) +Post Nodes: 35 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: plus_permute_2_in_3 +Pre Nodes : 117 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda z:nat. let DEFINED \def (plus_assoc_reverse x z y) in let DEFINED0 \def (plus_comm y z) in let DEFINED1 \def (plus_assoc_reverse x y z) in (eq_ind_r nat (plus x (plus y z)) (\lambda n:nat.(eq nat n (plus (plus x z) y))) (eq_ind_r nat (plus z y) (\lambda n:nat.(eq nat (plus x n) (plus (plus x z) y))) (eq_ind nat (plus (plus x z) y) (\lambda n:nat.(eq nat n (plus (plus x z) y))) (refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) DEFINED) (plus y z) DEFINED0) (plus (plus x y) z) DEFINED1)))) +Post Nodes: 123 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: plus_permute_2_in_3_assoc +Pre Nodes : 86 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda n:nat.(\lambda h:nat.(\lambda k:nat. let DEFINED \def (plus_assoc n k h) in let DEFINED0 \def (plus_permute_2_in_3 n h k) in (eq_ind_r nat (plus (plus n k) h) (\lambda n0:nat.(eq nat n0 (plus n (plus k h)))) (eq_ind_r nat (plus (plus n k) h) (\lambda n0:nat.(eq nat (plus (plus n k) h) n0)) (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) DEFINED) (plus (plus n h) k) DEFINED0)))) +Post Nodes: 90 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: plus_O +Pre Nodes : 191 +nat +nat +Warn: Optimizer: remove 3 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq nat (plus n y) O)\to (and (eq nat n O) (eq nat y O))))) (\lambda y:nat.(\lambda H:(eq nat (plus O y) O).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda n:nat.(\lambda _:(\forall y:nat.((eq nat (plus n y) O)\to (and (eq nat n O) (eq nat y O)))).(\lambda y:nat.(\lambda H0:(eq nat (plus (S n) y) O). let H1 \def (eq_ind nat (plus (S n) y) (\lambda n0:nat.((eq nat n0 O)\to (and (eq nat (S n) O) (eq nat y O)))) (\lambda H1:(eq nat (plus (S n) y) O). let H2 \def (eq_ind nat (plus (S n) y) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H1) in (False_ind (and (eq nat (S n) O) (eq nat y O)) H2)) O H0) in (H1 (refl_equal nat O)))))) x)) +Post Nodes: 189 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: minus_Sx_SO +Pre Nodes : 24 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat. let DEFINED \def (minus_n_O x) in (eq_ind nat x (\lambda n:nat.(eq nat n x)) (refl_equal nat x) (minus x O) DEFINED)) +Post Nodes: 26 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: eq_nat_dec +Pre Nodes : 303 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda i:nat.(nat_ind (\lambda n:nat.(\forall j:nat.(or (not (eq nat n j)) (eq nat n j)))) (\lambda j:nat.(nat_ind (\lambda n:nat.(or (not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O) (refl_equal nat O)) (\lambda n:nat.(\lambda _:(or (not (eq nat O n)) (eq nat O n)).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j)) (\lambda n:nat.(\lambda H:(\forall j:nat.(or (not (eq nat n j)) (eq nat n j))).(\lambda j:nat.(nat_ind (\lambda n0:nat.(or (not (eq nat (S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda n0:nat.(\lambda _:(or (not (eq nat (S n) n0)) (eq nat (S n) n0)). let DEFINED \def (H n0) in (or_ind (not (eq nat n n0)) (eq nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda H1:(not (eq nat n n0)).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (not_eq_S n n0 H1))) (\lambda H1:(eq nat n n0).(or_intror (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) DEFINED))) j)))) i)) +Post Nodes: 305 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: neq_eq_e +Pre Nodes : 47 +Optimized : (\lambda i:nat.(\lambda j:nat.(\lambda P:Prop.(\lambda H:((not (eq nat i j))\to P).(\lambda H0:((eq nat i j)\to P). let o \def (eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))) +Post Nodes: 47 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_false +Pre Nodes : 382 +nat +nat +nat +nat +Warn: Optimizer: remove 3 +Warn: Optimizer: swap 2 +Warn: Optimizer: nested application +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +nat +nat +nat +nat +Warn: Optimizer: remove 3 +Warn: Optimizer: swap 2 +Warn: Optimizer: nested application +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda m:nat.(nat_ind (\lambda n:nat.(\forall n0:nat.(\forall P:Prop.((le n n0)\to ((le (S n0) n)\to P))))) (\lambda n:nat.(\lambda P:Prop.(\lambda _:(le O n).(\lambda H0:(le (S n) O). let H1 \def (le_ind (S n) (\lambda n0:nat.((eq nat n0 O)\to P)) (\lambda H1:(eq nat (S n) O). let H2 \def (eq_ind nat (S n) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H1) in (False_ind P H2)) (\lambda m0:nat.(\lambda H1:(le (S n) m0).(\lambda _:((eq nat m0 O)\to P).(\lambda H2:(eq nat (S m0) O). let H3 \def (eq_ind nat (S m0) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H2) in let DEFINED \def (False_ind ((le (S n) m0)\to P) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O)))))) (\lambda n:nat.(\lambda H:(\forall n0:nat.(\forall P:Prop.((le n n0)\to ((le (S n0) n)\to P)))).(\lambda n0:nat.(nat_ind (\lambda n1:nat.(\forall P:Prop.((le (S n) n1)\to ((le (S n1) (S n))\to P)))) (\lambda P:Prop.(\lambda H0:(le (S n) O).(\lambda _:(le (S O) (S n)). let H2 \def (le_ind (S n) (\lambda n1:nat.((eq nat n1 O)\to P)) (\lambda H2:(eq nat (S n) O). let H3 \def (eq_ind nat (S n) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H2) in (False_ind P H3)) (\lambda m0:nat.(\lambda H2:(le (S n) m0).(\lambda _:((eq nat m0 O)\to P).(\lambda H3:(eq nat (S m0) O). let H4 \def (eq_ind nat (S m0) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H3) in let DEFINED \def (False_ind ((le (S n) m0)\to P) H4) in (DEFINED H2))))) O H0) in (H2 (refl_equal nat O))))) (\lambda n1:nat.(\lambda _:(\forall P:Prop.((le (S n) n1)\to ((le (S n1) (S n))\to P))).(\lambda P:Prop.(\lambda H1:(le (S n) (S n1)).(\lambda H2:(le (S (S n1)) (S n)). let DEFINED \def (le_S_n (S n1) n H2) in (H n1 P (le_S_n n n1 H1) DEFINED)))))) n0)))) m)) +Post Nodes: 400 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_Sx_x +Pre Nodes : 20 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda H:(le (S x) x).(\lambda P:Prop. let H0 \def le_Sn_n in let DEFINED \def (H0 x H) in (False_ind P DEFINED)))) +Post Nodes: 22 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: minus_le +Pre Nodes : 88 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.(le (minus n y) n))) (\lambda _:nat.(le_n O)) (\lambda n:nat.(\lambda H:(\forall y:nat.(le (minus n y) n)).(\lambda y:nat.(nat_ind (\lambda n0:nat.(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda n0:nat.(\lambda _:(le +match n0 return (\lambda n1:nat.nat) with + [ O => (S n) + | (S (l:nat)) => (minus n l) +] (S n)).(le_S (minus n n0) n (H n0)))) y)))) x)) +Post Nodes: 88 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_plus_minus_sym +Pre Nodes : 45 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda n:nat.(\lambda m:nat.(\lambda H:(le n m). let DEFINED \def (plus_comm (minus m n) n) in (eq_ind_r nat (plus n (minus m n)) (\lambda n0:nat.(eq nat m n0)) (le_plus_minus n m H) (plus (minus m n) n) DEFINED)))) +Post Nodes: 47 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_minus_minus +Pre Nodes : 84 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(le x y).(\lambda z:nat.(\lambda H0:(le y z). let DEFINED \def (le_plus_minus_r x z (le_trans x y z H H0)) in let DEFINED0 \def (le_plus_minus_r x y H) in (plus_le_reg_l x (minus y x) (minus z x) (eq_ind_r nat y (\lambda n:nat.(le n (plus x (minus z x)))) (eq_ind_r nat z (\lambda n:nat.(le y n)) H0 (plus x (minus z x)) DEFINED) (plus x (minus y x)) DEFINED0))))))) +Post Nodes: 88 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_minus_plus +Pre Nodes : 505 +Warn: Optimizer: remove 3 +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +nat +nat +nat +nat +Warn: Optimizer: remove 3 +Warn: Optimizer: swap 2 +Warn: Optimizer: nested application +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x:nat.((le n x)\to (\forall y:nat.(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) (\lambda x:nat.(\lambda H:(le O x). let H0 \def (le_ind O (\lambda n:nat.((eq nat n x)\to (\forall y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))))) (\lambda H0:(eq nat O x).(eq_ind nat O (\lambda n:nat.(\forall y:nat.(eq nat (minus (plus n y) O) (plus (minus n O) y)))) (\lambda y:nat.(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) (minus_n_O (plus O y)))) x H0)) (\lambda m:nat.(\lambda H0:(le O m).(\lambda _:((eq nat m x)\to (\forall y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y)))).(\lambda H1:(eq nat (S m) x). let DEFINED \def (eq_ind nat (S m) (\lambda n:nat.((le O m)\to (\forall y:nat.(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda _:(le O m).(\lambda y:nat.(refl_equal nat (plus (minus (S m) O) y)))) x H1) in (DEFINED H0))))) x H) in (H0 (refl_equal nat x)))) (\lambda z0:nat.(\lambda H:(\forall x:nat.((le z0 x)\to (\forall y:nat.(eq nat (minus (plus x y) z0) (plus (minus x z0) y))))).(\lambda x:nat.(nat_ind (\lambda n:nat.((le (S z0) n)\to (\forall y:nat.(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y))))) (\lambda H0:(le (S z0) O).(\lambda y:nat. let H1 \def (le_ind (S z0) (\lambda n:nat.((eq nat n O)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)))) (\lambda H1:(eq nat (S z0) O). let H2 \def (eq_ind nat (S z0) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H1) in (False_ind (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2)) (\lambda m:nat.(\lambda H1:(le (S z0) m).(\lambda _:((eq nat m O)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))).(\lambda H2:(eq nat (S m) O). let H3 \def (eq_ind nat (S m) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H2) in let DEFINED \def (False_ind ((le (S z0) m)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O)))) (\lambda n:nat.(\lambda _:((le (S z0) n)\to (\forall y:nat.(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y)))).(\lambda H1:(le (S z0) (S n)).(\lambda y:nat.(H n (le_S_n z0 n H1) y))))) x)))) z)) +Post Nodes: 560 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_minus +Pre Nodes : 51 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda z:nat.(\lambda y:nat.(\lambda H:(le (plus x y) z). let DEFINED \def (minus_plus_r x y) in (eq_ind nat (minus (plus x y) y) (\lambda n:nat.(le n (minus z y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x DEFINED))))) +Post Nodes: 53 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_trans_plus_r +Pre Nodes : 27 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda z:nat.(\lambda H:(le (plus x y) z).(le_trans y (plus x y) z (le_plus_r x y) H))))) +Post Nodes: 27 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_gen_S +Pre Nodes : 217 +Warn: Optimizer: remove 3 +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +Optimized : (\lambda m:nat.(\lambda x:nat.(\lambda H:(le (S m) x). let H0 \def (le_ind (S m) (\lambda n:nat.((eq nat n x)\to (ex2 nat (\lambda n0:nat.(eq nat x (S n0))) (\lambda n0:nat.(le m n0))))) (\lambda H0:(eq nat (S m) x).(eq_ind nat (S m) (\lambda n:nat.(ex2 nat (\lambda n0:nat.(eq nat n (S n0))) (\lambda n0:nat.(le m n0)))) (ex_intro2 nat (\lambda n:nat.(eq nat (S m) (S n))) (\lambda n:nat.(le m n)) m (refl_equal nat (S m)) (le_n m)) x H0)) (\lambda m0:nat.(\lambda H0:(le (S m) m0).(\lambda _:((eq nat m0 x)\to (ex2 nat (\lambda n0:nat.(eq nat x (S n0))) (\lambda n0:nat.(le m n0)))).(\lambda H1:(eq nat (S m0) x). let DEFINED \def (eq_ind nat (S m0) (\lambda n:nat.((le (S m) m0)\to (ex2 nat (\lambda n0:nat.(eq nat n (S n0))) (\lambda n0:nat.(le m n0))))) (\lambda H2:(le (S m) m0).(ex_intro2 nat (\lambda n:nat.(eq nat (S m0) (S n))) (\lambda n:nat.(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) x H1) in (DEFINED H0))))) x H) in (H0 (refl_equal nat x))))) +Post Nodes: 243 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_x_plus_x_Sy +Pre Nodes : 64 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda y:nat. let DEFINED \def (plus_comm x (S y)) in (eq_ind_r nat (plus (S y) x) (\lambda n:nat.(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) DEFINED))) +Post Nodes: 66 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: simpl_lt_plus_r +Pre Nodes : 75 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda p:nat.(\lambda n:nat.(\lambda m:nat.(\lambda H:(lt (plus n p) (plus m p)). let DEFINED \def (plus_comm n p) in let H0 \def (eq_ind nat (plus n p) (\lambda n0:nat.(lt n0 (plus m p))) H (plus p n) DEFINED) in let DEFINED0 \def (plus_comm m p) in let H1 \def (eq_ind nat (plus m p) (\lambda n0:nat.(lt (plus p n) n0)) H0 (plus p m) DEFINED0) in (plus_lt_reg_l n m p H1))))) +Post Nodes: 79 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: minus_x_Sy +Pre Nodes : 330 +nat +nat +nat +nat +Warn: Optimizer: remove 3 +Warn: Optimizer: swap 2 +Warn: Optimizer: nested application +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y))))))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq nat (minus O y) (S (minus O (S y)))))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H0) in (False_ind (eq nat (minus O y) (S (minus O (S y)))) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq nat (minus O y) (S (minus O (S y))))).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq nat (minus O y) (S (minus O (S y))))) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y)))))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda _:(lt O (S n)). let DEFINED \def (minus_n_O n) in (eq_ind nat n (\lambda n0:nat.(eq nat (S n) (S n0))) (refl_equal nat (S n)) (minus n O) DEFINED)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))).(\lambda H1:(lt (S n0) (S n)). let H2 \def (le_S_n (S n0) n H1) in (H n0 H2)))) y)))) x)) +Post Nodes: 354 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_plus_minus +Pre Nodes : 16 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y).(le_plus_minus (S x) y H)))) +Post Nodes: 16 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_plus_minus_r +Pre Nodes : 53 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y). let DEFINED \def (plus_comm (minus y (S x)) x) in (eq_ind_r nat (plus x (minus y (S x))) (\lambda n:nat.(eq nat y (S n))) (lt_plus_minus x y H) (plus (minus y (S x)) x) DEFINED)))) +Post Nodes: 55 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: minus_x_SO +Pre Nodes : 56 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda H:(lt O x). let DEFINED \def (minus_n_O x) in let DEFINED0 \def (minus_x_Sy x O H) in (eq_ind nat (minus x O) (\lambda n:nat.(eq nat x n)) (eq_ind nat x (\lambda n:nat.(eq nat x n)) (refl_equal nat x) (minus x O) DEFINED) (S (minus x (S O))) DEFINED0))) +Post Nodes: 60 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_x_pred_y +Pre Nodes : 175 +nat +nat +nat +nat +Warn: Optimizer: remove 3 +Warn: Optimizer: swap 2 +Warn: Optimizer: nested application +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +Optimized : (\lambda y:nat.(nat_ind (\lambda n:nat.(\forall x:nat.((lt x n)\to (le x (pred n))))) (\lambda x:nat.(\lambda H:(lt x O). let H0 \def (le_ind (S x) (\lambda n:nat.((eq nat n O)\to (le x O))) (\lambda H0:(eq nat (S x) O). let H1 \def (eq_ind nat (S x) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H0) in (False_ind (le x O) H1)) (\lambda m:nat.(\lambda H0:(le (S x) m).(\lambda _:((eq nat m O)\to (le x O)).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H1) in let DEFINED \def (False_ind ((le (S x) m)\to (le x O)) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda _:(\forall x:nat.((lt x n)\to (le x (pred n)))).(\lambda x:nat.(\lambda H0:(lt x (S n)).(le_S_n x n H0))))) y)) +Post Nodes: 186 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_le_minus +Pre Nodes : 44 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y). let DEFINED \def (plus_comm x (S O)) in (le_minus x y (S O) (eq_ind_r nat (plus (S O) x) (\lambda n:nat.(le n y)) H (plus x (S O)) DEFINED))))) +Post Nodes: 46 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_le_e +Pre Nodes : 39 +Optimized : (\lambda n:nat.(\lambda d:nat.(\lambda P:Prop.(\lambda H:((lt n d)\to P).(\lambda H0:((le d n)\to P). let H1 \def (le_or_lt d n) in (or_ind (le d n) (lt n d) P H0 H H1)))))) +Post Nodes: 39 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_eq_e +Pre Nodes : 45 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda P:Prop.(\lambda H:((lt x y)\to P).(\lambda H0:((eq nat x y)\to P).(\lambda H1:(le x y). let DEFINED \def (le_lt_or_eq x y H1) in (or_ind (lt x y) (eq nat x y) P H H0 DEFINED))))))) +Post Nodes: 47 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_eq_gt_e +Pre Nodes : 60 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda P:Prop.(\lambda H:((lt x y)\to P).(\lambda H0:((eq nat x y)\to P).(\lambda H1:((lt y x)\to P).(lt_le_e x y P H (\lambda H2:(le y x).(lt_eq_e y x P H1 (\lambda H3:(eq nat y x).(H0 (sym_eq nat y x H3))) H2))))))))) +Post Nodes: 60 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_gen_xS +Pre Nodes : 190 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall n0:nat.((lt n (S n0))\to (or (eq nat n O) (ex2 nat (\lambda m:nat.(eq nat n (S m))) (\lambda m:nat.(lt m n0))))))) (\lambda n:nat.(\lambda _:(lt O (S n)).(or_introl (eq nat O O) (ex2 nat (\lambda m:nat.(eq nat O (S m))) (\lambda m:nat.(lt m n))) (refl_equal nat O)))) (\lambda n:nat.(\lambda _:(\forall n0:nat.((lt n (S n0))\to (or (eq nat n O) (ex2 nat (\lambda m:nat.(eq nat n (S m))) (\lambda m:nat.(lt m n0)))))).(\lambda n0:nat.(\lambda H0:(lt (S n) (S n0)).(or_intror (eq nat (S n) O) (ex2 nat (\lambda m:nat.(eq nat (S n) (S m))) (\lambda m:nat.(lt m n0))) (ex_intro2 nat (\lambda m:nat.(eq nat (S n) (S m))) (\lambda m:nat.(lt m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x)) +Post Nodes: 190 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_lt_false +Pre Nodes : 25 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(le x y).(\lambda H0:(lt y x).(\lambda P:Prop. let DEFINED \def (le_not_lt x y H H0) in (False_ind P DEFINED)))))) +Post Nodes: 27 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: lt_neq +Pre Nodes : 33 +Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y).(\lambda H0:(eq nat x y). let H1 \def (eq_ind nat x (\lambda n:nat.(lt n y)) H y H0) in (lt_irrefl y H1))))) +Post Nodes: 33 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: arith0 +Pre Nodes : 185 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda h2:nat.(\lambda d2:nat.(\lambda n:nat.(\lambda H:(le (plus d2 h2) n).(\lambda h3:nat. let DEFINED \def (plus_comm h2 d2) in let DEFINED0 \def (plus_assoc h2 d2 h3) in let DEFINED1 \def (minus_plus h2 (plus d2 h3)) in (eq_ind nat (minus (plus h2 (plus d2 h3)) h2) (\lambda n0:nat.(le n0 (minus (plus n h3) h2))) (le_minus_minus h2 (plus h2 (plus d2 h3)) (le_plus_l h2 (plus d2 h3)) (plus n h3) (eq_ind_r nat (plus (plus h2 d2) h3) (\lambda n0:nat.(le n0 (plus n h3))) (eq_ind_r nat (plus d2 h2) (\lambda n0:nat.(le (plus n0 h3) (plus n h3))) (le_S_n (plus (plus d2 h2) h3) (plus n h3) (lt_le_S (plus (plus d2 h2) h3) (S (plus n h3)) (le_lt_n_Sm (plus (plus d2 h2) h3) (plus n h3) (plus_le_compat (plus d2 h2) n h3 h3 H (le_n h3))))) (plus h2 d2) DEFINED) (plus h2 (plus d2 h3)) DEFINED0)) (plus d2 h3) DEFINED1)))))) +Post Nodes: 191 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: O_minus +Pre Nodes : 211 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le n y)\to (eq nat (minus n y) O)))) (\lambda y:nat.(\lambda _:(le O y).(refl_equal nat O))) (\lambda x0:nat.(\lambda H:(\forall y:nat.((le x0 y)\to (eq nat (minus x0 y) O))).(\lambda y:nat.(nat_ind (\lambda n:nat.((le (S x0) n)\to (eq nat +match n return (\lambda n1:nat.nat) with + [ O => (S x0) + | (S (l:nat)) => (minus x0 l) +] O))) (\lambda H0:(le (S x0) O). let DEFINED \def (le_gen_S x0 O H0) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le x0 n)) (eq nat (S x0) O) (\lambda x1:nat.(\lambda H1:(eq nat O (S x1)).(\lambda _:(le x0 x1). let H3 \def (eq_ind nat O (\lambda ee:nat. +match ee return (\lambda _:nat.Prop) with + [ O => True + | (S (_:nat)) => False +]) I (S x1) H1) in (False_ind (eq nat (S x0) O) H3)))) DEFINED)) (\lambda n:nat.(\lambda _:((le (S x0) n)\to (eq nat +match n return (\lambda n1:nat.nat) with + [ O => (S x0) + | (S (l:nat)) => (minus x0 l) +] O)).(\lambda H1:(le (S x0) (S n)).(H n (le_S_n x0 n H1))))) y)))) x)) +Post Nodes: 213 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: minus_minus +Pre Nodes : 592 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x:nat.(\forall y:nat.((le n x)\to ((le n y)\to ((eq nat (minus x n) (minus y n))\to (eq nat x y))))))) (\lambda x:nat.(\lambda y:nat.(\lambda _:(le O x).(\lambda _:(le O y).(\lambda H1:(eq nat (minus x O) (minus y O)). let DEFINED \def (minus_n_O x) in let H2 \def (eq_ind_r nat (minus x O) (\lambda n:nat.(eq nat n (minus y O))) H1 x DEFINED) in let DEFINED0 \def (minus_n_O y) in let H3 \def (eq_ind_r nat (minus y O) (\lambda n:nat.(eq nat x n)) H2 y DEFINED0) in H3))))) (\lambda z0:nat.(\lambda IH:(\forall x:nat.(\forall y:nat.((le z0 x)\to ((le z0 y)\to ((eq nat (minus x z0) (minus y z0))\to (eq nat x y)))))).(\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le (S z0) n)\to ((le (S z0) y)\to ((eq nat (minus n (S z0)) (minus y (S z0)))\to (eq nat n y)))))) (\lambda y:nat.(\lambda H:(le (S z0) O).(\lambda _:(le (S z0) y).(\lambda _:(eq nat (minus O (S z0)) (minus y (S z0))). let DEFINED \def (le_gen_S z0 O H) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le z0 n)) (eq nat O y) (\lambda x0:nat.(\lambda H2:(eq nat O (S x0)).(\lambda _:(le z0 x0). let H4 \def (eq_ind nat O (\lambda ee:nat. +match ee return (\lambda _:nat.Prop) with + [ O => True + | (S (_:nat)) => False +]) I (S x0) H2) in (False_ind (eq nat O y) H4)))) DEFINED))))) (\lambda x0:nat.(\lambda _:(\forall y:nat.((le (S z0) x0)\to ((le (S z0) y)\to ((eq nat (minus x0 (S z0)) (minus y (S z0)))\to (eq nat x0 y))))).(\lambda y:nat.(nat_ind (\lambda n:nat.((le (S z0) (S x0))\to ((le (S z0) n)\to ((eq nat (minus (S x0) (S z0)) (minus n (S z0)))\to (eq nat (S x0) n))))) (\lambda _:(le (S z0) (S x0)).(\lambda H0:(le (S z0) O).(\lambda _:(eq nat (minus (S x0) (S z0)) (minus O (S z0))). let DEFINED \def (le_gen_S z0 O H0) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le z0 n)) (eq nat (S x0) O) (\lambda x1:nat.(\lambda H2:(eq nat O (S x1)).(\lambda _:(le z0 x1). let H4 \def (eq_ind nat O (\lambda ee:nat. +match ee return (\lambda _:nat.Prop) with + [ O => True + | (S (_:nat)) => False +]) I (S x1) H2) in (False_ind (eq nat (S x0) O) H4)))) DEFINED)))) (\lambda y0:nat.(\lambda _:((le (S z0) (S x0))\to ((le (S z0) y0)\to ((eq nat (minus (S x0) (S z0)) (minus y0 (S z0)))\to (eq nat (S x0) y0)))).(\lambda H:(le (S z0) (S x0)).(\lambda H0:(le (S z0) (S y0)).(\lambda H1:(eq nat (minus (S x0) (S z0)) (minus (S y0) (S z0))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z)) +Post Nodes: 600 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: plus_plus +Pre Nodes : 1222 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Warn: Optimizer: swap 1 +Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x1:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le x1 n)\to ((le x2 n)\to ((eq nat (plus (minus n x1) y1) (plus (minus n x2) y2))\to (eq nat (plus x1 y2) (plus x2 y1)))))))))) (\lambda x1:nat.(\lambda x2:nat.(\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le x1 O).(\lambda H0:(le x2 O).(\lambda H1:(eq nat y1 y2). let H_y \def (le_n_O_eq x2 H0) in let H_y0 \def (le_n_O_eq x1 H) in (eq_ind nat y1 (\lambda n:nat.(eq nat (plus x1 n) (plus x2 y1))) (eq_ind nat O (\lambda n:nat.(eq nat (plus x1 y1) (plus n y1))) (eq_ind nat O (\lambda n:nat.(eq nat (plus n y1) (plus O y1))) (refl_equal nat (plus O y1)) x1 H_y0) x2 H_y) y2 H1)))))))) (\lambda z0:nat.(\lambda IH:(\forall x1:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le x1 z0)\to ((le x2 z0)\to ((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2))\to (eq nat (plus x1 y2) (plus x2 y1))))))))).(\lambda x1:nat.(nat_ind (\lambda n:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le n (S z0))\to ((le x2 (S z0))\to ((eq nat (plus (minus (S z0) n) y1) (plus (minus (S z0) x2) y2))\to (eq nat (plus n y2) (plus x2 y1))))))))) (\lambda x2:nat.(nat_ind (\lambda n:nat.(\forall y1:nat.(\forall y2:nat.((le O (S z0))\to ((le n (S z0))\to ((eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) n) y2))\to (eq nat (plus O y2) (plus n y1)))))))) (\lambda y1:nat.(\lambda y2:nat.(\lambda _:(le O (S z0)).(\lambda _:(le O (S z0)).(\lambda H1:(eq nat (S (plus z0 y1)) (S (plus z0 y2))). let H_y \def (IH O O) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.(\forall y3:nat.(\forall y4:nat.((le O z0)\to ((le O z0)\to ((eq nat (plus n y3) (plus n y4))\to (eq nat y4 y3))))))) H_y z0 DEFINED) in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (H2 (plus z0 y2) (plus z0 y1) (le_O_n z0) (le_O_n z0) (f_equal nat nat (plus z0) (plus z0 y2) (plus z0 y1) (sym_eq nat (plus z0 y1) (plus z0 y2) (eq_add_S (plus z0 y1) (plus z0 y2) H1)))))))))) (\lambda x3:nat.(\lambda _:(\forall y1:nat.(\forall y2:nat.((le O (S z0))\to ((le x3 (S z0))\to ((eq nat (S (plus z0 y1)) (plus +match x3 return (\lambda n:nat.nat) with + [ O => (S z0) + | (S (l:nat)) => (minus z0 l) +] y2))\to (eq nat y2 (plus x3 y1))))))).(\lambda y1:nat.(\lambda y2:nat.(\lambda _:(le O (S z0)).(\lambda H0:(le (S x3) (S z0)).(\lambda H1:(eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2)). let H_y \def (IH O x3 (S y1)) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat (plus n (S y1)) (plus (minus z0 x3) y3))\to (eq nat y3 (plus x3 (S y1)))))))) H_y z0 DEFINED) in let DEFINED0 \def (plus_n_Sm z0 y1) in let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat n (plus (minus z0 x3) y3))\to (eq nat y3 (plus x3 (S y1)))))))) H2 (S (plus z0 y1)) DEFINED0) in let DEFINED1 \def (plus_n_Sm x3 y1) in let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat (S (plus z0 y1)) (plus (minus z0 x3) y3))\to (eq nat y3 n)))))) H3 (S (plus x3 y1)) DEFINED1) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1)))))))) x2)) (\lambda x2:nat.(\lambda _:(\forall x3:nat.(\forall y1:nat.(\forall y2:nat.((le x2 (S z0))\to ((le x3 (S z0))\to ((eq nat (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2))\to (eq nat (plus x2 y2) (plus x3 y1)))))))).(\lambda x3:nat.(nat_ind (\lambda n:nat.(\forall y1:nat.(\forall y2:nat.((le (S x2) (S z0))\to ((le n (S z0))\to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2))\to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le (S x2) (S z0)).(\lambda _:(le O (S z0)).(\lambda H1:(eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))). let H_y \def (IH x2 O y1 (S y2)) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) (plus n (S y2)))\to (eq nat (plus x2 (S y2)) y1))))) H_y z0 DEFINED) in let DEFINED0 \def (plus_n_Sm z0 y2) in let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) n)\to (eq nat (plus x2 (S y2)) y1))))) H2 (S (plus z0 y2)) DEFINED0) in let DEFINED1 \def (plus_n_Sm x2 y2) in let H4 \def (eq_ind_r nat (plus x2 (S y2)) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))\to (eq nat n y1))))) H3 (S (plus x2 y2)) DEFINED1) in (H4 (le_S_n x2 z0 H) (le_O_n z0) H1)))))) (\lambda x4:nat.(\lambda _:(\forall y1:nat.(\forall y2:nat.((le (S x2) (S z0))\to ((le x4 (S z0))\to ((eq nat (plus (minus z0 x2) y1) (plus +match x4 return (\lambda n:nat.nat) with + [ O => (S z0) + | (S (l:nat)) => (minus z0 l) +] y2))\to (eq nat (S (plus x2 y2)) (plus x4 y1))))))).(\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le (S x2) (S z0)).(\lambda H0:(le (S x4) (S z0)).(\lambda H1:(eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4) y2)).(f_equal nat nat S (plus x2 y2) (plus x4 y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3)))) x1)))) z)) +Post Nodes: 1236 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: le_S_minus +Pre Nodes : 41 +Warn: Optimizer: remove 1 +Optimized : (\lambda d:nat.(\lambda h:nat.(\lambda n:nat.(\lambda H:(le (plus d h) n).(le_S d (minus n h) (le_minus d n h H)))))) +Post Nodes: 27 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/arith.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of ext/arith.mma completed in 44''. +Info: execution of ext/tactics.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext ...'' +Info: baseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics is not empty +Info: cleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics +Info: Removing: cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics/* +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...'' +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: insert_eq +Pre Nodes : 36 +Optimized : (\lambda S:Set.(\lambda x:S.(\lambda P:(S\to Prop).(\lambda G:Prop.(\lambda H:(\forall y:S.((P y)\to ((eq S y x)\to G))).(\lambda H0:(P x).(H x H0 (refl_equal S x)))))))) +Post Nodes: 36 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: unintro +Pre Nodes : 17 +Optimized : (\lambda A:Set.(\lambda a:A.(\lambda P:(A\to Prop).(\lambda H:(\forall x:A.(P x)).(H a))))) +Post Nodes: 17 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: xinduction +Pre Nodes : 27 +Optimized : (\lambda A:Set.(\lambda t:A.(\lambda P:(A\to Prop).(\lambda H:(\forall x:A.((eq A t x)\to (P x))).(H t (refl_equal A t)))))) +Post Nodes: 27 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/tactics.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of ext/tactics.mma completed in 4''. +Info: execution of pippo.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pip ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...'' +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: minus_x_Sy +Pre Nodes : 330 +nat +nat +nat +nat +Warn: Optimizer: remove 3 +Warn: Optimizer: swap 2 +Warn: Optimizer: nested application +Warn: Optimizer: anticipate 2 +Warn: Optimizer: swap 2 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y))))))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq nat (minus O y) (S (minus O (S y)))))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H0) in (False_ind (eq nat (minus O y) (S (minus O (S y)))) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq nat (minus O y) (S (minus O (S y))))).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat. +match e return (\lambda _:nat.Prop) with + [ O => False + | (S (_:nat)) => True +]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq nat (minus O y) (S (minus O (S y))))) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y)))))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda _:(lt O (S n)). let DEFINED \def (minus_n_O n) in (eq_ind nat n (\lambda n0:nat.(eq nat (S n) (S n0))) (refl_equal nat (S n)) (minus n O) DEFINED)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))).(\lambda H1:(lt (S n0) (S n)). let H2 \def (le_S_n (S n0) n H1) in (H n0 H2)))) y)))) x)) +Post Nodes: 354 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./pippo.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of pippo.mma completed in 2''. +Info: execution of plist/defs.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pli ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of plist/defs.mma completed in 1''. +Info: execution of plist/props.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pli ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/plist/def ...'' +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: papp_ss +Pre Nodes : 121 +Warn: Optimizer: anticipate 3 +Warn: Optimizer: swap 3 +Optimized : (\lambda is1:PList.(PList_ind (\lambda p:PList.(\forall is2:PList.(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2))))) (\lambda is2:PList.(refl_equal PList (Ss is2))) (\lambda n:nat.(\lambda n0:nat.(\lambda p:PList.(\lambda H:(\forall is2:PList.(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2)))).(\lambda is2:PList. let DEFINED \def (H is2) in (eq_ind_r PList (Ss (papp p is2)) (\lambda p0:PList.(eq PList (PCons n (S n0) p0) (PCons n (S n0) (Ss (papp p is2))))) (refl_equal PList (PCons n (S n0) (Ss (papp p is2)))) (papp (Ss p) (Ss is2)) DEFINED)))))) is1)) +Post Nodes: 123 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of plist/props.mma completed in 2''. +Info: execution of types/defs.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/typ ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of types/defs.mma completed in 0''. +Info: execution of types/props.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/typ ...'' +Info: baseuri cic:/matita/LAMBDA-TYPES/Base-2/types/props is not empty +Info: cleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/types/props +Info: Removing: cic:/matita/LAMBDA-TYPES/Base-2/types/props/* +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/types/def ...'' +Debug: Executing: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...'' +BEGIN: ex2_sym +Pre Nodes : 77 +Optimized : (\lambda A:Set.(\lambda P:(A\to Prop).(\lambda Q:(A\to Prop).(\lambda H:(ex2 A (\lambda x:A.(P x)) (\lambda x:A.(Q x))).(ex2_ind A (\lambda x:A.(P x)) (\lambda x:A.(Q x)) (ex2 A (\lambda x:A.(Q x)) (\lambda x:A.(P x))) (\lambda x:A.(\lambda H0:(P x).(\lambda H1:(Q x).(ex_intro2 A (\lambda x0:A.(Q x0)) (\lambda x0:A.(P x0)) x H1 H0)))) H))))) +Post Nodes: 77 +Debug: Procedural: level 2 transformation +Debug: Procedural: grafite rendering +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of types/props.mma completed in 2''. +Info: execution of theory.mma started: +Debug: Executing: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/the ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/tactics.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/ext/tacti ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/arith.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/types/pro ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/blt/props ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Debug: Executing: ``include "cic:/matita/LAMBDA-TYPES/Base-2/plist/pro ...'' +Debug: Including /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./theory.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/. +Info: execution of theory.mma completed in 1''. diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/makefile b/matita/contribs/LAMBDA-TYPES/Base-2/makefile new file mode 100644 index 000000000..7615bb7e5 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/makefile @@ -0,0 +1,51 @@ +H=@ + +RT_BASEDIR=/home/fguidi/svn/software/matita/ +OPTIONS=-bench +MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) +CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) +MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) +CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) + +devel:=$(shell basename `pwd`) + +ifneq "$(SRC)" "" + XXX="SRC=$(SRC)" +endif + +all: build_mas preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) +clean: clean_mas preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) +cleanall: clean_mas preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all + +all.opt opt: build_mas preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) +clean.opt: clean_mas preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) +cleanall.opt: clean_mas preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all + +%.mo: preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ +%.mo.opt: preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=) + +preall: + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) + +preall.opt: + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) + + +# FG: added part ############################################################ + +build_mas: + $(H)$(MAKE) preamble.mo.opt + $(H)$(MAKE) -f Makefile + $(H)$(MAKE) preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) + +clean_mas: + $(H)$(MAKE) -f Makefile clean diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma b/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma new file mode 100644 index 000000000..a1b6cdfc1 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs". + +include "preamble.ma". + +(* object PList not inlined *) + + +(* object PConsTail not inlined *) + + +(* object Ss not inlined *) + + +(* object papp not inlined *) + + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma b/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma new file mode 100644 index 000000000..29357a88a --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/props". + +include "plist/defs.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con". + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma b/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma new file mode 100644 index 000000000..84a495545 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/preamble". + +include "../Base-1/definitions.ma". + +alias id "le_ind" = "cic:/Coq/Init/Peano/le_ind.con". + +default "equality" + cic:/Coq/Init/Logic/eq.ind + cic:/matita/LAMBDA-TYPES/Base-1/preamble/sym_eq.con + cic:/matita/LAMBDA-TYPES/Base-1/preamble/trans_eq.con + cic:/Coq/Init/Logic/eq_ind.con + cic:/Coq/Init/Logic/eq_ind_r.con + cic:/Coq/Init/Logic/eq_rec.con + cic:/Coq/Init/Logic/eq_rec_r.con + cic:/Coq/Init/Logic/eq_rect.con + cic:/Coq/Init/Logic/eq_rect_r.con + cic:/matita/LAMBDA-TYPES/Base-1/preamble/f_equal.con + cic:/matita/legacy/coq/f_equal1.con. diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma b/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma new file mode 100644 index 000000000..1adab3e2b --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory". + +include "ext/tactics.ma". + +include "ext/arith.ma". + +include "types/props.ma". + +include "blt/props.ma". + +include "plist/props.ma". + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma b/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma new file mode 100644 index 000000000..cad4f8024 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma @@ -0,0 +1,77 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs". + +include "preamble.ma". + +(* object and3 not inlined *) + + +(* object or3 not inlined *) + + +(* object or4 not inlined *) + + +(* object ex3 not inlined *) + + +(* object ex4 not inlined *) + + +(* object ex_2 not inlined *) + + +(* object ex2_2 not inlined *) + + +(* object ex3_2 not inlined *) + + +(* object ex4_2 not inlined *) + + +(* object ex_3 not inlined *) + + +(* object ex2_3 not inlined *) + + +(* object ex3_3 not inlined *) + + +(* object ex4_3 not inlined *) + + +(* object ex3_4 not inlined *) + + +(* object ex4_4 not inlined *) + + +(* object ex4_5 not inlined *) + + +(* object ex5_5 not inlined *) + + +(* object ex6_6 not inlined *) + + +(* object ex6_7 not inlined *) + + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma b/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma new file mode 100644 index 000000000..d79bfc46b --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/props". + +include "types/defs.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con". + diff --git a/matita/contribs/LAMBDA-TYPES/Makefile b/matita/contribs/LAMBDA-TYPES/Makefile index 285c55b99..8faf376f1 100644 --- a/matita/contribs/LAMBDA-TYPES/Makefile +++ b/matita/contribs/LAMBDA-TYPES/Makefile @@ -1,6 +1,6 @@ GOALS = all opt clean clean.opt -DEVELS = Base-1 LambdaDelta-1 Unified-Sub +DEVELS = Base-1 LambdaDelta-1 Base-2 Unified-Sub $(GOALS): @$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) diff --git a/matita/template_makefile_devel.in b/matita/template_makefile_devel.in index 73996380f..1c0b1687b 100644 --- a/matita/template_makefile_devel.in +++ b/matita/template_makefile_devel.in @@ -30,7 +30,7 @@ cleanall.opt: preall.opt %.mo: preall $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ %.mo.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@ + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=) preall: $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)