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/T/fwd.ma".
19 theorem not_abbr_abst:
22 \lambda (H: (eq B Abbr Abst)).(let TMP_1 \def (\lambda (ee: B).(match ee
23 with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow
24 False])) in (let H0 \def (eq_ind B Abbr TMP_1 I Abst H) in (False_ind False
27 theorem not_void_abst:
30 \lambda (H: (eq B Void Abst)).(let TMP_1 \def (\lambda (ee: B).(match ee
31 with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow
32 True])) in (let H0 \def (eq_ind B Void TMP_1 I Abst H) in (False_ind False
35 theorem not_abbr_void:
38 \lambda (H: (eq B Abbr Void)).(let TMP_1 \def (\lambda (ee: B).(match ee
39 with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow
40 False])) in (let H0 \def (eq_ind B Abbr TMP_1 I Void H) in (False_ind False
43 theorem not_abst_void:
46 \lambda (H: (eq B Abst Void)).(let TMP_1 \def (\lambda (ee: B).(match ee
47 with [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow
48 False])) in (let H0 \def (eq_ind B Abst TMP_1 I Void H) in (False_ind False
52 \forall (t: T).(lt O (tweight t))
54 \lambda (t: T).(let TMP_2 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0)
55 in (lt O TMP_1))) in (let TMP_4 \def (\lambda (_: nat).(let TMP_3 \def (S O)
56 in (le_n TMP_3))) in (let TMP_6 \def (\lambda (_: nat).(let TMP_5 \def (S O)
57 in (le_n TMP_5))) in (let TMP_15 \def (\lambda (_: K).(\lambda (t0:
58 T).(\lambda (H: (lt O (tweight t0))).(\lambda (t1: T).(\lambda (_: (lt O
59 (tweight t1))).(let TMP_7 \def (S O) in (let TMP_8 \def (tweight t0) in (let
60 TMP_9 \def (tweight t1) in (let TMP_10 \def (plus TMP_8 TMP_9) in (let TMP_11
61 \def (S O) in (let TMP_12 \def (tweight t0) in (let TMP_13 \def (tweight t1)
62 in (let TMP_14 \def (le_plus_trans TMP_11 TMP_12 TMP_13 H) in (le_S TMP_7
63 TMP_10 TMP_14)))))))))))))) in (T_ind TMP_2 TMP_4 TMP_6 TMP_15 t))))).
66 \forall (t: T).(tle t t)
68 \lambda (t: T).(let TMP_3 \def (\lambda (t0: T).(let TMP_1 \def (tweight t0)
69 in (let TMP_2 \def (tweight t0) in (le TMP_1 TMP_2)))) in (let TMP_5 \def
70 (\lambda (_: nat).(let TMP_4 \def (S O) in (le_n TMP_4))) in (let TMP_7 \def
71 (\lambda (_: nat).(let TMP_6 \def (S O) in (le_n TMP_6))) in (let TMP_12 \def
72 (\lambda (_: K).(\lambda (t0: T).(\lambda (_: (le (tweight t0) (tweight
73 t0))).(\lambda (t1: T).(\lambda (_: (le (tweight t1) (tweight t1))).(let
74 TMP_8 \def (tweight t0) in (let TMP_9 \def (tweight t1) in (let TMP_10 \def
75 (plus TMP_8 TMP_9) in (let TMP_11 \def (S TMP_10) in (le_n TMP_11))))))))))
76 in (T_ind TMP_3 TMP_5 TMP_7 TMP_12 t))))).