--- /dev/null
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+ ../../../matitac
+$(DIR).opt opt all.opt:
+ ../../../matitac.opt
+clean:
+ ../../../matitaclean
+clean.opt:
+ ../../../matitaclean.opt
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/defs".
+
include "preamble.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/props".
+
include "blt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/definitions".
+
include "types/defs.ma".
--- /dev/null
+definitions.ma blt/defs.ma plist/defs.ma types/defs.ma
+preamble.ma coq.ma
+theory.ma blt/props.ma ext/arith.ma ext/tactics.ma plist/props.ma types/props.ma
+spare.ma theory.ma
+plist/props.ma plist/defs.ma
+plist/defs.ma preamble.ma
+ext/tactics.ma preamble.ma
+ext/arith.ma preamble.ma
+types/props.ma types/defs.ma
+types/defs.ma preamble.ma
+blt/props.ma blt/defs.ma
+blt/defs.ma preamble.ma
+coq.ma
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith".
+
include "preamble.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics".
+
include "preamble.ma".
+++ /dev/null
-H= @
-
-RT_BASEDIR=../../../
-OPTIONS=-bench -onepass -system
-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: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
-clean: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
-cleanall: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
-
-all.opt opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
-clean.opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
-cleanall.opt: 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)
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/defs".
+
include "preamble.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/props".
+
include "plist/defs.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/preamble".
-include' "../../../legacy/coq.ma".
+
+include "coq.ma".
alias symbol "eq" = "Coq's leibnitz's equality".
alias symbol "leq" = "Coq's natural 'less or equal to'".
--- /dev/null
+baseuri=cic:/matita/LAMBDA-TYPES/Base-1
+include_paths= ../../../legacy
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/spare".
+
include "theory.ma".
(*
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/theory".
+
include "ext/tactics.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/defs".
+
include "preamble.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/props".
+
include "types/defs.ma".
--- /dev/null
+DIR=$(shell basename $$PWD)
+
+MMAS = $(shell find -name "*.mma")
+MAS = $(MMAS:%.mma=%.ma)
+
+%.ma: %.mma
+ echo -e "$< preamble.ma \npreamble.ma" > depends
+ ../../../matitac.opt -dump $@ $< 2>/dev/null
+ ../../../matitadep.opt
+ ../../../matitac.opt $@
+
+$(DIR) all: $(MAS)
+ ../../../matitac
+$(DIR).opt opt all.opt: $(MAS)
+ ../../../matitac.opt
+clean:
+ ../../../matitaclean
+ rm -f $(MAS)
+clean.opt:
+ ../../../matitaclean.opt
+ rm -f $(MAS)
+
+theory2.ma: theory2.mma ext/tactics2.ma ext/arith2.ma types/props2.ma blt/props2.ma plist/props2.ma
+types/props2.ma: types/props2.mma types/defs2.ma
+blt/props2.ma: blt/props2.mma blt/defs2.ma
+plist/props2.ma: plist/props2.mma plist/defs2.ma
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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 *)
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "preamble.ma".
+
+(* object blt not inlined *)
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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".
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "blt/defs2.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".
+
+++ /dev/null
-theory.ma: theory.mma ext/tactics.ma ext/arith.ma types/props.ma blt/props.ma plist/props.ma | ext/tactics.mo.opt ext/arith.mo.opt types/props.mo.opt blt/props.mo.opt plist/props.mo.opt
-ext/tactics.ma: ext/tactics.mma preamble.ma | preamble.mo.opt
-ext/arith.ma: ext/arith.mma preamble.ma | preamble.mo.opt
-types/defs.ma: types/defs.mma preamble.ma | preamble.mo.opt
-types/props.ma: types/props.mma types/defs.ma | types/defs.mo.opt
-blt/defs.ma: blt/defs.mma preamble.ma | preamble.mo.opt
-blt/props.ma: blt/props.mma blt/defs.ma | blt/defs.mo.opt
-plist/defs.ma: plist/defs.mma preamble.ma | preamble.mo.opt
-plist/props.ma: plist/props.mma plist/defs.ma | plist/defs.mo.opt
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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/le_n_pred.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/lt_x_O.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".
-
-inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con".
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+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/le_n_pred.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/lt_x_O.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".
+
+inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con".
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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".
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+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".
+
+++ /dev/null
-H=@
-
-RT_BASEDIR=../../../
-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 ############################################################
-
-MATITAC = $(RT_BASEDIR)/matitac.opt
-
-MMAS = $(shell find -name "*.mma")
-MAS = $(MMAS:%.mma=%.ma)
-
-build_mas: preall.opt $(MAS)
-
-clean_mas:
- $(H)rm -f $(MAS)
-
-%.ma: %.mma
- $(H)$(MATITAC) -dump $@ $< $(OPTIONS)
-
-include depend
-
-.DELETE_ON_ERROR:
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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 *)
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "preamble.ma".
+
+
+(* object PList not inlined *)
+
+
+(* object PConsTail not inlined *)
+
+
+(* object Ss not inlined *)
+
+
+(* object papp not inlined *)
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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".
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "plist/defs2.ma".
+
+inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con".
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/preamble".
-
-include "../Base-1/definitions.ma".
-
-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.
--- /dev/null
+baseuri=cic:/matita/LAMBDA-TYPES/Base-2
+include_paths= ../Base-1 ../../../legacy
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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".
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "ext/tactics2.ma".
+
+include "ext/arith2.ma".
+
+include "types/props2.ma".
+
+include "blt/props2.ma".
+
+include "plist/props2.ma".
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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 and4 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 *)
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "preamble.ma".
+
+
+(* object and3 not inlined *)
+
+
+(* object and4 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 *)
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* 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".
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "types/defs2.ma".
+
+inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con".
+
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/A/defs".
-include "preamble.ma".
+
+include "preamble3.ma".
inductive A: Set \def
| ASort: nat \to (nat \to A)
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/props".
+
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs".
-include "preamble.ma".
+
+include "preamble3.ma".
record G : Set \def {
next: (nat \to nat);
--- /dev/null
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+ ../../../matitac
+$(DIR).opt opt all.opt:
+ ../../../matitac.opt
+clean:
+ ../../../matitaclean
+clean.opt:
+ ../../../matitaclean.opt
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/dec".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs".
-include "preamble.ma".
+
+include "preamble3.ma".
inductive B: Set \def
| Abbr: B
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/props".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/defs".
+
include "asucc/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/props".
+
include "aplus/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aprem/defs".
+
include "A/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aprem/props".
+
include "aprem/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/aprem".
+
include "arity/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/cimp".
+
include "arity/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/defs".
+
include "leq/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/fwd".
+
include "arity/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/lift1".
+
include "arity/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/pr3".
+
include "csuba/arity.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/props".
+
include "arity/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/subst0".
+
include "arity/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/asucc/defs".
+
include "A/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd".
+
include "asucc/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cimp/defs".
+
include "getl/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cimp/props".
+
include "cimp/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/defs".
+
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/drop".
+
include "clear/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/fwd".
+
include "clear/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/props".
+
include "clear/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clen/defs".
+
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clen/getl".
+
include "clen/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cnt/defs".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cnt/props".
+
include "cnt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/arity".
+
include "csuba/getl.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/clear".
+
include "csuba/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/defs".
+
include "arity/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/drop".
+
include "csuba/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd".
+
include "csuba/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/getl".
+
include "csuba/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/props".
+
include "csuba/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/arity".
+
include "csubc/csuba.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/clear".
+
include "csubc/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba".
+
include "csubc/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/defs".
+
include "sc3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/drop".
+
include "csubc/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1".
+
include "csubc/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/getl".
+
include "csubc/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/props".
+
include "csubc/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear".
+
include "csubst0/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs".
+
include "subst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop".
+
include "csubst0/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd".
+
include "csubst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl".
+
include "csubst0/clear.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/props".
+
include "csubst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs".
+
include "csubst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd".
+
include "csubst1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl".
+
include "csubst1/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/props".
+
include "csubst1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/clear".
+
include "csubt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/defs".
+
include "ty3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/drop".
+
include "csubt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd".
+
include "csubt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/getl".
+
include "csubt/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3".
+
include "csubt/getl.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/props".
+
include "csubt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3".
+
include "csubt/pc3.ma".
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/definitions".
-
-include "tlt/defs.ma".
-
-include "iso/defs.ma".
-
-include "clen/defs.ma".
-
-include "flt/defs.ma".
-
-include "cnt/defs.ma".
-
-include "cimp/defs.ma".
-
-include "subst1/defs.ma".
-
-include "csubst1/defs.ma".
-
-include "fsubst0/defs.ma".
-
-include "next_plus/defs.ma".
-
-include "tau1/defs.ma".
-
-include "llt/defs.ma".
-
-include "aprem/defs.ma".
-
-include "ex0/defs.ma".
-
-include "wcpr0/defs.ma".
-
-include "csuba/defs.ma".
-
-include "nf2/defs.ma".
-
-include "ex2/defs.ma".
-
-include "csubc/defs.ma".
-
-include "pc1/defs.ma".
-
-include "ex1/defs.ma".
-
-include "csubt/defs.ma".
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+
+
+include "tlt/defs.ma".
+
+include "iso/defs.ma".
+
+include "clen/defs.ma".
+
+include "flt/defs.ma".
+
+include "cnt/defs.ma".
+
+include "cimp/defs.ma".
+
+include "subst1/defs.ma".
+
+include "csubst1/defs.ma".
+
+include "fsubst0/defs.ma".
+
+include "next_plus/defs.ma".
+
+include "tau1/defs.ma".
+
+include "llt/defs.ma".
+
+include "aprem/defs.ma".
+
+include "ex0/defs.ma".
+
+include "wcpr0/defs.ma".
+
+include "csuba/defs.ma".
+
+include "nf2/defs.ma".
+
+include "ex2/defs.ma".
+
+include "csubc/defs.ma".
+
+include "pc1/defs.ma".
+
+include "ex1/defs.ma".
+
+include "csubt/defs.ma".
+
--- /dev/null
+definitions3.ma aprem/defs.ma cimp/defs.ma clen/defs.ma cnt/defs.ma csuba/defs.ma csubc/defs.ma csubst1/defs.ma csubt/defs.ma ex0/defs.ma ex1/defs.ma ex2/defs.ma flt/defs.ma fsubst0/defs.ma iso/defs.ma llt/defs.ma next_plus/defs.ma nf2/defs.ma pc1/defs.ma subst1/defs.ma tau1/defs.ma tlt/defs.ma wcpr0/defs.ma
+preamble3.ma theory.ma
+spare.ma theory.ma
+theory3.ma ex0/props.ma ex1/props.ma ex2/props.ma pr3/wcpr0.ma subst0/tlt.ma tau1/cnt.ma ty3/dec.ma ty3/nf2.ma ty3/tau0.ma wcpr0/fwd.ma
+tlist/props.ma tlist/defs.ma
+tlist/defs.ma T/defs.ma
+clen/defs.ma C/defs.ma s/defs.ma
+clen/getl.ma clen/defs.ma getl/props.ma
+leq/props.ma aplus/props.ma leq/defs.ma
+leq/asucc.ma aplus/props.ma leq/props.ma
+leq/defs.ma aplus/defs.ma
+leq/fwd.ma leq/defs.ma
+pr3/props.ma pr1/props.ma pr2/props.ma pr3/pr1.ma
+pr3/pr3.ma pr2/pr2.ma pr3/props.ma
+pr3/defs.ma pr2/defs.ma
+pr3/fwd.ma pr2/fwd.ma pr3/props.ma
+pr3/subst1.ma pr2/subst1.ma pr3/defs.ma
+pr3/iso.ma iso/props.ma pr3/fwd.ma tlist/props.ma
+pr3/wcpr0.ma pr3/props.ma wcpr0/getl.ma
+pr3/pr1.ma pr1/defs.ma pr3/defs.ma
+ty3/fsubst0.ma csubst0/props.ma getl/getl.ma pc3/fsubst0.ma ty3/props.ma
+ty3/nf2.ma nf2/arity.ma pc3/nf2.ma ty3/arity.ma
+ty3/props.ma pc3/fwd.ma ty3/fwd.ma
+ty3/arity_props.ma sc3/arity.ma ty3/arity.ma ty3/fwd.ma
+ty3/arity.ma arity/pr3.ma asucc/fwd.ma ty3/pr3_props.ma
+ty3/pr3_props.ma ty3/pr3.ma
+ty3/tau0.ma tau0/defs.ma ty3/pr3_props.ma
+ty3/pr3.ma csubt/ty3.ma pc1/props.ma pc3/pc1.ma pc3/wcpr0.ma ty3/fsubst0.ma ty3/subst1.ma
+ty3/defs.ma G/defs.ma pc3/defs.ma
+ty3/fwd.ma pc3/props.ma ty3/defs.ma
+ty3/dec.ma getl/dec.ma getl/flt.ma pc3/dec.ma ty3/pr3_props.ma
+ty3/subst1.ma csubst1/fwd.ma csubst1/getl.ma getl/getl.ma pc3/fwd.ma pc3/subst1.ma ty3/props.ma
+cnt/props.ma cnt/defs.ma lift/fwd.ma
+cnt/defs.ma T/defs.ma
+fsubst0/defs.ma csubst0/defs.ma subst0/defs.ma
+fsubst0/fwd.ma fsubst0/defs.ma
+iso/props.ma iso/fwd.ma
+iso/defs.ma T/defs.ma
+iso/fwd.ma iso/defs.ma tlist/defs.ma
+lift/props.ma lift/fwd.ma s/props.ma tlist/defs.ma
+lift/defs.ma T/defs.ma s/defs.ma tlist/defs.ma
+lift/tlt.ma lift/fwd.ma tlt/props.ma
+lift/fwd.ma lift/defs.ma
+flt/props.ma C/props.ma flt/defs.ma
+flt/defs.ma C/defs.ma
+A/defs.ma preamble3.ma
+subst0/props.ma lift/props.ma subst0/fwd.ma
+subst0/defs.ma lift/defs.ma
+subst0/tlt.ma lift/props.ma lift/tlt.ma subst0/defs.ma
+subst0/fwd.ma lift/props.ma subst0/defs.ma
+subst0/subst0.ma subst0/props.ma
+subst0/dec.ma lift/props.ma subst0/defs.ma
+pr1/props.ma T/props.ma pr0/subst1.ma pr1/defs.ma subst1/props.ma
+pr1/defs.ma pr0/defs.ma
+pr1/pr1.ma pr0/pr0.ma pr1/props.ma
+T/props.ma T/defs.ma
+T/defs.ma preamble3.ma
+T/dec.ma T/defs.ma
+sc3/props.ma arity/aprem.ma arity/lift1.ma csuba/arity.ma drop1/getl.ma drop1/props.ma lift1/props.ma llt/props.ma nf2/lift1.ma sc3/defs.ma sn3/lift1.ma
+sc3/arity.ma csubc/arity.ma csubc/drop1.ma csubc/getl.ma csubc/props.ma
+sc3/defs.ma arity/defs.ma drop1/defs.ma sn3/defs.ma
+tau1/props.ma tau0/props.ma tau1/defs.ma
+tau1/defs.ma tau0/defs.ma
+tau1/cnt.ma cnt/props.ma tau1/props.ma
+aplus/props.ma aplus/defs.ma next_plus/props.ma
+aplus/defs.ma asucc/defs.ma
+asucc/defs.ma A/defs.ma G/defs.ma
+asucc/fwd.ma asucc/defs.ma
+aprem/props.ma aprem/defs.ma leq/defs.ma
+aprem/defs.ma A/defs.ma
+nf2/props.ma nf2/defs.ma pr2/fwd.ma
+nf2/arity.ma arity/subst0.ma nf2/fwd.ma
+nf2/pr3.ma nf2/defs.ma pr3/pr3.ma
+nf2/defs.ma pr2/defs.ma
+nf2/fwd.ma T/props.ma nf2/defs.ma pr2/clen.ma subst0/dec.ma
+nf2/dec.ma C/props.ma nf2/defs.ma pr0/dec.ma pr2/clen.ma pr2/fwd.ma
+nf2/lift1.ma drop1/defs.ma nf2/props.ma
+nf2/iso.ma iso/props.ma nf2/pr3.ma pr3/fwd.ma
+drop/props.ma drop/fwd.ma lift/props.ma r/props.ma
+drop/defs.ma C/defs.ma lift/defs.ma r/defs.ma
+drop/fwd.ma drop/defs.ma
+csuba/drop.ma csuba/fwd.ma drop/fwd.ma
+csuba/clear.ma clear/fwd.ma csuba/defs.ma
+csuba/props.ma csuba/defs.ma
+csuba/arity.ma T/props.ma arity/props.ma csuba/getl.ma csuba/props.ma
+csuba/defs.ma arity/defs.ma
+csuba/fwd.ma csuba/defs.ma
+csuba/getl.ma csuba/clear.ma csuba/drop.ma getl/clear.ma
+C/props.ma C/defs.ma T/props.ma
+C/defs.ma T/defs.ma
+csubt/drop.ma csubt/defs.ma drop/fwd.ma
+csubt/clear.ma clear/fwd.ma csubt/defs.ma
+csubt/props.ma csubt/defs.ma
+csubt/pc3.ma csubt/getl.ma pc3/left.ma
+csubt/defs.ma ty3/defs.ma
+csubt/fwd.ma csubt/defs.ma
+csubt/ty3.ma csubt/pc3.ma csubt/props.ma
+csubt/getl.ma csubt/clear.ma csubt/drop.ma csubt/fwd.ma getl/clear.ma
+cimp/props.ma cimp/defs.ma getl/getl.ma
+cimp/defs.ma getl/defs.ma
+drop1/props.ma drop/props.ma drop1/defs.ma getl/defs.ma
+drop1/defs.ma drop/defs.ma lift1/defs.ma
+drop1/getl.ma drop1/defs.ma getl/drop.ma
+lift1/props.ma drop1/defs.ma lift/props.ma lift1/defs.ma
+lift1/defs.ma lift/defs.ma
+lift1/fwd.ma lift/fwd.ma lift1/defs.ma
+pr2/pr2.ma getl/props.ma pr0/pr0.ma pr2/defs.ma
+pr2/props.ma getl/clear.ma getl/drop.ma pr0/props.ma pr2/defs.ma
+pr2/defs.ma getl/defs.ma pr0/defs.ma
+pr2/fwd.ma getl/clear.ma getl/drop.ma pr0/fwd.ma pr2/defs.ma
+pr2/subst1.ma csubst1/fwd.ma csubst1/getl.ma getl/drop.ma pr0/fwd.ma pr0/subst1.ma pr2/defs.ma subst1/subst1.ma
+pr2/clen.ma clen/getl.ma pr2/props.ma
+pc3/fsubst0.ma csubst0/getl.ma fsubst0/defs.ma pc3/left.ma
+pc3/nf2.ma nf2/pr3.ma pc3/defs.ma
+pc3/pc1.ma pc1/defs.ma pc3/defs.ma pr3/pr1.ma
+pc3/props.ma pc3/defs.ma pr3/pr3.ma
+pc3/left.ma pc3/props.ma
+pc3/defs.ma pr3/defs.ma
+pc3/fwd.ma pc3/props.ma pr3/fwd.ma
+pc3/dec.ma nf2/fwd.ma ty3/arity_props.ma ty3/pr3.ma
+pc3/subst1.ma pc3/props.ma pr3/subst1.ma
+pc3/wcpr0.ma pc3/props.ma wcpr0/getl.ma
+pr0/props.ma pr0/defs.ma subst0/subst0.ma
+pr0/pr0.ma lift/tlt.ma pr0/fwd.ma
+pr0/defs.ma subst0/defs.ma
+pr0/fwd.ma pr0/props.ma
+pr0/dec.ma T/dec.ma T/props.ma pr0/fwd.ma subst0/dec.ma
+pr0/subst1.ma pr0/props.ma subst1/defs.ma
+subst1/props.ma subst0/props.ma subst1/defs.ma
+subst1/defs.ma subst0/defs.ma
+subst1/fwd.ma subst0/props.ma subst1/defs.ma
+subst1/subst1.ma subst0/subst0.ma subst1/fwd.ma
+tlt/props.ma tlt/defs.ma
+tlt/defs.ma T/defs.ma
+r/props.ma r/defs.ma s/defs.ma
+r/defs.ma T/defs.ma
+wcpr0/defs.ma C/defs.ma pr0/defs.ma
+wcpr0/fwd.ma wcpr0/defs.ma
+wcpr0/getl.ma getl/props.ma wcpr0/defs.ma
+G/defs.ma preamble3.ma
+csubst0/drop.ma csubst0/fwd.ma drop/fwd.ma s/props.ma
+csubst0/clear.ma clear/fwd.ma csubst0/fwd.ma
+csubst0/props.ma csubst0/defs.ma
+csubst0/defs.ma C/defs.ma subst0/defs.ma
+csubst0/fwd.ma csubst0/defs.ma
+csubst0/getl.ma csubst0/clear.ma csubst0/drop.ma getl/fwd.ma
+next_plus/props.ma next_plus/defs.ma
+next_plus/defs.ma G/defs.ma
+tau0/props.ma getl/drop.ma tau0/defs.ma
+tau0/defs.ma G/defs.ma getl/defs.ma
+csubc/drop.ma csubc/defs.ma sc3/props.ma
+csubc/clear.ma csubc/defs.ma
+csubc/props.ma csubc/defs.ma sc3/props.ma
+csubc/arity.ma arity/defs.ma csubc/csuba.ma
+csubc/drop1.ma csubc/drop.ma
+csubc/defs.ma sc3/defs.ma
+csubc/csuba.ma csuba/defs.ma csubc/defs.ma sc3/props.ma
+csubc/getl.ma csubc/clear.ma csubc/drop.ma
+arity/props.ma arity/fwd.ma
+arity/aprem.ma aprem/props.ma arity/cimp.ma arity/props.ma
+arity/pr3.ma arity/subst0.ma csuba/arity.ma pr0/fwd.ma pr1/defs.ma pr3/defs.ma wcpr0/getl.ma
+arity/defs.ma getl/defs.ma leq/defs.ma
+arity/fwd.ma arity/defs.ma getl/drop.ma leq/asucc.ma leq/fwd.ma
+arity/subst0.ma arity/props.ma csubst0/getl.ma csubst0/props.ma fsubst0/fwd.ma getl/getl.ma subst0/dec.ma subst0/fwd.ma
+arity/lift1.ma arity/props.ma drop1/defs.ma
+arity/cimp.ma arity/defs.ma cimp/props.ma
+ex2/props.ma arity/fwd.ma ex2/defs.ma nf2/defs.ma pr2/fwd.ma
+ex2/defs.ma C/defs.ma
+getl/drop.ma clear/drop.ma getl/props.ma r/props.ma
+getl/clear.ma clear/drop.ma getl/props.ma
+getl/props.ma clear/props.ma drop/props.ma getl/fwd.ma
+getl/defs.ma clear/defs.ma drop/defs.ma
+getl/fwd.ma clear/fwd.ma drop/fwd.ma getl/defs.ma
+getl/dec.ma getl/props.ma
+getl/flt.ma clear/props.ma flt/props.ma getl/fwd.ma
+getl/getl.ma getl/clear.ma getl/drop.ma
+clear/drop.ma clear/fwd.ma drop/fwd.ma
+clear/props.ma clear/fwd.ma
+clear/defs.ma C/defs.ma
+clear/fwd.ma clear/defs.ma
+s/props.ma s/defs.ma
+s/defs.ma T/defs.ma
+pc1/props.ma pc1/defs.ma pr1/pr1.ma
+pc1/defs.ma pr1/defs.ma
+sn3/nf2.ma nf2/dec.ma nf2/pr3.ma sn3/defs.ma
+sn3/props.ma iso/props.ma nf2/iso.ma pr3/iso.ma sn3/fwd.ma sn3/nf2.ma
+sn3/defs.ma pr3/defs.ma
+sn3/fwd.ma pr3/props.ma sn3/defs.ma
+sn3/lift1.ma drop1/defs.ma lift1/fwd.ma sn3/props.ma
+llt/props.ma leq/defs.ma llt/defs.ma
+llt/defs.ma A/defs.ma
+ex1/props.ma arity/defs.ma ex1/defs.ma leq/props.ma nf2/pr3.ma nf2/props.ma pc3/fwd.ma ty3/fwd.ma
+ex1/defs.ma C/defs.ma
+ex0/props.ma aplus/props.ma ex0/defs.ma leq/defs.ma
+ex0/defs.ma A/defs.ma G/defs.ma
+csubst1/props.ma csubst1/defs.ma subst1/defs.ma
+csubst1/defs.ma csubst0/defs.ma
+csubst1/fwd.ma csubst0/fwd.ma csubst1/defs.ma subst1/props.ma
+csubst1/getl.ma csubst0/getl.ma csubst0/props.ma csubst1/props.ma drop/props.ma subst1/props.ma
+theory.ma
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/defs".
+
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/fwd".
+
include "drop/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/props".
+
include "drop/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/defs".
+
include "drop/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/getl".
+
include "drop1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/props".
+
include "drop1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex0/defs".
+
include "A/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex0/props".
+
include "ex0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/defs".
+
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/props".
+
include "ex1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex2/defs".
+
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex2/props".
+
include "ex2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/flt/defs".
+
include "C/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/flt/props".
+
include "flt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs".
+
include "csubst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd".
+
include "fsubst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/clear".
+
include "getl/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/dec".
+
include "getl/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/defs".
+
include "drop/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/drop".
+
include "getl/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/flt".
+
include "getl/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/fwd".
+
include "getl/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/getl".
+
include "getl/drop.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/props".
+
include "getl/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/defs".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/fwd".
+
include "iso/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/props".
+
include "iso/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/asucc".
+
include "leq/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/defs".
+
include "aplus/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/fwd".
+
include "leq/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/props".
+
include "leq/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/defs".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/fwd".
+
include "lift/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/props".
+
include "tlist/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/tlt".
+
include "lift/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/defs".
+
include "lift/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd".
+
include "lift1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/props".
+
include "lift1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/defs".
+
include "A/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/props".
+
include "llt/defs.ma".
+++ /dev/null
-H=@
-
-RT_BASEDIR=../../../
-OPTIONS=-bench -onepass -system
-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: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
-clean: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
-cleanall: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
-
-all.opt opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
-clean.opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
-cleanall.opt: 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)
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs".
+
include "G/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/props".
+
include "next_plus/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/arity".
+
include "nf2/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/dec".
+
include "nf2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/defs".
+
include "pr2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd".
+
include "nf2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/iso".
+
include "nf2/pr3.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1".
+
include "nf2/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3".
+
include "nf2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/props".
+
include "nf2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/defs".
+
include "pr1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/props".
+
include "pc1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/dec".
+
include "ty3/arity_props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs".
+
include "pr3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0".
+
include "pc3/left.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd".
+
include "pc3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/left".
+
include "pc3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2".
+
include "pc3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1".
+
include "pc3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props".
+
include "pc3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1".
+
include "pc3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0".
+
include "pc3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/dec".
+
include "pr0/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/defs".
+
include "subst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd".
+
include "pr0/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0".
+
include "pr0/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/props".
+
include "pr0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1".
+
include "pr0/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/defs".
+
include "pr0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1".
+
include "pr1/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/props".
+
include "pr1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/clen".
+
include "pr2/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/defs".
+
include "pr0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd".
+
include "pr2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2".
+
include "pr2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/props".
+
include "pr2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1".
+
include "pr2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/defs".
+
include "pr2/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd".
+
include "pr3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/iso".
+
include "pr3/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1".
+
include "pr3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3".
+
include "pr3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/props".
+
include "pr3/pr1.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1".
+
include "pr3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0".
+
include "pr3/props.ma".
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/preamble".
-
-include "../Base-1/theory.ma".
-
-alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con".
-alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con".
-alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)".
-alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con".
-alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
-alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
-alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con".
-alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con".
-alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
-alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
-alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
-alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con".
-alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con".
-alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
-alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
-alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con".
-alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
-alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con".
-alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con".
-alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
-alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con".
-alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con".
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+
+
+include "theory.ma".
+
+alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con".
+alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con".
+alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)".
+alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con".
+alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
+alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
+alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con".
+alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con".
+alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
+alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
+alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
+alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con".
+alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con".
+alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
+alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
+alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con".
+alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
+alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con".
+alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con".
+alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
+alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con".
+alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/r/defs".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/r/props".
+
include "r/defs.ma".
--- /dev/null
+baseuri=cic:/matita/LAMBDA-TYPES/LambdaDelta-1
+include_paths= ../Base-1
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/defs".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/props".
+
include "s/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/arity".
+
include "csubc/arity.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/defs".
+
include "sn3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/props".
+
include "sc3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/defs".
+
include "pr3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd".
+
include "sn3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1".
+
include "sn3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2".
+
include "sn3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/props".
+
include "sn3/nf2.ma".
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/spare".
-
-include "theory.ma".
-
-inductive sort: T \to Prop \def
-| sort_sort: \forall (n: nat).(sort (TSort n))
-| sort_abst: \forall (u: T).((sort u) \to (\forall (t: T).((sort t) \to (sort
-(THead (Bind Abst) u t))))).
-
-theorem sort_nf2:
- \forall (t: T).((sort t) \to (\forall (c: C).(nf2 c t)))
-\def
- \lambda (t: T).(\lambda (H: (sort t)).(sort_ind (\lambda (t0: T).(\forall
-(c: C).(nf2 c t0))) (\lambda (n: nat).(\lambda (c: C).(nf2_sort c n)))
-(\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1: ((\forall (c: C).(nf2 c
-u)))).(\lambda (t0: T).(\lambda (_: (sort t0)).(\lambda (H3: ((\forall (c:
-C).(nf2 c t0)))).(\lambda (c: C).(let H_y \def (H3 (CHead c (Bind Abst) u))
-in (nf2_abst_shift c u (H1 c) t0 H_y))))))))) t H)).
-
-theorem sort_pc3:
- \forall (t1: T).((sort t1) \to (\forall (t2: T).((sort t2) \to (\forall (c:
-C).((pc3 c t1 t2) \to (eq T t1 t2))))))
-\def
- \lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda (t: T).(\forall
-(t2: T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t t2))))))
-(\lambda (n: nat).(\lambda (t2: T).(\lambda (H0: (sort t2)).(sort_ind
-(\lambda (t: T).(\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n)
-t)))) (\lambda (n0: nat).(\lambda (c: C).(\lambda (H1: (pc3 c (TSort n)
-(TSort n0))).(eq_ind nat n (\lambda (n1: nat).(eq T (TSort n) (TSort n1)))
-(refl_equal T (TSort n)) n0 (pc3_gen_sort c n n0 H1))))) (\lambda (u:
-T).(\lambda (_: (sort u)).(\lambda (_: ((\forall (c: C).((pc3 c (TSort n) u)
-\to (eq T (TSort n) u))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda
-(_: ((\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n) t))))).(\lambda
-(c: C).(\lambda (H5: (pc3 c (TSort n) (THead (Bind Abst) u
-t))).(pc3_gen_sort_abst c u t n H5 (eq T (TSort n) (THead (Bind Abst) u
-t))))))))))) t2 H0)))) (\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1:
-((\forall (t2: T).((sort t2) \to (\forall (c: C).((pc3 c u t2) \to (eq T u
-t2))))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3: ((\forall (t2:
-T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t
-t2))))))).(\lambda (t2: T).(\lambda (H4: (sort t2)).(sort_ind (\lambda (t0:
-T).(\forall (c: C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind
-Abst) u t) t0)))) (\lambda (n: nat).(\lambda (c: C).(\lambda (H5: (pc3 c
-(THead (Bind Abst) u t) (TSort n))).(pc3_gen_sort_abst c u t n (pc3_s c
-(TSort n) (THead (Bind Abst) u t) H5) (eq T (THead (Bind Abst) u t) (TSort
-n)))))) (\lambda (u0: T).(\lambda (H5: (sort u0)).(\lambda (_: ((\forall (c:
-C).((pc3 c (THead (Bind Abst) u t) u0) \to (eq T (THead (Bind Abst) u t)
-u0))))).(\lambda (t0: T).(\lambda (H7: (sort t0)).(\lambda (_: ((\forall (c:
-C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind Abst) u t)
-t0))))).(\lambda (c: C).(\lambda (H9: (pc3 c (THead (Bind Abst) u t) (THead
-(Bind Abst) u0 t0))).(and_ind (pc3 c u u0) (\forall (b: B).(\forall (u1:
-T).(pc3 (CHead c (Bind b) u1) t t0))) (eq T (THead (Bind Abst) u t) (THead
-(Bind Abst) u0 t0)) (\lambda (H10: (pc3 c u u0)).(\lambda (H11: ((\forall (b:
-B).(\forall (u1: T).(pc3 (CHead c (Bind b) u1) t t0))))).(let H_y \def (H11
-Abbr u) in (let H_y0 \def (H1 u0 H5 c H10) in (let H_y1 \def (H3 t0 H7 (CHead
-c (Bind Abbr) u) H_y) in (let H12 \def (eq_ind_r T t0 (\lambda (t3: T).(pc3
-(CHead c (Bind Abbr) u) t t3)) H_y t H_y1) in (let H13 \def (eq_ind_r T t0
-(\lambda (t3: T).(sort t3)) H7 t H_y1) in (eq_ind T t (\lambda (t3: T).(eq T
-(THead (Bind Abst) u t) (THead (Bind Abst) u0 t3))) (let H14 \def (eq_ind_r T
-u0 (\lambda (t3: T).(pc3 c u t3)) H10 u H_y0) in (let H15 \def (eq_ind_r T u0
-(\lambda (t3: T).(sort t3)) H5 u H_y0) in (eq_ind T u (\lambda (t3: T).(eq T
-(THead (Bind Abst) u t) (THead (Bind Abst) t3 t))) (refl_equal T (THead (Bind
-Abst) u t)) u0 H_y0))) t0 H_y1)))))))) (pc3_gen_abst c u u0 t t0 H9))))))))))
-t2 H4))))))))) t1 H)).
-
-theorem sort_correct:
- \forall (g: G).(\forall (t1: T).((sort t1) \to (\forall (c: C).(ex3 T
-(\lambda (t2: T).(tau0 g c t1 t2)) (\lambda (t2: T).(ty3 g c t1 t2)) (\lambda
-(t2: T).(sort t2))))))
-\def
- \lambda (g: G).(\lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda
-(t: T).(\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2:
-T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2))))) (\lambda (n: nat).(\lambda
-(c: C).(ex3_intro T (\lambda (t2: T).(tau0 g c (TSort n) t2)) (\lambda (t2:
-T).(ty3 g c (TSort n) t2)) (\lambda (t2: T).(sort t2)) (TSort (next g n))
-(tau0_sort g c n) (ty3_sort g c n) (sort_sort (next g n))))) (\lambda (u:
-T).(\lambda (H0: (sort u)).(\lambda (H1: ((\forall (c: C).(ex3 T (\lambda
-(t2: T).(tau0 g c u t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2:
-T).(sort t2)))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3:
-((\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2:
-T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2)))))).(\lambda (c: C).(let H_x
-\def (H1 c) in (let H4 \def H_x in (ex3_ind T (\lambda (t2: T).(tau0 g c u
-t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2: T).(sort t2)) (ex3 T
-(\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(ty3
-g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) (\lambda (x0:
-T).(\lambda (_: (tau0 g c u x0)).(\lambda (H6: (ty3 g c u x0)).(\lambda (_:
-(sort x0)).(let H_x0 \def (H3 (CHead c (Bind Abst) u)) in (let H8 \def H_x0
-in (ex3_ind T (\lambda (t2: T).(tau0 g (CHead c (Bind Abst) u) t t2))
-(\lambda (t2: T).(ty3 g (CHead c (Bind Abst) u) t t2)) (\lambda (t2: T).(sort
-t2)) (ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda
-(t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2)))
-(\lambda (x1: T).(\lambda (H9: (tau0 g (CHead c (Bind Abst) u) t
-x1)).(\lambda (H10: (ty3 g (CHead c (Bind Abst) u) t x1)).(\lambda (H11:
-(sort x1)).(ex_ind T (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) u) x1 t0))
-(ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2:
-T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2)))
-(\lambda (x: T).(\lambda (H12: (ty3 g (CHead c (Bind Abst) u) x1
-x)).(ex3_intro T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2))
-(\lambda (t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort
-t2)) (THead (Bind Abst) u x1) (tau0_bind g Abst c u t x1 H9) (ty3_bind g c u
-x0 H6 Abst t x1 H10 x H12) (sort_abst u H0 x1 H11)))) (ty3_correct g (CHead c
-(Bind Abst) u) t x1 H10)))))) H8))))))) H4)))))))))) t1 H))).
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+
+
+include "theory.ma".
+
+inductive sort: T \to Prop \def
+| sort_sort: \forall (n: nat).(sort (TSort n))
+| sort_abst: \forall (u: T).((sort u) \to (\forall (t: T).((sort t) \to (sort
+(THead (Bind Abst) u t))))).
+
+theorem sort_nf2:
+ \forall (t: T).((sort t) \to (\forall (c: C).(nf2 c t)))
+\def
+ \lambda (t: T).(\lambda (H: (sort t)).(sort_ind (\lambda (t0: T).(\forall
+(c: C).(nf2 c t0))) (\lambda (n: nat).(\lambda (c: C).(nf2_sort c n)))
+(\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1: ((\forall (c: C).(nf2 c
+u)))).(\lambda (t0: T).(\lambda (_: (sort t0)).(\lambda (H3: ((\forall (c:
+C).(nf2 c t0)))).(\lambda (c: C).(let H_y \def (H3 (CHead c (Bind Abst) u))
+in (nf2_abst_shift c u (H1 c) t0 H_y))))))))) t H)).
+
+theorem sort_pc3:
+ \forall (t1: T).((sort t1) \to (\forall (t2: T).((sort t2) \to (\forall (c:
+C).((pc3 c t1 t2) \to (eq T t1 t2))))))
+\def
+ \lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda (t: T).(\forall
+(t2: T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t t2))))))
+(\lambda (n: nat).(\lambda (t2: T).(\lambda (H0: (sort t2)).(sort_ind
+(\lambda (t: T).(\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n)
+t)))) (\lambda (n0: nat).(\lambda (c: C).(\lambda (H1: (pc3 c (TSort n)
+(TSort n0))).(eq_ind nat n (\lambda (n1: nat).(eq T (TSort n) (TSort n1)))
+(refl_equal T (TSort n)) n0 (pc3_gen_sort c n n0 H1))))) (\lambda (u:
+T).(\lambda (_: (sort u)).(\lambda (_: ((\forall (c: C).((pc3 c (TSort n) u)
+\to (eq T (TSort n) u))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda
+(_: ((\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n) t))))).(\lambda
+(c: C).(\lambda (H5: (pc3 c (TSort n) (THead (Bind Abst) u
+t))).(pc3_gen_sort_abst c u t n H5 (eq T (TSort n) (THead (Bind Abst) u
+t))))))))))) t2 H0)))) (\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1:
+((\forall (t2: T).((sort t2) \to (\forall (c: C).((pc3 c u t2) \to (eq T u
+t2))))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3: ((\forall (t2:
+T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t
+t2))))))).(\lambda (t2: T).(\lambda (H4: (sort t2)).(sort_ind (\lambda (t0:
+T).(\forall (c: C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind
+Abst) u t) t0)))) (\lambda (n: nat).(\lambda (c: C).(\lambda (H5: (pc3 c
+(THead (Bind Abst) u t) (TSort n))).(pc3_gen_sort_abst c u t n (pc3_s c
+(TSort n) (THead (Bind Abst) u t) H5) (eq T (THead (Bind Abst) u t) (TSort
+n)))))) (\lambda (u0: T).(\lambda (H5: (sort u0)).(\lambda (_: ((\forall (c:
+C).((pc3 c (THead (Bind Abst) u t) u0) \to (eq T (THead (Bind Abst) u t)
+u0))))).(\lambda (t0: T).(\lambda (H7: (sort t0)).(\lambda (_: ((\forall (c:
+C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind Abst) u t)
+t0))))).(\lambda (c: C).(\lambda (H9: (pc3 c (THead (Bind Abst) u t) (THead
+(Bind Abst) u0 t0))).(and_ind (pc3 c u u0) (\forall (b: B).(\forall (u1:
+T).(pc3 (CHead c (Bind b) u1) t t0))) (eq T (THead (Bind Abst) u t) (THead
+(Bind Abst) u0 t0)) (\lambda (H10: (pc3 c u u0)).(\lambda (H11: ((\forall (b:
+B).(\forall (u1: T).(pc3 (CHead c (Bind b) u1) t t0))))).(let H_y \def (H11
+Abbr u) in (let H_y0 \def (H1 u0 H5 c H10) in (let H_y1 \def (H3 t0 H7 (CHead
+c (Bind Abbr) u) H_y) in (let H12 \def (eq_ind_r T t0 (\lambda (t3: T).(pc3
+(CHead c (Bind Abbr) u) t t3)) H_y t H_y1) in (let H13 \def (eq_ind_r T t0
+(\lambda (t3: T).(sort t3)) H7 t H_y1) in (eq_ind T t (\lambda (t3: T).(eq T
+(THead (Bind Abst) u t) (THead (Bind Abst) u0 t3))) (let H14 \def (eq_ind_r T
+u0 (\lambda (t3: T).(pc3 c u t3)) H10 u H_y0) in (let H15 \def (eq_ind_r T u0
+(\lambda (t3: T).(sort t3)) H5 u H_y0) in (eq_ind T u (\lambda (t3: T).(eq T
+(THead (Bind Abst) u t) (THead (Bind Abst) t3 t))) (refl_equal T (THead (Bind
+Abst) u t)) u0 H_y0))) t0 H_y1)))))))) (pc3_gen_abst c u u0 t t0 H9))))))))))
+t2 H4))))))))) t1 H)).
+
+theorem sort_correct:
+ \forall (g: G).(\forall (t1: T).((sort t1) \to (\forall (c: C).(ex3 T
+(\lambda (t2: T).(tau0 g c t1 t2)) (\lambda (t2: T).(ty3 g c t1 t2)) (\lambda
+(t2: T).(sort t2))))))
+\def
+ \lambda (g: G).(\lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda
+(t: T).(\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2:
+T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2))))) (\lambda (n: nat).(\lambda
+(c: C).(ex3_intro T (\lambda (t2: T).(tau0 g c (TSort n) t2)) (\lambda (t2:
+T).(ty3 g c (TSort n) t2)) (\lambda (t2: T).(sort t2)) (TSort (next g n))
+(tau0_sort g c n) (ty3_sort g c n) (sort_sort (next g n))))) (\lambda (u:
+T).(\lambda (H0: (sort u)).(\lambda (H1: ((\forall (c: C).(ex3 T (\lambda
+(t2: T).(tau0 g c u t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2:
+T).(sort t2)))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3:
+((\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2:
+T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2)))))).(\lambda (c: C).(let H_x
+\def (H1 c) in (let H4 \def H_x in (ex3_ind T (\lambda (t2: T).(tau0 g c u
+t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2: T).(sort t2)) (ex3 T
+(\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(ty3
+g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) (\lambda (x0:
+T).(\lambda (_: (tau0 g c u x0)).(\lambda (H6: (ty3 g c u x0)).(\lambda (_:
+(sort x0)).(let H_x0 \def (H3 (CHead c (Bind Abst) u)) in (let H8 \def H_x0
+in (ex3_ind T (\lambda (t2: T).(tau0 g (CHead c (Bind Abst) u) t t2))
+(\lambda (t2: T).(ty3 g (CHead c (Bind Abst) u) t t2)) (\lambda (t2: T).(sort
+t2)) (ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda
+(t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2)))
+(\lambda (x1: T).(\lambda (H9: (tau0 g (CHead c (Bind Abst) u) t
+x1)).(\lambda (H10: (ty3 g (CHead c (Bind Abst) u) t x1)).(\lambda (H11:
+(sort x1)).(ex_ind T (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) u) x1 t0))
+(ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2:
+T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2)))
+(\lambda (x: T).(\lambda (H12: (ty3 g (CHead c (Bind Abst) u) x1
+x)).(ex3_intro T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2))
+(\lambda (t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort
+t2)) (THead (Bind Abst) u x1) (tau0_bind g Abst c u t x1 H9) (ty3_bind g c u
+x0 H6 Abst t x1 H10 x H12) (sort_abst u H0 x1 H11)))) (ty3_correct g (CHead c
+(Bind Abst) u) t x1 H10)))))) H8))))))) H4)))))))))) t1 H))).
+
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/dec".
+
include "subst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/defs".
+
include "lift/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd".
+
include "subst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/props".
+
include "subst0/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0".
+
include "subst0/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt".
+
include "subst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/defs".
+
include "subst0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd".
+
include "subst1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/props".
+
include "subst1/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1".
+
include "subst1/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau0/defs".
+
include "G/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau0/props".
+
include "tau0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt".
+
include "tau1/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/defs".
+
include "tau0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/props".
+
include "tau1/defs.ma".
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/theory".
-
-include "subst0/tlt.ma".
-
-include "tau1/cnt.ma".
-
-include "ex0/props.ma".
-
-include "wcpr0/fwd.ma".
-
-include "pr3/wcpr0.ma".
-
-include "ex2/props.ma".
-
-include "ex1/props.ma".
-
-include "ty3/tau0.ma".
-
-include "ty3/nf2.ma".
-
-include "ty3/dec.ma".
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+
+
+include "subst0/tlt.ma".
+
+include "tau1/cnt.ma".
+
+include "ex0/props.ma".
+
+include "wcpr0/fwd.ma".
+
+include "pr3/wcpr0.ma".
+
+include "ex2/props.ma".
+
+include "ex1/props.ma".
+
+include "ty3/tau0.ma".
+
+include "ty3/nf2.ma".
+
+include "ty3/dec.ma".
+
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/defs".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/props".
+
include "tlist/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlt/defs".
+
include "T/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlt/props".
+
include "tlt/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity".
+
include "ty3/pr3_props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props".
+
include "ty3/arity.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/dec".
+
include "ty3/pr3_props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs".
+
include "G/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0".
+
include "ty3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd".
+
include "ty3/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2".
+
include "ty3/arity.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3".
+
include "csubt/ty3.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props".
+
include "ty3/pr3.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/props".
+
include "ty3/fwd.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1".
+
include "ty3/props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0".
+
include "ty3/pr3_props.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs".
+
include "pr0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd".
+
include "wcpr0/defs.ma".
(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl".
+
include "wcpr0/defs.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
+
(* LIFT RELATION
- Usage: invoke with positive polarity
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fun".
+
include "Lift/inv.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/inv".
+
include "Lift/defs.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
+
include "Lift/fun.ma".
--- /dev/null
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+ ../../../matitac
+$(DIR).opt opt all.opt:
+ ../../../matitac.opt
+clean:
+ ../../../matitaclean
+clean.opt:
+ ../../../matitaclean.opt
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Context".
+
(* FLAT CONTEXTS
- Naming policy:
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term".
+
(* POLARIZED TERMS
- Naming policy:
- terms : t u
*)
-include "preamble.ma".
+include "preamble4.ma".
inductive Bind: Type \def
| abbr: Bind
--- /dev/null
+preamble4.ma NLE/nplus.ma NLE/props.ma NPlus/monoid.ma datatypes/Bool.ma logic/equality.ma
+datatypes/Context.ma datatypes/Term.ma
+datatypes/Term.ma preamble4.ma
+Lift/props.ma Lift/fun.ma
+Lift/inv.ma Lift/defs.ma
+Lift/defs.ma datatypes/Term.ma
+Lift/fun.ma Lift/inv.ma
+NLE/nplus.ma
+NLE/props.ma
+NPlus/monoid.ma
+datatypes/Bool.ma
+logic/equality.ma
+++ /dev/null
-H=@
-
-RT_BASEDIR=../../../
-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: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
-clean: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
-cleanall: preall
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
-
-all.opt opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
-clean.opt: preall.opt
- $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
-cleanall.opt: 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)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* Project started Tue Aug 22, 2006 ***************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/preamble".
-
-(* PREAMBLE
-*)
-
-include "logic/equality.ma".
-include "../../RELATIONAL/datatypes/Bool.ma".
-include "../../RELATIONAL/NPlus/monoid.ma".
-include "../../RELATIONAL/NLE/props.ma".
-include "../../RELATIONAL/NLE/nplus.ma".
-
-axiom f_equal_3: \forall (A,B,C,D:Set).
- \forall (f:A \to B \to C \to D).
- \forall (x1,x2:A).
- \forall (y1,y2:B).
- \forall (z1,z2:C).
- x1 = x2 \to y1 = y2 \to z1 = z2 \to
- f x1 y1 z1 = f x2 y2 z2.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* Project started Tue Aug 22, 2006 ***************************************)
+
+
+
+(* PREAMBLE
+*)
+
+include "logic/equality.ma".
+include "datatypes/Bool.ma".
+include "NPlus/monoid.ma".
+include "NLE/props.ma".
+include "NLE/nplus.ma".
+
+axiom f_equal_3: \forall (A,B,C,D:Set).
+ \forall (f:A \to B \to C \to D).
+ \forall (x1,x2:A).
+ \forall (y1,y2:B).
+ \forall (z1,z2:C).
+ x1 = x2 \to y1 = y2 \to z1 = z2 \to
+ f x1 y1 z1 = f x2 y2 z2.
--- /dev/null
+baseuri=cic:/matita/LAMBDA-TYPES/Unified-Sub
+include_paths= ../../RELATIONAL/
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/test/prova".
-
-include "../legacy/coq.ma".
-
-theorem pippo: \forall (A,B:Prop). A \land B \to A.
- intros; decompose; assumption.
-qed.
-
-inline procedural "cic:/matita/test/prova/pippo.con".
-
-alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
-theorem plus_comm: \forall n:nat.\forall m:nat.eq nat (plus n m) (plus m n).
- intros; alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
-apply plus_comm.
-qed.
-(*
-include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma".
-alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)".
-alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con".
-alias id "THead" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1/3)".
-alias id "T" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1)".
-alias id "G" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G.ind#xpointer(1/1)".
-alias id "Flat" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1/2)".
-alias id "Cast" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1/2)".
-alias id "C" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C.ind#xpointer(1/1)".
-theorem ty3_gen_cast:
- (\forall g:G
- .\forall c:C
- .\forall t1:T
- .\forall t2:T
- .\forall x:T
- .ty3 g c (THead (Flat Cast) t2 t1) x
- \rarr pc3 c t2 x\land ty3 g c t1 t2)
-.
-(* tactics: 80 *)
-intros 6 (g c t1 t2 x H).
-apply insert_eq;(* 6 P P P C I I 3 0 *)
-[apply T(* dependent *)
-|apply (THead (Flat Cast) t2 t1)(* dependent *)
-|apply (\lambda t:T.ty3 g c t x)(* dependent *)
-|intros 2 (y H0).
-alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.con".
-elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *)
-[intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6).
-letin H7 \def (f_equal T T (\lambda e:T.e) u (THead (Flat Cast) t2 t1) H6).(* 6 C C C C C I *)
-rewrite > H7 in H4:(%) as (H8).
-cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10;
-[id
-|apply H8.(* 1 I *)
-apply refl_equal(* 2 C C *)
-].
-elim H10 using and_ind names 0.(* 5 P P C I I 3 0 *)
-intros 2 (H11 H12).
-apply conj;(* 4 C C I I *)
-[alias id "pc3_t" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_t.con".
-apply pc3_t;(* 6 P C C I C I *)
-[apply t3(* dependent *)
-|apply H11(* assumption *)
-|apply H5(* assumption *)
-]
-|apply H12(* assumption *)
-]
-|intros 3 (c0 m H1).
-alias id "K" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1)".
-cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr True
-|TLRef (_:nat)\rArr False
-|THead (_:K) (_:T) (_:T)\rArr False] as H2;
-[id
-|rewrite < H1 in \vdash (%).
-apply I
-].
-clearbody H2.
-change in H2:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr True
-|TLRef (_:nat)\rArr False
-|THead (_:K) (_:T) (_:T)\rArr False].
-elim H2 using False_ind names 0(* 2 C I 2 0 *)
-|intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
-cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr False
-|TLRef (_:nat)\rArr True
-|THead (_:K) (_:T) (_:T)\rArr False] as H5;
-[id
-|rewrite < H4 in \vdash (%).
-apply I
-].
-clearbody H5.
-change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr False
-|TLRef (_:nat)\rArr True
-|THead (_:K) (_:T) (_:T)\rArr False].
-elim H5 using False_ind names 0(* 2 C I 2 0 *)
-|intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
-cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr False
-|TLRef (_:nat)\rArr True
-|THead (_:K) (_:T) (_:T)\rArr False] as H5;
-[id
-|rewrite < H4 in \vdash (%).
-apply I
-].
-clearbody H5.
-change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr False
-|TLRef (_:nat)\rArr True
-|THead (_:K) (_:T) (_:T)\rArr False].
-elim H5 using False_ind names 0(* 2 C I 2 0 *)
-|intros 14 (c0 u t UNUSED UNUSED b t0 t3 UNUSED UNUSED t4 UNUSED UNUSED H7).
-alias id "F" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1)".
-alias id "B" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B.ind#xpointer(1/1)".
-cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr False
-|TLRef (_:nat)\rArr False
-|THead (k:K) (_:T) (_:T)\rArr
- match k in K return \lambda _:K.Prop with
- [Bind (_:B)\rArr True|Flat (_:F)\rArr False]] as H8;
-[id
-|rewrite < H7 in \vdash (%).
-apply I
-].
-clearbody H8.
-change in H8:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr False
-|TLRef (_:nat)\rArr False
-|THead (k:K) (_:T) (_:T)\rArr
- match k in K return \lambda _:K.Prop with
- [Bind (_:B)\rArr True|Flat (_:F)\rArr False]].
-elim H8 using False_ind names 0(* 2 C I 2 0 *)
-|intros 10 (c0 w u UNUSED UNUSED v t UNUSED UNUSED H5).
-cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr False
-|TLRef (_:nat)\rArr False
-|THead (k:K) (_:T) (_:T)\rArr
- match k in K return \lambda _:K.Prop with
- [Bind (_:B)\rArr False
- |Flat (f:F)\rArr
- match f in F return \lambda _:F.Prop with
- [Appl\rArr True|Cast\rArr False]]] as H6;
-[id
-|rewrite < H5 in \vdash (%).
-apply I
-].
-clearbody H6.
-change in H6:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
-[TSort (_:nat)\rArr False
-|TLRef (_:nat)\rArr False
-|THead (k:K) (_:T) (_:T)\rArr
- match k in K return \lambda _:K.Prop with
- [Bind (_:B)\rArr False
- |Flat (f:F)\rArr
- match f in F return \lambda _:F.Prop with
- [Appl\rArr True|Cast\rArr False]]].
-elim H6 using False_ind names 0(* 2 C I 2 0 *)
-|intros 9 (c0 t0 t3 H1 H2 t4 UNUSED UNUSED H5).
-letin H6 \def (f_equal T T
- (\lambda e:T
- .match e in T return \lambda _:T.T with
- [TSort (_:nat)\rArr t3
- |TLRef (_:nat)\rArr t3
- |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0)
- (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
-letin H7 \def (f_equal T T
- (\lambda e:T
- .match e in T return \lambda _:T.T with
- [TSort (_:nat)\rArr t0
- |TLRef (_:nat)\rArr t0
- |THead (_:K) (_:T) (t:T)\rArr t]) (THead (Flat Cast) t3 t0)
- (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
-cut (t3=t2\rarr pc3 c0 t2 t3\land ty3 g c0 t1 t2) as DEFINED;
-[id
-|intros 1 (H8).
-rewrite > H8 in H2:(%) as (UNUSED).
-rewrite > H8 in H1:(%) as (H12).
-rewrite > H8 in \vdash (%).
-clearbody H7.
-change in H7:(%) with (match THead (Flat Cast) t3 t0 in T return \lambda _:T.T with
- [TSort (_:nat)\rArr t0
- |TLRef (_:nat)\rArr t0
- |THead (_:K) (_:T) (t:T)\rArr t]
- =match THead (Flat Cast) t2 t1 in T return \lambda _:T.T with
- [TSort (_:nat)\rArr t0
- |TLRef (_:nat)\rArr t0
- |THead (_:K) (_:T) (t:T)\rArr t]).
-rewrite > H7 in H12:(%) as (H14).
-apply conj;(* 4 C C I I *)
-[alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con".
-apply pc3_refl(* 2 C C *)
-|apply H14(* assumption *)
-]
-].
-apply DEFINED.(* 1 I *)
-apply H6(* assumption *)
-]
-|apply H(* assumption *)
-].
-qed.
-*)
-(*
-include "nat/orders.ma".
-
-theorem le_inv:
- \forall P:nat \to Prop
- .\forall p2
- .\forall p1
- .p2 <= p1 \to
- (p1 = p2 \to P p2) \to
- (\forall n1
- .p2 <= n1 \to
- (p1 = n1 \to P n1) \to
- p1 = S n1 \to P (S n1)) \to
- P p1.
- intros 4; elim H names 0; clear H p1; intros;
- [ apply H; reflexivity
- | apply H3; clear H3; intros;
- [ apply H | apply H1; clear H1; intros; subst;
- [ apply H2; apply H3 | ]
- | reflexivity
- ]
-*)
projects / helm.git / commitdiff