From: Ferruccio Guidi Date: Wed, 4 Feb 2015 16:55:03 +0000 (+0000) Subject: - matitac: now directories are allowed as command line arguments X-Git-Tag: make_still_working~753 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=538c5526a6b3c3af44f92c9cc67d82f28995da96;p=helm.git - matitac: now directories are allowed as command line arguments all .ma files inside these directories are compiled - basic_1: commit os sections tlt iso --- diff --git a/matita/matita/contribs/lambdadelta/basic_1/iso/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/iso/defs.ma index 202b8a300..54a5e01fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/iso/defs.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/iso/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/T/defs.ma". +include "basic_1/T/defs.ma". inductive iso: T \to (T \to Prop) \def | iso_sort: \forall (n1: nat).(\forall (n2: nat).(iso (TSort n1) (TSort n2))) diff --git a/matita/matita/contribs/lambdadelta/basic_1/iso/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/iso/fwd.ma index 761e982f7..40917f7b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/iso/fwd.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/iso/fwd.ma @@ -14,67 +14,100 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/iso/defs.ma". +include "basic_1/iso/defs.ma". -include "Basic-1/tlist/defs.ma". +include "basic_1/tlist/defs.ma". + +theorem iso_ind: + \forall (P: ((T \to (T \to Prop)))).(((\forall (n1: nat).(\forall (n2: +nat).(P (TSort n1) (TSort n2))))) \to (((\forall (i1: nat).(\forall (i2: +nat).(P (TLRef i1) (TLRef i2))))) \to (((\forall (v1: T).(\forall (v2: +T).(\forall (t1: T).(\forall (t2: T).(\forall (k: K).(P (THead k v1 t1) +(THead k v2 t2)))))))) \to (\forall (t: T).(\forall (t0: T).((iso t t0) \to +(P t t0))))))) +\def + \lambda (P: ((T \to (T \to Prop)))).(\lambda (f: ((\forall (n1: +nat).(\forall (n2: nat).(P (TSort n1) (TSort n2)))))).(\lambda (f0: ((\forall +(i1: nat).(\forall (i2: nat).(P (TLRef i1) (TLRef i2)))))).(\lambda (f1: +((\forall (v1: T).(\forall (v2: T).(\forall (t1: T).(\forall (t2: T).(\forall +(k: K).(P (THead k v1 t1) (THead k v2 t2))))))))).(\lambda (t: T).(\lambda +(t0: T).(\lambda (i: (iso t t0)).(match i with [(iso_sort x x0) \Rightarrow +(f x x0) | (iso_lref x x0) \Rightarrow (f0 x x0) | (iso_head x x0 x1 x2 x3) +\Rightarrow (f1 x x0 x1 x2 x3)]))))))). theorem iso_gen_sort: \forall (u2: T).(\forall (n1: nat).((iso (TSort n1) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 (TSort n2)))))) \def - \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TSort n1) -u2)).(insert_eq T (TSort n1) (\lambda (t: T).(iso t u2)) (\lambda (_: T).(ex -nat (\lambda (n2: nat).(eq T u2 (TSort n2))))) (\lambda (y: T).(\lambda (H0: -(iso y u2)).(iso_ind (\lambda (t: T).(\lambda (t0: T).((eq T t (TSort n1)) -\to (ex nat (\lambda (n2: nat).(eq T t0 (TSort n2))))))) (\lambda (n0: -nat).(\lambda (n2: nat).(\lambda (H1: (eq T (TSort n0) (TSort n1))).(let H2 -\def (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) -with [(TSort n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _ _) -\Rightarrow n0])) (TSort n0) (TSort n1) H1) in (ex_intro nat (\lambda (n3: -nat).(eq T (TSort n2) (TSort n3))) n2 (refl_equal T (TSort n2))))))) (\lambda -(i1: nat).(\lambda (i2: nat).(\lambda (H1: (eq T (TLRef i1) (TSort n1))).(let -H2 \def (eq_ind T (TLRef i1) (\lambda (ee: T).(match ee in T return (\lambda -(_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | -(THead _ _ _) \Rightarrow False])) I (TSort n1) H1) in (False_ind (ex nat -(\lambda (n2: nat).(eq T (TLRef i2) (TSort n2)))) H2))))) (\lambda (v1: -T).(\lambda (v2: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (k: -K).(\lambda (H1: (eq T (THead k v1 t1) (TSort n1))).(let H2 \def (eq_ind T -(THead k v1 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) -with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ -_) \Rightarrow True])) I (TSort n1) H1) in (False_ind (ex nat (\lambda (n2: -nat).(eq T (THead k v2 t2) (TSort n2)))) H2)))))))) y u2 H0))) H))). -(* COMMENTS -Initial nodes: 321 -END *) + \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TSort n1) u2)).(let +TMP_1 \def (TSort n1) in (let TMP_2 \def (\lambda (t: T).(iso t u2)) in (let +TMP_5 \def (\lambda (_: T).(let TMP_4 \def (\lambda (n2: nat).(let TMP_3 \def +(TSort n2) in (eq T u2 TMP_3))) in (ex nat TMP_4))) in (let TMP_34 \def +(\lambda (y: T).(\lambda (H0: (iso y u2)).(let TMP_8 \def (\lambda (t: +T).(\lambda (t0: T).((eq T t (TSort n1)) \to (let TMP_7 \def (\lambda (n2: +nat).(let TMP_6 \def (TSort n2) in (eq T t0 TMP_6))) in (ex nat TMP_7))))) in +(let TMP_17 \def (\lambda (n0: nat).(\lambda (n2: nat).(\lambda (H1: (eq T +(TSort n0) (TSort n1))).(let TMP_9 \def (\lambda (e: T).(match e with [(TSort +n) \Rightarrow n | (TLRef _) \Rightarrow n0 | (THead _ _ _) \Rightarrow n0])) +in (let TMP_10 \def (TSort n0) in (let TMP_11 \def (TSort n1) in (let H2 \def +(f_equal T nat TMP_9 TMP_10 TMP_11 H1) in (let TMP_14 \def (\lambda (n3: +nat).(let TMP_12 \def (TSort n2) in (let TMP_13 \def (TSort n3) in (eq T +TMP_12 TMP_13)))) in (let TMP_15 \def (TSort n2) in (let TMP_16 \def +(refl_equal T TMP_15) in (ex_intro nat TMP_14 n2 TMP_16))))))))))) in (let +TMP_25 \def (\lambda (i1: nat).(\lambda (i2: nat).(\lambda (H1: (eq T (TLRef +i1) (TSort n1))).(let TMP_18 \def (TLRef i1) in (let TMP_19 \def (\lambda +(ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow +True | (THead _ _ _) \Rightarrow False])) in (let TMP_20 \def (TSort n1) in +(let H2 \def (eq_ind T TMP_18 TMP_19 I TMP_20 H1) in (let TMP_23 \def +(\lambda (n2: nat).(let TMP_21 \def (TLRef i2) in (let TMP_22 \def (TSort n2) +in (eq T TMP_21 TMP_22)))) in (let TMP_24 \def (ex nat TMP_23) in (False_ind +TMP_24 H2)))))))))) in (let TMP_33 \def (\lambda (v1: T).(\lambda (v2: +T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (k: K).(\lambda (H1: (eq T +(THead k v1 t1) (TSort n1))).(let TMP_26 \def (THead k v1 t1) in (let TMP_27 +\def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow False | (THead _ _ _) \Rightarrow True])) in (let TMP_28 \def +(TSort n1) in (let H2 \def (eq_ind T TMP_26 TMP_27 I TMP_28 H1) in (let +TMP_31 \def (\lambda (n2: nat).(let TMP_29 \def (THead k v2 t2) in (let +TMP_30 \def (TSort n2) in (eq T TMP_29 TMP_30)))) in (let TMP_32 \def (ex nat +TMP_31) in (False_ind TMP_32 H2))))))))))))) in (iso_ind TMP_8 TMP_17 TMP_25 +TMP_33 y u2 H0))))))) in (insert_eq T TMP_1 TMP_2 TMP_5 TMP_34 H))))))). theorem iso_gen_lref: \forall (u2: T).(\forall (n1: nat).((iso (TLRef n1) u2) \to (ex nat (\lambda (n2: nat).(eq T u2 (TLRef n2)))))) \def - \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TLRef n1) -u2)).(insert_eq T (TLRef n1) (\lambda (t: T).(iso t u2)) (\lambda (_: T).(ex -nat (\lambda (n2: nat).(eq T u2 (TLRef n2))))) (\lambda (y: T).(\lambda (H0: -(iso y u2)).(iso_ind (\lambda (t: T).(\lambda (t0: T).((eq T t (TLRef n1)) -\to (ex nat (\lambda (n2: nat).(eq T t0 (TLRef n2))))))) (\lambda (n0: -nat).(\lambda (n2: nat).(\lambda (H1: (eq T (TSort n0) (TLRef n1))).(let H2 -\def (eq_ind T (TSort n0) (\lambda (ee: T).(match ee in T return (\lambda (_: -T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | -(THead _ _ _) \Rightarrow False])) I (TLRef n1) H1) in (False_ind (ex nat -(\lambda (n3: nat).(eq T (TSort n2) (TLRef n3)))) H2))))) (\lambda (i1: -nat).(\lambda (i2: nat).(\lambda (H1: (eq T (TLRef i1) (TLRef n1))).(let H2 -\def (f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) -with [(TSort _) \Rightarrow i1 | (TLRef n) \Rightarrow n | (THead _ _ _) -\Rightarrow i1])) (TLRef i1) (TLRef n1) H1) in (ex_intro nat (\lambda (n2: -nat).(eq T (TLRef i2) (TLRef n2))) i2 (refl_equal T (TLRef i2))))))) (\lambda -(v1: T).(\lambda (v2: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (k: -K).(\lambda (H1: (eq T (THead k v1 t1) (TLRef n1))).(let H2 \def (eq_ind T -(THead k v1 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) -with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ -_) \Rightarrow True])) I (TLRef n1) H1) in (False_ind (ex nat (\lambda (n2: -nat).(eq T (THead k v2 t2) (TLRef n2)))) H2)))))))) y u2 H0))) H))). -(* COMMENTS -Initial nodes: 321 -END *) + \lambda (u2: T).(\lambda (n1: nat).(\lambda (H: (iso (TLRef n1) u2)).(let +TMP_1 \def (TLRef n1) in (let TMP_2 \def (\lambda (t: T).(iso t u2)) in (let +TMP_5 \def (\lambda (_: T).(let TMP_4 \def (\lambda (n2: nat).(let TMP_3 \def +(TLRef n2) in (eq T u2 TMP_3))) in (ex nat TMP_4))) in (let TMP_34 \def +(\lambda (y: T).(\lambda (H0: (iso y u2)).(let TMP_8 \def (\lambda (t: +T).(\lambda (t0: T).((eq T t (TLRef n1)) \to (let TMP_7 \def (\lambda (n2: +nat).(let TMP_6 \def (TLRef n2) in (eq T t0 TMP_6))) in (ex nat TMP_7))))) in +(let TMP_16 \def (\lambda (n0: nat).(\lambda (n2: nat).(\lambda (H1: (eq T +(TSort n0) (TLRef n1))).(let TMP_9 \def (TSort n0) in (let TMP_10 \def +(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow True | (TLRef _) +\Rightarrow False | (THead _ _ _) \Rightarrow False])) in (let TMP_11 \def +(TLRef n1) in (let H2 \def (eq_ind T TMP_9 TMP_10 I TMP_11 H1) in (let TMP_14 +\def (\lambda (n3: nat).(let TMP_12 \def (TSort n2) in (let TMP_13 \def +(TLRef n3) in (eq T TMP_12 TMP_13)))) in (let TMP_15 \def (ex nat TMP_14) in +(False_ind TMP_15 H2)))))))))) in (let TMP_25 \def (\lambda (i1: +nat).(\lambda (i2: nat).(\lambda (H1: (eq T (TLRef i1) (TLRef n1))).(let +TMP_17 \def (\lambda (e: T).(match e with [(TSort _) \Rightarrow i1 | (TLRef +n) \Rightarrow n | (THead _ _ _) \Rightarrow i1])) in (let TMP_18 \def (TLRef +i1) in (let TMP_19 \def (TLRef n1) in (let H2 \def (f_equal T nat TMP_17 +TMP_18 TMP_19 H1) in (let TMP_22 \def (\lambda (n2: nat).(let TMP_20 \def +(TLRef i2) in (let TMP_21 \def (TLRef n2) in (eq T TMP_20 TMP_21)))) in (let +TMP_23 \def (TLRef i2) in (let TMP_24 \def (refl_equal T TMP_23) in (ex_intro +nat TMP_22 i2 TMP_24))))))))))) in (let TMP_33 \def (\lambda (v1: T).(\lambda +(v2: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (k: K).(\lambda (H1: (eq T +(THead k v1 t1) (TLRef n1))).(let TMP_26 \def (THead k v1 t1) in (let TMP_27 +\def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow False | (THead _ _ _) \Rightarrow True])) in (let TMP_28 \def +(TLRef n1) in (let H2 \def (eq_ind T TMP_26 TMP_27 I TMP_28 H1) in (let +TMP_31 \def (\lambda (n2: nat).(let TMP_29 \def (THead k v2 t2) in (let +TMP_30 \def (TLRef n2) in (eq T TMP_29 TMP_30)))) in (let TMP_32 \def (ex nat +TMP_31) in (False_ind TMP_32 H2))))))))))))) in (iso_ind TMP_8 TMP_16 TMP_25 +TMP_33 y u2 H0))))))) in (insert_eq T TMP_1 TMP_2 TMP_5 TMP_34 H))))))). theorem iso_gen_head: \forall (k: K).(\forall (v1: T).(\forall (t1: T).(\forall (u2: T).((iso @@ -82,41 +115,53 @@ theorem iso_gen_head: (THead k v2 t2))))))))) \def \lambda (k: K).(\lambda (v1: T).(\lambda (t1: T).(\lambda (u2: T).(\lambda -(H: (iso (THead k v1 t1) u2)).(insert_eq T (THead k v1 t1) (\lambda (t: -T).(iso t u2)) (\lambda (_: T).(ex_2 T T (\lambda (v2: T).(\lambda (t2: -T).(eq T u2 (THead k v2 t2)))))) (\lambda (y: T).(\lambda (H0: (iso y -u2)).(iso_ind (\lambda (t: T).(\lambda (t0: T).((eq T t (THead k v1 t1)) \to -(ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T t0 (THead k v2 t2)))))))) -(\lambda (n1: nat).(\lambda (n2: nat).(\lambda (H1: (eq T (TSort n1) (THead k -v1 t1))).(let H2 \def (eq_ind T (TSort n1) (\lambda (ee: T).(match ee in T -return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) -\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead k v1 t1) H1) -in (False_ind (ex_2 T T (\lambda (v2: T).(\lambda (t2: T).(eq T (TSort n2) -(THead k v2 t2))))) H2))))) (\lambda (i1: nat).(\lambda (i2: nat).(\lambda -(H1: (eq T (TLRef i1) (THead k v1 t1))).(let H2 \def (eq_ind T (TLRef i1) -(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) -\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow -False])) I (THead k v1 t1) H1) in (False_ind (ex_2 T T (\lambda (v2: -T).(\lambda (t2: T).(eq T (TLRef i2) (THead k v2 t2))))) H2))))) (\lambda -(v0: T).(\lambda (v2: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (k0: -K).(\lambda (H1: (eq T (THead k0 v0 t0) (THead k v1 t1))).(let H2 \def -(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with -[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k1 _ _) -\Rightarrow k1])) (THead k0 v0 t0) (THead k v1 t1) H1) in ((let H3 \def -(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with +(H: (iso (THead k v1 t1) u2)).(let TMP_1 \def (THead k v1 t1) in (let TMP_2 +\def (\lambda (t: T).(iso t u2)) in (let TMP_5 \def (\lambda (_: T).(let +TMP_4 \def (\lambda (v2: T).(\lambda (t2: T).(let TMP_3 \def (THead k v2 t2) +in (eq T u2 TMP_3)))) in (ex_2 T T TMP_4))) in (let TMP_47 \def (\lambda (y: +T).(\lambda (H0: (iso y u2)).(let TMP_8 \def (\lambda (t: T).(\lambda (t0: +T).((eq T t (THead k v1 t1)) \to (let TMP_7 \def (\lambda (v2: T).(\lambda +(t2: T).(let TMP_6 \def (THead k v2 t2) in (eq T t0 TMP_6)))) in (ex_2 T T +TMP_7))))) in (let TMP_16 \def (\lambda (n1: nat).(\lambda (n2: nat).(\lambda +(H1: (eq T (TSort n1) (THead k v1 t1))).(let TMP_9 \def (TSort n1) in (let +TMP_10 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow True | +(TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) in (let +TMP_11 \def (THead k v1 t1) in (let H2 \def (eq_ind T TMP_9 TMP_10 I TMP_11 +H1) in (let TMP_14 \def (\lambda (v2: T).(\lambda (t2: T).(let TMP_12 \def +(TSort n2) in (let TMP_13 \def (THead k v2 t2) in (eq T TMP_12 TMP_13))))) in +(let TMP_15 \def (ex_2 T T TMP_14) in (False_ind TMP_15 H2)))))))))) in (let +TMP_24 \def (\lambda (i1: nat).(\lambda (i2: nat).(\lambda (H1: (eq T (TLRef +i1) (THead k v1 t1))).(let TMP_17 \def (TLRef i1) in (let TMP_18 \def +(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow True | (THead _ _ _) \Rightarrow False])) in (let TMP_19 \def +(THead k v1 t1) in (let H2 \def (eq_ind T TMP_17 TMP_18 I TMP_19 H1) in (let +TMP_22 \def (\lambda (v2: T).(\lambda (t2: T).(let TMP_20 \def (TLRef i2) in +(let TMP_21 \def (THead k v2 t2) in (eq T TMP_20 TMP_21))))) in (let TMP_23 +\def (ex_2 T T TMP_22) in (False_ind TMP_23 H2)))))))))) in (let TMP_46 \def +(\lambda (v0: T).(\lambda (v2: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda +(k0: K).(\lambda (H1: (eq T (THead k0 v0 t0) (THead k v1 t1))).(let TMP_25 +\def (\lambda (e: T).(match e with [(TSort _) \Rightarrow k0 | (TLRef _) +\Rightarrow k0 | (THead k1 _ _) \Rightarrow k1])) in (let TMP_26 \def (THead +k0 v0 t0) in (let TMP_27 \def (THead k v1 t1) in (let H2 \def (f_equal T K +TMP_25 TMP_26 TMP_27 H1) in (let TMP_28 \def (\lambda (e: T).(match e with [(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 | (THead _ t _) -\Rightarrow t])) (THead k0 v0 t0) (THead k v1 t1) H1) in ((let H4 \def -(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with -[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) -\Rightarrow t])) (THead k0 v0 t0) (THead k v1 t1) H1) in (\lambda (_: (eq T -v0 v1)).(\lambda (H6: (eq K k0 k)).(eq_ind_r K k (\lambda (k1: K).(ex_2 T T -(\lambda (v3: T).(\lambda (t3: T).(eq T (THead k1 v2 t2) (THead k v3 t3)))))) -(ex_2_intro T T (\lambda (v3: T).(\lambda (t3: T).(eq T (THead k v2 t2) -(THead k v3 t3)))) v2 t2 (refl_equal T (THead k v2 t2))) k0 H6)))) H3)) -H2)))))))) y u2 H0))) H))))). -(* COMMENTS -Initial nodes: 545 -END *) +\Rightarrow t])) in (let TMP_29 \def (THead k0 v0 t0) in (let TMP_30 \def +(THead k v1 t1) in (let H3 \def (f_equal T T TMP_28 TMP_29 TMP_30 H1) in (let +TMP_31 \def (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | (TLRef +_) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) in (let TMP_32 \def (THead +k0 v0 t0) in (let TMP_33 \def (THead k v1 t1) in (let H4 \def (f_equal T T +TMP_31 TMP_32 TMP_33 H1) in (let TMP_44 \def (\lambda (_: (eq T v0 +v1)).(\lambda (H6: (eq K k0 k)).(let TMP_37 \def (\lambda (k1: K).(let TMP_36 +\def (\lambda (v3: T).(\lambda (t3: T).(let TMP_34 \def (THead k1 v2 t2) in +(let TMP_35 \def (THead k v3 t3) in (eq T TMP_34 TMP_35))))) in (ex_2 T T +TMP_36))) in (let TMP_40 \def (\lambda (v3: T).(\lambda (t3: T).(let TMP_38 +\def (THead k v2 t2) in (let TMP_39 \def (THead k v3 t3) in (eq T TMP_38 +TMP_39))))) in (let TMP_41 \def (THead k v2 t2) in (let TMP_42 \def +(refl_equal T TMP_41) in (let TMP_43 \def (ex_2_intro T T TMP_40 v2 t2 +TMP_42) in (eq_ind_r K k TMP_37 TMP_43 k0 H6)))))))) in (let TMP_45 \def +(TMP_44 H3) in (TMP_45 H2))))))))))))))))))))) in (iso_ind TMP_8 TMP_16 +TMP_24 TMP_46 y u2 H0))))))) in (insert_eq T TMP_1 TMP_2 TMP_5 TMP_47 +H))))))))). theorem iso_flats_lref_bind_false: \forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall @@ -124,32 +169,39 @@ theorem iso_flats_lref_bind_false: b) v t)) \to (\forall (P: Prop).P))))))) \def \lambda (f: F).(\lambda (b: B).(\lambda (i: nat).(\lambda (v: T).(\lambda -(t: T).(\lambda (vs: TList).(TList_ind (\lambda (t0: TList).((iso (THeads -(Flat f) t0 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P: Prop).P))) -(\lambda (H: (iso (TLRef i) (THead (Bind b) v t))).(\lambda (P: Prop).(let -H_x \def (iso_gen_lref (THead (Bind b) v t) i H) in (let H0 \def H_x in -(ex_ind nat (\lambda (n2: nat).(eq T (THead (Bind b) v t) (TLRef n2))) P -(\lambda (x: nat).(\lambda (H1: (eq T (THead (Bind b) v t) (TLRef x))).(let -H2 \def (eq_ind T (THead (Bind b) v t) (\lambda (ee: T).(match ee in T return -(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) -\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef x) H1) in -(False_ind P H2)))) H0))))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda -(_: (((iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)) \to (\forall -(P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f) t0 (THeads (Flat f) t1 -(TLRef i))) (THead (Bind b) v t))).(\lambda (P: Prop).(let H_x \def -(iso_gen_head (Flat f) t0 (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t) -H0) in (let H1 \def H_x in (ex_2_ind T T (\lambda (v2: T).(\lambda (t2: -T).(eq T (THead (Bind b) v t) (THead (Flat f) v2 t2)))) P (\lambda (x0: -T).(\lambda (x1: T).(\lambda (H2: (eq T (THead (Bind b) v t) (THead (Flat f) -x0 x1))).(let H3 \def (eq_ind T (THead (Bind b) v t) (\lambda (ee: T).(match -ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | -(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return -(\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow -False])])) I (THead (Flat f) x0 x1) H2) in (False_ind P H3))))) H1)))))))) -vs)))))). -(* COMMENTS -Initial nodes: 391 -END *) +(t: T).(\lambda (vs: TList).(let TMP_1 \def (\lambda (t0: TList).((iso +(THeads (Flat f) t0 (TLRef i)) (THead (Bind b) v t)) \to (\forall (P: +Prop).P))) in (let TMP_13 \def (\lambda (H: (iso (TLRef i) (THead (Bind b) v +t))).(\lambda (P: Prop).(let TMP_2 \def (Bind b) in (let TMP_3 \def (THead +TMP_2 v t) in (let H_x \def (iso_gen_lref TMP_3 i H) in (let H0 \def H_x in +(let TMP_7 \def (\lambda (n2: nat).(let TMP_4 \def (Bind b) in (let TMP_5 +\def (THead TMP_4 v t) in (let TMP_6 \def (TLRef n2) in (eq T TMP_5 +TMP_6))))) in (let TMP_12 \def (\lambda (x: nat).(\lambda (H1: (eq T (THead +(Bind b) v t) (TLRef x))).(let TMP_8 \def (Bind b) in (let TMP_9 \def (THead +TMP_8 v t) in (let TMP_10 \def (\lambda (ee: T).(match ee with [(TSort _) +\Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow +True])) in (let TMP_11 \def (TLRef x) in (let H2 \def (eq_ind T TMP_9 TMP_10 +I TMP_11 H1) in (False_ind P H2)))))))) in (ex_ind nat TMP_7 P TMP_12 +H0))))))))) in (let TMP_31 \def (\lambda (t0: T).(\lambda (t1: +TList).(\lambda (_: (((iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v +t)) \to (\forall (P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f) t0 +(THeads (Flat f) t1 (TLRef i))) (THead (Bind b) v t))).(\lambda (P: +Prop).(let TMP_14 \def (Flat f) in (let TMP_15 \def (Flat f) in (let TMP_16 +\def (TLRef i) in (let TMP_17 \def (THeads TMP_15 t1 TMP_16) in (let TMP_18 +\def (Bind b) in (let TMP_19 \def (THead TMP_18 v t) in (let H_x \def +(iso_gen_head TMP_14 t0 TMP_17 TMP_19 H0) in (let H1 \def H_x in (let TMP_24 +\def (\lambda (v2: T).(\lambda (t2: T).(let TMP_20 \def (Bind b) in (let +TMP_21 \def (THead TMP_20 v t) in (let TMP_22 \def (Flat f) in (let TMP_23 +\def (THead TMP_22 v2 t2) in (eq T TMP_21 TMP_23))))))) in (let TMP_30 \def +(\lambda (x0: T).(\lambda (x1: T).(\lambda (H2: (eq T (THead (Bind b) v t) +(THead (Flat f) x0 x1))).(let TMP_25 \def (Bind b) in (let TMP_26 \def (THead +TMP_25 v t) in (let TMP_27 \def (\lambda (ee: T).(match ee with [(TSort _) +\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow +(match k with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) in +(let TMP_28 \def (Flat f) in (let TMP_29 \def (THead TMP_28 x0 x1) in (let H3 +\def (eq_ind T TMP_26 TMP_27 I TMP_29 H2) in (False_ind P H3)))))))))) in +(ex_2_ind T T TMP_24 P TMP_30 H1)))))))))))))))) in (TList_ind TMP_1 TMP_13 +TMP_31 vs))))))))). theorem iso_flats_flat_bind_false: \forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall @@ -158,34 +210,41 @@ theorem iso_flats_flat_bind_false: Prop).P))))))))) \def \lambda (f1: F).(\lambda (f2: F).(\lambda (b: B).(\lambda (v: T).(\lambda -(v2: T).(\lambda (t: T).(\lambda (t2: T).(\lambda (vs: TList).(TList_ind +(v2: T).(\lambda (t: T).(\lambda (t2: T).(\lambda (vs: TList).(let TMP_1 \def (\lambda (t0: TList).((iso (THeads (Flat f1) t0 (THead (Flat f2) v2 t2)) -(THead (Bind b) v t)) \to (\forall (P: Prop).P))) (\lambda (H: (iso (THead -(Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P: Prop).(let H_x \def -(iso_gen_head (Flat f2) v2 t2 (THead (Bind b) v t) H) in (let H0 \def H_x in -(ex_2_ind T T (\lambda (v3: T).(\lambda (t3: T).(eq T (THead (Bind b) v t) -(THead (Flat f2) v3 t3)))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: -(eq T (THead (Bind b) v t) (THead (Flat f2) x0 x1))).(let H2 \def (eq_ind T -(THead (Bind b) v t) (\lambda (ee: T).(match ee in T return (\lambda (_: -T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | -(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with -[(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat -f2) x0 x1) H1) in (False_ind P H2))))) H0))))) (\lambda (t0: T).(\lambda (t1: -TList).(\lambda (_: (((iso (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) -(THead (Bind b) v t)) \to (\forall (P: Prop).P)))).(\lambda (H0: (iso (THead -(Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v -t))).(\lambda (P: Prop).(let H_x \def (iso_gen_head (Flat f1) t0 (THeads -(Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t) H0) in (let H1 -\def H_x in (ex_2_ind T T (\lambda (v3: T).(\lambda (t3: T).(eq T (THead -(Bind b) v t) (THead (Flat f1) v3 t3)))) P (\lambda (x0: T).(\lambda (x1: -T).(\lambda (H2: (eq T (THead (Bind b) v t) (THead (Flat f1) x0 x1))).(let H3 -\def (eq_ind T (THead (Bind b) v t) (\lambda (ee: T).(match ee in T return -(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) -\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda -(_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow -False])])) I (THead (Flat f1) x0 x1) H2) in (False_ind P H3))))) H1)))))))) -vs)))))))). -(* COMMENTS -Initial nodes: 461 -END *) +(THead (Bind b) v t)) \to (\forall (P: Prop).P))) in (let TMP_16 \def +(\lambda (H: (iso (THead (Flat f2) v2 t2) (THead (Bind b) v t))).(\lambda (P: +Prop).(let TMP_2 \def (Flat f2) in (let TMP_3 \def (Bind b) in (let TMP_4 +\def (THead TMP_3 v t) in (let H_x \def (iso_gen_head TMP_2 v2 t2 TMP_4 H) in +(let H0 \def H_x in (let TMP_9 \def (\lambda (v3: T).(\lambda (t3: T).(let +TMP_5 \def (Bind b) in (let TMP_6 \def (THead TMP_5 v t) in (let TMP_7 \def +(Flat f2) in (let TMP_8 \def (THead TMP_7 v3 t3) in (eq T TMP_6 TMP_8))))))) +in (let TMP_15 \def (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T +(THead (Bind b) v t) (THead (Flat f2) x0 x1))).(let TMP_10 \def (Bind b) in +(let TMP_11 \def (THead TMP_10 v t) in (let TMP_12 \def (\lambda (ee: +T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False +| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat +_) \Rightarrow False])])) in (let TMP_13 \def (Flat f2) in (let TMP_14 \def +(THead TMP_13 x0 x1) in (let H2 \def (eq_ind T TMP_11 TMP_12 I TMP_14 H1) in +(False_ind P H2)))))))))) in (ex_2_ind T T TMP_9 P TMP_15 H0)))))))))) in +(let TMP_35 \def (\lambda (t0: T).(\lambda (t1: TList).(\lambda (_: (((iso +(THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) \to +(\forall (P: Prop).P)))).(\lambda (H0: (iso (THead (Flat f1) t0 (THeads (Flat +f1) t1 (THead (Flat f2) v2 t2))) (THead (Bind b) v t))).(\lambda (P: +Prop).(let TMP_17 \def (Flat f1) in (let TMP_18 \def (Flat f1) in (let TMP_19 +\def (Flat f2) in (let TMP_20 \def (THead TMP_19 v2 t2) in (let TMP_21 \def +(THeads TMP_18 t1 TMP_20) in (let TMP_22 \def (Bind b) in (let TMP_23 \def +(THead TMP_22 v t) in (let H_x \def (iso_gen_head TMP_17 t0 TMP_21 TMP_23 H0) +in (let H1 \def H_x in (let TMP_28 \def (\lambda (v3: T).(\lambda (t3: +T).(let TMP_24 \def (Bind b) in (let TMP_25 \def (THead TMP_24 v t) in (let +TMP_26 \def (Flat f1) in (let TMP_27 \def (THead TMP_26 v3 t3) in (eq T +TMP_25 TMP_27))))))) in (let TMP_34 \def (\lambda (x0: T).(\lambda (x1: +T).(\lambda (H2: (eq T (THead (Bind b) v t) (THead (Flat f1) x0 x1))).(let +TMP_29 \def (Bind b) in (let TMP_30 \def (THead TMP_29 v t) in (let TMP_31 +\def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _) +\Rightarrow True | (Flat _) \Rightarrow False])])) in (let TMP_32 \def (Flat +f1) in (let TMP_33 \def (THead TMP_32 x0 x1) in (let H3 \def (eq_ind T TMP_30 +TMP_31 I TMP_33 H2) in (False_ind P H3)))))))))) in (ex_2_ind T T TMP_28 P +TMP_34 H1))))))))))))))))) in (TList_ind TMP_1 TMP_16 TMP_35 vs))))))))))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/iso/props.ma b/matita/matita/contribs/lambdadelta/basic_1/iso/props.ma index af521d073..3a1c86826 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/iso/props.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/iso/props.ma @@ -14,43 +14,51 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/iso/fwd.ma". +include "basic_1/T/fwd.ma". + +include "basic_1/iso/fwd.ma". theorem iso_refl: \forall (t: T).(iso t t) \def - \lambda (t: T).(T_ind (\lambda (t0: T).(iso t0 t0)) (\lambda (n: -nat).(iso_sort n n)) (\lambda (n: nat).(iso_lref n n)) (\lambda (k: -K).(\lambda (t0: T).(\lambda (_: (iso t0 t0)).(\lambda (t1: T).(\lambda (_: -(iso t1 t1)).(iso_head t0 t0 t1 t1 k)))))) t). -(* COMMENTS -Initial nodes: 59 -END *) + \lambda (t: T).(let TMP_1 \def (\lambda (t0: T).(iso t0 t0)) in (let TMP_2 +\def (\lambda (n: nat).(iso_sort n n)) in (let TMP_3 \def (\lambda (n: +nat).(iso_lref n n)) in (let TMP_4 \def (\lambda (k: K).(\lambda (t0: +T).(\lambda (_: (iso t0 t0)).(\lambda (t1: T).(\lambda (_: (iso t1 +t1)).(iso_head t0 t0 t1 t1 k)))))) in (T_ind TMP_1 TMP_2 TMP_3 TMP_4 t))))). theorem iso_trans: \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2 t3) \to (iso t1 t3))))) \def - \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (iso t1 t2)).(iso_ind (\lambda -(t: T).(\lambda (t0: T).(\forall (t3: T).((iso t0 t3) \to (iso t t3))))) -(\lambda (n1: nat).(\lambda (n2: nat).(\lambda (t3: T).(\lambda (H0: (iso -(TSort n2) t3)).(let H_x \def (iso_gen_sort t3 n2 H0) in (let H1 \def H_x in -(ex_ind nat (\lambda (n3: nat).(eq T t3 (TSort n3))) (iso (TSort n1) t3) -(\lambda (x: nat).(\lambda (H2: (eq T t3 (TSort x))).(eq_ind_r T (TSort x) -(\lambda (t: T).(iso (TSort n1) t)) (iso_sort n1 x) t3 H2))) H1))))))) -(\lambda (i1: nat).(\lambda (i2: nat).(\lambda (t3: T).(\lambda (H0: (iso -(TLRef i2) t3)).(let H_x \def (iso_gen_lref t3 i2 H0) in (let H1 \def H_x in -(ex_ind nat (\lambda (n2: nat).(eq T t3 (TLRef n2))) (iso (TLRef i1) t3) -(\lambda (x: nat).(\lambda (H2: (eq T t3 (TLRef x))).(eq_ind_r T (TLRef x) -(\lambda (t: T).(iso (TLRef i1) t)) (iso_lref i1 x) t3 H2))) H1))))))) -(\lambda (v1: T).(\lambda (v2: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda -(k: K).(\lambda (t5: T).(\lambda (H0: (iso (THead k v2 t4) t5)).(let H_x \def -(iso_gen_head k v2 t4 t5 H0) in (let H1 \def H_x in (ex_2_ind T T (\lambda -(v3: T).(\lambda (t6: T).(eq T t5 (THead k v3 t6)))) (iso (THead k v1 t3) t5) -(\lambda (x0: T).(\lambda (x1: T).(\lambda (H2: (eq T t5 (THead k x0 -x1))).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(iso (THead k v1 t3) t)) -(iso_head v1 x0 t3 x1 k) t5 H2)))) H1)))))))))) t1 t2 H))). -(* COMMENTS -Initial nodes: 351 -END *) + \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (iso t1 t2)).(let TMP_1 \def +(\lambda (t: T).(\lambda (t0: T).(\forall (t3: T).((iso t0 t3) \to (iso t +t3))))) in (let TMP_11 \def (\lambda (n1: nat).(\lambda (n2: nat).(\lambda +(t3: T).(\lambda (H0: (iso (TSort n2) t3)).(let H_x \def (iso_gen_sort t3 n2 +H0) in (let H1 \def H_x in (let TMP_3 \def (\lambda (n3: nat).(let TMP_2 \def +(TSort n3) in (eq T t3 TMP_2))) in (let TMP_4 \def (TSort n1) in (let TMP_5 +\def (iso TMP_4 t3) in (let TMP_10 \def (\lambda (x: nat).(\lambda (H2: (eq T +t3 (TSort x))).(let TMP_6 \def (TSort x) in (let TMP_8 \def (\lambda (t: +T).(let TMP_7 \def (TSort n1) in (iso TMP_7 t))) in (let TMP_9 \def (iso_sort +n1 x) in (eq_ind_r T TMP_6 TMP_8 TMP_9 t3 H2)))))) in (ex_ind nat TMP_3 TMP_5 +TMP_10 H1))))))))))) in (let TMP_21 \def (\lambda (i1: nat).(\lambda (i2: +nat).(\lambda (t3: T).(\lambda (H0: (iso (TLRef i2) t3)).(let H_x \def +(iso_gen_lref t3 i2 H0) in (let H1 \def H_x in (let TMP_13 \def (\lambda (n2: +nat).(let TMP_12 \def (TLRef n2) in (eq T t3 TMP_12))) in (let TMP_14 \def +(TLRef i1) in (let TMP_15 \def (iso TMP_14 t3) in (let TMP_20 \def (\lambda +(x: nat).(\lambda (H2: (eq T t3 (TLRef x))).(let TMP_16 \def (TLRef x) in +(let TMP_18 \def (\lambda (t: T).(let TMP_17 \def (TLRef i1) in (iso TMP_17 +t))) in (let TMP_19 \def (iso_lref i1 x) in (eq_ind_r T TMP_16 TMP_18 TMP_19 +t3 H2)))))) in (ex_ind nat TMP_13 TMP_15 TMP_20 H1))))))))))) in (let TMP_31 +\def (\lambda (v1: T).(\lambda (v2: T).(\lambda (t3: T).(\lambda (t4: +T).(\lambda (k: K).(\lambda (t5: T).(\lambda (H0: (iso (THead k v2 t4) +t5)).(let H_x \def (iso_gen_head k v2 t4 t5 H0) in (let H1 \def H_x in (let +TMP_23 \def (\lambda (v3: T).(\lambda (t6: T).(let TMP_22 \def (THead k v3 +t6) in (eq T t5 TMP_22)))) in (let TMP_24 \def (THead k v1 t3) in (let TMP_25 +\def (iso TMP_24 t5) in (let TMP_30 \def (\lambda (x0: T).(\lambda (x1: +T).(\lambda (H2: (eq T t5 (THead k x0 x1))).(let TMP_26 \def (THead k x0 x1) +in (let TMP_28 \def (\lambda (t: T).(let TMP_27 \def (THead k v1 t3) in (iso +TMP_27 t))) in (let TMP_29 \def (iso_head v1 x0 t3 x1 k) in (eq_ind_r T +TMP_26 TMP_28 TMP_29 t5 H2))))))) in (ex_2_ind T T TMP_23 TMP_25 TMP_30 +H1)))))))))))))) in (iso_ind TMP_1 TMP_11 TMP_21 TMP_31 t1 t2 H))))))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlt/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/tlt/defs.ma index 546bdb78d..a75af6bd2 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/tlt/defs.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/tlt/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/T/defs.ma". +include "basic_1/T/defs.ma". definition wadd: ((nat \to nat)) \to (nat \to (nat \to nat)) @@ -22,25 +22,35 @@ definition wadd: \lambda (f: ((nat \to nat))).(\lambda (w: nat).(\lambda (n: nat).(match n with [O \Rightarrow w | (S m) \Rightarrow (f m)]))). -definition weight_map: - ((nat \to nat)) \to (T \to nat) -\def - let rec weight_map (f: ((nat \to nat))) (t: T) on t: nat \def (match t with +let rec weight_map (f: (nat \to nat)) (t: T) on t: nat \def match t with [(TSort _) \Rightarrow O | (TLRef n) \Rightarrow (f n) | (THead k u t0) \Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr -\Rightarrow (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f -u))) t0))) | Abst \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f -O) t0))) | Void \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f O) -t0)))]) | (Flat _) \Rightarrow (S (plus (weight_map f u) (weight_map f -t0)))])]) in weight_map. +\Rightarrow (let TMP_12 \def (weight_map f u) in (let TMP_13 \def (weight_map +f u) in (let TMP_14 \def (S TMP_13) in (let TMP_15 \def (wadd f TMP_14) in +(let TMP_16 \def (weight_map TMP_15 t0) in (let TMP_17 \def (plus TMP_12 +TMP_16) in (S TMP_17))))))) | Abst \Rightarrow (let TMP_8 \def (weight_map f +u) in (let TMP_9 \def (wadd f O) in (let TMP_10 \def (weight_map TMP_9 t0) in +(let TMP_11 \def (plus TMP_8 TMP_10) in (S TMP_11))))) | Void \Rightarrow +(let TMP_4 \def (weight_map f u) in (let TMP_5 \def (wadd f O) in (let TMP_6 +\def (weight_map TMP_5 t0) in (let TMP_7 \def (plus TMP_4 TMP_6) in (S +TMP_7)))))]) | (Flat _) \Rightarrow (let TMP_1 \def (weight_map f u) in (let +TMP_2 \def (weight_map f t0) in (let TMP_3 \def (plus TMP_1 TMP_2) in (S +TMP_3))))])]. definition weight: T \to nat \def - weight_map (\lambda (_: nat).O). + let TMP_1 \def (\lambda (_: nat).O) in (weight_map TMP_1). definition tlt: T \to (T \to Prop) \def - \lambda (t1: T).(\lambda (t2: T).(lt (weight t1) (weight t2))). + \lambda (t1: T).(\lambda (t2: T).(let TMP_1 \def (weight t1) in (let TMP_2 +\def (weight t2) in (lt TMP_1 TMP_2)))). + +definition tle: + T \to (T \to Prop) +\def + \lambda (t1: T).(\lambda (t2: T).(let TMP_1 \def (tweight t1) in (let TMP_2 +\def (tweight t2) in (le TMP_1 TMP_2)))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlt/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/tlt/fwd.ma new file mode 100644 index 000000000..f284327c1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_1/tlt/fwd.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "basic_1/tlt/defs.ma". + +theorem tlt_wf__q_ind: + \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to +Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0 +t))))) P n))) \to (\forall (t: T).(P t))) +\def + let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t: +T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to +Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t) +n) \to (P t)))))).(\lambda (t: T).(let TMP_1 \def (weight t) in (let TMP_2 +\def (weight t) in (let TMP_3 \def (refl_equal nat TMP_2) in (H TMP_1 t +TMP_3))))))). + +theorem tlt_wf_ind: + \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t) +\to (P v)))) \to (P t)))) \to (\forall (t: T).(P t))) +\def + let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t: +T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to +Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v) +(weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(let TMP_1 \def +(\lambda (t0: T).(P t0)) in (let TMP_11 \def (\lambda (n: nat).(let TMP_2 +\def (\lambda (t0: T).(P t0)) in (let TMP_3 \def (Q TMP_2) in (let TMP_10 +\def (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0) \to (Q +(\lambda (t0: T).(P t0)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat +(weight t0) n0)).(let TMP_4 \def (\lambda (n1: nat).(\forall (m: nat).((lt m +n1) \to (\forall (t1: T).((eq nat (weight t1) m) \to (P t1)))))) in (let +TMP_5 \def (weight t0) in (let H2 \def (eq_ind_r nat n0 TMP_4 H0 TMP_5 H1) in +(let TMP_9 \def (\lambda (v: T).(\lambda (H3: (lt (weight v) (weight +t0))).(let TMP_6 \def (weight v) in (let TMP_7 \def (weight v) in (let TMP_8 +\def (refl_equal nat TMP_7) in (H2 TMP_6 H3 v TMP_8)))))) in (H t0 +TMP_9))))))))) in (lt_wf_ind n TMP_3 TMP_10))))) in (tlt_wf__q_ind TMP_1 +TMP_11 t)))))). + diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma b/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma index 0b4f16d41..584fa7daf 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma @@ -14,7 +14,9 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/tlt/defs.ma". +include "basic_1/T/fwd.ma". + +include "basic_1/tlt/defs.ma". theorem wadd_le: \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: @@ -23,12 +25,10 @@ nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to \def \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w: -nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0: -nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le -(wadd f v n0) (wadd g w n0))).(H n0))) n))))))). -(* COMMENTS -Initial nodes: 81 -END *) +nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(let TMP_3 \def (\lambda (n0: +nat).(let TMP_1 \def (wadd f v n0) in (let TMP_2 \def (wadd g w n0) in (le +TMP_1 TMP_2)))) in (let TMP_4 \def (\lambda (n0: nat).(\lambda (_: (le (wadd +f v n0) (wadd g w n0))).(H n0))) in (nat_ind TMP_3 H0 TMP_4 n))))))))). theorem wadd_lt: \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: @@ -37,105 +37,158 @@ nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to \def \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w: -nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0: -nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0)) -(\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0))) -n))))))). -(* COMMENTS -Initial nodes: 95 -END *) +nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(let TMP_3 \def (\lambda (n0: +nat).(let TMP_1 \def (wadd f v n0) in (let TMP_2 \def (wadd g w n0) in (le +TMP_1 TMP_2)))) in (let TMP_4 \def (S v) in (let TMP_5 \def (S w) in (let +TMP_6 \def (S v) in (let TMP_7 \def (S TMP_6) in (let TMP_8 \def (S w) in +(let TMP_9 \def (S v) in (let TMP_10 \def (le_n_S TMP_9 w H0) in (let TMP_11 +\def (le_S TMP_7 TMP_8 TMP_10) in (let TMP_12 \def (le_S_n TMP_4 TMP_5 +TMP_11) in (let TMP_13 \def (le_S_n v w TMP_12) in (let TMP_14 \def (\lambda +(n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0))) in (nat_ind +TMP_3 TMP_13 TMP_14 n))))))))))))))))))). theorem wadd_O: \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O) \def - \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_: -nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat -(wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n). -(* COMMENTS -Initial nodes: 53 -END *) + \lambda (n: nat).(let TMP_3 \def (\lambda (n0: nat).(let TMP_1 \def (\lambda +(_: nat).O) in (let TMP_2 \def (wadd TMP_1 O n0) in (eq nat TMP_2 O)))) in +(let TMP_4 \def (refl_equal nat O) in (let TMP_5 \def (\lambda (n0: +nat).(\lambda (_: (eq nat (wadd (\lambda (_: nat).O) O n0) O)).(refl_equal +nat O))) in (nat_ind TMP_3 TMP_4 TMP_5 n)))). theorem weight_le: \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t) (weight_map g t))))) \def - \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (f: ((nat \to -nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) -\to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda -(f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall -(n0: nat).(le (f n0) (g n0))))).(le_n (weight_map g (TSort n))))))) (\lambda -(n: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda -(H: ((\forall (n0: nat).(le (f n0) (g n0))))).(H n))))) (\lambda (k: -K).(K_ind (\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat \to -nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) -\to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall (t1: -T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall -(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g t1)))))) -\to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall -(n: nat).(le (f n) (g n)))) \to (le (weight_map f (THead k0 t0 t1)) -(weight_map g (THead k0 t0 t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0: -B).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to -nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0) -(weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f: ((nat \to + \lambda (t: T).(let TMP_3 \def (\lambda (t0: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) -\to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f: ((nat \to -nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) -\to (le (match b0 with [Abbr \Rightarrow (S (plus (weight_map f t0) -(weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus -(weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus -(weight_map f t0) (weight_map (wadd f O) t1)))]) (match b0 with [Abbr -\Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g (S (weight_map g -t0))) t1))) | Abst \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g -O) t1))) | Void \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O) -t1)))])))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to -nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) -\to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda -(H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall -(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g -t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to -nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus -(weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus -(weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1)) -(le_plus_plus (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S -(weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g -H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0))) -(\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0)) -(le_n_S (weight_map f t0) (weight_map g t0) (H f g H1)) n)))))))))))) -(\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: -((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f -t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: +\to (let TMP_1 \def (weight_map f t0) in (let TMP_2 \def (weight_map g t0) in +(le TMP_1 TMP_2))))))) in (let TMP_6 \def (\lambda (n: nat).(\lambda (f: +((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (n0: +nat).(le (f n0) (g n0))))).(let TMP_4 \def (TSort n) in (let TMP_5 \def +(weight_map g TMP_4) in (le_O_n TMP_5))))))) in (let TMP_7 \def (\lambda (n: +nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: +((\forall (n0: nat).(le (f n0) (g n0))))).(H n))))) in (let TMP_144 \def +(\lambda (k: K).(let TMP_12 \def (\lambda (k0: K).(\forall (t0: T).(((\forall +(f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f +n) (g n)))) \to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall +(t1: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) +(weight_map g t1)))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat +\to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (let TMP_8 \def (THead +k0 t0 t1) in (let TMP_9 \def (weight_map f TMP_8) in (let TMP_10 \def (THead +k0 t0 t1) in (let TMP_11 \def (weight_map g TMP_10) in (le TMP_9 +TMP_11))))))))))))) in (let TMP_129 \def (\lambda (b: B).(let TMP_43 \def +(\lambda (b0: B).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall +(g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le +(weight_map f t0) (weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) -(g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat +(g n)))) \to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f: +((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) +(g n)))) \to (let TMP_27 \def (match b0 with [Abbr \Rightarrow (let TMP_21 +\def (weight_map f t0) in (let TMP_22 \def (weight_map f t0) in (let TMP_23 +\def (S TMP_22) in (let TMP_24 \def (wadd f TMP_23) in (let TMP_25 \def +(weight_map TMP_24 t1) in (let TMP_26 \def (plus TMP_21 TMP_25) in (S +TMP_26))))))) | Abst \Rightarrow (let TMP_17 \def (weight_map f t0) in (let +TMP_18 \def (wadd f O) in (let TMP_19 \def (weight_map TMP_18 t1) in (let +TMP_20 \def (plus TMP_17 TMP_19) in (S TMP_20))))) | Void \Rightarrow (let +TMP_13 \def (weight_map f t0) in (let TMP_14 \def (wadd f O) in (let TMP_15 +\def (weight_map TMP_14 t1) in (let TMP_16 \def (plus TMP_13 TMP_15) in (S +TMP_16)))))]) in (let TMP_42 \def (match b0 with [Abbr \Rightarrow (let +TMP_36 \def (weight_map g t0) in (let TMP_37 \def (weight_map g t0) in (let +TMP_38 \def (S TMP_37) in (let TMP_39 \def (wadd g TMP_38) in (let TMP_40 +\def (weight_map TMP_39 t1) in (let TMP_41 \def (plus TMP_36 TMP_40) in (S +TMP_41))))))) | Abst \Rightarrow (let TMP_32 \def (weight_map g t0) in (let +TMP_33 \def (wadd g O) in (let TMP_34 \def (weight_map TMP_33 t1) in (let +TMP_35 \def (plus TMP_32 TMP_34) in (S TMP_35))))) | Void \Rightarrow (let +TMP_28 \def (weight_map g t0) in (let TMP_29 \def (wadd g O) in (let TMP_30 +\def (weight_map TMP_29 t1) in (let TMP_31 \def (plus TMP_28 TMP_30) in (S +TMP_31)))))]) in (le TMP_27 TMP_42))))))))))) in (let TMP_84 \def (\lambda +(t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0) +(weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat +\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g +n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le -(f n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1)) -(plus (weight_map g t0) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map -f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map (wadd g O) t1) -(H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O -(le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to -nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) -\to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda -(H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall -(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g -t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to -nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus -(weight_map f t0) (weight_map (wadd f O) t1)) (plus (weight_map g t0) -(weight_map (wadd g O) t1)) (le_plus_plus (weight_map f t0) (weight_map g t0) -(weight_map (wadd f O) t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f -O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) -b)) (\lambda (_: F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to -nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n)))) -\to (le (weight_map f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda -(H0: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall -(n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t1) (weight_map g -t1))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to -nat))).(\lambda (H1: ((\forall (n: nat).(le (f0 n) (g n))))).(le_n_S (plus -(weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g -t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1) -(weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t). -(* COMMENTS -Initial nodes: 1309 -END *) +(f n) (g n))))).(let TMP_44 \def (weight_map f t0) in (let TMP_45 \def +(weight_map f t0) in (let TMP_46 \def (S TMP_45) in (let TMP_47 \def (wadd f +TMP_46) in (let TMP_48 \def (weight_map TMP_47 t1) in (let TMP_49 \def (plus +TMP_44 TMP_48) in (let TMP_50 \def (weight_map g t0) in (let TMP_51 \def +(weight_map g t0) in (let TMP_52 \def (S TMP_51) in (let TMP_53 \def (wadd g +TMP_52) in (let TMP_54 \def (weight_map TMP_53 t1) in (let TMP_55 \def (plus +TMP_50 TMP_54) in (let TMP_56 \def (weight_map f t0) in (let TMP_57 \def +(weight_map g t0) in (let TMP_58 \def (weight_map f t0) in (let TMP_59 \def +(S TMP_58) in (let TMP_60 \def (wadd f TMP_59) in (let TMP_61 \def +(weight_map TMP_60 t1) in (let TMP_62 \def (weight_map g t0) in (let TMP_63 +\def (S TMP_62) in (let TMP_64 \def (wadd g TMP_63) in (let TMP_65 \def +(weight_map TMP_64 t1) in (let TMP_66 \def (H f g H1) in (let TMP_67 \def +(weight_map f t0) in (let TMP_68 \def (S TMP_67) in (let TMP_69 \def (wadd f +TMP_68) in (let TMP_70 \def (weight_map g t0) in (let TMP_71 \def (S TMP_70) +in (let TMP_72 \def (wadd g TMP_71) in (let TMP_81 \def (\lambda (n: +nat).(let TMP_73 \def (weight_map f t0) in (let TMP_74 \def (S TMP_73) in +(let TMP_75 \def (weight_map g t0) in (let TMP_76 \def (S TMP_75) in (let +TMP_77 \def (weight_map f t0) in (let TMP_78 \def (weight_map g t0) in (let +TMP_79 \def (H f g H1) in (let TMP_80 \def (le_n_S TMP_77 TMP_78 TMP_79) in +(wadd_le f g H1 TMP_74 TMP_76 TMP_80 n)))))))))) in (let TMP_82 \def (H0 +TMP_69 TMP_72 TMP_81) in (let TMP_83 \def (le_plus_plus TMP_56 TMP_57 TMP_61 +TMP_65 TMP_66 TMP_82) in (le_n_S TMP_49 TMP_55 +TMP_83)))))))))))))))))))))))))))))))))))))))) in (let TMP_106 \def (\lambda +(t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0) +(weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat +\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g +n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat +\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le +(f n) (g n))))).(let TMP_85 \def (weight_map f t0) in (let TMP_86 \def (wadd +f O) in (let TMP_87 \def (weight_map TMP_86 t1) in (let TMP_88 \def (plus +TMP_85 TMP_87) in (let TMP_89 \def (weight_map g t0) in (let TMP_90 \def +(wadd g O) in (let TMP_91 \def (weight_map TMP_90 t1) in (let TMP_92 \def +(plus TMP_89 TMP_91) in (let TMP_93 \def (weight_map f t0) in (let TMP_94 +\def (weight_map g t0) in (let TMP_95 \def (wadd f O) in (let TMP_96 \def +(weight_map TMP_95 t1) in (let TMP_97 \def (wadd g O) in (let TMP_98 \def +(weight_map TMP_97 t1) in (let TMP_99 \def (H f g H1) in (let TMP_100 \def +(wadd f O) in (let TMP_101 \def (wadd g O) in (let TMP_103 \def (\lambda (n: +nat).(let TMP_102 \def (le_O_n O) in (wadd_le f g H1 O O TMP_102 n))) in (let +TMP_104 \def (H0 TMP_100 TMP_101 TMP_103) in (let TMP_105 \def (le_plus_plus +TMP_93 TMP_94 TMP_96 TMP_98 TMP_99 TMP_104) in (le_n_S TMP_88 TMP_92 +TMP_105)))))))))))))))))))))))))))) in (let TMP_128 \def (\lambda (t0: +T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0) +(weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat +\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g +n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat +\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le +(f n) (g n))))).(let TMP_107 \def (weight_map f t0) in (let TMP_108 \def +(wadd f O) in (let TMP_109 \def (weight_map TMP_108 t1) in (let TMP_110 \def +(plus TMP_107 TMP_109) in (let TMP_111 \def (weight_map g t0) in (let TMP_112 +\def (wadd g O) in (let TMP_113 \def (weight_map TMP_112 t1) in (let TMP_114 +\def (plus TMP_111 TMP_113) in (let TMP_115 \def (weight_map f t0) in (let +TMP_116 \def (weight_map g t0) in (let TMP_117 \def (wadd f O) in (let +TMP_118 \def (weight_map TMP_117 t1) in (let TMP_119 \def (wadd g O) in (let +TMP_120 \def (weight_map TMP_119 t1) in (let TMP_121 \def (H f g H1) in (let +TMP_122 \def (wadd f O) in (let TMP_123 \def (wadd g O) in (let TMP_125 \def +(\lambda (n: nat).(let TMP_124 \def (le_O_n O) in (wadd_le f g H1 O O TMP_124 +n))) in (let TMP_126 \def (H0 TMP_122 TMP_123 TMP_125) in (let TMP_127 \def +(le_plus_plus TMP_115 TMP_116 TMP_118 TMP_120 TMP_121 TMP_126) in (le_n_S +TMP_110 TMP_114 TMP_127)))))))))))))))))))))))))))) in (B_ind TMP_43 TMP_84 +TMP_106 TMP_128 b)))))) in (let TMP_143 \def (\lambda (_: F).(\lambda (t0: +T).(\lambda (H: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to +nat))).(((\forall (n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t0) +(weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f0: ((nat +\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g +n)))) \to (le (weight_map f0 t1) (weight_map g t1))))))).(\lambda (f0: ((nat +\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le +(f0 n) (g n))))).(let TMP_130 \def (weight_map f0 t0) in (let TMP_131 \def +(weight_map f0 t1) in (let TMP_132 \def (plus TMP_130 TMP_131) in (let +TMP_133 \def (weight_map g t0) in (let TMP_134 \def (weight_map g t1) in (let +TMP_135 \def (plus TMP_133 TMP_134) in (let TMP_136 \def (weight_map f0 t0) +in (let TMP_137 \def (weight_map g t0) in (let TMP_138 \def (weight_map f0 +t1) in (let TMP_139 \def (weight_map g t1) in (let TMP_140 \def (H f0 g H1) +in (let TMP_141 \def (H0 f0 g H1) in (let TMP_142 \def (le_plus_plus TMP_136 +TMP_137 TMP_138 TMP_139 TMP_140 TMP_141) in (le_n_S TMP_132 TMP_135 +TMP_142)))))))))))))))))))))) in (K_ind TMP_12 TMP_129 TMP_143 k))))) in +(T_ind TMP_3 TMP_6 TMP_7 TMP_144 t))))). theorem weight_eq: \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to @@ -143,158 +196,235 @@ nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f t) (weight_map g t))))) \def \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to -nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym -(weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n: -nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n) -(H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0: -nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))). -(* COMMENTS -Initial nodes: 121 -END *) +nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(let TMP_1 +\def (weight_map f t) in (let TMP_2 \def (weight_map g t) in (let TMP_10 \def +(\lambda (n: nat).(let TMP_3 \def (g n) in (let TMP_5 \def (\lambda (n0: +nat).(let TMP_4 \def (g n) in (le n0 TMP_4))) in (let TMP_6 \def (g n) in +(let TMP_7 \def (le_n TMP_6) in (let TMP_8 \def (f n) in (let TMP_9 \def (H +n) in (eq_ind_r nat TMP_3 TMP_5 TMP_7 TMP_8 TMP_9)))))))) in (let TMP_11 \def +(weight_le t f g TMP_10) in (let TMP_19 \def (\lambda (n: nat).(let TMP_12 +\def (g n) in (let TMP_14 \def (\lambda (n0: nat).(let TMP_13 \def (g n) in +(le TMP_13 n0))) in (let TMP_15 \def (g n) in (let TMP_16 \def (le_n TMP_15) +in (let TMP_17 \def (f n) in (let TMP_18 \def (H n) in (eq_ind_r nat TMP_12 +TMP_14 TMP_16 TMP_17 TMP_18)))))))) in (let TMP_20 \def (weight_le t g f +TMP_19) in (le_antisym TMP_1 TMP_2 TMP_11 TMP_20)))))))))). theorem weight_add_O: \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t) (weight_map (\lambda (_: nat).O) t)) \def - \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_: -nat).O) (\lambda (n: nat).(wadd_O n))). -(* COMMENTS -Initial nodes: 23 -END *) + \lambda (t: T).(let TMP_1 \def (\lambda (_: nat).O) in (let TMP_2 \def (wadd +TMP_1 O) in (let TMP_3 \def (\lambda (_: nat).O) in (let TMP_4 \def (\lambda +(n: nat).(wadd_O n)) in (weight_eq t TMP_2 TMP_3 TMP_4))))). theorem weight_add_S: \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O) O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t))) \def - \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O) -(wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_: -nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_S O m -(le_O_n m)) n)))). -(* COMMENTS -Initial nodes: 61 -END *) + \lambda (t: T).(\lambda (m: nat).(let TMP_1 \def (\lambda (_: nat).O) in +(let TMP_2 \def (wadd TMP_1 O) in (let TMP_3 \def (\lambda (_: nat).O) in +(let TMP_4 \def (S m) in (let TMP_5 \def (wadd TMP_3 TMP_4) in (let TMP_12 +\def (\lambda (n: nat).(let TMP_6 \def (\lambda (_: nat).O) in (let TMP_7 +\def (\lambda (_: nat).O) in (let TMP_8 \def (\lambda (_: nat).(le_O_n O)) in +(let TMP_9 \def (S m) in (let TMP_10 \def (S m) in (let TMP_11 \def (le_O_n +TMP_10) in (wadd_le TMP_6 TMP_7 TMP_8 O TMP_9 TMP_11 n)))))))) in (weight_le +t TMP_2 TMP_5 TMP_12)))))))). theorem tlt_trans: \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to (tlt u t))))) \def \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u) -(weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u) -(weight v) (weight t) H H0))))). -(* COMMENTS -Initial nodes: 43 -END *) +(weight v))).(\lambda (H0: (lt (weight v) (weight t))).(let TMP_1 \def +(weight u) in (let TMP_2 \def (weight v) in (let TMP_3 \def (weight t) in +(lt_trans TMP_1 TMP_2 TMP_3 H H0)))))))). theorem tlt_head_sx: \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t)))) \def - \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt -(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead -k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall -(t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr -\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd -(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst -\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd -(\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda -(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda -(u: T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus -(weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S -(weight_map (\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_: -nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: -nat).O) u))) t))))) (\lambda (u: T).(\lambda (t: T).(le_n_S (weight_map -(\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) (weight_map -(wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O) -u) (weight_map (wadd (\lambda (_: nat).O) O) t))))) (\lambda (u: T).(\lambda -(t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda -(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l -(weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) -t))))) b)) (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_n_S -(weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) -(weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_: -nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k). -(* COMMENTS -Initial nodes: 379 -END *) + \lambda (k: K).(let TMP_6 \def (\lambda (k0: K).(\forall (u: T).(\forall (t: +T).(let TMP_1 \def (\lambda (_: nat).O) in (let TMP_2 \def (weight_map TMP_1 +u) in (let TMP_3 \def (\lambda (_: nat).O) in (let TMP_4 \def (THead k0 u t) +in (let TMP_5 \def (weight_map TMP_3 TMP_4) in (lt TMP_2 TMP_5))))))))) in +(let TMP_83 \def (\lambda (b: B).(let TMP_31 \def (\lambda (b0: B).(\forall +(u: T).(\forall (t: T).(let TMP_7 \def (\lambda (_: nat).O) in (let TMP_8 +\def (weight_map TMP_7 u) in (let TMP_30 \def (match b0 with [Abbr +\Rightarrow (let TMP_21 \def (\lambda (_: nat).O) in (let TMP_22 \def +(weight_map TMP_21 u) in (let TMP_23 \def (\lambda (_: nat).O) in (let TMP_24 +\def (\lambda (_: nat).O) in (let TMP_25 \def (weight_map TMP_24 u) in (let +TMP_26 \def (S TMP_25) in (let TMP_27 \def (wadd TMP_23 TMP_26) in (let +TMP_28 \def (weight_map TMP_27 t) in (let TMP_29 \def (plus TMP_22 TMP_28) in +(S TMP_29)))))))))) | Abst \Rightarrow (let TMP_15 \def (\lambda (_: nat).O) +in (let TMP_16 \def (weight_map TMP_15 u) in (let TMP_17 \def (\lambda (_: +nat).O) in (let TMP_18 \def (wadd TMP_17 O) in (let TMP_19 \def (weight_map +TMP_18 t) in (let TMP_20 \def (plus TMP_16 TMP_19) in (S TMP_20))))))) | Void +\Rightarrow (let TMP_9 \def (\lambda (_: nat).O) in (let TMP_10 \def +(weight_map TMP_9 u) in (let TMP_11 \def (\lambda (_: nat).O) in (let TMP_12 +\def (wadd TMP_11 O) in (let TMP_13 \def (weight_map TMP_12 t) in (let TMP_14 +\def (plus TMP_10 TMP_13) in (S TMP_14)))))))]) in (lt TMP_8 TMP_30))))))) in +(let TMP_52 \def (\lambda (u: T).(\lambda (t: T).(let TMP_32 \def (\lambda +(_: nat).O) in (let TMP_33 \def (weight_map TMP_32 u) in (let TMP_34 \def +(\lambda (_: nat).O) in (let TMP_35 \def (weight_map TMP_34 u) in (let TMP_36 +\def (\lambda (_: nat).O) in (let TMP_37 \def (\lambda (_: nat).O) in (let +TMP_38 \def (weight_map TMP_37 u) in (let TMP_39 \def (S TMP_38) in (let +TMP_40 \def (wadd TMP_36 TMP_39) in (let TMP_41 \def (weight_map TMP_40 t) in +(let TMP_42 \def (plus TMP_35 TMP_41) in (let TMP_43 \def (\lambda (_: +nat).O) in (let TMP_44 \def (weight_map TMP_43 u) in (let TMP_45 \def +(\lambda (_: nat).O) in (let TMP_46 \def (\lambda (_: nat).O) in (let TMP_47 +\def (weight_map TMP_46 u) in (let TMP_48 \def (S TMP_47) in (let TMP_49 \def +(wadd TMP_45 TMP_48) in (let TMP_50 \def (weight_map TMP_49 t) in (let TMP_51 +\def (le_plus_l TMP_44 TMP_50) in (le_n_S TMP_33 TMP_42 +TMP_51))))))))))))))))))))))) in (let TMP_67 \def (\lambda (u: T).(\lambda +(t: T).(let TMP_53 \def (\lambda (_: nat).O) in (let TMP_54 \def (weight_map +TMP_53 u) in (let TMP_55 \def (\lambda (_: nat).O) in (let TMP_56 \def +(weight_map TMP_55 u) in (let TMP_57 \def (\lambda (_: nat).O) in (let TMP_58 +\def (wadd TMP_57 O) in (let TMP_59 \def (weight_map TMP_58 t) in (let TMP_60 +\def (plus TMP_56 TMP_59) in (let TMP_61 \def (\lambda (_: nat).O) in (let +TMP_62 \def (weight_map TMP_61 u) in (let TMP_63 \def (\lambda (_: nat).O) in +(let TMP_64 \def (wadd TMP_63 O) in (let TMP_65 \def (weight_map TMP_64 t) in +(let TMP_66 \def (le_plus_l TMP_62 TMP_65) in (le_n_S TMP_54 TMP_60 +TMP_66))))))))))))))))) in (let TMP_82 \def (\lambda (u: T).(\lambda (t: +T).(let TMP_68 \def (\lambda (_: nat).O) in (let TMP_69 \def (weight_map +TMP_68 u) in (let TMP_70 \def (\lambda (_: nat).O) in (let TMP_71 \def +(weight_map TMP_70 u) in (let TMP_72 \def (\lambda (_: nat).O) in (let TMP_73 +\def (wadd TMP_72 O) in (let TMP_74 \def (weight_map TMP_73 t) in (let TMP_75 +\def (plus TMP_71 TMP_74) in (let TMP_76 \def (\lambda (_: nat).O) in (let +TMP_77 \def (weight_map TMP_76 u) in (let TMP_78 \def (\lambda (_: nat).O) in +(let TMP_79 \def (wadd TMP_78 O) in (let TMP_80 \def (weight_map TMP_79 t) in +(let TMP_81 \def (le_plus_l TMP_77 TMP_80) in (le_n_S TMP_69 TMP_75 +TMP_81))))))))))))))))) in (B_ind TMP_31 TMP_52 TMP_67 TMP_82 b)))))) in (let +TMP_96 \def (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(let TMP_84 \def +(\lambda (_: nat).O) in (let TMP_85 \def (weight_map TMP_84 u) in (let TMP_86 +\def (\lambda (_: nat).O) in (let TMP_87 \def (weight_map TMP_86 u) in (let +TMP_88 \def (\lambda (_: nat).O) in (let TMP_89 \def (weight_map TMP_88 t) in +(let TMP_90 \def (plus TMP_87 TMP_89) in (let TMP_91 \def (\lambda (_: +nat).O) in (let TMP_92 \def (weight_map TMP_91 u) in (let TMP_93 \def +(\lambda (_: nat).O) in (let TMP_94 \def (weight_map TMP_93 t) in (let TMP_95 +\def (le_plus_l TMP_92 TMP_94) in (le_n_S TMP_85 TMP_90 +TMP_95)))))))))))))))) in (K_ind TMP_6 TMP_83 TMP_96 k)))). theorem tlt_head_dx: \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t)))) \def - \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt -(weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead -k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall -(t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr -\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd -(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst -\Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd -(\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda -(_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda -(u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S -(weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_: -nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: -nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S -(weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) -(weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) -u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd -(\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus -(weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S -(weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd -(\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda -(_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t -(weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t) -(weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map -(wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))))))) -(\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_: -nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus -(weight_map (\lambda (_: nat).O) u) n)))) (le_n_S (weight_map (\lambda (_: -nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: -nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map -(\lambda (_: nat).O) t))) (weight_map (wadd (\lambda (_: nat).O) O) t) -(weight_add_O t)))) (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map -(\lambda (_: nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: -nat).O) t) (S (plus (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S -(weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) -(weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_: -nat).O) u) (weight_map (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda -(_: nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u: -T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus -(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)) -(le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: -nat).O) t)))))) k). -(* COMMENTS -Initial nodes: 659 -END *) - -theorem tlt_wf__q_ind: - \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to -Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0 -t))))) P n))) \to (\forall (t: T).(P t))) -\def - let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t: -T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to -Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t) -n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight -t)))))). -(* COMMENTS -Initial nodes: 61 -END *) + \lambda (k: K).(let TMP_6 \def (\lambda (k0: K).(\forall (u: T).(\forall (t: +T).(let TMP_1 \def (\lambda (_: nat).O) in (let TMP_2 \def (weight_map TMP_1 +t) in (let TMP_3 \def (\lambda (_: nat).O) in (let TMP_4 \def (THead k0 u t) +in (let TMP_5 \def (weight_map TMP_3 TMP_4) in (lt TMP_2 TMP_5))))))))) in +(let TMP_161 \def (\lambda (b: B).(let TMP_31 \def (\lambda (b0: B).(\forall +(u: T).(\forall (t: T).(let TMP_7 \def (\lambda (_: nat).O) in (let TMP_8 +\def (weight_map TMP_7 t) in (let TMP_30 \def (match b0 with [Abbr +\Rightarrow (let TMP_21 \def (\lambda (_: nat).O) in (let TMP_22 \def +(weight_map TMP_21 u) in (let TMP_23 \def (\lambda (_: nat).O) in (let TMP_24 +\def (\lambda (_: nat).O) in (let TMP_25 \def (weight_map TMP_24 u) in (let +TMP_26 \def (S TMP_25) in (let TMP_27 \def (wadd TMP_23 TMP_26) in (let +TMP_28 \def (weight_map TMP_27 t) in (let TMP_29 \def (plus TMP_22 TMP_28) in +(S TMP_29)))))))))) | Abst \Rightarrow (let TMP_15 \def (\lambda (_: nat).O) +in (let TMP_16 \def (weight_map TMP_15 u) in (let TMP_17 \def (\lambda (_: +nat).O) in (let TMP_18 \def (wadd TMP_17 O) in (let TMP_19 \def (weight_map +TMP_18 t) in (let TMP_20 \def (plus TMP_16 TMP_19) in (S TMP_20))))))) | Void +\Rightarrow (let TMP_9 \def (\lambda (_: nat).O) in (let TMP_10 \def +(weight_map TMP_9 u) in (let TMP_11 \def (\lambda (_: nat).O) in (let TMP_12 +\def (wadd TMP_11 O) in (let TMP_13 \def (weight_map TMP_12 t) in (let TMP_14 +\def (plus TMP_10 TMP_13) in (S TMP_14)))))))]) in (lt TMP_8 TMP_30))))))) in +(let TMP_106 \def (\lambda (u: T).(\lambda (t: T).(let TMP_32 \def (\lambda +(_: nat).O) in (let TMP_33 \def (weight_map TMP_32 t) in (let TMP_34 \def +(\lambda (_: nat).O) in (let TMP_35 \def (weight_map TMP_34 t) in (let TMP_36 +\def (S TMP_35) in (let TMP_37 \def (\lambda (_: nat).O) in (let TMP_38 \def +(weight_map TMP_37 u) in (let TMP_39 \def (\lambda (_: nat).O) in (let TMP_40 +\def (\lambda (_: nat).O) in (let TMP_41 \def (weight_map TMP_40 u) in (let +TMP_42 \def (S TMP_41) in (let TMP_43 \def (wadd TMP_39 TMP_42) in (let +TMP_44 \def (weight_map TMP_43 t) in (let TMP_45 \def (plus TMP_38 TMP_44) in +(let TMP_46 \def (S TMP_45) in (let TMP_47 \def (\lambda (_: nat).O) in (let +TMP_48 \def (weight_map TMP_47 t) in (let TMP_49 \def (lt_n_Sn TMP_48) in +(let TMP_50 \def (\lambda (_: nat).O) in (let TMP_51 \def (weight_map TMP_50 +t) in (let TMP_52 \def (\lambda (_: nat).O) in (let TMP_53 \def (weight_map +TMP_52 u) in (let TMP_54 \def (\lambda (_: nat).O) in (let TMP_55 \def +(\lambda (_: nat).O) in (let TMP_56 \def (weight_map TMP_55 u) in (let TMP_57 +\def (S TMP_56) in (let TMP_58 \def (wadd TMP_54 TMP_57) in (let TMP_59 \def +(weight_map TMP_58 t) in (let TMP_60 \def (plus TMP_53 TMP_59) in (let TMP_61 +\def (\lambda (_: nat).O) in (let TMP_62 \def (weight_map TMP_61 t) in (let +TMP_63 \def (\lambda (_: nat).O) in (let TMP_64 \def (\lambda (_: nat).O) in +(let TMP_65 \def (weight_map TMP_64 u) in (let TMP_66 \def (S TMP_65) in (let +TMP_67 \def (wadd TMP_63 TMP_66) in (let TMP_68 \def (weight_map TMP_67 t) in +(let TMP_69 \def (\lambda (_: nat).O) in (let TMP_70 \def (weight_map TMP_69 +u) in (let TMP_71 \def (\lambda (_: nat).O) in (let TMP_72 \def (\lambda (_: +nat).O) in (let TMP_73 \def (weight_map TMP_72 u) in (let TMP_74 \def (S +TMP_73) in (let TMP_75 \def (wadd TMP_71 TMP_74) in (let TMP_76 \def +(weight_map TMP_75 t) in (let TMP_77 \def (plus TMP_70 TMP_76) in (let TMP_78 +\def (\lambda (_: nat).O) in (let TMP_79 \def (wadd TMP_78 O) in (let TMP_80 +\def (weight_map TMP_79 t) in (let TMP_87 \def (\lambda (n: nat).(let TMP_81 +\def (\lambda (_: nat).O) in (let TMP_82 \def (\lambda (_: nat).O) in (let +TMP_83 \def (weight_map TMP_82 u) in (let TMP_84 \def (S TMP_83) in (let +TMP_85 \def (wadd TMP_81 TMP_84) in (let TMP_86 \def (weight_map TMP_85 t) in +(le n TMP_86)))))))) in (let TMP_88 \def (\lambda (_: nat).O) in (let TMP_89 +\def (weight_map TMP_88 u) in (let TMP_90 \def (weight_add_S t TMP_89) in +(let TMP_91 \def (\lambda (_: nat).O) in (let TMP_92 \def (weight_map TMP_91 +t) in (let TMP_93 \def (weight_add_O t) in (let TMP_94 \def (eq_ind nat +TMP_80 TMP_87 TMP_90 TMP_92 TMP_93) in (let TMP_95 \def (\lambda (_: nat).O) +in (let TMP_96 \def (weight_map TMP_95 u) in (let TMP_97 \def (\lambda (_: +nat).O) in (let TMP_98 \def (\lambda (_: nat).O) in (let TMP_99 \def +(weight_map TMP_98 u) in (let TMP_100 \def (S TMP_99) in (let TMP_101 \def +(wadd TMP_97 TMP_100) in (let TMP_102 \def (weight_map TMP_101 t) in (let +TMP_103 \def (le_plus_r TMP_96 TMP_102) in (let TMP_104 \def (le_trans TMP_62 +TMP_68 TMP_77 TMP_94 TMP_103) in (let TMP_105 \def (le_n_S TMP_51 TMP_60 +TMP_104) in (lt_le_trans TMP_33 TMP_36 TMP_46 TMP_49 +TMP_105))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + in (let TMP_133 \def (\lambda (u: T).(\lambda (t: T).(let TMP_107 \def +(\lambda (_: nat).O) in (let TMP_108 \def (weight_map TMP_107 t) in (let +TMP_115 \def (\lambda (n: nat).(let TMP_109 \def (\lambda (_: nat).O) in (let +TMP_110 \def (weight_map TMP_109 t) in (let TMP_111 \def (\lambda (_: nat).O) +in (let TMP_112 \def (weight_map TMP_111 u) in (let TMP_113 \def (plus +TMP_112 n) in (let TMP_114 \def (S TMP_113) in (lt TMP_110 TMP_114)))))))) in +(let TMP_116 \def (\lambda (_: nat).O) in (let TMP_117 \def (weight_map +TMP_116 t) in (let TMP_118 \def (\lambda (_: nat).O) in (let TMP_119 \def +(weight_map TMP_118 u) in (let TMP_120 \def (\lambda (_: nat).O) in (let +TMP_121 \def (weight_map TMP_120 t) in (let TMP_122 \def (plus TMP_119 +TMP_121) in (let TMP_123 \def (\lambda (_: nat).O) in (let TMP_124 \def +(weight_map TMP_123 u) in (let TMP_125 \def (\lambda (_: nat).O) in (let +TMP_126 \def (weight_map TMP_125 t) in (let TMP_127 \def (le_plus_r TMP_124 +TMP_126) in (let TMP_128 \def (le_n_S TMP_117 TMP_122 TMP_127) in (let +TMP_129 \def (\lambda (_: nat).O) in (let TMP_130 \def (wadd TMP_129 O) in +(let TMP_131 \def (weight_map TMP_130 t) in (let TMP_132 \def (weight_add_O +t) in (eq_ind_r nat TMP_108 TMP_115 TMP_128 TMP_131 +TMP_132))))))))))))))))))))))) in (let TMP_160 \def (\lambda (u: T).(\lambda +(t: T).(let TMP_134 \def (\lambda (_: nat).O) in (let TMP_135 \def +(weight_map TMP_134 t) in (let TMP_142 \def (\lambda (n: nat).(let TMP_136 +\def (\lambda (_: nat).O) in (let TMP_137 \def (weight_map TMP_136 t) in (let +TMP_138 \def (\lambda (_: nat).O) in (let TMP_139 \def (weight_map TMP_138 u) +in (let TMP_140 \def (plus TMP_139 n) in (let TMP_141 \def (S TMP_140) in (lt +TMP_137 TMP_141)))))))) in (let TMP_143 \def (\lambda (_: nat).O) in (let +TMP_144 \def (weight_map TMP_143 t) in (let TMP_145 \def (\lambda (_: nat).O) +in (let TMP_146 \def (weight_map TMP_145 u) in (let TMP_147 \def (\lambda (_: +nat).O) in (let TMP_148 \def (weight_map TMP_147 t) in (let TMP_149 \def +(plus TMP_146 TMP_148) in (let TMP_150 \def (\lambda (_: nat).O) in (let +TMP_151 \def (weight_map TMP_150 u) in (let TMP_152 \def (\lambda (_: nat).O) +in (let TMP_153 \def (weight_map TMP_152 t) in (let TMP_154 \def (le_plus_r +TMP_151 TMP_153) in (let TMP_155 \def (le_n_S TMP_144 TMP_149 TMP_154) in +(let TMP_156 \def (\lambda (_: nat).O) in (let TMP_157 \def (wadd TMP_156 O) +in (let TMP_158 \def (weight_map TMP_157 t) in (let TMP_159 \def +(weight_add_O t) in (eq_ind_r nat TMP_135 TMP_142 TMP_155 TMP_158 +TMP_159))))))))))))))))))))))) in (B_ind TMP_31 TMP_106 TMP_133 TMP_160 +b)))))) in (let TMP_174 \def (\lambda (_: F).(\lambda (u: T).(\lambda (t: +T).(let TMP_162 \def (\lambda (_: nat).O) in (let TMP_163 \def (weight_map +TMP_162 t) in (let TMP_164 \def (\lambda (_: nat).O) in (let TMP_165 \def +(weight_map TMP_164 u) in (let TMP_166 \def (\lambda (_: nat).O) in (let +TMP_167 \def (weight_map TMP_166 t) in (let TMP_168 \def (plus TMP_165 +TMP_167) in (let TMP_169 \def (\lambda (_: nat).O) in (let TMP_170 \def +(weight_map TMP_169 u) in (let TMP_171 \def (\lambda (_: nat).O) in (let +TMP_172 \def (weight_map TMP_171 t) in (let TMP_173 \def (le_plus_r TMP_170 +TMP_172) in (le_n_S TMP_163 TMP_168 TMP_173)))))))))))))))) in (K_ind TMP_6 +TMP_161 TMP_174 k)))). -theorem tlt_wf_ind: - \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t) -\to (P v)))) \to (P t)))) \to (\forall (t: T).(P t))) +theorem tle_r: + \forall (t: T).(tle t t) \def - let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t: -T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to -Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v) -(weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind -(\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0: -T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0) -\to (Q (\lambda (t0: T).(P t0)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat -(weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1: nat).(\forall -(m: nat).((lt m n1) \to (\forall (t1: T).((eq nat (weight t1) m) \to (P -t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt -(weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight -v))))))))))))) t)))). -(* COMMENTS -Initial nodes: 179 -END *) + \lambda (t: T).(let TMP_3 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0) +in (let TMP_2 \def (tweight t0) in (le TMP_1 TMP_2)))) in (let TMP_5 \def +(\lambda (_: nat).(let TMP_4 \def (S O) in (le_n TMP_4))) in (let TMP_7 \def +(\lambda (_: nat).(let TMP_6 \def (S O) in (le_n TMP_6))) in (let TMP_12 \def +(\lambda (_: K).(\lambda (t0: T).(\lambda (_: (le (tweight t0) (tweight +t0))).(\lambda (t1: T).(\lambda (_: (le (tweight t1) (tweight t1))).(let +TMP_8 \def (tweight t0) in (let TMP_9 \def (tweight t1) in (let TMP_10 \def +(plus TMP_8 TMP_9) in (let TMP_11 \def (S TMP_10) in (le_n TMP_11)))))))))) +in (T_ind TMP_3 TMP_5 TMP_7 TMP_12 t))))). diff --git a/matita/matita/matitac.ml b/matita/matita/matitac.ml index a93d694dc..d0f5603e5 100644 --- a/matita/matita/matitac.ml +++ b/matita/matita/matitac.ml @@ -44,7 +44,14 @@ let main_compiler () = prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots); prerr_endline ("\nEnter one of these directories and retry"); exit 1); - | _ -> targets + | _ -> + let map targets file = + if HExtlib.is_dir file then + let files = HExtlib.find ~test:(fun path -> Filename.check_suffix path ".ma") file in + files @ targets + else file :: targets + in + List.fold_left map [] (List.rev targets) in (* must be called after init since args are set by cmdline parsing *) let system_mode = Helm_registry.get_bool "matita.system" in