-theory.ma: theory.mma ext/tactics.ma ext/arith.ma types/props.ma blt/props.ma plist/props.ma
-ext/tactics.ma: ext/tactics.mma preamble.ma
-ext/arith.ma: ext/arith.mma preamble.ma
-types/defs.ma: types/defs.mma preamble.ma
-types/props.ma: types/props.mma types/defs.ma
-blt/defs.ma: blt/defs.mma preamble.ma
-blt/props.ma: blt/props.mma blt/defs.ma
-plist/defs.ma: plist/defs.mma preamble.ma
-plist/props.ma: plist/props.mma plist/defs.ma
+Base-2/theory.ma: Base-2/theory.mma Base-2/ext/tactics.ma Base-2/ext/arith.ma Base-2/types/props.ma Base-2/blt/props.ma Base-2/plist/props.ma
+Base-2/ext/tactics.ma: Base-2/ext/tactics.mma Base-2/preamble.ma
+Base-2/ext/arith.ma: Base-2/ext/arith.mma Base-2/preamble.ma
+Base-2/types/defs.ma: Base-2/types/defs.mma Base-2/preamble.ma
+Base-2/types/props.ma: Base-2/types/props.mma Base-2/types/defs.ma
+Base-2/blt/defs.ma: Base-2/blt/defs.mma Base-2/preamble.ma
+Base-2/blt/props.ma: Base-2/blt/props.mma Base-2/blt/defs.ma
+Base-2/plist/defs.ma: Base-2/plist/defs.mma Base-2/preamble.ma
+Base-2/plist/props.ma: Base-2/plist/props.mma Base-2/plist/defs.ma
+++ /dev/null
-DIR=$(shell basename $$PWD)
-
-MMAS = $(shell find -name "*.mma")
-MAS = $(MMAS:%.mma=%.ma)
-
-%.ma: %.mma
- ../../../matitac.opt -dump $@ $< 2>/dev/null
- $(MAKE) depend.opt
- ../../../matitac.opt $@
-
-$(DIR) all: $(MAS)
- ../../../matitac
-$(DIR).opt opt all.opt: $(MAS)
- ../../../matitac.opt
-clean:
- ../../../matitaclean
- rm -f $(MAS)
- $(MAKE) depend
-clean.opt:
- ../../../matitaclean.opt
- rm -f $(MAS)
- $(MAKE) depend.opt
-depend:
- ../../../matitadep
- cat depends_mma >> depends
-depend.opt:
- ../../../matitadep.opt
- cat depends_mma >> depends
-
-include .depend
-theory.mma preamble.ma
-ext/tactics.mma preamble.ma
-ext/arith.mma preamble.ma
-types/defs.mma preamble.ma
-types/props.mma preamble.ma
-blt/defs.mma preamble.ma
-blt/props.mma preamble.ma
-plist/defs.mma preamble.ma
-plist/props.mma preamble.ma
+Base-2/theory.mma Base-2/preamble.ma Base-1/theory.ma
+Base-2/ext/tactics.mma Base-2/preamble.ma Base-1/ext/tactics.ma
+Base-2/ext/arith.mma Base-2/preamble.ma Base-1/ext/arith.ma
+Base-2/types/defs.mma Base-2/preamble.ma Base-1/types/defs.ma
+Base-2/types/props.mma Base-2/preamble.ma Base-1/types/props.ma
+Base-2/blt/defs.mma Base-2/preamble.ma Base-1/blt/defs.ma
+Base-2/blt/props.mma Base-2/preamble.ma Base-1/blt/props.ma
+Base-2/plist/defs.mma Base-2/preamble.ma Base-1/plist/defs.ma
+Base-2/plist/props.mma Base-2/preamble.ma Base-1/plist/props.ma
+++ /dev/null
-\e[0;32mInfo: \e[0mexecution of blt/defs.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of blt/defs.mma completed in 1''.
-\e[0;32mInfo: \e[0mexecution of blt/props.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt ...''
-\e[0;32mInfo: \e[0mbaseuri cic:/matita/LAMBDA-TYPES/Base-2/blt/props is not empty
-\e[0;32mInfo: \e[0mcleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/blt/props
-\e[0;32mInfo: \e[0mRemoving: cic:/matita/LAMBDA-TYPES/Base-2/blt/props/*
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs" ...''
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_blt
-Pre Nodes : 257
-nat
-nat
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: nested application
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq bool (blt y n) true)))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq bool (blt y O) true))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H0) in (False_ind (eq bool (blt y O) true) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq bool (blt y O) true)).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq bool (blt y O) true)) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq bool (blt y n) true))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq bool (blt n0 (S n)) true))) (\lambda _:(lt O (S n)).(refl_equal bool true)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq bool
-match n0 return (\lambda n1:nat.bool) with
- [ O => true
- | (S (m:nat)) => (blt m n)
-] true)).(\lambda H1:(lt (S n0) (S n)).(H n0 (le_S_n (S n0) n H1))))) y)))) x))
-Post Nodes: 272
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_bge
-Pre Nodes : 255
-nat
-nat
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: nested application
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le n y)\to (eq bool (blt y n) false)))) (\lambda y:nat.(\lambda _:(le O y).(refl_equal bool false))) (\lambda n:nat.(\lambda H:(\forall y:nat.((le n y)\to (eq bool (blt y n) false))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((le (S n) n0)\to (eq bool (blt n0 (S n)) false))) (\lambda H0:(le (S n) O). let H1 \def (le_ind (S n) (\lambda n0:nat.((eq nat n0 O)\to (eq bool (blt O (S n)) false))) (\lambda H1:(eq nat (S n) O). let H2 \def (eq_ind nat (S n) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H1) in (False_ind (eq bool (blt O (S n)) false) H2)) (\lambda m:nat.(\lambda H1:(le (S n) m).(\lambda _:((eq nat m O)\to (eq bool (blt O (S n)) false)).(\lambda H2:(eq nat (S m) O). let H3 \def (eq_ind nat (S m) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H2) in let DEFINED \def (False_ind ((le (S n) m)\to (eq bool (blt O (S n)) false)) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O))) (\lambda n0:nat.(\lambda _:((le (S n) n0)\to (eq bool (blt n0 (S n)) false)).(\lambda H1:(le (S n) (S n0)).(H n0 (le_S_n n n0 H1))))) y)))) x))
-Post Nodes: 272
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: blt_lt
-Pre Nodes : 221
-bool
-bool
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq bool (blt y n) true)\to (lt y n)))) (\lambda y:nat.(\lambda H:(eq bool (blt y O) true). let H0 \def (eq_ind bool (blt y O) (\lambda b:bool.((eq bool b true)\to (lt y O))) (\lambda H0:(eq bool (blt y O) true). let H1 \def (eq_ind bool (blt y O) (\lambda e:bool.
-match e return (\lambda _:bool.Prop) with
- [ true => False
- | false => True
-]) I true H0) in (False_ind (lt y O) H1)) true H) in (H0 (refl_equal bool true)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((eq bool (blt y n) true)\to (lt y n))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((eq bool (blt n0 (S n)) true)\to (lt n0 (S n)))) (\lambda _:(eq bool true true).(le_S_n (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n))))) (\lambda n0:nat.(\lambda _:((eq bool
-match n0 return (\lambda n1:nat.bool) with
- [ O => true
- | (S (m:nat)) => (blt m n)
-] true)\to (lt n0 (S n))).(\lambda H1:(eq bool (blt n0 n) true).(lt_le_S (S n0) (S n) (lt_n_S n0 n (H n0 H1)))))) y)))) x))
-Post Nodes: 219
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: bge_le
-Pre Nodes : 222
-bool
-bool
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq bool (blt y n) false)\to (le n y)))) (\lambda y:nat.(\lambda _:(eq bool (blt y O) false).(le_O_n y))) (\lambda n:nat.(\lambda H:(\forall y:nat.((eq bool (blt y n) false)\to (le n y))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((eq bool (blt n0 (S n)) false)\to (le (S n) n0))) (\lambda H0:(eq bool (blt O (S n)) false). let H1 \def (eq_ind bool (blt O (S n)) (\lambda b:bool.((eq bool b false)\to (le (S n) O))) (\lambda H1:(eq bool (blt O (S n)) false). let H2 \def (eq_ind bool (blt O (S n)) (\lambda e:bool.
-match e return (\lambda _:bool.Prop) with
- [ true => True
- | false => False
-]) I false H1) in (False_ind (le (S n) O) H2)) false H0) in (H1 (refl_equal bool false))) (\lambda n0:nat.(\lambda _:((eq bool (blt n0 (S n)) false)\to (le (S n) n0)).(\lambda H1:(eq bool (blt (S n0) (S n)) false).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0 H1))))))) y)))) x))
-Post Nodes: 220
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of blt/props.mma completed in 7''.
-\e[0;32mInfo: \e[0mexecution of ext/arith.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext ...''
-\e[0;32mInfo: \e[0mbaseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/arith is not empty
-\e[0;32mInfo: \e[0mcleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/arith
-\e[0;32mInfo: \e[0mRemoving: cic:/matita/LAMBDA-TYPES/Base-2/ext/arith/*
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: nat_dec
-Pre Nodes : 474
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda n1:nat.(nat_ind (\lambda n:nat.(\forall n2:nat.(or (eq nat n n2) ((eq nat n n2)\to (\forall P:Prop.P))))) (\lambda n2:nat.(nat_ind (\lambda n:nat.(or (eq nat O n) ((eq nat O n)\to (\forall P:Prop.P)))) (or_introl (eq nat O O) ((eq nat O O)\to (\forall P:Prop.P)) (refl_equal nat O)) (\lambda n3:nat.(\lambda _:(or (eq nat O n3) ((eq nat O n3)\to (\forall P:Prop.P))).(or_intror (eq nat O (S n3)) ((eq nat O (S n3))\to (\forall P:Prop.P)) (\lambda H0:(eq nat O (S n3)).(\lambda P:Prop. let H1 \def (eq_ind nat O (\lambda ee:nat.
-match ee return (\lambda _:nat.Prop) with
- [ O => True
- | (S (_:nat)) => False
-]) I (S n3) H0) in (False_ind P H1)))))) n2)) (\lambda n2:nat.(\lambda H:(\forall n2:nat.(or (eq nat n2 n2) ((eq nat n2 n2)\to (\forall P:Prop.P)))).(\lambda n3:nat.(nat_ind (\lambda n0:nat.(or (eq nat (S n2) n0) ((eq nat (S n2) n0)\to (\forall P:Prop.P)))) (or_intror (eq nat (S n2) O) ((eq nat (S n2) O)\to (\forall P:Prop.P)) (\lambda H0:(eq nat (S n2) O).(\lambda P:Prop. let H1 \def (eq_ind nat (S n2) (\lambda ee:nat.
-match ee return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H0) in (False_ind P H1)))) (\lambda n4:nat.(\lambda H0:(or (eq nat (S n2) n4) ((eq nat (S n2) n4)\to (\forall P:Prop.P))). let DEFINED \def (H n4) in (or_ind (eq nat n2 n4) ((eq nat n2 n4)\to (\forall P:Prop.P)) (or (eq nat (S n2) (S n4)) ((eq nat (S n2) (S n4))\to (\forall P:Prop.P))) (\lambda H1:(eq nat n2 n4).(eq_ind nat n2 (\lambda n3:nat.(or (eq nat (S n2) (S n3)) ((eq nat (S n2) (S n3))\to (\forall P:Prop.P)))) (or_introl (eq nat (S n2) (S n2)) ((eq nat (S n2) (S n2))\to (\forall P:Prop.P)) (refl_equal nat (S n2))) n4 H1)) (\lambda H1:((eq nat n2 n4)\to (\forall P:Prop.P)).(or_intror (eq nat (S n2) (S n4)) ((eq nat (S n2) (S n4))\to (\forall P:Prop.P)) (\lambda H2:(eq nat (S n2) (S n4)).(\lambda P:Prop. let H3 \def (f_equal nat nat (\lambda e:nat.
-match e return (\lambda _:nat.nat) with
- [ O => n2
- | (S (n3:nat)) => n3
-]) (S n2) (S n4) H2) in let H4 \def (eq_ind_r nat n4 (\lambda n3:nat.((eq nat n2 n3)\to (\forall P0:Prop.P0))) H1 n2 H3) in (H4 (refl_equal nat n2) P))))) DEFINED))) n3)))) n1))
-Post Nodes: 476
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: simpl_plus_r
-Pre Nodes : 85
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda n:nat.(\lambda m:nat.(\lambda p:nat.(\lambda H:(eq nat (plus m n) (plus p n)). let DEFINED \def (plus_comm n m) in (plus_reg_l n m p (eq_ind_r nat (plus m n) (\lambda n0:nat.(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda n0:nat.(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_comm n p)) (plus m n) H) (plus n m) DEFINED))))))
-Post Nodes: 87
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: minus_plus_r
-Pre Nodes : 33
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda m:nat.(\lambda n:nat. let DEFINED \def (plus_comm m n) in (eq_ind_r nat (plus n m) (\lambda n0:nat.(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) DEFINED)))
-Post Nodes: 35
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: plus_permute_2_in_3
-Pre Nodes : 117
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda z:nat. let DEFINED \def (plus_assoc_reverse x z y) in let DEFINED0 \def (plus_comm y z) in let DEFINED1 \def (plus_assoc_reverse x y z) in (eq_ind_r nat (plus x (plus y z)) (\lambda n:nat.(eq nat n (plus (plus x z) y))) (eq_ind_r nat (plus z y) (\lambda n:nat.(eq nat (plus x n) (plus (plus x z) y))) (eq_ind nat (plus (plus x z) y) (\lambda n:nat.(eq nat n (plus (plus x z) y))) (refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) DEFINED) (plus y z) DEFINED0) (plus (plus x y) z) DEFINED1))))
-Post Nodes: 123
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: plus_permute_2_in_3_assoc
-Pre Nodes : 86
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda n:nat.(\lambda h:nat.(\lambda k:nat. let DEFINED \def (plus_assoc n k h) in let DEFINED0 \def (plus_permute_2_in_3 n h k) in (eq_ind_r nat (plus (plus n k) h) (\lambda n0:nat.(eq nat n0 (plus n (plus k h)))) (eq_ind_r nat (plus (plus n k) h) (\lambda n0:nat.(eq nat (plus (plus n k) h) n0)) (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) DEFINED) (plus (plus n h) k) DEFINED0))))
-Post Nodes: 90
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: plus_O
-Pre Nodes : 191
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq nat (plus n y) O)\to (and (eq nat n O) (eq nat y O))))) (\lambda y:nat.(\lambda H:(eq nat (plus O y) O).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda n:nat.(\lambda _:(\forall y:nat.((eq nat (plus n y) O)\to (and (eq nat n O) (eq nat y O)))).(\lambda y:nat.(\lambda H0:(eq nat (plus (S n) y) O). let H1 \def (eq_ind nat (plus (S n) y) (\lambda n0:nat.((eq nat n0 O)\to (and (eq nat (S n) O) (eq nat y O)))) (\lambda H1:(eq nat (plus (S n) y) O). let H2 \def (eq_ind nat (plus (S n) y) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H1) in (False_ind (and (eq nat (S n) O) (eq nat y O)) H2)) O H0) in (H1 (refl_equal nat O)))))) x))
-Post Nodes: 189
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: minus_Sx_SO
-Pre Nodes : 24
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat. let DEFINED \def (minus_n_O x) in (eq_ind nat x (\lambda n:nat.(eq nat n x)) (refl_equal nat x) (minus x O) DEFINED))
-Post Nodes: 26
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: eq_nat_dec
-Pre Nodes : 303
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda i:nat.(nat_ind (\lambda n:nat.(\forall j:nat.(or (not (eq nat n j)) (eq nat n j)))) (\lambda j:nat.(nat_ind (\lambda n:nat.(or (not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O) (refl_equal nat O)) (\lambda n:nat.(\lambda _:(or (not (eq nat O n)) (eq nat O n)).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j)) (\lambda n:nat.(\lambda H:(\forall j:nat.(or (not (eq nat n j)) (eq nat n j))).(\lambda j:nat.(nat_ind (\lambda n0:nat.(or (not (eq nat (S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda n0:nat.(\lambda _:(or (not (eq nat (S n) n0)) (eq nat (S n) n0)). let DEFINED \def (H n0) in (or_ind (not (eq nat n n0)) (eq nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda H1:(not (eq nat n n0)).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (not_eq_S n n0 H1))) (\lambda H1:(eq nat n n0).(or_intror (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) DEFINED))) j)))) i))
-Post Nodes: 305
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: neq_eq_e
-Pre Nodes : 47
-Optimized : (\lambda i:nat.(\lambda j:nat.(\lambda P:Prop.(\lambda H:((not (eq nat i j))\to P).(\lambda H0:((eq nat i j)\to P). let o \def (eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o))))))
-Post Nodes: 47
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_false
-Pre Nodes : 382
-nat
-nat
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: nested application
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-nat
-nat
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: nested application
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda m:nat.(nat_ind (\lambda n:nat.(\forall n0:nat.(\forall P:Prop.((le n n0)\to ((le (S n0) n)\to P))))) (\lambda n:nat.(\lambda P:Prop.(\lambda _:(le O n).(\lambda H0:(le (S n) O). let H1 \def (le_ind (S n) (\lambda n0:nat.((eq nat n0 O)\to P)) (\lambda H1:(eq nat (S n) O). let H2 \def (eq_ind nat (S n) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H1) in (False_ind P H2)) (\lambda m0:nat.(\lambda H1:(le (S n) m0).(\lambda _:((eq nat m0 O)\to P).(\lambda H2:(eq nat (S m0) O). let H3 \def (eq_ind nat (S m0) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H2) in let DEFINED \def (False_ind ((le (S n) m0)\to P) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O)))))) (\lambda n:nat.(\lambda H:(\forall n0:nat.(\forall P:Prop.((le n n0)\to ((le (S n0) n)\to P)))).(\lambda n0:nat.(nat_ind (\lambda n1:nat.(\forall P:Prop.((le (S n) n1)\to ((le (S n1) (S n))\to P)))) (\lambda P:Prop.(\lambda H0:(le (S n) O).(\lambda _:(le (S O) (S n)). let H2 \def (le_ind (S n) (\lambda n1:nat.((eq nat n1 O)\to P)) (\lambda H2:(eq nat (S n) O). let H3 \def (eq_ind nat (S n) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H2) in (False_ind P H3)) (\lambda m0:nat.(\lambda H2:(le (S n) m0).(\lambda _:((eq nat m0 O)\to P).(\lambda H3:(eq nat (S m0) O). let H4 \def (eq_ind nat (S m0) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H3) in let DEFINED \def (False_ind ((le (S n) m0)\to P) H4) in (DEFINED H2))))) O H0) in (H2 (refl_equal nat O))))) (\lambda n1:nat.(\lambda _:(\forall P:Prop.((le (S n) n1)\to ((le (S n1) (S n))\to P))).(\lambda P:Prop.(\lambda H1:(le (S n) (S n1)).(\lambda H2:(le (S (S n1)) (S n)). let DEFINED \def (le_S_n (S n1) n H2) in (H n1 P (le_S_n n n1 H1) DEFINED)))))) n0)))) m))
-Post Nodes: 400
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_Sx_x
-Pre Nodes : 20
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda H:(le (S x) x).(\lambda P:Prop. let H0 \def le_Sn_n in let DEFINED \def (H0 x H) in (False_ind P DEFINED))))
-Post Nodes: 22
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: minus_le
-Pre Nodes : 88
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.(le (minus n y) n))) (\lambda _:nat.(le_n O)) (\lambda n:nat.(\lambda H:(\forall y:nat.(le (minus n y) n)).(\lambda y:nat.(nat_ind (\lambda n0:nat.(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda n0:nat.(\lambda _:(le
-match n0 return (\lambda n1:nat.nat) with
- [ O => (S n)
- | (S (l:nat)) => (minus n l)
-] (S n)).(le_S (minus n n0) n (H n0)))) y)))) x))
-Post Nodes: 88
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_plus_minus_sym
-Pre Nodes : 45
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda n:nat.(\lambda m:nat.(\lambda H:(le n m). let DEFINED \def (plus_comm (minus m n) n) in (eq_ind_r nat (plus n (minus m n)) (\lambda n0:nat.(eq nat m n0)) (le_plus_minus n m H) (plus (minus m n) n) DEFINED))))
-Post Nodes: 47
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_minus_minus
-Pre Nodes : 84
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(le x y).(\lambda z:nat.(\lambda H0:(le y z). let DEFINED \def (le_plus_minus_r x z (le_trans x y z H H0)) in let DEFINED0 \def (le_plus_minus_r x y H) in (plus_le_reg_l x (minus y x) (minus z x) (eq_ind_r nat y (\lambda n:nat.(le n (plus x (minus z x)))) (eq_ind_r nat z (\lambda n:nat.(le y n)) H0 (plus x (minus z x)) DEFINED) (plus x (minus y x)) DEFINED0)))))))
-Post Nodes: 88
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_minus_plus
-Pre Nodes : 505
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-nat
-nat
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: nested application
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x:nat.((le n x)\to (\forall y:nat.(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) (\lambda x:nat.(\lambda H:(le O x). let H0 \def (le_ind O (\lambda n:nat.((eq nat n x)\to (\forall y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))))) (\lambda H0:(eq nat O x).(eq_ind nat O (\lambda n:nat.(\forall y:nat.(eq nat (minus (plus n y) O) (plus (minus n O) y)))) (\lambda y:nat.(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) (minus_n_O (plus O y)))) x H0)) (\lambda m:nat.(\lambda H0:(le O m).(\lambda _:((eq nat m x)\to (\forall y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y)))).(\lambda H1:(eq nat (S m) x). let DEFINED \def (eq_ind nat (S m) (\lambda n:nat.((le O m)\to (\forall y:nat.(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda _:(le O m).(\lambda y:nat.(refl_equal nat (plus (minus (S m) O) y)))) x H1) in (DEFINED H0))))) x H) in (H0 (refl_equal nat x)))) (\lambda z0:nat.(\lambda H:(\forall x:nat.((le z0 x)\to (\forall y:nat.(eq nat (minus (plus x y) z0) (plus (minus x z0) y))))).(\lambda x:nat.(nat_ind (\lambda n:nat.((le (S z0) n)\to (\forall y:nat.(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y))))) (\lambda H0:(le (S z0) O).(\lambda y:nat. let H1 \def (le_ind (S z0) (\lambda n:nat.((eq nat n O)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)))) (\lambda H1:(eq nat (S z0) O). let H2 \def (eq_ind nat (S z0) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H1) in (False_ind (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2)) (\lambda m:nat.(\lambda H1:(le (S z0) m).(\lambda _:((eq nat m O)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))).(\lambda H2:(eq nat (S m) O). let H3 \def (eq_ind nat (S m) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H2) in let DEFINED \def (False_ind ((le (S z0) m)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O)))) (\lambda n:nat.(\lambda _:((le (S z0) n)\to (\forall y:nat.(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y)))).(\lambda H1:(le (S z0) (S n)).(\lambda y:nat.(H n (le_S_n z0 n H1) y))))) x)))) z))
-Post Nodes: 560
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_minus
-Pre Nodes : 51
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda z:nat.(\lambda y:nat.(\lambda H:(le (plus x y) z). let DEFINED \def (minus_plus_r x y) in (eq_ind nat (minus (plus x y) y) (\lambda n:nat.(le n (minus z y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x DEFINED)))))
-Post Nodes: 53
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_trans_plus_r
-Pre Nodes : 27
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda z:nat.(\lambda H:(le (plus x y) z).(le_trans y (plus x y) z (le_plus_r x y) H)))))
-Post Nodes: 27
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_gen_S
-Pre Nodes : 217
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-Optimized : (\lambda m:nat.(\lambda x:nat.(\lambda H:(le (S m) x). let H0 \def (le_ind (S m) (\lambda n:nat.((eq nat n x)\to (ex2 nat (\lambda n0:nat.(eq nat x (S n0))) (\lambda n0:nat.(le m n0))))) (\lambda H0:(eq nat (S m) x).(eq_ind nat (S m) (\lambda n:nat.(ex2 nat (\lambda n0:nat.(eq nat n (S n0))) (\lambda n0:nat.(le m n0)))) (ex_intro2 nat (\lambda n:nat.(eq nat (S m) (S n))) (\lambda n:nat.(le m n)) m (refl_equal nat (S m)) (le_n m)) x H0)) (\lambda m0:nat.(\lambda H0:(le (S m) m0).(\lambda _:((eq nat m0 x)\to (ex2 nat (\lambda n0:nat.(eq nat x (S n0))) (\lambda n0:nat.(le m n0)))).(\lambda H1:(eq nat (S m0) x). let DEFINED \def (eq_ind nat (S m0) (\lambda n:nat.((le (S m) m0)\to (ex2 nat (\lambda n0:nat.(eq nat n (S n0))) (\lambda n0:nat.(le m n0))))) (\lambda H2:(le (S m) m0).(ex_intro2 nat (\lambda n:nat.(eq nat (S m0) (S n))) (\lambda n:nat.(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) x H1) in (DEFINED H0))))) x H) in (H0 (refl_equal nat x)))))
-Post Nodes: 243
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_x_plus_x_Sy
-Pre Nodes : 64
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda y:nat. let DEFINED \def (plus_comm x (S y)) in (eq_ind_r nat (plus (S y) x) (\lambda n:nat.(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) DEFINED)))
-Post Nodes: 66
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: simpl_lt_plus_r
-Pre Nodes : 75
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda p:nat.(\lambda n:nat.(\lambda m:nat.(\lambda H:(lt (plus n p) (plus m p)). let DEFINED \def (plus_comm n p) in let H0 \def (eq_ind nat (plus n p) (\lambda n0:nat.(lt n0 (plus m p))) H (plus p n) DEFINED) in let DEFINED0 \def (plus_comm m p) in let H1 \def (eq_ind nat (plus m p) (\lambda n0:nat.(lt (plus p n) n0)) H0 (plus p m) DEFINED0) in (plus_lt_reg_l n m p H1)))))
-Post Nodes: 79
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: minus_x_Sy
-Pre Nodes : 330
-nat
-nat
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: nested application
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y))))))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq nat (minus O y) (S (minus O (S y)))))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H0) in (False_ind (eq nat (minus O y) (S (minus O (S y)))) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq nat (minus O y) (S (minus O (S y))))).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq nat (minus O y) (S (minus O (S y))))) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y)))))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda _:(lt O (S n)). let DEFINED \def (minus_n_O n) in (eq_ind nat n (\lambda n0:nat.(eq nat (S n) (S n0))) (refl_equal nat (S n)) (minus n O) DEFINED)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))).(\lambda H1:(lt (S n0) (S n)). let H2 \def (le_S_n (S n0) n H1) in (H n0 H2)))) y)))) x))
-Post Nodes: 354
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_plus_minus
-Pre Nodes : 16
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y).(le_plus_minus (S x) y H))))
-Post Nodes: 16
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_plus_minus_r
-Pre Nodes : 53
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y). let DEFINED \def (plus_comm (minus y (S x)) x) in (eq_ind_r nat (plus x (minus y (S x))) (\lambda n:nat.(eq nat y (S n))) (lt_plus_minus x y H) (plus (minus y (S x)) x) DEFINED))))
-Post Nodes: 55
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: minus_x_SO
-Pre Nodes : 56
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda H:(lt O x). let DEFINED \def (minus_n_O x) in let DEFINED0 \def (minus_x_Sy x O H) in (eq_ind nat (minus x O) (\lambda n:nat.(eq nat x n)) (eq_ind nat x (\lambda n:nat.(eq nat x n)) (refl_equal nat x) (minus x O) DEFINED) (S (minus x (S O))) DEFINED0)))
-Post Nodes: 60
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_x_pred_y
-Pre Nodes : 175
-nat
-nat
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: nested application
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-Optimized : (\lambda y:nat.(nat_ind (\lambda n:nat.(\forall x:nat.((lt x n)\to (le x (pred n))))) (\lambda x:nat.(\lambda H:(lt x O). let H0 \def (le_ind (S x) (\lambda n:nat.((eq nat n O)\to (le x O))) (\lambda H0:(eq nat (S x) O). let H1 \def (eq_ind nat (S x) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H0) in (False_ind (le x O) H1)) (\lambda m:nat.(\lambda H0:(le (S x) m).(\lambda _:((eq nat m O)\to (le x O)).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H1) in let DEFINED \def (False_ind ((le (S x) m)\to (le x O)) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda _:(\forall x:nat.((lt x n)\to (le x (pred n)))).(\lambda x:nat.(\lambda H0:(lt x (S n)).(le_S_n x n H0))))) y))
-Post Nodes: 186
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_le_minus
-Pre Nodes : 44
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y). let DEFINED \def (plus_comm x (S O)) in (le_minus x y (S O) (eq_ind_r nat (plus (S O) x) (\lambda n:nat.(le n y)) H (plus x (S O)) DEFINED)))))
-Post Nodes: 46
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_le_e
-Pre Nodes : 39
-Optimized : (\lambda n:nat.(\lambda d:nat.(\lambda P:Prop.(\lambda H:((lt n d)\to P).(\lambda H0:((le d n)\to P). let H1 \def (le_or_lt d n) in (or_ind (le d n) (lt n d) P H0 H H1))))))
-Post Nodes: 39
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_eq_e
-Pre Nodes : 45
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda P:Prop.(\lambda H:((lt x y)\to P).(\lambda H0:((eq nat x y)\to P).(\lambda H1:(le x y). let DEFINED \def (le_lt_or_eq x y H1) in (or_ind (lt x y) (eq nat x y) P H H0 DEFINED)))))))
-Post Nodes: 47
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_eq_gt_e
-Pre Nodes : 60
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda P:Prop.(\lambda H:((lt x y)\to P).(\lambda H0:((eq nat x y)\to P).(\lambda H1:((lt y x)\to P).(lt_le_e x y P H (\lambda H2:(le y x).(lt_eq_e y x P H1 (\lambda H3:(eq nat y x).(H0 (sym_eq nat y x H3))) H2)))))))))
-Post Nodes: 60
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_gen_xS
-Pre Nodes : 190
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall n0:nat.((lt n (S n0))\to (or (eq nat n O) (ex2 nat (\lambda m:nat.(eq nat n (S m))) (\lambda m:nat.(lt m n0))))))) (\lambda n:nat.(\lambda _:(lt O (S n)).(or_introl (eq nat O O) (ex2 nat (\lambda m:nat.(eq nat O (S m))) (\lambda m:nat.(lt m n))) (refl_equal nat O)))) (\lambda n:nat.(\lambda _:(\forall n0:nat.((lt n (S n0))\to (or (eq nat n O) (ex2 nat (\lambda m:nat.(eq nat n (S m))) (\lambda m:nat.(lt m n0)))))).(\lambda n0:nat.(\lambda H0:(lt (S n) (S n0)).(or_intror (eq nat (S n) O) (ex2 nat (\lambda m:nat.(eq nat (S n) (S m))) (\lambda m:nat.(lt m n0))) (ex_intro2 nat (\lambda m:nat.(eq nat (S n) (S m))) (\lambda m:nat.(lt m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x))
-Post Nodes: 190
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_lt_false
-Pre Nodes : 25
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(le x y).(\lambda H0:(lt y x).(\lambda P:Prop. let DEFINED \def (le_not_lt x y H H0) in (False_ind P DEFINED))))))
-Post Nodes: 27
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: lt_neq
-Pre Nodes : 33
-Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y).(\lambda H0:(eq nat x y). let H1 \def (eq_ind nat x (\lambda n:nat.(lt n y)) H y H0) in (lt_irrefl y H1)))))
-Post Nodes: 33
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: arith0
-Pre Nodes : 185
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda h2:nat.(\lambda d2:nat.(\lambda n:nat.(\lambda H:(le (plus d2 h2) n).(\lambda h3:nat. let DEFINED \def (plus_comm h2 d2) in let DEFINED0 \def (plus_assoc h2 d2 h3) in let DEFINED1 \def (minus_plus h2 (plus d2 h3)) in (eq_ind nat (minus (plus h2 (plus d2 h3)) h2) (\lambda n0:nat.(le n0 (minus (plus n h3) h2))) (le_minus_minus h2 (plus h2 (plus d2 h3)) (le_plus_l h2 (plus d2 h3)) (plus n h3) (eq_ind_r nat (plus (plus h2 d2) h3) (\lambda n0:nat.(le n0 (plus n h3))) (eq_ind_r nat (plus d2 h2) (\lambda n0:nat.(le (plus n0 h3) (plus n h3))) (le_S_n (plus (plus d2 h2) h3) (plus n h3) (lt_le_S (plus (plus d2 h2) h3) (S (plus n h3)) (le_lt_n_Sm (plus (plus d2 h2) h3) (plus n h3) (plus_le_compat (plus d2 h2) n h3 h3 H (le_n h3))))) (plus h2 d2) DEFINED) (plus h2 (plus d2 h3)) DEFINED0)) (plus d2 h3) DEFINED1))))))
-Post Nodes: 191
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: O_minus
-Pre Nodes : 211
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le n y)\to (eq nat (minus n y) O)))) (\lambda y:nat.(\lambda _:(le O y).(refl_equal nat O))) (\lambda x0:nat.(\lambda H:(\forall y:nat.((le x0 y)\to (eq nat (minus x0 y) O))).(\lambda y:nat.(nat_ind (\lambda n:nat.((le (S x0) n)\to (eq nat
-match n return (\lambda n1:nat.nat) with
- [ O => (S x0)
- | (S (l:nat)) => (minus x0 l)
-] O))) (\lambda H0:(le (S x0) O). let DEFINED \def (le_gen_S x0 O H0) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le x0 n)) (eq nat (S x0) O) (\lambda x1:nat.(\lambda H1:(eq nat O (S x1)).(\lambda _:(le x0 x1). let H3 \def (eq_ind nat O (\lambda ee:nat.
-match ee return (\lambda _:nat.Prop) with
- [ O => True
- | (S (_:nat)) => False
-]) I (S x1) H1) in (False_ind (eq nat (S x0) O) H3)))) DEFINED)) (\lambda n:nat.(\lambda _:((le (S x0) n)\to (eq nat
-match n return (\lambda n1:nat.nat) with
- [ O => (S x0)
- | (S (l:nat)) => (minus x0 l)
-] O)).(\lambda H1:(le (S x0) (S n)).(H n (le_S_n x0 n H1))))) y)))) x))
-Post Nodes: 213
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: minus_minus
-Pre Nodes : 592
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x:nat.(\forall y:nat.((le n x)\to ((le n y)\to ((eq nat (minus x n) (minus y n))\to (eq nat x y))))))) (\lambda x:nat.(\lambda y:nat.(\lambda _:(le O x).(\lambda _:(le O y).(\lambda H1:(eq nat (minus x O) (minus y O)). let DEFINED \def (minus_n_O x) in let H2 \def (eq_ind_r nat (minus x O) (\lambda n:nat.(eq nat n (minus y O))) H1 x DEFINED) in let DEFINED0 \def (minus_n_O y) in let H3 \def (eq_ind_r nat (minus y O) (\lambda n:nat.(eq nat x n)) H2 y DEFINED0) in H3))))) (\lambda z0:nat.(\lambda IH:(\forall x:nat.(\forall y:nat.((le z0 x)\to ((le z0 y)\to ((eq nat (minus x z0) (minus y z0))\to (eq nat x y)))))).(\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le (S z0) n)\to ((le (S z0) y)\to ((eq nat (minus n (S z0)) (minus y (S z0)))\to (eq nat n y)))))) (\lambda y:nat.(\lambda H:(le (S z0) O).(\lambda _:(le (S z0) y).(\lambda _:(eq nat (minus O (S z0)) (minus y (S z0))). let DEFINED \def (le_gen_S z0 O H) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le z0 n)) (eq nat O y) (\lambda x0:nat.(\lambda H2:(eq nat O (S x0)).(\lambda _:(le z0 x0). let H4 \def (eq_ind nat O (\lambda ee:nat.
-match ee return (\lambda _:nat.Prop) with
- [ O => True
- | (S (_:nat)) => False
-]) I (S x0) H2) in (False_ind (eq nat O y) H4)))) DEFINED))))) (\lambda x0:nat.(\lambda _:(\forall y:nat.((le (S z0) x0)\to ((le (S z0) y)\to ((eq nat (minus x0 (S z0)) (minus y (S z0)))\to (eq nat x0 y))))).(\lambda y:nat.(nat_ind (\lambda n:nat.((le (S z0) (S x0))\to ((le (S z0) n)\to ((eq nat (minus (S x0) (S z0)) (minus n (S z0)))\to (eq nat (S x0) n))))) (\lambda _:(le (S z0) (S x0)).(\lambda H0:(le (S z0) O).(\lambda _:(eq nat (minus (S x0) (S z0)) (minus O (S z0))). let DEFINED \def (le_gen_S z0 O H0) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le z0 n)) (eq nat (S x0) O) (\lambda x1:nat.(\lambda H2:(eq nat O (S x1)).(\lambda _:(le z0 x1). let H4 \def (eq_ind nat O (\lambda ee:nat.
-match ee return (\lambda _:nat.Prop) with
- [ O => True
- | (S (_:nat)) => False
-]) I (S x1) H2) in (False_ind (eq nat (S x0) O) H4)))) DEFINED)))) (\lambda y0:nat.(\lambda _:((le (S z0) (S x0))\to ((le (S z0) y0)\to ((eq nat (minus (S x0) (S z0)) (minus y0 (S z0)))\to (eq nat (S x0) y0)))).(\lambda H:(le (S z0) (S x0)).(\lambda H0:(le (S z0) (S y0)).(\lambda H1:(eq nat (minus (S x0) (S z0)) (minus (S y0) (S z0))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z))
-Post Nodes: 600
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: plus_plus
-Pre Nodes : 1222
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-\e[0;33mWarn: \e[0mOptimizer: swap 1
-Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x1:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le x1 n)\to ((le x2 n)\to ((eq nat (plus (minus n x1) y1) (plus (minus n x2) y2))\to (eq nat (plus x1 y2) (plus x2 y1)))))))))) (\lambda x1:nat.(\lambda x2:nat.(\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le x1 O).(\lambda H0:(le x2 O).(\lambda H1:(eq nat y1 y2). let H_y \def (le_n_O_eq x2 H0) in let H_y0 \def (le_n_O_eq x1 H) in (eq_ind nat y1 (\lambda n:nat.(eq nat (plus x1 n) (plus x2 y1))) (eq_ind nat O (\lambda n:nat.(eq nat (plus x1 y1) (plus n y1))) (eq_ind nat O (\lambda n:nat.(eq nat (plus n y1) (plus O y1))) (refl_equal nat (plus O y1)) x1 H_y0) x2 H_y) y2 H1)))))))) (\lambda z0:nat.(\lambda IH:(\forall x1:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le x1 z0)\to ((le x2 z0)\to ((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2))\to (eq nat (plus x1 y2) (plus x2 y1))))))))).(\lambda x1:nat.(nat_ind (\lambda n:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le n (S z0))\to ((le x2 (S z0))\to ((eq nat (plus (minus (S z0) n) y1) (plus (minus (S z0) x2) y2))\to (eq nat (plus n y2) (plus x2 y1))))))))) (\lambda x2:nat.(nat_ind (\lambda n:nat.(\forall y1:nat.(\forall y2:nat.((le O (S z0))\to ((le n (S z0))\to ((eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) n) y2))\to (eq nat (plus O y2) (plus n y1)))))))) (\lambda y1:nat.(\lambda y2:nat.(\lambda _:(le O (S z0)).(\lambda _:(le O (S z0)).(\lambda H1:(eq nat (S (plus z0 y1)) (S (plus z0 y2))). let H_y \def (IH O O) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.(\forall y3:nat.(\forall y4:nat.((le O z0)\to ((le O z0)\to ((eq nat (plus n y3) (plus n y4))\to (eq nat y4 y3))))))) H_y z0 DEFINED) in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (H2 (plus z0 y2) (plus z0 y1) (le_O_n z0) (le_O_n z0) (f_equal nat nat (plus z0) (plus z0 y2) (plus z0 y1) (sym_eq nat (plus z0 y1) (plus z0 y2) (eq_add_S (plus z0 y1) (plus z0 y2) H1)))))))))) (\lambda x3:nat.(\lambda _:(\forall y1:nat.(\forall y2:nat.((le O (S z0))\to ((le x3 (S z0))\to ((eq nat (S (plus z0 y1)) (plus
-match x3 return (\lambda n:nat.nat) with
- [ O => (S z0)
- | (S (l:nat)) => (minus z0 l)
-] y2))\to (eq nat y2 (plus x3 y1))))))).(\lambda y1:nat.(\lambda y2:nat.(\lambda _:(le O (S z0)).(\lambda H0:(le (S x3) (S z0)).(\lambda H1:(eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2)). let H_y \def (IH O x3 (S y1)) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat (plus n (S y1)) (plus (minus z0 x3) y3))\to (eq nat y3 (plus x3 (S y1)))))))) H_y z0 DEFINED) in let DEFINED0 \def (plus_n_Sm z0 y1) in let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat n (plus (minus z0 x3) y3))\to (eq nat y3 (plus x3 (S y1)))))))) H2 (S (plus z0 y1)) DEFINED0) in let DEFINED1 \def (plus_n_Sm x3 y1) in let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat (S (plus z0 y1)) (plus (minus z0 x3) y3))\to (eq nat y3 n)))))) H3 (S (plus x3 y1)) DEFINED1) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1)))))))) x2)) (\lambda x2:nat.(\lambda _:(\forall x3:nat.(\forall y1:nat.(\forall y2:nat.((le x2 (S z0))\to ((le x3 (S z0))\to ((eq nat (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2))\to (eq nat (plus x2 y2) (plus x3 y1)))))))).(\lambda x3:nat.(nat_ind (\lambda n:nat.(\forall y1:nat.(\forall y2:nat.((le (S x2) (S z0))\to ((le n (S z0))\to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2))\to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le (S x2) (S z0)).(\lambda _:(le O (S z0)).(\lambda H1:(eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))). let H_y \def (IH x2 O y1 (S y2)) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) (plus n (S y2)))\to (eq nat (plus x2 (S y2)) y1))))) H_y z0 DEFINED) in let DEFINED0 \def (plus_n_Sm z0 y2) in let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) n)\to (eq nat (plus x2 (S y2)) y1))))) H2 (S (plus z0 y2)) DEFINED0) in let DEFINED1 \def (plus_n_Sm x2 y2) in let H4 \def (eq_ind_r nat (plus x2 (S y2)) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))\to (eq nat n y1))))) H3 (S (plus x2 y2)) DEFINED1) in (H4 (le_S_n x2 z0 H) (le_O_n z0) H1)))))) (\lambda x4:nat.(\lambda _:(\forall y1:nat.(\forall y2:nat.((le (S x2) (S z0))\to ((le x4 (S z0))\to ((eq nat (plus (minus z0 x2) y1) (plus
-match x4 return (\lambda n:nat.nat) with
- [ O => (S z0)
- | (S (l:nat)) => (minus z0 l)
-] y2))\to (eq nat (S (plus x2 y2)) (plus x4 y1))))))).(\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le (S x2) (S z0)).(\lambda H0:(le (S x4) (S z0)).(\lambda H1:(eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4) y2)).(f_equal nat nat S (plus x2 y2) (plus x4 y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3)))) x1)))) z))
-Post Nodes: 1236
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: le_S_minus
-Pre Nodes : 41
-\e[0;33mWarn: \e[0mOptimizer: remove 1
-Optimized : (\lambda d:nat.(\lambda h:nat.(\lambda n:nat.(\lambda H:(le (plus d h) n).(le_S d (minus n h) (le_minus d n h H))))))
-Post Nodes: 27
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/arith.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of ext/arith.mma completed in 44''.
-\e[0;32mInfo: \e[0mexecution of ext/tactics.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext ...''
-\e[0;32mInfo: \e[0mbaseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics is not empty
-\e[0;32mInfo: \e[0mcleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics
-\e[0;32mInfo: \e[0mRemoving: cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics/*
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: insert_eq
-Pre Nodes : 36
-Optimized : (\lambda S:Set.(\lambda x:S.(\lambda P:(S\to Prop).(\lambda G:Prop.(\lambda H:(\forall y:S.((P y)\to ((eq S y x)\to G))).(\lambda H0:(P x).(H x H0 (refl_equal S x))))))))
-Post Nodes: 36
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: unintro
-Pre Nodes : 17
-Optimized : (\lambda A:Set.(\lambda a:A.(\lambda P:(A\to Prop).(\lambda H:(\forall x:A.(P x)).(H a)))))
-Post Nodes: 17
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: xinduction
-Pre Nodes : 27
-Optimized : (\lambda A:Set.(\lambda t:A.(\lambda P:(A\to Prop).(\lambda H:(\forall x:A.((eq A t x)\to (P x))).(H t (refl_equal A t))))))
-Post Nodes: 27
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/tactics.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of ext/tactics.mma completed in 4''.
-\e[0;32mInfo: \e[0mexecution of pippo.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pip ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: minus_x_Sy
-Pre Nodes : 330
-nat
-nat
-nat
-nat
-\e[0;33mWarn: \e[0mOptimizer: remove 3
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: nested application
-\e[0;33mWarn: \e[0mOptimizer: anticipate 2
-\e[0;33mWarn: \e[0mOptimizer: swap 2
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y))))))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq nat (minus O y) (S (minus O (S y)))))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H0) in (False_ind (eq nat (minus O y) (S (minus O (S y)))) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq nat (minus O y) (S (minus O (S y))))).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat.
-match e return (\lambda _:nat.Prop) with
- [ O => False
- | (S (_:nat)) => True
-]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq nat (minus O y) (S (minus O (S y))))) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y)))))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda _:(lt O (S n)). let DEFINED \def (minus_n_O n) in (eq_ind nat n (\lambda n0:nat.(eq nat (S n) (S n0))) (refl_equal nat (S n)) (minus n O) DEFINED)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))).(\lambda H1:(lt (S n0) (S n)). let H2 \def (le_S_n (S n0) n H1) in (H n0 H2)))) y)))) x))
-Post Nodes: 354
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./pippo.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of pippo.mma completed in 2''.
-\e[0;32mInfo: \e[0mexecution of plist/defs.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pli ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of plist/defs.mma completed in 1''.
-\e[0;32mInfo: \e[0mexecution of plist/props.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pli ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/plist/def ...''
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: papp_ss
-Pre Nodes : 121
-\e[0;33mWarn: \e[0mOptimizer: anticipate 3
-\e[0;33mWarn: \e[0mOptimizer: swap 3
-Optimized : (\lambda is1:PList.(PList_ind (\lambda p:PList.(\forall is2:PList.(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2))))) (\lambda is2:PList.(refl_equal PList (Ss is2))) (\lambda n:nat.(\lambda n0:nat.(\lambda p:PList.(\lambda H:(\forall is2:PList.(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2)))).(\lambda is2:PList. let DEFINED \def (H is2) in (eq_ind_r PList (Ss (papp p is2)) (\lambda p0:PList.(eq PList (PCons n (S n0) p0) (PCons n (S n0) (Ss (papp p is2))))) (refl_equal PList (PCons n (S n0) (Ss (papp p is2)))) (papp (Ss p) (Ss is2)) DEFINED)))))) is1))
-Post Nodes: 123
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of plist/props.mma completed in 2''.
-\e[0;32mInfo: \e[0mexecution of types/defs.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/typ ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of types/defs.mma completed in 0''.
-\e[0;32mInfo: \e[0mexecution of types/props.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/typ ...''
-\e[0;32mInfo: \e[0mbaseuri cic:/matita/LAMBDA-TYPES/Base-2/types/props is not empty
-\e[0;32mInfo: \e[0mcleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/types/props
-\e[0;32mInfo: \e[0mRemoving: cic:/matita/LAMBDA-TYPES/Base-2/types/props/*
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/types/def ...''
-\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
-BEGIN: ex2_sym
-Pre Nodes : 77
-Optimized : (\lambda A:Set.(\lambda P:(A\to Prop).(\lambda Q:(A\to Prop).(\lambda H:(ex2 A (\lambda x:A.(P x)) (\lambda x:A.(Q x))).(ex2_ind A (\lambda x:A.(P x)) (\lambda x:A.(Q x)) (ex2 A (\lambda x:A.(Q x)) (\lambda x:A.(P x))) (\lambda x:A.(\lambda H0:(P x).(\lambda H1:(Q x).(ex_intro2 A (\lambda x0:A.(Q x0)) (\lambda x0:A.(P x0)) x H1 H0)))) H)))))
-Post Nodes: 77
-\e[0;34mDebug: \e[0mProcedural: level 2 transformation
-\e[0;34mDebug: \e[0mProcedural: grafite rendering
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of types/props.mma completed in 2''.
-\e[0;32mInfo: \e[0mexecution of theory.mma started:
-\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/the ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/tactics.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/ext/tacti ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/arith.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/types/pro ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/blt/props ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/plist/pro ...''
-\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./theory.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
-\e[0;32mInfo: \e[0mexecution of theory.mma completed in 1''.
+++ /dev/null
-baseuri=cic:/matita/LAMBDA-TYPES/Base-2
DIR=$(shell basename $$PWD)
-MATITAOPTIONS=-onepass
-$(DIR) all:
- ../../../matitac $(MATITAOPTIONS)
-$(DIR).opt opt all.opt:
- ../../../matitac.opt $(MATITAOPTIONS)
+MMAS = $(shell find -name "*.mma")
+MAS = $(MMAS:%.mma=%.ma)
+
+%.ma: %.mma
+ ../../matitac.opt $< 2> /dev/null
+ ../../matitac.opt -dump $@ $< 2> /dev/null
+ $(MAKE) depend.opt
+
+$(DIR) all: $(MAS)
+ ../../matitac
+$(DIR).opt opt all.opt: $(MAS)
+ ../../matitac.opt
clean:
- ../../../matitaclean
+ ../../matitaclean
+ rm -f $(MAS)
+ $(MAKE) depend
clean.opt:
- ../../../matitaclean.opt
+ ../../matitaclean.opt
+ rm -f $(MAS)
+ $(MAKE) depend.opt
depend:
- ../../../matitadep
+ ../../matitadep
+ cat Base-2/depends_mma >> depends
depend.opt:
- ../../../matitadep.opt
+ ../../matitadep.opt
+ cat Base-2/depends_mma >> depends
+
+include Base-2/.depend
-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
+Base-1/theory.ma Base-1/blt/props.ma Base-1/ext/arith.ma Base-1/ext/tactics.ma Base-1/plist/props.ma Base-1/types/props.ma
+Base-1/definitions.ma Base-1/blt/defs.ma Base-1/plist/defs.ma Base-1/types/defs.ma
+Base-1/preamble.ma coq.ma
+Base-1/spare.ma Base-1/theory.ma
+Base-1/plist/defs.ma Base-1/preamble.ma
+Base-1/plist/props.ma Base-1/plist/defs.ma
+Base-1/types/props.ma Base-1/types/defs.ma
+Base-1/types/defs.ma Base-1/preamble.ma
+Base-1/blt/props.ma Base-1/blt/defs.ma
+Base-1/blt/defs.ma Base-1/preamble.ma
+Base-1/ext/tactics.ma Base-1/preamble.ma
+Base-1/ext/arith.ma Base-1/preamble.ma
+Base-2/preamble.ma Base-1/definitions.ma
+Base-2/theory.ma Base-2/blt/props.ma Base-2/ext/arith.ma Base-2/ext/tactics.ma Base-2/plist/props.ma Base-2/types/props.ma
+Base-2/types/defs.ma Base-2/preamble.ma
+Base-2/types/props.ma Base-2/types/defs.ma
+Base-2/plist/defs.ma Base-2/preamble.ma
+Base-2/plist/props.ma Base-2/plist/defs.ma
+Base-2/ext/arith.ma Base-2/preamble.ma
+Base-2/ext/tactics.ma Base-2/preamble.ma
+Base-2/blt/defs.ma Base-2/preamble.ma
+Base-2/blt/props.ma Base-2/blt/defs.ma
coq.ma
+Base-2/theory.mma Base-2/preamble.ma Base-1/theory.ma
+Base-2/ext/tactics.mma Base-2/preamble.ma Base-1/ext/tactics.ma
+Base-2/ext/arith.mma Base-2/preamble.ma Base-1/ext/arith.ma
+Base-2/types/defs.mma Base-2/preamble.ma Base-1/types/defs.ma
+Base-2/types/props.mma Base-2/preamble.ma Base-1/types/props.ma
+Base-2/blt/defs.mma Base-2/preamble.ma Base-1/blt/defs.ma
+Base-2/blt/props.mma Base-2/preamble.ma Base-1/blt/props.ma
+Base-2/plist/defs.mma Base-2/preamble.ma Base-1/plist/defs.ma
+Base-2/plist/props.mma Base-2/preamble.ma Base-1/plist/props.ma
--- /dev/null
+\e[0;32mInfo: \e[0mexecution of blt/defs.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of blt/defs.mma completed in 1''.
+\e[0;32mInfo: \e[0mexecution of blt/props.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt ...''
+\e[0;32mInfo: \e[0mbaseuri cic:/matita/LAMBDA-TYPES/Base-2/blt/props is not empty
+\e[0;32mInfo: \e[0mcleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/blt/props
+\e[0;32mInfo: \e[0mRemoving: cic:/matita/LAMBDA-TYPES/Base-2/blt/props/*
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs" ...''
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_blt
+Pre Nodes : 257
+nat
+nat
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: nested application
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq bool (blt y n) true)))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq bool (blt y O) true))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H0) in (False_ind (eq bool (blt y O) true) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq bool (blt y O) true)).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq bool (blt y O) true)) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq bool (blt y n) true))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq bool (blt n0 (S n)) true))) (\lambda _:(lt O (S n)).(refl_equal bool true)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq bool
+match n0 return (\lambda n1:nat.bool) with
+ [ O => true
+ | (S (m:nat)) => (blt m n)
+] true)).(\lambda H1:(lt (S n0) (S n)).(H n0 (le_S_n (S n0) n H1))))) y)))) x))
+Post Nodes: 272
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_bge
+Pre Nodes : 255
+nat
+nat
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: nested application
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le n y)\to (eq bool (blt y n) false)))) (\lambda y:nat.(\lambda _:(le O y).(refl_equal bool false))) (\lambda n:nat.(\lambda H:(\forall y:nat.((le n y)\to (eq bool (blt y n) false))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((le (S n) n0)\to (eq bool (blt n0 (S n)) false))) (\lambda H0:(le (S n) O). let H1 \def (le_ind (S n) (\lambda n0:nat.((eq nat n0 O)\to (eq bool (blt O (S n)) false))) (\lambda H1:(eq nat (S n) O). let H2 \def (eq_ind nat (S n) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H1) in (False_ind (eq bool (blt O (S n)) false) H2)) (\lambda m:nat.(\lambda H1:(le (S n) m).(\lambda _:((eq nat m O)\to (eq bool (blt O (S n)) false)).(\lambda H2:(eq nat (S m) O). let H3 \def (eq_ind nat (S m) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H2) in let DEFINED \def (False_ind ((le (S n) m)\to (eq bool (blt O (S n)) false)) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O))) (\lambda n0:nat.(\lambda _:((le (S n) n0)\to (eq bool (blt n0 (S n)) false)).(\lambda H1:(le (S n) (S n0)).(H n0 (le_S_n n n0 H1))))) y)))) x))
+Post Nodes: 272
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: blt_lt
+Pre Nodes : 221
+bool
+bool
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq bool (blt y n) true)\to (lt y n)))) (\lambda y:nat.(\lambda H:(eq bool (blt y O) true). let H0 \def (eq_ind bool (blt y O) (\lambda b:bool.((eq bool b true)\to (lt y O))) (\lambda H0:(eq bool (blt y O) true). let H1 \def (eq_ind bool (blt y O) (\lambda e:bool.
+match e return (\lambda _:bool.Prop) with
+ [ true => False
+ | false => True
+]) I true H0) in (False_ind (lt y O) H1)) true H) in (H0 (refl_equal bool true)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((eq bool (blt y n) true)\to (lt y n))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((eq bool (blt n0 (S n)) true)\to (lt n0 (S n)))) (\lambda _:(eq bool true true).(le_S_n (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n))))) (\lambda n0:nat.(\lambda _:((eq bool
+match n0 return (\lambda n1:nat.bool) with
+ [ O => true
+ | (S (m:nat)) => (blt m n)
+] true)\to (lt n0 (S n))).(\lambda H1:(eq bool (blt n0 n) true).(lt_le_S (S n0) (S n) (lt_n_S n0 n (H n0 H1)))))) y)))) x))
+Post Nodes: 219
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: bge_le
+Pre Nodes : 222
+bool
+bool
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq bool (blt y n) false)\to (le n y)))) (\lambda y:nat.(\lambda _:(eq bool (blt y O) false).(le_O_n y))) (\lambda n:nat.(\lambda H:(\forall y:nat.((eq bool (blt y n) false)\to (le n y))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((eq bool (blt n0 (S n)) false)\to (le (S n) n0))) (\lambda H0:(eq bool (blt O (S n)) false). let H1 \def (eq_ind bool (blt O (S n)) (\lambda b:bool.((eq bool b false)\to (le (S n) O))) (\lambda H1:(eq bool (blt O (S n)) false). let H2 \def (eq_ind bool (blt O (S n)) (\lambda e:bool.
+match e return (\lambda _:bool.Prop) with
+ [ true => True
+ | false => False
+]) I false H1) in (False_ind (le (S n) O) H2)) false H0) in (H1 (refl_equal bool false))) (\lambda n0:nat.(\lambda _:((eq bool (blt n0 (S n)) false)\to (le (S n) n0)).(\lambda H1:(eq bool (blt (S n0) (S n)) false).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0 H1))))))) y)))) x))
+Post Nodes: 220
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of blt/props.mma completed in 7''.
+\e[0;32mInfo: \e[0mexecution of ext/arith.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext ...''
+\e[0;32mInfo: \e[0mbaseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/arith is not empty
+\e[0;32mInfo: \e[0mcleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/arith
+\e[0;32mInfo: \e[0mRemoving: cic:/matita/LAMBDA-TYPES/Base-2/ext/arith/*
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: nat_dec
+Pre Nodes : 474
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda n1:nat.(nat_ind (\lambda n:nat.(\forall n2:nat.(or (eq nat n n2) ((eq nat n n2)\to (\forall P:Prop.P))))) (\lambda n2:nat.(nat_ind (\lambda n:nat.(or (eq nat O n) ((eq nat O n)\to (\forall P:Prop.P)))) (or_introl (eq nat O O) ((eq nat O O)\to (\forall P:Prop.P)) (refl_equal nat O)) (\lambda n3:nat.(\lambda _:(or (eq nat O n3) ((eq nat O n3)\to (\forall P:Prop.P))).(or_intror (eq nat O (S n3)) ((eq nat O (S n3))\to (\forall P:Prop.P)) (\lambda H0:(eq nat O (S n3)).(\lambda P:Prop. let H1 \def (eq_ind nat O (\lambda ee:nat.
+match ee return (\lambda _:nat.Prop) with
+ [ O => True
+ | (S (_:nat)) => False
+]) I (S n3) H0) in (False_ind P H1)))))) n2)) (\lambda n2:nat.(\lambda H:(\forall n2:nat.(or (eq nat n2 n2) ((eq nat n2 n2)\to (\forall P:Prop.P)))).(\lambda n3:nat.(nat_ind (\lambda n0:nat.(or (eq nat (S n2) n0) ((eq nat (S n2) n0)\to (\forall P:Prop.P)))) (or_intror (eq nat (S n2) O) ((eq nat (S n2) O)\to (\forall P:Prop.P)) (\lambda H0:(eq nat (S n2) O).(\lambda P:Prop. let H1 \def (eq_ind nat (S n2) (\lambda ee:nat.
+match ee return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H0) in (False_ind P H1)))) (\lambda n4:nat.(\lambda H0:(or (eq nat (S n2) n4) ((eq nat (S n2) n4)\to (\forall P:Prop.P))). let DEFINED \def (H n4) in (or_ind (eq nat n2 n4) ((eq nat n2 n4)\to (\forall P:Prop.P)) (or (eq nat (S n2) (S n4)) ((eq nat (S n2) (S n4))\to (\forall P:Prop.P))) (\lambda H1:(eq nat n2 n4).(eq_ind nat n2 (\lambda n3:nat.(or (eq nat (S n2) (S n3)) ((eq nat (S n2) (S n3))\to (\forall P:Prop.P)))) (or_introl (eq nat (S n2) (S n2)) ((eq nat (S n2) (S n2))\to (\forall P:Prop.P)) (refl_equal nat (S n2))) n4 H1)) (\lambda H1:((eq nat n2 n4)\to (\forall P:Prop.P)).(or_intror (eq nat (S n2) (S n4)) ((eq nat (S n2) (S n4))\to (\forall P:Prop.P)) (\lambda H2:(eq nat (S n2) (S n4)).(\lambda P:Prop. let H3 \def (f_equal nat nat (\lambda e:nat.
+match e return (\lambda _:nat.nat) with
+ [ O => n2
+ | (S (n3:nat)) => n3
+]) (S n2) (S n4) H2) in let H4 \def (eq_ind_r nat n4 (\lambda n3:nat.((eq nat n2 n3)\to (\forall P0:Prop.P0))) H1 n2 H3) in (H4 (refl_equal nat n2) P))))) DEFINED))) n3)))) n1))
+Post Nodes: 476
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: simpl_plus_r
+Pre Nodes : 85
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda n:nat.(\lambda m:nat.(\lambda p:nat.(\lambda H:(eq nat (plus m n) (plus p n)). let DEFINED \def (plus_comm n m) in (plus_reg_l n m p (eq_ind_r nat (plus m n) (\lambda n0:nat.(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda n0:nat.(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_comm n p)) (plus m n) H) (plus n m) DEFINED))))))
+Post Nodes: 87
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: minus_plus_r
+Pre Nodes : 33
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda m:nat.(\lambda n:nat. let DEFINED \def (plus_comm m n) in (eq_ind_r nat (plus n m) (\lambda n0:nat.(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) DEFINED)))
+Post Nodes: 35
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: plus_permute_2_in_3
+Pre Nodes : 117
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda z:nat. let DEFINED \def (plus_assoc_reverse x z y) in let DEFINED0 \def (plus_comm y z) in let DEFINED1 \def (plus_assoc_reverse x y z) in (eq_ind_r nat (plus x (plus y z)) (\lambda n:nat.(eq nat n (plus (plus x z) y))) (eq_ind_r nat (plus z y) (\lambda n:nat.(eq nat (plus x n) (plus (plus x z) y))) (eq_ind nat (plus (plus x z) y) (\lambda n:nat.(eq nat n (plus (plus x z) y))) (refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) DEFINED) (plus y z) DEFINED0) (plus (plus x y) z) DEFINED1))))
+Post Nodes: 123
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: plus_permute_2_in_3_assoc
+Pre Nodes : 86
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda n:nat.(\lambda h:nat.(\lambda k:nat. let DEFINED \def (plus_assoc n k h) in let DEFINED0 \def (plus_permute_2_in_3 n h k) in (eq_ind_r nat (plus (plus n k) h) (\lambda n0:nat.(eq nat n0 (plus n (plus k h)))) (eq_ind_r nat (plus (plus n k) h) (\lambda n0:nat.(eq nat (plus (plus n k) h) n0)) (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) DEFINED) (plus (plus n h) k) DEFINED0))))
+Post Nodes: 90
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: plus_O
+Pre Nodes : 191
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((eq nat (plus n y) O)\to (and (eq nat n O) (eq nat y O))))) (\lambda y:nat.(\lambda H:(eq nat (plus O y) O).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) H))) (\lambda n:nat.(\lambda _:(\forall y:nat.((eq nat (plus n y) O)\to (and (eq nat n O) (eq nat y O)))).(\lambda y:nat.(\lambda H0:(eq nat (plus (S n) y) O). let H1 \def (eq_ind nat (plus (S n) y) (\lambda n0:nat.((eq nat n0 O)\to (and (eq nat (S n) O) (eq nat y O)))) (\lambda H1:(eq nat (plus (S n) y) O). let H2 \def (eq_ind nat (plus (S n) y) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H1) in (False_ind (and (eq nat (S n) O) (eq nat y O)) H2)) O H0) in (H1 (refl_equal nat O)))))) x))
+Post Nodes: 189
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: minus_Sx_SO
+Pre Nodes : 24
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat. let DEFINED \def (minus_n_O x) in (eq_ind nat x (\lambda n:nat.(eq nat n x)) (refl_equal nat x) (minus x O) DEFINED))
+Post Nodes: 26
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: eq_nat_dec
+Pre Nodes : 303
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda i:nat.(nat_ind (\lambda n:nat.(\forall j:nat.(or (not (eq nat n j)) (eq nat n j)))) (\lambda j:nat.(nat_ind (\lambda n:nat.(or (not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O) (refl_equal nat O)) (\lambda n:nat.(\lambda _:(or (not (eq nat O n)) (eq nat O n)).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j)) (\lambda n:nat.(\lambda H:(\forall j:nat.(or (not (eq nat n j)) (eq nat n j))).(\lambda j:nat.(nat_ind (\lambda n0:nat.(or (not (eq nat (S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda n0:nat.(\lambda _:(or (not (eq nat (S n) n0)) (eq nat (S n) n0)). let DEFINED \def (H n0) in (or_ind (not (eq nat n n0)) (eq nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda H1:(not (eq nat n n0)).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (not_eq_S n n0 H1))) (\lambda H1:(eq nat n n0).(or_intror (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) DEFINED))) j)))) i))
+Post Nodes: 305
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: neq_eq_e
+Pre Nodes : 47
+Optimized : (\lambda i:nat.(\lambda j:nat.(\lambda P:Prop.(\lambda H:((not (eq nat i j))\to P).(\lambda H0:((eq nat i j)\to P). let o \def (eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o))))))
+Post Nodes: 47
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_false
+Pre Nodes : 382
+nat
+nat
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: nested application
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+nat
+nat
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: nested application
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda m:nat.(nat_ind (\lambda n:nat.(\forall n0:nat.(\forall P:Prop.((le n n0)\to ((le (S n0) n)\to P))))) (\lambda n:nat.(\lambda P:Prop.(\lambda _:(le O n).(\lambda H0:(le (S n) O). let H1 \def (le_ind (S n) (\lambda n0:nat.((eq nat n0 O)\to P)) (\lambda H1:(eq nat (S n) O). let H2 \def (eq_ind nat (S n) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H1) in (False_ind P H2)) (\lambda m0:nat.(\lambda H1:(le (S n) m0).(\lambda _:((eq nat m0 O)\to P).(\lambda H2:(eq nat (S m0) O). let H3 \def (eq_ind nat (S m0) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H2) in let DEFINED \def (False_ind ((le (S n) m0)\to P) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O)))))) (\lambda n:nat.(\lambda H:(\forall n0:nat.(\forall P:Prop.((le n n0)\to ((le (S n0) n)\to P)))).(\lambda n0:nat.(nat_ind (\lambda n1:nat.(\forall P:Prop.((le (S n) n1)\to ((le (S n1) (S n))\to P)))) (\lambda P:Prop.(\lambda H0:(le (S n) O).(\lambda _:(le (S O) (S n)). let H2 \def (le_ind (S n) (\lambda n1:nat.((eq nat n1 O)\to P)) (\lambda H2:(eq nat (S n) O). let H3 \def (eq_ind nat (S n) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H2) in (False_ind P H3)) (\lambda m0:nat.(\lambda H2:(le (S n) m0).(\lambda _:((eq nat m0 O)\to P).(\lambda H3:(eq nat (S m0) O). let H4 \def (eq_ind nat (S m0) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H3) in let DEFINED \def (False_ind ((le (S n) m0)\to P) H4) in (DEFINED H2))))) O H0) in (H2 (refl_equal nat O))))) (\lambda n1:nat.(\lambda _:(\forall P:Prop.((le (S n) n1)\to ((le (S n1) (S n))\to P))).(\lambda P:Prop.(\lambda H1:(le (S n) (S n1)).(\lambda H2:(le (S (S n1)) (S n)). let DEFINED \def (le_S_n (S n1) n H2) in (H n1 P (le_S_n n n1 H1) DEFINED)))))) n0)))) m))
+Post Nodes: 400
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_Sx_x
+Pre Nodes : 20
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda H:(le (S x) x).(\lambda P:Prop. let H0 \def le_Sn_n in let DEFINED \def (H0 x H) in (False_ind P DEFINED))))
+Post Nodes: 22
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: minus_le
+Pre Nodes : 88
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.(le (minus n y) n))) (\lambda _:nat.(le_n O)) (\lambda n:nat.(\lambda H:(\forall y:nat.(le (minus n y) n)).(\lambda y:nat.(nat_ind (\lambda n0:nat.(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda n0:nat.(\lambda _:(le
+match n0 return (\lambda n1:nat.nat) with
+ [ O => (S n)
+ | (S (l:nat)) => (minus n l)
+] (S n)).(le_S (minus n n0) n (H n0)))) y)))) x))
+Post Nodes: 88
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_plus_minus_sym
+Pre Nodes : 45
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda n:nat.(\lambda m:nat.(\lambda H:(le n m). let DEFINED \def (plus_comm (minus m n) n) in (eq_ind_r nat (plus n (minus m n)) (\lambda n0:nat.(eq nat m n0)) (le_plus_minus n m H) (plus (minus m n) n) DEFINED))))
+Post Nodes: 47
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_minus_minus
+Pre Nodes : 84
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(le x y).(\lambda z:nat.(\lambda H0:(le y z). let DEFINED \def (le_plus_minus_r x z (le_trans x y z H H0)) in let DEFINED0 \def (le_plus_minus_r x y H) in (plus_le_reg_l x (minus y x) (minus z x) (eq_ind_r nat y (\lambda n:nat.(le n (plus x (minus z x)))) (eq_ind_r nat z (\lambda n:nat.(le y n)) H0 (plus x (minus z x)) DEFINED) (plus x (minus y x)) DEFINED0)))))))
+Post Nodes: 88
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_minus_plus
+Pre Nodes : 505
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+nat
+nat
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: nested application
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x:nat.((le n x)\to (\forall y:nat.(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) (\lambda x:nat.(\lambda H:(le O x). let H0 \def (le_ind O (\lambda n:nat.((eq nat n x)\to (\forall y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))))) (\lambda H0:(eq nat O x).(eq_ind nat O (\lambda n:nat.(\forall y:nat.(eq nat (minus (plus n y) O) (plus (minus n O) y)))) (\lambda y:nat.(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) (minus_n_O (plus O y)))) x H0)) (\lambda m:nat.(\lambda H0:(le O m).(\lambda _:((eq nat m x)\to (\forall y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y)))).(\lambda H1:(eq nat (S m) x). let DEFINED \def (eq_ind nat (S m) (\lambda n:nat.((le O m)\to (\forall y:nat.(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda _:(le O m).(\lambda y:nat.(refl_equal nat (plus (minus (S m) O) y)))) x H1) in (DEFINED H0))))) x H) in (H0 (refl_equal nat x)))) (\lambda z0:nat.(\lambda H:(\forall x:nat.((le z0 x)\to (\forall y:nat.(eq nat (minus (plus x y) z0) (plus (minus x z0) y))))).(\lambda x:nat.(nat_ind (\lambda n:nat.((le (S z0) n)\to (\forall y:nat.(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y))))) (\lambda H0:(le (S z0) O).(\lambda y:nat. let H1 \def (le_ind (S z0) (\lambda n:nat.((eq nat n O)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)))) (\lambda H1:(eq nat (S z0) O). let H2 \def (eq_ind nat (S z0) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H1) in (False_ind (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2)) (\lambda m:nat.(\lambda H1:(le (S z0) m).(\lambda _:((eq nat m O)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))).(\lambda H2:(eq nat (S m) O). let H3 \def (eq_ind nat (S m) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H2) in let DEFINED \def (False_ind ((le (S z0) m)\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3) in (DEFINED H1))))) O H0) in (H1 (refl_equal nat O)))) (\lambda n:nat.(\lambda _:((le (S z0) n)\to (\forall y:nat.(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y)))).(\lambda H1:(le (S z0) (S n)).(\lambda y:nat.(H n (le_S_n z0 n H1) y))))) x)))) z))
+Post Nodes: 560
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_minus
+Pre Nodes : 51
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda z:nat.(\lambda y:nat.(\lambda H:(le (plus x y) z). let DEFINED \def (minus_plus_r x y) in (eq_ind nat (minus (plus x y) y) (\lambda n:nat.(le n (minus z y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x DEFINED)))))
+Post Nodes: 53
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_trans_plus_r
+Pre Nodes : 27
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda z:nat.(\lambda H:(le (plus x y) z).(le_trans y (plus x y) z (le_plus_r x y) H)))))
+Post Nodes: 27
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_gen_S
+Pre Nodes : 217
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+Optimized : (\lambda m:nat.(\lambda x:nat.(\lambda H:(le (S m) x). let H0 \def (le_ind (S m) (\lambda n:nat.((eq nat n x)\to (ex2 nat (\lambda n0:nat.(eq nat x (S n0))) (\lambda n0:nat.(le m n0))))) (\lambda H0:(eq nat (S m) x).(eq_ind nat (S m) (\lambda n:nat.(ex2 nat (\lambda n0:nat.(eq nat n (S n0))) (\lambda n0:nat.(le m n0)))) (ex_intro2 nat (\lambda n:nat.(eq nat (S m) (S n))) (\lambda n:nat.(le m n)) m (refl_equal nat (S m)) (le_n m)) x H0)) (\lambda m0:nat.(\lambda H0:(le (S m) m0).(\lambda _:((eq nat m0 x)\to (ex2 nat (\lambda n0:nat.(eq nat x (S n0))) (\lambda n0:nat.(le m n0)))).(\lambda H1:(eq nat (S m0) x). let DEFINED \def (eq_ind nat (S m0) (\lambda n:nat.((le (S m) m0)\to (ex2 nat (\lambda n0:nat.(eq nat n (S n0))) (\lambda n0:nat.(le m n0))))) (\lambda H2:(le (S m) m0).(ex_intro2 nat (\lambda n:nat.(eq nat (S m0) (S n))) (\lambda n:nat.(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) x H1) in (DEFINED H0))))) x H) in (H0 (refl_equal nat x)))))
+Post Nodes: 243
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_x_plus_x_Sy
+Pre Nodes : 64
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda y:nat. let DEFINED \def (plus_comm x (S y)) in (eq_ind_r nat (plus (S y) x) (\lambda n:nat.(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) DEFINED)))
+Post Nodes: 66
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: simpl_lt_plus_r
+Pre Nodes : 75
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda p:nat.(\lambda n:nat.(\lambda m:nat.(\lambda H:(lt (plus n p) (plus m p)). let DEFINED \def (plus_comm n p) in let H0 \def (eq_ind nat (plus n p) (\lambda n0:nat.(lt n0 (plus m p))) H (plus p n) DEFINED) in let DEFINED0 \def (plus_comm m p) in let H1 \def (eq_ind nat (plus m p) (\lambda n0:nat.(lt (plus p n) n0)) H0 (plus p m) DEFINED0) in (plus_lt_reg_l n m p H1)))))
+Post Nodes: 79
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: minus_x_Sy
+Pre Nodes : 330
+nat
+nat
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: nested application
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y))))))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq nat (minus O y) (S (minus O (S y)))))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H0) in (False_ind (eq nat (minus O y) (S (minus O (S y)))) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq nat (minus O y) (S (minus O (S y))))).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq nat (minus O y) (S (minus O (S y))))) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y)))))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda _:(lt O (S n)). let DEFINED \def (minus_n_O n) in (eq_ind nat n (\lambda n0:nat.(eq nat (S n) (S n0))) (refl_equal nat (S n)) (minus n O) DEFINED)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))).(\lambda H1:(lt (S n0) (S n)). let H2 \def (le_S_n (S n0) n H1) in (H n0 H2)))) y)))) x))
+Post Nodes: 354
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_plus_minus
+Pre Nodes : 16
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y).(le_plus_minus (S x) y H))))
+Post Nodes: 16
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_plus_minus_r
+Pre Nodes : 53
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y). let DEFINED \def (plus_comm (minus y (S x)) x) in (eq_ind_r nat (plus x (minus y (S x))) (\lambda n:nat.(eq nat y (S n))) (lt_plus_minus x y H) (plus (minus y (S x)) x) DEFINED))))
+Post Nodes: 55
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: minus_x_SO
+Pre Nodes : 56
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda H:(lt O x). let DEFINED \def (minus_n_O x) in let DEFINED0 \def (minus_x_Sy x O H) in (eq_ind nat (minus x O) (\lambda n:nat.(eq nat x n)) (eq_ind nat x (\lambda n:nat.(eq nat x n)) (refl_equal nat x) (minus x O) DEFINED) (S (minus x (S O))) DEFINED0)))
+Post Nodes: 60
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_x_pred_y
+Pre Nodes : 175
+nat
+nat
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: nested application
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+Optimized : (\lambda y:nat.(nat_ind (\lambda n:nat.(\forall x:nat.((lt x n)\to (le x (pred n))))) (\lambda x:nat.(\lambda H:(lt x O). let H0 \def (le_ind (S x) (\lambda n:nat.((eq nat n O)\to (le x O))) (\lambda H0:(eq nat (S x) O). let H1 \def (eq_ind nat (S x) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H0) in (False_ind (le x O) H1)) (\lambda m:nat.(\lambda H0:(le (S x) m).(\lambda _:((eq nat m O)\to (le x O)).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H1) in let DEFINED \def (False_ind ((le (S x) m)\to (le x O)) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda _:(\forall x:nat.((lt x n)\to (le x (pred n)))).(\lambda x:nat.(\lambda H0:(lt x (S n)).(le_S_n x n H0))))) y))
+Post Nodes: 186
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_le_minus
+Pre Nodes : 44
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y). let DEFINED \def (plus_comm x (S O)) in (le_minus x y (S O) (eq_ind_r nat (plus (S O) x) (\lambda n:nat.(le n y)) H (plus x (S O)) DEFINED)))))
+Post Nodes: 46
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_le_e
+Pre Nodes : 39
+Optimized : (\lambda n:nat.(\lambda d:nat.(\lambda P:Prop.(\lambda H:((lt n d)\to P).(\lambda H0:((le d n)\to P). let H1 \def (le_or_lt d n) in (or_ind (le d n) (lt n d) P H0 H H1))))))
+Post Nodes: 39
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_eq_e
+Pre Nodes : 45
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda P:Prop.(\lambda H:((lt x y)\to P).(\lambda H0:((eq nat x y)\to P).(\lambda H1:(le x y). let DEFINED \def (le_lt_or_eq x y H1) in (or_ind (lt x y) (eq nat x y) P H H0 DEFINED)))))))
+Post Nodes: 47
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_eq_gt_e
+Pre Nodes : 60
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda P:Prop.(\lambda H:((lt x y)\to P).(\lambda H0:((eq nat x y)\to P).(\lambda H1:((lt y x)\to P).(lt_le_e x y P H (\lambda H2:(le y x).(lt_eq_e y x P H1 (\lambda H3:(eq nat y x).(H0 (sym_eq nat y x H3))) H2)))))))))
+Post Nodes: 60
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_gen_xS
+Pre Nodes : 190
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall n0:nat.((lt n (S n0))\to (or (eq nat n O) (ex2 nat (\lambda m:nat.(eq nat n (S m))) (\lambda m:nat.(lt m n0))))))) (\lambda n:nat.(\lambda _:(lt O (S n)).(or_introl (eq nat O O) (ex2 nat (\lambda m:nat.(eq nat O (S m))) (\lambda m:nat.(lt m n))) (refl_equal nat O)))) (\lambda n:nat.(\lambda _:(\forall n0:nat.((lt n (S n0))\to (or (eq nat n O) (ex2 nat (\lambda m:nat.(eq nat n (S m))) (\lambda m:nat.(lt m n0)))))).(\lambda n0:nat.(\lambda H0:(lt (S n) (S n0)).(or_intror (eq nat (S n) O) (ex2 nat (\lambda m:nat.(eq nat (S n) (S m))) (\lambda m:nat.(lt m n0))) (ex_intro2 nat (\lambda m:nat.(eq nat (S n) (S m))) (\lambda m:nat.(lt m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x))
+Post Nodes: 190
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_lt_false
+Pre Nodes : 25
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(le x y).(\lambda H0:(lt y x).(\lambda P:Prop. let DEFINED \def (le_not_lt x y H H0) in (False_ind P DEFINED))))))
+Post Nodes: 27
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: lt_neq
+Pre Nodes : 33
+Optimized : (\lambda x:nat.(\lambda y:nat.(\lambda H:(lt x y).(\lambda H0:(eq nat x y). let H1 \def (eq_ind nat x (\lambda n:nat.(lt n y)) H y H0) in (lt_irrefl y H1)))))
+Post Nodes: 33
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: arith0
+Pre Nodes : 185
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda h2:nat.(\lambda d2:nat.(\lambda n:nat.(\lambda H:(le (plus d2 h2) n).(\lambda h3:nat. let DEFINED \def (plus_comm h2 d2) in let DEFINED0 \def (plus_assoc h2 d2 h3) in let DEFINED1 \def (minus_plus h2 (plus d2 h3)) in (eq_ind nat (minus (plus h2 (plus d2 h3)) h2) (\lambda n0:nat.(le n0 (minus (plus n h3) h2))) (le_minus_minus h2 (plus h2 (plus d2 h3)) (le_plus_l h2 (plus d2 h3)) (plus n h3) (eq_ind_r nat (plus (plus h2 d2) h3) (\lambda n0:nat.(le n0 (plus n h3))) (eq_ind_r nat (plus d2 h2) (\lambda n0:nat.(le (plus n0 h3) (plus n h3))) (le_S_n (plus (plus d2 h2) h3) (plus n h3) (lt_le_S (plus (plus d2 h2) h3) (S (plus n h3)) (le_lt_n_Sm (plus (plus d2 h2) h3) (plus n h3) (plus_le_compat (plus d2 h2) n h3 h3 H (le_n h3))))) (plus h2 d2) DEFINED) (plus h2 (plus d2 h3)) DEFINED0)) (plus d2 h3) DEFINED1))))))
+Post Nodes: 191
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: O_minus
+Pre Nodes : 211
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le n y)\to (eq nat (minus n y) O)))) (\lambda y:nat.(\lambda _:(le O y).(refl_equal nat O))) (\lambda x0:nat.(\lambda H:(\forall y:nat.((le x0 y)\to (eq nat (minus x0 y) O))).(\lambda y:nat.(nat_ind (\lambda n:nat.((le (S x0) n)\to (eq nat
+match n return (\lambda n1:nat.nat) with
+ [ O => (S x0)
+ | (S (l:nat)) => (minus x0 l)
+] O))) (\lambda H0:(le (S x0) O). let DEFINED \def (le_gen_S x0 O H0) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le x0 n)) (eq nat (S x0) O) (\lambda x1:nat.(\lambda H1:(eq nat O (S x1)).(\lambda _:(le x0 x1). let H3 \def (eq_ind nat O (\lambda ee:nat.
+match ee return (\lambda _:nat.Prop) with
+ [ O => True
+ | (S (_:nat)) => False
+]) I (S x1) H1) in (False_ind (eq nat (S x0) O) H3)))) DEFINED)) (\lambda n:nat.(\lambda _:((le (S x0) n)\to (eq nat
+match n return (\lambda n1:nat.nat) with
+ [ O => (S x0)
+ | (S (l:nat)) => (minus x0 l)
+] O)).(\lambda H1:(le (S x0) (S n)).(H n (le_S_n x0 n H1))))) y)))) x))
+Post Nodes: 213
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: minus_minus
+Pre Nodes : 592
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x:nat.(\forall y:nat.((le n x)\to ((le n y)\to ((eq nat (minus x n) (minus y n))\to (eq nat x y))))))) (\lambda x:nat.(\lambda y:nat.(\lambda _:(le O x).(\lambda _:(le O y).(\lambda H1:(eq nat (minus x O) (minus y O)). let DEFINED \def (minus_n_O x) in let H2 \def (eq_ind_r nat (minus x O) (\lambda n:nat.(eq nat n (minus y O))) H1 x DEFINED) in let DEFINED0 \def (minus_n_O y) in let H3 \def (eq_ind_r nat (minus y O) (\lambda n:nat.(eq nat x n)) H2 y DEFINED0) in H3))))) (\lambda z0:nat.(\lambda IH:(\forall x:nat.(\forall y:nat.((le z0 x)\to ((le z0 y)\to ((eq nat (minus x z0) (minus y z0))\to (eq nat x y)))))).(\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((le (S z0) n)\to ((le (S z0) y)\to ((eq nat (minus n (S z0)) (minus y (S z0)))\to (eq nat n y)))))) (\lambda y:nat.(\lambda H:(le (S z0) O).(\lambda _:(le (S z0) y).(\lambda _:(eq nat (minus O (S z0)) (minus y (S z0))). let DEFINED \def (le_gen_S z0 O H) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le z0 n)) (eq nat O y) (\lambda x0:nat.(\lambda H2:(eq nat O (S x0)).(\lambda _:(le z0 x0). let H4 \def (eq_ind nat O (\lambda ee:nat.
+match ee return (\lambda _:nat.Prop) with
+ [ O => True
+ | (S (_:nat)) => False
+]) I (S x0) H2) in (False_ind (eq nat O y) H4)))) DEFINED))))) (\lambda x0:nat.(\lambda _:(\forall y:nat.((le (S z0) x0)\to ((le (S z0) y)\to ((eq nat (minus x0 (S z0)) (minus y (S z0)))\to (eq nat x0 y))))).(\lambda y:nat.(nat_ind (\lambda n:nat.((le (S z0) (S x0))\to ((le (S z0) n)\to ((eq nat (minus (S x0) (S z0)) (minus n (S z0)))\to (eq nat (S x0) n))))) (\lambda _:(le (S z0) (S x0)).(\lambda H0:(le (S z0) O).(\lambda _:(eq nat (minus (S x0) (S z0)) (minus O (S z0))). let DEFINED \def (le_gen_S z0 O H0) in (ex2_ind nat (\lambda n:nat.(eq nat O (S n))) (\lambda n:nat.(le z0 n)) (eq nat (S x0) O) (\lambda x1:nat.(\lambda H2:(eq nat O (S x1)).(\lambda _:(le z0 x1). let H4 \def (eq_ind nat O (\lambda ee:nat.
+match ee return (\lambda _:nat.Prop) with
+ [ O => True
+ | (S (_:nat)) => False
+]) I (S x1) H2) in (False_ind (eq nat (S x0) O) H4)))) DEFINED)))) (\lambda y0:nat.(\lambda _:((le (S z0) (S x0))\to ((le (S z0) y0)\to ((eq nat (minus (S x0) (S z0)) (minus y0 (S z0)))\to (eq nat (S x0) y0)))).(\lambda H:(le (S z0) (S x0)).(\lambda H0:(le (S z0) (S y0)).(\lambda H1:(eq nat (minus (S x0) (S z0)) (minus (S y0) (S z0))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z))
+Post Nodes: 600
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: plus_plus
+Pre Nodes : 1222
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+\e[0;33mWarn: \e[0mOptimizer: swap 1
+Optimized : (\lambda z:nat.(nat_ind (\lambda n:nat.(\forall x1:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le x1 n)\to ((le x2 n)\to ((eq nat (plus (minus n x1) y1) (plus (minus n x2) y2))\to (eq nat (plus x1 y2) (plus x2 y1)))))))))) (\lambda x1:nat.(\lambda x2:nat.(\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le x1 O).(\lambda H0:(le x2 O).(\lambda H1:(eq nat y1 y2). let H_y \def (le_n_O_eq x2 H0) in let H_y0 \def (le_n_O_eq x1 H) in (eq_ind nat y1 (\lambda n:nat.(eq nat (plus x1 n) (plus x2 y1))) (eq_ind nat O (\lambda n:nat.(eq nat (plus x1 y1) (plus n y1))) (eq_ind nat O (\lambda n:nat.(eq nat (plus n y1) (plus O y1))) (refl_equal nat (plus O y1)) x1 H_y0) x2 H_y) y2 H1)))))))) (\lambda z0:nat.(\lambda IH:(\forall x1:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le x1 z0)\to ((le x2 z0)\to ((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2))\to (eq nat (plus x1 y2) (plus x2 y1))))))))).(\lambda x1:nat.(nat_ind (\lambda n:nat.(\forall x2:nat.(\forall y1:nat.(\forall y2:nat.((le n (S z0))\to ((le x2 (S z0))\to ((eq nat (plus (minus (S z0) n) y1) (plus (minus (S z0) x2) y2))\to (eq nat (plus n y2) (plus x2 y1))))))))) (\lambda x2:nat.(nat_ind (\lambda n:nat.(\forall y1:nat.(\forall y2:nat.((le O (S z0))\to ((le n (S z0))\to ((eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) n) y2))\to (eq nat (plus O y2) (plus n y1)))))))) (\lambda y1:nat.(\lambda y2:nat.(\lambda _:(le O (S z0)).(\lambda _:(le O (S z0)).(\lambda H1:(eq nat (S (plus z0 y1)) (S (plus z0 y2))). let H_y \def (IH O O) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.(\forall y3:nat.(\forall y4:nat.((le O z0)\to ((le O z0)\to ((eq nat (plus n y3) (plus n y4))\to (eq nat y4 y3))))))) H_y z0 DEFINED) in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (H2 (plus z0 y2) (plus z0 y1) (le_O_n z0) (le_O_n z0) (f_equal nat nat (plus z0) (plus z0 y2) (plus z0 y1) (sym_eq nat (plus z0 y1) (plus z0 y2) (eq_add_S (plus z0 y1) (plus z0 y2) H1)))))))))) (\lambda x3:nat.(\lambda _:(\forall y1:nat.(\forall y2:nat.((le O (S z0))\to ((le x3 (S z0))\to ((eq nat (S (plus z0 y1)) (plus
+match x3 return (\lambda n:nat.nat) with
+ [ O => (S z0)
+ | (S (l:nat)) => (minus z0 l)
+] y2))\to (eq nat y2 (plus x3 y1))))))).(\lambda y1:nat.(\lambda y2:nat.(\lambda _:(le O (S z0)).(\lambda H0:(le (S x3) (S z0)).(\lambda H1:(eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2)). let H_y \def (IH O x3 (S y1)) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat (plus n (S y1)) (plus (minus z0 x3) y3))\to (eq nat y3 (plus x3 (S y1)))))))) H_y z0 DEFINED) in let DEFINED0 \def (plus_n_Sm z0 y1) in let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat n (plus (minus z0 x3) y3))\to (eq nat y3 (plus x3 (S y1)))))))) H2 (S (plus z0 y1)) DEFINED0) in let DEFINED1 \def (plus_n_Sm x3 y1) in let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda n:nat.(\forall y3:nat.((le O z0)\to ((le x3 z0)\to ((eq nat (S (plus z0 y1)) (plus (minus z0 x3) y3))\to (eq nat y3 n)))))) H3 (S (plus x3 y1)) DEFINED1) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1)))))))) x2)) (\lambda x2:nat.(\lambda _:(\forall x3:nat.(\forall y1:nat.(\forall y2:nat.((le x2 (S z0))\to ((le x3 (S z0))\to ((eq nat (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2))\to (eq nat (plus x2 y2) (plus x3 y1)))))))).(\lambda x3:nat.(nat_ind (\lambda n:nat.(\forall y1:nat.(\forall y2:nat.((le (S x2) (S z0))\to ((le n (S z0))\to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2))\to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le (S x2) (S z0)).(\lambda _:(le O (S z0)).(\lambda H1:(eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))). let H_y \def (IH x2 O y1 (S y2)) in let DEFINED \def (minus_n_O z0) in let H2 \def (eq_ind_r nat (minus z0 O) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) (plus n (S y2)))\to (eq nat (plus x2 (S y2)) y1))))) H_y z0 DEFINED) in let DEFINED0 \def (plus_n_Sm z0 y2) in let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) n)\to (eq nat (plus x2 (S y2)) y1))))) H2 (S (plus z0 y2)) DEFINED0) in let DEFINED1 \def (plus_n_Sm x2 y2) in let H4 \def (eq_ind_r nat (plus x2 (S y2)) (\lambda n:nat.((le x2 z0)\to ((le O z0)\to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))\to (eq nat n y1))))) H3 (S (plus x2 y2)) DEFINED1) in (H4 (le_S_n x2 z0 H) (le_O_n z0) H1)))))) (\lambda x4:nat.(\lambda _:(\forall y1:nat.(\forall y2:nat.((le (S x2) (S z0))\to ((le x4 (S z0))\to ((eq nat (plus (minus z0 x2) y1) (plus
+match x4 return (\lambda n:nat.nat) with
+ [ O => (S z0)
+ | (S (l:nat)) => (minus z0 l)
+] y2))\to (eq nat (S (plus x2 y2)) (plus x4 y1))))))).(\lambda y1:nat.(\lambda y2:nat.(\lambda H:(le (S x2) (S z0)).(\lambda H0:(le (S x4) (S z0)).(\lambda H1:(eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4) y2)).(f_equal nat nat S (plus x2 y2) (plus x4 y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3)))) x1)))) z))
+Post Nodes: 1236
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: le_S_minus
+Pre Nodes : 41
+\e[0;33mWarn: \e[0mOptimizer: remove 1
+Optimized : (\lambda d:nat.(\lambda h:nat.(\lambda n:nat.(\lambda H:(le (plus d h) n).(le_S d (minus n h) (le_minus d n h H))))))
+Post Nodes: 27
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/arith.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of ext/arith.mma completed in 44''.
+\e[0;32mInfo: \e[0mexecution of ext/tactics.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext ...''
+\e[0;32mInfo: \e[0mbaseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics is not empty
+\e[0;32mInfo: \e[0mcleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics
+\e[0;32mInfo: \e[0mRemoving: cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics/*
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: insert_eq
+Pre Nodes : 36
+Optimized : (\lambda S:Set.(\lambda x:S.(\lambda P:(S\to Prop).(\lambda G:Prop.(\lambda H:(\forall y:S.((P y)\to ((eq S y x)\to G))).(\lambda H0:(P x).(H x H0 (refl_equal S x))))))))
+Post Nodes: 36
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: unintro
+Pre Nodes : 17
+Optimized : (\lambda A:Set.(\lambda a:A.(\lambda P:(A\to Prop).(\lambda H:(\forall x:A.(P x)).(H a)))))
+Post Nodes: 17
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: xinduction
+Pre Nodes : 27
+Optimized : (\lambda A:Set.(\lambda t:A.(\lambda P:(A\to Prop).(\lambda H:(\forall x:A.((eq A t x)\to (P x))).(H t (refl_equal A t))))))
+Post Nodes: 27
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/tactics.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of ext/tactics.mma completed in 4''.
+\e[0;32mInfo: \e[0mexecution of pippo.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pip ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: minus_x_Sy
+Pre Nodes : 330
+nat
+nat
+nat
+nat
+\e[0;33mWarn: \e[0mOptimizer: remove 3
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: nested application
+\e[0;33mWarn: \e[0mOptimizer: anticipate 2
+\e[0;33mWarn: \e[0mOptimizer: swap 2
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda x:nat.(nat_ind (\lambda n:nat.(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y))))))) (\lambda y:nat.(\lambda H:(lt y O). let H0 \def (le_ind (S y) (\lambda n:nat.((eq nat n O)\to (eq nat (minus O y) (S (minus O (S y)))))) (\lambda H0:(eq nat (S y) O). let H1 \def (eq_ind nat (S y) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H0) in (False_ind (eq nat (minus O y) (S (minus O (S y)))) H1)) (\lambda m:nat.(\lambda H0:(le (S y) m).(\lambda _:((eq nat m O)\to (eq nat (minus O y) (S (minus O (S y))))).(\lambda H1:(eq nat (S m) O). let H2 \def (eq_ind nat (S m) (\lambda e:nat.
+match e return (\lambda _:nat.Prop) with
+ [ O => False
+ | (S (_:nat)) => True
+]) I O H1) in let DEFINED \def (False_ind ((le (S y) m)\to (eq nat (minus O y) (S (minus O (S y))))) H2) in (DEFINED H0))))) O H) in (H0 (refl_equal nat O)))) (\lambda n:nat.(\lambda H:(\forall y:nat.((lt y n)\to (eq nat (minus n y) (S (minus n (S y)))))).(\lambda y:nat.(nat_ind (\lambda n0:nat.((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda _:(lt O (S n)). let DEFINED \def (minus_n_O n) in (eq_ind nat n (\lambda n0:nat.(eq nat (S n) (S n0))) (refl_equal nat (S n)) (minus n O) DEFINED)) (\lambda n0:nat.(\lambda _:((lt n0 (S n))\to (eq nat (minus (S n) n0) (S (minus (S n) (S n0))))).(\lambda H1:(lt (S n0) (S n)). let H2 \def (le_S_n (S n0) n H1) in (H n0 H2)))) y)))) x))
+Post Nodes: 354
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./pippo.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of pippo.mma completed in 2''.
+\e[0;32mInfo: \e[0mexecution of plist/defs.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pli ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of plist/defs.mma completed in 1''.
+\e[0;32mInfo: \e[0mexecution of plist/props.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/pli ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/plist/def ...''
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: papp_ss
+Pre Nodes : 121
+\e[0;33mWarn: \e[0mOptimizer: anticipate 3
+\e[0;33mWarn: \e[0mOptimizer: swap 3
+Optimized : (\lambda is1:PList.(PList_ind (\lambda p:PList.(\forall is2:PList.(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2))))) (\lambda is2:PList.(refl_equal PList (Ss is2))) (\lambda n:nat.(\lambda n0:nat.(\lambda p:PList.(\lambda H:(\forall is2:PList.(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2)))).(\lambda is2:PList. let DEFINED \def (H is2) in (eq_ind_r PList (Ss (papp p is2)) (\lambda p0:PList.(eq PList (PCons n (S n0) p0) (PCons n (S n0) (Ss (papp p is2))))) (refl_equal PList (PCons n (S n0) (Ss (papp p is2)))) (papp (Ss p) (Ss is2)) DEFINED)))))) is1))
+Post Nodes: 123
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of plist/props.mma completed in 2''.
+\e[0;32mInfo: \e[0mexecution of types/defs.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/typ ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./preamble.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/preamble" ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/defs.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of types/defs.mma completed in 0''.
+\e[0;32mInfo: \e[0mexecution of types/props.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/typ ...''
+\e[0;32mInfo: \e[0mbaseuri cic:/matita/LAMBDA-TYPES/Base-2/types/props is not empty
+\e[0;32mInfo: \e[0mcleaning baseuri cic:/matita/LAMBDA-TYPES/Base-2/types/props
+\e[0;32mInfo: \e[0mRemoving: cic:/matita/LAMBDA-TYPES/Base-2/types/props/*
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/defs.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/types/def ...''
+\e[0;34mDebug: \e[0mExecuting: ``inline procedural "cic:/matita/LAMBDA-TYPES/Base-1 ...''
+BEGIN: ex2_sym
+Pre Nodes : 77
+Optimized : (\lambda A:Set.(\lambda P:(A\to Prop).(\lambda Q:(A\to Prop).(\lambda H:(ex2 A (\lambda x:A.(P x)) (\lambda x:A.(Q x))).(ex2_ind A (\lambda x:A.(P x)) (\lambda x:A.(Q x)) (ex2 A (\lambda x:A.(Q x)) (\lambda x:A.(P x))) (\lambda x:A.(\lambda H0:(P x).(\lambda H1:(Q x).(ex_intro2 A (\lambda x0:A.(Q x0)) (\lambda x0:A.(P x0)) x H1 H0)))) H)))))
+Post Nodes: 77
+\e[0;34mDebug: \e[0mProcedural: level 2 transformation
+\e[0;34mDebug: \e[0mProcedural: grafite rendering
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/props.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of types/props.mma completed in 2''.
+\e[0;32mInfo: \e[0mexecution of theory.mma started:
+\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/the ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/tactics.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/ext/tacti ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./ext/arith.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./types/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/types/pro ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./blt/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/blt/props ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./plist/props.ma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;34mDebug: \e[0mExecuting: ``include "cic:/matita/LAMBDA-TYPES/Base-2/plist/pro ...''
+\e[0;34mDebug: \e[0mIncluding /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/./theory.mma with path: /home/fguidi/svn/software/matita/contribs/LAMBDA-TYPES/Base-2/.
+\e[0;32mInfo: \e[0mexecution of theory.mma completed in 1''.
-baseuri=cic:/matita/LAMBDA-TYPES/Base-1
-include_paths= ../../../legacy
+baseuri=cic:/matita/LAMBDA-TYPES
+include_paths= ../../legacy
projects / helm.git / commitdiff