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 in
23 B 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_2 \def (\lambda (ee: B).(match ee in
31 B with [Abbr \Rightarrow False | Abst \Rightarrow False | Void \Rightarrow
32 True])) in (let H0 \def (eq_ind B Void TMP_2 I Abst H) in (False_ind False
35 theorem not_abbr_void:
38 \lambda (H: (eq B Abbr Void)).(let TMP_3 \def (\lambda (ee: B).(match ee in
39 B with [Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow
40 False])) in (let H0 \def (eq_ind B Abbr TMP_3 I Void H) in (False_ind False
43 theorem not_abst_void:
46 \lambda (H: (eq B Abst Void)).(let TMP_4 \def (\lambda (ee: B).(match ee in
47 B with [Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow
48 False])) in (let H0 \def (eq_ind B Abst TMP_4 I Void H) in (False_ind False
52 \forall (t: T).(lt O (tweight t))
54 \lambda (t: T).(let TMP_1848 \def (\lambda (t0: T).(let TMP_1847 \def
55 (tweight t0) in (lt O TMP_1847))) in (let TMP_1846 \def (\lambda (_:
56 nat).(let TMP_1845 \def (S O) in (le_n TMP_1845))) in (let TMP_1844 \def
57 (\lambda (_: nat).(let TMP_1843 \def (S O) in (le_n TMP_1843))) in (let
58 TMP_1842 \def (\lambda (_: K).(\lambda (t0: T).(\lambda (H: (lt O (tweight
59 t0))).(\lambda (t1: T).(\lambda (_: (lt O (tweight t1))).(let TMP_1841 \def
60 (S O) in (let TMP_1839 \def (tweight t0) in (let TMP_1838 \def (tweight t1)
61 in (let TMP_1840 \def (plus TMP_1839 TMP_1838) in (let TMP_1836 \def (S O) in
62 (let TMP_1835 \def (tweight t0) in (let TMP_1834 \def (tweight t1) in (let
63 TMP_1837 \def (le_plus_trans TMP_1836 TMP_1835 TMP_1834 H) in (le_S TMP_1841
64 TMP_1840 TMP_1837)))))))))))))) in (T_ind TMP_1848 TMP_1846 TMP_1844 TMP_1842