1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1/flt/defs.ma".
19 include "basic_1/C/props.ma".
22 \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c u c
25 \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1
26 \def (tweight u) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight
27 t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (S TMP_4) in (let
28 TMP_6 \def (cweight c) in (let TMP_7 \def (tweight u) in (let TMP_8 \def
29 (tweight u) in (let TMP_9 \def (tweight t) in (let TMP_10 \def (plus TMP_8
30 TMP_9) in (let TMP_11 \def (tweight u) in (let TMP_12 \def (tweight t) in
31 (let TMP_13 \def (le_plus_l TMP_11 TMP_12) in (let TMP_14 \def (le_n_S TMP_7
32 TMP_10 TMP_13) in (lt_reg_l TMP_1 TMP_5 TMP_6 TMP_14)))))))))))))))))).
35 \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt c t c
38 \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1
39 \def (tweight t) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight
40 t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (S TMP_4) in (let
41 TMP_6 \def (cweight c) in (let TMP_7 \def (tweight t) in (let TMP_8 \def
42 (tweight u) in (let TMP_9 \def (tweight t) in (let TMP_10 \def (plus TMP_8
43 TMP_9) in (let TMP_11 \def (tweight u) in (let TMP_12 \def (tweight t) in
44 (let TMP_13 \def (le_plus_r TMP_11 TMP_12) in (let TMP_14 \def (le_n_S TMP_7
45 TMP_10 TMP_13) in (lt_reg_l TMP_1 TMP_5 TMP_6 TMP_14)))))))))))))))))).
48 \forall (k: K).(\forall (c: C).(\forall (u: T).(\forall (t: T).(flt (CHead c
49 k u) t c (THead k u t)))))
51 \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1
52 \def (cweight c) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight
53 t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (plus TMP_1
54 TMP_4) in (let TMP_6 \def (S TMP_5) in (let TMP_12 \def (\lambda (n:
55 nat).(let TMP_7 \def (cweight c) in (let TMP_8 \def (tweight u) in (let TMP_9
56 \def (plus TMP_7 TMP_8) in (let TMP_10 \def (tweight t) in (let TMP_11 \def
57 (plus TMP_9 TMP_10) in (lt TMP_11 n))))))) in (let TMP_13 \def (cweight c) in
58 (let TMP_14 \def (tweight u) in (let TMP_15 \def (plus TMP_13 TMP_14) in (let
59 TMP_16 \def (tweight t) in (let TMP_17 \def (plus TMP_15 TMP_16) in (let
60 TMP_24 \def (\lambda (n: nat).(let TMP_18 \def (cweight c) in (let TMP_19
61 \def (tweight u) in (let TMP_20 \def (plus TMP_18 TMP_19) in (let TMP_21 \def
62 (tweight t) in (let TMP_22 \def (plus TMP_20 TMP_21) in (let TMP_23 \def (S
63 n) in (lt TMP_22 TMP_23)))))))) in (let TMP_25 \def (cweight c) in (let
64 TMP_26 \def (tweight u) in (let TMP_27 \def (plus TMP_25 TMP_26) in (let
65 TMP_28 \def (tweight t) in (let TMP_29 \def (plus TMP_27 TMP_28) in (let
66 TMP_30 \def (S TMP_29) in (let TMP_31 \def (le_n TMP_30) in (let TMP_32 \def
67 (cweight c) in (let TMP_33 \def (tweight u) in (let TMP_34 \def (tweight t)
68 in (let TMP_35 \def (plus TMP_33 TMP_34) in (let TMP_36 \def (plus TMP_32
69 TMP_35) in (let TMP_37 \def (cweight c) in (let TMP_38 \def (tweight u) in
70 (let TMP_39 \def (tweight t) in (let TMP_40 \def (plus_assoc_l TMP_37 TMP_38
71 TMP_39) in (let TMP_41 \def (eq_ind_r nat TMP_17 TMP_24 TMP_31 TMP_36 TMP_40)
72 in (let TMP_42 \def (cweight c) in (let TMP_43 \def (tweight u) in (let
73 TMP_44 \def (tweight t) in (let TMP_45 \def (plus TMP_43 TMP_44) in (let
74 TMP_46 \def (S TMP_45) in (let TMP_47 \def (plus TMP_42 TMP_46) in (let
75 TMP_48 \def (cweight c) in (let TMP_49 \def (tweight u) in (let TMP_50 \def
76 (tweight t) in (let TMP_51 \def (plus TMP_49 TMP_50) in (let TMP_52 \def
77 (plus_n_Sm TMP_48 TMP_51) in (eq_ind nat TMP_6 TMP_12 TMP_41 TMP_47
78 TMP_52))))))))))))))))))))))))))))))))))))))))))))).
81 \forall (k: K).(\forall (c: C).(\forall (t: T).(\forall (i: nat).(flt c t
82 (CHead c k t) (TLRef i)))))
84 \lambda (_: K).(\lambda (c: C).(\lambda (t: T).(\lambda (_: nat).(let TMP_1
85 \def (cweight c) in (let TMP_2 \def (tweight t) in (let TMP_3 \def (plus
86 TMP_1 TMP_2) in (lt_x_plus_x_Sy TMP_3 O))))))).
89 \forall (k1: K).(\forall (c1: C).(\forall (c2: C).(\forall (t1: T).((cle
90 (CHead c1 k1 t1) c2) \to (\forall (k2: K).(\forall (t2: T).(\forall (i:
91 nat).(flt c1 t1 (CHead c2 k2 t2) (TLRef i)))))))))
93 \lambda (_: K).(\lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda
94 (H: (le (plus (cweight c1) (tweight t1)) (cweight c2))).(\lambda (_:
95 K).(\lambda (t2: T).(\lambda (_: nat).(let TMP_1 \def (cweight c1) in (let
96 TMP_2 \def (tweight t1) in (let TMP_3 \def (plus TMP_1 TMP_2) in (let TMP_4
97 \def (cweight c2) in (let TMP_5 \def (cweight c2) in (let TMP_6 \def (tweight
98 t2) in (let TMP_7 \def (plus TMP_5 TMP_6) in (let TMP_8 \def (S O) in (let
99 TMP_9 \def (plus TMP_7 TMP_8) in (let TMP_10 \def (S O) in (let TMP_11 \def
100 (cweight c2) in (let TMP_12 \def (tweight t2) in (let TMP_13 \def (plus
101 TMP_11 TMP_12) in (let TMP_14 \def (plus TMP_10 TMP_13) in (let TMP_16 \def
102 (\lambda (n: nat).(let TMP_15 \def (cweight c2) in (lt TMP_15 n))) in (let
103 TMP_17 \def (cweight c2) in (let TMP_18 \def (cweight c2) in (let TMP_19 \def
104 (tweight t2) in (let TMP_20 \def (plus TMP_18 TMP_19) in (let TMP_21 \def
105 (cweight c2) in (let TMP_22 \def (tweight t2) in (let TMP_23 \def (le_plus_l
106 TMP_21 TMP_22) in (let TMP_24 \def (le_lt_n_Sm TMP_17 TMP_20 TMP_23) in (let
107 TMP_25 \def (cweight c2) in (let TMP_26 \def (tweight t2) in (let TMP_27 \def
108 (plus TMP_25 TMP_26) in (let TMP_28 \def (S O) in (let TMP_29 \def (plus
109 TMP_27 TMP_28) in (let TMP_30 \def (cweight c2) in (let TMP_31 \def (tweight
110 t2) in (let TMP_32 \def (plus TMP_30 TMP_31) in (let TMP_33 \def (S O) in
111 (let TMP_34 \def (plus_sym TMP_32 TMP_33) in (let TMP_35 \def (eq_ind_r nat
112 TMP_14 TMP_16 TMP_24 TMP_29 TMP_34) in (le_lt_trans TMP_3 TMP_4 TMP_9 H
113 TMP_35)))))))))))))))))))))))))))))))))))))))))).
116 \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (i: nat).((flt c1
117 t1 c2 (TLRef i)) \to (\forall (k2: K).(\forall (t2: T).(\forall (j: nat).(flt
118 c1 t1 (CHead c2 k2 t2) (TLRef j)))))))))
120 \lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (_: nat).(\lambda
121 (H: (lt (plus (cweight c1) (tweight t1)) (plus (cweight c2) (S O)))).(\lambda
122 (_: K).(\lambda (t2: T).(\lambda (_: nat).(let TMP_1 \def (cweight c1) in
123 (let TMP_2 \def (tweight t1) in (let TMP_3 \def (plus TMP_1 TMP_2) in (let
124 TMP_4 \def (cweight c2) in (let TMP_5 \def (S O) in (let TMP_6 \def (plus
125 TMP_4 TMP_5) in (let TMP_7 \def (cweight c2) in (let TMP_8 \def (tweight t2)
126 in (let TMP_9 \def (plus TMP_7 TMP_8) in (let TMP_10 \def (S O) in (let
127 TMP_11 \def (plus TMP_9 TMP_10) in (let TMP_12 \def (cweight c2) in (let
128 TMP_13 \def (cweight c2) in (let TMP_14 \def (tweight t2) in (let TMP_15 \def
129 (plus TMP_13 TMP_14) in (let TMP_16 \def (S O) in (let TMP_17 \def (S O) in
130 (let TMP_18 \def (cweight c2) in (let TMP_19 \def (tweight t2) in (let TMP_20
131 \def (le_plus_l TMP_18 TMP_19) in (let TMP_21 \def (S O) in (let TMP_22 \def
132 (le_n TMP_21) in (let TMP_23 \def (le_plus_plus TMP_12 TMP_15 TMP_16 TMP_17
133 TMP_20 TMP_22) in (lt_le_trans TMP_3 TMP_6 TMP_11 H
134 TMP_23))))))))))))))))))))))))))))))).
136 theorem cle_flt_trans:
137 \forall (c1: C).(\forall (c2: C).((cle c1 c2) \to (\forall (c3: C).(\forall
138 (u2: T).(\forall (u3: T).((flt c2 u2 c3 u3) \to (flt c1 u2 c3 u3)))))))
140 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (le (cweight c1) (cweight
141 c2))).(\lambda (c3: C).(\lambda (u2: T).(\lambda (u3: T).(\lambda (H0: (lt
142 (plus (cweight c2) (tweight u2)) (plus (cweight c3) (tweight u3)))).(let
143 TMP_1 \def (cweight c1) in (let TMP_2 \def (tweight u2) in (let TMP_3 \def
144 (plus TMP_1 TMP_2) in (let TMP_4 \def (cweight c2) in (let TMP_5 \def
145 (tweight u2) in (let TMP_6 \def (plus TMP_4 TMP_5) in (let TMP_7 \def
146 (cweight c3) in (let TMP_8 \def (tweight u3) in (let TMP_9 \def (plus TMP_7
147 TMP_8) in (let TMP_10 \def (cweight c1) in (let TMP_11 \def (cweight c2) in
148 (let TMP_12 \def (tweight u2) in (let TMP_13 \def (tweight u2) in (let TMP_14
149 \def (tweight u2) in (let TMP_15 \def (le_n TMP_14) in (let TMP_16 \def
150 (le_plus_plus TMP_10 TMP_11 TMP_12 TMP_13 H TMP_15) in (le_lt_trans TMP_3
151 TMP_6 TMP_9 TMP_16 H0))))))))))))))))))))))).
154 \forall (c1: C).(\forall (c2: C).(\forall (t1: T).(\forall (t2: T).((flt c1
155 t1 c2 t2) \to (\forall (c3: C).(\forall (t3: T).((flt c2 t2 c3 t3) \to (flt
158 \lambda (c1: C).(\lambda (c2: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
159 (H: (lt (fweight c1 t1) (fweight c2 t2))).(\lambda (c3: C).(\lambda (t3:
160 T).(\lambda (H0: (lt (fweight c2 t2) (fweight c3 t3))).(let TMP_1 \def
161 (fweight c1 t1) in (let TMP_2 \def (fweight c2 t2) in (let TMP_3 \def
162 (fweight c3 t3) in (lt_trans TMP_1 TMP_2 TMP_3 H H0))))))))))).